GOTO-symex: propagate notequal conditions for boolean types

Conditional branches on "x != false", as well as "x" and "!x", can and should lead to constant
propagation just as "x == true" does now. This is particularly beneficial for the
"clinit_already_run" variables that are maintained to determine if a static initialiser should
be run or not -- the current "if(already_run != true) clinit(); already_run = true;" condition
now leaves symex certain that it has been run at the bottom of the function regardless of the
already_run flag's initial value, whereas before it could remain uncertain and so explore the
static initialiser more than is necessary.

Author: smowton

src/goto-symex/goto_state.cpp

@@ -10,6 +10,7 @@ Author: Romain Brenguier, [email protected]
 #include "goto_symex_is_constant.h"
 #include "goto_symex_state.h"
 
+#include <util/arith_tools.h>
 #include <util/format_expr.h>
 
 /// Print the constant propagation map in a human-friendly format.
@@ -46,16 +47,56 @@ void goto_statet::apply_condition(
 {
   if(condition.id() == ID_and)
   {
+    // A == B && C == D && E == F ...
+    // -->
+    // Apply each condition individually
     for(const auto &op : condition.operands())
       apply_condition(op, previous_state, ns);
   }
+  else if(condition.id() == ID_not)
+  {
+    if(to_not_expr(condition).op().id() == ID_notequal)
+    {
+      // !(A != B)
+      // -->
+      // A == B
+      const auto &notequal_expr = to_notequal_expr(to_not_expr(condition).op());
+      apply_condition(
+        equal_exprt(notequal_expr.lhs(), notequal_expr.rhs()),
+        previous_state,
+        ns);
+    }
+    else if(to_not_expr(condition).op().id() == ID_equal)
+    {
+      // !(A == B)
+      // -->
+      // A != B
+      const auto &equal_expr = to_equal_expr(to_not_expr(condition).op());
+      apply_condition(
+        notequal_exprt(equal_expr.lhs(), equal_expr.rhs()), previous_state, ns);
+    }
+    else
+    {
+      // !A
+      // -->
+      // A == false
+      apply_condition(
+        equal_exprt(to_not_expr(condition).op(), false_exprt()),
+        previous_state,
+        ns);
+    }
+  }
   else if(condition.id() == ID_equal)
   {
+    // Base case: try to apply a single equality constraint
     exprt lhs = to_equal_expr(condition).lhs();
     exprt rhs = to_equal_expr(condition).rhs();
-    if(is_ssa_expr(rhs))
+    if(is_ssa_expr(skip_typecast(rhs)))
       std::swap(lhs, rhs);
 
+    lhs = skip_typecast(lhs);
+    rhs = typecast_exprt::conditional_cast(rhs, lhs.type());
+
     if(is_ssa_expr(lhs) && goto_symex_is_constantt()(rhs))
     {
       const ssa_exprt &ssa_lhs = to_ssa_expr(lhs);
@@ -84,4 +125,23 @@ void goto_statet::apply_condition(
       }
     }
   }
+  else if(
+    condition.id() == ID_notequal &&
+    skip_typecast(to_notequal_expr(condition).lhs()).type().id() == ID_c_bool)
+  {
+    // A != (true|false)
+    // -->
+    // A == (false|true)
+    exprt lhs = to_notequal_expr(condition).lhs();
+    exprt rhs = to_notequal_expr(condition).rhs();
+    if(is_ssa_expr(rhs))
+      std::swap(lhs, rhs);
+
+    if(rhs.is_zero())
+      apply_condition(equal_exprt(lhs, from_integer(1, rhs.type())), previous_state, ns);
+    else if(rhs.is_one())
+      apply_condition(equal_exprt(lhs, from_integer(0, rhs.type())), previous_state, ns);
+    else
+      UNREACHABLE;
+  }
 }

src/goto-symex/symex_goto.cpp

@@ -55,21 +55,12 @@ void goto_symext::apply_goto_condition(
 
   jump_taken_state.apply_condition(new_guard, current_state, ns);
 
-  // Try to find a negative condition that implies an equality constraint on
-  // the branch-not-taken path.
   // Could use not_exprt + simplify, but let's avoid paying that cost on quite
   // a hot path:
-  if(new_guard.id() == ID_not)
-    jump_not_taken_state.apply_condition(
-      to_not_expr(new_guard).op(), current_state, ns);
-  else if(new_guard.id() == ID_notequal)
-  {
-    auto &not_equal_expr = to_notequal_expr(new_guard);
-    jump_not_taken_state.apply_condition(
-      equal_exprt(not_equal_expr.lhs(), not_equal_expr.rhs()),
-      current_state,
-      ns);
-  }
+  exprt negated_new_guard = new_guard.id() == ID_not
+                              ? to_not_expr(new_guard).op()
+                              : not_exprt(new_guard);
+  jump_not_taken_state.apply_condition(negated_new_guard, current_state, ns);
 }
 
 /// Try to evaluate a simple pointer comparison.