Skip to content

Commit

Permalink
Merge branch 'num'
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg committed Oct 30, 2024
2 parents 9c7108e + ab66ac9 commit a8000fe
Show file tree
Hide file tree
Showing 61 changed files with 1,590 additions and 1,516 deletions.
3 changes: 2 additions & 1 deletion document/core/syntax/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -317,6 +317,7 @@ The ${:ELEM.DROP} instruction prevents further use of a passive element segment.
.. _syntax-storen:
.. _syntax-memarg:
.. _syntax-loadop:
.. _syntax-storeop:
.. _syntax-vloadop:
.. _syntax-lanewidth:
.. _syntax-instr-memory:
Expand All @@ -326,7 +327,7 @@ Memory Instructions

Instructions in this group are concerned with linear :ref:`memory <syntax-mem>`.

$${syntax: memarg loadop_ vloadop_ {instr/memory instr/data}}
$${syntax: memarg loadop_ storeop_ vloadop_ {instr/memory instr/data}}

Memory is accessed with ${:LOAD} and ${:STORE} instructions for the different :ref:`number types <syntax-numtype>` and `vector types <syntax-vectype>`.
They all take a :ref:`memory index <syntax-memidx>` and a *memory argument* ${:memarg} that contains an address *offset* and the expected *alignment* (expressed as the exponent of a power of 2).
Expand Down
5 changes: 1 addition & 4 deletions document/core/util/macros.def
Original file line number Diff line number Diff line change
Expand Up @@ -785,11 +785,8 @@
.. |vftestop| mathdef:: \xref{syntax/instructions}{syntax-vtestop}{\X{vftestop}}
.. |vfrelop| mathdef:: \xref{syntax/instructions}{syntax-vrelop}{\X{vfrelop}}

.. TODO: obsolete, remove
.. |viminmaxop| mathdef:: \xref{syntax/instructions}{syntax-vbinop}{\X{viminmaxop}}
.. |visatbinop| mathdef:: \xref{syntax/instructions}{syntax-vbinop}{\X{visatbinop}}

.. |loadop| mathdef:: \xref{syntax/instructions}{syntax-loadop}{\X{loadop}}
.. |storeop| mathdef:: \xref{syntax/instructions}{syntax-storeop}{\X{storeop}}
.. |vloadop| mathdef:: \xref{syntax/instructions}{syntax-vloadop}{\X{vloadop}}

.. |sx| mathdef:: \xref{syntax/instructions}{syntax-sx}{\X{sx}}
Expand Down
11 changes: 8 additions & 3 deletions spectec/doc/Language.md
Original file line number Diff line number Diff line change
Expand Up @@ -68,14 +68,17 @@ atomop ::=
### Types

```
typ ::=
varid args type name
"bool" booleans
numtyp ::=
"nat" natural numbers
"int" integer numbers
"rat" rational numbers
"real" real numbers
typ ::=
varid args type name
"bool" booleans
"text" text strings
numtyp numbers
typ iter iteration
"(" list(typ, ",") ")" parentheses or tupling
Expand Down Expand Up @@ -150,6 +153,7 @@ exp ::=
"`" "[" list(exp, ",") "]"
"`" "{" list(exp, ",") "}"
"$" "(" arith ")" escape to arithmetic syntax
"$" numtyp "$" "(" arith ")" numeric conversion
hole hole (for syntax rewrites in hints)
exp "#" exp token concatenation (for syntax rewrites in hints)
"##" exp remove possible parentheses (for syntax rewrites in hints)
Expand All @@ -169,6 +173,7 @@ arith ::=
"|" exp "|" list length
"$" defid exp? function invocation
"$" "(" exp ")" escape back to general expression syntax
"$" numtyp "$" "(" arith ")" numeric conversion
path ::=
path? "[" arith "]" list element
Expand Down
15 changes: 9 additions & 6 deletions spectec/spec/wasm-1.0/1-syntax.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -148,6 +148,7 @@ syntax val_(Fnn) = fN($size(Fnn))
;; Operators

syntax sx hint(desc "signedness") = U | S
syntax sz hint(desc "pack size") = `8 | `16 | `32 | `64

syntax unop_(valtype)
syntax unop_(Inn) = CLZ | CTZ | POPCNT
Expand Down Expand Up @@ -176,10 +177,15 @@ syntax cvtop =
| EXTEND sx | WRAP | CONVERT sx | TRUNC sx | PROMOTE | DEMOTE | REINTERPRET


;; Memory operators

syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32}

