Added usage of dynamic-objects with recency

src/pointer-analysis/dynamic_object_name.h

@@ -0,0 +1,58 @@
+/*******************************************************************\
+
+Module: Dynamic object name
+
+Author: Marius-Constantin Melemciuc
+
+Date: April 2017
+
+@ Copyright Diffblue, Ltd.
+
+\*******************************************************************/
+
+#ifndef CPROVER_POINTER_ANALYSIS_DYNAMIC_OBJECT_NAME_H
+#define CPROVER_POINTER_ANALYSIS_DYNAMIC_OBJECT_NAME_H
+
+#include <string>
+
+#include <util/std_expr.h>
+
+/*******************************************************************\
+
+Function: get_dynamic_object_name
+
+  Inputs: dynamic_object: The dynamic-object.
+
+ Outputs: The name of the dynamic-object, composed of the
+          "value_set::dynamic_object",
+          it's instance,
+          and the keyword "most_recent_allocation" or
+          "any_allocation".
+
+ Purpose: To generate a name for dynamic-objects suitable for use
+          in the LHS of value-set maps.
+
+\*******************************************************************/
+
+inline std::string get_dynamic_object_name(
+  const dynamic_object_exprt &dynamic_object)
+{
+  std::string name=
+    "value_set::dynamic_object"+
+    std::to_string(dynamic_object.get_instance());
+
+  if(dynamic_object.get_recency()==
+    dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION)
+  {
+    name+=as_string(ID_most_recent_allocation);
+  }
+  else if(dynamic_object.get_recency()==
+    dynamic_object_exprt::recencyt::ANY_ALLOCATION)
+  {
+    name+=as_string(ID_any_allocation);
+  }
+
+  return name;
+}
+
+#endif // CPROVER_POINTER_ANALYSIS_DYNAMIC_OBJECT_NAME_H

src/pointer-analysis/value_set.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "value_set.h"
 #include "add_failed_symbols.h"
+#include "dynamic_object_name.h"
 
 const value_sett::object_map_dt value_sett::object_map_dt::blank;
 object_numberingt value_sett::object_numbering;
@@ -808,11 +809,12 @@ void value_sett::get_value_set_rec(
       const typet &dynamic_type=
         static_cast<const typet &>(expr.find("#type"));
 
-      dynamic_object_exprt dynamic_object(dynamic_type);
-      dynamic_object.set_instance(location_number);
-      dynamic_object.valid()=true_exprt();
+      // Create the most-recent-allocation dynamic-object
+      dynamic_object_exprt dynamic_object_recent(dynamic_type, true);
+      dynamic_object_recent.set_instance(location_number);
+      dynamic_object_recent.valid()=true_exprt();
 
-      insert(dest, dynamic_object, 0);
+      insert(dest, dynamic_object_recent, 0);
     }
     else if(statement==ID_cpp_new ||
             statement==ID_cpp_new_array)
