Project

General

Profile

« Previous | Next » 

Revision 15c3e4e7

Added by LĂ©lio Brun 11 months ago

generic ACSL spec generation

View differences:

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