## lustrec / src / causality.ml @ e6b644f4

History | View | Annotate | Download (25.5 KB)

1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|

2 | (* *) |
||

3 | (* The LustreC compiler toolset / The LustreC Development Team *) |
||

4 | (* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *) |
||

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 | (* This file was originally from the Prelude compiler *) |
||

11 | (* *) |
||

12 | (********************************************************************) |
||

13 | 22fe1c93 | ploc | |

14 | |||

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

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

17 | open Utils |
||

18 | 8446bf03 | ploc | open Lustre_types |

19 | 22fe1c93 | ploc | open Corelang |

20 | open Graph |
||

21 | |||

22 | e7cc5186 | ploc | |

23 | type identified_call = eq * tag |
||

24 | eb837d74 | xthirioux | type error = |

25 | e7cc5186 | ploc | | DataCycle of ident list list (* multiple failed partitions at once *) |

26 | eb837d74 | xthirioux | | NodeCycle of ident list |

27 | |||

28 | exception Error of error |
||

29 | 22fe1c93 | ploc | |

30 | |||

31 | eb837d74 | xthirioux | |

32 | 22fe1c93 | ploc | (* Dependency of mem variables on mem variables is cut off |

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

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

35 | 3bfed7f9 | xthirioux | non-mem variables are: |

36 | ec433d69 | xthirioux | - constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars |

37 | 3bfed7f9 | xthirioux | - read mems (fake vars): same remark as above. |

38 | - outputs: decoupled from mems, if necessary |
||

39 | - locals |
||

40 | - instance vars (fake vars): simplify causality analysis |
||

41 | 7352a936 | ploc | |

42 | 3bfed7f9 | xthirioux | global constants are not part of the dependency graph. |

43 | 7352a936 | ploc | |

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

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

46 | 3bfed7f9 | xthirioux | |

47 | 7352a936 | ploc | mem' = pre(no_mem, mem); |

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

49 | |||

50 | 22fe1c93 | ploc | Global roadmap: |

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

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

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

54 | - check cycles in g' |
||

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

56 | - insert g' into g |
||

57 | - return g |
||

58 | *) |
||

59 | |||

60 | 695d6f2f | xthirioux | (* Tests whether [v] is a root of graph [g], i.e. a source *) |

61 | let is_graph_root v g = |
||

62 | 7352a936 | ploc | IdentDepGraph.in_degree g v = 0 |

63 | 695d6f2f | xthirioux | |

64 | (* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *) |
||

65 | let graph_roots g = |
||

66 | 7352a936 | ploc | IdentDepGraph.fold_vertex |

67 | (fun v roots -> if is_graph_root v g then v::roots else roots) |
||

68 | g [] |
||

69 | 695d6f2f | xthirioux | |

70 | 22fe1c93 | ploc | let add_edges src tgt g = |

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

72 | List.iter |
||

73 | (fun s -> |
||

74 | List.iter |
||

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

76 | tgt) |
||

77 | src; |
||

78 | 22fe1c93 | ploc | g |

79 | |||

80 | let add_vertices vtc g = |
||

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

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

83 | 22fe1c93 | ploc | g |

84 | |||

85 | let new_graph () = |
||

86 | 7352a936 | ploc | IdentDepGraph.create () |

87 | 22fe1c93 | ploc | |

88 | a703ed0c | ploc | (* keep subgraph of [gr] consisting of nodes accessible from node [v] *) |

89 | let slice_graph gr v = |
||

90 | begin |
||

91 | let gr' = new_graph () in |
||

92 | IdentDepGraph.add_vertex gr' v; |
||

93 | 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; |
||

94 | gr' |
||

95 | end |
||

96 | |||

97 | 333e3a25 | ploc | |

98 | 22fe1c93 | ploc | module ExprDep = struct |

99 | 333e3a25 | ploc | let get_node_eqs nd = |

100 | let eqs, auts = get_node_eqs nd in |
||

