Revision 7352a936
Added by PierreLoïc Garoche over 7 years ago
src/causality.ml  

40  40 
 outputs: decoupled from mems, if necessary 
41  41 
 locals 
42  42 
 instance vars (fake vars): simplify causality analysis 
43  
43 


44  44 
global constants are not part of the dependency graph. 
45 


46 
no_mem' = combinational(no_mem, mem); 

47 
=> (mem > no_mem' > no_mem) 

45  48  
46 
no_mem' = combinational(no_mem, mem); 

47 
=> (mem > no_mem' > no_mem) 

48  
49 
mem' = pre(no_mem, mem); 

50 
=> (mem' > no_mem), (mem > mem') 

51  
49 
mem' = pre(no_mem, mem); 

50 
=> (mem' > no_mem), (mem > mem') 

51 


52  52 
Global roadmap: 
53  53 
 compute two dep graphs g (nonmem/nonmem&mem) and g' (mem/mem) 
54  54 
 check cycles in g (a cycle means a dependency error) 
...  ...  
61  61  
62  62 
(* Tests whether [v] is a root of graph [g], i.e. a source *) 
63  63 
let is_graph_root v g = 
64 
IdentDepGraph.in_degree g v = 0 

64 
IdentDepGraph.in_degree g v = 0


65  65  
66  66 
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *) 
67  67 
let graph_roots g = 
68 
IdentDepGraph.fold_vertex 

69 
(fun v roots > if is_graph_root v g then v::roots else roots) 

70 
g [] 

68 
IdentDepGraph.fold_vertex


69 
(fun v roots > if is_graph_root v g then v::roots else roots)


70 
g []


71  71  
72  72 
let add_edges src tgt g = 
73 
(*List.iter (fun s > List.iter (fun t > Format.eprintf "add %s > %s@." s t) tgt) src;*) 

74 
List.iter 

75 
(fun s > 

76 
List.iter 

77 
(fun t > IdentDepGraph.add_edge g s t)


78 
tgt)


79 
src; 

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


74 
List.iter


75 
(fun s >


76 
List.iter


77 
(fun t > IdentDepGraph.add_edge g s t)


78 
tgt)


79 
src;


80  80 
g 
81  81  
82  82 
let add_vertices vtc g = 
83 
(*List.iter (fun t > Format.eprintf "add %s@." t) vtc;*) 

84 
List.iter (fun v > IdentDepGraph.add_vertex g v) vtc; 

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


84 
List.iter (fun v > IdentDepGraph.add_vertex g v) vtc;


85  85 
g 
86  86  
87  87 
let new_graph () = 
88 
IdentDepGraph.create () 

88 
IdentDepGraph.create ()


89  89  
90  90 
module ExprDep = struct 
91  91  
92 
let instance_var_cpt = ref 0 

92 
let instance_var_cpt = ref 0


93  93  
94  94 
(* read vars represent input/mem readonly vars, 
95  95 
they are not part of the program/schedule, 
96  96 
as they are not assigned, 
97  97 
but used to compute useless inputs/mems. 
98  98 
a mem read var represents a mem at the beginning of a cycle *) 
99 
let mk_read_var id = 

100 
sprintf "#%s" id 

99 
let mk_read_var id =


100 
sprintf "#%s" id


101  101  
102  102 
(* instance vars represent node instance calls, 
103  103 
they are not part of the program/schedule, 
104  104 
but used to simplify causality analysis 
105 
*)


106 
let mk_instance_var id = 

107 
incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt 

105 
*) 

106 
let mk_instance_var id =


107 
incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt


108  108  
109 
let is_read_var v = v.[0] = '#' 

109 
let is_read_var v = v.[0] = '#'


110  110  
111 
let is_instance_var v = v.[0] = '!' 

111 
let is_instance_var v = v.[0] = '!'


112  112  
113 
let is_ghost_var v = is_instance_var v  is_read_var v 

113 
let is_ghost_var v = is_instance_var v  is_read_var v


114  114  
115 
let undo_read_var id = 

116 
assert (is_read_var id); 

117 
String.sub id 1 (String.length id  1) 

115 
let undo_read_var id =


116 
assert (is_read_var id);


117 
String.sub id 1 (String.length id  1)


118  118  
119 
let undo_instance_var id = 

120 
assert (is_instance_var id); 

121 
String.sub id 1 (String.length id  1) 

119 
let undo_instance_var id =


120 
assert (is_instance_var id);


