CONTRACTS: allow pointer predicates to fail in assume contexts

doc/man/cbmc.1

@@ -334,6 +334,13 @@ set malloc failure mode to return null
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
 .TP
+\fB\-\-dfcc\-debug\-lib\fR
+enable debug assertions in the cprover contracts library
+.TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
+.TP
 \fB\-\-reachability\-slice\fR
 remove instructions that cannot appear on a trace
 from entry point to a property

doc/man/goto-analyzer.1

@@ -585,6 +585,13 @@ set malloc failure mode to return null
 .TP
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
+\fB\-\-dfcc\-debug\-lib\fR
+enable debug assertions in the cprover contracts library
+.TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
+.TP
 .SS "Standard Checks"
 From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
 apply some checks to the program by default (called the "standard checks"), with the

doc/man/goto-instrument.1

@@ -706,6 +706,13 @@ do not allow malloc calls to fail by default
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
 .TP
+\fB\-\-dfcc\-debug\-lib\fR
+enable debug assertions in the cprover contracts library
+.TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
+.TP
 \fB\-\-model\-argc\-argv\fR \fIn\fR
 Create up to \fIn\fR non-deterministic C strings as entries to \fIargv\fR and
 set \fIargc\fR accordingly. In absence of such modelling, \fIargv\fR is left

regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only smt-backend broken-cprover-smt-backend
+FUTURE dfcc-only smt-backend broken-cprover-smt-backend
 main.c
 --dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --z3 --slice-formula --no-standard-checks
 ^EXIT=0$
@@ -7,6 +7,12 @@ main.c
 --
 ^warning: ignoring
 --
+
+Marked as FUTURE because:
+- z3 >v4.12 and up can solve the problem with `--dfcc-simple-invalid-pointer-model`,
+ but the CI uses older versions;
+- bitwuzla >v0.6 can solve the problem but we don't run bitwuzla in CI.
+
 Tests support for quantifiers in loop contracts with the SMT backend.
 When quantified loop invariants are used, they are inserted three times
 in the transformed program (base case assertion, step case assumption,

regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/main.c

@@ -0,0 +1,14 @@
+void foo(int *x)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)) || 1)
+  __CPROVER_assigns(*x)
+// clang-format on
+{
+  *x = 0;
+}
+
+void main()
+{
+  int *x;
+  foo(x);
+}

regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc

@@ -0,0 +1,20 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (FAILURE|UNKNOWN)$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (FAILURE|UNKNOWN)$
+^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: (FAILURE|UNKNOWN)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (FAILURE|UNKNOWN)
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (FAILURE|UNKNOWN)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (FAILURE|UNKNOWN)
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (FAILURE|UNKNOWN)
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (FAILURE|UNKNOWN)
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (FAILURE|UNKNOWN)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when `__CPROVER_is_fresh` is used in disjunctions,
+the program accepts models where `__CPROVER_is_fresh` evaluates to false
+and no object gets allocated, and pointers remain invalid.

regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c

@@ -0,0 +1,30 @@
+#include <stdlib.h>
+void foo(int *x, int *y)
+  // clang-format off
+  __CPROVER_requires(
+    (__CPROVER_is_fresh(x, sizeof(*x)) && y == NULL) ||
+    (x == NULL && __CPROVER_is_fresh(y, sizeof(*y)))
+  )
+  __CPROVER_assigns(y == NULL: *x)
+  __CPROVER_assigns(x == NULL: *y)
+// clang-format on
+{
+  if(y == NULL)
+  {
+    assert(0);
+    *x = 0;
+  }
+  else
+  {
+    assert(0);
+    assert(x == NULL);
+    *y = 0;
+  }
+}
+
+void main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+}

regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc

@@ -0,0 +1,30 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[foo.assertion.\d+\] line 14 assertion 0: FAILURE$
+^\[foo.assigns.\d+\] line 15 Check that \*x is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer NULL in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer invalid in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: dead object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: invalid integer address in \*x: SUCCESS$
+^\[foo.assertion.\d+\] line 19 assertion 0: FAILURE$
+^\[foo.assertion.\d+\] line 20 assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[foo.assigns.\d+\] line 21 Check that \*y is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer NULL in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer invalid in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: dead object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: invalid integer address in \*y: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Illustrates the behaviour of `__CPROVER_is_fresh` under disjunctions in assume contexts.
+The precondition of `foo` describes a disjunction of cases, either `x` is fresh and `y` is null,
+or `x` is null and `y` is fresh. The function `foo` branches on `y == NULL`.
+The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
+that both cases of the disjunction expressed in the requires clause are reachable.

regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/main.c

