Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/causality.ml | ||
---|---|---|
6 | 6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 | 7 |
(* under the terms of the GNU Lesser General Public License *) |
8 | 8 |
(* version 2.1. *) |
9 |
(* *)
|
|
9 |
(* *) |
|
10 | 10 |
(* This file was originally from the Prelude compiler *) |
11 |
(* *)
|
|
11 |
(* *) |
|
12 | 12 |
(********************************************************************) |
13 | 13 |
|
14 |
|
|
15 |
(** Simple modular syntactic causality analysis. Can reject correct |
|
16 |
programs, especially if the program is not flattened first. *) |
|
17 | 14 |
open Utils |
15 |
(** Simple modular syntactic causality analysis. Can reject correct programs, |
|
16 |
especially if the program is not flattened first. *) |
|
17 |
|
|
18 | 18 |
open Lustre_types |
19 | 19 |
open Corelang |
20 | 20 |
|
21 |
|
|
22 | 21 |
type identified_call = eq * tag |
22 |
|
|
23 | 23 |
type error = |
24 |
| DataCycle of ident list list (* multiple failed partitions at once *) |
|
24 |
| DataCycle of ident list list |
|
25 |
(* multiple failed partitions at once *) |
|
25 | 26 |
| NodeCycle of ident list |
26 | 27 |
|
27 | 28 |
exception Error of error |
28 | 29 |
|
30 |
(* Dependency of mem variables on mem variables is cut off by duplication of |
|
31 |
some mem vars into local node vars. Thus, cylic dependency errors may only |
|
32 |
arise between no-mem vars. non-mem variables are: - constants/inputs: not |
|
33 |
needed for causality/scheduling, needed only for detecting useless vars - |
|
34 |
read mems (fake vars): same remark as above. - outputs: decoupled from mems, |
|
35 |
if necessary - locals - instance vars (fake vars): simplify causality |
|
36 |
analysis |
|
29 | 37 |
|
30 |
|
|
31 |
(* Dependency of mem variables on mem variables is cut off |
|
32 |
by duplication of some mem vars into local node vars. |
|
33 |
Thus, cylic dependency errors may only arise between no-mem vars. |
|
34 |
non-mem variables are: |
|
35 |
- constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars |
|
36 |
- read mems (fake vars): same remark as above. |
|
37 |
- outputs: decoupled from mems, if necessary |
|
38 |
- locals |
|
39 |
- instance vars (fake vars): simplify causality analysis |
|
40 |
|
|
41 | 38 |
global constants are not part of the dependency graph. |
42 |
|
|
43 |
no_mem' = combinational(no_mem, mem); |
|
44 |
=> (mem -> no_mem' -> no_mem) |
|
45 |
|
|
46 |
mem' = pre(no_mem, mem); |
|
47 |
=> (mem' -> no_mem), (mem -> mem') |
|
48 |
|
|
49 |
Global roadmap: |
|
50 |
- compute two dep graphs g (non-mem/non-mem&mem) and g' (mem/mem) |
|
51 |
- check cycles in g (a cycle means a dependency error) |
|
52 |
- break cycles in g' (it's legal !): |
|
53 |
- check cycles in g' |
|
54 |
- if any, introduce aux var to break cycle, then start afresh |
|
55 |
- insert g' into g |
|
56 |
- return g |
|
57 |
*) |
|
39 |
|
|
40 |
no_mem' = combinational(no_mem, mem); => (mem -> no_mem' -> no_mem) |
|
41 |
|
|
42 |
mem' = pre(no_mem, mem); => (mem' -> no_mem), (mem -> mem') |
|
43 |
|
|
44 |
Global roadmap: - compute two dep graphs g (non-mem/non-mem&mem) and g' |
|
45 |
(mem/mem) - check cycles in g (a cycle means a dependency error) - break |
|
46 |
cycles in g' (it's legal !): - check cycles in g' - if any, introduce aux var |
|
47 |
to break cycle, then start afresh - insert g' into g - return g *) |
|
58 | 48 |
|
59 | 49 |
(* Tests whether [v] is a root of graph [g], i.e. a source *) |
60 |
let is_graph_root v g = |
|
61 |
IdentDepGraph.in_degree g v = 0 |
|
50 |
let is_graph_root v g = IdentDepGraph.in_degree g v = 0 |
|
62 | 51 |
|
63 | 52 |
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *) |
64 | 53 |
let graph_roots g = |
65 | 54 |
IdentDepGraph.fold_vertex |
66 |
(fun v roots -> if is_graph_root v g then v::roots else roots)
|
|
55 |
(fun v roots -> if is_graph_root v g then v :: roots else roots)
|
|
67 | 56 |
g [] |
68 | 57 |
|
69 | 58 |
let add_edges src tgt g = |
70 |
(*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*) |
|
71 |
List.iter |
|
72 |
(fun s -> List.iter (IdentDepGraph.add_edge g s) tgt) |
|
73 |
src; |
|
59 |
(*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) |
|
60 |
tgt) src;*) |
|
61 |
List.iter (fun s -> List.iter (IdentDepGraph.add_edge g s) tgt) src; |
|
74 | 62 |
g |
75 | 63 |
|
76 | 64 |
let add_vertices vtc g = |
77 |
(*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*) |
|
65 |
(*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)
|
|
78 | 66 |
List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc; |
79 | 67 |
g |
80 | 68 |
|
81 |
let new_graph () = |
|
82 |
IdentDepGraph.create () |
|
69 |
let new_graph () = IdentDepGraph.create () |
|
83 | 70 |
|
84 | 71 |
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *) |
85 | 72 |
let slice_graph gr v = |
86 |
begin |
|
87 |
let gr' = new_graph () in |
|
88 |
IdentDepGraph.add_vertex gr' v; |
|
89 |
Bfs.iter_component (fun v -> IdentDepGraph.iter_succ (fun s -> IdentDepGraph.add_vertex gr' s; IdentDepGraph.add_edge gr' v s) gr v) gr v; |
|
90 |
gr' |
|
91 |
end |
|
73 |
let gr' = new_graph () in |
|
74 |
IdentDepGraph.add_vertex gr' v; |
|
75 |
Bfs.iter_component |
|
76 |
(fun v -> |
|
77 |
IdentDepGraph.iter_succ |
|
78 |
(fun s -> |
|
79 |
IdentDepGraph.add_vertex gr' s; |
|
80 |
IdentDepGraph.add_edge gr' v s) |
|
81 |
gr v) |
|
82 |
gr v; |
|
83 |
gr' |
|
92 | 84 |
|
93 |
|
|
94 | 85 |
module ExprDep = struct |
95 | 86 |
let get_node_eqs nd = |
96 | 87 |
let eqs, auts = get_node_eqs nd in |
97 |
if auts != [] then assert false (* No call on causality on a Lustre model |
|
98 |
with automaton. They should be expanded by now. *); |
|
88 |
if auts != [] then assert false |
|
89 |
(* No call on causality on a Lustre model with automaton. They should be |
|
90 |
expanded by now. *); |
|
99 | 91 |
eqs |
100 |
|
|
92 |
|
|
101 | 93 |
let instance_var_cpt = ref 0 |
102 | 94 |
|
103 |
(* read vars represent input/mem read-only vars, |
|
104 |
they are not part of the program/schedule, |
|
105 |
as they are not assigned, |
|
106 |
but used to compute useless inputs/mems. |
|
107 |
a mem read var represents a mem at the beginning of a cycle *) |
|
108 |
let mk_read_var id = |
|
109 |
Format.sprintf "#%s" id |
|
110 |
|
|
111 |
(* instance vars represent node instance calls, |
|
112 |
they are not part of the program/schedule, |
|
113 |
but used to simplify causality analysis |
|
114 |
*) |
|
95 |
(* read vars represent input/mem read-only vars, they are not part of the |
|
96 |
program/schedule, as they are not assigned, but used to compute useless |
|
97 |
inputs/mems. a mem read var represents a mem at the beginning of a cycle *) |
|
98 |
let mk_read_var id = Format.sprintf "#%s" id |
|
99 |
|
|
100 |
(* instance vars represent node instance calls, they are not part of the |
|
101 |
program/schedule, but used to simplify causality analysis *) |
|
115 | 102 |
let mk_instance_var id = |
116 |
incr instance_var_cpt; Format.sprintf "!%s_%d" id !instance_var_cpt |
|
103 |
incr instance_var_cpt; |
|
104 |
Format.sprintf "!%s_%d" id !instance_var_cpt |
|
117 | 105 |
|
118 | 106 |
let is_read_var v = v.[0] = '#' |
119 | 107 |
|
... | ... | |
132 | 120 |
let eq_memory_variables mems eq = |
133 | 121 |
let rec match_mem lhs rhs mems = |
134 | 122 |
match rhs.expr_desc with |
135 |
| Expr_fby _ |
|
136 |
| Expr_pre _ -> List.fold_right ISet.add lhs mems |
|
137 |
| Expr_tuple tl -> |
|
138 |
let lhs' = (transpose_list [lhs]) in |
|
139 |
List.fold_right2 match_mem lhs' tl mems |
|
140 |
| _ -> mems in |
|
123 |
| Expr_fby _ | Expr_pre _ -> |
|
124 |
List.fold_right ISet.add lhs mems |
|
125 |
| Expr_tuple tl -> |
|
126 |
let lhs' = transpose_list [ lhs ] in |
|
127 |
List.fold_right2 match_mem lhs' tl mems |
|
128 |
| _ -> |
|
129 |
mems |
|
130 |
in |
|
141 | 131 |
match_mem eq.eq_lhs eq.eq_rhs mems |
142 | 132 |
|
143 | 133 |
let node_memory_variables nd = |
144 | 134 |
List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd) |
145 | 135 |
|
146 | 136 |
let node_input_variables nd = |
147 |
List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty
|
|
148 |
(if nd.node_iscontract then
|
|
149 |
nd.node_inputs@nd.node_outputs
|
|
150 |
else
|
|
151 |
nd.node_inputs)
|
|
152 |
|
|
137 |
List.fold_left |
|
138 |
(fun inputs v -> ISet.add v.var_id inputs)
|
|
139 |
ISet.empty
|
|
140 |
(if nd.node_iscontract then nd.node_inputs @ nd.node_outputs
|
|
141 |
else nd.node_inputs)
|
|
142 |
|
|
153 | 143 |
let node_output_variables nd = |
154 |
List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty |
|
144 |
List.fold_left |
|
145 |
(fun outputs v -> ISet.add v.var_id outputs) |
|
146 |
ISet.empty |
|
155 | 147 |
(if nd.node_iscontract then [] else nd.node_outputs) |
156 | 148 |
|
157 | 149 |
let node_local_variables nd = |
158 |
List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals |
|
150 |
List.fold_left |
|
151 |
(fun locals v -> ISet.add v.var_id locals) |
|
152 |
ISet.empty nd.node_locals |
|
159 | 153 |
|
160 | 154 |
let node_constant_variables nd = |
161 |
List.fold_left (fun locals v -> if v.var_dec_const then ISet.add v.var_id locals else locals) ISet.empty nd.node_locals |
|
155 |
List.fold_left |
|
156 |
(fun locals v -> |
|
157 |
if v.var_dec_const then ISet.add v.var_id locals else locals) |
|
158 |
ISet.empty nd.node_locals |
|
162 | 159 |
|
163 | 160 |
let node_auxiliary_variables nd = |
164 | 161 |
ISet.diff (node_local_variables nd) (node_memory_variables nd) |
165 | 162 |
|
166 | 163 |
let node_variables nd = |
167 | 164 |
let inputs = node_input_variables nd in |
168 |
let inoutputs = List.fold_left (fun inoutputs v -> ISet.add v.var_id inoutputs) inputs nd.node_outputs in |
|
169 |
List.fold_left (fun vars v -> ISet.add v.var_id vars) inoutputs nd.node_locals |
|
165 |
let inoutputs = |
|
166 |
List.fold_left |
|
167 |
(fun inoutputs v -> ISet.add v.var_id inoutputs) |
|
168 |
inputs nd.node_outputs |
|
169 |
in |
|
170 |
List.fold_left |
|
171 |
(fun vars v -> ISet.add v.var_id vars) |
|
172 |
inoutputs nd.node_locals |
|
170 | 173 |
|
171 |
(* computes the equivalence relation relating variables |
|
172 |
in the same equation lhs, under the form of a table |
|
173 |
of class representatives *) |
|
174 |
(* computes the equivalence relation relating variables in the same equation |
|
175 |
lhs, under the form of a table of class representatives *) |
|
174 | 176 |
let eqs_eq_equiv eqs = |
175 | 177 |
let eq_equiv = Hashtbl.create 23 in |
176 |
List.iter (fun eq ->
|
|
177 |
let first = List.hd eq.eq_lhs in
|
|
178 |
List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
|
|
179 |
) |
|
178 |
List.iter |
|
179 |
(fun eq ->
|
|
180 |
let first = List.hd eq.eq_lhs in
|
|
181 |
List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs)
|
|
180 | 182 |
eqs; |
181 | 183 |
eq_equiv |
182 |
|
|
183 |
let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd)
|
|
184 |
|
|
185 |
(* Create a tuple of right dimension, according to [expr] type, *) |
|
186 |
(* filled with variable [v] *) |
|
184 |
|
|
185 |
let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd) |
|
186 |
|
|
187 |
(* Create a tuple of right dimension, according to [expr] type, *)
|
|
188 |
(* filled with variable [v] *)
|
|
187 | 189 |
let adjust_tuple v expr = |
188 | 190 |
match expr.expr_type.Types.tdesc with |
189 |
| Types.Ttuple tl -> duplicate v (List.length tl) |
|
190 |
| _ -> [v] |
|
191 |
|
|
191 |
| Types.Ttuple tl -> |
|
192 |
duplicate v (List.length tl) |
|
193 |
| _ -> |
|
194 |
[ v ] |
|
192 | 195 |
|
193 | 196 |
(* Add dependencies from lhs to rhs in [g, g'], *) |
194 | 197 |
(* no-mem/no-mem and mem/no-mem in g *) |
195 | 198 |
(* mem/mem in g' *) |
196 |
(* match (lhs_is_mem, ISet.mem x mems) with |
|
197 |
| (false, true ) -> (add_edges [x] lhs g, |
|
198 |
g') |
|
199 |
| (false, false) -> (add_edges lhs [x] g, |
|
200 |
g') |
|
201 |
| (true , false) -> (add_edges lhs [x] g, |
|
202 |
g') |
|
203 |
| (true , true ) -> (g, |
|
204 |
add_edges [x] lhs g') |
|
205 |
*) |
|
199 |
(* match (lhs_is_mem, ISet.mem x mems) with | (false, true ) -> (add_edges [x] |
|
200 |
lhs g, g') | (false, false) -> (add_edges lhs [x] g, g') | (true , false) |
|
201 |
-> (add_edges lhs [x] g, g') | (true , true ) -> (g, add_edges [x] lhs g') *) |
|
206 | 202 |
let add_eq_dependencies mems inputs node_vars eq (g, g') = |
207 | 203 |
let add_var lhs_is_mem lhs x (g, g') = |
208 | 204 |
if is_instance_var x || ISet.mem x node_vars then |
209 |
if ISet.mem x mems |
|
210 |
then |
|
211 |
let g = add_edges lhs [mk_read_var x] g in |
|
212 |
if lhs_is_mem |
|
213 |
then |
|
214 |
(g, add_edges [x] lhs g') |
|
215 |
else |
|
216 |
(add_edges [x] lhs g, g') |
|
205 |
if ISet.mem x mems then |
|
206 |
let g = add_edges lhs [ mk_read_var x ] g in |
|
207 |
if lhs_is_mem then g, add_edges [ x ] lhs g' |
|
208 |
else add_edges [ x ] lhs g, g' |
|
217 | 209 |
else |
218 | 210 |
let x = if ISet.mem x inputs then mk_read_var x else x in |
219 |
(add_edges lhs [x] g, g') |
|
220 |
else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *) |
|
211 |
add_edges lhs [ x ] g, g' |
|
212 |
else add_edges lhs [ mk_read_var x ] g, g' |
|
213 |
(* x is a global constant, treated as a read var *) |
|
221 | 214 |
in |
222 | 215 |
(* Add dependencies from [lhs] to rhs clock [ck]. *) |
223 | 216 |
let rec add_clock lhs_is_mem lhs ck g = |
224 | 217 |
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) |
225 | 218 |
match (Clocks.repr ck).Clocks.cdesc with |
226 |
| Clocks.Con (ck', cr, _) -> |
|
227 |
add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) |
|
219 |
| Clocks.Con (ck', cr, _) -> |
|
220 |
add_var lhs_is_mem lhs |
|
221 |
(Clocks.const_of_carrier cr) |
|
228 | 222 |
(add_clock lhs_is_mem lhs ck' g) |
229 | 223 |
| Clocks.Ccarrying (_, ck') -> |
230 | 224 |
add_clock lhs_is_mem lhs ck' g |
231 |
| _ -> g |
|
225 |
| _ -> |
|
226 |
g |
|
232 | 227 |
in |
233 | 228 |
let rec add_dep lhs_is_mem lhs rhs g = |
234 | 229 |
(* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *) |
235 | 230 |
(* i.e every input is connected to every output, through a ghost var *) |
236 | 231 |
let mashup_appl_dependencies f e g = |
237 |
let f_var = mk_instance_var (Format.sprintf "%s_%d" f (fst eq.eq_loc).Lexing.pos_lnum) in |
|
238 |
List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) |
|
239 |
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) |
|
232 |
let f_var = |
|
233 |
mk_instance_var |
|
234 |
(Format.sprintf "%s_%d" f (fst eq.eq_loc).Lexing.pos_lnum) |
|
235 |
in |
|
236 |
List.fold_right |
|
237 |
(fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) |
|
238 |
(expr_list_of_expr e) |
|
239 |
(add_var lhs_is_mem lhs f_var g) |
|
240 | 240 |
in |
241 | 241 |
let g = add_clock lhs_is_mem lhs rhs.expr_clock g in |
242 | 242 |
match rhs.expr_desc with |
243 |
| Expr_const _ -> g |
|
244 |
| Expr_fby (e1, e2) -> add_dep true lhs e2 (add_dep false lhs e1 g) |
|
245 |
| Expr_pre e -> add_dep true lhs e g |
|
246 |
| Expr_ident x -> add_var lhs_is_mem lhs x g |
|
247 |
| Expr_access (e1, d) |
|
248 |
| Expr_power (e1, d) -> add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g) |
|
249 |
| Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g |
|
250 |
| Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g |
|
251 |
| Expr_merge (c, hl) -> add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g) |
|
252 |
| Expr_ite (c, t, e) -> add_dep lhs_is_mem lhs c (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g)) |
|
253 |
| Expr_arrow (e1, e2) -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) |
|
254 |
| Expr_when (e, c, _) -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) |
|
243 |
| Expr_const _ -> |
|
244 |
g |
|
245 |
| Expr_fby (e1, e2) -> |
|
246 |
add_dep true lhs e2 (add_dep false lhs e1 g) |
|
247 |
| Expr_pre e -> |
|
248 |
add_dep true lhs e g |
|
249 |
| Expr_ident x -> |
|
250 |
add_var lhs_is_mem lhs x g |
|
251 |
| Expr_access (e1, d) | Expr_power (e1, d) -> |
|
252 |
add_dep lhs_is_mem lhs e1 |
|
253 |
(add_dep lhs_is_mem lhs (expr_of_dimension d) g) |
|
254 |
| Expr_array a -> |
|
255 |
List.fold_right (add_dep lhs_is_mem lhs) a g |
|
256 |
| Expr_tuple t -> |
|
257 |
List.fold_right2 (fun l r -> add_dep lhs_is_mem [ l ] r) lhs t g |
|
258 |
| Expr_merge (c, hl) -> |
|
259 |
add_var lhs_is_mem lhs c |
|
260 |
(List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g) |
|
261 |
| Expr_ite (c, t, e) -> |
|
262 |
add_dep lhs_is_mem lhs c |
|
263 |
(add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g)) |
|
264 |
| Expr_arrow (e1, e2) -> |
|
265 |
add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) |
|
266 |
| Expr_when (e, c, _) -> |
|
267 |
add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) |
|
255 | 268 |
| Expr_appl (f, e, None) -> |
256 |
if Basic_library.is_expr_internal_fun rhs
|
|
257 |
(* tuple component-wise dependency for internal operators *)
|
|
258 |
then
|
|
259 |
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
|
|
269 |
if |
|
270 |
Basic_library.is_expr_internal_fun rhs
|
|
271 |
(* tuple component-wise dependency for internal operators *)
|
|
272 |
then List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
|
|
260 | 273 |
(* mashed up dependency for user-defined operators *) |
261 |
else |
|
262 |
mashup_appl_dependencies f e g |
|
274 |
else mashup_appl_dependencies f e g |
|
263 | 275 |
| Expr_appl (f, e, Some c) -> |
264 | 276 |
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g) |
265 | 277 |
in |
266 |
let g = List.fold_left (fun g lhs ->
|
|
267 |
if ISet.mem lhs mems then
|
|
268 |
add_vertices [lhs; mk_read_var lhs] g
|
|
269 |
else
|
|
270 |
add_vertices [lhs] g)
|
|
271 |
g eq.eq_lhs
|
|
278 |
let g = |
|
279 |
List.fold_left
|
|
280 |
(fun g lhs ->
|
|
281 |
if ISet.mem lhs mems then add_vertices [ lhs; mk_read_var lhs ] g
|
|
282 |
else add_vertices [ lhs ] g)
|
|
283 |
g eq.eq_lhs
|
|
272 | 284 |
in |
273 | 285 |
add_dep false eq.eq_lhs eq.eq_rhs (g, g') |
274 | 286 |
|
275 |
|
|
276 | 287 |
(* Returns the dependence graph for node [n] *) |
277 | 288 |
let dependence_graph mems inputs node_vars n = |
278 | 289 |
instance_var_cpt := 0; |
279 | 290 |
let g = new_graph (), new_graph () in |
280 | 291 |
(* Basic dependencies *) |
281 |
let g = List.fold_right (add_eq_dependencies mems inputs node_vars) |
|
282 |
(get_node_eqs n) g in |
|
292 |
let g = |
|
293 |
List.fold_right |
|
294 |
(add_eq_dependencies mems inputs node_vars) |
|
295 |
(get_node_eqs n) g |
|
296 |
in |
|
297 |
|
|
283 | 298 |
(* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il |
284 |
faut imposer que les outputs dépendent des asserts pour identifier que les |
|
285 |
fcn calls des asserts sont évalués avant le noeuds *) |
|
286 |
|
|
287 |
(* (\* In order to introduce dependencies between assert expressions and the node, *) |
|
288 |
(* we build an artificial dependency between node output and each assert *) |
|
289 |
(* expr. While these are not valid equations, they should properly propage in *) |
|
299 |
faut imposer que les outputs dépendent des asserts pour identifier que |
|
300 |
les fcn calls des asserts sont évalués avant le noeuds *) |
|
301 |
|
|
302 |
(* (\* In order to introduce dependencies between assert expressions and the |
|
303 |
node, *) |
|
304 |
(* we build an artificial dependency between node output and each assert *) |
|
305 |
(* expr. While these are not valid equations, they should properly propage |
|
306 |
in *) |
|
290 | 307 |
(* function add_eq_dependencies *\) *) |
291 | 308 |
(* let g = *) |
292 | 309 |
(* let output_vars_as_lhs = ISet.elements (node_output_variables n) in *) |
293 | 310 |
(* List.fold_left (fun g ae -> *) |
294 |
(* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *) |
|
311 |
(* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, |
|
312 |
ae.assert_expr) in *) |
|
295 | 313 |
(* add_eq_dependencies mems inputs node_vars fake_eq g *) |
296 | 314 |
(* ) g n.node_asserts in *) |
297 | 315 |
g |
298 |
|
|
299 | 316 |
end |
300 | 317 |
|
301 | 318 |
module NodeDep = struct |
302 |
|
|
303 |
module ExprModule = |
|
304 |
struct |
|
319 |
module ExprModule = struct |
|
305 | 320 |
type t = expr |
321 |
|
|
306 | 322 |
let compare = compare |
323 |
|
|
307 | 324 |
let hash n = Hashtbl.hash n |
325 |
|
|
308 | 326 |
let equal n1 n2 = n1 = n2 |
309 | 327 |
end |
310 | 328 |
|
311 |
module ESet = Set.Make(ExprModule) |
|
329 |
module ESet = Set.Make (ExprModule)
|
|
312 | 330 |
|
313 |
let rec get_expr_calls prednode expr =
|
|
331 |
let rec get_expr_calls prednode expr = |
|
314 | 332 |
match expr.expr_desc with |
315 |
| Expr_const _ |
|
316 |
| Expr_ident _ -> ESet.empty |
|
317 |
| Expr_access (e, _) |
|
318 |
| Expr_power (e, _) -> get_expr_calls prednode e |
|
319 |
| Expr_array t |
|
320 |
| Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty |
|
321 |
| Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty |
|
322 |
| Expr_fby (e1,e2) |
|
323 |
| Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) |
|
324 |
| Expr_ite (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) |
|
325 |
| Expr_pre e |
|
326 |
| Expr_when (e,_,_) -> get_expr_calls prednode e |
|
327 |
| Expr_appl (id,e, _) -> |
|
328 |
if not (Basic_library.is_expr_internal_fun expr) && prednode id |
|
329 |
then ESet.add expr (get_expr_calls prednode e) |
|
330 |
else (get_expr_calls prednode e) |
|
331 |
|
|
332 |
let get_eexpr_calls prednode ee = |
|
333 |
get_expr_calls prednode ee.eexpr_qfexpr |
|
334 |
|
|
333 |
| Expr_const _ | Expr_ident _ -> |
|
334 |
ESet.empty |
|
335 |
| Expr_access (e, _) | Expr_power (e, _) -> |
|
336 |
get_expr_calls prednode e |
|
337 |
| Expr_array t | Expr_tuple t -> |
|
338 |
List.fold_right |
|
339 |
(fun x set -> ESet.union (get_expr_calls prednode x) set) |
|
340 |
t ESet.empty |
|
341 |
| Expr_merge (_, hl) -> |
|
342 |
List.fold_right |
|
343 |
(fun (_, h) set -> ESet.union (get_expr_calls prednode h) set) |
|
344 |
hl ESet.empty |
|
345 |
| Expr_fby (e1, e2) | Expr_arrow (e1, e2) -> |
|
346 |
ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) |
|
347 |
| Expr_ite (c, t, e) -> |
|
348 |
ESet.union |
|
349 |
(get_expr_calls prednode c) |
|
350 |
(ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) |
|
351 |
| Expr_pre e | Expr_when (e, _, _) -> |
|
352 |
get_expr_calls prednode e |
|
353 |
| Expr_appl (id, e, _) -> |
|
354 |
if (not (Basic_library.is_expr_internal_fun expr)) && prednode id then |
|
355 |
ESet.add expr (get_expr_calls prednode e) |
|
356 |
else get_expr_calls prednode e |
|
357 |
|
|
358 |
let get_eexpr_calls prednode ee = get_expr_calls prednode ee.eexpr_qfexpr |
|
359 |
|
|
335 | 360 |
let get_callee expr = |
336 | 361 |
match expr.expr_desc with |
337 |
| Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args) |
|
338 |
| _ -> None |
|
362 |
| Expr_appl (id, args, _) -> |
|
363 |
Some (id, expr_list_of_expr args) |
|
364 |
| _ -> |
|
365 |
None |
|
339 | 366 |
|
340 |
let accu f init objl = List.fold_left (fun accu o -> ESet.union accu (f o)) init objl |
|
367 |
let accu f init objl = |
|
368 |
List.fold_left (fun accu o -> ESet.union accu (f o)) init objl |
|
341 | 369 |
|
342 | 370 |
let get_eq_calls prednode eq = get_expr_calls prednode eq.eq_rhs |
343 |
|
|
371 |
|
|
344 | 372 |
let rec get_stmt_calls prednode s = |
345 |
match s with Eq eq -> get_eq_calls prednode eq | Aut aut -> get_aut_calls prednode aut |
|
373 |
match s with |
|
374 |
| Eq eq -> |
|
375 |
get_eq_calls prednode eq |
|
376 |
| Aut aut -> |
|
377 |
get_aut_calls prednode aut |
|
378 |
|
|
346 | 379 |
and get_aut_calls prednode aut = |
347 | 380 |
let get_handler_calls prednode h = |
348 |
let get_cond_calls c = accu (fun (_,e,_,_) -> get_expr_calls prednode e) ESet.empty c in |
|
381 |
let get_cond_calls c = |
|
382 |
accu (fun (_, e, _, _) -> get_expr_calls prednode e) ESet.empty c |
|
383 |
in |
|
349 | 384 |
let until = get_cond_calls h.hand_until in |
350 | 385 |
let unless = get_cond_calls h.hand_unless in |
351 |
let calls = ESet.union until unless in
|
|
386 |
let calls = ESet.union until unless in |
|
352 | 387 |
let calls = accu (get_stmt_calls prednode) calls h.hand_stmts in |
353 |
let calls = accu (fun a -> get_expr_calls prednode a.assert_expr) calls h.hand_asserts in |
|
354 |
(* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *) |
|
388 |
let calls = |
|
389 |
accu |
|
390 |
(fun a -> get_expr_calls prednode a.assert_expr) |
|
391 |
calls h.hand_asserts |
|
392 |
in |
|
393 |
(* let calls = accu xx calls h.hand_annots in *) |
|
394 |
(* TODO: search for calls in eexpr *) |
|
355 | 395 |
calls |
356 | 396 |
in |
357 | 397 |
accu (get_handler_calls prednode) ESet.empty aut.aut_handlers |
358 |
|
|
398 |
|
|
359 | 399 |
let get_calls prednode nd = |
360 | 400 |
let eqs, auts = get_node_eqs nd in |
361 | 401 |
let deps = accu (get_eq_calls prednode) ESet.empty eqs in |
... | ... | |
364 | 404 |
|
365 | 405 |
let get_contract_calls prednode c = |
366 | 406 |
let deps = accu (get_stmt_calls prednode) ESet.empty c.stmts in |
367 |
let deps = accu (get_eexpr_calls prednode) deps ( c.assume @ c.guarantees @ (List.fold_left (fun accu m -> accu @ m.require @ m.ensure ) [] c.modes)) in |
|
368 |
let id_deps = List.map (fun e -> fst (desome (get_callee e))) (ESet.elements deps) in |
|
369 |
let id_deps = (List.fold_left (fun accu imp -> imp.import_nodeid::accu) [] c.imports) @ id_deps in |
|
407 |
let deps = |
|
408 |
accu (get_eexpr_calls prednode) deps |
|
409 |
(c.assume @ c.guarantees |
|
410 |
@ List.fold_left (fun accu m -> accu @ m.require @ m.ensure) [] c.modes |
|
411 |
) |
|
412 |
in |
|
413 |
let id_deps = |
|
414 |
List.map (fun e -> fst (desome (get_callee e))) (ESet.elements deps) |
|
415 |
in |
|
416 |
let id_deps = |
|
417 |
List.fold_left (fun accu imp -> imp.import_nodeid :: accu) [] c.imports |
|
418 |
@ id_deps |
|
419 |
in |
|
370 | 420 |
id_deps |
371 |
|
|
421 |
|
|
372 | 422 |
let dependence_graph prog = |
373 | 423 |
let g = new_graph () in |
374 |
let g = List.fold_right |
|
375 |
(fun td accu -> (* for each node we add its dependencies *) |
|
376 |
match td.top_decl_desc with |
|
377 |
| Node nd -> |
|
378 |
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) |
|
379 |
let accu = add_vertices [nd.node_id] accu in |
|
380 |
let deps = List.map |
|
381 |
(fun e -> fst (desome (get_callee e))) |
|
382 |
(get_calls (fun _ -> true) nd) |
|
383 |
in |
|
384 |
(* Adding assert expressions deps *) |
|
385 |
let deps_asserts = |
|
386 |
let prednode = (fun _ -> true) in (* what is this about? *) |
|
387 |
List.map |
|
388 |
(fun e -> fst (desome (get_callee e))) |
|
389 |
(ESet.elements |
|
390 |
(List.fold_left |
|
391 |
(fun accu assert_expr -> ESet.union accu (get_expr_calls prednode assert_expr)) |
|
392 |
ESet.empty |
|
393 |
(List.map (fun _assert -> _assert.assert_expr) nd.node_asserts) |
|
394 |
) |
|
395 |
) |
|
396 |
in |
|
397 |
let deps_spec = match nd.node_spec with |
|
398 |
| None -> [] |
|
399 |
| Some (NodeSpec id) -> [id] |
|
400 |
| Some (Contract c) -> get_contract_calls (fun _ -> true) c |
|
401 |
|
|
402 |
in |
|
403 |
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) |
|
404 |
add_edges [nd.node_id] (deps@deps_asserts@deps_spec) accu |
|
405 |
| _ -> assert false (* should not happen *) |
|
406 |
|
|
407 |
) prog g in |
|
408 |
g |
|
409 |
|
|
424 |
let g = |
|
425 |
List.fold_right |
|
426 |
(fun td accu -> |
|
427 |
(* for each node we add its dependencies *) |
|
428 |
match td.top_decl_desc with |
|
429 |
| Node nd -> |
|
430 |
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) |
|
431 |
let accu = add_vertices [ nd.node_id ] accu in |
|
432 |
let deps = |
|
433 |
List.map |
|
434 |
(fun e -> fst (desome (get_callee e))) |
|
435 |
(get_calls (fun _ -> true) nd) |
|
436 |
in |
|
437 |
(* Adding assert expressions deps *) |
|
438 |
let deps_asserts = |
|
439 |
let prednode _ = true in |
|
440 |
(* what is this about? *) |
|
441 |
List.map |
|
442 |
(fun e -> fst (desome (get_callee e))) |
|
443 |
(ESet.elements |
|
444 |
(List.fold_left |
|
445 |
(fun accu assert_expr -> |
|
446 |
ESet.union accu (get_expr_calls prednode assert_expr)) |
|
447 |
ESet.empty |
|
448 |
(List.map |
|
449 |
(fun _assert -> _assert.assert_expr) |
|
450 |
nd.node_asserts))) |
|
451 |
in |
|
452 |
let deps_spec = |
|
453 |
match nd.node_spec with |
|
454 |
| None -> |
|
455 |
[] |
|
456 |
| Some (NodeSpec id) -> |
|
457 |
[ id ] |
|
458 |
| Some (Contract c) -> |
|
459 |
get_contract_calls (fun _ -> true) c |
|
460 |
in |
|
461 |
|
|
462 |
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." |
|
463 |
Format.pp_print_string) deps; *) |
|
464 |
add_edges [ nd.node_id ] (deps @ deps_asserts @ deps_spec) accu |
|
465 |
| _ -> |
|
466 |
assert false |
|
467 |
(* should not happen *)) |
|
468 |
prog g |
|
469 |
in |
|
470 |
g |
|
471 |
|
|
410 | 472 |
let rec filter_static_inputs inputs args = |
411 | 473 |
match inputs, args with |
412 |
| [] , [] -> [] |
|
413 |
| v::vq, a::aq -> if v.var_dec_const && Types.is_dimension_type v.var_type then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq |
|
414 |
| _ -> assert false |
|
474 |
| [], [] -> |
|
475 |
[] |
|
476 |
| v :: vq, a :: aq -> |
|
477 |
if v.var_dec_const && Types.is_dimension_type v.var_type then |
|
478 |
dimension_of_expr a :: filter_static_inputs vq aq |
|
479 |
else filter_static_inputs vq aq |
|
480 |
| _ -> |
|
481 |
assert false |
|
415 | 482 |
|
416 | 483 |
let compute_generic_calls prog = |
417 | 484 |
List.iter |
418 | 485 |
(fun td -> |
419 |
match td.top_decl_desc with |
|
420 |
| Node nd -> |
|
421 |
let prednode n = is_generic_node (node_from_name n) in |
|
422 |
nd.node_gencalls <- get_calls prednode nd |
|
423 |
| _ -> () |
|
424 |
|
|
425 |
) prog |
|
426 |
|
|
486 |
match td.top_decl_desc with |
|
487 |
| Node nd -> |
|
488 |
let prednode n = is_generic_node (node_from_name n) in |
|
489 |
nd.node_gencalls <- get_calls prednode nd |
|
490 |
| _ -> |
|
491 |
()) |
|
492 |
prog |
|
427 | 493 |
end |
428 | 494 |
|
429 |
|
|
430 | 495 |
module CycleDetection = struct |
431 |
|
|
432 | 496 |
(* ---- Look for cycles in a dependency graph *) |
433 | 497 |
module Cycles = Graph.Components.Make (IdentDepGraph) |
434 | 498 |
|
435 | 499 |
let mk_copy_var n id = |
436 | 500 |
let used name = |
437 |
(List.exists (fun v -> v.var_id = name) n.node_locals) |
|
438 |
|| (List.exists (fun v -> v.var_id = name) n.node_inputs) |
|
439 |
|| (List.exists (fun v -> v.var_id = name) n.node_outputs) |
|
440 |
in mk_new_name used id |
|
501 |
List.exists (fun v -> v.var_id = name) n.node_locals |
|
502 |
|| List.exists (fun v -> v.var_id = name) n.node_inputs |
|
503 |
|| List.exists (fun v -> v.var_id = name) n.node_outputs |
|
504 |
in |
|
505 |
mk_new_name used id |
|
441 | 506 |
|
442 | 507 |
let mk_copy_eq n var = |
443 | 508 |
let var_decl = get_node_var var n in |
444 | 509 |
let cp_var = mk_copy_var n var in |
445 | 510 |
let expr = |
446 |
{ expr_tag = Utils.new_tag (); |
|
447 |
expr_desc = Expr_ident var; |
|
448 |
expr_type = var_decl.var_type; |
|
449 |
expr_clock = var_decl.var_clock; |
|
450 |
expr_delay = Delay.new_var (); |
|
451 |
expr_annot = None; |
|
452 |
expr_loc = var_decl.var_loc } in |
|
453 |
{ var_decl with var_id = cp_var; var_orig = false }, |
|
454 |
mkeq var_decl.var_loc ([cp_var], expr) |
|
511 |
{ |
|
512 |
expr_tag = Utils.new_tag (); |
|
513 |
expr_desc = Expr_ident var; |
|
514 |
expr_type = var_decl.var_type; |
|
515 |
expr_clock = var_decl.var_clock; |
|
516 |
expr_delay = Delay.new_var (); |
|
517 |
expr_annot = None; |
|
518 |
expr_loc = var_decl.var_loc; |
|
519 |
} |
|
520 |
in |
|
521 |
( { var_decl with var_id = cp_var; var_orig = false }, |
|
522 |
mkeq var_decl.var_loc ([ cp_var ], expr) ) |
|
455 | 523 |
|
456 | 524 |
let wrong_partition g partition = |
457 | 525 |
match partition with |
458 |
| [id] -> IdentDepGraph.mem_edge g id id |
|
459 |
| _::_::_ -> true |
|
460 |
| [] -> assert false |
|
526 |
| [ id ] -> |
|
527 |
IdentDepGraph.mem_edge g id id |
|
528 |
| _ :: _ :: _ -> |
|
529 |
true |
|
530 |
| [] -> |
|
531 |
assert false |
|
461 | 532 |
|
462 | 533 |
(* Checks that the dependency graph [g] does not contain a cycle. Raises |
463 |
[Cycle partition] if the succession of dependencies [partition] forms a cycle *) |
|
534 |
[Cycle partition] if the succession of dependencies [partition] forms a |
|
535 |
cycle *) |
|
464 | 536 |
let check_cycles g = |
465 | 537 |
let scc_l = Cycles.scc_list g in |
466 | 538 |
let algebraic_loops = List.filter (wrong_partition g) scc_l in |
467 | 539 |
if List.length algebraic_loops > 0 then |
468 | 540 |
raise (Error (DataCycle algebraic_loops)) |
469 |
(* We extract a hint to resolve the cycle: for each variable in the cycle
|
|
470 |
which is defined by a call, we return the name of the node call and
|
|
471 |
its specific id *)
|
|
541 |
(* We extract a hint to resolve the cycle: for each variable in the cycle
|
|
542 |
which is defined by a call, we return the name of the node call and its
|
|
543 |
specific id *)
|
|
472 | 544 |
|
473 | 545 |
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *) |
474 | 546 |
let copy_partition g partition = |
475 | 547 |
let copy_g = IdentDepGraph.create () in |
476 | 548 |
IdentDepGraph.iter_edges |
477 | 549 |
(fun src tgt -> |
478 |
if List.mem src partition && List.mem tgt partition
|
|
479 |
then IdentDepGraph.add_edge copy_g src tgt)
|
|
550 |
if List.mem src partition && List.mem tgt partition then
|
|
551 |
IdentDepGraph.add_edge copy_g src tgt)
|
|
480 | 552 |
g |
481 | 553 |
|
482 |
|
|
483 |
(* Breaks dependency cycles in a graph [g] by inserting aux variables. |
|
484 |
[head] is a head of a non-trivial scc of [g]. |
|
485 |
In Lustre, this is legal only for mem/mem cycles *) |
|
554 |
(* Breaks dependency cycles in a graph [g] by inserting aux variables. [head] |
|
555 |
is a head of a non-trivial scc of [g]. In Lustre, this is legal only for |
|
556 |
mem/mem cycles *) |
|
486 | 557 |
let break_cycle head cp_head g = |
487 | 558 |
let succs = IdentDepGraph.succ g head in |
488 | 559 |
IdentDepGraph.add_edge g head cp_head; |
489 | 560 |
IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head); |
490 | 561 |
List.iter |
491 | 562 |
(fun s -> |
492 |
IdentDepGraph.remove_edge g head s;
|
|
493 |
IdentDepGraph.add_edge g s cp_head)
|
|
563 |
IdentDepGraph.remove_edge g head s;
|
|
564 |
IdentDepGraph.add_edge g s cp_head)
|
|
494 | 565 |
succs |
495 | 566 |
|
496 | 567 |
(* Breaks cycles of the dependency graph [g] of memory variables [mems] |
497 |
belonging in node [node]. Returns: |
|
498 |
- a list of new auxiliary variable declarations |
|
499 |
- a list of new equations |
|
500 |
- a modified acyclic version of [g] |
|
501 |
*) |
|
568 |
belonging in node [node]. Returns: - a list of new auxiliary variable |
|
569 |
declarations - a list of new equations - a modified acyclic version of [g] *) |
|
502 | 570 |
let break_cycles node mems g = |
503 |
let eqs , auts = get_node_eqs node in |
|
504 |
assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *) |
|
505 |
let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) eqs in |
|
571 |
let eqs, auts = get_node_eqs node in |
|
572 |
assert (auts = []); |
|
573 |
(* TODO: check: For the moment we assume that auts are expanded by now *) |
|
574 |
let mem_eqs, non_mem_eqs = |
|
575 |
List.partition |
|
576 |
(fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) |
|
577 |
eqs |
|
578 |
in |
|
506 | 579 |
let rec break vdecls mem_eqs g = |
507 | 580 |
let scc_l = Cycles.scc_list g in |
508 | 581 |
let wrong = List.filter (wrong_partition g) scc_l in |
509 | 582 |
match wrong with |
510 |
| [] -> (vdecls, non_mem_eqs@mem_eqs, g) |
|
511 |
| [head]::_ -> |
|
512 |
begin |
|
513 |
IdentDepGraph.remove_edge g head head; |
|
514 |
break vdecls mem_eqs g |
|
515 |
end |
|
516 |
| (head::part)::_ -> |
|
517 |
begin |
|
518 |
let vdecl_cp_head, cp_eq = mk_copy_eq node head in |
|
519 |
let pvar v = List.mem v part in |
|
520 |
let fvar v = if v = head then vdecl_cp_head.var_id else v in |
|
521 |
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in |
|
522 |
break_cycle head vdecl_cp_head.var_id g; |
|
523 |
break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g |
|
524 |
end |
|
525 |
| _ -> assert false |
|
526 |
in break [] mem_eqs g |
|
527 |
|
|
583 |
| [] -> |
|
584 |
vdecls, non_mem_eqs @ mem_eqs, g |
|
585 |
| [ head ] :: _ -> |
|
586 |
IdentDepGraph.remove_edge g head head; |
|
587 |
break vdecls mem_eqs g |
|
588 |
| (head :: part) :: _ -> |
|
589 |
let vdecl_cp_head, cp_eq = mk_copy_eq node head in |
|
590 |
let pvar v = List.mem v part in |
|
591 |
let fvar v = if v = head then vdecl_cp_head.var_id else v in |
|
592 |
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in |
|
593 |
break_cycle head vdecl_cp_head.var_id g; |
|
594 |
break (vdecl_cp_head :: vdecls) (cp_eq :: mem_eqs') g |
|
595 |
| _ -> |
|
596 |
assert false |
|
597 |
in |
|
598 |
break [] mem_eqs g |
|
528 | 599 |
end |
529 | 600 |
|
530 |
(* Module used to compute static disjunction of variables based upon their clocks. *) |
|
531 |
module Disjunction = |
|
532 |
struct |
|
533 |
module ClockedIdentModule = |
|
534 |
struct |
|
601 |
(* Module used to compute static disjunction of variables based upon their |
|
602 |
clocks. *) |
|
603 |
module Disjunction = struct |
|
604 |
module ClockedIdentModule = struct |
|
535 | 605 |
type t = var_decl |
536 |
let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock |
|
537 |
let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id) |
|
606 |
|
|
607 |
let root_branch vdecl = |
|
608 |
Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock |
|
609 |
|
|
610 |
let compare v1 v2 = |
|
611 |
compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id) |
|
538 | 612 |
end |
539 | 613 |
|
540 |
module CISet = Set.Make(ClockedIdentModule) |
|
614 |
module CISet = Set.Make (ClockedIdentModule)
|
|
541 | 615 |
|
542 |
(* map: var |-> list of disjoint vars, sorted in increasing branch length order,
|
|
543 |
maybe removing shorter branches *) |
|
616 |
(* map: var |-> list of disjoint vars, sorted in increasing branch length |
|
617 |
order, maybe removing shorter branches *)
|
|
544 | 618 |
type disjoint_map = (ident, CISet.t) Hashtbl.t |
545 | 619 |
|
546 |
let pp_ciset fmt t = let open Format in |
|
620 |
let pp_ciset fmt t = |
|
621 |
let open Format in |
|
547 | 622 |
pp_print_braced' ~pp_sep:pp_print_space Printers.pp_var_name fmt |
548 | 623 |
(CISet.elements t) |
549 | 624 |
|
550 | 625 |
let clock_disjoint_map vdecls = |
551 | 626 |
let map = Hashtbl.create 23 in |
552 |
begin
|
|
553 |
List.iter
|
|
554 |
(fun v1 -> let disj_v1 =
|
|
555 |
List.fold_left
|
|
556 |
(fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
|
|
557 |
CISet.empty
|
|
558 |
vdecls in
|
|
559 |
(* disjoint vdecls are stored in increasing branch length order *)
|
|
560 |
Hashtbl.add map v1.var_id disj_v1)
|
|
561 |
vdecls;
|
|
562 |
(map : disjoint_map)
|
|
563 |
end
|
|
564 |
|
|
565 |
(* merge variables [v] and [v'] in disjunction [map]. Then: |
|
566 |
- the mapping v' becomes v' |-> (map v) inter (map v')
|
|
567 |
- the mapping v |-> ... then disappears
|
|
568 |
- other mappings become x |-> (map x) \ (if v in x then v else v')
|
|
569 |
*) |
|
627 |
List.iter
|
|
628 |
(fun v1 ->
|
|
629 |
let disj_v1 =
|
|
630 |
List.fold_left
|
|
631 |
(fun res v2 ->
|
|
632 |
if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res
|
|
633 |
else res)
|
|
634 |
CISet.empty vdecls
|
|
635 |
in
|
|
636 |
(* disjoint vdecls are stored in increasing branch length order *)
|
|
637 |
Hashtbl.add map v1.var_id disj_v1)
|
|
638 |
vdecls;
|
|
639 |
(map : disjoint_map) |
|
640 |
|
|
641 |
(* merge variables [v] and [v'] in disjunction [map]. Then: - the mapping v'
|
|
642 |
becomes v' |-> (map v) inter (map v') - the mapping v |-> ... then
|
|
643 |
disappears - other mappings become x |-> (map x) \ (if v in x then v else
|
|
644 |
v') *)
|
|
570 | 645 |
let merge_in_disjoint_map map v v' = |
571 |
begin |
|
572 |
Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id)); |
|
573 |
Hashtbl.remove map v.var_id; |
|
574 |
Hashtbl.iter (fun x map_x -> Hashtbl.replace map x (CISet.remove (if CISet.mem v map_x then v else v') map_x)) map; |
|
575 |
end |
|
576 |
|
|
577 |
(* replace variable [v] by [v'] in disjunction [map]. |
|
578 |
[v'] is a dead variable. Then: |
|
579 |
- the mapping v' becomes v' |-> (map v) |
|
580 |
- the mapping v |-> ... then disappears |
|
581 |
- all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x) |
|
582 |
*) |
|
646 |
Hashtbl.replace map v'.var_id |
|
647 |
(CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id)); |
|
648 |
Hashtbl.remove map v.var_id; |
|
649 |
Hashtbl.iter |
|
650 |
(fun x map_x -> |
|
651 |
Hashtbl.replace map x |
|
652 |
(CISet.remove (if CISet.mem v map_x then v else v') map_x)) |
|
653 |
map |
|
654 |
|
|
655 |
(* replace variable [v] by [v'] in disjunction [map]. [v'] is a dead variable. |
|
656 |
Then: - the mapping v' becomes v' |-> (map v) - the mapping v |-> ... then |
|
657 |
disappears - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in |
|
658 |
map x) *) |
|
583 | 659 |
let replace_in_disjoint_map map v v' = |
584 |
begin |
|
585 |
Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id); |
|
586 |
Hashtbl.remove map v.var_id; |
|
587 |
Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (if CISet.mem v mapx then CISet.add v' (CISet.remove v mapx) else CISet.remove v' mapx)) map; |
|
588 |
end |
|
589 |
|
|
590 |
(* remove variable [v] in disjunction [map]. Then: |
|
591 |
- the mapping v |-> ... then disappears |
|
592 |
- all mappings become x |-> (map x) \ { v} |
|
593 |
*) |
|
660 |
Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id); |
|
661 |
Hashtbl.remove map v.var_id; |
|
662 |
Hashtbl.iter |
|
663 |
(fun x mapx -> |
|
664 |
Hashtbl.replace map x |
|
665 |
(if CISet.mem v mapx then CISet.add v' (CISet.remove v mapx) |
|
666 |
else CISet.remove v' mapx)) |
|
667 |
map |
|
668 |
|
|
669 |
(* remove variable [v] in disjunction [map]. Then: - the mapping v |-> ... |
|
670 |
then disappears - all mappings become x |-> (map x) \ { v} *) |
|
594 | 671 |
let remove_in_disjoint_map map v = |
595 |
begin |
|
596 |
Hashtbl.remove map v.var_id; |
|
597 |
Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map; |
|
598 |
end |
|
672 |
Hashtbl.remove map v.var_id; |
|
673 |
Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map |
|
599 | 674 |
|
600 | 675 |
let pp_disjoint_map fmt map = |
601 |
Format.(fprintf fmt "@[<v 2>{ /* disjoint map */%t@] }" |
|
602 |
(fun fmt -> |
|
603 |
Hashtbl.iter (fun k v -> |
|
604 |
fprintf fmt "@,%s # %a" |
|
605 |
k (pp_print_braced' Printers.pp_var_name) |
|
606 |
(CISet.elements v)) map)) |
|
676 |
Format.( |
|
677 |
fprintf fmt "@[<v 2>{ /* disjoint map */%t@] }" (fun fmt -> |
|
678 |
Hashtbl.iter |
|
679 |
(fun k v -> |
|
680 |
fprintf fmt "@,%s # %a" k |
|
681 |
(pp_print_braced' Printers.pp_var_name) |
|
682 |
(CISet.elements v)) |
|
683 |
map)) |
|
607 | 684 |
end |
608 | 685 |
|
609 |
|
|
610 | 686 |
let pp_dep_graph fmt g = |
611 |
Format.fprintf fmt "@[<v 0>@[<v 2>{ /* graph */%t@]@ }@]" |
|
612 |
(fun fmt -> |
|
613 |
IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "@ %s -> %s" s t) g) |
|
687 |
Format.fprintf fmt "@[<v 0>@[<v 2>{ /* graph */%t@]@ }@]" (fun fmt -> |
|
688 |
IdentDepGraph.iter_edges |
|
689 |
(fun s t -> Format.fprintf fmt "@ %s -> %s" s t) |
|
690 |
g) |
|
614 | 691 |
|
615 | 692 |
let pp_error fmt err = |
616 | 693 |
match err with |
617 | 694 |
| NodeCycle trace -> |
618 |
Format.fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ "
|
|
619 |
(fprintf_list ~sep:",@ " Format.pp_print_string) trace
|
|
620 |
| DataCycle traces -> (
|
|
621 |
Format.fprintf fmt "Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ "
|
|
622 |
(fprintf_list ~sep:";@ "
|
|
623 |
(fun fmt trace ->
|
|
624 |
Format.fprintf fmt "@[<v 0>{%a}@]"
|
|
625 |
(fprintf_list ~sep:",@ " Format.pp_print_string)
|
|
626 |
trace
|
|
627 |
)) traces
|
|
628 |
)
|
|
629 |
|
|
695 |
Format.fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ " |
|
696 |
(fprintf_list ~sep:",@ " Format.pp_print_string)
|
|
697 |
trace
|
|
698 |
| DataCycle traces ->
|
|
699 |
Format.fprintf fmt
|
|
700 |
"Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ "
|
|
701 |
(fprintf_list ~sep:";@ " (fun fmt trace ->
|
|
702 |
Format.fprintf fmt "@[<v 0>{%a}@]"
|
|
703 |
(fprintf_list ~sep:",@ " Format.pp_print_string)
|
|
704 |
trace))
|
|
705 |
traces
|
|
706 |
|
|
630 | 707 |
(* Merges elements of graph [g2] into graph [g1] *) |
631 | 708 |
let merge_with g1 g2 = |
632 |
begin |
|
633 |
IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2; |
|
634 |
IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2 |
|
635 |
end |
|
709 |
IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2; |
|
710 |
IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2 |
|
636 | 711 |
|
637 | 712 |
let world = "!!_world" |
638 | 713 |
|
639 | 714 |
let add_external_dependency outputs mems g = |
640 |
begin |
|
641 |
IdentDepGraph.add_vertex g world; |
|
642 |
ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs; |
|
643 |
ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems; |
|
644 |
end |
|
715 |
IdentDepGraph.add_vertex g world; |
|
716 |
ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs; |
|
717 |
ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems |
|
645 | 718 |
|
646 |
(* Takes a node and return a pair (node', graph) where node' is node |
|
647 |
rebuilt with the equations enriched with new ones introduced to |
|
648 |
"break cycles" *) |
|
719 |
(* Takes a node and return a pair (node', graph) where node' is node rebuilt |
|
720 |
with the equations enriched with new ones introduced to "break cycles" *) |
|
649 | 721 |
let global_dependency node = |
650 | 722 |
let mems = ExprDep.node_memory_variables node in |
651 | 723 |
let inputs = |
652 | 724 |
ISet.union |
653 | 725 |
(ExprDep.node_input_variables node) |
654 |
(ExprDep.node_constant_variables node) in |
|
726 |
(ExprDep.node_constant_variables node) |
|
727 |
in |
|
655 | 728 |
let outputs = ExprDep.node_output_variables node in |
656 | 729 |
let node_vars = ExprDep.node_variables node in |
657 |
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in |
|
658 |
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; |
|
659 |
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) |
|
730 |
let g_non_mems, g_mems = |
|
731 |
ExprDep.dependence_graph mems inputs node_vars node |
|
732 |
in |
|
733 |
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; Format.eprintf |
|
734 |
"g_mems: %a" pp_dep_graph g_mems;*) |
|
660 | 735 |
try |
661 | 736 |
CycleDetection.check_cycles g_non_mems; |
662 |
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
|
|
737 |
let vdecls', eqs', g_mems' = CycleDetection.break_cycles node mems g_mems in
|
|
663 | 738 |
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) |
664 |
begin
|
|
665 |
merge_with g_non_mems g_mems';
|
|
666 |
add_external_dependency outputs mems g_non_mems;
|
|
667 |
{ node with
|
|
739 |
merge_with g_non_mems g_mems';
|
|
740 |
add_external_dependency outputs mems g_non_mems;
|
|
741 |
( {
|
|
742 |
node with
|
|
668 | 743 |
node_stmts = List.map (fun eq -> Eq eq) eqs'; |
669 |
node_locals = vdecls' @ node.node_locals }, |
|
670 |
g_non_mems |
|
671 |
end |
|
672 |
with Error (DataCycle _ as exc) -> |
|
673 |
raise (Error (exc)) |
|
674 |
|
|
675 |
(* A module to sort dependencies among local variables when relying on clocked declarations *) |
|
676 |
module VarClockDep = |
|
677 |
struct |
|
744 |
node_locals = vdecls' @ node.node_locals; |
|
745 |
}, |
|
746 |
g_non_mems ) |
|
747 |
with Error (DataCycle _ as exc) -> raise (Error exc) |
|
748 |
|
|
749 |
(* A module to sort dependencies among local variables when relying on clocked |
|
750 |
declarations *) |
|
751 |
module VarClockDep = struct |
|
678 | 752 |
let rec get_clock_dep ck = |
679 | 753 |
match ck.Clocks.cdesc with |
680 |
| Clocks.Con (ck , _ ,l) -> l::(get_clock_dep ck) |
|
681 |
| Clocks.Clink ck' |
|
682 |
| Clocks.Ccarrying (_, ck') -> get_clock_dep ck' |
|
683 |
| _ -> [] |
|
684 |
|
|
754 |
| Clocks.Con (ck, _, l) -> |
|
755 |
l :: get_clock_dep ck |
|
756 |
| Clocks.Clink ck' | Clocks.Ccarrying (_, ck') -> |
|
757 |
get_clock_dep ck' |
|
758 |
| _ -> |
|
759 |
[] |
|
760 |
|
|
685 | 761 |
let sort locals = |
686 | 762 |
let g = new_graph () in |
687 |
let g = List.fold_left ( |
|
688 |
fun g var_decl -> |
|
689 |
let deps = get_clock_dep var_decl.var_clock in |
|
690 |
add_edges [var_decl.var_id] deps g |
|
691 |
) g locals |
|
763 |
let g = |
|
764 |
List.fold_left |
|
765 |
(fun g var_decl -> |
|
766 |
let deps = get_clock_dep var_decl.var_clock in |
|
767 |
add_edges [ var_decl.var_id ] deps g) |
|
768 |
g locals |
|
692 | 769 |
in |
693 | 770 |
let sorted, no_deps = |
694 |
TopologicalDepGraph.fold (fun vid (accu, remaining) -> ( |
|
695 |
let select v = v.var_id = vid in |
|
696 |
let selected, not_selected = List.partition select remaining in |
|
697 |
selected@accu, not_selected |
|
698 |
)) g ([],locals) |
|
771 |
TopologicalDepGraph.fold |
|
772 |
(fun vid (accu, remaining) -> |
|
773 |
let select v = v.var_id = vid in |
|
774 |
let selected, not_selected = List.partition select remaining in |
|
775 |
selected @ accu, not_selected) |
|
776 |
g ([], locals) |
|
699 | 777 |
in |
700 | 778 |
no_deps @ sorted |
701 |
|
|
702 | 779 |
end |
703 |
|
|
780 |
|
|
704 | 781 |
(* Local Variables: *) |
705 | 782 |
(* compile-command:"make -C .." *) |
706 | 783 |
(* End: *) |
Also available in: Unified diff
reformatting