diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 25e769ce941..449853577ad 100644 --- a/regression/CMakeLists.txt +++ b/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) diff --git a/regression/Makefile b/regression/Makefile index ab47a8c4917..9e067b7dcf5 100644 --- a/regression/Makefile +++ b/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 diff --git a/regression/cbmc-primitives/CMakeLists.txt b/regression/cbmc-primitives/CMakeLists.txt new file mode 100644 index 00000000000..93d5ee716c2 --- /dev/null +++ b/regression/cbmc-primitives/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "$" +) diff --git a/regression/cbmc-primitives/Makefile b/regression/cbmc-primitives/Makefile new file mode 100644 index 00000000000..1b66f1b4124 --- /dev/null +++ b/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 diff --git a/regression/cbmc-primitives/r_w_ok_bug/main.c b/regression/cbmc-primitives/r_w_ok_bug/main.c new file mode 100644 index 00000000000..427099252e0 --- /dev/null +++ b/regression/cbmc-primitives/r_w_ok_bug/main.c @@ -0,0 +1,9 @@ +#include +#include + +void main() +{ + char *p1; + __CPROVER_assume(__CPROVER_r_ok(p1 - 1, 1)); + *p1; +} diff --git a/regression/cbmc-primitives/r_w_ok_bug/test.desc b/regression/cbmc-primitives/r_w_ok_bug/test.desc new file mode 100644 index 00000000000..2c6ff3474be --- /dev/null +++ b/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 diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_dead/main.c b/regression/cbmc-primitives/r_w_ok_inconsistent_dead/main.c new file mode 100644 index 00000000000..9fdd473329d --- /dev/null +++ b/regression/cbmc-primitives/r_w_ok_inconsistent_dead/main.c @@ -0,0 +1,16 @@ +#include +#include + +void main() +{ + char *p; + + { + char c; + p = &c; + } + + __CPROVER_assume(__CPROVER_r_ok(p, 1)); + assert(0); // fails + *p; // succeeds +} diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_dead/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_dead/test-no-cp.desc new file mode 100644 index 00000000000..0407f905f4d --- /dev/null +++ b/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. diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_dead/test.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_dead/test.desc new file mode 100644 index 00000000000..3393497c08d --- /dev/null +++ b/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). diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/main.c b/regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/main.c new file mode 100644 index 00000000000..45b934c80a7 --- /dev/null +++ b/regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/main.c @@ -0,0 +1,12 @@ +#include +#include + +void main() +{ + char *p = malloc(1); + free(p); + + __CPROVER_assume(__CPROVER_r_ok(p, 1)); + assert(0); // fails + *p; // succeeds +} diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/test-no-cp.desc new file mode 100644 index 00000000000..98ce59cbf3e --- /dev/null +++ b/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. diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/test.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/test.desc new file mode 100644 index 00000000000..041ac2e31d9 --- /dev/null +++ b/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). diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_integer/main.c b/regression/cbmc-primitives/r_w_ok_inconsistent_integer/main.c new file mode 100644 index 00000000000..88e025bf728 --- /dev/null +++ b/regression/cbmc-primitives/r_w_ok_inconsistent_integer/main.c @@ -0,0 +1,14 @@ +#include +#include + +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 +} diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test-no-cp.desc new file mode 100644 index 00000000000..98ce59cbf3e --- /dev/null +++ b/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. diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test.desc new file mode 100644 index 00000000000..041ac2e31d9 --- /dev/null +++ b/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). diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/main.c b/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/main.c new file mode 100644 index 00000000000..a4370b40faa --- /dev/null +++ b/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/main.c @@ -0,0 +1,12 @@ +#include +#include + +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 +} diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc new file mode 100644 index 00000000000..ada56588c85 --- /dev/null +++ b/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. diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc new file mode 100644 index 00000000000..2b2871e6642 --- /dev/null +++ b/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). diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/main.c b/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/main.c new file mode 100644 index 00000000000..b5516f5fe81 --- /dev/null +++ b/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/main.c @@ -0,0 +1,11 @@ +#include + +char *nondet(); + +void main() +{ + char *p = nondet(); + __CPROVER_assume(__CPROVER_r_ok(p, 10)); + assert(0); // fails + *p; // succeeds +} diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test-no-cp.desc new file mode 100644 index 00000000000..2f9ebc57929 --- /dev/null +++ b/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. diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test.desc new file mode 100644 index 00000000000..34641ac0acf --- /dev/null +++ b/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). diff --git a/regression/cbmc-primitives/r_w_ok_null/main.c b/regression/cbmc-primitives/r_w_ok_null/main.c new file mode 100644 index 00000000000..2e7d93e47c8 --- /dev/null +++ b/regression/cbmc-primitives/r_w_ok_null/main.c @@ -0,0 +1,8 @@ +#include +#include + +void main() +{ + char *p = NULL; + assert(!__CPROVER_r_ok(p, 10)); +} diff --git a/regression/cbmc-primitives/r_w_ok_null/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_null/test-no-cp.desc new file mode 100644 index 00000000000..2e9f6335203 --- /dev/null +++ b/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. diff --git a/regression/cbmc-primitives/r_w_ok_null/test.desc b/regression/cbmc-primitives/r_w_ok_null/test.desc new file mode 100644 index 00000000000..1823876a8c0 --- /dev/null +++ b/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 diff --git a/regression/cbmc-primitives/r_w_ok_valid/main.c b/regression/cbmc-primitives/r_w_ok_valid/main.c new file mode 100644 index 00000000000..e6ee04d5e33 --- /dev/null +++ b/regression/cbmc-primitives/r_w_ok_valid/main.c @@ -0,0 +1,19 @@ +#include +#include + +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)); +} diff --git a/regression/cbmc-primitives/r_w_ok_valid/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_valid/test-no-cp.desc new file mode 100644 index 00000000000..63d28ba42a1 --- /dev/null +++ b/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. diff --git a/regression/cbmc-primitives/r_w_ok_valid/test.desc b/regression/cbmc-primitives/r_w_ok_valid/test.desc new file mode 100644 index 00000000000..328c947b45c --- /dev/null +++ b/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 diff --git a/regression/cbmc-primitives/r_w_ok_valid_negated/main.c b/regression/cbmc-primitives/r_w_ok_valid_negated/main.c new file mode 100644 index 00000000000..3f86f1959fb --- /dev/null +++ b/regression/cbmc-primitives/r_w_ok_valid_negated/main.c @@ -0,0 +1,34 @@ +#include +#include + +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)); +} diff --git a/regression/cbmc-primitives/r_w_ok_valid_negated/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_valid_negated/test-no-cp.desc new file mode 100644 index 00000000000..58f78097780 --- /dev/null +++ b/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. diff --git a/regression/cbmc-primitives/r_w_ok_valid_negated/test.desc b/regression/cbmc-primitives/r_w_ok_valid_negated/test.desc new file mode 100644 index 00000000000..c3047928dc7 --- /dev/null +++ b/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.