CONTRACTS: demonic encoding for is_fresh separation set, uniqueness of pointer requires/ensures

To reduce array theory usage, use a nondet demonic variable to track the set of fresh objects
and implement separation checks for is fresh (replaces a bool array indexed by object ID).
In the same way, track the set of locations storing pointers that are targets of pointer predicates,
and add assertions to prove that at most one pointer predicate is established per pointer.
This detects and avoids situations where a badly written requires or ensures clause would require
conflicting predicates to hold for a same pointer in a requires or ensures clause.
Adds a new type `__CPROVER_contracts_ptr_pred_ctx_t` and utility functions in `cprover_contracts.c`
to store these new pointer predicate context information used to support pointer predicate evaluation.
Propagate changes to `dfcc_libraryt` and `dfcc_wrapper_programt`.
Add new tests for pointer assumption uniqueness checks
Fix failing tests that used is_fresh under negation in ensures
Update dev doc

Author: Remi Delmas

regression/contracts-dfcc/test_aliasing_ensure/main.c

@@ -1,35 +1,15 @@
-#include <assert.h>
-#include <stdbool.h>
-#include <stdlib.h>
-
-int z;
-
-// clang-format off
-int foo(int *x, int *y)
-  __CPROVER_assigns(z, *x)
-  __CPROVER_requires(
-    __CPROVER_is_fresh(x, sizeof(int)) &&
-    *x > 0 &&
-    *x < 4)
-  __CPROVER_ensures(
-    __CPROVER_is_fresh(y, sizeof(int)) &&
-    !__CPROVER_is_fresh(x, sizeof(int)) &&
-    x != NULL &&
-    x != y &&
-    __CPROVER_return_value == *x + 5)
+int *foo()
+  // clang-format off
+  __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value, sizeof(int)))
 // clang-format on
 {
-  *x = *x + 4;
-  y = malloc(sizeof(*y));
-  *y = *x;
-  z = *y;
-  return (*x + 5);
+  int *ret = malloc(sizeof(int));
+  __CPROVER_assume(ret);
+  return ret;
 }
 
 int main()
 {
-  int n = 4;
-  n = foo(&n, &n);
-  assert(!(n < 4));
+  foo();
   return 0;
 }

regression/contracts-dfcc/test_aliasing_ensure/test.desc

@@ -4,10 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$
-\[foo.assigns.\d+\].*Check that \*x is assignable: SUCCESS
-\[foo.assigns.\d+\].*Check that \*y is assignable: SUCCESS
-\[foo.assigns.\d+\].*Check that z is assignable: SUCCESS
-\[main.assertion.\d+\].*assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c

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

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c

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

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc

@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that a same pointer can be the target of multiple pointer predicates as
+long as they do not apply at the same time.

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c

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

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Tests that assuming the more than one pointer predicate on the same target pointer
+at the same time triggers a failure.

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c

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

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc

@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that more than one predicate can be assumed on a same target as long at
+they don't hold at the same time.