lustrec / src / machine_code.ml @ ef8a361a
History  View  Annotate  Download (27.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 LustreSpec 
13 
open Corelang 
14 
open Clocks 
15 
open Causality 
16  
17 
let print_statelocaltag = true 
18 

19 
exception NormalizationError 
20  
21 
module OrdVarDecl:Map.OrderedType with type t=var_decl = 
22 
struct type t = var_decl;; let compare = compare end 
23  
24 
module VSet = Set.Make(OrdVarDecl) 
25  
26 
let rec pp_val fmt v = 
27 
match v.value_desc with 
28 
 Cst c > Printers.pp_const fmt c 
29 
 LocalVar v > 
30 
if print_statelocaltag then 
31 
Format.fprintf fmt "%s(L)" v.var_id 
32 
else 
33 
Format.pp_print_string fmt v.var_id 
34 

35 
 StateVar v > 
36 
if print_statelocaltag then 
37 
Format.fprintf fmt "%s(S)" v.var_id 
38 
else 
39 
Format.pp_print_string fmt v.var_id 
40 
 Array vl > Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl 
41 
 Access (t, i) > Format.fprintf fmt "%a[%a]" pp_val t pp_val i 
42 
 Power (v, n) > Format.fprintf fmt "(%a^%a)" pp_val v pp_val n 
43 
 Fun (n, vl) > Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl 
44  
45 
let rec pp_instr fmt i = 
46 
let _ = 
47 
match i.instr_desc with 
48 
 MLocalAssign (i,v) > Format.fprintf fmt "%s<l %a" i.var_id pp_val v 
49 
 MStateAssign (i,v) > Format.fprintf fmt "%s<s %a" i.var_id pp_val v 
50 
 MReset i > Format.fprintf fmt "reset %s" i 
51 
 MNoReset i > Format.fprintf fmt "noreset %s" i 
52 
 MStep (il, i, vl) > 
53 
Format.fprintf fmt "%a = %s (%a)" 
54 
(Utils.fprintf_list ~sep:", " (fun fmt v > Format.pp_print_string fmt v.var_id)) il 
55 
i 
56 
(Utils.fprintf_list ~sep:", " pp_val) vl 
57 
 MBranch (g,hl) > 
58 
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]" 
59 
pp_val g 
60 
(Utils.fprintf_list ~sep:"@," pp_branch) hl 
61 
 MComment s > Format.pp_print_string fmt s 
62 

63 
in 
64 
(* Annotation *) 
65 
(* let _ = *) 
66 
(* match i.lustre_expr with None > ()  Some e > Format.fprintf fmt "  original expr: %a" Printers.pp_expr e *) 
67 
(* in *) 
68 
let _ = 
69 
match i.lustre_eq with None > ()  Some eq > Format.fprintf fmt "  original eq: %a" Printers.pp_node_eq eq 
70 
in 
71 
() 
72 

73 
and pp_branch fmt (t, h) = 
74 
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h 
75  
76 
and pp_instrs fmt il = 
77 
Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il 
78  
79 
type step_t = { 
80 
step_checks: (Location.t * value_t) list; 
81 
step_inputs: var_decl list; 
82 
step_outputs: var_decl list; 
83 
step_locals: var_decl list; 
84 
step_instrs: instr_t list; 
85 
step_asserts: value_t list; 
86 
} 
87  
88 
type static_call = top_decl * (Dimension.dim_expr list) 
89  
90 
type machine_t = { 
91 
mname: node_desc; 
92 
mmemory: var_decl list; 
93 
mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *) 
94 
minstances: (ident * static_call) list; (* submap of mcalls, from stateful instance to node *) 
95 
minit: instr_t list; 
96 
mstatic: var_decl list; (* static inputs only *) 
97 
mconst: instr_t list; (* assignments of node constant locals *) 
98 
mstep: step_t; 
99 
mspec: node_annot option; 
100 
mannot: expr_annot list; 
101 
} 
102  
103 
(* merge log: get_node_def was in c0f8 *) 
104 
(* Returns the node/machine associated to id in m calls *) 
105 
let get_node_def id m = 
106 
try 
107 
let (decl, _) = List.assoc id m.mcalls in 
108 
Corelang.node_of_top decl 
109 
with Not_found > ( 
110 
(* Format.eprintf "Unable to find node %s in list [%a]@.@?" *) 
111 
(* id *) 
112 
(* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) > Format.fprintf fmt "%s" n)) m.mcalls *) 
113 
(* ; *) 
114 
raise Not_found 
115 
) 
116 

