blob: 3fa96be75aec6236004a093b5fc35b1af1a5bbb2 (
plain)
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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
|
{-# OPTIONS --without-K --safe #-}
------------------------------------------------------------------------
-- 2.4 Types
module Wasm.Expression.Instructions where
open import Data.List using (List)
open import Data.Maybe using (Maybe)
open import Data.Product using (∃)
open import Data.Sum using (_⊎_)
open import Wasm.Expression.Values using (UnsignedInteger; UninterpretedInteger; Float)
open import Wasm.Expression.Types using (ValType; RefType)
open import Wasm.Expression.Utilities
------------------------------------------------------------------------
-- 2.4.1 Numeric Instructions
module IntOp (w : BitWidth) where
data Unary : Set where
clz : Unary
ctz : Unary
popcnt : Unary
data Binary : Set where
add : Binary
sub : Binary
mul : Binary
div : Signedness → Binary
rem : Signedness → Binary
and : Binary
or : Binary
xor : Binary
shl : Binary
shr : Signedness → Binary
rotl : Binary
rotr : Binary
data Test : Set where
eqz : Test
data Rel : Set where
eq : Rel
ne : Rel
lt : Signedness → Rel
gt : Signedness → Rel
le : Signedness → Rel
ge : Signedness → Rel
data IntInstr : Set where
const : UninterpretedInteger (BitWidth′.toℕ w) → IntInstr
iunop : Unary → IntInstr
ibinop : Binary → IntInstr
itestop : Test → IntInstr
irelop : Rel → IntInstr
extend8-s : IntInstr
extend16-s : IntInstr
trunc-f : BitWidth → Signedness → IntInstr
trunc-sat-f : BitWidth → Signedness → IntInstr
reinterpret-f : IntInstr
data IntInstr : Set where
ixx : ∀ w → IntOp.IntInstr w → IntInstr
i64-extend32-s : IntInstr
i32-wrap-i64 : IntInstr
i64-extend-i32 : Signedness → IntInstr
module FloatOp (w : BitWidth) where
data Unary : Set where
abs : Unary
neg : Unary
sqrt : Unary
ceil : Unary
floor : Unary
trunc : Unary
nearest : Unary
data Binary : Set where
add : Binary
sub : Binary
mul : Binary
div : Binary
min : Binary
max : Binary
copysign : Binary
data Rel : Set where
eq : Rel
ne : Rel
lt : Rel
gt : Rel
le : Rel
ge : Rel
data FloatInstr : Set where
const : Float w → FloatInstr
funop : Unary → FloatInstr
fbinop : Binary → FloatInstr
frelop : Rel → FloatInstr
convert-i : BitWidth → Signedness → FloatInstr
reinterpret-i : FloatInstr
data FloatInstr : Set where
fxx : ∀ w → FloatOp.FloatInstr w → FloatInstr
f32-demote-f64 : FloatInstr
f64-promote-f32 : FloatInstr
data NumInstr : Set where
int : IntInstr → NumInstr
float : FloatInstr → NumInstr
------------------------------------------------------------------------
-- 2.4.2 Reference Instructions
data RefInstr : Set where
null : RefType → RefInstr
is-null : RefInstr
func : Indices.FuncIdx → RefInstr
------------------------------------------------------------------------
-- 2.4.3 Parametric Instructions
data ParametricInstr : Set where
drop : ParametricInstr
select : Maybe (List ValType) → ParametricInstr
------------------------------------------------------------------------
-- 2.4.4 Variable Instructions
data VarInstr : Set where
local-get : Indices.LocalIdx → VarInstr
local-set : Indices.LocalIdx → VarInstr
local-tee : Indices.LocalIdx → VarInstr
global-get : Indices.GlobalIdx → VarInstr
global-set : Indices.GlobalIdx → VarInstr
------------------------------------------------------------------------
-- 2.4.5 Table Instructions
data TableInstr : Set where
get : Indices.TableIdx → TableInstr
set : Indices.TableIdx → TableInstr
size : Indices.TableIdx → TableInstr
grow : Indices.TableIdx → TableInstr
fill : Indices.TableIdx → TableInstr
copy : Indices.TableIdx → Indices.TableIdx → TableInstr
init : Indices.TableIdx → Indices.ElemIdx → TableInstr
drop : Indices.ElemIdx → TableInstr
------------------------------------------------------------------------
-- 2.4.6 Memory Instructions
record MemArg : Set where
field
offset : UnsignedInteger 32
align : UnsignedInteger 32
module IntMem (w : BitWidth) where
data IntMemInstr : Set where
load : MemArg → IntMemInstr
store : MemArg → IntMemInstr
load8 : Signedness → MemArg → IntMemInstr
load16 : Signedness → MemArg → IntMemInstr
store8 : MemArg → IntMemInstr
store16 : MemArg → IntMemInstr
data IntMemInstr : Set where
ixx : ∀ w → IntMem.IntMemInstr w → IntMemInstr
i64-load32 : Signedness → MemArg → IntMemInstr
i64-store32 : MemArg → IntMemInstr
module FloatMem (w : BitWidth) where
data FloatMemInstr : Set where
load : MemArg → FloatMemInstr
store : MemArg → FloatMemInstr
FloatMemInstr : Set
FloatMemInstr = ∃ FloatMem.FloatMemInstr
data MemInstr : Set where
int : IntMemInstr → MemInstr
float : FloatMemInstr → MemInstr
size : MemInstr
grow : MemInstr
fill : MemInstr
copy : MemInstr
init : Indices.DataIdx → MemInstr
drop : Indices.DataIdx → MemInstr
------------------------------------------------------------------------
-- 2.4.7 Control Instructions
BlockType : Set
BlockType = Indices.TypeIdx ⊎ Maybe ValType
data Instr : Set where
num : NumInstr → Instr
ref : RefInstr → Instr
parametric : ParametricInstr → Instr
var : VarInstr → Instr
table : TableInstr → Instr
mem : MemInstr → Instr
nop : Instr
unreachable : Instr
block : BlockType → List Instr → Instr
loop : BlockType → List Instr → Instr
if-else : BlockType → List Instr → List Instr → Instr
br : Indices.LabelIdx → Instr
br-if : Indices.LabelIdx → Instr
br-table : Vec′ Indices.LabelIdx → Indices.LabelIdx → Instr
return : Instr
call : Indices.FuncIdx → Instr
call-indirect : Indices.TableIdx → Indices.TypeIdx → Instr
------------------------------------------------------------------------
-- 2.4.8 Expressions
Expr : Set
Expr = List Instr
|
