Dereferencing a value-set of pointers

Remove expression_transform and write from value-set of pointers.
Dereference value-set of pointers to a single value

Author: jezhiggins

regression/goto-analyzer/pointer-dereference/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  int a = 10;
+  int *p = &a;
+
+  int q = *p;
+
+  assert(q == a);
+}

regression/goto-analyzer/pointer-dereference/test-constants.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-pointers constants
+^\[main.assertion.1\] line 10 assertion q == a: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-dereference/test-top-bottom.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-pointers top-bottom
+^\[main.assertion.1\] line 10 assertion q == a: UNKNOWN
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-dereference/test-value-sets.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-pointers value-set
+^\[main.assertion.1\] line 10 assertion q == a: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

src/analyses/variable-sensitivity/abstract_pointer_object.h

@@ -62,7 +62,6 @@ class abstract_pointer_objectt : public abstract_objectt,
     const abstract_environmentt &env,
     const namespacet &ns) const override;
 
-protected:
   /// Evaluate reading the pointer's value. More precise
   /// abstractions may override this to provide more precise results.
   ///
@@ -74,6 +73,7 @@ class abstract_pointer_objectt : public abstract_objectt,
     const abstract_environmentt &env,
     const namespacet &ns) const;
 
+protected:
   /// Evaluate writing to a pointer's value. More precise abstractions
   /// may override this provide more precise results.
   ///

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -14,13 +14,6 @@
 #include <analyses/variable-sensitivity/context_abstract_object.h>
 #include <analyses/variable-sensitivity/value_set_pointer_abstract_object.h>
 
-static exprt rewrite_expression(
-  const exprt &expr,
-  const std::vector<abstract_object_pointert> &ops);
-
-static std::vector<abstract_object_sett>
-unwrap_operands(const std::vector<abstract_object_pointert> &operands);
-
 static abstract_object_sett
 unwrap_and_extract_values(const abstract_object_sett &values);
 
@@ -101,81 +94,25 @@ value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt(
     std::make_shared<constant_pointer_abstract_objectt>(expr, environment, ns));
 }
 
