Merge pull request #6814 from remi-delmas-3000/contracts-object-slice

feliperodri · web-flow · commit 098898c4984f · 2022-04-25T13:24:23.000-04:00
CONTRACTS: Support object slices in assigns clauses
diff --git a/doc/cprover-manual/contracts-assigns.md b/doc/cprover-manual/contracts-assigns.md
@@ -13,6 +13,30 @@ design is based on the former. This means that memory not captured by an
 _assigns_ clause must not be written within the given function, even if the
 value(s) therein are not modified.
 
+### Object slice expressions
+
+The following functions can be used in assigns clause to specify ranges of 
+assignable addresses.
+
+Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_from(ptr)` 
+specifies that all bytes starting from the given pointer and until the end of 
+the object are assignable:
+```c
+__CPROVER_size_t __CPROVER_object_from(void *ptr); 
+```
+
+Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_from(ptr, size)` 
+specifies that `size` bytes starting from the given pointer and until the end of the object are assignable.
+The `size` value must such that `size <= __CPROVER_object_size(ptr) - __CPROVER_pointer_offset(ptr)` holds:
+
+```c
+__CPROVER_size_t __CPROVER_object_slice(void *ptr, __CPROVER_size_t size);
+```
+
+Caveats and limitations: The slices in question must *not*
+be interpreted as pointers by the program. During call-by-contract replacement, 
+`__CPROVER_havoc_slice(ptr, size)` is used to havoc these targets, 
+and `__CPROVER_havoc_slice` does not support havocing pointers. 
 ### Parameters
 
 An _assigns_ clause currently supports simple variable types and their pointers,
