Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Function Contracts: remove instances of _renamed #3274

Merged
merged 1 commit into from
Jun 19, 2024
Merged

Function Contracts: remove instances of _renamed #3274

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 2 additions & 4 deletions library/kani_macros/src/sysroot/contracts/check.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,14 +34,12 @@ impl<'a> ContractConditionsHandler<'a> {
)
}
ContractConditionsData::Ensures { attr } => {
let (arg_copies, copy_clean, ensures_clause) =
build_ensures(&self.annotated_fn.sig, attr);
let (remembers, ensures_clause) = build_ensures(attr);

// The code that enforces the postconditions and cleans up the shallow
// argument copies (with `mem::forget`).
let exec_postconditions = quote!(
kani::assert(#ensures_clause, stringify!(#attr_copy));
#copy_clean
);

assert!(matches!(
Expand All @@ -52,7 +50,7 @@ impl<'a> ContractConditionsHandler<'a> {

let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
quote!(
#arg_copies
#remembers
#(#inner)*
#exec_postconditions
#result
Expand Down
70 changes: 46 additions & 24 deletions library/kani_macros/src/sysroot/contracts/mod.rs
View file
Open in desktop
pi314mm marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
Expand Up @@ -242,8 +242,7 @@
//! state. Each occurrence of `old` is lifted, so is is necessary that
//! each lifted occurrence is closed with respect to the function arguments.
//! The results of these old computations are placed into
//! `remember_kani_internal_XXX` variables of incrementing index to avoid
//! collisions of variable names. Consider the following example:
//! `remember_kani_internal_XXX` variables which are hashed. Consider the following example:
//!
//! ```
//! #[kani::ensures(|result| old(*ptr + 1) == *ptr)]
Expand All @@ -265,50 +264,73 @@
//! This expands to
//!
//! ```
//! #[kanitool::checked_with = "modify_recursion_wrapper_633496"]
//! #[kanitool::replaced_with = "modify_replace_633496"]
//! #[kanitool::inner_check = "modify_wrapper_633496"]
//! fn modify(ptr: &mut u32) { { *ptr += 1; } }
//! #[allow(dead_code, unused_variables, unused_mut)]
//! #[kanitool::is_contract_generated(recursion_wrapper)]
//! fn modify_recursion_wrapper_633496(arg0: &mut u32) {
//! static mut REENTRY: bool = false;
//! if unsafe { REENTRY } {
//! modify_replace_633496(arg0)
//! } else {
//! unsafe { REENTRY = true };
//! let result_kani_internal = modify_check_633496(arg0);
//! unsafe { REENTRY = false };
//! result_kani_internal
//! }
//! }
//! #[allow(dead_code, unused_variables, unused_mut)]
//! #[kanitool::is_contract_generated(check)]
//! fn modify_check_633496(ptr: &mut u32) {
//! let _wrapper_arg_1 =
//! unsafe { kani::internal::Pointer::decouple_lifetime(&ptr) };
//! kani::assume(*ptr < 100);
//! let remember_kani_internal_1 = *ptr + 1;
//! let ptr_renamed = kani::internal::untracked_deref(&ptr);
//! let remember_kani_internal_0 = *ptr + 1;
//! let ptr_renamed = kani::internal::untracked_deref(&ptr);
//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
//! let result_kani_internal: () = modify_wrapper_633496(ptr, _wrapper_arg_1);
//! kani::assert((|result|
//! (remember_kani_internal_0) ==
//! *ptr_renamed)(&result_kani_internal),
//! (remember_kani_internal_92cc419d8aca576c) ==
//! *ptr)(&result_kani_internal),
//! "|result| old(*ptr + 1) == *ptr");
//! std::mem::forget(ptr_renamed);
//! kani::assert((|result|
//! (remember_kani_internal_1) ==
//! *ptr_renamed)(&result_kani_internal),
//! (remember_kani_internal_92cc419d8aca576c) ==
//! *ptr)(&result_kani_internal),
//! "|result| old(*ptr + 1) == *ptr");
//! std::mem::forget(ptr_renamed);
//! result_kani_internal
//! }
//! #[allow(dead_code, unused_variables, unused_mut)]
//! #[kanitool::is_contract_generated(replace)]
//! fn modify_replace_633496(ptr: &mut u32) {
//! kani::assert(*ptr < 100, "*ptr < 100");
//! let remember_kani_internal_1 = *ptr + 1;
//! let ptr_renamed = kani::internal::untracked_deref(&ptr);
//! let remember_kani_internal_0 = *ptr + 1;
//! let ptr_renamed = kani::internal::untracked_deref(&ptr);
//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
pi314mm marked this conversation as resolved.
Show resolved Hide resolved
//! let result_kani_internal: () = kani::any_modifies();
//! *unsafe { kani::internal::Pointer::assignable(ptr) } =
//! kani::any_modifies();
//! *unsafe {
pi314mm marked this conversation as resolved.
Show resolved Hide resolved
//! kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr)))
//! } = kani::any_modifies();
//! kani::assume((|result|
//! (remember_kani_internal_0) ==
//! *ptr_renamed)(&result_kani_internal));
//! std::mem::forget(ptr_renamed);
//! (remember_kani_internal_92cc419d8aca576c) ==
//! *ptr)(&result_kani_internal));
//! kani::assume((|result|
//! (remember_kani_internal_1) ==
//! *ptr_renamed)(&result_kani_internal));
//! std::mem::forget(ptr_renamed);
//! (remember_kani_internal_92cc419d8aca576c) ==
//! *ptr)(&result_kani_internal));
//! result_kani_internal
//! }
//! #[kanitool::modifies(_wrapper_arg_1)]
//! #[allow(dead_code, unused_variables, unused_mut)]
//! #[kanitool::is_contract_generated(wrapper)]
//! fn modify_wrapper_633496<'_wrapper_arg_1,
//! WrapperArgType1>(ptr: &mut u32, _wrapper_arg_1: &WrapperArgType1) {
//! *ptr += 1;
//! }
//! #[allow(dead_code)]
//! #[kanitool::proof_for_contract = "modify"]
//! fn main() {
//! kani::internal::init_contracts();
//! { let mut i = kani::any(); modify(&mut i); }
//! }
//! ```

use proc_macro::TokenStream;
Expand Down
8 changes: 3 additions & 5 deletions library/kani_macros/src/sysroot/contracts/replace.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,23 +80,21 @@ impl<'a> ContractConditionsHandler<'a> {
)
}
ContractConditionsData::Ensures { attr } => {
let (arg_copies, copy_clean, ensures_clause) =
build_ensures(&self.annotated_fn.sig, attr);
let (remembers, ensures_clause) = build_ensures(attr);
let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
quote!(
#arg_copies
#remembers
#(#before)*
#(#after)*
kani::assume(#ensures_clause);
#copy_clean
#result
)
}
ContractConditionsData::Modifies { attr } => {
let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
quote!(
#(#before)*
#(*unsafe { kani::internal::Pointer::assignable(#attr) } = kani::any_modifies();)*
#(*unsafe { kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(#attr))) } = kani::any_modifies();)*
#(#after)*
#result
)
Expand Down
116 changes: 7 additions & 109 deletions library/kani_macros/src/sysroot/contracts/shared.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,14 +7,13 @@
//! This is so we can keep [`super`] distraction-free as the definitions of data
//! structures and the entry point for contract handling.

use std::collections::{HashMap, HashSet};
use std::collections::HashMap;

use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
use quote::{quote, ToTokens};
use std::hash::{DefaultHasher, Hash, Hasher};
use syn::{
spanned::Spanned, visit::Visit, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure,
ExprPath, Path,
spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, Path,
};

use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT};
Expand Down Expand Up @@ -102,26 +101,6 @@ pub fn identifier_for_generated_function(
Ident::new(&identifier, proc_macro2::Span::mixed_site())
}

/// We make shallow copies of the argument for the postconditions in both
/// `requires` and `ensures` clauses and later clean them up.
///
/// This function creates the code necessary to both make the copies (first
/// tuple elem) and to clean them (second tuple elem).
pub fn make_unsafe_argument_copies(
renaming_map: &HashMap<Ident, Ident>,
) -> (TokenStream2, TokenStream2) {
let arg_names = renaming_map.values();
let also_arg_names = renaming_map.values();
let arg_values = renaming_map.keys();
(
quote!(#(let #arg_names = kani::internal::untracked_deref(&#arg_values);)*),
#[cfg(not(feature = "no_core"))]
quote!(#(std::mem::forget(#also_arg_names);)*),
#[cfg(feature = "no_core")]
quote!(#(core::mem::forget(#also_arg_names);)*),
)
}

/// Used as the "single source of truth" for [`try_as_result_assign`] and [`try_as_result_assign_mut`]
/// since we can't abstract over mutability. Input is the object to match on and the name of the
/// function used to convert an `Option<LocalInit>` into the result type (e.g. `as_ref` and `as_mut`
Expand Down Expand Up @@ -184,28 +163,20 @@ pub fn try_as_result_assign_mut(stmt: &mut syn::Stmt) -> Option<&mut syn::LocalI
/// When a `#[kani::ensures(|result|expr)]` is expanded, this function is called on with `build_ensures(|result|expr)`.
/// This function goes through the expr and extracts out all the `old` expressions and creates a sequence
/// of statements that instantiate these expressions as `let remember_kani_internal_x = old_expr;`
/// where x is a unique hash. This is returned as the first return parameter along with changing all the
/// variables to `_renamed`. The second parameter is the closing of all the unsafe argument copies. The third
/// return parameter is the expression formed by passing in the result variable into the input closure and
/// changing all the variables to `_renamed`.
pub fn build_ensures(
fn_sig: &syn::Signature,
data: &ExprClosure,
) -> (TokenStream2, TokenStream2, Expr) {
/// where x is a unique hash. This is returned as the first return parameter. The second
/// return parameter is the expression formed by passing in the result variable into the input closure.
pub fn build_ensures(data: &ExprClosure) -> (TokenStream2, Expr) {
let mut remembers_exprs = HashMap::new();
let mut vis = OldVisitor { t: OldLifter::new(), remembers_exprs: &mut remembers_exprs };
let mut expr = &mut data.clone();
vis.visit_expr_closure_mut(&mut expr);

let arg_names = rename_argument_occurrences(fn_sig, &mut expr);
let (start, end) = make_unsafe_argument_copies(&arg_names);

let remembers_stmts: TokenStream2 = remembers_exprs
.iter()
.fold(start, |collect, (ident, expr)| quote!(let #ident = #expr; #collect));
.fold(quote!(), |collect, (ident, expr)| quote!(let #ident = #expr; #collect));

let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
(remembers_stmts, end, Expr::Verbatim(quote!((#expr)(&#result))))
(remembers_stmts, Expr::Verbatim(quote!((#expr)(&#result))))
}

trait OldTrigger {
Expand Down Expand Up @@ -304,76 +275,3 @@ impl OldTrigger for OldLifter {
true
}
}

/// A supporting function for creating shallow, unsafe copies of the arguments
/// for the postconditions.
///
/// This function:
/// - Collects all [`Ident`]s found in the argument patterns;
/// - Creates new names for them;
/// - Replaces all occurrences of those idents in `attrs` with the new names and;
/// - Returns the mapping of old names to new names.
fn rename_argument_occurrences(
sig: &syn::Signature,
attr: &mut ExprClosure,
) -> HashMap<Ident, Ident> {
let mut arg_ident_collector = ArgumentIdentCollector::new();
arg_ident_collector.visit_signature(&sig);

let mk_new_ident_for = |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site());
let arg_idents = arg_ident_collector
.0
.into_iter()
.map(|i| {
let new = mk_new_ident_for(&i);
(i, new)
})
.collect::<HashMap<_, _>>();

let mut ident_rewriter = Renamer(&arg_idents);
ident_rewriter.visit_expr_closure_mut(attr);
arg_idents
}

/// Collect all named identifiers used in the argument patterns of a function.
struct ArgumentIdentCollector(HashSet<Ident>);

impl ArgumentIdentCollector {
fn new() -> Self {
Self(HashSet::new())
}
}

impl<'ast> Visit<'ast> for ArgumentIdentCollector {
fn visit_pat_ident(&mut self, i: &'ast syn::PatIdent) {
self.0.insert(i.ident.clone());
syn::visit::visit_pat_ident(self, i)
}
fn visit_receiver(&mut self, _: &'ast syn::Receiver) {
self.0.insert(Ident::new("self", proc_macro2::Span::call_site()));
}
}

/// Applies the contained renaming (key renamed to value) to every ident pattern
/// and ident expr visited.
struct Renamer<'a>(&'a HashMap<Ident, Ident>);

impl<'a> VisitMut for Renamer<'a> {
fn visit_expr_path_mut(&mut self, i: &mut syn::ExprPath) {
if i.path.segments.len() == 1 {
i.path
.segments
.first_mut()
.and_then(|p| self.0.get(&p.ident).map(|new| p.ident = new.clone()));
}
}

/// This restores shadowing. Without this we would rename all ident
/// occurrences, but not rebinding location. This is because our
/// [`Self::visit_expr_path_mut`] is scope-unaware.
fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) {
if let Some(new) = self.0.get(&i.ident) {
i.ident = new.clone();
}
}
}
6 changes: 3 additions & 3 deletions tests/expected/function-contract/modifies/field_replace_pass.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ struct S<'a> {
#[kani::requires(*s.target < 100)]
#[kani::modifies(s.target)]
#[kani::ensures(|result| *s.target == prior + 1)]
fn modify(s: S, prior: u32) {
fn modify(s: &mut S, prior: u32) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why are you changing this?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The test originally did not make sense as the S struct gets consumed by the modify function and so you cannot refer to the contents of it within the ensures. The test originally passed unsafely as it ignored the fact that it referred to a potentially deallocated memory address. Changing it to a pass by reference is better than deleting the test.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did the test break with your changes? I still believe we need tests to capture what the behavior would be here. Broken tests should trigger an error, not deleted since a user could make the same mistake

Copy link
Contributor Author

@pi314mm pi314mm Jun 19, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The test broke, but error cannot be represented within the current expected test framework because valid rust code is not produced after the macro expansion, so the kani compilation fails. In other words, it broke before we could check if it breaks. To include this failing test case, the harness for expected needs to be changed.

Basically, the test case expands to something like

modify(s, prior); // s is consumed here
kani::assert(*s.target == prior + 1, "*s.target == prior + 1"); // s is used here after it is consumed

which is definitely not valid Rust code, and kani is unable to compile it, and the expected test fails even with the error message being included into the .expected file.

A better test case that is now fixed by this code change was mentioned in the issue #3239

#[derive(Clone,Copy)]
struct Five;

impl Five {
    fn five(self : &Five) -> u32{
        5
    }
}

#[kani::ensures(|result : &Five| x.five() == result.five())]
fn id(x : Five) -> Five {
    x
}

#[kani::proof_for_contract(id)]
fn eat_harness() {
    let x = Five;
    id(x);
}

If you leave the copy/clone line, the test works (did not work before this change). If you delete the copy/clone line, you get the following error

error[E0382]: borrow of moved value: `x`
  --> ../test.rs:9:17
   |
9  | #[kani::ensures(|result : &Five| x.five() == result.five())]
   |                 ^^^^^^^^^^^^^^^^ - borrow occurs due to use in closure
   |                 |
   |                 value borrowed here after move
10 | fn id(x : Five) -> Five {
   |       -
   |       |
   |       value moved here
   |       move occurs because `x` has type `Five`, which does not implement the `Copy` trait
   |
note: consider changing this parameter type in function `id_wrapper_8110d0` to borrow instead if owning the value isn't necessary
  --> ../test.rs:10:11
   |
9  | #[kani::ensures(|result : &Five| x.five() == result.five())]
   | ------------------------------------------------------------ in this function
10 | fn id(x : Five) -> Five {
   |           ^^^^ this parameter takes ownership of the value
note: if `Five` implemented `Clone`, you could clone the value
  --> ../test.rs:1:1
   |
1  | struct Five;
   | ^^^^^^^^^^^ consider implementing `Clone` for this type
...
10 | fn id(x : Five) -> Five {
   |       - you could clone this value

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We usually use the ui suite to ensure compilation errors are user friendly. In this case, I would recommend to move the broken test there. Thanks

*s.target += 1;
}

Expand All @@ -20,8 +20,8 @@ fn main() {
let i_copy = i;
let mut distraction = kani::any();
let distraction_copy = distraction;
let s = S { distraction: &mut distraction, target: &mut i };
modify(s, i_copy);
let mut s = S { distraction: &mut distraction, target: &mut i };
modify(&mut s, i_copy);
kani::assert(i == i_copy + 1, "Increment");
kani::assert(distraction == distraction_copy, "Unchanged");
}
Loading