| ;; |
| ;; Auxiliary definitions on Values |
| ;; |
| |
| ;; Default values |
| |
| def $default_(valtype) : val |
| |
| def $default_(I32) = (CONST I32 0) |
| def $default_(I64) = (CONST I64 0) |
| def $default_(F32) = (CONST F32 $fzero(32)) |
| def $default_(F64) = (CONST F64 $fzero(64)) |
| |
| |
| ;; Projections |
| |
| def $funcsxa(externaddr*) : funcaddr* hint(show $funcs(%)) |
| def $globalsxa(externaddr*) : globaladdr* hint(show $globals(%)) |
| def $tablesxa(externaddr*) : tableaddr* hint(show $tables(%)) |
| def $memsxa(externaddr*) : memaddr* hint(show $mems(%)) |
| |
| def $funcsxa(eps) = eps |
| def $funcsxa((FUNC fa) xv*) = fa $funcsxa(xv*) |
| def $funcsxa(externaddr xv*) = $funcsxa(xv*) -- otherwise |
| |
| def $globalsxa(eps) = eps |
| def $globalsxa((GLOBAL ga) xv*) = ga $globalsxa(xv*) |
| def $globalsxa(externaddr xv*) = $globalsxa(xv*) -- otherwise |
| |
| def $tablesxa(eps) = eps |
| def $tablesxa((TABLE ta) xv*) = ta $tablesxa(xv*) |
| def $tablesxa(externaddr xv*) = $tablesxa(xv*) -- otherwise |
| |
| def $memsxa(eps) = eps |
| def $memsxa((MEM ma) xv*) = ma $memsxa(xv*) |
| def $memsxa(externaddr xv*) = $memsxa(xv*) -- otherwise |
| |
| |
| |
| ;; |
| ;; Auxiliary definitions on State |
| ;; |
| |
| ;; Short-hands |
| |
| def $store(state) : store hint(show %.STORE) |
| def $frame(state) : frame hint(show %.FRAME) |
| |
| def $store((s; f)) = s |
| def $frame((s; f)) = f |
| |
| |
| def $funcaddr(state) : funcaddr* hint(show %.MODULE.FUNCS) |
| def $funcaddr((s; f)) = f.MODULE.FUNCS |
| |
| def $funcinst(state) : funcinst* hint(show %.FUNCS) |
| def $globalinst(state) : globalinst* hint(show %.GLOBALS) |
| def $tableinst(state) : tableinst* hint(show %.TABLES) |
| def $meminst(state) : meminst* hint(show %.MEMS) |
| def $moduleinst(state) : moduleinst hint(show %.MODULE) |
| |
| def $funcinst((s; f)) = s.FUNCS |
| def $globalinst((s; f)) = s.GLOBALS |
| def $tableinst((s; f)) = s.TABLES |
| def $meminst((s; f)) = s.MEMS |
| def $moduleinst((s; f)) = f.MODULE |
| |
| def $type(state, typeidx) : functype hint(show %.TYPES[%]) |
| def $func(state, funcidx) : funcinst hint(show %.FUNCS[%]) |
| def $global(state, globalidx) : globalinst hint(show %.GLOBALS[%]) |
| def $table(state, tableidx) : tableinst hint(show %.TABLES[%]) |
| def $mem(state, memidx) : meminst hint(show %.MEMS[%]) |
| def $local(state, localidx) : val hint(show %.LOCALS[%]) |
| |
| def $type((s; f), x) = f.MODULE.TYPES[x] |
| def $func((s; f), x) = s.FUNCS[f.MODULE.FUNCS[x]] |
| def $global((s; f), x) = s.GLOBALS[f.MODULE.GLOBALS[x]] |
| def $table((s; f), x) = s.TABLES[f.MODULE.TABLES[x]] |
| def $mem((s; f), x) = s.MEMS[f.MODULE.MEMS[x]] |
| def $local((s; f), x) = f.LOCALS[x] |
| |
| |
| ;; Update |
| |
| def $with_local(state, localidx, val) : state hint(show %[.LOCALS[%] = %]) |
| def $with_global(state, globalidx, val) : state hint(show %[.GLOBALS[%].VALUE = %]) |
| def $with_table(state, tableidx, nat, funcaddr) : state hint(show %[.TABLES[%].REFS[%] = %]) |
| def $with_tableinst(state, tableidx, tableinst) : state hint(show %[.TABLES[%] = %]) |
| def $with_mem(state, memidx, nat, nat, byte*) : state hint(show %[.MEMS[%].BYTES[% : %] = %]) |
| def $with_meminst(state, memidx, meminst) : state hint(show %[.MEMS[%] = %]) |
| |
| def $with_local((s; f), x, v) = s; f[.LOCALS[x] = v] |
| def $with_global((s; f), x, v) = s[.GLOBALS[f.MODULE.GLOBALS[x]].VALUE = v]; f |
| def $with_table((s; f), x, i, a) = s[.TABLES[f.MODULE.TABLES[x]].REFS[i] = a]; f |
| def $with_tableinst((s; f), x, ti) = s[.TABLES[f.MODULE.TABLES[x]] = ti]; f |
| def $with_mem((s; f), x, i, j, b*) = s[.MEMS[f.MODULE.MEMS[x]].BYTES[i : j] = b*]; f |
| def $with_meminst((s; f), x, mi) = s[.MEMS[f.MODULE.MEMS[x]] = mi]; f |
| |
| |
| ;; Growing |
| |
| def $growtable(tableinst, nat) : tableinst hint(partial) |
| def $growmemory(meminst, nat) : meminst hint(partial) |
| |
| def $growtable(ti, n) = ti' |
| -- if ti = { TYPE `[i .. j?], REFS a* } |
| -- if i' = $(|a*| + n) |
| -- if ti' = { TYPE `[i' .. j?], REFS a* eps^n } |
| -- (if i' <= j)? |
| |
| def $growmemory(mi, n) = mi' |
| -- if mi = { TYPE `[i .. j?], BYTES b* } |
| -- if i' = $(|b*| / (64 * $Ki) + n) |
| -- if mi' = { TYPE `[i' .. j?], BYTES b* 0^(n * $($(64 * $Ki))) } |
| -- (if i' <= j)? |
