[TG-9390] GOTO-symex: propagate notequal conditions for boolean types

jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.java

@@ -0,0 +1,7 @@
+public class ClassWithStaticInit {
+  public static int x;
+
+  static { x = 42; }
+
+  public static int getStaticValue() { return x; }
+}

jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.java

@@ -0,0 +1,28 @@
+public class Test {
+  public static void test(boolean b) {
+    int x;
+    if (b) {
+      x = ClassWithStaticInit.getStaticValue();
+    }
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    assert (false);
+  }
+}

jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/test.desc

@@ -0,0 +1,13 @@
+CORE
+Test.class
+--function Test.test --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+--
+^BMC at file ClassWithStaticInit.java line .* function java::ClassWithStaticInit.<clinit>:\(\)V bytecode-index .* \(depth [1-9][0-9][0-9]\)$
+^warning: ignoring
+--
+If symex isn't able to determine that the static initialiser has already been
+run after the second call to getStaticValue() then it will keep on entering the
+static initialiser, and it will eventually do so with a depth greater than or
+equal to 100.

src/goto-symex/goto_state.cpp

@@ -44,15 +44,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 +119,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.

unit/Makefile

@@ -31,6 +31,7 @@ SRC += analyses/ai/ai.cpp \
        goto-programs/osx_fat_reader.cpp \
        goto-programs/remove_returns.cpp \
        goto-programs/xml_expr.cpp \
+       goto-symex/apply_condition.cpp \
        goto-symex/expr_skeleton.cpp \
        goto-symex/goto_symex_state.cpp \
        goto-symex/ssa_equation.cpp \

unit/goto-symex/apply_condition.cpp

@@ -0,0 +1,207 @@
+/*******************************************************************\
+
+Module: Unit tests for goto_statet::apply_condition
+
+Author: Owen Mansel-Chan, [email protected]
+
+\*******************************************************************/
+
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
+
+#include <goto-symex/goto_symex.h>
+
+static void add_to_symbol_table(
+  symbol_tablet &symbol_table,
+  const symbol_exprt &symbol_expr)
+{
+  symbolt symbol;
+  symbol.name = symbol_expr.get_identifier();
+  symbol.type = symbol_expr.type();
+  symbol.value = symbol_expr;
+  symbol.is_thread_local = true;
+  symbol_table.insert(symbol);
+}
+
+SCENARIO(
+  "Apply condition and update constant propagator and value-set",
+  "[core][goto-symex][apply_condition]")
+{
+  const symbol_exprt b{"b", bool_typet{}};
+  const symbol_exprt c{"c", bool_typet{}};
+
+  // Add symbols to symbol table
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  add_to_symbol_table(symbol_table, b);
+  add_to_symbol_table(symbol_table, c);
+
+  // Initialize goto state
+  std::list<goto_programt::instructiont> target;
+  symex_targett::sourcet source{"fun", target.begin()};
+  guard_managert guard_manager;
+  std::size_t count = 0;
+  auto fresh_name = [&count](const irep_idt &) { return count++; };
+  goto_symex_statet state{source,
+                          DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
+                          guard_manager,
+                          fresh_name};
+
+  goto_statet goto_state{state};
+  const exprt renamed_b = state.rename<L2>(b, ns).get();
+  const exprt renamed_c = state.rename<L2>(c, ns).get();
+
+  WHEN("Applying the condition 'b'")
+  {
+    const exprt condition = renamed_b;
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'true'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == true_exprt{});
+    }
+  }
+
+  WHEN("Applying the condition '!b'")
+  {
+    const exprt condition = not_exprt{renamed_b};
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'false'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == false_exprt{});
+    }
+  }
+
+  WHEN("Applying the condition 'b == true'")
+  {
+    const exprt condition = equal_exprt{renamed_b, true_exprt{}};
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'true'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == true_exprt{});
+    }
+  }
+
+  WHEN("Applying the condition 'b == false'")
+  {
+    const exprt condition = equal_exprt{renamed_b, false_exprt{}};
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'false'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == false_exprt{});
+    }
+  }
+
+  WHEN("Applying the condition '!(b == true)'")
+  {
+    const exprt condition = not_exprt{equal_exprt{renamed_b, true_exprt{}}};
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'false'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == false_exprt{});
+    }
+  }
+
+  WHEN("Applying the condition '!(b == false)'")
+  {
+    const exprt condition = not_exprt{equal_exprt{renamed_b, false_exprt{}}};
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'true'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == true_exprt{});
+    }
+  }
+
+  WHEN("Applying the condition 'b != true'")
+  {
+    const exprt condition = notequal_exprt{renamed_b, true_exprt{}};
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'false'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == false_exprt{});
+    }
+  }
+
+  WHEN("Applying the condition 'b != false'")
+  {
+    const exprt condition = notequal_exprt{renamed_b, false_exprt{}};
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'true'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == true_exprt{});
+    }
+  }
+
+  WHEN("Applying the condition '!(b != true)'")
+  {
+    const exprt condition = not_exprt{notequal_exprt{renamed_b, true_exprt{}}};
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'true'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == true_exprt{});
+    }
+  }
+
+  WHEN("Applying the condition '!(b != false)'")
+  {
+    const exprt condition = not_exprt{notequal_exprt{renamed_b, false_exprt{}}};
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'false'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == false_exprt{});
+    }
+  }
+
+  WHEN("Applying the condition 'b && c'")
+  {
+    const exprt condition = and_exprt{renamed_b, renamed_c};
+    goto_state.apply_condition(condition, state, ns);
+
+    THEN("b should be in the constant propagator with value 'true'")
+    {
+      auto it = goto_state.propagation.find(
+        to_ssa_expr(renamed_b).get_l1_object_identifier());
+      REQUIRE(it);
+      REQUIRE(it->get() == true_exprt{});
+    }
+  }
+}