Function Contracts: Support for defining and checking requires and ensures clauses

[JustusAdam]

Description of changes:

Adds simple function contracts in the form of requires and ensures clauses to Kani.

A contract for e.g. a function f can be checked by creating a harness and adding the proof_for_contract(f) annotation.

This is the first PR of a series that implement the function contact RFC which is under review (#2620) and can be seen rendered here

Contracts as implemented here cannot satisfactorily reason about unsafe memory manipulations. It cannot reason about write sets or mutation of values (history variables). To communicate this to the user any attempt to use a contract on a function which receives *mut pointers or returning any kind of pointer (*const or *mut) will result in a compile time error.
The error is restricted to pointers, because memory validity of references is enforced by the Rust type system. The lack of capability to reason about history is an issue for &mut references, however this only makes certain policies inexpressible, whereas raw pointer manipulation causes unsoundness, since the bounds of the manipulation are not checked by this implementation.

References can technically also be abused by casting them to raw pointers inside the function, which is not checked. This would require an pass over the actual body of the function and all functions it calls. Such a check might be desirable also to catch whether static globals are manipulated.

Resolved issues:

Resolves #2596
Resolves #2595

Related RFC:

Tracking issue for function contracts #2652

Call-outs:

There are some auxiliary changes here that are not strictly necessary.

• The testing framework compiletest has been changed so that multiple "expected" tests can be located in the same directory. In this case the runner expects there to be for each testfile.rs a testfile.expected file
• KaniAttributes have been encapsulated into a struct that is exported but opaque. This is not strictly necessary for this PR, but in later contract work the attributes will need to be requeried later in the compiler which would be inefficient with the way they were previously used. This leaves two options: Expose the internal attribute map, or expose the attribute map in encapsulated fashion (which is what is done here).
• The sysroot module in kani_macros has been refactored into a new file. This is because it is significantly larger now and mostly because my editor chokes on scrolling through it otherwise (because it grays it out which I guess is bad for the rendering engine).

Testing:

• How is this change tested? A suite of "expected" test cases is provided in the "function-contract" directory

• Is this a refactor change? No

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

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

[celinval]

Thanks for doing this!

[JustusAdam]

Changing this back to a draft because I've noticed an issue with the "functions wrapping" approach. Will have to change the macro code gen a bit.

[JustusAdam]

Okay the pivot has happened. The generation algorithm has been changed and should now not exhibit the weird drop issue.

There is still a lingering drop issue where if you move a value with heap data such that it's drop gets called early it causes a double-free.

[celinval]

@JustusAdam can you please revert the changes to kani_macro/lib.rs and move the refactoring of attributes to a separate PR. It will make reviewing this PR much easier.

Even though the compiletest changes should've be a different PR, at least the changes are fairly independent from everything else, and small enough. I've reviewed them already, so I'm OK keeping them here.

[celinval]

I was reviewing the tests. They are looking good, thanks for putting the effort.

I think there are a few things that we are not covering yet, but we can leave them for a follow up PR. Things like:

• Multiple requires and ensures
• Contract doesn't get checked in regular harnesses
• Only target contract is checked in the proof_for_contract harnesses.

[JustusAdam]

That last failing check is an out-of-disk error that I don't believe these changes are responsible for.

[celinval]

That last failing check is an out-of-disk error that I don't believe these changes are responsible for.

I'm looking into that. I'll probably fix that as part of #2703

[feliperodri]

Well done! Only minor comments over documentation and clean ups.

[JustusAdam]

@feliperodri Thanks for the review. I mostly just adopted your changes but a few I voiced objections to in the comments.