Type-check dead code and introduce assert_soft_invalid

[rossberg]

As discussed off-line, we want to require valid code to be type-correct even in dead code, but allow engines to skip its validation. That is analogous to the liberty we give engines for validating individual functions lazily (which may include not at all if they are never called).

Edit: The motivation for this design choice is that typing rules should be simple but permissive enough and not require programmers or code generators to consider reachability. At the same time, it can be beneficial for implementations to be able to ignore dead code. The design represents a compromise: we only specify code to be valid if all instructions type-check, whether reachable or not. At the same time, we do not require (but still allow) engines to actually check the validity of code they can prove is never executed. The spec implements full checking, but the test suite distinguishes code that has to be identified as invalid by all engines (assert_invalid) and invalid code that they don't need to diagnose because it is unreachable (assert_soft_invalid).

This patch is going back to type-checking of dead code (with unconstrained initial stack), but respective tests use the new assert_soft_invalid assertion, which can be turned off for implementations that choose to skip dead code validation.

Edit 2: Here is a sketch of a type-checking algorithm that engines can use if they wish to check all unreachable code:

;; Data structures

type value_type = i32 | i64 | f32 | f64
type operand_stack = stack(value_type | unknown)
type control_stack = stack(control_frame)
type control_frame = {
. out_types : array(value_type)
. label_types : array(value_type)
. height : int
. polymorphic : bool
}

;; Stack manipulation

var operands : operand_stack
var controls : control_stack

push_operand(type : value_type | unknown) =
. operands.push(type)

pop_operand(expect : value_type | unknown) : value_type | unknown =
. error_if(operands.size = controls[0].height && not(controls[0].polymorphic))
. if (operands.size = controls[0].height) return expect ;; polymorphic
. let actual = operands.pop()
. if (actual = expect || expect = unknown) return actual
. if (actual = unknown) return expect
. error()

push_operands(types : array(value_type)) =
. foreach t in types
. . push_operand(t)

pop_operands(types : array(value_type)) =
. foreach t in reverse(types)
. . pop_operand(t)

poly_operands() =
. operands.pop(operands.size - control[0].height)
. control[0].polymorphic := true

push_control(out : array(value_type), label : array(value_type)) =
. let frame = new {out_types = out; label_types = label; height = operands.size; polymorphic = false}
. controls.push(frame)

pop_control() : array(value_type) =
. error_if(controls.is_empty())
. let frame = controls.pop()
. pop_operands(frame.out_types)
. error_if(operands.size <> frame.height)
. return frame.out_types

;; Validation of representative cases

validate(i32.add) =
. pop_operand(i32)
. pop_operand(i32)
. push_operand(i32)

validate(drop) =
. pop_operand(unknown)

validate(select) =
. pop_operand(i32)
. let t = pop_operand(unknown)
. pop_operand(t)
. push_operand(t)

validate(block t1..tN) =
. push_control([t1..tN], [t1..tN])

validate(loop t1..tN) =
. push_control([t1..tN], [])

validate(if t1..tN) =
. pop_operand(i32)
. push_control([t1..tN], [t1..tN])

validate(else) =
. let out_types = pop_control()
. push_control(out_types, out_types)

validate(end) =
. let out_types = pop_control()
. push_operands(out_types)

validate(br N) =
. error_if(controls.size() < N)
. pop_operands(controls[N].label_types)
. poly_operands()

validate(unreachable) =
. poly_operands()

[sunfishcode]

In typecheck.wast, in $type-br-operand-missing-in-loop, the end of the function is unreachable, so a type error should not be required.

[sunfishcode]

It would be useful to have a public explanation for the design decision in this PR.

[rossberg]

@sunfishcode, removed offending test, which was a left-over of the 2-label loop. Extended the PR description with a bit of motivation.

[sunfishcode]

