From 93047331787d3943d67aa4b6d36cd98a6edb33fe Mon Sep 17 00:00:00 2001 From: johndumbell Date: Mon, 25 Feb 2019 16:01:23 +0000 Subject: [PATCH 1/5] Adding move constructors --- src/goto-symex/goto_state.h | 6 ++++++ src/goto-symex/renaming_level.h | 10 ++++++++++ src/goto-symex/symex_target.h | 9 +++++++++ src/pointer-analysis/value_set.h | 5 +++++ 4 files changed, 30 insertions(+) diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h index 452e2df446a..b2ca4f47644 100644 --- a/src/goto-symex/goto_state.h +++ b/src/goto-symex/goto_state.h @@ -55,6 +55,12 @@ class goto_statet unsigned atomic_section_id = 0; /// Constructors + goto_statet() = default; + goto_statet &operator=(const goto_statet &other) = default; + goto_statet &operator=(goto_statet &&other) = default; + goto_statet(const goto_statet &other) = default; + goto_statet(goto_statet &&other) = default; + explicit goto_statet(const class goto_symex_statet &s); explicit goto_statet(guard_managert &guard_manager) diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h index 268ba69a3e7..6a8e9353289 100644 --- a/src/goto-symex/renaming_level.h +++ b/src/goto-symex/renaming_level.h @@ -32,7 +32,13 @@ enum levelt /// during symex to ensure static single assignment (SSA) form. struct symex_renaming_levelt { + symex_renaming_levelt() = default; virtual ~symex_renaming_levelt() = default; + symex_renaming_levelt & + operator=(const symex_renaming_levelt &other) = default; + symex_renaming_levelt &operator=(symex_renaming_levelt &&other) = default; + symex_renaming_levelt(const symex_renaming_levelt &other) = default; + symex_renaming_levelt(symex_renaming_levelt &&other) = default; /// Map identifier to ssa_exprt and counter typedef std::map> current_namest; @@ -125,6 +131,10 @@ struct symex_level2t : public symex_renaming_levelt symex_level2t() = default; ~symex_level2t() override = default; + symex_level2t &operator=(const symex_level2t &other) = default; + symex_level2t &operator=(symex_level2t &&other) = default; + symex_level2t(const symex_level2t &other) = default; + symex_level2t(symex_level2t &&other) = default; }; /// Undo all levels of renaming diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h index 3eddaf1dd8a..f34d4ede04a 100644 --- a/src/goto-symex/symex_target.h +++ b/src/goto-symex/symex_target.h @@ -53,6 +53,15 @@ class symex_targett pc(_goto_program.instructions.begin()) { } + + sourcet(sourcet &&other) noexcept + : thread_nr(other.thread_nr), function_id(other.function_id), pc(other.pc) + { + } + + sourcet(const sourcet &other) = default; + sourcet &operator=(const sourcet &other) = default; + sourcet &operator=(sourcet &&other) = default; }; enum class assignment_typet diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index fff3f3afa94..78e63444cd2 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -45,6 +45,11 @@ class value_sett { } + value_sett(value_sett &&other) + : location_number(other.location_number), values(std::move(other.values)) + { + } + virtual ~value_sett() = default; value_sett(const value_sett &other) = default; From 131373b256fc824a46ca9df4f24a99f2ec5e6324 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Mon, 25 Feb 2019 16:13:55 +0000 Subject: [PATCH 2/5] 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 | 6 ++- 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 | 8 +++- 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 de101357478..e9366ada31e 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -37,7 +37,11 @@ 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 a0a42884a46..b9f98e2e88c 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -31,13 +31,15 @@ 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(manager), source(_source), 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); @@ -213,9 +215,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 @@ -440,10 +440,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); @@ -477,10 +474,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) { @@ -489,7 +482,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 @@ -500,6 +493,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 778b1743ddf..833fee7df46 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 @@ -202,7 +205,17 @@ class goto_symex_statet final : public goto_statet unsigned total_vccs = 0; unsigned remaining_vccs = 0; + /// 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 3753263d8ea..4a9410a8e79 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 ced74b85a52..96c065483dd 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 f274086ed6b..57a4209d426 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 31088fb9e8a..73dd13adaba 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 67dae5958ac..05f25253726 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 159d127be30..d0e66eb15ca 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -324,10 +324,16 @@ std::unique_ptr goto_symext::initialize_entry_point_state( throw unsupported_operation_exceptiont("the program has no entry point"); } + // Get our path_storage pointer because this state will live beyond + // this instance of goto_symext, so we can't take the reference directly. + auto *storage = &path_storage; + // create and prepare the state auto state = util_make_unique( symex_targett::sourcet(entry_point_id, start_function->body), - guard_manager); + guard_manager, + [storage](const irep_idt &id) { return 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 e4e5b8306f6..30343a54d02 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 From 2baf020ff1848aebe8c1d984e0d6d80c30b9d018 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Mon, 25 Feb 2019 16:14:30 +0000 Subject: [PATCH 3/5] Optimise symex state management for straight-line code with GOTOs In the situation of merge on a state that hasn't been traversed (with a false guard) try and move the names into the destination state instead of a merge or copy operation --- src/goto-symex/goto_symex_state.cpp | 5 +++- src/goto-symex/goto_symex_state.h | 3 ++- src/goto-symex/symex_dead.cpp | 1 - src/goto-symex/symex_decl.cpp | 6 ++--- src/goto-symex/symex_goto.cpp | 42 ++++++++++++++++++++--------- 5 files changed, 38 insertions(+), 19 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index b9f98e2e88c..97d898a60df 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -495,7 +495,8 @@ bool goto_symex_statet::l2_thread_read_encoding( /// 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( +/// \return the newly allocated generation number +std::size_t goto_symex_statet::increase_generation( const irep_idt l1_identifier, const ssa_exprt &lhs) { @@ -504,6 +505,8 @@ void goto_symex_statet::increase_generation( current_emplace_res.first->second.second = fresh_l2_name_provider(l1_identifier); + + return current_emplace_res.first->second.second; } /// Allocates a fresh L2 name for the given L1 identifier, and makes it the diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 833fee7df46..6d63f48677c 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -207,7 +207,8 @@ class goto_symex_statet final : public goto_statet /// 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); + std::size_t + 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. diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index 57a4209d426..a79ecd5faac 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -43,7 +43,6 @@ 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 state.increase_generation_if_exists(l1_identifier); diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index 73dd13adaba..a37e45f2ec4 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -66,10 +66,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) } // L2 renaming - bool is_new = - state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 1)) - .second; - CHECK_RETURN(is_new); + std::size_t generation = state.increase_generation(l1_identifier, ssa); + CHECK_RETURN(generation == 1); const bool record_events=state.record_events; state.record_events=false; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 2073ec5a85e..c932f3a9eb1 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -210,7 +210,17 @@ void goto_symext::symex_goto(statet &state) // merge_gotos when we visit new_state_pc framet::goto_state_listt &goto_state_list = state.call_stack().top().goto_state_map[new_state_pc]; - goto_state_list.emplace_back(state.source, state); + + // If the guard is true (and the alternative branch unreachable) we can move + // the state in this case as it'll never be accessed on the alternate branch. + if(new_guard.is_true()) + { + goto_state_list.emplace_back(state.source, std::move(state)); + } + else + { + goto_state_list.emplace_back(state.source, state); + } symex_transition(state, state_pc, backward); @@ -319,20 +329,28 @@ void goto_symext::merge_goto( "atomic sections differ across branches", state.source.pc->source_location); - // do SSA phi functions - phi_function(goto_state, state); + if(!goto_state.guard.is_false()) + { + if(state.guard.is_false()) + { + // Important to note that we're moving into our base class here. + static_cast(state) = std::move(goto_state); + } + else + { + // do SSA phi functions + phi_function(goto_state, state); - // merge value sets - if(state.guard.is_false() && !goto_state.guard.is_false()) - state.value_set = std::move(goto_state.value_set); - else if(!goto_state.guard.is_false()) - state.value_set.make_union(goto_state.value_set); + // merge value sets + state.value_set.make_union(goto_state.value_set); - // adjust guard - state.guard|=goto_state.guard; + // adjust guard + state.guard |= goto_state.guard; - // adjust depth - state.depth=std::min(state.depth, goto_state.depth); + // adjust depth + state.depth = std::min(state.depth, goto_state.depth); + } + } } /// Applies f to `(k, ssa, i, j)` if the first map maps k to (ssa, i) and From e12ae53ecd983090f0af954717c088d8945edef4 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Fri, 1 Mar 2019 13:14:19 +0000 Subject: [PATCH 4/5] Merge 'if new_guard == true' blocks This means that the symex_transition call is duplicated, but better that one call than multiple if statements. --- src/goto-symex/symex_goto.cpp | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index c932f3a9eb1..1e31254bb47 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -211,26 +211,25 @@ void goto_symext::symex_goto(statet &state) framet::goto_state_listt &goto_state_list = state.call_stack().top().goto_state_map[new_state_pc]; - // If the guard is true (and the alternative branch unreachable) we can move - // the state in this case as it'll never be accessed on the alternate branch. + // On an unconditional GOTO we don't need our state, as it will be overwritten + // by merge_goto. Therefore we move it onto goto_state_list instead of copying + // as usual. if(new_guard.is_true()) { + // The move here only moves goto_statet, the base class of goto_symex_statet + // and not the entire thing. goto_state_list.emplace_back(state.source, std::move(state)); - } - else - { - goto_state_list.emplace_back(state.source, state); - } - symex_transition(state, state_pc, backward); + symex_transition(state, state_pc, backward); - // adjust guards - if(new_guard.is_true()) - { state.guard = guardt(false_exprt(), guard_manager); } else { + goto_state_list.emplace_back(state.source, state); + + symex_transition(state, state_pc, backward); + // produce new guard symbol exprt guard_expr; From 939a169bcb2f3b3aa3305f61884b5d03bbe8f71d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 7 Mar 2019 17:02:55 +0000 Subject: [PATCH 5/5] Symex: protect level2 We really should protect the level 2 name map to prevent "allocating" a new generation by just making one up in the local name map, cf. applying for one properly using increase_generation. --- src/goto-symex/auto_objects.cpp | 5 +++-- src/goto-symex/goto_state.h | 7 +++++++ src/goto-symex/goto_symex_state.h | 6 ++++++ src/goto-symex/symex_atomic_section.cpp | 2 +- src/goto-symex/symex_function_call.cpp | 6 +++--- src/goto-symex/symex_goto.cpp | 8 ++++---- src/goto-symex/symex_start_thread.cpp | 4 ++-- 7 files changed, 26 insertions(+), 12 deletions(-) diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp index d0f7e300727..376f8e3feda 100644 --- a/src/goto-symex/auto_objects.cpp +++ b/src/goto-symex/auto_objects.cpp @@ -91,8 +91,9 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state) if(has_prefix(id2string(symbol.base_name), "auto_object")) { // done already? - if(state.level2.current_names.find(ssa_expr.get_identifier())== - state.level2.current_names.end()) + if( + state.get_level2().current_names.find(ssa_expr.get_identifier()) == + state.get_level2().current_names.end()) { initialize_auto_object(expr, state); } diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h index b2ca4f47644..23ae0b9c14a 100644 --- a/src/goto-symex/goto_state.h +++ b/src/goto-symex/goto_state.h @@ -28,8 +28,15 @@ class goto_statet /// Distance from entry unsigned depth = 0; +protected: symex_level2t level2; +public: + const symex_level2t &get_level2() const + { + return level2; + } + /// Uses level 1 names, and is used to do dereferencing value_sett value_set; diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 6d63f48677c..db38fbc74e3 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -214,6 +214,12 @@ class goto_symex_statet final : public goto_statet /// isn't an expression keyed by it. void increase_generation_if_exists(const irep_idt identifier); + /// Drops an L1 name from the local L2 map + void drop_l1_name(symex_renaming_levelt::current_namest::const_iterator it) + { + level2.current_names.erase(it); + } + private: std::function fresh_l2_name_provider; diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp index f7721c68673..f8c14dc41c0 100644 --- a/src/goto-symex/symex_atomic_section.cpp +++ b/src/goto-symex/symex_atomic_section.cpp @@ -70,7 +70,7 @@ void goto_symext::symex_atomic_end(statet &state) for(const auto &pair : state.written_in_atomic_section) { ssa_exprt w = pair.first; - w.set_level_2(state.level2.current_count(w.get_identifier())); + w.set_level_2(state.get_level2().current_count(w.get_identifier())); // guard is the disjunction over writes PRECONDITION(!pair.second.empty()); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 05f25253726..ccc3be8d87e 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -349,8 +349,8 @@ static void pop_frame(goto_symext::statet &state) state.level1.restore_from(frame.old_level1); // clear function-locals from L2 renaming - for(auto c_it = state.level2.current_names.begin(); - c_it != state.level2.current_names.end();) // no ++c_it + for(auto c_it = state.get_level2().current_names.begin(); + c_it != state.get_level2().current_names.end();) // no ++c_it { const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier(); // could use iteration over local_objects as l1_o_id is prefix @@ -364,7 +364,7 @@ static void pop_frame(goto_symext::statet &state) } auto cur = c_it; ++c_it; - state.level2.current_names.erase(cur); + state.drop_l1_name(cur); } } diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 1e31254bb47..390e03896bd 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -522,8 +522,8 @@ void goto_symext::phi_function( statet &dest_state) { if( - goto_state.level2.current_names.empty() && - dest_state.level2.current_names.empty()) + goto_state.get_level2().current_names.empty() && + dest_state.get_level2().current_names.empty()) return; guardt diff_guard = goto_state.guard; @@ -531,8 +531,8 @@ void goto_symext::phi_function( diff_guard -= dest_state.guard; for_each2( - goto_state.level2.current_names, - dest_state.level2.current_names, + goto_state.get_level2().current_names, + dest_state.get_level2().current_names, [&](const ssa_exprt &ssa, unsigned goto_count, unsigned dest_count) { merge_names( goto_state, diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index 30343a54d02..4f4807a1674 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -52,8 +52,8 @@ void goto_symext::symex_start_thread(statet &state) // create a copy of the local variables for the new thread framet &frame = state.call_stack().top(); - for(auto c_it = state.level2.current_names.begin(); - c_it != state.level2.current_names.end(); + for(auto c_it = state.get_level2().current_names.begin(); + c_it != state.get_level2().current_names.end(); ++c_it) { const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();