Skip to content

Commit aaf9ffb

Browse files
rossbergrossberg
authored
[spectec] Make definition of state access nicer (#2036)
1 parent be6efe6 commit aaf9ffb

11 files changed

Lines changed: 350 additions & 251 deletions

File tree

‎specification/sync-wasm-latest.sh‎

Lines changed: 13 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,19 +30,26 @@ for FILE in $HIGHEST_FILES; do
3030
if [ ! -f "$LATEST/$FILE" ]; then
3131
echo "Added file $HIGHEST/$FILE"
3232
((++HIGHEST_CHANGED))
33-
elif [ "$HIGHEST/$FILE" -nt "$LATEST/$FILE" ] && ! diff -q "$HIGHEST/$FILE" "$LATEST/$FILE" >/dev/null; then
34-
echo "Modified file $HIGHEST/$FILE"
35-
((++HIGHEST_CHANGED))
33+
elif ! diff -q "$HIGHEST/$FILE" "$LATEST/$FILE" >/dev/null; then
34+
if [ "$HIGHEST/$FILE" -nt "$LATEST/$FILE" ]; then
35+
echo "Modified file $HIGHEST/$FILE"
36+
((++HIGHEST_CHANGED))
37+
elif ! [ "$HIGHEST/$FILE" -ot "$LATEST/$FILE" ]; then
38+
echo "❌ Error: Changes in both $HIGHEST/$FILE and $LATEST/$FILE with same date."
39+
exit 1
40+
fi
3641
fi
3742
done
3843

3944
for FILE in $LATEST_FILES; do
4045
if [ ! -f "$HIGHEST/$FILE" ]; then
4146
echo "Added file $LATEST/$FILE"
4247
((++LATEST_CHANGED))
43-
elif [ "$LATEST/$FILE" -nt "$HIGHEST/$FILE" ] && ! diff -q "$HIGHEST/$FILE" "$LATEST/$FILE" >/dev/null; then
44-
echo "Modified file $LATEST/$FILE"
45-
((++LATEST_CHANGED))
48+
elif ! diff -q "$HIGHEST/$FILE" "$LATEST/$FILE" >/dev/null; then
49+
if [ "$LATEST/$FILE" -nt "$HIGHEST/$FILE" ]; then
50+
echo "Modified file $LATEST/$FILE"
51+
((++LATEST_CHANGED))
52+
fi
4653
fi
4754
done
4855

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

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

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

273279

274280
;; State update
@@ -284,25 +290,25 @@ def $with_data(state, dataidx, byte*) : state hint(show %[.DATAS[%
284290
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)
285291
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)
286292

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

298304

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

303-
def $add_structinst((s; f), si*) = s[.STRUCTS =++ si*]; f
304-
def $add_arrayinst((s; f), ai*) = s[.ARRAYS =++ ai*]; f
305-
def $add_exninst((s; f), exn*) = s[.EXNS =++ exn*]; f
309+
def $add_structinst(z, si*) = $sof(z)[.STRUCTS =++ si*]; $fof(z)
310+
def $add_arrayinst(z, ai*) = $sof(z)[.ARRAYS =++ ai*]; $fof(z)
311+
def $add_exninst(z, exn*) = $sof(z)[.EXNS =++ exn*]; $fof(z)
306312

307313

308314
;; Growing

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

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

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

273279

274280
;; State update
@@ -284,25 +290,25 @@ def $with_data(state, dataidx, byte*) : state hint(show %[.DATAS[%
284290
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)
285291
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)
286292

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

298304

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

303-
def $add_structinst((s; f), si*) = s[.STRUCTS =++ si*]; f
304-
def $add_arrayinst((s; f), ai*) = s[.ARRAYS =++ ai*]; f
305-
def $add_exninst((s; f), exn*) = s[.EXNS =++ exn*]; f
309+
def $add_structinst(z, si*) = $sof(z)[.STRUCTS =++ si*]; $fof(z)
310+
def $add_arrayinst(z, ai*) = $sof(z)[.ARRAYS =++ ai*]; $fof(z)
311+
def $add_exninst(z, exn*) = $sof(z)[.EXNS =++ exn*]; $fof(z)
306312

307313

308314
;; Growing

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

0 Bytes
Binary file not shown.

‎spectec/src/backend-interpreter/interpreter.ml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -359,6 +359,7 @@ and eval_expr env expr =
359359
fail_expr expr (sprintf "cannot choose an element from %s because it's empty" (string_of_expr e))
360360
else
361361
Array.get a 0
362+
(* HARDCODE: The variable s is always assumed to be the implicit store *)
362363
| VarE "s" -> Store.get ()
363364
| VarE name -> lookup_env name env
364365
(* Optimized getter for simple IterE(VarE, ...) *)
@@ -796,6 +797,9 @@ and create_context (name: string) (args: value list) : AlContext.mode =
796797
AlContext.al (name, params, body, env, 0)
797798

798799
and call_func (name: string) (args: value list) : value option =
800+
(* HARDCODE: Calling the function named `store` is always implicitly assumed to be the getting the global store, as if the variable named `s`. *)
801+
if name = "store" then Some (Store.get ()) else
802+
799803
let builtin_name, is_builtin =
800804
match find_hint name "builtin" with
801805
| None -> name, false

‎spectec/src/il2al/transpile.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1025,7 +1025,7 @@ let hide_state instr =
10251025
let access = { (mk_access ps s) with note } in
10261026
[ appendI (access, e) ~at:at ]
10271027
(* Return *)
1028-
| ReturnI (Some e) when is_state e || is_store e -> [ returnI None ~at:at ]
1028+
| ReturnI (Some ({it = VarE _; _} as e)) when is_state e || is_store e -> [ returnI None ~at:at ]
10291029
| _ -> [ instr ]
10301030

10311031
let remove_state algo =

0 commit comments

Comments
 (0)