Add an extra argument to domain_simplify so that the left hand side of assignment operations is treated differently.

Author: martin

src/analyses/ai.h

@@ -103,7 +103,8 @@ class ai_domain_baset
 
   // Used to evaluate or simplify conditions with respect to the domain
   virtual exprt domain_simplify (const exprt &condition,
-				 const namespacet &ns) const {
+				 const namespacet &ns,
+				 const bool lhs = false) const {
     return condition;
   }
 };

src/analyses/constant_propagator.cpp

@@ -334,7 +334,7 @@ void constant_propagator_domaint::assign(
 
 /*******************************************************************\
 
-Function: constant_propagator_domaint::assign
+Function: constant_propagator_domaint::domain_simplify
 
   Inputs: The condition to simplify and its namespace.
 
@@ -345,11 +345,17 @@ Function: constant_propagator_domaint::assign
 \*******************************************************************/
 
 exprt constant_propagator_domaint::domain_simplify (const exprt &condition,
-						    const namespacet &ns)
+						    const namespacet &ns,
+						    const bool lhs)
 {
-  exprt e(condition);
-  values.replace_const(e);
-  return simplify_expr(e, ns);
+  if (lhs) {
+    // For now do not simplify the left hand sides of assignments
+    return condition;
+  } else {
+    exprt e(condition);
+    values.replace_const(e);
+    return simplify_expr(e, ns);
+  }
 }
 
 /*******************************************************************\

src/analyses/constant_propagator.h

@@ -19,7 +19,7 @@ class constant_propagator_domaint:public ai_domain_baset
   virtual void transform(locationt, locationt, ai_baset &, const namespacet &);
   virtual void output(std::ostream &, const ai_baset &, const namespacet &) const;
   bool merge(const constant_propagator_domaint &, locationt, locationt);
-  virtual exprt domain_simplify (const exprt &condition, const namespacet &ns);
+  virtual exprt domain_simplify (const exprt &condition, const namespacet &ns, const bool lhs = false);
 
   struct valuest
   {

src/analyses/interval_domain.cpp

@@ -514,8 +514,14 @@ Function: interval_domaint::domain_simplify
 \*******************************************************************/
 
 exprt interval_domaint::domain_simplify (const exprt &condition,
-					 const namespacet &ns) const
+					 const namespacet &ns,
+					 const bool lhs) const
 {
+  if (lhs) {
+    // For now do not simplify the left hand side of assignments
+    return condition;
+  }
+  
   interval_domaint d(*this);
 
   //merge intervals to properly handle conjunction

src/analyses/interval_domain.h

@@ -82,7 +82,8 @@ class interval_domaint:public ai_domain_baset
   }
 
   virtual exprt domain_simplify (const exprt &condition,
-				 const namespacet &ns) const;
+				 const namespacet &ns,
+				 const bool lhs = false) const;
 
 protected:
   bool bottom;

src/goto-analyzer/static_simplifier.cpp

@@ -151,9 +151,16 @@ void static_simplifiert<analyzerT>::simplify_program()
       else if (i_it->is_assign())
       {
 	code_assignt assign(to_code_assign(i_it->code));
+
+	/*
+	** Simplification needs to be aware of which side of the
+	** expression it is handling as:
+	**   <i = 0, j = 1>  i = j
+	** should simplify to i = 1, not to 0 = 1.
+	*/
 
-	exprt simplified_lhs = domain[i_it].domain_simplify(assign.lhs(), ns);
-	exprt simplified_rhs = domain[i_it].domain_simplify(assign.rhs(), ns);
+	exprt simplified_lhs = domain[i_it].domain_simplify(assign.lhs(), ns, true);
+	exprt simplified_rhs = domain[i_it].domain_simplify(assign.rhs(), ns, false);
 
 	unsigned result = (simplified_lhs == assign.lhs() &&
 			   simplified_rhs == assign.rhs()) ? 0 : 1;