## lustrec / src / causality.ml @ 22fe1c93

History | View | Annotate | Download (13.3 KB)

1 | 22fe1c93 | ploc | (* ---------------------------------------------------------------------------- |
---|---|---|---|

2 | * SchedMCore - A MultiCore Scheduling Framework |
||

3 | * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
||

4 | * |
||

5 | * This file is part of Prelude |
||

6 | * |
||

7 | * Prelude is free software; you can redistribute it and/or |
||

8 | * modify it under the terms of the GNU Lesser General Public License |
||

9 | * as published by the Free Software Foundation ; either version 2 of |
||

10 | * the License, or (at your option) any later version. |
||

11 | * |
||

12 | * Prelude is distributed in the hope that it will be useful, but |
||

13 | * WITHOUT ANY WARRANTY ; without even the implied warranty of |
||

14 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
||

15 | * Lesser General Public License for more details. |
||

16 | * |
||

17 | * You should have received a copy of the GNU Lesser General Public |
||

18 | * License along with this program ; if not, write to the Free Software |
||

19 | * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
||

20 | * USA |
||

21 | *---------------------------------------------------------------------------- *) |
||

22 | |||

23 | |||

24 | (** Simple modular syntactic causality analysis. Can reject correct |
||

25 | programs, especially if the program is not flattened first. *) |
||

26 | open Utils |
||

27 | open LustreSpec |
||

28 | open Corelang |
||

29 | open Graph |
||

30 | open Format |
||

31 | |||

32 | exception Cycle of ident list |
||

33 | |||

34 | module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule) |
||

35 | |||

36 | (*module IdentDepGraphUtil = Oper.P(IdentDepGraph)*) |
||

37 | |||

38 | (* Dependency of mem variables on mem variables is cut off |
||

39 | by duplication of some mem vars into local node vars. |
||

40 | Thus, cylic dependency errors may only arise between no-mem vars. |
||

41 | |||

42 | no_mem' = combinational(no_mem, mem); |
||

43 | => (mem -> no_mem' -> no_mem) |
||

44 | |||

45 | mem' = pre(no_mem, mem); |
||

46 | => (mem' -> no_mem), (mem -> mem') |
||

47 | |||

48 | Global roadmap: |
||

49 | - compute two dep graphs g (non-mem/non-mem&mem) and g' (mem/mem) |
||

50 | - check cycles in g (a cycle means a dependency error) |
||

51 | - break cycles in g' (it's legal !): |
||

52 | - check cycles in g' |
||

53 | - if any, introduce aux var to break cycle, then start afresh |
||

54 | - insert g' into g |
||

55 | - return g |
||

56 | *) |
||

57 | |||

58 | let add_edges src tgt g = |
||

59 | (*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*) |
||

60 | List.iter |
||

61 | (fun s -> |
||

62 | List.iter |
||

63 | (fun t -> IdentDepGraph.add_edge g s t) |
||

64 | tgt) |
||

65 | src; |
||

66 | g |
||

67 | |||

68 | let add_vertices vtc g = |
||

69 | (*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*) |
||

70 | List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc; |
||

71 | g |
||

72 | |||

73 | let new_graph () = |
||

74 | IdentDepGraph.create () |
||

75 | |||

76 | module ExprDep = struct |
||

77 | |||

78 | let eq_var_cpt = ref 0 |
||

79 | |||

80 | let instance_var_cpt = ref 0 |
||

81 | |||

82 | let mk_eq_var id = |
||

83 | incr eq_var_cpt; sprintf "#%s_%d" id !eq_var_cpt |
||

84 | |||

85 | let mk_instance_var id = |
||

86 | incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt |
||

87 | |||

88 | let is_eq_var v = v.[0] = '#' |
||

89 | |||

90 | let is_instance_var v = v.[0] = '!' |
||

91 | |||

92 | let is_ghost_var v = is_instance_var v || is_eq_var v |
||

93 | |||

94 | let eq_memory_variables mems eq = |
||

95 | let rec match_mem lhs rhs mems = |
||

96 | match rhs.expr_desc with |
||

97 | | Expr_fby _ |
||

98 | | Expr_pre _ -> List.fold_right ISet.add lhs mems |
||

99 | | Expr_tuple tl -> List.fold_right2 match_mem (transpose_list [lhs]) tl mems |
||

100 | | _ -> mems in |
||

101 | match_mem eq.eq_lhs eq.eq_rhs mems |
||

102 | |||

