From ea86c8df52bf6b895d8c5e8f1b5713ef07b9c5ba Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Wed, 20 Nov 2024 16:18:09 -0800 Subject: [PATCH] add ability check on number constraints --- .../module_call_constraints_not_satisfied.exp | 11 ++-- .../pack_constraint_not_satisfied.exp | 23 ++++++++ .../pack_constraint_not_satisfied2.exp | 8 +-- .../tests/bytecode-generator/bug_14629.exp | 50 ++++++++++++++++++ .../tests/bytecode-generator/bug_14629.move | 14 +++++ .../bytecode-generator/bug_14629_fail.exp | 7 +++ .../bytecode-generator/bug_14629_fail.move | 8 +++ .../typing/global_builtins_invalid.exp | 6 +++ .../move-model/src/builder/exp_builder.rs | 3 +- third_party/move/move-model/src/ty.rs | 52 ++++++++++++++++++- 10 files changed, 168 insertions(+), 14 deletions(-) create mode 100644 third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629.exp create mode 100644 third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629.move create mode 100644 third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629_fail.exp create mode 100644 third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629_fail.move diff --git a/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/module_call_constraints_not_satisfied.exp b/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/module_call_constraints_not_satisfied.exp index f6d70f0d9eaaf0..2fc26b83053e4a 100644 --- a/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/module_call_constraints_not_satisfied.exp +++ b/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/module_call_constraints_not_satisfied.exp @@ -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: 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` is missing required ability `key` (type was inferred) ┌─ tests/ability-check/v1-typing/module_call_constraints_not_satisfied.move:33:9 diff --git a/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/pack_constraint_not_satisfied.exp b/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/pack_constraint_not_satisfied.exp index 4dc6e79fbcfaaa..735d68e511b940 100644 --- a/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/pack_constraint_not_satisfied.exp +++ b/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/pack_constraint_not_satisfied.exp @@ -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 │ @@ -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 { 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` is missing required ability `key` (type was inferred) ┌─ tests/ability-check/v1-typing/pack_constraint_not_satisfied.move:12:30 │ @@ -22,6 +39,12 @@ error: type `R` 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 │ diff --git a/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/pack_constraint_not_satisfied2.exp b/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/pack_constraint_not_satisfied2.exp index 159105ab0cca0b..0310e87e78cca6 100644 --- a/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/pack_constraint_not_satisfied2.exp +++ b/third_party/move/move-compiler-v2/tests/ability-check/v1-typing/pack_constraint_not_satisfied2.exp @@ -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 │ -6 │ fun t0() { - │ ^^ +7 │ R {r:_ } = R { r: 0 }; + │ ^ diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629.exp new file mode 100644 index 00000000000000..d9e172ab15ba61 --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629.exp @@ -0,0 +1,50 @@ +// -- Model dump before bytecode pipeline +module 0x8675309::M { + struct R { + r: T, + } + struct X { + r: T, + } + private fun t0() { + { + let y: R> = pack M::R>(pack M::X(0)); + { + let M::R>{ r: _r } = y; + Tuple() + } + } + } +} // end 0x8675309::M + +// -- Sourcified model before bytecode pipeline +module 0x8675309::M { + struct R { + r: T, + } + struct X has drop, key { + r: T, + } + fun t0() { + let y = R>{r: X{r: 0}}; + let R>{r: _r} = y; + } +} + +============ initial bytecode ================ + +[variant baseline] +fun M::t0() { + var $t0: 0x8675309::M::R<0x8675309::M::X> + var $t1: 0x8675309::M::X + var $t2: u64 + var $t3: 0x8675309::M::X + 0: $t2 := 0 + 1: $t1 := pack 0x8675309::M::X($t2) + 2: $t0 := pack 0x8675309::M::R<0x8675309::M::X>($t1) + 3: $t3 := unpack 0x8675309::M::R<0x8675309::M::X>($t0) + 4: return () +} + + +============ bytecode verification succeeded ======== diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629.move b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629.move new file mode 100644 index 00000000000000..604b2a158fe16b --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629.move @@ -0,0 +1,14 @@ +module 0x8675309::M { + // struct Coin {} + struct R { r: T } + struct X has key, drop { + r: T + } + // struct S has drop { c: T } + + fun t0() { + let y = R { r: X { r: 0} }; + let R { r: _r } = y; + // S { c: Coin {} }; + } +} diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629_fail.exp b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629_fail.exp new file mode 100644 index 00000000000000..2a80c7c6433bdc --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629_fail.exp @@ -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}; + │ ^ diff --git a/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629_fail.move b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629_fail.move new file mode 100644 index 00000000000000..839d55f56bf5e1 --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/bytecode-generator/bug_14629_fail.move @@ -0,0 +1,8 @@ +module 0x8675309::M { + // struct Coin {} + struct R { r: T } + + fun t1() { + let R { r: _ } = R {r: 0}; + } +} diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins_invalid.exp b/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins_invalid.exp index 73c27aa0989125..8297687e57d656 100644 --- a/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins_invalid.exp +++ b/third_party/move/move-compiler-v2/tests/checking/typing/global_builtins_invalid.exp @@ -42,6 +42,12 @@ error: cannot use `integer` with an operator which expects a value of type `R` 14 │ let () = move_to(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 │ diff --git a/third_party/move/move-model/src/builder/exp_builder.rs b/third_party/move/move-model/src/builder/exp_builder.rs index 992dbb07cf6038..8f16fa60111dec 100644 --- a/third_party/move/move-model/src/builder/exp_builder.rs +++ b/third_party/move/move-model/src/builder/exp_builder.rs @@ -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(); diff --git a/third_party/move/move-model/src/ty.rs b/third_party/move/move-model/src/ty.rs index 2bb9288cbd53b1..844550ae7024d8 100644 --- a/third_party/move/move-model/src/ty.rs +++ b/third_party/move/move-model/src/ty.rs @@ -459,6 +459,7 @@ impl Constraint { subs: &mut Substitution, loc: &Loc, other: &Constraint, + ctx_opt: Option, ) -> Result { match (&mut *self, other) { (Constraint::SomeNumber(opts1), Constraint::SomeNumber(opts2)) => { @@ -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), @@ -702,6 +729,8 @@ pub enum TypeUnificationError { ), /// The `HasAbilities` constraint failed: `MissingAbilities(loc, ty, missing, ctx)`. MissingAbilities(Loc, Type, AbilitySet, Option), + /// The `HasAbilities` constraint failed: `MissingAbilitiesForConstraints(loc, ctr, missing, ctx)`. + MissingAbilitiesForConstraints(Loc, Constraint, AbilitySet, Option), /// The two constraints are incompatible and cannot be joined. ConstraintsIncompatible(Loc, Constraint, Constraint), /// A cyclic substitution when trying to unify the given types. @@ -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; } @@ -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 {