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
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
|
indexvar n , m , i , j ::=
{{ phantom }}
{{ com Index variables for meta-lists }}
metavar nat ::=
{{ phantom }}
{{ ocaml int }}
{{ lem nat }}
metavar big_int ::=
{{ phantom }}
{{ lem integer }}
metavar id ::=
{{ phantom }}
{{ ocaml id }}
{{ lem id }}
metavar mid ::=
{{ phantom }}
{{ ocaml id option }}
{{ lem maybe id }}
metavar string ::=
{{ phantom }}
{{ ocaml string }}
{{ lem string }}
metavar mstring ::=
{{ phantom }}
{{ ocaml string option }}
{{ lem maybe string }}
metavar bool ::=
{{ phantom }}
{{ ocaml bool }}
{{ lem bool }}
metavar value ::=
{{ phantom }}
{{ lem vl }}
{{ ocaml vl }}
metavar alpha ::=
{{ phantom }}
{{ lem 'a }}
embed
{{ lem
open import Ast
open import Value2
}}
grammar
name :: '' ::=
| id nat :: :: name
| global id nat :: :: global
| have_exception nat :: :: have_exception
| current_exception nat :: :: current_exception
| throw_location nat :: :: throw_location
| return nat :: :: return
op :: '' ::=
| not :: :: bnot
| or :: :: bor
| and :: :: band
| hd :: :: list_hd
| tl :: :: list_tl
| eq :: :: eq
| neq :: :: neq
% Integer ops
| lt :: :: ilt
| lteq :: :: ilteq
| gt :: :: igt
| gteq :: :: igteq
| add :: :: iadd
| sub :: :: isub
| unsigned nat :: :: unsigned
| signed nat :: :: signed
% Bitvector ops
| bvnot :: :: bvnot
| bvor :: :: bvor
| bvand :: :: bvand
| bvxor :: :: bvxor
| bvadd :: :: bvadd
| bvsub :: :: bvsub
| bvaccess :: :: bvaccess
| concat :: :: concat
| zero_extend nat :: :: zero_extend
| sign_extend nat :: :: sign_extend
| slice nat :: :: slice
| sslice nat :: :: sslice
| set_slice :: :: set_slice
| replicate nat :: :: replicate
cval :: 'V_' ::=
| name : ctyp :: :: id
| value : ctyp :: :: lit
| struct { uid0 = cval0 , ... , uidn = cvaln } ctyp :: :: struct
| cval != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind
| unwrap id cval ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_unwrap
| cval nat0 nat1 :: :: tuple_member
| op ( cval0 , ... , cvaln ) :: :: call
| cval . uid :: :: field
| poly cval ctyp :: :: poly
% Note that init / clear are sometimes refered to as create / kill
%%% IR types
uid :: 'UId_' ::=
{{ phantom }}
{{ lem (id * list ctyp) }}
{{ ocaml (id * ctyp list) }}
ctyp :: 'CT_' ::=
{{ com C type }}
% Integer types
%
% lint is a large (l) arbitrary precision integer, mpz_t in C.
% fint(n) is a fixed precision signed integer that is representable in exactly n bits
| lint :: :: lint
| fint nat :: :: fint
| constant big_int :: :: constant
% Bitvector types - flag represents bit indexing direction, true - dec or false - inc
%
% lbits is a large (l) arbitrary precision bitvector
% sbits is a small (s) bitvector, such that sbits(n, _) is guaranteed to have a length of at most n.
% fbits is a fixed (f) bitvector, such that fbits(n, _) has a length of exactly n bits
| lbits ( bool ) :: :: lbits
| sbits ( nat , bool ) :: :: sbits
| fbits ( nat , bool ) :: :: fbits
% Other Sail types
| unit :: :: unit
| bool_t :: :: bool
| bit :: :: bit
| string_t :: :: string
% The real type in sail. Abstract here, so the code generator can
% choose to implement it using either GMP rationals or high-precision
% floating point.
| real :: :: real
| ( ctyp0 , ... , ctypn ) :: :: tup
% Abstractly represent how all the Sail user defined types get mapped
% into C. We don't fully worry about precise implementation details at
% this point, as C doesn't have variants or tuples natively, but these
% need to be encoded.
| enum id ( id0 , ... , idn ) :: :: enum
| struct id ( uid0 * ctyp0 , ... , uidn * ctypn ) :: :: struct
| variant id ( uid0 * ctyp0 , ... , uidn * ctypn ) :: :: variant
% A vector type for non-bit vectors, and a (linked) list type.
| fvector ( nat , bool , ctyp ) :: :: fvector
| vector ( bool , ctyp ) :: :: vector
| list ( ctyp ) :: :: list
| ref ( ctyp ) :: :: ref
% We can still have a very limited amount of polymorphism in this IR
% representation, as variants can have polymorphic constructors. The
% reason is we can put more precise types into constructors and then
% consume them as more general types meaning the underlying
% representation (rather than the high-level sail types) are what we
% need to specialise constructors, e.g. Some(0xFF) would be a Some
% constructor containing a fbits(8, true), but this could be pattern
% matched as Some(x) where the matching context expects x to have type
% lbits, and this must work without compiling to type incorrect C.
| poly :: :: poly
clexp :: 'CL_' ::=
| name : ctyp :: :: id
| name0 rmw name1 : ctyp :: :: rmw
| clexp . uid :: :: field
| * clexp :: :: addr
| clexp . nat :: :: tuple
| void :: :: void
ctype_def :: 'CTD_' ::=
{{ com C type definition }}
| enum id = id0 '|' ... '|' idn :: :: enum
| struct id = { uid0 : ctyp0 , ... , uidn : ctypn } :: :: struct
| variant id = { uid0 : ctyp0 , ... , uidn : ctypn } :: :: variant
iannot :: '' ::=
{{ lem nat * nat * nat }}
{{ ocaml int * int * int }}
instr :: 'I_' ::=
{{ aux _ iannot }}
% The following are the minimal set of instructions output by
% Jib_compile.ml.
| ctyp name :: :: decl
| ctyp name = cval :: :: init
| jump ( cval ) string :: :: jump
| goto string :: :: goto
| string : :: :: label
| clexp = bool uid ( cval0 , ... , cvaln ) :: :: funcall
| clexp = cval :: :: copy
| clear ctyp name :: :: clear
| undefined ctyp :: :: undefined
| match_failure :: :: match_failure
| end name :: :: end
% All instructions containing nested instructions can be flattened
% away. try and throw only exist for internal use within
% Jib_compile.ml, as exceptional control flow is handled by a separate
% Jib->Jib pass.
| if ( cval ) { instr0 ; ... ; instrn }
else { instr0 ; ... ; instrm } : ctyp :: :: if
| { instr0 ; ... ; instrn } :: :: block
| try { instr0 ; ... ; instrn } :: :: try_block
| throw cval :: :: throw
% We can embed either comments or pass raw-strings through to the
% code-generator. The first is useful for annotating generated source,
% the second for inserting instrumention. I_raw should be side-effect
% free.
| '//' string :: :: comment
| C string :: :: raw
% Jib_compile.ml will represent all returns as assigments to the clexp
% CL_return, followed by end to signify the end of the
% function.
| return cval :: :: return
% For optimising away allocations and copying.
| reset ctyp name :: :: reset
| ctyp name = cval :: :: reinit
cdef :: 'CDEF_' ::=
| register id : ctyp = {
instr0 ; ... ; instrn
} :: :: reg_dec
| ctype_def :: :: type
% The first list of instructions sets up the global letbinding, while
% the second clears it.
| let nat ( id0 : ctyp0 , ... , idn : ctypn ) = {
instr0 ; ... ; instrm
} :: :: let
| val id = mstring ( ctyp0 , ... , ctypn ) -> ctyp :: :: spec
% If mid = Some id this indicates that the caller should allocate the
% return type and passes a pointer to it as an extra argument id for
% the function to fill in. This is only done via Jib->Jib rewrites
% used when compiling to C.
| function id mid ( id0 , ... , idn ) {
instr0 ; ... ; instrm
} :: :: fundef
% Each function can have custom global state. In CDEF_startup and
% CDEF_finish all I_decl and I_init nodes are treated as global and no
% nested-instructions (if/block) are allowed.
| startup id {
instr0 ; ... ; instrn
} :: :: startup
| finish id {
instr0 ; ... ; instrn
} :: :: finish
|
