Merge pull request #3 from chrisr-diffblue/sharing-map-structs

martin-cs · web-flow · commit ada033cbecf1 · 2018-03-19T15:14:52.000Z
Use sharing_mapt instead of std::map in full_struct_abstract_object
diff --git a/src/analyses/variable-sensitivity/abstract_object.h b/src/analyses/variable-sensitivity/abstract_object.h
@@ -35,6 +35,7 @@
 
 #include <goto-programs/goto_program.h>
 #include <util/expr.h>
+#include <util/sharing_map.h>
 
 class typet;
 class constant_exprt;
@@ -116,7 +117,12 @@ class abstract_objectt:public std::enable_shared_from_this<abstract_objectt>
     std::ostream &out, const class ai_baset &ai, const namespacet &ns) const;
 
   typedef std::set<goto_programt::const_targett> locationst;
-
+  typedef sharing_mapt<irep_idt, abstract_object_pointert, irep_id_hash>
+    shared_mapt;
+    
+  static void dump_map(std::ostream out, const shared_mapt &m);
+  static void dump_map_diff(
+    std::ostream out, const shared_mapt &m1, const shared_mapt &m2);
 
   abstract_object_pointert clone() const
   {
@@ -194,7 +200,6 @@ class abstract_objectt:public std::enable_shared_from_this<abstract_objectt>
     const abstract_object_visitort &visitor) const
   { return shared_from_this(); }
 
-
 private:
   // To enforce copy-on-write these are private and have read-only accessors
   typet t;
@@ -238,6 +243,15 @@ class abstract_objectt:public std::enable_shared_from_this<abstract_objectt>
     const std::map<keyt, abstract_object_pointert> &map2,
     std::map<keyt, abstract_object_pointert> &out_map);
 
+
+  template<class keyt>
+  static bool merge_shared_maps(
+    const sharing_mapt<keyt, abstract_object_pointert, irep_id_hash> &map1,
+    const sharing_mapt<keyt, abstract_object_pointert, irep_id_hash> &map2,
+    sharing_mapt<keyt, abstract_object_pointert, irep_id_hash> &out_map);
+
+
+
   // The one exception is merge in descendant classes, which needs this
   void make_top() { top=true; this->make_top_internal(); }
   void clear_top() { top=false; this->clear_top_internal(); }
@@ -288,5 +302,34 @@ bool abstract_objectt::merge_maps(
   return modified;
 }
 
+template<typename keyt>
+bool abstract_objectt::merge_shared_maps(
+  const sharing_mapt<keyt, abstract_object_pointert, irep_id_hash> &m1,
+  const sharing_mapt<keyt, abstract_object_pointert, irep_id_hash> &m2,
+  sharing_mapt<keyt, abstract_object_pointert, irep_id_hash> &out_map)
+{
+  typedef sharing_mapt<irep_idt, abstract_object_pointert,
+    irep_id_hash>
+    abstract_object_mapt;
+
+  bool modified=false;
+
+  abstract_object_mapt::delta_viewt delta_view;
+  m1.get_delta_view(m2, delta_view, true);
+
+  for(auto &item : delta_view)
+  {
+    bool changes = false;
+    abstract_object_pointert v_new = abstract_objectt::merge(
+      item.m, item.other_m, changes);
+    if (changes)
+    {
+      modified = true;
+      out_map[item.k] = v_new;
+    }
+  }
+
+  return modified;
+}
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
diff --git a/src/analyses/variable-sensitivity/abstract_value.cpp b/src/analyses/variable-sensitivity/abstract_value.cpp
@@ -71,3 +71,44 @@ abstract_valuet::abstract_valuet(
   const namespacet &ns):
     abstract_objectt(expr, environment, ns)
 {}
+
+
+void abstract_objectt::dump_map(
+  std::ostream out, const abstract_objectt::shared_mapt &m)
+{
+  shared_mapt::viewt view;
+  m.get_view(view);
+
+  out << "{";
+  bool first=true;
+  for(auto &item : view)
+  {
+    out << (first ? "" : ", ") << item.first;
+    first = false;
+  }
+  out << "}";
+}
+
+/**
+ * \brief Dump all elements in m1 that are different or missing in m2
+ * 
+ * \param m1 the 'target' sharing_map
+ * \param m2 the reference sharing map
+ */
+void abstract_objectt::dump_map_diff(
+  std::ostream out,
+  const abstract_objectt::shared_mapt &m1,
+  const abstract_objectt::shared_mapt &m2)
+{
+  shared_mapt::delta_viewt delta_view;
+  m1.get_delta_view(m2, delta_view, false);
+
+  out << "DELTA{";
+  bool first = true;
+  for(auto &item : delta_view)
+  {
+    out << (first ? "" : ", ") << item.k << "=" << item.in_both;
+    first = false;
+  }
+  out << "}";
+}
diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
@@ -20,6 +20,18 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com
 #include <iostream>
 #endif
 
