full_array_abstract_objectt::to_predicate

Author: jezhiggins

src/analyses/variable-sensitivity/full_array_abstract_object.cpp

@@ -10,6 +10,7 @@
 
 #include <analyses/variable-sensitivity/abstract_environment.h>
 #include <util/arith_tools.h>
+#include <util/mathematical_types.h>
 #include <util/std_expr.h>
 
 #include "abstract_value_object.h"
@@ -401,6 +402,28 @@ abstract_object_pointert full_array_abstract_objectt::visit_sub_elements(
   }
 }
 
+exprt full_array_abstract_objectt::to_predicate_internal(
+  const exprt &name) const
+{
+  auto all_predicates = exprt::operandst{};
+
+  for(auto field : map.get_sorted_view())
+  {
+    auto ii = from_integer(field.first.to_long(), integer_typet());
+    auto index = index_exprt(name, ii);
+    auto field_expr = field.second->to_predicate(index);
+
+    if(!field_expr.is_true())
+      all_predicates.push_back(field_expr);
+  }
+
+  if(all_predicates.size() == 0)
+    return true_exprt();
+  if(all_predicates.size() == 1)
+    return all_predicates[0];
+  return and_exprt(all_predicates);
+}
+
 void full_array_abstract_objectt::statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/full_array_abstract_object.h

@@ -212,6 +212,8 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt<
   abstract_object_pointert full_array_merge(
     const full_array_pointert &other,
     const widen_modet &widen_mode) const;
+
+  exprt to_predicate_internal(const exprt &name) const override;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H

unit/Makefile

@@ -20,6 +20,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/variable-sensitivity/constant_abstract_value/meet.cpp \
        analyses/variable-sensitivity/constant_abstract_value/merge.cpp \
        analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp \
+       analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp \
        analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \
        analyses/variable-sensitivity/eval.cpp \
        analyses/variable-sensitivity/eval-member-access.cpp \
@@ -28,7 +29,6 @@ SRC += analyses/ai/ai.cpp \
        analyses/variable-sensitivity/interval_abstract_value/merge.cpp \
        analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp \
        analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \
-       analyses/variable-sensitivity/full_struct_abstract_object/array_builder.cpp \
        analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \
        analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp \
        analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp \

unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp

@@ -9,7 +9,7 @@
 #include <analyses/variable-sensitivity/abstract_environment.h>
 #include <analyses/variable-sensitivity/full_array_abstract_object.h>
 #include <analyses/variable-sensitivity/full_array_abstract_object/array_builder.h>
-#include <arith_tools.h>
+#include <util/arith_tools.h>
 #include <util/mathematical_types.h>
 
 full_array_abstract_objectt::full_array_pointert build_array(
@@ -32,7 +32,12 @@ full_array_abstract_objectt::full_array_pointert build_array(
   exprt::operandst element_ops;
 
   for(auto element : array)
-    element_ops.push_back(from_integer(element, integer_typet()));
+  {
+    if(element != TOP_MEMBER)
+      element_ops.push_back(from_integer(element, integer_typet()));
+    else
+      element_ops.push_back(nil_exprt());
+  }
 
   auto array_expr = array_exprt(element_ops, array_type);
   return build_array(array_expr, environment, ns);

unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h

@@ -15,6 +15,7 @@ full_array_abstract_objectt::full_array_pointert build_array(
   abstract_environmentt &environment,
   const namespacet &ns);
 
+const int TOP_MEMBER = std::numeric_limits<int>::max();
 full_array_abstract_objectt::full_array_pointert build_array(
   const std::vector<int> &array,
   abstract_environmentt &environment,

unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp

@@ -11,7 +11,6 @@
 
 #include <analyses/variable-sensitivity/abstract_environment.h>
 #include <analyses/variable-sensitivity/abstract_object.h>
-#include <analyses/variable-sensitivity/full_array_abstract_object.h>
 #include <analyses/variable-sensitivity/full_array_abstract_object/array_builder.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>

unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp

@@ -0,0 +1,67 @@
+/*******************************************************************\
+
+ Module: Tests for full_array_abstract_objectt::to_predicate
+
+ Author: Jez Higgins
+
+\*******************************************************************/
+
+#include <analyses/variable-sensitivity/abstract_environment.h>
+#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
+
+#include <analyses/variable-sensitivity/full_array_abstract_object/array_builder.h>
+#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
+#include <testing-utils/use_catch.h>
+
+SCENARIO(
+  "array to predicate",
+  "[core][analyses][variable-sensitivity][full_array_abstract_object][to_"
+  "predicate]")
+{
+  auto object_factory = variable_sensitivity_object_factoryt::configured_with(
+    vsd_configt::constant_domain());
+  abstract_environmentt environment(object_factory);
+  environment.make_top();
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  GIVEN("full_array_abstract_object to predicate")
+  {
+    WHEN("it is TOP")
+    {
+      auto obj = build_top_array();
+      THEN_PREDICATE(obj, "TRUE");
+    }
+    WHEN("it is BOTTOM")
+    {
+      auto obj = build_bottom_array();
+      THEN_PREDICATE(obj, "FALSE");
+    }
+    WHEN("[ 1 ]")
+    {
+      auto obj = build_array({1}, environment, ns);
+      THEN_PREDICATE(obj, "x[0] == 1");
+    }
+    WHEN("[ 1, 2, 3 ]")
+    {
+      auto obj = build_array({1, 2, 3}, environment, ns);
+      THEN_PREDICATE(obj, "x[0] == 1 && x[1] == 2 && x[2] == 3");
+    }
+    WHEN("[ 1, 2, TOP ]")
+    {
+      auto obj = build_array({1, 2, TOP_MEMBER}, environment, ns);
+      THEN_PREDICATE(obj, "x[0] == 1 && x[1] == 2");
+    }
+    WHEN("[ TOP, 2, TOP ]")
+    {
+      auto obj = build_array({TOP_MEMBER, 2, TOP_MEMBER}, environment, ns);
+      THEN_PREDICATE(obj, "x[1] == 2");
+    }
+    WHEN("[ TOP, TOP, TOP ]")
+    {
+      auto obj =
+        build_array({TOP_MEMBER, TOP_MEMBER, TOP_MEMBER}, environment, ns);
+      THEN_PREDICATE(obj, "TRUE");
+    }
+  }
+}