Merge pull request #6216 from feliperodri/assigns-clause-type-checking

Improves type checking for __CPROVER_assigns clauses

Author: feliperodri

regression/contracts/assigns_function_pointer/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stddef.h>
+
+int x = 0;
+
+void foo()
+{
+  x = 1;
+}
+
+void bar(void (*fun_ptr)()) __CPROVER_assigns(fun_ptr)
+{
+  fun_ptr = &foo;
+}
+
+int main()
+{
+  assert(x == 0);
+  void (*fun_ptr)() = NULL;
+  bar(fun_ptr);
+  fun_ptr();
+  assert(x == 1);
+  return 0;
+}

regression/contracts/assigns_function_pointer/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[bar.1\] line \d+ Check that fun\_ptr is assignable: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion x \=\= 1: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+Checks whether assigns clause accepts function pointers.

regression/contracts/assigns_replace_07/test.desc

@@ -0,0 +1,11 @@
+void foo(int a) __CPROVER_assigns(0)
+{
+  a = 0;
+}
+
+int main()
+{
+  int n;
+  foo(n);
+  return 0;
+}

regression/contracts/assigns_type_checking_invalid_case_01/main.c

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=(1|64)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+error: illegal target in assigns clause
+--
+Checks whether type checking reports illegal target in assigns clause.

regression/contracts/assigns_type_checking_invalid_case_01/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=(1|64)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+error: illegal target in assigns clause
+--
+--
+Checks whether parser fails for a single-index array assigns target.

regression/contracts/assigns_replace_07/main.c renamed to regression/contracts/assigns_type_checking_invalid_case_02/main.c

@@ -0,0 +1,102 @@
+#include <stdlib.h>
+
+int *x;
+int y;
+
+struct buf
+{
+  int *data;
+  size_t len;
+};
+
+void foo1(int a) __CPROVER_assigns(a)
+{
+  a = 0;
+}
+
+void foo2(int *b) __CPROVER_assigns(b)
+{
+  b = NULL;
+}
+
+void foo3(int a, int *b) __CPROVER_assigns(b, x, y)
+{
+  b = NULL;
+  x = malloc(sizeof(*x));
+  y = 0;
+}
+
+void foo4(int a, int *b, int *c) __CPROVER_requires(c != NULL)
+  __CPROVER_requires(x != NULL) __CPROVER_assigns(b, *c, *x)
+{
+  b = NULL;
+  *c = 0;
+  *x = 0;
+}
+
+void foo5(struct buf buffer) __CPROVER_assigns(buffer)
+{
+  buffer.data = NULL;
+  buffer.len = 0;
+}
+
+void foo6(struct buf *buffer)
+  __CPROVER_assigns(buffer->data, *(buffer->data), buffer->len)
+{
+  buffer->data = malloc(sizeof(*(buffer->data)));
+  *(buffer->data) = 1;
+  buffer->len = 1;
+}
+
+void foo7(int a, struct buf *buffer) __CPROVER_assigns(*buffer)
+{
+  buffer->data = malloc(sizeof(*(buffer->data)));
+  *(buffer->data) = 1;
+  buffer->len = 1;
+}
+
+void foo8(int array[]) __CPROVER_assigns(*array)
+{
+  array[0] = 1;
+  array[1] = 1;
+  array[2] = 1;
+  array[3] = 1;
+  array[4] = 1;
+  array[5] = 1;
+  array[6] = 1;
+  array[7] = 1;
+  array[8] = 1;
+  array[9] = 1;
+}
+
+void foo9(int array[]) __CPROVER_assigns(array)
+{
+  int *new_array = NULL;
+  array = new_array;
+}
+
+void foo10(struct buf *buffer) __CPROVER_requires(buffer != NULL)
+  __CPROVER_assigns(*buffer)
+{
+  buffer->len = 0;
+}
+
+int main()
+{
+  int n;
+  int *m;
+  int *o = malloc(sizeof(*o));
+  struct buf buffer;
+  int array_call[10] = {0};
+  foo1(n);
+  foo2(&n);
+  foo3(n, m);
+  foo4(n, m, o);
+  foo5(buffer);
+  foo6(&buffer);
+  foo7(n, &buffer);
+  foo8(array_call);
+  foo9(array_call);
+  foo10(&buffer);
+  return 0;
+}

regression/contracts/assigns_type_checking_invalid_case_02/test.desc

@@ -0,0 +1,34 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[foo1.\d+\] line \d+ Check that a is assignable: SUCCESS$
+^\[foo10.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
+^\[foo2.\d+\] line \d+ Check that b is assignable: SUCCESS$
+^\[foo3.\d+\] line \d+ Check that b is assignable: SUCCESS$
+^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$
+^\[foo4.\d+\] line \d+ Check that b is assignable: SUCCESS$
+^\[foo4.\d+\] line \d+ Check that \*c is assignable: SUCCESS$
+^\[foo4.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo5.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$
+^\[foo5.\d+\] line \d+ Check that buffer.len is assignable: SUCCESS$
+^\[foo6.\d+\] line \d+ Check that \*buffer\-\>data is assignable: SUCCESS$
+^\[foo6.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
+^\[foo7.\d+\] line \d+ Check that \*buffer\-\>data is assignable: SUCCESS$
+^\[foo7.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
+^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$
+^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$
+^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$
+^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)3\] is assignable: SUCCESS$
+^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)4\] is assignable: SUCCESS$
+^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)5\] is assignable: SUCCESS$
+^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)6\] is assignable: SUCCESS$
+^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$
+^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$
+^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$
+^\[foo9.\d+\] line \d+ Check that new_array is assignable: SUCCESS$
+^\[foo9.\d+\] line \d+ Check that array is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+Checks whether CBMC parses correctly all standard cases for assigns clauses.

regression/contracts/assigns_type_checking_valid_cases/main.c

@@ -253,6 +253,18 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     const exprt &as_expr =
       static_cast<const exprt &>(static_cast<const irept &>(type));
     assigns = to_unary_expr(as_expr).op();
+
+    for(const exprt &operand : assigns.operands())
+    {
+      if(
+        operand.id() != ID_symbol && operand.id() != ID_ptrmember &&
+        operand.id() != ID_dereference)
+      {
+        error().source_location = source_location;
+        error() << "illegal target in assigns clause" << eom;
+        throw 0;
+      }
+    }
   }
   else if(type.id() == ID_C_spec_ensures)
   {