Revision 15c3e4e7
Added by LĂ©lio Brun 11 months ago
src/checks/liveness.ml  

141  141 
end 
142  142  
143  143 
let pp_reuse_policy fmt policy = 
144 
begin 

145 
Format.fprintf fmt "{ /* reuse policy */@."; 

146 
Hashtbl.iter (fun s t > Format.fprintf fmt "%s > %s@." s t.var_id) policy; 

147 
Format.fprintf fmt "}@." 

148 
end 

144 
Format.(fprintf fmt "@[<v 2>{ /* reuse policy */%t@] }" 

145 
(fun fmt > Hashtbl.iter (fun s t > fprintf fmt "@,%s > %s" s t.var_id) policy)) 

149  146  
150  147 
let pp_context fmt ctx = 
151 
begin 

152 
Format.fprintf fmt "{ /*BEGIN context */@."; 

153 
Format.fprintf fmt "eval=%a;@." Disjunction.pp_ciset ctx.evaluated; 

154 
Format.fprintf fmt "graph=%a;@." pp_dep_graph ctx.dep_graph; 

155 
Format.fprintf fmt "disjoint=%a;@." Disjunction.pp_disjoint_map ctx.disjoint; 

156 
Format.fprintf fmt "policy=%a;@." pp_reuse_policy ctx.policy; 

157 
Format.fprintf fmt "/* END context */ }@."; 

158 
end 

148 
Format.fprintf fmt 

149 
"@[<v 2>{ /*BEGIN context */@,\ 

150 
eval = %a;@,\ 

151 
graph = %a;@,\ 

152 
disjoint = %a;@,\ 

153 
policy = %a;@,\ 

154 
/* END context */ }@]" 

155 
Disjunction.pp_ciset ctx.evaluated 

156 
pp_dep_graph ctx.dep_graph 

157 
Disjunction.pp_disjoint_map ctx.disjoint 

158 
pp_reuse_policy ctx.policy 

159  159  
160  160 
(* computes the reusable dependencies of variable [var] in graph [g], 
161  161 
once [var] has been evaluated 
...  ...  
197  197 
let locally_reusable v = 
198  198 
IdentDepGraph.fold_pred (fun p r > r && Disjunction.CISet.exists (fun d > p = d.var_id) disjoint) ctx.dep_graph v.var_id true in 
199  199 
let eligibles = Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated in 
200 
Log.report ~level:7 (fun fmt > Format.fprintf fmt "eligibles:%a@." Disjunction.pp_ciset eligibles); 

201  200 
let quasi_dead, live = Disjunction.CISet.partition locally_reusable eligibles in 
202 
Log.report ~level:7 (fun fmt > Format.fprintf fmt "live:%a@." Disjunction.pp_ciset live);


203 
try


204 
let disjoint_live = Disjunction.CISet.inter disjoint live in


205 
Log.report ~level:7 (fun fmt > Format.fprintf fmt "disjoint live:%a@." Disjunction.pp_ciset disjoint_live);


206 
let reuse = Disjunction.CISet.max_elt disjoint_live in


207 
begin


208 
IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;


209 
Hashtbl.add ctx.policy var.var_id reuse;


210 
ctx.evaluated < Disjunction.CISet.add var ctx.evaluated;


211 
(*Format.eprintf "%s reused by live@." var.var_id;*)


212 
end


213 
with Not_found >


214 
try


215 
let dead = Disjunction.CISet.filter (fun v > is_graph_root v.var_id ctx.dep_graph) quasi_dead in


216 
Log.report ~level:7 (fun fmt > Format.fprintf fmt "dead:%a@." Disjunction.pp_ciset dead);


217 
let reuse = Disjunction.CISet.choose dead in


218 
begin


201 
let disjoint_live = Disjunction.CISet.inter disjoint live in


202 
let dead = Disjunction.CISet.filter (fun v > is_graph_root v.var_id ctx.dep_graph) quasi_dead in


203 
Log.report ~level:7 (fun fmt >


204 
Format.fprintf fmt


205 
"@[<v>\


206 
eligibles : %a@,\


207 
live : %a@,\


208 
disjoint live: %a@,\


209 
dead : %a@,@]"


210 
Disjunction.pp_ciset eligibles


211 
Disjunction.pp_ciset live


212 
Disjunction.pp_ciset disjoint_live


213 
Disjunction.pp_ciset dead);


