From caf5f5d116a89d1749bac54a3848c3bdb0c35a5a Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 30 Apr 2024 00:51:33 -0500 Subject: [PATCH] RFC: Loop Contracts --- rfc/src/rfcs/0012-loop-contracts.md | 235 ++++++++++++++++++++++++++++ 1 file changed, 235 insertions(+) create mode 100644 rfc/src/rfcs/0012-loop-contracts.md diff --git a/rfc/src/rfcs/0012-loop-contracts.md b/rfc/src/rfcs/0012-loop-contracts.md new file mode 100644 index 000000000000..7c968990aa26 --- /dev/null +++ b/rfc/src/rfcs/0012-loop-contracts.md @@ -0,0 +1,235 @@ +- **Feature Name:** Loop Contracts +- **Feature Request Issue:** +- **RFC PR:** +- **Status:** Under Review +- **Version:** 1 +- **Proof-of-concept:** + +------------------- + +## Summary + +Loop contracts provide way to safely abstract loops of a program, typically +in order to accelerate the verification process, and remove the loop unwinding +bounds. The key idea is to overapproximate the possible set of program states, +while still being precise enough to be able to prove the desired property. + +## User Impact + +Loop contracts provide an interface for a verified, sound abstraction. +The goal for specifying loop contracts in the source code is three fold: + +* Unbounded verification: Currently Kani does not support proving correctness + (i.e. assertions never fail) on programs with unbounded control flow (e.g. + loops with dynamic bounds). Kani unrolls all unbounded loops until a few + iterations and then verifies this unrolled program — it thus provides a much + weaker guarantee on correctness. +* Faster CI runs: These contracts, when provided, would also significantly + improve Kani's verification time since all loops would be unrolled only to + a single iteration, as opposed to a small number of iterations which is + Kani's current behavior. + + + +Loop contracts are completely optional with no user impact if unused. This +RFC proposes the addition of new attributes, and functions, that shouldn't +interfere with existing functionalities. + + +## User Experience + +A loop contract specifies the behavior of a loop as a predicate that +can be checked against the loop implementation, and used to abstract out +the loop in the verification process. + +We illustrate the usage of loop contracts with an example. +Consider the following program: +```rs +fn main() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + while x > 1{ + x = x - 1; + }; + + assert!(x == 1); +} +``` +The loop in the `main` function keep subtracting 1 from `x` until `x` is 1. +However, Kani currently needs to unroll the loop for `u64::MAX` number of times +to verify the assertion at the end of the program. + +With loop contracts, the user can specify the behavior of the loop as follows: +```rs +fn main() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + #[kani::loop_invariant(x >= 1)] + while x > 1{ + x = x - 1; + }; + + assert!(x == 1); +} +``` +The loop invariant clause `#[kani::loop_invariant(x >= 1)]` specifies the loop +invariants that must hold at the beginning of each iteration of the loop right before +checking the loop guard. + +In this case, Kani verifies that the loop invariant `x >= 1` is inductive, i.e., +`x` is always greater than or equal to 1 at each iteration before checking `x > 1`. + + +Also, once Kani proved that the loop invariant is inductive, it can safely use the loop +invariants to abstract the loop out of the verification process. +The idea is, instead of exploring all possible branches of the loop, Kani can safely +substitute the loops with any of program states that satisfy the loop invariants and +the negation of the loop guard. The requirement of satisfying the negation of the loop +guard comes from the fact that a path exits the loop must fail the loop guard. +After the loop is abstracted, the program will be equivalent to the following: +```rs +fn main() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + x = kani::any(); // Arbitrary program state that + kani::assume( !(x > 1) && x >= 1); // satisfies !`guard` && `inv` + + assert!(x == 1); +} +``` +The assumption above is actually equivalent to `x == 1`, hence the assertion at the end +of the program is proved. + +### Write Sets and Havocking + +For those memory locations that are not modified in the loop, loop invariants state +that they stay unchanged throughout the loop are inductive. In other words, Kani should +only havoc the memory locations that are modified in the loop. This is achieved by +specifying the `modifies` clause for the loop. For example, the following program: +```rs +fn main() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + let mut y: u64 = kani::any_where(|i| *i >= 1); + + #[kani::loop_invariant(x >= 1)] + #[kani::loop_modifies(x)] + while x > 1{ + x = x - 1; + }; + + assert!(x == 1); +} +``` +write to only `x` in the loop, hence the `modifies` clause contains only `x`. +Then when use the loop contracts to abstract the loop, Kani will only havoc the memory +location `x` and keep `y` unchanged. + + +Kani will also verify if all writing targets in the loop are included in the `modifies` +clause. + + +Note that the `modifies` clause is optional, and Kani will infer the write set if not +provided. + +## Detailed Design + + +Kani implements the functionality of loop contracts in three places. + +1. Procedural macros `loop_invariant` and `loop_modifies`. +2. Code generation for builtin functions expanded from the above two macros. +3. GOTO-level loop contracts using CBMC's contract language generated in + `kani-compiler` for `loop-modifies` clauses. + +### Procedural macros `loop_invariant` and `loop_modifies`. + +The `loop_invariant` macro perform code generation for the loop invariant clause. +The generated code consists of two parts: +1. a closure definition to wrap the loop invariant, which is an boolean expression. +2. a call to a builtin function `kani_loop_invariant` at end of the loop. + +As an example, in the above program, the following code will be generated for the +loop invariants clauses: + +```rs +fn main() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + let _loop_invariant_closure = || x >= 1; + while x > 1{ + x = x - 1; + kani_loop_invariant_begin(); + _loop_invariant_closure() + kani_loop_invariant_end(); + }; + + assert!(x == 1); +} +``` + +Similarly, we generate a call to the builtin function `kani_loop_modifies` for modifies +clauses. + + +### Code Generation for Builtin Functions + +When generating GOTO program from MIR, Kani will first scan for the placeholder function +calls `kani_loop_invariant_begin` and `kani_loop_invariant_end` in the MIR. Then Kani +will generate the corresponding GOTO-level statement expression for all instructions +between the two placeholder function calls. At last, Kani will add the statement expression +to the loop latch---the jump back to the loop head. + +The artifact `goto-instrument` in CBMC will extract the loop contracts from the named-subs +of the loop latch, and the apply and prove the extracted loop contracts. + +Similarly, Kani will add the `modifies` targets into the named-subs of the loop latch for +CBMC to extract and prove the loop contracts. + + +### GOTO-Level Havocing + +The ordinary havocing in CBMC is not aware of the type constraints of Rust type. +Hence, we will use customized havocing functions for modifies targets. In detail, +Kani will generate code for the definition of corresponding `kani::any()` functions +for each modifies target. Then Kani will create a map from the modifies target to the +the name of its `kani::any()` function, and add the map to the loop latch too. + +On the CBMC site, `goto-instrument` will extract the map and instrument the customized +havocing functions for the modifies targets. + +## Rationale and alternatives + + + +### Rust-Level Transformation vs CBMC + +Besides transforming the loops in GOTO level using `goto-instrument`, +we could also do the transformation in Rust level using procedural macros, or +in MIR level. + +There are two reasons we prefer the GOTO-level transformation. +First, `goto-instrument` is a mature tool that can correctly instrument the frame +condition checking for the transformed loop, which will safe us from reinventing +the error-prone wheel. Second, the loop contracts synthesis tool we developed and +are developing are all based on GOTO level. Hence, doing the transformation in +the GOTO level will make the integration of loop contracts with the synthesis tool +easier. + +## Open questions + + + +- The idea of using closure to wrap the loop invariant is a bit hacky. It is not + clear what behavior of the loop will move the variables in the closure, and hence + invalidate the closure. Is there a better way to do this? + + +## Future possibilities + + + +---