117 
(* merge log: machine_vars was in 44686 *) 
118 
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory 
119  
120 
let pp_step fmt s = 
121 
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ " 
122 
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs 
123 
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs 
124 
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals 
125 
(Utils.fprintf_list ~sep:", " (fun fmt (_, c) > pp_val fmt c)) s.step_checks 
126 
(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs 
127 
(Utils.fprintf_list ~sep:", " pp_val) s.step_asserts 
128  
129  
130 
let pp_static_call fmt (node, args) = 
131 
Format.fprintf fmt "%s<%a>" 
132 
(node_name node) 
133 
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args 
134  
135 
let pp_machine fmt m = 
136 
Format.fprintf fmt 
137 
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ " 
138 
m.mname.node_id 
139 
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory 
140 
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) > Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances 
141 
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit 
142 
(Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst 
143 
pp_step m.mstep 
144 
(fun fmt > match m.mspec with  None > ()  Some spec > Printers.pp_spec fmt spec) 
145 
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot 
146  
147 
let pp_machines fmt ml = 
148 
Format.fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml 
149  
150 

151 
let rec is_const_value v = 
152 
match v.value_desc with 
153 
 Cst _ > true 
154 
 Fun (id, args) > Basic_library.is_value_internal_fun v && List.for_all is_const_value args 
155 
 _ > false 
156  
157 
(* Returns the declared stateless status and the computed one. *) 
158 
let get_stateless_status m = 
159 
(m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless) 
160  
161 
let is_input m id = 
162 
List.exists (fun o > o.var_id = id.var_id) m.mstep.step_inputs 
163  
164 
let is_output m id = 
165 
List.exists (fun o > o.var_id = id.var_id) m.mstep.step_outputs 
166  
167 
let is_memory m id = 
168 
List.exists (fun o > o.var_id = id.var_id) m.mmemory 
169  
170 
let conditional ?lustre_eq c t e = 
171 
mkinstr ?lustre_eq:lustre_eq (MBranch(c, [ (tag_true, t); (tag_false, e) ])) 
172  
173 
let dummy_var_decl name typ = 
174 
{ 
175 
var_id = name; 
176 
var_orig = false; 
177 
var_dec_type = dummy_type_dec; 
178 
var_dec_clock = dummy_clock_dec; 
179 
var_dec_const = false; 
180 
var_dec_value = None; 
181 
var_type = typ; 
182 
var_clock = Clocks.new_ck Clocks.Cvar true; 
183 
var_loc = Location.dummy_loc 
184 
} 
185  
186 
let arrow_id = "_arrow" 
187  
188 
let arrow_typ = Types.new_ty Types.Tunivar 
189  
190 
let arrow_desc = 
191 
{ 
192 
node_id = arrow_id; 
193 
node_type = Type_predef.type_bin_poly_op; 
194 
node_clock = Clock_predef.ck_bin_univ; 
195 
node_inputs= [dummy_var_decl "_in1" arrow_typ; dummy_var_decl "_in2" arrow_typ]; 
196 
node_outputs= [dummy_var_decl "_out" arrow_typ]; 
197 
node_locals= []; 
198 
node_gencalls = []; 
199 
node_checks = []; 
200 
node_asserts = []; 
201 
node_stmts= []; 
202 
node_dec_stateless = false; 
203 
node_stateless = Some false; 
204 
node_spec = None; 
205 
node_annot = []; } 
206  
207 
let arrow_top_decl = 
208 
{ 
209 
top_decl_desc = Node arrow_desc; 
210 
top_decl_owner = (Options_management.core_dependency "arrow"); 
211 
top_decl_itf = false; 
212 
top_decl_loc = Location.dummy_loc 
213 
} 
214  
215 
let mk_val v t = { value_desc = v; 
216 
value_type = t; 
217 
value_annot = None } 
218  
219 
let arrow_machine = 
220 
let state = "_first" in 
221 
let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in 
222 
let var_input1 = List.nth arrow_desc.node_inputs 0 in 
223 
let var_input2 = List.nth arrow_desc.node_inputs 1 in 
224 
let var_output = List.nth arrow_desc.node_outputs 0 in 
225 
let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in 
226 
let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *) 
227 
{ 
228 
mname = arrow_desc; 
229 
mmemory = [var_state]; 
230 
mcalls = []; 
231 
minstances = []; 
232 
minit = [mkinstr (MStateAssign(var_state, cst true))]; 
233 
mstatic = []; 
234 
mconst = []; 
235 
mstep = { 
236 
step_inputs = arrow_desc.node_inputs; 
237 
step_outputs = arrow_desc.node_outputs; 
238 
step_locals = []; 
239 
step_checks = []; 
240 
step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool) 
241 
(List.map mkinstr 
242 
[MStateAssign(var_state, cst false); 
243 
MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)]) 
244 
(List.map mkinstr 
245 
[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)]) ]; 
246 
step_asserts = []; 
247 
}; 
248 
mspec = None; 
249 
mannot = []; 
250 
} 
251  
252 
let empty_desc = 
253 
{ 
254 
node_id = arrow_id; 
255 
node_type = Types.bottom; 
256 
node_clock = Clocks.bottom; 
257 
node_inputs= []; 
258 
node_outputs= []; 
259 
node_locals= []; 
260 
node_gencalls = []; 
261 
node_checks = []; 
262 
node_asserts = []; 
263 
node_stmts= []; 
264 
node_dec_stateless = true; 
265 
node_stateless = Some true; 
266 
node_spec = None; 
267 
node_annot = []; } 
268  
269 
let empty_machine = 
270 
{ 
271 
mname = empty_desc; 
272 
mmemory = []; 
273 
mcalls = []; 
274 
minstances = []; 
275 
minit = []; 
276 
mstatic = []; 
277 
mconst = []; 
278 
mstep = { 
279 
step_inputs = []; 
280 
step_outputs = []; 
281 
step_locals = []; 
282 
step_checks = []; 
283 
step_instrs = []; 
284 
step_asserts = []; 
285 
}; 
286 
mspec = None; 
287 
mannot = []; 
288 
} 
289  
290 
let new_instance = 
291 
let cpt = ref (1) in 
292 
fun caller callee tag > 
293 
begin 
294 
let o = 
295 
if Stateless.check_node callee then 
296 
node_name callee 
297 
else 
298 
Printf.sprintf "ni_%d" (incr cpt; !cpt) in 
299 
let o = 
300 
if !Options.ansi && is_generic_node callee 
301 
then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e > e.expr_tag = tag) caller.node_gencalls) 
302 
else o in 
303 
o 
304 
end 
305  
306  
307 
(* translate_<foo> : node > context > <foo> > machine code/expression *) 
308 
(* the context contains m : state aka memory variables *) 
309 
(* si : initialization instructions *) 
310 
(* j : node aka machine instances *) 
311 
(* d : local variables *) 
312 
(* s : step instructions *) 
313 
let translate_ident node (m, si, j, d, s) id = 
314 
(* Format.eprintf "trnaslating ident: %s@." id; *) 
315 
try (* id is a node var *) 
316 
let var_id = get_node_var id node in 
317 
if VSet.exists (fun v > v.var_id = id) m 
318 
then ( 
319 
(* Format.eprintf "a STATE VAR@."; *) 
320 
mk_val (StateVar var_id) var_id.var_type 
321 
) 
322 
else ( 
323 
(* Format.eprintf "a LOCAL VAR@."; *) 
324 
mk_val (LocalVar var_id) var_id.var_type 
325 
) 
326 
with Not_found > 
327 
try (* id is a constant *) 
328 
let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in 
329 
mk_val (LocalVar vdecl) vdecl.var_type 
330 
with Not_found > 
331 
(* id is a tag *) 
332 
(* DONE construire une liste des enum declarรฉs et alors chercher dedans la liste 
333 
qui contient id *) 
334 
try 
335 
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in 
336 
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ) 
337 
with Not_found > (Format.eprintf "internal error: Machine_code.translate_ident %s" id; 
338 
assert false) 
339  
340 
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst = 
341 
match (Clocks.repr ck).cdesc with 
342 
 Con (ck1, cr, l) > 