101 | if auts != [] then assert false (* No call on causality on a Lustre model |
||

102 | with automaton. They should be expanded by now. *); |
||

103 | eqs |
||

104 | |||

105 | 7352a936 | ploc | let instance_var_cpt = ref 0 |

106 | 22fe1c93 | ploc | |

107 | 3bfed7f9 | xthirioux | (* read vars represent input/mem read-only vars, |

108 | they are not part of the program/schedule, |
||

109 | as they are not assigned, |
||

110 | but used to compute useless inputs/mems. |
||

111 | a mem read var represents a mem at the beginning of a cycle *) |
||

112 | 7352a936 | ploc | let mk_read_var id = |

113 | e7cc5186 | ploc | Format.sprintf "#%s" id |

114 | 3bfed7f9 | xthirioux | |

115 | (* instance vars represent node instance calls, |
||

116 | they are not part of the program/schedule, |
||

117 | but used to simplify causality analysis |
||

118 | 7352a936 | ploc | *) |

119 | let mk_instance_var id = |
||

120 | e7cc5186 | ploc | incr instance_var_cpt; Format.sprintf "!%s_%d" id !instance_var_cpt |

121 | 22fe1c93 | ploc | |

122 | 7352a936 | ploc | let is_read_var v = v.[0] = '#' |

123 | 22fe1c93 | ploc | |

124 | 7352a936 | ploc | let is_instance_var v = v.[0] = '!' |

125 | 22fe1c93 | ploc | |

126 | 7352a936 | ploc | let is_ghost_var v = is_instance_var v || is_read_var v |

127 | 3bfed7f9 | xthirioux | |

128 | 7352a936 | ploc | let undo_read_var id = |

129 | assert (is_read_var id); |
||

130 | String.sub id 1 (String.length id - 1) |
||

131 | 22fe1c93 | ploc | |

132 | 7352a936 | ploc | let undo_instance_var id = |

133 | assert (is_instance_var id); |
||

134 | String.sub id 1 (String.length id - 1) |
||

135 | 54d032f5 | xthirioux | |

136 | 7352a936 | ploc | let eq_memory_variables mems eq = |

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

138 | match rhs.expr_desc with |
||

139 | | Expr_fby _ |
||

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

141 | | Expr_tuple tl -> |
||

142 | let lhs' = (transpose_list [lhs]) in |
||

143 | List.fold_right2 match_mem lhs' tl mems |
||

144 | | _ -> mems in |
||

145 | match_mem eq.eq_lhs eq.eq_rhs mems |
||

146 | 22fe1c93 | ploc | |

147 | 7352a936 | ploc | let node_memory_variables nd = |

148 | List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd) |
||

149 | 22fe1c93 | ploc | |

150 | 7352a936 | ploc | let node_input_variables nd = |

151 | f4cba4b8 | ploc | List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty |

152 | (if nd.node_iscontract then |
||

153 | nd.node_inputs@nd.node_outputs |
||

154 | else |
||

155 | nd.node_inputs) |
||

156 | |||

157 | let node_output_variables nd = |
||

158 | List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty |
||

159 | (if nd.node_iscontract then [] else nd.node_outputs) |
||

160 | 8a183477 | xthirioux | |

161 | 7352a936 | ploc | let node_local_variables nd = |

162 | List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals |
||

163 | 3bfed7f9 | xthirioux | |

164 | 7352a936 | ploc | let node_constant_variables nd = |

165 | 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 |
||

166 | ec433d69 | xthirioux | |

167 | 7352a936 | ploc | let node_auxiliary_variables nd = |

168 | ISet.diff (node_local_variables nd) (node_memory_variables nd) |
||

169 | bb2ca5f4 | xthirioux | |

170 | 7352a936 | ploc | let node_variables nd = |

171 | let inputs = node_input_variables nd in |
||

172 | let inoutputs = List.fold_left (fun inoutputs v -> ISet.add v.var_id inoutputs) inputs nd.node_outputs in |
||

