blob: 0a32654d07f163510b755eac442cb968ac9771f1 (
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
|
module Big_int = Nat_big_num
open Initial_check
open Ast
open Ast_util
let bitvec size order =
Printf.sprintf "vector(%i, %s, bit)" size (string_of_order order)
let rec combine = function
| [] -> Defs []
| (Defs defs) :: ast ->
let (Defs defs') = combine ast in
Defs (defs @ defs')
let newtype name size order =
let nt = Printf.sprintf "newtype %s = Mk_%s : %s" name name (bitvec size order) in
ast_of_def_string order nt
let full_getter name size order =
let fg_val = Printf.sprintf "val _get_%s : %s -> %s" name name (bitvec size order) in
let fg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v" name name in
combine [ast_of_def_string order fg_val; ast_of_def_string order fg_function]
let full_setter name size order =
let fs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" name name (bitvec size order) in
let fs_function = String.concat "\n"
[ Printf.sprintf "function _set_%s (r_ref, v) = {" name;
" r = _reg_deref(r_ref);";
Printf.sprintf " r = Mk_%s(v);" name;
" (*r_ref) = r";
"}"
]
in
combine [ast_of_def_string order fs_val; ast_of_def_string order fs_function]
let full_overload name order =
ast_of_def_string order (Printf.sprintf "overload _mod_bits = {_get_%s, _set_%s}" name name)
let full_accessor name size order =
combine [full_getter name size order; full_setter name size order; full_overload name order]
let index_range_getter' name field order start stop =
let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
let irg_val = Printf.sprintf "val _get_%s : %s -> %s" field name (bitvec size order) in
let irg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v[%i .. %i]" field name start stop in
combine [ast_of_def_string order irg_val; ast_of_def_string order irg_function]
let index_range_setter' name field order start stop =
let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
let irs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" field name (bitvec size order) in
let irs_function = String.concat "\n"
[ Printf.sprintf "function _set_%s (r_ref, v) = {" field;
Printf.sprintf " r = _get_%s(_reg_deref(r_ref));" name;
Printf.sprintf " r[%i .. %i] = v;" start stop;
Printf.sprintf " (*r_ref) = Mk_%s(r)" name;
"}"
]
in
combine [ast_of_def_string order irs_val; ast_of_def_string order irs_function]
let index_range_overload field order =
ast_of_def_string order (Printf.sprintf "overload _mod_%s = {_get_%s, _set_%s}" field field field)
let index_range_accessor name field order (BF_aux (bf_aux, l)) =
let getter n m = index_range_getter' name field order (Big_int.to_int n) (Big_int.to_int m) in
let setter n m = index_range_setter' name field order (Big_int.to_int n) (Big_int.to_int m) in
let overload = index_range_overload field order in
match bf_aux with
| BF_single n -> combine [getter n n; setter n n; overload]
| BF_range (n, m) -> combine [getter n m; setter n m; overload]
| BF_concat _ -> failwith "Unimplemented"
let field_accessor name order (id, ir) = index_range_accessor name (string_of_id id) order ir
let macro id size order ranges =
let name = string_of_id id in
combine ([newtype name size order; full_accessor name size order] @ List.map (field_accessor name order) ranges)
|
