diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 93 |
2 files changed, 86 insertions, 8 deletions
@@ -1,6 +1,7 @@ # Temporary files of text editors *.swp *~ +tags # Tests : KCG & C build products tests/kcg diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 1eac551..fd31670 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -788,6 +788,12 @@ end = struct in v_ecl + let rec extract_const_vars_root (ecl, _, _) = + List.fold_left + (fun l (_, x, v) -> match v with + | EItem _ -> x::l + | _ -> l) + [] ecl (* scope_constrict : id list -> (id * id) list -> id list @@ -818,8 +824,7 @@ end = struct 0 cp_i in - let best = Array.make n 0 in - for i = 0 to n-1 do best.(i) <- i done; + let best = Array.init n (fun i -> i) in let usefull = ref true in Format.printf "SCA"; @@ -855,6 +860,58 @@ end = struct Array.to_list (Array.map (Array.get var_i) best) (* + force_ordering : id list -> (float * id list) list -> id list + + Determine a good ordering for enumerate variables based on the FORCE algorithm + *) + let force_ordering vars groups = + let var_i = Array.of_list vars in + let n = Array.length var_i in + + let i_var = Hashtbl.create n in + Array.iteri (fun i v -> Hashtbl.add i_var v i) var_i; + Hashtbl.add i_var "#BEGIN" (-1); + + let ngroups = List.map + (fun (w, l) -> w, List.map (Hashtbl.find i_var) l) + groups in + + let ord = Array.init n (fun i -> i) in + + for iter = 0 to 500 do + let rev = Array.make n (-1) in + for i = 0 to n-1 do rev.(ord.(i)) <- i done; + + let bw = Array.make n 0. in + let w = Array.make n 0. in + + let gfun (gw, l) = + let sp = List.fold_left (+.) 0. + (List.map + (fun i -> if i = -1 then -.gw else float_of_int (rev.(i))) l) + in + let b = sp /. float_of_int (List.length l) in + List.iter (fun i -> if i >= 0 then begin + bw.(i) <- bw.(i) +. (gw *. b); + w.(i) <- w.(i) +. gw end) + l + in + List.iter gfun ngroups; + + let b = Array.init n + (fun i -> + if w.(i) = 0. then + float_of_int i + else bw.(i) /. w.(i)) in + + let ol = List.sort + (fun i j -> Pervasives.compare b.(i) b.(j)) + (Array.to_list ord) in + Array.blit (Array.of_list ol) 0 ord 0 n + done; + List.map (Array.get var_i) (Array.to_list ord) + + (* init_env : cmdline_opt -> rooted_prog -> env *) let init_env opt rp = @@ -893,13 +950,31 @@ end = struct let lv = extract_linked_evars_root init_cl @ extract_linked_evars_root cl_g in - let lv = uniq_sorted (List.sort Pervasives.compare (List.map ord_couple lv)) in - let evars_ord = time "SCA" (fun () -> scope_constrict evars lv) in - let va, vb = List.partition (fun n -> is_suffix n "init") evars_ord in - let vb, vc = List.partition (fun n -> is_suffix n "state") vb in - let evars_ord = (List.rev va) @ vb @ vc in + + let lv_f = List.map (fun (a, b) -> (1.0, [a; b])) lv in + let lv_f = lv_f @ (List.map (fun v -> (10.0, ["#BEGIN"; v])) + (extract_const_vars_root cl)) in + let lv_f = lv_f @ (List.map (fun v -> (5.0, ["#BEGIN"; v])) + (List.filter (fun n -> is_suffix n "init") evars)) in + let lv_f = lv_f @ (List.map (fun v -> (3.0, ["#BEGIN"; v])) + (List.filter (fun n -> is_suffix n "state") evars)) in + let evars_ord = + if true then + time "FORCE" (fun () -> force_ordering evars lv_f) + else + time "SCA" (fun () -> scope_constrict evars lv) + in + + let evars_ord = + if false then + let va, vb = List.partition (fun n -> is_suffix n "init") evars_ord in + let vb, vc = List.partition (fun n -> is_suffix n "state") vb in + (List.rev va) @ vb @ vc + else + evars_ord + in let ev_order = Hashtbl.create (List.length evars) in List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord; @@ -1015,10 +1090,12 @@ end = struct (* Dump final state *) let acc = ch_it 0 init_acc in edd_dump_graphviz acc "/tmp/graph-final0.dot"; + Format.printf "Finishing up...@."; let final = edd_apply_cl acc e.cl in edd_dump_graphviz final "/tmp/graph-final.dot"; - (*Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;*) + if e.opt.verbose_ci then + Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final; (* Check guarantees *) let check_guarantee (id, f) = |