summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backend/Coloring.v309
-rw-r--r--backend/Coloringaux.ml867
-rw-r--r--backend/Coloringaux.mli22
-rw-r--r--backend/Coloringproof.v957
-rw-r--r--backend/InterfGraph.v302
-rw-r--r--backend/Parallelmove.v365
6 files changed, 0 insertions, 2822 deletions
diff --git a/backend/Coloring.v b/backend/Coloring.v
deleted file mode 100644
index a23bf55..0000000
--- a/backend/Coloring.v
+++ /dev/null
@@ -1,309 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-(** Construction and coloring of the interference graph. *)
-
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import RTLtyping.
-Require Import Locations.
-Require Import Conventions.
-Require Import InterfGraph.
-
-(** * Construction of the interference graph *)
-
-(** Two registers interfere if there exists a program point where
- they are both simultaneously live, and it is possible that they
- contain different values at this program point. Consequently,
- two registers that do not interfere can be merged into one register
- while preserving the program behavior: there is no program point
- where this merged register would have to hold two different values
- (for the two original registers), so to speak.
-
- The simplified algorithm for constructing the interference graph
- from the results of the liveness analysis is as follows:
-<<
- start with empty interference graph
- for each parameter p and register r live at the function entry point:
- add conflict edge p <-> r
- for each instruction I in function:
- let L be the live registers "after" I
- if I is a "move" instruction dst <- src, and dst is live:
- add conflict edges dst <-> r for each r in L \ {dst, src}
- else if I is an instruction with result dst, and dst is live:
- add conflict edges dst <-> r for each r in L \ {dst};
- if I is a "call" instruction dst <- f(args),
- add conflict edges between all pseudo-registers in L \ {dst}
- and all caller-save machine registers
- done
->>
- Notice that edges are added only when a register becomes live.
- A register becomes live either if it is the result of an operation
- (and is live afterwards), or if we are at the function entrance
- and the register is a function parameter. For two registers to
- be simultaneously live at some program point, it must be the case
- that one becomes live at a point where the other is already live.
- Hence, it suffices to add interference edges between registers
- that become live at some instruction and registers that are already
- live at this instruction.
-
- Notice also the special treatment of ``move'' instructions:
- since the destination register of the ``move'' is assigned the same value
- as the source register, it is semantically correct to assign
- the destination and the source registers to the same register,
- even if the source register remains live afterwards.
- (This is even desirable, since the ``move'' instruction can then
- be eliminated.) Thus, no interference is added between the
- source and the destination of a ``move'' instruction.
-
- Finally, for ``call'' instructions, we must make sure that
- pseudo-registers live across the instruction are allocated to
- callee-save machine register or to stack slots, but never to
- caller-save machine registers (these lose their values across
- the call). We therefore add the corresponding conflict edges
- between pseudo-registers live across and caller-save machine
- registers (pairwise).
-
- The full algorithm is similar to the simplified algorithm above,
- but records preference edges in addition to conflict edges.
- Preference edges guide the graph coloring algorithm by telling it
- that better code will be obtained eventually if it is possible
- to allocate certain pseudo-registers to the same location or to
- a given machine register. Preference edges are added:
-- between the destination and source pseudo-registers of a ``move''
- instruction;
-- between the arguments of a ``call'' instruction and the locations
- of the arguments as dictated by the calling conventions;
-- between the result of a ``call'' instruction and the location
- of the result as dictated by the calling conventions.
-*)
-
-Definition add_interf_live
- (filter: reg -> bool) (res: reg) (live: Regset.t) (g: graph): graph :=
- Regset.fold
- (fun r g => if filter r then add_interf r res g else g) live g.
-
-Definition add_interf_op
- (res: reg) (live: Regset.t) (g: graph): graph :=
- add_interf_live
- (fun r => if Reg.eq r res then false else true)
- res live g.
-
-Definition add_interf_move
- (arg res: reg) (live: Regset.t) (g: graph): graph :=
- add_interf_live
- (fun r =>
- if Reg.eq r res then false else
- if Reg.eq r arg then false else true)
- res live g.
-
-Definition add_interf_destroyed
- (live: Regset.t) (destroyed: list mreg) (g: graph): graph :=
- List.fold_left
- (fun g mr => Regset.fold (fun r g => add_interf_mreg r mr g) live g)
- destroyed g.
-
-Definition add_interfs_indirect_call
- (rfun: reg) (locs: list loc) (g: graph): graph :=
- List.fold_left
- (fun g loc =>
- match loc with R mr => add_interf_mreg rfun mr g | _ => g end)
- locs g.
-
-Definition add_interf_call
- (ros: reg + ident) (locs: list loc) (g: graph): graph :=
- match ros with
- | inl rfun => add_interfs_indirect_call rfun locs g
- | inr idfun => g
- end.
-
-Fixpoint add_prefs_call
- (args: list reg) (locs: list loc) (g: graph) {struct args} : graph :=
- match args, locs with
- | a1 :: al, l1 :: ll =>
- add_prefs_call al ll
- (match l1 with R mr => add_pref_mreg a1 mr g | _ => g end)
- | _, _ => g
- end.
-
-Definition add_prefs_builtin (ef: external_function)
- (args: list reg) (res: reg) (g: graph) : graph :=
- match ef, args with
- | EF_annot_val txt targ, arg1 :: _ => add_pref arg1 res g
- | _, _ => g
- end.
-
-Definition add_interf_entry
- (params: list reg) (live: Regset.t) (g: graph): graph :=
- List.fold_left (fun g r => add_interf_op r live g) params g.
-
-Fixpoint add_interf_params
- (params: list reg) (g: graph) {struct params}: graph :=
- match params with
- | nil => g
- | p1 :: pl =>
- add_interf_params pl
- (List.fold_left
- (fun g r => if Reg.eq r p1 then g else add_interf r p1 g)
- pl g)
- end.
-
-Definition add_edges_instr
- (sig: signature) (i: instruction) (live: Regset.t) (g: graph) : graph :=
- match i with
- | Iop op args res s =>
- if Regset.mem res live then
- match is_move_operation op args with
- | Some arg =>
- add_pref arg res (add_interf_move arg res live g)
- | None =>
- add_interf_op res live g
- end
- else g
- | Iload chunk addr args dst s =>
- if Regset.mem dst live
- then add_interf_op dst live g
- else g
- | Icall sig ros args res s =>
- let largs := loc_arguments sig in
- let lres := loc_result sig in
- add_prefs_call args largs
- (add_pref_mreg res lres
- (add_interf_op res live
- (add_interf_call ros largs
- (add_interf_destroyed
- (Regset.remove res live) destroyed_at_call_regs g))))
- | Itailcall sig ros args =>
- let largs := loc_arguments sig in
- add_prefs_call args largs
- (add_interf_call ros largs g)
- | Ibuiltin ef args res s =>
- add_prefs_builtin ef args res (add_interf_op res live g)
- | Ireturn (Some r) =>
- add_pref_mreg r (loc_result sig) g
- | _ => g
- end.
-
-Definition add_edges_instrs (f: function) (live: PMap.t Regset.t) : graph :=
- PTree.fold
- (fun g pc i => add_edges_instr f.(fn_sig) i live!!pc g)
- f.(fn_code)
- empty_graph.
-
-Definition interf_graph (f: function) (live: PMap.t Regset.t) (live0: Regset.t) :=
- add_prefs_call f.(fn_params) (loc_parameters f.(fn_sig))
- (add_interf_params f.(fn_params)
- (add_interf_entry f.(fn_params) live0
- (add_edges_instrs f live))).
-
-(** * Graph coloring *)
-
-(** The actual coloring of the graph is performed by a function written
- directly in Caml, and not proved correct in any way. This function
- takes as argument the [RTL] function, the interference graph for
- this function, an assignment of types to [RTL] pseudo-registers,
- and the set of all [RTL] pseudo-registers mentioned in the
- interference graph. It returns the coloring as a function from
- pseudo-registers to locations. *)
-
-Parameter graph_coloring:
- function -> graph -> regenv -> Regset.t -> (reg -> loc).
-
-(** To ensure that the result of [graph_coloring] is a correct coloring,
- we check a posteriori its result using the following Coq functions.
- Let [coloring] be the function [reg -> loc] returned by [graph_coloring].
- The three properties checked are:
-- [coloring r1 <> coloring r2] if there is a conflict edge between
- [r1] and [r2] in the interference graph.
-- [coloring r1 <> R m2] if there is a conflict edge between pseudo-register
- [r1] and machine register [m2] in the interference graph.
-- For all [r] mentioned in the interference graph,
- the location [coloring r] is acceptable and has the same type as [r].
-*)
-
-Definition check_coloring_1 (g: graph) (coloring: reg -> loc) :=
- SetRegReg.for_all
- (fun r1r2 =>
- if Loc.eq (coloring (fst r1r2)) (coloring (snd r1r2)) then false else true)
- g.(interf_reg_reg).
-
-Definition check_coloring_2 (g: graph) (coloring: reg -> loc) :=
- SetRegMreg.for_all
- (fun r1mr2 =>
- if Loc.eq (coloring (fst r1mr2)) (R (snd r1mr2)) then false else true)
- g.(interf_reg_mreg).
-
-Definition same_typ (t1 t2: typ) :=
- match t1, t2 with
- | Tint, Tint => true
- | Tfloat, Tfloat => true
- | _, _ => false
- end.
-
-Definition loc_is_acceptable (l: loc) :=
- match l with
- | R r =>
- if In_dec Loc.eq l temporaries then false else true
- | S (Local ofs ty) =>
- if zlt ofs 0 then false else true
- | _ =>
- false
- end.
-
-Definition check_coloring_3 (rs: Regset.t) (env: regenv) (coloring: reg -> loc) :=
- Regset.for_all
- (fun r =>
- let l := coloring r in
- andb (loc_is_acceptable l) (same_typ (env r) (Loc.type l)))
- rs.
-
-Definition check_coloring
- (g: graph) (env: regenv) (rs: Regset.t) (coloring: reg -> loc) :=
- andb (check_coloring_1 g coloring)
- (andb (check_coloring_2 g coloring)
- (check_coloring_3 rs env coloring)).
-
-(** To preserve decidability of checking, the checks
- (especially the third one) are performed for the pseudo-registers
- mentioned in the interference graph. To facilitate the proofs,
- it is convenient to ensure that the properties hold for all
- pseudo-registers. To this end, we ``clip'' the candidate coloring
- returned by [graph_coloring]: the final coloring behave identically
- over pseudo-registers mentioned in the interference graph,
- but returns a dummy machine register of the correct type otherwise. *)
-
-Definition alloc_of_coloring (coloring: reg -> loc) (env: regenv) (rs: Regset.t) :=
- fun r =>
- if Regset.mem r rs
- then coloring r
- else match env r with Tint => R dummy_int_reg | Tfloat => R dummy_float_reg end.
-
-(** * Coloring of the interference graph *)
-
-(** The following function combines the phases described above:
- construction of the interference graph, coloring by untrusted
- Caml code, checking of the candidate coloring returned,
- and adjustment of this coloring. If the coloring candidate is
- incorrect, [None] is returned, causing register allocation to fail. *)
-
-Definition regalloc
- (f: function) (live: PMap.t Regset.t) (live0: Regset.t) (env: regenv) :=
- let g := interf_graph f live live0 in
- let rs := all_interf_regs g in
- let coloring := graph_coloring f g env rs in
- if check_coloring g env rs coloring
- then Some (alloc_of_coloring coloring env rs)
- else None.
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml
deleted file mode 100644
index 09ffb8e..0000000
--- a/backend/Coloringaux.ml
+++ /dev/null
@@ -1,867 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-open Camlcoq
-open Datatypes
-open AST
-open Maps
-open Registers
-open Machregs
-open Locations
-open RTL
-open RTLtyping
-open InterfGraph
-open Conventions1
-open Conventions
-
-(* George-Appel graph coloring *)
-
-(* \subsection{Internal representation of the interference graph} *)
-
-(* To implement George-Appel coloring, we first transform the representation
- of the interference graph, switching to the following
- imperative representation that is well suited to the coloring algorithm. *)
-
-(* Each node of the graph (i.e. each pseudo-register) is represented as
- follows. *)
-
-type node =
- { ident: int; (*r unique identifier *)
- typ: typ; (*r its type *)
- regname: reg option; (*r the RTL register it comes from *)
- regclass: int; (*r identifier of register class *)
- mutable accesses: int; (*r number of defs and uses *)
- mutable spillcost: float; (*r estimated cost of spilling *)
- mutable adjlist: node list; (*r all nodes it interferes with *)
- mutable degree: int; (*r number of adjacent nodes *)
- mutable movelist: move list; (*r list of moves it is involved in *)
- mutable alias: node option; (*r [Some n] if coalesced with [n] *)
- mutable color: loc option; (*r chosen color *)
- mutable nstate: nodestate; (*r in which set of nodes it is *)
- mutable nprev: node; (*r for double linking *)
- mutable nnext: node (*r for double linking *)
- }
-
-(* These are the possible states for nodes. *)
-
-and nodestate =
- | Colored
- | Initial
- | SimplifyWorklist
- | FreezeWorklist
- | SpillWorklist
- | CoalescedNodes
- | SelectStack
-
-(* Each move (i.e. wish to be put in the same location) is represented
- as follows. *)
-
-and move =
- { src: node; (*r source of the move *)
- dst: node; (*r destination of the move *)
- mutable mstate: movestate; (*r in which set of moves it is *)
- mutable mprev: move; (*r for double linking *)
- mutable mnext: move (*r for double linking *)
- }
-
-(* These are the possible states for moves *)
-
-and movestate =
- | CoalescedMoves
- | ConstrainedMoves
- | FrozenMoves
- | WorklistMoves
- | ActiveMoves
-
-(*i
-let name_of_node n =
- match n.color, n.regname with
- | Some(R r), _ ->
- begin match Machregsaux.name_of_register r with
- | None -> "fixed-reg"
- | Some s -> s
- end
- | Some(S _), _ -> "fixed-slot"
- | None, Some r -> Printf.sprintf "x%ld" (P.to_int32 r)
- | None, None -> "unknown-reg"
-*)
-
-(* The algorithm manipulates partitions of the nodes and of the moves
- according to their states, frequently moving a node or a move from
- a state to another, and frequently enumerating all nodes or all moves
- of a given state. To support these operations efficiently,
- nodes or moves having the same state are put into imperative doubly-linked
- lists, allowing for constant-time insertion and removal, and linear-time
- scanning. We now define the operations over these doubly-linked lists. *)
-
-module DLinkNode = struct
- type t = node
- let make state =
- let rec empty =
- { ident = 0; typ = Tint; regname = None; regclass = 0;
- adjlist = []; degree = 0; accesses = 0; spillcost = 0.0;
- movelist = []; alias = None; color = None;
- nstate = state; nprev = empty; nnext = empty }
- in empty
- let dummy = make Colored
- let clear dl = dl.nnext <- dl; dl.nprev <- dl
- let notempty dl = dl.nnext != dl
- let insert n dl =
- n.nstate <- dl.nstate;
- n.nnext <- dl.nnext; n.nprev <- dl;
- dl.nnext.nprev <- n; dl.nnext <- n
- let remove n dl =
- assert (n.nstate = dl.nstate);
- n.nnext.nprev <- n.nprev; n.nprev.nnext <- n.nnext
- let move n dl1 dl2 =
- remove n dl1; insert n dl2
- let pick dl =
- let n = dl.nnext in remove n dl; n
- let iter f dl =
- let rec iter n = if n != dl then (f n; iter n.nnext)
- in iter dl.nnext
- let fold f dl accu =
- let rec fold n accu = if n == dl then accu else fold n.nnext (f n accu)
- in fold dl.nnext accu
-end
-
-module DLinkMove = struct
- type t = move
- let make state =
- let rec empty =
- { src = DLinkNode.dummy; dst = DLinkNode.dummy;
- mstate = state; mprev = empty; mnext = empty }
- in empty
- let dummy = make CoalescedMoves
- let clear dl = dl.mnext <- dl; dl.mprev <- dl
- let notempty dl = dl.mnext != dl
- let insert m dl =
- m.mstate <- dl.mstate;
- m.mnext <- dl.mnext; m.mprev <- dl;
- dl.mnext.mprev <- m; dl.mnext <- m
- let remove m dl =
- assert (m.mstate = dl.mstate);
- m.mnext.mprev <- m.mprev; m.mprev.mnext <- m.mnext
- let move m dl1 dl2 =
- remove m dl1; insert m dl2
- let pick dl =
- let m = dl.mnext in remove m dl; m
- let iter f dl =
- let rec iter m = if m != dl then (f m; iter m.mnext)
- in iter dl.mnext
- let fold f dl accu =
- let rec fold m accu = if m == dl then accu else fold m.mnext (f m accu)
- in fold dl.mnext accu
-end
-
-(* Auxiliary data structures *)
-
-module IntSet = Set.Make(struct
- type t = int
- let compare (x:int) (y:int) = compare x y
-end)
-
-module IntPairSet = Set.Make(struct
- type t = int * int
- let compare ((x1, y1): (int * int)) (x2, y2) =
- if x1 < x2 then -1 else
- if x1 > x2 then 1 else
- if y1 < y2 then -1 else
- if y1 > y2 then 1 else
- 0
- end)
-
-(* Register classes *)
-
-let class_of_type = function Tint -> 0 | Tfloat -> 1
-
-let num_register_classes = 2
-
-let caller_save_registers = Array.make num_register_classes [||]
-
-let callee_save_registers = Array.make num_register_classes [||]
-
-let num_available_registers = Array.make num_register_classes 0
-
-let reserved_registers = ref ([]: mreg list)
-
-let allocatable_registers = ref ([]: mreg list)
-
-let rec remove_reserved = function
- | [] -> []
- | hd :: tl ->
- if List.mem hd !reserved_registers
- then remove_reserved tl
- else hd :: remove_reserved tl
-
-let init_regs() =
- let int_caller_save = remove_reserved int_caller_save_regs
- and float_caller_save = remove_reserved float_caller_save_regs
- and int_callee_save = remove_reserved int_callee_save_regs
- and float_callee_save = remove_reserved float_callee_save_regs in
- allocatable_registers :=
- List.flatten [int_caller_save; float_caller_save;
- int_callee_save; float_callee_save];
- caller_save_registers.(0) <- Array.of_list int_caller_save;
- caller_save_registers.(1) <- Array.of_list float_caller_save;
- callee_save_registers.(0) <- Array.of_list int_callee_save;
- callee_save_registers.(1) <- Array.of_list float_callee_save;
- for i = 0 to num_register_classes - 1 do
- num_available_registers.(i) <-
- Array.length caller_save_registers.(i)
- + Array.length callee_save_registers.(i)
- done
-
-(* \subsection{The George-Appel algorithm} *)
-
-(* Below is a straigthforward translation of the pseudo-code at the end
- of the TOPLAS article by George and Appel. Two bugs were fixed
- and are marked as such. Please refer to the article for explanations. *)
-
-(* The adjacency set *)
-let adjSet = ref IntPairSet.empty
-
-(* Low-degree, non-move-related nodes *)
-let simplifyWorklist = DLinkNode.make SimplifyWorklist
-
-(* Low-degree, move-related nodes *)
-let freezeWorklist = DLinkNode.make FreezeWorklist
-
-(* High-degree nodes *)
-let spillWorklist = DLinkNode.make SpillWorklist
-
-(* Nodes that have been coalesced *)
-let coalescedNodes = DLinkNode.make CoalescedNodes
-
-(* Moves that have been coalesced *)
-let coalescedMoves = DLinkMove.make CoalescedMoves
-
-(* Moves whose source and destination interfere *)
-let constrainedMoves = DLinkMove.make ConstrainedMoves
-
-(* Moves that will no longer be considered for coalescing *)
-let frozenMoves = DLinkMove.make FrozenMoves
-
-(* Moves enabled for possible coalescing *)
-let worklistMoves = DLinkMove.make WorklistMoves
-
-(* Moves not yet ready for coalescing *)
-let activeMoves = DLinkMove.make ActiveMoves
-
-(* To generate node identifiers *)
-let nextRegIdent = ref 0
-
-(* Initialization of all global data structures *)
-
-let init_graph() =
- adjSet := IntPairSet.empty;
- nextRegIdent := 0;
- DLinkNode.clear simplifyWorklist;
- DLinkNode.clear freezeWorklist;
- DLinkNode.clear spillWorklist;
- DLinkNode.clear coalescedNodes;
- DLinkMove.clear coalescedMoves;
- DLinkMove.clear frozenMoves;
- DLinkMove.clear worklistMoves;
- DLinkMove.clear activeMoves
-
-(* Determine if two nodes interfere *)
-
-let interfere n1 n2 =
- let i1 = n1.ident and i2 = n2.ident in
- let p = if i1 < i2 then (i1, i2) else (i2, i1) in
- IntPairSet.mem p !adjSet
-
-(* Add an edge to the graph. Assume edge is not in graph already.
- Do not add edges between nodes of different types. *)
-
-let addEdge n1 n2 =
- if n1.typ = n2.typ then begin
- (*i Printf.printf " %s -- %s;\n" (name_of_node n1) (name_of_node n2); *)
- assert (n1 != n2 && not (interfere n1 n2));
- let i1 = n1.ident and i2 = n2.ident in
- let p = if i1 < i2 then (i1, i2) else (i2, i1) in
- adjSet := IntPairSet.add p !adjSet;
- if n1.nstate <> Colored then begin
- n1.adjlist <- n2 :: n1.adjlist;
- n1.degree <- 1 + n1.degree
- end;
- if n2.nstate <> Colored then begin
- n2.adjlist <- n1 :: n2.adjlist;
- n2.degree <- 1 + n2.degree
- end
- end
-
-(* Apply the given function to the relevant adjacent nodes of a node *)
-
-let iterAdjacent f n =
- List.iter
- (fun n ->
- match n.nstate with
- | SelectStack | CoalescedNodes -> ()
- | _ -> f n)
- n.adjlist
-
-(* Determine the moves affecting a node *)
-
-let moveIsActiveOrWorklist m =
- match m.mstate with
- | ActiveMoves | WorklistMoves -> true
- | _ -> false
-
-let nodeMoves n =
- List.filter moveIsActiveOrWorklist n.movelist
-
-(* Determine whether a node is involved in a move *)
-
-let moveRelated n =
- List.exists moveIsActiveOrWorklist n.movelist
-
-(*i
-(* Check invariants *)
-
-let name_of_node n = string_of_int n.ident
-
-let degreeInvariant n =
- let c = ref 0 in
- iterAdjacent (fun n -> incr c) n;
- if !c <> n.degree then
- failwith("degree invariant violated by " ^ name_of_node n)
-
-let simplifyWorklistInvariant n =
- if n.degree < num_available_registers.(n.regclass)
- && not (moveRelated n)
- then ()
- else failwith("simplify worklist invariant violated by " ^ name_of_node n)
-
-let freezeWorklistInvariant n =
- if n.degree < num_available_registers.(n.regclass)
- && moveRelated n
- then ()
- else failwith("freeze worklist invariant violated by " ^ name_of_node n)
-
-let spillWorklistInvariant n =
- if n.degree >= num_available_registers.(n.regclass)
- then ()
- else failwith("spill worklist invariant violated by " ^ name_of_node n)
-
-let checkInvariants () =
- DLinkNode.iter
- (fun n -> degreeInvariant n; simplifyWorklistInvariant n)
- simplifyWorklist;
- DLinkNode.iter
- (fun n -> degreeInvariant n; freezeWorklistInvariant n)
- freezeWorklist;
- DLinkNode.iter
- (fun n -> degreeInvariant n; spillWorklistInvariant n)
- spillWorklist
-*)
-
-(* Build the internal representation of the graph *)
-
-let nodeOfReg r typenv spillcosts =
- let ty = typenv r in
- incr nextRegIdent;
- let (acc, cost) = spillcosts r in
- { ident = !nextRegIdent; typ = ty;
- regname = Some r; regclass = class_of_type ty;
- accesses = acc; spillcost = float cost;
- adjlist = []; degree = 0; movelist = []; alias = None;
- color = None;
- nstate = Initial;
- nprev = DLinkNode.dummy; nnext = DLinkNode.dummy }
-
-let nodeOfMreg mr =
- let ty = mreg_type mr in
- incr nextRegIdent;
- { ident = !nextRegIdent; typ = ty;
- regname = None; regclass = class_of_type ty;
- accesses = 0; spillcost = 0.0;
- adjlist = []; degree = 0; movelist = []; alias = None;
- color = Some (R mr);
- nstate = Colored;
- nprev = DLinkNode.dummy; nnext = DLinkNode.dummy }
-
-let build g typenv spillcosts =
- (* Associate an internal node to each pseudo-register and each location *)
- let reg_mapping = Hashtbl.create 27
- and mreg_mapping = Hashtbl.create 27 in
- let find_reg_node r =
- try
- Hashtbl.find reg_mapping r
- with Not_found ->
- let n = nodeOfReg r typenv spillcosts in
- Hashtbl.add reg_mapping r n;
- n
- and find_mreg_node mr =
- try
- Hashtbl.find mreg_mapping mr
- with Not_found ->
- let n = nodeOfMreg mr in
- Hashtbl.add mreg_mapping mr n;
- n in
- (* Fill the adjacency set and the adjacency lists; compute the degrees. *)
- SetRegReg.fold
- (fun (r1, r2) () ->
- addEdge (find_reg_node r1) (find_reg_node r2))
- g.interf_reg_reg ();
- SetRegMreg.fold
- (fun (r1, mr2) () ->
- addEdge (find_reg_node r1) (find_mreg_node mr2))
- g.interf_reg_mreg ();
- (* Process the moves and insert them in worklistMoves *)
- let add_move n1 n2 =
- (*i Printf.printf " %s -- %s [color=\"red\"];\n" (name_of_node n1) (name_of_node n2); *)
- let m =
- { src = n1; dst = n2; mstate = WorklistMoves;
- mnext = DLinkMove.dummy; mprev = DLinkMove.dummy } in
- n1.movelist <- m :: n1.movelist;
- n2.movelist <- m :: n2.movelist;
- DLinkMove.insert m worklistMoves in
- SetRegReg.fold
- (fun (r1, r2) () ->
- add_move (find_reg_node r1) (find_reg_node r2))
- g.pref_reg_reg ();
- SetRegMreg.fold
- (fun (r1, mr2) () ->
- let r1' = find_reg_node r1 in
- if List.mem mr2 !allocatable_registers then
- add_move r1' (find_mreg_node mr2))
- g.pref_reg_mreg ();
- (* Initial partition of nodes into spill / freeze / simplify *)
- Hashtbl.iter
- (fun r n ->
- assert (n.nstate = Initial);
- let k = num_available_registers.(n.regclass) in
- if n.degree >= k then
- DLinkNode.insert n spillWorklist
- else if moveRelated n then
- DLinkNode.insert n freezeWorklist
- else
- DLinkNode.insert n simplifyWorklist)
- reg_mapping;
- (* Return mapping from pseudo-registers to nodes *)
- reg_mapping
-
-(* Enable moves that have become low-degree related *)
-
-let enableMoves n =
- List.iter
- (fun m ->
- if m.mstate = ActiveMoves
- then DLinkMove.move m activeMoves worklistMoves)
- (nodeMoves n)
-
-(* Simulate the removal of a node from the graph *)
-
-let decrementDegree n =
- let k = num_available_registers.(n.regclass) in
- let d = n.degree in
- n.degree <- d - 1;
- if d = k then begin
- enableMoves n;
- iterAdjacent enableMoves n;
-(* if n.nstate <> Colored then begin *)
- if moveRelated n
- then DLinkNode.move n spillWorklist freezeWorklist
- else DLinkNode.move n spillWorklist simplifyWorklist
-(* end *)
- end
-
-(* Simulate the effect of combining nodes [n1] and [n3] on [n2],
- where [n2] is a node adjacent to [n3]. *)
-
-let combineEdge n1 n2 =
- assert (n1 != n2);
- if interfere n1 n2 then begin
- (* The two edges n2--n3 and n2--n1 become one, so degree of n2 decreases *)
- decrementDegree n2
- end else begin
- (* Add new edge *)
- let i1 = n1.ident and i2 = n2.ident in
- let p = if i1 < i2 then (i1, i2) else (i2, i1) in
- adjSet := IntPairSet.add p !adjSet;
- if n1.nstate <> Colored then begin
- n1.adjlist <- n2 :: n1.adjlist;
- n1.degree <- 1 + n1.degree
- end;
- if n2.nstate <> Colored then begin
- n2.adjlist <- n1 :: n2.adjlist;
- (* n2's degree stays the same because the old edge n2--n3 disappears
- and becomes the new edge n2--n1 *)
- end
- end
-
-(* Simplification of a low-degree node *)
-
-let simplify () =
- let n = DLinkNode.pick simplifyWorklist in
- (*i Printf.printf "Simplifying %s\n" (name_of_node n); i*)
- n.nstate <- SelectStack;
- iterAdjacent decrementDegree n;
- n
-
-(* Briggs's conservative coalescing criterion. In the terminology of
- Hailperin, "Comparing Conservative Coalescing Criteria",
- TOPLAS 27(3) 2005, this is the full Briggs criterion, slightly
- more powerful than the one in George and Appel's paper. *)
-
-let canCoalesceBriggs u v =
- let seen = ref IntSet.empty in
- let k = num_available_registers.(u.regclass) in
- let c = ref 0 in
- let consider other n =
- if not (IntSet.mem n.ident !seen) then begin
- seen := IntSet.add n.ident !seen;
- (* if n interferes with both u and v, its degree will decrease by one
- after coalescing *)
- let degree_after_coalescing =
- if interfere n other then n.degree - 1 else n.degree in
- if degree_after_coalescing >= k then begin
- incr c;
- if !c >= k then raise Exit
- end
- end in
- try
- iterAdjacent (consider v) u;
- iterAdjacent (consider u) v;
- (*i Printf.printf " Briggs: OK\n"; *)
- true
- with Exit ->
- (*i Printf.printf " Briggs: no\n"; *)
- false
-
-(* George's conservative coalescing criterion: all high-degree neighbors
- of [v] are neighbors of [u]. *)
-
-let canCoalesceGeorge u v =
- let k = num_available_registers.(u.regclass) in
- let isOK t =
- if t.nstate = Colored then
- if u.nstate = Colored || interfere t u then () else raise Exit
- else
- if t.degree < k || interfere t u then () else raise Exit
- in
- try
- iterAdjacent isOK v;
- (*i Printf.printf " George: OK\n"; *)
- true
- with Exit ->
- (*i Printf.printf " George: no\n"; *)
- false
-
-(* The combined coalescing criterion. [u] can be precolored, but
- [v] is not. According to George and Appel's paper:
-- If [u] is precolored, use George's criterion.
-- If [u] is not precolored, use Briggs's criterion.
-
- As noted by Hailperin, for non-precolored nodes, George's criterion
- is incomparable with Briggs's: there are cases where G says yes
- and B says no. Typically, [u] is a long-lived variable with many
- interferences, and [v] is a short-lived temporary copy of [u]
- that has no more interferences than [u]. Coalescing [u] and [v]
- is "weakly safe" in Hailperin's terminology: [u] is no harder to color,
- [u]'s neighbors are no harder to color either, but if we end up
- spilling [u], we'll spill [v] as well. However, if [v] has at most
- one def and one use, CompCert generates equivalent code if
- both [u] and [v] are spilled and if [u] is spilled but not [v],
- so George's criterion is safe in this case.
-*)
-
-let thresholdGeorge = 2 (* = 1 def + 1 use *)
-
-let canCoalesce u v =
- if u.nstate = Colored
- then canCoalesceGeorge u v
- else canCoalesceBriggs u v
- || (v.accesses <= thresholdGeorge && canCoalesceGeorge u v)
- || (u.accesses <= thresholdGeorge && canCoalesceGeorge v u)
-
-(* Update worklists after a move was processed *)
-
-let addWorkList u =
- if (not (u.nstate = Colored))
- && u.degree < num_available_registers.(u.regclass)
- && (not (moveRelated u))
- then DLinkNode.move u freezeWorklist simplifyWorklist
-
-(* Return the canonical representative of a possibly coalesced node *)
-
-let rec getAlias n =
- match n.alias with None -> n | Some n' -> getAlias n'
-
-(* Combine two nodes *)
-
-let combine u v =
- (*i Printf.printf "Combining %s and %s\n" (name_of_node u) (name_of_node v); *)
- if v.nstate = FreezeWorklist
- then DLinkNode.move v freezeWorklist coalescedNodes
- else DLinkNode.move v spillWorklist coalescedNodes;
- v.alias <- Some u;
- (* Precolored nodes often have big movelists, and if one of [u] and [v]
- is precolored, it is []u. So, append [v.movelist] to [u.movelist]
- instead of the other way around. *)
- u.movelist <- List.rev_append v.movelist u.movelist;
- u.spillcost <- u.spillcost +. v.spillcost;
- iterAdjacent (combineEdge u) v; (*r original code using [decrementDegree] is buggy *)
- enableMoves v; (*r added as per Appel's book erratum *)
- if u.degree >= num_available_registers.(u.regclass)
- && u.nstate = FreezeWorklist
- then DLinkNode.move u freezeWorklist spillWorklist
-
-(* Attempt coalescing *)
-
-let coalesce () =
- let m = DLinkMove.pick worklistMoves in
- let x = getAlias m.src and y = getAlias m.dst in
- let (u, v) = if y.nstate = Colored then (y, x) else (x, y) in
- (*i Printf.printf "Attempt coalescing %s and %s\n" (name_of_node u) (name_of_node v); *)
- if u == v then begin
- DLinkMove.insert m coalescedMoves;
- addWorkList u
- end else if v.nstate = Colored || interfere u v then begin
- DLinkMove.insert m constrainedMoves;
- addWorkList u;
- addWorkList v
- end else if canCoalesce u v then begin
- DLinkMove.insert m coalescedMoves;
- combine u v;
- addWorkList u
- end else begin
- DLinkMove.insert m activeMoves
- end
-
-(* Freeze moves associated with node [u] *)
-
-let freezeMoves u =
- let u' = getAlias u in
- let freeze m =
- let y = getAlias m.src in
- let v = if y == u' then getAlias m.dst else y in
- DLinkMove.move m activeMoves frozenMoves;
- if not (moveRelated v)
- && v.degree < num_available_registers.(v.regclass)
- && v.nstate <> Colored
- then DLinkNode.move v freezeWorklist simplifyWorklist in
- List.iter freeze (nodeMoves u)
-
-(* Pick a move and freeze it *)
-
-let freeze () =
- let u = DLinkNode.pick freezeWorklist in
- (*i Printf.printf "Freezing %s\n" (name_of_node u);*)
- DLinkNode.insert u simplifyWorklist;
- freezeMoves u
-
-(* Chaitin's cost measure *)
-
-let spillCost n =
-(*i
- Printf.printf "spillCost %s: uses = %.0f degree = %d cost = %f\n"
- (name_of_node n) n.spillcost n.degree (n.spillcost /. float n.degree);
-*)
- n.spillcost /. float n.degree
-
-(* Spill a node *)
-
-let selectSpill () =
- (* Find a spillable node of minimal cost *)
- let (n, cost) =
- DLinkNode.fold
- (fun n (best_node, best_cost as best) ->
- let cost = spillCost n in
- if cost < best_cost then (n, cost) else best)
- spillWorklist (DLinkNode.dummy, infinity) in
- assert (n != DLinkNode.dummy);
- DLinkNode.remove n spillWorklist;
- (*i Printf.printf "Spilling %s\n" (name_of_node n);*)
- freezeMoves n;
- n.nstate <- SelectStack;
- iterAdjacent decrementDegree n;
- n
-
-(* Produce the order of nodes that we'll use for coloring *)
-
-let rec nodeOrder stack =
- (*i checkInvariants(); *)
- if DLinkNode.notempty simplifyWorklist then
- (let n = simplify() in nodeOrder (n :: stack))
- else if DLinkMove.notempty worklistMoves then
- (coalesce(); nodeOrder stack)
- else if DLinkNode.notempty freezeWorklist then
- (freeze(); nodeOrder stack)
- else if DLinkNode.notempty spillWorklist then
- (let n = selectSpill() in nodeOrder (n :: stack))
- else
- stack
-
-(* Assign a color (i.e. a hardware register or a stack location)
- to a node. The color is chosen among the colors that are not
- assigned to nodes with which this node interferes. The choice
- is guided by the following heuristics: consider first caller-save
- hardware register of the correct type; second, callee-save registers;
- third, a stack location. Callee-save registers and stack locations
- are ``expensive'' resources, so we try to minimize their number
- by picking the smallest available callee-save register or stack location.
- In contrast, caller-save registers are ``free'', so we pick an
- available one pseudo-randomly. *)
-
-module Locset =
- Set.Make(struct type t = loc let compare = compare end)
-
-let start_points = Array.make num_register_classes 0
-
-let find_reg conflicts regclass =
- let rec find avail curr last =
- if curr >= last then None else begin
- let l = R avail.(curr) in
- if Locset.mem l conflicts
- then find avail (curr + 1) last
- else Some l
- end in
- let caller_save = caller_save_registers.(regclass)
- and callee_save = callee_save_registers.(regclass)
- and start = start_points.(regclass) in
- match find caller_save start (Array.length caller_save) with
- | Some _ as res ->
- start_points.(regclass) <-
- (if start + 1 < Array.length caller_save then start + 1 else 0);
- res
- | None ->
- match find caller_save 0 start with
- | Some _ as res ->
- start_points.(regclass) <-
- (if start + 1 < Array.length caller_save then start + 1 else 0);
- res
- | None ->
- find callee_save 0 (Array.length callee_save)
-
-(* Aggressive coalescing of stack slots. When assigning a slot,
- try first the slots assigned to the temporaries for which we
- have a preference, provided no conflict occurs. *)
-
-let rec reuse_slot conflicts n mvlist =
- match mvlist with
- | [] -> None
- | mv :: rem ->
- let attempt_reuse n' =
- match n'.color with
- | Some(S _ as l) when not (Locset.mem l conflicts) -> Some l
- | _ -> reuse_slot conflicts n rem in
- let src = getAlias mv.src and dst = getAlias mv.dst in
- if n == src then attempt_reuse dst
- else if n == dst then attempt_reuse src
- else reuse_slot conflicts n rem (* should not happen? *)
-
-(* If no reuse possible, assign lowest nonconflicting stack slot. *)
-
-let find_slot conflicts typ =
- let rec find curr =
- let l = S(Local(curr, typ)) in
- if Locset.mem l conflicts then find (Z.succ curr) else l
- in find Z.zero
-
-let assign_color n =
- let conflicts = ref Locset.empty in
- List.iter
- (fun n' ->
- match (getAlias n').color with
- | None -> ()
- | Some l -> conflicts := Locset.add l !conflicts)
- n.adjlist;
- match find_reg !conflicts n.regclass with
- | Some loc ->
- n.color <- Some loc
- | None ->
- match reuse_slot !conflicts n n.movelist with
- | Some loc ->
- n.color <- Some loc
- | None ->
- n.color <- Some (find_slot !conflicts n.typ)
-
-(* Extract the location of a node *)
-
-let location_of_node n =
- match n.color with
- | None -> assert false
- | Some loc -> loc
-
-(* Estimate spilling costs and counts the number of defs and uses.
- Currently, we charge 10 for each access and 1 for each move.
- To do: take loops into account. *)
-
-let spill_costs f =
- let costs = ref (PMap.init (0,0)) in
- let cost r =
- PMap.get r !costs in
- let charge amount r =
- let (n, c) = cost r in
- costs := PMap.set r (n + 1, c + amount) !costs in
- let charge_list amount rl =
- List.iter (charge amount) rl in
- let charge_ros amount ros =
- match ros with Coq_inl r -> charge amount r | Coq_inr _ -> () in
- let process_instr () pc i =
- match i with
- | Inop _ -> ()
- | Iop(Op.Omove, arg::nil, res, _) ->
- charge 1 arg; charge 1 res
- | Iop(op, args, res, _) ->
- charge_list 10 args; charge 10 res
- | Iload(chunk, addr, args, dst, _) ->
- charge_list 10 args; charge 10 dst
- | Istore(chunk, addr, args, src, _) ->
- charge_list 10 args; charge 10 src
- | Icall(sg, ros, args, res, _) ->
- charge_ros 10 ros; charge_list 1 args; charge 1 res
- | Itailcall(sg, ros, args) ->
- charge_ros 10 ros; charge_list 1 args
- | Ibuiltin(EF_annot _, args, res, _) ->
- (* arguments are not actually used, so charge 0 for them;
- result is not used but should not be spilled, so charge a lot *)
- charge 1_000_000 res
- | Ibuiltin(EF_annot_val _, args, res, _) ->
- (* like a move *)
- charge_list 1 args; charge 1 res
- | Ibuiltin((EF_vstore _|EF_vstore_global _|EF_memcpy _), args, res, _) ->
- (* result is not used but should not be spilled, so charge a lot *)
- charge_list 10 args; charge 1_000_000 res
- | Ibuiltin(ef, args, res, _) ->
- charge_list 10 args; charge 10 res
- | Icond(cond, args, _, _) ->
- charge_list 10 args
- | Ijumptable(arg, _) ->
- charge 10 arg
- | Ireturn(Some r) ->
- charge 1 r
- | Ireturn None ->
- () in
- charge_list 1 f.fn_params;
- PTree.fold process_instr f.fn_code ();
- (* Result is cost function reg -> (num accesses, integer cost *)
- cost
-
-(* This is the entry point for graph coloring. *)
-
-let graph_coloring (f: coq_function) (g: graph) (env: regenv) (regs: Regset.t)
- : (reg -> loc) =
- init_regs();
- init_graph();
- Array.fill start_points 0 num_register_classes 0;
- (*i Printf.printf "graph G {\n"; *)
- let mapping = build g env (spill_costs f) in
- (*i Printf.printf "}\n"; *)
- List.iter assign_color (nodeOrder []);
- init_graph(); (* free data structures *)
- fun r ->
- try location_of_node (getAlias (Hashtbl.find mapping r))
- with Not_found -> R IT1 (* any location *)
diff --git a/backend/Coloringaux.mli b/backend/Coloringaux.mli
deleted file mode 100644
index 7597c7c..0000000
--- a/backend/Coloringaux.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-open Registers
-open Locations
-open RTL
-open RTLtyping
-open InterfGraph
-
-val graph_coloring:
- coq_function -> graph -> regenv -> Regset.t -> (reg -> loc)
-
-val reserved_registers: Machregs.mreg list ref
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v
deleted file mode 100644
index 8ebc87e..0000000
--- a/backend/Coloringproof.v
+++ /dev/null
@@ -1,957 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-(** Correctness of graph coloring. *)
-
-Require Import SetoidList.
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import RTLtyping.
-Require Import Locations.
-Require Import Conventions.
-Require Import InterfGraph.
-Require Import Coloring.
-
-(** * Correctness of the interference graph *)
-
-(** We show that the interference graph built by [interf_graph]
- is correct in the sense that it contains all conflict edges
- that we need.
-
- Many boring lemmas on the auxiliary functions used to construct
- the interference graph follow. The lemmas are of two kinds:
- the ``increasing'' lemmas show that the auxiliary functions only add
- edges to the interference graph, but do not remove existing edges;
- and the ``correct'' lemmas show that the auxiliary functions
- correctly add the edges that we'd like them to add. *)
-
-Lemma graph_incl_refl:
- forall g, graph_incl g g.
-Proof.
- intros; split; auto.
-Qed.
-
-Lemma add_interf_live_incl_aux:
- forall (filter: reg -> bool) res live g,
- graph_incl g
- (List.fold_left
- (fun g r => if filter r then add_interf r res g else g)
- live g).
-Proof.
- induction live; simpl; intros.
- apply graph_incl_refl.
- apply graph_incl_trans with (if filter a then add_interf a res g else g).
- case (filter a).
- apply add_interf_incl.
- apply graph_incl_refl.
- apply IHlive.
-Qed.
-
-Lemma add_interf_live_incl:
- forall (filter: reg -> bool) res live g,
- graph_incl g (add_interf_live filter res live g).
-Proof.
- intros. unfold add_interf_live. rewrite Regset.fold_1.
- apply add_interf_live_incl_aux.
-Qed.
-
-Lemma add_interf_live_correct_aux:
- forall filter res r live,
- InA Regset.E.eq r live -> filter r = true ->
- forall g,
- interfere r res
- (List.fold_left
- (fun g r => if filter r then add_interf r res g else g)
- live g).
-Proof.
- induction 1; simpl; intros.
- hnf in H. subst y. rewrite H0.
- generalize (add_interf_live_incl_aux filter res l (add_interf r res g)).
- intros [A B].
- apply A. apply add_interf_correct.
- apply IHInA; auto.
-Qed.
-
-Lemma add_interf_live_correct:
- forall filter res live g r,
- Regset.In r live ->
- filter r = true ->
- interfere r res (add_interf_live filter res live g).
-Proof.
- intros. unfold add_interf_live. rewrite Regset.fold_1.
- apply add_interf_live_correct_aux; auto.
- apply Regset.elements_1. auto.
-Qed.
-
-Lemma add_interf_op_incl:
- forall res live g,
- graph_incl g (add_interf_op res live g).
-Proof.
- intros; unfold add_interf_op. apply add_interf_live_incl.
-Qed.
-
-Lemma add_interf_op_correct:
- forall res live g r,
- Regset.In r live ->
- r <> res ->
- interfere r res (add_interf_op res live g).
-Proof.
- intros. unfold add_interf_op.
- apply add_interf_live_correct.
- auto. destruct (Reg.eq r res); congruence.
-Qed.
-
-Lemma add_interf_move_incl:
- forall arg res live g,
- graph_incl g (add_interf_move arg res live g).
-Proof.
- intros; unfold add_interf_move. apply add_interf_live_incl.
-Qed.
-
-Lemma add_interf_move_correct:
- forall arg res live g r,
- Regset.In r live ->
- r <> arg -> r <> res ->
- interfere r res (add_interf_move arg res live g).
-Proof.
- intros. unfold add_interf_move.
- apply add_interf_live_correct.
- auto.
- rewrite dec_eq_false; auto. rewrite dec_eq_false; auto.
-Qed.
-
-Lemma add_interf_destroyed_incl_aux_1:
- forall mr live g,
- graph_incl g
- (List.fold_left (fun g r => add_interf_mreg r mr g) live g).
-Proof.
- induction live; simpl; intros.
- apply graph_incl_refl.
- apply graph_incl_trans with (add_interf_mreg a mr g).
- apply add_interf_mreg_incl.
- auto.
-Qed.
-
-Lemma add_interf_destroyed_incl_aux_2:
- forall mr live g,
- graph_incl g
- (Regset.fold (fun r g => add_interf_mreg r mr g) live g).
-Proof.
- intros. rewrite Regset.fold_1. apply add_interf_destroyed_incl_aux_1.
-Qed.
-
-Lemma add_interf_destroyed_incl:
- forall live destroyed g,
- graph_incl g (add_interf_destroyed live destroyed g).
-Proof.
- induction destroyed; simpl; intros.
- apply graph_incl_refl.
- eapply graph_incl_trans; [idtac|apply IHdestroyed].
- apply add_interf_destroyed_incl_aux_2.
-Qed.
-
-Lemma add_interfs_indirect_call_incl:
- forall rfun locs g,
- graph_incl g (add_interfs_indirect_call rfun locs g).
-Proof.
- unfold add_interfs_indirect_call. induction locs; simpl; intros.
- apply graph_incl_refl.
- destruct a. eapply graph_incl_trans; [idtac|eauto].
- apply add_interf_mreg_incl.
- auto.
-Qed.
-
-Lemma add_interfs_call_incl:
- forall ros locs g,
- graph_incl g (add_interf_call ros locs g).
-Proof.
- intros. unfold add_interf_call. destruct ros.
- apply add_interfs_indirect_call_incl.
- apply graph_incl_refl.
-Qed.
-
-Lemma interfere_incl:
- forall r1 r2 g1 g2,
- graph_incl g1 g2 ->
- interfere r1 r2 g1 ->
- interfere r1 r2 g2.
-Proof.
- unfold graph_incl; intros. elim H; auto.
-Qed.
-
-Lemma interfere_mreg_incl:
- forall r1 r2 g1 g2,
- graph_incl g1 g2 ->
- interfere_mreg r1 r2 g1 ->
- interfere_mreg r1 r2 g2.
-Proof.
- unfold graph_incl; intros. elim H; auto.
-Qed.
-
-Lemma add_interf_destroyed_correct_aux_1:
- forall mr r live,
- InA Regset.E.eq r live ->
- forall g,
- interfere_mreg r mr
- (List.fold_left (fun g r => add_interf_mreg r mr g) live g).
-Proof.
- induction 1; simpl; intros.
- hnf in H; subst y. eapply interfere_mreg_incl.
- apply add_interf_destroyed_incl_aux_1.
- apply add_interf_mreg_correct.
- auto.
-Qed.
-
-Lemma add_interf_destroyed_correct_aux_2:
- forall mr live g r,
- Regset.In r live ->
- interfere_mreg r mr
- (Regset.fold (fun r g => add_interf_mreg r mr g) live g).
-Proof.
- intros. rewrite Regset.fold_1. apply add_interf_destroyed_correct_aux_1.
- apply Regset.elements_1. auto.
-Qed.
-
-Lemma add_interf_destroyed_correct:
- forall live destroyed g r mr,
- Regset.In r live ->
- In mr destroyed ->
- interfere_mreg r mr (add_interf_destroyed live destroyed g).
-Proof.
- induction destroyed; simpl; intros.
- elim H0.
- elim H0; intros.
- subst a. eapply interfere_mreg_incl.
- apply add_interf_destroyed_incl.
- apply add_interf_destroyed_correct_aux_2; auto.
- apply IHdestroyed; auto.
-Qed.
-
-Lemma add_interfs_indirect_call_correct:
- forall rfun mr locs g,
- In (R mr) locs ->
- interfere_mreg rfun mr (add_interfs_indirect_call rfun locs g).
-Proof.
- unfold add_interfs_indirect_call. induction locs; simpl; intros.
- elim H.
- destruct H. subst a.
- eapply interfere_mreg_incl.
- apply (add_interfs_indirect_call_incl rfun locs (add_interf_mreg rfun mr g)).
- apply add_interf_mreg_correct.
- auto.
-Qed.
-
-Lemma add_interfs_call_correct:
- forall rfun locs g mr,
- In (R mr) locs ->
- interfere_mreg rfun mr (add_interf_call (inl _ rfun) locs g).
-Proof.
- intros. unfold add_interf_call.
- apply add_interfs_indirect_call_correct. auto.
-Qed.
-
-Lemma add_prefs_call_incl:
- forall args locs g,
- graph_incl g (add_prefs_call args locs g).
-Proof.
- induction args; destruct locs; simpl; intros;
- try apply graph_incl_refl.
- destruct l.
- eapply graph_incl_trans; [idtac|eauto].
- apply add_pref_mreg_incl.
- auto.
-Qed.
-
-Lemma add_prefs_builtin_incl:
- forall ef args res g,
- graph_incl g (add_prefs_builtin ef args res g).
-Proof.
- intros. unfold add_prefs_builtin.
- destruct ef; try apply graph_incl_refl.
- destruct args; try apply graph_incl_refl.
- apply add_pref_incl.
-Qed.
-
-Lemma add_interf_entry_incl:
- forall params live g,
- graph_incl g (add_interf_entry params live g).
-Proof.
- unfold add_interf_entry; induction params; simpl; intros.
- apply graph_incl_refl.
- eapply graph_incl_trans; [idtac|eauto].
- apply add_interf_op_incl.
-Qed.
-
-Lemma add_interf_entry_correct:
- forall params live g r1 r2,
- In r1 params ->
- Regset.In r2 live ->
- r1 <> r2 ->
- interfere r1 r2 (add_interf_entry params live g).
-Proof.
- unfold add_interf_entry; induction params; simpl; intros.
- elim H.
- elim H; intro.
- subst a. apply interfere_incl with (add_interf_op r1 live g).
- exact (add_interf_entry_incl _ _ _).
- apply interfere_sym. apply add_interf_op_correct; auto.
- auto.
-Qed.
-
-Lemma add_interf_params_incl_aux:
- forall p1 pl g,
- graph_incl g
- (List.fold_left
- (fun g r => if Reg.eq r p1 then g else add_interf r p1 g)
- pl g).
-Proof.
- induction pl; simpl; intros.
- apply graph_incl_refl.
- eapply graph_incl_trans; [idtac|eauto].
- case (Reg.eq a p1); intro.
- apply graph_incl_refl. apply add_interf_incl.
-Qed.
-
-Lemma add_interf_params_incl:
- forall pl g,
- graph_incl g (add_interf_params pl g).
-Proof.
- induction pl; simpl; intros.
- apply graph_incl_refl.
- eapply graph_incl_trans; [idtac|eauto].
- apply add_interf_params_incl_aux.
-Qed.
-
-Lemma add_interf_params_correct_aux:
- forall p1 pl g p2,
- In p2 pl ->
- p1 <> p2 ->
- interfere p1 p2
- (List.fold_left
- (fun g r => if Reg.eq r p1 then g else add_interf r p1 g)
- pl g).
-Proof.
- induction pl; simpl; intros.
- elim H.
- elim H; intro; clear H.
- subst a. apply interfere_sym. eapply interfere_incl.
- apply add_interf_params_incl_aux.
- case (Reg.eq p2 p1); intro.
- congruence. apply add_interf_correct.
- auto.
-Qed.
-
-Lemma add_interf_params_correct:
- forall pl g r1 r2,
- In r1 pl -> In r2 pl -> r1 <> r2 ->
- interfere r1 r2 (add_interf_params pl g).
-Proof.
- induction pl; simpl; intros.
- elim H.
- elim H; intro; clear H; elim H0; intro; clear H0.
- congruence.
- subst a. eapply interfere_incl. apply add_interf_params_incl.
- apply add_interf_params_correct_aux; auto.
- subst a. apply interfere_sym.
- eapply interfere_incl. apply add_interf_params_incl.
- apply add_interf_params_correct_aux; auto.
- auto.
-Qed.
-
-Lemma add_edges_instr_incl:
- forall sig instr live g,
- graph_incl g (add_edges_instr sig instr live g).
-Proof.
- intros. destruct instr; unfold add_edges_instr;
- try apply graph_incl_refl.
- case (Regset.mem r live).
- destruct (is_move_operation o l).
- eapply graph_incl_trans; [idtac|apply add_pref_incl].
- apply add_interf_move_incl.
- apply add_interf_op_incl.
- apply graph_incl_refl.
- case (Regset.mem r live).
- apply add_interf_op_incl.
- apply graph_incl_refl.
- eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
- eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
- eapply graph_incl_trans; [idtac|apply add_interf_op_incl].
- eapply graph_incl_trans; [idtac|apply add_interfs_call_incl].
- apply add_interf_destroyed_incl.
- eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
- apply add_interfs_call_incl.
- eapply graph_incl_trans. apply add_interf_op_incl. apply add_prefs_builtin_incl.
- destruct o.
- apply add_pref_mreg_incl.
- apply graph_incl_refl.
-Qed.
-
-(** The proposition below states that graph [g] contains
- all the conflict edges expected for instruction [instr]. *)
-
-Definition correct_interf_instr
- (live: Regset.t) (instr: instruction) (g: graph) : Prop :=
- match instr with
- | Iop op args res s =>
- match is_move_operation op args with
- | Some arg =>
- forall r,
- Regset.In res live ->
- Regset.In r live ->
- r <> res -> r <> arg -> interfere r res g
- | None =>
- forall r,
- Regset.In res live ->
- Regset.In r live ->
- r <> res -> interfere r res g
- end
- | Iload chunk addr args res s =>
- forall r,
- Regset.In res live ->
- Regset.In r live ->
- r <> res -> interfere r res g
- | Icall sig ros args res s =>
- (forall r mr,
- Regset.In r live ->
- In mr destroyed_at_call_regs ->
- r <> res ->
- interfere_mreg r mr g)
- /\ (forall r,
- Regset.In r live ->
- r <> res -> interfere r res g)
- /\ (match ros with
- | inl rfun => forall mr, In (R mr) (loc_arguments sig) ->
- interfere_mreg rfun mr g
- | inr idfun => True
- end)
- | Itailcall sig ros args =>
- match ros with
- | inl rfun => forall mr, In (R mr) (loc_arguments sig) ->
- interfere_mreg rfun mr g
- | inr idfun => True
- end
- | Ibuiltin ef args res s =>
- forall r,
- Regset.In r live ->
- r <> res -> interfere r res g
- | _ =>
- True
- end.
-
-Lemma correct_interf_instr_incl:
- forall live instr g1 g2,
- graph_incl g1 g2 ->
- correct_interf_instr live instr g1 ->
- correct_interf_instr live instr g2.
-Proof.
- intros until g2. intro.
- unfold correct_interf_instr; destruct instr; auto.
- destruct (is_move_operation o l).
- intros. eapply interfere_incl; eauto.
- intros. eapply interfere_incl; eauto.
- intros. eapply interfere_incl; eauto.
- intros [A [B C]].
- split. intros. eapply interfere_mreg_incl; eauto.
- split. intros. eapply interfere_incl; eauto.
- destruct s0; auto. intros. eapply interfere_mreg_incl; eauto.
- destruct s0; auto. intros. eapply interfere_mreg_incl; eauto.
- intros. eapply interfere_incl; eauto.
-Qed.
-
-Lemma add_edges_instr_correct:
- forall sig instr live g,
- correct_interf_instr live instr (add_edges_instr sig instr live g).
-Proof.
- intros.
- destruct instr; unfold add_edges_instr; unfold correct_interf_instr; auto.
- destruct (is_move_operation o l); intros.
- rewrite Regset.mem_1; auto. eapply interfere_incl.
- apply add_pref_incl. apply add_interf_move_correct; auto.
- rewrite Regset.mem_1; auto. apply add_interf_op_correct; auto.
-
- intros. rewrite Regset.mem_1; auto. apply add_interf_op_correct; auto.
-
- (* Icall *)
- set (largs := loc_arguments s).
- set (lres := loc_result s).
- split. intros.
- apply interfere_mreg_incl with
- (add_interf_destroyed (Regset.remove r live) destroyed_at_call_regs g).
- eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
- eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
- eapply graph_incl_trans; [idtac|apply add_interf_op_incl].
- apply add_interfs_call_incl.
- apply add_interf_destroyed_correct; auto.
- apply Regset.remove_2; auto.
-
- split. intros.
- eapply interfere_incl.
- eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
- apply add_pref_mreg_incl.
- apply add_interf_op_correct; auto.
-
- destruct s0; auto; intros.
- eapply interfere_mreg_incl.
- eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
- eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
- apply add_interf_op_incl.
- apply add_interfs_call_correct. auto.
-
- (* Itailcall *)
- destruct s0; auto; intros.
- eapply interfere_mreg_incl.
- apply add_prefs_call_incl.
- apply add_interfs_call_correct. auto.
-
- (* Ibuiltin *)
- intros. eapply interfere_incl. apply add_prefs_builtin_incl.
- apply add_interf_op_correct; auto.
-Qed.
-
-Lemma add_edges_instrs_correct:
- forall f live pc i,
- f.(fn_code)!pc = Some i ->
- correct_interf_instr live!!pc i (add_edges_instrs f live).
-Proof.
- intros f live.
- set (P := fun (c: code) g =>
- forall pc i, c!pc = Some i -> correct_interf_instr live#pc i g).
- set (F := (fun (g : graph) (pc0 : positive) (i0 : instruction) =>
- add_edges_instr (fn_sig f) i0 live # pc0 g)).
- change (P f.(fn_code) (PTree.fold F f.(fn_code) empty_graph)).
- apply PTree_Properties.fold_rec; unfold P; intros.
- apply H0. rewrite H. auto.
- rewrite PTree.gempty in H. congruence.
- rewrite PTree.gsspec in H2. destruct (peq pc k).
- inv H2. unfold F. apply add_edges_instr_correct.
- apply correct_interf_instr_incl with a.
- unfold F; apply add_edges_instr_incl.
- apply H1; auto.
-Qed.
-
-(** Here are the three correctness properties of the generated
- inference graph. First, it contains the conflict edges
- needed by every instruction of the function. *)
-
-Lemma interf_graph_correct_1:
- forall f live live0 pc i,
- f.(fn_code)!pc = Some i ->
- correct_interf_instr live!!pc i (interf_graph f live live0).
-Proof.
- intros. unfold interf_graph.
- apply correct_interf_instr_incl with (add_edges_instrs f live).
- eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
- eapply graph_incl_trans; [idtac|apply add_interf_params_incl].
- apply add_interf_entry_incl.
- apply add_edges_instrs_correct; auto.
-Qed.
-
-(** Second, function parameters conflict pairwise. *)
-
-Lemma interf_graph_correct_2:
- forall f live live0 r1 r2,
- In r1 f.(fn_params) ->
- In r2 f.(fn_params) ->
- r1 <> r2 ->
- interfere r1 r2 (interf_graph f live live0).
-Proof.
- intros. unfold interf_graph.
- eapply interfere_incl.
- apply add_prefs_call_incl.
- apply add_interf_params_correct; auto.
-Qed.
-
-(** Third, function parameters conflict pairwise with pseudo-registers
- live at function entry. If the function never uses a pseudo-register
- before it is defined, pseudo-registers live at function entry
- are a subset of the function parameters and therefore this condition
- is implied by [interf_graph_correct_3]. However, we prefer not
- to make this assumption. *)
-
-Lemma interf_graph_correct_3:
- forall f live live0 r1 r2,
- In r1 f.(fn_params) ->
- Regset.In r2 live0 ->
- r1 <> r2 ->
- interfere r1 r2 (interf_graph f live live0).
-Proof.
- intros. unfold interf_graph.
- eapply interfere_incl.
- eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
- apply add_interf_params_incl.
- apply add_interf_entry_correct; auto.
-Qed.
-
-(** * Correctness of the a priori checks over the result of graph coloring *)
-
-(** We now show that the checks performed over the candidate coloring
- returned by [graph_coloring] are correct: candidate colorings that
- pass these checks are indeed correct colorings. *)
-
-Section CORRECT_COLORING.
-
-Variable g: graph.
-Variable env: regenv.
-Variable allregs: Regset.t.
-Variable coloring: reg -> loc.
-
-Lemma check_coloring_1_correct:
- forall r1 r2,
- check_coloring_1 g coloring = true ->
- SetRegReg.In (r1, r2) g.(interf_reg_reg) ->
- coloring r1 <> coloring r2.
-Proof.
- unfold check_coloring_1. intros.
- assert (compat_bool OrderedRegReg.eq
- (fun r1r2 => if Loc.eq (coloring (fst r1r2)) (coloring (snd r1r2))
- then false else true)).
- red. unfold OrderedRegReg.eq. unfold OrderedReg.eq.
- intros x y [EQ1 EQ2]. rewrite EQ1; rewrite EQ2; auto.
- generalize (SetRegReg.for_all_2 H1 H H0).
- simpl. case (Loc.eq (coloring r1) (coloring r2)); intro.
- intro; discriminate. auto.
-Qed.
-
-Lemma check_coloring_2_correct:
- forall r1 mr2,
- check_coloring_2 g coloring = true ->
- SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) ->
- coloring r1 <> R mr2.
-Proof.
- unfold check_coloring_2. intros.
- assert (compat_bool OrderedRegMreg.eq
- (fun r1r2 => if Loc.eq (coloring (fst r1r2)) (R (snd r1r2))
- then false else true)).
- red. unfold OrderedRegMreg.eq. unfold OrderedReg.eq.
- intros x y [EQ1 EQ2]. rewrite EQ1; rewrite EQ2; auto.
- generalize (SetRegMreg.for_all_2 H1 H H0).
- simpl. case (Loc.eq (coloring r1) (R mr2)); intro.
- intro; discriminate. auto.
-Qed.
-
-Lemma same_typ_correct:
- forall t1 t2, same_typ t1 t2 = true -> t1 = t2.
-Proof.
- destruct t1; destruct t2; simpl; congruence.
-Qed.
-
-Lemma loc_is_acceptable_correct:
- forall l, loc_is_acceptable l = true -> loc_acceptable l.
-Proof.
- destruct l; unfold loc_is_acceptable, loc_acceptable.
- case (In_dec Loc.eq (R m) temporaries); intro.
- intro; discriminate. auto.
- destruct s.
- case (zlt z 0); intro. intro; discriminate. auto.
- intro; discriminate.
- intro; discriminate.
-Qed.
-
-Lemma check_coloring_3_correct:
- forall r,
- check_coloring_3 allregs env coloring = true ->
- Regset.mem r allregs = true ->
- loc_acceptable (coloring r) /\ env r = Loc.type (coloring r).
-Proof.
- unfold check_coloring_3; intros.
- exploit Regset.for_all_2; eauto.
- red; intros. congruence.
- apply Regset.mem_2. eauto.
- simpl. intro. elim (andb_prop _ _ H1); intros.
- split. apply loc_is_acceptable_correct; auto.
- apply same_typ_correct; auto.
-Qed.
-
-End CORRECT_COLORING.
-
-(** * Correctness of clipping *)
-
-(** We then show the correctness of the ``clipped'' coloring
- returned by [alloc_of_coloring] applied to a candidate coloring
- that passes the a posteriori checks. *)
-
-Section ALLOC_OF_COLORING.
-
-Variable g: graph.
-Variable env: regenv.
-Let allregs := all_interf_regs g.
-Variable coloring: reg -> loc.
-Let alloc := alloc_of_coloring coloring env allregs.
-
-Lemma alloc_of_coloring_correct_1:
- forall r1 r2,
- check_coloring g env allregs coloring = true ->
- SetRegReg.In (r1, r2) g.(interf_reg_reg) ->
- alloc r1 <> alloc r2.
-Proof.
- unfold check_coloring, alloc, alloc_of_coloring; intros.
- elim (andb_prop _ _ H); intros.
- generalize (all_interf_regs_correct_1 _ _ _ H0).
- intros [A B].
- unfold allregs. rewrite Regset.mem_1; auto. rewrite Regset.mem_1; auto.
- eapply check_coloring_1_correct; eauto.
-Qed.
-
-Lemma alloc_of_coloring_correct_2:
- forall r1 mr2,
- check_coloring g env allregs coloring = true ->
- SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) ->
- alloc r1 <> R mr2.
-Proof.
- unfold check_coloring, alloc, alloc_of_coloring; intros.
- elim (andb_prop _ _ H); intros.
- elim (andb_prop _ _ H2); intros.
- generalize (all_interf_regs_correct_2 _ _ _ H0). intros.
- unfold allregs. rewrite Regset.mem_1; auto.
- eapply check_coloring_2_correct; eauto.
-Qed.
-
-Lemma alloc_of_coloring_correct_3:
- forall r,
- check_coloring g env allregs coloring = true ->
- loc_acceptable (alloc r).
-Proof.
- unfold check_coloring, alloc, alloc_of_coloring; intros.
- elim (andb_prop _ _ H); intros.
- elim (andb_prop _ _ H1); intros.
- caseEq (Regset.mem r allregs); intro.
- generalize (check_coloring_3_correct _ _ _ r H3 H4). tauto.
- case (env r); simpl.
- unfold dummy_int_reg. intuition congruence.
- unfold dummy_float_reg. intuition congruence.
-Qed.
-
-Lemma alloc_of_coloring_correct_4:
- forall r,
- check_coloring g env allregs coloring = true ->
- env r = Loc.type (alloc r).
-Proof.
- unfold check_coloring, alloc, alloc_of_coloring; intros.
- elim (andb_prop _ _ H); intros.
- elim (andb_prop _ _ H1); intros.
- caseEq (Regset.mem r allregs); intro.
- generalize (check_coloring_3_correct _ _ _ r H3 H4). tauto.
- case (env r); reflexivity.
-Qed.
-
-End ALLOC_OF_COLORING.
-
-(** * Correctness of the whole graph coloring algorithm *)
-
-(** Combining results from the previous sections, we now summarize
- the correctness properties of the assignment (of locations to
- registers) returned by [regalloc]. *)
-
-Definition correct_alloc_instr
- (live: PMap.t Regset.t) (alloc: reg -> loc)
- (pc: node) (instr: instruction) : Prop :=
- match instr with
- | Iop op args res s =>
- match is_move_operation op args with
- | Some arg =>
- forall r,
- Regset.In res live!!pc ->
- Regset.In r live!!pc ->
- r <> res -> r <> arg -> alloc r <> alloc res
- | None =>
- forall r,
- Regset.In res live!!pc ->
- Regset.In r live!!pc ->
- r <> res -> alloc r <> alloc res
- end
- | Iload chunk addr args res s =>
- forall r,
- Regset.In res live!!pc ->
- Regset.In r live!!pc ->
- r <> res -> alloc r <> alloc res
- | Icall sig ros args res s =>
- (forall r,
- Regset.In r live!!pc ->
- r <> res ->
- ~(In (alloc r) destroyed_at_call))
- /\ (forall r,
- Regset.In r live!!pc ->
- r <> res -> alloc r <> alloc res)
- /\ (match ros with
- | inl rfun => ~(In (alloc rfun) (loc_arguments sig))
- | inr idfun => True
- end)
- | Itailcall sig ros args =>
- (match ros with
- | inl rfun => ~(In (alloc rfun) (loc_arguments sig))
- | inr idfun => True
- end)
- | Ibuiltin ef args res s =>
- forall r,
- Regset.In r live!!pc ->
- r <> res -> alloc r <> alloc res
- | _ =>
- True
- end.
-
-Section REGALLOC_PROPERTIES.
-
-Variable f: function.
-Variable env: regenv.
-Variable live: PMap.t Regset.t.
-Variable live0: Regset.t.
-Variable alloc: reg -> loc.
-
-Let g := interf_graph f live live0.
-Let allregs := all_interf_regs g.
-Let coloring := graph_coloring f g env allregs.
-
-Lemma regalloc_ok:
- regalloc f live live0 env = Some alloc ->
- check_coloring g env allregs coloring = true /\
- alloc = alloc_of_coloring coloring env allregs.
-Proof.
- unfold regalloc, coloring, allregs, g.
- case (check_coloring (interf_graph f live live0) env).
- intro EQ; injection EQ; intro; clear EQ.
- split. auto. auto.
- intro; discriminate.
-Qed.
-
-Lemma regalloc_acceptable:
- forall r,
- regalloc f live live0 env = Some alloc ->
- loc_acceptable (alloc r).
-Proof.
- intros. elim (regalloc_ok H); intros.
- rewrite H1. unfold allregs. apply alloc_of_coloring_correct_3.
- exact H0.
-Qed.
-
-Lemma regsalloc_acceptable:
- forall rl,
- regalloc f live live0 env = Some alloc ->
- locs_acceptable (List.map alloc rl).
-Proof.
- intros; red; intros.
- elim (list_in_map_inv _ _ _ H0). intros r [EQ IN].
- subst l. apply regalloc_acceptable. auto.
-Qed.
-
-Lemma regalloc_preserves_types:
- forall r,
- regalloc f live live0 env = Some alloc ->
- Loc.type (alloc r) = env r.
-Proof.
- intros. elim (regalloc_ok H); intros.
- rewrite H1. unfold allregs. symmetry.
- apply alloc_of_coloring_correct_4.
- exact H0.
-Qed.
-
-Lemma correct_interf_alloc_instr:
- forall pc instr,
- (forall r1 r2, interfere r1 r2 g -> alloc r1 <> alloc r2) ->
- (forall r1 mr2, interfere_mreg r1 mr2 g -> alloc r1 <> R mr2) ->
- (forall r, loc_acceptable (alloc r)) ->
- correct_interf_instr live!!pc instr g ->
- correct_alloc_instr live alloc pc instr.
-Proof.
- intros pc instr ALL1 ALL2 ALL3.
- unfold correct_interf_instr, correct_alloc_instr;
- destruct instr; auto.
- destruct (is_move_operation o l); auto.
- (* Icall *)
- intros [A [B C]].
- split. intros; red; intros.
- unfold destroyed_at_call in H1.
- generalize (list_in_map_inv R _ _ H1).
- intros [mr [EQ IN]].
- generalize (A r0 mr H IN H0). intro.
- generalize (ALL2 _ _ H2). contradiction.
- split. auto.
- destruct s0; auto. red; intros.
- generalize (ALL3 r0). generalize (loc_arguments_acceptable _ _ H).
- unfold loc_argument_acceptable, loc_acceptable.
- caseEq (alloc r0). intros.
- elim (ALL2 r0 m). apply C; auto. congruence. auto.
- destruct s0; auto.
- (* Itailcall *)
- destruct s0; auto. red; intros.
- generalize (ALL3 r). generalize (loc_arguments_acceptable _ _ H0).
- unfold loc_argument_acceptable, loc_acceptable.
- caseEq (alloc r). intros.
- elim (ALL2 r m). apply H; auto. congruence. auto.
- destruct s0; auto.
-Qed.
-
-Lemma regalloc_correct_1:
- forall pc instr,
- regalloc f live live0 env = Some alloc ->
- f.(fn_code)!pc = Some instr ->
- correct_alloc_instr live alloc pc instr.
-Proof.
- intros. elim (regalloc_ok H); intros.
- apply correct_interf_alloc_instr.
- intros. rewrite H2. unfold allregs. red in H3.
- elim (ordered_pair_charact r1 r2); intro.
- apply alloc_of_coloring_correct_1. auto. rewrite H4 in H3; auto.
- apply sym_not_equal.
- apply alloc_of_coloring_correct_1. auto. rewrite H4 in H3; auto.
- intros. rewrite H2. unfold allregs.
- apply alloc_of_coloring_correct_2. auto. exact H3.
- intros. eapply regalloc_acceptable; eauto.
- unfold g. apply interf_graph_correct_1. auto.
-Qed.
-
-Lemma regalloc_correct_2:
- regalloc f live live0 env = Some alloc ->
- list_norepet f.(fn_params) ->
- list_norepet (List.map alloc f.(fn_params)).
-Proof.
- intros. elim (regalloc_ok H); intros.
- apply list_map_norepet; auto.
- intros. rewrite H2. unfold allregs.
- elim (ordered_pair_charact x y); intro.
- apply alloc_of_coloring_correct_1. auto.
- change positive with reg. rewrite <- H6.
- change (interfere x y g). unfold g.
- apply interf_graph_correct_2; auto.
- apply sym_not_equal.
- apply alloc_of_coloring_correct_1. auto.
- change positive with reg. rewrite <- H6.
- change (interfere x y g). unfold g.
- apply interf_graph_correct_2; auto.
-Qed.
-
-Lemma regalloc_correct_3:
- forall r1 r2,
- regalloc f live live0 env = Some alloc ->
- In r1 f.(fn_params) ->
- Regset.In r2 live0 ->
- r1 <> r2 ->
- alloc r1 <> alloc r2.
-Proof.
- intros. elim (regalloc_ok H); intros.
- rewrite H4; unfold allregs.
- elim (ordered_pair_charact r1 r2); intro.
- apply alloc_of_coloring_correct_1. auto.
- change positive with reg. rewrite <- H5.
- change (interfere r1 r2 g). unfold g.
- apply interf_graph_correct_3; auto.
- apply sym_not_equal.
- apply alloc_of_coloring_correct_1. auto.
- change positive with reg. rewrite <- H5.
- change (interfere r1 r2 g). unfold g.
- apply interf_graph_correct_3; auto.
-Qed.
-
-End REGALLOC_PROPERTIES.
diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v
deleted file mode 100644
index 877c7c6..0000000
--- a/backend/InterfGraph.v
+++ /dev/null
@@ -1,302 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-(** Representation of interference graphs for register allocation. *)
-
-Require Import Coqlib.
-Require Import FSets.
-Require Import FSetAVL.
-Require Import Ordered.
-Require Import Registers.
-Require Import Locations.
-
-(** Interference graphs are undirected graphs with two kinds of nodes:
-- RTL pseudo-registers;
-- Machine registers.
-
-and four kind of edges:
-- Conflict edges between two pseudo-registers.
- (Meaning: these two pseudo-registers must not be assigned the same
- location.)
-- Conflict edges between a pseudo-register and a machine register
- (Meaning: this pseudo-register must not be assigned this machine
- register.)
-- Preference edges between two pseudo-registers.
- (Meaning: the generated code would be more efficient if those two
- pseudo-registers were assigned the same location, but if this is not
- possible, the generated code will still be correct.)
-- Preference edges between a pseudo-register and a machine register
- (Meaning: the generated code would be more efficient if this
- pseudo-register was assigned this machine register, but if this is not
- possible, the generated code will still be correct.)
-
-A graph is represented by four finite sets of edges (one of each kind
-above). An edge is represented by a pair of two pseudo-registers or
-a pair (pseudo-register, machine register).
-In the case of two pseudo-registers ([r1], [r2]), we adopt the convention
-that [r1] <= [r2], so as to reflect the undirected nature of the edge.
-*)
-
-Module OrderedReg <: OrderedType with Definition t := reg := OrderedPositive.
-Module OrderedRegReg := OrderedPair(OrderedReg)(OrderedReg).
-Module OrderedMreg := OrderedIndexed(IndexedMreg).
-Module OrderedRegMreg := OrderedPair(OrderedReg)(OrderedMreg).
-
-Module SetRegReg := FSetAVL.Make(OrderedRegReg).
-Module SetRegMreg := FSetAVL.Make(OrderedRegMreg).
-
-Record graph: Type := mkgraph {
- interf_reg_reg: SetRegReg.t;
- interf_reg_mreg: SetRegMreg.t;
- pref_reg_reg: SetRegReg.t;
- pref_reg_mreg: SetRegMreg.t
-}.
-
-Definition empty_graph :=
- mkgraph SetRegReg.empty SetRegMreg.empty
- SetRegReg.empty SetRegMreg.empty.
-
-(** The following functions add a new edge (if not already present)
- to the given graph. *)
-
-Definition ordered_pair (x y: reg) :=
- if plt x y then (x, y) else (y, x).
-
-Definition add_interf (x y: reg) (g: graph) :=
- mkgraph (SetRegReg.add (ordered_pair x y) g.(interf_reg_reg))
- g.(interf_reg_mreg)
- g.(pref_reg_reg)
- g.(pref_reg_mreg).
-
-Definition add_interf_mreg (x: reg) (y: mreg) (g: graph) :=
- mkgraph g.(interf_reg_reg)
- (SetRegMreg.add (x, y) g.(interf_reg_mreg))
- g.(pref_reg_reg)
- g.(pref_reg_mreg).
-
-Definition add_pref (x y: reg) (g: graph) :=
- mkgraph g.(interf_reg_reg)
- g.(interf_reg_mreg)
- (SetRegReg.add (ordered_pair x y) g.(pref_reg_reg))
- g.(pref_reg_mreg).
-
-Definition add_pref_mreg (x: reg) (y: mreg) (g: graph) :=
- mkgraph g.(interf_reg_reg)
- g.(interf_reg_mreg)
- g.(pref_reg_reg)
- (SetRegMreg.add (x, y) g.(pref_reg_mreg)).
-
-(** [interfere x y g] holds iff there is a conflict edge in [g]
- between the two pseudo-registers [x] and [y]. *)
-
-Definition interfere (x y: reg) (g: graph) : Prop :=
- SetRegReg.In (ordered_pair x y) g.(interf_reg_reg).
-
-(** [interfere_mreg x y g] holds iff there is a conflict edge in [g]
- between the pseudo-register [x] and the machine register [y]. *)
-
-Definition interfere_mreg (x: reg) (y: mreg) (g: graph) : Prop :=
- SetRegMreg.In (x, y) g.(interf_reg_mreg).
-
-Lemma ordered_pair_charact:
- forall x y,
- ordered_pair x y = (x, y) \/ ordered_pair x y = (y, x).
-Proof.
- unfold ordered_pair; intros.
- case (plt x y); intro; tauto.
-Qed.
-
-Lemma ordered_pair_sym:
- forall x y, ordered_pair y x = ordered_pair x y.
-Proof.
- unfold ordered_pair; intros.
- destruct (plt y x); destruct (plt x y).
- elim (Plt_strict x). eapply Plt_trans; eauto.
- auto.
- auto.
- destruct (Pos.lt_total x y) as [A | [A | A]].
- elim n0; auto.
- congruence.
- elim n; auto.
-Qed.
-
-Lemma interfere_sym:
- forall x y g, interfere x y g -> interfere y x g.
-Proof.
- unfold interfere; intros.
- rewrite ordered_pair_sym. auto.
-Qed.
-
-(** [graph_incl g1 g2] holds if [g2] contains all the conflict edges of [g1]
- and possibly more. *)
-
-Definition graph_incl (g1 g2: graph) : Prop :=
- (forall x y, interfere x y g1 -> interfere x y g2) /\
- (forall x y, interfere_mreg x y g1 -> interfere_mreg x y g2).
-
-Lemma graph_incl_trans:
- forall g1 g2 g3, graph_incl g1 g2 -> graph_incl g2 g3 -> graph_incl g1 g3.
-Proof.
- unfold graph_incl; intros.
- elim H0; elim H; intros.
- split; eauto.
-Qed.
-
-(** We show that the [add_] functions correctly record the desired
- conflicts, and preserve whatever conflict edges were already present. *)
-
-Lemma add_interf_correct:
- forall x y g,
- interfere x y (add_interf x y g).
-Proof.
- intros. unfold interfere, add_interf; simpl.
- apply SetRegReg.add_1. auto.
-Qed.
-
-Lemma add_interf_incl:
- forall a b g, graph_incl g (add_interf a b g).
-Proof.
- intros. split; intros.
- unfold add_interf, interfere; simpl.
- apply SetRegReg.add_2. exact H.
- exact H.
-Qed.
-
-Lemma add_interf_mreg_correct:
- forall x y g,
- interfere_mreg x y (add_interf_mreg x y g).
-Proof.
- intros. unfold interfere_mreg, add_interf_mreg; simpl.
- apply SetRegMreg.add_1. auto.
-Qed.
-
-Lemma add_interf_mreg_incl:
- forall a b g, graph_incl g (add_interf_mreg a b g).
-Proof.
- intros. split; intros.
- exact H.
- unfold add_interf_mreg, interfere_mreg; simpl.
- apply SetRegMreg.add_2. exact H.
-Qed.
-
-Lemma add_pref_incl:
- forall a b g, graph_incl g (add_pref a b g).
-Proof.
- intros. split; intros.
- exact H.
- exact H.
-Qed.
-
-Lemma add_pref_mreg_incl:
- forall a b g, graph_incl g (add_pref_mreg a b g).
-Proof.
- intros. split; intros.
- exact H.
- exact H.
-Qed.
-
-(** [all_interf_regs g] returns the set of pseudo-registers that
- are nodes of [g]. *)
-
-Definition add_intf2 (r1r2: reg * reg) (u: Regset.t) : Regset.t :=
- Regset.add (fst r1r2) (Regset.add (snd r1r2) u).
-Definition add_intf1 (r1m2: reg * mreg) (u: Regset.t) : Regset.t :=
- Regset.add (fst r1m2) u.
-
-Definition all_interf_regs (g: graph) : Regset.t :=
- let s1 := SetRegMreg.fold add_intf1 g.(interf_reg_mreg) Regset.empty in
- let s2 := SetRegMreg.fold add_intf1 g.(pref_reg_mreg) s1 in
- let s3 := SetRegReg.fold add_intf2 g.(interf_reg_reg) s2 in
- SetRegReg.fold add_intf2 g.(pref_reg_reg) s3.
-
-Lemma in_setregreg_fold:
- forall g r1 r2 u,
- SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u ->
- Regset.In r1 (SetRegReg.fold add_intf2 g u) /\
- Regset.In r2 (SetRegReg.fold add_intf2 g u).
-Proof.
- set (add_intf2' := fun u r1r2 => add_intf2 r1r2 u).
- assert (forall l r1 r2 u,
- InA OrderedRegReg.eq (r1,r2) l \/ Regset.In r1 u /\ Regset.In r2 u ->
- Regset.In r1 (List.fold_left add_intf2' l u) /\
- Regset.In r2 (List.fold_left add_intf2' l u)).
- induction l; intros; simpl.
- elim H; intro. inversion H0. auto.
- apply IHl. destruct a as [a1 a2].
- elim H; intro. inversion H0; subst.
- red in H2. simpl in H2. destruct H2. subst r1 r2.
- right; unfold add_intf2', add_intf2; simpl; split.
- apply Regset.add_1. auto.
- apply Regset.add_2. apply Regset.add_1. auto.
- tauto.
- right; unfold add_intf2', add_intf2; simpl; split;
- apply Regset.add_2; apply Regset.add_2; tauto.
-
- intros. rewrite SetRegReg.fold_1. apply H.
- intuition.
-Qed.
-
-Lemma in_setregreg_fold':
- forall g r u,
- Regset.In r u ->
- Regset.In r (SetRegReg.fold add_intf2 g u).
-Proof.
- intros. exploit in_setregreg_fold. eauto.
- intros [A B]. eauto.
-Qed.
-
-Lemma in_setregmreg_fold:
- forall g r1 mr2 u,
- SetRegMreg.In (r1, mr2) g \/ Regset.In r1 u ->
- Regset.In r1 (SetRegMreg.fold add_intf1 g u).
-Proof.
- set (add_intf1' := fun u r1mr2 => add_intf1 r1mr2 u).
- assert (forall l r1 mr2 u,
- InA OrderedRegMreg.eq (r1,mr2) l \/ Regset.In r1 u ->
- Regset.In r1 (List.fold_left add_intf1' l u)).
- induction l; intros; simpl.
- elim H; intro. inversion H0. auto.
- apply IHl with mr2. destruct a as [a1 a2].
- elim H; intro. inversion H0; subst.
- red in H2. simpl in H2. destruct H2. subst r1 mr2.
- right; unfold add_intf1', add_intf1; simpl.
- apply Regset.add_1; auto.
- tauto.
- right; unfold add_intf1', add_intf1; simpl.
- apply Regset.add_2; auto.
-
- intros. rewrite SetRegMreg.fold_1. apply H with mr2.
- intuition.
-Qed.
-
-Lemma all_interf_regs_correct_1:
- forall r1 r2 g,
- SetRegReg.In (r1, r2) g.(interf_reg_reg) ->
- Regset.In r1 (all_interf_regs g) /\
- Regset.In r2 (all_interf_regs g).
-Proof.
- intros. unfold all_interf_regs.
- apply in_setregreg_fold. right.
- apply in_setregreg_fold. tauto.
-Qed.
-
-Lemma all_interf_regs_correct_2:
- forall r1 mr2 g,
- SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) ->
- Regset.In r1 (all_interf_regs g).
-Proof.
- intros. unfold all_interf_regs.
- apply in_setregreg_fold'. apply in_setregreg_fold'.
- apply in_setregmreg_fold with mr2. right.
- apply in_setregmreg_fold with mr2. eauto.
-Qed.
-
diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v
deleted file mode 100644
index 4930ccd..0000000
--- a/backend/Parallelmove.v
+++ /dev/null
@@ -1,365 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-(** Translation of parallel moves into sequences of individual moves.
-
- In this file, we adapt the generic "parallel move" algorithm
- (developed and proved correct in module [Parmov]) to the idiosyncraties
- of the [LTLin] and [Linear] intermediate languages. While the generic
- algorithm assumes that registers never overlap, the locations
- used in [LTLin] and [Linear] can overlap, and assigning one location
- can set the values of other, overlapping locations to [Vundef].
- We address this issue in the remainder of this file.
-*)
-
-Require Import Coqlib.
-Require Parmov.
-Require Import Values.
-Require Import AST.
-Require Import Locations.
-Require Import Conventions.
-
-(** * Instantiating the generic parallel move algorithm *)
-
-(** The temporary location to use for a move is determined
- by the type of the data being moved: register [IT2] for an
- integer datum, and register [FT2] for a floating-point datum. *)
-
-Definition temp_for (l: loc) : loc :=
- match Loc.type l with Tint => R IT2 | Tfloat => R FT2 end.
-
-Definition parmove (srcs dsts: list loc) :=
- Parmov.parmove2 loc Loc.eq temp_for srcs dsts.
-
-Definition moves := (list (loc * loc))%type.
-
-(** [exec_seq m] gives semantics to a sequence of elementary moves.
- This semantics ignores the possibility of overlap: only the
- target locations are updated, but the locations they
- overlap with are not set to [Vundef]. See [effect_seqmove] below
- for a semantics that accounts for overlaps. *)
-
-Definition exec_seq (m: moves) (e: Locmap.t) : Locmap.t :=
- Parmov.exec_seq loc Loc.eq val m e.
-
-Lemma temp_for_charact:
- forall l, temp_for l = R IT2 \/ temp_for l = R FT2.
-Proof.
- intro; unfold temp_for. destruct (Loc.type l); tauto.
-Qed.
-
-Lemma is_not_temp_charact:
- forall l,
- Parmov.is_not_temp loc temp_for l <-> l <> R IT2 /\ l <> R FT2.
-Proof.
- intros. unfold Parmov.is_not_temp.
- destruct (Loc.eq l (R IT2)).
- subst l. intuition. apply (H (R IT2)). reflexivity. discriminate.
- destruct (Loc.eq l (R FT2)).
- subst l. intuition. apply (H (R FT2)). reflexivity.
- assert (forall d, l <> temp_for d).
- intro. elim (temp_for_charact d); congruence.
- intuition.
-Qed.
-
-Lemma disjoint_temp_not_temp:
- forall l, Loc.notin l temporaries -> Parmov.is_not_temp loc temp_for l.
-Proof.
- intros. rewrite is_not_temp_charact.
- unfold temporaries in H; simpl in H.
- split; apply Loc.diff_not_eq; tauto.
-Qed.
-
-Lemma loc_norepet_norepet:
- forall l, Loc.norepet l -> list_norepet l.
-Proof.
- induction 1; constructor.
- apply Loc.notin_not_in; auto. auto.
-Qed.
-
-(** Instantiating the theorems proved in [Parmov], we obtain
- the following properties of semantic correctness and well-typedness
- of the generated sequence of moves. Note that the semantic
- correctness result is stated in terms of the [exec_seq] semantics,
- and therefore does not account for overlap between locations. *)
-
-Lemma parmove_prop_1:
- forall srcs dsts,
- List.length srcs = List.length dsts ->
- Loc.norepet dsts ->
- Loc.disjoint srcs temporaries ->
- Loc.disjoint dsts temporaries ->
- forall e,
- let e' := exec_seq (parmove srcs dsts) e in
- List.map e' dsts = List.map e srcs /\
- forall l, ~In l dsts -> l <> R IT2 -> l <> R FT2 -> e' l = e l.
-Proof.
- intros.
- assert (NR: list_norepet dsts) by (apply loc_norepet_norepet; auto).
- assert (NTS: forall r, In r srcs -> Parmov.is_not_temp loc temp_for r).
- intros. apply disjoint_temp_not_temp. apply Loc.disjoint_notin with srcs; auto.
- assert (NTD: forall r, In r dsts -> Parmov.is_not_temp loc temp_for r).
- intros. apply disjoint_temp_not_temp. apply Loc.disjoint_notin with dsts; auto.
- generalize (Parmov.parmove2_correctness loc Loc.eq temp_for val srcs dsts H NR NTS NTD e).
- change (Parmov.exec_seq loc Loc.eq val (Parmov.parmove2 loc Loc.eq temp_for srcs dsts) e) with e'.
- intros [A B].
- split. auto. intros. apply B. auto. rewrite is_not_temp_charact; auto.
-Qed.
-
-Lemma parmove_prop_2:
- forall srcs dsts s d,
- In (s, d) (parmove srcs dsts) ->
- (In s srcs \/ s = R IT2 \/ s = R FT2)
- /\ (In d dsts \/ d = R IT2 \/ d = R FT2).
-Proof.
- intros srcs dsts.
- set (mu := List.combine srcs dsts).
- assert (forall s d, Parmov.wf_move loc temp_for mu s d ->
- (In s srcs \/ s = R IT2 \/ s = R FT2)
- /\ (In d dsts \/ d = R IT2 \/ d = R FT2)).
- unfold mu; induction 1.
- split.
- left. eapply List.in_combine_l; eauto.
- left. eapply List.in_combine_r; eauto.
- split.
- right. apply temp_for_charact.
- tauto.
- split.
- tauto.
- right. apply temp_for_charact.
- intros. apply H.
- apply (Parmov.parmove2_wf_moves loc Loc.eq temp_for srcs dsts s d H0).
-Qed.
-
-Lemma loc_type_temp_for:
- forall l, Loc.type (temp_for l) = Loc.type l.
-Proof.
- intros; unfold temp_for. destruct (Loc.type l); reflexivity.
-Qed.
-
-Lemma loc_type_combine:
- forall srcs dsts,
- List.map Loc.type srcs = List.map Loc.type dsts ->
- forall s d,
- In (s, d) (List.combine srcs dsts) ->
- Loc.type s = Loc.type d.
-Proof.
- induction srcs; destruct dsts; simpl; intros; try discriminate.
- elim H0.
- elim H0; intros. inversion H1; subst. congruence.
- apply IHsrcs with dsts. congruence. auto.
-Qed.
-
-Lemma parmove_prop_3:
- forall srcs dsts,
- List.map Loc.type srcs = List.map Loc.type dsts ->
- forall s d,
- In (s, d) (parmove srcs dsts) -> Loc.type s = Loc.type d.
-Proof.
- intros srcs dsts TYP.
- set (mu := List.combine srcs dsts).
- assert (forall s d, Parmov.wf_move loc temp_for mu s d ->
- Loc.type s = Loc.type d).
- unfold mu; induction 1.
- eapply loc_type_combine; eauto.
- rewrite loc_type_temp_for; auto.
- rewrite loc_type_temp_for; auto.
- intros. apply H.
- apply (Parmov.parmove2_wf_moves loc Loc.eq temp_for srcs dsts s d H0).
-Qed.
-
-(** * Accounting for overlap between locations *)
-
-Section EQUIVALENCE.
-
-(** We now prove the correctness of the generated sequence of elementary
- moves, accounting for possible overlap between locations.
- The proof is conducted under the following hypotheses: there must
- be no partial overlap between
-- two distinct destinations (hypothesis [NOREPET]);
-- a source location and a destination location (hypothesis [NO_OVERLAP]).
-*)
-
-Variables srcs dsts: list loc.
-Hypothesis LENGTH: List.length srcs = List.length dsts.
-Hypothesis NOREPET: Loc.norepet dsts.
-Hypothesis NO_OVERLAP: Loc.no_overlap srcs dsts.
-Hypothesis NO_SRCS_TEMP: Loc.disjoint srcs temporaries.
-Hypothesis NO_DSTS_TEMP: Loc.disjoint dsts temporaries.
-
-(** [no_overlap_dests l] holds if location [l] does not partially overlap
- a destination location: either it is identical to one of the
- destinations, or it is disjoint from all destinations. *)
-
-Definition no_overlap_dests (l: loc) : Prop :=
- forall d, In d dsts -> l = d \/ Loc.diff l d.
-
-(** We show that [no_overlap_dests] holds for any destination location
- and for any source location. *)
-
-Lemma dests_no_overlap_dests:
- forall l, In l dsts -> no_overlap_dests l.
-Proof.
- assert (forall d, Loc.norepet d ->
- forall l1 l2, In l1 d -> In l2 d -> l1 = l2 \/ Loc.diff l1 l2).
- induction 1; simpl; intros.
- contradiction.
- elim H1; intro; elim H2; intro.
- left; congruence.
- right. subst l1. eapply Loc.in_notin_diff; eauto.
- right. subst l2. apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto.
- eauto.
- intros; red; intros. eauto.
-Qed.
-
-Lemma notin_dests_no_overlap_dests:
- forall l, Loc.notin l dsts -> no_overlap_dests l.
-Proof.
- intros; red; intros.
- right. eapply Loc.in_notin_diff; eauto.
-Qed.
-
-Lemma source_no_overlap_dests:
- forall s, In s srcs \/ s = R IT2 \/ s = R FT2 -> no_overlap_dests s.
-Proof.
- intros. elim H; intro. exact (NO_OVERLAP s H0).
- elim H0; intro; subst s; red; intros;
- right; apply Loc.diff_sym; apply NO_DSTS_TEMP; auto; simpl; tauto.
-Qed.
-
-Lemma source_not_temp1:
- forall s, In s srcs \/ s = R IT2 \/ s = R FT2 ->
- Loc.diff s (R IT1) /\ Loc.diff s (R FT1) /\ Loc.notin s destroyed_at_move.
-Proof.
- intros. destruct H.
- exploit Loc.disjoint_notin. eexact NO_SRCS_TEMP. eauto.
- simpl; tauto.
- destruct H; subst s; simpl; intuition congruence.
-Qed.
-
-Lemma dest_noteq_diff:
- forall d l,
- In d dsts \/ d = R IT2 \/ d = R FT2 ->
- l <> d ->
- no_overlap_dests l ->
- Loc.diff l d.
-Proof.
- intros. elim H; intro.
- elim (H1 d H2); intro. congruence. auto.
- assert (forall r, l <> R r -> Loc.diff l (R r)).
- intros. destruct l; simpl. congruence. destruct s; auto.
- elim H2; intro; subst d; auto.
-Qed.
-
-(** [locmap_equiv e1 e2] holds if the location maps [e1] and [e2]
- assign the same values to all locations except temporaries [IT1], [FT1]
- and except locations that partially overlap a destination. *)
-
-Definition locmap_equiv (e1 e2: Locmap.t): Prop :=
- forall l,
- no_overlap_dests l -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> Loc.notin l destroyed_at_move -> e2 l = e1 l.
-
-(** The following predicates characterize the effect of one move
- move ([effect_move]) and of a sequence of elementary moves
- ([effect_seqmove]). We allow the code generated for one move
- to use the temporaries [IT1] and [FT1] and [destroyed_at_move] in any way it needs. *)
-
-Definition effect_move (src dst: loc) (e e': Locmap.t): Prop :=
- e' dst = e src /\
- forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> Loc.notin l destroyed_at_move -> e' l = e l.
-
-Inductive effect_seqmove: list (loc * loc) -> Locmap.t -> Locmap.t -> Prop :=
- | effect_seqmove_nil: forall e,
- effect_seqmove nil e e
- | effect_seqmove_cons: forall s d m e1 e2 e3,
- effect_move s d e1 e2 ->
- effect_seqmove m e2 e3 ->
- effect_seqmove ((s, d) :: m) e1 e3.
-
-(** The following crucial lemma shows that [locmap_equiv] is preserved
- by executing one move [d <- s], once using the [effect_move]
- predicate that accounts for partial overlap and the use of
- temporaries [IT1], [FT1], or via the [Parmov.update] function that
- does not account for any of these. *)
-
-Lemma effect_move_equiv:
- forall s d e1 e2 e1',
- (In s srcs \/ s = R IT2 \/ s = R FT2) ->
- (In d dsts \/ d = R IT2 \/ d = R FT2) ->
- locmap_equiv e1 e2 -> effect_move s d e1 e1' ->
- locmap_equiv e1' (Parmov.update loc Loc.eq val d (e2 s) e2).
-Proof.
- intros. destruct H2. red; intros.
- unfold Parmov.update. destruct (Loc.eq l d).
- subst l. destruct (source_not_temp1 _ H) as [A [B C]].
- rewrite H2. apply H1; auto. apply source_no_overlap_dests; auto.
- rewrite H3; auto. apply dest_noteq_diff; auto.
-Qed.
-
-(** We then extend the previous lemma to a sequence [mu] of elementary moves.
-*)
-
-Lemma effect_seqmove_equiv:
- forall mu e1 e1',
- effect_seqmove mu e1 e1' ->
- forall e2,
- (forall s d, In (s, d) mu ->
- (In s srcs \/ s = R IT2 \/ s = R FT2) /\
- (In d dsts \/ d = R IT2 \/ d = R FT2)) ->
- locmap_equiv e1 e2 ->
- locmap_equiv e1' (exec_seq mu e2).
-Proof.
- induction 1; intros.
- simpl. auto.
- simpl. apply IHeffect_seqmove.
- intros. apply H1. apply in_cons; auto.
- destruct (H1 s d (in_eq _ _)).
- eapply effect_move_equiv; eauto.
-Qed.
-
-(** Here is the main result in this file: executing the sequence
- of moves returned by the [parmove] function results in the
- desired state for locations: the final values of destination locations
- are the initial values of source locations, and all locations
- that are disjoint from the temporaries and the destinations
- keep their initial values. *)
-
-Lemma effect_parmove:
- forall e e',
- effect_seqmove (parmove srcs dsts) e e' ->
- List.map e' dsts = List.map e srcs /\
- forall l, Loc.notin l dsts -> Loc.notin l temporaries -> e' l = e l.
-Proof.
- set (mu := parmove srcs dsts). intros.
- assert (locmap_equiv e e) by (red; auto).
- generalize (effect_seqmove_equiv mu e e' H e (parmove_prop_2 srcs dsts) H0).
- intro.
- generalize (parmove_prop_1 srcs dsts LENGTH NOREPET NO_SRCS_TEMP NO_DSTS_TEMP e).
- fold mu. intros [A B].
- (* e' dsts = e srcs *)
- split. rewrite <- A. apply list_map_exten; intros.
- exploit Loc.disjoint_notin. eexact NO_DSTS_TEMP. eauto. simpl; intros.
- apply H1. apply dests_no_overlap_dests; auto.
- tauto. tauto. simpl; tauto.
- (* other locations *)
- intros. transitivity (exec_seq mu e l).
- symmetry. apply H1. apply notin_dests_no_overlap_dests; auto.
- eapply Loc.in_notin_diff; eauto. simpl; tauto.
- eapply Loc.in_notin_diff; eauto. simpl; tauto.
- simpl in H3; simpl; tauto.
- apply B. apply Loc.notin_not_in; auto.
- apply Loc.diff_not_eq. eapply Loc.in_notin_diff; eauto. simpl; tauto.
- apply Loc.diff_not_eq. eapply Loc.in_notin_diff; eauto. simpl; tauto.
-Qed.
-
-End EQUIVALENCE.
-