Enable merge_ireps for goto traces

A goto trace includes freshly constructed expressions, which thus lack
sharing. This results in excessive memory use when storing multiple
traces, as is done for coverage computation. On a particular benchmark,
coverage computation previously ran out of memory at 768 GB. This same
benchmark can now be run with just 80 GB of memory.

Author: tautschnig

src/goto-checker/goto_trace_storage.cpp

@@ -27,6 +27,10 @@ const goto_tracet &goto_trace_storaget::insert(goto_tracet &&trace)
     emplace_result.second,
     "cannot associate more than one error trace with property " +
       id2string(last_step.property_id));
+
+  for(auto &step : traces.back().steps)
+    step.merge_ireps(merge_ireps);
+
   return traces.back();
 }
 
@@ -40,6 +44,10 @@ const goto_tracet &goto_trace_storaget::insert_all(goto_tracet &&trace)
   {
     property_id_to_trace_index.emplace(property_id, traces.size() - 1);
   }
+
+  for(auto &step : traces.back().steps)
+    step.merge_ireps(merge_ireps);
+
   return traces.back();
 }
 

src/goto-checker/goto_trace_storage.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-programs/goto_trace.h>
 
+#include <util/merge_irep.h>
+
 #include <list>
 
 class goto_trace_storaget
@@ -44,6 +46,9 @@ class goto_trace_storaget
 
   // maps property ID to index in traces
   std::unordered_map<irep_idt, std::size_t> property_id_to_trace_index;
+
+  /// irep container for shared ireps
+  merge_irept merge_ireps;
 };
 
 #endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H

src/goto-programs/goto_trace.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/format_expr.h>
+#include <util/merge_irep.h>
 #include <util/range.h>
 #include <util/string_utils.h>
 #include <util/symbol.h>
@@ -133,6 +134,20 @@ void goto_trace_stept::output(
 
   out << '\n';
 }
+
+void goto_trace_stept::merge_ireps(merge_irept &dest)
+{
+  dest(cond_expr);
+  dest(full_lhs);
+  dest(full_lhs_value);
+
+  for(auto &io_arg : io_args)
+    dest(io_arg);
+
+  for(auto &function_arg : function_arguments)
+    dest(function_arg);
+}
+
 /// Returns the numeric representation of an expression, based on
 /// options. The default is binary without a base-prefix. Setting
 /// options.hex_representation to be true outputs hex format. Setting

src/goto-programs/goto_trace.h

@@ -24,6 +24,8 @@ Date: July 2005
 
 #include <goto-programs/goto_program.h>
 
+class merge_irept;
+
 /// Step of the trace of a GOTO program
 ///
 /// A step is either:
@@ -162,6 +164,10 @@ class goto_trace_stept
     full_lhs_value.make_nil();
     cond_expr.make_nil();
   }
+
+  /// Use \p dest to establish sharing among ireps.
+  /// \param [out] dest: irep storage container.
+  void merge_ireps(merge_irept &dest);
 };
 
 /// Trace of a GOTO program.