From 2daf787de37564154f07d5b1132b8861aa3366c7 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 d544778fc37..da3f189829d 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -44,6 +44,7 @@ ['havoc_slice', 'functional_slice_bytes.desc'], ['havoc_slice', 'functional_slice_typed.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 8cbe0038a13..b62e21471d5 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 24d9e4dc33b..9bb5d7bd331 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -388,15 +388,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> @@ -407,16 +411,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 c359168b6a0..2abb89f36c3 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -116,6 +116,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); @@ -205,7 +206,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()) { @@ -213,6 +215,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)); @@ -448,7 +454,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 1745a8e445e..86a83fa0e30 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -637,7 +637,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); + } } { @@ -646,7 +652,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; @@ -763,6 +775,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 d207762c0a4..4fd74fe14a0 100644 --- a/unit/goto-symex/apply_condition.cpp +++ b/unit/goto-symex/apply_condition.cpp @@ -61,7 +61,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{}); @@ -75,7 +75,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{}); @@ -89,7 +89,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{}); @@ -103,7 +103,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{}); @@ -117,7 +117,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{}); @@ -131,7 +131,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{}); @@ -145,7 +145,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{}); @@ -159,7 +159,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{}); @@ -173,7 +173,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{}); @@ -187,7 +187,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{}); @@ -201,7 +201,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{});