Loop Contracts Annotation for While-Loop

[qinheping]

This PR introduce the loop contracts annotation for while-loops using proc-macro.
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!()
}
while 
kani_register_loop_contract_id(|| -> bool {inv}) && guard {
   loop_body;
}

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

In the loop-contract transformation, we move the calls to register functions to a new basic block as new loop latches and redirect all loop latches (for loops containing continue there can be multiple latches pointing to the same loop head) to the new loop latches to make sure that

1. each loop contain only one loop latch;
2. the terminator of the loop latch is a call to the register function.

In detail, we transform

loop_head_block: {
     loop_head_stmts
     _v = kani_register_loop_contract(move args) -> [return: next_idx];
}

 ...
loop_body_blocks
 ...

ori_loop_latch_block: {
     loop_latch_stmts
     goto -> loop_head_block;
}

to blocks

// loop head block
loop_head_block: {
     _v = true
     goto -> next_idx
}

...
loop_body_blocks
...

ori_loop_latch_block: {
     loop_latch_stmts
     goto -> new_loop_latch_block;
}

new_loop_latch_block: {
     _v = kani_register_loop_contract(move args) -> [return: next_idx];
}

The register functions will be transformed to

    bb0: {
        _0 = closure@fn as std::ops::FnOnce::call_once(move _1, ()) -> [return: bb1, unwind unreachable];
    }
    bb1: {
        return;
    }

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.

[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!

[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!

[celinval]

Sorry, might need to sync about this one offline. I'm not sure I understand your transformation

[celinval]

Suggested change

	const fn #register_ident<T, F: FnOnce() -> T>(f: F) -> T {
	unreachable!()
	}
	const fn #register_ident<F: FnOnce() -> bool>(_f: F) -> bool {
	unreachable!()
	}

BTW, I believe that if you take f by reference, you are able to return true here and fix #3586.

[qinheping]

I got the error error[E0493]: destructor of F cannot be evaluated at compile-time.
I think we can use the same idea of function contracts here that copy the loops when expanding the macro

let kani_loop_contract_mode = kani::internal::ORIGINAL
match kani_loop_contract_mode {
   kani::internal::loop_contract_check => #loop_with_loop_contracts_macro
   _ => #original_loop
}

And later modify the value of kani_loop_contract_mode during transformation.

But I plan to implement this after this PR.

[celinval]

What I'm saying is that the error will go away if you change it to a reference though. Something like:

        const fn #register_ident<F: FnOnce() -> bool>(_f: &F) -> bool {
            true
        }

[qinheping]

Yes, I also added two tests cases showing harness can be correctly proved when loop contracts disabled.

[celinval]

As we discussed offline, I am OK merging this just to unblock experimentation. This transformation is not sound since you are drastically moving where variables are used, and we cannot guarantee that the code does not violate the borrow checker (hence the fixme test).

Can you also please add a few more checks, including:

1. Function with multiple loops with annotations
2. Function with nested loops
3. Harness that invokes different functions that have loop contract in them
4. Test that has a loop_invariant but that does not pass -Z loop-contracts

Thanks

[celinval]

can you make it a more friendly error?

[celinval]

You can't cache this here. This object will get re-used for all body transformations. If you need to cache something that is relevant to a specific transformation, you should create a new object that only lives during the transformation of a function.

[celinval]

please document what this is actually doing.

[celinval]

What about closures (and co-routines)... won't they be ClosureDef?

[celinval]

I believe this is redundant today.

[celinval]

This should be a fixme test. Please also create an issue and add a link to it in the comments.