Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

modifies Clauses for Function Contracts #2800

Merged
merged 80 commits into from
Feb 2, 2024

Conversation

JustusAdam
Copy link
Contributor

@JustusAdam JustusAdam commented Oct 2, 2023

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

#[modifies(obj.some_expr())]
fn target(obj: ...) { ... }

And from this we generate code to the effect of (simplified here)

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:

#[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

TODOs

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@JustusAdam JustusAdam self-assigned this Oct 2, 2023
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Oct 2, 2023
@JustusAdam JustusAdam changed the title Basic Modifies Clauses for Function Contracts Basic modifies Clauses for Function Contracts Oct 3, 2023
@celinval
Copy link
Contributor

celinval commented Jan 4, 2024

  1. Can you please create a second PR that updates the RFC with the new syntax and semantics of modifies?
  2. For the error messages, I recommend you to rewrite the error string that comes from CBMC in a follow up PR. We shouldn't be printing internal variables in any user message. One possibility is to add a map in the contracts metadata that can be used to map the modify location to the internal variable name.

@JustusAdam
Copy link
Contributor Author

Thanks for the review. I'll get to your individual changes in a bit but I thought I'd address this question first.

From a design perspective, I was wondering why we need the ContractInfoChannel. Can we compute the information upfront at the same time we generate the HarnessMetadata?

Technically yes, we could compute it then, however the information relies on the output of the reachability analysis, so we'd have to run a separate reachability pass. If you're happy with that overhead, and also the complexity of having two separate passes or a generic, visitor-like, reusable pass then yes, we can precompute.

@celinval
Copy link
Contributor

Thanks for the review. I'll get to your individual changes in a bit but I thought I'd address this question first.

From a design perspective, I was wondering why we need the ContractInfoChannel. Can we compute the information upfront at the same time we generate the HarnessMetadata?

Technically yes, we could compute it then, however the information relies on the output of the reachability analysis, so we'd have to run a separate reachability pass. If you're happy with that overhead, and also the complexity of having two separate passes or a generic, visitor-like, reusable pass then yes, we can precompute.

That's because you need the mangled name for the function, right? If you need the result of the reachability analysis, the upfront analysis won't work, since the harness could have stubs that influence the reachability result.

Another possibility is to use the QueryDb which is already shared between KaniCompiler and GotocCodegenBackend

@JustusAdam
Copy link
Contributor Author

That's because you need the mangled name for the function, right? If you need the result of the reachability analysis, the upfront analysis won't work, since the harness could have stubs that influence the reachability result.

Not just the mangled name of the function, but the mangled name of the instance which we only know post-reachability.

@JustusAdam
Copy link
Contributor Author

Another possibility is to use the QueryDb which is already shared between KaniCompiler and GotocCodegenBackend

I can do that, however there is actually a comment in the code gen "Queries shouldn't change today once codegen starts." which I would be violating. Just so you know

Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a few more changes, and I think we'll be ready to go. Thanks

kani-compiler/src/kani_queries/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_queries/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_queries/mod.rs Outdated Show resolved Hide resolved
kani-driver/src/call_goto_instrument.rs Show resolved Hide resolved
@feliperodri feliperodri merged commit 3467ba1 into model-checking:main Feb 2, 2024
19 of 20 checks passed
@JustusAdam JustusAdam deleted the new-assigns-check branch February 5, 2024 16:27
feliperodri added a commit that referenced this pull request Feb 9, 2024
## What's Changed
* `modifies` Clauses for Function Contracts by @JustusAdam in
#2800
* Fix ICEs due to mismatched arguments by @celinval in
#2994. Resolves the following
issues:
  * #2260
  * #2312
* Enable powf*, exp*, log* intrinsics by @tautschnig in
#2996
* Upgrade Rust toolchain to nightly-2024-01-24 by @celinval @feliperodri
@qinheping

**Full Changelog**:
kani-0.45.0...kani-0.46.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Co-authored-by: Celina G. Val <celinval@amazon.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
Status: No status
Status: No status
Status: No status
Development

Successfully merging this pull request may close these issues.

Basic assigns clause implementation for function contracts
4 participants