lustrec / src / backends / Horn / horn_backend_traces.ml @ 86ae18b7
History | View | Annotate | Download (6.21 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(********************************************************************) |
11 |
|
12 |
(* The compilation presented here was first defined in Garoche, Gurfinkel, |
13 |
Kahsai, HCSV'14. |
14 |
|
15 |
This is a modified version that handle reset |
16 |
*) |
17 |
|
18 |
open Format |
19 |
open LustreSpec |
20 |
open Corelang |
21 |
open Machine_code |
22 |
|
23 |
open Horn_backend_common |
24 |
open Horn_backend_printers |
25 |
|
26 |
(* Compute memories associated to each machine *) |
27 |
let compute_mems machines m = |
28 |
let rec aux fst prefix m = |
29 |
(List.map (fun mem -> (prefix, mem)) m.mmemory) @ |
30 |
List.fold_left (fun accu (id, (n, _)) -> |
31 |
let name = node_name n in |
32 |
if name = "_arrow" then accu else |
33 |
let machine_n = get_machine machines name in |
34 |
( aux false ((id,machine_n)::prefix) machine_n ) |
35 |
@ accu |
36 |
) [] m.minstances |
37 |
in |
38 |
aux true [] m |
39 |
|
40 |
|
41 |
(* We extract the annotation dealing with traceability *) |
42 |
let machines_traces machines = |
43 |
List.map (fun m -> |
44 |
let traces : (ident * expr) list= |
45 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
46 |
let filtered = |
47 |
List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots |
48 |
in |
49 |
let content = List.map snd filtered in |
50 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
51 |
List.map (fun ee -> |
52 |
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with |
53 |
| [], Expr_tuple [v;e] -> ( |
54 |
match v.expr_desc with |
55 |
| Expr_ident vid -> vid, e |
56 |
| _ -> assert false ) |
57 |
| _ -> assert false) |
58 |
content |
59 |
in |
60 |
|
61 |
m, traces |
62 |
|
63 |
) machines |
64 |
|
65 |
let memories_old machines m = |
66 |
List.map (fun (p, v) -> |
67 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
68 |
let traces = List.assoc machine (machines_traces machines) in |
69 |
if List.mem_assoc v.var_id traces then |
70 |
( |
71 |
(* We take the expression associated to variable v in the trace |
72 |
info *) |
73 |
|
74 |
(* eprintf "Found variable %a in traces: %a@." pp_var v |
75 |
Printers.pp_expr (List.assoc v.var_id traces); *) |
76 |
p, List.assoc v.var_id traces |
77 |
) |
78 |
else |
79 |
begin |
80 |
|
81 |
(* We keep the variable as is: we create an expression v *) |
82 |
|
83 |
(* eprintf "Unable to found variable %a in traces (%a)@." pp_var v |
84 |
(Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst |
85 |
traces); *) |
86 |
|
87 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
88 |
end |
89 |
|
90 |
) (compute_mems machines m) |
91 |
|
92 |
let memories_next machines m = (* We remove the topest pre in each expression *) |
93 |
List.map |
94 |
(fun (prefix, ee) -> |
95 |
match ee.expr_desc with |
96 |
| Expr_pre e -> prefix, e |
97 |
| _ -> eprintf |
98 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
99 |
(Utils.fprintf_list ~sep:"," |
100 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) |
101 |
(List.rev prefix) |
102 |
Printers.pp_expr ee; |
103 |
assert false) |
104 |
(memories_old machines m) |
105 |
|
106 |
|
107 |
|
108 |
let pp_prefix_rev fmt prefix = |
109 |
Utils.fprintf_list ~sep:"." |
110 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) |
111 |
fmt |
112 |
(List.rev prefix) |
113 |
|
114 |
|
115 |
let traces_file fmt basename prog machines = |
116 |
fprintf fmt "<?xml version=\"1.0\"?>@."; |
117 |
fprintf fmt "<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@."; |
118 |
fprintf fmt "@[<v 5>@ %a@ @]@." |
119 |
(Utils.fprintf_list ~sep:"@ " (fun fmt m -> |
120 |
let pp_var = pp_horn_var m in |
121 |
let memories_old = memories_old machines m in |
122 |
let memories_next = memories_next machines m in |
123 |
|
124 |
(* fprintf fmt "; Node %s@." m.mname.node_id; *) |
125 |
fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id; |
126 |
|
127 |
let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in |
128 |
let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in |
129 |
fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ " |
130 |
(Utils.fprintf_list ~sep:" | " (pp_horn_var m)) input_vars |
131 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) input_vars |
132 |
(Utils.fprintf_list ~sep:" | " (pp_horn_var m)) (m.mstep.step_inputs); |
133 |
|
134 |
fprintf fmt "<output name=\"%a\" type=\"%a\">%a</output>@ " |
135 |
(Utils.fprintf_list ~sep:" | " pp_var) output_vars |
136 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) output_vars |
137 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs); |
138 |
|
139 |
let init_local_vars = |
140 |
(rename_next_list |
141 |
(try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false)) |
142 |
|
143 |
|
144 |
in |
145 |
let step_local_vars = (rename_current_list (full_memory_vars ~without_arrow:true machines m)) in |
146 |
|
147 |
fprintf fmt "<localInit name=\"%a\" type=\"%a\">%t%a</localInit>@ " |
148 |
(Utils.fprintf_list ~sep:" | " pp_var) init_local_vars |
149 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) init_local_vars |
150 |
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "") |
151 |
(Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" Printers.pp_expr ee)) memories_next; |
152 |
|
153 |
fprintf fmt "<localStep name=\"%a\" type=\"%a\">%t%a</localStep>@ " |
154 |
(Utils.fprintf_list ~sep:" | " pp_var) step_local_vars |
155 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) step_local_vars |
156 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "") |
157 |
(Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)" |
158 |
Printers.pp_expr ee)) (memories_old); |
159 |
|
160 |
fprintf fmt "@]@ </Node>"; |
161 |
)) (List.rev machines); |
162 |
fprintf fmt "</Traces>@." |
163 |
|
164 |
|
165 |
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt |
166 |
"%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *) |
167 |
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt |
168 |
"%a(%a)" *) |
169 |
(* pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *) |
170 |
|
171 |
|
172 |
(* Local Variables: *) |
173 |
(* compile-command:"make -C ../.." *) |
174 |
(* End: *) |