From 3e18c42ae83a2c686aaadc7c60eb6cb37c748ead Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Jul 2022 14:50:14 +0000 Subject: [PATCH] goto-symex: apply_condition should not change L2 index Updating the L2 index would result in additional phi assignments, which can result in more costly verification. One such example is that the use of `i != size` instead of `i < size` in loop conditions resulted increased verification time when we would expect not-equal to be cheaper than less-than. --- regression/cbmc/apply_condition2/main.c | 12 ++++++ regression/cbmc/apply_condition2/test.desc | 12 ++++++ regression/validate-trace-xml-schema/check.py | 1 + src/goto-symex/goto_state.cpp | 9 ++--- src/goto-symex/goto_state.h | 5 ++- src/goto-symex/goto_symex.cpp | 39 ++++++++++++------- src/goto-symex/goto_symex_state.cpp | 10 ++++- src/goto-symex/symex_dead.cpp | 1 + src/goto-symex/symex_goto.cpp | 22 ++++++++++- unit/goto-symex/apply_condition.cpp | 22 +++++------ 10 files changed, 98 insertions(+), 35 deletions(-) create mode 100644 regression/cbmc/apply_condition2/main.c create mode 100644 regression/cbmc/apply_condition2/test.desc diff --git a/regression/cbmc/apply_condition2/main.c b/regression/cbmc/apply_condition2/main.c new file mode 100644 index 00000000000..c475e50ee65 --- /dev/null +++ b/regression/cbmc/apply_condition2/main.c @@ -0,0 +1,12 @@ +int main() +{ + int s; + + int i = 0; + if(i != s) + ++i; + else + __CPROVER_assert(s == 0, "constant propagate"); + + int s2 = s; +} diff --git a/regression/cbmc/apply_condition2/test.desc b/regression/cbmc/apply_condition2/test.desc new file mode 100644 index 00000000000..61849b99dc1 --- /dev/null +++ b/regression/cbmc/apply_condition2/test.desc @@ -0,0 +1,12 @@ +CORE paths-lifo-expected-failure +main.c +--program-only +s2!0@1#2 == s!0@1#1 +^EXIT=0$ +^SIGNAL=0$ +-- +ASSERT +s2!0@1#[3-9] +-- +The branch condition should yield constant propagation on s without introducing +fresh assignments to s. diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 1ee1c781abd..53f4045b65e 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -38,6 +38,7 @@ ['Quantifiers-simplify', 'simplify_not_forall.desc'], ['array-cell-sensitivity15', 'test.desc'], ['saturating_arithmetric', 'output-formula.desc'], + ['apply_condition2', 'test.desc'], # these test for invalid command line handling ['bad_option', 'test_multiple.desc'], ['bad_option', 'test.desc'], diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index fb8e382f437..c0f53059eeb 100644 --- a/src/goto-symex/goto_state.cpp +++ b/src/goto-symex/goto_state.cpp @@ -107,14 +107,11 @@ void goto_statet::apply_condition( const ssa_exprt l1_lhs = remove_level_2(ssa_lhs); const irep_idt &l1_identifier = l1_lhs.get_identifier(); - level2.increase_generation( - l1_identifier, l1_lhs, previous_state.get_l2_name_provider()); - - const auto propagation_entry = propagation.find(l1_identifier); + const auto propagation_entry = branch_propagation.find(l1_identifier); if(!propagation_entry.has_value()) - propagation.insert(l1_identifier, rhs); + branch_propagation.insert(l1_identifier, rhs); else if(propagation_entry->get() != rhs) - propagation.replace(l1_identifier, rhs); + branch_propagation.replace(l1_identifier, rhs); value_set.assign(l1_lhs, rhs, ns, true, false); } diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h index 5fa398048bc..9715e3e8cf7 100644 --- a/src/goto-symex/goto_state.h +++ b/src/goto-symex/goto_state.h @@ -68,7 +68,10 @@ class goto_statet // "constants" can include symbols, but only in the context of an address-of // op (i.e. &x can be propagated), and an address-taken thing should only be // L1. - sharing_mapt propagation; + // + // Entries in branch_propagation are local to the current branch and will + // never be merged back in phi nodes. + sharing_mapt propagation, branch_propagation; void output_propagation_map(std::ostream &); diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index f2c88ae4b1b..8eb02e59f50 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -372,15 +372,19 @@ goto_symext::try_evaluate_constant_string( return {}; } - const auto s_pointer_opt = - state.propagation.find(to_symbol_expr(content).get_identifier()); + const irep_idt &content_id = to_symbol_expr(content).get_identifier(); - if(!s_pointer_opt) - { - return {}; - } + const auto s_pointer_opt = state.propagation.find(content_id); + + if(s_pointer_opt) + return try_get_string_data_array(s_pointer_opt->get(), ns); + + const auto b_entry = state.branch_propagation.find(content_id); + + if(b_entry) + return try_get_string_data_array(b_entry->get(), ns); - return try_get_string_data_array(s_pointer_opt->get(), ns); + return {}; } std::optional> @@ -391,16 +395,25 @@ goto_symext::try_evaluate_constant(const statet &state, const exprt &expr) return {}; } - const auto constant_expr_opt = - state.propagation.find(to_symbol_expr(expr).get_identifier()); + const irep_idt &expr_id = to_symbol_expr(expr).get_identifier(); - if(!constant_expr_opt || !constant_expr_opt->get().is_constant()) + const auto constant_expr_opt = state.propagation.find(expr_id); + + if(constant_expr_opt && constant_expr_opt->get().is_constant()) { - return {}; + return std::optional>( + to_constant_expr(constant_expr_opt->get())); + } + + const auto b_entry = state.branch_propagation.find(expr_id); + + if(b_entry && b_entry->get().id() == ID_constant) + { + return std::optional>( + to_constant_expr(b_entry->get())); } - return std::optional>( - to_constant_expr(constant_expr_opt->get())); + return {}; } void goto_symext::constant_propagate_empty_string( diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 6755b5636d5..284d7883419 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -112,6 +112,7 @@ renamedt goto_symex_statet::assignment( "pointer handling for concurrency is unsound"); // Update constant propagation map -- the RHS is L2 + branch_propagation.erase_if_exists(l1_identifier); if(!is_shared && record_value && goto_symex_can_forward_propagatet(ns)(rhs)) { const auto propagation_entry = propagation.find(l1_identifier); @@ -214,7 +215,8 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) { // We also consider propagation if we go up to L2. // L1 identifiers are used for propagation! - auto p_it = propagation.find(ssa.get_identifier()); + const auto &l1_identifier = ssa.get_identifier(); + auto p_it = propagation.find(l1_identifier); if(p_it.has_value()) { @@ -222,6 +224,10 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) } else { + auto b_entry = branch_propagation.find(l1_identifier); + if(b_entry.has_value()) + return renamedt(*b_entry); + if(level == L2) ssa = set_indices(std::move(ssa), ns).get(); return renamedt(std::move(ssa)); @@ -457,7 +463,7 @@ bool goto_symex_statet::l2_thread_read_encoding( // written this object within the atomic section. We must actually do this, // because goto_state::apply_condition may have placed the latest value in // the propagation map without recording an assignment. - auto p_it = propagation.find(ssa_l1.get_identifier()); + auto p_it = branch_propagation.find(ssa_l1.get_identifier()); const exprt l2_true_case = p_it.has_value() ? *p_it : set_indices(ssa_l1, ns).get(); diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index d373a46525a..dc344236ea9 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -41,6 +41,7 @@ static void remove_l1_object_rec( state.value_set.values.erase_if_exists(l1_identifier); } state.propagation.erase_if_exists(l1_identifier); + state.branch_propagation.erase_if_exists(l1_identifier); // Remove from the local L2 renaming map; this means any reads from the dead // identifier will use generation 0 (e.g. x!N@M#0, where N and M are // positive integers), which is never defined by any write, and will be diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 404f04fec72..a5a0a850866 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -799,7 +799,13 @@ static void merge_names( if(p_it.has_value()) goto_state_rhs = *p_it; else - to_ssa_expr(goto_state_rhs).set_level_2(goto_count); + { + auto b_entry = goto_state.branch_propagation.find(l1_identifier); + if(b_entry.has_value()) + goto_state_rhs = *b_entry; + else + to_ssa_expr(goto_state_rhs).set_level_2(goto_count); + } } { @@ -808,7 +814,13 @@ static void merge_names( if(p_it.has_value()) dest_state_rhs = *p_it; else - to_ssa_expr(dest_state_rhs).set_level_2(dest_count); + { + auto b_entry = dest_state.branch_propagation.find(l1_identifier); + if(b_entry.has_value()) + dest_state_rhs = *b_entry; + else + to_ssa_expr(dest_state_rhs).set_level_2(dest_count); + } } exprt rhs; @@ -921,6 +933,12 @@ void goto_symext::phi_function( goto_count, dest_count); } + + sharing_mapt::delta_viewt bp_delta_view = + dest_state.branch_propagation.get_delta_view( + goto_state.branch_propagation, false); + for(const auto &delta_item : bp_delta_view) + dest_state.branch_propagation.erase(delta_item.k); } void goto_symext::loop_bound_exceeded( diff --git a/unit/goto-symex/apply_condition.cpp b/unit/goto-symex/apply_condition.cpp index 9c22a88a024..42fbadcd9c6 100644 --- a/unit/goto-symex/apply_condition.cpp +++ b/unit/goto-symex/apply_condition.cpp @@ -60,7 +60,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'true'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == true_exprt{}); @@ -74,7 +74,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'false'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == false_exprt{}); @@ -88,7 +88,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'true'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == true_exprt{}); @@ -102,7 +102,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'false'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == false_exprt{}); @@ -116,7 +116,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'false'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == false_exprt{}); @@ -130,7 +130,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'true'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == true_exprt{}); @@ -144,7 +144,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'false'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == false_exprt{}); @@ -158,7 +158,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'true'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == true_exprt{}); @@ -172,7 +172,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'true'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == true_exprt{}); @@ -186,7 +186,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'false'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == false_exprt{}); @@ -200,7 +200,7 @@ SCENARIO( THEN("b should be in the constant propagator with value 'true'") { - auto it = goto_state.propagation.find( + auto it = goto_state.branch_propagation.find( to_ssa_expr(renamed_b).get_l1_object_identifier()); REQUIRE(it); REQUIRE(it->get() == true_exprt{});