121 
String.sub id 1 (String.length id  1)


122  122  
123 
let eq_memory_variables mems eq = 

124 
let rec match_mem lhs rhs mems = 

125 
match rhs.expr_desc with 

126 
 Expr_fby _ 

127 
 Expr_pre _ > List.fold_right ISet.add lhs mems 

128 
 Expr_tuple tl > 

129 
let lhs' = (transpose_list [lhs]) in


130 
List.fold_right2 match_mem lhs' tl mems


131 
 _ > mems in 

132 
match_mem eq.eq_lhs eq.eq_rhs mems 

123 
let eq_memory_variables mems eq =


124 
let rec match_mem lhs rhs mems =


125 
match rhs.expr_desc with


126 
 Expr_fby _


127 
 Expr_pre _ > List.fold_right ISet.add lhs mems


128 
 Expr_tuple tl >


129 
let lhs' = (transpose_list [lhs]) in


130 
List.fold_right2 match_mem lhs' tl mems


131 
 _ > mems in


132 
match_mem eq.eq_lhs eq.eq_rhs mems


133  133  
134 
let node_memory_variables nd = 

135 
List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd) 

134 
let node_memory_variables nd =


135 
List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)


136  136  
137 
let node_input_variables nd = 

138 
List.fold_left (fun inputs v > ISet.add v.var_id inputs) ISet.empty nd.node_inputs 

137 
let node_input_variables nd =


138 
List.fold_left (fun inputs v > ISet.add v.var_id inputs) ISet.empty nd.node_inputs


139  139  
140 
let node_local_variables nd = 

141 
List.fold_left (fun locals v > ISet.add v.var_id locals) ISet.empty nd.node_locals 

140 
let node_local_variables nd =


141 
List.fold_left (fun locals v > ISet.add v.var_id locals) ISet.empty nd.node_locals


142  142  
143 
let node_constant_variables nd = 

144 
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 

143 
let node_constant_variables nd =


144 
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


145  145  
146 
let node_output_variables nd = 

147 
List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs 

146 
let node_output_variables nd =


147 
List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs


148  148  
149 
let node_auxiliary_variables nd = 

150 
ISet.diff (node_local_variables nd) (node_memory_variables nd) 

149 
let node_auxiliary_variables nd =


150 
ISet.diff (node_local_variables nd) (node_memory_variables nd)


151  151  
152 
let node_variables nd = 

153 
let inputs = node_input_variables nd in 

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

155 
List.fold_left (fun vars v > ISet.add v.var_id vars) inoutputs nd.node_locals 

152 
let node_variables nd =


153 
let inputs = node_input_variables nd in


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


155 
List.fold_left (fun vars v > ISet.add v.var_id vars) inoutputs nd.node_locals


156  156  
157  157 
(* computes the equivalence relation relating variables 
158  158 
in the same equation lhs, under the form of a table 
159  159 
of class representatives *) 
160 
let node_eq_equiv nd = 

161 
let eq_equiv = Hashtbl.create 23 in 

162 
List.iter (fun eq > 

163 
let first = List.hd eq.eq_lhs in 

164 
List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs 

165 
) 

166 
(get_node_eqs nd); 

167 
eq_equiv 

160 
let node_eq_equiv nd =


161 
let eq_equiv = Hashtbl.create 23 in


162 
List.iter (fun eq >


163 
let first = List.hd eq.eq_lhs in


164 
List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs


165 
)


166 
(get_node_eqs nd);


167 
eq_equiv


168  168  
169  169 
(* Create a tuple of right dimension, according to [expr] type, *) 
170  170 
(* filled with variable [v] *) 
171 
let adjust_tuple v expr = 

172 
match expr.expr_type.Types.tdesc with 

173 
 Types.Ttuple tl > duplicate v (List.length tl) 

174 
 _ > [v] 