214 
begin try


215 
let reuse = match Disjunction.CISet.max_elt_opt disjoint_live with


216 
 Some reuse > reuse


217 
 None > Disjunction.CISet.choose dead in


219  218 
IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id; 
220 
Hashtbl.add ctx.policy var.var_id reuse; 

221 
ctx.evaluated < Disjunction.CISet.add var ctx.evaluated; 

222 
(*Format.eprintf "%s reused by dead %s@." var.var_id reuse.var_id;*) 

223 
end 

224 
with Not_found > 

225 
begin 

226 
Hashtbl.add ctx.policy var.var_id var; 

227 
ctx.evaluated < Disjunction.CISet.add var ctx.evaluated; 

228 
end 

219 
Hashtbl.add ctx.policy var.var_id reuse 

220 
with Not_found > Hashtbl.add ctx.policy var.var_id var 

221 
end; 

222 
ctx.evaluated < Disjunction.CISet.add var ctx.evaluated 

229  223  
230  224 
let compute_reuse_policy node schedule disjoint g = 
231 
let sort = ref schedule in 

232  225 
let ctx = { evaluated = Disjunction.CISet.empty; 
233 
dep_graph = g; 

234 
disjoint = disjoint; 

235 
policy = Hashtbl.create 23; } in 

236 
while !sort <> [] 

237 
do 

238 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "new context:%a@." pp_context ctx); 

239 
let heads = List.map (fun v > get_node_var v node) (List.hd !sort) in 

240 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "NEW HEADS:"); 

241 
List.iter (fun head > Log.report ~level:6 (fun fmt > Format.fprintf fmt "%s (%a)" head.var_id Printers.pp_node_eq (get_node_eq head.var_id node))) heads; 

242 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "@."); 

243 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "COMPUTE_DEPENDENCIES@."); 

244 
compute_dependencies heads ctx; 

245 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "new context:%a@." pp_context ctx); 

246 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "COMPUTE_REUSE@."); 

247 
List.iter (compute_reuse node ctx heads) heads; 

248 
(*compute_evaluated heads ctx;*) 

249 
List.iter (fun head > Log.report ~level:6 (fun fmt > Format.fprintf fmt "reuse %s instead of %s@." (Hashtbl.find ctx.policy head.var_id).var_id head.var_id)) heads; 

250 
sort := List.tl !sort; 

251 
done; 

226 
dep_graph = g; 

227 
disjoint = disjoint; 

228 
policy = Hashtbl.create 23; } in 

229 
List.iter (fun heads > 

230 
let heads = List.map (fun v > get_node_var v node) heads in 

231 
Log.report ~level:6 (fun fmt > 

232 
Format.(fprintf fmt 

233 
"@[<v>@[<v 2>new context:@,%a@]@,NEW HEADS:%a@,COMPUTE_DEPENDENCIES@,@]" 

234 
pp_context ctx 

235 
(pp_print_list 

236 
~pp_open_box:pp_open_hbox 

237 
~pp_sep:pp_print_space 

238 
(fun fmt head > 

239 
fprintf fmt "%s (%a)" 

240 
head.var_id Printers.pp_node_eq 

241 
(get_node_eq head.var_id node))) 

242 
heads)); 

243 
compute_dependencies heads ctx; 

244 
Log.report ~level:6 (fun fmt > 

245 
Format.fprintf fmt "@[<v>@[<v 2>new context:@,%a@]@,COMPUTE_REUSE@,@]" pp_context ctx); 

246 
List.iter (compute_reuse node ctx heads) heads; 

247 
(*compute_evaluated heads ctx;*) 

248 
Log.report ~level:6 (fun fmt > 

249 
Format.(fprintf fmt "@[<v>%a@,@]" 

250 
(pp_print_list 

251 
~pp_open_box:pp_open_vbox0 

252 
(fun fmt head > fprintf fmt "reuse %s instead of %s" 

253 
(Hashtbl.find ctx.policy head.var_id).var_id head.var_id)) 

254 
heads))) 

255 
schedule; 

252  256 
IdentDepGraph.clear ctx.dep_graph; 
253  257 
ctx.policy 
254  258 
Also available in: Unified diff
generic ACSL spec generation