Merge pull request diffblue#50 from diffblue/feature/tests-for-sensitivity

Feature/tests for sensitivity

Author: danpoe

src/analyses/Makefile

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

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -15,12 +15,12 @@
 #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/variable-sensitivity/variable_sensitivity_object_factory.h>
 #include <analyses/ai.h>
 #include <analyses/constant_propagator.h>
 #include <util/simplify_expr.h>
 
 
-
 /*******************************************************************\
 
 Function: abstract_environmentt::eval
@@ -36,7 +36,7 @@ Function: abstract_environmentt::eval
 \*******************************************************************/
 
 abstract_object_pointert abstract_environmentt::eval(
-  const exprt &expr, const namespacet &ns) const
+  const exprt &e, const namespacet &ns) const
 {
   assert(!is_bottom);
   typedef std::function<abstract_object_pointert(const exprt &)> eval_handlert;
@@ -49,7 +49,7 @@ abstract_object_pointert abstract_environmentt::eval(
         const auto &symbol_entry=map.find(symbol);
         if(symbol_entry==map.cend())
         {
-          return abstract_object_factory(expr.type(), true);
+          return abstract_object_factory(expr.type(), ns, true);
         }
         else
         {
@@ -72,7 +72,7 @@ abstract_object_pointert abstract_environmentt::eval(
           std::dynamic_pointer_cast<struct_abstract_objectt>(
             eval(member_expr.compound(), ns));
 
-        return struct_abstract_object->read_component(*this, member_expr);
+        return struct_abstract_object->read_component(*this, member_expr, ns);
       }
     },
     {
@@ -105,13 +105,13 @@ abstract_object_pointert abstract_environmentt::eval(
           std::dynamic_pointer_cast<array_abstract_objectt>(
             eval(index_expr.array(), ns));
 
-        return array_abstract_object->read_index(*this, index_expr);
+        return array_abstract_object->read_index(*this, index_expr, ns);
       }
     }
   };
 
   // first try to collapse constant folding
-  const exprt &simplified_expr=simplify_expr(expr, ns);
+  const exprt &simplified_expr=simplify_expr(e, ns);
 
   const auto &handler=handlers.find(simplified_expr.id());
   if(handler==handlers.cend())
@@ -124,7 +124,7 @@ abstract_object_pointert abstract_environmentt::eval(
     }
     else
     {
-      return abstract_object_factory(simplified_expr.type(), true);
+      return abstract_object_factory(simplified_expr.type(), ns, true);
     }
   }
   else