@@ -902,10 +904,7 @@ void value_sett::get_value_set_rec(
   {
     const dynamic_object_exprt &dynamic_object=
       to_dynamic_object_expr(expr);
-
-    const std::string prefix=
-      "value_set::dynamic_object"+
-      std::to_string(dynamic_object.get_instance());
+    std::string prefix=get_dynamic_object_name(dynamic_object);
 
     // first try with suffix
     const std::string full_name=prefix+suffix;
@@ -1466,9 +1465,12 @@ void value_sett::do_free(
     {
       const dynamic_object_exprt &dynamic_object=
         to_dynamic_object_expr(object);
+      dynamic_object_idt key_dynamic_object=std::make_pair(
+        dynamic_object.get_instance(),
+        dynamic_object.get_recency());
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.get_instance());
+        to_mark.insert(key_dynamic_object);
     }
   }
 
@@ -1497,7 +1499,11 @@ void value_sett::do_free(
         const dynamic_object_exprt &dynamic_object=
           to_dynamic_object_expr(object);
 
-        if(to_mark.count(dynamic_object.get_instance())==0)
+        dynamic_object_idt key_dynamic_object=std::make_pair(
+          dynamic_object.get_instance(),
+          dynamic_object.get_recency());
+
+        if(to_mark.count(key_dynamic_object)==0)
           set(new_object_map, o_it);
         else
         {
@@ -1564,10 +1570,7 @@ void value_sett::assign_rec(
   {
     const dynamic_object_exprt &dynamic_object=
       to_dynamic_object_expr(lhs);
-
-    const std::string name=
-      "value_set::dynamic_object"+
-      std::to_string(dynamic_object.get_instance());
+    std::string name=get_dynamic_object_name(dynamic_object);
 
     entryt &e=get_entry(entryt(name, suffix), lhs.type(), ns);
 

src/pointer-analysis/value_set.h

@@ -126,7 +126,9 @@ class value_sett
 
   typedef std::set<exprt> expr_sett;
 
-  typedef std::set<unsigned int> dynamic_object_id_sett;
+  typedef std::pair<unsigned int, dynamic_object_exprt::recencyt>
+    dynamic_object_idt;
+  typedef std::set<dynamic_object_idt> dynamic_object_id_sett;
 
   #ifdef USE_DSTRING
   typedef std::map<idt, entryt> valuest;

src/pointer-analysis/value_set_fi.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/c_types.h>
 
 #include "value_set_fi.h"
+#include "dynamic_object_name.h"
 
 const value_set_fit::object_map_dt value_set_fit::object_map_dt::blank;
 object_numberingt value_set_fit::object_numbering;
@@ -771,11 +772,7 @@ void value_set_fit::get_value_set_rec(
   {
     const dynamic_object_exprt &dynamic_object=
       to_dynamic_object_expr(expr);
-
-    const std::string name=
-      "value_set::dynamic_object"+
-      std::to_string(dynamic_object.get_instance())+
-      suffix;
+    std::string name=get_dynamic_object_name(dynamic_object)+suffix;
 
     // look it up
     valuest::const_iterator v_it=values.find(name);
@@ -1330,9 +1327,12 @@ void value_set_fit::do_free(
     {
       const dynamic_object_exprt &dynamic_object=
         to_dynamic_object_expr(object);
+      dynamic_object_idt key_dynamic_object=std::make_pair(
+        dynamic_object.get_instance(),
+        dynamic_object.get_recency());
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.get_instance());
+        to_mark.insert(key_dynamic_object);
     }
   }
 
@@ -1357,8 +1357,11 @@ void value_set_fit::do_free(
       {
         const dynamic_object_exprt &dynamic_object=
           to_dynamic_object_expr(object);
+        dynamic_object_idt key_dynamic_object=std::make_pair(
+          dynamic_object.get_instance(),
+          dynamic_object.get_recency());
 
-        if(to_mark.count(dynamic_object.get_instance())==0)
+        if(to_mark.count(key_dynamic_object)==0)
           set(new_object_map, o_it);
         else
         {
@@ -1447,10 +1450,7 @@ void value_set_fit::assign_rec(
   {
     const dynamic_object_exprt &dynamic_object=
       to_dynamic_object_expr(lhs);
-
-    const std::string name=
-      "value_set::dynamic_object"+
-      std::to_string(dynamic_object.get_instance());
+    std::string name=get_dynamic_object_name(dynamic_object);
 
     if(make_union(get_entry(name, suffix).object_map, values_rhs))
       changed = true;

src/pointer-analysis/value_set_fi.h

@@ -20,6 +20,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "object_numbering.h"
 
+#include <util/std_expr.h>
+
 class value_set_fit
 {
 public:
@@ -155,7 +157,9 @@ class value_set_fit
 
   typedef std::unordered_set<exprt, irep_hash> expr_sett;
 
-  typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
+  typedef std::pair<unsigned int, dynamic_object_exprt::recencyt>
+    dynamic_object_idt;
+  typedef std::set<dynamic_object_idt> dynamic_object_id_sett;
 
   #ifdef USE_DSTRING
   typedef std::map<idt, entryt> valuest;

src/pointer-analysis/value_set_fivr.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected],
 #include <ansi-c/c_types.h>
 
 #include "value_set_fivr.h"
+#include "dynamic_object_name.h"
 
 const value_set_fivrt::object_map_dt value_set_fivrt::object_map_dt::blank;
 object_numberingt value_set_fivrt::object_numbering;
@@ -897,11 +898,7 @@ void value_set_fivrt::get_value_set_rec(
   {
     const dynamic_object_exprt &dynamic_object=
       to_dynamic_object_expr(expr);
-
-    const std::string name=
-      "value_set::dynamic_object"+
-      std::to_string(dynamic_object.get_instance())+
-      suffix;
+    std::string name=get_dynamic_object_name(dynamic_object)+suffix;
 
     // look it up
     valuest::const_iterator v_it=values.find(name);
@@ -1454,9 +1451,12 @@ void value_set_fivrt::do_free(
     {
       const dynamic_object_exprt &dynamic_object=
         to_dynamic_object_expr(object);
+      dynamic_object_idt key_dynamic_object=std::make_pair(
+        dynamic_object.get_instance(),
+        dynamic_object.get_recency());
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.get_instance());
+        to_mark.insert(key_dynamic_object);
     }
   }
 
@@ -1481,8 +1481,11 @@ void value_set_fivrt::do_free(
       {
         const dynamic_object_exprt &dynamic_object=
           to_dynamic_object_expr(object);
+        dynamic_object_idt key_dynamic_object=std::make_pair(
+           dynamic_object.get_instance(),
+           dynamic_object.get_recency());
 
-        if(to_mark.count(dynamic_object.get_instance())==0)
+        if(to_mark.count(key_dynamic_object)==0)
           set(new_object_map, o_it);
         else
         {
@@ -1585,10 +1588,7 @@ void value_set_fivrt::assign_rec(
   {
     const dynamic_object_exprt &dynamic_object=
       to_dynamic_object_expr(lhs);
-
-    const std::string name=
-      "value_set::dynamic_object"+
-      std::to_string(dynamic_object.get_instance());
+    std::string name=get_dynamic_object_name(dynamic_object);
 
     entryt &temp_entry=get_temporary_entry(name, suffix);
 

src/pointer-analysis/value_set_fivr.h

@@ -13,13 +13,16 @@ Author: Daniel Kroening, [email protected]
 #include <list>
 #include <map>
 #include <unordered_set>
+#include <set>
 
 #include <util/mp_arith.h>
 #include <util/namespace.h>
 #include <util/reference_counting.h>
 
 #include "object_numbering.h"
 
+#include <util/std_expr.h>
+
 class value_set_fivrt
 {
 public:
@@ -216,7 +219,9 @@ class value_set_fivrt
 
   typedef std::unordered_set<exprt, irep_hash> expr_sett;
 
-  typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
+  typedef std::pair<unsigned int, dynamic_object_exprt::recencyt>
+    dynamic_object_idt;
+  typedef std::set<dynamic_object_idt> dynamic_object_id_sett;
 
   #ifdef USE_DSTRING
   typedef std::map<idt, entryt> valuest;

src/pointer-analysis/value_set_fivrns.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected],
 #include <ansi-c/c_types.h>
 
 #include "value_set_fivrns.h"
+#include "dynamic_object_name.h"
 
 const value_set_fivrnst::object_map_dt value_set_fivrnst::object_map_dt::blank;
 object_numberingt value_set_fivrnst::object_numbering;
@@ -671,11 +672,7 @@ void value_set_fivrnst::get_value_set_rec(
   {
     const dynamic_object_exprt &dynamic_object=
       to_dynamic_object_expr(expr);
-
-    const std::string name=
-      "value_set::dynamic_object"+
-      std::to_string(dynamic_object.get_instance())+
-      suffix;
+    std::string name=get_dynamic_object_name(dynamic_object)+suffix;
 
     // look it up
     valuest::const_iterator v_it=values.find(name);
@@ -1113,9 +1110,12 @@ void value_set_fivrnst::do_free(
     {
       const dynamic_object_exprt &dynamic_object=
         to_dynamic_object_expr(object);
+      dynamic_object_idt key_dynamic_object=std::make_pair(
+        dynamic_object.get_instance(),
+        dynamic_object.get_recency());
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.get_instance());
+        to_mark.insert(key_dynamic_object);
     }
   }
 
@@ -1140,8 +1140,11 @@ void value_set_fivrnst::do_free(
       {
         const dynamic_object_exprt &dynamic_object=
           to_dynamic_object_expr(object);
+        dynamic_object_idt key_dynamic_object=std::make_pair(
+          dynamic_object.get_instance(),
+          dynamic_object.get_recency());
 
-        if(to_mark.count(dynamic_object.get_instance())==0)
+        if(to_mark.count(key_dynamic_object)==0)
           set(new_object_map, o_it);
         else
         {
@@ -1220,10 +1223,7 @@ void value_set_fivrnst::assign_rec(
   {
     const dynamic_object_exprt &dynamic_object=
       to_dynamic_object_expr(lhs);
-
-    const std::string name=
-      "value_set::dynamic_object"+
-      std::to_string(dynamic_object.get_instance());
+    std::string name=get_dynamic_object_name(dynamic_object);
 
     entryt &temp_entry = get_temporary_entry(name, suffix);