From 365f246775483b6320b605c034b3178c0a9485a0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Jan 2019 18:35:52 +0000 Subject: [PATCH 1/2] Clarify comments in symex_dead Try to make clearer what we can(not) remove from renaming maps. Also do small cleanups of the code. --- src/goto-symex/symex_dead.cpp | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index f954f3c1131..f274086ed6b 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" -#include - #include #include @@ -23,9 +21,6 @@ void goto_symext::symex_dead(statet &state) const code_deadt &code = instruction.get_dead(); - // We increase the L2 renaming to make these non-deterministic. - // We also prevent propagation of old values. - ssa_exprt ssa = state.rename_ssa(ssa_exprt{code.symbol()}, ns); // in case of pointers, put something into the value set @@ -43,10 +38,13 @@ void goto_symext::symex_dead(statet &state) const irep_idt &l1_identifier = ssa.get_identifier(); - // prevent propagation + // we cannot remove the object from the L1 renaming map, because L1 renaming + // information is not local to a path, but removing it from the propagation + // map is safe as 1) it is local to a path and 2) this instance can no longer + // appear state.propagation.erase(l1_identifier); - - // L2 renaming + // increment the L2 index to ensure a merge on join points will propagate the + // value for branches that are still live auto level2_it = state.level2.current_names.find(l1_identifier); if(level2_it != state.level2.current_names.end()) symex_renaming_levelt::increase_counter(level2_it); From a397a58be580dac27a7c9f47b15cab7232a8b0d3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 27 Jan 2019 20:16:41 +0000 Subject: [PATCH 2/2] L1 renaming at each declaration This was done up until c8f0f7b7e77c6d0bf872ef4e3c91bfa6c5c692b4. The (observable) problem tackled here is that objects declared in loops got the same L1 name, which implies they had the same address. Thus objects were spuriously reported as dead when their address was taken, because a pointer to the latest (live) object would be the same as one to an earlier (genuinely dead) object. A side effect of this change is objects generated for test suites now have L1 indices, as witnessed in the pointer-function-parameters test. --- .../pointer-function-parameters/test.desc | 4 +- regression/cbmc/Local_out_of_scope4/main.c | 10 ++++ regression/cbmc/Local_out_of_scope4/test.desc | 8 +++ regression/cbmc/vla3/test.desc | 3 +- src/goto-programs/goto_clean_expr.cpp | 3 +- src/goto-symex/goto_symex_state.cpp | 26 ++++++++ src/goto-symex/goto_symex_state.h | 8 ++- src/goto-symex/path_storage.h | 14 +++++ src/goto-symex/symex_decl.cpp | 27 +++++---- src/goto-symex/symex_function_call.cpp | 60 ++++--------------- src/goto-symex/symex_start_thread.cpp | 4 +- 11 files changed, 95 insertions(+), 72 deletions(-) create mode 100644 regression/cbmc/Local_out_of_scope4/main.c create mode 100644 regression/cbmc/Local_out_of_scope4/test.desc diff --git a/regression/cbmc-cover/pointer-function-parameters/test.desc b/regression/cbmc-cover/pointer-function-parameters/test.desc index 8070ac7cbbb..46e8ef03507 100644 --- a/regression/cbmc-cover/pointer-function-parameters/test.desc +++ b/regression/cbmc-cover/pointer-function-parameters/test.desc @@ -4,8 +4,8 @@ main.c ^\*\* 5 of 5 covered \(100\.0%\)$ ^Test suite:$ ^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$ -^(a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0)$ -^(a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0)$ +^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0@1)$ +^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0@1)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/Local_out_of_scope4/main.c b/regression/cbmc/Local_out_of_scope4/main.c new file mode 100644 index 00000000000..24db40a0a3d --- /dev/null +++ b/regression/cbmc/Local_out_of_scope4/main.c @@ -0,0 +1,10 @@ +int g; + +int main() +{ + for(int i = 0; i < 4; ++i) + { + int *x; + *&x = &g; + } +} diff --git a/regression/cbmc/Local_out_of_scope4/test.desc b/regression/cbmc/Local_out_of_scope4/test.desc new file mode 100644 index 00000000000..39c491ba8bb --- /dev/null +++ b/regression/cbmc/Local_out_of_scope4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/vla3/test.desc b/regression/cbmc/vla3/test.desc index 44ce0e9d192..9ad552b679b 100644 --- a/regression/cbmc/vla3/test.desc +++ b/regression/cbmc/vla3/test.desc @@ -7,5 +7,4 @@ main.c -- ^warning: ignoring -- -Renaming is inconsistent across loop iterations as we map L1 names to types, but -do not actually introduce new L1 ids each time we declare an object. +The array decision procedure does not yet handle member expressions. diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index 0967f96c773..8222a5f901e 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -45,7 +45,8 @@ symbol_exprt goto_convertt::make_compound_literal( // The lifetime of compound literals is really that of // the block they are in. - copy(code_declt(result), DECL, dest); + if(!new_symbol.is_static_lifetime) + copy(code_declt(result), DECL, dest); code_assignt code_assign(result, expr); code_assign.add_source_location()=source_location; diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 69b1151cba2..6e9283025be 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -766,3 +766,29 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const << frame.calling_location.pc->location_number << "\n"; } } + +void goto_symex_statet::add_object( + ssa_exprt &ssa, + std::size_t l1_index, + const namespacet &ns) +{ + framet &frame = call_stack().top(); + + const irep_idt l0_name = ssa.get_identifier(); + + // save old L1 name, if any + auto existing_or_new_entry = level1.current_names.emplace( + std::piecewise_construct, + std::forward_as_tuple(l0_name), + std::forward_as_tuple(ssa, l1_index)); + + if(!existing_or_new_entry.second) + { + frame.old_level1.emplace(l0_name, existing_or_new_entry.first->second); + existing_or_new_entry.first->second = std::make_pair(ssa, l1_index); + } + + ssa = rename_ssa(std::move(ssa), ns); + const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second; + INVARIANT(inserted, "l1_name expected to be unique by construction"); +} diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 044479cff71..88a0c8549a3 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -60,9 +60,6 @@ class goto_symex_statet final : public goto_statet symex_target_equationt *symex_target; - // we remember all L1 renamings - std::set l1_history; - symex_level0t level0; symex_level1t level1; @@ -141,6 +138,11 @@ class goto_symex_statet final : public goto_statet return threads[source.thread_nr].call_stack; } + /// Create a new instance of the L0-renamed object \p ssa. As part of this, + /// turn \p ssa into an L1-renamed SSA expression. When doing so, use + /// \p l1_index as the L1 index, which must not previously have been used. + void add_object(ssa_exprt &ssa, std::size_t l1_index, const namespacet &ns); + void print_backtrace(std::ostream &) const; // threads diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h index 0742b291d67..3753263d8ea 100644 --- a/src/goto-symex/path_storage.h +++ b/src/goto-symex/path_storage.h @@ -98,11 +98,25 @@ class path_storaget /// error-handling paths. std::unordered_map safe_pointers; + /// Provide a unique index for a given \p id, starting from \p minimum_index. + std::size_t get_unique_index(const irep_idt &id, std::size_t minimum_index) + { + auto entry = unique_index_map.emplace(id, minimum_index); + + if(!entry.second) + entry.first->second = std::max(entry.first->second + 1, minimum_index); + + return entry.first->second; + } + private: // Derived classes should override these methods, allowing the base class to // enforce preconditions. virtual patht &private_peek() = 0; virtual void private_pop() = 0; + + /// Storage used by \ref get_unique_index. + std::unordered_map unique_index_map; }; /// \brief LIFO save queue: depth-first search, try to finish paths diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index e29a6d33da5..9f72ddba427 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -34,10 +34,16 @@ void goto_symext::symex_decl(statet &state) void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) { - // We increase the L2 renaming to make these non-deterministic. - // We also prevent propagation of old values. - - ssa_exprt ssa = state.rename_ssa(ssa_exprt{expr}, ns); + // each declaration introduces a new object, which we record as a fresh L1 + // index + + ssa_exprt ssa = state.rename_ssa(ssa_exprt{expr}, ns); + // We use "1" as the first level-1 index, which is in line with doing so for + // level-2 indices (but it's an arbitrary choice, we have just always been + // doing it this way). + const std::size_t fresh_l1_index = + path_storage.get_unique_index(ssa.get_identifier(), 1); + state.add_object(ssa, fresh_l1_index, ns); const irep_idt &l1_identifier = ssa.get_identifier(); // rename type to L2 @@ -57,16 +63,11 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) state.value_set.assign(ssa, l1_rhs, ns, true, false); } - // prevent propagation - state.propagation.erase(l1_identifier); - // L2 renaming - // inlining may yield multiple declarations of the same identifier - // within the same L1 context - const auto level2_it = - state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 0)) - .first; - symex_renaming_levelt::increase_counter(level2_it); + bool is_new = + state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 1)) + .second; + CHECK_RETURN(is_new); const bool record_events=state.record_events; state.record_events=false; exprt expr_l2 = state.rename(std::move(ssa), ns); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 36a27757a40..2347c464f72 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com static void locality( const irep_idt &function_identifier, goto_symext::statet &state, + path_storaget &path_storage, const goto_functionst::goto_functiont &goto_function, const namespacet &ns); @@ -307,7 +308,7 @@ void goto_symext::symex_function_call_code( framet &frame = state.call_stack().new_frame(state.source); // preserve locality of local variables - locality(identifier, state, goto_function, ns); + locality(identifier, state, path_storage, goto_function, ns); // assign actuals to formal parameters parameter_assignments(identifier, goto_function, state, arguments); @@ -383,11 +384,12 @@ void goto_symext::symex_end_of_function(statet &state) pop_frame(state); } -/// preserves locality of local variables of a given function by applying L1 -/// renaming to the local identifiers +/// Preserves locality of parameters of a given function by applying L1 +/// renaming to them. static void locality( const irep_idt &function_identifier, goto_symext::statet &state, + path_storaget &path_storage, const goto_functionst::goto_functiont &goto_function, const namespacet &ns) { @@ -395,56 +397,14 @@ static void locality( state.threads[state.source.thread_nr].function_frame[function_identifier]; frame_nr++; - std::set local_identifiers; - - get_local_identifiers(goto_function, local_identifiers); - - framet &frame = state.call_stack().top(); - - for(std::set::const_iterator - it=local_identifiers.begin(); - it!=local_identifiers.end(); - it++) + for(const auto ¶m : goto_function.parameter_identifiers) { // get L0 name ssa_exprt ssa = - state.rename_ssa(ssa_exprt{ns.lookup(*it).symbol_expr()}, ns); - const irep_idt l0_name=ssa.get_identifier(); - - // save old L1 name for popping the frame - auto c_it = state.level1.current_names.find(l0_name); - - if(c_it != state.level1.current_names.end()) - { - frame.old_level1.emplace(l0_name, c_it->second); - c_it->second = std::make_pair(ssa, frame_nr); - } - else - { - c_it = state.level1.current_names - .emplace(l0_name, std::make_pair(ssa, frame_nr)) - .first; - } - - // do L1 renaming -- these need not be unique, as - // identifiers may be shared among functions - // (e.g., due to inlining or other code restructuring) - - ssa_exprt ssa_l1 = state.rename_ssa(std::move(ssa), ns); - - irep_idt l1_name = ssa_l1.get_identifier(); - unsigned offset=0; - - while(state.l1_history.find(l1_name)!=state.l1_history.end()) - { - symex_renaming_levelt::increase_counter(c_it); - ++offset; - ssa_l1.set_level_1(frame_nr + offset); - l1_name = ssa_l1.get_identifier(); - } + state.rename_ssa(ssa_exprt{ns.lookup(param).symbol_expr()}, ns); - // now unique -- store - frame.local_objects.insert(l1_name); - state.l1_history.insert(l1_name); + const std::size_t fresh_l1_index = + path_storage.get_unique_index(ssa.get_identifier(), frame_nr); + state.add_object(ssa, fresh_l1_index, ns); } } diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index 8253890b9c6..ddae9b68886 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -66,6 +66,9 @@ void goto_symext::symex_start_thread(statet &state) // get L0 name for current thread lhs.set_level_0(t); + const irep_idt &l0_name = lhs.get_identifier(); + std::size_t l1_index = path_storage.get_unique_index(l0_name, 0); + CHECK_RETURN(l1_index == 0); // set up L1 name auto emplace_result = state.level1.current_names.emplace( @@ -76,7 +79,6 @@ void goto_symext::symex_start_thread(statet &state) const ssa_exprt lhs_l1 = state.rename_ssa(std::move(lhs), ns); const irep_idt l1_name = lhs_l1.get_l1_object_identifier(); // store it - state.l1_history.insert(l1_name); new_thread.call_stack.back().local_objects.insert(l1_name); // make copy