Maintain ID_C_expr_simplified

src/goto-symex/goto_symex.h

@@ -131,13 +131,13 @@ class goto_symext
     statet &state,
     const bool write);
 
-  void dereference_rec(
+  bool dereference_rec(
     exprt &expr,
     statet &state,
     guardt &guard,
     const bool write);
 
-  void dereference_rec_address_of(
+  bool dereference_rec_address_of(
     exprt &expr,
     statet &state,
     guardt &guard);

src/goto-symex/goto_symex_state.cpp

@@ -436,12 +436,13 @@ void goto_symex_statet::set_ssa_indices(
   }
 }
 
-void goto_symex_statet::rename(
+bool goto_symex_statet::rename(
   exprt &expr,
   const namespacet &ns,
   levelt level)
 {
   // rename all the symbols with their last known value
+  bool result=false;
 
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
@@ -476,7 +477,10 @@ void goto_symex_statet::rename(
           propagation.values.find(ssa.get_identifier());
 
         if(p_it!=propagation.values.end())
+        {
           expr=p_it->second; // already L2
+          result=true;
+        }
         else
           set_ssa_indices(ssa, ns, L2);
       }
@@ -493,16 +497,16 @@ void goto_symex_statet::rename(
         ns,
         level);
 
-      return;
+      return false;
     }
 
     expr=ssa_exprt(expr);
-    rename(expr, ns, level);
+    result=rename(expr, ns, level);
   }
   else if(expr.id()==ID_address_of)
   {
     assert(expr.operands().size()==1);
-    rename_address(expr.op0(), ns, level);
+    result=rename_address(expr.op0(), ns, level);
     assert(expr.type().id()==ID_pointer);
     expr.type().subtype()=expr.op0().type();
   }
@@ -513,7 +517,7 @@ void goto_symex_statet::rename(
 
     // do this recursively
     Forall_operands(it, expr)
-      rename(*it, ns, level);
+      result=rename(*it, ns, level) || result;
 
     // some fixes
     if(expr.id()==ID_with)
@@ -525,6 +529,11 @@ void goto_symex_statet::rename(
       expr.type()=to_if_expr(expr).true_case().type();
     }
   }
+
+  if(result)
+    expr.remove(ID_C_expr_simplified);
+
+  return result;
 }
 
 /// thread encoding
@@ -709,11 +718,13 @@ bool goto_symex_statet::l2_thread_write_encoding(
   return threads.size()>1;
 }
 
