Support for slices in modifies clauses
#2908
Assignees
Labels
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
Milestone
Comments
10 tasks
JustusAdam
added
the
[C] Feature / Enhancement
feliperodri
added a commit
that referenced
this issue
Feb 2, 2024
Extends the function contract functionality with a `modifies` clause. The design is different from #2594 but serves a similar purpose. The `modifies` clause allows the user to specify which parts of a structure a function may assign to. Essentially refining the `mut` annotation. We allow arbitrary (side-effect free) expressions in the `modifies` clause. The expressions are evaluated as part of the preconditions and passed to the function-under-verification as additional arguments. CBMC is then instructed to check that those locations are assigned. Aliasing means that this also adds the location in the original structure to the write set. Each expression must return a pointer to a value that implements `Arbitrary`. On replacement we then simply assign `*ptr = kani::any()`, relying again on aliasing to update the original structure. Additional tests for the new functionality are provided. Resolves #2594 ## Open Questions ### API divergence from CBMC (accepted) The current design goes roughly as follows: We start with a `modifies` annotation on a function ```rs #[modifies(obj.some_expr())] fn target(obj: ...) { ... } ``` And from this we generate code to the effect of (simplified here) ```rs fn target_check(obj: ...) { // Undo the lifetime entanglements let modified_1 = std::mem::transmute::<&'a _, &'b _>(obj.some_expr()); target_wrapper(obj, modified_1); } #[cbmc::assigns(*modified_1)] fn target_wrapper(obj: ..., modified_1: &impl kani::Arbitrary) { ... } ``` Unlike CBMC we expect `obj.some_expr()` to be of a **pointer type** (`*const`, `*mut`, `&mut` or `&`) that points to the object which is target of the modification. So if we had a `t : &mut T` that was modified, CBMC would expect its assigns clause to say `*t`, but we expect `t` (no dereference). The reason is that the code we generate uses the workaround of creating an alias to whichever part of `obj` is modified and registers the alias with CBMC (thereby registering the original also). If we generated code where the right side of `let modified_1 =` is not of pointer type, then the object is moved to the stack and the aliasing destroyed. The open questions is whether we are happy with this change in API. (Yes) ### Test cases when expressions are used in the clause. With more complex expressions in the modifies clause it becomes hard to define good test cases because they reference generated code as in this case: ```rs #[kani::requires(**ptr < 100)] #[kani::modifies(ptr.as_ref())] fn modify(ptr: &mut Box<u32>) { *ptr.as_mut() += 1; } ``` This passes (as it should) and when commenting out the `modifies` clause we get this error: ``` Check 56: modify_wrapper_895c4e.assigns.2 - Status: FAILURE - Description: "Check that *var_2 is assignable" - Location: assigns_expr_pass.rs:8:5 in function modify_wrapper_895c4e ``` The information in this error is very non-specific, hard to read and brittle. How should we define robust "expected" test cases for such errors? ### Corner Cases / Future Improvements - #2907 - #2908 - #2909 ## TODOs - [ ] Test Cases where the clause contains - [x] `Rc` + (`RefCell` or `unsafe`) (see #2907) - [x] Fields - [x] Statement expressions - [x] `Vec` (see #2909) - [ ] Fat pointers - [ ] update contracts documentation - [x] Make sure the wrapper arguments are unique. - [x] Ensure `nondet-static-exclude` always uses the correct filepath (relative or absolute) - [ ] Test case for multiple `modifies` clauses. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
This was referenced Jun 24, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The
modifiesclause currently supports only pointers to a single object. To also support sequences (arrays) it should allow and specially handle slices.The text was updated successfully, but these errors were encountered: