From 2ae229b6de70e3c54acb64bf8b113a2f5616410f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 5 Sep 2019 11:37:24 +0100 Subject: [PATCH 1/3] 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. --- src/goto-symex/goto_state.cpp | 74 ++++++++++++++++++++++++++++++++--- src/goto-symex/symex_goto.cpp | 15 +------ 2 files changed, 71 insertions(+), 18 deletions(-) diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index dd6214f935..4803654fc5 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 6a1c5ab50c..1499666969 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. From d955e288d8f8cfbd7e34f4f7fed2914235121ea5 Mon Sep 17 00:00:00 2001 From: Owen Date: Mon, 9 Sep 2019 14:47:35 +0100 Subject: [PATCH 2/3] Unit tests for goto_state::apply_condition All the main branches are now covered --- unit/Makefile | 1 + unit/goto-symex/apply_condition.cpp | 207 ++++++++++++++++++++++++++++ 2 files changed, 208 insertions(+) create mode 100644 unit/goto-symex/apply_condition.cpp diff --git a/unit/Makefile b/unit/Makefile index 760972db0c..83d7a06c64 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 0000000000..e172e6fbae --- /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{}); + } + } +} From a2cbcc2d547af419021344f8eaa38527037b1a2b Mon Sep 17 00:00:00 2001 From: Owen Date: Mon, 9 Sep 2019 16:25:01 +0100 Subject: [PATCH 3/3] Test we don't call static initialisers unnecessarily Previously we couldn't properly track when we had definitely already called them. --- .../ClassWithStaticInit.class | Bin 0 -> 428 bytes .../ClassWithStaticInit.java | 7 +++++ .../Test.class | Bin 0 -> 821 bytes .../Test.java | 28 ++++++++++++++++++ .../test.desc | 13 ++++++++ 5 files changed, 48 insertions(+) create mode 100644 jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.class create mode 100644 jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.java create mode 100644 jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.class create mode 100644 jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.java create mode 100644 jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/test.desc 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 0000000000000000000000000000000000000000..9e003d99456f16f8cd90c5475817c7ca810e4c27 GIT binary patch literal 428 zcmZus!A^rf6r2YX3Sx_`RS(9*oAw|VZ#G_J~fyMYyUetq$2S31% zGCn9VJ@l}YAXRoreTtnm;Cl zeju~twt9+^;$B24D}x}9MH-4i*1Q!BwUi}c6iic5mJd=b=SnCU&p7gm&|4&GErcSi zID|X6vO9^>w$z#DRS_pQvaUGVl5(*U&%%X;u8R&#!f=a;;MF!i71_eSi&jajaLUUX zygb3K2N~&%Ij2zopI>6NGyVj*Mh|^fY{tjU4`94Qdu2`= bvnE$~|1~GA)AYt4(CVH|ufc4OH4TG5hgM4x literal 0 HcmV?d00001 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 0000000000..2995e0e794 --- /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 0000000000000000000000000000000000000000..440aaf986f35102b50254bd0131a36767970dd6a GIT binary patch literal 821 zcmb_ZO>fgc6r8o4ICkAOO(3L6fdT>23K0%DAQ7RW7DT1+AvH?X9FS~h)ow8{vK_=< zp?`ogAW;Mo-1$uvV%81xz!h1$@9plJ_h!aFe|`N9po?`EB{W^E;G%;fF4?&3!a~!= zs*5YQYU7$fwdJR&OfnTu(k+$xK_tflVkA)Psfo(&3z+S-p@6j+kEOt3UrprG>8n5{ z16?do>BpfT4gEyv^X$^f4phn>{eeugdqii94DFHbB?7LuT-yTkJDDH8eB!^JAxph5 znhkb$;%O4fM@o-zbf?>g{u|%J96TE>57%+Sg9BHft{*y)KiTg*_@n1xlEevTYM_mq z9@@P5S|8sqWd4#!du=b8o_@SwpIkgwKz}(_jpfa2EN~GrC9M#pS zY=t+gq}O6~n*wg}^$w|bN&GIU_gJ}s^VmWSkJ+nF)N?FjfCd6IbIG++S$R)wz%J`+ z6s;%QFiI!b6C7L5z0po|bB}:\(\)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.