173 | List.fold_left (fun vars v -> ISet.add v.var_id vars) inoutputs nd.node_locals |
||

174 | d4807c3d | xthirioux | |

175 | 22fe1c93 | ploc | (* computes the equivalence relation relating variables |

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

177 | of class representatives *) |
||

178 | f4cba4b8 | ploc | let eqs_eq_equiv eqs = |

179 | 7352a936 | ploc | let eq_equiv = Hashtbl.create 23 in |

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

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

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

183 | ) |
||

184 | f4cba4b8 | ploc | eqs; |

185 | 7352a936 | ploc | eq_equiv |

186 | f4cba4b8 | ploc | |

187 | let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd) |
||

188 | |||

189 | 22fe1c93 | ploc | (* Create a tuple of right dimension, according to [expr] type, *) |

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

191 | 7352a936 | ploc | let adjust_tuple v expr = |

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

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

194 | | _ -> [v] |
||

195 | |||

196 | |||

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

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

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

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

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

202 | g') |
||

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

204 | g') |
||

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

206 | g') |
||

207 | | (true , true ) -> (g, |
||

208 | add_edges [x] lhs g') |
||

209 | *) |
||

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

211 | let add_var lhs_is_mem lhs x (g, g') = |
||

212 | if is_instance_var x || ISet.mem x node_vars then |
||

213 | if ISet.mem x mems |
||

214 | 3bfed7f9 | xthirioux | then |

215 | 7352a936 | ploc | let g = add_edges lhs [mk_read_var x] g in |

216 | if lhs_is_mem |
||

217 | then |
||

218 | (g, add_edges [x] lhs g') |
||

219 | else |
||

220 | (add_edges [x] lhs g, g') |
||

221 | 3bfed7f9 | xthirioux | else |

222 | 7352a936 | ploc | let x = if ISet.mem x inputs then mk_read_var x else x in |

223 | (add_edges lhs [x] g, g') |
||

224 | else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *) |
||

225 | in |
||

226 | c9043042 | ploc | (* Add dependencies from [lhs] to rhs clock [ck]. *) |

227 | 7352a936 | ploc | let rec add_clock lhs_is_mem lhs ck g = |

228 | d4807c3d | xthirioux | (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) |

229 | 7352a936 | ploc | match (Clocks.repr ck).Clocks.cdesc with |

230 | | Clocks.Con (ck', cr, _) -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g) |
||

231 | | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g |
||

232 | | _ -> g |
||

233 | in |
||

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

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

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

237 | 7352a936 | ploc | let mashup_appl_dependencies f e g = |

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

239 | 7352a936 | ploc | List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) |

240 | (expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) |
||

241 | in |
||

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 (add_clock lhs_is_mem lhs rhs.expr_clock 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) |
||

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

256 | if Basic_library.is_expr_internal_fun rhs |
||

257 | 1b01da98 | ploc | (* tuple component-wise dependency for internal operators *) |

258 | 7352a936 | ploc | then |

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

260 | 1b01da98 | ploc | (* mashed up dependency for user-defined operators *) |

261 | 7352a936 | ploc | else |

262 | mashup_appl_dependencies f e g |
||

263 | | Expr_appl (f, e, Some c) -> |
||

264 | mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g) |
||

265 | in |
||

266 | let g = |
||

267 | List.fold_left |
||

268 | (fun g lhs -> |
||

269 | if ISet.mem lhs mems then |
||

270 | add_vertices [lhs; mk_read_var lhs] g |
||

271 | else |
||

272 | add_vertices [lhs] g |
||

273 | ) |
||

274 | g eq.eq_lhs |
||

275 | in |
||

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

277 | |||

278 | 22fe1c93 | ploc | |

279 | 7352a936 | ploc | (* Returns the dependence graph for node [n] *) |

280 | let dependence_graph mems inputs node_vars n = |
||

281 | instance_var_cpt := 0; |
||

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

283 | (* Basic dependencies *) |
||

284 | let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in |
||

285 | (* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il |
||

286 | faut imposer que les outputs dépendent des asserts pour identifier que les |
||

287 | fcn calls des asserts sont évalués avant le noeuds *) |
||

288 | |||

289 | (* (\* In order to introduce dependencies between assert expressions and the node, *) |
||

290 | (* we build an artificial dependency between node output and each assert *) |
||

291 | (* expr. While these are not valid equations, they should properly propage in *) |
||

292 | (* function add_eq_dependencies *\) *) |
||

293 | (* let g = *) |
||

294 | (* let output_vars_as_lhs = ISet.elements (node_output_variables n) in *) |
||

295 | (* List.fold_left (fun g ae -> *) |
||

296 | (* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *) |
||

297 | (* add_eq_dependencies mems inputs node_vars fake_eq g *) |
||

298 | (* ) g n.node_asserts in *) |
||

299 | g |
||

300 | |||

301 | end |
||

302 | |||

303 | module NodeDep = struct |
||

304 | 22fe1c93 | ploc | |

305 | 7352a936 | ploc | module ExprModule = |

306 | struct |
||

307 | type t = expr |
||

308 | let compare = compare |
||

309 | let hash n = Hashtbl.hash n |
||

310 | let equal n1 n2 = n1 = n2 |
||

311 | end |
||

312 | |||

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

314 | |||

315 | let rec get_expr_calls prednode expr = |
||

316 | match expr.expr_desc with |
||

317 | | Expr_const _ |
||

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

319 | | Expr_access (e, _) |
||

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

321 | | Expr_array t |
||

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

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

324 | | Expr_fby (e1,e2) |
||

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

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

327 | | Expr_pre e |
||

328 | | Expr_when (e,_,_) -> get_expr_calls prednode e |
||

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

330 | if not (Basic_library.is_expr_internal_fun expr) && prednode id |
||

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

332 | else (get_expr_calls prednode e) |
||

333 | |||

334 | 861f327f | ploc | let get_eexpr_calls prednode ee = |

335 | get_expr_calls prednode ee.eexpr_qfexpr |
||

336 | |||

337 | 7352a936 | ploc | let get_callee expr = |

338 | match expr.expr_desc with |
||

339 | | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args) |
||

340 | | _ -> None |
||

341 | |||

342 | 861f327f | ploc | let accu f init objl = List.fold_left (fun accu o -> ESet.union accu (f o)) init objl |

343 | |||

344 | let get_eq_calls prednode eq = get_expr_calls prednode eq.eq_rhs |
||

345 | |||

346 | let rec get_stmt_calls prednode s = |
||

347 | match s with Eq eq -> get_eq_calls prednode eq | Aut aut -> get_aut_calls prednode aut |
||

348 | and get_aut_calls prednode aut = |
||

349 | let get_handler_calls prednode h = |
||

350 | let get_cond_calls c = accu (fun (_,e,_,_) -> get_expr_calls prednode e) ESet.empty c in |
||

351 | let until = get_cond_calls h.hand_until in |
||

352 | let unless = get_cond_calls h.hand_unless in |
||

353 | let calls = ESet.union until unless in |
||

354 | let calls = accu (get_stmt_calls prednode) calls h.hand_stmts in |
||

355 | let calls = accu (fun a -> get_expr_calls prednode a.assert_expr) calls h.hand_asserts in |
||

356 | (* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *) |
||

357 | calls |
||

358 | 333e3a25 | ploc | in |

359 | 861f327f | ploc | accu (get_handler_calls prednode) ESet.empty aut.aut_handlers |

360 | |||

361 | let get_calls prednode nd = |
||

362 | 333e3a25 | ploc | let eqs, auts = get_node_eqs nd in |

363 | 861f327f | ploc | let deps = accu (get_eq_calls prednode) ESet.empty eqs in |

364 | let deps = accu (get_aut_calls prednode) deps auts in |
||

365 | 7352a936 | ploc | ESet.elements deps |

366 | |||

367 | 861f327f | ploc | let get_contract_calls prednode c = |

368 | let deps = accu (get_stmt_calls prednode) ESet.empty c.stmts in |
||

369 | 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 |
||

370 | let id_deps = List.map (fun e -> fst (desome (get_callee e))) (ESet.elements deps) in |
||

371 | let id_deps = (List.fold_left (fun accu imp -> imp.import_nodeid::accu) [] c.imports) @ id_deps in |
||

372 | id_deps |
||

373 | |||

374 | 7352a936 | ploc | let dependence_graph prog = |

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

376 | let g = List.fold_right |
||

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

378 | match td.top_decl_desc with |
||

379 | 22fe1c93 | ploc | | Node nd -> |

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

381 | 7352a936 | ploc | let accu = add_vertices [nd.node_id] accu in |

382 | let deps = List.map |
||

383 | (fun e -> fst (desome (get_callee e))) |
||

384 | 333e3a25 | ploc | (get_calls (fun _ -> true) nd) |

385 | 7352a936 | ploc | in |

386 | (* Adding assert expressions deps *) |
||

387 | let deps_asserts = |
||

388 | let prednode = (fun _ -> true) in (* what is this about? *) |
||

389 | List.map |
||

390 | (fun e -> fst (desome (get_callee e))) |
||

391 | (ESet.elements |
||

392 | (List.fold_left |
||

393 | (fun accu assert_expr -> ESet.union accu (get_expr_calls prednode assert_expr)) |
||

394 | ESet.empty |
||

395 | (List.map (fun _assert -> _assert.assert_expr) nd.node_asserts) |
||

396 | ) |
||

397 | ) |
||

398 | in |
||

399 | 1fd3d002 | ploc | let deps_spec = match nd.node_spec with |

400 | | None -> [] |
||

401 | | Some (NodeSpec id) -> [id] |
||

402 | 861f327f | ploc | | Some (Contract c) -> get_contract_calls (fun _ -> true) c |

403 | |||

404 | 1fd3d002 | ploc | in |

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

406 | 1fd3d002 | ploc | add_edges [nd.node_id] (deps@deps_asserts@deps_spec) accu |

407 | 22fe1c93 | ploc | | _ -> assert false (* should not happen *) |

408 | 7352a936 | ploc | |

409 | ) prog g in |
||

