diff options
| -rw-r--r-- | backend/Coloring.v | 309 | ||||
| -rw-r--r-- | backend/Coloringaux.ml | 867 | ||||
| -rw-r--r-- | backend/Coloringaux.mli | 22 | ||||
| -rw-r--r-- | backend/Coloringproof.v | 957 | ||||
| -rw-r--r-- | backend/InterfGraph.v | 302 | ||||
| -rw-r--r-- | backend/Parallelmove.v | 365 |
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. - |