Skip to content

Commit

Permalink
Re-organize kani_macros lib to improve maintainability (rust-lang#2361
Browse files Browse the repository at this point in the history 
)

- Split `proc_macro` implementation into two different modules:
  - sysroot: module that ships with Kani.
  - regular: module that is compiled when Kani is imported as a regular crate.
- Provide macros to reduce code duplication.
  • Loading branch information
@celinval
celinval authored Apr 11, 2023
1 parent 3336996 commit 868b13b
Show file tree
Hide file tree
Showing 4 changed files with 160 additions and 145 deletions.
2 changes: 1 addition & 1 deletion library/kani/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,4 +12,4 @@ publish = false
kani_macros = { path = "../kani_macros" }

[features]
concrete_playback = ["kani_macros/concrete_playback"]
concrete_playback = []
3 changes: 0 additions & 3 deletions library/kani_macros/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,3 @@ proc-macro2 = "1.0"
proc-macro-error = "1.0.4"
quote = "1.0.20"
syn = { version = "1.0.98", features = ["full"] }

[features]
concrete_playback = []
293 changes: 154 additions & 139 deletions library/kani_macros/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,138 +13,44 @@ mod derive;
// proc_macro::quote is nightly-only, so we'll cobble things together instead
use proc_macro::TokenStream;
use proc_macro_error::proc_macro_error;
#[cfg(kani)]
use {
quote::quote,
syn::{parse_macro_input, ItemFn},
};

#[cfg(any(not(kani), feature = "concrete_playback"))]
#[proc_macro_attribute]
pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
// Leave the code intact, so it can be easily be edited in an IDE,
// but outside Kani, this code is likely never called.
let mut result = TokenStream::new();

result.extend("#[allow(dead_code)]".parse::<TokenStream>().unwrap());
result.extend(item);
result
// quote!(
// #[allow(dead_code)]
// $item
// )
}
#[cfg(kani_sysroot)]
use sysroot as attr_impl;

#[cfg(not(kani_sysroot))]
use regular as attr_impl;

/// Marks a Kani proof harness
///
/// For async harnesses, this will call [`kani::block_on`] (see its documentation for more information).
#[cfg(all(kani, not(feature = "concrete_playback")))]
#[proc_macro_attribute]
pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
let fn_item = parse_macro_input!(item as ItemFn);
let attrs = fn_item.attrs;
let vis = fn_item.vis;
let sig = fn_item.sig;
let body = fn_item.block;

let kani_attributes = quote!(
#[allow(dead_code)]
#[kanitool::proof]
);

assert!(attr.is_empty(), "#[kani::proof] does not take any arguments currently");

if sig.asyncness.is_none() {
// Adds `#[kanitool::proof]` and other attributes
quote!(
#kani_attributes
#(#attrs)*
#vis #sig #body
)
.into()
} else {
// For async functions, it translates to a synchronous function that calls `kani::block_on`.
// Specifically, it translates
// ```ignore
// #[kani::async_proof]
// #[attribute]
// pub async fn harness() { ... }
// ```
// to
// ```ignore
// #[kani::proof]
// #[attribute]
// pub fn harness() {
// async fn harness() { ... }
// kani::block_on(harness())
// }
// ```
assert!(
sig.inputs.is_empty(),
"#[kani::proof] cannot be applied to async functions that take inputs for now"
);
let mut modified_sig = sig.clone();
modified_sig.asyncness = None;
let fn_name = &sig.ident;
quote!(
#kani_attributes
#(#attrs)*
#vis #modified_sig {
#sig #body
kani::block_on(#fn_name())
}
)
.into()
}
attr_impl::proof(attr, item)
}

#[cfg(any(not(kani), feature = "concrete_playback"))]
#[proc_macro_attribute]
pub fn should_panic(_attr: TokenStream, item: TokenStream) -> TokenStream {
// No-op in non-kani mode
item
}