410 | g |
||

411 | |||

412 | 22fe1c93 | ploc | let rec filter_static_inputs inputs args = |

413 | 7352a936 | ploc | match inputs, args with |

414 | | [] , [] -> [] |
||

415 | | 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 |
||

416 | | _ -> assert false |
||

417 | 22fe1c93 | ploc | |

418 | let compute_generic_calls prog = |
||

419 | List.iter |
||

420 | (fun td -> |
||

421 | match td.top_decl_desc with |
||

422 | | Node nd -> |
||

423 | 95944ba1 | ploc | let prednode n = is_generic_node (node_from_name n) in |

424 | 333e3a25 | ploc | nd.node_gencalls <- get_calls prednode nd |

425 | 22fe1c93 | ploc | | _ -> () |

426 | 7352a936 | ploc | |

427 | 22fe1c93 | ploc | ) prog |

428 | |||

429 | end |
||

430 | |||

431 | e7cc5186 | ploc | |

432 | 22fe1c93 | ploc | module CycleDetection = struct |

433 | |||

434 | 7352a936 | ploc | (* ---- Look for cycles in a dependency graph *) |

435 | 22fe1c93 | ploc | module Cycles = Graph.Components.Make (IdentDepGraph) |

436 | |||

437 | let mk_copy_var n id = |
||

