spec/specification/wasm-3.0/4.1-execution.values.spectec at 5fc15841e8f7cbebc052d0d621d97424d3fb220e · WebAssembly/spec · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
;;
;; Runtime Inspection of Values
;;

;; Default values

def $default_(valtype) : val?
def $default_(Inn) = (CONST Inn 0)
def $default_(Fnn) = (CONST Fnn $fzero($size(Fnn)))
def $default_(Vnn) = (VCONST Vnn 0)
def $default_(REF NULL ht) = REF.NULL_ADDR
def $default_(REF ht) = eps

;;relation Defaultable: |- valtype DEFAULTABLE ;; forward-declared in validation.instructions
rule Defaultable: |- t DEFAULTABLE -- if $default_(t) =/= eps

;;relation Nondefaultable: |- valtype NONDEFAULTABLE ;; forward-declared in validation.instructions
rule Nondefaultable: |- t NONDEFAULTABLE -- if $default_(t) = eps


;; Values

relation Num_ok: store |- num : numtype  hint(macro "%num")
relation Vec_ok: store |- vec : vectype  hint(macro "%vec")
relation Ref_ok: store |- ref : reftype  hint(macro "%ref")
relation Val_ok: store |- val : valtype  hint(macro "%val")

rule Num_ok:
  s |- CONST nt c : nt

rule Vec_ok:
  s |- VCONST vt c : vt


rule Ref_ok/null:
  s |- REF.NULL_ADDR : (REF NULL BOT)

rule Ref_ok/i31:
  s |- REF.I31_NUM i : (REF I31)

rule Ref_ok/struct:
  s |- REF.STRUCT_ADDR a : (REF dt)
  -- if s.STRUCTS[a].TYPE = dt

rule Ref_ok/array:
  s |- REF.ARRAY_ADDR a : (REF dt)
  -- if s.ARRAYS[a].TYPE = dt

rule Ref_ok/func:
  s |- REF.FUNC_ADDR a : (REF dt)
  -- if s.FUNCS[a].TYPE = dt

rule Ref_ok/exn:
  s |- REF.EXN_ADDR a : (REF EXN)
  -- if s.EXNS[a] = exn

rule Ref_ok/host:
  s |- REF.HOST_ADDR a : (REF ANY)

rule Ref_ok/extern:
  s |- REF.EXTERN ref : (REF EXTERN)
  -- Ref_ok: s |- ref : (REF ANY)
  -- if ref =/= REF.NULL_ADDR

rule Ref_ok/sub:
  s |- ref : rt
  -- Ref_ok: s |- ref : rt'
  -- Reftype_sub: {} |- rt' <: rt


rule Val_ok/num:
  s |- num : nt
  -- Num_ok: s |- num : nt

rule Val_ok/vec:
  s |- vec : vt
  -- Vec_ok: s |- vec : vt

rule Val_ok/ref:
  s |- ref : rt
  -- Ref_ok: s |- ref : rt


;; Field values

relation Packval_ok: store |- packval : packtype
relation Fieldval_ok: store |- fieldval : storagetype

rule Packval_ok:
  s |- PACK pt c : pt

rule Fieldval_ok/val:
  s |- val : t
  -- Val_ok: s |- val : t

rule Fieldval_ok/packval:
  s |- packval : pt
  -- Packval_ok: s |- packval : pt


;; External addresses

relation Externaddr_ok: store |- externaddr : externtype  hint(macro "%externaddr")

rule Externaddr_ok/tag:
  s |- TAG a : TAG taginst.TYPE
  -- if s.TAGS[a] = taginst

rule Externaddr_ok/global:
  s |- GLOBAL a : GLOBAL globalinst.TYPE
  -- if s.GLOBALS[a] = globalinst

rule Externaddr_ok/mem:
  s |- MEM a : MEM meminst.TYPE
  -- if s.MEMS[a] = meminst

rule Externaddr_ok/table:
  s |- TABLE a : TABLE tableinst.TYPE
  -- if s.TABLES[a] = tableinst

rule Externaddr_ok/func:
  s |- FUNC a : FUNC funcinst.TYPE
  -- if s.FUNCS[a] = funcinst

rule Externaddr_ok/sub:
  s |- externaddr : xt
  -- Externaddr_ok: s |- externaddr : xt'
  -- Externtype_sub: {} |- xt' <: xt