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.

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

Enable an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros #3283

Merged
merged 38 commits into from
Jul 22, 2024
Merged
Show file tree
Hide file tree
Changes from 32 commits
Commits
Show all changes
38 commits
Select commit Hold shift + click to select a range
294c9e1
Add helper attribute for `Invariant` derive macro
adpaco-aws Jun 21, 2024
e6a966e
Add `expected` & `ui` tests
adpaco-aws Jun 21, 2024
846a248
Merge branch 'main' into derive-invariant-2
adpaco-aws Jun 21, 2024
d8a64a9
Newlines
adpaco-aws Jun 21, 2024
b1c9071
Another newline
adpaco-aws Jun 21, 2024
b0f6adc
remove problematic lines
adpaco-aws Jun 21, 2024
3143d82
Use references for expressions (`Invariant` needs fix)
adpaco-aws Jun 28, 2024
7beec3e
Fixed generation for `Invariant`
adpaco-aws Jun 28, 2024
a6fa7ee
Apply fixes for format
adpaco-aws Jun 28, 2024
ad2da6f
Some refactoring and documentation
adpaco-aws Jun 28, 2024
4c749ec
Refactor using `extract_expr`
adpaco-aws Jun 28, 2024
29aee75
Document remaining funs
adpaco-aws Jun 28, 2024
adacc40
Move inner funs around
adpaco-aws Jun 28, 2024
6cc81f5
Merge branch 'main' into derive-invariant-2
adpaco-aws Jun 28, 2024
79350dc
Fix bug and all tests
adpaco-aws Jun 28, 2024
0c686ba
Add new test for `Arbitrary`-only invariant behavior
adpaco-aws Jun 28, 2024
43c1d79
remove location line from tests
adpaco-aws Jun 28, 2024
d13015f
Add newline on `expected` test
adpaco-aws Jul 8, 2024
ccf3cf6
Add test with functions
adpaco-aws Jul 8, 2024
07bf2a1
Add test where invariant is violated thru mut
adpaco-aws Jul 8, 2024
98504be
minor comment revision
adpaco-aws Jul 8, 2024
bac08cb
Better handling of error messages
adpaco-aws Jul 8, 2024
ea52605
Merge branch 'main' into derive-invariant-2
adpaco-aws Jul 8, 2024
08ffc4d
Always check `is_safe()` for each field
adpaco-aws Jul 17, 2024
6722aae
Add documentation for traits
adpaco-aws Jul 17, 2024
f42e724
`#[invariant(...)]` -> `#[safety_constraint(...)]`
adpaco-aws Jul 17, 2024
ca962ed
Merge branch 'main' into derive-invariant-2
adpaco-aws Jul 17, 2024
b6ec5b9
Missing important rename
adpaco-aws Jul 17, 2024
c3fc474
Fix helper pick-up and rename tests
adpaco-aws Jul 18, 2024
546ecf9
Merge branch 'main' into derive-invariant-2
adpaco-aws Jul 18, 2024
1a549be
Last renames
adpaco-aws Jul 18, 2024
eba5ef9
Fixes for renaming
adpaco-aws Jul 18, 2024
2e7c94c
Add two more tests
adpaco-aws Jul 22, 2024
477d9bf
Update comments so they're clear.
adpaco-aws Jul 22, 2024
11e5597
Updated UI tests to not have line numbers
adpaco-aws Jul 22, 2024
05dea45
Add side-effect test
adpaco-aws Jul 22, 2024
bc3b3e9
Merge branch 'main' into derive-invariant-2
adpaco-aws Jul 22, 2024
bf93601
Remove path line
adpaco-aws Jul 22, 2024
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
202 changes: 186 additions & 16 deletions library/kani_macros/src/derive.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,11 +28,30 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok
let (impl_generics, ty_generics, where_clause) = generics.split_for_impl();

let body = fn_any_body(&item_name, &derive_item.data);
let expanded = quote! {
// The generated implementation.
impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
fn any() -> Self {
#body

// Get the safety constraints (if any) to produce type-safe values
let safety_conds_opt = safety_conds(&item_name, &derive_item.data);

let expanded = if let Some(safety_cond) = safety_conds_opt {
let field_refs = field_refs(&item_name, &derive_item.data);
quote! {
// The generated implementation.
impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
fn any() -> Self {
let obj = #body;
#field_refs
kani::assume(#safety_cond);
obj
}
}
}
} else {
quote! {
// The generated implementation.
impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
fn any() -> Self {
#body
}
}
}
};
Expand Down Expand Up @@ -75,6 +94,103 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream {
}
}

