Skip to content

Commit

Permalink
Extract normal specs on abstract trait methods (#106)
Browse files Browse the repository at this point in the history
* Add test case.
* Preliminary refactor.
* Generate unimplemented body and specs with macro.
* Annotate pseudo-abstract methods.
* Pick up the flag "is_abstract".
* Conditionally compile macro implementation.
  • Loading branch information
yannbolliger authored Mar 16, 2021
1 parent a968c81 commit 24dad76
Show file tree
Hide file tree
Showing 14 changed files with 299 additions and 168 deletions.
2 changes: 2 additions & 0 deletions .cargo/config
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
[build]
rustflags = ["--cfg", "stainless"]
16 changes: 8 additions & 8 deletions demo/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

26 changes: 26 additions & 0 deletions demo/examples/type_class_specs.rs
Original file line number Diff line number Diff line change
@@ -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)
}
2 changes: 1 addition & 1 deletion libstainless_macros/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
37 changes: 0 additions & 37 deletions libstainless_macros/lib.rs

This file was deleted.

Original file line number Diff line number Diff line change
@@ -1,103 +1,103 @@
#![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<String> for SpecType {
type Error = ();
/// Flags

fn try_from(name: String) -> std::result::Result<Self, Self::Error> {
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<Self, Self::Error> {
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<Attribute>,
sig: Signature,
vis: Option<Visibility>,
block: Option<Box<Block>>,
specs: Vec<Spec>,
}

/// Parse the decorated function and all specs
fn try_parse(
first_spec_type: SpecType,
first_attr_args: TokenStream,
item: TokenStream,
) -> Result<(ItemFn, Vec<Spec>)> {
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<Expr>)> = 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<FnSpecs> {
let first_args: Expr = parse2(first_attr_args)?;

let specs: Vec<Spec> = specs
// Parse function OR abstract trait method.
let (attrs, sig, block, vis) = parse2::<ItemFn>(item.clone())
.map(|i| (i.attrs, i.sig, Some(i.block), Some(i.vis)))
.or_else(|_| parse2::<TraitItemMethod>(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::<Result<Vec<_>>>()?;

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<Spec>) -> 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<FnArg, Token![,]> = (match &fn_arg_tys[..] {
Expand All @@ -113,13 +113,12 @@ fn generate_fn_with_spec(mut item_fn: ItemFn, specs: Vec<Spec>) -> 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! { () },
};
Expand All @@ -131,8 +130,7 @@ fn generate_fn_with_spec(mut item_fn: ItemFn, specs: Vec<Spec>) -> 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; }),
Expand All @@ -148,51 +146,33 @@ fn generate_fn_with_spec(mut item_fn: ItemFn, specs: Vec<Spec>) -> 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),
}
}

Expand Down
Loading

0 comments on commit 24dad76

Please sign in to comment.