Introduce a renamedt type for renamed expressions in symex

src/goto-instrument/accelerate/scratch_program.cpp

@@ -69,7 +69,7 @@ bool scratch_programt::check_sat(bool do_slice)
 
 exprt scratch_programt::eval(const exprt &e)
 {
-  return checker->get(symex_state->rename<goto_symex_statet::L2>(e, ns));
+  return checker->get(symex_state->rename<L2>(e, ns));
 }
 
 void scratch_programt::append(goto_programt::instructionst &new_instructions)

src/goto-symex/goto_symex_state.cpp

@@ -237,7 +237,9 @@ void goto_symex_statet::set_l0_indices(
   ssa_exprt &ssa_expr,
   const namespacet &ns)
 {
-  level0(ssa_expr, ns, source.thread_nr);
+  renamedt<ssa_exprt, L0> renamed =
+    level0(std::move(ssa_expr), ns, source.thread_nr);
+  ssa_expr = renamed.get();
 }
 
 void goto_symex_statet::set_l1_indices(
@@ -248,8 +250,9 @@ void goto_symex_statet::set_l1_indices(
     return;
   if(!ssa_expr.get_level_1().empty())
     return;
-  level0(ssa_expr, ns, source.thread_nr);
-  level1(ssa_expr);
+  renamedt<ssa_exprt, L1> l1 =
+    level1(level0(std::move(ssa_expr), ns, source.thread_nr));
+  ssa_expr = l1.get();
 }
 
 void goto_symex_statet::set_l2_indices(
@@ -258,12 +261,12 @@ void goto_symex_statet::set_l2_indices(
 {
   if(!ssa_expr.get_level_2().empty())
     return;
-  level0(ssa_expr, ns, source.thread_nr);
-  level1(ssa_expr);
-  ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
+  renamedt<ssa_exprt, L2> l2 =
+    level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
+  ssa_expr = l2.get();
 }
 
-template <goto_symex_statet::levelt level>
+template <levelt level>
 ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
 {
   static_assert(
@@ -282,11 +285,12 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
 }
 
 /// Ensure `rename_ssa` gets compiled for L0
-template ssa_exprt goto_symex_statet::rename_ssa<goto_symex_statet::L0>(
-  ssa_exprt ssa,
-  const namespacet &ns);
+template ssa_exprt
+goto_symex_statet::rename_ssa<L0>(ssa_exprt ssa, const namespacet &ns);
+template ssa_exprt
+goto_symex_statet::rename_ssa<L1>(ssa_exprt ssa, const namespacet &ns);
 
-template <goto_symex_statet::levelt level>
+template <levelt level>
 exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
@@ -367,6 +371,8 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
   return expr;
 }
 
+template exprt goto_symex_statet::rename<L1>(exprt expr, const namespacet &ns);
+
 /// thread encoding
 bool goto_symex_statet::l2_thread_read_encoding(
   ssa_exprt &expr,
@@ -544,7 +550,7 @@ bool goto_symex_statet::l2_thread_write_encoding(
   return threads.size()>1;
 }
 
-template <goto_symex_statet::levelt level>
+template <levelt level>
 void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
 {
   if(expr.id()==ID_symbol &&
@@ -669,7 +675,7 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
   return false;
 }
 
-template <goto_symex_statet::levelt level>
+template <levelt level>
 void goto_symex_statet::rename(
   typet &type,
   const irep_idt &l1_identifier,

src/goto-symex/goto_symex_state.h

@@ -150,9 +150,6 @@ class goto_symex_statet final : public goto_statet
   symex_level0t level0;
   symex_level1t level1;
 
-  // Symex renaming levels.
-  enum levelt { L0=0, L1=1, L2=2 };
-
   /// Rewrites symbol expressions in \ref exprt, applying a suffix to each
   /// symbol reflecting its most recent version, which differs depending on
   /// which level you requested. Each level also updates its predecessors, so

src/goto-symex/renaming_level.cpp

@@ -17,45 +17,54 @@ Author: Romain Brenguier, [email protected]
 
 #include "goto_symex_state.h"
 
-void symex_level0t::
-operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr) const
+renamedt<ssa_exprt, L0> symex_level0t::
+operator()(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) const
 {
   // already renamed?
   if(!ssa_expr.get_level_0().empty())
-    return;
+    return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
 
   const irep_idt &obj_identifier = ssa_expr.get_object_name();
 
   // guards are not L0-renamed
   if(obj_identifier == goto_symex_statet::guard_identifier())
-    return;
+    return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
 
   const symbolt *s;
   const bool found_l0 = !ns.lookup(obj_identifier, s);
   INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
 
   // don't rename shared variables or functions
   if(s->type.id() == ID_code || s->is_shared())
-    return;
+    return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
 
   // rename!
   ssa_expr.set_level_0(thread_nr);
+  return renamedt<ssa_exprt, L0>{ssa_expr};
 }
 
-void symex_level1t::operator()(ssa_exprt &ssa_expr) const
+renamedt<ssa_exprt, L1> symex_level1t::
+operator()(renamedt<ssa_exprt, L0> l0_expr) const
 {
-  // already renamed?
-  if(!ssa_expr.get_level_1().empty())
-    return;
+  if(!l0_expr.get().get_level_1().empty())
+    return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
 
-  const irep_idt l0_name = ssa_expr.get_l1_object_identifier();
+  const irep_idt l0_name = l0_expr.get().get_l1_object_identifier();
 
   const auto it = current_names.find(l0_name);
   if(it == current_names.end())
-    return;
+    return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
 
   // rename!
-  ssa_expr.set_level_1(it->second.second);
+  l0_expr.value.set_level_1(it->second.second);
+  return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
+}
+
+renamedt<ssa_exprt, L2> symex_level2t::
+operator()(renamedt<ssa_exprt, L1> l1_expr) const
+{
+  l1_expr.value.set_level_2(current_count(l1_expr.get().get_identifier()));
+  return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
 }
 
 void symex_level1t::restore_from(

src/goto-symex/renaming_level.h

@@ -18,6 +18,14 @@ Author: Romain Brenguier, [email protected]
 #include <util/irep.h>
 #include <util/ssa_expr.h>
 
+/// Symex renaming level names.
+enum levelt
+{
+  L0 = 0,
+  L1 = 1,
+  L2 = 2
+};
+
 /// Wrapper for a \c current_names map, which maps each identifier to an SSA
 /// expression and a counter.
 /// This is extended by the different symex_level structures which are used
@@ -51,13 +59,44 @@ struct symex_renaming_levelt
   }
 };
 
+/// Wrapper for expressions or types which have been renamed up to a given
+/// \p level
+template <typename underlyingt, levelt level>
+class renamedt
+{
+public:
+  static_assert(
+    std::is_base_of<exprt, underlyingt>::value ||
+      std::is_base_of<typet, underlyingt>::value,
+    "underlyingt should inherit from exprt or typet");
+
+  const underlyingt &get() const
+  {
+    return value;
+  }
+
+private:
+  underlyingt value;
+
+  friend struct symex_level0t;
+  friend struct symex_level1t;
+  friend struct symex_level2t;
+
+  /// Only symex_levelXt classes can create renamedt objects
+  explicit renamedt(underlyingt value) : value(std::move(value))
+  {
+  }
+};
+
 /// Functor to set the level 0 renaming of SSA expressions.
 /// Level 0 corresponds to threads.
 /// The renaming is built for one particular interleaving.
 struct symex_level0t : public symex_renaming_levelt
 {
-  void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
-    const;
+  renamedt<ssa_exprt, L0> operator()(
+    ssa_exprt ssa_expr,
+    const namespacet &ns,
+    unsigned thread_nr) const;
 
   symex_level0t() = default;
   ~symex_level0t() override = default;
@@ -68,7 +107,7 @@ struct symex_level0t : public symex_renaming_levelt
 /// This is to preserve locality in case of recursion
 struct symex_level1t : public symex_renaming_levelt
 {
-  void operator()(ssa_exprt &ssa_expr) const;
+  renamedt<ssa_exprt, L1> operator()(renamedt<ssa_exprt, L0> l0_expr) const;
 
   /// Insert the content of \p other into this renaming
   void restore_from(const current_namest &other);
@@ -82,6 +121,8 @@ struct symex_level1t : public symex_renaming_levelt
 /// This is to ensure each variable is only assigned once.
 struct symex_level2t : public symex_renaming_levelt
 {
+  renamedt<ssa_exprt, L2> operator()(renamedt<ssa_exprt, L1> l1_expr) const;
+
   symex_level2t() = default;
   ~symex_level2t() override = default;
 };

src/goto-symex/symex_dead.cpp

@@ -26,7 +26,7 @@ void goto_symext::symex_dead(statet &state)
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
-  ssa_exprt ssa = state.rename_ssa<statet::L1>(ssa_exprt{code.symbol()}, ns);
+  ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns);
 
   // in case of pointers, put something into the value set
   if(code.symbol().type().id() == ID_pointer)
@@ -37,8 +37,7 @@ void goto_symext::symex_dead(statet &state)
     else
       rhs=exprt(ID_invalid);
 
-    const exprt l1_rhs =
-      state.rename<goto_symex_statet::L1>(std::move(rhs), ns);
+    const exprt l1_rhs = state.rename<L1>(std::move(rhs), ns);
     state.value_set.assign(ssa, l1_rhs, ns, true, false);
   }
 

src/goto-symex/symex_decl.cpp

@@ -37,7 +37,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
-  ssa_exprt ssa = state.rename_ssa<statet::L1>(ssa_exprt{expr}, ns);
+  ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{expr}, ns);
   const irep_idt &l1_identifier = ssa.get_identifier();
 
   // rename type to L2
@@ -53,7 +53,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     else
       rhs=exprt(ID_invalid);
 
-    exprt l1_rhs = state.rename<goto_symex_statet::L1>(std::move(rhs), ns);
+    exprt l1_rhs = state.rename<L1>(std::move(rhs), ns);
     state.value_set.assign(ssa, l1_rhs, ns, true, false);
   }
 

src/goto-symex/symex_dereference.cpp

@@ -356,11 +356,11 @@ void goto_symext::dereference(exprt &expr, statet &state)
   // from different frames. Would be enough to rename
   // symbols whose address is taken.
   PRECONDITION(!state.call_stack().empty());
-  exprt l1_expr = state.rename<goto_symex_statet::L1>(expr, ns);
+  exprt l1_expr = state.rename<L1>(expr, ns);
 
   // start the recursion!
   dereference_rec(l1_expr, state);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
-  expr = state.rename<goto_symex_statet::L1>(std::move(l1_expr), ns);
+  expr = state.rename<L1>(std::move(l1_expr), ns);
 }

src/goto-symex/symex_dereference_state.cpp

@@ -48,8 +48,8 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
     {
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
-      const ssa_exprt sym_expr = state.rename_ssa<goto_symex_statet::L1>(
-        ssa_exprt{sym.symbol_expr()}, ns);
+      const ssa_exprt sym_expr =
+        state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns);
       sym.name = sym_expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;
@@ -68,8 +68,8 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
     {
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
-      const ssa_exprt sym_expr = state.rename_ssa<goto_symex_statet::L1>(
-        ssa_exprt{sym.symbol_expr()}, ns);
+      const ssa_exprt sym_expr =
+        state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns);
       sym.name = sym_expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;

src/goto-symex/symex_function_call.cpp

@@ -395,8 +395,8 @@ static void locality(
       it++)
   {
     // get L0 name
-    ssa_exprt ssa = state.rename_ssa<goto_symex_statet::L0>(
-      ssa_exprt{ns.lookup(*it).symbol_expr()}, ns);
+    ssa_exprt ssa =
+      state.rename_ssa<L0>(ssa_exprt{ns.lookup(*it).symbol_expr()}, ns);
     const irep_idt l0_name=ssa.get_identifier();
 
     // save old L1 name for popping the frame
@@ -418,8 +418,7 @@ static void locality(
     // identifiers may be shared among functions
     // (e.g., due to inlining or other code restructuring)
 
-    ssa_exprt ssa_l1 =
-      state.rename_ssa<goto_symex_statet::L1>(std::move(ssa), ns);
+    ssa_exprt ssa_l1 = state.rename_ssa<L1>(std::move(ssa), ns);
 
     irep_idt l1_name = ssa_l1.get_identifier();
     unsigned offset=0;

src/goto-symex/symex_goto.cpp

@@ -246,7 +246,7 @@ void goto_symext::symex_goto(statet &state)
       exprt new_rhs = boolean_negate(new_guard);
 
       ssa_exprt new_lhs =
-        state.rename_ssa<statet::L1>(ssa_exprt{guard_symbol_expr}, ns);
+        state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns);
       state.assignment(new_lhs, new_rhs, ns, true, false);
 
       guardt guard{true_exprt{}};

src/goto-symex/symex_start_thread.cpp

@@ -73,7 +73,7 @@ void goto_symext::symex_start_thread(statet &state)
       std::forward_as_tuple(lhs.get_l1_object_identifier()),
       std::forward_as_tuple(lhs, 0));
     CHECK_RETURN(emplace_result.second);
-    const ssa_exprt lhs_l1 = state.rename_ssa<statet::L1>(std::move(lhs), ns);
+    const ssa_exprt lhs_l1 = state.rename_ssa<L1>(std::move(lhs), ns);
     const irep_idt l1_name = lhs_l1.get_l1_object_identifier();
     // store it
     state.l1_history.insert(l1_name);