175  
176  
177 
(* Add dependencies from lhs to rhs in [g, g'], *) 

178 
(* nomem/nomem and mem/nomem in g *) 

179 
(* mem/mem in g' *) 

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

181 
 (false, true ) > (add_edges [x] lhs g, 

182 
g') 

183 
 (false, false) > (add_edges lhs [x] g, 

184 
g') 

185 
 (true , false) > (add_edges lhs [x] g, 

186 
g') 

187 
 (true , true ) > (g, 

188 
add_edges [x] lhs g') 

189 
*) 

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

191 
let add_var lhs_is_mem lhs x (g, g') = 

192 
if is_instance_var x  ISet.mem x node_vars then 

193 
if ISet.mem x mems 

194 
then 

195 
let g = add_edges lhs [mk_read_var x] g in 

196 
if lhs_is_mem 

171 
let adjust_tuple v expr = 

172 
match expr.expr_type.Types.tdesc with 

173 
 Types.Ttuple tl > duplicate v (List.length tl) 

174 
 _ > [v] 

175  
176  
177 
(* Add dependencies from lhs to rhs in [g, g'], *) 

178 
(* nomem/nomem and mem/nomem in g *) 

179 
(* mem/mem in g' *) 

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

181 
 (false, true ) > (add_edges [x] lhs g, 

182 
g') 

183 
 (false, false) > (add_edges lhs [x] g, 

184 
g') 

185 
 (true , false) > (add_edges lhs [x] g, 

186 
g') 

187 
 (true , true ) > (g, 

188 
add_edges [x] lhs g') 

189 
*) 

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

191 
let add_var lhs_is_mem lhs x (g, g') = 

192 
if is_instance_var x  ISet.mem x node_vars then 

193 
if ISet.mem x mems 

197  194 
then 
198 
(g, add_edges [x] lhs g') 

195 
let g = add_edges lhs [mk_read_var x] g in 

196 
if lhs_is_mem 

197 
then 

198 
(g, add_edges [x] lhs g') 

199 
else 

200 
(add_edges [x] lhs g, g') 

199  201 
else 
200 
(add_edges [x] lhs g, g') 

201 
else 

202 
let x = if ISet.mem x inputs then mk_read_var x else x in 

203 
(add_edges lhs [x] g, g') 

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

205 
in 

202 
let x = if ISet.mem x inputs then mk_read_var x else x in 

203 
(add_edges lhs [x] g, g') 

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

205 
in 

206  206 
(* Add dependencies from [lhs] to rhs clock [ck]. *) 
207 
let rec add_clock lhs_is_mem lhs ck g = 

207 
let rec add_clock lhs_is_mem lhs ck g =


208  208 
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) 
209 
match (Clocks.repr ck).Clocks.cdesc with 

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

211 
 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g 

212 
 _ > g 

213 
in 

214 
let rec add_dep lhs_is_mem lhs rhs g = 

209 
match (Clocks.repr ck).Clocks.cdesc with


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


211 
 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g


212 
 _ > g


213 
in


214 
let rec add_dep lhs_is_mem lhs rhs g =


215  215 
(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *) 
216  216 
(* i.e every input is connected to every output, through a ghost var *) 
217 
let mashup_appl_dependencies f e g = 

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


219 
List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)


220 
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 

221 
in 

222 
match rhs.expr_desc with 

223 
 Expr_const _ > g 

224 
 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g) 

225 
 Expr_pre e > add_dep true lhs e g 

226 
 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g) 

227 
 Expr_access (e1, d) 

228 
 Expr_power (e1, d) > add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g) 

229 
 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g 

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

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

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

233 
 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) 

234 
 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) 

235 
 Expr_appl (f, e, None) > 

236 
if Basic_library.is_expr_internal_fun rhs


217 
let mashup_appl_dependencies f e g =


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


219 
List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)


220 
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g)


221 
in


222 
match rhs.expr_desc with


223 
 Expr_const _ > g


224 
 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g)


225 
 Expr_pre e > add_dep true lhs e g


226 
 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)


227 
 Expr_access (e1, d)


228 
 Expr_power (e1, d) > add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g)


229 
 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g


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


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


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


233 
 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)


234 
 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)


235 
 Expr_appl (f, e, None) >


236 
if Basic_library.is_expr_internal_fun rhs


237  237 
(* tuple componentwise dependency for internal operators *) 
238 
then


239 
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g 

238 
then


239 
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g


240  240 
(* mashed up dependency for userdefined operators *) 
241 
else


242 
mashup_appl_dependencies f e g 

243 
 Expr_appl (f, e, Some c) > 

244 
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)


245 
in 

246 
let g = 

247 
List.fold_left 

248 
(fun g lhs >


249 
if ISet.mem lhs mems then 

250 
add_vertices [lhs; mk_read_var lhs] g 

251 
else 

252 
add_vertices [lhs] g 

253 
)


254 
g eq.eq_lhs


255 
in 

256 
add_dep false eq.eq_lhs eq.eq_rhs (g, g') 

257 


241 
else


242 
mashup_appl_dependencies f e g


243 
 Expr_appl (f, e, Some c) >


244 
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)


245 
in


246 
let g =


247 
List.fold_left


248 
(fun g lhs >


249 
if ISet.mem lhs mems then


250 
add_vertices [lhs; mk_read_var lhs] g


251 
else


252 
add_vertices [lhs] g


253 
)


254 
g eq.eq_lhs


255 
in


256 
add_dep false eq.eq_lhs eq.eq_rhs (g, g')


257 


258  258  
259 
(* Returns the dependence graph for node [n] *) 

260 
let dependence_graph mems inputs node_vars n = 

261 
instance_var_cpt := 0; 

262 
let g = new_graph (), new_graph () in 

263 
(* Basic dependencies *) 

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

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

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

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

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

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

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

272 
(* function add_eq_dependencies *\) *) 

273 
(* let g = *) 

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

275 
(* List.fold_left (fun g ae > *) 

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

277 
(* add_eq_dependencies mems inputs node_vars fake_eq g *) 

278 
(* ) g n.node_asserts in *) 

279 
g 

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

260 
let dependence_graph mems inputs node_vars n = 

261 
instance_var_cpt := 0; 

262 
let g = new_graph (), new_graph () in 

263 
(* Basic dependencies *) 

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

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

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

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

268 


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

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

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

272 
(* function add_eq_dependencies *\) *) 

273 
(* let g = *) 

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

275 
(* List.fold_left (fun g ae > *) 

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

277 
(* add_eq_dependencies mems inputs node_vars fake_eq g *) 

278 
(* ) g n.node_asserts in *) 

279 
g 

280  
281 
end 

282  
283 
module NodeDep = struct 

280  284  
281 
end 

282  
283 
module NodeDep = struct 

284  
285 
module ExprModule = 

286 
struct 

287 
type t = expr 

288 
let compare = compare 

289 
let hash n = Hashtbl.hash n 

290 
let equal n1 n2 = n1 = n2 

291 
end 

292  
293 
module ESet = Set.Make(ExprModule) 

294  
295 
let rec get_expr_calls prednode expr = 

296 
match expr.expr_desc with 

297 
 Expr_const _ 

298 
 Expr_ident _ > ESet.empty 

299 
 Expr_access (e, _) 

300 
 Expr_power (e, _) > get_expr_calls prednode e 

301 
 Expr_array t 

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

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

304 
 Expr_fby (e1,e2) 

305 
 Expr_arrow (e1,e2) > ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) 

306 
 Expr_ite (c, t, e) > ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) 

307 
 Expr_pre e 

308 
 Expr_when (e,_,_) > get_expr_calls prednode e 

309 
 Expr_appl (id,e, _) > 

310 
if not (Basic_library.is_expr_internal_fun expr) && prednode id 

311 
then ESet.add expr (get_expr_calls prednode e) 

312 
else (get_expr_calls prednode e) 

313  
314 
let get_callee expr = 

315 
match expr.expr_desc with 

316 
 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args) 

317 
 _ > None 

318  
319 
let get_calls prednode eqs = 

320 
let deps = 

321 
List.fold_left 

322 
(fun accu eq > ESet.union accu (get_expr_calls prednode eq.eq_rhs)) 

323 
ESet.empty 

324 
eqs in 

325 
ESet.elements deps 

326  
327 
let dependence_graph prog = 

328 
let g = new_graph () in 

329 
let g = List.fold_right 

330 
(fun td accu > (* for each node we add its dependencies *) 

331 
match td.top_decl_desc with 

285 
module ExprModule = 

286 
struct 

287 
type t = expr 

288 
let compare = compare 

289 
let hash n = Hashtbl.hash n 

290 
let equal n1 n2 = n1 = n2 

291 
end 

292  
293 
module ESet = Set.Make(ExprModule) 

294  
295 
let rec get_expr_calls prednode expr = 

296 
match expr.expr_desc with 

297 
 Expr_const _ 

298 
 Expr_ident _ > ESet.empty 

299 
 Expr_access (e, _) 

300 
 Expr_power (e, _) > get_expr_calls prednode e 

301 
 Expr_array t 

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

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

304 
 Expr_fby (e1,e2) 

305 
 Expr_arrow (e1,e2) > ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) 

306 
 Expr_ite (c, t, e) > ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) 

