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
|
indexvar n , m , i , j ::=
{{ phantom }}
{{ com Index variables for meta-lists }}
metavar nat ::=
{{ phantom }}
{{ ocaml int }}
{{ lem nat }}
metavar id ::=
{{ phantom }}
{{ ocaml id }}
{{ lem id }}
metavar mid ::=
{{ phantom }}
{{ ocaml id option }}
{{ lem maybe id }}
metavar string ::=
{{ phantom }}
{{ ocaml string }}
{{ lem string }}
metavar op ::=
{{ phantom }}
{{ ocaml string }}
{{ lem string }}
metavar bool ::=
{{ phantom }}
{{ ocaml bool }}
{{ lem bool }}
metavar value ::=
{{ phantom }}
{{ lem vl }}
{{ ocaml vl }}
embed
{{ lem
open import Ast
open import Value2
}}
grammar
% Fragments are small pure snippets of (abstract) C code, mostly
% expressions, used by the aval and cval types.
fragment :: 'F_' ::=
| id :: :: id
| '&' id :: :: ref
| value :: :: lit
| have_exception :: :: have_exception
| current_exception :: :: current_exception
| fragment op fragment' :: :: op
| op fragment :: :: unary
| string ( fragment0 , ... , fragmentn ) :: :: call
| fragment . string :: :: field
| string :: :: raw
| poly fragment :: :: poly
% init / clear -> create / kill
ctyp :: 'CT_' ::=
{{ com C type }}
| mpz_t :: :: int
% Arbitrary precision GMP integer, mpz_t in C.
| bv_t ( bool ) :: :: lbits
% Variable length bitvector - flag represents direction, true - dec or false - inc
| sbv_t ( bool ) :: :: sbits
% Small variable length bitvector - less than 64 bits
| 'uint64_t' ( nat , bool ) :: :: fbits
% Fixed length bitvector that fits within a 64-bit word. - int
% represents length, and flag is the same as CT_bv.
| 'int64_t' :: :: int64
% Used for (signed) integers that fit within 64-bits.
| unit_t :: :: unit
% unit is a value in sail, so we represent it as a one element type
% here too for clarity but we actually compile it to an int which is
% always 0.
| bool_t :: :: bool
| real_t :: :: real
| bit_t :: :: bit
% The real type in sail. Abstract here, but implemented using either
% GMP rationals or high-precision floating point.
| ( ctyp0 , ... , ctypn ) :: :: tup
| string_t :: :: string
| enum id ( id0 , ... , idn ) :: :: enum
| struct id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: struct
| variant id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: variant
% 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.
| vector ( bool , ctyp ) :: :: vector
| list ( ctyp ) :: :: list
% A vector type for non-bit vectors, and a list type.
| ref ( ctyp ) :: :: ref
| poly :: :: poly
cval :: 'CV_' ::=
{{ ocaml fragment * ctyp }}
{{ lem fragment * ctyp }}
clexp :: 'CL_' ::=
| id : ctyp :: :: id
| clexp . string :: :: field
| * clexp :: :: addr
| clexp . nat :: :: tuple
| current_exception : ctyp :: :: current_exception
| have_exception :: :: have_exception
ctype_def :: 'CTD_' ::=
{{ com C type definition }}
| enum id = id0 '|' ... '|' idn :: :: enum
| struct id = { id0 : ctyp0 , ... , idn : ctypn } :: :: struct
| variant id = { id0 : ctyp0 , ... , idn : ctypn } :: :: variant
iannot :: 'IA_' ::=
{{ lem nat * nat * nat }}
{{ ocaml int * int * int }}
instr :: 'I_' ::=
{{ aux _ iannot }}
| ctyp id :: :: decl
| ctyp id = cval :: :: init
| if ( cval ) { instr0 ; ... ; instrn }
else { instr0 ; ... ; instrm } : ctyp :: :: if
| jump ( cval ) string :: :: jump
| clexp = bool id ( cval0 , ... , cvaln ) :: :: funcall
| clexp = cval :: :: copy
| alias clexp = cval :: :: alias
| clear ctyp id :: :: clear
| return cval :: :: return
| { instr0 ; ... ; instrn } :: :: block
| try { instr0 ; ... ; instrn } :: :: try_block
| throw cval :: :: throw
| '//' string :: :: comment
| C string :: :: raw % only used for GCC attributes
| string : :: :: label
| goto string :: :: goto
| undefined ctyp :: :: undefined
| match_failure :: :: match_failure
% For optimising away allocations.
| reset ctyp id :: :: reset
| ctyp id = cval :: :: reinit
cdef :: 'CDEF_' ::=
| register id : ctyp = {
instr0 ; ... ; instrn
} :: :: reg_dec
| ctype_def :: :: type
| let nat ( id0 : ctyp0 , ... , idn : ctypn ) = {
instr0 ; ... ; instrm
} :: :: let
% The first list of instructions creates up the global letbinding, the
% second kills it.
| val id ( ctyp0 , ... , ctypn ) -> ctyp
:: :: spec
| function id mid ( id0 , ... , idn ) {
instr0 ; ... ; instrm
} :: :: fundef
| startup id {
instr0 ; ... ; instrn
} :: :: startup
| finish id {
instr0 ; ... ; instrn
} :: :: finish
|
