Addressing code review

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -260,33 +260,7 @@ impl<'tcx> GotocCtx<'tcx> {
  let goto_contract = self.as_goto_contract(contract);
  let name = self.current_fn().name();
 
- // CBMC has two ways of attaching the contract and it seems the
- // difference is whether dfcc is used or not. With dfcc it's stored in
- // `contract::<fn name>`, otherwise directly on the type of the
- // function.
- //
- // Actually the issue sees to haver been something else and ataching to
- // the symbol directly seems ot also work if dfcc is used.
- let create_separate_contract_sym = false;
-
- let contract_target_name = if create_separate_contract_sym {
- let contract_sym_name = format!("contract::{}", name);
- self.ensure(&contract_sym_name, |ctx, fname| {
- Symbol::function(
- fname,
- ctx.fn_typ(),
- None,
- format!("contract::{}", ctx.current_fn().readable_name()),
- ctx.codegen_span(&ctx.current_fn().mir().span),
- )
- .with_is_property(true)
- });
- contract_sym_name
- } else {
- name
- };
-
- self.symbol_table.attach_contract(contract_target_name, goto_contract);
+ self.symbol_table.attach_contract(name, goto_contract);
  self.reset_current_fn()
  }
 

kani-compiler/src/kani_middle/attributes.rs

@@ -58,7 +58,16 @@ enum KaniAttributeKind {
  /// Attribute on a function that was auto-generated from expanding a
  /// function contract.
  IsContractGenerated,
+ /// Identifies a set of pointer arguments that should be added to the write
+ /// set when checking a function contract. Placed on the inner check function.
+ ///
+ /// Emitted by the expansion of a `modifies` function contract clause.
  Modifies,
+ /// A function used as the inner code of a contract check.
+ ///
+ /// Contains the original body of the contracted function. The signature is
+ /// expanded with additional pointer arguments that are not used in the function
+ /// but referenced by the `modifies` annotation.
  InnerCheck,
 }
 

tests/expected/function-contract/modifies/expr_pass.rs

@@ -2,6 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
+// Test that a modifies clause works when a (function call)
+// expression is provided
+
 #[kani::requires(**ptr < 100)]
 #[kani::modifies(ptr.as_ref())]
 fn modify(ptr: &mut Box<u32>) {

tests/expected/function-contract/modifies/expr_replace_fail.rs

@@ -2,6 +2,10 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
+// Tests that providing the "modifies" clause havocks the pointer such
+// that the increment can no longer be observed (in the absence of an
+// "ensures" clause)
+
 #[kani::requires(**ptr < 100)]
 #[kani::modifies(ptr.as_ref())]
 fn modify(ptr: &mut Box<u32>) {

tests/expected/function-contract/modifies/expr_replace_pass.rs

@@ -4,7 +4,7 @@
 
 #[kani::requires(**ptr < 100)]
 #[kani::modifies(ptr.as_ref())]
-#[kani::ensures(*ptr.as_ref() == prior + 1)]
+#[kani::ensures(**ptr == prior + 1)]
 fn modify(ptr: &mut Box<u32>, prior: u32) {
  *ptr.as_mut() += 1;
 }

tests/expected/function-contract/modifies/havoc_pass.rs

@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-// These two are reordered in comparison to `havoc_pass` and we expect the test case to pass still
 #[kani::modifies(dst)]
 #[kani::ensures(*dst == src)]
 fn copy(src: u32, dst: &mut u32) {

tests/expected/function-contract/modifies/havoc_pass_reordered.rs

@@ -3,8 +3,8 @@
 // kani-flags: -Zfunction-contracts
 
 // These two are reordered in comparison to `havoc_pass` and we expect the test case to pass still
-#[kani::modifies(dst)]
 #[kani::ensures(*dst == src)]
+#[kani::modifies(dst)]
 fn copy(src: u32, dst: &mut u32) {
  *dst = src;
 }

tests/expected/function-contract/modifies/simple_fail.rs

@@ -9,7 +9,6 @@ fn modify(ptr: &mut u32) {
 
 #[kani::proof_for_contract(modify)]
 fn main() {
- let _ = Box::new(());
  let mut i = kani::any();
  modify(&mut i);
 }

tests/expected/function-contract/modifies/simple_pass.rs

@@ -10,7 +10,6 @@ fn modify(ptr: &mut u32) {
 
 #[kani::proof_for_contract(modify)]
 fn main() {
- let _ = Box::new(());
  let mut i = kani::any();
  modify(&mut i);
 }

tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs

@@ -9,8 +9,8 @@ fn modify(v: &mut Vec<u32>, src: u32) {
  v[0] = src
 }
 
-#[kani::unwind(10)]
-#[kani::proof_for_contract(modify)]
+//#[kani::unwind(10)]
+//#[kani::proof_for_contract(modify)]
 fn main() {
  let v_len = kani::any_where(|i| *i < 4);
  let mut v: Vec<u32> = vec![kani::any()];
@@ -24,23 +24,11 @@ fn main() {
 #[kani::proof]
 #[kani::stub_verified(modify)]
 fn modify_replace() {
- let v_len : usize = kani::any_where(|i| *i < 4);
- let mut v: Vec<u32> = Vec::with_capacity(v_len + 1);
- v.push(kani::any());
- let mut compare = Vec::with_capacity(v_len);
- for _ in 0..v_len {
- let elem = kani::any();
- v.push(elem);
- compare.push(elem);
- }
+ let v_len = kani::any_where(|i| *i < 4 && *i > 0);
+ let mut v: Vec<u32> = vec![kani::any(); v_len].to_vec();
+ let compare = v[1..].to_vec();
  let src = kani::any();
  modify(&mut v, src);
- kani::assert(
- v[0] == src,
- "element set"
- );
- kani::assert(
- v[1..] == compare[..],
- "vector tail equality"
- );
+ kani::assert(v[0] == src, "element set");
+ kani::assert(compare == v[1..v_len], "vector tail equality");
 }