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

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.

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_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_in_range_dfcc(x, 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_in_range_fail/test.desc

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

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_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_in_range_dfcc(x, 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_in_range_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_is_fresh_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_is_fresh(y, sizeof(int)) && __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_is_fresh_equals_fail/test.desc

@@ -0,0 +1,10 @@
+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 more than one pointer predicate on the same target pointer triggers a failure.

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_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_is_fresh(y, sizeof(int)) || __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_is_fresh_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_is_fresh_in_range_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_is_fresh(y, sizeof(int)) &&
+  __CPROVER_pointer_in_range_dfcc(x, 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_is_fresh_in_range_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_is_fresh_in_range_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_is_fresh(y, sizeof(int)) ||
+  __CPROVER_pointer_in_range_dfcc(x, 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_is_fresh_in_range_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.