Merge pull request diffblue#1 from mariusmc92/security_scanner_support

Updated LVSA data structures for Recency Analysis

Author: smowton

src/pointer-analysis/value_set.cpp

@@ -195,7 +195,17 @@ void value_sett::output(
       else
       {
         result="<"+from_expr(ns, identifier, o)+", ";
-
+        if(o.id()==ID_dynamic_object)
+        {
+          dynamic_object_exprt::recencyt recency=
+            to_dynamic_object_expr(o).get_recency();
+            
+          if(recency==dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION)
+            result+=as_string(ID_most_recent_allocation)+", ";
+          else if(recency==dynamic_object_exprt::recencyt::ANY_ALLOCATION)
+            result+=as_string(ID_any_allocation)+", ";
+        }
+        
         if(o_it->second.offset_is_set)
           result+=integer2string(o_it->second.offset)+"";
         else
@@ -894,10 +904,23 @@ void value_sett::get_value_set_rec(
   {
     const dynamic_object_exprt &dynamic_object=
       to_dynamic_object_expr(expr);
+    std::string recency_str="";
+
+    if(dynamic_object.get_recency()==
+      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=as_string(ID_any_allocation);
+    }
 
     const std::string prefix=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      dynamic_object.instance().get_string(ID_value)+
+      recency_str;
 
     // first try with suffix
     const std::string full_name=prefix+suffix;
@@ -1532,10 +1555,23 @@ void value_sett::assign_rec(
   {
     const dynamic_object_exprt &dynamic_object=
       to_dynamic_object_expr(lhs);
+    std::string recency_str="";
+
+    if(dynamic_object.get_recency()==
+      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=as_string(ID_any_allocation);
+    }
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      dynamic_object.instance().get_string(ID_value)+
+      recency_str;
 
     entryt &e=get_entry(entryt(name, suffix), lhs.type(), ns);
 

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();