Adds regression test to cover code contracts support

feliperodri · feliperodri · commit eafdbc0eb6e5 · 2021-03-23T22:17:23.000-04:00
Code contracts now supports assigns clause with structs and array ranges.
It also supports contracts specified across multiple source files.
So, we added regression tests to cover these capabilites.

Signed-off-by: Felipe R. Monteiro &lt;felisous@amazon.com&gt;
diff --git a/regression/contracts/assigns_enforce_arrays_01/main.c b/regression/contracts/assigns_enforce_arrays_01/main.c
@@ -0,0 +1,15 @@
+void f1(int a[], int len) __CPROVER_assigns(a)
+{
+  int b[10];
+  a = b;
+  int *indr = a + 2;
+  *indr = 5;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_01/test.desc b/regression/contracts/assigns_enforce_arrays_01/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks their assigns clause behavior when it reasons (indirectly)
+over a freshly-allocated variable.
diff --git a/regression/contracts/assigns_enforce_arrays_02/main.c b/regression/contracts/assigns_enforce_arrays_02/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)
+{
+  a[nextIdx()] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr, 10);
+
+  assert(idx == 5);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_02/test.desc b/regression/contracts/assigns_enforce_arrays_02/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+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.
diff --git a/regression/contracts/assigns_enforce_arrays_03/main.c b/regression/contracts/assigns_enforce_arrays_03/main.c
@@ -0,0 +1,12 @@
+void assign_out_under(int a[], int len) __CPROVER_assigns(a)
+{
+  a[1] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  assign_out_under(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_03/test.desc b/regression/contracts/assigns_enforce_arrays_03/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned at an index
+below its lower bound.
diff --git a/regression/contracts/assigns_enforce_arrays_04/main.c b/regression/contracts/assigns_enforce_arrays_04/main.c
@@ -0,0 +1,21 @@
+void assigns_single(int a[], int len) __CPROVER_assigns(a)
+{
+}
+
+void assigns_range(int a[], int len) __CPROVER_assigns(a)
+{
+}
+
+void assigns_big_range(int a[], int len) __CPROVER_assigns(a)
+{
+  assigns_single(a, len);
+  assigns_range(a, len);
+}
+
+int main()
+{
+  int arr[10];
+  assigns_big_range(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_04/test.desc b/regression/contracts/assigns_enforce_arrays_04/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when an array is assigned through
+calls to functions with array assigns clauses which are compatible with
+that of the caller.
diff --git a/regression/contracts/assigns_enforce_arrays_05/main.c b/regression/contracts/assigns_enforce_arrays_05/main.c
@@ -0,0 +1,18 @@
+void assigns_ptr(int *x) __CPROVER_assigns(*x)
+{
+  *x = 200;
+}
+
+void assigns_range(int a[], int len) __CPROVER_assigns(a)
+{
+  int *ptr = &(a[7]);
+  assigns_ptr(ptr);
+}
+
+int main()
+{
+  int arr[10];
+  assigns_range(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^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.
diff --git a/regression/contracts/assigns_enforce_multi_file_01/header.h b/regression/contracts/assigns_enforce_multi_file_01/header.h
@@ -0,0 +1,22 @@
+void f1(int *x1, int *y1, int *z1);
+
+void f2(int *x2, int *y2, int *z2);
+
+void f3(int *x3, int *y3, int *z3);
+
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3)
+{
+  *x3 = *x3 + 1;
+  *y3 = *y3 + 1;
+  *z3 = *z3 + 1;
+}
diff --git a/regression/contracts/assigns_enforce_multi_file_01/main.c b/regression/contracts/assigns_enforce_multi_file_01/main.c
@@ -0,0 +1,11 @@
+#include "header.h"
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f1(&p, &q, &r);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_multi_file_01/test.desc b/regression/contracts/assigns_enforce_multi_file_01/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test replicates the behavior of assigns_enforce_04, but separates
+the function headers and contracts into a separate file header.h.
diff --git a/regression/contracts/assigns_enforce_multi_file_02/header.h b/regression/contracts/assigns_enforce_multi_file_02/header.h
@@ -0,0 +1,23 @@
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int y;
+};
+
+struct pair_of_pairs
+{
+  struct pair p1;
+  struct pair p2;
+};
+
+int f1(int *a, struct pair *b);
+
+int f1(int *a, struct pair *b) __CPROVER_assigns(*a)
+{
+  struct pair_of_pairs *pop =
+    (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));
+  b = &(pop->p2);
+  b->y = 5;
+}
diff --git a/regression/contracts/assigns_enforce_multi_file_02/main.c b/regression/contracts/assigns_enforce_multi_file_02/main.c
@@ -0,0 +1,10 @@
+#include "header.h"
+
+int main()
+{
+  int m = 4;
+  struct pair n;
+  f1(&m, &n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_multi_file_02/test.desc b/regression/contracts/assigns_enforce_multi_file_02/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test replicates the behavior of assigns_enforce_structs_03, but separates
+the structs, function headers, and contracts into a separate file header.h.
diff --git a/regression/contracts/assigns_enforce_structs_01/main.c b/regression/contracts/assigns_enforce_structs_01/main.c
@@ -0,0 +1,23 @@
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int y;
+};
+
+int f1(int *a, int *b) __CPROVER_assigns(*a)
+{
+  struct pair *p = (struct pair *)malloc(sizeof(struct pair));
+  b = &(p->y);
+  *b = 5;
+}
+
+int main()
+{
+  int m = 4;
+  int n = 3;
+  f1(&m, &n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_structs_01/test.desc b/regression/contracts/assigns_enforce_structs_01/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when a formal parameter pointer outside
+of the assigns clause is instead pointed at the location of a member of a
+freshly allocated struct before being assigned.
diff --git a/regression/contracts/assigns_enforce_structs_02/main.c b/regression/contracts/assigns_enforce_structs_02/main.c
@@ -0,0 +1,30 @@
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int y;
+};
+
+struct pair_of_pairs
+{
+  struct pair p1;
+  struct pair p2;
+};
+
+int f1(int *a, int *b) __CPROVER_assigns(*a)
+{
+  struct pair_of_pairs *pop =
+    (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));
+  b = &(pop->p2.x);
+  *b = 5;
+}
+
+int main()
+{
+  int m = 4;
+  int n = 3;
+  f1(&m, &n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_structs_02/test.desc b/regression/contracts/assigns_enforce_structs_02/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when a formal parameter pointer outside
+of the assigns clause is assigned after being pointed at the location of a
+member of a sub-struct of a freshly allocated struct before being assigned.
+This is meant to show that all contained members (and their contained members)
+of assignable structs are valid to assign.
diff --git a/regression/contracts/assigns_enforce_structs_03/main.c b/regression/contracts/assigns_enforce_structs_03/main.c
@@ -0,0 +1,30 @@
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int y;
+};
+
+struct pair_of_pairs
+{
+  struct pair p1;
+  struct pair p2;
+};
+
+int f1(int *a, struct pair *b) __CPROVER_assigns(*a)
+{
+  struct pair_of_pairs *pop =
+    (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));
+  b = &(pop->p2);
+  b->y = 5;
+}
+
+int main()
+{
+  int m = 4;
+  struct pair n;
+  f1(&m, &n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_structs_03/test.desc b/regression/contracts/assigns_enforce_structs_03/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when a member of formal parameter
+(with type of pointer to struct) outside of the assigns clause is assigned
+after being pointed at the location of a member sub-struct of a freshly
+allocated struct before being assigned. This is meant to show that all
+contained members (and their contained members) of assignable structs
+are valid to assign.
diff --git a/regression/contracts/assigns_replace_06/main.c b/regression/contracts/assigns_replace_06/main.c
diff --git a/regression/contracts/assigns_replace_06/test.desc b/regression/contracts/assigns_replace_06/test.desc
diff --git a/regression/contracts/assigns_replace_07/main.c b/regression/contracts/assigns_replace_07/main.c
diff --git a/regression/contracts/assigns_replace_07/test.desc b/regression/contracts/assigns_replace_07/test.desc
diff --git a/regression/contracts/function-calls-02-1/test-enf.desc b/regression/contracts/function-calls-02-1/test-enf.desc
diff --git a/regression/contracts/function-calls-02/test-enf.desc b/regression/contracts/function-calls-02/test-enf.desc
diff --git a/regression/contracts/function-calls-03/test-enf.desc b/regression/contracts/function-calls-03/test-enf.desc
diff --git a/regression/contracts/function-calls-04/test-enf.desc b/regression/contracts/function-calls-04/test-enf.desc
diff --git a/regression/contracts/function-calls-04/test-mix-2.desc b/regression/contracts/function-calls-04/test-mix-2.desc
