lustrec / src / machine_code.ml @ e8f55c25
History  View  Annotate  Download (16.6 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 
(* Format.eprintf "Translating node %s@." nd.node_id; *) 
381 
(* Extracting eqs, variables .. *) 
382 
let eqs, auts = get_node_eqs nd in 
383 
assert (auts = []); (* Automata should be expanded by now *) 
384 

385 
(* In case of non functional backend (eg. C), additional local variables have 
386 
to be declared for each assert *) 
387 
let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in 
388  
389 
(* Build the env: variables visible in the current scope *) 
390 
let locals_list = nd.node_locals @ new_locals in 
391 
let locals = VSet.of_list locals_list in 
392 
let inout_vars = (VSet.of_list (nd.node_inputs @ nd.node_outputs)) in 
393 
let env = build_env locals inout_vars in 
394  
395 
(* Format.eprintf "Node content is %a@." Printers.pp_node nd; *) 
396 

397 
(* Computing main content *) 
398 
(* Format.eprintf "ok1@.@?"; *) 
399 
let schedule = sch.Scheduling_type.schedule in 
400 
(* Format.eprintf "ok2@.@?"; *) 
401 
let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in 
402 
(* Format.eprintf "ok3@.locals=%a@.inout:%a@?" 
403 
* VSet.pp locals 
404 
* VSet.pp inout_vars 
405 
* ; *) 
406 

407 
let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in 
408 

409 
(* Format.eprintf "ok4@.@?"; *) 
410  
411 
(* Removing computed memories from locals. We also removed unused variables. *) 
412 
let updated_locals = 
413 
let l = VSet.elements (VSet.diff locals ctx.m) in 
414 
List.fold_left (fun res v > if List.mem v.var_id unused then res else v::res) [] l 
415 
in 
416 
let mmap = Utils.IMap.elements ctx.j in 
417 
{ 
418 
mname = nd; 
419 
mmemory = VSet.elements ctx.m; 
420 
mcalls = mmap; 
421 
minstances = List.filter (fun (_, (n,_)) > not (Stateless.check_node n)) mmap; 
422 
minit = ctx.si; 
423 
mconst = ctx0_s; 
424 
mstatic = List.filter (fun v > v.var_dec_const) nd.node_inputs; 
425 
mstep = { 
426 
step_inputs = nd.node_inputs; 
427 
step_outputs = nd.node_outputs; 
428 
step_locals = updated_locals; 
429 
step_checks = List.map (fun d > d.Dimension.dim_loc, 
430 
translate_expr env 
431 
(expr_of_dimension d)) 
432 
nd.node_checks; 
433 
step_instrs = ( 
434 
(* special treatment depending on the active backend. For horn backend, 
435 
common branches are not merged while they are in C or Java 
436 
backends. *) 
437 
if !Backends.join_guards then 
438 
join_guards_list ctx.s 
439 
else 
440 
ctx.s 
441 
); 
442 
step_asserts = List.map (translate_expr env) nd_node_asserts; 
443 
}; 
444  
445 
(* Processing spec: there is no processing performed here. Contract 
446 
have been processed already. Either one of the other machine is a 
447 
cocospec node, or the current one is a cocospec node. Contract do 
448 
not contain any statement or import. *) 
449 

450 
mspec = nd.node_spec; 
451 
mannot = nd.node_annot; 
452 
msch = Some sch; 
453 
} 
454  
455 
(** takes the global declarations and the scheduling associated to each node *) 
456 
let translate_prog decls node_schs = 
457 
let nodes = get_nodes decls in 
458 
let machines = 
459 
List.map 
460 
(fun decl > 
461 
let node = node_of_top decl in 
462 
let sch = Utils.IMap.find node.node_id node_schs in 
463 
translate_decl node sch 
464 
) nodes 
465 
in 
466 
machines 
467  
468 
(* Local Variables: *) 
469 
(* compilecommand:"make C .." *) 
470 
(* End: *) 