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

@@ -46,11 +46,71 @@ 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_notequal &&
+    to_notequal_expr(condition).lhs().type() == bool_typet())
+  {
+    // 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_true())
+      apply_condition(equal_exprt(lhs, false_exprt()), previous_state, ns);
+    else if(rhs.is_false())
+      apply_condition(equal_exprt(lhs, true_exprt()), previous_state, ns);
+  }
+  else if(
+    condition.id() == ID_not && 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(
+    condition.id() == ID_not && 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 if(condition.id() == ID_not)
+  {
+    // !A
+    // -->
+    // A == false
+    apply_condition(
+      equal_exprt(to_not_expr(condition).op(), false_exprt()),
+      previous_state,
+      ns);
+  }
+  else if(condition.id() == ID_symbol && condition.type() == bool_typet())
+  {
+    // A
+    // -->
+    // A == true
+    apply_condition(equal_exprt(condition, true_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))

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.