343 
let id = Clocks.const_of_carrier cr in 
344 
control_on_clock node args ck1 (mkinstr 
345 
(* TODO il faudrait prendre le lustre 
346 
associรฉ ร instr et rajouter print_ck_suffix 
347 
ck) de clocks.ml *) 
348 
(MBranch (translate_ident node args id, 
349 
[l, [inst]] ))) 
350 
 _ > inst 
351  
352 
let rec join_branches hl1 hl2 = 
353 
match hl1, hl2 with 
354 
 [] , _ > hl2 
355 
 _ , [] > hl1 
356 
 (t1, h1)::q1, (t2, h2)::q2 > 
357 
if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else 
358 
if t1 > t2 then (t2, h2) :: join_branches hl1 q2 
359 
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2 
360  
361 
and join_guards inst1 insts2 = 
362 
match get_instr_desc inst1, List.map get_instr_desc insts2 with 
363 
 _ , [] > 
364 
[inst1] 
365 
 MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 > 
366 
mkinstr 
367 
(* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *) 
368 
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2))) 
369 
:: (List.tl insts2) 
370 
 _ > inst1 :: insts2 
371  
372 
let join_guards_list insts = 
373 
List.fold_right join_guards insts [] 
374  
375 
(* specialize predefined (polymorphic) operators 
376 
wrt their instances, so that the C semantics 
377 
is preserved *) 
378 
let specialize_to_c expr = 
379 
match expr.expr_desc with 
380 
 Expr_appl (id, e, r) > 
