Merge pull request #7035 from esteffin/esteffin/is-invalid-pointer-to-smt

Add support for is_invalid_pointer in new SMT2 backend

Author: NlightNFotis

regression/cbmc-incr-smt2/pointers/pointer_is_invalid.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  // special value of the invalid pointer (object bits = 1 and offset = 0), as
+  // checked for by __CPROVER_is_invalid_pointer()
+  char *p = (size_t)1 << (sizeof(char *) * 8 - 8);
+  __CPROVER_assert(
+    __CPROVER_is_invalid_pointer(p), "INVALID pointer, so passing");
+  int i;
+  __CPROVER_assert(
+    __CPROVER_is_invalid_pointer(&i), "VALID pointer, so failing");
+}

regression/cbmc-incr-smt2/pointers/pointer_is_invalid.desc

@@ -0,0 +1,13 @@
+CORE
+pointer_is_invalid.c
+
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line \d+ INVALID pointer, so passing: SUCCESS
+\[main\.assertion\.2\] line \d+ VALID pointer, so failing: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Tests that an inconsistent assumption involving the special invalid pointer
+value and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc-incr-smt2/pointers/pointer_object3.c

@@ -12,8 +12,9 @@ int main()
     __CPROVER_POINTER_OBJECT(NULL) != 0,
     "expected to fail with object ID == 0");
   // In the case where the program contains a single address of operation,
-  // the pointer object is going to be 1.
+  // the pointer object is going to be 2 (1 is invalid pointer that is tested
+  // somewhere else).
   __CPROVER_assert(
-    __CPROVER_POINTER_OBJECT(&foo) != 1,
-    "expected to fail with object ID == 1");
+    __CPROVER_POINTER_OBJECT(&foo) != 2,
+    "expected to fail with object ID == 2");
 }

regression/cbmc-incr-smt2/pointers/pointer_object3.desc

@@ -2,7 +2,7 @@ CORE
 pointer_object3.c
 
 \[main\.assertion\.1] line \d+ expected to fail with object ID == 0: FAILURE
-\[main\.assertion\.2] line \d+ expected to fail with object ID == 1: FAILURE
+\[main\.assertion\.2] line \d+ expected to fail with object ID == 2: FAILURE
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1046,20 +1046,37 @@ static smt_termt convert_expr_to_smt(
 
 static smt_termt convert_expr_to_smt(
   const is_invalid_pointer_exprt &is_invalid_pointer,
+  const smt_object_mapt &object_map,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is invalid pointer expression: " +
-    is_invalid_pointer.pretty());
+  const exprt &pointer_expr(to_unary_expr(is_invalid_pointer).op());
+  const bitvector_typet *pointer_type =
+    type_try_dynamic_cast<bitvector_typet>(pointer_expr.type());
+  INVARIANT(pointer_type, "Pointer object should have a bitvector-based type.");
+  const std::size_t object_bits = config.bv_encoding.object_bits;
+  const std::size_t width = pointer_type->get_width();
+  INVARIANT(
+    width >= object_bits,
+    "Width should be at least as big as the number of object bits.");
+
+  const auto extract_op = smt_bit_vector_theoryt::extract(
+    width - 1, width - object_bits)(converted.at(pointer_expr));
+
+  const auto &invalid_pointer = object_map.at(make_invalid_pointer_expr());
+
+  const smt_termt invalid_pointer_address = smt_bit_vector_constant_termt(
+    invalid_pointer.unique_id, config.bv_encoding.object_bits);
+
+  return smt_core_theoryt::equal(invalid_pointer_address, extract_op);
 }
 
 static smt_termt convert_expr_to_smt(
-  const string_constantt &is_invalid_pointer,
+  const string_constantt &string_constant,
   const sub_expression_mapt &converted)
 {
   UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is invalid pointer expression: " +
-    is_invalid_pointer.pretty());
+    "Generation of SMT formula for string constant expression: " +
+    string_constant.pretty());
 }
 
 static smt_termt convert_expr_to_smt(
@@ -1643,7 +1660,7 @@ static smt_termt dispatch_expr_to_smt_conversion(
     const auto is_invalid_pointer =
       expr_try_dynamic_cast<is_invalid_pointer_exprt>(expr))
   {
-    return convert_expr_to_smt(*is_invalid_pointer, converted);
+    return convert_expr_to_smt(*is_invalid_pointer, object_map, converted);
   }
   if(const auto string_constant = expr_try_dynamic_cast<string_constantt>(expr))
   {

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

@@ -222,6 +222,27 @@ TEST_CASE(
   REQUIRE_THROWS(test.convert(or_exprt{{true_exprt{}}}));
 }
 
+TEST_CASE(
+  "expr to smt conversion for \"is_invalid_pointer\" operator",
+  "[core][smt2_incremental]")
+{
+  const std::size_t object_bits = config.bv_encoding.object_bits;
+  const auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+  const pointer_typet pointer_type = ::pointer_type(void_type());
+  const std::size_t pointer_width = pointer_type.get_width();
+  const constant_exprt invalid_ptr{
+    integer2bvrep(1ul << (pointer_width - object_bits), pointer_width),
+    pointer_type};
+  const is_invalid_pointer_exprt is_invalid_ptr{invalid_ptr};
+  const smt_termt expected_smt_term = smt_core_theoryt::equal(
+    smt_bit_vector_constant_termt{1, config.bv_encoding.object_bits},
+    smt_bit_vector_theoryt::extract(
+      pointer_width - 1,
+      pointer_width - object_bits)(test.convert(invalid_ptr)));
+  CHECK(test.convert(is_invalid_ptr) == expected_smt_term);
+}
+
 TEST_CASE(
   "expr to smt conversion for \"xor\" operator",
   "[core][smt2_incremental]")
@@ -1358,20 +1379,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 +1450,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 +1564,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();