## 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: *) |