307 
 Expr_pre e 

308 
 Expr_when (e,_,_) > get_expr_calls prednode e 

309 
 Expr_appl (id,e, _) > 

310 
if not (Basic_library.is_expr_internal_fun expr) && prednode id 

311 
then ESet.add expr (get_expr_calls prednode e) 

312 
else (get_expr_calls prednode e) 

313  
314 
let get_callee expr = 

315 
match expr.expr_desc with 

316 
 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args) 

317 
 _ > None 

318  
319 
let get_calls prednode eqs = 

320 
let deps = 

321 
List.fold_left 

322 
(fun accu eq > ESet.union accu (get_expr_calls prednode eq.eq_rhs)) 

323 
ESet.empty 

324 
eqs in 

325 
ESet.elements deps 

326  
327 
let dependence_graph prog = 

328 
let g = new_graph () in 

329 
let g = List.fold_right 

330 
(fun td accu > (* for each node we add its dependencies *) 

331 
match td.top_decl_desc with 

332  332 
 Node nd > 
333  333 
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) 
334 
let accu = add_vertices [nd.node_id] accu in 

335 
let deps = List.map (fun e > fst (desome (get_callee e))) (get_calls (fun _ > true) (get_node_eqs nd)) in 

334 
let accu = add_vertices [nd.node_id] accu in 

