Add object tracking

Author: thomasspriggs

src/solvers/Makefile

@@ -195,6 +195,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2irep.cpp \
       smt2_incremental/construct_value_expr_from_smt.cpp \
       smt2_incremental/convert_expr_to_smt.cpp \
+      smt2_incremental/object_tracking.cpp \
       smt2_incremental/smt_bit_vector_theory.cpp \
       smt2_incremental/smt_commands.cpp \
       smt2_incremental/smt_core_theory.cpp \

src/solvers/smt2_incremental/object_tracking.cpp

@@ -0,0 +1,88 @@
+// Author: Diffblue Ltd.
+
+#include "object_tracking.h"
+
+#include <util/c_types.h>
+#include <util/pointer_offset_size.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/string_constant.h>
+
+exprt find_object_base_expression(const address_of_exprt &address_of)
+{
+  auto current = std::ref(address_of.object());
+  while(
+    !(can_cast_expr<symbol_exprt>(current) ||
+      can_cast_expr<constant_exprt>(current) ||
+      can_cast_expr<string_constantt>(current) ||
+      can_cast_expr<code_labelt>(current)))
+  {
+    if(const auto index = expr_try_dynamic_cast<index_exprt>(current.get()))
+    {
+      // For the case `my_array[bar]` the base expression is `my_array`.
+      current = index->array();
+      continue;
+    }
+    if(const auto member = expr_try_dynamic_cast<member_exprt>(current.get()))
+    {
+      // For the case `my_struct.field_name` the base expression is `my_struct`.
+      current = member->compound();
+      continue;
+    }
+    INVARIANT(
+      false,
+      "Unable to find base object of expression: " +
+        current.get().pretty(1, 0));
+  }
+  return current.get();
+}
+
+static decision_procedure_objectt make_null_object()
+{
+  decision_procedure_objectt null_object;
+  null_object.unique_id = 0;
+  null_object.base_expression = null_pointer_exprt{pointer_type(void_type())};
+  return null_object;
+}
+
+smt_object_mapt initial_smt_object_map()
+{
+  smt_object_mapt object_map;
+  decision_procedure_objectt null_object = make_null_object();
+  exprt base = null_object.base_expression;
+  object_map.emplace(std::move(base), std::move(null_object));
+  return object_map;
+}
+
+void track_expression_objects(
+  const exprt &expression,
+  const namespacet &ns,
+  smt_object_mapt &object_map)
+{
+  find_object_base_expressions(
+    expression, [&](const exprt &object_base) -> void {
+      const auto find_result = object_map.find(object_base);
+      if(find_result != object_map.cend())
+        return;
+      decision_procedure_objectt object;
+      object.base_expression = object_base;
+      object.unique_id = object_map.size();
+      object.size = size_of_expr(object_base.type(), ns);
+      object_map.emplace_hint(find_result, object_base, std::move(object));
+    });
+}
+
+bool objects_are_already_tracked(
+  const exprt &expression,
+  const smt_object_mapt &object_map)
+{
+  bool all_objects_tracked = true;
+  find_object_base_expressions(
+    expression, [&](const exprt &object_base) -> void {
+      const auto find_result = object_map.find(object_base);
+      if(find_result != object_map.cend())
+        return;
+      all_objects_tracked = false;
+    });
+  return all_objects_tracked;
+}

src/solvers/smt2_incremental/object_tracking.h

@@ -0,0 +1,90 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H
+
+#include <util/expr.h>
+#include <util/pointer_expr.h>
+
+#include <unordered_map>
+
+/// Information the decision procedure holds about each object.
+struct decision_procedure_objectt
+{
+  /// The expression for the root of the object. This is expression equivalent
+  /// to deferencing a pointer to this object with a zero offset.
+  exprt base_expression;
+  /// Number which uniquely identifies this particular object.
+  std::size_t unique_id;
+  /// Expression which evaluates to the size of the object in bytes.
+  optionalt<exprt> size;
+};
+
+/// The model of addresses we use consists of a unique object identifier and an
+/// offset. In order to encode the offset identifiers we need to assign unique
+/// identifiers to the objects. This function finds the base object expression
+/// in an address of expression for which a unique identifier needs to be
+/// assigned.
+exprt find_object_base_expression(const address_of_exprt &address_of);
+
+/// Arbitary expressions passed to the decision procedure may have multiple
+/// address of operations as its sub expressions. This means the overall
+/// expression may contain multiple base objects which need to be assigned
+/// unique identifiers.
+/// \param expression
+///   The expression within which to find base objects.
+/// \param output_object
+///   This function is called with each of the base object expressions found, as
+///   they are found.
+/// \details
+///   The found objects are returned through an output function in order to
+///   separate the implementation of the storage and deduplication of the
+///   results from finding the object expressions. The type of \p output_object
+///   is a template parameter in order to eliminate potential performance
+///   overheads of using `std::function`.
+template <typename output_object_functiont>
+void find_object_base_expressions(
+  const exprt &expression,
+  const output_object_functiont &output_object)
+{
+  expression.visit_pre([&](const exprt &node) {
+    if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(node))
+    {
+      output_object(find_object_base_expression(*address_of));
+    }
+  });
+}
+
+/// Mapping from an object's base expression to the set of information about it
+/// which we track.
+using smt_object_mapt =
+  std::unordered_map<exprt, decision_procedure_objectt, irep_hash>;
+
+/// Constructs an initial object map containing the null object. The null object
+/// must be added at construction in order to ensure it is allocated a unique
+/// identifier of 0.
+smt_object_mapt initial_smt_object_map();
+
+/// \brief
+///   Finds all the object expressions in the given expression and adds them to
+///   the object map for cases where the map does not contain them already.
+/// \param expression
+///   The expression within which to find and base object expressions.
+/// \param ns
+///   The namespace used to look up the size of object types.
+/// \param object_map
+///   The map into which any new tracking information should be inserted.
+void track_expression_objects(
+  const exprt &expression,
+  const namespacet &ns,
+  smt_object_mapt &object_map);
+
+/// Finds whether all base object expressions in the given expression are
+/// already tracked in the given object map. This supports writing invariants
+/// on the base object expressions already being tracked in the map in contexts
+/// where the map is const.
+bool objects_are_already_tracked(
+  const exprt &expression,
+  const smt_object_mapt &object_map);
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H

