From fc3dfc1b69c86a5cfa74a5325789226a524812c0 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Mon, 25 Feb 2019 16:13:55 +0000 Subject: [PATCH] Add global name map to goto_symex_state This global name map will be used to check what generation is currently available for each level1 name, and shared across all states. This will only be used when a particular state tries to find out what the next free generation is. The main draw of this is that all branches will now assign unique generations that won't clash with assignments done across other branches. One minor downside is that in VCC's the generation number might jump sporadically (say from #4 to #40). --- .../accelerate/scratch_program.cpp | 7 ++- src/goto-symex/goto_symex_state.cpp | 47 +++++++++++++------ src/goto-symex/goto_symex_state.h | 15 +++++- src/goto-symex/path_storage.h | 33 +++++++++---- src/goto-symex/renaming_level.cpp | 3 +- src/goto-symex/symex_dead.cpp | 5 +- src/goto-symex/symex_decl.cpp | 3 +- src/goto-symex/symex_function_call.cpp | 2 +- src/goto-symex/symex_main.cpp | 7 ++- src/goto-symex/symex_start_thread.cpp | 2 +- 10 files changed, 91 insertions(+), 33 deletions(-) diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index de1013574780..feaedf2482d0 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -37,7 +37,12 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager) symex_state = util_make_unique( symex_targett::sourcet(goto_functionst::entry_point(), *this), - guard_manager); + guard_manager, + [this](const irep_idt &id) + { + return path_storage.get_unique_l2_index(id); + }); + symex.symex_with_state( *symex_state, [this](const irep_idt &key) -> const goto_functionst::goto_functiont & { diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 2981ab44b08e..a71e57978e82 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -31,12 +31,14 @@ static void get_l1_name(exprt &expr); goto_symex_statet::goto_symex_statet( const symex_targett::sourcet &_source, - guard_managert &manager) + guard_managert &manager, + std::function fresh_l2_name_provider) : goto_statet(_source, manager), guard_manager(manager), symex_target(nullptr), record_events(true), - dirty() + dirty(), + fresh_l2_name_provider(fresh_l2_name_provider) { threads.emplace_back(guard_manager); call_stack().new_frame(source); @@ -212,9 +214,7 @@ void goto_symex_statet::assignment( #endif // do the l2 renaming - const auto level2_it = - level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)).first; - symex_renaming_levelt::increase_counter(level2_it); + increase_generation(l1_identifier, lhs); lhs = set_indices(std::move(lhs), ns).get(); // in case we happen to be multi-threaded, record the memory access @@ -439,10 +439,7 @@ bool goto_symex_statet::l2_thread_read_encoding( if(a_s_read.second.empty()) { - auto level2_it = - level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0)) - .first; - symex_renaming_levelt::increase_counter(level2_it); + increase_generation(l1_identifier, ssa_l1); a_s_read.first=level2.current_count(l1_identifier); } const renamedt l2_false_case = set_indices(ssa_l1, ns); @@ -476,10 +473,6 @@ bool goto_symex_statet::l2_thread_read_encoding( return true; } - const auto level2_it = - level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0)) - .first; - // No event and no fresh index, but avoid constant propagation if(!record_events) { @@ -488,7 +481,7 @@ bool goto_symex_statet::l2_thread_read_encoding( } // produce a fresh L2 name - symex_renaming_levelt::increase_counter(level2_it); + increase_generation(l1_identifier, ssa_l1); expr = set_indices(std::move(ssa_l1), ns).get(); // and record that @@ -499,6 +492,32 @@ bool goto_symex_statet::l2_thread_read_encoding( return true; } +/// Allocates a fresh L2 name for the given L1 identifier, and makes it the +/// latest generation on this path. +void goto_symex_statet::increase_generation( + const irep_idt l1_identifier, + const ssa_exprt &lhs) +{ + auto current_emplace_res = + level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)); + + current_emplace_res.first->second.second = + fresh_l2_name_provider(l1_identifier); +} + +/// Allocates a fresh L2 name for the given L1 identifier, and makes it the +/// latest generation on this path. Does nothing if there isn't an expression +/// keyed by the l1 identifier. +void goto_symex_statet::increase_generation_if_exists(const irep_idt identifier) +{ + // If we can't find the name in the local scope, this is a no-op. + auto current_names_iter = level2.current_names.find(identifier); + if(current_names_iter == level2.current_names.end()) + return; + + current_names_iter->second.second = fresh_l2_name_provider(identifier); +} + /// thread encoding bool goto_symex_statet::l2_thread_write_encoding( const ssa_exprt &expr, diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 7e8d6469cbdf..62a8c65dc1f2 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -42,7 +42,10 @@ Author: Daniel Kroening, kroening@kroening.com class goto_symex_statet final : public goto_statet { public: - goto_symex_statet(const symex_targett::sourcet &, guard_managert &manager); + goto_symex_statet( + const symex_targett::sourcet &, + guard_managert &manager, + std::function fresh_l2_name_provider); ~goto_symex_statet(); /// \brief Fake "copy constructor" that initializes the `symex_target` member @@ -197,7 +200,17 @@ class goto_symex_statet final : public goto_statet /// \brief Should the additional validation checks be run? bool run_validation_checks; + /// Allocates a fresh L2 name for the given L1 identifier, and makes it the + // latest generation on this path. + void increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs); + + /// Increases the generation of the L1 identifier. Does nothing if there + /// isn't an expression keyed by it. + void increase_generation_if_exists(const irep_idt identifier); + private: + std::function fresh_l2_name_provider; + /// \brief Dangerous, do not use /// /// Copying a state S1 to S2 risks S2 pointing to a deallocated diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h index 3753263d8ea1..4a9410a8e79d 100644 --- a/src/goto-symex/path_storage.h +++ b/src/goto-symex/path_storage.h @@ -98,15 +98,16 @@ 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) + /// Provide a unique L1 index for a given \p id, starting from + /// \p minimum_index. + std::size_t get_unique_l1_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 get_unique_index(l1_indices, id, minimum_index); + } - return entry.first->second; + std::size_t get_unique_l2_index(const irep_idt &id) + { + return get_unique_index(l2_indices, id, 1); } private: @@ -115,8 +116,24 @@ class path_storaget virtual patht &private_peek() = 0; virtual void private_pop() = 0; + typedef std::unordered_map name_index_mapt; + + std::size_t get_unique_index( + name_index_mapt &unique_index_map, + 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; + } + /// Storage used by \ref get_unique_index. - std::unordered_map unique_index_map; + name_index_mapt l1_indices; + name_index_mapt l2_indices; }; /// \brief LIFO save queue: depth-first search, try to finish paths diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index ced74b85a52a..96c065483ddb 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -73,8 +73,7 @@ operator()(renamedt l1_expr) const return renamedt{std::move(l1_expr.value)}; } -void symex_level1t::restore_from( - const symex_renaming_levelt::current_namest &other) +void symex_level1t::restore_from(const current_namest &other) { auto it = current_names.begin(); for(const auto &pair : other) diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index f274086ed6bd..57a4209d4269 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -43,9 +43,8 @@ void goto_symext::symex_dead(statet &state) // map is safe as 1) it is local to a path and 2) this instance can no longer // appear state.propagation.erase(l1_identifier); + // 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); + state.increase_generation_if_exists(l1_identifier); } diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index 31088fb9e8a1..73dd13adaba2 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -43,7 +43,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) ssa_exprt ssa = state.add_object( expr, [this](const irep_idt &l0_name) { - return path_storage.get_unique_index(l0_name, 1); + return path_storage.get_unique_l1_index(l0_name, 1); }, ns); const irep_idt &l1_identifier = ssa.get_identifier(); @@ -70,6 +70,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) 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 67dae5958acd..05f25253726f 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -402,7 +402,7 @@ static void locality( (void)state.add_object( ns.lookup(param).symbol_expr(), [&path_storage, &frame_nr](const irep_idt &l0_name) { - return path_storage.get_unique_index(l0_name, frame_nr); + return path_storage.get_unique_l1_index(l0_name, frame_nr); }, ns); } diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 159d127be306..59c0cb6a0808 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -327,7 +327,12 @@ std::unique_ptr goto_symext::initialize_entry_point_state( // create and prepare the state auto state = util_make_unique( symex_targett::sourcet(entry_point_id, start_function->body), - guard_manager); + guard_manager, + [this](const irep_idt &id) + { + return path_storage.get_unique_l2_index(id); + }); + CHECK_RETURN(!state->threads.empty()); CHECK_RETURN(!state->call_stack().empty()); diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index e4e5b8306f67..30343a54d028 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -67,7 +67,7 @@ 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); + std::size_t l1_index = path_storage.get_unique_l1_index(l0_name, 0); CHECK_RETURN(l1_index == 0); // set up L1 name