Skip to content

Fuzz Tests and more #360

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Primata wants to merge 9 commits into
base: m1
Choose a base branch
from
Open

Fuzz Tests and more #360

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
494085b
pre fixing errors
Primata May 18, 2026
b07f4f8
passing tests
Primata May 18, 2026
4f04007
handle empty array of values
Primata May 18, 2026
aafd73e
code review
Primata Jun 2, 2026
a268b6a
remove artifact
Primata Jun 3, 2026
ac69042
code review
Primata Jun 4, 2026
8bc7af2
debloat and raise default to 64 runs
Primata Jun 6, 2026
d01e857
fix constants
Primata Jun 6, 2026
b428708
aggregate results
Primata Jul 1, 2026
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
7,629 changes: 7,629 additions & 0 deletions aptos-move/framework/aptos-framework/boogie.shard_1.bpl
View file
Open in desktop

Large diffs are not rendered by default.

54 changes: 53 additions & 1 deletion third_party/move/move-compiler-v2/legacy-move-compiler/src/expansion/ast.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,14 +45,28 @@ pub enum AttributeValue_ {
Value(Value),
Module(ModuleIdent),
ModuleAccess(ModuleAccess),
List(Vec<AttributeValue>),
Range {
lo: Box<AttributeValue>,
hi: Box<AttributeValue>,
inclusive_hi: bool,
},
Union(Vec<AttributeValue>),
}
pub type AttributeValue = Spanned<AttributeValue_>;

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ConstraintOp {
Ne,
In,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Attribute_ {
Name(Name),
Assigned(Name, Box<AttributeValue>),
Parameterized(Name, Attributes),
Constrained(Name, ConstraintOp, Box<AttributeValue>),
}
pub type Attribute = Spanned<Attribute_>;

Expand All @@ -61,7 +75,8 @@ impl Attribute_ {
match self {
Attribute_::Name(nm)
| Attribute_::Assigned(nm, _)
| Attribute_::Parameterized(nm, _) => nm,
| Attribute_::Parameterized(nm, _)
| Attribute_::Constrained(nm, _, _) => nm,
}
}
}
Expand All @@ -70,6 +85,11 @@ impl Attribute_ {
pub enum AttributeName_ {
Unknown(Symbol),
Known(KnownAttribute),
/// Unique-by-construction key used by `Attribute_::Constrained` entries.
/// `slot` makes duplicate constraints on the same parameter (e.g.
/// `a in X, a != Y`) distinct in the [`UniqueMap`] that stores attributes,
/// while [`Display`](std::fmt::Display) still shows the underlying name.
Disambiguated(Symbol, u32),
}
pub type AttributeName = Spanned<AttributeName_>;

Expand Down Expand Up @@ -880,6 +900,7 @@ impl fmt::Display for AttributeName_ {
match self {
AttributeName_::Unknown(sym) => write!(f, "{}", sym),
AttributeName_::Known(known) => write!(f, "{}", known.name()),
AttributeName_::Disambiguated(sym, _) => write!(f, "{}", sym),
}
}
}
Expand Down Expand Up @@ -990,6 +1011,29 @@ impl AstDebug for AttributeValue_ {
AttributeValue_::Value(v) => v.ast_debug(w),
AttributeValue_::Module(m) => w.write(&format!("{}", m)),
AttributeValue_::ModuleAccess(n) => n.ast_debug(w),
AttributeValue_::List(items) => {
w.write("[");
w.list(items, ", ", |w, item| {
item.value.ast_debug(w);
false
});
w.write("]");
},
AttributeValue_::Range {
lo,
hi,
inclusive_hi,
} => {
lo.value.ast_debug(w);
w.write(if *inclusive_hi { "..=" } else { ".." });
hi.value.ast_debug(w);
},
AttributeValue_::Union(items) => {
w.list(items, " | ", |w, item| {
item.value.ast_debug(w);
false
});
},
}
}
}
Expand All @@ -1012,6 +1056,14 @@ impl AstDebug for Attribute_ {
});
w.write(")");
},
Attribute_::Constrained(n, op, v) => {
w.write(&format!("{}", n));
w.write(match op {
ConstraintOp::Ne => " != ",
ConstraintOp::In => " in ",
});
v.ast_debug(w);
},
}
}
}
Expand Down
50 changes: 47 additions & 3 deletions third_party/move/move-compiler-v2/legacy-move-compiler/src/expansion/translate.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -698,7 +698,8 @@ fn deprecated_attribute_location(attributes: &[P::Attributes]) -> Option<Loc> {
let sp!(nloc, sym) = match &attr.value {
P::Attribute_::Name(n)
| P::Attribute_::Assigned(n, _)
| P::Attribute_::Parameterized(n, _) => *n,
| P::Attribute_::Parameterized(n, _)
| P::Attribute_::Constrained(n, _, _) => *n,
};
match KnownAttribute::resolve(sym) {
Some(KnownAttribute::Deprecation(_dep)) => Some(nloc),
Expand Down Expand Up @@ -728,11 +729,14 @@ fn unique_attributes(
attributes: impl IntoIterator<Item = E::Attribute>,
) -> E::Attributes {
let mut attr_map = UniqueMap::new();
let mut constrained_slot: u32 = 0;
for sp!(loc, attr_) in attributes {
let is_constrained = matches!(&attr_, E::Attribute_::Constrained(..));
let sp!(nloc, sym) = match &attr_ {
E::Attribute_::Name(n)
| E::Attribute_::Assigned(n, _)
| E::Attribute_::Parameterized(n, _) => *n,
| E::Attribute_::Parameterized(n, _)
| E::Attribute_::Constrained(n, _, _) => *n,
};
let name_ = match KnownAttribute::resolve(sym) {
None => {
Expand Down Expand Up @@ -797,7 +801,17 @@ fn unique_attributes(
E::AttributeName_::Known(known)
},
};
if let Err((_, old_loc)) = attr_map.add(sp(nloc, name_), sp(loc, attr_)) {
// `Constrained` entries are deliberately allowed to repeat on the same parameter
// (e.g. `a in [..], a != 5`) — give each a unique slot so the `UniqueMap` accepts
// them. The `Disambiguated` key still `Display`s as the underlying name.
let key = if is_constrained {
let slot = constrained_slot;
constrained_slot += 1;
sp(nloc, E::AttributeName_::Disambiguated(sym, slot))
} else {
sp(nloc, name_)
};
if let Err((_, old_loc)) = attr_map.add(key, sp(loc, attr_)) {
let msg = format!("Duplicate attribute '{}' attached to the same item", name_);
context.env.add_diag(diag!(
Declarations::DuplicateItem,
Expand Down Expand Up @@ -826,6 +840,13 @@ fn attribute(
.collect::<Option<Vec<_>>>()?;
EA::Parameterized(n, unique_attributes(context, attr_position, true, attrs))
},
PA::Constrained(n, op, v) => {
let op = match op {
P::ConstraintOp::Ne => E::ConstraintOp::Ne,
P::ConstraintOp::In => E::ConstraintOp::In,
};
EA::Constrained(n, op, Box::new(attribute_value(context, *v)?))
},
}))
}

Expand Down Expand Up @@ -919,6 +940,29 @@ fn attribute_value(
)?),
}
},
PV::List(items) => {
let items = items
.into_iter()
.map(|v| attribute_value(context, v))
.collect::<Option<Vec<_>>>()?;
EV::List(items)
},
PV::Range {
lo,
hi,
inclusive_hi,
} => EV::Range {
lo: Box::new(attribute_value(context, *lo)?),
hi: Box::new(attribute_value(context, *hi)?),
inclusive_hi,
},
PV::Union(items) => {
let items = items
.into_iter()
.map(|v| attribute_value(context, v))
.collect::<Option<Vec<_>>>()?;
EV::Union(items)
},
}))
}

