Merge pull request #6815 from NlightNFotis/pointer_objects_smt

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

Author: NlightNFotis

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$
+--
+--