+/**
+ * \brief Explicit copy-constructor to make it clear that the shared_map
+ *        used to store the values of fields is copy-constructed as well
+ *        to ensure it shares as much data as possible.
+ */
+full_struct_abstract_objectt::full_struct_abstract_objectt(
+  const full_struct_abstract_objectt &ao):
+    struct_abstract_objectt(ao), map(ao.map)
+{
+  DATA_INVARIANT(verify(), "Structural invariants maintained");
+}
+
 /*******************************************************************\
 
 Function: full_struct_abstract_objectt::struct_abstract_objectt
@@ -124,13 +136,13 @@ abstract_object_pointert full_struct_abstract_objectt::read_component(
   {
     PRECONDITION(!is_bottom());
 
-    irep_idt c=member_expr.get_component_name();
+    const irep_idt c=member_expr.get_component_name();
 
-    struct_mapt::const_iterator it=map.find(c);
+    shared_struct_mapt::const_find_type value=map.find(c);
 
-    if(it!=map.cend())
+    if(value.second)
     {
-      return it->second;
+      return value.first;
     }
     else
     {
@@ -182,29 +194,31 @@ sharing_ptrt<struct_abstract_objectt>
         member_expr.compound().type(), false, true));
   }
 
-  internal_sharing_ptrt<full_struct_abstract_objectt> copy(
-    new full_struct_abstract_objectt(*this));
+  const auto &result=
+    std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
 
   if(!stack.empty())
   {
     abstract_object_pointert starting_value;
-    irep_idt c=member_expr.get_component_name();
-    if(map.find(c)==map.cend())
+    const irep_idt c=member_expr.get_component_name();
+    shared_struct_mapt::const_find_type old_value = map.find(c);
+    if(!old_value.second)
     {
       starting_value=
         environment.abstract_object_factory(
           member_expr.type(), ns, true, false);
     }
     else
     {
-      starting_value=map.at(c);
+      starting_value=old_value.first;
     }
 
-    copy->map[c]=
+    result->map[c] =
       environment.write(starting_value, value, stack, ns, merging_write);
-    copy->clear_top();
-    DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;
-    return copy;
+
+    result->clear_top();
+    DATA_INVARIANT(result->verify(), "Structural invariants maintained");
+    return result;
   }
   else
   {
@@ -213,41 +227,40 @@ sharing_ptrt<struct_abstract_objectt>
     std::cout << "Setting component" << std::endl;
 #endif
 
-    irep_idt c=member_expr.get_component_name();
+    const irep_idt c=member_expr.get_component_name();
 
     if(merging_write)
     {
       if(is_top()) // struct is top
       {
-        DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;
-        return copy;
+        DATA_INVARIANT(result->verify(), "Structural invariants maintained");
+        return result;
       }
 
-      INVARIANT(!copy->map.empty(), "If not top, map cannot be empty");
+      INVARIANT(!result->map.empty(), "If not top, map cannot be empty");
 
-      struct_mapt &m=copy->map;
+      shared_struct_mapt::const_find_type old_value=result->map.find(c);
 
-      struct_mapt::iterator it=m.find(c);
-
-      if(it==m.end()) // component is top
+      if(!old_value.second) // component is top
       {
-        DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;
-        return copy;
+        DATA_INVARIANT(result->verify(), "Structural invariants maintained");
+        return result;
       }
 
       bool dummy;
 
-      it->second=abstract_objectt::merge(it->second, value, dummy);
+      result->map[c] = abstract_objectt::merge(old_value.first, value, dummy);
     }
     else
     {
-      copy->map[c]=value;
-      copy->clear_top();
-      INVARIANT(!copy->is_bottom(), "top != bottom");
+      result->map[c] = value;
+      result->clear_top();
+      INVARIANT(!result->is_bottom(), "top != bottom");
     }
 
-    DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;
-    return copy;
+    DATA_INVARIANT(result->verify(), "Structural invariants maintained");
+
+    return result;
   }
 }
 
@@ -272,15 +285,27 @@ Function: full_struct_abstract_objectt::output
 void full_struct_abstract_objectt::output(
   std::ostream &out, const ai_baset &ai, const namespacet &ns) const
 {
+  // To ensure that a consistent ordering of fields is output, use
+  // the underlying type declaration for this struct to determine
+  // the ordering
+  struct_union_typet type_decl = to_struct_union_type(ns.follow(type()));
+
+  bool first = true;
+
   out << "{";
-  for(const auto &entry : map)
+  for(const auto field : type_decl.components())
   {
-    if(entry.first!=map.cbegin()->first)
+    auto value = map.find(field.get_name());
+    if(value.second)
     {
-      out << ", ";
+      if(!first)
+      {
+        out << ", ";
+      }
+      out << '.' << field.get_name() << '=';
+      value.first->output(out, ai, ns);
+      first = false;
     }
-    out << "." << entry.first << "=";
-    entry.second->output(out, ai, ns);
   }
   out << "}";
 }
@@ -362,22 +387,19 @@ abstract_object_pointert full_struct_abstract_objectt::merge_constant_structs(
   }
   else
   {
-    struct_mapt merged_map;
-    bool modified=
-      abstract_objectt::merge_maps<irep_idt>(map, other->map, merged_map);
+    const auto &result=
+      std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
+
+    bool modified = abstract_objectt::merge_shared_maps<irep_idt>(
+      map, other->map, result->map);
+
     if(!modified)
     {
       DATA_INVARIANT(verify(), "Structural invariants maintained");
       return shared_from_this();
     }
     else
     {
-      const auto &result=
-        std::dynamic_pointer_cast<full_struct_abstract_objectt>(
-          mutable_clone());
-
-      result->map=merged_map;
-
       INVARIANT(!result->is_top(), "Merge of maps will not generate top");
       INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom");
       DATA_INVARIANT(result->verify(), "Structural invariants maintained");
@@ -397,18 +419,33 @@ abstract_object_pointert full_struct_abstract_objectt::merge_constant_structs(
  * \return A new abstract_object if it's contents is modifed, or this if
  * no modification is needed
  */
