Loop Contracts Annotation for While-Loop

[qinheping]

This PR introduce the loop contracts annotation for while-loops using proc-macro.
The A while loop of the form

#[kani::loop_invariant(inv)]
while guard {
   body
}

is annotated as

#[inline(never)]
#[kanitool::fn_marker = "kani_register_loop_contract"]
const fn kani_register_loop_contract_id<T, F: FnOnce() -> T>(f: F) -> T {
   unreachable!()
}
let kani_loop_invariant = || -> bool {inv};
kani_register_loop_contract_id(kani_loop_invariant)
while guard {
   loop_body;
   kani_register_loop_contract_id(||->bool{true});
}

We then replace the function body of the register function kani_register_loop_contract_id by a call to its function argument f.

There are two calls to the register function, an actual with loop invariant closure as its argument, and a dummy one with dummy argument to bypass borrow checking. We later remove the dummy call and move the actual call to the position of the dummy call during MIR transformation.

At the end, the call to the register function will be codegened as backward goto with loop contracts annotated.

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

[celinval]

I think I'm missing the big picture here, since the PR itself is currently a no-op and the attribute itself has no documentation.

[adpaco-aws]

It's looking good but I'm also missing the big picture when it comes to

• the general approach to loop invariants - are we planning on doing the same for for loops?
• the code generation for invariant/latch blocks - do you describe this transformation in the RFC?
• postprocessing of reachability checks - not sure what's being done or why it's needed

[qinheping]

@celinval @feliperodri , I refactored the implementation with closure. It is ready for review now.

[celinval]

@celinval @feliperodri , I refactored the implementation with closure. It is ready for review now.

Can you please update the description of the PR with an overview of the approach you implemented? Thanks

[celinval]

This is awesome! Looking forward to merging this!

[celinval]

wait, why do you register a dummy closure down here?

I think we want to redefine the closure so it captures the arguments again and don't violate the borrow checker. Something like:

let kani_loop_invariant_entry = || -> bool {inv};
kani_register_loop_contract(kani_loop_invariant_entry)
while guard {
    loop_body;
    let kani_loop_invariant_latch = || -> bool {inv};
    kani_register_loop_contract(kani_loop_invariant_latch);
}

[qinheping]

The idea of this implementation (and also the loop contracts in CBMC) is that we want to use one single expression as the loop invariants, and let CBMC do the transformation: rewrite loop to if, duplicate the loop invariant (check and induction assumption) to the entry of the loop as base case, instrument havocing instructions after the induction assumption, and check the loop invariant at the end of the loop.

The one single loop invariant expression in my mind should be kani_loop_invariant which is || -> bool {inv}. As it will be called before the entry of the loop after the transformation, it should be assigned before the loop. However, without dummy call, expanding the macro in the following way will violate the borrow check.

let kani_loop_invariant = || -> bool {inv};
while guard {
    loop_body;
    kani_register_loop_contract(kani_loop_invariant);
}

So I choose to use a dummy call as a place holder and later replace it with the actual call during MIR transform.

[celinval]

don't we need to check the invariant before the loop entry?

[qinheping]

We annotate the loop invariants in the loop latch goto and let CBMC instrument the checks.

[celinval]

This could break the aliasing and ownership model.

[qinheping]

I understand that it will violate the borrow check in Rust. But is it also a problem if we do it in MIR level?

[celinval]

Why is that?

[qinheping]

Because loop contracts now are wrapped in a closure which will be a side-effect expression in CBMC even they may not contain side-effect. So we disable the side-effect check for now and will implement a better check instead of simply rejecting function calls and statement expressions.
diffblue/cbmc#8393

[celinval]

Please add the link.

BTW, will this enable the entire flow where a loop is checked and later replaced?

[qinheping]

Yes, this will enable the entire flow. The two test cases run with loop contracts enable, where the running time is only ~1 seconds comparing to timeout when running without loop contracts

[celinval]

This transformation seems very CBMC specific. I wonder if we should make this more explicit here. @zhassan-aws any thoughts on how would loop invariant be handled with the Aeneas backend?

[qinheping]

@celinval
I modified the description and addressed most of the comments. The one I am not sure about is will the MIR transform break aliasing and ownership model?

Thank you!