Merge pull request #4394 from romainbrenguier/refactor/symex-rename-type-2

Make rename return a renamedt<exprt, level>

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

@@ -74,7 +74,7 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
 
 exprt scratch_programt::eval(const exprt &e)
 {
-  return checker->get(symex_state->rename<L2>(e, ns));
+  return checker->get(symex_state->rename<L2>(e, ns).get());
 }
 
 void scratch_programt::append(goto_programt::instructionst &new_instructions)

src/goto-symex/goto_symex_state.cpp

@@ -161,7 +161,7 @@ void goto_symex_statet::assignment(
   bool allow_pointer_unsoundness)
 {
   // identifier should be l0 or l1, make sure it's l1
-  lhs = rename_ssa<L1>(std::move(lhs), ns);
+  lhs = rename_ssa<L1>(std::move(lhs), ns).get();
   irep_idt l1_identifier=lhs.get_identifier();
 
   // the type might need renaming
@@ -230,25 +230,27 @@ void goto_symex_statet::assignment(
 }
 
 template <levelt level>
-ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
+renamedt<ssa_exprt, level>
+goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
 {
   static_assert(
     level == L0 || level == L1,
     "rename_ssa can only be used for levels L0 and L1");
   ssa = set_indices<level>(std::move(ssa), ns).get();
   rename<level>(ssa.type(), ssa.get_identifier(), ns);
   ssa.update_type();
-  return ssa;
+  return renamedt<ssa_exprt, level>{ssa};
 }
 
 /// Ensure `rename_ssa` gets compiled for L0
-template ssa_exprt
+template renamedt<ssa_exprt, L0>
 goto_symex_statet::rename_ssa<L0>(ssa_exprt ssa, const namespacet &ns);
-template ssa_exprt
+template renamedt<ssa_exprt, L1>
 goto_symex_statet::rename_ssa<L1>(ssa_exprt ssa, const namespacet &ns);
 
 template <levelt level>
-exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
+renamedt<exprt, level>
+goto_symex_statet::rename(exprt expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
 
@@ -259,11 +261,13 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
 
     if(level == L0)
     {
-      ssa = rename_ssa<L0>(std::move(ssa), ns);
+      return renamedt<exprt, level>{
+        std::move(rename_ssa<L0>(std::move(ssa), ns).value)};
     }
     else if(level == L1)
     {
-      ssa = rename_ssa<L1>(std::move(ssa), ns);
+      return renamedt<exprt, level>{
+        std::move(rename_ssa<L1>(std::move(ssa), ns).value)};
     }
     else if(level==L2)
     {
@@ -290,6 +294,7 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
         else
           ssa = set_indices<L2>(std::move(ssa), ns).get();
       }
+      return renamedt<exprt, level>(std::move(ssa));
     }
   }
   else if(expr.id()==ID_symbol)
@@ -298,24 +303,28 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
 
     // we never rename function symbols
     if(type.id() == ID_code || type.id() == ID_mathematical_function)
+    {
       rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
+      return renamedt<exprt, level>{std::move(expr)};
+    }
     else
-      expr = rename<level>(ssa_exprt{expr}, ns);
+      return rename<level>(ssa_exprt{expr}, ns);
   }
   else if(expr.id()==ID_address_of)
   {
     auto &address_of_expr = to_address_of_expr(expr);
     rename_address<level>(address_of_expr.object(), ns);
     to_pointer_type(expr.type()).subtype() =
       as_const(address_of_expr).object().type();
+    return renamedt<exprt, level>{std::move(expr)};
   }
   else
   {
     rename<level>(expr.type(), irep_idt(), ns);
 
     // do this recursively
     Forall_operands(it, expr)
-      *it = rename<level>(std::move(*it), ns);
+      *it = rename<level>(std::move(*it), ns).get();
 
     const exprt &c_expr = as_const(expr);
     INVARIANT(
@@ -326,11 +335,12 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
           c_expr.type() == to_if_expr(c_expr).false_case().type())),
       "Type of renamed expr should be the same as operands for with_exprt and "
       "if_exprt");
+    return renamedt<exprt, level>{std::move(expr)};
   }
-  return expr;
 }
 
-template exprt goto_symex_statet::rename<L1>(exprt expr, const namespacet &ns);
+template renamedt<exprt, L1>
+goto_symex_statet::rename<L1>(exprt expr, const namespacet &ns);
 
 /// thread encoding
 bool goto_symex_statet::l2_thread_read_encoding(
@@ -555,13 +565,14 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
       expr.type() = to_array_type(index_expr.array().type()).subtype();
 
       // the index is not an address
-      index_expr.index() = rename<level>(std::move(index_expr.index()), ns);
+      index_expr.index() =
+        rename<level>(std::move(index_expr.index()), ns).get();
     }
     else if(expr.id()==ID_if)
     {
       // the condition is not an address
       if_exprt &if_expr=to_if_expr(expr);
-      if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns);
+      if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns).get();
       rename_address<level>(if_expr.true_case(), ns);
       rename_address<level>(if_expr.false_case(), ns);
 
