diff options
author | blazy <blazy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-08 07:53:02 +0000 |
---|---|---|
committer | blazy <blazy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-08 07:53:02 +0000 |
commit | a8c744000247af207b489d3cdd4e3d3cf60f72e1 (patch) | |
tree | 96c7ee4e244fccdb840233007604ba52d97c09e0 /backend/IRC.v | |
parent | 283afabc594b385e4f17fa59647aa8cddee27f85 (diff) | |
download | compcert-a8c744000247af207b489d3cdd4e3d3cf60f72e1.tar.gz compcert-a8c744000247af207b489d3cdd4e3d3cf60f72e1.zip |
ajout branche allocation de registres
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/IRC.v')
-rwxr-xr-x | backend/IRC.v | 122 |
1 files changed, 122 insertions, 0 deletions
diff --git a/backend/IRC.v b/backend/IRC.v new file mode 100755 index 00000000..7842a4bd --- /dev/null +++ b/backend/IRC.v @@ -0,0 +1,122 @@ +Require Import Recdef. +Require Import FSetInterface. +Require Import InterfGraphMapImp. +Require Import OrderedOption. +Require Import FMapAVL. +Require Import IRC_termination. +Require Import IRC_graph. +Require Import IRC_Graph_Functions. +Require Import Edges. + +Import Edge RegFacts Props OTFacts. + +(* Definition of Register options *) + +Module OptionReg := OrderedOpt Register. + +(* Definition of the type of colorings *) + +Definition Coloring := Register.t -> OptionReg.t. + +(* Map used to build a coloring of the graph. + A coloring is a the function find applied to the map *) + +Module ColorMap := FMapAVL.Make Register. + +(* Function to complete a coloring by giving the + same color to coalesced vertices *) + +Definition complete_coloring e col : ColorMap.t Register.t := +let x := snd_ext e in let y := fst_ext e in +match ColorMap.find y col with +| None => col +| Some c => ColorMap.add x c col +end. + +(* Function to compute forbidden colors when completing the coloring + for simplified or spilled registers (optimistic spilling) *) + +Section add_monad. + +Definition vertex_add_monad (o : option Register.t) (VS : VertexSet.t) := +match o with +|Some v => VertexSet.add v VS +|None => VS +end. + +Variable A : Type. + +Lemma monad_fold : forall f a l s, +VertexSet.Equal (fold_left + (fun (x : VertexSet.t) (e : A) => vertex_add_monad (f e) x) + (a :: l) s) + (vertex_add_monad (f a) + (fold_left (fun (x : VertexSet.t) (e : A) => vertex_add_monad (f e) x) l s)). + +Proof. +intros f a l s;apply fold_left_assoc. +intros y z e;unfold vertex_add_monad. +destruct (f y);destruct (f z);[apply add_add|intuition|intuition|intuition]. +intros e1 e2 y H. unfold vertex_add_monad. +destruct (f y);intuition. +apply Dec.F.add_m; intuition. +Qed. + +End add_monad. + +Definition forbidden_colors x col g := +VertexSet.fold (fun v => vertex_add_monad (ColorMap.find v col)) + (interference_adj x g) + VertexSet.empty. + +(* Function to complete the coloring for simplified or spilled vertices. + Calls forbidden_colors. Is choosing yet any available color *) + +Definition available_coloring ircg x (col : ColorMap.t Register.t) := +let g := (irc_g ircg) in let palette := (pal ircg) in +match (VertexSet.choose (VertexSet.diff palette (forbidden_colors x col g))) with +| None => col +| Some c => ColorMap.add x c col +end. + +(* Definition of the empty coloring as the coloring where the only + colored vertices are the precolored ones *) + +Definition precoloring_map g := +VertexSet.fold (fun x => ColorMap.add x x) (precolored g) (ColorMap.empty Register.t). + +Function IRC_map (g : irc_graph) +{measure irc_measure g} : ColorMap.t Register.t := +match simplify g with +|Some rg' => let (r,g') := rg' in available_coloring g r (IRC_map g') +|None => match coalesce g with + |Some eg' => let (e,g') := eg' in complete_coloring e (IRC_map g') + |None => match freeze g with + |Some rg' => let (r,g') := rg' in IRC_map g' + |None => match spill g with + |Some rg' => let (r,g') := rg' in available_coloring g r (IRC_map g') + |None => precoloring_map (irc_g g) + end + end + end +end. + +Proof. +intros. apply (simplify_dec g r g' teq). +intros. apply (coalesce_dec g e g' teq0). +intros. apply (freeze_dec g r g' teq1). +intros. apply (spill_dec g r g' teq2). +Qed. + +(* Definition of the transformation from a map to a coloring, + simply by using find *) + +Definition map_to_coloring (colmap : ColorMap.t Register.t) := +fun x => ColorMap.find x colmap. + +(* Final definition of iterated register coalescing *) + +Definition IRC g palette := +let g' := graph_to_IRC_graph g palette in map_to_coloring (IRC_map g'). + +Definition precoloring g := map_to_coloring (precoloring_map g). |