-abstract_object_pointert
-value_set_pointer_abstract_objectt::expression_transform(
-  const exprt &expr,
-  const std::vector<abstract_object_pointert> &operands,
-  const abstract_environmentt &environment,
-  const namespacet &ns) const
-{
-  PRECONDITION(operands.size() == expr.operands().size());
-
-  auto collective_operands = unwrap_operands(operands);
-
-  if(expr.id() == ID_if)
-    return evaluate_conditional(
-      expr.type(), collective_operands, environment, ns);
-
-  abstract_object_sett resulting_objects;
-
-  auto dispatcher = values.first();
-  for_each_comb(
-    collective_operands,
-    [&resulting_objects, &dispatcher, &expr, &environment, &ns](
-      const std::vector<abstract_object_pointert> &ops) {
-      auto rewritten_expr = rewrite_expression(expr, ops);
-      resulting_objects.insert(
-        dispatcher->expression_transform(rewritten_expr, ops, environment, ns));
-    });
-
-  return resolve_new_values(resulting_objects, environment);
-}
-
-abstract_object_pointert
-value_set_pointer_abstract_objectt::evaluate_conditional(
-  const typet &type,
-  const std::vector<abstract_object_sett> &operands,
+abstract_object_pointert value_set_pointer_abstract_objectt::read_dereference(
   const abstract_environmentt &env,
   const namespacet &ns) const
 {
-  auto const condition = operands[0];
-
-  auto const true_result = operands[1];
-  auto const false_result = operands[2];
-
-  auto all_true = true;
-  auto all_false = true;
-  for(auto v : condition)
+  if(is_top() || is_bottom())
   {
-    auto expr = v->to_constant();
-    all_true = all_true && expr.is_true();
-    all_false = all_false && expr.is_false();
+    return env.abstract_object_factory(
+      type().subtype(), ns, is_top(), !is_top());
   }
-  auto indeterminate = !all_true && !all_false;
-
-  abstract_object_sett resulting_objects;
-  if(all_true || indeterminate)
-    resulting_objects.insert(true_result);
-  if(all_false || indeterminate)
-    resulting_objects.insert(false_result);
-  return resolve_new_values(resulting_objects, env);
-}
 
-abstract_object_pointert value_set_pointer_abstract_objectt::write(
-  abstract_environmentt &environment,
-  const namespacet &ns,
-  const std::stack<exprt> &stack,
-  const exprt &specifier,
-  const abstract_object_pointert &value,
-  bool merging_write) const
-{
-  abstract_object_sett new_values;
-  for(const auto &st_value : values)
+  abstract_object_sett results;
+  for(auto value : values)
   {
-    new_values.insert(
-      st_value->write(environment, ns, stack, specifier, value, merging_write));
+    auto pointer =
+      std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
+    results.insert(pointer->read_dereference(env, ns));
   }
-  return resolve_new_values(new_values, environment);
+
+  return results.first();
 }
 
 abstract_object_pointert value_set_pointer_abstract_objectt::resolve_new_values(
@@ -255,33 +192,6 @@ void value_set_pointer_abstract_objectt::output(
   }
 }
 
-exprt rewrite_expression(
-  const exprt &expr,
-  const std::vector<abstract_object_pointert> &ops)
-{
-  auto operands_expr = exprt::operandst{};
-  for(auto v : ops)
-    operands_expr.push_back(v->to_constant());
-  auto rewritten_expr = exprt(expr.id(), expr.type(), std::move(operands_expr));
-  return rewritten_expr;
-}
-
-std::vector<abstract_object_sett>
-unwrap_operands(const std::vector<abstract_object_pointert> &operands)
-{
-  auto unwrapped = std::vector<abstract_object_sett>{};
-
-  for(const auto &op : operands)
-  {
-    auto vsab =
-      std::dynamic_pointer_cast<const value_set_tag>(maybe_unwrap_context(op));
-    INVARIANT(vsab, "should be a value set abstract object");
-    unwrapped.push_back(vsab->get_values());
-  }
-
-  return unwrapped;
-}
-
 abstract_object_sett
 unwrap_and_extract_values(const abstract_object_sett &values)
 {

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

@@ -38,19 +38,9 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
                               : abstract_objectt::to_constant();
   }
 
-  /// \copydoc abstract_objectt::expression_transform
-  ///
-  /// Transforms the \p expr for every combination of \p operands (since these
-  /// can be value-sets as well).
-  abstract_object_pointert expression_transform(
-    const exprt &expr,
-    const std::vector<abstract_object_pointert> &operands,
-    const abstract_environmentt &environment,
-    const namespacet &ns) const override;
-
   /// Getter for the set of stored abstract objects.
   /// \return the values represented by this abstract object
-  const abstract_object_sett &get_values() const
+  const abstract_object_sett &get_values() const override
   {
     return values;
   }
@@ -63,16 +53,9 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
   /// either converted to interval or marked as `top`.
   static const size_t max_value_set_size = 10;
 
-  /// \copydoc abstract_objectt::write
-  ///
-  /// Delegate writing to stored values.
-  abstract_object_pointert write(
-    abstract_environmentt &environment,
-    const namespacet &ns,
-    const std::stack<exprt> &stack,
-    const exprt &specifier,
-    const abstract_object_pointert &value,
-    bool merging_write) const override;
+  abstract_object_pointert read_dereference(
+    const abstract_environmentt &env,
+    const namespacet &ns) const override;
 
   void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
     const override;
@@ -84,12 +67,6 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
   abstract_object_pointert merge(abstract_object_pointert other) const override;
 
 private:
-  abstract_object_pointert evaluate_conditional(
-    const typet &type,
-    const std::vector<abstract_object_sett> &operands,
-    const abstract_environmentt &env,
-    const namespacet &ns) const;
-
   /// Update the set of stored values to \p new_values. Build a new abstract
   ///   object of the right type if necessary.
   /// \param new_values: potentially new set of values