Constant propagator: improve GOTO condition propagation

This was disabled due to unspecified problems with two-way constant prop
(e.g. trying to propagate x => y and y => x when we have ASSUME(x == y)
or IF x == y THEN GOTO ...

Rather than try to fix those bugs, this provides a simpler implementation that
only propagates from constants.

Author: smowton

src/analyses/constant_propagator.cpp

@@ -113,15 +113,7 @@ void constant_propagator_domaint::transform(
     if(g.is_false())
      values.set_to_bottom();
     else
-    {
       two_way_propagate_rec(g, ns, cp);
-      // If two way propagate is enabled then it may be possible to detect
-      // that the branch condition is infeasible and thus the domain should
-      // be set to bottom.  Without it the domain will only be set to bottom
-      // if the guard expression is trivially (i.e. without context) false.
-      INVARIANT(!values.is_bottom,
-                "Without two-way propagation this should be impossible.");
-    }
   }
   else if(from->is_dead())
   {
@@ -222,7 +214,7 @@ void constant_propagator_domaint::transform(
 
 
 /// handles equalities and conjunctions containing equalities
-bool constant_propagator_domaint::two_way_propagate_rec(
+void constant_propagator_domaint::two_way_propagate_rec(
   const exprt &expr,
   const namespacet &ns,
   const constant_propagator_ait *cp)
@@ -231,42 +223,79 @@ bool constant_propagator_domaint::two_way_propagate_rec(
   std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
 #endif
 
-  bool change=false;
+  // This used to attempt to propagate equalities both ways, but the original
+  // author noted it is "buggy at the moment," so I only propagate constants
+  // onto non-constants.
 
-  // this seems to be buggy at present
-#if 0
   if(expr.id()==ID_and)
   {
-    // need a fixed point here to get the most out of it
-    do
+    forall_operands(it, expr)
+      two_way_propagate_rec(*it, ns, cp);
+  }
+  else if(expr.id() == ID_not)
+  {
+    if(expr.op0().id() == ID_equal || expr.op0().id() == ID_notequal)
     {
-      change = false;
-
-      forall_operands(it, expr)
-        if(two_way_propagate_rec(*it, ns, cp))
-          change=true;
+      exprt subexpr = expr.op0();
+      subexpr.id(subexpr.id() == ID_equal ? ID_notequal : ID_equal);
+      two_way_propagate_rec(subexpr, ns, cp);
+    }
+    else if(expr.op0().id() == ID_symbol && expr.type() == bool_typet())
+    {
+      // Treat `IF !x` like `IF x == FALSE`:
+      two_way_propagate_rec(equal_exprt(expr.op0(), false_exprt()), ns, cp);
     }
-    while(change);
   }
-  else if(expr.id()==ID_equal)
+  else if(expr.id() == ID_symbol)
   {
-    const exprt &lhs=expr.op0();
-    const exprt &rhs=expr.op1();
-
-    // two-way propagation
-    valuest copy_values=values;
-    assign_rec(copy_values, lhs, rhs, ns);
-    if(!values.is_constant(rhs) || values.is_constant(lhs))
-       assign_rec(values, rhs, lhs, ns);
-    change=values.meet(copy_values);
+    if(expr.type() == bool_typet())
+    {
+      // Treat `IF x` like `IF x == TRUE`:
+      two_way_propagate_rec(equal_exprt(expr, true_exprt()), ns, cp);
+    }
   }
-#endif
+  else if(expr.id() == ID_equal || expr.id() == ID_notequal)
+  {
+    exprt lhs = expr.op0();
+    exprt rhs = expr.op1();
 
-#ifdef DEBUG
-  std::cout << "two_way_propagate_rec: " << change << '\n';
-#endif
+    if(lhs.is_constant() && !rhs.is_constant())
+      std::swap(lhs, rhs);
+
+    if(lhs.is_constant() || !rhs.is_constant())
+      return;
 
-  return change;
+    // (int)var xx 0 ==> var xx (_Bool)0 or similar
+    // Note this is restricted to bools because in general turning a widening
+    // into a narrowing typecast is not correct.
+    if(lhs.id() == ID_typecast
+       (lhs.op0().type().id() == ID_bool || lhs.op0().type().id() == ID_c_bool))
+    {
+      rhs = typecast_exprt(rhs, lhs.op0().type());
+      simplify(rhs, ns);
+
+      lhs = lhs.op0();
+    }
+
+    if(expr.id() == ID_notequal)
+    {
+      if(lhs.type().id() != ID_bool && lhs.type().id() != ID_c_bool)
+        return;
+
+      // x != FALSE ==> x == TRUE
+
+      if(rhs.is_zero() || rhs.is_false())
+        rhs = from_integer(1, rhs.type());
+      else
+        rhs = from_integer(0, rhs.type());
+
+      two_way_propagate_rec(equal_exprt(lhs, rhs), ns, cp);
+    }
+    else // expr.id() == ID_equal
+    {
+      assign_rec(values, lhs, rhs, ns, cp);
+    }
+  }
 }
 
 /// Simplify the condition given context-sensitive knowledge from the abstract

src/analyses/constant_propagator.h

@@ -150,7 +150,7 @@ class constant_propagator_domaint:public ai_domain_baset
     const namespacet &ns,
     const constant_propagator_ait *cp);
 
-  bool two_way_propagate_rec(
+  void two_way_propagate_rec(
     const exprt &expr,
     const namespacet &ns,
     const constant_propagator_ait *cp);