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_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); 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