381 
if List.exists (fun e > Types.is_bool_type e.expr_type) (expr_list_of_expr e) 
382 
then let id = 
383 
match id with 
384 
 "=" > "equi" 
385 
 "!=" > "xor" 
386 
 _ > id in 
387 
{ expr with expr_desc = Expr_appl (id, e, r) } 
388 
else expr 
389 
 _ > expr 
390  
391 
let specialize_op expr = 
392 
match !Options.output with 
393 
 "C" > specialize_to_c expr 
394 
 _ > expr 
395  
396 
let rec translate_expr node ((m, si, j, d, s) as args) expr = 
397 
let expr = specialize_op expr in 
398 
let value_desc = 
399 
match expr.expr_desc with 
400 
 Expr_const v > Cst v 
401 
 Expr_ident x > (translate_ident node args x).value_desc 
402 
 Expr_array el > Array (List.map (translate_expr node args) el) 
403 
 Expr_access (t, i) > Access (translate_expr node args t, translate_expr node args (expr_of_dimension i)) 
404 
 Expr_power (e, n) > Power (translate_expr node args e, translate_expr node args (expr_of_dimension n)) 
405 
 Expr_tuple _ 
406 
 Expr_arrow _ 
407 
 Expr_fby _ 
408 
 Expr_pre _ > (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) 
409 
 Expr_when (e1, _, _) > (translate_expr node args e1).value_desc 
410 
 Expr_merge (x, _) > raise NormalizationError 
411 
 Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr > 
412 
let nd = node_from_name id in 
413 
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e)) 
414 
 Expr_ite (g,t,e) > ( 
415 
(* special treatment depending on the active backend. For horn backend, ite 
416 
are preserved in expression. While they are removed for C or Java 
417 
backends. *) 
418 
match !Options.output with 
419 
 "horn" > 
420 
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e]) 
421 
 "C"  "java"  _ > 
422 
(Format.eprintf "Normalization error for backend %s: %a@." 
423 
!Options.output 
424 
Printers.pp_expr expr; 
425 
raise NormalizationError) 
426 
) 
427 
 _ > raise NormalizationError 
428 
in 
429 
mk_val value_desc expr.expr_type 
430  
431 
let translate_guard node args expr = 
432 
match expr.expr_desc with 
433 
 Expr_ident x > translate_ident node args x 
434 
 _ > (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false) 
435  
436 
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = 
437 
let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in 
438 
match expr.expr_desc with 
439 
 Expr_ite (c, t, e) > let g = translate_guard node args c in 
440 
conditional ?lustre_eq:(Some eq) g 
441 
[translate_act node args (y, t)] 
442 
[translate_act node args (y, e)] 
443 
 Expr_merge (x, hl) > mkinstr ?lustre_eq:(Some eq) (MBranch (translate_ident node args x, 
444 
List.map (fun (t, h) > t, [translate_act node args (y, h)]) hl)) 
445 
 _ > mkinstr ?lustre_eq:(Some eq) (MLocalAssign (y, translate_expr node args expr)) 
