Skip to content

Commit

Permalink
add ability check on number constraints
Browse files Browse the repository at this point in the history
  • Loading branch information
rahxephon89 committed Nov 21, 2024
1 parent dbdb613 commit b9355c7
Show file tree
Hide file tree
Showing 10 changed files with 168 additions and 14 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -11,16 +11,11 @@ error: type `S` is missing required ability `key` (type was inferred)
= required by instantiating type parameter `R:key` of function `both`

error: type `Coin` is missing required ability `copy` (type was inferred)
┌─ tests/ability-check/v1-typing/module_call_constraints_not_satisfied.move:29:9
error: constraint `integer` does not have required ability `key`
┌─ tests/ability-check/v1-typing/module_call_constraints_not_satisfied.move:29:14
15 │ fun both<R: key, C: copy>(_r: R, _c: C) {
│ - declaration of type parameter `C`
·
29 │ both(0, Coin{})
│ ^^^^
= required by instantiating type parameter `C:copy` of function `both`
│ ^

error: type `Box<C>` is missing required ability `key` (type was inferred)
┌─ tests/ability-check/v1-typing/module_call_constraints_not_satisfied.move:33:9
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,11 @@

Diagnostics:
error: constraint `integer` does not have required ability `key`
┌─ tests/ability-check/v1-typing/pack_constraint_not_satisfied.move:7:27
7 │ R {r:_ } = R { r: 0 };
│ ^

error: type `Coin` is missing required ability `drop` (type was inferred)
┌─ tests/ability-check/v1-typing/pack_constraint_not_satisfied.move:8:9
Expand All @@ -11,6 +17,17 @@ error: type `Coin` is missing required ability `drop` (type was inferred)
= required by instantiating type parameter `T:drop` of struct `S`

error: type `R<*error*>` is missing required ability `key` (type was inferred)
┌─ tests/ability-check/v1-typing/pack_constraint_not_satisfied.move:12:30
3 │ struct R<T: key> { r: T }
│ - declaration of type parameter `T`
·
12 │ R {r: R { r: _ } } = R { r: R { r: 0 }};
│ ^
= required by instantiating type parameter `T:key` of struct `R`

error: type `R<key>` is missing required ability `key` (type was inferred)
┌─ tests/ability-check/v1-typing/pack_constraint_not_satisfied.move:12:30
Expand All @@ -22,6 +39,12 @@ error: type `R<key>` is missing required ability `key` (type was inferred)
= required by instantiating type parameter `T:key` of struct `R`

error: constraint `integer` does not have required ability `key`
┌─ tests/ability-check/v1-typing/pack_constraint_not_satisfied.move:12:44
12 │ R {r: R { r: _ } } = R { r: R { r: 0 }};
│ ^

error: type `Coin` is missing required ability `drop` (type was inferred)
┌─ tests/ability-check/v1-typing/pack_constraint_not_satisfied.move:13:16
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@

Diagnostics:
bug: unexpected type: _
┌─ tests/ability-check/v1-typing/pack_constraint_not_satisfied2.move:6:9
error: constraint `integer` does not have required ability `key`
┌─ tests/ability-check/v1-typing/pack_constraint_not_satisfied2.move:7:27
6fun t0() {
^^
7 R {r:_ } = R { r: 0 };
^
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
// -- Model dump before bytecode pipeline
module 0x8675309::M {
struct R<T> {
r: T,
}
struct X<T> {
r: T,
}
private fun t0() {
{
let y: R<X<u64>> = pack M::R<X<u64>>(pack M::X<u64>(0));
{
let M::R<X<u64>>{ r: _r } = y;
Tuple()
}
}
}
} // end 0x8675309::M

// -- Sourcified model before bytecode pipeline
module 0x8675309::M {
struct R<T: key> {
r: T,
}
struct X<T> has drop, key {
r: T,
}
fun t0() {
let y = R<X<u64>>{r: X<u64>{r: 0}};
let R<X<u64>>{r: _r} = y;
}
}

============ initial bytecode ================

[variant baseline]
fun M::t0() {
var $t0: 0x8675309::M::R<0x8675309::M::X<u64>>
var $t1: 0x8675309::M::X<u64>
var $t2: u64
var $t3: 0x8675309::M::X<u64>
0: $t2 := 0
1: $t1 := pack 0x8675309::M::X<u64>($t2)
2: $t0 := pack 0x8675309::M::R<0x8675309::M::X<u64>>($t1)
3: $t3 := unpack 0x8675309::M::R<0x8675309::M::X<u64>>($t0)
4: return ()
}


============ bytecode verification succeeded ========
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
module 0x8675309::M {
// struct Coin {}
struct R<T: key> { r: T }
struct X<T> has key, drop {
r: T
}
// struct S<T: drop> has drop { c: T }

fun t0() {
let y = R { r: X { r: 0} };
let R { r: _r } = y;
// S { c: Coin {} };
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@

Diagnostics:
error: constraint `integer` does not have required ability `key`
┌─ tests/bytecode-generator/bug_14629_fail.move:6:32
6 │ let R { r: _ } = R {r: 0};
│ ^
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
module 0x8675309::M {
// struct Coin {}
struct R<T: key> { r: T }

fun t1() {
let R { r: _ } = R {r: 0};
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,12 @@ error: cannot use `integer` with an operator which expects a value of type `R`
14 │ let () = move_to<R>(a, 0);
│ ^

error: constraint `integer` does not have required ability `key`
┌─ tests/checking/typing/global_builtins_invalid.move:15:29
15 │ let () = move_to(a, 0);
│ ^

error: cannot use `integer` with an operator which expects a value of type `address`
┌─ tests/checking/typing/global_builtins_invalid.move:16:39
Expand Down
3 changes: 2 additions & 1 deletion third_party/move/move-model/src/builder/exp_builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2089,7 +2089,8 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo
Pattern::Struct(sid, std, variant, patterns) => {
let mut new_inst = vec![];
for ty in &std.inst {
let nty = subs.specialize(ty);
// use `specialize_with_defaults` to get type info from constraints
let nty: Type = subs.specialize_with_defaults(ty);
new_inst.push(nty);
}
let mut new_std = std.clone();
Expand Down
52 changes: 51 additions & 1 deletion third_party/move/move-model/src/ty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -459,6 +459,7 @@ impl Constraint {
subs: &mut Substitution,
loc: &Loc,
other: &Constraint,
ctx_opt: Option<ConstraintContext>,
) -> Result<bool, TypeUnificationError> {
match (&mut *self, other) {
(Constraint::SomeNumber(opts1), Constraint::SomeNumber(opts2)) => {
Expand Down Expand Up @@ -543,6 +544,32 @@ impl Constraint {
*a1 = a1.union(*a2);
Ok(true)
},
// After the above checks on same type of contraint
// Check compatibility between ability and number
(Constraint::HasAbilities(a1, _), Constraint::SomeNumber(_)) => {
let unsupported_abilities = a1.setminus(AbilitySet::PRIMITIVES);
if !unsupported_abilities.is_empty() {
return Err(TypeUnificationError::MissingAbilitiesForConstraints(
loc.clone(),
other.clone(),
unsupported_abilities,
ctx_opt,
));
}
Ok(false)
},
(Constraint::SomeNumber(_), Constraint::HasAbilities(a1, _)) => {
let unsupported_abilities = a1.setminus(AbilitySet::PRIMITIVES);
if !unsupported_abilities.is_empty() {
return Err(TypeUnificationError::MissingAbilitiesForConstraints(
loc.clone(),
self.clone(),
unsupported_abilities,
ctx_opt,
));
}
Ok(false)
},
// After the above checks, if one of the constraints is
// accumulating, indicate its compatible but cannot be joined.
(c1, c2) if c1.accumulating() || c2.accumulating() => Ok(false),
Expand Down Expand Up @@ -702,6 +729,8 @@ pub enum TypeUnificationError {
),
/// The `HasAbilities` constraint failed: `MissingAbilities(loc, ty, missing, ctx)`.
MissingAbilities(Loc, Type, AbilitySet, Option<ConstraintContext>),
/// The `HasAbilities` constraint failed: `MissingAbilitiesForConstraints(loc, ctr, missing, ctx)`.
MissingAbilitiesForConstraints(Loc, Constraint, AbilitySet, Option<ConstraintContext>),
/// The two constraints are incompatible and cannot be joined.
ConstraintsIncompatible(Loc, Constraint, Constraint),
/// A cyclic substitution when trying to unify the given types.
Expand Down Expand Up @@ -1668,7 +1697,7 @@ impl Substitution {
let mut absorbed = false;
for (_, _, c) in current.iter_mut() {
// Join constraints. If join returns true the constraint is absorbed.
absorbed = c.join(context, self, &loc, &ctr)?;
absorbed = c.join(context, self, &loc, &ctr, ctx_opt.clone())?;
if absorbed {
break;
}
Expand Down Expand Up @@ -3015,6 +3044,27 @@ impl TypeUnificationError {
labels,
)
},
TypeUnificationError::MissingAbilitiesForConstraints(_, ctr, missing, ctx_opt) => {
let (note, hints, labels) = ctx_opt
.as_ref()
.map(|ctx| ctx.describe(display_context))
.unwrap_or_default();
(
format!(
"constraint `{}` does not have required {} `{}`{}",
ctr.display(display_context),
pluralize("ability", missing.iter().count()),
missing,
if !note.is_empty() {
format!(" ({})", note)
} else {
"".to_string()
}
),
hints,
labels,
)
},
TypeUnificationError::ConstraintUnsatisfied(_, ty, order, constr, ctx_opt) => {
let item_name = || match ctx_opt {
Some(ConstraintContext {
Expand Down

0 comments on commit b9355c7

Please sign in to comment.