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
|
open Ast
open Mapfold
open Static
open Static_utils
open Location
open Errors
(** Inlines all nodes with static paramaters. *)
let expect_bool env se =
let se = simplify env se in
match se.se_desc with
| SBool v -> v
| _ -> Format.eprintf "Expected a boolean@."; raise Error
let expect_int env se =
let se = simplify env se in
match se.se_desc with
| SInt v -> v
| _ -> Format.eprintf "Expected an integer@."; raise Error
let simplify_ty env ty = match ty with
| TBitArray se -> TBitArray (simplify env se)
| _ -> ty
(** Find a node by name*)
let nodes_list = ref []
let find_node f =
List.find (fun n -> f = n.n_name) !nodes_list
let vars_of_pat env pat =
let exp_of_ident id =
try
let ty = IdentEnv.find id env in
mk_exp ~ty:ty (Evar id)
with
| Not_found -> Format.eprintf "Not in env: %a@." Ident.print_ident id; assert false
in
let rec _vars_of_pat acc pat = match pat with
| Evarpat id -> (exp_of_ident id)::acc
| Etuplepat l -> List.fold_left (fun acc id -> (exp_of_ident id)::acc) acc l
in
_vars_of_pat [] pat
let ident_of_exp e = match e.e_desc with
| Evar x -> x
| _ -> assert false
let rename env vd =
let e = mk_exp ~ty:vd.v_ty (Evar (Ident.copy vd.v_ident)) in
IdentEnv.add vd.v_ident e env
let build_params m names values =
List.fold_left2 (fun m { p_name = n } v -> NameEnv.add n v m) m names values
let build_exp m vds values =
List.fold_left2 (fun m { v_ident = n } e -> IdentEnv.add n e m) m vds values
let build_env env vds =
List.fold_left (fun env vd -> IdentEnv.add vd.v_ident vd.v_ty env) env vds
let rec find_local_vars b = match b with
| BEqs (_, vds) -> vds
| BIf (_, trueb, falseb) -> (find_local_vars trueb) @ (find_local_vars falseb)
(** Substitutes idents with new names, static params with their values *)
let do_subst_block m subst b =
let translate_ident subst id =
try
ident_of_exp (IdentEnv.find id subst)
with
| Not_found -> id
in
let static_exp funs (subst, m) se =
simplify m se, (subst, m)
in
let exp funs (subst, m) e =
let e, _ = Mapfold.exp funs (subst, m) e in
match e.e_desc with
| Evar x ->
let e = if IdentEnv.mem x subst then IdentEnv.find x subst else e in
e, (subst, m)
| _ -> Mapfold.exp funs (subst, m) e
in
let pat funs (subst, m) pat = match pat with
| Evarpat id -> Evarpat (translate_ident subst id), (subst, m)
| Etuplepat ids -> Etuplepat (List.map (translate_ident subst) ids), (subst, m)
in
let var_dec funs (subst, m) vd =
(* iterate on the type *)
let vd, _ = Mapfold.var_dec funs (subst, m) vd in
{ vd with v_ident = translate_ident subst vd.v_ident }, (subst, m)
in
let funs =
{ Mapfold.defaults with static_exp = static_exp; exp = exp;
pat = pat; var_dec = var_dec }
in
let b, _ = Mapfold.block_it funs (subst, m) b in
b
let check_params loc m param_names params cl =
let env = build_params NameEnv.empty param_names params in
let cl = List.map (simplify env) cl in
try
check_true m cl
with Unsatisfiable(c) ->
Format.eprintf "%aThe following constraint is not satisfied: %a@."
print_location loc Printer.print_static_exp c;
raise Error
let rec inline_node loc env m call_stack f params args pat =
(* Check that the definition is sound *)
if List.mem (f, params) call_stack then (
Format.eprintf "The definition of %s is circular.@." f;
raise Error
);
let call_stack = (f, params)::call_stack in
(* do the actual work *)
let n = find_node f in
check_params loc m n.n_params params n.n_constraints;
let m = build_params m n.n_params params in
let subst = build_exp IdentEnv.empty n.n_inputs args in
let subst = build_exp subst n.n_outputs (List.rev (vars_of_pat env pat)) in
let locals = find_local_vars n.n_body in
let subst = List.fold_left rename subst locals in
let b = do_subst_block m subst n.n_body in
let b = Normalize.block b in
b, call_stack
and translate_eq env m subst call_stack (eqs, vds) ((pat, e) as eq) =
match e.e_desc with
(* Inline all nodes or only those with params or declared inline
if no_inline_all = true *)
| Ecall(f, params, args) ->
(try
let n = find_node f in
if not !Cli_options.no_inline_all
|| not (Misc.is_empty params)
|| n.n_inlined = Inlined then
let params = List.map (simplify m) params in
let b, call_stack = inline_node e.e_loc env m call_stack f params args pat in
let new_eqs, new_vds = translate_block env m subst call_stack b in
new_eqs@eqs, new_vds@vds
else
eq::eqs, vds
with
| Not_found -> eq::eqs, vds (* Predefined function*)
)
| _ -> eq::eqs, vds
and translate_eqs env m subst call_stack acc eqs =
List.fold_left (translate_eq env m subst call_stack) acc eqs
and translate_block env m subst call_stack b =
match b with
| BEqs (eqs, vds) ->
let vds = List.map (fun vd -> { vd with v_ty = simplify_ty m vd.v_ty }) vds in
let env = build_env env vds in
translate_eqs env m subst call_stack ([], vds) eqs
| BIf(se, trueb, elseb) ->
if expect_bool m se then
translate_block env m subst call_stack trueb
else
translate_block env m subst call_stack elseb
let node m n =
(*Init state*)
let call_stack = [(n.n_name, [])] in
(*Do the translation*)
let env = build_env IdentEnv.empty n.n_inputs in
let env = build_env env n.n_outputs in
let eqs, vds = translate_block env m IdentEnv.empty call_stack n.n_body in
{ n with n_body = BEqs (eqs, vds) }
let build_cd env cd =
NameEnv.add cd.c_name cd.c_value env
let program p =
nodes_list := p.p_nodes;
let m = List.fold_left build_cd NameEnv.empty p.p_consts in
if !Cli_options.no_inline_all then (
(* Find the nodes without static parameters *)
let nodes = List.filter (fun n -> Misc.is_empty n.n_params) p.p_nodes in
let nodes = List.map (fun n -> node m n) nodes in
{ p with p_nodes = nodes }
) else (
try
let n = List.find (fun n -> n.n_name = !Cli_options.main_node) p.p_nodes in
if n.n_params <> [] then (
Format.eprintf "The main node '%s' cannot have static parameters@." n.n_name;
raise Error
);
{ p with p_nodes = [node m n] }
with Not_found ->
Format.eprintf "Cannot find the main node '%s'@." !Cli_options.main_node;
raise Error
)
|
