full_struct_abstract_objectt::to_predicate

Author: jezhiggins

src/analyses/variable-sensitivity/full_struct_abstract_object.cpp

@@ -307,6 +307,27 @@ abstract_object_pointert full_struct_abstract_objectt::visit_sub_elements(
   }
 }
 
+exprt full_struct_abstract_objectt::to_predicate_internal(
+  const exprt &name) const
+{
+  auto all_predicates = exprt::operandst{};
+
+  for(auto field : map.get_sorted_view())
+  {
+    auto field_name = member_exprt(name, field.first, name.type());
+    auto field_expr = field.second->to_predicate(field_name);
+
+    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_struct_abstract_objectt::statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/full_struct_abstract_object.h

@@ -169,6 +169,8 @@ class full_struct_abstract_objectt : public abstract_aggregate_objectt<
   abstract_object_pointert merge(
     const abstract_object_pointert &other,
     const widen_modet &widen_mode) const override;
+
+  exprt to_predicate_internal(const exprt &name) const override;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_H

unit/Makefile

@@ -30,6 +30,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/variable-sensitivity/interval_abstract_value/widening_merge.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 \
        analyses/variable-sensitivity/last_written_location.cpp \
        analyses/variable-sensitivity/value_expression_evaluation/assume.cpp \
        analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp \

unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp

@@ -53,8 +53,10 @@ full_struct_abstract_objectt::constant_struct_pointert build_struct(
       struct_union_typet::componentt(member.first, integer_typet());
     struct_type.components().push_back(component);
 
-    auto value = from_integer(member.second, integer_typet());
-    val1_op.push_back(value);
+    if(member.second != TOP_MEMBER)
+      val1_op.push_back(from_integer(member.second, integer_typet()));
+    else
+      val1_op.push_back(nil_exprt());
   }
 
   auto val1 = struct_exprt(val1_op, struct_type);

unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.h

@@ -8,7 +8,7 @@
 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_STRUCT_BUILDER_H
 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_STRUCT_BUILDER_H
 
-#include <variable-sensitivity/full_struct_abstract_object.h>
+#include <analyses/variable-sensitivity/full_struct_abstract_object.h>
 
 #include <map>
 
@@ -20,6 +20,7 @@ full_struct_abstract_objectt::constant_struct_pointert build_struct(
   abstract_environmentt &environment,
   const namespacet &ns);
 
+const int TOP_MEMBER = std::numeric_limits<int>::max();
 full_struct_abstract_objectt::constant_struct_pointert build_struct(
   const std::map<std::string, int> &members,
   abstract_environmentt &environment,

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

@@ -0,0 +1,75 @@
+/*******************************************************************\
+
+ Module: Tests for full_struct_abstract_objectt::to_predicate
+
+ Author: Jez Higgins
+
+\*******************************************************************/
+
+#include <analyses/variable-sensitivity/abstract_environment.h>
+#include <analyses/variable-sensitivity/full_struct_abstract_object.h>
+#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
+
+#include <analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.h>
+#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
+#include <testing-utils/use_catch.h>
+
+#include <util/arith_tools.h>
+#include <util/mathematical_types.h>
+
+SCENARIO(
+  "struct to predicate",
+  "[core][analyses][variable-sensitivity][full_struct_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_struct_abstract_object to predicate")
+  {
+    WHEN("it is TOP")
+    {
+      auto obj = build_top_struct();
+      THEN_PREDICATE(obj, "TRUE");
+    }
+    WHEN("it is BOTTOM")
+    {
+      auto obj = build_bottom_struct();
+      THEN_PREDICATE(obj, "FALSE");
+    }
+    WHEN("{ .a = 1 }")
+    {
+      auto obj = build_struct({{"a", 1}}, environment, ns);
+      THEN_PREDICATE(obj, "x.a == 1");
+    }
+    WHEN("{ .a = 1, .b = 2, .c = 3 }")
+    {
+      auto obj = build_struct({{"a", 1}, {"b", 2}, {"c", 3}}, environment, ns);
+      THEN_PREDICATE(obj, "x.a == 1 && x.b == 2 && x.c == 3");
+    }
+    WHEN("{ .a = 1, .b = 2, .c = TOP }")
+    {
+      auto obj =
+        build_struct({{"a", 1}, {"b", 2}, {"c", TOP_MEMBER}}, environment, ns);
+      THEN_PREDICATE(obj, "x.a == 1 && x.b == 2");
+    }
+    WHEN("{ .a = TOP, .b = 2, .c = TOP }")
+    {
+      auto obj = build_struct(
+        {{"a", TOP_MEMBER}, {"b", 2}, {"c", TOP_MEMBER}}, environment, ns);
+      THEN_PREDICATE(obj, "x.b == 2");
+    }
+    WHEN("{ .a = TOP, .b = TOP, .c = TOP }")
+    {
+      auto obj = build_struct(
+        {{"a", TOP_MEMBER}, {"b", TOP_MEMBER}, {"c", TOP_MEMBER}},
+        environment,
+        ns);
+      THEN_PREDICATE(obj, "TRUE");
+    }
+  }
+}