@@ -694,7 +705,7 @@ void goto_symex_statet::rename(
   {
     auto &array_type = to_array_type(type);
     rename<level>(array_type.subtype(), irep_idt(), ns);
-    array_type.size() = rename<level>(std::move(array_type.size()), ns);
+    array_type.size() = rename<level>(std::move(array_type.size()), ns).get();
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
@@ -707,7 +718,8 @@ void goto_symex_statet::rename(
       if(component.type().id() == ID_array)
       {
         auto &array_type = to_array_type(component.type());
-        array_type.size() = rename<level>(std::move(array_type.size()), ns);
+        array_type.size() =
+          rename<level>(std::move(array_type.size()), ns).get();
       }
       else if(component.type().id() != ID_pointer)
         rename<level>(component.type(), irep_idt(), ns);
@@ -768,7 +780,7 @@ ssa_exprt goto_symex_statet::add_object(
 {
   framet &frame = call_stack().top();
 
-  ssa_exprt ssa = rename_ssa<L0>(ssa_exprt{expr}, ns);
+  ssa_exprt ssa = rename_ssa<L0>(ssa_exprt{expr}, ns).get();
   const irep_idt l0_name = ssa.get_identifier();
   const std::size_t l1_index = index_generator(l0_name);
 
@@ -784,7 +796,7 @@ ssa_exprt goto_symex_statet::add_object(
     existing_or_new_entry.first->second = std::make_pair(ssa, l1_index);
   }
 
-  ssa = rename_ssa<L1>(std::move(ssa), ns);
+  ssa = rename_ssa<L1>(std::move(ssa), ns).get();
   const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second;
   INVARIANT(inserted, "l1_name expected to be unique by construction");
 

src/goto-symex/goto_symex_state.h

@@ -96,12 +96,12 @@ 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.
   template <levelt level = L2>
-  exprt rename(exprt expr, const namespacet &ns);
+  renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
 
   /// Version of rename which is specialized for SSA exprt.
   /// Implementation only exists for level L0 and L1.
   template <levelt level>
-  ssa_exprt rename_ssa(ssa_exprt ssa, const namespacet &ns);
+  renamedt<ssa_exprt, level> rename_ssa(ssa_exprt ssa, const namespacet &ns);
 
   template <levelt level = L2>
   void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);

src/goto-symex/renaming_level.h

@@ -16,6 +16,7 @@ Author: Romain Brenguier, [email protected]
 #include <unordered_set>
 
 #include <util/irep.h>
+#include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 
 /// Symex renaming level names.
@@ -81,14 +82,20 @@ class renamedt
     return value;
   }
 
+  void simplify(const namespacet &ns)
+  {
+    (void)::simplify(value, ns);
+  }
+
 private:
   underlyingt value;
 
   friend struct symex_level0t;
   friend struct symex_level1t;
   friend struct symex_level2t;
+  friend class goto_symex_statet;
 
-  /// Only symex_levelXt classes can create renamedt objects
+  /// Only the friend classes can create renamedt objects
   explicit renamedt(underlyingt value) : value(std::move(value))
   {
   }

src/goto-symex/symex_assign.cpp

@@ -215,7 +215,7 @@ void goto_symext::symex_assign_symbol(
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
-  exprt l2_rhs = state.rename(std::move(ssa_rhs), ns);
+  exprt l2_rhs = state.rename(std::move(ssa_rhs), ns).get();
   do_simplify(l2_rhs);
 
   ssa_exprt ssa_lhs=lhs;
@@ -231,7 +231,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(std::move(ssa_full_lhs), ns);
+  exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns).get();
   state.record_events=record_events;
 
   // do the assignment
@@ -410,7 +410,7 @@ void goto_symext::symex_assign_if(
   assignment_typet assignment_type)
 {
   // we have (c?a:b)=e;
-  exprt renamed_guard = state.rename(lhs.cond(), ns);
+  exprt renamed_guard = state.rename(lhs.cond(), ns).get();
   do_simplify(renamed_guard);
 
   if(!renamed_guard.is_false())

src/goto-symex/symex_builtin_functions.cpp

@@ -72,7 +72,7 @@ void goto_symext::symex_allocate(
   else
   {
     // to allow constant propagation
-    exprt tmp_size = state.rename(size, ns);
+    exprt tmp_size = state.rename(size, ns).get();
     simplify(tmp_size, ns);
 
     // special treatment for sizeof(T)*x
@@ -165,7 +165,7 @@ void goto_symext::symex_allocate(
   state.symbol_table.add(value_symbol);
 
   // to allow constant propagation
-  exprt zero_init = state.rename(code.op1(), ns);
+  exprt zero_init = state.rename(code.op1(), ns).get();
   simplify(zero_init, ns);
 
   INVARIANT(
@@ -234,7 +234,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
     return; // ignore
 
   // to allow constant propagation
-  exprt tmp = state.rename(code.op0(), ns);
+  exprt tmp = state.rename(code.op0(), ns).get();
   do_simplify(tmp);
   irep_idt id=get_symbol(tmp);
 
@@ -311,7 +311,7 @@ void goto_symext::symex_printf(
 {
   PRECONDITION(!rhs.operands().empty());
 
-  exprt tmp_rhs = state.rename(rhs, ns);
+  exprt tmp_rhs = state.rename(rhs, ns).get();
   do_simplify(tmp_rhs);
 
   const exprt::operandst &operands=tmp_rhs.operands();
@@ -335,13 +335,13 @@ void goto_symext::symex_input(
 {
   PRECONDITION(code.operands().size() >= 2);
 
-  exprt id_arg = state.rename(code.op0(), ns);
+  exprt id_arg = state.rename(code.op0(), ns).get();
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
-    exprt l2_arg = state.rename(code.operands()[i], ns);
+    exprt l2_arg = state.rename(code.operands()[i], ns).get();
     do_simplify(l2_arg);
     args.emplace_back(std::move(l2_arg));
   }
@@ -356,15 +356,16 @@ void goto_symext::symex_output(
   const codet &code)
 {
   PRECONDITION(code.operands().size() >= 2);
-  exprt id_arg = state.rename(code.op0(), ns);
+  exprt id_arg = state.rename(code.op0(), ns).get();
 
-  std::list<exprt> args;
+  std::list<renamedt<exprt, L2>> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
-    exprt l2_arg = state.rename(code.operands()[i], ns);
-    do_simplify(l2_arg);
-    args.emplace_back(std::move(l2_arg));
+    renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
+    if(symex_config.simplify_opt)
+      l2_arg.simplify(ns);
+    args.emplace_back(l2_arg);
   }
 
   const irep_idt output_id=get_string_argument(id_arg, ns);
@@ -470,7 +471,7 @@ void goto_symext::symex_trace(
 
   if(symex_config.debug_level >= debug_lvl)
   {
-    std::list<exprt> vars;
+    std::list<renamedt<exprt, L2>> vars;
 
     irep_idt event = to_string_constant(code.arguments()[1].op0()).get_value();
 

src/goto-symex/symex_dead.cpp

@@ -21,7 +21,7 @@ void goto_symext::symex_dead(statet &state)
 
   const code_deadt &code = instruction.get_dead();
 
-  ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns);
+  ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns).get();
   const irep_idt &l1_identifier = ssa.get_identifier();
 
   // we cannot remove the object from the L1 renaming map, because L1 renaming

src/goto-symex/symex_decl.cpp

@@ -61,7 +61,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     else
       rhs=exprt(ID_invalid);
 
-    exprt l1_rhs = state.rename<L1>(std::move(rhs), ns);
+    exprt l1_rhs = state.rename<L1>(std::move(rhs), ns).get();
     state.value_set.assign(ssa, l1_rhs, ns, true, false);
   }
 
@@ -71,7 +71,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
 
   const bool record_events=state.record_events;
   state.record_events=false;
-  exprt expr_l2 = state.rename(std::move(ssa), ns);
+  exprt expr_l2 = state.rename(std::move(ssa), ns).get();
   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

@@ -356,13 +356,13 @@ 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<L1>(expr, ns);
+  exprt l1_expr = state.rename<L1>(expr, ns).get();
 
   // start the recursion!
   dereference_rec(l1_expr, state);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
-  expr = state.rename<L1>(std::move(l1_expr), ns);
+  expr = state.rename<L1>(std::move(l1_expr), ns).get();
 
   // Dereferencing is likely to introduce new member-of-if constructs --
   // for example, "x->field" may have become "(x == &o1 ? o1 : o2).field."

src/goto-symex/symex_dereference_state.cpp

@@ -49,7 +49,7 @@ 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<L1>(ssa_exprt{sym.symbol_expr()}, ns);
+        state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns).get();
       sym.name = sym_expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;
@@ -69,7 +69,7 @@ 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<L1>(ssa_exprt{sym.symbol_expr()}, ns);
+        state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns).get();
       sym.name = sym_expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;