Skip to content

Commit

Permalink
move fuzz into term trait
Browse files Browse the repository at this point in the history
  • Loading branch information
nikomatsakis committed Jul 2, 2024
1 parent 1c14dce commit 44f92f4
Show file tree
Hide file tree
Showing 8 changed files with 30 additions and 25 deletions.
1 change: 1 addition & 0 deletions Cargo.lock

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

2 changes: 2 additions & 0 deletions crates/formality-macros/src/custom.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ pub(crate) struct Customize {
pub constructors: bool,
pub fold: bool,
pub visit: bool,
pub fuzz: bool,
}

impl syn::parse::Parse for Customize {
Expand Down Expand Up @@ -45,6 +46,7 @@ impl syn::parse::Parse for Customize {
constructors,
fold,
visit,
fuzz,
}

if let Some(token) = tokens.next() {
Expand Down
18 changes: 17 additions & 1 deletion crates/formality-macros/src/term.rs
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,24 @@ pub fn term(spec: Option<FormalitySpec>, mut input: DeriveInput) -> syn::Result<
};
remove_formality_attributes(&mut input);

let derives: Vec<TokenStream> = vec![
quote!(Clone),
quote!(PartialEq),
quote!(Eq),
quote!(PartialOrd),
quote!(Ord),
quote!(Hash),
]
.into_iter()
.chain(if customize.fuzz {
None
} else {
Some(quote!(bolero::TypeGenerator))
})
.collect();

Ok(quote! {
#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
#[derive(#(#derives),*)]
#input

#fold_impl
Expand Down
1 change: 1 addition & 0 deletions crates/formality-prove/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ formality-core = { path = "../formality-core" }
tracing = "0.1"
contracts = "0.6.3"
anyhow = "1.0.66"
bolero = "0.11.1"

[dev-dependencies]
expect-test = "1.4.0"
11 changes: 4 additions & 7 deletions crates/formality-rust/src/grammar.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ use crate::grammar::mir::MirFnBody;
pub mod mir;

#[term($crates)]
#[customize(fuzz)]
pub struct Program {
/// List of all crates.
/// The last crate in the list is the current crate.
Expand Down Expand Up @@ -45,12 +46,14 @@ impl Program {
}

#[term(crate $id { $*items })]
#[customize(fuzz)]
pub struct Crate {
pub id: CrateId,
pub items: Vec<CrateItem>,
}

#[term]
#[customize(fuzz)]
pub enum CrateItem {
#[cast]
Struct(Struct),
Expand Down Expand Up @@ -111,21 +114,18 @@ impl Struct {
}

#[term($:where $,where_clauses { $,fields })]
#[derive(bolero::TypeGenerator)]
pub struct StructBoundData {
pub where_clauses: Vec<WhereClause>,
pub fields: Vec<Field>,
}

#[term($name : $ty)]
#[derive(bolero::TypeGenerator)]
pub struct Field {
pub name: FieldName,
pub ty: Ty,
}

#[term]
#[derive(bolero::TypeGenerator)]
pub enum FieldName {
#[cast]
Id(FieldId),
Expand Down Expand Up @@ -166,20 +166,19 @@ pub struct Adt {
}

#[term($:where $,where_clauses { $,variants })]
#[derive(bolero::TypeGenerator)]
pub struct AdtBoundData {
pub where_clauses: Vec<WhereClause>,
pub variants: Vec<Variant>,
}

#[term($name { $,fields })]
#[derive(bolero::TypeGenerator)]
pub struct Variant {
pub name: VariantId,
pub fields: Vec<Field>,
}

#[term($?safety trait $id $binder)]
#[customize(fuzz)]
pub struct Trait {
pub safety: Safety,
pub id: TraitId,
Expand Down Expand Up @@ -329,7 +328,6 @@ pub struct AssociatedTyValueBoundData {
}

#[term($data)]
#[derive(bolero::TypeGenerator)]
pub struct WhereClause {
pub data: Arc<WhereClauseData>,
}
Expand Down Expand Up @@ -360,7 +358,6 @@ impl WhereClause {
}

#[term]
#[derive(bolero::TypeGenerator)]
pub enum WhereClauseData {
#[grammar($v0 : $v1 $<?v2>)]
IsImplemented(Ty, TraitId, Vec<Parameter>),
Expand Down
2 changes: 1 addition & 1 deletion crates/formality-rust/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
use formality_types::rust::FormalityLang;
// ANCHOR_END: use_rust_language

mod fuzz;
pub mod fuzz;
pub mod grammar;
pub mod prove;
mod test;
Expand Down
2 changes: 0 additions & 2 deletions crates/formality-types/src/grammar/consts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ pub use valtree::*;
#[term]
#[cast]
#[customize(constructors)] // FIXME: figure out upcasts with arc or special-case
#[derive(bolero::TypeGenerator)]
pub struct Const {
data: Arc<ConstData>,
}
Expand Down Expand Up @@ -44,7 +43,6 @@ impl Const {

#[term]
#[customize(parse)]
#[derive(bolero::TypeGenerator)]
pub enum ConstData {
Value(ValTree, Ty),

Expand Down
18 changes: 4 additions & 14 deletions crates/formality-types/src/grammar/ty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ use super::{

#[term]
#[cast]
#[derive(bolero::TypeGenerator)]
#[customize(constructors)] // FIXME: figure out upcasts with arc or special-case
pub struct Ty {
data: Arc<TyData>,
Expand Down Expand Up @@ -101,7 +100,6 @@ impl DowncastTo<TyData> for Ty {
// NB: TyData doesn't implement Fold; you fold types, not TyData,
// because variables might not map to the same variant.
#[term]
#[derive(bolero::TypeGenerator)]
pub enum TyData {
#[cast]
RigidTy(RigidTy),
Expand All @@ -121,7 +119,7 @@ impl UpcastFrom<Ty> for TyData {

// ANCHOR: RigidTy_decl
#[term((rigid $name $*parameters))]
#[customize(parse, debug)]
#[customize(parse, debug, fuzz)]
pub struct RigidTy {
pub name: RigidName,
pub parameters: Parameters,
Expand All @@ -144,7 +142,6 @@ impl DowncastTo<ScalarId> for RigidTy {
}

#[term]
#[derive(bolero::TypeGenerator)]
pub enum RigidName {
#[grammar((adt $v0))]
#[cast]
Expand All @@ -161,14 +158,12 @@ pub enum RigidName {
}

#[term]
#[derive(bolero::TypeGenerator)]
pub enum RefKind {
Shared,
Mut,
}

#[term]
#[derive(bolero::TypeGenerator)]
pub enum ScalarId {
#[grammar(u8)]
U8,
Expand Down Expand Up @@ -196,7 +191,6 @@ pub enum ScalarId {

#[term((alias $name $*parameters))]
#[customize(parse, debug)]
#[derive(bolero::TypeGenerator)]
pub struct AliasTy {
pub name: AliasName,
pub parameters: Parameters,
Expand Down Expand Up @@ -224,13 +218,13 @@ impl AliasTy {
}

#[term]
#[derive(bolero::TypeGenerator)]
pub enum AliasName {
#[cast]
AssociatedTyId(AssociatedTyName),
}

#[term(($trait_id :: $item_id / $item_arity))]
#[customize(fuzz)]
pub struct AssociatedTyName {
/// The trait in which the associated type was declared.
pub trait_id: TraitId,
Expand All @@ -243,13 +237,11 @@ pub struct AssociatedTyName {
}

#[term]
#[derive(bolero::TypeGenerator)]
pub enum PredicateTy {
ForAll(Binder<Ty>),
}

#[term]
#[derive(bolero::TypeGenerator)]
pub enum Parameter {
#[cast]
Ty(Ty),
Expand Down Expand Up @@ -284,15 +276,15 @@ impl Parameter {
pub type Parameters = Vec<Parameter>;

#[term]
#[derive(Copy, bolero::TypeGenerator)]
#[derive(Copy)]
pub enum ParameterKind {
Ty,
Lt,
Const,
}

#[term]
#[derive(Copy, bolero::TypeGenerator)]
#[derive(Copy)]
pub enum Variance {
#[grammar(+)]
Covariant,
Expand All @@ -304,7 +296,6 @@ pub enum Variance {

#[term]
#[cast]
#[derive(bolero::TypeGenerator)]
#[customize(constructors)] // FIXME: figure out upcasts with arc or special-case
pub struct Lt {
data: Arc<LtData>,
Expand Down Expand Up @@ -346,7 +337,6 @@ impl DowncastTo<LtData> for Lt {
}

#[term]
#[derive(bolero::TypeGenerator)]
pub enum LtData {
Static,

Expand Down

0 comments on commit 44f92f4

Please sign in to comment.