Fix for iterators into unordered_maps

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.

Author: kroening

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,

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