Merge pull request #6148 from feliperodri/is-fresh

Adds is_fresh predicate for function contracts

Author: feliperodri

regression/contracts/is_unique_01_replace/main.c

@@ -0,0 +1,84 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+bool dummy_for_definitions(int *n)
+{
+  assert(__CPROVER_is_fresh(&n, sizeof(int)));
+  int *x = malloc(sizeof(int));
+}
+
+bool ptr_ok(int *x)
+{
+  return *x < 5;
+}
+
+/*
+	Here are the meanings of the predicates: 
+
+static _Bool __foo_memory_map[__CPROVER_constant_infinity_uint]; 
+
+bool __foo_requires_is_fresh(void **elem, size_t size) {
+	*elem = malloc(size);
+	if (!*elem || (__foo_memory_map[__CPROVER_POINTER_OBJECT(*elem)] != 0)) return false;
+
+	__foo_memory_map[__CPROVER_POINTER_OBJECT(*elem)] = 1;
+	return true;
+}
+
+bool __foo_ensures_is_fresh(void *elem, size_t size) {
+	bool ok = (__foo_memory_map[__CPROVER_POINTER_OBJECT(elem)] == 0 && 
+		  	   __CPROVER_r_ok(elem, size));
+	__foo_memory_map[__CPROVER_POINTER_OBJECT(elem)] = 1;
+	return ok;
+}
+
+
+_Bool __call_foo_requires_is_fresh(void *elem, size_t size) {
+	_Bool r_ok = __CPROVER_r_ok(elem, size);
+	if (!__CPROVER_r_ok(elem, size) || 
+	    __foo_memory_map[__CPROVER_POINTER_OBJECT(elem)]) return 0;
+	__foo_memory_map[__CPROVER_POINTER_OBJECT(elem)] = 1;
+	return 1;
+}
+
+// In the calling context, we assume freshness means new 
+// allocation from within the function.
+bool __call_foo_ensures_is_fresh(void **elem, size_t size) {
+	*elem = malloc(size);
+	return (*elem != NULL);
+}
+*/
+
+bool return_ok(int ret_value, int *x)
+{
+  int a;
+  a = *x;
+  return ret_value == *x + 5;
+}
+
+// The 'ensures' __CPROVER_is_fresh test is unnecessary, but left in just to test the function is working correctly.
+// If you remove the negation, the program will fail, because 'x' is not fresh.
+
+int foo(int *x, int y) __CPROVER_assigns(*x)
+  __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)) && *x > 0 && ptr_ok(x))
+    __CPROVER_ensures(
+      !ptr_ok(x) && !__CPROVER_is_fresh(x, sizeof(int)) &&
+      return_ok(__CPROVER_return_value, x))
+{
+  *x = *x + 4;
+  int y = *x + 5;
+  return *x + 5;
+}
+
+int main()
+{
+  int *n = malloc(sizeof(int));
+  assert(__CPROVER_r_ok(n, sizeof(int)));
+  *n = 3;
+  int o = foo(n, 10);
+  assert(o >= 10 && o == *n + 5);
+  return 0;
+}

regression/contracts/is_unique_01_replace/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function.
+
+Note: For all 'enforce' tests, nothing can be assumed about the return value of the function (as the function call is not replaced at this point).
+
+To make such assumptions would cause verification to fail.

regression/contracts/quantifiers-loop-02/test.desc

@@ -3,9 +3,9 @@ main.c
 --enforce-all-contracts _ --z3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] line .* Check loop invariant before entry: SUCCESS
-^\[main.2\] line .* Check that loop invariant is preserved: SUCCESS
-^\[main.assertion.1\] line .* assertion .*: SUCCESS
+^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS
+^\[main.\d+\] line .* Check that loop invariant is preserved: SUCCESS
+^\[main.assertion.\d+\] line .* assertion .*: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/test_aliasing_enforce/main.c

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

regression/contracts/test_aliasing_enforce/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS
+\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether assuming __CPROVER_is_fresh will guarantee a new freshly
+allocated pointer (no aliasing) for structs.

regression/contracts/test_aliasing_ensure/main.c

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

regression/contracts/test_aliasing_ensure/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS
+\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether ensures(is_fresh()) pass on functions that perform allocation
+directly and return a new object.

regression/contracts/test_aliasing_ensure_indirect/main.c

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

regression/contracts/test_aliasing_ensure_indirect/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[bar.\d+\] line \d+ Check that z is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check compatibility of assigns clause with the called function: SUCCESS
+\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether CBMC propagates freshness correctly across contracts.

regression/contracts/test_aliasing_replace/main.c

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

regression/contracts/test_aliasing_replace/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE
+\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
+^VERIFICATION FAILED$
+--
+--
+Checks whether asserting __CPROVER_is_fresh will guarantee that objects
+mapped to distinct objetcs.

regression/contracts/test_array_memory_enforce/main.c

@@ -0,0 +1,41 @@
+#include <stdbool.h>
+
+bool ptr_ok(int *x)
+{
+  return (*x < 5);
+}
+
+bool return_ok(int ret_value, int *x)
+{
+  int a;
+  a = *x;
+  return (ret_value == *x + 5);
+}
+
+// clang-format off
+int foo(int *x)
+  __CPROVER_assigns(*x)
+  __CPROVER_requires(
+    __CPROVER_is_fresh(x, sizeof(int) * 10) &&
+    x[0] > 0 &&
+    ptr_ok(x))
+  __CPROVER_ensures(
+    !ptr_ok(x) &&
+    !__CPROVER_is_fresh(x, sizeof(int) * 10) && /* `x` is not fresh anymore. */
+    x[9] == 113 &&
+    return_ok(__CPROVER_return_value, x))
+// clang-format on
+{
+  *x = *x + 4;
+  x[5] = 12;
+  x[9] = 113;
+  int y = *x + 5;
+  return *x + 5;
+}
+
+int main()
+{
+  int *n;
+  int o = foo(n);
+  return 0;
+}

regression/contracts/test_array_memory_enforce/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether __CPROVER_is_fresh behaves correctly for arrays both in
+requires and ensures clauses. In the ensures clause, the __CPROVER_is_fresh
+is unnecessary. By negating the predicate in the ensures clause, the test
+proves that `x` is not fresh at end of the function.