Merge pull request #6049 from feliperodri/fix-contracts-asserts-and-assumes

Properly converts conditions into assertions and assumptions in function contracts

Author: feliperodri

regression/contracts/assigns_enforce_arrays_01/main.c

@@ -4,6 +4,7 @@ void f1(int a[], int len) __CPROVER_assigns(a)
   a = b;
   int *indr = a + 2;
   *indr = 5;
+  a[5] = 2;
 }
 
 int main()

regression/contracts/assigns_enforce_arrays_02/main.c

@@ -8,7 +8,7 @@ int nextIdx() __CPROVER_assigns(idx)
   return idx;
 }
 
-void f1(int a[], int len)
+void f1(int a[], int len) __CPROVER_assigns(*a, idx)
 {
   a[nextIdx()] = 5;
 }

regression/contracts/assigns_enforce_arrays_02/test.desc

@@ -10,3 +10,5 @@ Checks whether the instrumentation process does not duplicate function calls
 used as part of array-index operations, i.e., if a function call is used in
 the computation of the index of an array assignment, then instrumenting that
 statement with an assigns clause will not result in multiple function calls.
+This test also ensures that assigns clauses correctly check for global
+variables modified by subcalls.

regression/contracts/assigns_enforce_arrays_03/test.desc

@@ -6,5 +6,5 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Checks whether verification fails when an array is assigned at an index
-below its lower bound.
+Checks whether verification fails when an assigns clause contains pointer,
+but function only modifies its content.

regression/contracts/assigns_enforce_arrays_05/test.desc

@@ -6,6 +6,6 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Checks whether verification fails when an array is assigned via a
-function call which assigns a pointer to an element out of the
-allowable range.
+Checks whether verification fails when an assigns clause of a function
+indicates the pointer might change, but one of its internal function only
+modified its content.

regression/contracts/assigns_enforce_arrays_10/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int idx = 4;
+
+int nextIdx() __CPROVER_assigns(idx)
+{
+  idx++;
+  return idx;
+}
+
+void f1(int a[], int len) __CPROVER_assigns(*a)
+{
+  a[nextIdx()] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr, 10);
+
+  assert(idx == 5);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_10/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test also ensures that assigns clauses correctly check for global
+variables modified by subcalls. In this case, since the assigns clause
+doesn't include the modified global variable, the verification should failed.

regression/contracts/assigns_enforce_functions_in_contracts/header.h

@@ -0,0 +1,11 @@
+#include "utility.h"
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(int *x) __CPROVER_requires(s2n_result_is_ok(validity3(x)))
+  __CPROVER_assigns(*x) __CPROVER_ensures(
+    __CPROVER_return_value == *x + 5 && s2n_result_is_ok(validity3(x)))
+{
+  *x = *x + 0;
+  return *x + 5;
+}

regression/contracts/assigns_enforce_functions_in_contracts/main.c

@@ -0,0 +1,9 @@
+#include "header.h"
+
+int main()
+{
+  int *n = malloc(sizeof(*n));
+  *n = foo(n);
+
+  return 0;
+}

regression/contracts/assigns_enforce_functions_in_contracts/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks whether verification succeeds when requires and ensures
+contain functions.
+
+Note: We still don't check for function purity, i.e.,
+functions in contracts must only work as predicates.