@rossberg-chromium As the maintainer of a code generator, I can report that the new rules require my code generator to reason about reachability more than the previous rules did. There is a practical cost here, to my codebase and likely to others like it. Is there a practical advantage in having engines enforce this particular type-checking system for unreachable code which justifies this cost?

I'm not objecting the decision here. I wish to understand it.

[rossberg]

@sunfishcode, by previous rules, you mean not type-checking dead code? IIRC there were concerns about having to accept unvalidated code (you were present in the discussions, I think). Also, it leads to the conceptual complication that we need to define a specific notion of reachability in the spec (with some subtle design space). The current resolution gets rid of that, while engines are free to continue doing what they did.

Code generators are free to ignore reachability entirely. AFAICS, they only need to care, naturally, if they want to do dead code elimination. But even in that case they should be able to use whatever approximation they see fit, instead of having to match one made up by the spec. Or so I'd hope.

Can you elaborate what specifically got more complicated on your end?

[ghost]

Would be curious how the following is not invalid?

(func f1 (result i32)
  (return (i32.const 1))
)

Is this valid only because the return leaves the (i32.const 1) on the stack? Or does the return consume the value and push an unreachable marker? If it does push an unreachable marker then does it push as many as the number of values consumed or always one?

What about:

(func f2 (result i32)
  (loop ... (return (i32.const 1)) ...)
  )

Above the fall-through might not have a correctly typed value on the stack at the function block fall-through. Does the producer need to insert a dummy fall-through value.

Also another challenge, does (unreachable) push to the values stack during decoding? So is the following valid? Does the br push an unreachable type, or leave the i64.const here?

(i32.eqz (br $l0 (i64.const 1)))

[rossberg]

@JSStats, your first and third example are valid because return and br have a polymorphic result stack, i.e., in your words, "[pop everything and] push as many as the number of values consumed". The latter example is more obvious when you desugar it into (i64.const 1) (br $l0) (i32.eqz).

The second example is invalid, because the loop does not have type i32, regardless of its body.

[ghost]

@rossberg-chromium How does "push as many as the number of values consumed" work when we add pick and values might be consumed multiple times? Does it literally have to look ahead to all consumers and fill in stack values as needed.

What about (block (drop (br $l0))) does it materialize a value for the drop here, or is this invalid?

[rossberg]

@JSStats, pick is not much harder -- in terms of typing it is essentially like popping n values and then re-pushing them immediately. You only would need to track which unknown stack slots have the same type, i.e., use type variables for them. (But engines are free to not do so.)

The drop example is valid, same as your previous eqz example, except that there is no constraint on the type, so an implementation is free to pick one for compilation (if it looks at the code at all, which it does not have to).

[ghost]

@rossberg-chromium Thank you for engaging. If the drop example is valid then this seems to presume that the br pushes an element on the values stack, an element with the unreachable type, otherwise it would be invalid due to trying to pop a non-existent value from the values stack?

If so then the (block (br $l0)) would be invalid under the current block fall-through rules that appear to demand an empty stack?

The pick challenge seems to also demand that an unreachable element is pushed onto the values stack, otherwise the pops would not match. For example: (block i32 (i32.const 1) (unreachable) (pick 1) (i32.add) (i32.add))?

[rossberg]

@JSStats, br is polymorphic, so as you phrased it type-checking pretends it to "push as many values as consumed". In the simple block example that's none, so it's valid as well. The pick example would also be valid by pretending that the unreachable "pushes two i32 values".

It's the same as in the JVM, for example (though newer JVMs will require giving the assumed stack type explicitly in form of a stack map entry).

[ghost]

@rossberg-chromium So if br here pushes no values because it consumes no values then the drop will not have a value to consume so the example (block (drop (br $l0))) would then be invalid?

"type-checking pretends" does not appear to be a well defined concept? This makes it difficult to understand where this is going.

