Skip to content

Commit

Permalink
[compiler v2][type checker] Make arithmetic operators generic with co…
Browse files Browse the repository at this point in the history
…nstraints (#9792)

* [compiler v2][type checker] Make arithmetic operators generic with constraints

Until now, we had represented arithmetic operators via overloads. For instance, we had `fun _+_(u8,u8):u8, fun _+_(u16,u16):u16` and so on for all integer types. The problem with this approach is that it does not work for constants, as described in #9330. Move allows to write `1+2` and this expression gets its type inferred from the context.

In this PR, arithmetic ops are represented not longer as overloads but as generic functions with constraints. Basically:

```
fun _+_<A>(x: A, y: A): A where A:u8|u16|u32|..|u256;
fun _-_<A>(...)...
```

This has the following effects:

- Expressions over constants inherit their generic result type (that is, `1 + 2` does not fix the operator to a specific integer type. Instead the context may do this.)
- Error messages get better. The messages where we just printed non-matching overloads were not very good, no we see more precise error messages.

Technically, this needed some refinements of the type constraint system. Also, some error reporting has been fixed which was before only working in very specific contexts.

* Addressing reviewer comments.

* Addressing more reviewer comments. This revamps the generation of error messages, removing some older broken heuristics and trying to fix the problem of orientation of 'expected' vs 'found' at the core. Some context annotation 'from assignment context' not tries to clarify the error message if the typing error is for an lvalue, where the expected type is a _lower bound_ instead of an upper bound, which may leads to confusion for end users. The messages are now more systematic but perhaps a bit harder to understand, yet this is not trivial to fix and we have to iterate on this.
  • Loading branch information
wrwg authored Sep 1, 2023
1 parent e3e4c26 commit 6a1cded
Show file tree
Hide file tree
Showing 89 changed files with 1,303 additions and 2,338 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ module 0x42::assign {
}
private fun assign_pattern(s: assign::S,f: u64,h: u64) {
assign::S{ f: f: u64, g: assign::T{ h: h: u64 } } = s;
Add(f, h)
Add<u64>(f, h)
}
private fun assign_struct(s: &mut assign::S) {
s = pack assign::S(42, pack assign::T(42));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module 0x42::borrow {
}
private fun mut_expr(x: u64) {
{
let r: &mut u64 = Borrow(Mutable)(Add(x, 1));
let r: &mut u64 = Borrow(Mutable)(Add<u64>(x, 1));
r = 22;
Deref(r)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,20 @@
module 0x42::if_else {
private fun if_else(cond: bool,x: u64) {
if cond {
Add(x, 1)
Add<u64>(x, 1)
} else {
Sub(x, 1)
Sub<u64>(x, 1)
}
}
private fun if_else_nested(cond: bool,x: u64) {
if Gt(if cond {
Add(x, 1)
if Gt<u64>(if cond {
Add<u64>(x, 1)
} else {
Sub(x, 1)
Sub<u64>(x, 1)
}, 10) {
Mul(x, 2)
Mul<u64>(x, 2)
} else {
Div(x, 2)
Div<u64>(x, 2)
}
}
} // end 0x42::if_else
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,17 +2,17 @@
module 0x42::loops {
private fun nested_loop(x: u64) {
loop {
if Gt(x, 0) {
if Gt<u64>(x, 0) {
loop {
if Gt(x, 10) {
x: u64 = Sub(x, 1);
if Gt<u64>(x, 10) {
x: u64 = Sub<u64>(x, 1);
break;
Tuple()
} else {
break
}
};
x: u64 = Sub(x, 1);
x: u64 = Sub<u64>(x, 1);
continue;
Tuple()
} else {
Expand All @@ -23,8 +23,8 @@ module 0x42::loops {
}
private fun while_loop(x: u64) {
loop {
if Gt(x, 0) {
x: u64 = Sub(x, 1);
if Gt<u64>(x, 0) {
x: u64 = Sub<u64>(x, 1);
Tuple()
} else {
break
Expand All @@ -34,7 +34,7 @@ module 0x42::loops {
}
private fun while_loop_with_break_and_continue(x: u64) {
loop {
if Gt(x, 0) {
if Gt<u64>(x, 0) {
if Eq<u64>(x, 42) {
break
} else {
Expand All @@ -45,7 +45,7 @@ module 0x42::loops {
} else {
Tuple()
};
x: u64 = Sub(x, 1);
x: u64 = Sub<u64>(x, 1);
Tuple()
} else {
break
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
module 0x42::loop_invalid {
private fun misplaced_break(x: u64) {
loop {
if Gt(x, 0) {
if Gt<u64>(x, 0) {
break
} else {
break
Expand All @@ -14,7 +14,7 @@ module 0x42::loop_invalid {
private fun misplaced_continue(x: u64) {
continue;
loop {
if Gt(x, 0) {
if Gt<u64>(x, 0) {
continue
} else {
break
Expand Down
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
// ---- Model Dump
module 0x42::operators {
private fun arithm(x: u64,y: u64) {
Add(x, Mod(Mul(Div(y, Sub(x, y)), y), x))
Add<u64>(x, Mod<u64>(Mul<u64>(Div<u64>(y, Sub<u64>(x, y)), y), x))
}
private fun bits(x: u64,y: u8) {
BitAnd(Shl(x, y), x)
BitAnd<u64>(Shl<u64>(x, y), x)
}
private fun bools(x: bool,y: bool) {
Or(Or(Or(And(x, y), And(x, Not(y))), And(Not(x), y)), And(Not(x), Not(y)))
Expand All @@ -16,7 +16,7 @@ module 0x42::operators {
Neq<T>(x, y)
}
private fun order(x: u64,y: u64) {
And(And(And(Lt(x, y), Le(x, y)), Not(Gt(x, y))), Not(Ge(x, y)))
And(And(And(Lt<u64>(x, y), Le<u64>(x, y)), Not(Gt<u64>(x, y))), Not(Ge<u64>(x, y)))
}
} // end 0x42::operators

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,12 @@ module 0x42::tuple {
f: u64,
}
private fun tuple(x: u64) {
Tuple(x, pack tuple::S(Add(x, 1)))
Tuple(x, pack tuple::S(Add<u64>(x, 1)))
}
private fun use_tuple(x: u64) {
{
let (x: u64, tuple::S{ f: y: u64 }) = tuple::tuple(x);
Add(x, y)
Add<u64>(x, y)
}
}
} // end 0x42::tuple
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ module 0x42::tuple_invalid {
f: u64,
}
private fun tuple(x: u64) {
Tuple(x, pack tuple_invalid::S(Add(x, 1)))
Tuple(x, pack tuple_invalid::S(Add<u64>(x, 1)))
}
private fun use_tuple1(x: u64) {
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,10 @@ error: expected `S` but found `M::S`
│ ^^^^

error: invalid call of `M::bar`: expected `M::S` but found `S` for argument 1
┌─ tests/checking/naming/generics_shadowing_invalid.move:9:9
┌─ tests/checking/naming/generics_shadowing_invalid.move:9:13
9 │ bar(s1);
^^^^^^^
^^

error: expected `S` but found `M::S`
┌─ tests/checking/naming/generics_shadowing_invalid.move:10:9
Expand Down
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
// ---- Model Dump
module 0x42::M {
private fun bar(x: u64) {
if Gt(x, 0) {
if Gt<u64>(x, 0) {
Tuple()
} else {
Abort(1)
};
Sub(x, 1)
Sub<u64>(x, 1)
}
} // end 0x42::M
Original file line number Diff line number Diff line change
@@ -1,36 +1,36 @@

Diagnostics:
error: expected `&u64` but found `integer`
┌─ tests/checking/typing/assign_unpack_references_invalid.move:9:13
error: expected `&u64` but found `integer` (from assignment or declaration context)
┌─ tests/checking/typing/assign_unpack_references_invalid.move:9:9
9 │ f = 0;
^
│ ^

error: expected `&M::S` but found `M::S`
error: expected `&M::S` but found `M::S` (from assignment or declaration context)
┌─ tests/checking/typing/assign_unpack_references_invalid.move:10:9
10 │ s2 = S { f: 0 }
│ ^^

error: expected `&mut u64` but found `integer`
┌─ tests/checking/typing/assign_unpack_references_invalid.move:17:13
error: expected `&mut u64` but found `integer` (from assignment or declaration context)
┌─ tests/checking/typing/assign_unpack_references_invalid.move:17:9
17 │ f = 0;
^
│ ^

error: expected `&mut M::S` but found `M::S`
error: expected `&mut M::S` but found `M::S` (from assignment or declaration context)
┌─ tests/checking/typing/assign_unpack_references_invalid.move:18:9
18 │ s2 = S { f: 0 }
│ ^^

error: mutability mismatch (&mut != &)
error: mutability mismatch (&mut != &) (from assignment or declaration context)
┌─ tests/checking/typing/assign_unpack_references_invalid.move:26:9
26 │ f = &0;
│ ^

error: mutability mismatch (&mut != &)
error: mutability mismatch (&mut != &) (from assignment or declaration context)
┌─ tests/checking/typing/assign_unpack_references_invalid.move:27:9
27 │ s2 = &S { f: 0 }
Expand Down
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@

Diagnostics:
error: tuples have different arity (0 != 3)
error: tuples have different arity (0 != 3) (from assignment or declaration context)
┌─ tests/checking/typing/assign_wrong_arity.move:7:9
7 │ x = (0, 1, 2);
│ ^

error: expected `()` but found `integer`
┌─ tests/checking/typing/assign_wrong_arity.move:8:14
error: expected `()` but found `integer` (from assignment or declaration context)
┌─ tests/checking/typing/assign_wrong_arity.move:8:9
8 │ () = 0;
^
^^

error: expected 4 item(s), found 3
┌─ tests/checking/typing/assign_wrong_arity.move:11:9
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,11 @@ error: expected `M::S` but found `M::R`
9 │ (S { g }, R { f }) = (R{ f: 0 }, R{ f: 1 });
│ ^^^^^^^

error: expected `()` but found `integer`
┌─ tests/checking/typing/assign_wrong_type.move:17:14
error: expected `()` but found `integer` (from assignment or declaration context)
┌─ tests/checking/typing/assign_wrong_type.move:17:9
17 │ () = 0;
^
^^

error: expected 4 item(s), found 3
┌─ tests/checking/typing/assign_wrong_type.move:18:9
Expand All @@ -30,25 +30,25 @@ error: expected 2 item(s), found 3
19 │ (x, b, R{f}) = (0, false);
│ ^^^^^^^^^^^^

error: expected `bool` but found `integer`
┌─ tests/checking/typing/assign_wrong_type.move:27:28
error: expected `bool` but found `integer` (from assignment or declaration context)
┌─ tests/checking/typing/assign_wrong_type.move:27:10
27 │ (x, b, R{f}, r) = (0, false, R{f: 0}, R{f: 0});
^
│ ^

error: expected `bool` but found `integer`
┌─ tests/checking/typing/assign_wrong_type.move:24:17
error: expected `integer` but found `bool` (from assignment or declaration context)
┌─ tests/checking/typing/assign_wrong_type.move:27:13
24let b = 0;
^
27(x, b, R{f}, r) = (0, false, R{f: 0}, R{f: 0});
│ ^

error: expected `address` but found `u64`
error: expected `address` but found `u64` (from assignment or declaration context)
┌─ tests/checking/typing/assign_wrong_type.move:27:18
27 │ (x, b, R{f}, r) = (0, false, R{f: 0}, R{f: 0});
│ ^

error: expected `M::S` but found `M::R`
error: expected `M::S` but found `M::R` (from assignment or declaration context)
┌─ tests/checking/typing/assign_wrong_type.move:27:22
27 │ (x, b, R{f}, r) = (0, false, R{f: 0}, R{f: 0});
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,17 +4,17 @@ module 0x8675309::M {
f: u64,
}
private fun t0(x: u64,r: M::R) {
Add(0, 0);
Add(1, 0);
Add(0, 1);
Add(0, 1);
Add(0, 1);
Add(0, 1);
Add(0, 1);
Add(0, 1);
Add(x, x);
Add(select M::R.f(r), select M::R.f(r));
Add(Add(Add(1, select M::R.f(r)), select M::R.f(r)), 0);
Add<u64>(0, 0);
Add<u64>(1, 0);
Add<u64>(0, 1);
Add<u8>(0, 1);
Add<u8>(0, 1);
Add<u128>(0, 1);
Add<u128>(0, 1);
Add<u64>(0, 1);
Add<u64>(x, x);
Add<u64>(select M::R.f(r), select M::R.f(r));
Add<u64>(Add<u64>(Add<u64>(1, select M::R.f(r)), select M::R.f(r)), 0);
{
let M::R{ f: _ } = r;
Tuple()
Expand Down
Loading

0 comments on commit 6a1cded

Please sign in to comment.