Expand Down
48 changes: 47 additions & 1 deletion third_party/move/move-compiler-v2/legacy-move-compiler/src/parser/ast.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,14 +115,28 @@ pub struct UseDecl {
pub enum AttributeValue_ {
Value(Value),
ModuleAccess(NameAccessChain),
List(Vec<AttributeValue>),
Range {
lo: Box<AttributeValue>,
hi: Box<AttributeValue>,
inclusive_hi: bool,
},
Union(Vec<AttributeValue>),
}
pub type AttributeValue = Spanned<AttributeValue_>;

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ConstraintOp {
Ne,
In,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Attribute_ {
Name(Name),
Assigned(Name, Box<AttributeValue>),
Parameterized(Name, Attributes),
Constrained(Name, ConstraintOp, Box<AttributeValue>),
}
pub type Attribute = Spanned<Attribute_>;

Expand All @@ -133,7 +147,8 @@ impl Attribute_ {
match self {
Attribute_::Name(nm)
| Attribute_::Assigned(nm, _)
| Attribute_::Parameterized(nm, _) => nm,
| Attribute_::Parameterized(nm, _)
| Attribute_::Constrained(nm, _, _) => nm,
}
}
}
Expand Down Expand Up @@ -1195,6 +1210,29 @@ impl AstDebug for AttributeValue_ {
match self {
AttributeValue_::Value(v) => v.ast_debug(w),
AttributeValue_::ModuleAccess(n) => n.ast_debug(w),
AttributeValue_::List(items) => {
w.write("[");
w.list(items, ", ", |w, item| {
item.value.ast_debug(w);
false
});
w.write("]");
},
AttributeValue_::Range {
lo,
hi,
inclusive_hi,
} => {
lo.value.ast_debug(w);
w.write(if *inclusive_hi { "..=" } else { ".." });
hi.value.ast_debug(w);
},
AttributeValue_::Union(items) => {
w.list(items, " | ", |w, item| {
item.value.ast_debug(w);
false
});
},
}
}
}
Expand All @@ -1217,6 +1255,14 @@ impl AstDebug for Attribute_ {
});
w.write(")");
},
Attribute_::Constrained(n, op, v) => {
w.write(&format!("{}", n));
w.write(match op {
ConstraintOp::Ne => " != ",
ConstraintOp::In => " in ",
});
v.ast_debug(w);
},
}
}
}
Expand Down
6 changes: 5 additions & 1 deletion third_party/move/move-compiler-v2/legacy-move-compiler/src/parser/lexer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ pub enum Tok {
Minus,
Period,
PeriodPeriod,
PeriodPeriodEqual,
Slash,
Colon,
ColonColon,
Expand Down Expand Up @@ -130,6 +131,7 @@ impl fmt::Display for Tok {
Minus => "-",
Period => ".",
PeriodPeriod => "..",
PeriodPeriodEqual => "..=",
Slash => "/",
Colon => ":",
ColonColon => "::",
Expand Down Expand Up @@ -649,7 +651,9 @@ fn find_token(
}
},
'.' => {
if text.starts_with("..") {
if text.starts_with("..=") {
(Tok::PeriodPeriodEqual, 3)
} else if text.starts_with("..") {
(Tok::PeriodPeriod, 2)
} else {
(Tok::Period, 1)
Expand Down
Loading
Loading