Merge pull request diffblue#45 from diffblue/feature/binary-transforms

Transforms handled by abstract object

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -16,6 +16,7 @@
 #include <analyses/variable-sensitivity/array_abstract_object.h>
 #include <analyses/ai.h>
 #include <analyses/constant_propagator.h>
+#include <util/simplify_expr.h>
 
 
 
@@ -33,7 +34,7 @@ Function: abstract_environmentt::eval
 \*******************************************************************/
 
 abstract_object_pointert abstract_environmentt::eval(
-  const exprt &expr) const
+  const exprt &expr, const namespacet &ns) const
 {
   assert(!is_bottom);
   typedef std::function<abstract_object_pointert(const exprt &)> eval_handlert;
@@ -67,7 +68,7 @@ abstract_object_pointert abstract_environmentt::eval(
         member_exprt member_expr(to_member_expr(expr));
         sharing_ptrt<struct_abstract_objectt> struct_abstract_object=
           std::dynamic_pointer_cast<struct_abstract_objectt>(
-            eval(member_expr.compound()));
+            eval(member_expr.compound(), ns));
 
         return struct_abstract_object->read_component(*this, member_expr);
       }
@@ -80,8 +81,7 @@ abstract_object_pointert abstract_environmentt::eval(
   #endif
         // TODO(tkiley): This needs special handling
         // For now just return top
-        return abstract_object_pointert(
-          new abstract_objectt(expr.type(), true, false));
+        return abstract_object_factory(expr.type(), true, false);
       }
     },
     {
@@ -90,7 +90,7 @@ abstract_object_pointert abstract_environmentt::eval(
         dereference_exprt dereference(to_dereference_expr(expr));
         sharing_ptrt<pointer_abstract_objectt> pointer_abstract_object=
           std::dynamic_pointer_cast<pointer_abstract_objectt>(
-            eval(dereference.pointer()));
+            eval(dereference.pointer(), ns));
 
         return pointer_abstract_object->read_dereference(*this);
       }
@@ -101,21 +101,33 @@ abstract_object_pointert abstract_environmentt::eval(
         index_exprt index_expr(to_index_expr(expr));
         sharing_ptrt<array_abstract_objectt> array_abstract_object=
           std::dynamic_pointer_cast<array_abstract_objectt>(
-            eval(index_expr.array()));
+            eval(index_expr.array(), ns));
 
         return array_abstract_object->read_index(*this, index_expr);
       }
     }
   };
 
-  const auto &handler=handlers.find(expr.id());
+  // first try to collapse constant folding
+  const exprt &simplified_expr=simplify_expr(expr, ns);
+
+  const auto &handler=handlers.find(simplified_expr.id());
   if(handler==handlers.cend())
   {
-    return abstract_object_factory(expr.type(), true);
+    // No special handling required by the abstract environment
+    // delegate to the abstract object
+    if(simplified_expr.operands().size()>0)
+    {
+      return eval_expression(simplified_expr, ns);
+    }
+    else
+    {
+      return abstract_object_factory(simplified_expr.type(), true);
+    }
   }
   else
   {
-    return handler->second(expr);
+    return handler->second(simplified_expr);
   }
 }
 
@@ -233,14 +245,14 @@ bool abstract_environmentt::assign(
   }
 
   // Write the value for the root symbol back into the map
-  if (value->is_top())
+  if (final_value->is_top())
   {
     map.erase(symbol_expr);
 
   }
   else
   {
-    map[symbol_expr]=value;
+    map[symbol_expr]=final_value;
   }
   return true;
 }
@@ -258,9 +270,9 @@ Function: abstract_environmentt::assume
 
 \*******************************************************************/
 
