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