Adds regression test to cover code contracts support

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 <[email protected]>

Author: feliperodri

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;
+}

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.

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;
+}

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.

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;
+}

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.

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;
+}

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.

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;
+}

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.

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;
+}

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;
+}

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.

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;
+}

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;
+}

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.

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;
+}

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.

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;
+}

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.

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;
+}

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.