Add induction attribute

Signed-off-by: Felipe R. Monteiro <[email protected]>

kani-compiler/src/kani_middle/attributes.rs

@@ -70,6 +70,7 @@ enum KaniAttributeKind {
     /// expanded with additional pointer arguments that are not used in the function
     /// but referenced by the `modifies` annotation.
     InnerCheck,
+    Induction,
 }
 
 impl KaniAttributeKind {
@@ -84,6 +85,7 @@ impl KaniAttributeKind {
             | KaniAttributeKind::StubVerified
             | KaniAttributeKind::Unwind => true,
             KaniAttributeKind::Unstable
+            | KaniAttributeKind::Induction
             | KaniAttributeKind::ReplacedWith
             | KaniAttributeKind::CheckedWith
             | KaniAttributeKind::Modifies
@@ -204,6 +206,10 @@ impl<'tcx> KaniAttributes<'tcx> {
         self.map.contains_key(&KaniAttributeKind::IsContractGenerated)
     }
 
+    pub(crate) fn request_induction(&self) -> bool {
+        self.map.contains_key(&KaniAttributeKind::Induction)
+    }
+
     /// Parse and extract the `proof_for_contract(TARGET)` attribute. The
     /// returned symbol and DefId are respectively the name and id of `TARGET`,
     /// the span in the span for the attribute (contents).
@@ -320,6 +326,12 @@ impl<'tcx> KaniAttributes<'tcx> {
                         expect_no_args(self.tcx, kind, attr);
                     })
                 }
