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.

Author: tautschnig

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

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<valuest::iterator, bool> r =
-    values.insert(std::pair<irep_idt, entryt>(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->first<v_it->first)
+    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->first<it->first)
+    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,77 +379,55 @@ static std::string strip_first_field_from_suffix(
   return suffix.substr(field.length() + 1);
 }
 
-template <class maybe_const_value_sett>
-auto value_sett::get_entry_for_symbol(
-  maybe_const_value_sett &value_set,
-  const irep_idt identifier,
+optionalt<irep_idt> value_sett::get_index_of_symbol(
+  irep_idt identifier,
   const typet &type,
   const std::string &suffix,
-  const namespacet &ns) ->
-  typename std::conditional<std::is_const<maybe_const_value_sett>::value,
-                            const value_sett::entryt *,
-                            value_sett::entryt *>::type
+  const namespacet &ns) const
 {
   if(
     type.id() != ID_pointer && type.id() != ID_signedbv &&
     type.id() != ID_unsignedbv && type.id() != ID_array &&
     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);
 
     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<exprt, irep_hash> &values_to_erase)
 {
+  if(values_to_erase.empty())
+    return;
+
+  auto entry = find_entry(index);
+  if(!entry)
+    return;
+
   std::vector<object_map_dt::key_type> 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));
 }