diff --git a/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.class b/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.class new file mode 100644 index 00000000000..9e003d99456 Binary files /dev/null and b/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.class differ diff --git a/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.java b/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.java new file mode 100644 index 00000000000..2995e0e7945 --- /dev/null +++ b/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; } +} diff --git a/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.class b/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.class new file mode 100644 index 00000000000..440aaf986f3 Binary files /dev/null and b/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.class differ diff --git a/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.java b/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.java new file mode 100644 index 00000000000..c20c76eee75 --- /dev/null +++ b/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); + } +} diff --git a/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/test.desc b/jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/test.desc new file mode 100644 index 00000000000..9674304640b --- /dev/null +++ b/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.:\(\)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. diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index dd6214f9351..4803654fc51 100644 --- a/src/goto-symex/goto_state.cpp +++ b/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(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(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(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(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(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(condition) && condition.type() == bool_typet()) + { + // A + // --> + // A == true + apply_condition(equal_exprt{condition, true_exprt()}, previous_state, ns); + } + else if( + can_cast_expr(condition) && + expr_checked_cast(condition).lhs().type() == bool_typet{}) + { + // A != (true|false) + // --> + // A == (false|true) + const notequal_exprt ¬equal_expr = + expr_dynamic_cast(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; + } } diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 6a1c5ab50ce..1499666969f 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/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 ¬_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. diff --git a/unit/Makefile b/unit/Makefile index 760972db0c9..83d7a06c649 100644 --- a/unit/Makefile +++ b/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 \ diff --git a/unit/goto-symex/apply_condition.cpp b/unit/goto-symex/apply_condition.cpp new file mode 100644 index 00000000000..e172e6fbae0 --- /dev/null +++ b/unit/goto-symex/apply_condition.cpp @@ -0,0 +1,207 @@ +/*******************************************************************\ + +Module: Unit tests for goto_statet::apply_condition + +Author: Owen Mansel-Chan, owen.mansel-chan@diffblue.com + +\*******************************************************************/ + +#include +#include + +#include + +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 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(b, ns).get(); + const exprt renamed_c = state.rename(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{}); + } + } +}