@@ -184,7 +184,8 @@ bool abstract_environmentt::assign(
     abstract_object_pointert symbol_object;
     if(map.find(symbol_expr)==map.end())
     {
-      symbol_object=abstract_object_factory(symbol_expr.type(), true, false);
+      symbol_object=abstract_object_factory(
+        symbol_expr.type(), ns, true, false);
     }
     else
     {
@@ -376,6 +377,7 @@ Function: abstract_environmentt::abstract_object_factory
   Inputs:
    type - the type of the object whose state should be tracked
    top - does the type of the object start as top
+   bottom - does the type of the object start as bottom in the two-value domain
 
  Outputs: The abstract object that has been created
 
@@ -385,23 +387,10 @@ Function: abstract_environmentt::abstract_object_factory
 \*******************************************************************/
 
 abstract_object_pointert abstract_environmentt::abstract_object_factory(
-  const typet type, bool top, bool bottom) const
+  const typet type, const namespacet &ns, bool top, bool bottom) const
 {
-  // TODO (tkiley): Here we should look at some config file
-  if(type.id()==ID_signedbv || type.id()==ID_bool || type.id()==ID_c_bool)
-  {
-    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));
-  }
+  exprt empty_constant_expr=exprt();
+  return abstract_object_factory(type, top, bottom, empty_constant_expr, ns);
 }
 
 /*******************************************************************\
@@ -420,23 +409,34 @@ Function: abstract_environmentt::abstract_object_factory
 \*******************************************************************/
 
 abstract_object_pointert abstract_environmentt::abstract_object_factory(
-  const typet type, const exprt e, const namespacet &ns) 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));
-  }
+  return abstract_object_factory(type, false, false, e, ns);
+}
+
+/*******************************************************************\
+
+Function: abstract_environmentt::abstract_object_factory
+
+  Inputs:
+   type - the type of the object whose state should be tracked
+   top - does the type of the object start as top in the two-value domain
+   bottom - does the type of the object start as bottom in the two-value domain
+   expr - the starting value of the symbol if top and bottom are both false
+
+ Outputs: The abstract object that has been created
+
+ Purpose: Look at the configuration for the sensitivity and create an
+          appropriate abstract_object
+
+\*******************************************************************/
+
+abstract_object_pointert abstract_environmentt::abstract_object_factory(
+  const typet type, bool top, bool bottom, const exprt &e,
+  const namespacet &ns) const
+{
+  return variable_sensitivity_object_factoryt::instance().get_abstract_object(
+    type, top, bottom, e, ns);
 }
 
 /*******************************************************************\
@@ -662,8 +662,3 @@ abstract_object_pointert abstract_environmentt::eval_expression(
   abstract_object_pointert lhs=eval(e.op0(), ns);
   return lhs->expression_transform(e, *this, ns);
 }
-
-abstract_object_pointert abstract_environmentt::eval_rest(const exprt &e) const
-{
-  return abstract_object_factory(e.type());
-}

src/analyses/variable-sensitivity/abstract_enviroment.h

@@ -36,17 +36,21 @@ class abstract_environmentt
     bool merge_write);
 
   virtual abstract_object_pointert abstract_object_factory(
-    const typet type, bool top=true, bool bottom=false) const;
+    const typet type,
+    const namespacet &ns,
+    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 exprt e, const namespacet &ns) const;
+    const typet type, const exprt &e, const namespacet &ns) const;
 
 
   virtual bool merge(const abstract_environmentt &env);
 
   // This should be used as a default case / everything else has failed
-  // The string is so that I can easily find and diagnose cases where this occurs
+  // The string is so that I can easily find and diagnose cases where this
+  // occurs
   virtual void havoc(const std::string &havoc_string);
 
   void make_top();
@@ -69,14 +73,13 @@ class abstract_environmentt
  virtual abstract_object_pointert eval_expression(
     const exprt &e, const namespacet &ns) const;
 
- // 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;
+  typedef symbol_exprt map_keyt;
+  std::map<map_keyt, abstract_object_pointert> map;
 
+private:
+  abstract_object_pointert abstract_object_factory(
+    const typet type, bool top, bool bottom, const exprt &e,
+    const namespacet &ns) const;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -206,7 +206,7 @@ abstract_object_pointert abstract_objectt::expression_transform(
   }
   else
   {
-    return environment.abstract_object_factory(expr.type(), true, false);
+    return environment.abstract_object_factory(expr.type(), ns, true, false);
   }
 }
 

src/analyses/variable-sensitivity/array_abstract_object.cpp

@@ -85,7 +85,7 @@ Function: array_abstract_objectt::array_abstract_objectt
 
 \*******************************************************************/
 
