Move levelt to renaming_level.h

This seems a more appropriate to find it, and we could use the levelt
type for templates we will define in this file.

Author: romainbrenguier

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

@@ -263,7 +263,7 @@ void goto_symex_statet::set_l2_indices(
   ssa_expr = level2(std::move(l1));
 }
 
-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 +282,10 @@ 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 <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
@@ -544,7 +543,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 +668,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.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

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);