Skip to content

Commit acaebb2

Browse files
rossbergrossberg
committed
[spec] Add definitions for state access shorthands
1 parent d825fa0 commit acaebb2

File tree

3 files changed

+44
-60
lines changed

3 files changed

+44
-60
lines changed

‎specification/wasm-3.0/4.0-execution.configurations.spectec‎

Lines changed: 22 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -263,21 +263,15 @@ def $data(state, dataidx) : datainst hint(show %.DATAS[%]) hint(macro "
263263
def $elem(state, tableidx) : eleminst hint(show %.ELEMS[%]) hint(macro "Z%")
264264
def $local(state, localidx) : val? hint(show %.LOCALS[%]) hint(macro "Z%")
265265

266-
def $sof(state) : store hint(show s)
267-
def $fof(state) : frame hint(show f)
268-
269-
def $sof(z) = $store(z)
270-
def $fof(z) = $frame(z)
271-
272-
def $type(z, x) = $fof(z).MODULE.TYPES[x]
273-
def $tag(z, x) = $sof(z).TAGS[$fof(z).MODULE.TAGS[x]]
274-
def $global(z, x) = $sof(z).GLOBALS[$fof(z).MODULE.GLOBALS[x]]
275-
def $mem(z, x) = $sof(z).MEMS[$fof(z).MODULE.MEMS[x]]
276-
def $table(z, x) = $sof(z).TABLES[$fof(z).MODULE.TABLES[x]]
277-
def $func(z, x) = $sof(z).FUNCS[$fof(z).MODULE.FUNCS[x]]
278-
def $data(z, x) = $sof(z).DATAS[$fof(z).MODULE.DATAS[x]]
279-
def $elem(z, x) = $sof(z).ELEMS[$fof(z).MODULE.ELEMS[x]]
280-
def $local(z, x) = $fof(z).LOCALS[x]
266+
def $type((s; f), x) = f.MODULE.TYPES[x]
267+
def $tag((s; f), x) = s.TAGS[f.MODULE.TAGS[x]]
268+
def $global((s; f), x) = s.GLOBALS[f.MODULE.GLOBALS[x]]
269+
def $mem((s; f), x) = s.MEMS[f.MODULE.MEMS[x]]
270+
def $table((s; f), x) = s.TABLES[f.MODULE.TABLES[x]]
271+
def $func((s; f), x) = s.FUNCS[f.MODULE.FUNCS[x]]
272+
def $data((s; f), x) = s.DATAS[f.MODULE.DATAS[x]]
273+
def $elem((s; f), x) = s.ELEMS[f.MODULE.ELEMS[x]]
274+
def $local((s; f), x) = f.LOCALS[x]
281275

282276

283277
;; State update
@@ -293,25 +287,25 @@ def $with_data(state, dataidx, byte*) : state hint(show %[.DATAS[%
293287
def $with_struct(state, structaddr, nat, fieldval) : state hint(show %[.STRUCTS[%].FIELDS[%] = %]) hint(macro "ZS%") hint(prose "Replace" $structinst(%1)[%2].FIELDS[%3] "with" %4)
294288
def $with_array(state, arrayaddr, nat, fieldval) : state hint(show %[.ARRAYS[%].FIELDS[%] = %]) hint(macro "ZA%") hint(prose "Replace" $arrayinst(%1)[%2].FIELDS[%3] "with" %4)
295289

296-
def $with_local(z, x, v) = $sof(z); $fof(z)[.LOCALS[x] = v]
297-
def $with_global(z, x, v) = $sof(z)[.GLOBALS[$fof(z).MODULE.GLOBALS[x]].VALUE = v]; $fof(z)
298-
def $with_table(z, x, i, r) = $sof(z)[.TABLES[$fof(z).MODULE.TABLES[x]].REFS[i] = r]; $fof(z)
299-
def $with_tableinst(z, x, ti) = $sof(z)[.TABLES[$fof(z).MODULE.TABLES[x]] = ti]; $fof(z)
300-
def $with_mem(z, x, i, j, b*) = $sof(z)[.MEMS[$fof(z).MODULE.MEMS[x]].BYTES[i : j] = b*]; $fof(z)
301-
def $with_meminst(z, x, mi) = $sof(z)[.MEMS[$fof(z).MODULE.MEMS[x]] = mi]; $fof(z)
302-
def $with_elem(z, x, r*) = $sof(z)[.ELEMS[$fof(z).MODULE.ELEMS[x]].REFS = r*]; $fof(z)
303-
def $with_data(z, x, b*) = $sof(z)[.DATAS[$fof(z).MODULE.DATAS[x]].BYTES = b*]; $fof(z)
304-
def $with_struct(z, a, i, fv) = $sof(z)[.STRUCTS[a].FIELDS[i] = fv]; $fof(z)
305-
def $with_array(z, a, i, fv) = $sof(z)[.ARRAYS[a].FIELDS[i] = fv]; $fof(z)
290+
def $with_local((s; f), x, v) = s; f[.LOCALS[x] = v]
291+
def $with_global((s; f), x, v) = s[.GLOBALS[f.MODULE.GLOBALS[x]].VALUE = v]; f
292+
def $with_table((s; f), x, i, r) = s[.TABLES[f.MODULE.TABLES[x]].REFS[i] = r]; f
293+
def $with_tableinst((s; f), x, ti) = s[.TABLES[f.MODULE.TABLES[x]] = ti]; f
294+
def $with_mem((s; f), x, i, j, b*) = s[.MEMS[f.MODULE.MEMS[x]].BYTES[i : j] = b*]; f
295+
def $with_meminst((s; f), x, mi) = s[.MEMS[f.MODULE.MEMS[x]] = mi]; f
296+
def $with_elem((s; f), x, r*) = s[.ELEMS[f.MODULE.ELEMS[x]].REFS = r*]; f
297+
def $with_data((s; f), x, b*) = s[.DATAS[f.MODULE.DATAS[x]].BYTES = b*]; f
298+
def $with_struct((s; f), a, i, fv) = s[.STRUCTS[a].FIELDS[i] = fv]; f
299+
def $with_array((s; f), a, i, fv) = s[.ARRAYS[a].FIELDS[i] = fv]; f
306300

307301

308302
def $add_structinst(state, structinst*) : state hint(show %[.STRUCTS =++ %]) hint(macro "Z%") hint(prose "Append" %2 "to" $structinst(%1))
309303
def $add_arrayinst(state, arrayinst*) : state hint(show %[.ARRAYS =++ %]) hint(macro "Z%") hint(prose "Append" %2 "to" $arrayinst(%1))
310304
def $add_exninst(state, exninst*) : state hint(show %[.EXNS =++ %]) hint(macro "Z%") hint(prose "Append" %2 "to" $exninst(%1))
311305

312-
def $add_structinst(z, si*) = $sof(z)[.STRUCTS =++ si*]; $fof(z)
313-
def $add_arrayinst(z, ai*) = $sof(z)[.ARRAYS =++ ai*]; $fof(z)
314-
def $add_exninst(z, exn*) = $sof(z)[.EXNS =++ exn*]; $fof(z)
306+
def $add_structinst((s; f), si*) = s[.STRUCTS =++ si*]; f
307+
def $add_arrayinst((s; f), ai*) = s[.ARRAYS =++ ai*]; f
308+
def $add_exninst((s; f), exn*) = s[.EXNS =++ exn*]; f
315309

316310

317311
;; Growing

‎spectec/doc/example/output/NanoWasm.pdf‎

-69 Bytes
Binary file not shown.

‎spectec/test-frontend/TEST.md‎

Lines changed: 22 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -5670,125 +5670,115 @@ def $exninst(state : state) : exninst*
56705670
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
56715671
def $exninst{s : store, f : frame}(`%;%`_state(s, f)) = s.EXNS_store
56725672

5673-
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5674-
def $fof(state : state) : frame
5675-
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5676-
def $fof{z : state}(z) = $frame(z)
5677-
56785673
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
56795674
def $type(state : state, typeidx : typeidx) : deftype
56805675
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5681-
def $type{z : state, x : idx}(z, x) = $fof(z).MODULE_frame.TYPES_moduleinst[x!`%`_idx.0]
5682-
5683-
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5684-
def $sof(state : state) : store
5685-
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5686-
def $sof{z : state}(z) = $store(z)
5676+
def $type{s : store, f : frame, x : idx}(`%;%`_state(s, f), x) = f.MODULE_frame.TYPES_moduleinst[x!`%`_idx.0]
56875677

56885678
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
56895679
def $tag(state : state, tagidx : tagidx) : taginst
56905680
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5691-
def $tag{z : state, x : idx}(z, x) = $sof(z).TAGS_store[$fof(z).MODULE_frame.TAGS_moduleinst[x!`%`_idx.0]]
5681+
def $tag{s : store, f : frame, x : idx}(`%;%`_state(s, f), x) = s.TAGS_store[f.MODULE_frame.TAGS_moduleinst[x!`%`_idx.0]]
56925682

56935683
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
56945684
def $global(state : state, globalidx : globalidx) : globalinst
56955685
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5696-
def $global{z : state, x : idx}(z, x) = $sof(z).GLOBALS_store[$fof(z).MODULE_frame.GLOBALS_moduleinst[x!`%`_idx.0]]
5686+
def $global{s : store, f : frame, x : idx}(`%;%`_state(s, f), x) = s.GLOBALS_store[f.MODULE_frame.GLOBALS_moduleinst[x!`%`_idx.0]]
56975687

56985688
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
56995689
def $mem(state : state, memidx : memidx) : meminst
57005690
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5701-
def $mem{z : state, x : idx}(z, x) = $sof(z).MEMS_store[$fof(z).MODULE_frame.MEMS_moduleinst[x!`%`_idx.0]]
5691+
def $mem{s : store, f : frame, x : idx}(`%;%`_state(s, f), x) = s.MEMS_store[f.MODULE_frame.MEMS_moduleinst[x!`%`_idx.0]]
57025692

57035693
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57045694
def $table(state : state, tableidx : tableidx) : tableinst
57055695
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5706-
def $table{z : state, x : idx}(z, x) = $sof(z).TABLES_store[$fof(z).MODULE_frame.TABLES_moduleinst[x!`%`_idx.0]]
5696+
def $table{s : store, f : frame, x : idx}(`%;%`_state(s, f), x) = s.TABLES_store[f.MODULE_frame.TABLES_moduleinst[x!`%`_idx.0]]
57075697

57085698
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57095699
def $func(state : state, funcidx : funcidx) : funcinst
57105700
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5711-
def $func{z : state, x : idx}(z, x) = $sof(z).FUNCS_store[$fof(z).MODULE_frame.FUNCS_moduleinst[x!`%`_idx.0]]
5701+
def $func{s : store, f : frame, x : idx}(`%;%`_state(s, f), x) = s.FUNCS_store[f.MODULE_frame.FUNCS_moduleinst[x!`%`_idx.0]]
57125702

57135703
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57145704
def $data(state : state, dataidx : dataidx) : datainst
57155705
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5716-
def $data{z : state, x : idx}(z, x) = $sof(z).DATAS_store[$fof(z).MODULE_frame.DATAS_moduleinst[x!`%`_idx.0]]
5706+
def $data{s : store, f : frame, x : idx}(`%;%`_state(s, f), x) = s.DATAS_store[f.MODULE_frame.DATAS_moduleinst[x!`%`_idx.0]]
57175707

57185708
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57195709
def $elem(state : state, tableidx : tableidx) : eleminst
57205710
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5721-
def $elem{z : state, x : idx}(z, x) = $sof(z).ELEMS_store[$fof(z).MODULE_frame.ELEMS_moduleinst[x!`%`_idx.0]]
5711+
def $elem{s : store, f : frame, x : idx}(`%;%`_state(s, f), x) = s.ELEMS_store[f.MODULE_frame.ELEMS_moduleinst[x!`%`_idx.0]]
57225712

57235713
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57245714
def $local(state : state, localidx : localidx) : val?
57255715
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5726-
def $local{z : state, x : idx}(z, x) = $fof(z).LOCALS_frame[x!`%`_idx.0]
5716+
def $local{s : store, f : frame, x : idx}(`%;%`_state(s, f), x) = f.LOCALS_frame[x!`%`_idx.0]
57275717

57285718
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57295719
def $with_local(state : state, localidx : localidx, val : val) : state
57305720
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5731-
def $with_local{z : state, x : idx, v : val}(z, x, v) = `%;%`_state($sof(z), $fof(z)[LOCALS_frame[x!`%`_idx.0] = ?(v)])
5721+
def $with_local{s : store, f : frame, x : idx, v : val}(`%;%`_state(s, f), x, v) = `%;%`_state(s, f[LOCALS_frame[x!`%`_idx.0] = ?(v)])
57325722

57335723
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57345724
def $with_global(state : state, globalidx : globalidx, val : val) : state
57355725
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5736-
def $with_global{z : state, x : idx, v : val}(z, x, v) = `%;%`_state($sof(z)[GLOBALS_store[$fof(z).MODULE_frame.GLOBALS_moduleinst[x!`%`_idx.0]].VALUE_globalinst = v], $fof(z))
5726+
def $with_global{s : store, f : frame, x : idx, v : val}(`%;%`_state(s, f), x, v) = `%;%`_state(s[GLOBALS_store[f.MODULE_frame.GLOBALS_moduleinst[x!`%`_idx.0]].VALUE_globalinst = v], f)
57375727

57385728
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57395729
def $with_table(state : state, tableidx : tableidx, nat : nat, ref : ref) : state
57405730
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5741-
def $with_table{z : state, x : idx, i : nat, r : ref}(z, x, i, r) = `%;%`_state($sof(z)[TABLES_store[$fof(z).MODULE_frame.TABLES_moduleinst[x!`%`_idx.0]].REFS_tableinst[i] = r], $fof(z))
5731+
def $with_table{s : store, f : frame, x : idx, i : nat, r : ref}(`%;%`_state(s, f), x, i, r) = `%;%`_state(s[TABLES_store[f.MODULE_frame.TABLES_moduleinst[x!`%`_idx.0]].REFS_tableinst[i] = r], f)
57425732

57435733
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57445734
def $with_tableinst(state : state, tableidx : tableidx, tableinst : tableinst) : state
57455735
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5746-
def $with_tableinst{z : state, x : idx, ti : tableinst}(z, x, ti) = `%;%`_state($sof(z)[TABLES_store[$fof(z).MODULE_frame.TABLES_moduleinst[x!`%`_idx.0]] = ti], $fof(z))
5736+
def $with_tableinst{s : store, f : frame, x : idx, ti : tableinst}(`%;%`_state(s, f), x, ti) = `%;%`_state(s[TABLES_store[f.MODULE_frame.TABLES_moduleinst[x!`%`_idx.0]] = ti], f)
57475737

57485738
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57495739
def $with_mem(state : state, memidx : memidx, nat : nat, nat : nat, byte*) : state
57505740
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5751-
def $with_mem{z : state, x : idx, i : nat, j : nat, `b*` : byte*}(z, x, i, j, b*{b <- `b*`}) = `%;%`_state($sof(z)[MEMS_store[$fof(z).MODULE_frame.MEMS_moduleinst[x!`%`_idx.0]].BYTES_meminst[i : j] = b*{b <- `b*`}], $fof(z))
5741+
def $with_mem{s : store, f : frame, x : idx, i : nat, j : nat, `b*` : byte*}(`%;%`_state(s, f), x, i, j, b*{b <- `b*`}) = `%;%`_state(s[MEMS_store[f.MODULE_frame.MEMS_moduleinst[x!`%`_idx.0]].BYTES_meminst[i : j] = b*{b <- `b*`}], f)
57525742

57535743
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57545744
def $with_meminst(state : state, memidx : memidx, meminst : meminst) : state
57555745
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5756-
def $with_meminst{z : state, x : idx, mi : meminst}(z, x, mi) = `%;%`_state($sof(z)[MEMS_store[$fof(z).MODULE_frame.MEMS_moduleinst[x!`%`_idx.0]] = mi], $fof(z))
5746+
def $with_meminst{s : store, f : frame, x : idx, mi : meminst}(`%;%`_state(s, f), x, mi) = `%;%`_state(s[MEMS_store[f.MODULE_frame.MEMS_moduleinst[x!`%`_idx.0]] = mi], f)
57575747

57585748
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57595749
def $with_elem(state : state, elemidx : elemidx, ref*) : state
57605750
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5761-
def $with_elem{z : state, x : idx, `r*` : ref*}(z, x, r*{r <- `r*`}) = `%;%`_state($sof(z)[ELEMS_store[$fof(z).MODULE_frame.ELEMS_moduleinst[x!`%`_idx.0]].REFS_eleminst = r*{r <- `r*`}], $fof(z))
5751+
def $with_elem{s : store, f : frame, x : idx, `r*` : ref*}(`%;%`_state(s, f), x, r*{r <- `r*`}) = `%;%`_state(s[ELEMS_store[f.MODULE_frame.ELEMS_moduleinst[x!`%`_idx.0]].REFS_eleminst = r*{r <- `r*`}], f)
57625752

57635753
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57645754
def $with_data(state : state, dataidx : dataidx, byte*) : state
57655755
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5766-
def $with_data{z : state, x : idx, `b*` : byte*}(z, x, b*{b <- `b*`}) = `%;%`_state($sof(z)[DATAS_store[$fof(z).MODULE_frame.DATAS_moduleinst[x!`%`_idx.0]].BYTES_datainst = b*{b <- `b*`}], $fof(z))
5756+
def $with_data{s : store, f : frame, x : idx, `b*` : byte*}(`%;%`_state(s, f), x, b*{b <- `b*`}) = `%;%`_state(s[DATAS_store[f.MODULE_frame.DATAS_moduleinst[x!`%`_idx.0]].BYTES_datainst = b*{b <- `b*`}], f)
57675757

57685758
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57695759
def $with_struct(state : state, structaddr : structaddr, nat : nat, fieldval : fieldval) : state
57705760
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5771-
def $with_struct{z : state, a : addr, i : nat, fv : fieldval}(z, a, i, fv) = `%;%`_state($sof(z)[STRUCTS_store[a].FIELDS_structinst[i] = fv], $fof(z))
5761+
def $with_struct{s : store, f : frame, a : addr, i : nat, fv : fieldval}(`%;%`_state(s, f), a, i, fv) = `%;%`_state(s[STRUCTS_store[a].FIELDS_structinst[i] = fv], f)
57725762

57735763
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57745764
def $with_array(state : state, arrayaddr : arrayaddr, nat : nat, fieldval : fieldval) : state
57755765
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5776-
def $with_array{z : state, a : addr, i : nat, fv : fieldval}(z, a, i, fv) = `%;%`_state($sof(z)[ARRAYS_store[a].FIELDS_arrayinst[i] = fv], $fof(z))
5766+
def $with_array{s : store, f : frame, a : addr, i : nat, fv : fieldval}(`%;%`_state(s, f), a, i, fv) = `%;%`_state(s[ARRAYS_store[a].FIELDS_arrayinst[i] = fv], f)
57775767

57785768
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57795769
def $add_structinst(state : state, structinst*) : state
57805770
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5781-
def $add_structinst{z : state, `si*` : structinst*}(z, si*{si <- `si*`}) = `%;%`_state($sof(z)[STRUCTS_store =++ si*{si <- `si*`}], $fof(z))
5771+
def $add_structinst{s : store, f : frame, `si*` : structinst*}(`%;%`_state(s, f), si*{si <- `si*`}) = `%;%`_state(s[STRUCTS_store =++ si*{si <- `si*`}], f)
57825772

57835773
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57845774
def $add_arrayinst(state : state, arrayinst*) : state
57855775
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5786-
def $add_arrayinst{z : state, `ai*` : arrayinst*}(z, ai*{ai <- `ai*`}) = `%;%`_state($sof(z)[ARRAYS_store =++ ai*{ai <- `ai*`}], $fof(z))
5776+
def $add_arrayinst{s : store, f : frame, `ai*` : arrayinst*}(`%;%`_state(s, f), ai*{ai <- `ai*`}) = `%;%`_state(s[ARRAYS_store =++ ai*{ai <- `ai*`}], f)
57875777

57885778
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57895779
def $add_exninst(state : state, exninst*) : state
57905780
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
5791-
def $add_exninst{z : state, `exn*` : exninst*}(z, exn*{exn <- `exn*`}) = `%;%`_state($sof(z)[EXNS_store =++ exn*{exn <- `exn*`}], $fof(z))
5781+
def $add_exninst{s : store, f : frame, `exn*` : exninst*}(`%;%`_state(s, f), exn*{exn <- `exn*`}) = `%;%`_state(s[EXNS_store =++ exn*{exn <- `exn*`}], f)
57925782

57935783
;; ../../../../specification/wasm-3.0/4.0-execution.configurations.spectec
57945784
def $growtable(tableinst : tableinst, nat : nat, ref : ref) : tableinst

0 commit comments

Comments
 (0)