Merge pull request #5644 from jezhiggins/abstract_environmentt-eval

abstract_environmentt::eval rework

Author: martin-cs

regression/goto-analyzer/simple-union-access/test.desc

@@ -0,0 +1,15 @@
+CORE
+union.c
+--variable-sensitivity --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line 13 x.a==0: UNKNOWN$
+^\[main.assertion.2\] line 14 x.a==1: UNKNOWN$
+^\[main.assertion.3\] line 15 x.b==0: UNKNOWN$
+^\[main.assertion.4\] line 16 x.b==1: UNKNOWN$
+^\[main.assertion.5\] line 19 x.a==0: UNKNOWN$
+^\[main.assertion.6\] line 20 x.a==1: UNKNOWN$
+^\[main.assertion.7\] line 21 x.b==0: UNKNOWN$
+^\[main.assertion.8\] line 22 x.b==1: UNKNOWN$
+--
+^warning: ignoring

regression/goto-analyzer/simple-union-access/union.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  // Test if we can represent constant structs
+  union union_struct {
+    int a;
+    int b;
+  };
+
+  union union_struct x = {0};
+  x.a = 0;
+  __CPROVER_assert(x.a == 0, "x.a==0");
+  __CPROVER_assert(x.a == 1, "x.a==1");
+  __CPROVER_assert(x.b == 0, "x.b==0");
+  __CPROVER_assert(x.b == 1, "x.b==1");
+
+  x.b = 1;
+  __CPROVER_assert(x.a == 0, "x.a==0");
+  __CPROVER_assert(x.a == 1, "x.a==1");
+  __CPROVER_assert(x.b == 0, "x.b==0");
+  __CPROVER_assert(x.b == 1, "x.b==1");
+
+  return 0;
+}

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -27,6 +27,11 @@
 #  include <iostream>
 #endif
 
+std::vector<abstract_object_pointert> eval_operands(
+  const exprt &expr,
+  const abstract_environmentt &env,
+  const namespacet &ns);
+
 abstract_object_pointert
 abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
 {
@@ -51,14 +56,15 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
       return found_symbol_value;
     }
   }
-  else if(simplified_id == ID_member)
+  else if(
+    simplified_id == ID_member || simplified_id == ID_index ||
+    simplified_id == ID_dereference)
   {
-    member_exprt member_expr(to_member_expr(simplified_expr));
+    auto access_expr = simplified_expr;
+    auto target = eval(access_expr.operands()[0], ns);
 
-    const exprt &parent = member_expr.compound();
-
-    abstract_object_pointert parent_abstract_object = eval(parent, ns);
-    return parent_abstract_object->read(*this, member_expr, ns);
+    return target->expression_transform(
+      access_expr, eval_operands(access_expr, *this, ns), *this, ns);
   }
   else if(simplified_id == ID_address_of)
   {
@@ -68,35 +74,12 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
     // Store the abstract object in the pointer
     return pointer_object;
   }
-  else if(simplified_id == ID_dereference)
-  {
-    dereference_exprt dereference(to_dereference_expr(simplified_expr));
-    abstract_object_pointert pointer_abstract_object =
-      eval(dereference.pointer(), ns);
-
-    return pointer_abstract_object->read(*this, nil_exprt(), ns);
-  }
-  else if(simplified_id == ID_index)
-  {
-    index_exprt index_expr(to_index_expr(simplified_expr));
-    abstract_object_pointert array_abstract_object =
-      eval(index_expr.array(), ns);
-
-    return array_abstract_object->read(*this, index_expr, ns);
-  }
-  else if(simplified_id == ID_array)
+  else if(
+    simplified_id == ID_array || simplified_id == ID_struct ||
+    simplified_id == ID_constant)
   {
     return abstract_object_factory(simplified_expr.type(), simplified_expr, ns);
   }
-  else if(simplified_id == ID_struct)
-  {
-    return abstract_object_factory(simplified_expr.type(), simplified_expr, ns);
-  }
-  else if(simplified_id == ID_constant)
-  {
-    return abstract_object_factory(
-      simplified_expr.type(), to_constant_expr(simplified_expr), ns);
-  }
   else
   {
     // No special handling required by the abstract environment
@@ -448,14 +431,8 @@ abstract_object_pointert abstract_environmentt::eval_expression(
   abstract_object_pointert eval_obj =
     abstract_object_factory(e.type(), ns, true);
 
-  std::vector<abstract_object_pointert> operands;
-
-  for(const auto &op : e.operands())
-  {
-    operands.push_back(eval(op, ns));
-  }
-
-  return eval_obj->expression_transform(e, operands, *this, ns);
+  return eval_obj->expression_transform(
+    e, eval_operands(e, *this, ns), *this, ns);
 }
 
 void abstract_environmentt::erase(const symbol_exprt &expr)
@@ -527,3 +504,16 @@ abstract_environmentt::gather_statistics(const namespacet &ns) const
   }
   return statistics;
 }
+
+std::vector<abstract_object_pointert> eval_operands(
+  const exprt &expr,
+  const abstract_environmentt &env,
+  const namespacet &ns)
+{
+  std::vector<abstract_object_pointert> operands;
+
+  for(const auto &op : expr.operands())
+    operands.push_back(env.eval(op, ns));
+
+  return operands;
+}

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -136,14 +136,6 @@ abstract_object_pointert abstract_objectt::expression_transform(
   return environment.abstract_object_factory(copy.type(), copy, ns);
 }
 
