From d4b811b95ecebca3f5582962b2580eb8ad671350 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 14 Feb 2019 15:01:03 +0000 Subject: [PATCH] Use sharing_mapt as container in value_sett goto-symex copies a state, which contains a value set, at each branching point. The paths originating at that branch point typically share most of the points-to information. Thus the copy is unnecessarily expensive, and so is the merge at the next join point, which will also result in one of the value sets to be destroyed. With sharing_mapt, the copy has constant cost, merging can make use of the delta view, and the cost of destruction only depends on the size of the delta. --- src/goto-symex/symex_main.cpp | 8 +- src/pointer-analysis/value_set.cpp | 179 +++++++++----------- src/pointer-analysis/value_set.h | 69 +++----- src/pointer-analysis/value_set_analysis.cpp | 5 +- 4 files changed, 118 insertions(+), 143 deletions(-) diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 3755bcc5ca4..7b37b5238b6 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -676,16 +676,16 @@ void goto_symext::try_filter_value_sets( } if(jump_taken_value_set && !erase_from_jump_taken_value_set.empty()) { - value_sett::entryt *entry = jump_taken_value_set->get_entry_for_symbol( + auto entry_index = jump_taken_value_set->get_index_of_symbol( symbol_expr->get_identifier(), symbol_type, "", ns); jump_taken_value_set->erase_values_from_entry( - *entry, erase_from_jump_taken_value_set); + *entry_index, erase_from_jump_taken_value_set); } if(jump_not_taken_value_set && !erase_from_jump_not_taken_value_set.empty()) { - value_sett::entryt *entry = jump_not_taken_value_set->get_entry_for_symbol( + auto entry_index = jump_not_taken_value_set->get_index_of_symbol( symbol_expr->get_identifier(), symbol_type, "", ns); jump_not_taken_value_set->erase_values_from_entry( - *entry, erase_from_jump_not_taken_value_set); + *entry_index, erase_from_jump_not_taken_value_set); } } diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 3d76e386609..6a5a507ce57 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -48,19 +48,17 @@ bool value_sett::field_sensitive(const irep_idt &id, const typet &type) return type.id() == ID_struct || type.id() == ID_struct_tag; } -value_sett::entryt *value_sett::find_entry(const irep_idt &id) -{ - auto found = values.find(id); - return found == values.end() ? nullptr : &found->second; -} - const value_sett::entryt *value_sett::find_entry(const irep_idt &id) const { auto found = values.find(id); - return found == values.end() ? nullptr : &found->second; + return !found.has_value() ? nullptr : &(found->get()); } -value_sett::entryt &value_sett::get_entry(const entryt &e, const typet &type) +void value_sett::update_entry( + const entryt &e, + const typet &type, + const object_mapt &new_values, + bool add_to_sets) { irep_idt index; @@ -69,10 +67,27 @@ value_sett::entryt &value_sett::get_entry(const entryt &e, const typet &type) else index=e.identifier; - std::pair r = - values.insert(std::pair(index, e)); - - return r.first->second; + auto existing_entry = values.find(index); + if(existing_entry.has_value()) + { + entryt replacement = *existing_entry; + if(add_to_sets) + { + if(make_union(replacement.object_map, new_values)) + values.replace(index, std::move(replacement)); + } + else + { + replacement.object_map = new_values; + values.replace(index, std::move(replacement)); + } + } + else + { + entryt new_entry = e; + new_entry.object_map = new_values; + values.insert(index, std::move(new_entry)); + } } bool value_sett::insert( @@ -103,7 +118,10 @@ void value_sett::output( const namespacet &ns, std::ostream &out) const { - for(const auto &values_entry : values) + valuest::viewt view; + values.get_view(view); + + for(const auto &values_entry : view) { irep_idt identifier, display_name; @@ -210,36 +228,26 @@ bool value_sett::make_union(const value_sett::valuest &new_values) { bool result=false; - valuest::iterator v_it=values.begin(); + value_sett::valuest::delta_viewt delta_view; + + new_values.get_delta_view(values, delta_view, false); - for(valuest::const_iterator - it=new_values.begin(); - it!=new_values.end(); - ) // no it++ + for(const auto &delta_entry : delta_view) { - if(v_it==values.end() || it->firstfirst) + if(delta_entry.in_both) { - values.insert(v_it, *it); - result=true; - it++; - continue; + entryt merged_entry = *values.find(delta_entry.k); + if(make_union(merged_entry.object_map, delta_entry.m.object_map)) + { + values.replace(delta_entry.k, std::move(merged_entry)); + result = true; + } } - else if(v_it->firstfirst) + else { - v_it++; - continue; + values.insert(delta_entry.k, delta_entry.m); + result = true; } - - assert(v_it->first==it->first); - - entryt &e=v_it->second; - const entryt &new_e=it->second; - - if(make_union(e.object_map, new_e.object_map)) - result=true; - - v_it++; - it++; } return result; @@ -371,16 +379,11 @@ static std::string strip_first_field_from_suffix( return suffix.substr(field.length() + 1); } -template -auto value_sett::get_entry_for_symbol( - maybe_const_value_sett &value_set, - const irep_idt identifier, +optionalt value_sett::get_index_of_symbol( + irep_idt identifier, const typet &type, const std::string &suffix, - const namespacet &ns) -> - typename std::conditional::value, - const value_sett::entryt *, - value_sett::entryt *>::type + const namespacet &ns) const { if( type.id() != ID_pointer && type.id() != ID_signedbv && @@ -388,22 +391,23 @@ auto value_sett::get_entry_for_symbol( type.id() != ID_struct && type.id() != ID_struct_tag && type.id() != ID_union && type.id() != ID_union_tag) { - return nullptr; + return {}; } + // look it up + irep_idt index = id2string(identifier) + suffix; + auto *entry = find_entry(index); + if(entry) + return std::move(index); + const typet &followed_type = type.id() == ID_struct_tag ? ns.follow_tag(to_struct_tag_type(type)) : type.id() == ID_union_tag ? ns.follow_tag(to_union_tag_type(type)) : type; - // look it up - auto *entry = value_set.find_entry(id2string(identifier) + suffix); - // try first component name as suffix if not yet found - if( - !entry && - (followed_type.id() == ID_struct || followed_type.id() == ID_union)) + if(followed_type.id() == ID_struct || followed_type.id() == ID_union) { const struct_union_typet &struct_union_type = to_struct_union_type(followed_type); @@ -411,37 +415,19 @@ auto value_sett::get_entry_for_symbol( const irep_idt &first_component_name = struct_union_type.components().front().get_name(); - entry = value_set.find_entry( - id2string(identifier) + "." + id2string(first_component_name) + suffix); - } - - if(!entry) - { - // not found? try without suffix - entry = value_set.find_entry(identifier); + index = + id2string(identifier) + "." + id2string(first_component_name) + suffix; + entry = find_entry(index); + if(entry) + return std::move(index); } - return entry; -} - -// Explicitly instantiate the two possible versions of the method above: - -value_sett::entryt *value_sett::get_entry_for_symbol( - irep_idt identifier, - const typet &type, - const std::string &suffix, - const namespacet &ns) -{ - return get_entry_for_symbol(*this, identifier, type, suffix, ns); -} + // not found? try without suffix + entry = find_entry(identifier); + if(entry) + return std::move(identifier); -const value_sett::entryt *value_sett::get_entry_for_symbol( - irep_idt identifier, - const typet &type, - const std::string &suffix, - const namespacet &ns) const -{ - return get_entry_for_symbol(*this, identifier, type, suffix, ns); + return {}; } void value_sett::get_value_set_rec( @@ -491,11 +477,11 @@ void value_sett::get_value_set_rec( } else if(expr.id()==ID_symbol) { - const entryt *entry = get_entry_for_symbol( + auto entry_index = get_index_of_symbol( to_symbol_expr(expr).get_identifier(), expr_type, suffix, ns); - if(entry) - make_union(dest, entry->object_map); + if(entry_index.has_value()) + make_union(dest, find_entry(*entry_index)->object_map); else insert(dest, exprt(ID_unknown, original_type)); } @@ -1314,12 +1300,8 @@ void value_sett::assign_rec( { const irep_idt &identifier=to_symbol_expr(lhs).get_identifier(); - entryt &e = get_entry(entryt(identifier, suffix), lhs.type()); - - if(add_to_sets) - make_union(e.object_map, values_rhs); - else - e.object_map=values_rhs; + update_entry( + entryt{identifier, suffix}, lhs.type(), values_rhs, add_to_sets); } else if(lhs.id()==ID_dynamic_object) { @@ -1330,9 +1312,7 @@ void value_sett::assign_rec( "value_set::dynamic_object"+ std::to_string(dynamic_object.get_instance()); - entryt &e = get_entry(entryt(name, suffix), lhs.type()); - - make_union(e.object_map, values_rhs); + update_entry(entryt{name, suffix}, lhs.type(), values_rhs, true); } else if(lhs.id()==ID_dereference) { @@ -1640,12 +1620,19 @@ void value_sett::guard( } void value_sett::erase_values_from_entry( - entryt &entry, + const irep_idt &index, const std::unordered_set &values_to_erase) { + if(values_to_erase.empty()) + return; + + auto entry = find_entry(index); + if(!entry) + return; + std::vector keys_to_erase; - for(auto &key_value : entry.object_map.read()) + for(auto &key_value : entry->object_map.read()) { const auto &rhs_object = to_expr(key_value); if(values_to_erase.count(rhs_object)) @@ -1659,8 +1646,10 @@ void value_sett::erase_values_from_entry( "value_sett::erase_value_from_entry() should erase exactly one value for " "each element in the set it is given"); + entryt replacement = *entry; for(const auto &key_to_erase : keys_to_erase) { - entry.object_map.write().erase(key_to_erase); + replacement.object_map.write().erase(key_to_erase); } + values.replace(index, std::move(replacement)); } diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index 74dc870a1c8..c576f632fd9 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "object_numbering.h" #include "value_sets.h" @@ -294,11 +295,7 @@ class value_sett /// /// The components of the ID are thus duplicated in the `valuest` key and in /// `entryt` fields. -#ifdef USE_DSTRING - typedef std::map valuest; -#else - typedef std::unordered_map valuest; -#endif + typedef sharing_mapt valuest; /// Gets values pointed to by `expr`, including following dereference /// operators (i.e. this is not a simple lookup in `valuest`). @@ -318,28 +315,31 @@ class value_sett values.clear(); } - /// Finds an entry in this value-set. The interface differs from get_entry - /// because get_value_set_rec wants to check for a struct's first component - /// before stripping the suffix as is done in get_entry. + /// Finds an entry in this value-set. The interface differs from + /// \ref update_entry because get_value_set_rec wants to check for a struct's + /// first component before stripping the suffix as is done in + /// \ref update_entry. /// \param id: identifier to find. /// \return a constant pointer to an entry if found, or null otherwise. - /// Note the pointer may be invalidated by insert operations, including - /// get_entry. - entryt *find_entry(const irep_idt &id); - - /// Const version of \ref find_entry const entryt *find_entry(const irep_idt &id) const; - /// Gets or inserts an entry in this value-set. + /// Adds or replaces an entry in this value-set. /// \param e: entry to find. Its `id` and `suffix` fields will be used /// to find a corresponding entry; if a fresh entry is created its - /// `object_map` (RHS value set) will be copied; otherwise it will be - /// ignored. Therefore it should probably be left blank and any RHS updates - /// conducted against the returned reference. + /// `object_map` (RHS value set) will be merged with or replaced by \p + /// new_values, depending on the value of \p add_to_sets. If an entry + /// already exists, the object map of \p e is ignored. /// \param type: type of `e.identifier`, used to determine whether `e`'s /// suffix should be used to find a field-sensitive value-set or whether /// a single entry should be shared by all of symbol `e.identifier`. - entryt &get_entry(const entryt &e, const typet &type); + /// \param new_values: values to be stored for the entry. + /// \param add_to_sets: if true, merge in \p new_values instead of replacing + /// the existing values. + void update_entry( + const entryt &e, + const typet &type, + const object_mapt &new_values, + bool add_to_sets); /// Pretty-print this value-set /// \param ns: global namespace @@ -460,42 +460,25 @@ class value_sett exprt &expr, const namespacet &ns) const; -private: - /// Helper method for \ref get_entry_for_symbol - template - static auto get_entry_for_symbol( - maybe_const_value_sett &value_set, - irep_idt identifier, - const typet &type, - const std::string &suffix, - const namespacet &ns) -> - typename std::conditional::value, - const value_sett::entryt *, - value_sett::entryt *>::type; - -public: - /// Get the entry for the symbol and suffix + /// Get the index of the symbol and suffix /// \param identifier: The identifier for the symbol /// \param type: The type of the symbol /// \param suffix: The suffix for the entry /// \param ns: The global namespace, for following \p type if it is a /// struct tag type or a union tag type - /// \return The entry for the symbol and suffix - value_sett::entryt *get_entry_for_symbol( - irep_idt identifier, - const typet &type, - const std::string &suffix, - const namespacet &ns); - - /// const version of /ref get_entry_for_symbol - const value_sett::entryt *get_entry_for_symbol( + /// \return The index if the symbol is known, else `nullopt`. + optionalt get_index_of_symbol( irep_idt identifier, const typet &type, const std::string &suffix, const namespacet &ns) const; + /// Update the entry stored at \p index by erasing any values listed in + /// \p values_to_erase. + /// \param index: index in the value set + /// \param values_to_erase: set of values to remove from the entry void erase_values_from_entry( - entryt &entry, + const irep_idt &index, const std::unordered_set &values_to_erase); protected: diff --git a/src/pointer-analysis/value_set_analysis.cpp b/src/pointer-analysis/value_set_analysis.cpp index 59e5fa54545..39ccf846941 100644 --- a/src/pointer-analysis/value_set_analysis.cpp +++ b/src/pointer-analysis/value_set_analysis.cpp @@ -41,7 +41,10 @@ void value_sets_to_xml( xmlt &i=dest.new_element("instruction"); i.new_element()=::xml(location); - for(const auto &values_entry : value_set.values) + value_sett::valuest::viewt view; + value_set.values.get_view(view); + + for(const auto &values_entry : view) { xmlt &var=i.new_element("variable"); var.new_element("identifier").data = id2string(values_entry.first);