From 707b6a1ae9660b13cf6f68c7c0ce74017f5981c5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 16 Mar 2013 16:51:42 +0000 Subject: Assorted changes to reduce stack and heap requirements when compiling very big functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Allocation.v | 98 +--------------------------- backend/Allocproof.v | 10 +-- backend/Alloctyping.v | 1 + backend/Asmgenproof0.v | 22 +++++++ backend/CleanupLabels.v | 18 +++--- backend/CleanupLabelsproof.v | 19 +++++- backend/CleanupLabelstyping.v | 4 +- backend/Coloringaux.ml | 9 ++- backend/Constprop.v | 16 ++++- backend/Constpropproof.v | 33 +++++++--- backend/Linearize.v | 16 ++--- backend/Linearizeproof.v | 26 ++++++-- backend/Linearizetyping.v | 4 +- backend/Liveness.v | 147 ++++++++++++++++++++++++++++++++++++++++++ backend/PrintCminor.ml | 2 +- backend/PrintRTL.ml | 2 +- backend/RRE.v | 46 +++++++------ backend/RREproof.v | 84 ++++++++++++++++-------- backend/RREtyping.v | 5 +- backend/Reload.v | 2 +- backend/Reloadproof.v | 9 ++- backend/Reloadtyping.v | 1 + backend/Stacking.v | 2 +- backend/Stackingproof.v | 20 +++--- 24 files changed, 389 insertions(+), 207 deletions(-) create mode 100644 backend/Liveness.v (limited to 'backend') diff --git a/backend/Allocation.v b/backend/Allocation.v index 4a4c2198..caaf09da 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -21,107 +21,13 @@ Require Import Op. Require Import Registers. Require Import RTL. Require Import RTLtyping. -Require Import Kildall. +Require Import Liveness. Require Import Locations. +Require Import LTL. Require Import Coloring. -(** * Liveness analysis over RTL *) - -(** A register [r] is live at a point [p] if there exists a path - from [p] to some instruction that uses [r] as argument, - and [r] is not redefined along this path. - Liveness can be computed by a backward dataflow analysis. - The analysis operates over sets of (live) pseudo-registers. *) - -Notation reg_live := Regset.add. -Notation reg_dead := Regset.remove. - -Definition reg_option_live (or: option reg) (lv: Regset.t) := - match or with None => lv | Some r => reg_live r lv end. - -Definition reg_sum_live (ros: reg + ident) (lv: Regset.t) := - match ros with inl r => reg_live r lv | inr s => lv end. - -Fixpoint reg_list_live - (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t := - match rl with - | nil => lv - | r1 :: rs => reg_list_live rs (reg_live r1 lv) - end. - -Fixpoint reg_list_dead - (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t := - match rl with - | nil => lv - | r1 :: rs => reg_list_dead rs (reg_dead r1 lv) - end. - -(** Here is the transfer function for the dataflow analysis. - Since this is a backward dataflow analysis, it takes as argument - the abstract register set ``after'' the given instruction, - i.e. the registers that are live after; and it returns as result - the abstract register set ``before'' the given instruction, - i.e. the registers that must be live before. - The general relation between ``live before'' and ``live after'' - an instruction is that a register is live before if either - it is one of the arguments of the instruction, or it is not the result - of the instruction and it is live after. - However, if the result of a side-effect-free instruction is not - live ``after'', the whole instruction will be removed later - (since it computes a useless result), thus its arguments need not - be live ``before''. *) - -Definition transfer - (f: RTL.function) (pc: node) (after: Regset.t) : Regset.t := - match f.(fn_code)!pc with - | None => - Regset.empty - | Some i => - match i with - | Inop s => - after - | Iop op args res s => - if Regset.mem res after then - reg_list_live args (reg_dead res after) - else - after - | Iload chunk addr args dst s => - if Regset.mem dst after then - reg_list_live args (reg_dead dst after) - else - after - | Istore chunk addr args src s => - reg_list_live args (reg_live src after) - | Icall sig ros args res s => - reg_list_live args - (reg_sum_live ros (reg_dead res after)) - | Itailcall sig ros args => - reg_list_live args (reg_sum_live ros Regset.empty) - | Ibuiltin ef args res s => - reg_list_live args (reg_dead res after) - | Icond cond args ifso ifnot => - reg_list_live args after - | Ijumptable arg tbl => - reg_live arg after - | Ireturn optarg => - reg_option_live optarg Regset.empty - end - end. - -(** The liveness analysis is then obtained by instantiating the - general framework for backward dataflow analysis provided by - module [Kildall]. *) - -Module RegsetLat := LFSet(Regset). -Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward). - -Definition analyze (f: RTL.function): option (PMap.t Regset.t) := - DS.fixpoint (successors f) (transfer f) nil. - (** * Translation from RTL to LTL *) -Require Import LTL. - (** Each [RTL] instruction translates to an [LTL] instruction. The register assignment [assign] returned by register allocation is applied to the arguments and results of the RTL diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 20114852..8dfa2d46 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -28,7 +28,9 @@ Require Import Op. Require Import Registers. Require Import RTL. Require Import RTLtyping. +Require Import Liveness. Require Import Locations. +Require Import LTL. Require Import Conventions. Require Import Coloring. Require Import Coloringproof. @@ -42,7 +44,7 @@ Require Import Allocation. Section REGALLOC_PROPERTIES. -Variable f: function. +Variable f: RTL.function. Variable env: regenv. Variable live: PMap.t Regset.t. Variable alloc: reg -> loc. @@ -145,7 +147,7 @@ Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop := Lemma agree_increasing: forall live1 live2 rs ls, - RegsetLat.ge live1 live2 -> agree live1 rs ls -> + Regset.Subset live2 live1 -> agree live1 rs ls -> agree live2 rs ls. Proof. unfold agree; intros. @@ -162,9 +164,7 @@ Lemma agree_succ: Proof. intros. apply agree_increasing with (live!!n). - eapply DS.fixpoint_solution. unfold analyze in H; eauto. - unfold RTL.successors, Kildall.successors_list. - rewrite PTree.gmap1. rewrite H0. simpl. auto. + eapply Liveness.analyze_solution; eauto. auto. Qed. diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index a6536831..59bf621b 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -19,6 +19,7 @@ Require Import AST. Require Import Op. Require Import Registers. Require Import RTL. +Require Import Liveness. Require Import Locations. Require Import LTL. Require Import Coloring. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index e1a3abcc..72de80af 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -452,6 +452,28 @@ Inductive transl_code_at_pc (ge: Mach.genv): code_tail (Int.unsigned ofs) (fn_code tf) tc -> transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc. +(** Equivalence between [transl_code] and [transl_code']. *) + +Local Open Scope error_monad_scope. + +Lemma transl_code_rec_transl_code: + forall f il ep k, + transl_code_rec f il ep k = (do c <- transl_code f il ep; k c). +Proof. + induction il; simpl; intros. + auto. + rewrite IHil. + destruct (transl_code f il (it1_is_parent ep a)); simpl; auto. +Qed. + +Lemma transl_code'_transl_code: + forall f il ep, + transl_code' f il ep = transl_code f il ep. +Proof. + intros. unfold transl_code'. rewrite transl_code_rec_transl_code. + destruct (transl_code f il ep); auto. +Qed. + (** Predictor for return addresses in generated Asm code. The [return_address_offset] predicate defined here is used in the diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v index 0ed2be10..8db871e9 100644 --- a/backend/CleanupLabels.v +++ b/backend/CleanupLabels.v @@ -44,17 +44,17 @@ Definition labels_branched_to (c: code) : Labelset.t := (** Remove label declarations for labels that are not in the [bto] (branched-to) set. *) -Fixpoint remove_unused_labels (bto: Labelset.t) (c: code) : code := - match c with - | nil => nil - | Llabel lbl :: c' => - if Labelset.mem lbl bto - then Llabel lbl :: remove_unused_labels bto c' - else remove_unused_labels bto c' - | i :: c' => - i :: remove_unused_labels bto c' +Definition remove_unused (bto: Labelset.t) (i: instruction) (k: code) : code := + match i with + | Llabel lbl => + if Labelset.mem lbl bto then i :: k else k + | _ => + i :: k end. +Definition remove_unused_labels (bto: Labelset.t) (c: code) : code := + list_fold_right (remove_unused bto) c nil. + Definition cleanup_labels (c: code) := remove_unused_labels (labels_branched_to c) c. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index dbd33c16..70f0eb36 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -143,6 +143,20 @@ Qed. (** Commutation with [find_label]. *) +Lemma remove_unused_labels_cons: + forall bto i c, + remove_unused_labels bto (i :: c) = + match i with + | Llabel lbl => + if Labelset.mem lbl bto then i :: remove_unused_labels bto c else remove_unused_labels bto c + | _ => + i :: remove_unused_labels bto c + end. +Proof. + unfold remove_unused_labels; intros. rewrite list_fold_right_eq. auto. +Qed. + + Lemma find_label_commut: forall lbl bto, Labelset.In lbl bto -> @@ -152,6 +166,7 @@ Lemma find_label_commut: Proof. induction c; simpl; intros. congruence. + rewrite remove_unused_labels_cons. unfold is_label in H0. destruct a; simpl; auto. destruct (peq lbl l). subst l. inv H0. rewrite Labelset.mem_1; auto. @@ -222,7 +237,7 @@ Theorem transf_step_correct: (exists s2', step tge s1' t s2' /\ match_states s2 s2') \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat. Proof. - induction 1; intros; inv MS; simpl. + induction 1; intros; inv MS; try rewrite remove_unused_labels_cons. (* Lop *) left; econstructor; split. econstructor; eauto. instantiate (1 := v). rewrite <- H. @@ -263,7 +278,7 @@ Proof. constructor. econstructor; eauto with coqlib. (* eliminated *) - right. split. omega. split. auto. econstructor; eauto with coqlib. + right. split. simpl. omega. split. auto. econstructor; eauto with coqlib. (* Lgoto *) left; econstructor; split. econstructor. eapply find_label_translated; eauto. red; auto. diff --git a/backend/CleanupLabelstyping.v b/backend/CleanupLabelstyping.v index f58a910f..11b516fe 100644 --- a/backend/CleanupLabelstyping.v +++ b/backend/CleanupLabelstyping.v @@ -24,9 +24,9 @@ Require Import LTLintyping. Lemma in_remove_unused_labels: forall bto i c, In i (remove_unused_labels bto c) -> In i c. Proof. - induction c; simpl. + unfold remove_unused_labels, remove_unused. induction c; simpl. auto. - destruct a; simpl; intuition. + rewrite list_fold_right_eq. destruct a; simpl; intuition. destruct (Labelset.mem l bto); simpl in H; intuition. Qed. diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml index ddd30944..09ffb8ee 100644 --- a/backend/Coloringaux.ml +++ b/backend/Coloringaux.ml @@ -91,7 +91,7 @@ let name_of_node n = | Some s -> s end | Some(S _), _ -> "fixed-slot" - | None, Some r -> Printf.sprintf "x%ld" (camlint_of_positive r) + | None, Some r -> Printf.sprintf "x%ld" (P.to_int32 r) | None, None -> "unknown-reg" *) @@ -602,12 +602,15 @@ let rec 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);*) + (*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; - u.movelist <- u.movelist @ v.movelist; + (* 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 *) diff --git a/backend/Constprop.v b/backend/Constprop.v index 2f3123f3..f85405d6 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -24,6 +24,7 @@ Require Import Registers. Require Import RTL. Require Import Lattice. Require Import Kildall. +Require Import Liveness. Require Import ConstpropOp. (** * Static analysis *) @@ -211,6 +212,18 @@ Definition transfer (gapp: global_approx) (f: function) (pc: node) (before: D.t) end end. +(** To reduce the size of approximations, we preventively set to [Top] + the approximations of registers used for the last time in the + current instruction. *) + +Definition transfer' (gapp: global_approx) (f: function) (lastuses: PTree.t (list reg)) + (pc: node) (before: D.t) := + let after := transfer gapp f pc before in + match lastuses!pc with + | None => after + | Some regs => List.fold_left (fun a r => D.set r Unknown a) regs after + end. + (** The static analysis itself is then an instantiation of Kildall's generic solver for forward dataflow inequations. [analyze f] returns a mapping from program points to mappings of pseudo-registers @@ -221,7 +234,8 @@ Definition transfer (gapp: global_approx) (f: function) (pc: node) (before: D.t) Module DS := Dataflow_Solver(D)(NodeSetForward). Definition analyze (gapp: global_approx) (f: RTL.function): PMap.t D.t := - match DS.fixpoint (successors f) (transfer gapp f) + let lu := Liveness.last_uses f in + match DS.fixpoint (successors f) (transfer' gapp f lu) ((f.(fn_entrypoint), D.top) :: nil) with | None => PMap.init D.top | Some res => res diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index b223e892..580d5518 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -26,6 +26,7 @@ Require Import Registers. Require Import RTL. Require Import Lattice. Require Import Kildall. +Require Import Liveness. Require Import ConstpropOp. Require Import Constprop. Require Import ConstpropOpproof. @@ -95,6 +96,18 @@ Proof. constructor. apply H. auto. Qed. +Lemma regs_match_approx_forget: + forall rs rl ra, + regs_match_approx ra rs -> + regs_match_approx (List.fold_left (fun a r => D.set r Unknown a) rl ra) rs. +Proof. + induction rl; simpl; intros. + auto. + apply IHrl. red; intros. destruct (peq r a). + subst a. rewrite D.gss. constructor. + rewrite D.gso; auto. +Qed. + (** The correctness of the static analysis follows from the results of module [ConstpropOpproof] and the fact that the result of the static analysis is a solution of the forward dataflow inequations. *) @@ -106,13 +119,15 @@ Lemma analyze_correct_1: regs_match_approx (transfer gapp f pc (analyze gapp f)!!pc) rs -> regs_match_approx (analyze gapp f)!!pc' rs. Proof. - intros until i. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer gapp f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. - apply regs_match_approx_increasing with (transfer gapp f pc approxs!!pc). + unfold analyze; intros. + set (lu := last_uses f) in *. + destruct (DS.fixpoint (successors f) (transfer' gapp f lu) + ((fn_entrypoint f, D.top) :: nil)) as [approxs|] eqn:FIX. + apply regs_match_approx_increasing with (transfer' gapp f lu pc approxs!!pc). eapply DS.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto. + unfold successors_list, successors. rewrite PTree.gmap1. rewrite H. auto. + unfold transfer'. destruct (lu!pc) as [regs|]. + apply regs_match_approx_forget; auto. auto. intros. rewrite PMap.gi. apply regs_match_approx_top. Qed. @@ -122,9 +137,9 @@ Lemma analyze_correct_3: regs_match_approx (analyze gapp f)!!(f.(fn_entrypoint)) rs. Proof. intros. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer gapp f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. + set (lu := last_uses f) in *. + destruct (DS.fixpoint (successors f) (transfer' gapp f lu) + ((fn_entrypoint f, D.top) :: nil)) as [approxs|] eqn:FIX. apply regs_match_approx_increasing with D.top. eapply DS.fixpoint_entry; eauto. auto with coqlib. apply regs_match_approx_top. diff --git a/backend/Linearize.v b/backend/Linearize.v index 636cb224..6fc8e489 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -198,17 +198,15 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code := (** Linearize a function body according to an enumeration of its nodes. *) -Fixpoint linearize_body (f: LTL.function) (enum: list node) - {struct enum} : code := - match enum with - | nil => nil - | pc :: rem => - match f.(LTL.fn_code)!pc with - | None => linearize_body f rem - | Some b => Llabel pc :: linearize_instr b (linearize_body f rem) - end +Definition linearize_node (f: LTL.function) (pc: node) (k: code) : code := + match f.(LTL.fn_code)!pc with + | None => k + | Some b => Llabel pc :: linearize_instr b k end. +Definition linearize_body (f: LTL.function) (enum: list node) : code := + list_fold_right (linearize_node f) enum nil. + (** * Entry points for code linearization *) Definition transf_function (f: LTL.function) : res LTLin.function := diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index b72268a6..d3683110 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -293,6 +293,18 @@ Proof. case (starts_with n k); simpl; auto. Qed. +Remark linearize_body_cons: + forall f pc enum, + linearize_body f (pc :: enum) = + match f.(LTL.fn_code)!pc with + | None => linearize_body f enum + | Some b => Llabel pc :: linearize_instr b (linearize_body f enum) + end. +Proof. + intros. unfold linearize_body. rewrite list_fold_right_eq. + unfold linearize_node. destruct (LTL.fn_code f)!pc; auto. +Qed. + Lemma find_label_lin_rec: forall f enum pc b, In pc enum -> @@ -301,12 +313,13 @@ Lemma find_label_lin_rec: Proof. induction enum; intros. elim H. - case (peq a pc); intro. + rewrite linearize_body_cons. + destruct (peq a pc). subst a. exists (linearize_body f enum). - simpl. rewrite H0. simpl. rewrite peq_true. auto. + rewrite H0. simpl. rewrite peq_true. auto. assert (In pc enum). simpl in H. tauto. - elim (IHenum pc b H1 H0). intros k FIND. - exists k. simpl. destruct (LTL.fn_code f)!a. + destruct (IHenum pc b H1 H0) as [k FIND]. + exists k. destruct (LTL.fn_code f)!a. simpl. rewrite peq_false. rewrite find_label_lin_instr. auto. auto. auto. Qed. @@ -377,7 +390,7 @@ Lemma label_in_lin_rec: Proof. induction enum. simpl; auto. - simpl. destruct (LTL.fn_code f)!a. + rewrite linearize_body_cons. destruct (LTL.fn_code f)!a. simpl. intros [A|B]. left; congruence. right. apply IHenum. eapply label_in_lin_instr; eauto. intro; right; auto. @@ -406,7 +419,8 @@ Lemma unique_labels_lin_rec: Proof. induction enum. simpl; auto. - intro. simpl. destruct (LTL.fn_code f)!a. + rewrite linearize_body_cons. + intro. destruct (LTL.fn_code f)!a. simpl. split. red. intro. inversion H. elim H3. apply label_in_lin_rec with f. apply label_in_lin_instr with i. auto. diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index 7393535d..b4e25de7 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -71,9 +71,9 @@ Lemma wt_linearize_body: forall enum, wt_code f.(LTL.fn_sig) (linearize_body f enum). Proof. - induction enum; simpl. + unfold linearize_body; induction enum; rewrite list_fold_right_eq. red; simpl; intros; contradiction. - caseEq ((LTL.fn_code f)!a); intros. + unfold linearize_node. caseEq ((LTL.fn_code f)!a); intros. apply wt_add_instr. constructor. apply wt_linearize_instr; eauto with coqlib. auto. Qed. diff --git a/backend/Liveness.v b/backend/Liveness.v new file mode 100644 index 00000000..b97455fc --- /dev/null +++ b/backend/Liveness.v @@ -0,0 +1,147 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Liveness analysis over RTL *) + +Require Import Coqlib. +Require Import Maps. +Require Import Lattice. +Require Import AST. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import Kildall. + +(** A register [r] is live at a point [p] if there exists a path + from [p] to some instruction that uses [r] as argument, + and [r] is not redefined along this path. + Liveness can be computed by a backward dataflow analysis. + The analysis operates over sets of (live) pseudo-registers. *) + +Notation reg_live := Regset.add. +Notation reg_dead := Regset.remove. + +Definition reg_option_live (or: option reg) (lv: Regset.t) := + match or with None => lv | Some r => reg_live r lv end. + +Definition reg_sum_live (ros: reg + ident) (lv: Regset.t) := + match ros with inl r => reg_live r lv | inr s => lv end. + +Fixpoint reg_list_live + (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t := + match rl with + | nil => lv + | r1 :: rs => reg_list_live rs (reg_live r1 lv) + end. + +Fixpoint reg_list_dead + (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t := + match rl with + | nil => lv + | r1 :: rs => reg_list_dead rs (reg_dead r1 lv) + end. + +(** Here is the transfer function for the dataflow analysis. + Since this is a backward dataflow analysis, it takes as argument + the abstract register set ``after'' the given instruction, + i.e. the registers that are live after; and it returns as result + the abstract register set ``before'' the given instruction, + i.e. the registers that must be live before. + The general relation between ``live before'' and ``live after'' + an instruction is that a register is live before if either + it is one of the arguments of the instruction, or it is not the result + of the instruction and it is live after. + However, if the result of a side-effect-free instruction is not + live ``after'', the whole instruction will be removed later + (since it computes a useless result), thus its arguments need not + be live ``before''. *) + +Definition transfer + (f: function) (pc: node) (after: Regset.t) : Regset.t := + match f.(fn_code)!pc with + | None => + Regset.empty + | Some i => + match i with + | Inop s => + after + | Iop op args res s => + if Regset.mem res after then + reg_list_live args (reg_dead res after) + else + after + | Iload chunk addr args dst s => + if Regset.mem dst after then + reg_list_live args (reg_dead dst after) + else + after + | Istore chunk addr args src s => + reg_list_live args (reg_live src after) + | Icall sig ros args res s => + reg_list_live args + (reg_sum_live ros (reg_dead res after)) + | Itailcall sig ros args => + reg_list_live args (reg_sum_live ros Regset.empty) + | Ibuiltin ef args res s => + reg_list_live args (reg_dead res after) + | Icond cond args ifso ifnot => + reg_list_live args after + | Ijumptable arg tbl => + reg_live arg after + | Ireturn optarg => + reg_option_live optarg Regset.empty + end + end. + +(** The liveness analysis is then obtained by instantiating the + general framework for backward dataflow analysis provided by + module [Kildall]. *) + +Module RegsetLat := LFSet(Regset). +Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward). + +Definition analyze (f: function): option (PMap.t Regset.t) := + DS.fixpoint (successors f) (transfer f) nil. + +(** Basic property of the liveness information computed by [analyze]. *) + +Lemma analyze_solution: + forall f live n i s, + analyze f = Some live -> + f.(fn_code)!n = Some i -> + In s (successors_instr i) -> + Regset.Subset (transfer f s live!!s) live!!n. +Proof. + unfold analyze; intros. eapply DS.fixpoint_solution; eauto. + unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. simpl. auto. +Qed. + +(** Given an RTL function, compute (for every PC) the list of + pseudo-registers that are used for the last time in the instruction + at PC. These are the registers that are used or defined by the instruction + and dead afterwards. *) + +Definition last_uses_at (live: PMap.t Regset.t) (pc: node) (i: instruction) : list reg := + let l := live!!pc in + let lu := List.filter (fun r => negb (Regset.mem r l)) (instr_uses i) in + match instr_defs i with + | None => lu + | Some r => if Regset.mem r l then lu else r :: lu + end. + +Definition last_uses (f: function) : PTree.t (list reg) := + match analyze f with + | None => PTree.empty (list reg) + | Some live => PTree.map (last_uses_at live) f.(fn_code) + end. + + diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index ef6ba1d8..01ea1e6e 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -255,7 +255,7 @@ let print_function p id f = fprintf p "@;<0 -2>}@]@ " let print_extfun p id ef = - fprintf p "@[extern @[\"%s\" =@ %s :@ %a@]@ " + fprintf p "@[extern @[\"%s\" =@ %s :@ %a@]@]@ " (extern_atom id) (name_of_external ef) print_sig (ef_sig ef) let print_init_data p = function diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 0bafcde1..0cdf5056 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -95,7 +95,7 @@ let print_function pp id f = let instrs = List.sort (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) - (List.map + (List.rev_map (fun (pc, i) -> (P.to_int32 pc, i)) (PTree.elements f.fn_code)) in print_succ pp f.fn_entrypoint diff --git a/backend/RRE.v b/backend/RRE.v index b8409e33..bee57f67 100644 --- a/backend/RRE.v +++ b/backend/RRE.v @@ -109,57 +109,61 @@ Fixpoint safe_move_insertion (c: code) : bool := into register-to-register move whenever possible. Simultaneously, it propagates valid (register, slot) equations across basic blocks. *) -Fixpoint transf_code (eqs: equations) (c: code) : code := +(** [transf_code] is written in accumulator-passing style so that it runs + in constant stack space. The [k] parameter accumulates the instructions + to be generated, in reverse order, and is then reversed at the end *) + +Fixpoint transf_code (eqs: equations) (c: code) (k: code) : code := match c with - | nil => nil + | nil => List.rev' k | Lgetstack s r :: c => if is_incoming s then - Lgetstack s r :: transf_code (kill_loc (R r) (kill_loc (R IT1) eqs)) c + transf_code (kill_loc (R r) (kill_loc (R IT1) eqs)) c (Lgetstack s r :: k) else if contains_equation s r eqs then - transf_code eqs c + transf_code eqs c k else match find_reg_containing s eqs with | Some r' => if safe_move_insertion c then - Lop Omove (r' :: nil) r :: transf_code (kill_at_move (mkeq r s :: kill_loc (R r) eqs)) c + transf_code (kill_at_move (mkeq r s :: kill_loc (R r) eqs)) c (Lop Omove (r' :: nil) r :: k) else - Lgetstack s r:: transf_code (mkeq r s :: kill_loc (R r) eqs) c + transf_code (mkeq r s :: kill_loc (R r) eqs) c (Lgetstack s r :: k) | None => - Lgetstack s r:: transf_code (mkeq r s :: kill_loc (R r) eqs) c + transf_code (mkeq r s :: kill_loc (R r) eqs) c (Lgetstack s r :: k) end | Lsetstack r s :: c => - Lsetstack r s :: transf_code (kill_at_move (mkeq r s :: kill_loc (S s) eqs)) c + transf_code (kill_at_move (mkeq r s :: kill_loc (S s) eqs)) c (Lsetstack r s :: k) | Lop op args res :: c => - Lop op args res :: transf_code (kill_loc (R res) (kill_op op eqs)) c + transf_code (kill_loc (R res) (kill_op op eqs)) c (Lop op args res :: k) | Lload chunk addr args res :: c => - Lload chunk addr args res :: transf_code (kill_loc (R res) (kill_temps eqs)) c + transf_code (kill_loc (R res) (kill_temps eqs)) c (Lload chunk addr args res :: k) | Lstore chunk addr args src :: c => - Lstore chunk addr args src :: transf_code (kill_temps eqs) c + transf_code (kill_temps eqs) c (Lstore chunk addr args src :: k) | Lcall sg ros :: c => - Lcall sg ros :: transf_code nil c + transf_code nil c (Lcall sg ros :: k) | Ltailcall sg ros :: c => - Ltailcall sg ros :: transf_code nil c + transf_code nil c (Ltailcall sg ros :: k) | Lbuiltin ef args res :: c => - Lbuiltin ef args res :: transf_code (kill_loc (R res) (kill_temps eqs)) c + transf_code (kill_loc (R res) (kill_temps eqs)) c (Lbuiltin ef args res :: k) | Lannot ef args :: c => - Lannot ef args :: transf_code eqs c + transf_code eqs c (Lannot ef args :: k) | Llabel lbl :: c => - Llabel lbl :: transf_code nil c + transf_code nil c (Llabel lbl :: k) | Lgoto lbl :: c => - Lgoto lbl :: transf_code nil c + transf_code nil c (Lgoto lbl :: k) | Lcond cond args lbl :: c => - Lcond cond args lbl :: transf_code (kill_temps eqs) c + transf_code (kill_temps eqs) c (Lcond cond args lbl :: k) | Ljumptable arg lbls :: c => - Ljumptable arg lbls :: transf_code nil c + transf_code nil c (Ljumptable arg lbls :: k) | Lreturn :: c => - Lreturn :: transf_code nil c + transf_code nil c (Lreturn :: k) end. Definition transf_function (f: function) : function := mkfunction (fn_sig f) (fn_stacksize f) - (transf_code nil (fn_code f)). + (transf_code nil (fn_code f) nil). Definition transf_fundef (fd: fundef) : fundef := transf_fundef transf_function fd. diff --git a/backend/RREproof.v b/backend/RREproof.v index 40632f74..98de7a86 100644 --- a/backend/RREproof.v +++ b/backend/RREproof.v @@ -280,18 +280,44 @@ Proof. destruct op; exact agree_undef_temps || exact agree_undef_move_2. Qed. +Lemma transf_code_cont: + forall c eqs k1 k2, + transf_code eqs c (k1 ++ k2) = List.rev k2 ++ transf_code eqs c k1. +Proof. + induction c; simpl; intros. + unfold rev'; rewrite <- ! rev_alt; apply rev_app_distr. + destruct a; try (rewrite <- IHc; reflexivity). + destruct (is_incoming s). + rewrite <- IHc; reflexivity. + destruct (contains_equation s m eqs). + auto. + destruct (find_reg_containing s eqs). + destruct (safe_move_insertion c). + rewrite <- IHc; reflexivity. + rewrite <- IHc; reflexivity. + rewrite <- IHc; reflexivity. +Qed. + +Corollary transf_code_eq: + forall eqs c i, transf_code eqs c (i :: nil) = i :: transf_code eqs c nil. +Proof. + intros. change (i :: nil) with (nil ++ (i :: nil)). + rewrite transf_code_cont. auto. +Qed. + Lemma transl_find_label: forall lbl c eqs, - find_label lbl (transf_code eqs c) = - option_map (transf_code nil) (find_label lbl c). + find_label lbl (transf_code eqs c nil) = + option_map (fun c => transf_code nil c nil) (find_label lbl c). Proof. - induction c; simpl; intros. + induction c; intros. auto. - destruct a; simpl; auto. + destruct a; simpl; try (rewrite transf_code_eq; simpl; auto). destruct (is_incoming s); simpl; auto. - destruct (contains_equation s m eqs); auto. - destruct (find_reg_containing s eqs); simpl; auto. - destruct (safe_move_insertion c); simpl; auto. + destruct (contains_equation s m eqs). auto. + destruct (find_reg_containing s eqs); rewrite !transf_code_eq. + destruct (safe_move_insertion c); simpl; auto. + simpl; auto. destruct (peq lbl l); simpl; auto. Qed. @@ -348,7 +374,7 @@ Inductive match_frames: stackframe -> stackframe -> Prop := | match_frames_intro: forall f sp rs c, match_frames (Stackframe f sp rs c) - (Stackframe (transf_function f) sp rs (transf_code nil c)). + (Stackframe (transf_function f) sp rs (transf_code nil c nil)). Inductive match_states: state -> state -> Prop := | match_states_regular: @@ -358,7 +384,7 @@ Inductive match_states: state -> state -> Prop := (AG: agree sm rs rs') (SAFE: sm = false \/ safe_move_insertion c = true), match_states (State stk f sp c rs m) - (State stk' (transf_function f) sp (transf_code eqs c) rs' m) + (State stk' (transf_function f) sp (transf_code eqs c nil) rs' m) | match_states_call: forall stk f rs m stk' (STK: list_forall2 match_frames stk stk'), @@ -400,7 +426,8 @@ Opaque destroyed_at_move_regs. (* incoming, stays as getstack *) assert (UGS: forall rs, undef_getstack sl rs = Locmap.set (R IT1) Vundef rs). destruct sl; simpl in Heqb0; discriminate || auto. - left; econstructor; split. constructor. + left; econstructor; split. + rewrite transf_code_eq; constructor. repeat rewrite UGS. apply match_states_regular with sm. auto. apply kill_loc_hold. apply kill_loc_hold; auto. @@ -424,20 +451,23 @@ Opaque destroyed_at_move_regs. simpl; intro EQ. (* turned into a move *) destruct (safe_move_insertion b) eqn:?. - left; econstructor; split. constructor. simpl; eauto. + left; econstructor; split. + rewrite transf_code_eq. constructor. simpl; eauto. rewrite UGS. rewrite <- EQ. apply match_states_regular with true; auto. apply eqs_movestack_hold; auto. rewrite (agree_slot _ _ _ sl AG). apply agree_set. eapply agree_undef_move_1; eauto. (* left as a getstack *) - left; econstructor; split. constructor. + left; econstructor; split. + rewrite transf_code_eq. constructor. repeat rewrite UGS. apply match_states_regular with sm. auto. apply eqs_getstack_hold; auto. rewrite (agree_slot _ _ _ sl AG). apply agree_set. auto. intuition congruence. (* no equation, left as a getstack *) - left; econstructor; split. constructor. + left; econstructor; split. + rewrite transf_code_eq; constructor. repeat rewrite UGS. apply match_states_regular with sm. auto. apply eqs_getstack_hold; auto. @@ -445,14 +475,14 @@ Opaque destroyed_at_move_regs. tauto. (* setstack *) - left; econstructor; split. constructor. + left; econstructor; split. rewrite transf_code_eq; constructor. apply match_states_regular with false; auto. apply eqs_setstack_hold; auto. rewrite (agree_reg _ _ _ r AG). apply agree_set. eapply agree_undef_move_2; eauto. simpl in SAFE. destruct (in_dec mreg_eq r destroyed_at_move_regs); simpl in SAFE; intuition congruence. (* op *) - left; econstructor; split. constructor. + left; econstructor; split. rewrite transf_code_eq; constructor. instantiate (1 := v). rewrite <- H. rewrite (agree_regs _ _ _ args AG). apply eval_operation_preserved. exact symbols_preserved. @@ -463,7 +493,7 @@ Opaque destroyed_at_move_regs. (* load *) left; econstructor; split. - econstructor. instantiate (1 := a). rewrite <- H. + rewrite transf_code_eq; econstructor. instantiate (1 := a). rewrite <- H. rewrite (agree_regs _ _ _ args AG). apply eval_addressing_preserved. exact symbols_preserved. simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence. @@ -480,7 +510,7 @@ Opaque list_disjoint_dec. destruct (list_disjoint_dec mreg_eq (src :: args) destroyed_at_move_regs); try discriminate. split. eapply list_disjoint_notin; eauto with coqlib. eapply list_disjoint_cons_left; eauto. left; econstructor; split. - econstructor. instantiate (1 := a). rewrite <- H. + rewrite transf_code_eq; econstructor. instantiate (1 := a). rewrite <- H. rewrite (agree_regs _ _ _ args AG). apply eval_addressing_preserved. exact symbols_preserved. tauto. @@ -495,7 +525,7 @@ Opaque list_disjoint_dec. simpl in SAFE. assert (sm = false) by intuition congruence. subst sm. rewrite agree_false in AG. subst rs'. left; econstructor; split. - constructor. eapply find_function_translated; eauto. + rewrite transf_code_eq; constructor. eapply find_function_translated; eauto. symmetry; apply sig_preserved. constructor. constructor; auto. constructor. @@ -503,13 +533,13 @@ Opaque list_disjoint_dec. simpl in SAFE. assert (sm = false) by intuition congruence. subst sm. rewrite agree_false in AG. subst rs'. left; econstructor; split. - constructor. eapply find_function_translated; eauto. + rewrite transf_code_eq; constructor. eapply find_function_translated; eauto. symmetry; apply sig_preserved. eauto. rewrite (match_parent_locset _ _ STK). constructor; auto. (* builtin *) left; econstructor; split. - constructor. + rewrite transf_code_eq; constructor. rewrite (agree_regs _ _ _ args AG). eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. @@ -522,20 +552,20 @@ Opaque list_disjoint_dec. simpl in SAFE. assert (sm = false) by intuition congruence. subst sm. rewrite agree_false in AG. subst rs'. left; econstructor; split. - econstructor. eapply external_call_symbols_preserved; eauto. + rewrite transf_code_eq; econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. apply match_states_regular with false; auto. rewrite agree_false; auto. (* label *) - left; econstructor; split. constructor. + left; econstructor; split. rewrite transf_code_eq; constructor. apply match_states_regular with false; auto. apply nil_hold. simpl in SAFE. destruct SAFE. subst sm. auto. congruence. (* goto *) generalize (transl_find_label lbl (fn_code f) nil). rewrite H. simpl. intros. - left; econstructor; split. constructor; eauto. + left; econstructor; split. rewrite transf_code_eq; constructor; eauto. apply match_states_regular with false; auto. apply nil_hold. simpl in SAFE. destruct SAFE. subst sm. auto. congruence. @@ -543,7 +573,7 @@ Opaque list_disjoint_dec. (* cond true *) generalize (transl_find_label lbl (fn_code f) nil). rewrite H0. simpl. intros. left; econstructor; split. - apply exec_Lcond_true; auto. + rewrite transf_code_eq; apply exec_Lcond_true; auto. rewrite (agree_regs _ _ _ args AG). auto. simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence. eauto. @@ -552,7 +582,7 @@ Opaque list_disjoint_dec. eapply agree_undef_temps; eauto. (* cond false *) - left; econstructor; split. apply exec_Lcond_false; auto. + left; econstructor; split. rewrite transf_code_eq; apply exec_Lcond_false; auto. rewrite (agree_regs _ _ _ args AG). auto. simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence. apply match_states_regular with false; auto. @@ -561,7 +591,7 @@ Opaque list_disjoint_dec. (* jumptable *) generalize (transl_find_label lbl (fn_code f) nil). rewrite H1. simpl. intros. - left; econstructor; split. econstructor; eauto. + left; econstructor; split. rewrite transf_code_eq; econstructor; eauto. rewrite (agree_reg _ _ _ arg AG). auto. simpl in SAFE. destruct (in_dec mreg_eq arg destroyed_at_move_regs); simpl in SAFE; intuition congruence. apply match_states_regular with false; auto. @@ -571,7 +601,7 @@ Opaque list_disjoint_dec. (* return *) simpl in SAFE. destruct SAFE; try discriminate. subst sm. rewrite agree_false in AG. subst rs'. left; econstructor; split. - constructor. simpl. eauto. + rewrite transf_code_eq; constructor. simpl. eauto. rewrite (match_parent_locset _ _ STK). constructor; auto. diff --git a/backend/RREtyping.v b/backend/RREtyping.v index 539fb20b..170d8adc 100644 --- a/backend/RREtyping.v +++ b/backend/RREtyping.v @@ -83,19 +83,20 @@ Hint Resolve wt_kill_op: linearty. Lemma wt_transf_code: forall f c eqs, wt_code f c -> wt_eqs eqs -> - wt_code (transf_function f) (transf_code eqs c). + wt_code (transf_function f) (transf_code eqs c nil). Proof. induction c; intros; simpl. red; simpl; tauto. assert (WI: wt_instr f a) by auto with coqlib. assert (WC: wt_code f c) by (red; auto with coqlib). clear H. - inv WI; auto 10 with linearty. + inv WI; rewrite ? transf_code_eq; auto 10 with linearty. destruct (is_incoming s) eqn:?. auto with linearty. destruct (contains_equation s r eqs). auto with linearty. destruct (find_reg_containing s eqs) as [r'|] eqn:?; auto with linearty. assert (mreg_type r' = mreg_type r). exploit H0. eapply find_reg_containing_sound; eauto. simpl. congruence. + rewrite ! transf_code_eq. destruct (safe_move_insertion c); auto 10 with linearty. Qed. diff --git a/backend/Reload.v b/backend/Reload.v index 31bddcd0..be844b30 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -257,7 +257,7 @@ Definition transf_instr end. Definition transf_code (f: LTLin.function) (c: LTLin.code) : code := - List.fold_right (transf_instr f) nil c. + list_fold_right (transf_instr f) c nil. Definition transf_function (f: LTLin.function) : function := mkfunction diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 64022378..fe6e475c 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -837,6 +837,12 @@ Proof. destruct o; FL. Qed. +Lemma transf_code_cons: + forall f i c, transf_code f (i :: c) = transf_instr f i (transf_code f c). +Proof. + unfold transf_code; intros. rewrite list_fold_right_eq; auto. +Qed. + Lemma find_label_transf_code: forall sg lbl c, find_label lbl (transf_code sg c) = @@ -844,6 +850,7 @@ Lemma find_label_transf_code: Proof. induction c; simpl. auto. + rewrite transf_code_cons. rewrite find_label_transf_instr. destruct (LTLin.is_label lbl a); auto. Qed. @@ -1022,7 +1029,7 @@ Theorem transf_step_correct: \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat. Proof. Opaque regs_for. Opaque add_reloads. - induction 1; intros; try inv MS; simpl. + induction 1; intros; try inv MS; try rewrite transf_code_cons; simpl. (* Lop *) ExploitWT. inv WTI. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index c0051399..70d79bcb 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -317,6 +317,7 @@ Lemma wt_transf_code: Proof. induction c; simpl; intros. red; simpl; tauto. + rewrite transf_code_cons. apply wt_transf_instr; auto with coqlib. apply IHc. red; auto with coqlib. Qed. diff --git a/backend/Stacking.v b/backend/Stacking.v index 732443bf..03e882ea 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -207,7 +207,7 @@ Definition transl_instr Definition transl_code (fe: frame_env) (il: list Linear.instruction) : Mach.code := - List.fold_right (transl_instr fe) nil il. + list_fold_right (transl_instr fe) il nil. Definition transl_body (f: Linear.function) (fe: frame_env) := save_callee_save fe (transl_code fe f.(Linear.fn_code)). diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d97ec930..a73f0aa6 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1997,6 +1997,12 @@ Proof. intro; reflexivity. Qed. +Lemma transl_code_eq: + forall fe i c, transl_code fe (i :: c) = transl_instr fe i (transl_code fe c). +Proof. + unfold transl_code; intros. rewrite list_fold_right_eq. auto. +Qed. + Lemma find_label_transl_code: forall fe lbl c, Mach.find_label lbl (transl_code fe c) = @@ -2004,6 +2010,7 @@ Lemma find_label_transl_code: Proof. induction c; simpl; intros. auto. + rewrite transl_code_eq. destruct a; unfold transl_instr; auto. destruct s; simpl; auto. destruct s; simpl; auto. @@ -2089,7 +2096,8 @@ Qed. Lemma is_tail_transl_code: forall fe c1 c2, is_tail c1 c2 -> is_tail (transl_code fe c1) (transl_code fe c2). Proof. - induction 1; simpl. auto with coqlib. + induction 1; simpl. auto with coqlib. + rewrite transl_code_eq. eapply is_tail_trans. eauto. apply is_tail_transl_instr. Qed. @@ -2364,14 +2372,9 @@ Theorem transf_step_correct: forall s1' (MS: match_states s1 s1'), exists s2', plus step tge s1' t s2' /\ match_states s2 s2'. Proof. - assert (RED: forall f i c, - transl_code (make_env (function_bounds f)) (i :: c) = - transl_instr (make_env (function_bounds f)) i - (transl_code (make_env (function_bounds f)) c)). - intros. reflexivity. induction 1; intros; try inv MS; - try rewrite RED; + try rewrite transl_code_eq; try (generalize (WTF _ (is_tail_in TAIL)); intro WTI); try (generalize (function_is_within_bounds f WTF _ (is_tail_in TAIL)); intro BOUND; simpl in BOUND); @@ -2512,7 +2515,8 @@ Proof. (* Lcall *) exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. - exploit is_tail_transf_function; eauto. intros IST. simpl in IST. + exploit is_tail_transf_function; eauto. intros IST. + rewrite transl_code_eq in IST. simpl in IST. exploit return_address_offset_exists. eexact IST. intros [ra D]. econstructor; split. -- cgit