var ao : memarg

syntax loadop_(valtype)
syntax loadop_(Inn) = sz sx hint(show %0#_#%1) -- if sz < $size(Inn)


;; Instructions

Expand Down Expand Up @@ -233,13 +239,10 @@ syntax instr/global hint(desc "global instruction") = ...
| GLOBAL.SET globalidx
| ...

syntax sz hint(desc "pack size") = `8 | `16 | `32 | `64

syntax instr/memory hint(desc "memory instruction") = ...
| LOAD valtype (sz _ sx)? memarg hint(show %.LOAD % %) hint(show %.LOAD#% % %)
-- (if valtype = Inn /\ sz < $size(Inn))? ;; TODO: take size implicitly
| STORE valtype sz? memarg hint(show %.STORE % %) hint(show %.STORE#% % %)
-- (if valtype = Inn /\ sz < $size(Inn))? ;; TODO: take size implicitly
| LOAD valtype loadop_(valtype)? memarg hint(show %.LOAD % %) hint(show %.LOAD# ##% %)
| STORE valtype sz? memarg hint(show %.STORE % %) hint(show %.STORE#% %)
-- (if valtype = Inn /\ sz < $size(Inn))?
| MEMORY.SIZE
| MEMORY.GROW

Expand Down
40 changes: 32 additions & 8 deletions spectec/spec/wasm-1.0/6-typing.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -268,19 +268,43 @@ rule Instr_ok/memory.grow:
C |- MEMORY.GROW : I32 -> I32
-- if C.MEMS[0] = mt

(;
rule Instr_ok/load:
C |- LOAD nt (n _ sx)? memarg : I32 -> nt
C |- LOAD t (n sx)? memarg : I32 -> t
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(nt)/8)
-- if $(2^(memarg.ALIGN) <= n/8 < $size(nt)/8)?
-- if n? = eps \/ nt = Inn
-- if $(2^(memarg.ALIGN) <= $size(t)/8)
-- if $(2^(memarg.ALIGN) <= n/8 < $size(t)/8)?
-- if n? = eps \/ t = Inn
;)

rule Instr_ok/load-val:
C |- LOAD t memarg : I32 -> t
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(t)/8)

rule Instr_ok/load-pack:
C |- LOAD Inn (M sx) memarg : I32 -> Inn
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= M/8)

(;
rule Instr_ok/store:
C |- STORE nt n? memarg : I32 nt -> eps
C |- STORE t n? memarg : I32 t -> eps
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(t)/8)
-- if $(2^(memarg.ALIGN) <= n/8 < $size(t)/8)?
-- if n? = eps \/ t = Inn
;)

rule Instr_ok/store-val:
C |- STORE t memarg : I32 t -> eps
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(t)/8)

rule Instr_ok/store-pack:
C |- STORE Inn M memarg : I32 Inn -> eps
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(nt)/8)
-- if $(2^(memarg.ALIGN) <= n/8 < $size(nt)/8)?
-- if n? = eps \/ nt = Inn
-- if $(2^(memarg.ALIGN) <= M/8)


;;
Expand Down
4 changes: 2 additions & 2 deletions spectec/spec/wasm-1.0/8-reduction.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -233,11 +233,11 @@ rule Step_read/load-num-val:
-- if $bytes_(t, c) = $mem(z, 0).BYTES[i + ao.OFFSET : $size(t)/8]

rule Step_read/load-pack-trap:
z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> TRAP
z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> TRAP
-- if $(i + ao.OFFSET + n/8 > |$mem(z, 0).BYTES|)

rule Step_read/load-pack-val:
z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c))
z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c))
-- if $ibytes_(n, c) = $mem(z, 0).BYTES[i + ao.OFFSET : n/8]


