Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/machine_code.ml | ||
---|---|---|
23 | 23 |
|
24 | 24 |
(* Questions: |
25 | 25 |
|
26 |
- where are used the mconst. They contain initialization of |
|
27 |
constant in nodes. But they do not seem to be used by c_backend *) |
|
28 |
|
|
26 |
- where are used the mconst. They contain initialization of constant in |
|
27 |
nodes. But they do not seem to be used by c_backend *) |
|
29 | 28 |
|
30 | 29 |
(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *) |
31 | 30 |
(* the context contains m : state aka memory variables *) |
... | ... | |
34 | 33 |
(* d : local variables *) |
35 | 34 |
(* s : step instructions *) |
36 | 35 |
|
37 |
(* Machine processing requires knowledge about variables and local |
|
38 |
variables. Local could be memories while other could not. *) |
|
39 |
type machine_env = { |
|
40 |
is_local: string -> bool; |
|
41 |
get_var: string -> var_decl |
|
42 |
} |
|
43 |
|
|
36 |
(* Machine processing requires knowledge about variables and local variables. |
|
37 |
Local could be memories while other could not. *) |
|
38 |
type machine_env = { is_local : string -> bool; get_var : string -> var_decl } |
|
44 | 39 |
|
45 | 40 |
let build_env inputs locals outputs = |
46 | 41 |
let all = List.sort_uniq VDeclModule.compare (locals @ inputs @ outputs) in |
47 |
{ is_local = (fun id -> List.exists (fun v -> v.var_id = id) locals); |
|
48 |
get_var = (fun id -> try List.find (fun v -> v.var_id = id) all with Not_found -> |
|
49 |
(* Format.eprintf "Impossible to find variable %s in set %a@.@?" |
|
50 |
* id |
|
51 |
* VSet.pp all; *) |
|
52 |
raise Not_found) |
|
42 |
{ |
|
43 |
is_local = (fun id -> List.exists (fun v -> v.var_id = id) locals); |
|
44 |
get_var = |
|
45 |
(fun id -> |
|
46 |
try List.find (fun v -> v.var_id = id) all |
|
47 |
with Not_found -> |
|
48 |
(* Format.eprintf "Impossible to find variable %s in set %a@.@?" * id |
|
49 |
* VSet.pp all; *) |
|
50 |
raise Not_found); |
|
53 | 51 |
} |
54 | 52 |
|
55 |
|
|
56 |
|
|
57 | 53 |
(****************************************************************) |
58 |
(* Basic functions to translate to machine values, instructions *)
|
|
54 |
(* Basic functions to translate to machine values, instructions *) |
|
59 | 55 |
(****************************************************************) |
60 | 56 |
|
61 | 57 |
let translate_ident env id = |
... | ... | |
64 | 60 |
try |
65 | 61 |
let var_id = env.get_var id in |
66 | 62 |
vdecl_to_val var_id |
67 |
with Not_found -> |
|
68 |
|
|
69 |
(* id is a constant *) |
|
70 |
try |
|
71 |
let vdecl = (Corelang.var_decl_of_const |
|
72 |
(const_of_top (Hashtbl.find Corelang.consts_table id))) |
|
73 |
in |
|
74 |
vdecl_to_val vdecl |
|
75 |
with Not_found -> |
|
76 |
|
|
77 |
(* id is a tag, getting its type in the list of declared enums *) |
|
78 |
try |
|
79 |
id_to_tag id |
|
80 |
with Not_found -> |
|
81 |
Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id; |
|
82 |
assert false |
|
83 |
|
|
84 |
|
|
85 |
(* specialize predefined (polymorphic) operators wrt their instances, |
|
86 |
so that the C semantics is preserved *) |
|
63 |
with Not_found -> ( |
|
64 |
(* id is a constant *) |
|
65 |
try |
|
66 |
let vdecl = |
|
67 |
Corelang.var_decl_of_const |
|
68 |
(const_of_top (Hashtbl.find Corelang.consts_table id)) |
|
69 |
in |
|
70 |
vdecl_to_val vdecl |
|
71 |
with Not_found -> ( |
|
72 |
(* id is a tag, getting its type in the list of declared enums *) |
|
73 |
try id_to_tag id |
|
74 |
with Not_found -> |
|
75 |
Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id; |
|
76 |
assert false)) |
|
77 |
|
|
78 |
(* specialize predefined (polymorphic) operators wrt their instances, so that |
|
79 |
the C semantics is preserved *) |
|
87 | 80 |
let specialize_to_c expr = |
88 | 81 |
match expr.expr_desc with |
89 | 82 |
| Expr_appl (id, e, r) -> |
90 |
if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e)
|
|
91 |
then let id =
|
|
92 |
match id with
|
|
93 |
| "=" -> "equi"
|
|
94 |
| "!=" -> "xor"
|
|
95 |
| _ -> id in
|
|
83 |
if |
|
84 |
List.exists
|
|
85 |
(fun e -> Types.is_bool_type e.expr_type)
|
|
86 |
(expr_list_of_expr e)
|
|
87 |
then
|
|
88 |
let id = match id with "=" -> "equi" | "!=" -> "xor" | _ -> id in
|
|
96 | 89 |
{ expr with expr_desc = Expr_appl (id, e, r) } |
97 | 90 |
else expr |
98 |
| _ -> expr |
|
91 |
| _ -> |
|
92 |
expr |
|
99 | 93 |
|
100 | 94 |
let specialize_op expr = |
101 |
match !Options.output with |
|
102 |
| "C" -> specialize_to_c expr |
|
103 |
| _ -> expr |
|
95 |
match !Options.output with "C" -> specialize_to_c expr | _ -> expr |
|
104 | 96 |
|
105 | 97 |
let rec translate_expr env expr = |
106 | 98 |
let expr = specialize_op expr in |
107 | 99 |
let translate_expr = translate_expr env in |
108 |
let value_desc =
|
|
100 |
let value_desc = |
|
109 | 101 |
match expr.expr_desc with |
110 | 102 |
| Expr_const v -> |
111 | 103 |
Cst v |
... | ... | |
115 | 107 |
Array (List.map translate_expr el) |
116 | 108 |
| Expr_access (t, i) -> |
117 | 109 |
Access (translate_expr t, translate_expr (expr_of_dimension i)) |
118 |
| Expr_power (e, n) ->
|
|
110 |
| Expr_power (e, n) -> |
|
119 | 111 |
Power (translate_expr e, translate_expr (expr_of_dimension n)) |
120 | 112 |
| Expr_when (e1, _, _) -> |
121 | 113 |
(translate_expr e1).value_desc |
122 | 114 |
| Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr -> |
123 | 115 |
let nd = node_from_name id in |
124 | 116 |
Fun (node_name nd, List.map translate_expr (expr_list_of_expr e)) |
125 |
| Expr_ite (g,t,e) when Backends.is_functional () ->
|
|
126 |
(* special treatment depending on the active backend. For |
|
127 |
functional ones, like horn backend, ite are preserved in
|
|
128 |
expression. While they are removed for C or Java backends. *)
|
|
129 |
Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
|
|
117 |
| Expr_ite (g, t, e) when Backends.is_functional () ->
|
|
118 |
(* special treatment depending on the active backend. For functional ones,
|
|
119 |
like horn backend, ite are preserved in expression. While they are
|
|
120 |
removed for C or Java backends. *) |
|
121 |
Fun ("ite", [ translate_expr g; translate_expr t; translate_expr e ])
|
|
130 | 122 |
| _ -> |
131 |
Format.eprintf "Normalization error for backend %s: %a@." |
|
132 |
!Options.output |
|
123 |
Format.eprintf "Normalization error for backend %s: %a@." !Options.output |
|
133 | 124 |
Printers.pp_expr expr; |
134 | 125 |
raise NormalizationError |
135 | 126 |
in |
... | ... | |
137 | 128 |
|
138 | 129 |
let translate_guard env expr = |
139 | 130 |
match expr.expr_desc with |
140 |
| Expr_ident x -> translate_ident env x |
|
131 |
| Expr_ident x -> |
|
132 |
translate_ident env x |
|
141 | 133 |
| _ -> |
142 | 134 |
Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr; |
143 | 135 |
assert false |
... | ... | |
147 | 139 |
let translate_guard = translate_guard env in |
148 | 140 |
(* let translate_ident = translate_ident env in *) |
149 | 141 |
let translate_expr = translate_expr env in |
150 |
let lustre_eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
|
|
142 |
let lustre_eq = Corelang.mkeq Location.dummy_loc ([ y.var_id ], expr) in
|
|
151 | 143 |
match expr.expr_desc with |
152 | 144 |
| Expr_ite (c, t, e) -> |
153 | 145 |
let c = translate_guard c in |
154 | 146 |
let t, spec_t = translate_act (y, t) in |
155 | 147 |
let e, spec_e = translate_act (y, e) in |
156 |
mk_conditional ~lustre_eq c [t] [e], |
|
157 |
mk_conditional_tr c spec_t spec_e |
|
148 |
mk_conditional ~lustre_eq c [ t ] [ e ], mk_conditional_tr c spec_t spec_e |
|
158 | 149 |
| Expr_merge (x, hl) -> |
159 | 150 |
let var_x = env.get_var x in |
160 |
let hl, spec_hl = List.(split (map (fun (t, h) -> |
|
161 |
let h, spec_h = translate_act (y, h) in |
|
162 |
(t, [h]), (t, spec_h)) |
|
163 |
hl)) in |
|
164 |
mk_branch' ~lustre_eq var_x hl, |
|
165 |
mk_branch_tr var_x spec_hl |
|
151 |
let hl, spec_hl = |
|
152 |
List.( |
|
153 |
split |
|
154 |
(map |
|
155 |
(fun (t, h) -> |
|
156 |
let h, spec_h = translate_act (y, h) in |
|
157 |
(t, [ h ]), (t, spec_h)) |
|
158 |
hl)) |
|
159 |
in |
|
160 |
mk_branch' ~lustre_eq var_x hl, mk_branch_tr var_x spec_hl |
|
166 | 161 |
| _ -> |
167 | 162 |
let e = translate_expr expr in |
168 |
mk_assign ~lustre_eq y e, |
|
169 |
mk_assign_tr y e |
|
163 |
mk_assign ~lustre_eq y e, mk_assign_tr y e |
|
170 | 164 |
|
171 |
let get_memory env mems eq = match eq.eq_lhs, eq.eq_rhs.expr_desc with |
|
172 |
| ([x], Expr_pre _ | [x], Expr_fby _) when env.is_local x -> |
|
165 |
let get_memory env mems eq = |
|
166 |
match eq.eq_lhs, eq.eq_rhs.expr_desc with |
|
167 |
| ([ x ], Expr_pre _ | [ x ], Expr_fby _) when env.is_local x -> |
|
173 | 168 |
let var_x = env.get_var x in |
174 | 169 |
VSet.add var_x mems |
175 |
| _ -> mems |
|
170 |
| _ -> |
|
171 |
mems |
|
176 | 172 |
|
177 |
let get_memories env = |
|
178 |
List.fold_left (get_memory env) VSet.empty |
|
173 |
let get_memories env = List.fold_left (get_memory env) VSet.empty |
|
179 | 174 |
|
180 | 175 |
(* Datastructure updated while visiting equations *) |
181 | 176 |
type machine_ctx = { |
182 | 177 |
(* memories *) |
183 |
m: ISet.t; |
|
178 |
m : ISet.t;
|
|
184 | 179 |
(* Reset instructions *) |
185 |
si: instr_t list; |
|
180 |
si : instr_t list;
|
|
186 | 181 |
(* Instances *) |
187 |
j: (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t; |
|
182 |
j : (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t;
|
|
188 | 183 |
(* Step instructions *) |
189 |
s: instr_t list; |
|
184 |
s : instr_t list;
|
|
190 | 185 |
(* Memory pack spec *) |
191 |
mp: mc_formula_t list; |
|
186 |
mp : mc_formula_t list;
|
|
192 | 187 |
(* Transition spec *) |
193 |
t: (var_decl list (* inputs *) |
|
194 |
* var_decl list (* locals *) |
|
195 |
* var_decl list (* outputs *) |
|
196 |
* ISet.t (* memory footprint *) |
|
197 |
* mc_formula_t (* formula *) |
|
198 |
) list; |
|
188 |
t : |
|
189 |
(var_decl list |
|
190 |
(* inputs *) |
|
191 |
* var_decl list |
|
192 |
(* locals *) |
|
193 |
* var_decl list |
|
194 |
(* outputs *) |
|
195 |
* ISet.t (* memory footprint *) |
|
196 |
* mc_formula_t) |
|
197 |
(* formula *) |
|
198 |
list; |
|
199 | 199 |
} |
200 | 200 |
|
201 |
let ctx_init = { |
|
202 |
m = ISet.empty; |
|
203 |
si = []; |
|
204 |
j = IMap.empty; |
|
205 |
s = []; |
|
206 |
mp = []; |
|
207 |
t = [] |
|
208 |
} |
|
201 |
let ctx_init = |
|
202 |
{ m = ISet.empty; si = []; j = IMap.empty; s = []; mp = []; t = [] } |
|
209 | 203 |
|
210 | 204 |
(****************************************************************) |
211 |
(* Main function to translate equations into this machine context we |
|
212 |
are building *)
|
|
205 |
(* Main function to translate equations into this machine context we are
|
|
206 |
building *)
|
|
213 | 207 |
(****************************************************************) |
214 | 208 |
|
215 |
let mk_control v l inst = |
|
216 |
mkinstr |
|
217 |
(MBranch (vdecl_to_val v, [l, [inst]])) |
|
209 |
let mk_control v l inst = mkinstr (MBranch (vdecl_to_val v, [ l, [ inst ] ])) |
|
218 | 210 |
|
219 | 211 |
let control_on_clock env ck inst = |
220 |
let rec aux (fspec, inst as acc) ck =
|
|
212 |
let rec aux ((fspec, inst) as acc) ck =
|
|
221 | 213 |
match (Clocks.repr ck).cdesc with |
222 | 214 |
| Con (ck, cr, l) -> |
223 | 215 |
let id = Clocks.const_of_carrier cr in |
224 | 216 |
let v = env.get_var id in |
225 |
aux ((fun spec -> Imply (Equal (Var v, Tag l), fspec spec)), |
|
226 |
mk_control v l inst) |
|
217 |
aux |
|
218 |
( (fun spec -> Imply (Equal (Var v, Tag l), fspec spec)), |
|
219 |
mk_control v l inst ) |
|
227 | 220 |
ck |
228 |
| _ -> acc |
|
221 |
| _ -> |
|
222 |
acc |
|
229 | 223 |
in |
230 | 224 |
let fspec, inst = aux ((fun spec -> spec), inst) ck in |
231 | 225 |
fspec, inst |
... | ... | |
234 | 228 |
match r with |
235 | 229 |
| Some r -> |
236 | 230 |
let r = translate_guard env r in |
237 |
let _, inst = control_on_clock env c |
|
238 |
(mk_conditional |
|
239 |
r |
|
240 |
[mkinstr (MSetReset i)] |
|
241 |
[mkinstr (MNoReset i)]) in |
|
231 |
let _, inst = |
|
232 |
control_on_clock env c |
|
233 |
(mk_conditional r [ mkinstr (MSetReset i) ] [ mkinstr (MNoReset i) ]) |
|
234 |
in |
|
242 | 235 |
Some r, [ inst ] |
243 |
| None -> None, [] |
|
236 |
| None -> |
|
237 |
None, [] |
|
244 | 238 |
|
245 | 239 |
let translate_eq env ctx id inputs locals outputs i eq = |
246 | 240 |
let translate_expr = translate_expr env in |
247 | 241 |
let translate_act = translate_act env in |
248 |
let locals_pi = Lustre_live.inter_live_i_with id (i-1) locals in
|
|
249 |
let outputs_pi = Lustre_live.inter_live_i_with id (i-1) outputs in
|
|
242 |
let locals_pi = Lustre_live.inter_live_i_with id (i - 1) locals in
|
|
243 |
let outputs_pi = Lustre_live.inter_live_i_with id (i - 1) outputs in
|
|
250 | 244 |
let locals_i = Lustre_live.inter_live_i_with id i locals in |
251 | 245 |
let outputs_i = Lustre_live.inter_live_i_with id i outputs in |
252 |
let pred_mp ctx a = |
|
253 |
And [mk_memory_pack ~i:(i-1) id; a] :: ctx.mp in |
|
246 |
let pred_mp ctx a = And [ mk_memory_pack ~i:(i - 1) id; a ] :: ctx.mp in |
|
254 | 247 |
let pred_t ctx a = |
255 |
(inputs, locals_i, outputs_i, ctx.m, |
|
256 |
Exists |
|
257 |
(Lustre_live.existential_vars id i eq (locals @ outputs), |
|
258 |
And [ |
|
259 |
mk_transition ~i:(i-1) id |
|
260 |
(vdecls_to_vals inputs) |
|
261 |
(vdecls_to_vals locals_pi) |
|
262 |
(vdecls_to_vals outputs_pi); |
|
263 |
a |
|
264 |
])) |
|
265 |
:: ctx.t in |
|
248 |
( inputs, |
|
249 |
locals_i, |
|
250 |
outputs_i, |
|
251 |
ctx.m, |
|
252 |
Exists |
|
253 |
( Lustre_live.existential_vars id i eq (locals @ outputs), |
|
254 |
And |
|
255 |
[ |
|
256 |
mk_transition ~i:(i - 1) id (vdecls_to_vals inputs) |
|
257 |
(vdecls_to_vals locals_pi) |
|
258 |
(vdecls_to_vals outputs_pi); |
|
259 |
a; |
|
260 |
] ) ) |
|
261 |
:: ctx.t |
|
262 |
in |
|
266 | 263 |
let control_on_clock ck inst spec_mp spec_t ctx = |
267 | 264 |
let fspec, inst = control_on_clock env ck inst in |
268 |
{ ctx with |
|
269 |
s = { inst with |
|
270 |
instr_spec = [ |
|
265 |
{ |
|
266 |
ctx with |
|
267 |
s = |
|
268 |
{ |
|
269 |
inst with |
|
270 |
instr_spec = |
|
271 |
[ |
|
271 | 272 |
mk_memory_pack ~i id; |
272 |
mk_transition ~i id |
|
273 |
(vdecls_to_vals inputs) |
|
274 |
(vdecls_to_vals locals_i) |
|
275 |
(vdecls_to_vals outputs_i) |
|
276 |
] } |
|
277 |
:: ctx.s; |
|
273 |
mk_transition ~i id (vdecls_to_vals inputs) |
|
274 |
(vdecls_to_vals locals_i) (vdecls_to_vals outputs_i); |
|
275 |
]; |
|
276 |
} |
|
277 |
:: ctx.s; |
|
278 | 278 |
mp = pred_mp ctx spec_mp; |
279 | 279 |
t = pred_t ctx (fspec spec_t); |
280 | 280 |
} |
281 | 281 |
in |
282 | 282 |
let reset_instance = reset_instance env in |
283 | 283 |
let mkinstr' = mkinstr ~lustre_eq:eq in |
284 |
let ctl ?(ck=eq.eq_rhs.expr_clock) instr = |
|
285 |
control_on_clock ck (mkinstr' instr) in |
|
284 |
let ctl ?(ck = eq.eq_rhs.expr_clock) instr = |
|
285 |
control_on_clock ck (mkinstr' instr) |
|
286 |
in |
|
286 | 287 |
|
287 |
(* Format.eprintf "translate_eq %a with clock %a@." |
|
288 |
Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
|
|
288 |
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq
|
|
289 |
Clocks.print_ck eq.eq_rhs.expr_clock; *)
|
|
289 | 290 |
match eq.eq_lhs, eq.eq_rhs.expr_desc with |
290 |
| [x], Expr_arrow (e1, e2) ->
|
|
291 |
| [ x ], Expr_arrow (e1, e2) ->
|
|
291 | 292 |
let var_x = env.get_var x in |
292 | 293 |
let td = Arrow.arrow_top_decl () in |
293 | 294 |
let inst = new_instance td eq.eq_rhs.expr_tag in |
... | ... | |
295 | 296 |
let c2 = translate_expr e2 in |
296 | 297 |
assert (c1.value_desc = Cst (Const_tag "true")); |
297 | 298 |
assert (c2.value_desc = Cst (Const_tag "false")); |
298 |
let ctx = ctl |
|
299 |
(MStep ([var_x], inst, [c1; c2])) |
|
299 |
let ctx = |
|
300 |
ctl |
|
301 |
(MStep ([ var_x ], inst, [ c1; c2 ])) |
|
300 | 302 |
(mk_memory_pack ~inst (node_name td)) |
301 |
(mk_transition ~inst (node_name td) [] [] [vdecl_to_val var_x])
|
|
303 |
(mk_transition ~inst (node_name td) [] [] [ vdecl_to_val var_x ])
|
|
302 | 304 |
ctx |
303 | 305 |
in |
304 |
{ ctx with |
|
306 |
{ |
|
307 |
ctx with |
|
305 | 308 |
si = mkinstr (MSetReset inst) :: ctx.si; |
306 | 309 |
j = IMap.add inst (td, []) ctx.j; |
307 | 310 |
} |
308 |
|
|
309 |
| [x], Expr_pre e when env.is_local x -> |
|
311 |
| [ x ], Expr_pre e when env.is_local x -> |
|
310 | 312 |
let var_x = env.get_var x in |
311 | 313 |
let e = translate_expr e in |
312 | 314 |
ctl |
... | ... | |
314 | 316 |
(mk_state_variable_pack var_x) |
315 | 317 |
(mk_state_assign_tr var_x e) |
316 | 318 |
{ ctx with m = ISet.add x ctx.m } |
317 |
|
|
318 |
| [x], Expr_fby (e1, e2) when env.is_local x -> |
|
319 |
| [ x ], Expr_fby (e1, e2) when env.is_local x -> |
|
319 | 320 |
let var_x = env.get_var x in |
320 | 321 |
let e2 = translate_expr e2 in |
321 |
let ctx = ctl |
|
322 |
let ctx = |
|
323 |
ctl |
|
322 | 324 |
(MStateAssign (var_x, e2)) |
323 | 325 |
(mk_state_variable_pack var_x) |
324 | 326 |
(mk_state_assign_tr var_x e2) |
325 | 327 |
{ ctx with m = ISet.add x ctx.m } |
326 | 328 |
in |
327 |
{ ctx with |
|
329 |
{ |
|
330 |
ctx with |
|
328 | 331 |
si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si; |
329 | 332 |
} |
330 |
|
|
331 | 333 |
| p, Expr_appl (f, arg, r) |
332 | 334 |
when not (Basic_library.is_expr_internal_fun eq.eq_rhs) -> |
333 | 335 |
let var_p = List.map (fun v -> env.get_var v) p in |
... | ... | |
336 | 338 |
let node_f = node_from_name f in |
337 | 339 |
let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in |
338 | 340 |
let inst = new_instance node_f eq.eq_rhs.expr_tag in |
339 |
let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) |
|
340 |
el [eq.eq_rhs.expr_clock] in |
|
341 |
let call_ck = Clock_calculus.compute_root_clock |
|
342 |
(Clock_predef.ck_tuple env_cks) in |
|
341 |
let env_cks = |
|
342 |
List.fold_right |
|
343 |
(fun arg cks -> arg.expr_clock :: cks) |
|
344 |
el [ eq.eq_rhs.expr_clock ] |
|
345 |
in |
|
346 |
let call_ck = |
|
347 |
Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) |
|
348 |
in |
|
343 | 349 |
let r, reset_inst = reset_instance inst r call_ck in |
344 |
let ctx = ctl
|
|
345 |
~ck:call_ck
|
|
350 |
let ctx = |
|
351 |
ctl ~ck:call_ck
|
|
346 | 352 |
(MStep (var_p, inst, vl)) |
347 | 353 |
(mk_memory_pack ~inst (node_name node_f)) |
348 | 354 |
(mk_transition ?r ~inst (node_name node_f) vl [] (vdecls_to_vals var_p)) |
349 | 355 |
ctx |
350 | 356 |
in |
351 |
(*Clocks.new_var true in |
|
352 |
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; |
|
353 |
Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*) |
|
354 |
{ ctx with |
|
355 |
si = if Stateless.check_node node_f |
|
356 |
then ctx.si else mkinstr (MSetReset inst) :: ctx.si; |
|
357 |
(*Clocks.new_var true in Clock_calculus.unify_imported_clock (Some call_ck) |
|
358 |
eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; Format.eprintf "call %a: %a: |
|
359 |
%a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple |
|
360 |
env_cks) Clocks.print_ck call_ck;*) |
|
361 |
{ |
|
362 |
ctx with |
|
363 |
si = |
|
364 |
(if Stateless.check_node node_f then ctx.si |
|
365 |
else mkinstr (MSetReset inst) :: ctx.si); |
|
357 | 366 |
j = IMap.add inst call_f ctx.j; |
358 |
s = (if Stateless.check_node node_f then [] else reset_inst) |
|
359 |
@ ctx.s; |
|
367 |
s = (if Stateless.check_node node_f then [] else reset_inst) @ ctx.s; |
|
360 | 368 |
} |
361 |
|
|
362 |
| [x], _ -> |
|
369 |
| [ x ], _ -> |
|
363 | 370 |
let var_x = env.get_var x in |
364 | 371 |
let instr, spec = translate_act (var_x, eq.eq_rhs) in |
365 | 372 |
control_on_clock eq.eq_rhs.expr_clock instr True spec ctx |
366 |
|
|
367 | 373 |
| _ -> |
368 | 374 |
Format.eprintf "internal error: Machine_code.translate_eq %a@?" |
369 | 375 |
Printers.pp_node_eq eq; |
370 | 376 |
assert false |
371 | 377 |
|
372 | 378 |
let constant_equations locals = |
373 |
List.fold_left (fun eqs vdecl -> |
|
374 |
if vdecl.var_dec_const |
|
375 |
then |
|
376 |
{ eq_lhs = [vdecl.var_id]; |
|
379 |
List.fold_left |
|
380 |
(fun eqs vdecl -> |
|
381 |
if vdecl.var_dec_const then |
|
382 |
{ |
|
383 |
eq_lhs = [ vdecl.var_id ]; |
|
377 | 384 |
eq_rhs = desome vdecl.var_dec_value; |
378 |
eq_loc = vdecl.var_loc |
|
379 |
} :: eqs |
|
385 |
eq_loc = vdecl.var_loc; |
|
386 |
} |
|
387 |
:: eqs |
|
380 | 388 |
else eqs) |
381 | 389 |
[] locals |
382 | 390 |
|
383 | 391 |
let translate_eqs env ctx id inputs locals outputs eqs = |
384 |
List.fold_left (fun (ctx, i) eq -> |
|
392 |
List.fold_left |
|
393 |
(fun (ctx, i) eq -> |
|
385 | 394 |
let ctx = translate_eq env ctx id inputs locals outputs i eq in |
386 | 395 |
ctx, i + 1) |
387 | 396 |
(ctx, 1) eqs |
388 | 397 |
|> fst |
389 | 398 |
|
390 |
|
|
391 | 399 |
(****************************************************************) |
392 |
(* Processing nodes *)
|
|
400 |
(* Processing nodes *) |
|
393 | 401 |
(****************************************************************) |
394 | 402 |
|
395 | 403 |
let process_asserts nd = |
396 |
|
|
397 |
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in |
|
398 |
if Backends.is_functional () then |
|
399 |
[], [], exprl |
|
400 |
else (* Each assert(e) is associated to a fresh variable v and declared as |
|
401 |
v=e; assert (v); *) |
|
404 |
let exprl = List.map (fun assert_ -> assert_.assert_expr) nd.node_asserts in |
|
405 |
if Backends.is_functional () then [], [], exprl |
|
406 |
else |
|
407 |
(* Each assert(e) is associated to a fresh variable v and declared as v=e; |
|
408 |
assert (v); *) |
|
402 | 409 |
let _, vars, eql, assertl = |
403 |
List.fold_left (fun (i, vars, eqlist, assertlist) expr -> |
|
410 |
List.fold_left |
|
411 |
(fun (i, vars, eqlist, assertlist) expr -> |
|
404 | 412 |
let loc = expr.expr_loc in |
405 | 413 |
let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in |
406 | 414 |
let assert_var = |
407 |
mkvar_decl |
|
408 |
loc
|
|
409 |
~orig:false (* fresh var *)
|
|
410 |
(var_id,
|
|
411 |
mktyp loc Tydec_bool,
|
|
412 |
mkclock loc Ckdec_any,
|
|
413 |
false, (* not a constant *)
|
|
414 |
None, (* no default value *)
|
|
415 |
Some nd.node_id
|
|
416 |
) |
|
415 |
mkvar_decl loc ~orig:false
|
|
416 |
(* fresh var *)
|
|
417 |
( var_id,
|
|
418 |
mktyp loc Tydec_bool,
|
|
419 |
mkclock loc Ckdec_any,
|
|
420 |
false,
|
|
421 |
(* not a constant *) |
|
422 |
None,
|
|
423 |
(* no default value *)
|
|
424 |
Some nd.node_id )
|
|
417 | 425 |
in |
418 |
assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *); |
|
419 |
let eq = mkeq loc ([var_id], expr) in |
|
420 |
(i+1, |
|
421 |
assert_var::vars, |
|
422 |
eq::eqlist, |
|
423 |
{expr with expr_desc = Expr_ident var_id}::assertlist) |
|
424 |
) (1, [], [], []) exprl |
|
426 |
assert_var.var_type <- Type_predef.type_bool |
|
427 |
(* Types.new_ty (Types.Tbool) *); |
|
428 |
let eq = mkeq loc ([ var_id ], expr) in |
|
429 |
( i + 1, |
|
430 |
assert_var :: vars, |
|
431 |
eq :: eqlist, |
|
432 |
{ expr with expr_desc = Expr_ident var_id } :: assertlist )) |
|
433 |
(1, [], [], []) exprl |
|
425 | 434 |
in |
426 | 435 |
vars, eql, assertl |
427 | 436 |
|
428 | 437 |
let translate_core env nid sorted_eqs inputs locals outputs = |
429 | 438 |
let constant_eqs = constant_equations locals in |
430 | 439 |
|
431 |
(* Compute constants' instructions *) |
|
432 |
let ctx0 = translate_eqs env ctx_init nid inputs locals outputs constant_eqs in |
|
440 |
(* Compute constants' instructions *) |
|
441 |
let ctx0 = |
|
442 |
translate_eqs env ctx_init nid inputs locals outputs constant_eqs |
|
443 |
in |
|
433 | 444 |
assert (ctx0.si = []); |
434 | 445 |
assert (IMap.is_empty ctx0.j); |
435 | 446 |
|
... | ... | |
444 | 455 |
{ |
445 | 456 |
mpname = nd; |
446 | 457 |
mpindex = Some 0; |
447 |
mpformula = And [StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero)] |
|
458 |
mpformula = |
|
459 |
And [ StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero) ]; |
|
448 | 460 |
} |
449 | 461 |
|
450 | 462 |
let memory_pack_toplevel nd i = |
451 | 463 |
{ |
452 | 464 |
mpname = nd; |
453 | 465 |
mpindex = None; |
454 |
mpformula = Ternary (Memory ResetFlag,
|
|
455 |
StateVarPack ResetFlag,
|
|
456 |
mk_memory_pack ~i nd.node_id)
|
|
466 |
mpformula = |
|
467 |
Ternary
|
|
468 |
(Memory ResetFlag, StateVarPack ResetFlag, mk_memory_pack ~i nd.node_id);
|
|
457 | 469 |
} |
458 | 470 |
|
459 | 471 |
let transition_0 nd = |
... | ... | |
464 | 476 |
tlocals = []; |
465 | 477 |
toutputs = []; |
466 | 478 |
tformula = True; |
467 |
tfootprint = ISet.empty |
|
479 |
tfootprint = ISet.empty;
|
|
468 | 480 |
} |
469 | 481 |
|
470 | 482 |
let transition_toplevel nd i = |
... | ... | |
474 | 486 |
tinputs = nd.node_inputs; |
475 | 487 |
tlocals = []; |
476 | 488 |
toutputs = nd.node_outputs; |
477 |
tformula = ExistsMem (nd.node_id, |
|
478 |
Predicate (ResetCleared nd.node_id), |
|
479 |
mk_transition nd.node_id ~i |
|
480 |
(vdecls_to_vals (nd.node_inputs)) |
|
481 |
[] |
|
482 |
(vdecls_to_vals nd.node_outputs)); |
|
489 |
tformula = |
|
490 |
ExistsMem |
|
491 |
( nd.node_id, |
|
492 |
Predicate (ResetCleared nd.node_id), |
|
493 |
mk_transition nd.node_id ~i |
|
494 |
(vdecls_to_vals nd.node_inputs) |
|
495 |
[] |
|
496 |
(vdecls_to_vals nd.node_outputs) ); |
|
483 | 497 |
tfootprint = ISet.empty; |
484 | 498 |
} |
485 | 499 |
|
... | ... | |
487 | 501 |
(* Format.eprintf "Translating node %s@." nd.node_id; *) |
488 | 502 |
(* Extracting eqs, variables .. *) |
489 | 503 |
let eqs, auts = get_node_eqs nd in |
490 |
assert (auts = []); (* Automata should be expanded by now *) |
|
504 |
assert (auts = []); |
|
505 |
|
|
506 |
(* Automata should be expanded by now *) |
|
491 | 507 |
|
492 | 508 |
(* In case of non functional backend (eg. C), additional local variables have |
493 | 509 |
to be declared for each assert *) |
... | ... | |
505 | 521 |
(* Format.eprintf "ok1@.@?"; *) |
506 | 522 |
let schedule = sch.Scheduling_type.schedule in |
507 | 523 |
(* Format.eprintf "ok2@.@?"; *) |
508 |
let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in |
|
524 |
let sorted_eqs, unused = |
|
525 |
Scheduling.sort_equations_from_schedule eqs schedule |
|
526 |
in |
|
527 |
|
|
509 | 528 |
(* Format.eprintf "ok3@.locals=%a@.inout:%a@?" |
510 | 529 |
* VSet.pp locals |
511 | 530 |
* VSet.pp inout_vars |
512 | 531 |
* ; *) |
513 |
|
|
514 | 532 |
let equations = assert_instrs @ sorted_eqs in |
515 | 533 |
let mems = get_memories env equations in |
516 | 534 |
(* Removing computed memories from locals. We also removed unused variables. *) |
517 |
let locals = List.filter |
|
518 |
(fun v -> not (VSet.mem v mems) && not (List.mem v.var_id unused)) locals in |
|
535 |
let locals = |
|
536 |
List.filter |
|
537 |
(fun v -> (not (VSet.mem v mems)) && not (List.mem v.var_id unused)) |
|
538 |
locals |
|
539 |
in |
|
519 | 540 |
(* Compute live sets for spec *) |
520 | 541 |
Lustre_live.set_live_of nd.node_id nd.node_outputs locals equations; |
521 | 542 |
|
522 | 543 |
(* Translate equations *) |
523 |
let ctx, ctx0_s = translate_core env nd.node_id equations |
|
524 |
nd.node_inputs locals nd.node_outputs in |
|
544 |
let ctx, ctx0_s = |
|
545 |
translate_core env nd.node_id equations nd.node_inputs locals |
|
546 |
nd.node_outputs |
|
547 |
in |
|
525 | 548 |
|
526 | 549 |
(* Format.eprintf "ok4@.@?"; *) |
527 | 550 |
|
... | ... | |
529 | 552 |
let mmap = IMap.bindings ctx.j in |
530 | 553 |
let mmemory_packs = |
531 | 554 |
memory_pack_0 nd |
532 |
:: List.mapi (fun i f -> |
|
533 |
{ |
|
534 |
mpname = nd; |
|
535 |
mpindex = Some (i + 1); |
|
536 |
mpformula = red f |
|
537 |
}) (List.rev ctx.mp) |
|
538 |
@ [memory_pack_toplevel nd (List.length ctx.mp)] |
|
555 |
:: |
|
556 |
List.mapi |
|
557 |
(fun i f -> { mpname = nd; mpindex = Some (i + 1); mpformula = red f }) |
|
558 |
(List.rev ctx.mp) |
|
559 |
@ [ memory_pack_toplevel nd (List.length ctx.mp) ] |
|
539 | 560 |
in |
540 | 561 |
let mtransitions = |
541 | 562 |
transition_0 nd |
542 |
:: List.mapi (fun i (tinputs, tlocals, toutputs, tfootprint, f) -> |
|
563 |
:: |
|
564 |
List.mapi |
|
565 |
(fun i (tinputs, tlocals, toutputs, tfootprint, f) -> |
|
543 | 566 |
{ |
544 | 567 |
tname = nd; |
545 | 568 |
tindex = Some (i + 1); |
... | ... | |
547 | 570 |
tlocals; |
548 | 571 |
toutputs; |
549 | 572 |
tformula = red f; |
550 |
tfootprint |
|
551 |
}) (List.rev ctx.t) |
|
552 |
@ [transition_toplevel nd (List.length ctx.t)] |
|
573 |
tfootprint; |
|
574 |
}) |
|
575 |
(List.rev ctx.t) |
|
576 |
@ [ transition_toplevel nd (List.length ctx.t) ] |
|
577 |
in |
|
578 |
let clear_reset = |
|
579 |
mkinstr |
|
580 |
~instr_spec: |
|
581 |
[ |
|
582 |
mk_memory_pack ~i:0 nd.node_id; |
|
583 |
mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] []; |
|
584 |
] |
|
585 |
MClearReset |
|
553 | 586 |
in |
554 |
let clear_reset = mkinstr ~instr_spec:[ |
|
555 |
mk_memory_pack ~i:0 nd.node_id; |
|
556 |
mk_transition ~i:0 nd.node_id |
|
557 |
(vdecls_to_vals nd.node_inputs) |
|
558 |
[] |
|
559 |
[]] MClearReset in |
|
560 | 587 |
{ |
561 | 588 |
mname = nd; |
562 | 589 |
mmemory = VSet.elements mems; |
563 | 590 |
mcalls = mmap; |
564 |
minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap; |
|
591 |
minstances = |
|
592 |
List.filter (fun (_, (n, _)) -> not (Stateless.check_node n)) mmap; |
|
565 | 593 |
minit = List.rev ctx.si; |
566 | 594 |
mconst = List.rev ctx0_s; |
567 | 595 |
mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs; |
568 |
mstep = {
|
|
569 |
step_inputs = nd.node_inputs;
|
|
570 |
step_outputs = nd.node_outputs;
|
|
571 |
step_locals = locals;
|
|
572 |
step_checks = List.map (fun d -> d.Dimension.dim_loc,
|
|
573 |
translate_expr env
|
|
574 |
(expr_of_dimension d))
|
|
575 |
nd.node_checks;
|
|
576 |
step_instrs = clear_reset ::
|
|
577 |
(* special treatment depending on the active backend. For horn backend,
|
|
578 |
common branches are not merged while they are in C or Java
|
|
579 |
backends. *)
|
|
580 |
(if !Backends.join_guards then
|
|
581 |
join_guards_list (List.rev ctx.s)
|
|
582 |
else
|
|
583 |
List.rev ctx.s);
|
|
584 |
step_asserts = List.map (translate_expr env) nd_node_asserts;
|
|
585 |
};
|
|
586 |
|
|
587 |
(* Processing spec: there is no processing performed here. Contract
|
|
588 |
have been processed already. Either one of the other machine is a
|
|
589 |
cocospec node, or the current one is a cocospec node. Contract do
|
|
590 |
not contain any statement or import. *)
|
|
591 |
|
|
596 |
mstep = |
|
597 |
{
|
|
598 |
step_inputs = nd.node_inputs;
|
|
599 |
step_outputs = nd.node_outputs;
|
|
600 |
step_locals = locals;
|
|
601 |
step_checks =
|
|
602 |
List.map
|
|
603 |
(fun d ->
|
|
604 |
d.Dimension.dim_loc, translate_expr env (expr_of_dimension d))
|
|
605 |
nd.node_checks;
|
|
606 |
step_instrs =
|
|
607 |
clear_reset
|
|
608 |
::
|
|
609 |
(* special treatment depending on the active backend. For horn
|
|
610 |
backend, common branches are not merged while they are in C or Java
|
|
611 |
backends. *)
|
|
612 |
(if !Backends.join_guards then join_guards_list (List.rev ctx.s)
|
|
613 |
else List.rev ctx.s);
|
|
614 |
step_asserts = List.map (translate_expr env) nd_node_asserts; |
|
615 |
};
|
|
616 |
(* Processing spec: there is no processing performed here. Contract have
|
|
617 |
been processed already. Either one of the other machine is a cocospec
|
|
618 |
node, or the current one is a cocospec node. Contract do not contain any
|
|
619 |
statement or import. *) |
|
592 | 620 |
mspec = { mnode_spec = nd.node_spec; mtransitions; mmemory_packs }; |
593 | 621 |
mannot = nd.node_annot; |
594 | 622 |
msch = Some sch; |
... | ... | |
600 | 628 |
let machines = |
601 | 629 |
List.map |
602 | 630 |
(fun decl -> |
603 |
let node = node_of_top decl in
|
|
604 |
let sch = IMap.find node.node_id node_schs in
|
|
605 |
translate_decl node sch
|
|
606 |
) nodes
|
|
631 |
let node = node_of_top decl in |
|
632 |
let sch = IMap.find node.node_id node_schs in |
|
633 |
translate_decl node sch)
|
|
634 |
nodes |
|
607 | 635 |
in |
608 | 636 |
machines |
609 | 637 |
|
Also available in: Unified diff
reformatting