446  
447 
let reset_instance node args i r c = 
448 
match r with 
449 
 None > [] 
450 
 Some r > let g = translate_guard node args r in 
451 
[control_on_clock node args c (conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])] 
452  
453 
let translate_eq node ((m, si, j, d, s) as args) eq = 
454 
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) 
455 
match eq.eq_lhs, eq.eq_rhs.expr_desc with 
456 
 [x], Expr_arrow (e1, e2) > 
457 
let var_x = get_node_var x node in 
458 
let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in 
459 
let c1 = translate_expr node args e1 in 
460 
let c2 = translate_expr node args e2 in 
461 
(m, 
462 
mkinstr (MReset o) :: si, 
463 
Utils.IMap.add o (arrow_top_decl, []) j, 
464 
d, 
465 
(control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s) 
466 
 [x], Expr_pre e1 when VSet.mem (get_node_var x node) d > 
467 
let var_x = get_node_var x node in 
468 
(VSet.add var_x m, 
469 
si, 
470 
j, 
471 
d, 
472 
control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1))) :: s) 
473 
 [x], Expr_fby (e1, e2) when VSet.mem (get_node_var x node) d > 
474 
let var_x = get_node_var x node in 
475 
(VSet.add var_x m, 
476 
mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1)) :: si, 
477 
j, 
478 
d, 
479 
control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e2))) :: s) 
480  
481 
 p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) > 