diff --git a/regression/contracts/assigns-slice-targets/main-enforce.c b/regression/contracts/assigns-slice-targets/main-enforce.c
@@ -0,0 +1,53 @@
+struct st
+{
+  int a;
+  char arr1[10];
+  int b;
+  char arr2[10];
+  int c;
+};
+
+void foo(struct st *s)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s)))
+  __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5))
+  __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5))
+// clang-format on
+{
+  // PASS
+  s->arr1[0] = 0;
+  s->arr1[1] = 0;
+  s->arr1[2] = 0;
+  s->arr1[3] = 0;
+  s->arr1[4] = 0;
+
+  // FAIL
+  s->arr1[5] = 0;
+  s->arr1[6] = 0;
+  s->arr1[7] = 0;
+  s->arr1[8] = 0;
+  s->arr1[9] = 0;
+
+  // FAIL
+  s->arr2[0] = 0;
+  s->arr2[1] = 0;
+  s->arr2[2] = 0;
+  s->arr2[3] = 0;
+  s->arr2[4] = 0;
+
+  // PASS
+  s->arr2[5] = 0;
+  s->arr2[6] = 0;
+  s->arr2[7] = 0;
+  s->arr2[8] = 0;
+  s->arr2[9] = 0;
+}
+
+int main()
+{
+  struct st s;
+
+  foo(&s);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns-slice-targets/main-replace.c b/regression/contracts/assigns-slice-targets/main-replace.c
@@ -0,0 +1,96 @@
+struct st
+{
+  int a;
+  char arr1[10];
+  int b;
+  char arr2[10];
+  int c;
+};
+
+void foo(struct st *s)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s)))
+  __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5))
+  __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5))
+// clang-format on
+{
+  s->arr1[0] = 0;
+  s->arr1[1] = 0;
+  s->arr1[2] = 0;
+  s->arr1[3] = 0;
+  s->arr1[4] = 0;
+
+  s->arr2[5] = 0;
+  s->arr2[6] = 0;
+  s->arr2[7] = 0;
+  s->arr2[8] = 0;
+  s->arr2[9] = 0;
+}
+
+int main()
+{
+  struct st s;
+  s.a = 0;
+  s.arr1[0] = 0;
+  s.arr1[1] = 0;
+  s.arr1[2] = 0;
+  s.arr1[3] = 0;
+  s.arr1[4] = 0;
+  s.arr1[5] = 0;
+  s.arr1[6] = 0;
+  s.arr1[7] = 0;
+  s.arr1[8] = 0;
+  s.arr1[9] = 0;
+
+  s.arr2[0] = 0;
+  s.arr2[1] = 0;
+  s.arr2[2] = 0;
+  s.arr2[3] = 0;
+  s.arr2[4] = 0;
+  s.arr2[5] = 0;
+  s.arr2[6] = 0;
+  s.arr2[7] = 0;
+  s.arr2[8] = 0;
+  s.arr2[9] = 0;
+  s.c = 0;
+
+  foo(&s);
+
+  // PASS
+  assert(s.a == 0);
+
+  // FAIL
+  assert(s.arr1[0] == 0);
+  assert(s.arr1[1] == 0);
+  assert(s.arr1[2] == 0);
+  assert(s.arr1[3] == 0);
+  assert(s.arr1[4] == 0);
+
+  // PASS
+  assert(s.arr1[5] == 0);
+  assert(s.arr1[6] == 0);
+  assert(s.arr1[7] == 0);
+  assert(s.arr1[8] == 0);
+  assert(s.arr1[9] == 0);
+
+  // PASS
+  assert(s.b == 0);
+
+  // PASS
+  assert(s.arr2[0] == 0);
+  assert(s.arr2[1] == 0);
+  assert(s.arr2[2] == 0);
+  assert(s.arr2[3] == 0);
+  assert(s.arr2[4] == 0);
+
+  // FAIL
+  assert(s.arr2[5] == 0);
+  assert(s.arr2[6] == 0);
+  assert(s.arr2[7] == 0);
+  assert(s.arr2[8] == 0);
+  assert(s.arr2[9] == 0);
+
+  // PASS
+  assert(s.c == 0);
+  return 0;
+}
diff --git a/regression/contracts/assigns-slice-targets/test-enforce.desc b/regression/contracts/assigns-slice-targets/test-enforce.desc
@@ -0,0 +1,32 @@
+CORE
+main-enforce.c
+--enforce-contract foo
+^\[foo.assigns.\d+\].* Check that __CPROVER_object_slice\(\(void \*\)s->arr1, \(.*\)5\) is valid: SUCCESS$
+^\[foo.assigns.\d+\].* Check that __CPROVER_object_from\(\(void \*\)\(s->arr2 \+ \(.*\)5\)\) is valid: SUCCESS$
+^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)3\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)4\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)5\] is assignable: FAILURE$
+^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)6\] is assignable: FAILURE$
+^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)7\] is assignable: FAILURE$
+^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)8\] is assignable: FAILURE$
+^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)9\] is assignable: FAILURE$
+^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)0\] is assignable: FAILURE$
+^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)1\] is assignable: FAILURE$
+^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)2\] is assignable: FAILURE$
+^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)3\] is assignable: FAILURE$
+^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)4\] is assignable: FAILURE$
+^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)5\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)6\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that assigns clause checking of slice expressions works as expected when 
+enforcing a contract.
diff --git a/regression/contracts/assigns-slice-targets/test-replace.desc b/regression/contracts/assigns-slice-targets/test-replace.desc
@@ -0,0 +1,34 @@
+CORE
+main-replace.c
+--replace-call-with-contract foo
+^\[main.assertion.\d+\].*assertion s.a == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)0\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)1\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)2\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)3\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)4\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)5\] == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)6\] == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)7\] == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)8\] == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)9\] == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion s.b == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)0\] == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)1\] == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)2\] == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)3\] == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)4\] == 0: SUCCESS$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)5\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)6\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)7\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)8\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)9\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion s.c == 0: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that havocking of slice expressions works as expected when 
+replacing a call by a contract. We manually express frame conditions as 
+assertions in the main function.
diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/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 an lvalue or __CPROVER_POINTER_OBJECT expression$
+^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc b/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 an lvalue or __CPROVER_POINTER_OBJECT expression$
+^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc b/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 an lvalue or __CPROVER_POINTER_OBJECT expression$
+^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc
@@ -3,8 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
-^.*error: side-effects not allowed in assigns clause targets$
+^.*error: function calls in assigns clause targets must be to __CPROVER_object_from, __CPROVER_object_slice$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/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 an lvalue or __CPROVER_POINTER_OBJECT expression$
+^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_1/test.desc b/regression/contracts/assigns_enforce_side_effects_1/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --enforce-contract foo
 activate-multi-line-match
-.*error: (dereferencing void pointer|void-typed expressions not allowed as assigns clause targets\n.*\n.*error: side-effects not allowed in assigns clause targets\n.*\n.*error: ternary expressions not allowed in assigns clause targets\n)
+.*error: (dereferencing void pointer|void-typed expressions not allowed as assigns clause targets)
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc
@@ -3,8 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
-^.*error: side-effects not allowed in assigns clause targets$
+^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc
@@ -3,8 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
-^.*error: side-effects not allowed in assigns clause targets$
+^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc b/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 an lvalue or __CPROVER_POINTER_OBJECT expression$
+^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
 --
 Checks whether type checking rejects literal constants in assigns clause.
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h
diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp
diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h
diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.h b/src/goto-instrument/contracts/instrument_spec_assigns.h
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