103 | let node_memory_variables nd = |
||

104 | List.fold_left eq_memory_variables ISet.empty nd.node_eqs |
||

105 | |||

106 | (* computes the equivalence relation relating variables |
||

107 | in the same equation lhs, under the form of a table |
||

108 | of class representatives *) |
||

109 | let node_eq_equiv nd = |
||

110 | let eq_equiv = Hashtbl.create 23 in |
||

111 | List.iter (fun eq -> |
||

112 | let first = List.hd eq.eq_lhs in |
||

113 | List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs |
||

114 | ) |
||

115 | nd.node_eqs; |
||

116 | eq_equiv |
||

117 | |||

118 | (* Create a tuple of right dimension, according to [expr] type, *) |
||

119 | (* filled with variable [v] *) |
||

120 | let adjust_tuple v expr = |
||

121 | match expr.expr_type.Types.tdesc with |
||

122 | | Types.Ttuple tl -> duplicate v (List.length tl) |
||

123 | | _ -> [v] |
||

124 | |||

125 | (* Add dependencies from lhs to rhs in [g, g'], *) |
||

126 | (* no-mem/no-mem and mem/no-mem in g *) |
||

127 | (* mem/mem in g' *) |
||

128 | (* excluding all/[inputs] *) |
||

129 | let add_eq_dependencies mems inputs eq (g, g') = |
||

130 | let rec add_dep lhs_is_mem lhs rhs g = |
||

131 | let add_var x (g, g') = |
||

132 | if ISet.mem x inputs then (g, g') else |
||

133 | match (lhs_is_mem, ISet.mem x mems) with |
||

134 | | (false, true ) -> (add_edges [x] lhs g, g' ) |
||

135 | | (false, false) -> (add_edges lhs [x] g, g' ) |
||

136 | | (true , false) -> (add_edges lhs [x] g, g' ) |
||

137 | | (true , true ) -> (g , add_edges [x] lhs g') in |
||

138 | (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *) |
||

139 | (* i.e every input is connected to every output, through a ghost var *) |
||

140 | let mashup_appl_dependencies f e g = |
||

141 | let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in |
||

142 | List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) |
||

143 | (expr_list_of_expr e) (add_var f_var g) in |
||

144 | match rhs.expr_desc with |
||

145 | | Expr_const _ -> g |
||

146 | | Expr_fby (e1, e2) -> add_dep true lhs e2 (add_dep false lhs e1 g) |
||

147 | | Expr_pre e -> add_dep true lhs e g |
||

148 | | Expr_ident x -> add_var x g |
||

149 | | Expr_access (e1, _) |
||

150 | | Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g |
||

151 | | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g |
||

152 | | Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g |
||

153 | | Expr_merge (c, hl) -> add_var c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g) |
||

154 | | 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)) |
||

155 | | Expr_arrow (e1, e2) -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) |
||

156 | | Expr_when (e, c, _) -> add_dep lhs_is_mem lhs e (add_var c g) |
||

157 | | Expr_appl (f, e, None) -> |
||

158 | if Basic_library.is_internal_fun f |
||

159 | (* tuple component-wise dependency for internal operators *) |
||

160 | then |
||

161 | List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g |
||

162 | (* mashed up dependency for user-defined operators *) |
||

163 | else |
||

164 | mashup_appl_dependencies f e g |
||

165 | | Expr_appl (f, e, Some (r, _)) -> |
||

166 | mashup_appl_dependencies f e (add_var r g) |
||

167 | | Expr_uclock (e, _) |
||

168 | | Expr_dclock (e, _) |
||

169 | | Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g |
||

170 | in |
||

171 | add_dep false eq.eq_lhs eq.eq_rhs (add_vertices eq.eq_lhs g, g') |
||

172 | |||

173 | |||

174 | (* Returns the dependence graph for node [n] *) |
||

175 | let dependence_graph mems n = |
||

176 | eq_var_cpt := 0; |
||

177 | instance_var_cpt := 0; |
||

178 | let g = new_graph (), new_graph () in |
||

179 | let inputs = List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty n.node_inputs in |
||

180 | (* Basic dependencies *) |
||

181 | let g = List.fold_right (add_eq_dependencies mems inputs) n.node_eqs g in |
||

182 | g |
||

183 | |||

184 | end |
||

185 | |||

186 | module NodeDep = struct |
||

187 | |||

188 | module ExprModule = |
||

189 | struct |
||

190 | type t = expr |
||

191 | let compare = compare |
||

192 | let hash n = Hashtbl.hash n |
||

193 | let equal n1 n2 = n1 = n2 |
||

194 | end |
||

195 | |||

196 | module ESet = Set.Make(ExprModule) |
||

197 | |||

198 | let rec get_expr_calls prednode expr = |
||

199 | match expr.expr_desc with |
||

200 | | Expr_const _ |
||

201 | | Expr_ident _ -> ESet.empty |
||

202 | | Expr_access (e, _) |
||

203 | | Expr_power (e, _) -> get_expr_calls prednode e |
||

204 | | Expr_array t |
||

205 | | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty |
||

206 | | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty |
||

207 | | Expr_fby (e1,e2) |
||

208 | | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) |
||

209 | | Expr_ite (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) |
||

210 | | Expr_pre e |
||

211 | | Expr_when (e,_,_) |
||

212 | | Expr_uclock (e,_) |
||

213 | | Expr_dclock (e,_) |
||

214 | | Expr_phclock (e,_) -> get_expr_calls prednode e |
||

215 | | Expr_appl (id,e, _) -> |
||

216 | if not (Basic_library.is_internal_fun id) && prednode id |
||

217 | then ESet.add expr (get_expr_calls prednode e) |
||

218 | else (get_expr_calls prednode e) |
||

219 | |||

220 | let get_callee expr = |
||

221 | match expr.expr_desc with |
||

222 | | Expr_appl (id, args, _) -> id, expr_list_of_expr args |
||

223 | | _ -> assert false |
||

224 | |||

225 | let get_calls prednode eqs = |
||

226 | let deps = |
||

227 | List.fold_left |
||

228 | (fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs)) |
||

229 | ESet.empty |
||

230 | eqs in |
||

231 | ESet.elements deps |
||

232 | |||

233 | let dependence_graph prog = |
||

234 | let g = new_graph () in |
||

235 | let g = List.fold_right |
||

236 | (fun td accu -> (* for each node we add its dependencies *) |
||

237 | match td.top_decl_desc with |
||

238 | | Node nd -> |
||

239 | (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) |
||

240 | let accu = add_vertices [nd.node_id] accu in |
||

241 | let deps = List.map (fun e -> fst (get_callee e)) (get_calls (fun _ -> true) nd.node_eqs) in |
||

242 | (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) |
||

243 | add_edges [nd.node_id] deps accu |
||

244 | | _ -> assert false (* should not happen *) |
||

245 | |||

246 | ) prog g in |
||

247 | g |
||

248 | |||

249 | let rec filter_static_inputs inputs args = |
||

250 | match inputs, args with |
||

251 | | [] , [] -> [] |
||

252 | | v::vq, a::aq -> if v.var_dec_const then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq |
||

253 | | _ -> assert false |
||

254 | |||

255 | let compute_generic_calls prog = |
||

256 | List.iter |
||

257 | (fun td -> |
||

258 | match td.top_decl_desc with |
||

259 | | Node nd -> |
||

260 | let prednode n = is_generic_node (Hashtbl.find node_table n) in |
||

261 | nd.node_gencalls <- get_calls prednode nd.node_eqs |
||

262 | | _ -> () |
||

263 | |||

264 | ) prog |
||

265 | |||

266 | end |
||

267 | |||

268 | module CycleDetection = struct |
||

269 | |||

270 | (* ---- Look for cycles in a dependency graph *) |
||

271 | module Cycles = Graph.Components.Make (IdentDepGraph) |
||

272 | |||

273 | let mk_copy_var n id = |
||

274 | mk_new_name (node_vars n) id |
||

275 | |||

276 | let mk_copy_eq n var = |
||

277 | let var_decl = node_var var n in |
||

278 | let cp_var = mk_copy_var n var in |
||

279 | let expr = |
||

280 | { expr_tag = Utils.new_tag (); |
||

281 | expr_desc = Expr_ident var; |
||

282 | expr_type = var_decl.var_type; |
||

283 | expr_clock = var_decl.var_clock; |
||

284 | expr_delay = Delay.new_var (); |
||

285 | expr_annot = None; |
||

286 | expr_loc = var_decl.var_loc } in |
||

287 | { var_decl with var_id = cp_var }, |
||

288 | mkeq var_decl.var_loc ([cp_var], expr) |
||

289 | |||

290 | let wrong_partition g partition = |
||

291 | match partition with |
||

292 | | [id] -> IdentDepGraph.mem_edge g id id |
||

293 | | _::_::_ -> true |
||

294 | | [] -> assert false |
||

295 | |||

296 | (* Checks that the dependency graph [g] does not contain a cycle. Raises |
||

297 | [Cycle partition] if the succession of dependencies [partition] forms a cycle *) |
||

298 | let check_cycles g = |
||

299 | let scc_l = Cycles.scc_list g in |
||

300 | List.iter (fun partition -> |
||

301 | if wrong_partition g partition then |
||

302 | raise (Cycle partition) |
||

303 | else () |
||

304 | ) scc_l |
||

305 | |||

306 | (* Creates the sub-graph of [g] restricted to vertices and edges in partition *) |
||

307 | let copy_partition g partition = |
||

308 | let copy_g = IdentDepGraph.create () in |
||

309 | IdentDepGraph.iter_edges |
||

310 | (fun src tgt -> |
||

311 | if List.mem src partition && List.mem tgt partition |
||

312 | then IdentDepGraph.add_edge copy_g src tgt) |
||

313 | g |
||

314 | |||

315 | |||

316 | (* Breaks dependency cycles in a graph [g] by inserting aux variables. |
||

317 | [head] is a head of a non-trivial scc of [g]. |
||

318 | In Lustre, this is legal only for mem/mem cycles *) |
||

319 | let break_cycle head cp_head g = |
||

320 | let succs = IdentDepGraph.succ g head in |
||

321 | IdentDepGraph.add_edge g head cp_head; |
||

322 | List.iter |
||

323 | (fun s -> |
||

324 | IdentDepGraph.remove_edge g head s; |
||

325 | IdentDepGraph.add_edge g s cp_head) |
||

326 | succs |
||

327 | |||

328 | (* Breaks cycles of the dependency graph [g] of memory variables [mems] |
||

329 | belonging in node [node]. Returns: |
||

330 | - a list of new auxiliary variable declarations |
||

331 | - a list of new equations |
||

332 | - a modified acyclic version of [g] |
||

333 | *) |
||

334 | let break_cycles node mems g = |
||

335 | let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) node.node_eqs in |
||

336 | let rec break vdecls mem_eqs g = |
||

337 | let scc_l = Cycles.scc_list g in |
||

338 | let wrong = List.filter (wrong_partition g) scc_l in |
||

339 | match wrong with |
||

340 | | [] -> (vdecls, non_mem_eqs@mem_eqs, g) |
||

341 | | [head]::_ -> |
||

342 | begin |
||

343 | IdentDepGraph.remove_edge g head head; |
||

344 | break vdecls mem_eqs g |
||

345 | end |
||

346 | | (head::part)::_ -> |
||

347 | begin |
||

348 | let vdecl_cp_head, cp_eq = mk_copy_eq node head in |
||

349 | let pvar v = List.mem v part in |
||

350 | let fvar v = if v = head then vdecl_cp_head.var_id else v in |
||

351 | let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in |
||

352 | break_cycle head vdecl_cp_head.var_id g; |
||

353 | break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g |
||

354 | end |
||

355 | | _ -> assert false |
||

356 | in break [] mem_eqs g |
||

357 | |||

358 | end |
||

359 | |||

360 | let pp_dep_graph fmt g = |
||

361 | begin |
||

362 | Format.fprintf fmt "{ /* graph */@."; |
||

363 | IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g; |
||

364 | Format.fprintf fmt "}@." |
||

365 | end |
||

366 | |||

367 | let pp_error fmt trace = |
||

368 | fprintf fmt "@.Causality error, cyclic data dependencies: %a@." |
||

369 | (fprintf_list ~sep:"->" pp_print_string) trace |
||

370 | |||

371 | (* Merges elements of graph [g2] into graph [g1] *) |
||

372 | let merge_with g1 g2 = |
||

373 | IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2; |
||

374 | IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2 |
||

375 | |||

376 | let global_dependency node = |
||

377 | let mems = ExprDep.node_memory_variables node in |
||

378 | let (g_non_mems, g_mems) = ExprDep.dependence_graph mems node in |
||

379 | (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; |
||

380 | Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) |
||

381 | CycleDetection.check_cycles g_non_mems; |
||

382 | let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in |
||

383 | (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) |
||

384 | merge_with g_non_mems g_mems'; |
||

385 | { node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, |
||

386 | g_non_mems |
||

387 | |||

388 | |||

389 | (* Local Variables: *) |
||

390 | (* compile-command:"make -C .." *) |
||

391 | (* End: *) |