Revision 3ca27bc7 src/machine_code.ml
src/machine_code.ml  

43  43 
 Fun (n, vl) > Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl 
44  44  
45  45 
let rec pp_instr fmt i = 
46 
match i with 

46 
match i.instr_desc with


47  47 
 MLocalAssign (i,v) > Format.fprintf fmt "%s<l %a" i.var_id pp_val v 
48  48 
 MStateAssign (i,v) > Format.fprintf fmt "%s<s %a" i.var_id pp_val v 
49  49 
 MReset i > Format.fprintf fmt "reset %s" i 
...  ...  
149  149 
let is_memory m id = 
150  150 
List.exists (fun o > o.var_id = id.var_id) m.mmemory 
151  151  
152 
let conditional c t e = 

153 
MBranch(c, [ (tag_true, t); (tag_false, e) ])


152 
let conditional (* TODO ?(lustre_expr:expr option=None) *) c t e =


153 
mkinstr (* TODO ?lustre_expr *) (MBranch(c, [ (tag_true, t); (tag_false, e) ]))


154  154  
155  155 
let dummy_var_decl name typ = 
156  156 
{ 
...  ...  
211  211 
mmemory = [var_state]; 
212  212 
mcalls = []; 
213  213 
minstances = []; 
214 
minit = [MStateAssign(var_state, cst true)];


214 
minit = [mkinstr (MStateAssign(var_state, cst true))];


215  215 
mstatic = []; 
216  216 
mconst = []; 
217  217 
mstep = { 
...  ...  
220  220 
step_locals = []; 
221  221 
step_checks = []; 
222  222 
step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool) 
223 
[MStateAssign(var_state, cst false); 

224 
MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)] 

225 
[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)] ]; 

223 
(List.map mkinstr 

224 
[MStateAssign(var_state, cst false); 

225 
MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)]) 

226 
(List.map mkinstr 

227 
[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)]) ]; 

226  228 
step_asserts = []; 
227  229 
}; 
228  230 
mspec = None; 
...  ...  
314  316 
match (Clocks.repr ck).cdesc with 
315  317 
 Con (ck1, cr, l) > 
316  318 
let id = Clocks.const_of_carrier cr in 
317 
control_on_clock node args ck1 (MBranch (translate_ident node args id, 

318 
[l, [inst]] )) 

319 
control_on_clock node args ck1 (mkinstr 

320 
(* TODO il faudrait prendre le lustre 

321 
associé à instr et rajouter print_ck_suffix 

322 
ck) de clocks.ml *) 

323 
(MBranch (translate_ident node args id, 

324 
[l, [inst]] ))) 

319  325 
 _ > inst 
320  326  
321  327 
let rec join_branches hl1 hl2 = 
...  ...  
328  334 
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2 
329  335  
330  336 
and join_guards inst1 insts2 = 
331 
match inst1, insts2 with


337 
match get_instr_desc inst1, List.map get_instr_desc insts2 with


332  338 
 _ , [] > 
333  339 
[inst1] 
334  340 
 MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 > 
335 
MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)) 

336 
:: q 

341 
mkinstr 

342 
(* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *) 

343 
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2))) 

344 
:: (List.tl insts2) 

337  345 
 _ > inst1 :: insts2 
338  346  
339  347 
let join_guards_list insts = 
...  ...  
403  411 
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = 
404  412 
match expr.expr_desc with 
405  413 
 Expr_ite (c, t, e) > let g = translate_guard node args c in 
406 
conditional g 

414 
conditional (* TODO ?lustre_expr:(Some expr) *) g


407  415 
[translate_act node args (y, t)] 
408  416 
[translate_act node args (y, e)] 
409 
 Expr_merge (x, hl) > MBranch (translate_ident node args x, 

410 
List.map (fun (t, h) > t, [translate_act node args (y, h)]) hl) 

411 
 _ > MLocalAssign (y, translate_expr node args expr)


417 
 Expr_merge (x, hl) > mkinstr (* TODO ?lustre_expr:(Some expr) *) (MBranch (translate_ident node args x,


418 
List.map (fun (t, h) > t, [translate_act node args (y, h)]) hl))


419 
 _ > mkinstr (* TODO ?lustre_expr:(Some expr) *) (MLocalAssign (y, translate_expr node args expr))


412  420  
413  421 
let reset_instance node args i r c = 
414  422 
match r with 
415  423 
 None > [] 
416  424 
 Some r > let g = translate_guard node args r in 
417 
[control_on_clock node args c (conditional g [MReset i] [MNoReset i])]


425 
[control_on_clock node args c (conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])]


418  426  
419  427 
let translate_eq node ((m, si, j, d, s) as args) eq = 
420  428 
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) 
...  ...  
425  433 
let c1 = translate_expr node args e1 in 
426  434 
let c2 = translate_expr node args e2 in 
427  435 
(m, 
428 
MReset o :: si,


436 
mkinstr (MReset o) :: si,


429  437 
Utils.IMap.add o (arrow_top_decl, []) j, 
430  438 
d, 
431 
(control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)


439 
(control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:eq *) (MStep ([var_x], o, [c1;c2])))) :: s)


432  440 
 [x], Expr_pre e1 when ISet.mem (get_node_var x node) d > 
433  441 
let var_x = get_node_var x node in 
434  442 
(ISet.add var_x m, 
435  443 
si, 
436  444 
j, 
437  445 
d, 
438 
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)


446 
control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e1))) :: s)


439  447 
 [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d > 
440  448 
let var_x = get_node_var x node in 
441  449 
(ISet.add var_x m, 
442 
MStateAssign (var_x, translate_expr node args e1) :: si,


450 
mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e1)) :: si,


443  451 
j, 
444  452 
d, 
445 
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)


453 
control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e2))) :: s)


446  454  
447  455 
 p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) > 
448  456 
let var_p = List.map (fun v > get_node_var v node) p in 
...  ...  
459  467 
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; 
460  468 
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;*) 
461  469 
(m, 
462 
(if Stateless.check_node node_f then si else MReset o :: si),


470 
(if Stateless.check_node node_f then si else mkinstr (MReset o) :: si),


463  471 
Utils.IMap.add o call_f j, 
464  472 
d, 
465  473 
(if Stateless.check_node node_f 
466  474 
then [] 
467  475 
else reset_instance node args o r call_ck) @ 
468 
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)


476 
(control_on_clock node args call_ck (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStep (var_p, o, vl)))) :: s)


469  477 
(* 
470  478 
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) 
471  479 
are preserved. While they are replaced as if g then x = t else x = e in C or Java 
...  ...  
656  664  
657  665 
let get_const_assign m id = 
658  666 
try 
659 
match (List.find (fun instr > match instr with MLocalAssign (v, _) > v == id  _ > false) m.mconst) with 

667 
match get_instr_desc (List.find 

668 
(fun instr > match get_instr_desc instr with 

669 
 MLocalAssign (v, _) > v == id 

670 
 _ > false) 

671 
m.mconst 

672 
) with 

660  673 
 MLocalAssign (_, e) > e 
661  674 
 _ > assert false 
662  675 
with Not_found > assert false 
Also available in: Unified diff