Revision 58272238
Added by Teme Kahsai almost 10 years ago
src/machine_code.ml | ||
---|---|---|
21 | 21 |
|
22 | 22 |
module ISet = Set.Make(OrdVarDecl) |
23 | 23 |
|
24 |
type value_t =
|
|
24 |
type value_t = |
|
25 | 25 |
| Cst of constant |
26 | 26 |
| LocalVar of var_decl |
27 | 27 |
| StateVar of var_decl |
28 |
| Fun of ident * value_t list
|
|
28 |
| Fun of ident * value_t list |
|
29 | 29 |
| Array of value_t list |
30 | 30 |
| Access of value_t * value_t |
31 | 31 |
| Power of value_t * value_t |
... | ... | |
36 | 36 |
| MReset of ident |
37 | 37 |
| MStep of var_decl list * ident * value_t list |
38 | 38 |
| MBranch of value_t * (label * instr_t list) list |
39 |
|
|
39 |
|
|
40 | 40 |
let rec pp_val fmt v = |
41 | 41 |
match v with |
42 |
| Cst c -> Printers.pp_const fmt c
|
|
42 |
| Cst c -> Printers.pp_const fmt c |
|
43 | 43 |
| LocalVar v -> Format.pp_print_string fmt v.var_id |
44 | 44 |
| StateVar v -> Format.pp_print_string fmt v.var_id |
45 | 45 |
| Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl |
... | ... | |
48 | 48 |
| Fun (n, vl) -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl |
49 | 49 |
|
50 | 50 |
let rec pp_instr fmt i = |
51 |
match i with
|
|
51 |
match i with |
|
52 | 52 |
| MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v |
53 | 53 |
| MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v |
54 | 54 |
| MReset i -> Format.fprintf fmt "reset %s" i |
55 | 55 |
| MStep (il, i, vl) -> |
56 | 56 |
Format.fprintf fmt "%a = %s (%a)" |
57 | 57 |
(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il |
58 |
i
|
|
58 |
i |
|
59 | 59 |
(Utils.fprintf_list ~sep:", " pp_val) vl |
60 | 60 |
| MBranch (g,hl) -> |
61 | 61 |
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]" |
... | ... | |
104 | 104 |
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args |
105 | 105 |
|
106 | 106 |
let pp_machine fmt m = |
107 |
Format.fprintf fmt
|
|
107 |
Format.fprintf fmt |
|
108 | 108 |
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ " |
109 | 109 |
m.mname.node_id |
110 | 110 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory |
... | ... | |
264 | 264 |
List.fold_right join_guards insts [] |
265 | 265 |
|
266 | 266 |
(* specialize predefined (polymorphic) operators |
267 |
wrt their instances, so that the C semantics
|
|
267 |
wrt their instances, so that the C semantics |
|
268 | 268 |
is preserved *) |
269 | 269 |
let specialize_to_c expr = |
270 | 270 |
match expr.expr_desc with |
... | ... | |
293 | 293 |
| Expr_access (t, i) -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i)) |
294 | 294 |
| Expr_power (e, n) -> Power (translate_expr node args e, translate_expr node args (expr_of_dimension n)) |
295 | 295 |
| Expr_tuple _ |
296 |
| Expr_arrow _
|
|
296 |
| Expr_arrow _ |
|
297 | 297 |
| Expr_fby _ |
298 | 298 |
| Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) |
299 | 299 |
| Expr_when (e1, _, _) -> translate_expr node args e1 |
... | ... | |
305 | 305 |
(* special treatment depending on the active backend. For horn backend, ite |
306 | 306 |
are preserved in expression. While they are removed for C or Java |
307 | 307 |
backends. *) |
308 |
match !Options.output with | "horn" ->
|
|
308 |
match !Options.output with | "horn" -> |
|
309 | 309 |
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e]) |
310 |
| "C" | "java" | _ ->
|
|
310 |
| "C" | "java" | _ -> |
|
311 | 311 |
(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) |
312 | 312 |
) |
313 | 313 |
| _ -> raise NormalizationError |
... | ... | |
323 | 323 |
conditional g [translate_act node args (y, t)] |
324 | 324 |
[translate_act node args (y, e)] |
325 | 325 |
| Expr_merge (x, hl) -> MBranch (translate_ident node args x, List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl) |
326 |
| _ ->
|
|
326 |
| _ -> |
|
327 | 327 |
MLocalAssign (y, translate_expr node args expr) |
328 | 328 |
|
329 | 329 |
let reset_instance node args i r c = |
... | ... | |
367 | 367 |
let node_f = node_from_name f in |
368 | 368 |
let call_f = |
369 | 369 |
node_f, |
370 |
NodeDep.filter_static_inputs (node_inputs node_f) el in
|
|
370 |
NodeDep.filter_static_inputs (node_inputs node_f) el in |
|
371 | 371 |
let o = new_instance node node_f eq.eq_rhs.expr_tag in |
372 | 372 |
let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in |
373 | 373 |
let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in |
... | ... | |
386 | 386 |
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) |
387 | 387 |
are preserved. While they are replaced as if g then x = t else x = e in C or Java |
388 | 388 |
backends. *) |
389 |
| [x], Expr_ite (c, t, e)
|
|
389 |
| [x], Expr_ite (c, t, e) |
|
390 | 390 |
when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false) |
391 |
->
|
|
391 |
-> |
|
392 | 392 |
let var_x = get_node_var x node in |
393 |
(m,
|
|
394 |
si,
|
|
395 |
j,
|
|
396 |
d,
|
|
397 |
(control_on_clock node args eq.eq_rhs.expr_clock
|
|
393 |
(m, |
|
394 |
si, |
|
395 |
j, |
|
396 |
d, |
|
397 |
(control_on_clock node args eq.eq_rhs.expr_clock |
|
398 | 398 |
(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s) |
399 | 399 |
) |
400 |
|
|
400 |
|
|
401 | 401 |
| [x], _ -> ( |
402 | 402 |
let var_x = get_node_var x node in |
403 |
(m, si, j, d,
|
|
404 |
control_on_clock
|
|
403 |
(m, si, j, d, |
|
404 |
control_on_clock |
|
405 | 405 |
node |
406 | 406 |
args |
407 | 407 |
eq.eq_rhs.expr_clock |
... | ... | |
424 | 424 |
Printers.pp_node_eqs eqs; |
425 | 425 |
assert false |
426 | 426 |
end |
427 |
| hd::tl ->
|
|
427 |
| hd::tl -> |
|
428 | 428 |
if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl |
429 | 429 |
in |
430 | 430 |
aux [] eqs |
431 | 431 |
|
432 |
(* Sort the set of equations of node [nd] according
|
|
432 |
(* Sort the set of equations of node [nd] according |
|
433 | 433 |
to the computed schedule [sch] |
434 | 434 |
*) |
435 | 435 |
let sort_equations_from_schedule nd sch = |
... | ... | |
438 | 438 |
(Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*) |
439 | 439 |
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in |
440 | 440 |
let eqs_rev, remainder = |
441 |
List.fold_left
|
|
442 |
(fun (accu, node_eqs_remainder) vl ->
|
|
441 |
List.fold_left |
|
442 |
(fun (accu, node_eqs_remainder) vl -> |
|
443 | 443 |
if List.exists (fun eq -> List.exists (fun v -> List.mem v eq.eq_lhs) vl) accu |
444 | 444 |
then |
445 | 445 |
(accu, node_eqs_remainder) |
446 | 446 |
else |
447 | 447 |
let eq_v, remainder = find_eq vl node_eqs_remainder in |
448 | 448 |
eq_v::accu, remainder |
449 |
)
|
|
450 |
([], split_eqs)
|
|
451 |
sch
|
|
449 |
) |
|
450 |
([], split_eqs) |
|
451 |
sch |
|
452 | 452 |
in |
453 | 453 |
begin |
454 | 454 |
if List.length remainder > 0 then ( |
... | ... | |
491 | 491 |
| "horn" -> s |
492 | 492 |
| "C" | "java" | _ -> join_guards_list s |
493 | 493 |
); |
494 |
step_asserts =
|
|
494 |
step_asserts = |
|
495 | 495 |
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in |
496 | 496 |
List.map (translate_expr nd init_args) exprl |
497 | 497 |
; |
... | ... | |
502 | 502 |
|
503 | 503 |
(** takes the global delcarations and the scheduling associated to each node *) |
504 | 504 |
let translate_prog decls node_schs = |
505 |
let nodes = get_nodes decls in
|
|
506 |
List.map
|
|
507 |
(fun decl ->
|
|
505 |
let nodes = get_nodes decls in |
|
506 |
List.map |
|
507 |
(fun decl -> |
|
508 | 508 |
let node = node_of_top decl in |
509 | 509 |
let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in |
510 |
translate_decl node sch
|
|
510 |
translate_decl node sch |
|
511 | 511 |
) nodes |
512 | 512 |
|
513 |
let get_machine_opt name machines =
|
|
514 |
List.fold_left
|
|
515 |
(fun res m ->
|
|
516 |
match res with
|
|
517 |
| Some _ -> res
|
|
513 |
let get_machine_opt name machines = |
|
514 |
List.fold_left |
|
515 |
(fun res m -> |
|
516 |
match res with |
|
517 |
| Some _ -> res |
|
518 | 518 |
| None -> if m.mname.node_id = name then Some m else None) |
519 | 519 |
None machines |
520 |
|
|
520 |
|
|
521 | 521 |
|
522 | 522 |
(* Local Variables: *) |
523 | 523 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff
modifed / to div in horn backend