Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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