-bool abstract_environmentt::assume(const exprt &expr)
+bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
 {
-  abstract_object_pointert res = eval(expr);
+  abstract_object_pointert res = eval(expr, ns);
   std::string not_implemented_string=__func__;
   not_implemented_string.append(" not implemented");
   throw not_implemented_string;
@@ -300,7 +312,7 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory(
   const typet type, bool top, bool bottom) const
 {
   // TODO (tkiley): Here we should look at some config file
-  if(type.id()==ID_signedbv)
+  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));
@@ -330,7 +342,7 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory(
   const typet type, const constant_exprt e) const
 {
   assert(type==e.type());
-  if(type.id()==ID_signedbv)
+  if(type.id()==ID_signedbv || type.id()==ID_bool || type.id()==ID_c_bool)
   {
     return abstract_object_pointert(
       new constant_abstract_valuet(e));
@@ -558,48 +570,13 @@ void abstract_environmentt::output(
   out << "}\n";
 }
 
-abstract_object_pointert abstract_environmentt::eval_logical(
-  const exprt &e) const
+abstract_object_pointert abstract_environmentt::eval_expression(
+  const exprt &e, const namespacet &ns) const
 {
-  typedef std::function<abstract_object_pointert(const exprt &)> eval_handlert;
-  std::map<irep_idt, eval_handlert> handlers=
-  {
-    {
-      ID_equal, [&](const exprt &expr)
-      {
-        abstract_object_pointert lhs=eval(expr.op0());
-        abstract_object_pointert rhs=eval(expr.op1());
-
-        const exprt &lhs_value=lhs->to_constant();
-        const exprt &rhs_value=rhs->to_constant();
-
-        if(lhs_value.id()==ID_nil || rhs_value.id()==ID_nil)
-        {
-          // One or both of the values is unknown so therefore we can't conclude
-          // whether this is true or false
-          return abstract_object_pointert(
-            new abstract_objectt(expr.type(), true, false));
-        }
-        else
-        {
-          bool logical_result=lhs_value==rhs_value;
-          if(logical_result)
-          {
-            return abstract_object_pointert(
-              new constant_abstract_valuet(true_exprt()));
-          }
-          else
-          {
-            return abstract_object_pointert(
-              new constant_abstract_valuet(false_exprt()));
-          }
-        }
-      }
-    }
-  };
-
-  assert(handlers.find(e.id())!=handlers.end());
-  return handlers[e.id()](e);
+  // Delegate responsibility of resolving to a boolean abstract object
+  // to the abstract object being compared against
+  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

src/analyses/variable-sensitivity/abstract_enviroment.h

@@ -19,9 +19,10 @@ class abstract_environmentt
 {
 public:
   // These three are really the heart of the method
-  virtual abstract_object_pointert eval(const exprt &expr) const;
+  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 assume(const exprt &expr);
+  virtual bool assume(const exprt &expr, const namespacet &ns);
 
   virtual abstract_object_pointert abstract_object_factory(
     const typet type, bool top=true, bool bottom=false) const;
@@ -54,7 +55,8 @@ class abstract_environmentt
   bool is_bottom;
 
  // We may need to break out more of these cases into these
- virtual abstract_object_pointert eval_logical(const exprt &e) const;
+ 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;

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -6,10 +6,17 @@
 
 \*******************************************************************/
 
-#include "abstract_object.h"
 #include <iostream>
+
 #include <util/type.h>
 #include <util/std_expr.h>
+#include <analyses/variable-sensitivity/abstract_enviroment.h>
+#include <analyses/variable-sensitivity/constant_abstract_value.h>
+
+#include <util/simplify_expr.h>
+#include <util/namespace.h>
+
+#include "abstract_object.h"
 
 /*******************************************************************\
 
@@ -143,13 +150,65 @@ abstract_object_pointert abstract_objectt::merge(
   return m;
 }
 
-#if 0
-abstract_object_pointert abstract_objectt::expression_transform_logical(
-  const exprt &expr, abstract_environmentt &environment)
+/*******************************************************************\
+
+Function: abstract_objectt::expression_transform
+
+  Inputs:
+   expr - the expression to evaluate and find the result of it. this will
+          be the symbol referred to be op0()
+
+ Outputs: Returns the abstract_object representing the result of this expression
+          to the maximum precision available.
+
+ Purpose: To try and resolve different expressions with the maximum level
+          of precision available.
+
+\*******************************************************************/
+
+abstract_object_pointert abstract_objectt::expression_transform(
+  const exprt &expr,
+  const abstract_environmentt &environment,
+  const namespacet &ns) const
 {
+  exprt constant_replaced_expr=expr;
+  constant_replaced_expr.operands().clear();
+  for(const exprt &op : expr.operands())
+  {
+    abstract_object_pointert lhs_abstract_object=environment.eval(op, ns);
+    const exprt &lhs_value=lhs_abstract_object->to_constant();
+
+    if(lhs_value.id()==ID_nil)
+    {
+      // One of the values is true so we can't really do anything more with
+      // this expression and should just return top for the result
+      return abstract_object_pointert(
+        new abstract_objectt(expr.type(), true, false));
+    }
+    else
+    {
+      // rebuild the operands list with constant versions of
+      // any symbols
+      constant_replaced_expr.operands().push_back(lhs_value);
+    }
+  }
 
+  exprt simplified=simplify_expr(constant_replaced_expr, ns);
+  if(simplified.is_constant())
+  {
+    constant_exprt constant_expr=to_constant_expr(simplified);
+
+    // TODO(tkiley): This should be going through the abstract_object_factory
+    // but at the moment this produces a two value abstraction for type bool
+    // so for now we force it to be the constant abstraction
+    return abstract_object_pointert(
+      new constant_abstract_valuet(constant_expr));
+  }
+  else
+  {
+    return environment.abstract_object_factory(expr.type(), true, false);
+  }
 }
-#endif
 
 /*******************************************************************\
 

src/analyses/variable-sensitivity/abstract_object.h

@@ -11,6 +11,7 @@
 class typet;
 class constant_exprt;
 class abstract_environmentt;
+class namespacet;
 
 #include <util/expr.h>
 #include <memory>
@@ -82,12 +83,15 @@ class abstract_objectt
     const abstract_object_pointert op, bool &out_any_modifications);
 
   // Interface for transforms
-  //abstract_object_pointert expression_transform_logical(const exprt &expr, abstract_environmentt &environment);
+  abstract_object_pointert expression_transform(
+    const exprt &expr,
+    const abstract_environmentt &environment,
+    const namespacet &ns) const;
 
   virtual exprt to_constant(void) const;
 
   virtual void output(
-    std::ostream &out, const class ai_baset &ai, const class namespacet &ns);
+    std::ostream &out, const class ai_baset &ai, const namespacet &ns);
 
   CLONE
 

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -63,7 +63,7 @@ void variable_sensitivity_domaint::transform(
       const code_assignt &inst = to_code_assign(instruction.code);
 
       // TODO : check return values
-      abstract_object_pointert r = abstract_state.eval(inst.rhs());
+      abstract_object_pointert r = abstract_state.eval(inst.rhs(), ns);
       abstract_state.assign(inst.lhs(), r);
     }
     break;
@@ -86,7 +86,7 @@ void variable_sensitivity_domaint::transform(
     break;
 
   case ASSUME:
-    abstract_state.assume(instruction.guard);
+    abstract_state.assume(instruction.guard, ns);
     break;
 
   case FUNCTION_CALL:
@@ -251,7 +251,7 @@ bool variable_sensitivity_domaint::ai_simplify(
     return false;
   else
   {
-    sharing_ptrt<abstract_objectt> res = abstract_state.eval(condition);
+    sharing_ptrt<abstract_objectt> res = abstract_state.eval(condition, ns);
     exprt c = res->to_constant();
 
     if (c.id() == ID_nil)