Change erase() method of the sharing map to require that the given key exists

Previously when sharing_map.erase(key) was called, two traversals of the path to
the leaf to erase were done. One to check whether the key was in the map, and if
it was, a second one to copy and detach the nodes on the path to the leaf to
erase. This commit changes erase() to require that the given key exists in the
map. This simplifies the implementation and avoids two traversals of the path to
the leaf to erase when it is known that the key exists. If it is not known
whether the key exists, sharing_map.has_key(key) should be explicitely called
first.

Author: danpoe

src/goto-symex/symex_dead.cpp

@@ -28,7 +28,11 @@ void goto_symext::symex_dead(statet &state)
   // information is not local to a path, but removing it from the propagation
   // map and value-set is safe as 1) it is local to a path and 2) this instance
   // can no longer appear
-  state.value_set.values.erase(l1_identifier);
+
+  if (state.value_set.values.has_key(l1_identifier)) {
+    state.value_set.values.erase(l1_identifier);
+  }
+
   state.propagation.erase(l1_identifier);
   // Remove from the local L2 renaming map; this means any reads from the dead
   // identifier will use generation 0 (e.g. x!N@M#0, where N and M are positive

src/util/sharing_map.h

@@ -157,14 +157,6 @@ Author: Daniel Poetzl
 /// For this to work, the type of the values stored in the map needs to have a
 /// defined equality operator (operator==).
 ///
-/// Several methods take a hint indicating whether the element is known not to
-/// be in the map (`false`), known to be in the map (`true`), or it is unknown
-/// whether the element is in the map (`unknown`). The value `unknown` is always
-/// valid. When `true` or `false` are given they need to be accurate, otherwise
-/// the behavior is undefined. A correct hint can prevent the need to follow a
-/// path from the root to a key-value pair twice (e.g., once for checking that
-/// it exists, and second for copying nodes).
-///
 /// In the descriptions of the methods of the sharing map we also give the
 /// complexity of the operations. We use the following symbols:
 /// - N: number of key-value pairs in the map
@@ -221,31 +213,14 @@ class sharing_mapt
 public:
   // interface
 
-  /// Erase element
+  /// Erase element, element must exist in map
   ///
   /// Complexity:
   /// - Worst case: O(H * S + M)
   /// - Best case: O(H)
   ///
   /// \param k: The key of the element to erase
-  /// \param key_exists: Hint to indicate whether the element is known to exist
-  ///   (possible values `unknown` or` true`)
-  size_type erase(const key_type &k, const tvt &key_exists = tvt::unknown());
-
-  /// Erase all elements
-  ///
-  /// Complexity:
-  /// - Worst case: O(K * (H * S + M))
-  /// - Best case: O(K * H)
-  ///
-  /// \param ks: The keys of the element to erase
-  /// \param key_exists: Hint to indicate whether the elements are known to
-  ///   exist (possible values `unknown` or `true`). Applies to all elements
-  ///   (i.e., have to use `unknown` if for at least one element it is not known
-  ///   whether it exists)
-  size_type erase_all(
-    const keyst &ks,
-    const tvt &key_exists = tvt::unknown()); // applies to all keys
+  void erase(const key_type &k);
 
   /// Insert element, element must not exist in map
   ///
@@ -871,18 +846,9 @@ SHARING_MAPT2(const, innert *)::get_container_node(const key_type &k) const
   return ip;
 }
 
-SHARING_MAPT2(, size_type)::erase(const key_type &k, const tvt &key_exists)
-{
-  SM_ASSERT(!key_exists.is_false());
-  SM_ASSERT(!key_exists.is_true() || has_key(k));
-
-  // check if key exists
-  if(key_exists.is_unknown() && !has_key(k))
-    return 0;
-
+SHARING_MAPT(void)::erase(const key_type &k) {
   innert *del = nullptr;
   std::size_t del_bit = 0;
-  std::size_t del_level = 0;
 
   std::size_t key = hash()(k);
   innert *ip = ↦
@@ -897,52 +863,26 @@ SHARING_MAPT2(, size_type)::erase(const key_type &k, const tvt &key_exists)
     {
       del = ip;
       del_bit=bit;
-      del_level = i;
     }
 
     ip = ip->add_child(bit);
 
     key >>= chunk;
   }
 
+  PRECONDITION(!ip->empty());
   const leaf_listt &ll = as_const(ip)->get_container();
+  PRECONDITION(!ll.empty());
 
   // forward list has one element
-  if(!ll.empty() && std::next(ll.begin()) == ll.end())
-  {
-    if(del_level < steps - 1)
-    {
-      del->remove_child(del_bit);
-    }
-    else
-    {
-      SM_ASSERT(del_level == steps - 1);
-      del->remove_child(del_bit);
-    }
-
-    num--;
-    return 1;
+  if (std::next(ll.begin()) == ll.end()) {
+    PRECONDITION(equalT()(ll.front().get_key(), k));
+    del->remove_child(del_bit);
+  } else {
+    ip->remove_leaf(k);
   }
 
-  SM_ASSERT(!ll.empty());
-
-  ip->remove_leaf(k);
   num--;
-
-  return 1;
-}
-
-SHARING_MAPT2(, size_type)
-::erase_all(const keyst &ks, const tvt &key_exists)
-{
-  size_type cnt = 0;
-
-  for(const key_type &k : ks)
-  {
-    cnt+=erase(k, key_exists);
-  }
-
-  return cnt;
 }
 
 SHARING_MAPT4(valueU, void)

unit/util/sharing_map.cpp

@@ -193,13 +193,12 @@ TEST_CASE("Sharing map interface", "[core][util]")
     sm.insert("i", "0");
     sm.insert("j", "1");
 
-    REQUIRE(sm.erase("k") == 0);
     REQUIRE(sm.size() == 2);
 
-    REQUIRE(sm.erase("i") == 1);
+    sm.erase("i");
     REQUIRE(!sm.has_key("i"));
 
-    REQUIRE(sm.erase("j") == 1);
+    sm.erase("j");
     REQUIRE(!sm.has_key("j"));
 
     sm.insert("i", "0");
@@ -232,7 +231,7 @@ TEST_CASE("Sharing map copying", "[core][util]")
 
   sharing_map_standardt sm2(sm1);
 
-  REQUIRE(sm2.erase("i") == 1);
+  sm2.erase("i");
   REQUIRE(!sm2.has_key("i"));
   REQUIRE(sm1.has_key("i"));
 
@@ -510,3 +509,10 @@ TEST_CASE("Sharing map insert existing", "[.]")
 
   sm.insert("i", "4");
 }
+
+TEST_CASE("Sharing map erase non-existing", "[.]") {
+  sharing_map_standardt sm;
+  fill(sm);
+
+  sm.erase("x");
+}