Add conversion of address_of(symbol) to SMT terms

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -4,6 +4,7 @@
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/expr.h>
 #include <util/expr_cast.h>
 #include <util/expr_util.h>
@@ -732,10 +733,53 @@ static smt_termt convert_expr_to_smt(
   }
 }
 
+#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
+static mp_integer power2(unsigned exponent)
+{
+  mp_integer result;
+  result.setPower2(exponent);
+  return result;
+}
+#endif
+
+/// \details
+/// This conversion constructs a bit vector representation of the memory
+/// address. This address is composed of 2 concatenated bit vector components.
+/// The first part is the base object's unique identifier. The second is the
+/// offset into that object. For address of symbols the offset will be 0. The
+/// offset may be non-zero for cases such as the address of a member field of a
+/// struct or a the address of a non-zero index into an array.
 static smt_termt convert_expr_to_smt(
   const address_of_exprt &address_of,
-  const sub_expression_mapt &converted)
+  const sub_expression_mapt &converted,
+  const smt_object_mapt &object_map)
 {
+  const auto type = type_try_dynamic_cast<pointer_typet>(address_of.type());
+  INVARIANT(
+    type, "Result of the address_of operator should have pointer type.");
+  const auto base = find_object_base_expression(address_of);
+  const auto object = object_map.find(base);
+  INVARIANT(
+    object != object_map.end(),
+    "Objects should be tracked before converting their address to SMT terms");
+  const std::size_t object_id = object->second.unique_id;
+  INVARIANT(
+    object_id < power2(config.bv_encoding.object_bits),
+    "There should be sufficient bits to encode unique object identifier.");
+  const smt_termt object_bit_vector =
+    smt_bit_vector_constant_termt{object_id, config.bv_encoding.object_bits};
+  INVARIANT(
+    type->get_width() > config.bv_encoding.object_bits,
+    "Pointer should be wider than object_bits in order to allow for offset "
+    "encoding.");
+  const size_t offset_bits = type->get_width() - config.bv_encoding.object_bits;
+  if(
+    const auto symbol =
+      expr_try_dynamic_cast<symbol_exprt>(address_of.object()))
+  {
+    const smt_bit_vector_constant_termt offset{0, offset_bits};
+    return smt_bit_vector_theoryt::concat(object_bit_vector, offset);
+  }
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for address of expression: " +
     address_of.pretty());
