CONTRACTS: support slice operators in loop assigns clauses

Changes:
- Drop support for __CPROVER_POINTER_OBJECT
  in assigns clauses in the front-end
- Add methods to havoc __CPROVER_assignable,
  __CPROVER_object_whole, __CPROVER_object_from,
  __CPROVER_object_upto in havoc_assigns_targett.
- update tests
- add new tests

Author: Remi Delmas

regression/contracts-dfcc/assigns_enforce_address_of/test.desc

@@ -3,7 +3,7 @@ main.c
 --dfcc main --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target_list/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_literal/test.desc

@@ -3,7 +3,7 @@ main.c
 --dfcc main --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts-dfcc/assigns_enforce_side_effects_2/test.desc

@@ -3,7 +3,7 @@ main.c
 --dfcc main --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts-dfcc/assigns_enforce_side_effects_3/test.desc

@@ -3,7 +3,7 @@ main.c
 --dfcc main --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts-dfcc/assigns_type_checking_invalid_case_01/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 --
 Checks whether type checking rejects literal constants in assigns clause.

regression/contracts-dfcc/reject_history_expr_in_assigns_clause/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^main.c.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_address_of/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_literal/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_side_effects_2/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_side_effects_3/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_type_checking_invalid_case_01/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 --
 Checks whether type checking rejects literal constants in assigns clause.

regression/contracts/invar_havoc_dynamic_array/main.c

