-
Notifications
You must be signed in to change notification settings - Fork 509
Description
On https://github.com/WebAssembly/spec/blob/main/specification/wasm-3.0/2.3-validation.instructions.spectec#L262, we have the validation rule for struct.get, possibly with a sign extension:
rule Instr_ok/struct.get:
C |- STRUCT.GET sx? x i : (REF NULL (_IDX x)) -> $unpack(zt)
-- Expand: C.TYPES[x] ~~ STRUCT ft*
-- if ft*[i] = mut? zt
-- if sx? = eps <=> $is_packtype(zt)
And $is_packtype is defined as (https://github.com/WebAssembly/spec/blob/main/specification/wasm-3.0/2.3-validation.instructions.spectec#L255):
def $is_packtype(storagetype) : bool hint(show %1 = $unpack(%1)) hint(prose "%1 is a packed type")
def $is_packtype(zt) = zt = $unpack(zt)
Which, I think is exactly the opposite according to the definition of packtype in https://github.com/WebAssembly/spec/blob/main/specification/wasm-3.0/1.2-syntax.types.spectec#L88-L92. i8 and i16 are the only packed types: the only types for which zt != $unpack(zt).
In the semantics there is no bug AFAIU. However when translated to text, https://webassembly.github.io/spec/core/valid/instructions.html#aggregate-reference-instructions says that The signedness sx? is absent if and only if zt is a packed type where it should actually be something like "sx is present if and only if zt is a packed type".