335 
let deps = List.map 

336 
(fun e > fst (desome (get_callee e))) 

337 
(get_calls (fun _ > true) (get_node_eqs nd)) 

338 
in 

339 
(* Adding assert expressions deps *) 

340 
let deps_asserts = 

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

342 
List.map 

343 
(fun e > fst (desome (get_callee e))) 

344 
(ESet.elements 

345 
(List.fold_left 

346 
(fun accu assert_expr > ESet.union accu (get_expr_calls prednode assert_expr)) 

347 
ESet.empty 

348 
(List.map (fun _assert > _assert.assert_expr) nd.node_asserts) 

349 
) 

350 
) 

351 
in 

336  352 
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) 
337 
add_edges [nd.node_id] deps accu


353 
add_edges [nd.node_id] (deps@deps_asserts) accu


338  354 
 _ > assert false (* should not happen *) 
339 


340 
) prog g in 

341 
g 

355 


356 
) prog g in


357 
g


342  358  
343  359 
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *) 
344  360 
let slice_graph gr v = 
...  ...  
348  364 
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; 
349  365 
gr' 
350  366 
end 
351 


367 


352  368 
let rec filter_static_inputs inputs args = 
353 
match inputs, args with 

354 
 [] , [] > [] 

355 
 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 

356 
 _ > assert false 

369 
match inputs, args with


370 
 [] , [] > []


371 
 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


372 
 _ > assert false


357  373  
358  374 
let compute_generic_calls prog = 
359  375 
List.iter 
360  376 
(fun td > 
361  377 
match td.top_decl_desc with 
362  378 
 Node nd > 
363 
let prednode n = is_generic_node (Hashtbl.find node_table n) in 

364 
nd.node_gencalls < get_calls prednode (get_node_eqs nd) 

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


380 
nd.node_gencalls < get_calls prednode (get_node_eqs nd)


365  381 
 _ > () 
366 


382 


367  383 
) prog 
368  384  
369  385 
end 
370  386  
371  387 
module CycleDetection = struct 
372  388  
373 
(*  Look for cycles in a dependency graph *) 

389 
(*  Look for cycles in a dependency graph *)


374  390 
module Cycles = Graph.Components.Make (IdentDepGraph) 
375  391  
376  392 
let mk_copy_var n id = 
377  393 
let used name = 
378 
(List.exists (fun v > v.var_id = name) n.node_locals)


394 
(List.exists (fun v > v.var_id = name) n.node_locals) 

379  395 
 (List.exists (fun v > v.var_id = name) n.node_inputs) 
380  396 
 (List.exists (fun v > v.var_id = name) n.node_outputs) 
381  397 
in mk_new_name used id 
...  ...  
400  416 
 _::_::_ > true 
401  417 
 [] > assert false 
402  418  
403 
(* Checks that the dependency graph [g] does not contain a cycle. Raises 

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

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


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


405  421 
let check_cycles g = 
406  422 
let scc_l = Cycles.scc_list g in 
407  423 
List.iter (fun partition > 
...  ...  
410  426 
else () 
411  427 
) scc_l 
412  428  
413 
(* Creates the subgraph of [g] restricted to vertices and edges in partition *) 

429 
(* Creates the subgraph of [g] restricted to vertices and edges in partition *)


414  430 
let copy_partition g partition = 
415  431 
let copy_g = IdentDepGraph.create () in 
416  432 
IdentDepGraph.iter_edges 
...  ...  
419  435 
then IdentDepGraph.add_edge copy_g src tgt) 
420  436 
g 
421  437  
422 


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