-void goto_symex_statet::rename_address(
+bool goto_symex_statet::rename_address(
   exprt &expr,
   const namespacet &ns,
   levelt level)
 {
+  bool result=false;
+
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
   {
@@ -728,36 +739,36 @@ void goto_symex_statet::rename_address(
   else if(expr.id()==ID_symbol)
   {
     expr=ssa_exprt(expr);
-    rename_address(expr, ns, level);
+    result=rename_address(expr, ns, level);
   }
   else
   {
     if(expr.id()==ID_index)
     {
       index_exprt &index_expr=to_index_expr(expr);
 
-      rename_address(index_expr.array(), ns, level);
+      result=rename_address(index_expr.array(), ns, level);
       assert(index_expr.array().type().id()==ID_array);
       expr.type()=index_expr.array().type().subtype();
 
       // the index is not an address
-      rename(index_expr.index(), ns, level);
+      result=rename(index_expr.index(), ns, level) || result;
     }
     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);
+      result=rename(if_expr.cond(), ns, level);
+      result=rename_address(if_expr.true_case(), ns, level) || result;
+      result=rename_address(if_expr.false_case(), ns, level) || result;
 
       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);
+      result=rename_address(member_expr.struct_op(), ns, level);
 
       // type might not have been renamed in case of nesting of
       // structs and pointers/arrays
@@ -781,9 +792,14 @@ void goto_symex_statet::rename_address(
       // do this recursively; we assume here
       // that all the operands are addresses
       Forall_operands(it, expr)
-        rename_address(*it, ns, level);
+        result=rename_address(*it, ns, level) || result;
     }
   }
+
+  if(result)
+    expr.remove(ID_C_expr_simplified);
+
+  return result;
 }
 
 void goto_symex_statet::rename(

src/goto-symex/goto_symex_state.h

@@ -148,7 +148,7 @@ class goto_symex_statet
   enum levelt { L0=0, L1=1, L2=2 };
 
   // performs renaming _up to_ the given level
-  void rename(exprt &expr, const namespacet &ns, levelt level=L2);
+  bool rename(exprt &expr, const namespacet &ns, levelt level=L2);
   void rename(
     typet &type,
     const irep_idt &l1_identifier,
@@ -170,7 +170,7 @@ class goto_symex_statet
   void get_original_name(exprt &expr) const;
   void get_original_name(typet &type) const;
 protected:
-  void rename_address(exprt &expr, const namespacet &ns, levelt level);
+  bool rename_address(exprt &expr, const namespacet &ns, levelt level);
 
   void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2);
   // only required for value_set.assign

src/goto-symex/symex_dereference.cpp

@@ -23,44 +23,48 @@ Author: Daniel Kroening, [email protected]
 #include "goto_symex.h"
 #include "symex_dereference_state.h"
 
-void goto_symext::dereference_rec_address_of(
+bool goto_symext::dereference_rec_address_of(
   exprt &expr,
   statet &state,
   guardt &guard)
 {
+  bool result=false;
+
   // Could be member, could be if, could be index.
 
   if(expr.id()==ID_member)
-    dereference_rec_address_of(
+    result=dereference_rec_address_of(
       to_member_expr(expr).struct_op(), state, guard);
   else if(expr.id()==ID_if)
   {
     // the condition is not an address
-    dereference_rec(
+    result=dereference_rec(
       to_if_expr(expr).cond(), state, guard, false);
 
     // add to guard?
-    dereference_rec_address_of(
-      to_if_expr(expr).true_case(), state, guard);
-    dereference_rec_address_of(
-      to_if_expr(expr).false_case(), state, guard);
+    result=dereference_rec_address_of(
+      to_if_expr(expr).true_case(), state, guard) || result;
+    result=dereference_rec_address_of(
+      to_if_expr(expr).false_case(), state, guard) || result;
   }
   else if(expr.id()==ID_index)
   {
     // the index is not an address
-    dereference_rec(
+    result=dereference_rec(
       to_index_expr(expr).index(), state, guard, false);
 
     // the array _is_ an address
-    dereference_rec_address_of(
-      to_index_expr(expr).array(), state, guard);
+    result=dereference_rec_address_of(
+      to_index_expr(expr).array(), state, guard) || result;
   }
   else
   {
     // give up and dereference
 
-    dereference_rec(expr, state, guard, false);
+    result=dereference_rec(expr, state, guard, false);
   }
+
+  return result;
 }
 
 bool goto_symext::is_index_member_symbol_if(const exprt &expr)
@@ -226,12 +230,14 @@ exprt goto_symext::address_arithmetic(
   return result;
 }
 
-void goto_symext::dereference_rec(
+bool goto_symext::dereference_rec(
   exprt &expr,
   statet &state,
   guardt &guard,
   const bool write)
 {
+  bool result=false;
+
   if(expr.id()==ID_dereference)
   {
     if(expr.operands().size()!=1)
@@ -267,6 +273,8 @@ void goto_symext::dereference_rec(
 
     // this may yield a new auto-object
     trigger_auto_object(expr, state);
+
+    result=true;
   }
   else if(expr.id()==ID_index &&
           to_index_expr(expr).array().id()==ID_member &&
@@ -291,6 +299,8 @@ void goto_symext::dereference_rec(
     dereference_rec(tmp, state, guard, write);
 
     expr.swap(tmp);
+
+    result=true;
   }
   else if(expr.id()==ID_index &&
           to_index_expr(expr).array().type().id()==ID_pointer)
@@ -307,6 +317,8 @@ void goto_symext::dereference_rec(
     const typet &expr_type=ns.follow(expr.type());
     expr=address_arithmetic(object, state, guard,
                             expr_type.subtype().id()==ID_array);
+
+    result=true;
   }
   else if(expr.id()==ID_typecast)
   {
@@ -327,17 +339,24 @@ void goto_symext::dereference_rec(
             from_integer(0, index_type())));
 
       dereference_rec(expr, state, guard, write);
+
+      result=true;
     }
     else
     {
-      dereference_rec(tc_op, state, guard, write);
+      result=dereference_rec(tc_op, state, guard, write) || result;
     }
   }
   else
   {
     Forall_operands(it, expr)
-      dereference_rec(*it, state, guard, write);
+      result=dereference_rec(*it, state, guard, write) || result;
   }
+
+  if(result)
+    expr.remove(ID_C_expr_simplified);
+
+  return result;
 }
 
 void goto_symext::dereference(

src/util/irep_ids.def

@@ -810,6 +810,7 @@ IREP_ID_ONE(cprover_string_to_upper_case_func)
 IREP_ID_ONE(cprover_string_trim_func)
 IREP_ID_ONE(cprover_string_value_of_func)
 IREP_ID_ONE(array_replace)
+IREP_ID_TWO(C_expr_simplified, #expr_simplified)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO

src/util/replace_expr.cpp

@@ -22,6 +22,9 @@ bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
   Forall_operands(it, dest)
     result=replace_expr(what, by, *it) && result;
 
+  if(!result)
+    dest.remove(ID_C_expr_simplified);
+
   return result;
 }
 
@@ -42,5 +45,8 @@ bool replace_expr(const replace_mapt &what, exprt &dest)
   Forall_operands(it, dest)
     result=replace_expr(what, *it) && result;
 
+  if(!result)
+    dest.remove(ID_C_expr_simplified);
+
   return result;
 }

src/util/replace_symbol.cpp

@@ -70,6 +70,9 @@ bool replace_symbolt::replace(exprt &dest) const
      !replace(static_cast<typet&>(dest.add(ID_C_va_arg_type))))
     result=false;
 
+  if(!result)
+    dest.remove(ID_C_expr_simplified);
+
   return result;
 }
 
@@ -162,6 +165,9 @@ bool replace_symbolt::replace(typet &dest) const
       result=false;
   }
 
+  if(!result)
+    dest.remove(ID_C_expr_simplified);
+
   return result;
 }
 

src/util/simplify_expr.cpp

@@ -2334,20 +2334,22 @@ bool simplify_exprt::simplify_rec(exprt &expr)
   exprt tmp=expr;
   bool result=true;
 
+  if(!tmp.get_bool(ID_C_expr_simplified))
+  {
   result=simplify_node_preorder(tmp);
 
   if(!simplify_node(tmp))
     result=false;
 
-  #if 1
   replace_mapt::const_iterator it=local_replace_map.find(tmp);
   if(it!=local_replace_map.end())
   {
     tmp=it->second;
     result=false;
   }
-  #else
-  if(!local_replace_map.empty() &&
+  }
+  #if 0
+  else if(!local_replace_map.empty() &&
      !replace_expr(local_replace_map, tmp))
   {
     simplify_rec(tmp);
@@ -2357,6 +2359,7 @@ bool simplify_exprt::simplify_rec(exprt &expr)
 
   if(!result)
   {
+    tmp.set(ID_C_expr_simplified, true);
     expr.swap(tmp);
 
     #ifdef USE_CACHE