lustrec / src / dot_backend.ml @ df647a81
History | View | Annotate | Download (4.33 KB)
1 |
open Format |
---|---|
2 |
open Corelang |
3 |
open Machine_code |
4 |
|
5 |
let pp_fun i = |
6 |
match i with |
7 |
| "ite" -> "ite" |
8 |
| "uminus" -> "uminus" |
9 |
| "not" -> "not" |
10 |
| "=" -> "equal" |
11 |
| "&&" -> "and" |
12 |
| "||" -> "or" |
13 |
| "impl" -> "impl" |
14 |
| "xor" -> "xor" |
15 |
| "!=" -> "different" |
16 |
| "mod" -> "mod" |
17 |
| ">" -> "gt" |
18 |
| "<" -> "lt" |
19 |
| ">=" -> "gte" |
20 |
| "<=" -> "lte" |
21 |
| _ -> Printf.printf "%s\n" i;assert false |
22 |
|
23 |
let rec print_instr_dep instances name fmt instr = |
24 |
match instr with |
25 |
| MReset i -> () |
26 |
| MLocalAssign (i,v) -> () |
27 |
| MStateAssign (i,v) -> () |
28 |
| MStep (il, i, vl) -> |
29 |
let name' = try node_name (fst (List.assoc i instances)) with Not_found -> pp_fun i in |
30 |
Format.fprintf fmt " %s -> %s;" name name' |
31 |
| MBranch (g,hl) -> () |
32 |
|
33 |
let print_machine_dep fmt m = |
34 |
Format.fprintf fmt "%s [color=red];@.%a" |
35 |
m.mname.node_id |
36 |
(Utils.fprintf_list ~sep:"@." (print_instr_dep m.minstances m.mname.node_id)) m.mstep.step_instrs |
37 |
|
38 |
(* |
39 |
let rec print_instr_struct instances name fmt instr = |
40 |
match instr with |
41 |
| MReset i -> () |
42 |
| MLocalAssign (i,v) -> () |
43 |
| MStateAssign (i,v) -> () |
44 |
| MStep (il, i, vl) -> |
45 |
let name' = try node_name (fst (List.assoc i instances)) with Not_found -> pp_fun i in |
46 |
Format.fprintf fmt " %s -> %s;@." name name' |
47 |
| MBranch (g,hl) -> () |
48 |
|
49 |
let rec translate_expr vars ((m, si, j, d, s) as args) expr = |
50 |
match expr.expr_desc with |
51 |
| Expr_const v -> Cst v |
52 |
| Expr_ident x -> translate_ident vars args x |
53 |
| Expr_array el -> Array (List.map (translate_expr vars args) el) |
54 |
| Expr_access (t, i) -> Access (translate_expr vars args t, translate_expr vars args (expr_of_dimension i)) |
55 |
| Expr_power (e, n) -> Power (translate_expr vars args e, translate_expr vars args (expr_of_dimension n)) |
56 |
| Expr_tuple _ |
57 |
| Expr_arrow _ |
58 |
| Expr_fby _ |
59 |
| Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) |
60 |
| Expr_when (e1, _, _) -> translate_expr vars args e1 |
61 |
| Expr_merge (x, _) -> raise NormalizationError |
62 |
| Expr_appl (id, e, _) when Basic_library.is_internal_fun id -> |
63 |
let nd = node_from_name id in |
64 |
(match e.expr_desc with |
65 |
| Expr_tuple el -> Fun (node_name nd, List.map (translate_expr vars args) el) |
66 |
| _ -> Fun (node_name nd, [translate_expr vars args e])) |
67 |
| Expr_ite (g,t,e) -> ( |
68 |
(* special treatment depending on the active backend. For horn backend or |
69 |
acsl spec, ite are preserved in expression. While they are removed for C |
70 |
or Java backends. *) |
71 |
Fun ("ite", [translate_expr vars args g; translate_expr vars args t; translate_expr vars args e]) |
72 |
) |
73 |
| _ -> raise NormalizationError |
74 |
|
75 |
|
76 |
let nd = match top.top_decl_desc with Node nd -> nd | _ -> assert false in |
77 |
|
78 |
List.map (fun d -> d.Dimension.dim_loc, translate_expr (node_vars nd) init_args (expr_of_dimension d)) nd.node_checks; |
79 |
*) |
80 |
|
81 |
let print_machine_struct orig dest fmt m = |
82 |
Format.fprintf fmt "subgraph cluster_%s {@.label = \"%s\"@.}@." m.mname.node_id m.mname.node_id |
83 |
|
84 |
(* |
85 |
digraph G { |
86 |
subgraph cluster_0 { |
87 |
style=filled; |
88 |
color=lightgrey; |
89 |
node [style=filled,color=white]; |
90 |
a0 -> a1 -> a2 -> a3; |
91 |
label = "process #1"; |
92 |
} |
93 |
|
94 |
subgraph cluster_1 { |
95 |
node [style=filled]; |
96 |
b0 -> b1 -> b2 -> b3; |
97 |
label = "process #2"; |
98 |
color=blue |
99 |
} |
100 |
start -> a0; |
101 |
start -> b0; |
102 |
a1 -> b3; |
103 |
b2 -> a3; |
104 |
a3 -> a0; |
105 |
a3 -> end; |
106 |
b3 -> end; |
107 |
|
108 |
start [shape=Mdiamond]; |
109 |
end [shape=Msquare]; |
110 |
} |
111 |
*) |
112 |
let translate_to_dep destname basename prog machines = |
113 |
let source_file = destname ^ "_dep.dot" in |
114 |
let source_out = open_out source_file in |
115 |
let fmt = formatter_of_out_channel source_out in |
116 |
Format.fprintf fmt "digraph %s {@.%a}@." basename (Utils.fprintf_list ~sep:"@." print_machine_dep) machines |
117 |
|
118 |
let translate_to_struct destname basename prog machines = () (* |
119 |
let source_file = destname ^ "_struct.dot" in |
120 |
let source_out = open_out source_file in |
121 |
let fmt = formatter_of_out_channel source_out in |
122 |
Format.fprintf fmt "digraph %s {@.%a}@." basename (Utils.fprintf_list ~sep:"" (print_machine_struct "input" "output")) (get_nodes prog)*) |
123 |
|
124 |
let translate destname basename prog machines = |
125 |
translate_to_dep destname basename prog machines; |
126 |
translate_to_struct destname basename prog machines |
127 |
|
128 |
|
129 |
(* Local Variables: *) |
130 |
(* compile-command:"make -C .." *) |
131 |
(* End: *) |