Expand Down
20 changes: 10 additions & 10 deletions spectec/spec/wasm-1.0/A-binary.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -181,16 +181,16 @@ grammar Binstr/memory : instr = ...
| 0x29 ao:Bmemarg => LOAD I64 ao
| 0x2A ao:Bmemarg => LOAD F32 ao
| 0x2B ao:Bmemarg => LOAD F64 ao
| 0x2C ao:Bmemarg => LOAD I32 (8 _ S) ao
| 0x2D ao:Bmemarg => LOAD I32 (8 _ U) ao
| 0x2E ao:Bmemarg => LOAD I32 (16 _ S) ao
| 0x2F ao:Bmemarg => LOAD I32 (16 _ U) ao
| 0x30 ao:Bmemarg => LOAD I64 (8 _ S) ao
| 0x31 ao:Bmemarg => LOAD I64 (8 _ U) ao
| 0x32 ao:Bmemarg => LOAD I64 (16 _ S) ao
| 0x33 ao:Bmemarg => LOAD I64 (16 _ U) ao
| 0x34 ao:Bmemarg => LOAD I64 (32 _ S) ao
| 0x35 ao:Bmemarg => LOAD I64 (32 _ U) ao
| 0x2C ao:Bmemarg => LOAD I32 (8 S) ao
| 0x2D ao:Bmemarg => LOAD I32 (8 U) ao
| 0x2E ao:Bmemarg => LOAD I32 (16 S) ao
| 0x2F ao:Bmemarg => LOAD I32 (16 U) ao
| 0x30 ao:Bmemarg => LOAD I64 (8 S) ao
| 0x31 ao:Bmemarg => LOAD I64 (8 U) ao
| 0x32 ao:Bmemarg => LOAD I64 (16 S) ao
| 0x33 ao:Bmemarg => LOAD I64 (16 U) ao
| 0x34 ao:Bmemarg => LOAD I64 (32 S) ao
| 0x35 ao:Bmemarg => LOAD I64 (32 U) ao
| 0x36 ao:Bmemarg => STORE I32 ao
| 0x37 ao:Bmemarg => STORE I64 ao
| 0x38 ao:Bmemarg => STORE F32 ao
Expand Down
13 changes: 7 additions & 6 deletions spectec/spec/wasm-2.0/1-syntax.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -242,6 +242,7 @@ def $zero(Fnn) = $fzero($size(Fnn))
;; Numeric operators

syntax sx hint(desc "signedness") = U | S
syntax sz hint(desc "pack size") = `8 | `16 | `32 | `64

syntax unop_(numtype)
syntax unop_(Inn) = CLZ | CTZ | POPCNT | EXTEND n
Expand Down Expand Up @@ -343,6 +344,9 @@ syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32}

var ao : memarg

syntax loadop_(numtype)
syntax loadop_(Inn) = sz sx hint(show %0#_#%1) -- if sz < $sizenn(Inn)

syntax vloadop =
| SHAPE nat X nat sx hint(show %#X#%#_#%)
| SPLAT nat hint(show %#_#SPLAT)
Expand Down Expand Up @@ -462,13 +466,10 @@ syntax instr/elem hint(desc "element instruction") = ...
| ELEM.DROP elemidx
| ...

syntax sz hint(desc "pack size") = `8 | `16 | `32 | `64

syntax instr/memory hint(desc "memory instruction") = ...
| LOAD numtype (sz _ sx)? memarg hint(show %.LOAD % %) hint(show %.LOAD#% % %)
-- (if numtype = Inn /\ sz < $size(Inn))? ;; TODO: take size implicitly
| STORE numtype sz? memarg hint(show %.STORE % %) hint(show %.STORE#% % %)
-- (if numtype = Inn /\ sz < $size(Inn))? ;; TODO: take size implicitly
| LOAD numtype loadop_(numtype)? memarg hint(show %.LOAD % %) hint(show %.LOAD# ##% %)
| STORE numtype sz? memarg hint(show %.STORE % %) hint(show %.STORE#% %)
-- (if numtype = Inn /\ sz < $sizenn(Inn))?
| VLOAD vectype vloadop? memarg hint(show %.LOAD % %) hint(show %.LOAD#% % %)
| VLOAD_LANE vectype sz memarg laneidx hint(show %.LOAD#%#_#LANE % % %)
| VSTORE vectype memarg hint(show %.STORE % %)
Expand Down
26 changes: 25 additions & 1 deletion spectec/spec/wasm-2.0/6-typing.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -446,19 +446,43 @@ rule Instr_ok/data.drop:
C |- DATA.DROP x : eps -> eps
-- if C.DATAS[x] = OK

(;
rule Instr_ok/load:
C |- LOAD nt (n _ sx)? memarg : I32 -> nt
C |- LOAD nt (n sx)? memarg : I32 -> nt
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(nt)/8)
-- if $(2^(memarg.ALIGN) <= n/8 < $size(nt)/8)?
-- if n? = eps \/ nt = Inn
;)

rule Instr_ok/load-val:
C |- LOAD nt memarg : I32 -> nt
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(nt)/8)

rule Instr_ok/load-pack:
C |- LOAD Inn (M sx) memarg : I32 -> Inn
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= M/8)

(;
rule Instr_ok/store:
C |- STORE nt n? memarg : I32 nt -> eps
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(nt)/8)
-- if $(2^(memarg.ALIGN) <= n/8 < $size(nt)/8)?
-- if n? = eps \/ nt = Inn
;)

rule Instr_ok/store-val:
C |- STORE nt memarg : I32 nt -> eps
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(nt)/8)

rule Instr_ok/store-pack:
C |- STORE Inn M memarg : I32 Inn -> eps
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= M/8)

rule Instr_ok/vload:
C |- VLOAD V128 (SHAPE M X N sx) memarg : I32 -> V128
Expand Down
8 changes: 4 additions & 4 deletions spectec/spec/wasm-2.0/8-reduction.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -492,11 +492,11 @@ rule Step_read/load-num-val:
-- if $nbytes_(nt, c) = $mem(z, 0).BYTES[i + ao.OFFSET : $size(nt)/8]

rule Step_read/load-pack-trap:
z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> TRAP
z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> TRAP
-- if $(i + ao.OFFSET + n/8 > |$mem(z, 0).BYTES|)

rule Step_read/load-pack-val:
z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c))
z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c))
-- if $ibytes_(n, c) = $mem(z, 0).BYTES[i + ao.OFFSET : n/8]