424 
[head] is a head of a nontrivial scc of [g]. 

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

438 


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


440 
[head] is a head of a nontrivial scc of [g].


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


426  442 
let break_cycle head cp_head g = 
427  443 
let succs = IdentDepGraph.succ g head in 
428  444 
IdentDepGraph.add_edge g head cp_head; 
...  ...  
433  449 
IdentDepGraph.add_edge g s cp_head) 
434  450 
succs 
435  451  
436 
(* Breaks cycles of the dependency graph [g] of memory variables [mems] 

437 
belonging in node [node]. Returns: 

438 
 a list of new auxiliary variable declarations 

439 
 a list of new equations 

440 
 a modified acyclic version of [g] 

441 
*) 

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


453 
belonging in node [node]. Returns:


454 
 a list of new auxiliary variable declarations


455 
 a list of new equations


456 
 a modified acyclic version of [g]


457 
*)


442  458 
let break_cycles node mems g = 
443  459 
let (mem_eqs, non_mem_eqs) = List.partition (fun eq > List.exists (fun v > ISet.mem v mems) eq.eq_lhs) (get_node_eqs node) in 
444  460 
let rec break vdecls mem_eqs g = 
...  ...  
447  463 
match wrong with 
448  464 
 [] > (vdecls, non_mem_eqs@mem_eqs, g) 
449  465 
 [head]::_ > 
450 
begin 

451 
IdentDepGraph.remove_edge g head head; 

452 
break vdecls mem_eqs g 

453 
end 

466 
begin


467 
IdentDepGraph.remove_edge g head head;


468 
break vdecls mem_eqs g


469 
end


454  470 
 (head::part)::_ > 
455 
begin 

456 
let vdecl_cp_head, cp_eq = mk_copy_eq node head in 

457 
let pvar v = List.mem v part in 

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

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

460 
break_cycle head vdecl_cp_head.var_id g; 

461 
break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g 

462 
end 

471 
begin


472 
let vdecl_cp_head, cp_eq = mk_copy_eq node head in


473 
let pvar v = List.mem v part in


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


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


476 
break_cycle head vdecl_cp_head.var_id g;


477 
break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g


478 
end


463  479 
 _ > assert false 
464  480 
in break [] mem_eqs g 
465  481  
...  ...  
504  520 
end 
505  521  
506  522 
(* merge variables [v] and [v'] in disjunction [map]. Then: 
507 
 the mapping v' becomes v' > (map v) inter (map v')


508 
 the mapping v > ... then disappears


509 
 other mappings become x > (map x) \ (if v in x then v else v')


523 
 the mapping v' becomes v' > (map v) inter (map v') 

524 
 the mapping v > ... then disappears 

525 
 other mappings become x > (map x) \ (if v in x then v else v') 

510  526 
*) 
511  527 
let merge_in_disjoint_map map v v' = 
512  528 
begin 
...  ...  
516  532 
end 
517  533  
518  534 
(* replace variable [v] by [v'] in disjunction [map]. 
519 
[v'] is a dead variable. Then: 

520 
 the mapping v' becomes v' > (map v)


521 
 the mapping v > ... then disappears


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


535 
[v'] is a dead variable. Then:


536 
 the mapping v' becomes v' > (map v) 

537 
 the mapping v > ... then disappears 

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

523  539 
*) 
524  540 
let replace_in_disjoint_map map v v' = 
525  541 
begin 
...  ...  
529  545 
end 
530  546  
531  547 
(* remove variable [v] in disjunction [map]. Then: 
532 
 the mapping v > ... then disappears


533 
 all mappings become x > (map x) \ { v}


548 
 the mapping v > ... then disappears 

549 
 all mappings become x > (map x) \ { v} 

534  550 
*) 
535  551 
let remove_in_disjoint_map map v = 
536  552 
begin 
...  ...  
588  604 
let node_vars = ExprDep.node_variables node in 
589  605 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in 
590  606 
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; 
591 
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) 

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


592  608 
CycleDetection.check_cycles g_non_mems; 
593  609 
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in 
594  610 
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) 
Also available in: Unified diff
Addressing node calls in asserts