diff --git a/.cargo/config b/.cargo/config new file mode 100644 index 00000000..f6beadb9 --- /dev/null +++ b/.cargo/config @@ -0,0 +1,2 @@ +[build] +rustflags = ["--cfg", "stainless"] \ No newline at end of file diff --git a/demo/Cargo.lock b/demo/Cargo.lock index b6c9bf24..27b16b96 100644 --- a/demo/Cargo.lock +++ b/demo/Cargo.lock @@ -45,18 +45,18 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.18" +version = "1.0.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "beae6331a816b1f65d04c45b078fd8e6c93e8071771f41b8163255bbd8d7c8fa" +checksum = "1e0704ee1a7e00d7bb417d0770ea303c1bccbabf0ef1667dae92b5967f5f8a71" dependencies = [ "unicode-xid", ] [[package]] name = "quote" -version = "1.0.7" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aa563d17ecb180e500da1cfd2b028310ac758de548efdd203e18f283af693f37" +checksum = "c3d0b9745dc2debf507c8422de05d7226cc1f0644216dfdfead988f9b1ab32a7" dependencies = [ "proc-macro2", ] @@ -80,9 +80,9 @@ dependencies = [ [[package]] name = "syn" -version = "1.0.31" +version = "1.0.63" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5304cfdf27365b7585c25d4af91b35016ed21ef88f17ced89c7093b43dba8b6" +checksum = "8fd9bc7ccc2688b3344c2f48b9b546648b25ce0b20fc717ee7fa7981a8ca9717" dependencies = [ "proc-macro2", "quote", @@ -91,6 +91,6 @@ dependencies = [ [[package]] name = "unicode-xid" -version = "0.2.0" +version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "826e7639553986605ec5979c7dd957c7895e93eabed50ab2ffa7f6128a75097c" +checksum = "f7fe0bb3479651439c9112f72b6c505038574c9fbb575ed1bf3b797fa39dd564" diff --git a/demo/examples/type_class_specs.rs b/demo/examples/type_class_specs.rs new file mode 100644 index 00000000..d6da7543 --- /dev/null +++ b/demo/examples/type_class_specs.rs @@ -0,0 +1,26 @@ +extern crate stainless; +use stainless::*; + +trait SpecsNotLaws { + #[post(ret > 0)] + fn always_positive(&self) -> i32; + + #[pre(b)] + fn always_call_true(b: bool) { + let _a = 1; + } +} + +impl SpecsNotLaws for u32 { + fn always_positive(&self) -> i32 { + 123 + } + + fn always_call_true(_b: bool) {} +} + +pub fn main() { + let number: u32 = 465; + u32::always_call_true(true); + assert!(number.always_positive() > 0) +} diff --git a/libstainless_macros/Cargo.toml b/libstainless_macros/Cargo.toml index 42b46b43..b456cf09 100644 --- a/libstainless_macros/Cargo.toml +++ b/libstainless_macros/Cargo.toml @@ -8,7 +8,7 @@ categories = ["development-tools"] [lib] name = "stainless_macros" -path = "lib.rs" +path = "src/lib.rs" test = false doctest = false proc-macro = true diff --git a/libstainless_macros/lib.rs b/libstainless_macros/lib.rs deleted file mode 100644 index 41e4cc22..00000000 --- a/libstainless_macros/lib.rs +++ /dev/null @@ -1,37 +0,0 @@ -use proc_macro::TokenStream; -mod implementation; -use implementation::*; - -/// Specs - -/// Precondition -#[proc_macro_attribute] -pub fn pre(attr: TokenStream, item: TokenStream) -> TokenStream { - extract_specs_and_expand(SpecType::Pre, attr.into(), item.into()).into() -} - -/// Postcondition -#[proc_macro_attribute] -pub fn post(attr: TokenStream, item: TokenStream) -> TokenStream { - extract_specs_and_expand(SpecType::Post, attr.into(), item.into()).into() -} - -#[proc_macro_attribute] -pub fn measure(attr: TokenStream, item: TokenStream) -> TokenStream { - extract_specs_and_expand(SpecType::Measure, attr.into(), item.into()).into() -} - -/// Flags - -macro_rules! define_flags { - ($($flag:ident),*) => { - $( - #[proc_macro_attribute] - pub fn $flag(attr: TokenStream, item: TokenStream) -> TokenStream { - rewrite_flag(stringify!($flag), attr.into(), item.into()).into() - } - )* - } -} - -define_flags!(external, pure, mutable, var, law); diff --git a/libstainless_macros/implementation.rs b/libstainless_macros/src/implementation.rs similarity index 52% rename from libstainless_macros/implementation.rs rename to libstainless_macros/src/implementation.rs index 65f6c0c3..92f8bf13 100644 --- a/libstainless_macros/implementation.rs +++ b/libstainless_macros/src/implementation.rs @@ -1,61 +1,58 @@ +#![cfg(stainless)] + use proc_macro2::{Group, Ident, Span, TokenStream, TokenTree}; use quote::{quote, ToTokens}; use syn::{ - parse_quote, Attribute, Expr, FnArg, ItemFn, Receiver, Result, ReturnType, Stmt, Token, Type, + parse2, parse_quote, punctuated::Punctuated, token::Brace, Attribute, Block, Expr, FnArg, ItemFn, + Receiver, Result, ReturnType, Signature, Stmt, Token, TraitItemMethod, Type, Visibility, }; +use super::spec::*; use std::convert::TryFrom; use std::iter; -use syn::punctuated::Punctuated; - -/// Specs (pre-, postconditions, ...) -#[derive(Debug, PartialEq, Eq)] -pub enum SpecType { - Pre, - Post, - Measure, -} +use syn::parse::Parser; -impl SpecType { - fn name(&self) -> &'static str { - match self { - SpecType::Pre => "pre", - SpecType::Post => "post", - SpecType::Measure => "measure", - } - } +/// Extract all the specs from a given function and insert spec functions +pub fn extract_specs_and_expand( + first_spec_type: SpecType, + first_attr_args: TokenStream, + item: TokenStream, +) -> TokenStream { + try_parse(first_spec_type, first_attr_args, item).map_or_else( + |err| err.to_compile_error(), + |f| generate_fn_with_spec(f).to_token_stream(), + ) } -impl TryFrom for SpecType { - type Error = (); +/// Flags - fn try_from(name: String) -> std::result::Result { - match name.as_str() { - "pre" => Ok(SpecType::Pre), - "post" => Ok(SpecType::Post), - "measure" => Ok(SpecType::Measure), - _ => Err(()), - } +/// Note that we simply want to attach some attributes to the item in question. Currently, +/// Rust doesn't permit user-defined attributes that stay around until the later phases of +/// rustc. However, any attribute in the `clippy::` group is accepted, and clippy itself +/// doesn't seem to complain about unknown attributes. We therefore abuse this to attach +/// some attributes of our own for the stainless extraction pass to detect. +pub fn rewrite_flag( + flag_name: &'static str, + mut args: TokenStream, + item: TokenStream, +) -> TokenStream { + let flag_name = Ident::new(flag_name, Span::call_site()); + if !args.is_empty() { + args = quote! { ( #args ) }; } -} - -impl<'a> TryFrom<&'a Attribute> for SpecType { - type Error = (); - - fn try_from(attr: &'a Attribute) -> std::result::Result { - let segments = &attr.path.segments; - if segments.len() == 1 { - SpecType::try_from(segments[0].ident.to_string()) - } else { - Err(()) - } + quote! { + #[clippy::stainless::#flag_name#args] + #item } } #[derive(Debug)] -struct Spec { - typ: SpecType, - expr: Expr, +struct FnSpecs { + attrs: Vec, + sig: Signature, + vis: Option, + block: Option>, + specs: Vec, } /// Parse the decorated function and all specs @@ -63,41 +60,44 @@ fn try_parse( first_spec_type: SpecType, first_attr_args: TokenStream, item: TokenStream, -) -> Result<(ItemFn, Vec)> { - let item_fn: ItemFn = parse_quote!(#item); - let first_args: Expr = parse_quote!(#first_attr_args); - - // Filter out & parse all the remaining specs - let specs = item_fn.attrs.iter().filter_map(|attr: &Attribute| { - SpecType::try_from(attr) - .ok() - .map(|typ| (typ, attr.parse_args())) - }); - // Add the first spec to the head of the list - let specs: Vec<(SpecType, Result)> = iter::once((first_spec_type, Ok(first_args))) - .chain(specs) - .collect(); - - // Check whether any parsing has caused errors and fail if so. - if let Some((_, Err(err))) = specs.iter().find(|(_, cond)| cond.is_err()) { - return Err(err.clone()); - } +) -> Result { + let first_args: Expr = parse2(first_attr_args)?; - let specs: Vec = specs + // Parse function OR abstract trait method. + let (attrs, sig, block, vis) = parse2::(item.clone()) + .map(|i| (i.attrs, i.sig, Some(i.block), Some(i.vis))) + .or_else(|_| parse2::(item).map(|i| (i.attrs, i.sig, None, None)))?; + + let (specs, attrs): (Vec<_>, Vec<_>) = attrs .into_iter() - .map(|(typ, cond)| Spec { - typ, - expr: cond.unwrap(), + .map(|a| (SpecType::try_from(&a), a)) + .partition(|(s, _)| s.is_ok()); + + let specs: Vec<_> = iter::once(Ok(Spec { + typ: first_spec_type, + expr: first_args, + })) + .chain(specs.into_iter().map(|(t, a)| { + a.parse_args().map(|expr| Spec { + typ: t.unwrap(), + expr, }) - .collect(); - - Ok((item_fn, specs)) + })) + // collect and return early if there's an error + .collect::>>()?; + + Ok(FnSpecs { + attrs: attrs.into_iter().map(|(_, a)| a).collect(), + sig, + block, + specs, + vis, + }) } -fn generate_fn_with_spec(mut item_fn: ItemFn, specs: Vec) -> ItemFn { - // Take the arguments of the actual function to create the arguments of the - // closure. - let fn_arg_tys: Vec<_> = item_fn.sig.inputs.iter().cloned().collect(); +fn generate_fn_with_spec(fn_specs: FnSpecs) -> ItemFn { + // Take the arguments of the actual function to create the closure's arguments. + let fn_arg_tys: Vec<_> = fn_specs.sig.inputs.iter().cloned().collect(); // Replace the [&]self param with a _self: [&]Self let fn_arg_tys: Punctuated = (match &fn_arg_tys[..] { @@ -113,13 +113,12 @@ fn generate_fn_with_spec(mut item_fn: ItemFn, specs: Vec) -> ItemFn { }; [&[new_self], args].concat() } - args => args.to_vec(), }) .into_iter() .collect(); - let fn_return_ty: Type = match &item_fn.sig.output { + let fn_return_ty: Type = match &fn_specs.sig.output { ReturnType::Type(_, ty) => *ty.clone(), ReturnType::Default => parse_quote! { () }, }; @@ -131,8 +130,7 @@ fn generate_fn_with_spec(mut item_fn: ItemFn, specs: Vec) -> ItemFn { SpecType::Post => quote! { , ret: #fn_return_ty }, _ => quote! {}, }; - - let expr: TokenStream = replace_ident(spec.expr.to_token_stream(), "self", "_self"); + let expr = replace_ident(spec.expr.to_token_stream(), "self", "_self"); let (return_type, body): (Type, TokenStream) = match spec.typ { SpecType::Measure => (parse_quote!(()), parse_quote! { #expr; }), @@ -148,51 +146,33 @@ fn generate_fn_with_spec(mut item_fn: ItemFn, specs: Vec) -> ItemFn { } }; - let spec_closures = specs.into_iter().map(make_spec_fn); - #[allow(clippy::reversed_empty_ranges)] - item_fn.block.stmts.splice(0..0, spec_closures); - item_fn -} - -/// Extract all the specs from a given function and insert spec functions -pub fn extract_specs_and_expand( - first_spec_type: SpecType, - first_attr_args: TokenStream, - item: TokenStream, -) -> TokenStream { - match try_parse(first_spec_type, first_attr_args, item) { - Ok((mut item_fn, specs)) => { - // Remove all remaining spec attributes - item_fn - .attrs - .retain(|attr| SpecType::try_from(attr).is_err()); - - // Build the spec function and insert it into the original function - generate_fn_with_spec(item_fn, specs).to_token_stream() - } - Err(err) => err.to_compile_error(), + // Annotate "abstract" functions with a flag + let mut attrs = fn_specs.attrs; + if fn_specs.block.is_none() { + attrs.extend( + Attribute::parse_outer + .parse_str("#[clippy::stainless::is_abstract]") + .unwrap(), + ) } -} -/// Flags + let spec_closures = fn_specs.specs.into_iter().map(make_spec_fn); + let block = Box::new(Block { + brace_token: Brace::default(), + stmts: spec_closures + .chain( + fn_specs + .block + .map_or_else(|| parse_quote! { unimplemented!() }, |b| b.stmts), + ) + .collect(), + }); -/// Note that we simply want to attach some attributes to the item in question. Currently, -/// Rust doesn't permit user-defined attributes that stay around until the later phases of -/// rustc. However, any attribute in the `clippy::` group is accepted, and clippy itself -/// doesn't seem to complain about unknown attributes. We therefore abuse this to attach -/// some attributes of our own for the stainless extraction pass to detect. -pub fn rewrite_flag( - flag_name: &'static str, - mut args: TokenStream, - item: TokenStream, -) -> TokenStream { - let flag_name = Ident::new(flag_name, Span::call_site()); - if !args.is_empty() { - args = quote! { ( #args ) }; - } - quote! { - #[clippy::stainless::#flag_name#args] - #item + ItemFn { + attrs, + sig: fn_specs.sig, + block, + vis: fn_specs.vis.unwrap_or(Visibility::Inherited), } } diff --git a/libstainless_macros/src/lib.rs b/libstainless_macros/src/lib.rs new file mode 100644 index 00000000..ab0ec0d5 --- /dev/null +++ b/libstainless_macros/src/lib.rs @@ -0,0 +1,77 @@ +mod implementation; +mod spec; + +use spec::SpecType; + +use proc_macro::TokenStream; + +/// Specs + +/// Precondition +#[proc_macro_attribute] +pub fn pre(attr: TokenStream, item: TokenStream) -> TokenStream { + specs(SpecType::Pre, attr, item) +} + +/// Postcondition +#[proc_macro_attribute] +pub fn post(attr: TokenStream, item: TokenStream) -> TokenStream { + specs(SpecType::Post, attr, item) +} + +#[proc_macro_attribute] +pub fn measure(attr: TokenStream, item: TokenStream) -> TokenStream { + specs(SpecType::Measure, attr, item) +} + +/// Flags + +macro_rules! define_flags { + ($($flag:ident),*) => { + $( + #[proc_macro_attribute] + pub fn $flag(attr: TokenStream, item: TokenStream) -> TokenStream { + flags(stringify!($flag), attr, item) + } + )* + } +} + +define_flags!(external, pure, mutable, var, law); + +#[cfg(stainless)] +mod entry_point { + use super::*; + use implementation::*; + + pub fn specs( + first_spec_type: SpecType, + first_attr_args: TokenStream, + item: TokenStream, + ) -> TokenStream { + extract_specs_and_expand(first_spec_type, first_attr_args.into(), item.into()).into() + } + + pub fn flags(flag_name: &'static str, args: TokenStream, item: TokenStream) -> TokenStream { + rewrite_flag(flag_name, args.into(), item.into()).into() + } +} + +#[cfg(not(stainless))] +mod entry_point { + use super::*; + + pub fn specs( + _first_spec_type: SpecType, + _first_attr_args: TokenStream, + item: TokenStream, + ) -> TokenStream { + item + } + + pub fn flags(_flag_name: &'static str, _args: TokenStream, item: TokenStream) -> TokenStream { + item + } +} + +use entry_point::*; diff --git a/libstainless_macros/src/spec.rs b/libstainless_macros/src/spec.rs new file mode 100644 index 00000000..b056233b --- /dev/null +++ b/libstainless_macros/src/spec.rs @@ -0,0 +1,52 @@ +use std::convert::TryFrom; +use syn::{Attribute, Expr}; + +/// Specs (pre-, postconditions, ...) +#[derive(Debug)] +pub struct Spec { + pub typ: SpecType, + pub expr: Expr, +} + +#[derive(Debug, PartialEq, Eq)] +pub enum SpecType { + Pre, + Post, + Measure, +} + +impl SpecType { + #[cfg(stainless)] + pub fn name(&self) -> &'static str { + match self { + SpecType::Pre => "pre", + SpecType::Post => "post", + SpecType::Measure => "measure", + } + } +} +impl TryFrom for SpecType { + type Error = (); + + fn try_from(name: String) -> std::result::Result { + match name.as_str() { + "pre" => Ok(SpecType::Pre), + "post" => Ok(SpecType::Post), + "measure" => Ok(SpecType::Measure), + _ => Err(()), + } + } +} + +impl<'a> TryFrom<&'a Attribute> for SpecType { + type Error = (); + + fn try_from(attr: &'a Attribute) -> std::result::Result { + let segments = &attr.path.segments; + if segments.len() == 1 { + SpecType::try_from(segments[0].ident.to_string()) + } else { + Err(()) + } + } +} diff --git a/stainless_extraction/src/flags.rs b/stainless_extraction/src/flags.rs index a28ac699..f53e26b3 100644 --- a/stainless_extraction/src/flags.rs +++ b/stainless_extraction/src/flags.rs @@ -17,6 +17,7 @@ pub(super) enum Flag { IsPure, IsMutable, IsVar, + IsAbstract, Law, Pre, Post, @@ -49,6 +50,7 @@ impl Flags { IsMutable => Some(f.IsMutable().into()), IsVar => Some(f.IsVar().into()), Law => Some(f.Law().into()), + IsAbstract => Some(f.IsAbstract().into()), // Or pattern instead of wildcard '_' to keep the compiler checking that // all variants are covered. @@ -67,6 +69,7 @@ impl Flag { IsPure => "pure", IsMutable => "mutable", IsVar => "var", + IsAbstract => "is_abstract", Law => "law", Pre => "pre", Post => "post", diff --git a/stainless_extraction/src/krate.rs b/stainless_extraction/src/krate.rs index 5fda02fd..085091ab 100644 --- a/stainless_extraction/src/krate.rs +++ b/stainless_extraction/src/krate.rs @@ -391,7 +391,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> { }; let (params, return_tpe, body_expr): (Params<'l>, st::Type<'l>, st::Expr<'l>) = self - .enter_body(hir_id, txtcx.clone(), class_def, |bxtor| { + .enter_body(hir_id, txtcx, class_def, |bxtor| { // Register parameters and local bindings in the DefContext bxtor.populate_def_context(&mut flags_by_symbol, &ev_params); diff --git a/stainless_frontend/Cargo.toml b/stainless_frontend/Cargo.toml index 1773957e..4c49d610 100644 --- a/stainless_frontend/Cargo.toml +++ b/stainless_frontend/Cargo.toml @@ -29,5 +29,4 @@ serde_json = "1.0" stainless = { path = "../libstainless" } tempfile = "3" -[features] -default = [] + diff --git a/stainless_frontend/src/lib.rs b/stainless_frontend/src/lib.rs index c63d747f..6767b099 100644 --- a/stainless_frontend/src/lib.rs +++ b/stainless_frontend/src/lib.rs @@ -18,11 +18,13 @@ use rustc_middle::ty::TyCtxt; use stainless_data::ast as st; pub fn run, st::Symbols<'_>) + Send>( - args: Vec, + mut args: Vec, on_extraction: E, ) -> Result<(), ()> { let mut callbacks = ExtractionCallbacks::new(on_extraction); let file_loader = None; + args.extend(vec!["--cfg".into(), "stainless".into()]); + rustc_driver::install_ice_hook(); rustc_driver::catch_fatal_errors(|| run_compiler(&args, &mut callbacks, file_loader, None)) .map(|_| ()) diff --git a/stainless_frontend/tests/extraction_tests.rs b/stainless_frontend/tests/extraction_tests.rs index 2d29c354..8d7c93dc 100644 --- a/stainless_frontend/tests/extraction_tests.rs +++ b/stainless_frontend/tests/extraction_tests.rs @@ -106,6 +106,7 @@ define_tests!( pass: tuples, pass: type_class, pass: type_class_multi_lookup, + pass: type_class_specs, pass: type_class_without_evidence, pass: use_std, fail_verification: box_as_ref, diff --git a/stainless_frontend/tests/pass/type_class_specs.rs b/stainless_frontend/tests/pass/type_class_specs.rs new file mode 100644 index 00000000..d6da7543 --- /dev/null +++ b/stainless_frontend/tests/pass/type_class_specs.rs @@ -0,0 +1,26 @@ +extern crate stainless; +use stainless::*; + +trait SpecsNotLaws { + #[post(ret > 0)] + fn always_positive(&self) -> i32; + + #[pre(b)] + fn always_call_true(b: bool) { + let _a = 1; + } +} + +impl SpecsNotLaws for u32 { + fn always_positive(&self) -> i32 { + 123 + } + + fn always_call_true(_b: bool) {} +} + +pub fn main() { + let number: u32 = 465; + u32::always_call_true(true); + assert!(number.always_positive() > 0) +}