Revision d4807c3d src/causality.ml
src/causality.ml | ||
---|---|---|
113 | 113 |
let node_memory_variables nd = |
114 | 114 |
List.fold_left eq_memory_variables ISet.empty nd.node_eqs |
115 | 115 |
|
116 |
let node_non_input_variables nd = |
|
117 |
let outputs = List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs in |
|
118 |
List.fold_left (fun non_inputs v -> ISet.add v.var_id non_inputs) outputs nd.node_locals |
|
119 |
|
|
116 | 120 |
(* computes the equivalence relation relating variables |
117 | 121 |
in the same equation lhs, under the form of a table |
118 | 122 |
of class representatives *) |
... | ... | |
132 | 136 |
| Types.Ttuple tl -> duplicate v (List.length tl) |
133 | 137 |
| _ -> [v] |
134 | 138 |
|
139 |
|
|
135 | 140 |
(* Add dependencies from lhs to rhs in [g, g'], *) |
136 | 141 |
(* no-mem/no-mem and mem/no-mem in g *) |
137 | 142 |
(* mem/mem in g' *) |
138 | 143 |
(* excluding all/[inputs] *) |
139 |
let add_eq_dependencies mems inputs eq (g, g') = |
|
140 |
let rec add_dep lhs_is_mem lhs rhs g = |
|
141 |
let add_var x (g, g') = |
|
142 |
if ISet.mem x inputs then (g, g') else |
|
144 |
let add_eq_dependencies mems non_inputs eq (g, g') = |
|
145 |
let add_var lhs_is_mem lhs x (g, g') = |
|
146 |
if ISet.mem x non_inputs then |
|
143 | 147 |
match (lhs_is_mem, ISet.mem x mems) with |
144 | 148 |
| (false, true ) -> (add_edges [x] lhs g, g' ) |
145 | 149 |
| (false, false) -> (add_edges lhs [x] g, g' ) |
146 | 150 |
| (true , false) -> (add_edges lhs [x] g, g' ) |
147 |
| (true , true ) -> (g , add_edges [x] lhs g') in |
|
151 |
| (true , true ) -> (g , add_edges [x] lhs g') |
|
152 |
else (g, g') in |
|
153 |
(* Add dependencies from [lhs] to rhs clock [ck]. *) |
|
154 |
let rec add_clock lhs_is_mem lhs ck g = |
|
155 |
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) |
|
156 |
match (Clocks.repr ck).Clocks.cdesc with |
|
157 |
| Clocks.Con (ck', cr, _) -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g) |
|
158 |
| Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g |
|
159 |
| _ -> g in |
|
160 |
let rec add_dep lhs_is_mem lhs rhs g = |
|
148 | 161 |
(* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *) |
149 | 162 |
(* i.e every input is connected to every output, through a ghost var *) |
150 | 163 |
let mashup_appl_dependencies f e g = |
151 | 164 |
let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in |
152 | 165 |
List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) |
153 |
(expr_list_of_expr e) (add_var f_var g) in |
|
166 |
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) in
|
|
154 | 167 |
match rhs.expr_desc with |
155 | 168 |
| Expr_const _ -> g |
156 | 169 |
| Expr_fby (e1, e2) -> add_dep true lhs e2 (add_dep false lhs e1 g) |
157 | 170 |
| Expr_pre e -> add_dep true lhs e g |
158 |
| Expr_ident x -> add_var x g
|
|
171 |
| Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
|
|
159 | 172 |
| Expr_access (e1, _) |
160 | 173 |
| Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g |
161 | 174 |
| Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g |
162 | 175 |
| Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g |
163 |
| Expr_merge (c, hl) -> add_var c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g) |
|
176 |
| 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)
|
|
164 | 177 |
| 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)) |
165 | 178 |
| Expr_arrow (e1, e2) -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) |
166 |
| Expr_when (e, c, _) -> add_dep lhs_is_mem lhs e (add_var c g) |
|
179 |
| Expr_when (e, c, _) -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
|
|
167 | 180 |
| Expr_appl (f, e, None) -> |
168 | 181 |
if Basic_library.is_internal_fun f |
169 | 182 |
(* tuple component-wise dependency for internal operators *) |
... | ... | |
173 | 186 |
else |
174 | 187 |
mashup_appl_dependencies f e g |
175 | 188 |
| Expr_appl (f, e, Some (r, _)) -> |
176 |
mashup_appl_dependencies f e (add_var r g) |
|
189 |
mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g)
|
|
177 | 190 |
| Expr_uclock (e, _) |
178 | 191 |
| Expr_dclock (e, _) |
179 | 192 |
| Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g |
... | ... | |
182 | 195 |
|
183 | 196 |
|
184 | 197 |
(* Returns the dependence graph for node [n] *) |
185 |
let dependence_graph mems n = |
|
198 |
let dependence_graph mems non_inputs n =
|
|
186 | 199 |
eq_var_cpt := 0; |
187 | 200 |
instance_var_cpt := 0; |
188 | 201 |
let g = new_graph (), new_graph () in |
189 |
let inputs = List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty n.node_inputs in |
|
190 | 202 |
(* Basic dependencies *) |
191 |
let g = List.fold_right (add_eq_dependencies mems inputs) n.node_eqs g in |
|
203 |
let g = List.fold_right (add_eq_dependencies mems non_inputs) n.node_eqs g in
|
|
192 | 204 |
g |
193 | 205 |
|
194 | 206 |
end |
... | ... | |
385 | 397 |
|
386 | 398 |
let global_dependency node = |
387 | 399 |
let mems = ExprDep.node_memory_variables node in |
388 |
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems node in |
|
400 |
let non_inputs = ExprDep.node_non_input_variables node in |
|
401 |
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems non_inputs node in |
|
389 | 402 |
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; |
390 | 403 |
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) |
391 | 404 |
CycleDetection.check_cycles g_non_mems; |
Also available in: Unified diff