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

@@ -280,7 +280,7 @@ goto_symex_statet::rename_level1_ssa(ssa_exprt ssa, const namespacet &ns)
   return ssa;
 }
 
-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
@@ -538,7 +538,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 +669,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

@@ -152,9 +152,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,9 @@ 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_assign.cpp

@@ -212,7 +212,7 @@ void goto_symext::symex_assign_symbol(
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
-  exprt l2_rhs = state.rename<goto_symex_statet::L2>(std::move(ssa_rhs), ns);
+  exprt l2_rhs = state.rename<L2>(std::move(ssa_rhs), ns);
   do_simplify(l2_rhs);
 
   ssa_exprt ssa_lhs=lhs;
@@ -228,8 +228,7 @@ void goto_symext::symex_assign_symbol(
   ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);
   const bool record_events=state.record_events;
   state.record_events=false;
-  exprt l2_full_lhs =
-    state.rename<goto_symex_statet::L2>(std::move(ssa_full_lhs), ns);
+  exprt l2_full_lhs = state.rename<L2>(std::move(ssa_full_lhs), ns);
   state.record_events=record_events;
 
   guardt tmp_guard(state.guard);
@@ -408,7 +407,7 @@ void goto_symext::symex_assign_if(
 
   guardt old_guard=guard;
 
-  exprt renamed_guard = state.rename<goto_symex_statet::L2>(lhs.cond(), ns);
+  exprt renamed_guard = state.rename<L2>(lhs.cond(), ns);
   do_simplify(renamed_guard);
 
   if(!renamed_guard.is_false())

src/goto-symex/symex_builtin_functions.cpp

@@ -71,7 +71,7 @@ void goto_symext::symex_allocate(
   else
   {
     // to allow constant propagation
-    exprt tmp_size = state.rename<goto_symex_statet::L2>(size, ns);
+    exprt tmp_size = state.rename<L2>(size, ns);
     simplify(tmp_size, ns);
 
     // special treatment for sizeof(T)*x
@@ -163,7 +163,7 @@ void goto_symext::symex_allocate(
   state.symbol_table.add(value_symbol);
 
   // to allow constant propagation
-  exprt zero_init = state.rename<goto_symex_statet::L2>(code.op1(), ns);
+  exprt zero_init = state.rename<L2>(code.op1(), ns);
   simplify(zero_init, ns);
 
   INVARIANT(
@@ -232,7 +232,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
     return; // ignore
 
   // to allow constant propagation
-  exprt tmp = state.rename<goto_symex_statet::L2>(code.op0(), ns);
+  exprt tmp = state.rename<L2>(code.op0(), ns);
   do_simplify(tmp);
   irep_idt id=get_symbol(tmp);
 
@@ -309,7 +309,7 @@ void goto_symext::symex_printf(
 {
   PRECONDITION(!rhs.operands().empty());
 
-  exprt tmp_rhs = state.rename<goto_symex_statet::L2>(rhs, ns);
+  exprt tmp_rhs = state.rename<L2>(rhs, ns);
   do_simplify(tmp_rhs);
 
   const exprt::operandst &operands = tmp_rhs.operands();
@@ -333,14 +333,14 @@ void goto_symext::symex_input(
 {
   PRECONDITION(code.operands().size() >= 2);
 
-  exprt id_arg = state.rename<goto_symex_statet::L2>(code.op0(), ns);
+  exprt id_arg = state.rename<L2>(code.op0(), ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     args.push_back(code.operands()[i]);
-    exprt l2_arg = state.rename<goto_symex_statet::L2>(args.back(), ns);
+    exprt l2_arg = state.rename<L2>(args.back(), ns);
     do_simplify(l2_arg);
     args.back() = std::move(l2_arg);
   }
@@ -355,14 +355,14 @@ void goto_symext::symex_output(
   const codet &code)
 {
   PRECONDITION(code.operands().size() >= 2);
-  exprt id_arg = state.rename<goto_symex_statet::L2>(code.op0(), ns);
+  exprt id_arg = state.rename<L2>(code.op0(), ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     args.push_back(code.operands()[i]);
-    exprt l2_arg = state.rename<goto_symex_statet::L2>(args.back(), ns);
+    exprt l2_arg = state.rename<L2>(args.back(), ns);
     do_simplify(l2_arg);
     args.back() = std::move(l2_arg);
   }
@@ -475,8 +475,7 @@ void goto_symext::symex_trace(
     irep_idt event = to_string_constant(code.arguments()[1].op0()).get_value();
 
     for(std::size_t j=2; j<code.arguments().size(); j++)
-      vars.push_back(
-        state.rename<goto_symex_statet::L2>(code.arguments()[j], ns));
+      vars.push_back(state.rename<L2>(code.arguments()[j], ns));
 
     target.output(state.guard.as_expr(), state.source, event, vars);
   }

src/goto-symex/symex_dead.cpp

@@ -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

@@ -41,7 +41,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   const irep_idt &l1_identifier = ssa.get_identifier();
 
   // rename type to L2
-  state.rename<goto_symex_statet::L2>(ssa.type(), l1_identifier, ns);
+  state.rename<L2>(ssa.type(), l1_identifier, ns);
   ssa.update_type();
 
   // in case of pointers, put something into the value set
@@ -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);
   }
 
@@ -69,7 +69,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   symex_renaming_levelt::increase_counter(level2_it);
   const bool record_events=state.record_events;
   state.record_events=false;
-  exprt expr_l2 = state.rename<statet::L2>(std::move(ssa), ns);
+  exprt expr_l2 = state.rename<L2>(std::move(ssa), ns);
   INVARIANT(
     expr_l2.id() == ID_symbol && expr_l2.get_bool(ID_C_SSA_symbol),
     "symbol to declare should not be replaced by constant propagation");

src/goto-symex/symex_dereference.cpp

@@ -357,11 +357,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_function_call.cpp

@@ -261,7 +261,7 @@ void goto_symext::symex_function_call_code(
   // read the arguments -- before the locality renaming
   exprt::operandst arguments = call.arguments();
   for(auto &a : arguments)
-    a = state.rename<statet::L2>(std::move(a), ns);
+    a = state.rename<L2>(std::move(a), ns);
 
   // we hide the call if the caller and callee are both hidden
   const bool hidden = state.top().hidden_function && goto_function.is_hidden();

src/goto-symex/symex_goto.cpp

@@ -37,7 +37,7 @@ void goto_symext::symex_goto(statet &state)
   exprt old_guard = instruction.get_condition();
   clean_expr(old_guard, state, false);
 
-  exprt new_guard = state.rename<goto_symex_statet::L2>(old_guard, ns);
+  exprt new_guard = state.rename<L2>(old_guard, ns);
   do_simplify(new_guard);
 
   if(new_guard.is_false())
@@ -268,7 +268,7 @@ void goto_symext::symex_goto(statet &state)
         original_source,
         symex_targett::assignment_typet::GUARD);
 
-      guard_expr = state.rename<goto_symex_statet::L2>(
+      guard_expr = state.rename<L2>(
         boolean_negate(guard_symbol_expr), ns);
     }
 

src/goto-symex/symex_main.cpp

@@ -95,7 +95,7 @@ void goto_symext::vcc(
   }
 
   // now rename, enables propagation
-  exprt l2_expr = state.rename<goto_symex_statet::L2>(std::move(expr), ns);
+  exprt l2_expr = state.rename<L2>(std::move(expr), ns);
 
   // now try simplifier on it
   do_simplify(l2_expr);
@@ -411,7 +411,7 @@ void goto_symext::symex_step(
       exprt tmp = instruction.get_condition();
       clean_expr(tmp, state, false);
       symex_assume(
-        state, state.rename<goto_symex_statet::L2>(std::move(tmp), ns));
+        state, state.rename<L2>(std::move(tmp), ns));
     }
 
     symex_transition(state);