CONTRACTS: optimize is_fresh separation checks, add ptr predicate uniqueness checks

- Replaces a bool array indexed by object ID by a nondet demonic variable to
track the set of fresh objects and implement separation checks.
- Ensures requires or ensures clause assume/assert at most one predicate
per pointer by tracking locations where these pointers are stored and adding
separation checks on them as well. This is necessary to catch occurences like
`__CPROVER_is_fresh(p, size) && __CPROVER_is_fresh(p, size)` in assume contexts.
- Adds a new type `__CPROVER_contracts_ptr_pred_ctx_t` in `cprover_contracts.c`
to store all contextual information needed to evaluate all pointer predicates.
- 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_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_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.