Updated LVSA data structures for Recency Analysis

Added recency to dynamic-objects' class.
Minor coding style changes to the
recency output of the LVSA.

Author: mariusmc92

src/pointer-analysis/value_set.cpp

@@ -194,22 +194,18 @@ void value_sett::output(
         result=from_expr(ns, identifier, o);
       else
       {
+        result="<"+from_expr(ns, identifier, o)+", ";
         if(o.id()==ID_dynamic_object)
         {
-          dynamic_object_exprt::recencyt recency;
-          std::string recency_str="";
-
-          recency=to_dynamic_object_expr(o).get_recency();
+          dynamic_object_exprt::recencyt recency=
+            to_dynamic_object_expr(o).get_recency();
+            
           if(recency==dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION)
-            recency_str="most-recent-allocation";
+            result+=as_string(ID_most_recent_allocation)+", ";
           else if(recency==dynamic_object_exprt::recencyt::ANY_ALLOCATION)
-            recency_str="any-allocation";
-          result="<"+from_expr(ns, identifier, o)+", "+recency_str+", ";
-        }
-        else
-        {
-          result="<"+from_expr(ns, identifier, o)+", ";
+            result+=as_string(ID_any_allocation)+", ";
         }
+        
         if(o_it->second.offset_is_set)
           result+=integer2string(o_it->second.offset)+"";
         else
@@ -911,11 +907,15 @@ void value_sett::get_value_set_rec(
     std::string recency_str="";
 
     if(dynamic_object.get_recency()==
-       dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION)
-      recency_str="most-recent-allocation";
+      dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION)
+    {
+      recency_str=as_string(ID_most_recent_allocation);
+    }
     else if(dynamic_object.get_recency()==
-            dynamic_object_exprt::recencyt::ANY_ALLOCATION)
-      recency_str="any-allocation";
+      dynamic_object_exprt::recencyt::ANY_ALLOCATION)
+    {
+      recency_str=as_string(ID_any_allocation);
+    }
 
     const std::string prefix=
       "value_set::dynamic_object"+
@@ -1558,11 +1558,15 @@ void value_sett::assign_rec(
     std::string recency_str="";
 
     if(dynamic_object.get_recency()==
-       dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION)
-      recency_str="most-recent-allocation";
+      dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION)
+    {
+      recency_str=as_string(ID_most_recent_allocation);
+    }
     else if(dynamic_object.get_recency()==
-            dynamic_object_exprt::recencyt::ANY_ALLOCATION)
-      recency_str="any-allocation";
+      dynamic_object_exprt::recencyt::ANY_ALLOCATION)
+    {
+      recency_str=as_string(ID_any_allocation);
+    }
 
     const std::string name=
       "value_set::dynamic_object"+

src/util/irep_ids.txt

@@ -511,6 +511,9 @@ overflow_mult overflow-*
 overflow_unary_minus overflow-unary-
 object_descriptor
 dynamic_object
+is_most_recent_allocation
+most_recent_allocation
+any_allocation
 object_size
 good_pointer
 integer_address

src/util/std_expr.h

@@ -1490,6 +1490,8 @@ inline object_descriptor_exprt &to_object_descriptor_expr(exprt &expr)
 class dynamic_object_exprt:public exprt
 {
 public:
+  enum recencyt { MOST_RECENT_ALLOCATION, ANY_ALLOCATION, RECENCY_UNSET };
+
   dynamic_object_exprt():exprt(ID_dynamic_object)
   {
     operands().resize(2);
@@ -1505,6 +1507,40 @@ class dynamic_object_exprt:public exprt
     op1().id(ID_unknown);
   }
 
+  explicit dynamic_object_exprt(bool recent):
+    exprt(ID_dynamic_object)
+  {
+    operands().resize(2);
+    op0().id(ID_unknown);
+    op1().id(ID_unknown);
+    set_recency(recent);
+  }
+
+  dynamic_object_exprt(const typet &type, bool recent):
+    exprt(ID_dynamic_object, type)
+  {
+    operands().resize(2);
+    op0().id(ID_unknown);
+    op1().id(ID_unknown);
+    set_recency(recent);
+  }
+
+  recencyt get_recency() const
+  {
+    if(get(ID_is_most_recent_allocation)==ID_most_recent_allocation)
+      return MOST_RECENT_ALLOCATION;
+    else if(get(ID_is_most_recent_allocation)==ID_any_allocation)
+      return ANY_ALLOCATION;
+    else
+      return RECENCY_UNSET;
+  }
+
+  void set_recency(bool recent)
+  {
+    set(ID_is_most_recent_allocation,
+      (recent ? ID_most_recent_allocation : ID_any_allocation));
+  }
+
   exprt &instance()
   {
     return op0();