unit/Makefile

@@ -102,6 +102,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2/smt2irep.cpp \
        solvers/smt2_incremental/construct_value_expr_from_smt.cpp \
        solvers/smt2_incremental/convert_expr_to_smt.cpp \
+       solvers/smt2_incremental/object_tracking.cpp \
        solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp \
        solvers/smt2_incremental/smt_bit_vector_theory.cpp \
        solvers/smt2_incremental/smt_commands.cpp \

unit/solvers/smt2_incremental/object_tracking.cpp

@@ -0,0 +1,101 @@
+// Author: Diffblue Ltd.
+
+#include <util/c_types.h>
+#include <util/namespace.h>
+#include <util/optional.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+#include <solvers/smt2_incremental/object_tracking.h>
+#include <testing-utils/use_catch.h>
+
+#include <string>
+#include <utility>
+
+TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
+{
+  const typet base_type = pointer_typet{unsignedbv_typet{8}, 18};
+  const symbol_exprt object_base{"base", base_type};
+  const symbol_exprt index{"index", base_type};
+  const pointer_typet pointer_type{base_type, 12};
+  std::string description;
+  optionalt<address_of_exprt> address_of;
+  using rowt = std::pair<std::string, address_of_exprt>;
+  std::tie(description, address_of) = GENERATE_REF(
+    rowt{"Address of symbol", {object_base, pointer_type}},
+    rowt{"Address of index", {index_exprt{object_base, index}, pointer_type}},
+    rowt{
+      "Address of struct member",
+      {member_exprt{object_base, "baz", unsignedbv_typet{8}}, pointer_type}},
+    rowt{
+      "Address of index of struct member",
+      {index_exprt{
+         member_exprt{object_base, "baz", unsignedbv_typet{8}}, index},
+       pointer_type}},
+    rowt{
+      "Address of struct member at index",
+      {member_exprt{
+         index_exprt{object_base, index}, "baz", unsignedbv_typet{8}},
+       pointer_type}});
+  SECTION(description)
+  {
+    CHECK(find_object_base_expression(*address_of) == object_base);
+  }
+}
+
+TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]")
+{
+  const typet base_type = pointer_typet{signedbv_typet{16}, 18};
+  const symbol_exprt foo{"foo", base_type};
+  const symbol_exprt bar{"bar", base_type};
+  const symbol_exprt index{"index", base_type};
+  const pointer_typet pointer_type{base_type, 32};
+  const exprt bar_address = address_of_exprt{bar, pointer_type};
+  const exprt compound_expression = and_exprt{
+    equal_exprt{
+      address_of_exprt{index_exprt{foo, index}, pointer_type}, bar_address},
+    notequal_exprt{
+      address_of_exprt{
+        member_exprt{foo, "baz", unsignedbv_typet{8}}, pointer_type},
+      bar_address}};
+  SECTION("Find base expressions")
+  {
+    std::vector<exprt> expressions;
+    find_object_base_expressions(compound_expression, [&](const exprt &expr) {
+      expressions.push_back(expr);
+    });
+    CHECK(expressions == std::vector<exprt>{bar, foo, bar, foo});
+  }
+  smt_object_mapt object_map = initial_smt_object_map();
+  SECTION("Check initial object map has null pointer")
+  {
+    REQUIRE(object_map.size() == 1);
+    const exprt null_pointer = null_pointer_exprt{::pointer_type(void_type())};
+    CHECK(object_map.begin()->first == null_pointer);
+    CHECK(object_map.begin()->second.unique_id == 0);
+    CHECK(object_map.begin()->second.base_expression == null_pointer);
+  }
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  SECTION("Check objects of compound expression not yet tracked")
+  {
+    CHECK_FALSE(objects_are_already_tracked(compound_expression, object_map));
+  }
+  track_expression_objects(compound_expression, ns, object_map);
+  SECTION("Tracking expression objects")
+  {
+    CHECK(object_map.size() == 3);
+    const auto foo_object = object_map.find(foo);
+    REQUIRE(foo_object != object_map.end());
+    CHECK(foo_object->second.base_expression == foo);
+    CHECK(foo_object->second.unique_id == 2);
+    const auto bar_object = object_map.find(bar);
+    REQUIRE(bar_object != object_map.end());
+    CHECK(bar_object->second.base_expression == bar);
+    CHECK(bar_object->second.unique_id == 1);
+  }
+  SECTION("Confirming objects are tracked.")
+  {
+    CHECK(objects_are_already_tracked(compound_expression, object_map));
+  }
+}