/// Parse the condition expressions in `#[safety_constraint(<cond>)]` attached to struct
/// fields and, it at least one was found, generate a conjunction to be assumed.
///
/// For example, if we're deriving implementations for the struct
/// ```
/// #[derive(Arbitrary)]
/// #[derive(Invariant)]
/// struct PositivePoint {
/// #[safety_constraint(*x >= 0)]
/// x: i32,
/// #[safety_constraint(*y >= 0)]
/// y: i32,
/// }
/// ```
/// this function will generate the `TokenStream`
/// ```
/// *x >= 0 && *y >= 0
/// ```
/// which can be passed to `kani::assume` to constrain the values generated
/// through the `Arbitrary` impl so that they are type-safe by construction.
fn safety_conds(ident: &Ident, data: &Data) -> Option<TokenStream> {
match data {
Data::Struct(struct_data) => safety_conds_inner(ident, &struct_data.fields),
Data::Enum(_) => None,
Data::Union(_) => None,
}
}

/// Generates an expression resulting from the conjunction of conditions
/// specified as safety constraints for each field. See `safety_conds` for more details.
fn safety_conds_inner(ident: &Ident, fields: &Fields) -> Option<TokenStream> {
match fields {
Fields::Named(ref fields) => {
let conds: Vec<TokenStream> =
fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect();
if !conds.is_empty() { Some(quote! { #(#conds)&&* }) } else { None }
}
Fields::Unnamed(_) => None,
Fields::Unit => None,
}
}

/// Generates the sequence of expressions to initialize the variables used as
/// references to the struct fields.
///
/// For example, if we're deriving implementations for the struct
/// ```
/// #[derive(Arbitrary)]
/// #[derive(Invariant)]
/// struct PositivePoint {
/// #[safety_constraint(*x >= 0)]
/// x: i32,
/// #[safety_constraint(*y >= 0)]
/// y: i32,
/// }
/// ```
/// this function will generate the `TokenStream`
/// ```
/// let x = &obj.x;
/// let y = &obj.y;
/// ```
/// which allows us to refer to the struct fields without using `self`.
/// Note that the actual stream is generated in the `field_refs_inner` function.
fn field_refs(ident: &Ident, data: &Data) -> TokenStream {
match data {
Data::Struct(struct_data) => field_refs_inner(ident, &struct_data.fields),
Data::Enum(_) => unreachable!(),
Data::Union(_) => unreachable!(),
}
}

/// Generates the sequence of expressions to initialize the variables used as
/// references to the struct fields. See `field_refs` for more details.
fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
match fields {
Fields::Named(ref fields) => {
let field_refs: Vec<TokenStream> = fields
.named
.iter()
.map(|field| {
let name = &field.ident;
quote_spanned! {field.span()=>
let #name = &obj.#name;
}
})
.collect();
if !field_refs.is_empty() {
quote! { #( #field_refs )* }
} else {
quote! {}
}
}
Fields::Unnamed(_) => quote! {},
Fields::Unit => quote! {},
}
}

/// Generate an item initialization where an item can be a struct or a variant.
/// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }`
/// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)`
Expand Down Expand Up @@ -115,6 +231,42 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream {
}
}

/// Extract, parse and return the expression `cond` (i.e., `Some(cond)`) in the
/// `#[safety_constraint(<cond>)]` attribute helper associated with a given field.
/// Return `None` if the attribute isn't specified.
fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option<TokenStream> {
let name = &field.ident;
let mut safety_helper_attr = None;

// Keep the helper attribute if we find it
for attr in &field.attrs {
if attr.path().is_ident("safety_constraint") {
safety_helper_attr = Some(attr);
}
}

// Parse the arguments in the `#[safety_constraint(...)]` attribute
if let Some(attr) = safety_helper_attr {
let expr_args: Result<syn::Expr, syn::Error> = attr.parse_args();

// Check if there was an error parsing the arguments
if let Err(err) = expr_args {
abort!(Span::call_site(), "Cannot derive impl for `{}`", ident;
note = attr.span() =>
"safety constraint in field `{}` could not be parsed: {}", name.as_ref().unwrap().to_string(), err
)
}

// Return the expression associated to the safety constraint
let safety_expr = expr_args.unwrap();
Some(quote_spanned! {field.span()=>
#safety_expr
})
} else {
None
}
}

/// Generate the body of the function `any()` for enums. The cases are:
/// 1. For zero-variants enumerations, this will encode a `panic!()` statement.
/// 2. For one or more variants, the code will be something like:
Expand Down Expand Up @@ -176,10 +328,14 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok
let (impl_generics, ty_generics, where_clause) = generics.split_for_impl();

let body = is_safe_body(&item_name, &derive_item.data);
let field_refs = field_refs(&item_name, &derive_item.data);

let expanded = quote! {
// The generated implementation.
impl #impl_generics kani::Invariant for #item_name #ty_generics #where_clause {
fn is_safe(&self) -> bool {
let obj = self;
#field_refs
#body
}
}
Expand All @@ -199,7 +355,7 @@ fn add_trait_bound_invariant(mut generics: Generics) -> Generics {

fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream {
match data {
Data::Struct(struct_data) => struct_safe_conjunction(ident, &struct_data.fields),
Data::Struct(struct_data) => struct_invariant_conjunction(ident, &struct_data.fields),
Data::Enum(_) => {
abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` enum", ident;
note = ident.span() =>
Expand All @@ -215,21 +371,35 @@ fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream {
}
}

/// Generates an expression that is the conjunction of `is_safe` calls for each field in the struct.
fn struct_safe_conjunction(_ident: &Ident, fields: &Fields) -> TokenStream {
/// Generates an expression that is the conjunction of safety constraints for each field in the struct.
fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream {
match fields {
// Expands to the expression
// `true && <safety_cond1> && <safety_cond2> && ..`
// where `safety_condN` is
// - `self.fieldN.is_safe() && <cond>` if a condition `<cond>` was
// specified through the `#[safety_constraint(<cond>)]` helper attribute, or
// - `self.fieldN.is_safe()` otherwise
//
// Therefore, if `#[safety_constraint(<cond>)]` isn't specified for any field, this expands to
// `true && self.field1.is_safe() && self.field2.is_safe() && ..`
Fields::Named(ref fields) => {
let safe_calls = fields.named.iter().map(|field| {
let name = &field.ident;
quote_spanned! {field.span()=>
self.#name.is_safe()
}
});
let safety_conds: Vec<TokenStream> = fields
.named
.iter()
.map(|field| {
let name = &field.ident;
let default_expr = quote_spanned! {field.span()=>
#name.is_safe()
};
parse_safety_expr(ident, field)
.map(|expr| quote! { #expr && #default_expr})
.unwrap_or(default_expr)
})
.collect();
// An initial value is required for empty structs
safe_calls.fold(quote! { true }, |acc, call| {
quote! { #acc && #call }
safety_conds.iter().fold(quote! { true }, |acc, cond| {
quote! { #acc && #cond }
})
}
Fields::Unnamed(ref fields) => {
Expand Down
112 changes: 108 additions & 4 deletions library/kani_macros/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -100,16 +100,120 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream {
attr_impl::unstable(attr, item)
}

/// Allow users to auto generate Arbitrary implementations by using `#[derive(Arbitrary)]` macro.
/// Allow users to auto generate `Arbitrary` implementations by using
/// `#[derive(Arbitrary)]` macro.
///
/// When using `#[derive(Arbitrary)]` on a struct, the `#[safety_constraint(<cond>)]`
/// attribute can be added to its fields to indicate a type safety invariant
/// condition `<cond>`. Since `kani::any()` is always expected to produce
/// type-safe values, **adding `#[safety_constraint(...)]` to any fields will further
/// constrain the objects generated with `kani::any()`**.
///
/// For example, the `check_positive` harness in this code is expected to
/// pass:
///
/// ```rs
/// #[derive(kani::Arbitrary)]
/// struct AlwaysPositive {
/// #[safety_constraint(*inner >= 0)]
/// inner: i32,
/// }
///
/// #[kani::proof]
/// fn check_positive() {
/// let val: AlwaysPositive = kani::any();
/// assert!(val.inner >= 0);
/// }
/// ```
///
/// Therefore, using the `#[safety_constraint(...)]` attribute can lead to vacuous
/// results when the values are over-constrained. For example, in this code
/// the `check_positive` harness will pass too:
///
/// ```rs
/// #[derive(kani::Arbitrary)]
/// struct AlwaysPositive {
/// #[safety_constraint(*inner >= 0 && *inner < i32::MIN)]
/// inner: i32,
/// }
///
/// #[kani::proof]
/// fn check_positive() {
/// let val: AlwaysPositive = kani::any();
/// assert!(val.inner >= 0);
/// }
/// ```
///
/// Unfortunately, we made a mistake when specifying the condition because
/// `*inner >= 0 && *inner < i32::MIN` is equivalent to `false`. This results
/// in the relevant assertion being unreachable:
///
/// ```
/// Check 1: check_positive.assertion.1
/// - Status: UNREACHABLE
/// - Description: "assertion failed: val.inner >= 0"
/// - Location: src/main.rs:22:5 in function check_positive
/// ```
///
/// As usual, we recommend users to defend against these behaviors by using
/// `kani::cover!(...)` checks and watching out for unreachable assertions in
/// their project's code.
#[proc_macro_error]
#[proc_macro_derive(Arbitrary)]
#[proc_macro_derive(Arbitrary, attributes(safety_constraint))]
pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
derive::expand_derive_arbitrary(item)
}

/// Allow users to auto generate Invariant implementations by using `#[derive(Invariant)]` macro.
/// Allow users to auto generate `Invariant` implementations by using
/// `#[derive(Invariant)]` macro.
///
/// When using `#[derive(Invariant)]` on a struct, the `#[safety_constraint(<cond>)]`
/// attribute can be added to its fields to indicate a type safety invariant
/// condition `<cond>`. This will ensure that the gets additionally checked when
/// using the `is_safe()` method generated by the `#[derive(Invariant)]` macro.
///
/// For example, the `check_positive` harness in this code is expected to
/// fail:
///
/// ```rs
/// #[derive(kani::Invariant)]
/// struct AlwaysPositive {
/// #[safety_constraint(*inner >= 0)]
/// inner: i32,
/// }
///
/// #[kani::proof]
/// fn check_positive() {
/// let val = AlwaysPositive { inner: -1 };
/// assert!(val.is_safe());
/// }
/// ```
///
/// This is not too surprising since the type safety invariant that we indicated
/// is not being taken into account when we create the `AlwaysPositive` object.
///
/// As mentioned, the `is_safe()` methods generated by the
/// `#[derive(Invariant)]` macro check the corresponding `is_safe()` method for
/// each field in addition to any type safety invariants specified through the
/// `#[safety_constraint(...)]` attribute.
///
/// For example, for the `AlwaysPositive` struct from above, we will generate
/// the following implementation:
///
/// ```rs
/// impl kani::Invariant for AlwaysPositive {
/// fn is_safe(&self) -> bool {
/// let obj = self;
/// let inner = &obj.inner;
/// true && *inner >= 0 && inner.is_safe()
/// }
/// }
/// ```
///
/// Note: the assignments to `obj` and `inner` are made so that we can treat the
/// fields as if they were references.
#[proc_macro_error]
#[proc_macro_derive(Invariant)]
#[proc_macro_derive(Invariant, attributes(safety_constraint))]
pub fn derive_invariant(item: TokenStream) -> TokenStream {
derive::expand_derive_invariant(item)
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
Check 1: check_invariant_helper_ok.assertion.1\
- Status: SUCCESS\
- Description: "assertion failed: pos_point.x >= 0"

Check 2: check_invariant_helper_ok.assertion.2\
- Status: SUCCESS\
- Description: "assertion failed: pos_point.y >= 0"

Check 1: check_invariant_helper_fail.assertion.1\
- Status: FAILURE\
- Description: "assertion failed: pos_point.x >= 0"

Check 2: check_invariant_helper_fail.assertion.2\
- Status: FAILURE\
- Description: "assertion failed: pos_point.y >= 0"

Complete - 2 successfully verified harnesses, 0 failures, 2 total.
Loading
Loading