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.
@@ -44,15 +45,50 @@ void goto_statet::apply_condition(
   const goto_symex_statet &previous_state,
   const namespacet &ns)
 {
-  if(condition.id() == ID_and)
+  if(auto and_expr = expr_try_dynamic_cast<and_exprt>(condition))
   {
-    for(const auto &op : condition.operands())
+    // A == B && C == D && E == F ...
+    // -->
+    // Apply each condition individually
+    for(const auto &op : and_expr->operands())
       apply_condition(op, previous_state, ns);
   }
-  else if(condition.id() == ID_equal)
+  else if(auto not_expr = expr_try_dynamic_cast<not_exprt>(condition))
   {
-    exprt lhs = to_equal_expr(condition).lhs();
-    exprt rhs = to_equal_expr(condition).rhs();
+    const exprt &operand = not_expr->op();
+    if(auto notequal_expr = expr_try_dynamic_cast<notequal_exprt>(operand))
+    {
+      // !(A != B)
+      // -->
+      // A == B
+      apply_condition(
+        equal_exprt{notequal_expr->lhs(), notequal_expr->rhs()},
+        previous_state,
+        ns);
+    }
+    else if(auto equal_expr = expr_try_dynamic_cast<equal_exprt>(operand))
+    {
+      // !(A == B)
+      // -->
+      // A != B
+      apply_condition(
+        notequal_exprt{equal_expr->lhs(), equal_expr->rhs()},
+        previous_state,
+        ns);
+    }
+    else
+    {
+      // !A
+      // -->
+      // A == false
+      apply_condition(equal_exprt{operand, false_exprt{}}, previous_state, ns);
+    }
+  }
+  else if(auto equal_expr = expr_try_dynamic_cast<equal_exprt>(condition))
+  {
+    // Base case: try to apply a single equality constraint
+    exprt lhs = equal_expr->lhs();
+    exprt rhs = equal_expr->rhs();
     if(is_ssa_expr(rhs))
       std::swap(lhs, rhs);
 
@@ -84,4 +120,33 @@ void goto_statet::apply_condition(
       }
     }
   }
+  else if(
+    can_cast_expr<symbol_exprt>(condition) && condition.type() == bool_typet())
+  {
+    // A
+    // -->
+    // A == true
+    apply_condition(equal_exprt{condition, true_exprt()}, previous_state, ns);
+  }
+  else if(
+    can_cast_expr<notequal_exprt>(condition) &&
+    expr_checked_cast<notequal_exprt>(condition).lhs().type() == bool_typet{})
+  {
+    // A != (true|false)
+    // -->
+    // A == (false|true)
+    const notequal_exprt &notequal_expr =
+      expr_dynamic_cast<notequal_exprt>(condition);
+    exprt lhs = notequal_expr.lhs();
+    exprt rhs = notequal_expr.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
+      UNREACHABLE;
+  }
 }

src/goto-symex/symex_goto.cpp

@@ -55,21 +55,10 @@ 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);
-  }
+  const exprt negated_new_guard = boolean_negate(new_guard);
+  jump_not_taken_state.apply_condition(negated_new_guard, current_state, ns);
 }
 
 /// Try to evaluate a simple pointer comparison.