Add support for non-nullable tables and init expressions

[pufferfish101007]

Resolves #5628

Adds support for non-nullable tables with init expressions. I'm not totally sure how I should go about adding new tests, but manual test cases are below. I have also unignored previously ignored spec tests instance.wast, ref_is_null.wast, table.wast, i31.wast, global.wast which now all pass. I have also changed the reason for ignoring array.wast as it does not (and has not in the past, AFAICT) rely on non-nullable table types.

This introduces a breaking change in the C api, as it adds an extra argument to addTable. Is this ok? Should a new method be added instead? (e.g. addTableWithInit?)

Manual tests

click to expand

The validation ones might overlap with the spec tests. Unchecked boxes indicate tests that currently fail.

• Nullable tables should continue to round-trip correctly:

(module
 (type $0 (func (param i32)))
 (table $0 0 funcref)
 (elem $0 (i32.const 0))
 (func $0 (param $0 i32)
 )
)

• Non-nullable tables with init expr should round-trip correctly:

(module
 (type $0 (func (param i32)))
 (table $0 0 (ref $0) (ref.func $0))
 (func $0 (param $0 i32)
 )
)

• Non-nullable table without an init expr should fail validation:

(module
 (type $0 (func (param i32)))
 (table $0 0 (ref $0))
 (func $0 (param $0 i32)
 )
)

Correctly fails with [wasm-validator error in module] unexpected false: tables with non-nullable types require an initializer expression, on table

• Nullable table with init expr should rountrip correctly:

(module
 (type $0 (func (param i32)))
 (table $0 0 funcref (ref.func $0))
 (func $0 (type $0) (param $0 i32)
 )
)

• Non-nullable table init expr should be validated to be a subtype of the table type

(module
 (type $0 (func (param i32)))
 (table $0 0 (ref $0) (i32.const 0))
 (func $0 (param $0 i32)
 )
)

Correctly fails with [wasm-validator error in module] init expression must be a subtype of the table type, on (i32.const 0)

• Nullable table init expr (if present) should be validated to be a subtype of the table type

(module
 (type $0 (func (param i32)))
 (table $0 0 funcref (i32.const 0))
 (func $0 (param $0 i32)
 )
)

Correctly fails with [wasm-validator error in module] init expression must be a subtype of the table type, on (i32.const 0)

• wasm-opt doesn't remove init expr as dead code

(module
 (type $0 (func (param i32)))
 (table $0 0 funcref (ref.func $0))
 (export "table" (table $0))
 (func $0 (type $0) (param $0 i32)
 )
)

TODO:

• Add test that imported globals can be referenced in the init expr
• add remove unused module elements pass test
• add unsubtyping pass test
• validate that imported tables do not have init exprs, add test for this
• add fuzzing support

---

dummy PR for CI tests to run automatically: pufferfish101007#2

[stevenfontanella]

I have also unignored previously ignored spec tests instance.wast, ref_is_null.wast, table.wast, i31.wast, which now all pass. I have also changed the reason for ignoring array.wast as it does not (and has not in the past, AFAICT) rely on non-nullable table types.

I don't see these changes in shared.py, can we add them?

[stevenfontanella]

Looks good from my side. I'll let @tlively have the final review. Thanks for the contribution!

[pufferfish101007]

@stevenfontanella thank you for such a thorough review!

[pufferfish101007]

Thanks for the additional comments! I've addressed the easy fixes and probably won't have time to address the others for a week or so (but I'll try to do so as soon as possible to keep momentum going).

I will aim to add fuzzer support now, so that this doesn't come back to bite me later on.

A question:
For lit tests, I notice that each lit test says at the top ;; NOTE: Assertions have been generated by update_lit_checks.py --all-items and should not be edited., and I'm not entirely clear what this actually means - are there some parts of lit tests that are generated, and some that are written manually? What do I need to write manually? Sorry if this is documented somewhere that I haven't found!

[tlively]

The way the lit tests work is that you write the module (or modules) and the RUN lines at the top saying how the test should execute. The filecheck command in those run lines compares its input against the expected output in the CHECK comments in the file. (There may be other check prefixes as well.) After you write the RUN lines and the input, the script can generate the expected output in the CHECK lines. You can put multiple input modules in the same wast file if the RUN line uses the foreach tool.

I recommend copying the RUN lines and general structure from other recent tests in the same directory. You can run specific new tests with bin/binaryen-lit -vv path/to/test.wast.

[pufferfish101007]

Fuzzer support has been added (with room for improvements still, but it's already thrown up a bug). That's caused a test to fail though, with test/passes/translate-to-fuzz_all-features_metrics_noprint.txt failing to match - is this expected, and should it be updated to match what the test now produces?

[tlively]

is this expected, and should it be updated to match what the test now produces?

Yes and yes 👍

[pufferfish101007]

I've run the fuzzer 10159 times with no problems, so hopefully everything that needs to be updated has been.

[stevenfontanella]

LGTM, will let Thomas have the last look!

[stevenfontanella]

Looks like it is used and the [[maybe_unused]] attribute isn't needed