Wasm-DSL / spectec

Wasm SpecTec specification tools
https://wasm-dsl.github.io/spectec/
Other
26 stars 9 forks source link

Replace more execution; fix array.new/init_data rules #88

Closed rossberg closed 6 months ago

rossberg commented 6 months ago

@jaehyun1ee, @f52985, as discussed today, this fixes a bug in the reduction of array.new_data/init_data. The new version requires the inverse of the packconst helper, which I'm not sure how to implement, hence the failure below.

 ===== ../../test-interpreter/spec-test-3/gc/array_init_data.wast =====
-- 31/31 (100.00%)
+- Test failed at ../../test-interpreter/spec-test-3/gc/array_init_data.wast:95.1-95.85 (Failure("Invalid assignment on value 0x63: CallE (packconst, [ VarE (zt), VarE (c) ]) @8-reduction.watsup:522.21-522.38"))
+Result: 0 : [i32]
+Expect: 99 : [i32]
+- Test failed at ../../test-interpreter/spec-test-3/gc/array_init_data.wast:97.1-97.70 (Error(_, "wrong return values"))
+Result: 0 : [i32]
+Expect: 100 : [i32]
+- Test failed at ../../test-interpreter/spec-test-3/gc/array_init_data.wast:98.1-98.71 (Error(_, "wrong return values"))
+- Test failed at ../../test-interpreter/spec-test-3/gc/array_init_data.wast:101.1-101.89 (Failure("Invalid assignment on value 0x6766: CallE (packconst, [ VarE (zt), VarE (c) ]) @8-reduction.watsup:522.21-522.38"))
+Result: 0 : [i32]
+Expect: 26_470 : [i32]
+- Test failed at ../../test-interpreter/spec-test-3/gc/array_init_data.wast:103.1-103.78 (Error(_, "wrong return values"))
+Result: 0 : [i32]
+Expect: 26_984 : [i32]
+- Test failed at ../../test-interpreter/spec-test-3/gc/array_init_data.wast:104.1-104.78 (Error(_, "wrong return values"))
+- 25/31 (80.65%)
rossberg commented 6 months ago

Sleeping over this I realised that my fix wasn't quite what we wanted, because packconst is, in fact, not invertible: because it wraps its argument, it is a lossy operation. So I changed it the other way round, using unpackconst on the RHS, which also fixed the test failures.

(For the semantics of these ops it wouldn't matter which inverse value to pick, because they all result in the same value being written in the next step. So underspecifying it as before wasn't incorrect per se, but it still resulted in a local non-determinism that we'd like to avoid.)

In short, problem solved, you can ignore the above. I hope you haven't yet wasted time on it...

f52985 commented 6 months ago

That's great! I was just about to have a look at it, so no time wasted at all.