438 | b08ffca7 | xthirioux | let used name = |

439 | 7352a936 | ploc | (List.exists (fun v -> v.var_id = name) n.node_locals) |

440 | b08ffca7 | xthirioux | || (List.exists (fun v -> v.var_id = name) n.node_inputs) |

441 | || (List.exists (fun v -> v.var_id = name) n.node_outputs) |
||

442 | in mk_new_name used id |
||

443 | 22fe1c93 | ploc | |

444 | let mk_copy_eq n var = |
||

445 | 01c7d5e1 | ploc | let var_decl = get_node_var var n in |

446 | 22fe1c93 | ploc | let cp_var = mk_copy_var n var in |

447 | let expr = |
||

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

449 | expr_desc = Expr_ident var; |
||

450 | expr_type = var_decl.var_type; |
||

451 | expr_clock = var_decl.var_clock; |
||

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

453 | expr_annot = None; |
||

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

455 | 54d032f5 | xthirioux | { var_decl with var_id = cp_var; var_orig = false }, |

456 | 22fe1c93 | ploc | mkeq var_decl.var_loc ([cp_var], expr) |

457 | |||

458 | let wrong_partition g partition = |
||

459 | match partition with |
||

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

461 | | _::_::_ -> true |
||

462 | | [] -> assert false |
||

