level1t type for the result of rename_level1

This makes it explicit in the type that the expression has been renamed
up to level1.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -174,7 +174,7 @@ void goto_symex_statet::assignment(
   bool allow_pointer_unsoundness)
 {
   // identifier should be l0 or l1, make sure it's l1
-  lhs = rename_level1_ssa(std::move(lhs), ns);
+  lhs = rename_level1_ssa(std::move(lhs), ns).expr;
   irep_idt l1_identifier=lhs.get_identifier();
 
   // the type might need renaming
@@ -330,38 +330,50 @@ goto_symex_statet::rename_level0(const symbol_exprt &expr, const namespacet &ns)
   return level0t<ssa_exprt>{ssa};
 }
 
-ssa_exprt goto_symex_statet::rename_level1_ssa(
-  ssa_exprt ssa, const namespacet &ns)
+level1t<ssa_exprt> goto_symex_statet::rename_level1(
+  level0t<ssa_exprt> l0_expr,
+  const namespacet &ns)
+{
+  set_l1_indices(level0, level1, l0_expr.expr, source.thread_nr, ns);
+  rename(l0_expr.expr.type(), l0_expr.expr.get_identifier(), ns, L1);
+  l0_expr.expr.update_type();
+  return level1t<ssa_exprt>{l0_expr.expr};
+}
+
+level1t<ssa_exprt>
+goto_symex_statet::rename_level1_ssa(ssa_exprt ssa, const namespacet &ns)
 {
   set_l1_indices(level0, level1, ssa, source.thread_nr, ns);
   rename(ssa.type(), ssa.get_identifier(), ns, L1);
   ssa.update_type();
-  return ssa;
+  return level1t<ssa_exprt>{ssa};
 }
 
-exprt goto_symex_statet::rename_level1(exprt expr, const namespacet &ns)
+level1t<exprt>
+goto_symex_statet::rename_level1(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_level1_ssa(*ssa, ns);
+    expr = rename_level1_ssa(std::move(*ssa), ns).expr;
+    return level1t<exprt>{expr};
   }
-  else if(expr.id() == ID_symbol)
+  else if(auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
   {
     // we never rename function symbols
-    if(expr.type().id() == ID_code)
+    if(symbol->type().id() == ID_code)
     {
-      rename(expr.type(), to_symbol_expr(expr).get_identifier(), ns, L1);
-      return expr;
+      rename(symbol->type(), symbol->get_identifier(), ns, L1);
+      return level1t<exprt>{std::move(*symbol)};
     }
 
-    return rename_level1_ssa(ssa_exprt{expr}, ns);
+    return level1t<exprt>{rename_level1_ssa(ssa_exprt{*symbol}, ns).expr};
   }
   else if(auto address_of_expr = expr_try_dynamic_cast<address_of_exprt>(expr))
   {
     rename_address(address_of_expr->object(), ns, L1);
     to_pointer_type(expr.type()).subtype() = address_of_expr->object().type();
-    return expr;
+    return level1t<exprt>{expr};
   }
   else
   {
@@ -370,10 +382,10 @@ exprt goto_symex_statet::rename_level1(exprt expr, const namespacet &ns)
 
     // do this recursively
     for(auto &op : expr.operands())
-      op = rename_level1(std::move(op), ns);
+      op = rename_level1(std::move(op), ns).expr;
 
     fix_type(expr);
-    return expr;
+    return level1t<exprt>{expr};
   }
 }
 
@@ -662,7 +674,7 @@ void goto_symex_statet::rename_address(
   PRECONDITION(level != L0);
   auto rename_expr = [&](exprt &e) {
     if(level == L1)
-      e = rename_level1(e, ns);
+      e = rename_level1(e, ns).expr;
     else
       rename_level2(e, ns);
   };
@@ -766,7 +778,7 @@ void goto_symex_statet::rename(
     if(level == L0)
       e = rename_level0(std::move(e), ns);
     if(level == L1)
-      e = rename_level1(e, ns);
+      e = rename_level1(e, ns).expr;
     else
       rename_level2(e, ns);
   };

src/goto-symex/goto_symex_state.h

@@ -73,10 +73,11 @@ class goto_symex_statet final
   // performs renaming _up to_ the given level
   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);
