Merge pull request diffblue#47 from diffblue/feature/sensitive-pointers

Sensitive pointers

Author: danpoe

src/analyses/Makefile

@@ -15,6 +15,7 @@ SRC = natural_loops.cpp is_threaded.cpp dirty.cpp interval_analysis.cpp \
       variable-sensitivity/pointer_abstract_object.cpp \
       variable-sensitivity/struct_abstract_object.cpp \
       variable-sensitivity/array_abstract_object.cpp \
+      variable-sensitivity/constant_pointer_abstract_object.cpp \
       # Empty last line
 
 INCLUDES= -I ..

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -14,6 +14,7 @@
 #include <analyses/variable-sensitivity/struct_abstract_object.h>
 #include <analyses/variable-sensitivity/pointer_abstract_object.h>
 #include <analyses/variable-sensitivity/array_abstract_object.h>
+#include <analyses/variable-sensitivity/constant_pointer_abstract_object.h>
 #include <analyses/ai.h>
 #include <analyses/constant_propagator.h>
 #include <util/simplify_expr.h>
@@ -60,7 +61,7 @@ abstract_object_pointert abstract_environmentt::eval(
       ID_constant, [&](const exprt &expr)
       {
         return abstract_object_factory(
-          expr.type(), to_constant_expr(expr));
+          expr.type(), to_constant_expr(expr), ns);
       }
     },
     {
@@ -77,12 +78,12 @@ abstract_object_pointert abstract_environmentt::eval(
     {
       ID_address_of, [&](const exprt &expr)
       {
-  #if 0
-        address_of_exprt address_expr(to_address_of_expr(expr));
-  #endif
-        // TODO(tkiley): This needs special handling
-        // For now just return top
-        return abstract_object_factory(expr.type(), true, false);
+        sharing_ptrt<pointer_abstract_objectt> pointer_object=
+          std::dynamic_pointer_cast<pointer_abstract_objectt>(
+            abstract_object_factory(expr.type(), expr, ns));
+
+        // Store the abstract object in the pointer
+        return pointer_object;
       }
     },
     {
@@ -93,7 +94,7 @@ abstract_object_pointert abstract_environmentt::eval(
           std::dynamic_pointer_cast<pointer_abstract_objectt>(
             eval(dereference.pointer(), ns));
 
-        return pointer_abstract_object->read_dereference(*this);
+        return pointer_abstract_object->read_dereference(*this, ns);
       }
     },
     {
@@ -139,6 +140,7 @@ Function: abstract_environmentt::assign
   Inputs:
    expr - the expression to assign to
    value - the value to assign to the expression
+   ns - the namespace
 
  Outputs: A boolean, true if the assignment has changed the domain.
 
@@ -147,11 +149,14 @@ Function: abstract_environmentt::assign
 \*******************************************************************/
 
 bool abstract_environmentt::assign(
-  const exprt &expr, const abstract_object_pointert value)
+  const exprt &expr, const abstract_object_pointert value, const namespacet &ns)
 {
+  assert(value);
+
+  // Build a stack of index, member and dereference accesses which
+  // we will work through the relevant abstract objects
   exprt s = expr;
   std::stack<exprt> stactions;    // I'm not a continuation, honest guv'
-
   while (s.id() != ID_symbol)
   {
     if (s.id() == ID_index || s.id() == ID_member || s.id() == ID_dereference)
@@ -169,76 +174,12 @@ bool abstract_environmentt::assign(
 
   symbol_exprt symbol_expr=to_symbol_expr(s);
 
+  // This is the root abstract object that is in the map of abstract objects
+  // It might not have the same type as value if the above stack isn't empty
   abstract_object_pointert final_value;
 
   if(!stactions.empty())
   {
-    const exprt & next_expr=stactions.top();
-    stactions.pop();
-
-    typedef std::function<
-      abstract_object_pointert(
-        abstract_object_pointert,  // The symbol we are modifying
-        std::stack<exprt>, // The remaining stack
-        abstract_object_pointert)> // The value we are writing.
-        stacion_functiont;
-
-    // Each handler takes the abstract object referenced, copies it,
-    // writes according to the type of expression (e.g. for ID_member)
-    // we would (should!) have an abstract_struct_objectt which has a
-    // write_member which will attempt to update the abstract object for the
-    // relevant member. This modified abstract object is returned and this
-    // is inserted back into the map
-    std::map<irep_idt,stacion_functiont> handlers=
-    {
-      {
-        ID_index, [&](
-          const abstract_object_pointert lhs_object,
-          std::stack<exprt> stack,
-          abstract_object_pointert rhs_object)
-        {
-          sharing_ptrt<array_abstract_objectt> array_abstract_object=
-            std::dynamic_pointer_cast<array_abstract_objectt>(lhs_object);
-          sharing_ptrt<array_abstract_objectt> modified_array=
-            array_abstract_object->write_index(
-              *this, stactions, to_index_expr(next_expr), rhs_object, false);
-          return modified_array;
-        }
-      },
-      {
-        ID_member, [&](
-          const abstract_object_pointert lhs_object,
-          std::stack<exprt> stack,
-          abstract_object_pointert rhs_object)
-        {
-          sharing_ptrt<struct_abstract_objectt> struct_abstract_object=
-            std::dynamic_pointer_cast<struct_abstract_objectt>(lhs_object);
-          sharing_ptrt<struct_abstract_objectt> modified_struct=
-            struct_abstract_object->write_component(
-              *this, stactions, to_member_expr(next_expr), rhs_object);
-          return modified_struct;
-        }
-      },
-      {
-        ID_dereference, [&](
-          const abstract_object_pointert lhs_object,
-          std::stack<exprt> stack,
-          abstract_object_pointert rhs_object)
-        {
-          sharing_ptrt<pointer_abstract_objectt> pointer_abstract_object=
-            std::dynamic_pointer_cast<pointer_abstract_objectt>(lhs_object);
-          sharing_ptrt<pointer_abstract_objectt> modified_pointer=
-            pointer_abstract_object->write_dereference(
-              *this, stactions, rhs_object, false);
-          return modified_pointer;
-        }
-      }
-    };
-
-    // We added something to the stack that we couldn't deal with
-    assert(handlers.find(next_expr.id())!=handlers.end());
-    assert(value);
-
     // The symbol is not in the map - it is therefore top
     abstract_object_pointert symbol_object;
     if(map.find(symbol_expr)==map.end())
@@ -249,7 +190,7 @@ bool abstract_environmentt::assign(
     {
       symbol_object=map[symbol_expr];
     }
-    final_value=handlers[next_expr.id()](symbol_object, stactions, value);
+    final_value=write(symbol_object, value, stactions, ns, false);
   }
   else
   {
@@ -261,7 +202,6 @@ bool abstract_environmentt::assign(
   if (final_value->is_top())
   {
     map.erase(symbol_expr);
-
   }
   else
   {
@@ -272,6 +212,120 @@ bool abstract_environmentt::assign(
 
 /*******************************************************************\
 
+Function: abstract_object_pointert abstract_environmentt::write
+
+  Inputs:
+   lhs - the abstract object for the left hand side of the write (i.e. the one
+         to update).
+   rhs - the value we are trying to write to the left hand side
+   remaining_stack - what is left of the stack before the rhs can replace or be
+                     merged with the rhs
+   ns - the namespace
+   merge_write - Are re replacing the left hand side with the right hand side
+                 (e.g. we know for a fact that we are overwriting this object)
+                 or could the write in fact not take place and therefore we
+                 should merge to model the case where it did not.
+
+ Outputs: A modified version of the rhs after the write has taken place
+
+ Purpose: Write an abstract object onto another respecting a stack of
+          member, index and dereference access. This ping-pongs between
+          this method and the relevant write methods in abstract_struct,
+          abstract_pointer and abstract_array until the stack is empty
+
+\*******************************************************************/
+
+abstract_object_pointert abstract_environmentt::write(
+  abstract_object_pointert lhs,
+  abstract_object_pointert rhs,
+  std::stack<exprt> remaining_stack,
+  const namespacet &ns,
+  bool merge_write)
+{
+  assert(!remaining_stack.empty());
+  const exprt & next_expr=remaining_stack.top();
+  remaining_stack.pop();
+
+  typedef std::function<
+    abstract_object_pointert(
+      abstract_object_pointert,  // The symbol we are modifying
+      std::stack<exprt>, // The remaining stack
+      abstract_object_pointert)> // The value we are writing.
+      stacion_functiont;
+
+  // Each handler takes the abstract object referenced, copies it,
+  // writes according to the type of expression (e.g. for ID_member)
+  // we would (should!) have an abstract_struct_objectt which has a
+  // write_member which will attempt to update the abstract object for the
+  // relevant member. This modified abstract object is returned and this
+  // is inserted back into the map
+  std::map<irep_idt, stacion_functiont> handlers=
+  {
+    {
+      ID_index, [&](
+        const abstract_object_pointert lhs_object,
+        std::stack<exprt> stack,
+        abstract_object_pointert rhs_object)
+      {
+        sharing_ptrt<array_abstract_objectt> array_abstract_object=
+          std::dynamic_pointer_cast<array_abstract_objectt>(lhs_object);
+
+        sharing_ptrt<array_abstract_objectt> modified_array=
+          array_abstract_object->write_index(
+            *this,
+            stack,
+            to_index_expr(next_expr),
+            rhs_object,
+            merge_write);
+
+        return modified_array;
+      }
+    },
+    {
+      ID_member, [&](
+        const abstract_object_pointert lhs_object,
+        std::stack<exprt> stack,
+        abstract_object_pointert rhs_object)
+      {
+        sharing_ptrt<struct_abstract_objectt> struct_abstract_object=
+          std::dynamic_pointer_cast<struct_abstract_objectt>(lhs_object);
+
+        sharing_ptrt<struct_abstract_objectt> modified_struct=
+          struct_abstract_object->write_component(
+            *this,
+            stack,
+            to_member_expr(next_expr),
+            rhs_object,
+            merge_write);
+
+        return modified_struct;
+      }
+    },
+    {
+      ID_dereference, [&](
+        const abstract_object_pointert lhs_object,
+        std::stack<exprt> stack,
+        abstract_object_pointert rhs_object)
+      {
+        sharing_ptrt<pointer_abstract_objectt> pointer_abstract_object=
+          std::dynamic_pointer_cast<pointer_abstract_objectt>(lhs_object);
+
+        sharing_ptrt<pointer_abstract_objectt> modified_pointer=
+          pointer_abstract_object->write_dereference(
+            *this, ns, stack, rhs_object, merge_write);
+
+        return modified_pointer;
+      }
+    }
+  };
+
+  // We added something to the stack that we couldn't deal with
+  assert(handlers.find(next_expr.id())!=handlers.end());
+  return handlers[next_expr.id()](lhs, remaining_stack, rhs);
+}
+
+/*******************************************************************\
+
 Function: abstract_environmentt::assume
 
   Inputs:
@@ -339,6 +393,11 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory(
     return abstract_object_pointert(
       new constant_abstract_valuet(type, top, bottom));
   }
+  else if(type.id()==ID_pointer)
+  {
+    return abstract_object_pointert(
+      new constant_pointer_abstract_objectt(type, top, bottom, *this));
+  }
   else
   {
     return abstract_object_pointert(new abstract_objectt(type, top, false));
@@ -361,14 +420,19 @@ Function: abstract_environmentt::abstract_object_factory
 \*******************************************************************/
 
 abstract_object_pointert abstract_environmentt::abstract_object_factory(
-  const typet type, const constant_exprt e) const
+  const typet type, const exprt e, const namespacet &ns) const
 {
   assert(type==e.type());
   if(type.id()==ID_signedbv || type.id()==ID_bool || type.id()==ID_c_bool)
   {
     return abstract_object_pointert(
       new constant_abstract_valuet(e));
   }
+  else if(type.id()==ID_pointer)
+  {
+    return abstract_object_pointert(
+      new constant_pointer_abstract_objectt(e, *this, ns));
+  }
   else
   {
     return abstract_object_pointert(new abstract_objectt(e));
@@ -401,7 +465,6 @@ bool abstract_environmentt::merge(const abstract_environmentt &env)
 
   std::stringstream merge_message;
 
-
   ait<constant_propagator_domaint> ai;
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);

src/analyses/variable-sensitivity/abstract_enviroment.h

@@ -10,6 +10,7 @@
 
 #include <map>
 #include <memory>
+#include <stack>
 
 #include <util/std_expr.h>
 #include <util/message.h>
@@ -21,15 +22,25 @@ class abstract_environmentt
   // These three are really the heart of the method
   virtual abstract_object_pointert eval(
     const exprt &expr, const namespacet &ns) const;
-  virtual bool assign(const exprt &expr, const abstract_object_pointert value);
+  virtual bool assign(
+    const exprt &expr,
+    const abstract_object_pointert value,
+    const namespacet &ns);
   virtual bool assume(const exprt &expr, const namespacet &ns);
 
+  virtual abstract_object_pointert write(
+    abstract_object_pointert lhs,
+    abstract_object_pointert rhs,
+    std::stack<exprt> remaining_stack,
+    const namespacet &ns,
+    bool merge_write);
+
   virtual abstract_object_pointert abstract_object_factory(
     const typet type, bool top=true, bool bottom=false) const;
   // For converting constants in the program
   // Maybe these two should be compacted to one call...
   virtual abstract_object_pointert abstract_object_factory(
-    const typet type, const constant_exprt e) const;
+    const typet type, const exprt e, const namespacet &ns) const;
 
 
   virtual bool merge(const abstract_environmentt &env);
@@ -61,6 +72,8 @@ class abstract_environmentt
  // Hook for domain specific handling of operators
  virtual abstract_object_pointert eval_rest(const exprt &e) const;
 
+
+
  typedef symbol_exprt map_keyt;
  std::map<map_keyt, abstract_object_pointert> map;
 

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -87,7 +87,7 @@ Function: abstract_objectt::abstract_objectt
 
 \*******************************************************************/
 
-abstract_objectt::abstract_objectt(const constant_exprt &expr):
+abstract_objectt::abstract_objectt(const exprt &expr):
 type(expr.type()), top(true), bottom(false)
 {}
 
@@ -123,8 +123,8 @@ bool abstract_objectt::merge_state(
   top=op1->top||op2->top;
   bottom=op1->bottom && op2->bottom;
 
-  return top!=op1->top || bottom!=op1->bottom;
   assert(!(top && bottom));
+  return top!=op1->top || bottom!=op1->bottom;
 }
 
 /*******************************************************************\