482 
let var_p = List.map (fun v > get_node_var v node) p in 
483 
let el = expr_list_of_expr arg in 
484 
let vl = List.map (translate_expr node args) el in 
485 
let node_f = node_from_name f in 
486 
let call_f = 
487 
node_f, 
488 
NodeDep.filter_static_inputs (node_inputs node_f) el in 
489 
let o = new_instance node node_f eq.eq_rhs.expr_tag in 
490 
let env_cks = List.fold_right (fun arg cks > arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in 
491 
let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in 
492 
(*Clocks.new_var true in 
493 
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; 
494 
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;*) 
495 
(m, 
496 
(if Stateless.check_node node_f then si else mkinstr (MReset o) :: si), 
497 
Utils.IMap.add o call_f j, 
498 
d, 
499 
(if Stateless.check_node node_f 
500 
then [] 
501 
else reset_instance node args o r call_ck) @ 
502 
(control_on_clock node args call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s) 
503 
(* 
504 
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) 
505 
are preserved. While they are replaced as if g then x = t else x = e in C or Java 
506 
backends. *) 
507 
 [x], Expr_ite (c, t, e) 
508 
when (match !Options.output with  "horn" > true  "C"  "java"  _ > false) 
509 
> 
510 
let var_x = get_node_var x node in 
511 
(m, 
512 
si, 
513 
j, 
514 
d, 
515 
(control_on_clock node args eq.eq_rhs.expr_clock 
516 
(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s) 
517 
) 
518  
519 
*) 
520 
 [x], _ > ( 
521 
let var_x = get_node_var x node in 
522 
(m, si, j, d, 
523 
control_on_clock 
524 
node 
525 
args 
526 
eq.eq_rhs.expr_clock 
527 
(translate_act node args (var_x, eq.eq_rhs)) :: s 
528 
) 
529 
) 
530 
 _ > 
531 
begin 
532 
Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq; 
533 
assert false 
534 
end 
535  
536 
let find_eq xl eqs = 
537 
let rec aux accu eqs = 
538 
match eqs with 
539 
 [] > 
540 
begin 
541 
Format.eprintf "Looking for variables %a in the following equations@.%a@." 
542 
(Utils.fprintf_list ~sep:" , " (fun fmt v > Format.fprintf fmt "%s" v)) xl 
543 
Printers.pp_node_eqs eqs; 
544 
assert false 
545 
end 
546 
 hd::tl > 
547 
if List.exists (fun x > List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl 
548 
in 
549 
aux [] eqs 
550  
551 
(* Sort the set of equations of node [nd] according 
552 
to the computed schedule [sch] 
553 
*) 
554 
let sort_equations_from_schedule nd sch = 
555 
(* Format.eprintf "%s schedule: %a@." *) 
556 
(* nd.node_id *) 
557 
(* (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *) 
558 
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in 
559 
let eqs_rev, remainder = 
560 
List.fold_left 
561 
(fun (accu, node_eqs_remainder) vl > 
562 
if List.exists (fun eq > List.exists (fun v > List.mem v eq.eq_lhs) vl) accu 
563 
then 
564 
(accu, node_eqs_remainder) 
565 
else 
566 
let eq_v, remainder = find_eq vl node_eqs_remainder in 
567 
eq_v::accu, remainder 
568 
) 
569 
([], split_eqs) 
570 
sch 
571 
in 
572 
begin 
573 
if List.length remainder > 0 then ( 
574 
Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?" 
575 
Printers.pp_node_eqs remainder 
576 
Printers.pp_node_eqs (get_node_eqs nd); 
577 
assert false); 
578 
List.rev eqs_rev 
579 
end 
580  
581 
let constant_equations nd = 
582 
List.fold_right (fun vdecl eqs > 
583 
if vdecl.var_dec_const 
584 
then 
585 
{ eq_lhs = [vdecl.var_id]; 
586 
eq_rhs = Utils.desome vdecl.var_dec_value; 
587 
eq_loc = vdecl.var_loc 
588 
} :: eqs 
589 
else eqs) 
590 
nd.node_locals [] 
591  
592 
let translate_eqs node args eqs = 
593 
List.fold_right (fun eq args > translate_eq node args eq) eqs args;; 
594  
595 
let translate_decl nd sch = 
596 
(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*) 
597  
598 
let sorted_eqs = sort_equations_from_schedule nd sch in 
599 
let constant_eqs = constant_equations nd in 
600  
601 
(* In case of non functional backend (eg. C), additional local variables have 
602 
to be declared for each assert *) 
603 
let new_locals, assert_instrs, nd_node_asserts = 
604 
let exprl = List.map (fun assert_ > assert_.assert_expr ) nd.node_asserts in 
605 
if Backends.is_functional () then 
606 
[], [], exprl 
607 
else (* Each assert(e) is associated to a fresh variable v and declared as 
608 
v=e; assert (v); *) 
609 
let _, vars, eql, assertl = 
610 
List.fold_left (fun (i, vars, eqlist, assertlist) expr > 
611 
let loc = expr.expr_loc in 
612 
let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in 
613 
let assert_var = 
614 
mkvar_decl 
615 
loc 
616 
~orig:false (* fresh var *) 
617 
(var_id, 
618 
mktyp loc Tydec_bool, 
619 
mkclock loc Ckdec_any, 
620 
false, (* not a constant *) 
621 
None (* no default value *) 
622 
) 
623 
in 
624 
assert_var.var_type < Types.new_ty (Types.Tbool); 
625 
let eq = mkeq loc ([var_id], expr) in 
626 
(i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist) 
627 
) (1, [], [], []) exprl 
628 
in 
629 
vars, eql, assertl 
630 
in 
631 
let locals_list = nd.node_locals @ new_locals in 
632  
633 
let nd = { nd with node_locals = locals_list } in 
634 
let init_args = VSet.empty, [], Utils.IMap.empty, List.fold_right (fun l > VSet.add l) locals_list VSet.empty, [] in 
635 
(* memories, init instructions, node calls, local variables (including memories), step instrs *) 
636 
let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in 
637 
assert (VSet.is_empty m0); 
638 
assert (init0 = []); 
639 
assert (Utils.IMap.is_empty j0); 
640 
let m, init, j, locals, s as context_with_asserts = translate_eqs nd (m0, init0, j0, locals0, []) (assert_instrs@sorted_eqs) in 
641 
let mmap = Utils.IMap.fold (fun i n res > (i, n)::res) j [] in 
642 
{ 
643 
mname = nd; 
644 
mmemory = VSet.elements m; 
645 
mcalls = mmap; 
646 
minstances = List.filter (fun (_, (n,_)) > not (Stateless.check_node n)) mmap; 
647 
minit = init; 
648 
mconst = s0; 
649 
mstatic = List.filter (fun v > v.var_dec_const) nd.node_inputs; 
650 
mstep = { 
651 
step_inputs = nd.node_inputs; 
652 
step_outputs = nd.node_outputs; 
653 
step_locals = VSet.elements (VSet.diff locals m); 
654 
step_checks = List.map (fun d > d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks; 
655 
step_instrs = ( 
656 
(* special treatment depending on the active backend. For horn backend, 
657 
common branches are not merged while they are in C or Java 
658 
backends. *) 
659 
(*match !Options.output with 
660 
 "horn" > s 
661 
 "C"  "java"  _ >*) 
662 
if !Backends.join_guards then 
663 
join_guards_list s 
664 
else 
665 
s 
666 
); 
667 
step_asserts = List.map (translate_expr nd context_with_asserts) nd_node_asserts; 
668 
}; 
669 
mspec = nd.node_spec; 
670 
mannot = nd.node_annot; 
671 
} 
672  
673 
(** takes the global declarations and the scheduling associated to each node *) 
674 
let translate_prog decls node_schs = 
675 
let nodes = get_nodes decls in 
676 
List.map 
677 
(fun decl > 
678 
let node = node_of_top decl in 
679 
let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in 
680 
translate_decl node sch 
681 
) nodes 
682  
683 
let get_machine_opt name machines = 
684 
List.fold_left 
685 
(fun res m > 
686 
match res with 
687 
 Some _ > res 
688 
 None > if m.mname.node_id = name then Some m else None) 
689 
None machines 
690  
691 
let get_const_assign m id = 
692 
try 
693 
match get_instr_desc (List.find 
694 
(fun instr > match get_instr_desc instr with 
695 
 MLocalAssign (v, _) > v == id 
696 
 _ > false) 
697 
m.mconst 
698 
) with 
699 
 MLocalAssign (_, e) > e 
700 
 _ > assert false 
701 
with Not_found > assert false 
702  
703  
704 
let value_of_ident loc m id = 
705 
(* is is a state var *) 
706 
try 
707 
let v = List.find (fun v > v.var_id = id) m.mmemory 
708 
in mk_val (StateVar v) v.var_type 
709 
with Not_found > 
710 
try (* id is a node var *) 
711 
let v = get_node_var id m.mname 
712 
in mk_val (LocalVar v) v.var_type 
713 
with Not_found > 
714 
try (* id is a constant *) 
715 
let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)) 
716 
in mk_val (LocalVar c) c.var_type 
717 
with Not_found > 
718 
(* id is a tag *) 
719 
let t = Const_tag id 
720 
in mk_val (Cst t) (Typing.type_const loc t) 
721  
722 
(* type of internal fun used in dimension expression *) 
723 
let type_of_value_appl f args = 
724 
if List.mem f Basic_library.arith_funs 
725 
then (List.hd args).value_type 
726 
else Type_predef.type_bool 
727  
728 
let rec value_of_dimension m dim = 
729 
match dim.Dimension.dim_desc with 
730 
 Dimension.Dbool b > 
731 
mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool 
732 
 Dimension.Dint i > 
733 
mk_val (Cst (Const_int i)) Type_predef.type_int 
734 
 Dimension.Dident v > value_of_ident dim.Dimension.dim_loc m v 
735 
 Dimension.Dappl (f, args) > 
736 
let vargs = List.map (value_of_dimension m) args 
737 
in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) 
738 
 Dimension.Dite (i, t, e) > 
739 
(match List.map (value_of_dimension m) [i; t; e] with 
740 
 [vi; vt; ve] > mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type 
741 
 _ > assert false) 
742 
 Dimension.Dlink dim' > value_of_dimension m dim' 
743 
 _ > assert false 
744  
745 
let rec dimension_of_value value = 
746 
match value.value_desc with 
747 
 Cst (Const_tag t) when t = Corelang.tag_true > Dimension.mkdim_bool Location.dummy_loc true 
748 
 Cst (Const_tag t) when t = Corelang.tag_false > Dimension.mkdim_bool Location.dummy_loc false 
749 
 Cst (Const_int i) > Dimension.mkdim_int Location.dummy_loc i 
750 
 LocalVar v > Dimension.mkdim_ident Location.dummy_loc v.var_id 
751 
 Fun (f, args) > Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args) 
752 
 _ > assert false 
753  
754 
(* Local Variables: *) 
755 
(* compilecommand:"make C .." *) 
756 
(* End: *) 