lustrec / src / machine_code.ml @ 4f26dcf5
History  View  Annotate  Download (14.9 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  
22 
(* translate_<foo> : node > context > <foo> > machine code/expression *) 
23 
(* the context contains m : state aka memory variables *) 
24 
(* si : initialization instructions *) 
25 
(* j : node aka machine instances *) 
26 
(* d : local variables *) 
27 
(* s : step instructions *) 
28 
let translate_ident node (m, si, j, d, s) id = 
29 
(* Format.eprintf "trnaslating ident: %s@." id; *) 
30 
try (* id is a node var *) 
31 
let var_id = get_node_var id node in 
32 
if VSet.exists (fun v > v.var_id = id) m 
33 
then ( 
34 
(* Format.eprintf "a STATE VAR@."; *) 
35 
mk_val (StateVar var_id) var_id.var_type 
36 
) 
37 
else ( 
38 
(* Format.eprintf "a LOCAL VAR@."; *) 
39 
mk_val (LocalVar var_id) var_id.var_type 
40 
) 
41 
with Not_found > 
42 
try (* id is a constant *) 
43 
let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in 
44 
mk_val (LocalVar vdecl) vdecl.var_type 
45 
with Not_found > 
46 
(* id is a tag *) 
47 
(* DONE construire une liste des enum declarés et alors chercher dedans la liste 
48 
qui contient id *) 
49 
try 
50 
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in 
51 
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ) 
52 
with Not_found > (Format.eprintf "internal error: Machine_code.translate_ident %s" id; 
53 
assert false) 
54  
55 
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst = 
56 
match (Clocks.repr ck).cdesc with 
57 
 Con (ck1, cr, l) > 
58 
let id = Clocks.const_of_carrier cr in 
59 
control_on_clock node args ck1 (mkinstr 
60 
(* TODO il faudrait prendre le lustre 
61 
associé à instr et rajouter print_ck_suffix 
62 
ck) de clocks.ml *) 
63 
(MBranch (translate_ident node args id, 
64 
[l, [inst]] ))) 
65 
 _ > inst 
66  
67  
68 
(* specialize predefined (polymorphic) operators 
69 
wrt their instances, so that the C semantics 
70 
is preserved *) 
71 
let specialize_to_c expr = 
72 
match expr.expr_desc with 
73 
 Expr_appl (id, e, r) > 
74 
if List.exists (fun e > Types.is_bool_type e.expr_type) (expr_list_of_expr e) 
75 
then let id = 
76 
match id with 
77 
 "=" > "equi" 
78 
 "!=" > "xor" 
79 
 _ > id in 
80 
{ expr with expr_desc = Expr_appl (id, e, r) } 
81 
else expr 
82 
 _ > expr 
83  
84 
let specialize_op expr = 
85 
match !Options.output with 
86 
 "C" > specialize_to_c expr 
87 
 _ > expr 
88  
89 
let rec translate_expr node ((m, si, j, d, s) as args) expr = 
90 
let expr = specialize_op expr in 
91 
let value_desc = 
92 
match expr.expr_desc with 
93 
 Expr_const v > Cst v 
94 
 Expr_ident x > (translate_ident node args x).value_desc 
95 
 Expr_array el > Array (List.map (translate_expr node args) el) 
96 
 Expr_access (t, i) > Access (translate_expr node args t, translate_expr node args (expr_of_dimension i)) 
97 
 Expr_power (e, n) > Power (translate_expr node args e, translate_expr node args (expr_of_dimension n)) 
98 
 Expr_tuple _ 
99 
 Expr_arrow _ 
100 
 Expr_fby _ 
101 
 Expr_pre _ > (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) 
102 
 Expr_when (e1, _, _) > (translate_expr node args e1).value_desc 
103 
 Expr_merge (x, _) > raise NormalizationError 
104 
 Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr > 
105 
let nd = node_from_name id in 
106 
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e)) 
107 
 Expr_ite (g,t,e) > ( 
108 
(* special treatment depending on the active backend. For horn backend, ite 
109 
are preserved in expression. While they are removed for C or Java 
110 
backends. *) 
111 
match !Options.output with 
112 
 "horn" > 
113 
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e]) 
114 
 "C"  "java"  _ > 
115 
(Format.eprintf "Normalization error for backend %s: %a@." 
116 
!Options.output 
117 
Printers.pp_expr expr; 
118 
raise NormalizationError) 
119 
) 
120 
 _ > raise NormalizationError 
121 
in 
122 
mk_val value_desc expr.expr_type 
123  
124 
let translate_guard node args expr = 
125 
match expr.expr_desc with 
126 
 Expr_ident x > translate_ident node args x 
127 
 _ > (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false) 
128  
129 
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = 
130 
let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in 
131 
match expr.expr_desc with 
132 
 Expr_ite (c, t, e) > let g = translate_guard node args c in 
133 
mk_conditional ?lustre_eq:(Some eq) g 
134 
[translate_act node args (y, t)] 
135 
[translate_act node args (y, e)] 
136 
 Expr_merge (x, hl) > mkinstr ?lustre_eq:(Some eq) (MBranch (translate_ident node args x, 
137 
List.map (fun (t, h) > t, [translate_act node args (y, h)]) hl)) 
138 
 _ > mkinstr ?lustre_eq:(Some eq) (MLocalAssign (y, translate_expr node args expr)) 
