Merge pull request #5 from chrisr-diffblue/sharing-map-arrays

martin-cs · web-flow · commit eac0027a3a24 · 2018-03-19T16:18:37.000Z
Use sharing_mapt in constant_array_abstract_objectt
diff --git a/src/analyses/variable-sensitivity/abstract_object.h b/src/analyses/variable-sensitivity/abstract_object.h
@@ -244,11 +244,11 @@ class abstract_objectt:public std::enable_shared_from_this<abstract_objectt>
     std::map<keyt, abstract_object_pointert> &out_map);
 
 
-  template<class keyt>
+  template<class keyt, typename hash>
   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);
+    const sharing_mapt<keyt, abstract_object_pointert, hash> &map1,
+    const sharing_mapt<keyt, abstract_object_pointert, hash> &map2,
+    sharing_mapt<keyt, abstract_object_pointert, hash> &out_map);
 
 
 
@@ -302,20 +302,15 @@ bool abstract_objectt::merge_maps(
   return modified;
 }
 
-template<typename keyt>
+template<typename keyt, typename hash>
 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)
+  const sharing_mapt<keyt, abstract_object_pointert, hash> &m1,
+  const sharing_mapt<keyt, abstract_object_pointert, hash> &m2,
+  sharing_mapt<keyt, abstract_object_pointert, 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);
+  auto delta_view = m1.get_delta_view(m2, true);
 
   for(auto &item : delta_view)
   {
diff --git a/src/analyses/variable-sensitivity/constant_array_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_array_abstract_object.cpp
@@ -139,9 +139,9 @@ abstract_object_pointert constant_array_abstract_objectt::constant_array_merge(
   }
   else
   {
-    array_mapt merged_map=array_mapt();
+    shared_array_mapt merged_map(map);
     bool modified=
-      abstract_objectt::merge_maps<mp_integer>(map, other->map, merged_map);
+      abstract_objectt::merge_shared_maps<mp_integer, mp_integer_hash>(map, other->map, merged_map);
     if(!modified)
     {
       return shared_from_this();
@@ -188,8 +188,11 @@ void constant_array_abstract_objectt::output(
   }
   else
   {
+    shared_array_mapt::sorted_viewt view;
+    map.get_view(view);
+
     out << "{";
-    for(const auto &entry : map)
+    for(const auto &entry : view)
     {
       out << "[" << entry.first << "] = ";
       entry.second->output(out, ai, ns);
@@ -281,14 +284,16 @@ abstract_object_pointert constant_array_abstract_objectt::read_index(
     mp_integer index_value;
     if(eval_index(index, env, ns, index_value))
     {
+      shared_array_mapt::const_find_type value = map.find(index_value);
+
       // Here we are assuming it is always in bounds
-      if(map.find(index_value)==map.cend())
+      if(!value.second)
       {
         return env.abstract_object_factory(type().subtype(), ns, true, false);
       }
       else
       {
-        return map.find(index_value)->second;
+        return value.first;
       }
     }
     else
@@ -339,7 +344,7 @@ sharing_ptrt<array_abstract_objectt>
   {
     if(stack.empty())
     {
-      auto copy=
+      auto result=
         internal_sharing_ptrt<constant_array_abstract_objectt>(
           new constant_array_abstract_objectt(*this));
 
@@ -348,11 +353,11 @@ sharing_ptrt<array_abstract_objectt>
       {
         if(is_top())
         {
-          copy->clear_top();
+          result->clear_top();
         }
 
-        copy->map[index_value]=value;
-        return copy;
+        result->map[index_value]=value;
+        return result;
       }
       else
       {
@@ -364,7 +369,7 @@ sharing_ptrt<array_abstract_objectt>
     }
     else
     {
-      auto copy=
+      auto result=
         internal_sharing_ptrt<constant_array_abstract_objectt>(
           new constant_array_abstract_objectt(*this));
 
@@ -373,9 +378,11 @@ sharing_ptrt<array_abstract_objectt>
       {
         // Here we assume the write is in bounds
         abstract_object_pointert array_entry;
-        if(map.find(index_value)!=map.cend())
+        shared_array_mapt::const_find_type old_value = map.find(index_value);
+
+        if(old_value.second)
         {
-          array_entry=map.at(index_value);
+          array_entry=old_value.first;
         }
         else
         {
@@ -384,28 +391,31 @@ sharing_ptrt<array_abstract_objectt>
 
         if(is_top())
         {
-          copy->clear_top();
+          result->clear_top();
         }
-        copy->map[index_value]=environment.write(
+        result->map[index_value]=environment.write(
           array_entry, value, stack, ns, merging_write);
 
-        return copy;
+        return result;
       }
       else
       {
-        for(const auto &array_entry : map)
+        shared_array_mapt::viewt view;
+        map.get_view(view);
+
+        for(const auto &array_entry : view)
         {
           // Merging write since we don't know which index we are writing to
-          copy->map[array_entry.first]=
+          result->map[array_entry.first]=
             environment.write(
               array_entry.second, value, stack, ns, true);
           if(is_top())
           {
-            copy->clear_top();
+            result->clear_top();
           }
         }
 
-        return copy;
+        return result;
       }
     }
   }
@@ -486,10 +496,27 @@ constant_array_abstract_objectt::visit_sub_elements(
     std::dynamic_pointer_cast<constant_array_abstract_objectt>(
       mutable_clone());
 
-  for(auto &item : result->map)
+  bool modified = false;
+
+  shared_array_mapt::viewt view;
+  result->map.get_view(view);
+
+  for(auto &item : view)
   {
-    item.second=visitor.visit(item.second);
+    auto newval = visitor.visit(item.second);
+    if(newval != item.second)
+    {
+      result->map[item.first]=newval; 
+      modified = true;
+    } 
   }
 
-  return result;
+  if(modified)
+  {
+    return result;
+  }
+  else
+  {
+    return shared_from_this();
+  }
 }
diff --git a/src/analyses/variable-sensitivity/constant_array_abstract_object.h b/src/analyses/variable-sensitivity/constant_array_abstract_object.h
@@ -74,8 +74,15 @@ class constant_array_abstract_objectt:public array_abstract_objectt
   // Since we don't store for any index where the value is top
   // we don't use a regular array but instead a map of array indices
   // to the value at that index
-  typedef std::map<mp_integer, abstract_object_pointert> array_mapt;
-  array_mapt map;
+  struct mp_integer_hash
+  {
+    size_t operator()(const mp_integer &i) const { return std::hash<BigInt::ullong_t>{}(i.to_ulong()); }
+  };
+
+  typedef sharing_mapt<mp_integer, abstract_object_pointert, mp_integer_hash>
+    shared_array_mapt;
+
+  shared_array_mapt map;
 
   bool eval_index(
     const index_exprt &index,
diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h
@@ -39,6 +39,11 @@ Author: Daniel Poetzl
   CV typename sharing_mapt<keyT, valueT, hashT, predT>::ST \
   sharing_mapt<keyT, valueT, hashT, predT>
 
+#define SHARING_MAPTV(R, V) \
+  template <class keyT, class valueT, class hashT, class predT> \
+  template <class V> \
+  R sharing_mapt<keyT, valueT, hashT, predT>
+
 template <
   class keyT,
   class valueT,
@@ -175,6 +180,17 @@ class sharing_mapt
 
   typedef std::pair<const key_type &, const mapped_type &> view_itemt;
   typedef std::vector<view_itemt> viewt;
+  typedef std::set<view_itemt> sorted_viewt;
+
+  void insert_view_item(viewt &v, view_itemt &&vi) const
+  {
+      v.push_back(vi);
+  }
+
+  void insert_view_item(sorted_viewt &v, view_itemt &&vi) const
+  {
+      v.insert(vi);
+  }
 
   class delta_view_itemt
   {
@@ -201,7 +217,7 @@ class sharing_mapt
 
   typedef std::vector<delta_view_itemt> delta_viewt;
 
-  void get_view(viewt &view) const;
+  template <class V> void get_view(V&) const;
   viewt get_view() const
   {
     viewt result;
@@ -214,6 +230,9 @@ class sharing_mapt
     delta_viewt &delta_view,
     const bool only_common=true) const;
 
+  delta_viewt get_delta_view(
+    const self_type &other, const bool only_common=true) const;
+
 protected:
   // helpers
 
@@ -225,7 +244,7 @@ class sharing_mapt
   void gather_all(const node_type &n, delta_viewt &delta_view) const;
 };
 
-SHARING_MAPT(void)::get_view(viewt &view) const
+SHARING_MAPTV(void, view_type)::get_view(view_type &view) const
 {
   assert(view.empty());
 
@@ -245,7 +264,7 @@ SHARING_MAPT(void)::get_view(viewt &view) const
     {
       for(const auto &child : n->get_container())
       {
-        view.push_back(view_itemt(child.get_key(), child.get_value()));
+        insert_view_item(view, view_itemt(child.get_key(), child.get_value()));
       }
     }
     else
@@ -403,6 +422,15 @@ SHARING_MAPT(void)::get_delta_view(
   while(!stack.empty());
 }
 
+SHARING_MAPT2(, delta_viewt)::get_delta_view(
+  const self_type &other,
+  const bool only_common) const
+{
+  delta_viewt delta_view;
+  get_delta_view(other, delta_view, only_common);
+  return delta_view;
+}
+
 SHARING_MAPT2(, node_type *)::get_container_node(const key_type &k)
 {
   size_t key=hash()(k);

Original file line number	Diff line number	Diff line change
`@@ -139,9 +139,9 @@ abstract_object_pointert constant_array_abstract_objectt::constant_array_merge(`
`139`	`139`	`}`
`140`	`140`	`else`
`141`	`141`	`{`
`142`		`- array_mapt merged_map=array_mapt();`
	`142`	`+ shared_array_mapt merged_map(map);`
`143`	`143`	`bool modified=`
`144`		`- abstract_objectt::merge_maps<mp_integer>(map, other->map, merged_map);`
	`144`	`+ abstract_objectt::merge_shared_maps<mp_integer, mp_integer_hash>(map, other->map, merged_map);`
`145`	`145`	`if(!modified)`
`146`	`146`	`{`
`147`	`147`	`return shared_from_this();`
`@@ -188,8 +188,11 @@ void constant_array_abstract_objectt::output(`
`188`	`188`	`}`
`189`	`189`	`else`
`190`	`190`	`{`
	`191`	`+ shared_array_mapt::sorted_viewt view;`
	`192`	`+ map.get_view(view);`
	`193`	`+`
`191`	`194`	`out << "{";`
`192`		`- for(const auto &entry : map)`
	`195`	`+ for(const auto &entry : view)`
`193`	`196`	`{`
`194`	`197`	`out << "[" << entry.first << "] = ";`
`195`	`198`	`entry.second->output(out, ai, ns);`
`@@ -281,14 +284,16 @@ abstract_object_pointert constant_array_abstract_objectt::read_index(`
`281`	`284`	`mp_integer index_value;`
`282`	`285`	`if(eval_index(index, env, ns, index_value))`
`283`	`286`	`{`
	`287`	`+ shared_array_mapt::const_find_type value = map.find(index_value);`
	`288`	`+`
`284`	`289`	`// Here we are assuming it is always in bounds`
`285`		`- if(map.find(index_value)==map.cend())`
	`290`	`+ if(!value.second)`
`286`	`291`	`{`
`287`	`292`	`return env.abstract_object_factory(type().subtype(), ns, true, false);`
`288`	`293`	`}`
`289`	`294`	`else`
`290`	`295`	`{`
`291`		`- return map.find(index_value)->second;`
	`296`	`+ return value.first;`
`292`	`297`	`}`
`293`	`298`	`}`
`294`	`299`	`else`
`@@ -339,7 +344,7 @@ sharing_ptrt<array_abstract_objectt>`
`339`	`344`	`{`
`340`	`345`	`if(stack.empty())`
`341`	`346`	`{`
`342`		`- auto copy=`
	`347`	`+ auto result=`
`343`	`348`	`internal_sharing_ptrt<constant_array_abstract_objectt>(`
`344`	`349`	`new constant_array_abstract_objectt(*this));`
`345`	`350`
`@@ -348,11 +353,11 @@ sharing_ptrt<array_abstract_objectt>`
`348`	`353`	`{`
`349`	`354`	`if(is_top())`
`350`	`355`	`{`
`351`		`- copy->clear_top();`
	`356`	`+ result->clear_top();`
`352`	`357`	`}`
`353`	`358`
`354`		`- copy->map[index_value]=value;`
`355`		`- return copy;`
	`359`	`+ result->map[index_value]=value;`
	`360`	`+ return result;`
`356`	`361`	`}`
`357`	`362`	`else`
`358`	`363`	`{`
`@@ -364,7 +369,7 @@ sharing_ptrt<array_abstract_objectt>`
`364`	`369`	`}`
`365`	`370`	`else`
`366`	`371`	`{`
`367`		`- auto copy=`
	`372`	`+ auto result=`
`368`	`373`	`internal_sharing_ptrt<constant_array_abstract_objectt>(`
`369`	`374`	`new constant_array_abstract_objectt(*this));`
`370`	`375`
`@@ -373,9 +378,11 @@ sharing_ptrt<array_abstract_objectt>`
`373`	`378`	`{`
`374`	`379`	`// Here we assume the write is in bounds`
`375`	`380`	`abstract_object_pointert array_entry;`
`376`		`- if(map.find(index_value)!=map.cend())`
	`381`	`+ shared_array_mapt::const_find_type old_value = map.find(index_value);`
	`382`	`+`
	`383`	`+ if(old_value.second)`
`377`	`384`	`{`
`378`		`- array_entry=map.at(index_value);`
	`385`	`+ array_entry=old_value.first;`
`379`	`386`	`}`
`380`	`387`	`else`
`381`	`388`	`{`
`@@ -384,28 +391,31 @@ sharing_ptrt<array_abstract_objectt>`
`384`	`391`
`385`	`392`	`if(is_top())`
`386`	`393`	`{`
`387`		`- copy->clear_top();`
	`394`	`+ result->clear_top();`
`388`	`395`	`}`
`389`		`- copy->map[index_value]=environment.write(`
	`396`	`+ result->map[index_value]=environment.write(`
`390`	`397`	`array_entry, value, stack, ns, merging_write);`
`391`	`398`
`392`		`- return copy;`
	`399`	`+ return result;`
`393`	`400`	`}`
`394`	`401`	`else`
`395`	`402`	`{`
`396`		`- for(const auto &array_entry : map)`
	`403`	`+ shared_array_mapt::viewt view;`
	`404`	`+ map.get_view(view);`
	`405`	`+`
	`406`	`+ for(const auto &array_entry : view)`
`397`	`407`	`{`
`398`	`408`	`// Merging write since we don't know which index we are writing to`
`399`		`- copy->map[array_entry.first]=`
	`409`	`+ result->map[array_entry.first]=`
`400`	`410`	`environment.write(`
`401`	`411`	`array_entry.second, value, stack, ns, true);`
`402`	`412`	`if(is_top())`
`403`	`413`	`{`
`404`		`- copy->clear_top();`
	`414`	`+ result->clear_top();`
`405`	`415`	`}`
`406`	`416`	`}`
`407`	`417`
`408`		`- return copy;`
	`418`	`+ return result;`
`409`	`419`	`}`
`410`	`420`	`}`
`411`	`421`	`}`
`@@ -486,10 +496,27 @@ constant_array_abstract_objectt::visit_sub_elements(`
`486`	`496`	`std::dynamic_pointer_cast<constant_array_abstract_objectt>(`
`487`	`497`	`mutable_clone());`
`488`	`498`
`489`		`- for(auto &item : result->map)`
	`499`	`+ bool modified = false;`
	`500`	`+`
	`501`	`+ shared_array_mapt::viewt view;`
	`502`	`+ result->map.get_view(view);`
	`503`	`+`
	`504`	`+ for(auto &item : view)`
`490`	`505`	`{`
`491`		`- item.second=visitor.visit(item.second);`
	`506`	`+ auto newval = visitor.visit(item.second);`
	`507`	`+ if(newval != item.second)`
	`508`	`+ {`
	`509`	`+ result->map[item.first]=newval;`
	`510`	`+ modified = true;`
	`511`	`+ }`
`492`	`512`	`}`
`493`	`513`
`494`		`- return result;`
	`514`	`+ if(modified)`
	`515`	`+ {`
	`516`	`+ return result;`
	`517`	`+ }`
	`518`	`+ else`
	`519`	`+ {`
	`520`	`+ return shared_from_this();`
	`521`	`+ }`
`495`	`522`	`}`