-abstract_object_pointert
-  full_struct_abstract_objectt::visit_sub_elements(
+abstract_object_pointert full_struct_abstract_objectt::visit_sub_elements(
   const abstract_object_visitort &visitor) const
 {
   const auto &result=
-    std::dynamic_pointer_cast<full_struct_abstract_objectt>(
-      mutable_clone());
+    std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
+
+  bool modified = false;
+
+  shared_struct_mapt::viewt view;
+  result->map.get_view(view);
 
-  for(auto &item : result->map)
+  for(auto &item : view)
   {
-    item.second=visitor.visit(item.second);
+    auto newval = visitor.visit(item.second);
+    if(newval != item.second)
+    {
+      result->map[item.first] = visitor.visit(item.second);
+      modified = true;
+    }
   }
 
-  return result;
+  if(modified)
+  {
+    return result;
+  }
+  else
+  {
+    return shared_from_this();
+  }
 }
diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.h b/src/analyses/variable-sensitivity/full_struct_abstract_object.h
@@ -13,6 +13,7 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com
 #include <iosfwd>
 #include <analyses/variable-sensitivity/abstract_object.h>
 #include <analyses/variable-sensitivity/struct_abstract_object.h>
+#include <util/sharing_map.h>
 
 class abstract_environmentt;
 class member_exprt;
@@ -22,6 +23,9 @@ class full_struct_abstract_objectt:public struct_abstract_objectt
 public:
   typedef sharing_ptrt<full_struct_abstract_objectt> constant_struct_pointert;
 
+  // Define an explicit copy constructor to ensure sharing of maps
+  full_struct_abstract_objectt(const full_struct_abstract_objectt &ao);
+
   explicit full_struct_abstract_objectt(const typet &type);
 
   full_struct_abstract_objectt(const typet &type, bool top, bool bottom);
@@ -41,8 +45,9 @@ class full_struct_abstract_objectt:public struct_abstract_objectt
 
 private:
   // no entry means component is top
-  typedef std::map<irep_idt, abstract_object_pointert> struct_mapt;
-  struct_mapt map;
+  typedef sharing_mapt<irep_idt, abstract_object_pointert, irep_id_hash>
+    shared_struct_mapt;
+  shared_struct_mapt map;
 
   abstract_object_pointert merge_constant_structs(
     constant_struct_pointert other) const;
