Type for the result of rename_level0

This makes explicit the fact that the expression has been renamed.
Making it possible to define functions which only accept expression
which have been through renaming.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -285,7 +285,7 @@ exprt goto_symex_statet::rename_level0(exprt expr, const namespacet &ns)
   // rename all the symbols with their last known value
   if(auto ssa = expr_try_dynamic_cast<ssa_exprt>(expr))
   {
-    return rename_level0(*ssa, ns);
+    return rename_level0(*ssa, ns).expr;
   }
   else if(expr.id() == ID_symbol)
   {
@@ -320,14 +320,14 @@ exprt goto_symex_statet::rename_level0(exprt expr, const namespacet &ns)
   }
 }
 
-ssa_exprt
+level0t<ssa_exprt>
 goto_symex_statet::rename_level0(const symbol_exprt &expr, const namespacet &ns)
 {
   ssa_exprt ssa{expr};
   set_l0_indices(level0, ssa, source.thread_nr, ns);
   rename(ssa.type(), ssa.get_identifier(), ns, L0);
   ssa.update_type();
-  return ssa;
+  return level0t<ssa_exprt>{ssa};
 }
 
 ssa_exprt goto_symex_statet::rename_level1_ssa(

src/goto-symex/goto_symex_state.h

@@ -71,7 +71,8 @@ class goto_symex_statet final
   enum levelt { L0=0, L1=1, L2=2 };
 
   // performs renaming _up to_ the given level
-  ssa_exprt rename_level0(const symbol_exprt &expr, const namespacet &ns);
+  level0t<ssa_exprt>
+  rename_level0(const symbol_exprt &expr, const namespacet &ns);
   ssa_exprt rename_level1_ssa(ssa_exprt expr, const namespacet &ns);
   exprt rename_level1(exprt expr, const namespacet &ns);
   ssa_exprt rename_level2_ssa(ssa_exprt expr, const namespacet &ns);

src/goto-symex/renaming_level.h

@@ -51,6 +51,16 @@ struct symex_renaming_levelt
   }
 };
 
+/// Wrapper for expressions that have been renamed at level0
+template <typename underlyingt>
+struct level0t
+{
+  static_assert(
+    std::is_base_of<exprt, underlyingt>::value,
+    "underlyingt should inherit from exprt");
+  underlyingt expr;
+};
+
 /// Set the level 0 renaming of SSA expressions.
 /// Level 0 corresponds to threads.
 /// The renaming is built for one particular interleaving.

src/goto-symex/symex_function_call.cpp

@@ -399,39 +399,40 @@ void goto_symext::locality(
       it++)
   {
     // get L0 name
-    ssa_exprt ssa = state.rename_level0(ns.lookup(*it).symbol_expr(), ns);
-    const irep_idt l0_name=ssa.get_identifier();
+    level0t<ssa_exprt> l0 =
+      state.rename_level0(ns.lookup(*it).symbol_expr(), ns);
+    const irep_idt l0_name = l0.expr.get_identifier();
 
     // save old L1 name for popping the frame
     auto c_it = state.level1.current_names.find(l0_name);
 
     if(c_it != state.level1.current_names.end())
     {
       frame.old_level1.emplace(l0_name, c_it->second);
-      c_it->second = std::make_pair(ssa, frame_nr);
+      c_it->second = std::make_pair(l0.expr, frame_nr);
     }
     else
     {
       c_it = state.level1.current_names
-               .emplace(l0_name, std::make_pair(ssa, frame_nr))
+               .emplace(l0_name, std::make_pair(l0.expr, frame_nr))
                .first;
     }
 
     // do L1 renaming -- these need not be unique, as
     // identifiers may be shared among functions
     // (e.g., due to inlining or other code restructuring)
 
-    state.rename_level1(ssa, ns);
+    state.rename_level1(l0.expr, ns);
 
-    irep_idt l1_name=ssa.get_identifier();
+    irep_idt l1_name = l0.expr.get_identifier();
     unsigned offset=0;
 
     while(state.l1_history.find(l1_name)!=state.l1_history.end())
     {
       symex_renaming_levelt::increase_counter(c_it);
       ++offset;
-      ssa.set_level_1(frame_nr+offset);
-      l1_name=ssa.get_identifier();
+      l0.expr.set_level_1(frame_nr + offset);
+      l1_name = l0.expr.get_identifier();
     }
 
     // now unique -- store

src/goto-symex/symex_start_thread.cpp

@@ -65,14 +65,14 @@ void goto_symext::symex_start_thread(statet &state)
     ssa_exprt lhs(c_it->second.first.get_original_expr());
 
     // get L0 name for current thread
-    lhs.set_level_0(t);
+    level0t<ssa_exprt> l0_lhs = state.rename_level0(lhs, ns);
 
     // set up L1 name
     auto emplace_result = state.level1.current_names.emplace(
-      lhs.get_l1_object_identifier(), std::make_pair(lhs, 0));
+      lhs.get_l1_object_identifier(), std::make_pair(l0_lhs.expr, 0));
     CHECK_RETURN(emplace_result.second);
-    state.rename_level1(lhs, ns);
-    const irep_idt l1_name=lhs.get_l1_object_identifier();
+    state.rename_level1(l0_lhs.expr, ns);
+    const irep_idt l1_name = l0_lhs.expr.get_l1_object_identifier();
     // store it
     state.l1_history.insert(l1_name);
     new_thread.call_stack.back().local_objects.insert(l1_name);
@@ -85,7 +85,7 @@ void goto_symext::symex_start_thread(statet &state)
     state.record_events=false;
     symex_assign_symbol(
       state,
-      lhs,
+      l0_lhs.expr,
       nil_exprt(),
       rhs,
       guard,