Merge pull request #6265 from feliperodri/fix-assigns-for-structs

Properly checks struct members in alias expression

Author: feliperodri

doc/cprover-manual/contracts-assigns.md

@@ -114,7 +114,7 @@ Clauses](contracts-requires-and-ensures.md) - Replacement section, and it will a
 non-deterministic assignments for each object listed in the `__CPROVER_assigns`
 clause. Since these objects might be modified by the function, CBMC uses
 non-deterministic assignments to havoc them and restrict their values only by
-assuming the postconditions (i.e., requires clauses).
+assuming the postconditions (i.e., ensures clauses).
 
 In our example, consider that a function `foo` may call `sum`.
 

regression/contracts/assigns_enforce_structs_04/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int y;
+};
+
+void f1(struct pair *p) __CPROVER_assigns(p->x)
+{
+  p->y = 2;
+}
+
+void f2(struct pair *p) __CPROVER_assigns(p->y)
+{
+  p->x = 2;
+}
+
+void f3(struct pair *p) __CPROVER_assigns(p->y)
+{
+  p->y = 0;
+}
+
+void f4(struct pair *p) __CPROVER_assigns(*p)
+{
+  p = NULL;
+}
+
+int main()
+{
+  struct pair p = {0};
+  f1(&p);
+  f2(&p);
+  assert(p.y == 2);
+  assert(p.x == 2);
+  f3(&p);
+  assert(p.y == 0);
+  f4(&p);
+  return 0;
+}

regression/contracts/assigns_enforce_structs_04/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[f1.\d+\] line \d+ Check that p\-\>y is assignable\: FAILURE$
+^\[f2.\d+\] line \d+ Check that p\-\>x is assignable\: FAILURE$
+^\[f3.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
+^\[f4.\d+\] line \d+ Check that p is assignable\: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks whether CBMC properly evaluates write set of members
+from the same object.

regression/contracts/assigns_enforce_structs_05/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+
+struct pair
+{
+  int x[3];
+  int y;
+};
+
+int f1(struct pair *p) __CPROVER_assigns(p->x)
+{
+  p->y = 2;
+  p->x[0] = 0;
+  p->x[1] = 1;
+  p->x[2] = 2;
+  return 0;
+}
+
+int main()
+{
+  struct pair p = {0};
+  f1(&p);
+  assert(p.y == 2);
+  assert(p.x[0] == 0);
+  assert(p.x[1] == 1);
+  assert(p.x[2] == 2);
+  return 0;
+}

regression/contracts/assigns_enforce_structs_05/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[f1.\d+\] line \d+ Check that p\-\>y is assignable\: FAILURE$
+^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)0\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)1\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)2\] is assignable\: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+Checks whether CBMC properly evaluates write set of members
+from the same object. In this case, we have an assigns clause 
+with a struct member `x[3]` and an assignment to the struct member `y`.
+CBMC must considers only the region of `x[3]` is assignable.

regression/contracts/assigns_enforce_structs_06/main.c

@@ -0,0 +1,46 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+struct pair
+{
+  uint8_t *buf;
+  size_t size;
+};
+
+void f1(struct pair *p) __CPROVER_assigns(*(p->buf))
+{
+  p->buf[0] = 0;
+  p->buf[1] = 1;
+  p->buf[2] = 2;
+  p->size = 4;
+}
+
+void f2(struct pair *p) __CPROVER_assigns(p->size)
+{
+  p->buf[0] = 0;
+  p->size = 0;
+}
+
+void f3(struct pair *p) __CPROVER_assigns(*p)
+{
+  p->buf = NULL;
+  p->size = 0;
+}
+
+int main()
+{
+  struct pair *p = malloc(sizeof(*p));
+  p->size = 3;
+  p->buf = malloc(p->size);
+  f1(p);
+  assert(p->buf[0] == 0);
+  assert(p->buf[1] == 1);
+  assert(p->buf[2] == 2);
+  f2(p);
+  assert(p->size == 0);
+  f3(p);
+  assert(p->buf == NULL);
+  assert(p->size == 0);
+  return 0;
+}

regression/contracts/assigns_enforce_structs_06/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)1\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)2\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p\-\>size is assignable\: FAILURE$
+^\[f2.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: FAILURE$
+^\[f2.\d+\] line \d+ Check that p\-\>size is assignable\: SUCCESS$
+^\[f3.\d+\] line \d+ Check that p\-\>buf is assignable\: SUCCESS$
+^\[f3.\d+\] line \d+ Check that p\-\>size is assignable\: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+Checks whether CBMC properly evaluates write set of members
+from the same object. In this case, we have a dynamic object
+as one of the struct members.