Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
4 changes: 2 additions & 2 deletions ml-proto/spec/check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -134,9 +134,9 @@ let rec check_expr c et e =
check_expr_opt c (label c x) eo e.at

| Br_if (x, eo, e) ->
check_expr_opt c et eo e.at;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This doesn't look right, it breaks the implicit result dropping subsumption that is allowed for all other expressions. For example, you could no longer use a br_if with argument in a block, as your test cases already demonstrate:

(block (br_if $l (arg) (cond)) (other))

becomes a type error. That violates a basic design principle of the type system, and doesn't make sense from a practical perspective.

However, the previous version of this PR changed the typing of br and return. As @JSStats pointed out, it effectively reverted PR #180, which addressed issue #179. We could work around that with more special casing, but that would be fairly ugly, and I'm not convinced it's worth it.

I think the least inconsistent way to implement this change is to reach agreement that we undo #180. @jcbeyler, @lukewagner, would you be okay with that? It's not ideal either, but at this point, I don't have a particularly strong opinion about that one. It's still much better than introducing special case rules for optional arguments, which I'd very much like to avoid.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

From a purely practical perspective, there's no problem with making

    (block (br_if $l (arg) (cond)) (other))

a type error, because one can achieve a similar effect writing this code as

   (block (arg) (br_if $l (cond)) (other))

The practical restriction is that one can't use br_if to pass a value to one successor and drop it in the other. However, this restriction is consistent with how I expect to use br_if, and it's consistent with br_if's operand being strict. It's evaluated for both values of the condition, so it makes sense to type-check it for both values of the condition.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rossberg-chromium Rather than revert, could we do br0/br0_if? That way we keep the syntactic arity match (which is what postorder needs) and then this PR would switch to check_type of an expr and the result-dropping works.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@sunfishcode, that's not correct, the two expressions are completely different. The latter won't transfer arg to $l, and thus won't type-check if $l actually requires a value. There is no trivial way to rewrite the former under the current PR. You'll essentially need the encoding of a "drop" operator, avoiding which was a core design goal of the type system. (The simplest such encoding I can see would be (block (if (i32.const 1) (br_if $l (arg) (cond)) (other)).)

@lukewagner, special-casing typing on label arity would paint us into a corner regarding multiple values. I think we need a more future-proof solution. Reverting #180 is the one I can see.

I'm starting to wish we had a let-like construct, then we could easily desugar (br_if $l (arg) (cond)) as follows and get the desired typing for free:

(let $x (arg) (block (if (cond) (br $l (get_value $x))) (get_value $x)))

:)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rossberg-chromium If we decoupled construction of tuples of values from br (such that you'd write (br_if $1 (tuple a b) (cond)) or just (br_if $1 (call foo_returning_tuple) (cond)), then is there a problem? In the model of this I have in my head, a tuple would just be 1 entry on the expr stack (so that means each entry on the expr stack is a Vector<Pair<Def,Type>> where Def is your compiler SSA definition) so you still want the binary br0/br split.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

By any lucky chance are you so inclined to write such a PR :) ?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rossberg-chromium Re: stack machine: yes, there are certainly CL implementations that are stack machines and these support multiple value expressions, but they keep a count of values on the stack at some points or a frame pointer as a reference position, but I think you are right that wasm would not need to do this because the runtime compiler always knows the number of actual and expected values at compile time, so even if wasm allows a mismatch between expected values of br_if consumers it would still know to pop any unused values. The only remaining concern might be if people expected to execute the AST literally as a byte code and then might need to keep track of the number of expression values at runtime (as opposed to the runtime compiler which can account for them at compile time).

I notice that if desugars to if_else in the ml-proto and that it can return a different number of values depending on the condition, and it might need to be the responsibility of the operators to return a consistent number of values here so if would want to return the empty-values irrespective of condition. Also if_else and selection might want to be defined to return a consistent number of values irrespective of the condition.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@JSStats, under the tuple interpretation used in ml-proto's eval, it is neither necessary nor desirable to do that. Only a stack machine would require adjustments. But the approach you suggest would be the wrong one. Instead, you'd need to pop off the stack whenever the type system uses subsumption (i.e., "forgets" a non-empty value in check_type). That occurs in more places than just branches, e.g. (block (i32.const 0) (i32.const 1)) requires dropping the first value. Branches do not need any special treatment.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rossberg-chromium Sorry, it's not clear to me what you are referring to as 'neither necessary nor desirable to do that'. As I understand your position, the 'tuple' proposal, it would only be possible to either discard the entire tuple or consume all the values, whereas for my 'values' proposal it would be possible to consume any length head of the values which includes both none and all as limiting cases and thus subsumes your tuple proposal and I believe can be demonstrate to be practically more useful and efficiently at encoding the lowered wasm for at least some languages. I believe these two proposals can be judged on their efficiency at encoding lowered code, and that a 'right' or 'wrong' subjective judgement is not necessary, and perhaps we could stop using such words and I apologise if I have framed some aspects of this issue in those terms.