463 | |||

464 | 7352a936 | ploc | (* Checks that the dependency graph [g] does not contain a cycle. Raises |

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

466 | 22fe1c93 | ploc | let check_cycles g = |

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

468 | e7cc5186 | ploc | let algebraic_loops = List.filter (wrong_partition g) scc_l in |

469 | if List.length algebraic_loops > 0 then |
||

470 | raise (Error (DataCycle algebraic_loops)) |
||

471 | (* We extract a hint to resolve the cycle: for each variable in the cycle |
||

472 | which is defined by a call, we return the name of the node call and |
||

473 | its specific id *) |
||

474 | 22fe1c93 | ploc | |

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

476 | 22fe1c93 | ploc | let copy_partition g partition = |

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

478 | IdentDepGraph.iter_edges |
||

479 | (fun src tgt -> |
||

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

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

482 | g |
||

483 | |||

484 | 7352a936 | ploc | |

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

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

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

488 | 22fe1c93 | ploc | let break_cycle head cp_head g = |

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

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

491 | 3bfed7f9 | xthirioux | IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head); |

492 | 22fe1c93 | ploc | List.iter |

493 | (fun s -> |
||

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

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

496 | succs |
||

497 | |||

498 | 7352a936 | ploc | (* Breaks cycles of the dependency graph [g] of memory variables [mems] |

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

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

501 | - a list of new equations |
||

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

503 | *) |
||

504 | 22fe1c93 | ploc | let break_cycles node mems g = |

505 | 333e3a25 | ploc | let eqs , auts = get_node_eqs node in |

506 | assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *) |
||

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

508 | 22fe1c93 | ploc | let rec break vdecls mem_eqs g = |

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

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

511 | match wrong with |
||

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

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

514 | 7352a936 | ploc | begin |

515 | IdentDepGraph.remove_edge g head head; |
||

516 | break vdecls mem_eqs g |
||

517 | end |
||

518 | 22fe1c93 | ploc | | (head::part)::_ -> |

519 | 7352a936 | ploc | begin |

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

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

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

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

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

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

526 | end |
||

527 | 22fe1c93 | ploc | | _ -> assert false |

528 | in break [] mem_eqs g |
||

529 | |||

530 | end |
||

531 | |||

532 | 8f89eba8 | xthirioux | (* Module used to compute static disjunction of variables based upon their clocks. *) |

533 | module Disjunction = |
||

534 | struct |
||

535 | add75bcb | xthirioux | module ClockedIdentModule = |

536 | struct |
||

537 | type t = var_decl |
||

538 | let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock |
||

539 | 28c58de1 | xthirioux | let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id) |

540 | add75bcb | xthirioux | end |

541 | |||

542 | module CISet = Set.Make(ClockedIdentModule) |
||

543 | 8f89eba8 | xthirioux | |

544 | add75bcb | xthirioux | (* map: var |-> list of disjoint vars, sorted in increasing branch length order, |

545 | maybe removing shorter branches *) |
||