-  exprt rename_level2(exprt expr, const namespacet &ns);
+  level1t<ssa_exprt> rename_level1_ssa(ssa_exprt expr, const namespacet &ns);
+  level1t<exprt> rename_level1(exprt expr, const namespacet &ns);
+  level1t<ssa_exprt>
+  rename_level1(level0t<ssa_exprt> l0_expr, const namespacet &ns);
+  void rename_level2(exprt &expr, const namespacet &ns);
   void rename(
     typet &type,
     const irep_idt &l1_identifier,

src/goto-symex/renaming_level.h

@@ -61,6 +61,16 @@ struct level0t
   underlyingt expr;
 };
 
+/// Wrapper for expressions that have been renamed at level1
+template <typename underlyingt>
+struct level1t
+{
+  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_dead.cpp

@@ -26,7 +26,8 @@ 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_level1_ssa(ssa_exprt{code.symbol()}, ns);
+  level1t<ssa_exprt> ssa =
+    state.rename_level1_ssa(ssa_exprt{code.symbol()}, ns);
 
   // in case of pointers, put something into the value set
   if(code.symbol().type().id() == ID_pointer)
@@ -37,11 +38,11 @@ void goto_symext::symex_dead(statet &state)
       return exprt(ID_invalid);
     }();
 
-    exprt l1_rhs = state.rename_level1(std::move(rhs), ns);
-    state.value_set.assign(ssa, l1_rhs, ns, true, false);
+    level1t<exprt> l1_rhs = state.rename_level1(std::move(rhs), ns);
+    state.value_set.assign(ssa.expr, l1_rhs.expr, ns, true, false);
   }
 
-  const irep_idt &l1_identifier = ssa.get_identifier();
+  const irep_idt &l1_identifier=ssa.expr.get_identifier();
 
   // prevent propagation
   state.propagation.erase(l1_identifier);

src/goto-symex/symex_decl.cpp

@@ -37,12 +37,12 @@ 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_level1_ssa(ssa_exprt{expr}, ns);
-  const irep_idt &l1_identifier = ssa.get_identifier();
+  level1t<ssa_exprt> ssa = state.rename_level1_ssa(ssa_exprt{expr}, ns);
+  const irep_idt &l1_identifier = ssa.expr.get_identifier();
 
   // rename type to L2
-  state.rename(ssa.type(), l1_identifier, ns);
-  ssa.update_type();
+  state.rename(ssa.expr.type(), l1_identifier, ns);
+  ssa.expr.update_type();
 
   // in case of pointers, put something into the value set
   if(expr.type().id() == ID_pointer)
@@ -53,8 +53,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
       return exprt(ID_invalid);
     }();
 
-    exprt l1_rhs = state.rename_level1(std::move(rhs), ns);
-    state.value_set.assign(ssa, l1_rhs, ns, true, false);
+    level1t<exprt> l1_rhs = state.rename_level1(std::move(rhs), ns);
+    state.value_set.assign(ssa.expr, l1_rhs.expr, ns, true, false);
   }
 
   // prevent propagation
@@ -64,12 +64,12 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   // inlining may yield multiple declarations of the same identifier
   // within the same L1 context
   const auto level2_it = state.level2.current_names
-                           .emplace(l1_identifier, std::make_pair(ssa, 0))
+                           .emplace(l1_identifier, std::make_pair(ssa.expr, 0))
                            .first;
   symex_renaming_levelt::increase_counter(level2_it);
   const bool record_events=state.record_events;
   state.record_events=false;
-  state.rename_level2_ssa(ssa, ns);
+  state.rename_level2(ssa.expr, ns);
   state.record_events=record_events;
 
   // we hide the declaration of auxiliary variables
@@ -81,12 +81,12 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
 
   target.decl(
     state.guard.as_expr(),
-    ssa,
+    ssa.expr,
     state.source,
     hidden ? symex_targett::assignment_typet::HIDDEN
            : symex_targett::assignment_typet::STATE);
 
-  if(state.dirty(ssa.get_object_name()) && state.atomic_section_id == 0)
+  if(state.dirty(ssa.expr.get_object_name()) && state.atomic_section_id == 0)
     target.shared_write(
-      state.guard.as_expr(), ssa, state.atomic_section_id, state.source);
+      state.guard.as_expr(), ssa.expr, state.atomic_section_id, state.source);
 }

src/goto-symex/symex_dereference.cpp

@@ -381,12 +381,12 @@ void goto_symext::dereference(
   // from different frames. Would be enough to rename
   // symbols whose address is taken.
   PRECONDITION(!state.call_stack().empty());
-  state.rename_level1(expr, ns);
+  level1t<exprt> l1_expr = state.rename_level1(expr, ns);
 
   // start the recursion!
   guardt guard{true_exprt{}};
-  dereference_rec(expr, state, guard, write);
+  dereference_rec(l1_expr.expr, state, guard, write);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
-  state.rename_level1(expr, ns);
+  expr = state.rename_level1(std::move(l1_expr.expr), ns).expr;
 }

