Add macro expansion for function contracts.

[monal]

1. Add #[kani::requires(..)] procedural macro for specifying preconditions on functions.

   Example:

   #[kani::proof]
   #[kani::requires(x != 0)]
   fn inverse(x: i32) -> f32 {
        1 / x
   }
   

   The attribute #[kani::requires(..)] (and all other contract attributes listed below) can only to be called alongside #[kani::proof]. This ensures that the inputs are nondetted during when we check if a function satisfies its contract.

2. Add #[kani::ensures(..)] procedural macro for specifying postconditions on functions.

   Example:

   #[kani::proof]
   #[kani::ensures(ret <= 10)]
   fn saturate(x: i32) -> i32 {
        if x > 10 {
            10
        } else {
            x
        }
   }
   

   Note: ret is a special variable that represents the return value of the function.

3. Add #[kani::modifies(..)] procedural macro for specifying the write set of the function. The write set includes a comma-separated list of "targets" - which can include function parameters and global variables.

   Example:

   #[kani::proof]
   #[kani::modifies(ret <= 10)]
   fn saturate(x: i32) -> i32 {
        if x > 10 {
            10
        } else {
            x
        }
   }
   

Note: References will not be supported as a "target" in the modifies clause yet. Kani needs to support a memory predicate like CBMC's "__CPROVER_r_ok" or "__CPROVER_w_ok" first.

Consider the following example,

// DOES NOT WORK
#[kani::modifies(*r)]
fn increment(r: &mut i32) {
   *r = *r + 1;
}

During contract checking, Kani will always complain about potential null pointer dereference since it non-dets the function arguments (that is , r). To fix this, we need to automatically inject a precondition (during the macro expansion) that would say that r can be written into (it is not null). Hence, we need to support a memory predicate that talks about pointer read/write before we can support references in the modifies clause.

Finally, a function can have multiple #[kani::requires(..)], #[kani::ensures(..)], and
#[kani::modifies(..)]clauses. All these clauses together are treated as a single contract specification on the function.

During the macro expansion stage,

In the contract checking flow (that is, when Kani is called with the --check-contracts flag)

1. A requires clause gets inlined as an assume statement before the actual body of the function begins.
2. An ensures clauses gets inlined as an assert statement after the actual body of the function ends.
3. The body of the function is wrapped into a closure and called with the same function parameters. The return value is stored into a variable called ret.
4. Note: [kani::modifies(..)] gets expanded to [kanitool::modifies(..)] independently and is checked via CBMC using a contract symbol (that resides as a separate symbol in the symbol table. See CONTRACTS: store contracts in dedicated symbols diffblue/cbmc#6799).

For example,

#[kani::proof]
#[kani::requires(x != 0)]
#[kani::ensures(ret != 0 && x % ret == 0 && y % ret == 0)]
fn gcd(x : u8, y: u8) -> u8 { ... } 

becomes

#[kanitool::proof]
#[kani::ensures(ret != 0 && x % ret == 0 && y % ret == 0)]
fn gcd(x : u8, y: u8) -> u8 { 
   kani::assume(x != 0);
   fn gcd_<uuid>(x: u8, y: u8) { ... //same body }
   let ret = gcd_<uuid>(x: u8, y: u8);
   kani::assert(ret != 0 && x % ret == 0 && y % ret == 0);
   ret
} 

In the replace with contracts flow (that is, when Kani is called with the --replace-with-contracts flag)

1. A requires clause gets inlined as an assert statement before the actual body of the function begins.
2. An ensures clause gets inlined as an assume statement after the actual body of the function ends.
3. The body of the function is nondetted and a ret gets a non-deterministic value of type=return type of the function.
4. Note: [kani::modifies(..)] gets expanded to [kanitool::modifies(..)] independently and is checked via CBMC using a contract symbol (that resides as a separate symbol in the symbol table. See CONTRACTS: store contracts in dedicated symbols diffblue/cbmc#6799).

For example,

#[kani::proof]
#[kani::requires(x != 0)]
#[kani::ensures(ret != 0 && x % ret == 0 && y % ret == 0)]
fn gcd(x : u8, y: u8) -> u8 { ... } 

becomes

#[kanitool::proof]
#[kani::ensures(ret != 0 && x % ret == 0 && y % ret == 0)]
fn gcd(x : u8, y: u8) -> u8 { 
   kani::assert(x != 0);
   let ret: u8 = kani::any();
   kani::assume(ret != 0 && x % ret == 0 && y % ret == 0);
   ret
}