@@ -1193,7 +1237,8 @@ static smt_termt convert_expr_to_smt(
 
 static smt_termt dispatch_expr_to_smt_conversion(
   const exprt &expr,
-  const sub_expression_mapt &converted)
+  const sub_expression_mapt &converted,
+  const smt_object_mapt &object_map)
 {
   if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
   {
@@ -1347,7 +1392,7 @@ static smt_termt dispatch_expr_to_smt_conversion(
 #endif
   if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
   {
-    return convert_expr_to_smt(*address_of, converted);
+    return convert_expr_to_smt(*address_of, converted, object_map);
   }
   if(const auto array_of = expr_try_dynamic_cast<array_of_exprt>(expr))
   {
@@ -1547,7 +1592,8 @@ at_scope_exitt<functiont> at_scope_exit(functiont exit_function)
 }
 #endif
 
-smt_termt convert_expr_to_smt(const exprt &expr)
+smt_termt
+convert_expr_to_smt(const exprt &expr, const smt_object_mapt &object_map)
 {
 #ifndef CPROVER_INVARIANT_DO_NOT_CHECK
   static bool in_conversion = false;
@@ -1564,7 +1610,8 @@ smt_termt convert_expr_to_smt(const exprt &expr)
     const auto find_result = sub_expression_map.find(expr);
     if(find_result != sub_expression_map.cend())
       return;
-    smt_termt term = dispatch_expr_to_smt_conversion(expr, sub_expression_map);
+    smt_termt term =
+      dispatch_expr_to_smt_conversion(expr, sub_expression_map, object_map);
     sub_expression_map.emplace_hint(find_result, expr, std::move(term));
   });
   return std::move(sub_expression_map.at(expr));

src/solvers/smt2_incremental/convert_expr_to_smt.h

@@ -3,6 +3,7 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
 
+#include <solvers/smt2_incremental/object_tracking.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 
@@ -15,6 +16,7 @@ smt_sortt convert_type_to_smt_sort(const typet &type);
 
 /// \brief Converts the \p expression to an smt encoding of the same expression
 ///   stored as term ast (abstract syntax tree).
-smt_termt convert_expr_to_smt(const exprt &expression);
+smt_termt
+convert_expr_to_smt(const exprt &expression, const smt_object_mapt &object_map);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -132,7 +132,8 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
   : ns{_ns},
     number_of_solver_calls{0},
     solver_process(std::move(_solver_process)),
-    log{message_handler}
+    log{message_handler},
+    object_map{initial_smt_object_map()}
 {
   solver_process->send(
     smt_set_option_commandt{smt_option_produce_modelst{true}});
@@ -157,6 +158,13 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
   solver_process->send(function);
 }
 
+smt_termt
+smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
+{
+  track_expression_objects(expr, ns, object_map);
+  return ::convert_expr_to_smt(expr, object_map);
+}
+
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
 {
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
@@ -193,7 +201,11 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
   {
     if(gather_dependent_expressions(expr).empty())
     {
-      descriptor = convert_expr_to_smt(expr);
+      INVARIANT(
+        objects_are_already_tracked(expr, object_map),
+        "Objects in expressions being read should already be tracked from "
+        "point of being set/handled.");
+      descriptor = ::convert_expr_to_smt(expr, object_map);
     }
     else
     {

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -6,11 +6,13 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 
-#include <solvers/smt2_incremental/smt_terms.h>
-#include <solvers/stack_decision_procedure.h>
 #include <util/message.h>
 #include <util/std_expr.h>
 
+#include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/smt_terms.h>
+#include <solvers/stack_decision_procedure.h>
+
 #include <memory>
 #include <unordered_map>
 #include <unordered_set>
@@ -55,6 +57,9 @@ class smt2_incremental_decision_proceduret final
   ///   been defined, along with their dependencies in turn.
   void define_dependent_functions(const exprt &expr);
   void ensure_handle_for_expr_defined(const exprt &expr);
+  /// \brief Add objects in \p expr to object_map if needed and convert to smt.
+  /// \note This function is non-const because it mutates the object_map.
+  smt_termt convert_expr_to_smt(const exprt &expr);
 
   const namespacet &ns;
 
@@ -78,6 +83,7 @@ class smt2_incremental_decision_proceduret final
     expression_handle_identifiers;
   std::unordered_map<exprt, smt_identifier_termt, irep_hash>
     expression_identifiers;
+  smt_object_mapt object_map;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -7,13 +7,17 @@
 #include <util/config.h>
 #include <util/constructor_of.h>
 #include <util/format.h>
+#include <util/namespace.h>
 #include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
+#include <solvers/smt2_incremental/object_tracking.h>
 #include <solvers/smt2_incremental/smt_bit_vector_theory.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
+#include <testing-utils/invariant.h>
 #include <testing-utils/use_catch.h>
 
 TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]")
@@ -38,6 +42,11 @@ TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]")
   }
 }
 
+smt_termt convert_expr_to_smt(const exprt &expression)
+{
+  return convert_expr_to_smt(expression, initial_smt_object_map());
+}
+
 TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]")
 {
   CHECK(
@@ -1072,3 +1081,108 @@ TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]")
     }
   }
 }
