Add conversion of is_dynamic_object_exprt to SMT

This is the final step required to complete the implementation of the
support for this kind of expression.

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1042,11 +1042,18 @@ static smt_termt convert_expr_to_smt(
 
 static smt_termt convert_expr_to_smt(
   const is_dynamic_object_exprt &is_dynamic_object,
-  const sub_expression_mapt &converted)
+  const sub_expression_mapt &converted,
+  const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is dynamic object expression: " +
-    is_dynamic_object.pretty());
+  const smt_termt &pointer = converted.at(is_dynamic_object.address());
+  const auto pointer_sort = pointer.get_sort().cast<smt_bit_vector_sortt>();
+  INVARIANT(
+    pointer_sort, "Pointers should be encoded as bit vector sorted terms.");
+  const std::size_t pointer_width = pointer_sort->bit_width();
+  return apply_is_dynamic_object(
+    std::vector<smt_termt>{smt_bit_vector_theoryt::extract(
+      pointer_width - 1,
+      pointer_width - config.bv_encoding.object_bits)(pointer)});
 }
 
 static smt_termt convert_expr_to_smt(
@@ -1458,7 +1465,8 @@ static smt_termt dispatch_expr_to_smt_conversion(
   const sub_expression_mapt &converted,
   const smt_object_mapt &object_map,
   const type_size_mapt &pointer_sizes,
-  const smt_object_sizet::make_applicationt &call_object_size)
+  const smt_object_sizet::make_applicationt &call_object_size,
+  const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
 {
   if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
   {
@@ -1660,7 +1668,8 @@ static smt_termt dispatch_expr_to_smt_conversion(
     const auto is_dynamic_object =
       expr_try_dynamic_cast<is_dynamic_object_exprt>(expr))
   {
-    return convert_expr_to_smt(*is_dynamic_object, converted);
+    return convert_expr_to_smt(
+      *is_dynamic_object, converted, apply_is_dynamic_object);
   }
   if(
     const auto is_invalid_pointer =
@@ -1837,7 +1846,8 @@ smt_termt convert_expr_to_smt(
   const exprt &expr,
   const smt_object_mapt &object_map,
   const type_size_mapt &pointer_sizes,
-  const smt_object_sizet::make_applicationt &object_size)
+  const smt_object_sizet::make_applicationt &object_size,
+  const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
 {
 #ifndef CPROVER_INVARIANT_DO_NOT_CHECK
   static bool in_conversion = false;
@@ -1856,7 +1866,12 @@ smt_termt convert_expr_to_smt(
     if(find_result != sub_expression_map.cend())
       return;
     smt_termt term = dispatch_expr_to_smt_conversion(
-      expr, sub_expression_map, object_map, pointer_sizes, object_size);
+      expr,
+      sub_expression_map,
+      object_map,
+      pointer_sizes,
+      object_size,
+      is_dynamic_object);
     sub_expression_map.emplace_hint(find_result, expr, std::move(term));
   });
   return std::move(sub_expression_map.at(lowered_expr));

src/solvers/smt2_incremental/convert_expr_to_smt.h

@@ -6,6 +6,7 @@
 #include <solvers/smt2_incremental/ast/smt_sorts.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/smt_is_dynamic_object.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 
@@ -27,6 +28,7 @@ smt_termt convert_expr_to_smt(
   const exprt &expression,
   const smt_object_mapt &object_map,
   const type_size_mapt &pointer_sizes,
-  const smt_object_sizet::make_applicationt &object_size);
+  const smt_object_sizet::make_applicationt &object_size,
+  const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -322,12 +322,14 @@ smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
     ns,
     pointer_sizes_map,
     object_map,
-    object_size_function.make_application);
+    object_size_function.make_application,
+    is_dynamic_object_function.make_application);
   return ::convert_expr_to_smt(
     substituted,
     object_map,
     pointer_sizes_map,
-    object_size_function.make_application);
+    object_size_function.make_application,
+    is_dynamic_object_function.make_application);
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
@@ -377,7 +379,8 @@ array_exprt smt2_incremental_decision_proceduret::get_expr(
           from_integer(index, index_type),
           object_map,
           pointer_sizes_map,
-          object_size_function.make_application)),
+          object_size_function.make_application,
+          is_dynamic_object_function.make_application)),
       type.element_type()));
   }
   return array_exprt{elements, type};
@@ -443,7 +446,8 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
         expr,
         object_map,
         pointer_sizes_map,