rule Step_read/vload-oob:
Expand Down Expand Up @@ -629,14 +629,14 @@ rule Step_read/memory.copy-zero:

rule Step_read/memory.copy-le:
z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (MEMORY.COPY) ~>
(CONST I32 j) (CONST I32 i) (LOAD I32 (8 _ U) $memarg0) (STORE I32 8 $memarg0)
(CONST I32 j) (CONST I32 i) (LOAD I32 (8 U) $memarg0) (STORE I32 8 $memarg0)
(CONST I32 $(j+1)) (CONST I32 $(i+1)) (CONST I32 $(n-1)) (MEMORY.COPY)
-- otherwise
-- if j <= i

rule Step_read/memory.copy-gt:
z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (MEMORY.COPY) ~>
(CONST I32 $(j+n-1)) (CONST I32 $(i+n-1)) (LOAD I32 (8 _ U) $memarg0) (STORE I32 8 $memarg0)
(CONST I32 $(j+n-1)) (CONST I32 $(i+n-1)) (LOAD I32 (8 U) $memarg0) (STORE I32 8 $memarg0)
(CONST I32 j) (CONST I32 i) (CONST I32 $(n-1)) (MEMORY.COPY)
-- otherwise

Expand Down
20 changes: 10 additions & 10 deletions spectec/spec/wasm-2.0/A-binary.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -221,16 +221,16 @@ grammar Binstr/memory : instr = ...
| 0x29 ao:Bmemarg => LOAD I64 ao
| 0x2A ao:Bmemarg => LOAD F32 ao
| 0x2B ao:Bmemarg => LOAD F64 ao
| 0x2C ao:Bmemarg => LOAD I32 (8 _ S) ao
| 0x2D ao:Bmemarg => LOAD I32 (8 _ U) ao
| 0x2E ao:Bmemarg => LOAD I32 (16 _ S) ao
| 0x2F ao:Bmemarg => LOAD I32 (16 _ U) ao
| 0x30 ao:Bmemarg => LOAD I64 (8 _ S) ao
| 0x31 ao:Bmemarg => LOAD I64 (8 _ U) ao
| 0x32 ao:Bmemarg => LOAD I64 (16 _ S) ao
| 0x33 ao:Bmemarg => LOAD I64 (16 _ U) ao
| 0x34 ao:Bmemarg => LOAD I64 (32 _ S) ao
| 0x35 ao:Bmemarg => LOAD I64 (32 _ U) ao
| 0x2C ao:Bmemarg => LOAD I32 (8 S) ao
| 0x2D ao:Bmemarg => LOAD I32 (8 U) ao
| 0x2E ao:Bmemarg => LOAD I32 (16 S) ao
| 0x2F ao:Bmemarg => LOAD I32 (16 U) ao
| 0x30 ao:Bmemarg => LOAD I64 (8 S) ao
| 0x31 ao:Bmemarg => LOAD I64 (8 U) ao
| 0x32 ao:Bmemarg => LOAD I64 (16 S) ao
| 0x33 ao:Bmemarg => LOAD I64 (16 U) ao
| 0x34 ao:Bmemarg => LOAD I64 (32 S) ao
| 0x35 ao:Bmemarg => LOAD I64 (32 U) ao
| 0x36 ao:Bmemarg => STORE I32 ao
| 0x37 ao:Bmemarg => STORE I64 ao
| 0x38 ao:Bmemarg => STORE F32 ao
Expand Down
9 changes: 5 additions & 4 deletions spectec/spec/wasm-3.0/1-syntax.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -567,9 +567,10 @@ syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32}
var ao : memarg

