Minor sharing-map improvements, used to avoid copying in value_sett

src/pointer-analysis/value_set.cpp

@@ -70,16 +70,19 @@ void value_sett::update_entry(
   auto existing_entry = values.find(index);
   if(existing_entry.has_value())
   {
-    entryt replacement = *existing_entry;
     if(add_to_sets)
     {
-      if(make_union(replacement.object_map, new_values))
-        values.replace(index, std::move(replacement));
+      if(make_union_would_change(existing_entry->get().object_map, new_values))
+      {
+        values.update(index, [&new_values, this](entryt &entry) {
+          make_union(entry.object_map, new_values);
+        });
+      }
     }
     else
     {
-      replacement.object_map = new_values;
-      values.replace(index, std::move(replacement));
+      values.update(
+        index, [&new_values](entryt &entry) { entry.object_map = new_values; });
     }
   }
   else
@@ -90,8 +93,8 @@ void value_sett::update_entry(
   }
 }
 
-bool value_sett::insert(
-  object_mapt &dest,
+value_sett::insert_actiont value_sett::get_insert_action(
+  const object_mapt &dest,
   object_numberingt::number_type n,
   const offsett &offset) const
 {
@@ -100,108 +103,113 @@ bool value_sett::insert(
   if(entry==dest.read().end())
   {
     // new
-    dest.write()[n] = offset;
-    return true;
+    return insert_actiont::INSERT;
   }
   else if(!entry->second)
-    return false; // no change
+    return insert_actiont::NONE;
   else if(offset && *entry->second == *offset)
-    return false; // no change
+    return insert_actiont::NONE;
   else
-  {
-    dest.write()[n].reset();
-    return true;
-  }
+    return insert_actiont::RESET_OFFSET;
 }
 
-void value_sett::output(
-  const namespacet &ns,
-  std::ostream &out) const
+bool value_sett::insert(
+  object_mapt &dest,
+  object_numberingt::number_type n,
+  const offsett &offset) const
 {
-  valuest::viewt view;
-  values.get_view(view);
+  auto insert_action = get_insert_action(dest, n, offset);
+  if(insert_action == insert_actiont::NONE)
+    return false;
 
-  for(const auto &values_entry : view)
-  {
-    irep_idt identifier, display_name;
+  auto &new_offset = dest.write()[n];
+  if(insert_action == insert_actiont::INSERT)
+    new_offset = offset;
+  else
+    new_offset.reset();
 
-    const entryt &e = values_entry.second;
+  return true;
+}
+
+void value_sett::output(const namespacet &ns, std::ostream &out) const
+{
+  values.iterate([&](const irep_idt &, const entryt &e) {
+    irep_idt identifier, display_name;
 
     if(has_prefix(id2string(e.identifier), "value_set::dynamic_object"))
     {
-      display_name=id2string(e.identifier)+e.suffix;
-      identifier="";
+      display_name = id2string(e.identifier) + e.suffix;
+      identifier = "";
     }
-    else if(e.identifier=="value_set::return_value")
+    else if(e.identifier == "value_set::return_value")
     {
-      display_name="RETURN_VALUE"+e.suffix;
-      identifier="";
+      display_name = "RETURN_VALUE" + e.suffix;
+      identifier = "";
     }
     else
     {
-      #if 0
-      const symbolt &symbol=ns.lookup(e.identifier);
-      display_name=id2string(symbol.display_name())+e.suffix;
-      identifier=symbol.name;
-      #else
-      identifier=id2string(e.identifier);
-      display_name=id2string(identifier)+e.suffix;
-      #endif
+#if 0
+        const symbolt &symbol=ns.lookup(e.identifier);
+        display_name=id2string(symbol.display_name())+e.suffix;
+        identifier=symbol.name;
+#else
+      identifier = id2string(e.identifier);
+      display_name = id2string(identifier) + e.suffix;
+#endif
     }
 
     out << display_name;
 
     out << " = { ";
 
-    const object_map_dt &object_map=e.object_map.read();
+    const object_map_dt &object_map = e.object_map.read();
 
-    std::size_t width=0;
+    std::size_t width = 0;
 
-    for(object_map_dt::const_iterator
-        o_it=object_map.begin();
-        o_it!=object_map.end();
+    for(object_map_dt::const_iterator o_it = object_map.begin();
+        o_it != object_map.end();
         o_it++)
     {
-      const exprt &o=object_numbering[o_it->first];
+      const exprt &o = object_numbering[o_it->first];
 
       std::string result;
 
-      if(o.id()==ID_invalid || o.id()==ID_unknown)
-        result=from_expr(ns, identifier, o);
+      if(o.id() == ID_invalid || o.id() == ID_unknown)
+        result = from_expr(ns, identifier, o);
       else
       {
-        result="<"+from_expr(ns, identifier, o)+", ";
+        result = "<" + from_expr(ns, identifier, o) + ", ";
 
         if(o_it->second)
           result += integer2string(*o_it->second) + "";
         else
-          result+='*';
+          result += '*';
 
         if(o.type().is_nil())
-          result+=", ?";
+          result += ", ?";
         else
-          result+=", "+from_type(ns, identifier, o.type());
+          result += ", " + from_type(ns, identifier, o.type());
 
-        result+='>';
+        result += '>';
       }
 
       out << result;
 
-      width+=result.size();
+      width += result.size();
 
       object_map_dt::const_iterator next(o_it);
       next++;
 
-      if(next!=object_map.end())
+      if(next != object_map.end())
       {
         out << ", ";
-        if(width>=40)
+        if(width >= 40)
           out << "\n      ";
       }
     }
 
     out << " } \n";
-  }
+  });
 }
 
 exprt value_sett::to_expr(const object_map_dt::value_type &it) const
@@ -236,10 +244,12 @@ bool value_sett::make_union(const value_sett::valuest &new_values)
   {
     if(delta_entry.in_both)
     {
-      entryt merged_entry = *values.find(delta_entry.k);
-      if(make_union(merged_entry.object_map, delta_entry.m.object_map))
+      if(make_union_would_change(
+           delta_entry.other_m.object_map, delta_entry.m.object_map))
       {
-        values.replace(delta_entry.k, std::move(merged_entry));
+        values.update(delta_entry.k, [&](entryt &existing_entry) {
+          make_union(existing_entry.object_map, delta_entry.m.object_map);
+        });
         result = true;
       }
     }
@@ -253,6 +263,24 @@ bool value_sett::make_union(const value_sett::valuest &new_values)
   return result;
 }
 
+bool value_sett::make_union_would_change(
+  const object_mapt &dest,
+  const object_mapt &src) const
+{
+  for(const auto &number_and_offset : src.read())
+  {
+    if(
+      get_insert_action(
+        dest, number_and_offset.first, number_and_offset.second) !=
+      insert_actiont::NONE)
+    {
+      return true;
+    }
+  }
+
+  return false;
+}
+
 bool value_sett::make_union(object_mapt &dest, const object_mapt &src) const
 {
   bool result=false;

src/pointer-analysis/value_set.h

@@ -232,6 +232,24 @@ class value_sett
     object_numberingt::number_type n,
     const offsett &offset) const;
 
+  enum class insert_actiont
+  {
+    INSERT,
+    RESET_OFFSET,
+    NONE
+  };
+
+  /// Determines what would happen if object number \p n was inserted into map
+  /// \p dest with offset \p offset -- the possibilities being, nothing (the
+  /// entry is already present), a new entry would be inserted (no existing
+  /// entry with number \p n was found), or an existing entry's offset would be
+  /// reset (indicating there is already an entry with number \p n, but with
+  /// differing offset).
+  insert_actiont get_insert_action(
+    const object_mapt &dest,
+    object_numberingt::number_type n,
+    const offsett &offset) const;
+
   /// Adds an expression and offset to an object map. If the
   /// destination map has an existing element for the same expression
   /// with a differing offset its offset is marked unknown.
@@ -360,6 +378,13 @@ class value_sett
   /// \return true if anything changed.
   bool make_union(object_mapt &dest, const object_mapt &src) const;
 
+  /// Determines whether merging two RHS expression sets would cause any change
+  /// \param dest: set that would be merged into
+  /// \param src: set that would be merged in
+  /// \return true if anything changed.
+  bool make_union_would_change(const object_mapt &dest, const object_mapt &src)
+    const;
+
   /// Merges an entire existing value_sett's data into this one
   /// \param new_values: new values to merge in
   /// \return true if anything changed.

src/util/invariant.cpp

@@ -16,6 +16,8 @@ Author: Martin Brain, [email protected]
 
 #include <iostream>
 
+bool cbmc_invariants_should_throw = false;
+
 // Backtraces compiler and C library specific
 // So we should include something explicitly from the C library
 // to check if the C library is glibc.
@@ -26,7 +28,6 @@ Author: Martin Brain, [email protected]
 #include <execinfo.h>
 #include <cxxabi.h>
 
-
 /// Attempts to demangle the function name assuming the glibc
 /// format of stack entry:
 ///

src/util/invariant.h

@@ -64,6 +64,28 @@ Author: Martin Brain, [email protected]
 ** CPROVER_INVARIANT_* macros.
 */
 
+/// Set this to true to cause invariants to throw a C++ exception rather than
+/// abort the program. This is currently untested behaviour, and may fail to
+/// clean up partly-completed CBMC operations or release resources. You should
+/// probably only use this to gather or report more information about the
+/// failure and then abort. Default off.
+extern bool cbmc_invariants_should_throw;
+
+/// Helper to enable invariant throwing as above bounded to an object lifetime:
+struct cbmc_invariants_should_throwt
+{
+  bool old_state;
+  cbmc_invariants_should_throwt() : old_state(cbmc_invariants_should_throw)
+  {
+    cbmc_invariants_should_throw = true;
+  }
+
+  ~cbmc_invariants_should_throwt()
+  {
+    cbmc_invariants_should_throw = old_state;
+  }
+};
+
 /// A logic error, augmented with a distinguished field to hold a backtrace.
 /// Classes that extend this one should share the same initial constructor
 /// parameters: their constructor signature should be of the form:
@@ -230,10 +252,14 @@ CBMC_NORETURN
     backtrace,
     condition,
     std::forward<Params>(params)...);
-  // We now have a structured exception ready to use;
-  // in future this is the place to put a 'throw'.
-  report_exception_to_stderr(to_throw);
-  abort();
+
+  if(cbmc_invariants_should_throw)
+    throw to_throw;
+  else
+  {
+    report_exception_to_stderr(to_throw);
+    abort();
+  }
 }
 
 /// This is a wrapper function used by the macro 'INVARIANT(CONDITION, REASON)'.