Make level argument of rename a template argument

The level argument is always known from the call site (except for
rename recursive calls), and there are only 3 possible values, so it
makes sense to have it as a template argument.
This will be useful in particular, when we want the return type to
depend on the level.

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

@@ -71,7 +71,7 @@ exprt scratch_programt::eval(const exprt &e)
 {
   exprt ssa=e;
 
-  symex_state->rename(ssa, ns);
+  symex_state->rename<goto_symex_statet::L2>(ssa, ns);
 
   return checker->get(ssa);
 }

src/goto-symex/goto_symex_state.cpp

@@ -162,11 +162,11 @@ void goto_symex_statet::assignment(
   bool allow_pointer_unsoundness)
 {
   // identifier should be l0 or l1, make sure it's l1
-  rename(lhs, ns, L1);
+  rename<L1>(lhs, ns);
   irep_idt l1_identifier=lhs.get_identifier();
 
   // the type might need renaming
-  rename(lhs.type(), l1_identifier, ns);
+  rename<L2>(lhs.type(), l1_identifier, ns);
   lhs.update_type();
   if(run_validation_checks)
   {
@@ -266,15 +266,13 @@ ssa_exprt
 goto_symex_statet::rename_level0_ssa(ssa_exprt ssa, const namespacet &ns)
 {
   set_l0_indices(ssa, ns);
-  rename(ssa.type(), ssa.get_identifier(), ns, L0);
+  rename<L0>(ssa.type(), ssa.get_identifier(), ns);
   ssa.update_type();
   return ssa;
 }
 
-void goto_symex_statet::rename(
-  exprt &expr,
-  const namespacet &ns,
-  levelt level)
+template <goto_symex_statet::levelt level>
+void goto_symex_statet::rename(exprt &expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
 
@@ -290,13 +288,13 @@ void goto_symex_statet::rename(
     else if(level == L1)
     {
       set_l1_indices(ssa, ns);
-      rename(expr.type(), ssa.get_identifier(), ns, level);
+      rename<level>(expr.type(), ssa.get_identifier(), ns);
       ssa.update_type();
     }
     else if(level==L2)
     {
       set_l1_indices(ssa, ns);
-      rename(expr.type(), ssa.get_identifier(), ns, level);
+      rename<level>(expr.type(), ssa.get_identifier(), ns);
       ssa.update_type();
 
       if(l2_thread_read_encoding(ssa, ns))
@@ -325,32 +323,27 @@ void goto_symex_statet::rename(
     // we never rename function symbols
     if(as_const(expr).type().id() == ID_code)
     {
-      rename(
-        expr.type(),
-        to_symbol_expr(expr).get_identifier(),
-        ns,
-        level);
-
+      rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
       return;
     }
 
     expr=ssa_exprt(expr);
-    rename(expr, ns, level);
+    rename<level>(expr, ns);
   }
   else if(expr.id()==ID_address_of)
   {
     auto &address_of_expr = to_address_of_expr(expr);
-    rename_address(address_of_expr.object(), ns, level);
+    rename_address<level>(address_of_expr.object(), ns);
     to_pointer_type(expr.type()).subtype() =
       as_const(address_of_expr).object().type();
   }
   else
   {
-    rename(expr.type(), irep_idt(), ns, level);
+    rename<level>(expr.type(), irep_idt(), ns);
 
     // do this recursively
     Forall_operands(it, expr)
-      rename(*it, ns, level);
+      rename<level>(*it, ns);
 
     const exprt &c_expr = as_const(expr);
     INVARIANT(
@@ -541,10 +534,8 @@ bool goto_symex_statet::l2_thread_write_encoding(
   return threads.size()>1;
 }
 
-void goto_symex_statet::rename_address(
-  exprt &expr,
-  const namespacet &ns,
-  levelt level)
+template <goto_symex_statet::levelt level>
+void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
 {
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
@@ -554,42 +545,42 @@ void goto_symex_statet::rename_address(
     // only do L1!
     set_l1_indices(ssa, ns);
 
-    rename(expr.type(), ssa.get_identifier(), ns, level);
+    rename<level>(expr.type(), ssa.get_identifier(), ns);
     ssa.update_type();
   }
   else if(expr.id()==ID_symbol)
   {
     expr=ssa_exprt(expr);
-    rename_address(expr, ns, level);
+    rename_address<level>(expr, ns);
   }
   else
   {
     if(expr.id()==ID_index)
     {
       index_exprt &index_expr=to_index_expr(expr);
 
-      rename_address(index_expr.array(), ns, level);
+      rename_address<level>(index_expr.array(), ns);
       PRECONDITION(index_expr.array().type().id() == ID_array);
       expr.type() = to_array_type(index_expr.array().type()).subtype();
 
       // the index is not an address
-      rename(index_expr.index(), ns, level);
+      rename<level>(index_expr.index(), ns);
     }
     else if(expr.id()==ID_if)
     {
       // the condition is not an address
       if_exprt &if_expr=to_if_expr(expr);
-      rename(if_expr.cond(), ns, level);
-      rename_address(if_expr.true_case(), ns, level);
-      rename_address(if_expr.false_case(), ns, level);
+      rename<level>(if_expr.cond(), ns);
+      rename_address<level>(if_expr.true_case(), ns);
+      rename_address<level>(if_expr.false_case(), ns);
 
       if_expr.type()=if_expr.true_case().type();
     }
     else if(expr.id()==ID_member)
     {
       member_exprt &member_expr=to_member_expr(expr);
 
-      rename_address(member_expr.struct_op(), ns, level);
+      rename_address<level>(member_expr.struct_op(), ns);
 
       // type might not have been renamed in case of nesting of
       // structs and pointers/arrays
@@ -606,17 +597,17 @@ void goto_symex_statet::rename_address(
         expr.type()=comp.type();
       }
       else
-        rename(expr.type(), irep_idt(), ns, level);
+        rename<level>(expr.type(), irep_idt(), ns);
     }
     else
     {
       // this could go wrong, but we would have to re-typecheck ...
-      rename(expr.type(), irep_idt(), ns, level);
+      rename<level>(expr.type(), irep_idt(), ns);
 
       // do this recursively; we assume here
       // that all the operands are addresses
       Forall_operands(it, expr)
-        rename_address(*it, ns, level);
+        rename_address<level>(*it, ns);
     }
   }
 }
@@ -674,11 +665,11 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
   return false;
 }
 
+template <goto_symex_statet::levelt level>
 void goto_symex_statet::rename(
   typet &type,
   const irep_idt &l1_identifier,
-  const namespacet &ns,
-  levelt level)
+  const namespacet &ns)
 {
   // check whether there are symbol expressions in the type; if not, there
   // is no need to expand the struct/union tags in the type
@@ -717,8 +708,8 @@ void goto_symex_statet::rename(
   if(type.id()==ID_array)
   {
     auto &array_type = to_array_type(type);
-    rename(array_type.subtype(), irep_idt(), ns, level);
-    rename(array_type.size(), ns, level);
+    rename<level>(array_type.subtype(), irep_idt(), ns);
+    rename<level>(array_type.size(), ns);
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
@@ -729,14 +720,14 @@ void goto_symex_statet::rename(
     {
       // be careful, or it might get cyclic
       if(component.type().id() == ID_array)
-        rename(to_array_type(component.type()).size(), ns, level);
+        rename<level>(to_array_type(component.type()).size(), ns);
       else if(component.type().id() != ID_pointer)
-        rename(component.type(), irep_idt(), ns, level);
+        rename<level>(component.type(), irep_idt(), ns);
     }
   }
   else if(type.id()==ID_pointer)
   {
-    rename(to_pointer_type(type).subtype(), irep_idt(), ns, level);
+    rename<level>(to_pointer_type(type).subtype(), irep_idt(), ns);
   }
 
   if(level==L2 &&

src/goto-symex/goto_symex_state.h

@@ -179,15 +179,13 @@ class goto_symex_statet final : public goto_statet
   ///
   /// A full explanation of SSA (which is why we do this renaming) is in
   /// the SSA section of background-concepts.md.
-  void rename(exprt &expr, const namespacet &ns, levelt level=L2);
+  template <levelt>
+  void rename(exprt &expr, const namespacet &ns);
 
   ssa_exprt rename_level0_ssa(ssa_exprt ssa, const namespacet &ns);
 
-  void rename(
-    typet &type,
-    const irep_idt &l1_identifier,
-    const namespacet &ns,
-    levelt level=L2);
+  template <levelt>
+  void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
 
   void assignment(
     ssa_exprt &lhs, // L0/L1
@@ -198,7 +196,8 @@ class goto_symex_statet final : public goto_statet
     bool allow_pointer_unsoundness=false);
 
 protected:
-  void rename_address(exprt &expr, const namespacet &ns, levelt level);
+  template <levelt>
+  void rename_address(exprt &expr, const namespacet &ns);
 
   /// Update level 0 values.
   void set_l0_indices(ssa_exprt &expr, const namespacet &ns);

src/goto-symex/symex_assign.cpp

@@ -212,7 +212,7 @@ void goto_symext::symex_assign_symbol(
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
-  state.rename(ssa_rhs, ns);
+  state.rename<goto_symex_statet::L2>(ssa_rhs, ns);
   do_simplify(ssa_rhs);
 
   ssa_exprt ssa_lhs=lhs;
@@ -228,7 +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;
-  state.rename(ssa_full_lhs, ns);
+  state.rename<goto_symex_statet::L2>(ssa_full_lhs, ns);
   state.record_events=record_events;
 
   guardt tmp_guard(state.guard);
@@ -407,7 +407,7 @@ void goto_symext::symex_assign_if(
   guardt old_guard=guard;
 
   exprt renamed_guard=lhs.cond();
-  state.rename(renamed_guard, ns);
+  state.rename<goto_symex_statet::L2>(renamed_guard, ns);
   do_simplify(renamed_guard);
 
   if(!renamed_guard.is_false())

src/goto-symex/symex_builtin_functions.cpp

@@ -71,7 +71,8 @@ void goto_symext::symex_allocate(
   else
   {
     exprt tmp_size=size;
-    state.rename(tmp_size, ns); // to allow constant propagation
+    state.rename<goto_symex_statet::L2>(
+      tmp_size, ns); // to allow constant propagation
     simplify(tmp_size, ns);
 
     // special treatment for sizeof(T)*x
@@ -163,7 +164,8 @@ void goto_symext::symex_allocate(
   state.symbol_table.add(value_symbol);
 
   exprt zero_init=code.op1();
-  state.rename(zero_init, ns); // to allow constant propagation
+  state.rename<goto_symex_statet::L2>(
+    zero_init, ns); // to allow constant propagation
   simplify(zero_init, ns);
 
   INVARIANT(
@@ -232,7 +234,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
     return; // ignore
 
   exprt tmp=code.op0();
-  state.rename(tmp, ns); // to allow constant propagation
+  state.rename<goto_symex_statet::L2>(tmp, ns); // to allow constant propagation
   do_simplify(tmp);
   irep_idt id=get_symbol(tmp);
 
@@ -310,7 +312,7 @@ void goto_symext::symex_printf(
   PRECONDITION(!rhs.operands().empty());
 
   exprt tmp_rhs=rhs;
-  state.rename(tmp_rhs, ns);
+  state.rename<goto_symex_statet::L2>(tmp_rhs, ns);
   do_simplify(tmp_rhs);
 
   const exprt::operandst &operands=tmp_rhs.operands();
@@ -336,14 +338,14 @@ void goto_symext::symex_input(
 
   exprt id_arg=code.op0();
 
-  state.rename(id_arg, ns);
+  state.rename<goto_symex_statet::L2>(id_arg, ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     args.push_back(code.operands()[i]);
-    state.rename(args.back(), ns);
+    state.rename<goto_symex_statet::L2>(args.back(), ns);
     do_simplify(args.back());
   }
 
@@ -360,14 +362,14 @@ void goto_symext::symex_output(
 
   exprt id_arg=code.op0();
 
-  state.rename(id_arg, ns);
+  state.rename<goto_symex_statet::L2>(id_arg, ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     args.push_back(code.operands()[i]);
-    state.rename(args.back(), ns);
+    state.rename<goto_symex_statet::L2>(args.back(), ns);
     do_simplify(args.back());
   }
 
@@ -481,7 +483,7 @@ void goto_symext::symex_trace(
     for(std::size_t j=2; j<code.arguments().size(); j++)
     {
       exprt var(code.arguments()[j]);
-      state.rename(var, ns);
+      state.rename<goto_symex_statet::L2>(var, ns);
       vars.push_back(var);
     }
 

src/goto-symex/symex_dead.cpp

@@ -27,7 +27,7 @@ void goto_symext::symex_dead(statet &state)
   // We also prevent propagation of old values.
 
   ssa_exprt ssa(code.symbol());
-  state.rename(ssa, ns, goto_symex_statet::L1);
+  state.rename<goto_symex_statet::L1>(ssa, ns);
 
   // in case of pointers, put something into the value set
   if(code.symbol().type().id() == ID_pointer)
@@ -38,7 +38,7 @@ void goto_symext::symex_dead(statet &state)
     else
       rhs=exprt(ID_invalid);
 
-    state.rename(rhs, ns, goto_symex_statet::L1);
+    state.rename<goto_symex_statet::L1>(rhs, ns);
     state.value_set.assign(ssa, rhs, ns, true, false);
   }