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