Add regression tests to for inconsistent assumptions involving __CPROVER_r_ok()

Adds tests to check that inconsistent assumptions involving __CPROVER_r_ok() can
be detected by checking if a subsequent assert(0) fails.

Author: danpoe

regression/CMakeLists.txt

@@ -55,6 +55,7 @@ add_subdirectory(goto-harness)
 add_subdirectory(goto-cc-file-local)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)
+add_subdirectory(cbmc-primitives)
 
 if(WITH_MEMORY_ANALYZER)
   add_subdirectory(snapshot-harness)

regression/Makefile

@@ -32,6 +32,7 @@ DIRS = cbmc \
        symtab2gb \
        solver-hardness \
        goto-ld \
+       cbmc-primitives \
        # Empty last line
 
 ifeq ($(OS),Windows_NT)

regression/cbmc-primitives/r_w_ok_inconsistent_dead/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p;
+
+  {
+    char c;
+    p = &c;
+  }
+
+  __CPROVER_assume(__CPROVER_r_ok(p, 1));
+  assert(0); // fails
+  *p;        // succeeds
+}

regression/cbmc-primitives/r_w_ok_inconsistent_dead/test-no-cp.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--function test_global_pointer --pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer to an out of scope
+variable and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc-primitives/r_w_ok_inconsistent_dead/test.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--function test_global_pointer --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer to an out of scope
+variable and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  free(p);
+
+  __CPROVER_assume(__CPROVER_r_ok(p, 1));
+  assert(0); // fails
+  *p;        // succeeds
+}

regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/test-no-cp.desc

@@ -0,0 +1,12 @@
+FUTURE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer initialized to an
+integer address not pointing to memory and __CPROVER_r_ok() can be detected via
+assert(0).

regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/test.desc

@@ -0,0 +1,12 @@
+FUTURE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer initialized to an
+integer address not pointing to memory and __CPROVER_r_ok() can be detected via
+assert(0).

regression/cbmc-primitives/r_w_ok_inconsistent_integer/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  // pointer with object bits = 123 and offset = 123
+  char *p = (size_t)123 << (sizeof(char *) * 8 - 8) | 123;
+  __CPROVER_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // fails
+  *p;        // succeeds
+}

regression/cbmc-primitives/r_w_ok_inconsistent_integer/test-no-cp.desc

@@ -0,0 +1,12 @@
+FUTURE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer initialized to an
+integer address not pointing to memory and __CPROVER_r_ok() can be detected via
+assert(0).

regression/cbmc-primitives/r_w_ok_inconsistent_integer/test.desc

@@ -0,0 +1,12 @@
+FUTURE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer initialized to an
+integer address not pointing to memory and __CPROVER_r_ok() can be detected via
+assert(0).

regression/cbmc-primitives/r_w_ok_inconsistent_invalid/main.c

@@ -0,0 +1,12 @@
+#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_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // fails
+  *p;        // succeeds
+}

regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving the special invalid pointer
+value and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving the special invalid pointer
+value and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc-primitives/r_w_ok_inconsistent_nondet/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+char *nondet();
+
+void main()
+{
+  char *p = nondet();
+  __CPROVER_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // fails
+  *p;        // succeeds
+}

regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test-no-cp.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a nondet pointer and
+__CPROVER_r_ok() can be detected via assert(0).

regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a nondet pointer and
+__CPROVER_r_ok() can be detected via assert(0).

regression/cbmc-primitives/r_w_ok_null/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = NULL;
+  assert(!__CPROVER_r_ok(p, 10));
+}

regression/cbmc-primitives/r_w_ok_null/test-no-cp.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that __CPROVER_r_ok() on a null pointers is false

regression/cbmc-primitives/r_w_ok_null/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that __CPROVER_r_ok() on a null pointers is false

regression/cbmc-primitives/r_w_ok_valid/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+char c1;
+
+void main()
+{
+  char c2;
+
+  char *p1 = &c1;
+  assert(__CPROVER_r_ok(p1, 1));
+
+  char *p2 = &c2;
+  assert(__CPROVER_r_ok(p2, 1));
+
+  char *p3 = malloc(1);
+  __CPROVER_assume(p1 != NULL);
+  assert(__CPROVER_r_ok(p3, 1));
+}

regression/cbmc-primitives/r_w_ok_valid/test-no-cp.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that __CPROVER_r_ok() is true for valid pointers to global, local, or
+malloced memory

regression/cbmc-primitives/r_w_ok_valid/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that __CPROVER_r_ok() is true for valid pointers to global, local, or
+malloced memory

regression/cbmc-primitives/r_w_ok_valid_negated/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+#include <stdlib.h>
+
+char c1;
+
+void main()
+{
+  // We check the conditions for a pointer to global static memory (p1), a
+  // pointer to local memory (p2), and a pointer to dynamic memory (p3).
+  // For each pointer, we check:
+  // (1) whether it is unsafe to access one byte more than was allocated
+  // (2) whether it is unsafe to access one byte before the allocated memory
+  // (3) whether it is unsafe to access one byte after the allocated memory
+
+  char c2;
+
+  char *p1 = &c1;
+
+  assert(!__CPROVER_r_ok(p1, 2));
+  assert(!__CPROVER_r_ok(p1 - 1, 1));
+  assert(!__CPROVER_r_ok(p1 + 1, 1));
+
+  char *p2 = &c2;
+
+  assert(!__CPROVER_r_ok(p2, 2));
+  assert(!__CPROVER_r_ok(p2 - 1, 1));
+  assert(!__CPROVER_r_ok(p2 + 1, 1));
+
+  char *p3 = malloc(1);
+
+  assert(!__CPROVER_r_ok(p3, 2));
+  assert(!__CPROVER_r_ok(p3 - 1, 1));
+  assert(!__CPROVER_r_ok(p3 + 1, 1));
+}

regression/cbmc-primitives/r_w_ok_valid_negated/test-no-cp.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that __CPROVER_r_ok() is false for a pointer to a valid memory object,
+though potentially with an offset that is out of bounds.

regression/cbmc-primitives/r_w_ok_valid_negated/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that __CPROVER_r_ok() is false for a pointer to a valid memory object,
+though potentially with an offset that is out of bounds.