Make rename_level2 return a level2t

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

@@ -62,11 +62,8 @@ bool scratch_programt::check_sat(bool do_slice)
 
 exprt scratch_programt::eval(const exprt &e)
 {
-  exprt ssa=e;
+  return checker->get(symex_state.rename_level2(e, ns).expr);
 
-  symex_state.rename_level2(ssa, ns);
-
-  return checker->get(ssa);
 }
 
 void scratch_programt::append(goto_programt::instructionst &new_instructions)

src/goto-symex/goto_symex_state.cpp

@@ -414,8 +414,38 @@ level1t<exprt> goto_symex_statet::rename_level1(
   }
 }
 
-void goto_symex_statet::rename_level2(
-  exprt &expr,
+level2t<ssa_exprt> goto_symex_statet::rename_level2(
+  ssa_exprt ssa,
+  const namespacet &ns)
+{
+  set_l1_indices(level0, level1, ssa, source.thread_nr, ns);
+  rename(ssa.type(), ssa.get_identifier(), ns);
+  ssa.update_type();
+
+  if(l2_thread_read_encoding(ssa, ns))
+  {
+    // renaming taken care of by l2_thread_encoding
+  }
+  else if(!ssa.get_level_2().empty())
+  {
+    // already at L2
+  }
+  else
+  {
+    // We also consider propagation if we go up to L2.
+    // L1 identifiers are used for propagation!
+    auto p_it = propagation.find(ssa.get_identifier());
+
+    if(p_it != propagation.end())
+      ssa = to_ssa_expr(p_it->second); // already L2
+    else
+      set_l2_indices(level0, level1, level2, ssa, source.thread_nr, ns);
+  }
+  return level2t<ssa_exprt>{ssa};
+}
+
+level2t<exprt> goto_symex_statet::rename_level2(
+  exprt expr,
   const namespacet &ns)
 {
   // rename all the symbols with their last known value
@@ -457,12 +487,12 @@ void goto_symex_statet::rename_level2(
         to_symbol_expr(expr).get_identifier(),
         ns,
         L2);
-
-      return;
     }
-
-    expr=ssa_exprt(expr);
-    rename_level2(expr, ns);
+    else
+    {
+      expr=ssa_exprt(expr);
+      return rename_level2(expr, ns);
+    }
   }
   else if(expr.id()==ID_address_of)
   {
@@ -476,10 +506,12 @@ void goto_symex_statet::rename_level2(
     rename(expr.type(), irep_idt(), ns, L2);
 
     // do this recursively
-    Forall_operands(it, expr)rename_level2(*it, ns);
+    Forall_operands(it, expr)
+        *it = rename_level2(std::move(*it), ns).expr;
 
     fix_type(expr);
   }
+  return level2t<exprt>{expr};
 }
 
 /// thread encoding
@@ -770,7 +802,7 @@ void goto_symex_statet::rename(
     if(level == L1)
       e = rename_level1(e, ns).expr;
     else
-      rename_level2(e, ns);
+      e = rename_level2(e, ns).expr;
   };
 
   // rename all the symbols with their last known value

src/goto-symex/goto_symex_state.h

@@ -76,7 +76,8 @@ class goto_symex_statet final
   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);
+  level2t<exprt> rename_level2(exprt expr, const namespacet &ns);
+  level2t<ssa_exprt> rename_level2(ssa_exprt ssa, const namespacet &ns);
   void rename(
     typet &type,
     const irep_idt &l1_identifier,

src/goto-symex/renaming_level.h

@@ -71,6 +71,16 @@ struct level1t
   underlyingt expr;
 };
 