139  
140 
let reset_instance node args i r c = 
141 
match r with 
142 
 None > [] 
143 
 Some r > let g = translate_guard node args r in 
144 
[control_on_clock node args c (mk_conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])] 
145  
146 
let translate_eq node ((m, si, j, d, s) as args) eq = 
147 
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) 
148 
match eq.eq_lhs, eq.eq_rhs.expr_desc with 
149 
 [x], Expr_arrow (e1, e2) > 
150 
let var_x = get_node_var x node in 
151 
let o = new_instance node Arrow.arrow_top_decl eq.eq_rhs.expr_tag in 
152 
let c1 = translate_expr node args e1 in 
153 
let c2 = translate_expr node args e2 in 
154 
(m, 
155 
mkinstr (MReset o) :: si, 
156 
Utils.IMap.add o (Arrow.arrow_top_decl, []) j, 
157 
d, 
158 
(control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s) 
159 
 [x], Expr_pre e1 when VSet.mem (get_node_var x node) d > 
160 
let var_x = get_node_var x node in 
161 
(VSet.add var_x m, 
162 
si, 
163 
j, 
164 
d, 
165 
control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1))) :: s) 
166 
 [x], Expr_fby (e1, e2) when VSet.mem (get_node_var x node) d > 
167 
let var_x = get_node_var x node in 
168 
(VSet.add var_x m, 
169 
mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1)) :: si, 
170 
j, 
171 
d, 
172 
control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e2))) :: s) 
173  
174 
 p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) > 