syntax loadop_(numtype)
syntax loadop_(Inn) =
sz sx hint(show %0#_#%1) -- if sz < $sizenn(Inn)
;; syntax loadop_(Fnn) = | ;; uninhabited
syntax loadop_(Inn) = sz sx hint(show %0#_#%1) -- if sz < $sizenn(Inn)

syntax storeop_(numtype)
syntax storeop_(Inn) = sz -- if sz < $sizenn(Inn)

syntax vloadop_(vectype) hint(macro "%" "L%") =
| SHAPE sz X M sx hint(show %1#X#%3#_#%4) hint(macro "%shape") -- if $(sz * M = $vsize(vectype)/2)
Expand Down Expand Up @@ -753,7 +754,7 @@ syntax instr/elem hint(desc "element instruction") = ...

syntax instr/memory hint(desc "memory instruction") = ...
| LOAD numtype loadop_(numtype)? memidx memarg hint(show %.LOAD % %) hint(show %.LOAD# ##% % %)
| STORE numtype sz? memidx memarg hint(show %.STORE % %) hint(show %.STORE#% % %)
| STORE numtype storeop_(numtype)? memidx memarg hint(show %.STORE % %) hint(show %.STORE#% % %)
| VLOAD vectype vloadop_(vectype)? memidx memarg hint(show %.LOAD % %) hint(show %.LOAD# ##% % %) hint(macro "V%")
| VLOAD_LANE vectype sz memidx memarg laneidx hint(show %.LOAD#%#_#LANE % % %) hint(macro "V%")
| VSTORE vectype memidx memarg hint(show %.STORE % %) hint(macro "V%")
Expand Down
4 changes: 2 additions & 2 deletions spectec/spec/wasm-3.0/2-syntax-aux.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -539,9 +539,9 @@ def $free_instr(TABLE.INIT tableidx elemidx) =
$free_tableidx(tableidx) ++ $free_elemidx(elemidx)
def $free_instr(ELEM.DROP elemidx) = $free_elemidx(elemidx)

def $free_instr(LOAD numtype loadop memidx memarg) =
def $free_instr(LOAD numtype loadop? memidx memarg) =
$free_numtype(numtype) ++ $free_memidx(memidx)
def $free_instr(STORE numtype sz? memidx memarg) =
def $free_instr(STORE numtype storeop? memidx memarg) =
$free_numtype(numtype) ++ $free_memidx(memidx)
def $free_instr(VLOAD vectype vloadop? memidx memarg) =
$free_vectype(vectype) ++ $free_memidx(memidx)
Expand Down
2 changes: 1 addition & 1 deletion spectec/spec/wasm-3.0/5-runtime.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ syntax val hint(desc "value") =
| num | vec | ref

syntax result hint(desc "result") =
| _VALS val* | _EXN (REF.EXN_ADDR exnaddr) THROW_REF | TRAP
| _VALS val* | `(REF.EXN_ADDR exnaddr) THROW_REF | TRAP


var r : ref
Expand Down
4 changes: 2 additions & 2 deletions spectec/spec/wasm-3.0/8-reduction.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -979,12 +979,12 @@ rule Step/store-num-val:
-- if b* = $nbytes_(nt, c)

rule Step/store-pack-oob:
z; (CONST I32 i) (CONST Inn c) (STORE nt n x ao) ~> z; TRAP
z; (CONST I32 i) (CONST Inn c) (STORE Inn n x ao) ~> z; TRAP
----
-- if $(i + ao.OFFSET + n/8) > |$mem(z, x).BYTES|

rule Step/store-pack-val:
z; (CONST I32 i) (CONST Inn c) (STORE nt n x ao) ~> $with_mem(z, x, $(i + ao.OFFSET), $(n/8), b*); eps
z; (CONST I32 i) (CONST Inn c) (STORE Inn n x ao) ~> $with_mem(z, x, $(i + ao.OFFSET), $(n/8), b*); eps
----
;; TODO(3, rossberg): enable otherwise?
-- if b* = $ibytes_(n, $wrap__($size(Inn), n, c))
Expand Down
Loading

0 comments on commit a8000fe

Please sign in to comment.