-array_abstract_objectt::array_abstract_objectt(const constant_exprt &e):
+array_abstract_objectt::array_abstract_objectt(const exprt &e):
   abstract_objectt(e)
 {
   assert(e.type().id()==ID_array);
@@ -107,14 +107,16 @@ Function: array_abstract_objectt::read_index
 \*******************************************************************/
 
 abstract_object_pointert array_abstract_objectt::read_index(
-  const abstract_environmentt &env, const index_exprt &index) const
+  const abstract_environmentt &env,
+  const index_exprt &index,
+  const namespacet& ns) const
 {
   array_typet array_type(to_array_type(type));
   const typet &subtype=array_type.subtype();
 
   // if we are bottom then so are the values in the array
   // otherwise the values are top
-  return env.abstract_object_factory(subtype, !is_bottom(), is_bottom());
+  return env.abstract_object_factory(subtype, ns, !is_bottom(), is_bottom());
 }
 
 /*******************************************************************\

src/analyses/variable-sensitivity/array_abstract_object.h

@@ -22,13 +22,15 @@ class array_abstract_objectt:public abstract_objectt
   explicit array_abstract_objectt(const typet &type);
   array_abstract_objectt(const typet &type, bool top, bool bottom);
   explicit array_abstract_objectt(const array_abstract_objectt &old);
-  explicit array_abstract_objectt(const constant_exprt &expr);
+  explicit array_abstract_objectt(const exprt &expr);
 
   CLONE
   MERGE(abstract_objectt)
 
   virtual abstract_object_pointert read_index(
-    const abstract_environmentt &env, const index_exprt &index) const;
+    const abstract_environmentt &env,
+    const index_exprt &index,
+    const namespacet &ns) const;
 
   virtual sharing_ptrt<array_abstract_objectt> write_index(
     abstract_environmentt &environment,

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -276,7 +276,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
     // Return top if dereferencing a null pointer or we are top
     bool is_value_top = top || value.id()==ID_nil;
     return env.abstract_object_factory(
-      type.subtype(), is_value_top, !is_value_top);
+      type.subtype(), ns, is_value_top, !is_value_top);
   }
   else
   {
@@ -287,11 +287,11 @@ abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
     else if(value.id()==ID_constant)
     {
       // Reading a null pointer, return top
-      return env.abstract_object_factory(type.subtype(), true, false);
+      return env.abstract_object_factory(type.subtype(), ns, true, false);
     }
     else
     {
-      return env.abstract_object_factory(type.subtype(), true, false);
+      return env.abstract_object_factory(type.subtype(), ns, true, false);
     }
   }
 }

src/analyses/variable-sensitivity/pointer_abstract_object.cpp

@@ -113,7 +113,7 @@ abstract_object_pointert pointer_abstract_objectt::read_dereference(
   pointer_typet pointer_type(to_pointer_type(type));
   const typet &pointed_to_type=pointer_type.subtype();
 
-  return env.abstract_object_factory(pointed_to_type, true, false);
+  return env.abstract_object_factory(pointed_to_type, ns, true, false);
 }
 
 /*******************************************************************\

src/analyses/variable-sensitivity/struct_abstract_object.cpp

@@ -86,7 +86,7 @@ Function: struct_abstract_objectt::struct_abstract_objectt
 
 \*******************************************************************/
 
-struct_abstract_objectt::struct_abstract_objectt(const constant_exprt &e):
+struct_abstract_objectt::struct_abstract_objectt(const exprt &e):
   abstract_objectt(e)
 {
   assert(e.type().id()==ID_struct);
@@ -111,12 +111,14 @@ Function: struct_abstract_objectt::read_component
 \*******************************************************************/
 
 abstract_object_pointert struct_abstract_objectt::read_component(
-  const abstract_environmentt &environment, const member_exprt &member_expr)
+  const abstract_environmentt &environment,
+  const member_exprt &member_expr,
+  const namespacet& ns)
 {
   // If we are bottom then so are the components
   // otherwise the components could be anything
   return environment.abstract_object_factory(
-    member_expr.type(), !is_bottom(), is_bottom());
+    member_expr.type(), ns, !is_bottom(), is_bottom());
 }
 
 /*******************************************************************\

src/analyses/variable-sensitivity/struct_abstract_object.h

@@ -21,14 +21,16 @@ class struct_abstract_objectt:public abstract_objectt
   explicit struct_abstract_objectt(const typet &type);
   struct_abstract_objectt(const typet &type, bool top, bool bottom);
   explicit struct_abstract_objectt(const struct_abstract_objectt &old);
-  explicit struct_abstract_objectt(const constant_exprt &expr);
+  explicit struct_abstract_objectt(const exprt &expr);
 
   CLONE
   MERGE(abstract_objectt)
 
   // struct interface
   virtual abstract_object_pointert read_component(
-    const abstract_environmentt &environment, const member_exprt &member_expr);
+    const abstract_environmentt &environment,
+    const member_exprt &member_expr,
+    const namespacet& ns);
 
   virtual sharing_ptrt<struct_abstract_objectt> write_component(
     const abstract_environmentt &environment,

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -53,7 +53,7 @@ void variable_sensitivity_domaint::transform(
     // Assign to top is the same as removing
     abstract_object_pointert top_object=
       abstract_state.abstract_object_factory(
-        to_code_dead(instruction.code).symbol().type(), true);
+        to_code_dead(instruction.code).symbol().type(), ns, true);
     abstract_state.assign(
       to_code_dead(instruction.code).symbol(), top_object, ns);
     }