Speed up erasing from value sets

Author: Owen

src/goto-symex/symex_main.cpp

@@ -606,10 +606,11 @@ void goto_symext::try_filter_value_sets(
   value_setst::valuest value_set_elements;
   original_value_set.get_value_set(*symbol_expr, value_set_elements, ns);
 
-  std::vector<exprt> delete_from_jump_taken_value_set;
-  std::vector<exprt> delete_from_jump_not_taken_value_set;
-  delete_from_jump_taken_value_set.reserve(value_set_elements.size());
-  delete_from_jump_not_taken_value_set.reserve(value_set_elements.size());
+
+  std::unordered_set<exprt, irep_hash> erase_from_jump_taken_value_set;
+  std::unordered_set<exprt, irep_hash> erase_from_jump_not_taken_value_set;
+  erase_from_jump_taken_value_set.reserve(value_set_elements.size());
+  erase_from_jump_not_taken_value_set.reserve(value_set_elements.size());
 
   // Try evaluating the condition with the symbol replaced by a pointer to each
   // one of its possible values in turn. If that leads to a true for some
@@ -667,29 +668,25 @@ void goto_symext::try_filter_value_sets(
 
     if(jump_taken_value_set && modified_condition.is_false())
     {
-      delete_from_jump_taken_value_set.emplace_back(value_set_element);
+      erase_from_jump_taken_value_set.insert(value_set_element);
     }
     else if(jump_not_taken_value_set && modified_condition.is_true())
     {
-      delete_from_jump_not_taken_value_set.emplace_back(value_set_element);
+      erase_from_jump_not_taken_value_set.insert(value_set_element);
     }
   }
-  if(jump_taken_value_set && !delete_from_jump_taken_value_set.empty())
+  if(jump_taken_value_set && !erase_from_jump_taken_value_set.empty())
   {
     value_sett::entryt *entry = jump_taken_value_set->get_entry_for_symbol(
       symbol_expr->get_identifier(), symbol_type, "", ns);
-    for(const exprt &value_to_erase : delete_from_jump_taken_value_set)
-    {
-      jump_taken_value_set->erase_value_from_entry(*entry, value_to_erase);
-    }
+    jump_taken_value_set->erase_values_from_entry(
+      *entry, erase_from_jump_taken_value_set);
   }
-  if(jump_not_taken_value_set && !delete_from_jump_not_taken_value_set.empty())
+  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(
       symbol_expr->get_identifier(), symbol_type, "", ns);
-    for(const exprt &value_to_erase : delete_from_jump_not_taken_value_set)
-    {
-      jump_not_taken_value_set->erase_value_from_entry(*entry, value_to_erase);
-    }
+    jump_not_taken_value_set->erase_values_from_entry(
+      *entry, erase_from_jump_not_taken_value_set);
   }
 }

src/pointer-analysis/value_set.cpp

@@ -1624,24 +1624,28 @@ void value_sett::guard(
   }
 }
 
-void value_sett::erase_value_from_entry(
+void value_sett::erase_values_from_entry(
   entryt &entry,
-  const exprt &value_to_erase)
+  const std::unordered_set<exprt, irep_hash> &values_to_erase)
 {
   std::vector<object_map_dt::key_type> keys_to_erase;
 
-  for(const auto &key_value : entry.object_map.read())
+  for(auto &key_value : entry.object_map.read())
   {
     const auto &rhs_object = to_expr(key_value);
-    if(rhs_object == value_to_erase)
+    if(values_to_erase.count(rhs_object))
     {
       keys_to_erase.emplace_back(key_value.first);
     }
   }
 
   DATA_INVARIANT(
-    keys_to_erase.size() == 1,
-    "value_sett::erase_value_from_entry() should erase exactly one value");
+    keys_to_erase.size() == values_to_erase.size(),
+    "value_sett::erase_value_from_entry() should erase exactly one value for "
+    "each element in the set it is given");
 
-  entry.object_map.write().erase(keys_to_erase[0]);
+  for(const auto &key_to_erase : keys_to_erase)
+  {
+    entry.object_map.write().erase(key_to_erase);
+  }
 }

src/pointer-analysis/value_set.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_H
 
 #include <set>
+#include <unordered_set>
 
 #include <util/mp_arith.h>
 #include <util/reference_counting.h>
@@ -483,7 +484,9 @@ class value_sett
     const std::string &suffix,
     const namespacet &ns) const;
 
-  void erase_value_from_entry(entryt &entry, const exprt &value_to_erase);
+  void erase_values_from_entry(
+    entryt &entry,
+    const std::unordered_set<exprt, irep_hash> &values_to_erase);
 
 protected:
   /// Reads the set of objects pointed to by `expr`, including making