175 
let var_p = List.map (fun v > get_node_var v node) p in 
176 
let el = expr_list_of_expr arg in 
177 
let vl = List.map (translate_expr node args) el in 
178 
let node_f = node_from_name f in 
179 
let call_f = 
180 
node_f, 
181 
NodeDep.filter_static_inputs (node_inputs node_f) el in 
182 
let o = new_instance node node_f eq.eq_rhs.expr_tag in 
183 
let env_cks = List.fold_right (fun arg cks > arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in 
184 
let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in 
185 
(*Clocks.new_var true in 
186 
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; 
187 
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;*) 
188 
(m, 
189 
(if Stateless.check_node node_f then si else mkinstr (MReset o) :: si), 
190 
Utils.IMap.add o call_f j, 
191 
d, 
192 
(if Stateless.check_node node_f 
193 
then [] 
194 
else reset_instance node args o r call_ck) @ 
195 
(control_on_clock node args call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s) 
196 
(* 
197 
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) 
198 
are preserved. While they are replaced as if g then x = t else x = e in C or Java 
199 
backends. *) 
200 
 [x], Expr_ite (c, t, e) 
201 
when (match !Options.output with  "horn" > true  "C"  "java"  _ > false) 
202 
> 
203 
let var_x = get_node_var x node in 
204 
(m, 
205 
si, 
206 
j, 
207 
d, 
208 
(control_on_clock node args eq.eq_rhs.expr_clock 
209 
(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s) 
210 
) 
211  
212 
*) 
213 
 [x], _ > ( 
214 
let var_x = get_node_var x node in 
215 
(m, si, j, d, 
216 
control_on_clock 
217 
node 
218 
args 
219 
eq.eq_rhs.expr_clock 
220 
(translate_act node args (var_x, eq.eq_rhs)) :: s 
221 
) 
222 
) 
223 
 _ > 
224 
begin 
225 
Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq; 
226 
assert false 
227 
end 
228  
229 
let find_eq xl eqs = 
230 
let rec aux accu eqs = 
231 
match eqs with 
232 
 [] > 
233 
begin 
234 
Format.eprintf "Looking for variables %a in the following equations@.%a@." 
235 
(Utils.fprintf_list ~sep:" , " (fun fmt v > Format.fprintf fmt "%s" v)) xl 
236 
Printers.pp_node_eqs eqs; 
237 
assert false 
238 
end 
239 
 hd::tl > 
240 
if List.exists (fun x > List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl 
241 
in 
242 
aux [] eqs 
243  
244 
(* Sort the set of equations of node [nd] according 
245 
to the computed schedule [sch] 
246 
*) 
247 
let sort_equations_from_schedule nd sch = 
248 
(* Format.eprintf "%s schedule: %a@." *) 
249 
(* nd.node_id *) 
250 
(* (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *) 
251 
let eqs, auts = get_node_eqs nd in 
252 
assert (auts = []); (* Automata should be expanded by now *) 
253 
let split_eqs = Splitting.tuple_split_eq_list eqs in 
254 
let eqs_rev, remainder = 
255 
List.fold_left 
256 
(fun (accu, node_eqs_remainder) vl > 
257 
if List.exists (fun eq > List.exists (fun v > List.mem v eq.eq_lhs) vl) accu 
258 
then 
259 
(accu, node_eqs_remainder) 
260 
else 
261 
let eq_v, remainder = find_eq vl node_eqs_remainder in 
262 
eq_v::accu, remainder 
263 
) 
264 
([], split_eqs) 
265 
sch 
266 
in 
267 
begin 
268 
if List.length remainder > 0 then ( 
269 
let eqs, auts = get_node_eqs nd in 
270 
assert (auts = []); (* Automata should be expanded by now *) 
271 
Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?" 
272 
Printers.pp_node_eqs remainder 
273 
Printers.pp_node_eqs eqs; 
274 
assert false); 
275 
List.rev eqs_rev 
276 
end 
277  
278 
let constant_equations nd = 
279 
List.fold_right (fun vdecl eqs > 
280 
if vdecl.var_dec_const 
281 
then 
282 
{ eq_lhs = [vdecl.var_id]; 
283 
eq_rhs = Utils.desome vdecl.var_dec_value; 
284 
eq_loc = vdecl.var_loc 
285 
} :: eqs 
286 
else eqs) 
287 
nd.node_locals [] 
288  
289 
let translate_eqs node args eqs = 
290 
List.fold_right (fun eq args > translate_eq node args eq) eqs args;; 
291  
292 
let translate_decl nd sch = 
293 
(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*) 
294  
295 
let sorted_eqs = sort_equations_from_schedule nd sch in 
296 
let constant_eqs = constant_equations nd in 
297  
298 
(* In case of non functional backend (eg. C), additional local variables have 
299 
to be declared for each assert *) 
300 
let new_locals, assert_instrs, nd_node_asserts = 
301 
let exprl = List.map (fun assert_ > assert_.assert_expr ) nd.node_asserts in 
302 
if Backends.is_functional () then 
303 
[], [], exprl 
304 
else (* Each assert(e) is associated to a fresh variable v and declared as 
305 
v=e; assert (v); *) 
306 
let _, vars, eql, assertl = 
307 
List.fold_left (fun (i, vars, eqlist, assertlist) expr > 
308 
let loc = expr.expr_loc in 
309 
let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in 
310 
let assert_var = 
311 
mkvar_decl 
312 
loc 
313 
~orig:false (* fresh var *) 
314 
(var_id, 
315 
mktyp loc Tydec_bool, 
316 
mkclock loc Ckdec_any, 
317 
false, (* not a constant *) 
318 
None, (* no default value *) 
319 
Some nd.node_id 
320 
) 
321 
in 
322 
assert_var.var_type < Type_predef.type_bool (* Types.new_ty (Types.Tbool) *); 
323 
let eq = mkeq loc ([var_id], expr) in 
324 
(i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist) 
325 
) (1, [], [], []) exprl 
326 
in 
327 
vars, eql, assertl 
328 
in 
329 
let locals_list = nd.node_locals @ new_locals in 
330  
331 
let nd = { nd with node_locals = locals_list } in 
332 
let init_args = VSet.empty, [], Utils.IMap.empty, List.fold_right (fun l > VSet.add l) locals_list VSet.empty, [] in 
333 
(* memories, init instructions, node calls, local variables (including memories), step instrs *) 
334 
let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in 
335 
assert (VSet.is_empty m0); 
336 
assert (init0 = []); 
337 
assert (Utils.IMap.is_empty j0); 
338 
let m, init, j, locals, s as context_with_asserts = translate_eqs nd (m0, init0, j0, locals0, []) (assert_instrs@sorted_eqs) in 
339 
let mmap = Utils.IMap.fold (fun i n res > (i, n)::res) j [] in 
340 
{ 
341 
mname = nd; 
342 
mmemory = VSet.elements m; 
343 
mcalls = mmap; 
344 
minstances = List.filter (fun (_, (n,_)) > not (Stateless.check_node n)) mmap; 
345 
minit = init; 
346 
mconst = s0; 
347 
mstatic = List.filter (fun v > v.var_dec_const) nd.node_inputs; 
348 
mstep = { 
349 
step_inputs = nd.node_inputs; 
350 
step_outputs = nd.node_outputs; 
351 
step_locals = VSet.elements (VSet.diff locals m); 
352 
step_checks = List.map (fun d > d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks; 
353 
step_instrs = ( 
354 
(* special treatment depending on the active backend. For horn backend, 
355 
common branches are not merged while they are in C or Java 
356 
backends. *) 
357 
(*match !Options.output with 
358 
 "horn" > s 
359 
 "C"  "java"  _ >*) 
360 
if !Backends.join_guards then 
361 
join_guards_list s 
362 
else 
363 
s 
364 
); 
365 
step_asserts = List.map (translate_expr nd context_with_asserts) nd_node_asserts; 
366 
}; 
367 
mspec = nd.node_spec; 
368 
mannot = nd.node_annot; 
369 
} 
370  
371 
(** takes the global declarations and the scheduling associated to each node *) 
372 
let translate_prog decls node_schs = 
373 
let nodes = get_nodes decls in 
374 
List.map 
375 
(fun decl > 
376 
let node = node_of_top decl in 
377 
let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in 
378 
translate_decl node sch 
379 
) nodes 
380  
381  
382 
(* Local Variables: *) 
383 
(* compilecommand:"make C .." *) 
384 
(* End: *) 