Suspicious data section count invalid module tests

[Janrupf]

The test here:

testsuite/memory_init.wast

Lines 189 to 193 in aa6e47b

	(assert_invalid
	(module
	(func (export "test")
	(data.drop 0)))
	"unknown data segment")

Specifies that this is an invalid module. Indeed, attempting to compile the module with wat2wasm leads to:

❯ wat2wasm src/test/resources/assembler/simple.wat -o /tmp/simple.wasm           
src/test/resources/assembler/simple.wat:3:16: error: data_segment variable out of range: 0 (max 0)
    (data.drop 0)))

Notably, the error message is different. Further, wast2json compiles with effectively --no-check, which however doesn't actually yield an invalid module, but a malformed one:

❯ wat2wasm src/test/resources/assembler/simple.wat -o /tmp/simple.wasm --no-check

❯ wasm2wat /tmp/simple.wasm -o /tmp/simple.wat                                   
0000023: error: data.drop requires data count section

This seems to more or less be the following check:

testsuite/binary.wast

Lines 515 to 533 in aa6e47b

	;; data.drop requires a data count section
	(assert_malformed
	(module binary
	"\00asm" "\01\00\00\00"
	"\01\04\01\60\00\00" ;; Type section
	"\03\02\01\00" ;; Function section
	"\05\03\01\00\00" ;; Memory section
	"\0a\07\01" ;; Code section
	;; function 0
	"\05\00"
	"\fc\09\00" ;; data.drop
	"\0b"
	"\0b\03\01\01\00" ;; Data section
	) ;; end
	"data count section required"
	)

So the question now is whether this is a malformed module (though then it shouldn't even be possibly to create it with --no-check as far as I understand) or an invalid module, but then the binary tests would be wrong.

(NOTE: the same applies to the memory.init tests)

To be clear why I'm raising this issue: While testing my WASM implementation against the spec tests I noticed that I fail the assert_invalid tests from above because my implementation asserts them as malformed, and moving this check to the validation phase makes it fail the assert_malformed tests.

[tlively]

The text format has no way of providing an explicit data count, so the first test is correct in saying that the module is invalid.

The binary format specification says, "Similarly, the optional data count must match the length of the data segment vector. Furthermore, it must be present if any data index occurs in the code section." So the second test is also correct.

I guess the bug here is that wast2json does not produce a data count section containing 0 in this case, which would make the binary module well-formed but still invalid.

[Janrupf]

I assume this would then better be reported over here at the wabt repository as a bug in the wat2wasm tool?

[tlively]

Yes, that would make sense. I don't know if it's worth fixing, though. The distinction between an invalid and malformed WebAssembly module doesn't matter much in practice. The module is incorrect and unusable either way. In Binaryen, for example, we let modules we consider to be malformed pass both assert_malformed and assert_invalid checks.

[Janrupf]

I see. I'll close this issue either way and report it at wabt. In my personal opinion the distinction should matter, and it seems to actually only be "wrong" for a very small amount of test cases (I only found these 2 so far, though I'm currently skipping the whole SIMD and post 1.0 tests)