Merge pull request #6815 from NlightNFotis/pointer_objects_smt

Conversion of `pointer_object_exprt` and `pointer_offset_exprt` for new SMT backend

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

@@ -0,0 +1,20 @@
+int main()
+{
+  int a = 10;
+  int nondet_bool;
+  int flag = 1;
+
+  int *b = &a;
+  int *c = nondet_bool ? &a : 0;
+  int *d = flag ? &a : 0;
+  int *e;
+
+  // __CPROVER_same_object is True when
+  // `__CPROVER_pointer_object(a) == __CPROVER_pointer_object(b)`
+  __CPROVER_assert(
+    __CPROVER_same_object(b, c), "expected fail as c can be null");
+  __CPROVER_assert(
+    __CPROVER_same_object(b, d), "expected success because d is &a");
+  __CPROVER_assert(
+    __CPROVER_same_object(b, e), "expected fail as e can be null");
+}

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

@@ -0,0 +1,10 @@
+CORE
+pointer_object.c
+--trace --verbosity 10
+\[main\.assertion\.1\] line \d+ expected fail as c can be null: FAILURE
+\[main\.assertion\.2\] line \d+ expected success because d is &a: SUCCESS
+\[main\.assertion\.3\] line \d+ expected fail as e can be null: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--

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

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdbool.h>
+
+int main()
+{
+  int x;
+  int y;
+  int z;
+  bool nondet1;
+  bool nondet2;
+  int *a = nondet1 ? &x : &y;
+  int *b = nondet2 ? &y : &z;
+  __CPROVER_assert(!__CPROVER_same_object(a, b), "Can be violated.");
+}

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

@@ -0,0 +1,17 @@
+CORE
+pointer_object2.c
+--trace --verbosity 10
+\[main\.assertion\.1\] line 13 Can be violated.: FAILURE
+nondet1=FALSE
+nondet2=TRUE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Ensure that two variables which can get assigned the address of the
+same object satisfy the __CPROVER_same_object predicate. In the code
+under test, we negate the predicate to be able to get a failure and a
+trace which we can then match against expected values which guide
+through the path that leads to the two variables getting assigned the
+same object. 

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

@@ -0,0 +1,19 @@
+#define NULL (void *)0
+
+int main()
+{
+  int foo;
+
+  // The identifiers are allocated deterministically, so we want to check the
+  // following properties hold:
+
+  // The pointer object of NULL is always going to be zero.
+  __CPROVER_assert(
+    __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.
+  __CPROVER_assert(
+    __CPROVER_POINTER_OBJECT(&foo) != 1,
+    "expected to fail with object ID == 1");
+}

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

@@ -0,0 +1,13 @@
+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
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that the assignment of object IDs to objects is deterministic:
+* 0 for the NULL object, and
+* 1 for the single object which is the result of an address of operation

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

@@ -0,0 +1,16 @@
+int main()
+{
+  int a;
+  int *p = &a;
+  int *q = &a;
+
+  __CPROVER_assert(
+    __CPROVER_POINTER_OFFSET(p) != __CPROVER_POINTER_OFFSET(q),
+    "expected failure because offsets should be the same");
+
+  // TODO: Remove comments once pointer arithmetic works:
+
+  // *q = p + 2;
+
+  // __CPROVER_assert(__CPROVER_POINTER_OFFSET(p) != __CPROVER_POINTER_OFFSET(q), "expected failure");
+}

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

@@ -0,0 +1,16 @@
+CORE
+pointer_offset.c
+--trace
+\[main\.assertion\.1\] line \d+ expected failure because offsets should be the same: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that the pointer offset bits of two pointers pointing to
+the same object are equal.
+
+The test also contains a fragment of the test which doesn't work
+for now, but would be good to be added as soon as we get pointer
+arithmetic to work, so we can make sure that pointer offset fails
+appropriately.

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

@@ -0,0 +1,14 @@
+int main()
+{
+  int a = 10;
+  int *b = &a;
+  int c;
+
+  *b = 12;
+
+  __CPROVER_assert(a != *b, "a should be different than b");
+  __CPROVER_assert(a == *b, "a should not be different than b");
+  __CPROVER_assert(
+    *b != c,
+    "c can get assigned a value that makes it the same what b points to");
+}

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

@@ -0,0 +1,12 @@
+CORE
+pointers_simple.c
+--trace
+Passing problem to incremental SMT2 solving
+\[main\.assertion.\d\] line \d a should be different than b: FAILURE
+\[main\.assertion.\d\] line \d+ a should not be different than b: SUCCESS
+\[main\.assertion.\d\] line \d+ c can get assigned a value that makes it the same what b points to: FAILURE
+c=12
+^EXIT=10$
+^SIGNAL=0$
+--
+--

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1142,6 +1142,50 @@ static smt_termt convert_expr_to_smt(
     mult_overflow.pretty());
 }
 