@@ -10,7 +10,7 @@ void main()
 
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
-    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
+    __CPROVER_assigns(i, __CPROVER_object_whole(data))
     __CPROVER_loop_invariant(i <= SIZE)
     // clang-format on
     {

regression/contracts/invar_havoc_static_array/main.c

@@ -10,7 +10,7 @@ void main()
 
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
-    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
+    __CPROVER_assigns(i, __CPROVER_object_whole(data))
     __CPROVER_loop_invariant(i <= SIZE)
     // clang-format on
     {

regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c

@@ -11,7 +11,7 @@ void main()
   data[4][5][6] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
-    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
+    __CPROVER_assigns(i, __CPROVER_object_whole(data))
       __CPROVER_loop_invariant(i <= SIZE)
     {
       data[4][i][6] = 1;

regression/contracts/loop_assigns-01/main.c

@@ -16,7 +16,7 @@ void main()
   b->data[5] = 0;
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
-    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(b->data))
+    __CPROVER_assigns(i, __CPROVER_object_whole(b->data))
     __CPROVER_loop_invariant(i <= SIZE)
     // clang-format on
     {

regression/contracts/loop_assigns-03/main.c

@@ -16,7 +16,7 @@ void main()
   b->data[5] = 0;
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
-    __CPROVER_assigns(__CPROVER_POINTER_OBJECT(b->data))
+    __CPROVER_assigns(__CPROVER_object_whole(b->data))
     __CPROVER_loop_invariant(i <= SIZE)
     // clang-format on
     {

regression/contracts/loop_assigns-04/main.c

@@ -17,7 +17,7 @@ void main()
   b->data[5] = 0;
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
-    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(b->data))
+    __CPROVER_assigns(i, __CPROVER_object_whole(b->data))
     __CPROVER_loop_invariant(i <= SIZE)
     // clang-format on
     {

regression/contracts/loop_assigns-slice-assignable-ptr/main.c

@@ -0,0 +1,42 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 5
+
+struct blob
+{
+  char *data;
+};
+
+void main()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  b->data = malloc(SIZE);
+  b->data[0] = 0;
+  b->data[1] = 1;
+  b->data[2] = 2;
+  b->data[3] = 3;
+  b->data[4] = 4;
+
+  char *start = b->data;
+  char *end = b->data + SIZE;
+
+  for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(i,
+      __CPROVER_object_upto(b->data, SIZE),
+      __CPROVER_typed_target(b->data))
+    __CPROVER_loop_invariant(
+      i <= SIZE &&
+      start <= b->data && b->data < end)
+    // clang-format on
+    {
+      b->data = b->data; // must pass
+      *(b->data) = 0;    // must pass
+    }
+
+  // must pass
+  assert(start <= b->data && b->data <= end);
+  // must fail
+  assert(b->data == start);
+}

regression/contracts/loop_assigns-slice-assignable-ptr/test.desc

@@ -0,0 +1,22 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.\d+\] .* Check that loop instrumentation was not truncated: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is valid: SUCCESS$
+^\[main.assigns.\d+\] .* Check that __CPROVER_object_upto\(\(.*\)b->data, \(.*\)5\) is valid: SUCCESS$
+^\[main.assigns.\d+\] .* Check that __CPROVER_assignable\(\(.*\)&b->data, (4|8).*, TRUE\) is valid: SUCCESS$
+^\[main.assigns.\d+\] .* Check that b->data is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that \*b->data is assignable: SUCCESS$
+^\[main.assertion.\d+\] .* assertion b->data == start: FAILURE$
+^\[main.assertion.\d+\] .* assertion start <= b->data && b->data <= end: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+This test checks that __CPROVER_typed_target(ptr) is supported in loop contracts
+for pointer typed targets and gets translated to
+__CPROVER_assignable(address_of(ptr), sizeof(ptr), TRUE).

regression/contracts/loop_assigns-slice-assignable-scalar/main.c

@@ -0,0 +1,40 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 5
+
+struct blob
+{
+  char *data;
+};
+
+void main()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  b->data = malloc(SIZE);
+  b->data[0] = 0;
+  b->data[1] = 0;
+  b->data[2] = 0;
+  b->data[3] = 0;
+  b->data[4] = 0;
+
+  for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(i, __CPROVER_typed_target(b->data[0]))
+    __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
+    {
+      // must pass
+      b->data[0] = 1;
+      // must fail
+      b->data[i] = 1;
+    }
+
+  // must fail
+  assert(b->data[0] == 0);
+  // must pass
+  assert(b->data[1] == 0);
+  assert(b->data[2] == 0);
+  assert(b->data[3] == 0);
+  assert(b->data[4] == 0);
+}

regression/contracts/loop_assigns-slice-assignable-scalar/test.desc

@@ -0,0 +1,23 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)0\] is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)i\] is assignable: FAILURE$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assigns.\d+\] .* Check that __CPROVER_assignable\(\(.*\)&b->data\[\(.*\)0\], 1ul, FALSE\) is valid: SUCCESS$
+^\[main.assertion.\d+\] .* assertion b->data\[0\] == 0: FAILURE$
+^\[main.assertion.\d+\] .* assertion b->data\[1\] == 0: SUCCESS$
+^\[main.assertion.\d+\] .* assertion b->data\[2\] == 0: SUCCESS$
+^\[main.assertion.\d+\] .* assertion b->data\[3\] == 0: SUCCESS$
+^\[main.assertion.\d+\] .* assertion b->data\[4\] == 0: SUCCESS$
+^VERIFICATION FAILED$
+--
+^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILED$
+--
+This test shows that __CPROVER_typed_target is supported in loop contracts,
+and gets translated to __CPROVER_assignable(&target, sizeof(target), FALSE)
+for scalar targets.

regression/contracts/loop_assigns-slice-from/main.c

@@ -0,0 +1,37 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 5
+
+struct blob
+{
+  char *data;
+};
+
+void main()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  b->data = malloc(SIZE);
+  b->data[0] = 0;
+  b->data[1] = 0;
+  b->data[2] = 0;
+  b->data[3] = 0;
+  b->data[4] = 0;
+
+  for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(i, __CPROVER_object_from(b->data))
+    __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
+    {
+      // must pass
+      b->data[i] = 1;
+    }
+
+  // these should all fail
+  assert(b->data[0] == 0);
+  assert(b->data[1] == 0);
+  assert(b->data[2] == 0);
+  assert(b->data[3] == 0);
+  assert(b->data[4] == 0);
+}

regression/contracts/loop_assigns-slice-from/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.\d+\] .* assertion b->data\[0\] == 0: FAILURE$
+^\[main.assertion.\d+\] .* assertion b->data\[1\] == 0: FAILURE$
+^\[main.assertion.\d+\] .* assertion b->data\[2\] == 0: FAILURE$
+^\[main.assertion.\d+\] .* assertion b->data\[3\] == 0: FAILURE$
+^\[main.assertion.\d+\] .* assertion b->data\[4\] == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$
+--
+This test shows that __CPROVER_object_from is supported in loop contracts.