546 | b6a94a4e | xthirioux | type disjoint_map = (ident, CISet.t) Hashtbl.t |

547 | 8f89eba8 | xthirioux | |

548 | a38c681e | xthirioux | let pp_ciset fmt t = |

549 | begin |
||

550 | Format.fprintf fmt "{@ "; |
||

551 | CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t; |
||

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

553 | end |
||

554 | |||

555 | b1a97ade | xthirioux | let clock_disjoint_map vdecls = |

556 | 8f89eba8 | xthirioux | let map = Hashtbl.create 23 in |

557 | begin |
||

558 | add75bcb | xthirioux | List.iter |

559 | (fun v1 -> let disj_v1 = |
||

560 | List.fold_left |
||

561 | b6a94a4e | xthirioux | (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res) |

562 | CISet.empty |
||

563 | add75bcb | xthirioux | vdecls in |

564 | (* disjoint vdecls are stored in increasing branch length order *) |
||

565 | Hashtbl.add map v1.var_id disj_v1) |
||

566 | vdecls; |
||

567 | b6a94a4e | xthirioux | (map : disjoint_map) |

568 | 8f89eba8 | xthirioux | end |

569 | b1a97ade | xthirioux | |

570 | 45c13277 | xthirioux | (* merge variables [v] and [v'] in disjunction [map]. Then: |

571 | 7352a936 | ploc | - the mapping v' becomes v' |-> (map v) inter (map v') |

572 | - the mapping v |-> ... then disappears |
||

573 | - other mappings become x |-> (map x) \ (if v in x then v else v') |
||

574 | add75bcb | xthirioux | *) |

575 | 45c13277 | xthirioux | let merge_in_disjoint_map map v v' = |

576 | add75bcb | xthirioux | begin |

577 | b6a94a4e | xthirioux | Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id)); |

578 | Hashtbl.remove map v.var_id; |
||

579 | 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; |
||

580 | add75bcb | xthirioux | end |

581 | |||

582 | 45c13277 | xthirioux | (* replace variable [v] by [v'] in disjunction [map]. |

583 | 7352a936 | ploc | [v'] is a dead variable. Then: |

584 | - the mapping v' becomes v' |-> (map v) |
||

585 | - the mapping v |-> ... then disappears |
||

586 | - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x) |
||

587 | 45c13277 | xthirioux | *) |

588 | let replace_in_disjoint_map map v v' = |
||

589 | begin |
||

590 | Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id); |
||

591 | Hashtbl.remove map v.var_id; |
||

592 | 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; |
||

593 | end |
||

594 | |||

595 | (* remove variable [v] in disjunction [map]. Then: |
||

596 | 7352a936 | ploc | - the mapping v |-> ... then disappears |

597 | - all mappings become x |-> (map x) \ { v} |
||

598 | 45c13277 | xthirioux | *) |

599 | let remove_in_disjoint_map map v = |
||

600 | begin |
||

601 | Hashtbl.remove map v.var_id; |
||

602 | Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map; |
||

603 | end |
||

604 | |||

605 | b1a97ade | xthirioux | let pp_disjoint_map fmt map = |

606 | begin |
||

607 | Format.fprintf fmt "{ /* disjoint map */@."; |
||

608 | b6a94a4e | xthirioux | Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map; |

609 | b1a97ade | xthirioux | Format.fprintf fmt "}@." |

610 | end |
||

611 | 8f89eba8 | xthirioux | end |

612 | |||

613 | e7cc5186 | ploc | |

614 | 22fe1c93 | ploc | let pp_dep_graph fmt g = |

615 | begin |
||

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

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

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

619 | end |
||

620 | |||

621 | eb837d74 | xthirioux | let pp_error fmt err = |

622 | match err with |
||

623 | | NodeCycle trace -> |
||

624 | e7cc5186 | ploc | Format.fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ " |

625 | (fprintf_list ~sep:",@ " Format.pp_print_string) trace |
||

626 | | DataCycle traces -> ( |
||

627 | Format.fprintf fmt "Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ " |
||

628 | (fprintf_list ~sep:";@ " |
||

629 | (fun fmt trace -> |
||

630 | Format.fprintf fmt "@[<v 0>{%a}@]" |
||

631 | (fprintf_list ~sep:",@ " Format.pp_print_string) |
||

632 | trace |
||

633 | )) traces |
||

634 | ) |
||

635 | |||

636 | 22fe1c93 | ploc | (* Merges elements of graph [g2] into graph [g1] *) |

637 | b1a97ade | xthirioux | let merge_with g1 g2 = |

638 | 45c13277 | xthirioux | begin |

639 | 22fe1c93 | ploc | IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2; |

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

641 | 45c13277 | xthirioux | end |

642 | |||

643 | 57115ec0 | xthirioux | let world = "!!_world" |

644 | |||

645 | 45c13277 | xthirioux | let add_external_dependency outputs mems g = |

646 | begin |
||

647 | 57115ec0 | xthirioux | IdentDepGraph.add_vertex g world; |

648 | ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs; |
||

649 | ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems; |
||

650 | 45c13277 | xthirioux | end |

651 | 22fe1c93 | ploc | |

652 | f4cba4b8 | ploc | (* Takes a node and return a pair (node', graph) where node' is node |

653 | rebuilt with the equations enriched with new ones introduced to |
||

654 | "break cycles" *) |
||

655 | 22fe1c93 | ploc | let global_dependency node = |

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

657 | ec433d69 | xthirioux | let inputs = |

658 | ISet.union |
||

659 | (ExprDep.node_input_variables node) |
||

660 | (ExprDep.node_constant_variables node) in |
||

661 | 45c13277 | xthirioux | let outputs = ExprDep.node_output_variables node in |

662 | 3bfed7f9 | xthirioux | let node_vars = ExprDep.node_variables node in |

663 | let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in |
||

664 | 22fe1c93 | ploc | (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; |

665 | 7352a936 | ploc | Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) |

666 | e7cc5186 | ploc | try |

667 | CycleDetection.check_cycles g_non_mems; |
||

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

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

670 | begin |
||

671 | merge_with g_non_mems g_mems'; |
||

672 | add_external_dependency outputs mems g_non_mems; |
||

673 | { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, |
||

674 | g_non_mems |
||

675 | end |
||

676 | with Error (DataCycle _ as exc) -> ( |
||

677 | raise (Error (exc)) |
||

678 | ) |
||

679 | 22fe1c93 | ploc | |

680 | 70466917 | ploc | (* A module to sort dependencies among local variables when relying on clocked declarations *) |

681 | module VarClockDep = |
||

682 | struct |
||

683 | let rec get_clock_dep ck = |
||

684 | match ck.Clocks.cdesc with |
||

685 | | Clocks.Con (ck ,c ,l) -> l::(get_clock_dep ck) |
||

686 | | Clocks.Clink ck' |
||

687 | | Clocks.Ccarrying (_, ck') -> get_clock_dep ck' |
||

688 | | _ -> [] |
||

689 | |||

690 | let sort locals = |
||

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

692 | let g = List.fold_left ( |
||

693 | fun g var_decl -> |
||

694 | let deps = get_clock_dep var_decl.var_clock in |
||

695 | add_edges [var_decl.var_id] deps g |
||

696 | ) g locals |
||

697 | in |
||

698 | let sorted, no_deps = |
||

699 | TopologicalDepGraph.fold (fun vid (accu, remaining) -> ( |
||

700 | let select v = v.var_id = vid in |
||

701 | let selected, not_selected = List.partition select remaining in |
||

702 | selected@accu, not_selected |
||

703 | )) g ([],locals) |
||

704 | in |
||

705 | no_deps @ sorted |
||

706 | |||

707 | end |
||

708 | |||

709 | 22fe1c93 | ploc | (* Local Variables: *) |

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

711 | (* End: *) |