+                KaniAttributeKind::Induction => {
+                    expect_single(self.tcx, kind, &attrs);
+                    attrs.iter().for_each(|attr| {
+                        expect_no_args(self.tcx, kind, attr);
+                    })
+                }
                 KaniAttributeKind::Solver => {
                     expect_single(self.tcx, kind, &attrs);
                     attrs.iter().for_each(|attr| {
@@ -456,6 +468,7 @@ impl<'tcx> KaniAttributes<'tcx> {
         self.map.iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| {
             match kind {
                 KaniAttributeKind::ShouldPanic => harness.should_panic = true,
+                KaniAttributeKind::Induction => harness.induction = true,
                 KaniAttributeKind::Solver => {
                     harness.solver = parse_solver(self.tcx, attributes[0]);
                 }

kani-compiler/src/kani_middle/provide.rs

@@ -14,6 +14,8 @@ use rustc_middle::util::Providers;
 use rustc_middle::{mir::Body, query::queries, ty::TyCtxt};
 use stable_mir::mir::mono::MonoItem;
 
+use crate::kani_middle::KaniAttributes;
+
 /// Sets up rustc's query mechanism to apply Kani's custom queries to code from
 /// a crate.
 pub fn provide(providers: &mut Providers, queries: &QueryDb) {
@@ -60,6 +62,12 @@ fn run_kani_mir_passes<'tcx>(
     tracing::debug!(?def_id, "Run Kani transformation passes");
     let mut transformed_body = stubbing::transform(tcx, def_id, body);
     stubbing::transform_foreign_functions(tcx, &mut transformed_body);
+    if KaniAttributes::for_item(tcx, def_id).is_contract_generated()
+        && (stubbing::get_stub_key(tcx, def_id).is_some()
+            || KaniAttributes::for_item(tcx, def_id).request_induction())
+    {
+        stubbing::transform_any_modifies(tcx, &mut transformed_body);
+    }
     // This should be applied after stubbing so user stubs take precedence.
     ModelIntrinsics::run_pass(tcx, &mut transformed_body);
     tcx.arena.alloc(transformed_body)

kani-compiler/src/kani_middle/stubbing/transform.rs

@@ -20,13 +20,16 @@ use rustc_middle::ty::{self, TyCtxt};
 
 use tracing::debug;
 
-use crate::kani_middle::attributes::KaniAttributes;
-
 /// Returns the `DefId` of the stub for the function/method identified by the
 /// parameter `def_id`, and `None` if the function/method is not stubbed.
 pub fn get_stub(tcx: TyCtxt, def_id: DefId) -> Option<DefId> {
-    let mapping = get_stub_mapping(tcx)?;
-    mapping.get(&def_id).copied()
+    let stub_map = get_stub_mapping(tcx)?;
+    stub_map.get(&def_id).copied()
+}
+
+pub fn get_stub_key(tcx: TyCtxt, def_id: DefId) -> Option<DefId> {
+    let stub_map = get_stub_mapping(tcx)?;
+    stub_map.iter().find_map(|(&key, &val)| if val == def_id { Some(key) } else { None })
 }
 
 /// Returns the new body of a function/method if it has been stubbed out;
@@ -38,11 +41,8 @@ pub fn transform<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, old_body: &'tcx Body<'t
             replaced = tcx.def_path_debug_str(replacement),
             "transform"
         );
-        let mut new_body = tcx.optimized_mir(replacement).clone();
+        let new_body = tcx.optimized_mir(replacement).clone();
         if check_compatibility(tcx, def_id, old_body, replacement, &new_body) {
-            if KaniAttributes::for_item(tcx, replacement).is_contract_generated() {
-                transform_any_modifies(tcx, &mut new_body);
-            }
             return new_body;
         }
     }

kani-driver/src/metadata.rs

@@ -182,7 +182,12 @@ pub fn mock_proof_harness(
         original_file: "<unknown>".into(),
         original_start_line: 0,
         original_end_line: 0,
-        attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() },
+        attributes: HarnessAttributes {
+            unwind_value,
+            proof: true,
+            induction: false,
+            ..Default::default()
+        },
         goto_file: model_file,
         contract: Default::default(),
     }

kani_metadata/src/harness.rs

@@ -50,6 +50,8 @@ pub struct HarnessAttributes {
     pub unwind_value: Option<u32>,
     /// The stubs used in this harness.
     pub stubs: Vec<Stub>,
+    /// Whether the harness should be annotated for induction or not.
+    pub induction: bool,
 }
 
 /// The stubbing type.

library/kani_macros/Cargo.toml

@@ -16,3 +16,7 @@ proc-macro2 = "1.0"
 proc-macro-error = "1.0.4"
 quote = "1.0.20"
 syn = { version = "2.0.18", features = ["full", "visit-mut", "visit"] }
+
+[package.metadata.rust-analyzer]
+# This package uses rustc crates.
+rustc_private=true

library/kani_macros/src/lib.rs

@@ -52,6 +52,11 @@ pub fn should_panic(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::should_panic(attr, item)
 }
 
+#[proc_macro_attribute]
+pub fn induction(attr: TokenStream, item: TokenStream) -> TokenStream {
+    attr_impl::induction(attr, item)
+}
+
 /// Set Loop unwind limit for proof harnesses
 /// The attribute `#[kani::unwind(arg)]` can only be called alongside `#[kani::proof]`.
 /// arg - Takes in a integer value (u32) that represents the unwind value for the harness.
@@ -331,6 +336,7 @@ mod sysroot {
     }
 
     kani_attribute!(should_panic, no_args);
+    kani_attribute!(induction, no_args);
     kani_attribute!(solver);
     kani_attribute!(stub);
     kani_attribute!(unstable);
@@ -363,6 +369,7 @@ mod regular {
     }
 
     no_op!(should_panic);
+    no_op!(induction);
     no_op!(solver);
     no_op!(stub);
     no_op!(unstable);

tests/expected/function-contract/fail_on_two.rs

@@ -17,6 +17,7 @@
 //! contract replacement) is used we'd expect the verification to succeed.
 
 #[kani::ensures(result < 3)]
+#[kani::induction]
 fn fail_on_two(i: i32) -> i32 {
     match i {
         0 => fail_on_two(i + 1),
@@ -32,6 +33,7 @@ fn harness() {
 }
 
 #[kani::ensures(result < 3)]
+#[kani::induction]
 fn fail_on_two_in_postcondition(i: i32) -> i32 {
     let j = i + 1;
     if i < 2 { fail_on_two_in_postcondition(j) } else { j }

tests/expected/function-contract/gcd_rec_code_fail.rs

@@ -6,6 +6,7 @@ type T = u8;
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
 #[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+#[kani::induction]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
     let mut min = y;

tests/expected/function-contract/modifies/check_only_verification.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/modifies/check_only_verification.rs

@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Check that Kani does not report any error when unused modifies clauses
+//! includes objects of types that do not implement `kani::Arbitrary`.
+
+#[kani::requires(*ptr < 100)]
+#[kani::modifies(ptr)]
+#[kani::ensures(result == 100)]
+fn modify(ptr: &mut u32) -> u32 {
+    *ptr += 1;
+    *ptr
+}
+
+#[kani::requires(*ptr < 100)]
+#[kani::modifies(ptr)]
+fn wrong_modify(ptr: &mut u32) -> &'static str {
+    *ptr += 1;
+    let msg: &'static str = "done";
+    msg
+}
+
+fn use_modify(ptr: &mut u32) {
+    *ptr = 99;
+    assert!(modify(ptr) == 100);
+}
+
+#[kani::proof]
+#[kani::stub_verified(modify)]
+fn harness() {
+    let mut i = kani::any_where(|x| *x < 100);
+    use_modify(&mut i);
+}

tests/expected/function-contract/modifies/mistake_condition_return.expected

@@ -1,4 +1,3 @@
-Failed Checks: assertion failed: res == 100 \
- File: "mistake_condition_return.rs", line 31, in use_modify \
+Failed Checks: assertion failed: res == 100
 
 VERIFICATION:- FAILED