From c920010985db836a3150b5b2ec965819ff80b3ad Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 1 Jul 2021 17:23:52 +0100
Subject: [PATCH] Fix for iterators into unordered_maps
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

C++11 §23.2.5/13 states:

The insert and emplace members shall not affect the validity of references
to container elements, but may invalidate all iterators to the container.

This fixes two instances where the iterators are assumed to remain valid
while inserting additional elements into an unordered_map.  The problem is
exposed when using -D_GLIBCXX_DEBUG.
---
 src/solvers/flattening/boolbv.cpp     | 21 +++++++++++++--------
 src/solvers/prop/prop_conv_solver.cpp | 13 +++++++++----
 2 files changed, 22 insertions(+), 12 deletions(-)

diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index dce9c55f267..71d6c50f1fc 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -42,24 +42,29 @@ boolbvt::convert_bv(const exprt &expr, optionalt<std::size_t> expected_width)
   // check cache first
   std::pair<bv_cachet::iterator, bool> cache_result=
     bv_cache.insert(std::make_pair(expr, bvt()));
+
+  // get a reference to the cache entry
+  auto &cache_entry = cache_result.first->second;
+
   if(!cache_result.second)
   {
-    return cache_result.first->second;
+    // Found in cache
+    return cache_entry;
   }
 
-  // Iterators into hash_maps supposedly stay stable
-  // even though we are inserting more elements recursively.
-
-  cache_result.first->second = convert_bitvector(expr);
+  // Iterators into hash_maps do not remain valid when inserting
+  // more elements recursively. C++11 §23.2.5/13
+  // However, the _reference_ to the entry does!
+  cache_entry = convert_bitvector(expr);
 
   INVARIANT_WITH_DIAGNOSTICS(
-    !expected_width || cache_result.first->second.size() == *expected_width,
+    !expected_width || cache_entry.size() == *expected_width,
     "bitvector width shall match the indicated expected width",
     expr.find_source_location(),
     irep_pretty_diagnosticst(expr));
 
   // check
-  for(const auto &literal : cache_result.first->second)
+  for(const auto &literal : cache_entry)
   {
     if(freeze_all && !literal.is_constant())
       prop.set_frozen(literal);
@@ -71,7 +76,7 @@ boolbvt::convert_bv(const exprt &expr, optionalt<std::size_t> expected_width)
       irep_pretty_diagnosticst(expr));
   }
 
-  return cache_result.first->second;
+  return cache_entry;
 }
 
 /// Print that the expression of x has failed conversion,
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index aec587abdf2..f9bcb0bd4de 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/src/solvers/prop/prop_conv_solver.cpp
@@ -166,13 +166,18 @@ literalt prop_conv_solvert::convert(const exprt &expr)
   // check cache first
   auto result = cache.insert({expr, literalt()});
 
-  if(!result.second)
-    return result.first->second;
+  // get a reference to the cache entry
+  auto &cache_entry = result.first->second;
 
+  if(!result.second) // found in cache
+    return cache_entry;
+
+  // The following may invalidate the iterator result.first,
+  // but note that the _reference_ is guaranteed to remain valid.
   literalt literal = convert_bool(expr);
 
-  // insert into cache
-  result.first->second = literal;
+  // store the literal in the cache using the reference
+  cache_entry = literal;
 
   if(freeze_all && !literal.is_constant())
     prop.set_frozen(literal);