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