What about (block i32 $l0 (block (br $l0 (i32.const 1))) where the inner block tailing br consumes one value so would push one unreachable values stack element causing the block fall-through to not have an empty stack?

The pick example did not depend on the unreachable pushing two values, rather one value. The intent of the example was that the (i32.const 1) is duplicated by the pick. The unreachable is eventually consumed, but it is assumed to be consumed as a single stack element being popped with i32 elements before and after so it can't represent more or less than one stack element.

[rossberg]

@JSStats, if there is a drop then of course that consumes a value, so that's fine, too. The block example is invalid regardless of the branch, because the outer block has type i32 but its body has not.

The technical concept here is polymorphism, which is well-defined and well-understood. In a nutshell, after a control flow transfer instruction any suitable type can be assumed for the stack, and typing picks what makes the rest of the instructions type-check. Wasm is simple enough that such inference is straightforward.

In the pick example, the stack after the unreachable would need to have type [i32, i32]. It doesn't matter where the virtual values are coming from, i.e., you can't tell the difference whether a single value got pushed, or one popped and two pushed. So inference can simply assume that the previous stack always gets cleared.

I added a sketch of a type checking algorithm to the original comment. Hope that clarifies. Adding pick is left as an exercise to the reader. :)

[ghost]

@rossberg-chromium Thank you for the detailed explanation. However seeing this I don't think it is workable, does not meet the use case of reconciling with the AST and its data-flow typing, and thus probably not better than simply ignoring dead code apart from skipping over the operators.

For example (block i32 (br $l0) (i32.add (i32.const 1))) - the unreachable code is clearly not valid from an AST perspective because there are not enough arguments, yet this would be valid under the algorithm proposed here. This is going to cause problems for text formats and AST based tools that need to handle the dead code.

Could you please consider the limits of WebAssembly/design#778 ? Can you see any cases that slip through that proposal, or any show stoppers - it looks like the better solution but it would be good to hear from some experience.

[rossberg]

@JSStats, for better or worse, Wasm is a stack machine now, which is more liberal, so arguing that typing is too permissive for an AST is besides the point. The basic scheme of not restricting stack types after branches has precedence in both major stack machines, JVM and CLR (the latter with some quirks).

[ghost]

@rossberg-chromium Sorry, 'stack-machine' is a very general term, not a basis for technical decision making. If 'stack-machine' is going to be used like that to make decisions then all mention of this term needs to be remove from this project. This PR does not even respect the structure constraints of this stack machine which is the cause of the problems, so it's not the 'stack-machine' rather just the approach in this PR.

There is a better proposal on the table that does appear to better solve the technical use case of consistency with the AST model, it can be done and is consistent with the 'stack-machine', and this is the wasm way. JVM and CLR have different approaches, whereas wasm is to be presentable in a much more familar text format. If you want to work on CLR then that is a separate project.

I have made many appeals to consider the alternative path, and no show stoppers have been presented, it stands as the best path forward. Thus I must object to this PR's path at this point.

[titzer]

LGTM

@JSStats There has been a lot of discussion about typechecking dead code both in the context of the AST and (now) in the context of a stack machine. In general, a stack machine is more general than an AST, so it needs to have typing rules that capture that.

As @rossberg-chromium notes, this PR is a compromise between not checking dead code at all, which was considered by many to be a security risk, and requiring that all code typecheck as if it were an AST, which would require the insertion of even more dead code in the general case. IMO the rules here are pretty easy to follow and since they are easily formalized, easier to reason about. I have an older patch that implements them for V8 and will probably land that to match the spec exactly, even though V8 actually has a more sophisticated dead code analysis built in due to its tracking of SSA environments.

Other proposed approaches like many dead code syntactically impossible don't serve simple producers well (without solving the actual problem anyway).

[ghost]

@titzer Lets see your example of wasm 'stack-machine' code that can not be presented in an AST? I have been following the discussions and your claim that 'a stack machine is more general than an AST' is surprising to me, but it's always good to learn more.

