Revision d4807c3d
Added by Xavier Thirioux almost 8 years ago
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 
(* nomem/nomem and mem/nomem 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 userdefined 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 componentwise 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
 corrected causality bug (cf. previous commit)
gitsvnid: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@227 041b043f8d7c46b2b46eef0dd855326e