#[cfg(all(kani, not(feature = "concrete_playback")))]
/// Specifies that a proof harness is expected to panic.**
///
/// This attribute allows users to exercise *negative verification*.
/// It's analogous to how
/// [`#[should_panic]`](https://doc.rust-lang.org/rust-by-example/testing/unit_testing.html#testing-panics)
/// allows users to exercise [negative testing](https://en.wikipedia.org/wiki/Negative_testing)
/// for Rust unit tests.
///
/// # Limitations
///
/// The `#[kani::should_panic]` attribute verifies that there are one or more failed checks related to panics.
/// At the moment, it's not possible to pin it down to specific panics.
#[proc_macro_attribute]
pub fn should_panic(attr: TokenStream, item: TokenStream) -> TokenStream {
assert!(attr.is_empty(), "`#[kani::should_panic]` does not take any arguments currently");
let mut result = TokenStream::new();
let insert_string = "#[kanitool::should_panic]";
result.extend(insert_string.parse::<TokenStream>().unwrap());

result.extend(item);
result
}

#[cfg(any(not(kani), feature = "concrete_playback"))]
#[proc_macro_attribute]
pub fn unwind(_attr: TokenStream, item: TokenStream) -> TokenStream {
// When the config is not kani, we should leave the function alone
item
attr_impl::should_panic(attr, item)
}

/// Set Loop unwind limit for proof harnesses
/// The attribute '#[kani::unwind(arg)]' can only be called alongside '#[kani::proof]'.
/// arg - Takes in a integer value (u32) that represents the unwind value for the harness.
#[cfg(all(kani, not(feature = "concrete_playback")))]
#[proc_macro_attribute]
pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream {
let mut result = TokenStream::new();

// Translate #[kani::unwind(arg)] to #[kanitool::unwind(arg)]
let insert_string = "#[kanitool::unwind(".to_owned() + &attr.to_string() + ")]";
result.extend(insert_string.parse::<TokenStream>().unwrap());

result.extend(item);
result
}

#[cfg(any(not(kani), feature = "concrete_playback"))]
#[proc_macro_attribute]
pub fn stub(_attr: TokenStream, item: TokenStream) -> TokenStream {
// When the config is not kani, we should leave the function alone
item
attr_impl::unwind(attr, item)
}

/// Specify a function/method stub pair to use for proof harness
Expand All @@ -154,45 +60,154 @@ pub fn stub(_attr: TokenStream, item: TokenStream) -> TokenStream {
/// # Arguments
/// * `original` - The function or method to replace, specified as a path.
/// * `replacement` - The function or method to use as a replacement, specified as a path.
#[cfg(all(kani, not(feature = "concrete_playback")))]
#[proc_macro_attribute]
pub fn stub(attr: TokenStream, item: TokenStream) -> TokenStream {
let mut result = TokenStream::new();

// Translate #[kani::stub(original, replacement)] to #[kanitool::stub(original, replacement)]
let insert_string = "#[kanitool::stub(".to_owned() + &attr.to_string() + ")]";
result.extend(insert_string.parse::<TokenStream>().unwrap());

result.extend(item);
result
}

#[cfg(any(not(kani), feature = "concrete_playback"))]
#[proc_macro_attribute]
pub fn solver(_attr: TokenStream, item: TokenStream) -> TokenStream {
// No-op in non-kani mode
item
attr_impl::stub(attr, item)
}

/// Select the SAT solver to use with CBMC for this harness
/// The attribute `#[kani::solver(arg)]` can only be used alongside `#[kani::proof]``
///
/// arg - name of solver, e.g. kissat
#[cfg(all(kani, not(feature = "concrete_playback")))]
#[proc_macro_attribute]
pub fn solver(attr: TokenStream, item: TokenStream) -> TokenStream {
let mut result = TokenStream::new();
// Translate `#[kani::solver(arg)]` to `#[kanitool::solver(arg)]`
let insert_string = "#[kanitool::solver(".to_owned() + &attr.to_string() + ")]";
result.extend(insert_string.parse::<TokenStream>().unwrap());

result.extend(item);
result
attr_impl::solver(attr, item)
}

/// Allow users to auto generate Arbitrary implementations by using `#[derive(Arbitrary)]` macro.
#[proc_macro_error]
#[proc_macro_derive(Arbitrary)]
pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
derive::expand_derive_arbitrary(item)
}