If you have an example where 'making dead code syntactically impossible don't serve simple producers well' then could you please post it to WebAssembly/design#778 In the absence of such example, it seems only fair that that stands as the best solution. I would also like to hear the binaryen experience.

[titzer]

E.g. you can have {x} {... void-returning-code ...} {y} ADD, which technically you can represent as the AST ADD(x, ..., y), but it isn't the natural representation, and typechecking this AST is more involved, since the algorithm basically has to ignore child nodes that do not produce values.

[ghost]

@titzer Yes, such examples were discussed and it seemed settled that they have natural familiar text presentations as:

const $c1 = {x};
void-returning-code;
$c1 + {y};

So we can keep this structure stack-machine and the familiar text format, and that seem very worthy of considering in relation to this dead-code matter. Wouldn't it be great if wasm could address this in the dead code too.

Some of the rules in the PR might be expressed as in the following example, but perhaps not all, but it requires more complexity in the text format code, looking ahead to consumers of the values.

(block i32 (unreachable) (i32.add) (i32.add) (i32.add))
=>
{
  const ($c1, $c2, $c3, $c4) = unreachable();
  $c1 + $c2 + $c3 + $c4;
}

[ghost]

Here's a counter proposal, adopting some of the rules in this PR but also moving us closer to WebAssembly/design#778 and also fully validating the types in unreachable code with one exception.

• When the last operation in a block is an operator that has an unreachable result the block fall-through type checking is ignored. This allows a producer to flush all the trailing unreachable operators in a block without the burden of inserting type valid fill.

For example (block i32 $l0 (br $l0 (i32.const))) is valid even though the block fall-through is not fully valid.

• When an block contains an operator with an unreachable result, that operator has a void result type for type checking, and the remainder of the block must be type valid.

For example:
(block i32 $l0 (br $l0 (i32.const 1)) (i32.const 2)) is valid
(block i32 $l0 (i32.const 2) (br $l0 (i32.const 1))) is valid
(block i32 $l0 (br $l0 (i32.const)) (i64.const 2)) is invalid
(block i32 $l0 (br $l0 (i32.const)) (nop)) is invalid.

Where the producer wants to fill a typed operator, such as i32.const with an operator with an unreachable result, and still retain the trailing operators until the end of the block it would have two easy options:

1. wrap it in a block with a declared type e.g. (i32.add (i32.const 1) (i32.const 2)) => (i32.add (block i32 (unreachable)) (i32.const 2)).
2. insert a dummy value which is very practical for the current constants. e.g. (i32.add (i32.const 1) (i32.const 2)) => (i32.add (unreachable) (i32.const 0) (i32.const 2)). The AST would need to handle this special case in some clever way, a virtual block etc. A text printer would handler this in a similar manner to a nop, reusing the same logic.

This proposal would eliminate the unreachable type from wasm. Replaced by either pattern matching the operators that returned unreachable and the immediately following block end (which seems to be a property of WebAssembly/design#778) or they return the void type same as a nop.

This proposal avoids introducing the unknown type.

Open to other suggestions, problems, etc.

[rossberg]

@JSStats, we want to have a single logical representation that byte code encodes/decodes into, the text format prints/parses into, validation is defined on, and evaluation is defined on. That is not possible with the syntax you sketch: converting between this and the rest represents an actual translation that in one direction even is type-dependent. Conceptually, making that work would require defining two languages and a compile/decompile logic between them. There is no point in doing that rather than just consistently defining a stack machine.

And as Ben mentions, proposals like WebAssembly/design#778 would penalise any compiler that does not use a control-flow graph because they require all producers to track reachability. No external code format (as opposed to compiler ILs) that I'm aware of does that, and for good reason.

It's of course fine for anybody to invent other languages that Wasm compiles/decompiles outof/into, but that's outside the scope of the Wasm specification.

[lukewagner]

lgtm per previous discussion

[rossberg]

Landing based on above LGTMs and earlier discussions.