In any case I still fail to see how tracking the number of values can be avoided. As noted, the runtime compiler seems to know the number of values at compile time so can optimize away tracking the number of values, but I fail to see how an interpreter of the literal AST could avoid tracking the number of values, be it the number of values in a tuple or the number of values in a values list? Even if the interpreter boxed the tuple, the tuple object would be encoding the number of values. Sorry if I am missing some obvious optimization that the tuple strategy supports, but perhaps you could share this if there is one?

I certainly agree that accounting for differences between the number of expected and actual values is a general operation and not specific to branches, and I just gave this as an example because this is the topic of this issue. However bf_if does seem to be a unique operation in wasm as it is the only operation that has multiple consumers of its result values and this might make it uniquely useful for discussing some aspects of the type system. Every other case of multiple references seems to go through variables. I support each consumer being handled separately for br_if so that one consumer can drop the values and the other consume them, and for the reason that this is more flexible and can thus increase the efficiency of coding some patterns.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@JSStats, you are now talking about a language extension again, I wasn't. But even with more general subtyping like you propose, you wouldn't need or want to adjust tuples in the operational semantics. In a tuple-based implementation, subtyping just works, without coercing, because there is no operation that can ever observe excess values. They just get ignored when decomposing a tuple. A real-world implementation might of course want to implement that differently, e.g. a stack-based one has to.

check_expr_opt c (label c x) eo e.at;
check_expr c (Some Int32Type) e;
check_type None et e.at
check_expr c (Some Int32Type) e

| If (e1, e2, e3) ->
check_expr c (Some Int32Type) e1;
Expand Down
2 changes: 1 addition & 1 deletion ml-proto/spec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ let rec eval_expr (c : config) (e : expr) =
| Br_if (x, eo, e) ->
let v = eval_expr_opt c eo in
let i = int32 (eval_expr c e) e.at in
if i <> 0l then raise (label c x v) else None
if i <> 0l then raise (label c x v) else v

| If (e1, e2, e3) ->
let i = int32 (eval_expr c e1) e1.at in
Expand Down
180 changes: 129 additions & 51 deletions ml-proto/test/labels.wast
Original file line number Diff line number Diff line change
Expand Up @@ -90,28 +90,6 @@
)
)

(func $br_if0 (result i32)
(local $i i32)
(set_local $i (i32.const 0))
(block $outer
(block $inner
(br_if $inner (i32.const 0))
(set_local $i (i32.or (get_local $i) (i32.const 0x1)))
(br_if $inner (i32.const 1))
(set_local $i (i32.or (get_local $i) (i32.const 0x2)))
)
(br_if $outer (set_local $i (i32.or (get_local $i) (i32.const 0x4))) (i32.const 0))
(set_local $i (i32.or (get_local $i) (i32.const 0x8)))
(br_if $outer (set_local $i (i32.or (get_local $i) (i32.const 0x10))) (i32.const 1))
(set_local $i (i32.or (get_local $i) (i32.const 0x20)))
)
)

(func $br_if1 (result i32)
(block $l0
(br_if $l0 (block $l1 (br $l1 (i32.const 1))) (i32.const 1))
(i32.const 1)))

(func $br_if2 (result i32)
(block $l0
(if (i32.const 1)
Expand All @@ -120,15 +98,15 @@
(br $l1 (i32.const 1)))))
(i32.const 1)))

(func $br_if3 (result i32)
(local $i1 i32)
(i32.add (block $l0
(br_if $l0
(set_local $i1 (i32.const 1))
(set_local $i1 (i32.const 2)))
(i32.const 0))
(i32.const 0))
(get_local $i1))
(func $br_if4 (result f32)
(block $l
(br_if $l (f32.const 0) (i32.const 1))))

(func $br_if5 (param i32) (result f32)
(block $l
(f32.neg
(block $i
(br_if $l (f32.const 3) (get_local 0))))))

(func $misc1 (result i32)
(block $l1 (i32.xor (br $l1 (i32.const 1)) (i32.const 2)))
Expand All @@ -146,10 +124,9 @@
(export "loop5" $loop5)
(export "switch" $switch)
(export "return" $return)
(export "br_if0" $br_if0)
(export "br_if1" $br_if1)
(export "br_if2" $br_if2)
(export "br_if3" $br_if3)
(export "br_if4" $br_if4)
(export "br_if5" $br_if5)
(export "misc1" $misc1)
(export "misc2" $misc2)
)
Expand All @@ -169,29 +146,130 @@
(assert_return (invoke "return" (i32.const 0)) (i32.const 0))
(assert_return (invoke "return" (i32.const 1)) (i32.const 2))
(assert_return (invoke "return" (i32.const 2)) (i32.const 2))
(assert_return (invoke "br_if0") (i32.const 0x1d))
(assert_return (invoke "br_if1") (i32.const 1))
(assert_return (invoke "br_if2") (i32.const 1))
(assert_return (invoke "br_if3") (i32.const 2))
(assert_return (invoke "br_if4") (f32.const 0))
(assert_return (invoke "br_if5" (i32.const 0)) (f32.const -3))
(assert_return (invoke "br_if5" (i32.const 1)) (f32.const 3))
(assert_return (invoke "misc1") (i32.const 1))
(assert_return (invoke "misc2") (i32.const 1))

