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{});