lustrec / src / machine_code.ml @ f4cba4b8
History | View | Annotate | Download (16.1 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(********************************************************************) |
11 |
|
12 |
open Lustre_types |
13 |
open Machine_code_types |
14 |
open Machine_code_common |
15 |
open Corelang |
16 |
open Clocks |
17 |
open Causality |
18 |
|
19 |
exception NormalizationError |
20 |
|
21 |
(* Questions: |
22 |
|
23 |
- where are used the mconst. They contain initialization of |
24 |
constant in nodes. But they do not seem to be used by c_backend *) |
25 |
|
26 |
|
27 |
(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *) |
28 |
(* the context contains m : state aka memory variables *) |
29 |
(* si : initialization instructions *) |
30 |
(* j : node aka machine instances *) |
31 |
(* d : local variables *) |
32 |
(* s : step instructions *) |
33 |
|
34 |
(* Machine processing requires knowledge about variables and local |
35 |
variables. Local could be memories while other could not. *) |
36 |
type machine_env = { |
37 |
is_local: string -> bool; |
38 |
get_var: string -> var_decl |
39 |
} |
40 |
|
41 |
|
42 |
let build_env locals non_locals = |
43 |
let all = VSet.union locals non_locals in |
44 |
{ |
45 |
is_local = (fun id -> VSet.exists (fun v -> v.var_id = id) locals); |
46 |
get_var = (fun id -> try |
47 |
VSet.get id all |
48 |
with Not_found -> ( |
49 |
Format.eprintf "Impossible to find variable %s in set %a@.@?" |
50 |
id |
51 |
VSet.pp all; |
52 |
raise Not_found |
53 |
) |
54 |
) |
55 |
} |
56 |
|
57 |
|
58 |
|
59 |
(****************************************************************) |
60 |
(* Basic functions to translate to machine values, instructions *) |
61 |
(****************************************************************) |
62 |
|
63 |
let translate_ident env id = |
64 |
(* Format.eprintf "trnaslating ident: %s@." id; *) |
65 |
try (* id is a var that shall be visible here , ie. in vars *) |
66 |
let var_id = env.get_var id in |
67 |
mk_val (Var var_id) var_id.var_type |
68 |
with Not_found -> |
69 |
try (* id is a constant *) |
70 |
let vdecl = (Corelang.var_decl_of_const |
71 |
(const_of_top (Hashtbl.find Corelang.consts_table id))) |
72 |
in |
73 |
mk_val (Var vdecl) vdecl.var_type |
74 |
with Not_found -> |
75 |
(* id is a tag, getting its type in the list of declared enums *) |
76 |
try |
77 |
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in |
78 |
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ) |
79 |
with Not_found -> (Format.eprintf |
80 |
"internal error: Machine_code.translate_ident %s" |
81 |
id; |
82 |
assert false) |
83 |
|
84 |
let rec control_on_clock env ck inst = |
85 |
match (Clocks.repr ck).cdesc with |
86 |
| Con (ck1, cr, l) -> |
87 |
let id = Clocks.const_of_carrier cr in |
88 |
control_on_clock env ck1 |
89 |
(mkinstr |
90 |
(MBranch (translate_ident env id, |
91 |
[l, [inst]] ))) |
92 |
| _ -> inst |
93 |
|
94 |
|
95 |
(* specialize predefined (polymorphic) operators wrt their instances, |
96 |
so that the C semantics is preserved *) |
97 |
let specialize_to_c expr = |
98 |
match expr.expr_desc with |
99 |
| Expr_appl (id, e, r) -> |
100 |
if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e) |
101 |
then let id = |
102 |
match id with |
103 |
| "=" -> "equi" |
104 |
| "!=" -> "xor" |
105 |
| _ -> id in |
106 |
{ expr with expr_desc = Expr_appl (id, e, r) } |
107 |
else expr |
108 |
| _ -> expr |
109 |
|
110 |
let specialize_op expr = |
111 |
match !Options.output with |
112 |
| "C" -> specialize_to_c expr |
113 |
| _ -> expr |
114 |
|
115 |
let rec translate_expr env expr = |
116 |
let expr = specialize_op expr in |
117 |
let translate_expr = translate_expr env in |
118 |
let value_desc = |
119 |
match expr.expr_desc with |
120 |
| Expr_const v -> Cst v |
121 |
| Expr_ident x -> (translate_ident env x).value_desc |
122 |
| Expr_array el -> Array (List.map translate_expr el) |
123 |
| Expr_access (t, i) -> Access (translate_expr t, |
124 |
translate_expr |
125 |
(expr_of_dimension i)) |
126 |
| Expr_power (e, n) -> Power (translate_expr e, |
127 |
translate_expr |
128 |
(expr_of_dimension n)) |
129 |
| Expr_tuple _ |
130 |
| Expr_arrow _ |
131 |
| Expr_fby _ |
132 |
| Expr_pre _ -> (Printers.pp_expr |
133 |
Format.err_formatter expr; |
134 |
Format.pp_print_flush |
135 |
Format.err_formatter (); |
136 |
raise NormalizationError) |
137 |
|
138 |
| Expr_when (e1, _, _) -> (translate_expr e1).value_desc |
139 |
| Expr_merge (x, _) -> raise NormalizationError |
140 |
| Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr -> |
141 |
let nd = node_from_name id in |
142 |
Fun (node_name nd, List.map translate_expr (expr_list_of_expr e)) |
143 |
| Expr_ite (g,t,e) -> ( |
144 |
(* special treatment depending on the active backend. For |
145 |
functional ones, like horn backend, ite are preserved in |
146 |
expression. While they are removed for C or Java backends. *) |
147 |
if Backends.is_functional () then |
148 |
Fun ("ite", [translate_expr g; translate_expr t; translate_expr e]) |
149 |
else |
150 |
(Format.eprintf "Normalization error for backend %s: %a@." |
151 |
!Options.output |
152 |
Printers.pp_expr expr; |
153 |
raise NormalizationError) |
154 |
) |
155 |
| _ -> raise NormalizationError |
156 |
in |
157 |
mk_val value_desc expr.expr_type |
158 |
|
159 |
let translate_guard env expr = |
160 |
match expr.expr_desc with |
161 |
| Expr_ident x -> translate_ident env x |
162 |
| _ -> (Format.eprintf "internal error: translate_guard %a@." |
163 |
Printers.pp_expr expr; |
164 |
assert false) |
165 |
|
166 |
let rec translate_act env (y, expr) = |
167 |
let translate_act = translate_act env in |
168 |
let translate_guard = translate_guard env in |
169 |
let translate_ident = translate_ident env in |
170 |
let translate_expr = translate_expr env in |
171 |
let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in |
172 |
match expr.expr_desc with |
173 |
| Expr_ite (c, t, e) -> let g = translate_guard c in |
174 |
mk_conditional ?lustre_eq:(Some eq) g |
175 |
[translate_act (y, t)] |
176 |
[translate_act (y, e)] |
177 |
| Expr_merge (x, hl) -> mkinstr ?lustre_eq:(Some eq) |
178 |
(MBranch (translate_ident x, |
179 |
List.map (fun (t, h) -> |
180 |
t, [translate_act (y, h)]) |
181 |
hl)) |
182 |
| _ -> mkinstr ?lustre_eq:(Some eq) |
183 |
(MLocalAssign (y, translate_expr expr)) |
184 |
|
185 |
let reset_instance env i r c = |
186 |
match r with |
187 |
| None -> [] |
188 |
| Some r -> let g = translate_guard env r in |
189 |
[control_on_clock |
190 |
env |
191 |
c |
192 |
(mk_conditional |
193 |
g |
194 |
[mkinstr (MReset i)] |
195 |
[mkinstr (MNoReset i)]) |
196 |
] |
197 |
|
198 |
|
199 |
(* Datastructure updated while visiting equations *) |
200 |
type machine_ctx = { |
201 |
m: VSet.t; (* Memories *) |
202 |
si: instr_t list; |
203 |
j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t; |
204 |
s: instr_t list; |
205 |
} |
206 |
|
207 |
let ctx_init = { m = VSet.empty; (* memories *) |
208 |
si = []; (* init instr *) |
209 |
j = Utils.IMap.empty; |
210 |
s = [] } |
211 |
|
212 |
(****************************************************************) |
213 |
(* Main function to translate equations into this machine context we |
214 |
are building *) |
215 |
(****************************************************************) |
216 |
|
217 |
|
218 |
|
219 |
let translate_eq env ctx eq = |
220 |
let translate_expr = translate_expr env in |
221 |
let translate_act = translate_act env in |
222 |
let control_on_clock = control_on_clock env in |
223 |
let reset_instance = reset_instance env in |
224 |
|
225 |
(* Format.eprintf "translate_eq %a with clock %a@." |
226 |
Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) |
227 |
match eq.eq_lhs, eq.eq_rhs.expr_desc with |
228 |
| [x], Expr_arrow (e1, e2) -> |
229 |
let var_x = env.get_var x in |
230 |
let o = new_instance Arrow.arrow_top_decl eq.eq_rhs.expr_tag in |
231 |
let c1 = translate_expr e1 in |
232 |
let c2 = translate_expr e2 in |
233 |
{ ctx with |
234 |
si = mkinstr (MReset o) :: ctx.si; |
235 |
j = Utils.IMap.add o (Arrow.arrow_top_decl, []) ctx.j; |
236 |
s = (control_on_clock |
237 |
eq.eq_rhs.expr_clock |
238 |
(mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2]))) |
239 |
) :: ctx.s |
240 |
} |
241 |
| [x], Expr_pre e1 when env.is_local x -> |
242 |
let var_x = env.get_var x in |
243 |
|
244 |
{ ctx with |
245 |
m = VSet.add var_x ctx.m; |
246 |
s = control_on_clock |
247 |
eq.eq_rhs.expr_clock |
248 |
(mkinstr ?lustre_eq:(Some eq) |
249 |
(MStateAssign (var_x, translate_expr e1))) |
250 |
:: ctx.s |
251 |
} |
252 |
| [x], Expr_fby (e1, e2) when env.is_local x -> |
253 |
let var_x = env.get_var x in |
254 |
{ ctx with |
255 |
m = VSet.add var_x ctx.m; |
256 |
si = mkinstr ?lustre_eq:(Some eq) |
257 |
(MStateAssign (var_x, translate_expr e1)) |
258 |
:: ctx.si; |
259 |
s = control_on_clock |
260 |
eq.eq_rhs.expr_clock |
261 |
(mkinstr ?lustre_eq:(Some eq) |
262 |
(MStateAssign (var_x, translate_expr e2))) |
263 |
:: ctx.s |
264 |
} |
265 |
|
266 |
| p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) -> |
267 |
let var_p = List.map (fun v -> env.get_var v) p in |
268 |
let el = expr_list_of_expr arg in |
269 |
let vl = List.map translate_expr el in |
270 |
let node_f = node_from_name f in |
271 |
let call_f = |
272 |
node_f, |
273 |
NodeDep.filter_static_inputs (node_inputs node_f) el in |
274 |
let o = new_instance node_f eq.eq_rhs.expr_tag in |
275 |
let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in |
276 |
let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in |
277 |
(*Clocks.new_var true in |
278 |
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; |
279 |
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;*) |
280 |
{ ctx with |
281 |
si = |
282 |
(if Stateless.check_node node_f then ctx.si else mkinstr (MReset o) :: ctx.si); |
283 |
j = Utils.IMap.add o call_f ctx.j; |
284 |
s = (if Stateless.check_node node_f |
285 |
then [] |
286 |
else reset_instance o r call_ck) @ |
287 |
(control_on_clock call_ck |
288 |
(mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) |
289 |
:: ctx.s |
290 |
} |
291 |
|
292 |
| [x], _ -> ( |
293 |
let var_x = env.get_var x in |
294 |
{ ctx with |
295 |
s = |
296 |
control_on_clock |
297 |
eq.eq_rhs.expr_clock |
298 |
(translate_act (var_x, eq.eq_rhs)) :: ctx.s |
299 |
} |
300 |
) |
301 |
| _ -> |
302 |
begin |
303 |
Format.eprintf "internal error: Machine_code.translate_eq %a@?" |
304 |
Printers.pp_node_eq eq; |
305 |
assert false |
306 |
end |
307 |
|
308 |
|
309 |
|
310 |
let constant_equations locals = |
311 |
VSet.fold (fun vdecl eqs -> |
312 |
if vdecl.var_dec_const |
313 |
then |
314 |
{ eq_lhs = [vdecl.var_id]; |
315 |
eq_rhs = Utils.desome vdecl.var_dec_value; |
316 |
eq_loc = vdecl.var_loc |
317 |
} :: eqs |
318 |
else eqs) |
319 |
locals [] |
320 |
|
321 |
let translate_eqs env ctx eqs = |
322 |
List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx;; |
323 |
|
324 |
|
325 |
(****************************************************************) |
326 |
(* Processing nodes *) |
327 |
(****************************************************************) |
328 |
|
329 |
let process_asserts nd = |
330 |
|
331 |
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in |
332 |
if Backends.is_functional () then |
333 |
[], [], exprl |
334 |
else (* Each assert(e) is associated to a fresh variable v and declared as |
335 |
v=e; assert (v); *) |
336 |
let _, vars, eql, assertl = |
337 |
List.fold_left (fun (i, vars, eqlist, assertlist) expr -> |
338 |
let loc = expr.expr_loc in |
339 |
let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in |
340 |
let assert_var = |
341 |
mkvar_decl |
342 |
loc |
343 |
~orig:false (* fresh var *) |
344 |
(var_id, |
345 |
mktyp loc Tydec_bool, |
346 |
mkclock loc Ckdec_any, |
347 |
false, (* not a constant *) |
348 |
None, (* no default value *) |
349 |
Some nd.node_id |
350 |
) |
351 |
in |
352 |
assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *); |
353 |
let eq = mkeq loc ([var_id], expr) in |
354 |
(i+1, |
355 |
assert_var::vars, |
356 |
eq::eqlist, |
357 |
{expr with expr_desc = Expr_ident var_id}::assertlist) |
358 |
) (1, [], [], []) exprl |
359 |
in |
360 |
vars, eql, assertl |
361 |
|
362 |
let translate_core sorted_eqs locals other_vars = |
363 |
let constant_eqs = constant_equations locals in |
364 |
|
365 |
let env = build_env locals other_vars in |
366 |
|
367 |
(* Compute constants' instructions *) |
368 |
let ctx0 = translate_eqs env ctx_init constant_eqs in |
369 |
assert (VSet.is_empty ctx0.m); |
370 |
assert (ctx0.si = []); |
371 |
assert (Utils.IMap.is_empty ctx0.j); |
372 |
|
373 |
(* Compute ctx for all eqs *) |
374 |
let ctx = translate_eqs env ctx_init sorted_eqs in |
375 |
|
376 |
ctx, ctx0.s |
377 |
|
378 |
|
379 |
let translate_decl nd sch = |
380 |
(* Extracting eqs, variables .. *) |
381 |
let eqs, auts = get_node_eqs nd in |
382 |
assert (auts = []); (* Automata should be expanded by now *) |
383 |
|
384 |
(* In case of non functional backend (eg. C), additional local variables have |
385 |
to be declared for each assert *) |
386 |
let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in |
387 |
|
388 |
(* Build the env: variables visible in the current scope *) |
389 |
let locals_list = nd.node_locals @ new_locals in |
390 |
let locals = VSet.of_list locals_list in |
391 |
let inout_vars = (VSet.of_list (nd.node_inputs @ nd.node_outputs)) in |
392 |
let env = build_env locals inout_vars in |
393 |
|
394 |
(* Computing main content *) |
395 |
let schedule = sch.Scheduling_type.schedule in |
396 |
let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in |
397 |
|
398 |
let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in |
399 |
|
400 |
|
401 |
|
402 |
let mmap = Utils.IMap.elements ctx.j in |
403 |
{ |
404 |
mname = nd; |
405 |
mmemory = VSet.elements ctx.m; |
406 |
mcalls = mmap; |
407 |
minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap; |
408 |
minit = ctx.si; |
409 |
mconst = ctx0_s; |
410 |
mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs; |
411 |
mstep = { |
412 |
step_inputs = nd.node_inputs; |
413 |
step_outputs = nd.node_outputs; |
414 |
step_locals = (* Removing computed memories from locals *) |
415 |
VSet.elements (VSet.diff locals ctx.m); |
416 |
step_checks = List.map (fun d -> d.Dimension.dim_loc, |
417 |
translate_expr env |
418 |
(expr_of_dimension d)) |
419 |
nd.node_checks; |
420 |
step_instrs = ( |
421 |
(* special treatment depending on the active backend. For horn backend, |
422 |
common branches are not merged while they are in C or Java |
423 |
backends. *) |
424 |
if !Backends.join_guards then |
425 |
join_guards_list ctx.s |
426 |
else |
427 |
ctx.s |
428 |
); |
429 |
step_asserts = List.map (translate_expr env) nd_node_asserts; |
430 |
}; |
431 |
|
432 |
(* Processing spec: there is no processing performed here. Contract |
433 |
have been processed already. Either one of the other machine is a |
434 |
cocospec node, or the current one is a cocospec node. Contract do |
435 |
not contain any statement or import. *) |
436 |
|
437 |
mspec = nd.node_spec; |
438 |
mannot = nd.node_annot; |
439 |
msch = Some sch; |
440 |
} |
441 |
|
442 |
(** takes the global declarations and the scheduling associated to each node *) |
443 |
let translate_prog decls node_schs = |
444 |
let nodes = get_nodes decls in |
445 |
let machines = |
446 |
List.map |
447 |
(fun decl -> |
448 |
let node = node_of_top decl in |
449 |
let sch = Utils.IMap.find node.node_id node_schs in |
450 |
translate_decl node sch |
451 |
) nodes |
452 |
in |
453 |
machines |
454 |
|
455 |
(* Local Variables: *) |
456 |
(* compile-command:"make -C .." *) |
457 |
(* End: *) |