src/goto-symex/symex_dereference_state.cpp

@@ -36,9 +36,9 @@ bool symex_dereference_statet::has_failed_symbol(
     {
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
-      const ssa_exprt sym_expr =
+      const level1t<ssa_exprt> sym_expr =
         state.rename_level1_ssa(ssa_exprt{sym.symbol_expr()}, ns);
-      sym.name = sym_expr.get_identifier();
+      sym.name = sym_expr.expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       symbol=sym_ptr;
       return true;
@@ -56,9 +56,9 @@ bool symex_dereference_statet::has_failed_symbol(
     {
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
-      const ssa_exprt sym_expr =
+      const level1t<ssa_exprt> sym_expr =
         state.rename_level1_ssa(ssa_exprt{sym.symbol_expr()}, ns);
-      sym.name = sym_expr.get_identifier();
+      sym.name = sym_expr.expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       symbol=sym_ptr;
       return true;

src/goto-symex/symex_function_call.cpp

@@ -422,17 +422,17 @@ void goto_symext::locality(
     // identifiers may be shared among functions
     // (e.g., due to inlining or other code restructuring)
 
-    state.rename_level1(l0.expr, ns);
+    level1t<ssa_exprt> ssa = state.rename_level1(std::move(l0), ns);
 
-    irep_idt l1_name = l0.expr.get_identifier();
+    irep_idt l1_name = ssa.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;
-      l0.expr.set_level_1(frame_nr + offset);
-      l1_name = l0.expr.get_identifier();
+      ssa.expr.set_level_1(frame_nr + offset);
+      l1_name = ssa.expr.get_identifier();
     }
 
     // now unique -- store

src/goto-symex/symex_goto.cpp

@@ -246,23 +246,24 @@ void goto_symext::symex_goto(statet &state)
         symbol_exprt(guard_identifier, bool_typet());
       exprt new_rhs = boolean_negate(new_guard);
 
-      ssa_exprt new_lhs =
+      level1t<ssa_exprt> new_lhs =
         state.rename_level1_ssa(ssa_exprt{guard_symbol_expr}, ns);
-      state.assignment(new_lhs, new_rhs, ns, true, false);
+      state.assignment(new_lhs.expr, new_rhs, ns, true, false);
 
       guardt guard{true_exprt{}};
 
       log.conditional_output(
-        log.debug(),
-        [this, &new_lhs](messaget::mstreamt &mstream) {
-          mstream << "Assignment to " << new_lhs.get_identifier()
-                  << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
-                  << messaget::eom;
+        log.debug(), [this, &new_lhs](messaget::mstreamt &mstream) {
+          mstream << "Assignment to " << new_lhs.expr.get_identifier() << " ["
+                  << pointer_offset_bits(new_lhs.expr.type(), ns).value_or(0)
+                  << " bits]" << messaget::eom;
         });
 
       target.assignment(
         guard.as_expr(),
-        new_lhs, new_lhs, guard_symbol_expr,
+        new_lhs.expr,
+        new_lhs.expr,
+        guard_symbol_expr,
         new_rhs,
         original_source,
         symex_targett::assignment_typet::GUARD);

src/goto-symex/symex_start_thread.cpp

@@ -70,8 +70,8 @@ void goto_symext::symex_start_thread(statet &state)
     auto emplace_result = state.level1.current_names.emplace(
       lhs.get_l1_object_identifier(), std::make_pair(l0_lhs.expr, 0));
     CHECK_RETURN(emplace_result.second);
-    state.rename_level1(l0_lhs.expr, ns);
-    const irep_idt l1_name = l0_lhs.expr.get_l1_object_identifier();
+    const level1t<ssa_exprt> l1_lhs = state.rename_level1(l0_lhs, ns);
+    const irep_idt l1_name = l1_lhs.expr.get_l1_object_identifier();
     // store it
     state.l1_history.insert(l1_name);
     new_thread.call_stack.back().local_objects.insert(l1_name);
@@ -84,7 +84,7 @@ void goto_symext::symex_start_thread(statet &state)
     state.record_events=false;
     symex_assign_symbol(
       state,
-      l0_lhs.expr,
+      l1_lhs.expr,
       nil_exprt(),
       rhs,
       guard,