Add loop-contracts support for `for` loop

[thanhnguyen-aws]

This PR adds loop-contracts support for for loop for 4 types: array, slice, Iter, Vec, Range<Integer>, StepBy, Map, Chain, Zip, Enumerate.

Main ideas: for loop implementation: A for loop of the form

for pat in expr {
    body
}

is transformed into a while loop:

let kaniiter = kani::KaniIntoIter::kani_into_iter(expr); \\ init_iter_stmt
let kaniiterlen = kani::KaniIter::len(&kaniiter); \\ init_len_stmt
if kaniiterlen > 0 {
    let mut kaniindex = 0; \\ init_index_stmt
    kani::assume (kani::KaniIter::assumption(&kaniiter)); \\ iter_assume_stmt
    let pat = kani::KaniIter::first(&kaniiter); \\ init_pat_stmt
    while kaniindex < kaniiterlen {
        kani::assume (kani::KaniIter::assumption(&kaniiter)); \\ iter_assume_stmt
        let pat = kani::KaniIter::indexing(&kaniiter, kaniindex); \\ pat_assign_stmt
        kaniindex = kaniindex + 1; \\ increase_iter_stmt
        body
    }
}

Note that

1. expr's type is required to impl KaniIntoIter trait, which is the override impl of Rust's IntoIter (see library/kani_core/src/iter.rs). Reason: a) Reduce stack-call b) Avoid types that cannot be havoc effectively (user cannot state the type invariant in the loop invariant due to private fields) c) There is no generic way to handle Rust's into_iter().

2. The init_index_stmt and init_pat_stmt support writing the loop-invariant properties that involve pat and kaniindex

3. The iter_assume_stmt assumes some truths about allocation, so that the user does not need to specify them in the loop invariant

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[zhassan-aws]

Can you expand the PR description and/or the comments in library/kani_macros/src/sysroot/loop_contracts/mod.rs to explain the idea behind the implementation? It is hard to infer what this is doing just through reading the code.

[tautschnig]

The PR description says "for loop for 4 types: array, slice, Iter, Vec, Range, StepBy, Map, Chain, Zip, Enumerate." -- that's 10 items enumerated here, not 4?

[tautschnig]

A few notes from a discussion that was held out-of-band: it would be nice to have a syntax like kani::index (instead of kaniindex or kani_index) to make it entirely obvious that this isn't a user-provided variable. Apart from this, however: let's get this merged and experiment with it to see what the user experience will be like.

[rod-chapman]

Please translate and verify the inc_vector() function that I wrote here: https://github.com/rod-chapman/cbmc-examples/blob/8a708ed2f47aba237afe049e902686f2206c595a/arrays/ar.c#L315

using Kani. This should be an interesting demo that combines "for" loops with quantified invariants.

[thanhnguyen-aws]

A few notes from a discussion that was held out-of-band: it would be nice to have a syntax like kani::index (instead of kaniindex or kani_index) to make it entirely obvious that this isn't a user-provided variable. Apart from this, however: let's get this merged and experiment with it to see what the user experience will be like.

I changed it.

[rod-chapman]

Have you got my inc_vector() test case done? If so, please point me at the sources in the repo...

[thanhnguyen-aws]

Have you got my inc_vector() test case done? If so, please point me at the sources in the repo...

Hello, we are fixing some issue with using quantifiers in loop invariants. I will let you know when we finish. Thank you very much.

[zhassan-aws]

Also, can you add an example where verification fails because the invariant is not strong enough?