+/// Wrapper for expressions that have been renamed at level2
+template<typename underlyingt>
+struct level2t
+{
+  static_assert(
+    std::is_base_of<exprt, underlyingt>::value,
+    "underlyingt should inherit from exprt");
+  underlyingt expr;
+};
+
 inline level1t<ssa_exprt> remove_level2(ssa_exprt ssa)
 {
   ssa.remove_level_2();

src/goto-symex/symex_assign.cpp

@@ -212,13 +212,13 @@ void goto_symext::symex_assign_symbol(
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
-  state.rename_level2(ssa_rhs, ns);
-  do_simplify(ssa_rhs);
+  level2t<exprt> l2_rhs = state.rename_level2(ssa_rhs, ns);
+  do_simplify(l2_rhs.expr);
 
   ssa_exprt ssa_lhs=lhs;
   state.assignment(
     ssa_lhs,
-    ssa_rhs,
+    l2_rhs.expr,
     ns,
     symex_config.simplify_opt,
     symex_config.constant_propagation,
@@ -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_level2(ssa_full_lhs, ns);
+  level2t<exprt> l2_full_lhs = state.rename_level2(ssa_full_lhs, ns);
   state.record_events=record_events;
 
   guardt tmp_guard(state.guard);
@@ -254,8 +254,9 @@ void goto_symext::symex_assign_symbol(
   target.assignment(
     tmp_guard.as_expr(),
     ssa_lhs,
-    ssa_full_lhs, add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
-    ssa_rhs,
+    l2_full_lhs.expr,
+    add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
+    l2_rhs.expr,
     state.source,
     assignment_type);
 }
@@ -407,21 +408,20 @@ void goto_symext::symex_assign_if(
 
   guardt old_guard=guard;
 
-  exprt renamed_guard=lhs.cond();
-  state.rename_level2(renamed_guard, ns);
-  do_simplify(renamed_guard);
+  level2t<exprt> renamed_guard = state.rename_level2(lhs.cond(), ns);
+  do_simplify(renamed_guard.expr);
 
-  if(!renamed_guard.is_false())
+  if(!renamed_guard.expr.is_false())
   {
-    guard.add(renamed_guard);
+    guard.add(renamed_guard.expr);
     symex_assign_rec(
       state, lhs.true_case(), full_lhs, rhs, guard, assignment_type);
     guard = std::move(old_guard);
   }
 
-  if(!renamed_guard.is_true())
+  if(!renamed_guard.expr.is_true())
   {
-    guard.add(not_exprt(renamed_guard));
+    guard.add(not_exprt(renamed_guard.expr));
     symex_assign_rec(
       state, lhs.false_case(), full_lhs, rhs, guard, assignment_type);
     guard = std::move(old_guard);

src/goto-symex/symex_builtin_functions.cpp

@@ -69,36 +69,36 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    exprt tmp_size=size;
-    state.rename_level2(tmp_size, ns); // to allow constant propagation
-    simplify(tmp_size, ns);
+    // to allow constant propagation
+    level2t<exprt> tmp_size = state.rename_level2(size, ns);
+    simplify(tmp_size.expr, ns);
 
     // special treatment for sizeof(T)*x
     {
-      const auto tmp_type = c_sizeof_type_rec(tmp_size);
+      const auto tmp_type = c_sizeof_type_rec(tmp_size.expr);
 
       if(tmp_type.has_value())
       {
         // Did the size get multiplied?
         auto elem_size = pointer_offset_size(*tmp_type, ns);
-        const auto alloc_size = numeric_cast<mp_integer>(tmp_size);
+        const auto alloc_size = numeric_cast<mp_integer>(tmp_size.expr);
 
         if(!elem_size.has_value() || *elem_size==0)
         {
         }
         else if(
-          !alloc_size.has_value() && tmp_size.id() == ID_mult &&
-          tmp_size.operands().size() == 2 &&
-          (tmp_size.op0().is_constant() || tmp_size.op1().is_constant()))
+          !alloc_size.has_value() && tmp_size.expr.id() == ID_mult &&
+          tmp_size.expr.operands().size() == 2 &&
+          (tmp_size.expr.op0().is_constant() || tmp_size.expr.op1().is_constant()))
         {
-          exprt s=tmp_size.op0();
+          exprt s=tmp_size.expr.op0();
           if(s.is_constant())
           {
-            s=tmp_size.op1();
-            PRECONDITION(*c_sizeof_type_rec(tmp_size.op0()) == *tmp_type);
+            s=tmp_size.expr.op1();
+            PRECONDITION(*c_sizeof_type_rec(tmp_size.expr.op0()) == *tmp_type);
           }
           else
-            PRECONDITION(*c_sizeof_type_rec(tmp_size.op1()) == *tmp_type);
+            PRECONDITION(*c_sizeof_type_rec(tmp_size.expr.op1()) == *tmp_type);
 
           object_type = array_typet(*tmp_type, s);
         }
@@ -112,14 +112,14 @@ void goto_symext::symex_allocate(
 
             if(elements * (*elem_size) == *alloc_size)
               object_type =
-                array_typet(*tmp_type, from_integer(elements, tmp_size.type()));
+                array_typet(*tmp_type, from_integer(elements, tmp_size.expr.type()));
           }
         }
       }
     }
 
     if(!object_type.has_value())
-      object_type=array_typet(unsigned_char_type(), tmp_size);
+      object_type=array_typet(unsigned_char_type(), tmp_size.expr);
 
     // we introduce a fresh symbol for the size
     // to prevent any issues of the size getting ever changed
@@ -135,7 +135,7 @@ void goto_symext::symex_allocate(
       size_symbol.base_name=
         "dynamic_object_size"+std::to_string(dynamic_counter);
       size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
-      size_symbol.type=tmp_size.type();
+      size_symbol.type=tmp_size.expr.type();
       size_symbol.mode = mode;
       size_symbol.type.set(ID_C_constant, true);
       size_symbol.value = array_size;
@@ -161,14 +161,14 @@ void goto_symext::symex_allocate(
 
   state.symbol_table.add(value_symbol);
 
-  exprt zero_init=code.op1();
-  state.rename_level2(zero_init, ns); // to allow constant propagation
-  simplify(zero_init, ns);
+  // to allow constant propagation
+  level2t<exprt> zero_init = state.rename_level2(code.op1(), ns);
+  simplify(zero_init.expr, ns);
 
   INVARIANT(
-    zero_init.is_constant(), "allocate expects constant as second argument");
+    zero_init.expr.is_constant(), "allocate expects constant as second argument");
 
-  if(!zero_init.is_zero() && !zero_init.is_false())
+  if(!zero_init.expr.is_zero() && !zero_init.expr.is_false())
   {
     const auto zero_value =
       zero_initializer(*object_type, code.source_location(), ns);
@@ -231,10 +231,10 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   if(lhs.is_nil())
     return; // ignore
 
-  exprt tmp=code.op0();
-  state.rename_level2(tmp, ns); // to allow constant propagation
-  do_simplify(tmp);
-  irep_idt id=get_symbol(tmp);
+  // to allow constant propagation
+  level2t<exprt> tmp = state.rename_level2(code.op0(), ns);
+  do_simplify(tmp.expr);
+  irep_idt id=get_symbol(tmp.expr);
 
   const auto zero = zero_initializer(lhs.type(), code.source_location(), ns);
   CHECK_RETURN(zero.has_value());
@@ -309,11 +309,10 @@ void goto_symext::symex_printf(
 {
   PRECONDITION(!rhs.operands().empty());
 
-  exprt tmp_rhs=rhs;
-  state.rename_level2(tmp_rhs, ns);
-  do_simplify(tmp_rhs);
+  level2t<exprt> tmp_rhs = state.rename_level2(rhs, ns);
+  do_simplify(tmp_rhs.expr);
 
-  const exprt::operandst &operands=tmp_rhs.operands();
+  const exprt::operandst &operands=tmp_rhs.expr.operands();
   std::list<exprt> args;
 
   for(std::size_t i=1; i<operands.size(); i++)
@@ -334,20 +333,19 @@ void goto_symext::symex_input(
 {
   PRECONDITION(code.operands().size() >= 2);
 
-  exprt id_arg=code.op0();
-
-  state.rename_level2(id_arg, ns);
+  level2t<exprt> id_arg = state.rename_level2(code.op0(), ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     args.push_back(code.operands()[i]);
-    state.rename_level2(args.back(), ns);
-    do_simplify(args.back());
+    level2t<exprt> l2_arg = state.rename_level2(args.back(), ns);
+    do_simplify(l2_arg.expr);
+    args.back() = std::move(l2_arg.expr);
   }
 
-  const irep_idt input_id=get_string_argument(id_arg, ns);
+  const irep_idt input_id=get_string_argument(id_arg.expr, ns);
 
   target.input(state.guard.as_expr(), state.source, input_id, args);
 }
@@ -357,21 +355,19 @@ void goto_symext::symex_output(
   const codet &code)
 {
   PRECONDITION(code.operands().size() >= 2);
-
-  exprt id_arg=code.op0();
-
-  state.rename_level2(id_arg, ns);
+  level2t<exprt> id_arg = state.rename_level2(code.op0(), ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     args.push_back(code.operands()[i]);
-    state.rename_level2(args.back(), ns);
-    do_simplify(args.back());
+    level2t<exprt> l2_arg = state.rename_level2(args.back(), ns);
+    do_simplify(l2_arg.expr);
+    args.back() = std::move(l2_arg.expr);
   }
 
-  const irep_idt output_id=get_string_argument(id_arg, ns);
+  const irep_idt output_id=get_string_argument(id_arg.expr, ns);
 
   target.output(state.guard.as_expr(), state.source, output_id, args);
 }
@@ -480,9 +476,8 @@ void goto_symext::symex_trace(
 
     for(std::size_t j=2; j<code.arguments().size(); j++)
     {
-      exprt var(code.arguments()[j]);
-      state.rename_level2(var, ns);
-      vars.push_back(var);
+      level2t<exprt> var = state.rename_level2(code.arguments()[j], ns);
+      vars.push_back(var.expr);
     }
 
     target.output(state.guard.as_expr(), state.source, event, vars);