diff options
| -rw-r--r-- | Changelog | 2 | ||||
| -rw-r--r-- | backend/Regalloc.ml | 8 | ||||
| -rw-r--r-- | backend/Splitting.ml | 33 | ||||
| -rw-r--r-- | backend/XTL.ml | 4 | ||||
| -rw-r--r-- | lib/Camlcoq.ml | 22 | ||||
| -rw-r--r-- | lib/Maps.v | 39 |
6 files changed, 86 insertions, 22 deletions
@@ -14,6 +14,8 @@ Development trunk: of small integer or FP types. - PowerPC: more efficient implementation of division on 64-bit integers. - Minor simplifications in the generic solvers for dataflow analysis. +- Small improvements in compilation times for the register allocation pass. + Release 2.0, 2013-06-21 ======================= diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index b73cbf5..3c56b43 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -424,8 +424,8 @@ let spill_costs f = let charge_block blk = List.iter charge_instr blk in - PTree.fold - (fun () pc blk -> charge_block blk) + PTree.fold1 + (fun () blk -> charge_block blk) f.fn_code (); if !option_dalloctrace then begin fprintf !pp "------------------ Unspillable variables --------------@ @."; @@ -615,8 +615,8 @@ let rec tospill_block alloc blk ts = | instr :: blk' -> tospill_block alloc blk' (tospill_instr alloc instr ts) let tospill_function f alloc = - PTree.fold - (fun ts pc blk -> tospill_block alloc blk ts) + PTree.fold1 + (fun ts blk -> tospill_block alloc blk ts) f.fn_code VSet.empty diff --git a/backend/Splitting.ml b/backend/Splitting.ml index 85de636..b238cef 100644 --- a/backend/Splitting.ml +++ b/backend/Splitting.ml @@ -65,22 +65,24 @@ let reg_for lr = a live range to the reg if it is live, and no live range if it is dead. *) +module RMap = Map.Make(P) + module LRMap = struct - type t = live_range PTree.t (* live register -> live range *) + type t = live_range RMap.t (* live register -> live range *) - let beq m1 m2 = PTree.beq same_range m1 m2 + let beq m1 m2 = RMap.equal same_range m1 m2 - let bot : t = PTree.empty + let bot : t = RMap.empty - let lub_opt_range olr1 olr2 = + let lub_opt_range r olr1 olr2 = match olr1, olr2 with | Some lr1, Some lr2 -> unify lr1 lr2; olr1 | Some _, None -> olr1 | None, _ -> olr2 let lub m1 m2 = - PTree.combine lub_opt_range m1 m2 + RMap.merge lub_opt_range m1 m2 end @@ -89,11 +91,11 @@ module Solver = Backward_Dataflow_Solver(LRMap)(NodeSetBackward) (* A cache of live ranges associated to (pc, used reg) pairs. *) let live_range_cache = - (Hashtbl.create 123 : (int32 * int32, live_range) Hashtbl.t) + (Hashtbl.create 123 : (int * int, live_range) Hashtbl.t) let live_range_for pc r = - let pc' = P.to_int32 pc - and r' = P.to_int32 r in + let pc' = P.to_int pc + and r' = P.to_int r in try Hashtbl.find live_range_cache (pc',r') with Not_found -> @@ -104,14 +106,14 @@ let live_range_for pc r = (* The transfer function *) let reg_live pc r map = - match PTree.get r map with - | Some lr -> map (* already live *) - | None -> PTree.set r (live_range_for pc r) map (* becomes live *) + if RMap.mem r map + then map (* already live *) + else RMap.add r (live_range_for pc r) map (* becomes live *) let reg_list_live pc rl map = List.fold_right (reg_live pc) rl map let reg_dead r map = - PTree.remove r map + RMap.remove r map let transfer f pc after = match PTree.get pc f.fn_code with @@ -131,9 +133,10 @@ let analysis f = Solver.fixpoint f.fn_code successors_instr (transfer f) [] (* Produce renamed registers for each instruction. *) let ren_reg map r = - match PTree.get r map with - | Some lr -> reg_for lr - | None -> XTL.new_reg() + try + reg_for (RMap.find r map) + with Not_found -> + XTL.new_reg() let ren_regs map rl = List.map (ren_reg map) rl diff --git a/backend/XTL.ml b/backend/XTL.ml index 53c478d..46c59b0 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -176,9 +176,9 @@ let type_function f = let basic_blocks_map f = (* return mapping pc -> number of predecessors *) let add_successor map s = PMap.set s (1 + PMap.get s map) map in - let add_successors_block map pc blk = + let add_successors_block map blk = List.fold_left add_successor map (successors_block blk) in - PTree.fold add_successors_block f.fn_code + PTree.fold1 add_successors_block f.fn_code (PMap.set f.fn_entrypoint 2 (PMap.init 0)) let transform_basic_blocks diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index e057771..2415e1d 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -267,7 +267,7 @@ let camlfloat_of_coqfloat f = (* Timing facility *) (* -let timers = (Hashtbl.create 9 : (string, float) Hashtbl.t) +let timers = Hashtbl.create 9 let add_to_timer name time = let old = try Hashtbl.find timers name with Not_found -> 0.0 in @@ -283,6 +283,26 @@ let time name fn arg = add_to_timer name (Unix.gettimeofday() -. start); raise x +let time2 name fn arg1 arg2 = + let start = Unix.gettimeofday() in + try + let res = fn arg1 arg2 in + add_to_timer name (Unix.gettimeofday() -. start); + res + with x -> + add_to_timer name (Unix.gettimeofday() -. start); + raise x + +let time3 name fn arg1 arg2 arg3 = + let start = Unix.gettimeofday() in + try + let res = fn arg1 arg2 arg3 in + add_to_timer name (Unix.gettimeofday() -. start); + res + with x -> + add_to_timer name (Unix.gettimeofday() -. start); + raise x + let print_timers () = Hashtbl.iter (fun name time -> Printf.printf "%-20s %.3f\n" name time) @@ -141,6 +141,13 @@ Module Type TREE. forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A), fold f m v = List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. + (** Same as [fold], but the function does not receive the [elt] argument. *) + Variable fold1: + forall (A B: Type), (B -> A -> B) -> t A -> B -> B. + Hypothesis fold1_spec: + forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A), + fold1 f m v = + List.fold_left (fun a p => f a (snd p)) (elements m) v. End TREE. (** * The abstract signatures of maps *) @@ -932,6 +939,38 @@ Module PTree <: TREE. intros. unfold fold, elements. rewrite <- xfold_xelements. auto. Qed. + Fixpoint fold1 (A B: Type) (f: B -> A -> B) (m: t A) (v: B) {struct m} : B := + match m with + | Leaf => v + | Node l None r => + let v1 := fold1 f l v in + fold1 f r v1 + | Node l (Some x) r => + let v1 := fold1 f l v in + let v2 := f v1 x in + fold1 f r v2 + end. + + Lemma fold1_xelements: + forall (A B: Type) (f: B -> A -> B) m i v l, + List.fold_left (fun a p => f a (snd p)) l (fold1 f m v) = + List.fold_left (fun a p => f a (snd p)) (xelements m i l) v. + Proof. + induction m; intros. + simpl. auto. + destruct o; simpl. + rewrite <- IHm1. simpl. rewrite <- IHm2. auto. + rewrite <- IHm1. rewrite <- IHm2. auto. + Qed. + + Theorem fold1_spec: + forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A), + fold1 f m v = + List.fold_left (fun a p => f a (snd p)) (elements m) v. + Proof. + intros. apply fold1_xelements with (l := @nil (positive * A)). + Qed. + End PTree. (** * An implementation of maps over type [positive] *) |