Add invalid pointer object to smt_object_map and fix tests

Author: Enrico Steffinlongo

src/solvers/smt2_incremental/object_tracking.cpp

@@ -9,6 +9,11 @@
 #include <util/std_expr.h>
 #include <util/string_constant.h>
 
+exprt make_invalid_pointer_expr()
+{
+  return constant_exprt(ID_invalid, pointer_type(void_type()));
+}
+
 exprt find_object_base_expression(const address_of_exprt &address_of)
 {
   auto current = std::ref(address_of.object());
@@ -47,12 +52,28 @@ static decision_procedure_objectt make_null_object()
   return null_object;
 }
 
+static decision_procedure_objectt make_invalid_pointer_object()
+{
+  decision_procedure_objectt invalid_pointer_object;
+  // Using unique_id = 1, so 0 is the NULL object, 1 is the invalid object and
+  // other valid objects have unique_id > 1.
+  invalid_pointer_object.unique_id = 1;
+  invalid_pointer_object.base_expression = make_invalid_pointer_expr();
+  invalid_pointer_object.size = from_integer(0, size_type());
+  return invalid_pointer_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));
+  exprt null_object_base = null_object.base_expression;
+  object_map.emplace(std::move(null_object_base), std::move(null_object));
+  decision_procedure_objectt invalid_pointer_object =
+    make_invalid_pointer_object();
+  exprt invalid_pointer_object_base = invalid_pointer_object.base_expression;
+  object_map.emplace(
+    std::move(invalid_pointer_object_base), std::move(invalid_pointer_object));
   return object_map;
 }
 

src/solvers/smt2_incremental/object_tracking.h

@@ -115,4 +115,7 @@ bool objects_are_already_tracked(
   const exprt &expression,
   const smt_object_mapt &object_map);
 
+/// \brief Create the invalid pointer constant
+exprt make_invalid_pointer_expr();
+
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1358,20 +1358,20 @@ TEST_CASE(
     {
       config.bv_encoding.object_bits = 8;
       const auto converted = test.convert(address_of_foo);
-      CHECK(test.object_map.at(foo).unique_id == 1);
+      CHECK(test.object_map.at(foo).unique_id == 2);
       CHECK(
         converted == smt_bit_vector_theoryt::concat(
-                       smt_bit_vector_constant_termt{1, 8},
+                       smt_bit_vector_constant_termt{2, 8},
                        smt_bit_vector_constant_termt{0, 56}));
     }
     SECTION("16 object bits")
     {
       config.bv_encoding.object_bits = 16;
       const auto converted = test.convert(address_of_foo);
-      CHECK(test.object_map.at(foo).unique_id == 1);
+      CHECK(test.object_map.at(foo).unique_id == 2);
       CHECK(
         converted == smt_bit_vector_theoryt::concat(
-                       smt_bit_vector_constant_termt{1, 16},
+                       smt_bit_vector_constant_termt{2, 16},
                        smt_bit_vector_constant_termt{0, 48}));
     }
   }
@@ -1429,15 +1429,15 @@ TEST_CASE(
     track_expression_objects(comparison, ns, test.object_map);
     INFO("Expression " + comparison.pretty(1, 0));
     const auto converted = test.convert(comparison);
-    CHECK(test.object_map.at(foo).unique_id == 2);
-    CHECK(test.object_map.at(bar).unique_id == 1);
+    CHECK(test.object_map.at(foo).unique_id == 3);
+    CHECK(test.object_map.at(bar).unique_id == 2);
     CHECK(
       converted == smt_core_theoryt::distinct(
                      smt_bit_vector_theoryt::concat(
-                       smt_bit_vector_constant_termt{2, 8},
+                       smt_bit_vector_constant_termt{3, 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{2, 8},
                        smt_bit_vector_constant_termt{0, 56})));
   }
 }
@@ -1543,7 +1543,7 @@ TEST_CASE(
   const object_size_exprt object_size{
     address_of_exprt{foo}, unsignedbv_typet{64}};
   track_expression_objects(object_size, ns, test.object_map);
-  const auto foo_id = 1;
+  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};

unit/solvers/smt2_incremental/object_tracking.cpp

@@ -118,11 +118,20 @@ TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]")
   smt_object_mapt object_map = initial_smt_object_map();
   SECTION("Check initial object map has null pointer")
   {
-    REQUIRE(object_map.size() == 1);
+    REQUIRE(object_map.size() == 2);
     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);
+    const auto actual_null_object = object_map.find(null_pointer);
+    CHECK(actual_null_object->first == null_pointer);
+    CHECK(actual_null_object->second.unique_id == 0);
+    CHECK(actual_null_object->second.base_expression == null_pointer);
+    const exprt invalid_object_pointer = make_invalid_pointer_expr();
+    const auto actual_invalid_object_pointer =
+      object_map.find(invalid_object_pointer);
+    CHECK(actual_invalid_object_pointer->first == invalid_object_pointer);
+    CHECK(actual_invalid_object_pointer->second.unique_id == 1);
+    CHECK(
+      actual_invalid_object_pointer->second.base_expression ==
+      invalid_object_pointer);
   }
   symbol_tablet symbol_table;
   namespacet ns{symbol_table};
@@ -133,15 +142,15 @@ TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]")
   track_expression_objects(compound_expression, ns, object_map);
   SECTION("Tracking expression objects")
   {
-    CHECK(object_map.size() == 4);
+    CHECK(object_map.size() == 5);
     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 == 3);
+    CHECK(foo_object->second.unique_id == 4);
     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);
+    CHECK(bar_object->second.unique_id == 2);
   }
   SECTION("Confirming objects are tracked.")
   {

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -414,6 +414,9 @@ TEST_CASE(
   const auto null_object_size_definition =
     test.object_size_function.make_definition(
       0, smt_bit_vector_constant_termt{0, 32});
+  const auto invalid_pointer_object_size_definition =
+    test.object_size_function.make_definition(
+      1, smt_bit_vector_constant_termt{0, 32});
   const symbolt foo = make_test_symbol("foo", signedbv_typet{16});
   const smt_identifier_termt foo_term{"foo", smt_bit_vector_sortt{16}};
   const exprt expr_42 = from_integer({42}, signedbv_typet{16});
@@ -425,13 +428,23 @@ TEST_CASE(
     test.procedure.set_to(equal_42, true);
     test.mock_responses.push_back(smt_check_sat_responset{smt_sat_responset{}});
     test.procedure();
+    std::vector<smt_commandt> expected_commands{
+      smt_declare_function_commandt{foo_term, {}},
+      smt_assert_commandt{smt_core_theoryt::equal(foo_term, term_42)},
+      invalid_pointer_object_size_definition,
+      null_object_size_definition,
+      smt_check_sat_commandt{}};
     REQUIRE(
-      test.sent_commands ==
-      std::vector<smt_commandt>{
-        smt_declare_function_commandt{foo_term, {}},
-        smt_assert_commandt{smt_core_theoryt::equal(foo_term, term_42)},
-        null_object_size_definition,
-        smt_check_sat_commandt{}});
+      (test.sent_commands.size() == expected_commands.size() &&
+       std::all_of(
+         expected_commands.begin(),
+         expected_commands.end(),
+         [&](const smt_commandt &command) -> bool {
+           return std::find(
+                    test.sent_commands.begin(),
+                    test.sent_commands.end(),
+                    command) != test.sent_commands.end();
+         })));
     SECTION("Get \"foo\" value back")
     {
       test.sent_commands.clear();