+
+TEST_CASE(
+  "expr to smt conversion for address of operator",
+  "[core][smt2_incremental]")
+{
+  // The config lines are necessary to ensure that pointer width in configured.
+  config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
+  config.ansi_c.set_arch_spec_x86_64();
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+  smt_object_mapt object_map = initial_smt_object_map();
+  const symbol_exprt foo{"foo", unsignedbv_typet{32}};
+  const symbol_exprt bar{"bar", unsignedbv_typet{32}};
+  SECTION("Address of symbol")
+  {
+    const address_of_exprt address_of_foo{foo};
+    track_expression_objects(address_of_foo, ns, object_map);
+    INFO("Expression " + address_of_foo.pretty(1, 0));
+    SECTION("8 object bits")
+    {
+      config.bv_encoding.object_bits = 8;
+      const auto converted = convert_expr_to_smt(address_of_foo, object_map);
+      CHECK(object_map.at(foo).unique_id == 1);
+      CHECK(
+        converted == smt_bit_vector_theoryt::concat(
+                       smt_bit_vector_constant_termt{1, 8},
+                       smt_bit_vector_constant_termt{0, 56}));
+    }
+    SECTION("16 object bits")
+    {
+      config.bv_encoding.object_bits = 16;
+      const auto converted = convert_expr_to_smt(address_of_foo, object_map);
+      CHECK(object_map.at(foo).unique_id == 1);
+      CHECK(
+        converted == smt_bit_vector_theoryt::concat(
+                       smt_bit_vector_constant_termt{1, 16},
+                       smt_bit_vector_constant_termt{0, 48}));
+    }
+  }
+  SECTION("Invariant checks")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    SECTION("Address of should result in a pointer")
+    {
+      exprt address_of = address_of_exprt{foo};
+      address_of.type() = bool_typet{};
+      REQUIRE_THROWS_MATCHES(
+        convert_expr_to_smt(address_of, object_map),
+        invariant_failedt,
+        invariant_failure_containing(
+          "Result of the address_of operator should have pointer type."));
+    }
+    SECTION("Objects should already be tracked")
+    {
+      REQUIRE_THROWS_MATCHES(
+        convert_expr_to_smt(address_of_exprt{foo}, object_map),
+        invariant_failedt,
+        invariant_failure_containing("Objects should be tracked before "
+                                     "converting their address to SMT terms"));
+    }
+    SECTION("There should be enough bits for object id")
+    {
+      config.bv_encoding.object_bits = 8;
+      const address_of_exprt address_of_foo{foo};
+      track_expression_objects(address_of_foo, ns, object_map);
+      object_map.at(foo).unique_id = 256;
+      REQUIRE_THROWS_MATCHES(
+        convert_expr_to_smt(address_of_exprt{foo}, object_map),
+        invariant_failedt,
+        invariant_failure_containing("There should be sufficient bits to "
+                                     "encode unique object identifier."));
+    }
+    SECTION("Pointer should be wide enough to encode offset")
+    {
+      config.bv_encoding.object_bits = 64;
+      const address_of_exprt address_of_foo{foo};
+      track_expression_objects(address_of_foo, ns, object_map);
+      object_map.at(foo).unique_id = 256;
+      REQUIRE_THROWS_MATCHES(
+        convert_expr_to_smt(address_of_exprt{foo}, object_map),
+        invariant_failedt,
+        invariant_failure_containing("Pointer should be wider than object_bits "
+                                     "in order to allow for offset encoding."));
+    }
+  }
+  SECTION("Comparison of address of operations.")
+  {
+    config.bv_encoding.object_bits = 8;
+    const exprt comparison =
+      notequal_exprt{address_of_exprt{foo}, address_of_exprt{bar}};
+    track_expression_objects(comparison, ns, object_map);
+    INFO("Expression " + comparison.pretty(1, 0));
+    const auto converted = convert_expr_to_smt(comparison, object_map);
+    CHECK(object_map.at(foo).unique_id == 2);
+    CHECK(object_map.at(bar).unique_id == 1);
+    CHECK(
+      converted == smt_core_theoryt::distinct(
+                     smt_bit_vector_theoryt::concat(
+                       smt_bit_vector_constant_termt{2, 8},
+                       smt_bit_vector_constant_termt{0, 56}),
+                     smt_bit_vector_theoryt::concat(
+                       smt_bit_vector_constant_termt{1, 8},
+                       smt_bit_vector_constant_termt{0, 56})));
+  }
+}