Remove shared_read entries from target equation when simplify removes them from an expression

Author: tautschnig

src/goto-symex/symex_assign.cpp

@@ -280,8 +280,11 @@ void goto_symext::symex_assign_symbol(
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
+  target.set_mark();
   state.rename(ssa_rhs, ns);
   do_simplify(ssa_rhs);
+  std::cerr << from_expr(ns, "", ssa_rhs) << std::endl;
+  target.remove_unused_reads(ssa_rhs);
 
   ssa_exprt ssa_lhs=lhs;
   bool required=
@@ -526,9 +529,11 @@ void goto_symext::symex_assign_if(
 
   guardt old_guard=guard;
 
+  target.set_mark();
   exprt renamed_guard=lhs.cond();
   state.rename(renamed_guard, ns);
   do_simplify(renamed_guard);
+  target.remove_unused_reads(renamed_guard);
 
   if(!renamed_guard.is_false())  
   {

src/goto-symex/symex_goto.cpp

@@ -39,6 +39,7 @@ void goto_symext::symex_goto(statet &state)
   exprt old_guard=instruction.guard;
   clean_expr(old_guard, state, false);
 
+  target.set_mark();
   exprt new_guard=old_guard;
   state.rename(new_guard, ns);
   ++four_times;
@@ -50,6 +51,7 @@ void goto_symext::symex_goto(statet &state)
   //if(four_times>LB && four_times<UB)
   //std::cerr << "simplified_new_guard: " << from_expr(ns, "", new_guard) << std::endl;
   //assert(four_times<UB);
+  target.remove_unused_reads(new_guard);
 
   if(new_guard.is_false() ||
      state.guard.is_false())
@@ -204,12 +206,14 @@ void goto_symext::symex_step_goto(statet &state, bool taken)
 
   exprt guard(instruction.guard);
   dereference(guard, state, false);
+  target.set_mark();
   state.rename(guard, ns);
 
   if(!taken) guard.make_not();
 
   state.guard.guard_expr(guard);
   do_simplify(guard);
+  target.remove_unused_reads(guard);
 
   target.assumption(state.guard.as_expr(), guard, state.source);  
 }

src/goto-symex/symex_main.cpp

@@ -62,6 +62,7 @@ void goto_symext::vcc(
   rewrite_quantifiers(expr, state);
 
   // now rename, enables propagation    
+  target.set_mark();
   state.rename(expr, ns);
 
   // now try simplifier on it
@@ -71,6 +72,7 @@ void goto_symext::vcc(
   do_simplify(expr);
   //if(three_times<4)
   //std::cerr << "simplified_vcc: " << from_expr(ns, "", expr) << std::endl;
+  target.remove_unused_reads(expr);
 
   if(expr.is_true()) return;
 
@@ -493,8 +495,10 @@ void goto_symext::symex_step(
     {
       exprt tmp=instruction.guard;
       clean_expr(tmp, state, false);
+      target.set_mark();
       state.rename(tmp, ns);
       symex_assume(state, tmp);
+      target.remove_unused_reads(tmp);
     }
 
     state.source.pc++;

src/goto-symex/symex_target.h

@@ -182,6 +182,10 @@ class symex_targett
     const exprt &guard,
     unsigned atomic_section_id,
     const sourcet &source)=0;
+
+  // cleanup unused shared memory reads
+  virtual void set_mark() {}
+  virtual void remove_unused_reads(const exprt &expr) {}
 };
 
 bool operator < (

src/goto-symex/symex_target_equation.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/i2string.h>
 #include <util/std_expr.h>
 #include <util/expr_util.h>
+#include <util/find_symbols.h>
 
 #include <langapi/language_util.h>
 #include <solvers/prop/prop_conv.h>
@@ -33,7 +34,7 @@ Function: symex_target_equationt::symex_target_equationt
 \*******************************************************************/
 
 symex_target_equationt::symex_target_equationt(
-  const namespacet &_ns):ns(_ns)
+  const namespacet &_ns):ns(_ns), mark(SSA_steps.end())
 {
 }
 
@@ -115,6 +116,42 @@ void symex_target_equationt::shared_read(
 
 /*******************************************************************\
 
+Function: symex_target_equationt::remove_unused_reads
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void symex_target_equationt::remove_unused_reads(const exprt &expr)
+{
+  find_symbols_sett symbols;
+  find_symbols(expr, symbols);
+
+  for(SSA_stepst::iterator it=mark;
+      it!=SSA_steps.end();
+      ) // no ++it
+  {
+    if(it==mark ||
+       !it->is_shared_read() ||
+       symbols.find(it->ssa_lhs.get_identifier())!=symbols.end())
+    {
+      ++it;
+      continue;
+    }
+
+    SSA_stepst::iterator next=it;
+    ++next;
+    SSA_steps.erase(it);
+    it=next;
+  }
+}
+
+/*******************************************************************\
+
 Function: symex_target_equationt::shared_write
 
   Inputs:

src/goto-symex/symex_target_equation.h

@@ -159,6 +159,14 @@ class symex_target_equationt:public symex_targett
     unsigned atomic_section_id,
     const sourcet &source);
 
+  // cleanup unused shared memory reads
+  virtual void set_mark()
+  {
+    mark=SSA_steps.end();
+    if(!SSA_steps.empty()) --mark;
+  }
+  virtual void remove_unused_reads(const exprt &expr);
+
   void convert(prop_convt &prop_conv);
   void convert_assignments(decision_proceduret &decision_procedure) const;
   void convert_decls(prop_convt &prop_conv) const;
@@ -304,6 +312,7 @@ class symex_target_equationt:public symex_targett
 
 protected:
   const namespacet &ns;
+  SSA_stepst::iterator mark;
 
   // for enforcing sharing in the expressions stored
   merged_irepst merge_irep;