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
module Big_int = Nat_big_num
open Initial_check
open Ast
open Ast_defs
open Ast_util
let bitvec_typ size order = bitvector_typ (nconstant size) order
let fun_typschm arg_typs ret_typ = mk_typschm (mk_typquant []) (function_typ arg_typs ret_typ)
let index_of_nexp nexp =
match int_of_nexp_opt (nexp_simp nexp) with
| Some i -> i
| None -> raise (Reporting.err_typ (nexp_loc nexp) "non-constant bitfield index")
let mk_num_exp i = mk_lit_exp (L_num i)
let mk_id_exp id = mk_exp (E_id id)
let mk_id_pat id = mk_pat (P_id id)
let rec indices_of_range = function
| BF_aux (BF_single i, _) -> [(index_of_nexp i, index_of_nexp i)]
| BF_aux (BF_range (i, j), _) -> [(index_of_nexp i, index_of_nexp j)]
| BF_aux (BF_concat (l, r), _) -> indices_of_range l @ indices_of_range r
let slice_width (i, j) = Big_int.succ (Big_int.abs (Big_int.sub i j))
let range_width r = List.map slice_width (indices_of_range r) |> List.fold_left Big_int.add Big_int.zero
let constructor name order size =
let typschm = fun_typschm [bitvec_typ size order] (mk_id_typ name) in
let constructor_val = mk_val_spec (VS_val_spec (typschm, prepend_id "Mk_" name, None)) in
let constructor_fun = Printf.sprintf "function Mk_%s v = struct { bits = v }" (string_of_id name) in
constructor_val :: defs_of_string __POS__ constructor_fun
let get_field_exp range inner_exp =
let mk_slice (i, j) = mk_exp (E_vector_subrange (inner_exp, mk_num_exp i, mk_num_exp j)) in
let rec aux = function
| [e] -> e
| e :: es -> mk_exp (E_vector_append (e, aux es))
| [] -> assert false
in
aux (List.map mk_slice (indices_of_range range))
let construct_bitfield_struct _ exp = mk_exp (E_struct [mk_fexp (mk_id "bits") exp])
let construct_bitfield_exp name exp = mk_exp (E_app (prepend_id "Mk_" name, [exp]))
let set_field_lexp range inner_lexp =
let mk_slice (i, j) = mk_lexp (LE_vector_range (inner_lexp, mk_num_exp i, mk_num_exp j)) in
match List.map mk_slice (indices_of_range range) with [e] -> e | es -> mk_lexp (LE_vector_concat es)
let set_bits_field_lexp inner_lexp = mk_lexp (LE_field (inner_lexp, mk_id "bits"))
let get_bits_field exp = mk_exp (E_field (exp, mk_id "bits"))
let set_bits_field exp value = mk_exp (E_struct_update (exp, [mk_fexp (mk_id "bits") value]))
let update_field_exp range order inner_exp new_value =
let single = List.length (indices_of_range range) == 1 in
let rec aux e vi = function
| (i, j) :: is ->
let w = slice_width (i, j) in
let vi' = if is_order_inc order then Big_int.add vi w else Big_int.sub vi w in
let rhs =
if single then new_value
else begin
let vj = if is_order_inc order then Big_int.pred vi' else Big_int.succ vi' in
mk_exp (E_vector_subrange (new_value, mk_num_exp vi, mk_num_exp vj))
end
in
let update = mk_exp (E_vector_update_subrange (e, mk_num_exp i, mk_num_exp j, rhs)) in
aux update vi' is
| [] -> e
in
let vi = if is_order_inc order then Big_int.zero else Big_int.pred (range_width range) in
aux inner_exp vi (indices_of_range range)
type field_accessor_ids = { get : id; set : id; update : id; overload : id }
let field_accessor_ids type_name field =
let type_name = string_of_id type_name in
let field = string_of_id field in
{
get = mk_id (Printf.sprintf "_get_%s_%s" type_name field);
set = mk_id (Printf.sprintf "_set_%s_%s" type_name field);
update = mk_id (Printf.sprintf "_update_%s_%s" type_name field);
overload = mk_id (Printf.sprintf "_mod_%s" field);
}
let field_getter typ_name field order range =
let size = range_width range in
let typschm = fun_typschm [mk_id_typ typ_name] (bitvec_typ size order) in
let fun_id = (field_accessor_ids typ_name field).get in
let spec = mk_val_spec (VS_val_spec (typschm, fun_id, None)) in
let body = get_field_exp range (get_bits_field (mk_exp (E_id (mk_id "v")))) in
let funcl = mk_funcl fun_id (mk_pat (P_id (mk_id "v"))) body in
[spec; mk_fundef [funcl]]
let field_updater typ_name field order range =
let size = range_width range in
let typ = mk_id_typ typ_name in
let typschm = fun_typschm [typ; bitvec_typ size order] typ in
let fun_id = (field_accessor_ids typ_name field).update in
let spec = mk_val_spec (VS_val_spec (typschm, fun_id, None)) in
let orig_var = mk_id "v" in
let new_val_var = mk_id "x" in
let bits_exp = get_bits_field (mk_id_exp orig_var) in
let new_bits = update_field_exp range order bits_exp (mk_id_exp new_val_var) in
let body = set_bits_field (mk_id_exp orig_var) new_bits in
let funcl = mk_funcl fun_id (mk_pat (P_tuple [mk_id_pat orig_var; mk_id_pat new_val_var])) body in
let overload =
defs_of_string __POS__ (Printf.sprintf "overload update_%s = {%s}" (string_of_id field) (string_of_id fun_id))
in
[spec; mk_fundef [funcl]] @ overload
let register_field_setter typ_name field order range =
let size = range_width range in
let fun_id = string_of_id (field_accessor_ids typ_name field).set in
let update_fun_id = string_of_id (field_accessor_ids typ_name field).update in
let typ_name = string_of_id typ_name in
let field_typ = string_of_typ (bitvec_typ size order) in
let rfs_val = Printf.sprintf "val %s : (register(%s), %s) -> unit" fun_id typ_name field_typ in
let rfs_function =
String.concat "\n"
[
Printf.sprintf "function %s (r_ref, v) = {" fun_id;
" r = __deref(r_ref);";
Printf.sprintf " (*r_ref) = %s(r, v)" update_fun_id;
"}";
]
in
List.concat [defs_of_string __POS__ rfs_val; defs_of_string __POS__ rfs_function]
let field_overload name field =
let fun_id = string_of_id (field_accessor_ids name field).overload in
let get_id = string_of_id (field_accessor_ids name field).get in
let set_id = string_of_id (field_accessor_ids name field).set in
defs_of_string __POS__ (Printf.sprintf "overload %s = {%s, %s}" fun_id get_id set_id)
let field_accessors typ_name field order range =
List.concat
[
field_getter typ_name field order range;
field_updater typ_name field order range;
register_field_setter typ_name field order range;
field_overload typ_name field;
]
let macro id size order ranges =
let full_range = BF_aux (BF_range (nconstant (Big_int.pred size), nconstant Big_int.zero), Parse_ast.Unknown) in
let ranges = (mk_id "bits", full_range) :: Bindings.bindings ranges in
let accessors = List.map (fun (field, range) -> field_accessors id field order range) ranges in
List.concat ([constructor id order size] @ accessors)