Diverging `modifies` clauses cause unsound vacuity #2909

JustusAdam · 2023-12-01T15:59:12Z

Diverging (panicking) expressions, such as indexing, in a modifies clause lead to vacuous verification.

The text was updated successfully, but these errors were encountered:

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>

celinval · 2024-03-25T21:55:25Z

Can you please clarify what you mean here? Maybe an example with the current output would be helpful. Will the overall verification succeed?

jsalzbergedu · 2024-05-30T16:24:42Z

An example of code that verifies vacuously, found with the help of @pi314mm :

// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: -Zfunction-contracts

// Test that a modifies clause works when a (function call)
// expression is provided
fn infinite_looper() -> usize {
    loop {};
    1
}

#[kani::requires(arr[idx] == 1)]
#[kani::modifies(&arr[infinite_looper()])]
#[kani::ensures(arr[idx] == 2)]
fn modify(idx: usize, arr: &mut [i64]) {
    arr[idx] += 1;
}

#[kani::proof_for_contract(modify)]
fn main() {
    let mut arr: [i64; 4] = [1, 2, 3, 4];
    modify(1, &mut arr);
}

jsalzbergedu · 2024-05-30T21:19:13Z

A note: Justus mentioned over email that code like this may have been the original source of the bug, but it was bugged in an earlier version.
https://github.com/JustusAdam/kani/blob/10208dc9f99e8bb5cd80d7b1bb0be69334906388/tests/expected/function-contract/fixme_vec_map_example.rs#L111

zhassan-aws · 2024-05-30T21:35:18Z

This can be reproduced without modifies clauses as well, e.g.:

#[kani::ensures(result == 1)]
fn foo() -> i32 {
    loop {};
    2
}

#[kani::proof_for_contract(foo)]
fn check_foo() {
    let _ = foo();
}

$ kani contract_loop.rs -Zfunction-contracts
Kani Rust Verifier 0.51.0 (standalone)
warning: unreachable expression
 --> contract_loop.rs:4:5
  |
3 |     loop {};
  |     ------- any code following this expression is unreachable
4 |     2
  |     ^ unreachable expression
  |
  = note: `#[warn(unreachable_code)]` on by default

warning: 1 warning emitted

warning: unreachable expression
 --> contract_loop.rs:4:5
  |
3 |     loop {};
  |     ------- any code following this expression is unreachable
4 |     2
  |     ^ unreachable expression
  |
  = note: `#[warn(unreachable_code)]` on by default

warning: Found the following unsupported constructs:
             - caller_location (1)
             - foreign function (2)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

warning: 2 warnings emitted

Checking harness check_foo...
CBMC 5.95.1 (cbmc-5.95.1)
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Reading GOTO program from file /home/ubuntu/examples/contract_loop__RNvCsiqQmiVO2X69_13contract_loop9check_foo.out
...
SUMMARY:
 ** 0 of 1312 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 1.7906353s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

zhassan-aws · 2024-05-30T21:41:25Z

And with a divergent while loop as well if loop contract synthesis is enabled:

#[kani::ensures(result == 1)]
fn foo() -> i32 {
    let i = 0;
    while i < 10 {}
    2
}

#[kani::proof_for_contract(foo)]
fn check_foo() {
    let _ = foo();
}

$ kani contract_loop.rs -Zfunction-contracts --synthesize-loop-contracts --enable-unstable
Kani Rust Verifier 0.51.0 (standalone)
warning: Found the following unsupported constructs:
             - caller_location (1)
             - foreign function (2)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

warning: 1 warning emitted

Running loop contract synthesizer.
warning: This process may not terminate.
warning: Loop-contracts synthesizer is not compatible with unwinding bounds. Unwind bounds will be ignored.
Checking harness check_foo...
CBMC 5.95.1 (cbmc-5.95.1)
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Reading GOTO program from file /home/ubuntu/examples/contract_loop__RNvCsiqQmiVO2X69_13contract_loop9check_foo.out

...


SUMMARY:
 ** 0 of 1318 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 1.8091615s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

zhassan-aws · 2024-05-30T21:44:13Z

One way to fix that is to fail if the post-condition is unreachable. In the cases above, the check is indeed reported as unreachable:

Check 116: foo_check_516471.assertion.1
         - Status: UNREACHABLE
         - Description: "result == 1"
         - Location: contract_loop.rs:1:1 in function foo_check_516471

celinval · 2024-05-31T17:19:48Z

Why isn't the unwinding assertion failing in this case?

zhassan-aws · 2024-05-31T17:25:08Z

Apparently, CBMC replaces infinite loops with assume(false). This is an excerpt from the CBMC output:

Starting Bounded Model Checking
replacing self-loop at file contract_loop.rs line 5 column 5 function foo_wrapper_493980 by assume(FALSE)
no unwinding assertion will be generated for self-loop at file contract_loop.rs line 5 column 5 function foo_wrapper_493980

zhassan-aws · 2024-05-31T17:27:48Z

But in the case of using the loop synthesizer, one has to prove that the loop terminates for the loop abstraction to be sound.

JustusAdam · 2024-05-31T20:41:35Z

Apparently, CBMC replaces infinite loops with assume(false). This is an excerpt from the CBMC output:

Starting Bounded Model Checking
replacing self-loop at file contract_loop.rs line 5 column 5 function foo_wrapper_493980 by assume(FALSE)
no unwinding assertion will be generated for self-loop at file contract_loop.rs line 5 column 5 function foo_wrapper_493980

This sounds like UB. C compilers also assume that you never write infinite loops.

jsalzbergedu · 2024-06-03T17:02:10Z

@JustusAdam ,
Could you provide the context in which this error can be reproduced? Building kani on your fork and then running it on this seems to fail.

tautschnig · 2024-06-04T09:51:04Z

#3223 should address most of what is discussed here, except #2909 (comment) requires further investigation.

JustusAdam · 2024-06-04T20:12:42Z

Oh I made a mistake. I thought this issue was from the old assigns clause implementation, not modifies (I also observed vacuous verifications for that assigns clause though). I don't recall the example I tried this on, sorry.

feliperodri · 2024-06-05T18:43:35Z

I suggest that we close this issue once #3223 is merged and @qinheping could investigate the example from #2909 (comment), which it seems to be more related to loop synthesis, as a separate issue. @zhassan-aws @tautschnig any thoughts?

CBMC's symbolic execution by default turns `while(true) {}` loops into `assume(false)` to counter trivial non-termination of symbolic execution. When unwinding assertions are enabled, however, we should report the non-termination of such loops. Resolves: #2909

JustusAdam changed the title ~~Diverging modifies clauses cause vacuity~~ Diverging modifies clauses cause unsound vacuity Dec 1, 2023

JustusAdam mentioned this issue Dec 1, 2023

modifies Clauses for Function Contracts #2800

Merged

10 tasks

JustusAdam added this to the Function Contracts MVP milestone Dec 4, 2023

feliperodri self-assigned this Feb 28, 2024

pi314mm mentioned this issue May 30, 2024

Disallow side effects in contract expressions #3213

Open

celinval added [C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue labels May 31, 2024

tautschnig mentioned this issue Jun 4, 2024

Do not turn trivially diverging loops into assume(false) #3223

Merged

tautschnig closed this as completed in #3223 Jun 8, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Diverging `modifies` clauses cause unsound vacuity #2909

Diverging `modifies` clauses cause unsound vacuity #2909

JustusAdam commented Dec 1, 2023

celinval commented Mar 25, 2024

jsalzbergedu commented May 30, 2024

jsalzbergedu commented May 30, 2024

zhassan-aws commented May 30, 2024

zhassan-aws commented May 30, 2024

zhassan-aws commented May 30, 2024 •

edited

Loading

celinval commented May 31, 2024 •

edited

Loading

zhassan-aws commented May 31, 2024

zhassan-aws commented May 31, 2024

JustusAdam commented May 31, 2024

jsalzbergedu commented Jun 3, 2024

tautschnig commented Jun 4, 2024

JustusAdam commented Jun 4, 2024

feliperodri commented Jun 5, 2024

Diverging modifies clauses cause unsound vacuity #2909

Diverging modifies clauses cause unsound vacuity #2909

Comments

JustusAdam commented Dec 1, 2023

celinval commented Mar 25, 2024

jsalzbergedu commented May 30, 2024

jsalzbergedu commented May 30, 2024

zhassan-aws commented May 30, 2024

zhassan-aws commented May 30, 2024

zhassan-aws commented May 30, 2024 • edited Loading

celinval commented May 31, 2024 • edited Loading

zhassan-aws commented May 31, 2024

zhassan-aws commented May 31, 2024

JustusAdam commented May 31, 2024

jsalzbergedu commented Jun 3, 2024

tautschnig commented Jun 4, 2024

JustusAdam commented Jun 4, 2024

feliperodri commented Jun 5, 2024

Diverging `modifies` clauses cause unsound vacuity #2909

Diverging `modifies` clauses cause unsound vacuity #2909

zhassan-aws commented May 30, 2024 •

edited

Loading

celinval commented May 31, 2024 •

edited

Loading