Add smt_is_dynamic_objectt function

The SMT function which this commit implements declaration / application
/ definition will be used in follow up commits in order to convert
dynamic_object expressions to smt terms.

Author: thomasspriggs

src/solvers/Makefile

@@ -204,6 +204,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/convert_expr_to_smt.cpp \
       smt2_incremental/object_tracking.cpp \
       smt2_incremental/type_size_mapping.cpp \
+      smt2_incremental/smt_is_dynamic_object.cpp \
       smt2_incremental/smt_object_size.cpp \
       smt2_incremental/smt_response_validation.cpp \
       smt2_incremental/smt_solver_process.cpp \

src/solvers/smt2_incremental/smt_is_dynamic_object.cpp

@@ -0,0 +1,36 @@
+// Author: Diffblue Ltd.
+
+#include "smt_is_dynamic_object.h"
+
+#include <util/c_types.h>
+#include <util/config.h>
+
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
+
+static smt_declare_function_commandt
+make_is_dynamic_object_function_declaration()
+{
+  return smt_declare_function_commandt{
+    smt_identifier_termt{"is_dynamic_object", smt_bool_sortt{}},
+    {smt_bit_vector_sortt{config.bv_encoding.object_bits}}};
+}
+
+smt_is_dynamic_objectt::smt_is_dynamic_objectt()
+  : declaration{make_is_dynamic_object_function_declaration()},
+    make_application{smt_command_functiont{declaration}}
+{
+}
+
+smt_commandt smt_is_dynamic_objectt::make_definition(
+  std::size_t unique_id,
+  bool is_dynamic_object) const
+{
+  const auto id_sort =
+    declaration.parameter_sorts().at(0).get().cast<smt_bit_vector_sortt>();
+  INVARIANT(id_sort, "Object identifiers are expected to have bit vector sort");
+  const auto bit_vector_of_id =
+    smt_bit_vector_constant_termt{unique_id, *id_sort};
+  return smt_assert_commandt{smt_core_theoryt::equal(
+    make_application(std::vector<smt_termt>{bit_vector_of_id}),
+    smt_bool_literal_termt{is_dynamic_object})};
+}

src/solvers/smt2_incremental/smt_is_dynamic_object.h

@@ -0,0 +1,31 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H
+
+#include <solvers/smt2_incremental/ast/smt_commands.h>
+#include <solvers/smt2_incremental/ast/smt_terms.h>
+
+/// Specifics of how the dynamic object status lookup is implemented in SMT
+/// terms. This uses an uninterpreted function as a lookup. Because these
+/// functions must return the same result for a specific input, we can just
+/// assert the value of the function output for the inputs where we want to
+/// define specific ID input / dynamic_object output pairs.
+struct smt_is_dynamic_objectt final
+{
+  smt_is_dynamic_objectt();
+  /// The command for declaring the is_dynamic_object function. The defined
+  /// function takes a bit vector encoded unique object identifier and returns
+  /// a boolean value.
+  smt_declare_function_commandt declaration;
+  /// Function which makes applications of the smt function.
+  using make_applicationt =
+    smt_function_application_termt::factoryt<smt_command_functiont>;
+  make_applicationt make_application;
+  /// Makes the command to define the resulting \p is_dynamic_object status for
+  /// calls to the `is_dynamic_object` function with \p unique_id.
+  smt_commandt
+  make_definition(std::size_t unique_id, bool is_dynamic_object) const;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H

unit/Makefile

@@ -110,6 +110,7 @@ SRC += analyses/ai/ai.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_is_dynamic_object.cpp \
        solvers/smt2_incremental/smt_object_size.cpp \
        solvers/smt2_incremental/smt_response_validation.cpp \
        solvers/smt2_incremental/smt_to_smt2_string.cpp \

unit/solvers/smt2_incremental/smt_is_dynamic_object.cpp

@@ -0,0 +1,53 @@
+// Author: Diffblue Ltd.
+
+#include <util/c_types.h>
+#include <util/config.h>
+
+#include <solvers/smt2_incremental/smt_is_dynamic_object.h>
+#include <solvers/smt2_incremental/theories/smt_core_theory.h>
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("Test smt_is_dynamic_objectt", "[core][smt2_incremental]")
+{
+  const std::size_t object_bits = GENERATE(8, 16);
+  INFO("Using " + std::to_string(object_bits) + " object id bits.");
+  // Configuration needs to be set because smt_is_dynamic_objectt uses it.
+  config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
+  config.ansi_c.set_arch_spec_x86_64();
+  config.bv_encoding.object_bits = object_bits;
+  const smt_is_dynamic_objectt is_dynamic_object;
+  SECTION("Declare function")
+  {
+    CHECK(
+      is_dynamic_object.declaration ==
+      smt_declare_function_commandt{
+        smt_identifier_termt{"is_dynamic_object", smt_bool_sortt{}},
+        {smt_bit_vector_sortt{object_bits}}});
+  }
+  SECTION("Apply function")
+  {
+    const smt_identifier_termt object_id{
+      "foo", smt_bit_vector_sortt{object_bits}};
+    const smt_function_application_termt function_application =
+      is_dynamic_object.make_application(std::vector<smt_termt>{object_id});
+    CHECK(
+      function_application.function_identifier() ==
+      smt_identifier_termt{"is_dynamic_object", smt_bool_sortt{}});
+    REQUIRE(function_application.arguments().size() == 1);
+    REQUIRE(function_application.arguments().at(0).get() == object_id);
+  }
+  SECTION("Define result")
+  {
+    const bool dynamic_status = GENERATE(true, false);
+    INFO(
+      "Testing for dynamic status of " +
+      std::string(dynamic_status ? "true" : "false"));
+    const smt_commandt definition =
+      is_dynamic_object.make_definition(42, dynamic_status);
+    CHECK(
+      definition == smt_assert_commandt{smt_core_theoryt::equal(
+                      is_dynamic_object.make_application(std::vector<smt_termt>{
+                        smt_bit_vector_constant_termt{42, object_bits}}),
+                      smt_bool_literal_termt{dynamic_status})});
+  }
+}