Merge pull request #4342 from tautschnig/cleanup-add_object

Simplify the interface to goto_symex_statet::add_object

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -773,14 +773,16 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
   }
 }
 
-void goto_symex_statet::add_object(
-  ssa_exprt &ssa,
-  std::size_t l1_index,
+ssa_exprt goto_symex_statet::add_object(
+  const symbol_exprt &expr,
+  std::function<std::size_t(const irep_idt &)> index_generator,
   const namespacet &ns)
 {
   framet &frame = call_stack().top();
 
+  ssa_exprt ssa = rename_ssa<L0>(ssa_exprt{expr}, ns);
   const irep_idt l0_name = ssa.get_identifier();
+  const std::size_t l1_index = index_generator(l0_name);
 
   // save old L1 name, if any
   auto existing_or_new_entry = level1.current_names.emplace(
@@ -797,4 +799,6 @@ void goto_symex_statet::add_object(
   ssa = rename_ssa<L1>(std::move(ssa), ns);
   const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second;
   INVARIANT(inserted, "l1_name expected to be unique by construction");
+
+  return ssa;
 }

src/goto-symex/goto_symex_state.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
 
+#include <functional>
 #include <memory>
 #include <unordered_set>
 
@@ -140,10 +141,16 @@ class goto_symex_statet final : public goto_statet
     return threads[source.thread_nr].call_stack;
   }
 
-  /// Create a new instance of the L0-renamed object \p ssa. As part of this,
-  /// turn \p ssa into an L1-renamed SSA expression. When doing so, use
-  /// \p l1_index as the L1 index, which must not previously have been used.
-  void add_object(ssa_exprt &ssa, std::size_t l1_index, const namespacet &ns);
+  /// Instantiate the object \p expr. An instance of an object is an L1-renamed
+  /// SSA expression such that its L1-index has not previously been used.
+  /// \param expr: Symbol to be instantiated
+  /// \param index_generator: A function to produce a new index for a given name
+  /// \param ns: A namespace
+  /// \return L1-renamed SSA expression
+  ssa_exprt add_object(
+    const symbol_exprt &expr,
+    std::function<std::size_t(const irep_idt &)> index_generator,
+    const namespacet &ns);
 
   void print_backtrace(std::ostream &) const;
 

src/goto-symex/symex_decl.cpp

@@ -37,13 +37,15 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   // each declaration introduces a new object, which we record as a fresh L1
   // index
 
-  ssa_exprt ssa = state.rename_ssa<L0>(ssa_exprt{expr}, ns);
   // We use "1" as the first level-1 index, which is in line with doing so for
   // level-2 indices (but it's an arbitrary choice, we have just always been
   // doing it this way).
-  const std::size_t fresh_l1_index =
-    path_storage.get_unique_index(ssa.get_identifier(), 1);
-  state.add_object(ssa, fresh_l1_index, ns);
+  ssa_exprt ssa = state.add_object(
+    expr,
+    [this](const irep_idt &l0_name) {
+      return path_storage.get_unique_index(l0_name, 1);
+    },
+    ns);
   const irep_idt &l1_identifier = ssa.get_identifier();
 
   // rename type to L2

src/goto-symex/symex_function_call.cpp

@@ -399,12 +399,11 @@ static void locality(
 
   for(const auto &param : goto_function.parameter_identifiers)
   {
-    // get L0 name
-    ssa_exprt ssa =
-      state.rename_ssa<L0>(ssa_exprt{ns.lookup(param).symbol_expr()}, ns);
-
-    const std::size_t fresh_l1_index =
-      path_storage.get_unique_index(ssa.get_identifier(), frame_nr);
-    state.add_object(ssa, fresh_l1_index, ns);
+    (void)state.add_object(
+      ns.lookup(param).symbol_expr(),
+      [&path_storage, &frame_nr](const irep_idt &l0_name) {
+        return path_storage.get_unique_index(l0_name, frame_nr);
+      },
+      ns);
   }
 }