Add loop-contracts support for for loop

docs/src/reference/experimental/loop-contracts.md

@@ -168,7 +168,7 @@ Kani automatically contracts (instead of unwinds) all loops in the functions tha
 
 Loop contracts comes with the following limitations.
 
-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).
+1. `while` loops, `loop` loops are supported. `for` loops are supported for array, slice, Iter, Vec, Range, StepBy, Chain, Zip, Map, and Enumerate. The other kinds of loops are not supported: [`while let` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#predicate-pattern-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.

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

@@ -324,7 +324,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::CopyForDeref(rplace) => {
+                            Rvalue::Ref(_,_,rplace) | Rvalue::CopyForDeref(rplace) | Rvalue::Use(Operand::Copy(rplace)) => {
                                 if supported_vars.contains(&rplace.local) {
                                     supported_vars.push(place.local);
                                 } }

library/kani/src/iter.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This macro generates implementations of the `KaniIntoIter` trait for various common types that are used in `for` loops.
+//! We use this trait to overwrite the Rust IntoIter trait to reduce call stacks and avoid complicated loop invariant specifications,
+//! while maintaining the semantics of the loop.
+use crate::{KaniIntoIter, KaniPtrIter};
+
+impl<T: Copy> KaniIntoIter for Vec<T> {
+    type Iter = KaniPtrIter<T>;
+    fn kani_into_iter(self) -> Self::Iter {
+        let s = self.iter();
+        KaniPtrIter::new(s.as_slice().as_ptr(), s.len())
+    }
+}

library/kani/src/lib.rs

@@ -31,6 +31,7 @@ pub mod bounded_arbitrary;
 mod concrete_playback;
 pub mod futures;
 pub mod invariant;
+pub mod iter;
 pub mod shadow;
 pub mod vec;