Tests to check inconsistent assumptions involving __CPROVER_r_ok

regression/CMakeLists.txt

@@ -56,6 +56,7 @@ add_subdirectory(goto-cc-file-local)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)
 add_subdirectory(validate-trace-xml-schema)
+add_subdirectory(cbmc-primitives)
 
 if(WITH_MEMORY_ANALYZER)
   add_subdirectory(snapshot-harness)

regression/Makefile

@@ -33,7 +33,8 @@ DIRS = cbmc \
        solver-hardness \
        goto-ld \
        validate-trace-xml-schema \
-			 # Empty last line
+       cbmc-primitives \
+       # Empty last line
 
 ifeq ($(OS),Windows_NT)
     detected_OS := Windows

regression/cbmc-primitives/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)

regression/cbmc-primitives/Makefile

@@ -0,0 +1,18 @@
+default: tests.log
+
+test:
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+
+tests.log: ../test.pl
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/cbmc-primitives/r_w_ok_bug/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p1;
+  __CPROVER_assume(__CPROVER_r_ok(p1 - 1, 1));
+  *p1;
+}

regression/cbmc-primitives/r_w_ok_bug/test.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Crashes during the flattening, issue #5328

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,13 @@
+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 to an out of scope
+variable and __CPROVER_r_ok() can be detected via assert(0). We use
+--no-simplify and --no-propagation to ensure that the case is not solved by the
+constant propagation and thus tests the constraint encoding.

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,13 @@
+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). We use --no-simplify and --no-propagation to ensure that the case is
+not solved by the constant propagation and thus tests the constraint encoding.

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,14 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  // pointer with object bits = 123 and offset = 123
+  // this is to test with a pointer that does not point to valid memory, but the
+  // value of which is otherwise not special in any way (like for example a null
+  // pointer)
+  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,13 @@
+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). We use --no-simplify and --no-propagation to ensure that the case is
+not solved by the constant propagation and thus tests the constraint encoding.

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,13 @@
+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). We use --no-simplify
+and --no-propagation to ensure that the case is not solved by the constant
+propagation and thus tests the constraint encoding.

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,13 @@
+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). We use --no-simplify and
+--no-propagation to ensure that the case is not solved by the constant
+propagation and thus tests the constraint encoding.

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,12 @@
+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. We use --no-simplify
+and --no-propagation to ensure that the case is not solved by the constant
+propagation and thus tests the constraint encoding.

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,13 @@
+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. We use --no-simplify and --no-propagation to ensure that the
+case is not solved by the constant propagation and thus tests the constraint
+encoding.

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,13 @@
+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. We use --no-simplify
+and --no-propagation to ensure that the case is not solved by the constant
+propagation and thus tests the constraint encoding.