(assert_invalid (module (func (loop $l (br $l (i32.const 0))))) "arity mismatch")
(assert_invalid (module (func (block $l (f32.neg (br_if $l (i32.const 1))) (nop)))) "type mismatch")
(assert_invalid (module (func (block $l (f32.neg (br_if $l (i32.const 1))) (nop)))) "arity mismatch")

(assert_invalid (module (func (result f32) (block $l (br_if $l (f32.const 0) (i32.const 1))))) "type mismatch")
(assert_invalid (module (func (result i32) (block $l (br_if $l (f32.const 0) (i32.const 1))))) "type mismatch")
(assert_invalid (module (func (block $l (f32.neg (br_if $l (f32.const 0) (i32.const 1)))))) "arity mismatch")
(assert_invalid (module (func (param i32) (result i32) (block $l (f32.neg (br_if $l (f32.const 0) (get_local 0)))))) "type mismatch")
(assert_invalid (module (func (param i32) (result f32)
(block $l (f32.neg (block $i (br_if $l (f32.const 3) (get_local 0)))))))

;; If br_if has a value, it should be used in both successors.
(assert_invalid (module
(func (result i32)
(local $i i32)
(set_local $i (i32.const 0))
(block $outer
(block $inner
(br_if $inner (i32.const 0))
(set_local $i (i32.or (get_local $i) (i32.const 0x1)))
(br_if $inner (i32.const 1))
(set_local $i (i32.or (get_local $i) (i32.const 0x2)))
)
(br_if $outer (set_local $i (i32.or (get_local $i) (i32.const 0x4))) (i32.const 0))
(set_local $i (i32.or (get_local $i) (i32.const 0x8)))
(br_if $outer (set_local $i (i32.or (get_local $i) (i32.const 0x10))) (i32.const 1))
(set_local $i (i32.or (get_local $i) (i32.const 0x20)))
))
) "arity mismatch")

;; If br_if has a value, it should be used in both successors.
(assert_invalid (module
(func (result i32)
(block $l0
(br_if $l0 (block $l1 (br $l1 (i32.const 1))) (i32.const 1))
(i32.const 1)))
) "arity mismatch")

;; If br_if has a value, it should be used in both successors.
(assert_invalid (module
(func (result i32)
(local $i1 i32)
(i32.add (block $l0
(br_if $l0
(set_local $i1 (i32.const 1))
(set_local $i1 (i32.const 2)))
(i32.const 0))
(i32.const 0))
(get_local $i1))
) "arity mismatch")

;; If br_if has a value, it should be used in both successors.
(assert_invalid (module
(func
(loop $l0 $l1
(br $l0 (i32.const 0))))
) "arity mismatch")

;; If br_if has a value, it should be used in both successors.
(assert_invalid (module
(func
(block $l0
(br_if $l0 (nop) (i32.const 1))))
) "arity mismatch")

;; If br_if has a value, it should be used in both successors.
(assert_invalid (module
(func
(block $l0
(if_else (i32.const 1)
(br $l0 (block $l1 (br $l1 (i32.const 1))))
(block (block $l1 (br $l1 (i32.const 1))) (nop))
)
(i32.const 1)))
) "arity mismatch")

;; If br_if has a value, it should be used in both successors.
(assert_invalid (module
(func
(block $l
(f32.neg (br_if $l (f32.const 0) (i32.const 1)))))
) "arity mismatch")

;; br_if's own result type doesn't match the result type of the block it's in.
(assert_invalid (module
(func (param i32) (result f32)
(block $l
(f32.convert_s/i32
(block $i
(br_if $l (f32.const 3) (get_local 0)))))))
"type mismatch")

;; br_if's result value's type doesn't match the type of the destination block.
(assert_invalid (module
(func (param i32) (result f32)
(block $l
(i32.trunc_s/f32
(block $i
(br_if $l (f32.const 3) (get_local 0)))))))
"type mismatch")

;; br_if operand has incorrect type.
(assert_invalid (module
(func (param i32) (result f32)
(block $l
(f32.neg
(block $i
(br_if $l (i32.const 3) (get_local 0)))))))
"type mismatch")
(assert_invalid (module (func (block $l0 (br_if $l0 (nop) (i32.const 1)))))

;; Function return type is wrong.
(assert_invalid (module
(func (param i32) (result i32)
(block $l
(f32.neg
(block $i
(br_if $l (f32.const 3) (get_local 0)))))))
"type mismatch")

;; br_if result not used, but value's type doesn't match branched-to block.
(assert_invalid (module
(func (param i32) (result i32)
(block $l
(br_if $l (f32.const 3) (get_local 0))
(i32.const 0))))
"arity mismatch")
(assert_invalid (module (func (result i32)
(block $l0
(if_else (i32.const 1)
(br $l0 (block $l1 (br $l1 (i32.const 1))))
(block (block $l1 (br $l1 (i32.const 1))) (nop))
)
(i32.const 1)))) "arity mismatch")