-        object_size_function.make_application);
+        object_size_function.make_application,
+        is_dynamic_object_function.make_application);
     }
     else
     {

src/solvers/smt2_incremental/type_size_mapping.cpp

@@ -15,7 +15,8 @@ void associate_pointer_sizes(
   const namespacet &ns,
   type_size_mapt &type_size_map,
   const smt_object_mapt &object_map,
-  const smt_object_sizet::make_applicationt &object_size)
+  const smt_object_sizet::make_applicationt &object_size,
+  const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
 {
   expression.visit_pre([&](const exprt &sub_expression) {
     if(
@@ -42,7 +43,11 @@ void associate_pointer_sizes(
         pointer_size_expr = pointer_size_opt.value();
       }
       auto pointer_size_term = convert_expr_to_smt(
-        pointer_size_expr, object_map, type_size_map, object_size);
+        pointer_size_expr,
+        object_map,
+        type_size_map,
+        object_size,
+        is_dynamic_object);
       type_size_map.emplace_hint(
         find_result, pointer_type->base_type(), pointer_size_term);
     }

src/solvers/smt2_incremental/type_size_mapping.h

@@ -10,6 +10,7 @@
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/smt_is_dynamic_object.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
 
 #include <unordered_map>
@@ -33,6 +34,7 @@ void associate_pointer_sizes(
   const namespacet &ns,
   type_size_mapt &type_size_map,
   const smt_object_mapt &object_map,
-  const smt_object_sizet::make_applicationt &object_size);
+  const smt_object_sizet::make_applicationt &object_size,
+  const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object);
 
 #endif

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -59,6 +59,7 @@ struct expr_to_smt_conversion_test_environmentt
 
   smt_object_mapt object_map;
   smt_object_sizet object_size_function;
+  smt_is_dynamic_objectt is_dynamic_object_function;
   type_size_mapt pointer_sizes;
 
 private:
@@ -94,7 +95,8 @@ expr_to_smt_conversion_test_environmentt::convert(const exprt &expression) const
     expression,
     object_map,
     pointer_sizes,
-    object_size_function.make_application);
+    object_size_function.make_application,
+    is_dynamic_object_function.make_application);
 }
 
 TEST_CASE("\"array_typet\" to smt sort conversion", "[core][smt2_incremental]")
@@ -471,7 +473,8 @@ TEST_CASE(
       ns,
       test.pointer_sizes,
       test.object_map,
-      test.object_size_function.make_application);
+      test.object_size_function.make_application,
+      test.is_dynamic_object_function.make_application);
 
     INFO("Input expr: " + pointer_arith_expr.pretty(2, 0));
     const auto constructed_term = test.convert(pointer_arith_expr);
@@ -546,7 +549,8 @@ TEST_CASE(
       ns,
       test.pointer_sizes,
       test.object_map,
-      test.object_size_function.make_application);
+      test.object_size_function.make_application,
+      test.is_dynamic_object_function.make_application);
 
     INFO("Input expr: " + pointer_arith_expr.pretty(2, 0));
     const auto constructed_term = test.convert(pointer_arith_expr);
@@ -577,7 +581,8 @@ TEST_CASE(
       ns,
       test.pointer_sizes,
       test.object_map,
-      test.object_size_function.make_application);
+      test.object_size_function.make_application,
+      test.is_dynamic_object_function.make_application);
     INFO("Input expr: " + pointer_arith_expr.pretty(2, 0));
     const auto constructed_term = test.convert(pointer_arith_expr);
     const auto expected_term = smt_bit_vector_theoryt::subtract(
@@ -614,7 +619,8 @@ TEST_CASE(
       ns,
       test.pointer_sizes,
       test.object_map,
-      test.object_size_function.make_application);
+      test.object_size_function.make_application,
+      test.is_dynamic_object_function.make_application);
     INFO("Input expr: " + pointer_subtraction.pretty(2, 0));
     const auto constructed_term = test.convert(pointer_subtraction);
     const auto expected_term = smt_bit_vector_theoryt::signed_divide(
@@ -1673,6 +1679,30 @@ TEST_CASE(
         smt_bit_vector_theoryt::concat(object, offset))}));
 }
 
+TEST_CASE(
+  "expr to smt conversion for is_dynamic_object expressions",
+  "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+  const symbol_exprt foo{"foo", unsignedbv_typet{32}};
+  const is_dynamic_object_exprt is_dynamic_object{address_of_exprt{foo}};
+  track_expression_objects(is_dynamic_object, ns, test.object_map);
+  const auto foo_id = 2;
+  CHECK(test.object_map.at(foo).unique_id == foo_id);
+  const auto object_bits = config.bv_encoding.object_bits;
+  const auto object = smt_bit_vector_constant_termt{foo_id, object_bits};
+  const auto offset = smt_bit_vector_constant_termt{0, 64 - object_bits};
+  INFO("Expression " + is_dynamic_object.pretty(1, 0));
+  CHECK(
+    test.convert(is_dynamic_object) ==
+    test.is_dynamic_object_function.make_application(std::vector<smt_termt>{
+      smt_bit_vector_theoryt::extract(63, 64 - object_bits)(
+        smt_bit_vector_theoryt::concat(object, offset))}));
+}
+
 TEST_CASE(
   "lower_address_of_array_index works correctly",
   "[core][smt2_incremental]")
@@ -1718,7 +1748,8 @@ TEST_CASE(
       ns,
       test.pointer_sizes,
       test.object_map,
-      test.object_size_function.make_application);
+      test.object_size_function.make_application,
+      test.is_dynamic_object_function.make_application);
     const smt_termt expected = smt_core_theoryt::equal(
       smt_identifier_termt(symbol.get_identifier(), smt_bit_vector_sortt{64}),
       smt_bit_vector_theoryt::add(