Update default vector

Wasm-DSL · Feb 2, 2024 · fba9908 · fba9908
1 parent d82ff53
commit fba9908
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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).