@@ -0,0 +1,15 @@
+int *foo()
+  // clang-format off
+  __CPROVER_ensures(
+    __CPROVER_is_fresh(__CPROVER_return_value, sizeof(int)) || 1);
+// clang-format on
+
+void bar()
+{
+  int *x = foo();
+  *x = 0; //expected to fail
+}
+void main()
+{
+  bar();
+}

regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc

@@ -0,0 +1,17 @@
+CORE dfcc-only
+main.c
+--dfcc main --replace-call-with-contract foo
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when `__CPROVER_is_fresh` is used in disjunctions,
+the program accepts models where `__CPROVER_is_fresh` evaluates to false
+and no object gets allocated, and pointers remain invalid.

regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/main.c

@@ -0,0 +1,41 @@
+#include <stdlib.h>
+typedef struct
+{
+  int *x;
+  int *y;
+} ret_t;
+
+ret_t foo()
+  // clang-format off
+  __CPROVER_ensures((
+      __CPROVER_is_fresh(__CPROVER_return_value.x, sizeof(int)) &&
+      __CPROVER_return_value.y == NULL
+    ) || (
+      __CPROVER_return_value.x == NULL &&
+      __CPROVER_is_fresh(__CPROVER_return_value.y, sizeof(int))
+    ))
+  // clang-format on
+  ;
+
+void bar()
+{
+  ret_t ret = foo();
+  int *x = ret.x;
+  int *y = ret.y;
+  if(y == NULL)
+  {
+    assert(0);
+    *x = 0;
+  }
+  else
+  {
+    assert(0);
+    assert(x == NULL);
+    *y = 0;
+  }
+}
+
+void main()
+{
+  bar();
+}

regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc

@@ -0,0 +1,30 @@
+CORE dfcc-only
+main.c
+--dfcc main --replace-call-with-contract foo
+^\[bar.assertion.\d+\] line 27 assertion 0: FAILURE$
+^\[bar.assigns.\d+\] line 28 Check that \*x is assignable: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer NULL in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer invalid in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: dead object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: invalid integer address in \*x: SUCCESS$
+^\[bar.assertion.\d+\] line 32 assertion 0: FAILURE$
+^\[bar.assertion.\d+\] line 33 assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[bar.assigns.\d+\] line 34 Check that \*y is assignable: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer NULL in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer invalid in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: dead object in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: invalid integer address in \*y: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Illustrates the behaviour of `__CPROVER_is_fresh` under disjunctions in assume contexts.
+The postcondition of `foo` describes a disjunction of cases: either `x` is fresh and `y` is null,
+or `x` is null and `y` is fresh. The function `bar` branches on `y == NULL`.
+The test succeeds if the two `assert(0)` are falsifiable, which which shows that
+both cases of the disjunction expressed in the ensures clause of `foo` are reachable.

regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c

@@ -0,0 +1,16 @@
+void foo(int *x, int *y)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+  __CPROVER_requires(__CPROVER_pointer_equals(y, x) || 1)
+  __CPROVER_assigns(*y)
+// clang-format on
+{
+  *y = 0;
+}
+
+void main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+}

regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc

@@ -0,0 +1,20 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
+^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: (UNKNOWN|FAILURE)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when `__CPROVER_pointer_equals` is used in disjunctions,
+the program accepts models where `__CPROVER_pointer_equals` evaluates to
+false and the target pointer remains invalid.

regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c

@@ -0,0 +1,34 @@
+#include <stdlib.h>
+void foo(int *a, int *x, int *y)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(a, sizeof(int)))
+  __CPROVER_requires(
+    (__CPROVER_pointer_equals(x,a) && y == NULL) ||
+    (x == NULL && __CPROVER_pointer_equals(y,a))
+  )
+  __CPROVER_assigns(y == NULL: *x)
+  __CPROVER_assigns(x == NULL: *y)
+// clang-format on
+{
+  if(y == NULL)
+  {
+    assert(0);
+    assert(__CPROVER_same_object(a, x));
+    *x = 0;
+  }
+  else
+  {
+    assert(0);
+    assert(x == NULL);
+    assert(__CPROVER_same_object(a, y));
+    *y = 0;
+  }
+}
+
+void main()
+{
+  int *a;
+  int *x;
+  int *y;
+  foo(a, x, y);
+}

regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc

@@ -0,0 +1,32 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[foo.assertion.\d+\] line 15 assertion 0: FAILURE$
+^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$
+^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$
+^\[foo.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts.
+The precondition of `foo` describes a disjunction of cases, either `x` equals `a` and `y` is null,
+or `x` is null and `y` equals `a`. The function `foo` branches on `y == NULL`.
+The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
+that both cases of the disjunction expressed in the requires clause are reachable.