+static smt_termt convert_expr_to_smt(
+  const pointer_object_exprt &pointer_object,
+  const sub_expression_mapt &converted)
+{
+  const auto type =
+    type_try_dynamic_cast<bitvector_typet>(pointer_object.type());
+  INVARIANT(type, "Pointer object should have a bitvector-based type.");
+  const auto converted_expr = converted.at(pointer_object.pointer());
+  const std::size_t width = type->get_width();
+  const std::size_t object_bits = config.bv_encoding.object_bits;
+  INVARIANT(
+    width >= object_bits,
+    "Width should be at least as big as the number of object bits.");
+  const std::size_t ext = width - object_bits;
+  const auto extract_op = smt_bit_vector_theoryt::extract(
+    width - 1, width - object_bits)(converted_expr);
+  if(ext > 0)
+  {
+    return smt_bit_vector_theoryt::zero_extend(ext)(extract_op);
+  }
+  return extract_op;
+}
+
+static smt_termt convert_expr_to_smt(
+  const pointer_offset_exprt &pointer_offset,
+  const sub_expression_mapt &converted)
+{
+  const auto type =
+    type_try_dynamic_cast<bitvector_typet>(pointer_offset.type());
+  INVARIANT(type, "Pointer offset should have a bitvector-based type.");
+  const auto converted_expr = converted.at(pointer_offset.pointer());
+  const std::size_t width = type->get_width();
+  std::size_t offset_bits = width - config.bv_encoding.object_bits;
+  if(offset_bits > width)
+    offset_bits = width;
+  const auto extract_op =
+    smt_bit_vector_theoryt::extract(offset_bits - 1, 0)(converted_expr);
+  if(width > offset_bits)
+  {
+    return smt_bit_vector_theoryt::zero_extend(width - offset_bits)(extract_op);
+  }
+  return extract_op;
+}
+
 static smt_termt convert_expr_to_smt(
   const shl_overflow_exprt &shl_overflow,
   const sub_expression_mapt &converted)
@@ -1433,14 +1477,18 @@ static smt_termt dispatch_expr_to_smt_conversion(
   {
     return convert_expr_to_smt(*member_extraction, converted);
   }
-#if 0
-  else if(expr.id()==ID_pointer_offset)
+  else if(
+    const auto pointer_offset =
+      expr_try_dynamic_cast<pointer_offset_exprt>(expr))
   {
+    return convert_expr_to_smt(*pointer_offset, converted);
   }
-  else if(expr.id()==ID_pointer_object)
+  else if(
+    const auto pointer_object =
+      expr_try_dynamic_cast<pointer_object_exprt>(expr))
   {
+    return convert_expr_to_smt(*pointer_object, converted);
   }
-#endif
   if(
     const auto is_dynamic_object =
       expr_try_dynamic_cast<is_dynamic_object_exprt>(expr))

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -8,6 +8,7 @@
 #include <util/constructor_of.h>
 #include <util/format.h>
 #include <util/namespace.h>
+#include <util/pointer_predicates.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
@@ -1186,3 +1187,94 @@ TEST_CASE(
                        smt_bit_vector_constant_termt{0, 56})));
   }
 }
+
+TEST_CASE(
+  "expr to smt conversion for pointer object expression",
+  "[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();
+  config.bv_encoding.object_bits = 8;
+
+  const auto pointer_type = pointer_typet(unsigned_int_type(), 64 /* bits */);
+  const pointer_object_exprt foo{
+    symbol_exprt{"foo", pointer_type}, pointer_type};
+  const pointer_object_exprt foobar{
+    symbol_exprt{"foobar", pointer_type}, pointer_type};
+
+  SECTION("Pointer object expression")
+  {
+    const auto converted = convert_expr_to_smt(foo);
+    const auto expected =
+      smt_bit_vector_theoryt::zero_extend(56)(smt_bit_vector_theoryt::extract(
+        63, 56)(smt_identifier_termt("foo", smt_bit_vector_sortt(64))));
+    CHECK(converted == expected);
+  }
+
+  SECTION("Invariant checks")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    SECTION("Pointer object's operand type should be a bitvector type")
+    {
+      auto copy_of_foo = foo;
+      copy_of_foo.type() = bool_typet{};
+      REQUIRE_THROWS_MATCHES(
+        convert_expr_to_smt(copy_of_foo),
+        invariant_failedt,
+        invariant_failure_containing(
+          "Pointer object should have a bitvector-based type."));
+    }
+  }
+
+  SECTION("Comparison of pointer objects.")
+  {
+    const exprt comparison = notequal_exprt{foobar, foo};
+    INFO("Expression " + comparison.pretty(1, 0));
+    const auto converted = convert_expr_to_smt(comparison);
+    const auto bv1 =
+      smt_bit_vector_theoryt::zero_extend(56)(smt_bit_vector_theoryt::extract(
+        63, 56)(smt_identifier_termt("foo", smt_bit_vector_sortt(64))));
+    const auto bv2 =
+      smt_bit_vector_theoryt::zero_extend(56)(smt_bit_vector_theoryt::extract(
+        63, 56)(smt_identifier_termt("foobar", smt_bit_vector_sortt(64))));
+    const auto expected = smt_core_theoryt::distinct(bv2, bv1);
+    CHECK(converted == expected);
+  }
+}
+
+TEST_CASE("pointer_offset_exprt to SMT conversion", "[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();
+  config.bv_encoding.object_bits = 8;
+
+  const auto pointer_type = pointer_typet(unsigned_int_type(), 64 /* bits */);
+  const pointer_offset_exprt pointer_offset{
+    symbol_exprt{"foo", pointer_type}, pointer_type};
+
+  SECTION("simple pointer_offset_exprt conversion")
+  {
+    const auto converted = convert_expr_to_smt(pointer_offset);
+    const auto expected =
+      smt_bit_vector_theoryt::zero_extend(8)(smt_bit_vector_theoryt::extract(
+        55, 0)(smt_identifier_termt("foo", smt_bit_vector_sortt(64))));
+    CHECK(converted == expected);
+  }
+
+  SECTION("Invariant checks")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    SECTION("pointer_offset_exprt's operand type should be a bitvector type")
+    {
+      auto pointer_offset_copy = pointer_offset;
+      pointer_offset_copy.type() = bool_typet{};
+      REQUIRE_THROWS_MATCHES(
+        convert_expr_to_smt(pointer_offset_copy),
+        invariant_failedt,
+        invariant_failure_containing(
+          "Pointer offset should have a bitvector-based type."));
+    }
+  }
+}