From feec92f31bd4cb675ee20dfa0c1c683d986c9be4 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 1 Apr 2025 12:54:58 -0700 Subject: [PATCH 01/13] save file --- .../kani_middle/transform/loop_contracts.rs | 28 ++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index 323cff742ee7..fa592f6cd55b 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -23,6 +23,25 @@ use stable_mir::ty::{FnDef, MirConst, RigidTy, UintTy}; use std::collections::{HashMap, HashSet, VecDeque}; use std::fmt::Debug; +fn print_stable_mir(body: &Body) { + // Print basic blocks in order + for (bb_idx, bb) in body.blocks.iter().enumerate() { + println!("bb{bb_idx}:"); + + // Print statements + for stmt in &bb.statements { + println!(" {stmt:?}"); + } + + // Print terminator + let terminator = &bb.terminator; + println!(" terminator: {:?}", terminator.kind); + //println!(" span: {:?}", terminator.span); + + } +} + + #[derive(Debug, Default)] pub struct LoopContractPass { /// Cache KaniRunContract function used to implement contracts. @@ -133,7 +152,14 @@ impl TransformPass for LoopContractPass { } } } - (contain_loop_contracts, new_body.into()) + //println!("Loop contracts: {}", contain_loop_contracts); + let nb : Body = new_body.into(); + if contain_loop_contracts { + //println!("{:#?}", nb); + print_stable_mir(&nb); + assert!(1==0); + } + (contain_loop_contracts, nb) } } _ => { From d9974c9e4363fd95799060919b96577c09c22c5f Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 2 Apr 2025 11:38:00 -0700 Subject: [PATCH 02/13] support for funtion + loop contract --- .../kani_middle/transform/loop_contracts.rs | 100 +++++++----------- 1 file changed, 41 insertions(+), 59 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index fa592f6cd55b..31fa225c196b 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -8,8 +8,8 @@ use super::TransformPass; use crate::kani_middle::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::kani_functions::KaniModel; -use crate::kani_middle::transform::TransformationType; use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::{TransformationType, body}; use crate::kani_queries::QueryDb; use crate::stable_mir::CrateDef; use rustc_middle::ty::TyCtxt; @@ -23,25 +23,6 @@ use stable_mir::ty::{FnDef, MirConst, RigidTy, UintTy}; use std::collections::{HashMap, HashSet, VecDeque}; use std::fmt::Debug; -fn print_stable_mir(body: &Body) { - // Print basic blocks in order - for (bb_idx, bb) in body.blocks.iter().enumerate() { - println!("bb{bb_idx}:"); - - // Print statements - for stmt in &bb.statements { - println!(" {stmt:?}"); - } - - // Print terminator - let terminator = &bb.terminator; - println!(" terminator: {:?}", terminator.kind); - //println!(" span: {:?}", terminator.span); - - } -} - - #[derive(Debug, Default)] pub struct LoopContractPass { /// Cache KaniRunContract function used to implement contracts. @@ -122,47 +103,13 @@ impl TransformPass for LoopContractPass { let run = Instance::resolve(self.run_contract_fn.unwrap(), args).unwrap(); (true, run.body().unwrap()) } else { - let mut new_body = MutableBody::from(body); - let mut contain_loop_contracts: bool = false; - - // Visit basic blocks in control flow order (BFS). - let mut visited: HashSet = HashSet::new(); - let mut queue: VecDeque = VecDeque::new(); - // Visit blocks in loops only when there is no blocks in queue. - let mut loop_queue: VecDeque = VecDeque::new(); - queue.push_back(0); - - while let Some(bb_idx) = queue.pop_front().or_else(|| loop_queue.pop_front()) { - visited.insert(bb_idx); - - let terminator = new_body.blocks()[bb_idx].terminator.clone(); - - let is_loop_head = self.transform_bb(tcx, &mut new_body, bb_idx); - contain_loop_contracts |= is_loop_head; - - // Add successors of the current basic blocks to - // the visiting queue. - for to_visit in terminator.successors() { - if !visited.contains(&to_visit) { - if is_loop_head { - loop_queue.push_back(to_visit); - } else { - queue.push_back(to_visit) - }; - } - } - } - //println!("Loop contracts: {}", contain_loop_contracts); - let nb : Body = new_body.into(); - if contain_loop_contracts { - //println!("{:#?}", nb); - print_stable_mir(&nb); - assert!(1==0); - } - (contain_loop_contracts, nb) + self.transform_body_with_loop(tcx, body) } } + RigidTy::Closure(_, _) => self.transform_body_with_loop(tcx, body), _ => { + println!("Instance defid: {:?}", instance.def.name()); + println!("Instance ty: {:?}", instance.ty().kind().rigid().unwrap()); /* static variables case */ (false, body) } @@ -220,6 +167,41 @@ impl LoopContractPass { )) } + fn transform_body_with_loop(&mut self, tcx: TyCtxt, body: Body) -> (bool, Body) { + let mut new_body = MutableBody::from(body); + let mut contain_loop_contracts: bool = false; + + // Visit basic blocks in control flow order (BFS). + let mut visited: HashSet = HashSet::new(); + let mut queue: VecDeque = VecDeque::new(); + // Visit blocks in loops only when there is no blocks in queue. + let mut loop_queue: VecDeque = VecDeque::new(); + queue.push_back(0); + + while let Some(bb_idx) = queue.pop_front().or_else(|| loop_queue.pop_front()) { + visited.insert(bb_idx); + + let terminator = new_body.blocks()[bb_idx].terminator.clone(); + + let is_loop_head = self.transform_bb(tcx, &mut new_body, bb_idx); + contain_loop_contracts |= is_loop_head; + + // Add successors of the current basic blocks to + // the visiting queue. + for to_visit in terminator.successors() { + if !visited.contains(&to_visit) { + if is_loop_head { + loop_queue.push_back(to_visit); + } else { + queue.push_back(to_visit) + }; + } + } + } + + (contain_loop_contracts, new_body.into()) + } + /// Transform loops with contracts from /// ```ignore /// bb_idx: { @@ -336,7 +318,7 @@ impl LoopContractPass { for stmt in &new_body.blocks()[bb_idx].statements { if let StatementKind::Assign(place, rvalue) = &stmt.kind { match rvalue { - Rvalue::Ref(_,_,rplace) => { + Rvalue::Ref(_,_,rplace) | Rvalue::CopyForDeref(rplace) => { if supported_vars.contains(&rplace.local) { supported_vars.push(place.local); } } From 06439f7ba4bbeca84ab995e4c9ba79ab5d20988a Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 2 Apr 2025 11:38:32 -0700 Subject: [PATCH 03/13] add expected tests --- ...contract_proof_function_with_loop.expected | 13 ++++++++++ .../contract_proof_function_with_loop.rs | 25 +++++++++++++++++++ .../function_call_with_loop.expected | 11 ++++++++ .../loop-contract/function_call_with_loop.rs | 25 +++++++++++++++++++ 4 files changed, 74 insertions(+) create mode 100644 tests/expected/loop-contract/contract_proof_function_with_loop.expected create mode 100644 tests/expected/loop-contract/contract_proof_function_with_loop.rs create mode 100644 tests/expected/loop-contract/function_call_with_loop.expected create mode 100644 tests/expected/loop-contract/function_call_with_loop.rs diff --git a/tests/expected/loop-contract/contract_proof_function_with_loop.expected b/tests/expected/loop-contract/contract_proof_function_with_loop.expected new file mode 100644 index 000000000000..0109678c22fd --- /dev/null +++ b/tests/expected/loop-contract/contract_proof_function_with_loop.expected @@ -0,0 +1,13 @@ +has_loop::{closure#2}::{closure#1}.loop_invariant_step.1\ + - Status: SUCCESS\ + - Description: "Check invariant after step for loop has_loop::{closure#2}::{closure#1}.0"\ +in function has_loop::{closure#2}::{closure#1} + + + +has_loop::{closure#2}::{closure#1}.precondition_instance.1\ + - Status: SUCCESS\ + - Description: "free argument must be NULL or valid pointer"\ +in function has_loop::{closure#2}::{closure#1} + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/contract_proof_function_with_loop.rs b/tests/expected/loop-contract/contract_proof_function_with_loop.rs new file mode 100644 index 000000000000..1fecda900e23 --- /dev/null +++ b/tests/expected/loop-contract/contract_proof_function_with_loop.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Proving contract for function with loop + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +#[kani::requires(i>=2)] +#[kani::ensures(|ret| *ret == 2)] +pub fn has_loop(mut i: u16) -> u16 { + #[kani::loop_invariant(i>=2)] + while i > 2 { + i = i - 1 + } + i +} + +#[kani::proof_for_contract(has_loop)] +fn contract_proof() { + let i: u16 = kani::any(); + let j = has_loop(i); +} diff --git a/tests/expected/loop-contract/function_call_with_loop.expected b/tests/expected/loop-contract/function_call_with_loop.expected new file mode 100644 index 000000000000..d16789b1d209 --- /dev/null +++ b/tests/expected/loop-contract/function_call_with_loop.expected @@ -0,0 +1,11 @@ +has_loop::{closure#3}::{closure#0}.loop_invariant_base.1\ + - Status: SUCCESS\ + - Description: "Check invariant before entry for loop has_loop::{closure#3}::{closure#0}.0"\ +in function has_loop::{closure#3}::{closure#0} + +has_loop::{closure#3}::{closure#0}.precondition_instance.5\ + - Status: SUCCESS\ + - Description: "free called for new[] object"\ +in function has_loop::{closure#3}::{closure#0} + +Failed Checks: i>=2 diff --git a/tests/expected/loop-contract/function_call_with_loop.rs b/tests/expected/loop-contract/function_call_with_loop.rs new file mode 100644 index 000000000000..2e3f9112f2eb --- /dev/null +++ b/tests/expected/loop-contract/function_call_with_loop.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Calling a function that contains loops + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +#[kani::requires(i>=2)] +#[kani::ensures(|ret| *ret == 2)] +pub fn has_loop(mut i: u16) -> u16 { + #[kani::loop_invariant(i>=2)] + while i > 2 { + i = i - 1 + } + i +} + +#[kani::proof] +fn call_has_loop() { + let i: u16 = kani::any(); + let j = has_loop(i); +} From a56661742a7b274a506db0e592780b7eb91104e9 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 2 Apr 2025 11:43:22 -0700 Subject: [PATCH 04/13] fix clippy --- kani-compiler/src/kani_middle/transform/loop_contracts.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index 31fa225c196b..66db10b2aa33 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -9,7 +9,7 @@ use crate::kani_middle::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::kani_functions::KaniModel; use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; -use crate::kani_middle::transform::{TransformationType, body}; +use crate::kani_middle::transform::TransformationType; use crate::kani_queries::QueryDb; use crate::stable_mir::CrateDef; use rustc_middle::ty::TyCtxt; From 246b82f0e2332d5cbaf7106b0a7ff79ba6eda01f Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 2 Apr 2025 11:48:05 -0700 Subject: [PATCH 05/13] fix format --- kani-compiler/src/kani_middle/transform/loop_contracts.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index 66db10b2aa33..c85b9b87c9a4 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -8,8 +8,8 @@ use super::TransformPass; use crate::kani_middle::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::kani_functions::KaniModel; -use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use crate::kani_middle::transform::TransformationType; +use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use crate::kani_queries::QueryDb; use crate::stable_mir::CrateDef; use rustc_middle::ty::TyCtxt; From fd2d98b7a41596d1cc0f261e827b61dcfd5d16a3 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 2 Apr 2025 13:10:22 -0700 Subject: [PATCH 06/13] fix command flag --- .../expected/loop-contract/contract_proof_function_with_loop.rs | 2 +- tests/expected/loop-contract/function_call_with_loop.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/expected/loop-contract/contract_proof_function_with_loop.rs b/tests/expected/loop-contract/contract_proof_function_with_loop.rs index 1fecda900e23..d979b017f9fb 100644 --- a/tests/expected/loop-contract/contract_proof_function_with_loop.rs +++ b/tests/expected/loop-contract/contract_proof_function_with_loop.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z loop-contracts +// kani-flags: -Z loop-contracts -Z function-contracts //! Proving contract for function with loop diff --git a/tests/expected/loop-contract/function_call_with_loop.rs b/tests/expected/loop-contract/function_call_with_loop.rs index 2e3f9112f2eb..6022111038c2 100644 --- a/tests/expected/loop-contract/function_call_with_loop.rs +++ b/tests/expected/loop-contract/function_call_with_loop.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z loop-contracts +// kani-flags: -Z loop-contracts -Z function-contracts //! Calling a function that contains loops From b681408d6f667b85d18e80d012e0e7bb3e1811aa Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 7 Apr 2025 13:51:59 -0700 Subject: [PATCH 07/13] Update kani-compiler/src/kani_middle/transform/loop_contracts.rs Co-authored-by: Carolyn Zech --- kani-compiler/src/kani_middle/transform/loop_contracts.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index c85b9b87c9a4..e6be671311fd 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -108,8 +108,6 @@ impl TransformPass for LoopContractPass { } RigidTy::Closure(_, _) => self.transform_body_with_loop(tcx, body), _ => { - println!("Instance defid: {:?}", instance.def.name()); - println!("Instance ty: {:?}", instance.ty().kind().rigid().unwrap()); /* static variables case */ (false, body) } From 46cbe09e362b3f2c51649955717e66898772f632 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 7 Apr 2025 13:52:14 -0700 Subject: [PATCH 08/13] Update tests/expected/loop-contract/contract_proof_function_with_loop.rs Co-authored-by: Carolyn Zech --- .../expected/loop-contract/contract_proof_function_with_loop.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/loop-contract/contract_proof_function_with_loop.rs b/tests/expected/loop-contract/contract_proof_function_with_loop.rs index d979b017f9fb..446214979c69 100644 --- a/tests/expected/loop-contract/contract_proof_function_with_loop.rs +++ b/tests/expected/loop-contract/contract_proof_function_with_loop.rs @@ -3,7 +3,7 @@ // kani-flags: -Z loop-contracts -Z function-contracts -//! Proving contract for function with loop +//! Test that we can prove a function contract and a loop contract in tandem. #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] From 098242daab94aa38e67992bbb6ec74fdaa567796 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 11 Apr 2025 07:48:43 -0700 Subject: [PATCH 09/13] add new test and comments --- .../loop-contract/function_call_with_loop.rs | 2 +- .../function_with_loop_no_assertion.expected | 10 ++++++++ .../function_with_loop_no_assertion.rs | 25 +++++++++++++++++++ 3 files changed, 36 insertions(+), 1 deletion(-) create mode 100644 tests/expected/loop-contract/function_with_loop_no_assertion.expected create mode 100644 tests/expected/loop-contract/function_with_loop_no_assertion.rs diff --git a/tests/expected/loop-contract/function_call_with_loop.rs b/tests/expected/loop-contract/function_call_with_loop.rs index 6022111038c2..cb2453496187 100644 --- a/tests/expected/loop-contract/function_call_with_loop.rs +++ b/tests/expected/loop-contract/function_call_with_loop.rs @@ -3,7 +3,7 @@ // kani-flags: -Z loop-contracts -Z function-contracts -//! Calling a function that contains loops +//! Calling a function that contains loops and test that using a #[kani::proof] harness fails because the function's precondition gets asserted. #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] diff --git a/tests/expected/loop-contract/function_with_loop_no_assertion.expected b/tests/expected/loop-contract/function_with_loop_no_assertion.expected new file mode 100644 index 000000000000..f13255a796f8 --- /dev/null +++ b/tests/expected/loop-contract/function_with_loop_no_assertion.expected @@ -0,0 +1,10 @@ +has_loop.loop_invariant_base.1\\ + - Status: SUCCESS\\ + - Description: "Check invariant before entry for loop has_loop.0"\\ +in function has_loop + + +SUMMARY: + ** 0 of 102 failed + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/function_with_loop_no_assertion.rs b/tests/expected/loop-contract/function_with_loop_no_assertion.rs new file mode 100644 index 000000000000..5609796d56be --- /dev/null +++ b/tests/expected/loop-contract/function_with_loop_no_assertion.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts -Z function-contracts --no-assert-contracts + +//Call a function with loop without checking the contract. + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +#[kani::requires(i>=2)] +#[kani::ensures(|ret| *ret == 2)] +pub fn has_loop(mut i: u16) -> u16 { + #[kani::loop_invariant(i>=2)] + while i > 2 { + i = i - 1 + } + i +} + +#[kani::proof] +fn contract_proof() { + let i: u16 = kani::any(); + let j = has_loop(i); +} From fd3758f09ccd54c2de24e7125def9bae4aa27c52 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 11 Apr 2025 08:52:56 -0700 Subject: [PATCH 10/13] fix expected --- .../loop-contract/function_with_loop_no_assertion.expected | 2 -- 1 file changed, 2 deletions(-) diff --git a/tests/expected/loop-contract/function_with_loop_no_assertion.expected b/tests/expected/loop-contract/function_with_loop_no_assertion.expected index f13255a796f8..955254748bc0 100644 --- a/tests/expected/loop-contract/function_with_loop_no_assertion.expected +++ b/tests/expected/loop-contract/function_with_loop_no_assertion.expected @@ -4,7 +4,5 @@ has_loop.loop_invariant_base.1\\ in function has_loop -SUMMARY: - ** 0 of 102 failed VERIFICATION:- SUCCESSFUL From 609c656f13a93c70acb5389c3c3f3c3c2b250d2e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 11 Apr 2025 09:20:58 -0700 Subject: [PATCH 11/13] fix expected --- .../loop-contract/function_with_loop_no_assertion.expected | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/expected/loop-contract/function_with_loop_no_assertion.expected b/tests/expected/loop-contract/function_with_loop_no_assertion.expected index 955254748bc0..afd863b2937b 100644 --- a/tests/expected/loop-contract/function_with_loop_no_assertion.expected +++ b/tests/expected/loop-contract/function_with_loop_no_assertion.expected @@ -1,6 +1,6 @@ -has_loop.loop_invariant_base.1\\ - - Status: SUCCESS\\ - - Description: "Check invariant before entry for loop has_loop.0"\\ +has_loop.loop_invariant_base.1\ + - Status: SUCCESS\ + - Description: "Check invariant before entry for loop has_loop.0"\ in function has_loop From 4509c4388d087172f512ddb9e8ede4de0e1f6a28 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 15 Apr 2025 14:27:01 -0700 Subject: [PATCH 12/13] add comments --- kani-compiler/src/kani_middle/transform/loop_contracts.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index e6be671311fd..a310db036d94 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -165,6 +165,8 @@ impl LoopContractPass { )) } + /// This function transform the function body as described in fn transform. + /// It is the core of fn transform, and is separated just to avoid code repetition. fn transform_body_with_loop(&mut self, tcx: TyCtxt, body: Body) -> (bool, Body) { let mut new_body = MutableBody::from(body); let mut contain_loop_contracts: bool = false; From 38382789258b85b0281760828425c65b83097414 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 9 May 2025 10:37:24 -0700 Subject: [PATCH 13/13] update loop contract doc --- .../reference/experimental/loop-contracts.md | 27 +++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md index 3cf5ecd429cc..2a07f5c2c1aa 100644 --- a/docs/src/reference/experimental/loop-contracts.md +++ b/docs/src/reference/experimental/loop-contracts.md @@ -139,13 +139,36 @@ In proof path 1, we prove properties inside the loop and at last check that the In proof path 2, we prove properties after leaving the loop. As we leave the loop only when the loop guard is violated, the post condition of the loop can be expressed as `!guard && inv`, which is `x <= 1 && x >= 1` in the example. The postcondition implies `x == 1`—the property we want to prove at the end of `simple_loop_with_loop_contracts`. +## Loop contracts inside functions with contracts +Kani supports using loop contracts together with function contracts, as demonstrated in the following example: +``` Rust +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +#[kani::requires(i>=2)] +#[kani::ensures(|ret| *ret == 2)] +pub fn has_loop(mut i: u16) -> u16 { + #[kani::loop_invariant(i>=2)] + while i > 2 { + i = i - 1 + } + i +} + +#[kani::proof_for_contract(has_loop)] +fn contract_proof() { + let i: u16 = kani::any(); + let j = has_loop(i); +} +``` +When loop contracts and function contracts are both enabled (by flags `-Z loop-contracts -Z function-contracts`), +Kani automatically contracts (instead of unwinds) all loops in the functions that we want to prove contracts for. ## Limitations Loop contracts comes with the following limitations. -1. Only `while` loops are supported. The other three kinds of loops are not supported: [`loop` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#infinite-loops) - , [`while let` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#predicate-pattern-loops), and [`for` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#iterator-loops). +1. `while` loops and `loop` loops are supported. The other kinds of loops are not supported: [`while let` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#predicate-pattern-loops), and [`for` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#iterator-loops). 2. Kani infers *loop modifies* with alias analysis. Loop modifies are those variables we assume to be arbitrary in the inductive hypothesis, and should cover all memory locations that are written to during the execution of the loops. A proof will fail if the inferred loop modifies misses some targets written in the loops. We observed this happens when some fields of structs are modified by some other functions called in the loops.