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/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 452e2df446a..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; @@ -55,6 +62,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/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index a0a42884a46..97d898a60df 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,35 @@ 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. +/// \return the newly allocated generation number +std::size_t 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); + + return current_emplace_res.first->second.second; +} + +/// 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..db38fbc74e3 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,24 @@ 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. + 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. + 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; + /// \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/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_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_dead.cpp b/src/goto-symex/symex_dead.cpp index f274086ed6b..a79ecd5faac 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -45,7 +45,5 @@ void goto_symext::symex_dead(statet &state) 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..a37e45f2ec4 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(); @@ -66,10 +66,9 @@ 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; 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..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); } } @@ -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_goto.cpp b/src/goto-symex/symex_goto.cpp index 2073ec5a85e..390e03896bd 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -210,17 +210,26 @@ 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); - symex_transition(state, state_pc, backward); - - // adjust guards + // 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)); + + symex_transition(state, state_pc, backward); + 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; @@ -319,20 +328,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 @@ -505,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; @@ -514,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_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..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(); @@ -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 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;