-abstract_object_pointert abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
-  const namespacet &ns) const
-{
-  return shared_from_this();
-}
-
 abstract_object_pointert abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/abstract_object.h

@@ -177,23 +177,6 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   /// that allows an object to be built from a value.
   virtual exprt to_constant() const;
 
-  /**
-   * A helper function to evaluate an abstract object contained
-   * within a container object. More precise abstractions may override this
-   * to return more precise results.
-   *
-   * \param env the abstract environment
-   * \param specifier a modifier expression, such as an array index or field
-   * specifier used to indicate access to a specific component
-   * \param ns the current namespace
-   *
-   * \return the abstract_objectt representing the value of the read component.
-   */
-  virtual abstract_object_pointert read(
-    const abstract_environmentt &env,
-    const exprt &specifier,
-    const namespacet &ns) const;
-
   /**
    * A helper function to evaluate writing to a component of an
    * abstract object. More precise abstractions may override this to

src/analyses/variable-sensitivity/array_abstract_object.cpp

@@ -35,12 +35,19 @@ array_abstract_objectt::array_abstract_objectt(
   PRECONDITION(e.type().id() == ID_array);
 }
 
-abstract_object_pointert array_abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
+abstract_object_pointert array_abstract_objectt::expression_transform(
+  const exprt &expr,
+  const std::vector<abstract_object_pointert> &operands,
+  const abstract_environmentt &environment,
   const namespacet &ns) const
 {
-  return this->read_index(env, to_index_expr(specifier), ns);
+  if(expr.id() == ID_index)
+  {
+    return read_index(environment, to_index_expr(expr), ns);
+  }
+
+  return abstract_objectt::expression_transform(
+    expr, operands, environment, ns);
 }
 
 abstract_object_pointert array_abstract_objectt::write(

src/analyses/variable-sensitivity/array_abstract_object.h

@@ -42,21 +42,25 @@ class array_abstract_objectt : public abstract_objectt
     const abstract_environmentt &environment,
     const namespacet &ns);
 
-  /**
-   * A helper function to evaluate an abstract object contained
-   * within a container object. More precise abstractions may override this
-   * to return more precise results.
-   *
-   * \param env the abstract environment
-   * \param specifier a modifier expression, such as an array index or field
-   * specifier used to indicate access to a specific component
-   * \param ns the current namespace
-   *
-   * \return the abstract_objectt representing the value of the read component.
-   */
-  abstract_object_pointert read(
-    const abstract_environmentt &env,
-    const exprt &specifier,
+  /// Interface for transforms
+  ///
+  /// \param expr: the expression to evaluate and find the result of it.
+  ///              This will be the symbol referred to be op0()
+  /// \param operands: an abstract_object (pointer) that represent
+  ///                  the possible values of each operand
+  /// \param environment: the abstract environment in which the
+  ///                     expression is being evaluated
+  /// \param ns: the current variable namespace
+  ///
+  /// \return Returns the abstract_object representing the result of
+  ///         this expression to the maximum precision available.
+  ///
+  /// To try and resolve different expressions with the maximum level
+  /// of precision available.
+  abstract_object_pointert expression_transform(
+    const exprt &expr,
+    const std::vector<abstract_object_pointert> &operands,
+    const abstract_environmentt &environment,
     const namespacet &ns) const override;
 
   /**

src/analyses/variable-sensitivity/context_abstract_object.cpp

@@ -30,28 +30,6 @@ void context_abstract_objectt::set_not_top_internal()
     set_child(child_abstract_object->clear_top());
 }
 
-/**
- * A helper function to evaluate an abstract object contained
- * within a container object. More precise abstractions may override this
- * to return more precise results.
- *
- * \param env the abstract environment
- * \param specifier a modifier expression, such as an array index or field
- * specifier used to indicate access to a specific component
- * \param ns the current namespace
- *
- * \return the abstract_objectt representing the value of the read component.
- * For the dependency context, the operation is simply delegated to the
- * child object
- */
-abstract_object_pointert context_abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
-  const namespacet &ns) const
-{
-  return child_abstract_object->read(env, specifier, ns);
-}
-
 /**
  * A helper function to evaluate writing to a component of an
  * abstract object. More precise abstractions may override this to

src/analyses/variable-sensitivity/context_abstract_object.h

@@ -107,11 +107,6 @@ class context_abstract_objectt : public abstract_objectt
   void set_top_internal() override;
   void set_not_top_internal() override;
 
-  abstract_object_pointert read(
-    const abstract_environmentt &env,
-    const exprt &specifier,
-    const namespacet &ns) const override;
-
   abstract_object_pointert write(
     abstract_environmentt &environment,
     const namespacet &ns,

src/analyses/variable-sensitivity/pointer_abstract_object.cpp

@@ -36,12 +36,19 @@ pointer_abstract_objectt::pointer_abstract_objectt(
   PRECONDITION(e.type().id() == ID_pointer);
 }
 
-abstract_object_pointert pointer_abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
+abstract_object_pointert pointer_abstract_objectt::expression_transform(
+  const exprt &expr,
+  const std::vector<abstract_object_pointert> &operands,
+  const abstract_environmentt &environment,
   const namespacet &ns) const
 {
-  return read_dereference(env, ns);
+  if(expr.id() == ID_dereference)
+  {
+    return read_dereference(environment, ns);
+  }
+
+  return abstract_objectt::expression_transform(
+    expr, operands, environment, ns);
 }
 
 abstract_object_pointert pointer_abstract_objectt::write(