From caf5f5d116a89d1749bac54a3848c3bdb0c35a5a Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 30 Apr 2024 00:51:33 -0500 Subject: [PATCH 1/9] 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 + + + +--- From b6745ead6c254ef0d49d403611f09563c870d5a2 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 12 Aug 2024 03:23:58 -0500 Subject: [PATCH 2/9] Address Celina's and Felipe's comments --- rfc/src/rfcs/0012-loop-contracts.md | 123 ++++++++++++++++++---------- 1 file changed, 78 insertions(+), 45 deletions(-) diff --git a/rfc/src/rfcs/0012-loop-contracts.md b/rfc/src/rfcs/0012-loop-contracts.md index 7c968990aa26..7c72b4377fe4 100644 --- a/rfc/src/rfcs/0012-loop-contracts.md +++ b/rfc/src/rfcs/0012-loop-contracts.md @@ -1,6 +1,6 @@ - **Feature Name:** Loop Contracts -- **Feature Request Issue:** -- **RFC PR:** +- **Feature Request Issue:** [#3168](https://github.com/model-checking/kani/issues/3168) +- **RFC PR:** [#3167](https://github.com/model-checking/kani/pull/3167) - **Status:** Under Review - **Version:** 1 - **Proof-of-concept:** @@ -11,23 +11,22 @@ 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, +bounds. The key idea is to over-approximate 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: +The goal for specifying loop contracts in the source code is two fold: -* Unbounded verification: Currently Kani does not support proving correctness +* Unbounded verification: Currently, 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 + loops with dynamic bounds) Kani requires unwinding loops for a large number of + times, which is not always feasible. Loop contracts provide a way to abstract + out loops, and hence remove the need for unwinding loops. +* Faster CI runs: In most cases, the provided contracts 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. + a single iteration. @@ -38,14 +37,15 @@ 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 +A loop contract specifies the behavior of a loop as a boolean predicate +(loop invariants clauses) with certain frames conditions (loop modifies clauses) +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() { +fn simple_loop() { let mut x: u64 = kani::any_where(|i| *i >= 1); while x > 1{ @@ -55,13 +55,13 @@ fn main() { assert!(x == 1); } ``` -The loop in the `main` function keep subtracting 1 from `x` until `x` is 1. +The loop in the `simple_loop` 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() { +fn simple_loop_with_loop_contracts() { let mut x: u64 = kani::any_where(|i| *i >= 1); #[kani::loop_invariant(x >= 1)] @@ -88,7 +88,7 @@ the negation of the loop guard. The requirement of satisfying the negation of th 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() { +fn simple_loop_transformed() { let mut x: u64 = kani::any_where(|i| *i >= 1); x = kani::any(); // Arbitrary program state that @@ -107,9 +107,9 @@ that they stay unchanged throughout the loop are inductive. In other words, Kani 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() { +fn simple_loop_two_vars() { let mut x: u64 = kani::any_where(|i| *i >= 1); - let mut y: u64 = kani::any_where(|i| *i >= 1); + let mut y: u64 = 1; #[kani::loop_invariant(x >= 1)] #[kani::loop_modifies(x)] @@ -118,11 +118,13 @@ fn main() { }; assert!(x == 1); + assert!(y == 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. +location `x` and keep `y` unchanged. Note that if the `modifies` clause contains also +`y`, Kani will havoc both `x` and `y`, and hence violate the assertion `y == 1`. Kani will also verify if all writing targets in the loop are included in the `modifies` @@ -132,56 +134,97 @@ clause. Note that the `modifies` clause is optional, and Kani will infer the write set if not provided. + +### Proof of termination + + Loop contracts also provide a way to prove the termination of the loop. + Without the proof of termination, the loop contracts could lead to a false + positive result. For example, consider the following program: + +```rs +fn simple_loop_non_terminating() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + #[kani::loop_invariant(x >= 1)] + while true{ + x = x; + }; + + assert!(x >= 1); +} +``` +After abstracting the loop, the loop will be transformed to no-op, and the assertion +`x >= 1` will be proved. However, the loop is actually an infinite loop, and the +assertion will never be reached. + +For this reason, Kani will also require the user to provide a `decreases` clause that +specifies a decreasing expression to prove the termination of the loop. For example, in +```rs +fn simple_loop_terminating() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + #[kani::loop_invariant(x >= 1)] + #[kani::loop_decreases(x)] + while x > 1{ + x = x - 1; + }; + + assert!(x >= 1); +} +``` +, the `decreases` clause `#[kani::loop_decreases(x)]` specifies that the value of `x` +decreases at each iteration of the loop, and hence the loop will terminate. + + ## 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. +1. Procedural macros `loop_invariant`, `loop_modifies`, and `loop_decreases`. +2. Code generation for builtin functions expanded from the above macros. 3. GOTO-level loop contracts using CBMC's contract language generated in - `kani-compiler` for `loop-modifies` clauses. + `kani-compiler`. -### Procedural macros `loop_invariant` and `loop_modifies`. +### Procedural macros `loop_invariant`, `loop_modifies`, and `loop_decreases`. 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. +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() { +fn simple_loop_macro_expanded() { 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(); + kani::kani_loop_invariant_begin_marker(); + let __kani_loop_invariant: bool = x >= 1; + kani::kani_loop_invariant_end_marker(); }; assert!(x == 1); } ``` -Similarly, we generate a call to the builtin function `kani_loop_modifies` for modifies +Similarly, we generate calls to the corresponding builtin functions for `modifies` and `decreases` 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 +calls `kani_loop_invariant_begin_marker` and `kani_loop_invariant_end_marker` 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. +of the loop latch, and then 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. @@ -210,7 +253,7 @@ 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 +condition checking for the transformed loop, which will save 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 @@ -218,16 +261,6 @@ 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 From c2d64eedf5500e82259084b4a19ea6e2c5a6d1c3 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 13 Aug 2024 01:12:20 -0500 Subject: [PATCH 3/9] Add explanation about loops with break --- rfc/src/rfcs/0012-loop-contracts.md | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/rfc/src/rfcs/0012-loop-contracts.md b/rfc/src/rfcs/0012-loop-contracts.md index 7c72b4377fe4..366f8adbdb3e 100644 --- a/rfc/src/rfcs/0012-loop-contracts.md +++ b/rfc/src/rfcs/0012-loop-contracts.md @@ -82,11 +82,17 @@ In this case, Kani verifies that the loop invariant `x >= 1` is inductive, i.e., 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: +The idea is, instead of exploring all possible branches of the loop, Kani only needs to +prove those branches reached from an arbitrary program state that satisfies the loop contracts, +after the execution of one iteration of the loop. + +So, for loops without break statements, proving post-loops properties with loop contracts is +equivalent to proving the properties with the loop abstracted out as assuming the post-states +of the loops should satisfying the disjunction of the invariant 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 loops without break statements must fail the loop guard. + +For example, applying loop contracts in `simple_loop` function is equivalent to the following: ```rs fn simple_loop_transformed() { let mut x: u64 = kani::any_where(|i| *i >= 1); From 1afc4a5a769c709a5484746c6eefe8e77ffafb69 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 21 Aug 2024 02:12:43 -0500 Subject: [PATCH 4/9] Update rfc/src/rfcs/0012-loop-contracts.md Co-authored-by: Celina G. Val --- rfc/src/rfcs/0012-loop-contracts.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/rfc/src/rfcs/0012-loop-contracts.md b/rfc/src/rfcs/0012-loop-contracts.md index 366f8adbdb3e..c5d90111fdef 100644 --- a/rfc/src/rfcs/0012-loop-contracts.md +++ b/rfc/src/rfcs/0012-loop-contracts.md @@ -143,9 +143,9 @@ provided. ### Proof of termination - Loop contracts also provide a way to prove the termination of the loop. - Without the proof of termination, the loop contracts could lead to a false - positive result. For example, consider the following program: +Loop contracts also provide a way to prove the termination of the loop. +Without the proof of termination, the loop contracts could lead to a false +positive result. For example, consider the following program: ```rs fn simple_loop_non_terminating() { From 0492ac6ee2d80bb85435f8173f294eccf03eb67f Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 21 Aug 2024 02:57:45 -0500 Subject: [PATCH 5/9] More Celina's comments --- rfc/src/rfcs/0012-loop-contracts.md | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/rfc/src/rfcs/0012-loop-contracts.md b/rfc/src/rfcs/0012-loop-contracts.md index c5d90111fdef..70b2aff9c7fa 100644 --- a/rfc/src/rfcs/0012-loop-contracts.md +++ b/rfc/src/rfcs/0012-loop-contracts.md @@ -86,9 +86,8 @@ The idea is, instead of exploring all possible branches of the loop, Kani only n prove those branches reached from an arbitrary program state that satisfies the loop contracts, after the execution of one iteration of the loop. -So, for loops without break statements, proving post-loops properties with loop contracts is -equivalent to proving the properties with the loop abstracted out as assuming the post-states -of the loops should satisfying the disjunction of the invariant and the negation of the loop guard. +So, for loops without break statements, we can assume all post-states of the loop satisfying +`inv && !loop_guard` for proving post-loops properties. The requirement of satisfying the negation of the loop guard comes from the fact that a path exits loops without break statements must fail the loop guard. @@ -144,8 +143,9 @@ provided. ### Proof of termination Loop contracts also provide a way to prove the termination of the loop. -Without the proof of termination, the loop contracts could lead to a false -positive result. For example, consider the following program: +Without the proof of termination, Kani could report success of some assertions that +are actually unreachable due to non-terminating loops. +For example, consider the following program: ```rs fn simple_loop_non_terminating() { @@ -227,7 +227,7 @@ When generating GOTO program from MIR, Kani will first scan for the placeholder calls `kani_loop_invariant_begin_marker` and `kani_loop_invariant_end_marker` 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. +to the loop latches---the jumps 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 then apply and prove the extracted loop contracts. @@ -267,6 +267,11 @@ easier. ## Open questions +- How do we integrate loop contracts with the synthesis tool? When the user-provided + loop contracts are not enough prove the harness, we expect the loop-contract synthesizer + can fix the loop contracts. +- How do we translate back modify targets that inferred by CBMC to Rust level? + ## Future possibilities From 14ca09a5090aa9a2ee7e98923213f48a3d3d230f Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 23 Aug 2024 02:21:10 -0500 Subject: [PATCH 6/9] Remove implmentation detail and add more open Qs --- rfc/src/rfcs/0012-loop-contracts.md | 39 +++++------------------------ 1 file changed, 6 insertions(+), 33 deletions(-) diff --git a/rfc/src/rfcs/0012-loop-contracts.md b/rfc/src/rfcs/0012-loop-contracts.md index 70b2aff9c7fa..760712319b92 100644 --- a/rfc/src/rfcs/0012-loop-contracts.md +++ b/rfc/src/rfcs/0012-loop-contracts.md @@ -194,47 +194,18 @@ Kani implements the functionality of loop contracts in three places. ### Procedural macros `loop_invariant`, `loop_modifies`, and `loop_decreases`. -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 simple_loop_macro_expanded() { - let mut x: u64 = kani::any_where(|i| *i >= 1); - - while x > 1{ - x = x - 1; - kani::kani_loop_invariant_begin_marker(); - let __kani_loop_invariant: bool = x >= 1; - kani::kani_loop_invariant_end_marker(); - }; - - assert!(x == 1); -} -``` - -Similarly, we generate calls to the corresponding builtin functions for `modifies` and `decreases` -clauses. +We extend the three macros `loop_invariant`, `loop_modifies`, and `loop_decreases` to +corresponding Rust code. Kani will then compile them into MIR-level code. ### Code Generation for Builtin Functions -When generating GOTO program from MIR, Kani will first scan for the placeholder function -calls `kani_loop_invariant_begin_marker` and `kani_loop_invariant_end_marker` 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 latches---the jumps back to the loop head. +Then in the MIR, we codegen the loop contracts as GOTO-level expressions and annotate them +into the corresponding loop latches---the jumps 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 then 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 @@ -271,6 +242,8 @@ easier. loop contracts are not enough prove the harness, we expect the loop-contract synthesizer can fix the loop contracts. - How do we translate back modify targets that inferred by CBMC to Rust level? +- It is not clear how the CBMC loop modifies inference works for Rust code. We need to + experiment more to decide what would be the best UX of using loop modifies. ## Future possibilities From 4c7c1327b3227b6fffe3716b63edd00e8abd8b94 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 29 Aug 2024 02:58:21 -0500 Subject: [PATCH 7/9] Update rfc/src/rfcs/0012-loop-contracts.md Co-authored-by: Celina G. Val --- rfc/src/rfcs/0012-loop-contracts.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0012-loop-contracts.md b/rfc/src/rfcs/0012-loop-contracts.md index 760712319b92..e20abb3a3d7b 100644 --- a/rfc/src/rfcs/0012-loop-contracts.md +++ b/rfc/src/rfcs/0012-loop-contracts.md @@ -194,8 +194,8 @@ Kani implements the functionality of loop contracts in three places. ### Procedural macros `loop_invariant`, `loop_modifies`, and `loop_decreases`. -We extend the three macros `loop_invariant`, `loop_modifies`, and `loop_decreases` to -corresponding Rust code. Kani will then compile them into MIR-level code. +We will implement the three proc-macros `loop_invariant`, `loop_modifies`, and `loop_decreases` to +embed the annotation logic as Rust code. Kani will then compile them into MIR-level code. ### Code Generation for Builtin Functions From 6b1acfcec468982c3eab49f474f1faca7c776339 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 29 Aug 2024 15:29:35 -0500 Subject: [PATCH 8/9] More future possibilities and open questions --- rfc/src/rfcs/0012-loop-contracts.md | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/rfc/src/rfcs/0012-loop-contracts.md b/rfc/src/rfcs/0012-loop-contracts.md index e20abb3a3d7b..31d1362184fa 100644 --- a/rfc/src/rfcs/0012-loop-contracts.md +++ b/rfc/src/rfcs/0012-loop-contracts.md @@ -131,14 +131,10 @@ Then when use the loop contracts to abstract the loop, Kani will only havoc the location `x` and keep `y` unchanged. Note that if the `modifies` clause contains also `y`, Kani will havoc both `x` and `y`, and hence violate the assertion `y == 1`. - -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. - +Kani can employs CBMC's write set inference to infer the write set of the loop. +So users have to specify the `modifies` clauses by their self only when the inferred write +sets are not complete---there exists some target that could be written to in the loop but +is not in the inferred write set. ### Proof of termination @@ -244,9 +240,17 @@ easier. - How do we translate back modify targets that inferred by CBMC to Rust level? - It is not clear how the CBMC loop modifies inference works for Rust code. We need to experiment more to decide what would be the best UX of using loop modifies. +- How do we handle havocing in unsafe code where it is fine to break the safety invariant + of Rust? In that case, we may need havocing function that preserves validity invariant + but not safety invariant. ## Future possibilities +- We can improve the UX by allowing users to choose if they want to apply loop contracts + to certain annotated loops or not. +- We can employ CBMC's decreases inference to infer the decreases clauses to reduce the + user burden of specifying the decreases clauses. + --- From 6d373c2dc195ecca9f688f4d57a64fbe1c4f12a4 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Sun, 1 Sep 2024 11:10:04 -0500 Subject: [PATCH 9/9] Added clarification about question of opt-out from loop contracts --- rfc/src/rfcs/0012-loop-contracts.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0012-loop-contracts.md b/rfc/src/rfcs/0012-loop-contracts.md index 31d1362184fa..1c0bcdafd750 100644 --- a/rfc/src/rfcs/0012-loop-contracts.md +++ b/rfc/src/rfcs/0012-loop-contracts.md @@ -243,11 +243,10 @@ easier. - How do we handle havocing in unsafe code where it is fine to break the safety invariant of Rust? In that case, we may need havocing function that preserves validity invariant but not safety invariant. +- What is the proper mechanism for users to specify the loops that they want to opt-out from applying loop contracts, and (optionally) the unwind numbers for them. Such options should be per-harness. ## Future possibilities -- We can improve the UX by allowing users to choose if they want to apply loop contracts - to certain annotated loops or not. - We can employ CBMC's decreases inference to infer the decreases clauses to reduce the user burden of specifying the decreases clauses.