CONTRACTS: at most one predicate occurence per pointer

Remi Delmas · Remi Delmas · commit a23bcae5da7d · 2025-01-25T16:49:35.000-05:00
This fixes the problem that
`is_fresh(p, n) &amp;&amp; is_fresh(p, n)` would
fail in assertion contexts but pass in
assumption contexts by allocating twice.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc b/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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc b/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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc b/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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc b/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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/test.desc b/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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc b/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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc b/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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc b/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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc b/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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc b/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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c
@@ -0,0 +1,17 @@
+void foo(int *x)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(x, sizeof(int)) && __CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_assigns(*x)
+__CPROVER_ensures(*x == 0)
+// clang-format on
+{
+  *x = 0;
+}
+
+int main()
+{
+  int *x;
+  foo(x);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc
@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh 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.
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c
@@ -0,0 +1,17 @@
+void foo(int *x)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(x, sizeof(int)) || __CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_assigns(*x)
+__CPROVER_ensures(*x == 0)
+// clang-format on
+{
+  *x = 0;
+}
+
+int main()
+{
+  int *x;
+  foo(x);
+  return 0;
+}
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc
@@ -0,0 +1,14 @@
+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.
+- `x` is fresh and inialized to 0
+- `y` is equal to `x`if select is true, or fresh otherwise
+- foo assigns y to 1
+- x is equal to 1 if select is true, 0 otherwise
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/main.c
diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/test.desc
diff --git a/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/main.c
diff --git a/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/test.desc
diff --git a/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c
diff --git a/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc
diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c