/// This module implements Kani attributes in a way that only Kani's compiler can understand.
/// This code should only be activated when pre-building Kani's sysroot.
#[cfg(kani_sysroot)]
mod sysroot {
use super::*;

use {
quote::{format_ident, quote},
syn::{parse_macro_input, ItemFn},
};

/// Annotate the harness with a #[kanitool::<name>] with optional arguments.
macro_rules! kani_attribute {
($name:ident) => {
pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream {
let args = proc_macro2::TokenStream::from(attr);
let fn_item = parse_macro_input!(item as ItemFn);
let attribute = format_ident!("{}", stringify!($name));
quote!(
#[kanitool::#attribute(#args)]
#fn_item
).into()
}
};
($name:ident, no_args) => {
pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream {
assert!(attr.is_empty(), "`#[kani::{}]` does not take any arguments currently", stringify!($name));
let fn_item = parse_macro_input!(item as ItemFn);
let attribute = format_ident!("{}", stringify!($name));
quote!(
#[kanitool::#attribute]
#fn_item
).into()
}
};
}

pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
let fn_item = parse_macro_input!(item as ItemFn);
let attrs = fn_item.attrs;
let vis = fn_item.vis;
let sig = fn_item.sig;
let body = fn_item.block;

let kani_attributes = quote!(
#[allow(dead_code)]
#[kanitool::proof]
);

assert!(attr.is_empty(), "#[kani::proof] does not take any arguments currently");

if sig.asyncness.is_none() {
// Adds `#[kanitool::proof]` and other attributes
quote!(
#kani_attributes
#(#attrs)*
#vis #sig #body
)
.into()
} else {
// For async functions, it translates to a synchronous function that calls `kani::block_on`.
// Specifically, it translates
// ```ignore
// #[kani::async_proof]
// #[attribute]
// pub async fn harness() { ... }
// ```
// to
// ```ignore
// #[kani::proof]
// #[attribute]
// pub fn harness() {
// async fn harness() { ... }
// kani::block_on(harness())
// }
// ```
assert!(
sig.inputs.is_empty(),
"#[kani::proof] cannot be applied to async functions that take inputs for now"
);
let mut modified_sig = sig.clone();
modified_sig.asyncness = None;
let fn_name = &sig.ident;
quote!(
#kani_attributes
#(#attrs)*
#vis #modified_sig {
#sig #body
kani::block_on(#fn_name())
}
)
.into()
}
}

kani_attribute!(should_panic, no_args);
kani_attribute!(unwind);
kani_attribute!(stub);
kani_attribute!(solver);
}

/// This module provides dummy implementations of Kani attributes which cannot be interpreted by
/// other tools such as MIRI and the regular rust compiler.
///
/// This allow users to use code marked with Kani attributes, for example, during concrete playback.
#[cfg(not(kani_sysroot))]
mod regular {
use super::*;

/// Encode a noop proc macro which ignores the given attribute.
macro_rules! no_op {
($name:ident) => {
pub fn $name(_attr: TokenStream, item: TokenStream) -> TokenStream {
item
}
};
}

/// Add #[allow(dead_code)] to a proof harness to avoid dead code warnings.
pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
let mut result = TokenStream::new();
result.extend("#[allow(dead_code)]".parse::<TokenStream>().unwrap());
result.extend(item);
result
}

no_op!(should_panic);
no_op!(unwind);
no_op!(stub);
no_op!(solver);
}
7 changes: 5 additions & 2 deletions tools/build-kani/src/sysroot.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,14 +88,17 @@ pub fn build_lib() {
"--config",
"profile.dev.debug-assertions=false",
"--config",
"host.rustflags=[\"--cfg=kani\"]",
"host.rustflags=[\"--cfg=kani\", \"--cfg=kani_sysroot\"]",
"--target",
target,
"--message-format",
"json-diagnostic-rendered-ansi",
];
let mut cmd = Command::new("cargo")
.env("CARGO_ENCODED_RUSTFLAGS", ["--cfg=kani", "-Z", "always-encode-mir"].join("\x1f"))
.env(
"CARGO_ENCODED_RUSTFLAGS",
["--cfg=kani", "--cfg=kani_sysroot", "-Z", "always-encode-mir"].join("\x1f"),
)
.args(args)
.stdout(Stdio::piped())
.spawn()
Expand Down

0 comments on commit 868b13b

Please sign in to comment.