Merge pull request #4484 from danpoe/refactor/sharing-map-erase

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

Author: tautschnig

src/goto-symex/symex_dead.cpp

@@ -28,7 +28,12 @@ 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,10 @@ 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)
+SHARING_MAPT(void)::erase(const key_type &k)
 {
-  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;
-
   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 +864,29 @@ 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(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;
+    PRECONDITION(equalT()(ll.front().get_key(), k));
+    del->remove_child(del_bit);
   }
-
-  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)
+  else
   {
-    cnt+=erase(k, key_exists);
+    ip->remove_leaf(k);
   }
 
-  return cnt;
+  num--;
 }
 
 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,11 @@ 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");
+}