From 97a397b8efece753ff0714b9d56fcb6bb1b44ea1 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 28 Jan 2026 15:53:15 +0100 Subject: [PATCH] [spec] Fix definition of is_packtype --- .../2.3-validation.instructions.spectec | 4 ++-- spectec/doc/example/output/NanoWasm.pdf | Bin 245627 -> 245627 bytes spectec/src/backend-prose/render.ml | 6 +++++- spectec/test-frontend/TEST.md | 6 +++--- spectec/test-latex/TEST.md | 4 ++-- spectec/test-middlend/TEST.md | 18 +++++++++--------- spectec/test-prose/TEST.md | 10 +++++----- 7 files changed, 26 insertions(+), 22 deletions(-) diff --git a/specification/wasm-3.0/2.3-validation.instructions.spectec b/specification/wasm-3.0/2.3-validation.instructions.spectec index a89f98c092..e57e5d90f5 100644 --- a/specification/wasm-3.0/2.3-validation.instructions.spectec +++ b/specification/wasm-3.0/2.3-validation.instructions.spectec @@ -253,13 +253,13 @@ rule Instr_ok/struct.new_default: -- (Defaultable: |- $unpack(zt) DEFAULTABLE)* def $is_packtype(storagetype) : bool hint(show %1 = $unpack(%1)) hint(prose "%1 is a packed type") -def $is_packtype(zt) = zt = $unpack(zt) +def $is_packtype(zt) = zt =/= $unpack(zt) 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) + -- if sx? =/= eps <=> $is_packtype(zt) rule Instr_ok/struct.set: C |- STRUCT.SET x i : (REF NULL (_IDX x)) $unpack(zt) -> eps diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index 270dac88bda2add7033b7a4c96b48ff378bc2cb6..302e3da9e9b21410b633a4db2aeb3d360fa53011 100644 GIT binary patch delta 344 zcmezUkMH+Cz70u2^}gAM4S3id?5=O^Gt*h8Qh#Ef*fvML=D@>zvHWUhuN|6{m$PC2 z{w10s*CxktzGPI~!+dD*q57}h7efR&S{#+4&NJ?E%q{2moq3Px)*R(O^R}~nXw>nZ z^NBs@%IDtgdRbo|$ZXg?sb#?)#?3bzn4EGrm8aO|e4U)B@xp3eT#s`^?0)vk8&vlG ze6#zpw$=Ts^B-rL?7lS5Qs}hEpEDDmYgT7?G?l)5G}XCYv`g?x?RK7N%lN{(bNCw5 zwJp1EIzCRD|JiA4X^fub-B_lgIp_2D?bUz9pYhShyV+8>-BOqlh?%xq3N!mIVz)3f zH8nIbo!+~ZSq8@0zF{kKA)B+Kfr*=mp^2HHg_D`3tFw`%p@D^~lcR;Jo3purvze2f Pf(;=h+f(*1i!%cNLFJ30 delta 344 zcmezUkMH+Cz70u2^|slE9eCIt{H<$slfTlnP;I{0+x>?&DW(2j||9p+X&YRK2e++0I>Twg z%`BOqqJZ5ur*8?!m7MNufw-jdfUBqr~ zXl`I(WHG&WE3*uYvwg!>=0Y}SLsM4+CpR-gM^_g|GjnGHV^?ES7h@+2LsxSnGiL)A QI|Um;O17u$VHRfw0I>^{oB#j- diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml index aa34ec1b2a..7632cf1519 100644 --- a/spectec/src/backend-prose/render.ml +++ b/spectec/src/backend-prose/render.ml @@ -941,7 +941,11 @@ let rec render_single_stmt ?(with_type=true) env stmt = | CmpS (e1, cmpop, e2) -> let cmpop, rhs = match e2.it with - | OptE None -> render_prose_cmpop_eps cmpop, "absent" + | OptE None -> + if cmpop = `NeOp then + render_prose_cmpop_eps `EqOp, "present" + else + render_prose_cmpop_eps cmpop, "absent" | ListE [] -> render_prose_cmpop_eps cmpop, "empty" | BoolE _ -> render_prose_cmpop_eps cmpop, render_expr env e2 | _ -> render_prose_cmpop cmpop, render_expr env e2 diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 310c7aaa93..e1fee92447 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -3340,7 +3340,7 @@ relation Memarg_ok: `|-%:%->%`(memarg, addrtype, N) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec def $is_packtype(storagetype : storagetype) : bool ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec - def $is_packtype{zt : storagetype}(zt) = (zt = ($unpack(zt) : valtype <: storagetype)) + def $is_packtype{zt : storagetype}(zt) = (zt =/= ($unpack(zt) : valtype <: storagetype)) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec rec { @@ -3564,12 +3564,12 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} - ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.39 + ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.41 rule struct.get{C : context, `sx?` : sx?, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*, `mut?` : mut?}: `%|-%:%`(C, STRUCT.GET_instr(sx?{sx <- `sx?`}, x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x))]), [], `%`_resulttype([$unpack(zt)]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`}))) -- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(mut?{mut <- `mut?`}, zt)) - -- if ((sx?{sx <- `sx?`} = ?()) <=> $is_packtype(zt)) + -- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt)) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:264.1-267.24 rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}: diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 6b6193a24b..5e4e6345c5 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -6360,7 +6360,7 @@ $$ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}}) & = & {\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}}) \\ +{\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}}) & = & {\mathit{zt}} \neq {\mathrm{unpack}}({\mathit{zt}}) \\ \end{array} $$ @@ -6371,7 +6371,7 @@ C{.}\mathsf{types}{}[x] \approx \mathsf{struct}~{{\mathit{ft}}^\ast} \qquad {{\mathit{ft}}^\ast}{}[i] = {\mathsf{mut}^?}~{\mathit{zt}} \qquad -{{\mathit{sx}}^?} = \epsilon \Leftrightarrow {\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}}) +{{\mathit{sx}}^?} \neq \epsilon \Leftrightarrow {\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}}) }{ C \vdash {\mathsf{struct{.}get}}{\mathsf{\_}}{{{\mathit{sx}}^?}}~x~i : (\mathsf{ref}~\mathsf{null}~x) \rightarrow {\mathrm{unpack}}({\mathit{zt}}) } \, {[\textsc{\scriptsize T{-}instr{-}struct.get}]} diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 018c3d0c8a..98e1801b30 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -3330,7 +3330,7 @@ relation Memarg_ok: `|-%:%->%`(memarg, addrtype, N) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec def $is_packtype(storagetype : storagetype) : bool ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec - def $is_packtype{zt : storagetype}(zt) = (zt = ($unpack(zt) : valtype <: storagetype)) + def $is_packtype{zt : storagetype}(zt) = (zt =/= ($unpack(zt) : valtype <: storagetype)) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec rec { @@ -3554,12 +3554,12 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} - ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.39 + ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.41 rule struct.get{C : context, `sx?` : sx?, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*, `mut?` : mut?}: `%|-%:%`(C, STRUCT.GET_instr(sx?{sx <- `sx?`}, x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x))]), [], `%`_resulttype([$unpack(zt)]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`}))) -- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(mut?{mut <- `mut?`}, zt)) - -- if ((sx?{sx <- `sx?`} = ?()) <=> $is_packtype(zt)) + -- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt)) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:264.1-267.24 rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}: @@ -14684,7 +14684,7 @@ relation Memarg_ok: `|-%:%->%`(memarg, addrtype, N) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec def $is_packtype(storagetype : storagetype) : bool ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec - def $is_packtype{zt : storagetype}(zt) = (zt = ($unpack(zt) : valtype <: storagetype)) + def $is_packtype{zt : storagetype}(zt) = (zt =/= ($unpack(zt) : valtype <: storagetype)) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec rec { @@ -14908,12 +14908,12 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} - ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.39 + ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.41 rule struct.get{C : context, `sx?` : sx?, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*, `mut?` : mut?}: `%|-%:%`(C, STRUCT.GET_instr(sx?{sx <- `sx?`}, x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x))]), [], `%`_resulttype([$unpack(zt)]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`}))) -- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(mut?{mut <- `mut?`}, zt)) - -- if ((sx?{sx <- `sx?`} = ?()) <=> $is_packtype(zt)) + -- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt)) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:264.1-267.24 rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}: @@ -26066,7 +26066,7 @@ relation Memarg_ok: `|-%:%->%`(memarg, addrtype, N) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec def $is_packtype(storagetype : storagetype) : bool ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec - def $is_packtype{zt : storagetype}(zt) = (zt = ($unpack(zt) : valtype <: storagetype)) + def $is_packtype{zt : storagetype}(zt) = (zt =/= ($unpack(zt) : valtype <: storagetype)) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec rec { @@ -26311,14 +26311,14 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} - ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.39 + ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.41 rule struct.get{C : context, `sx?` : sx?, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*, `mut?` : mut?}: `%|-%:%`(C, STRUCT.GET_instr(sx?{sx <- `sx?`}, x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x))]), [], `%`_resulttype([$unpack(zt)]))) -- if (x!`%`_idx.0 < |C.TYPES_context|) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`}))) -- if (i!`%`_u32.0 < |ft*{ft <- `ft*`}|) -- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(mut?{mut <- `mut?`}, zt)) - -- if ((sx?{sx <- `sx?`} = ?()) <=> $is_packtype(zt)) + -- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt)) ;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:264.1-267.24 rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}: diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index e6750e02b2..da9e30d05b 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -15216,7 +15216,7 @@ The catch clause :math:`(\mathsf{catch\_all\_ref}~l)` is :ref:`valid The value type :math:`t` is defaultable if: - * The value :math:`{{\mathrm{default}}}_{t}` is not absent. + * The value :math:`{{\mathrm{default}}}_{t}` is present. @@ -15658,7 +15658,7 @@ The instruction :math:`({\mathsf{struct{.}get}}{\mathsf{\_}}{{{\mathit{sx}}^?}}~ * The field type :math:`{{\mathit{ft}}^\ast}{}[i]` is of the form :math:`({\mathsf{mut}^?}~{\mathit{zt}})`. - * The signedness :math:`{{\mathit{sx}}^?}` is absent if and only if :math:`{\mathit{zt}}` is a packed type. + * The signedness :math:`{{\mathit{sx}}^?}` is present if and only if :math:`{\mathit{zt}}` is a packed type. * The value type :math:`t` is :math:`{\mathrm{unpack}}({\mathit{zt}})`. @@ -23690,7 +23690,7 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i ...................................... -1. Return :math:`{\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}})`. +1. Return :math:`{\mathit{zt}} \neq {\mathrm{unpack}}({\mathit{zt}})`. :math:`{\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast})` @@ -27741,7 +27741,7 @@ Instr_ok/struct.get - The :ref:`expansion ` of C.TYPES[x] is (STRUCT ft*). - |ft*| is greater than i. - the field type ft*[i] is (mut? zt). - - the signedness sx? is ?() if and only if $is_packtype(zt). + - the signedness sx? is not ?() if and only if $is_packtype(zt). - the value type t is $unpack(zt). Instr_ok/struct.set @@ -31617,7 +31617,7 @@ default_ valtype 8. Return ?(). is_packtype zt -1. Return (zt = $unpack(zt)). +1. Return (zt =/= $unpack(zt)). funcidx_nonfuncs (global* mem* table* elem*) 1. Return $funcidx_module((MODULE [] [] [] global* mem* table* [] [] elem* ?() [])).