diff --git a/spectec/spec/wasm-2.0/5-runtime-aux.watsup b/spectec/spec/wasm-2.0/5-runtime-aux.watsup index 2413c9103c..94cc59cca4 100644 --- a/spectec/spec/wasm-2.0/5-runtime-aux.watsup +++ b/spectec/spec/wasm-2.0/5-runtime-aux.watsup @@ -4,13 +4,15 @@ ;; Default values +def $vzero: c_vectype ;; HACK for algorithmic backend + def $default(valtype) : val hint(show $default_%) def $default(I32) = (CONST I32 0) def $default(I64) = (CONST I64 0) def $default(F32) = (CONST F32 0) def $default(F64) = (CONST F64 0) -def $default(V128) = (VVCONST V128 0) +def $default(V128) = (VVCONST V128 $vzero) def $default(FUNCREF) = (REF.NULL FUNCREF) def $default(EXTERNREF) = (REF.NULL EXTERNREF) diff --git a/spectec/spec/wasm-2.0/8-reduction.watsup b/spectec/spec/wasm-2.0/8-reduction.watsup index 7bb46b3ba0..d8f5bfcaa0 100644 --- a/spectec/spec/wasm-2.0/8-reduction.watsup +++ b/spectec/spec/wasm-2.0/8-reduction.watsup @@ -219,7 +219,6 @@ rule Step_pure/vvternop: -- if $vvternop(vvternop, V128, cv_1, cv_2, cv_3) = cv ;; TODO -def $vzero: c_vectype ;; HACK for algorithmic backend rule Step_pure/vvtestop: (VVCONST V128 cv_1) (VVTESTOP V128 (_VV ANY_TRUE)) ~> (CONST I32 i) -- if i = $ine(128, cv_1, $vzero) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 3d02b9c7ab..6d594a4d8f 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -1400,7 +1400,7 @@ default valty_u0 4. If (valty_u0 is F64), then: a. Return (F64.CONST 0). 5. If (valty_u0 is V128), then: - a. Return (VVCONST V128 0). + a. Return (VVCONST V128 $vzero()). 6. If (valty_u0 is FUNCREF), then: a. Return (REF.NULL FUNCREF). 7. Assert: Due to validation, (valty_u0 is EXTERNREF).