Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
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
11 changes: 10 additions & 1 deletion src/implementation/ensures.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,16 @@ use crate::implementation::{ContractMode, ContractType, FuncWithContracts};
pub(crate) fn ensures(mode: ContractMode, attr: TokenStream, toks: TokenStream) -> TokenStream {
let ty = ContractType::Ensures;

let func = syn::parse_quote!(#toks);
let func = match syn::parse2(toks.clone()) {
Ok(func) => func,
Err(err) => {
let error = err.to_compile_error();
return quote::quote! {
#error
#toks
};
}
};

let f = FuncWithContracts::new_with_initial_contract(func, ty, mode, attr);

Expand Down
32 changes: 26 additions & 6 deletions src/implementation/invariant.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,17 +9,37 @@ use syn::{FnArg, ImplItem, ImplItemFn, Item, ItemFn, ItemImpl};
use crate::implementation::{ContractMode, ContractType, FuncWithContracts};

pub(crate) fn invariant(mode: ContractMode, attr: TokenStream, toks: TokenStream) -> TokenStream {
let item: Item = syn::parse_quote!(#toks);

let name = mode.name().unwrap().to_string() + "invariant";

let item: Item = match syn::parse2(toks.clone()) {
Ok(item) => item,
Err(err) => {
let error = err.to_compile_error();
return quote::quote! {
#error
#toks
};
}
};

match item {
Item::Fn(fn_) => invariant_fn(mode, attr, fn_),
Item::Impl(impl_) => invariant_impl(mode, attr, impl_),
_ => unimplemented!(
"The #[{}] attribute only works on functions and impl-blocks.",
name
),
item => {
let error = syn::Error::new_spanned(
&item,
format!(
"the #[{}] attribute only works on functions and impl blocks",
name
),
)
.to_compile_error();

quote::quote! {
#error
#item
}
}
}
}

Expand Down
35 changes: 25 additions & 10 deletions src/implementation/parse.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,23 +19,25 @@ pub(crate) fn parse_attributes(

let mut conds: Vec<Expr> = vec![];

for seg in rewritten_segs {
let last_segment_idx = rewritten_segs.len().saturating_sub(1);

for (idx, seg) in rewritten_segs.into_iter().enumerate() {
let expr = match syn::parse2::<Expr>(seg) {
Ok(val) => val,
Err(err) => Expr::Verbatim(err.to_compile_error()),
};

if idx != last_segment_idx && is_string_lit(&expr) {
let err =
syn::Error::new_spanned(expr, "contract description must be the last argument");
conds.push(Expr::Verbatim(err.to_compile_error()));
continue;
}

conds.push(expr);
}

let desc = conds
.last()
.map(|expr| match expr {
Expr::Lit(ExprLit {
lit: Lit::Str(str), ..
}) => Some(str.value()),
_ => None,
})
.unwrap_or(None);
let desc = conds.last().map(string_lit_value).unwrap_or(None);

if desc.is_some() {
conds.pop();
Expand All @@ -45,6 +47,19 @@ pub(crate) fn parse_attributes(
(conds, segments_stream, desc)
}

fn is_string_lit(expr: &Expr) -> bool {
string_lit_value(expr).is_some()
}

fn string_lit_value(expr: &Expr) -> Option<String> {
match expr {
Expr::Lit(ExprLit {
lit: Lit::Str(str), ..
}) => Some(str.value()),
_ => None,
}
}

// This function rewrites a list of TokenTrees so that the "pseudooperator" for
// implication `==>` gets transformed into an `if` expression.
//
Expand Down
11 changes: 10 additions & 1 deletion src/implementation/requires.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,16 @@ use crate::implementation::{ContractMode, ContractType, FuncWithContracts};
pub(crate) fn requires(mode: ContractMode, attr: TokenStream, toks: TokenStream) -> TokenStream {
let ty = ContractType::Requires;

let func: ItemFn = syn::parse_quote!(#toks);
let func: ItemFn = match syn::parse2(toks.clone()) {
Ok(func) => func,
Err(err) => {
let error = err.to_compile_error();
return quote::quote! {
#error
#toks
};
}
};

let f = FuncWithContracts::new_with_initial_contract(func, ty, mode, attr);

Expand Down
6 changes: 2 additions & 4 deletions tests/ui/fail/description_must_be_last.stderr
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
error[E0600]: cannot apply unary operator `!` to type `&'static str`
error: contract description must be the last argument
--> tests/ui/fail/description_must_be_last.rs:3:12
|
3 | #[requires("x must be positive", x > 0)]
| ^^^^^^^^^^^^^^^^^^^^ cannot apply unary operator `!`
|
= note: this error originates in the macro `assert` (in Nightly builds, run with -Z macro-backtrace for more info)
| ^^^^^^^^^^^^^^^^^^^^
10 changes: 10 additions & 0 deletions tests/ui/fail/invalid_predicate_syntax.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
use contracts::requires;

#[requires(x >)]
fn checked(x: i32) -> i32 {
x
}

fn main() {
let _ = checked(1);
}
7 changes: 7 additions & 0 deletions tests/ui/fail/invalid_predicate_syntax.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
error: unexpected end of input, expected an expression
--> tests/ui/fail/invalid_predicate_syntax.rs:3:1
|
3 | #[requires(x >)]
| ^^^^^^^^^^^^^^^^
|
= note: this error originates in the attribute macro `requires` (in Nightly builds, run with -Z macro-backtrace for more info)
18 changes: 6 additions & 12 deletions tests/ui/fail/invariant_on_struct.stderr
Original file line number Diff line number Diff line change
@@ -1,13 +1,7 @@
error: custom attribute panicked
--> tests/ui/fail/invariant_on_struct.rs:3:1
error: the #[invariant] attribute only works on functions and impl blocks
--> tests/ui/fail/invariant_on_struct.rs:4:1
|
3 | #[invariant(self.value > 0)]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= help: message: not implemented: The #[invariant] attribute only works on functions and impl-blocks.

error[E0422]: cannot find struct, variant or union type `Positive` in this scope
--> tests/ui/fail/invariant_on_struct.rs:9:13
|
9 | let _ = Positive { value: 1 };
| ^^^^^^^^ not found in this scope
4 | / struct Positive {
5 | | value: i32,
6 | | }
| |_^
16 changes: 4 additions & 12 deletions tests/ui/fail/requires_on_struct.stderr
Original file line number Diff line number Diff line change
@@ -1,13 +1,5 @@
error: custom attribute panicked
--> tests/ui/fail/requires_on_struct.rs:3:1
error: expected `fn`
--> tests/ui/fail/requires_on_struct.rs:4:1
|
3 | #[requires(true)]
| ^^^^^^^^^^^^^^^^^
|
= help: message: expected `fn`

error[E0425]: cannot find value `NotAFunction` in this scope
--> tests/ui/fail/requires_on_struct.rs:7:13
|
7 | let _ = NotAFunction;
| ^^^^^^^^^^^^ not found in this scope
4 | struct NotAFunction;
| ^^^^^^
Loading