Make rename_level2 return a level2t

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

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

src/goto-symex/goto_symex_state.cpp

@@ -408,7 +408,37 @@ goto_symex_statet::rename_level1(exprt expr, const namespacet &ns)
   }
 }
 
-void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
+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
   if(expr.id()==ID_symbol &&
@@ -445,12 +475,12 @@ void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
     if(expr.type().id() == ID_code)
     {
       rename(expr.type(), 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)
   {
@@ -465,10 +495,11 @@ void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
 
     // do this recursively
     Forall_operands(it, expr)
-      rename_level2(*it, ns);
+      *it = rename_level2(std::move(*it), ns).expr;
 
     fix_type(expr);
   }
+  return level2t<exprt>{expr};
 }
 
 /// thread encoding
@@ -759,7 +790,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

@@ -78,7 +78,8 @@ class goto_symex_statet final
   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,37 @@ 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);
         }
@@ -111,15 +112,15 @@ void goto_symext::symex_allocate(
             mp_integer elements = *alloc_size / (*elem_size);
 
             if(elements * (*elem_size) == *alloc_size)
-              object_type =
-                array_typet(*tmp_type, from_integer(elements, tmp_size.type()));
+              object_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 +136,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 +162,15 @@ 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 +233,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 +311,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 +335,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 +357,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 +478,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);