diff options
| -rw-r--r-- | .depend | 5 | ||||
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | backend/Locations.v | 35 | ||||
| -rw-r--r-- | backend/RRE.v | 172 | ||||
| -rw-r--r-- | backend/RREproof.v | 630 | ||||
| -rw-r--r-- | backend/RREtyping.v | 109 | ||||
| -rw-r--r-- | driver/Compiler.v | 8 |
7 files changed, 938 insertions, 22 deletions
@@ -75,6 +75,9 @@ backend/Parallelmove.vo backend/Parallelmove.glob: backend/Parallelmove.v lib/Co backend/Reload.vo backend/Reload.glob: backend/Reload.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/Conventions.vo backend/Parallelmove.vo backend/Linear.vo backend/Reloadproof.vo backend/Reloadproof.glob: backend/Reloadproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Parallelmove.vo backend/Reload.vo backend/Reloadtyping.vo backend/Reloadtyping.glob: backend/Reloadtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Parallelmove.vo backend/Reload.vo backend/Reloadproof.vo +backend/RRE.vo backend/RRE.glob: backend/RRE.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo +backend/RREproof.vo backend/RREproof.glob: backend/RREproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/RRE.vo +backend/RREtyping.vo backend/RREtyping.glob: backend/RREtyping.v lib/Coqlib.vo common/AST.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/RRE.vo backend/RREproof.vo backend/Mach.vo backend/Mach.glob: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Machtyping.vo backend/Machtyping.glob: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Bounds.vo backend/Bounds.glob: backend/Bounds.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo @@ -103,5 +106,5 @@ cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo common/Smallstep.vo cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo -driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo +driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/RRE.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/RREproof.vo backend/RREtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo driver/Complements.vo driver/Complements.glob: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo @@ -63,6 +63,7 @@ BACKEND=\ CleanupLabels.v CleanupLabelsproof.v CleanupLabelstyping.v \ Linear.v Lineartyping.v \ Parallelmove.v Reload.v Reloadproof.v Reloadtyping.v \ + RRE.v RREproof.v RREtyping.v \ Mach.v Machtyping.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v Stackingtyping.v \ Machsem.v \ diff --git a/backend/Locations.v b/backend/Locations.v index 8a0b5ea..0b538fd 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -301,22 +301,26 @@ Module Loc. | l1 :: ls => diff l l1 /\ notin l ls end. + Lemma notin_iff: + forall l ll, notin l ll <-> (forall l', In l' ll -> Loc.diff l l'). + Proof. + induction ll; simpl. + tauto. + rewrite IHll. intuition. subst a. auto. + Qed. + Lemma notin_not_in: forall l ll, notin l ll -> ~(In l ll). Proof. - unfold not; induction ll; simpl; intros. - auto. - elim H; intros. elim H0; intro. - subst l. exact (same_not_diff a H1). - auto. + intros; red; intros. rewrite notin_iff in H. + elim (diff_not_eq l l); auto. Qed. Lemma reg_notin: forall r ll, ~(In (R r) ll) -> notin (R r) ll. Proof. - induction ll; simpl; intros. auto. - split. destruct a; auto. intuition congruence. - apply IHll. intuition. + intros. rewrite notin_iff; intros. + destruct l'; simpl. congruence. auto. Qed. (** [Loc.disjoint l1 l2] is true if the locations in list [l1] @@ -347,29 +351,20 @@ Module Loc. Lemma in_notin_diff: forall l1 l2 ll, notin l1 ll -> In l2 ll -> diff l1 l2. Proof. - induction ll; simpl; intros. - elim H0. - elim H0; intro. subst a. tauto. apply IHll; tauto. + intros. rewrite notin_iff in H. auto. Qed. Lemma notin_disjoint: forall l1 l2, (forall x, In x l1 -> notin x l2) -> disjoint l1 l2. Proof. - unfold disjoint; induction l1; intros. - elim H0. - elim H0; intro. - subst x1. eapply in_notin_diff. apply H. auto with coqlib. auto. - eapply IHl1; eauto. intros. apply H. auto with coqlib. + intros; red; intros. exploit H; eauto. rewrite notin_iff; intros. auto. Qed. Lemma disjoint_notin: forall l1 l2 x, disjoint l1 l2 -> In x l1 -> notin x l2. Proof. - unfold disjoint; induction l2; simpl; intros. - auto. - split. apply H. auto. tauto. - apply IHl2. intros. apply H. auto. tauto. auto. + intros; rewrite notin_iff; intros. red in H. auto. Qed. (** [Loc.norepet ll] holds if the locations in list [ll] are pairwise diff --git a/backend/RRE.v b/backend/RRE.v new file mode 100644 index 0000000..95eadce --- /dev/null +++ b/backend/RRE.v @@ -0,0 +1,172 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Redundant Reloads Elimination *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Values. +Require Import Globalenvs. +Require Import Op. +Require Import Locations. +Require Import Conventions. +Require Import Linear. + +(** * Equations between slots and machine registers *) + +(** The RRE pass keeps track of which register holds the value of which + stack slot, using sets of equations like the following. *) + +Record equation := mkeq { e_reg: mreg; e_slot: slot }. + +Definition equations : Type := list equation. + +Fixpoint find_reg_containing (s: slot) (eqs: equations) : option mreg := + match eqs with + | nil => None + | e :: eqs' => if slot_eq (e_slot e) s then Some (e_reg e) else find_reg_containing s eqs' + end. + +Definition eq_equation (eq1 eq2: equation) : {eq1=eq2} + {eq1<>eq2}. +Proof. + generalize slot_eq mreg_eq. decide equality. +Qed. + +Definition contains_equation (s: slot) (r: mreg) (eqs: equations) : bool := + In_dec eq_equation (mkeq r s) eqs. + +(** Remove equations that are invalidated by an assignment to location [l]. *) + +Fixpoint kill_loc (l: loc) (eqs: equations) : equations := + match eqs with + | nil => nil + | e :: eqs' => + if Loc.diff_dec (S (e_slot e)) l && Loc.diff_dec (R (e_reg e)) l + then e :: kill_loc l eqs' + else kill_loc l eqs' + end. + +(** Same, for a list of locations [ll]. *) + +Definition kill_locs (ll: list loc) (eqs: equations) : equations := + List.fold_left (fun eqs l => kill_loc l eqs) ll eqs. + +Definition kill_temps (eqs: equations) : equations := + kill_locs temporaries eqs. + +Definition kill_at_move (eqs: equations) : equations := + kill_locs destroyed_at_move eqs. + +Definition kill_op (op: operation) (eqs: equations) : equations := + match op with Omove => kill_at_move eqs | _ => kill_temps eqs end. + +(** * Safety criterion *) + +Definition is_incoming (s: slot) : bool := + match s with + | Incoming _ _ => true + | _ => false + end. + +(** Turning a [Lgetstack] into a register-to-register move is not always + safe: at least on x86, the move destroys some registers + (those from [destroyed_at_move] list) while the [Lgetstack] does not. + Therefore, we perform this transformation only if the destroyed + registers are not used before being destroyed by a later + [Lop], [Lload], [Lstore], [Lbuiltin], [Lcond] or [Ljumptable] operation. *) + +Fixpoint safe_move_insertion (c: code) : bool := + match c with + | Lgetstack s r :: c' => + negb(In_dec mreg_eq r destroyed_at_move_regs) && safe_move_insertion c' + | Lsetstack r s :: c' => + negb(In_dec mreg_eq r destroyed_at_move_regs) + | Lop op args res :: c' => + list_disjoint_dec mreg_eq args destroyed_at_move_regs + | Lload chunk addr args res :: c' => + list_disjoint_dec mreg_eq args destroyed_at_move_regs + | Lstore chunk addr args src :: c' => + list_disjoint_dec mreg_eq (src :: args) destroyed_at_move_regs + | Lbuiltin ef args res :: c' => + list_disjoint_dec mreg_eq args destroyed_at_move_regs + | Lcond cond args lbl :: c' => + list_disjoint_dec mreg_eq args destroyed_at_move_regs + | Ljumptable arg tbl :: c' => + negb(In_dec mreg_eq arg destroyed_at_move_regs) + | _ => false + end. + +(** * Code transformation *) + +(** The following function eliminates [Lgetstack] instructions or turn them + 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 := + match c with + | nil => nil + | Lgetstack s r :: c => + if is_incoming s then + Lgetstack s r :: transf_code (kill_loc (R r) (kill_loc (R IT1) eqs)) c + else if contains_equation s r eqs then + transf_code eqs c + 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 + else + Lgetstack s r:: transf_code (mkeq r s :: kill_loc (R r) eqs) c + | None => + Lgetstack s r:: transf_code (mkeq r s :: kill_loc (R r) eqs) c + end + | Lsetstack r s :: c => + Lsetstack r s :: transf_code (kill_at_move (mkeq r s :: kill_loc (S s) eqs)) c + | Lop op args res :: c => + Lop op args res :: transf_code (kill_loc (R res) (kill_op op eqs)) c + | Lload chunk addr args res :: c => + Lload chunk addr args res :: transf_code (kill_loc (R res) (kill_temps eqs)) c + | Lstore chunk addr args src :: c => + Lstore chunk addr args src :: transf_code (kill_temps eqs) c + | Lcall sg ros :: c => + Lcall sg ros :: transf_code nil c + | Ltailcall sg ros :: c => + Ltailcall sg ros :: transf_code nil c + | Lbuiltin ef args res :: c => + Lbuiltin ef args res :: transf_code (kill_loc (R res) (kill_temps eqs)) c + | Lannot ef args :: c => + Lannot ef args :: transf_code eqs c + | Llabel lbl :: c => + Llabel lbl :: transf_code nil c + | Lgoto lbl :: c => + Lgoto lbl :: transf_code nil c + | Lcond cond args lbl :: c => + Lcond cond args lbl :: transf_code (kill_temps eqs) c + | Ljumptable arg lbls :: c => + Ljumptable arg lbls :: transf_code nil c + | Lreturn :: c => + Lreturn :: transf_code nil c + end. + +Definition transf_function (f: function) : function := + mkfunction + (fn_sig f) + (fn_stacksize f) + (transf_code nil (fn_code f)). + +Definition transf_fundef (fd: fundef) : fundef := + transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. + diff --git a/backend/RREproof.v b/backend/RREproof.v new file mode 100644 index 0000000..da959ea --- /dev/null +++ b/backend/RREproof.v @@ -0,0 +1,630 @@ +(* *********************************************************************) +(* *) +(* 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 proof for the [RRE] pass. *) + +Require Import Axioms. +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Values. +Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. +Require Import Op. +Require Import Locations. +Require Import Conventions. +Require Import Linear. +Require Import RRE. + +(** * Operations over equations *) + +Lemma find_reg_containing_sound: + forall s r eqs, find_reg_containing s eqs = Some r -> In (mkeq r s) eqs. +Proof. + induction eqs; simpl; intros. + congruence. + destruct (slot_eq (e_slot a) s). inv H. left; destruct a; auto. right; eauto. +Qed. + +Definition equations_hold (ls: locset) (eqs: equations) : Prop := + forall e, In e eqs -> ls (S (e_slot e)) = ls (R (e_reg e)). + +Lemma nil_hold: + forall ls, equations_hold ls nil. +Proof. + red; intros; contradiction. +Qed. + +Lemma In_kill_loc: + forall e l eqs, + In e (kill_loc l eqs) -> + In e eqs /\ Loc.diff (S (e_slot e)) l /\ Loc.diff (R (e_reg e)) l. +Proof. + induction eqs; simpl kill_loc; simpl In; intros. + tauto. + destruct (Loc.diff_dec (S (e_slot a)) l). + destruct (Loc.diff_dec (R (e_reg a)) l). + simpl in H. intuition congruence. + simpl in H. intuition. + simpl in H. intuition. +Qed. + +Lemma kill_loc_hold: + forall ls eqs l v, + equations_hold ls eqs -> + equations_hold (Locmap.set l v ls) (kill_loc l eqs). +Proof. + intros; red; intros. + exploit In_kill_loc; eauto. intros [A [B C]]. + repeat rewrite Locmap.gso; auto; apply Loc.diff_sym; auto. +Qed. + +Lemma In_kill_locs: + forall e ll eqs, + In e (kill_locs ll eqs) -> + In e eqs /\ Loc.notin (S (e_slot e)) ll /\ Loc.notin (R (e_reg e)) ll. +Proof. +Opaque Loc.diff. + induction ll; simpl; intros. + tauto. + exploit IHll; eauto. intros [A [B C]]. exploit In_kill_loc; eauto. intros [D [E F]]. + tauto. +Qed. + +Lemma kill_locs_hold: + forall ll ls eqs, + equations_hold ls eqs -> + equations_hold (Locmap.undef ll ls) (kill_locs ll eqs). +Proof. + intros; red; intros. exploit In_kill_locs; eauto. intros [A [B C]]. + repeat rewrite Locmap.guo; auto. +Qed. + +Lemma kill_temps_hold: + forall ls eqs, + equations_hold ls eqs -> + equations_hold (LTL.undef_temps ls) (kill_temps eqs). +Proof. + exact (kill_locs_hold temporaries). +Qed. + +Lemma kill_at_move_hold: + forall ls eqs, + equations_hold ls eqs -> + equations_hold (undef_setstack ls) (kill_at_move eqs). +Proof. + exact (kill_locs_hold destroyed_at_move). +Qed. + +Lemma kill_at_op_hold: + forall op ls eqs, + equations_hold ls eqs -> + equations_hold (undef_op op ls) (kill_op op eqs). +Proof. + intros op. + destruct op; exact kill_temps_hold || exact kill_at_move_hold. +Qed. + +Lemma eqs_getstack_hold: + forall rs r s eqs, + equations_hold rs eqs -> + equations_hold (Locmap.set (R r) (rs (S s)) rs) + (mkeq r s :: kill_loc (R r) eqs). +Proof. +Transparent Loc.diff. + intros; red; intros. simpl in H0; destruct H0. + subst e. simpl. rewrite Locmap.gss; rewrite Locmap.gso; auto. red; auto. + exploit In_kill_loc; eauto. intros [D [E F]]. + repeat rewrite Locmap.gso. auto. + apply Loc.diff_sym; auto. apply Loc.diff_sym; auto. +Qed. + +Lemma eqs_movestack_hold: + forall rs r s eqs, + equations_hold rs eqs -> + equations_hold (Locmap.set (R r) (rs (S s)) (undef_setstack rs)) + (kill_at_move (mkeq r s :: kill_loc (R r) eqs)). +Proof. + unfold undef_setstack, kill_at_move; intros; red; intros. + exploit In_kill_locs; eauto. intros [A [B C]]. + simpl in A; destruct A. + subst e. rewrite Locmap.gss. rewrite Locmap.gso. apply Locmap.guo. auto. + simpl; auto. + exploit In_kill_loc; eauto. intros [D [E F]]. + repeat rewrite Locmap.gso. repeat rewrite Locmap.guo; auto. + apply Loc.diff_sym; auto. apply Loc.diff_sym; auto. +Qed. + +Lemma eqs_setstack_hold: + forall rs r s eqs, + equations_hold rs eqs -> + equations_hold (Locmap.set (S s) (rs (R r)) (undef_setstack rs)) + (kill_at_move (mkeq r s :: kill_loc (S s) eqs)). +Proof. + unfold undef_setstack, kill_at_move; intros; red; intros. + exploit In_kill_locs; eauto. intros [A [B C]]. + simpl in A; destruct A. + subst e. rewrite Locmap.gss. rewrite Locmap.gso. rewrite Locmap.guo. auto. + auto. simpl. destruct s; auto. + exploit In_kill_loc; eauto. intros [D [E F]]. + repeat rewrite Locmap.gso. repeat rewrite Locmap.guo; auto. + apply Loc.diff_sym; auto. apply Loc.diff_sym; auto. +Qed. + +Lemma locmap_set_reg_same: + forall rs r, + Locmap.set (R r) (rs (R r)) rs = rs. +Proof. + intros. apply extensionality; intros. + destruct (Loc.eq x (R r)). + subst x. apply Locmap.gss. + apply Locmap.gso. apply Loc.diff_reg_right; auto. +Qed. + +(** * Agreement between values of locations *) + +(** Values of locations may differ between the original and transformed + program: after a [Lgetstack] is optimized to a [Lop Omove], + the values of [destroyed_at_move] temporaries differ. This + can only happen in parts of the code where the [safe_move_insertion] + function returns [true]. *) + +Definition agree (sm: bool) (rs rs': locset) : Prop := + forall l, sm = false \/ Loc.notin l destroyed_at_move -> rs' l = rs l. + +Lemma agree_false: + forall rs rs', + agree false rs rs' <-> rs' = rs. +Proof. + intros; split; intros. + apply extensionality; intros. auto. + subst rs'. red; auto. +Qed. + +Lemma agree_slot: + forall sm rs rs' s, + agree sm rs rs' -> rs' (S s) = rs (S s). +Proof. +Transparent Loc.diff. + intros. apply H. right. simpl; destruct s; tauto. +Qed. + +Lemma agree_reg: + forall sm rs rs' r, + agree sm rs rs' -> + sm = false \/ ~In r destroyed_at_move_regs -> rs' (R r) = rs (R r). +Proof. + intros. apply H. destruct H0; auto. right. + simpl in H0; simpl; intuition congruence. +Qed. + +Lemma agree_regs: + forall sm rs rs' rl, + agree sm rs rs' -> + sm = false \/ list_disjoint rl destroyed_at_move_regs -> reglist rs' rl = reglist rs rl. +Proof. + induction rl; intros; simpl. + auto. + decEq. apply agree_reg with sm; auto. + destruct H0; auto. + right. eapply list_disjoint_notin; eauto with coqlib. + apply IHrl; auto. destruct H0; auto. right. eapply list_disjoint_cons_left; eauto. +Qed. + +Lemma agree_set: + forall sm rs rs' l v, + agree sm rs rs' -> + agree sm (Locmap.set l v rs) (Locmap.set l v rs'). +Proof. + intros; red; intros. + unfold Locmap.set. + destruct (Loc.eq l l0). auto. + destruct (Loc.overlap l l0). auto. + apply H; auto. +Qed. + +Lemma agree_undef_move_1: + forall sm rs rs', + agree sm rs rs' -> + agree true rs (undef_setstack rs'). +Proof. + intros. unfold undef_setstack. red; intros. + destruct H0. congruence. rewrite Locmap.guo; auto. +Qed. + +Remark locmap_undef_equal: + forall x ll rs rs', + (forall l, Loc.notin l ll -> rs' l = rs l) -> + Locmap.undef ll rs' x = Locmap.undef ll rs x. +Proof. + induction ll; intros; simpl. + apply H. simpl. auto. + apply IHll. intros. unfold Locmap.set. + destruct (Loc.eq a l). auto. destruct (Loc.overlap a l) as []_eqn. auto. + apply H. simpl. split; auto. apply Loc.diff_sym. apply Loc.non_overlap_diff; auto. +Qed. + +Lemma agree_undef_move_2: + forall sm rs rs', + agree sm rs rs' -> + agree false (undef_setstack rs) (undef_setstack rs'). +Proof. + intros. rewrite agree_false. + apply extensionality; intros. unfold undef_setstack. apply locmap_undef_equal. auto. +Qed. + +Lemma agree_undef_temps: + forall sm rs rs', + agree sm rs rs' -> + agree false (LTL.undef_temps rs) (LTL.undef_temps rs'). +Proof. + intros. rewrite agree_false. + apply extensionality; intros. unfold LTL.undef_temps. apply locmap_undef_equal. + intros. apply H. right. simpl in H0; simpl; tauto. +Qed. + +Lemma agree_undef_op: + forall op sm rs rs', + agree sm rs rs' -> + agree false (undef_op op rs) (undef_op op rs'). +Proof. + intros op. + destruct op; exact agree_undef_temps || exact agree_undef_move_2. +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). +Proof. + induction c; simpl; intros. + auto. + destruct a; 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 (peq lbl l); simpl; auto. +Qed. + +(** * Semantic preservation *) + +Section PRESERVATION. + +Variable prog: program. +Let tprog := transf_program prog. + +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + Genv.find_funct_ptr tge v = Some (transf_fundef f). +Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog). + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (@Genv.find_symbol_transf _ _ _ transf_fundef prog). + +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof (@Genv.find_var_info_transf _ _ _ transf_fundef prog). + +Lemma sig_preserved: + forall f, funsig (transf_fundef f) = funsig f. +Proof. + destruct f; reflexivity. +Qed. + +Lemma find_function_translated: + forall ros rs fd, + find_function ge ros rs = Some fd -> + find_function tge ros rs = Some (transf_fundef fd). +Proof. + intros. destruct ros; simpl in *. + apply functions_translated; auto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge i). + apply function_ptr_translated; auto. + congruence. +Qed. + +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)). + +Inductive match_states: state -> state -> Prop := + | match_states_regular: + forall sm stk f sp c rs m stk' rs' eqs + (STK: list_forall2 match_frames stk stk') + (EQH: equations_hold rs' eqs) + (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) + | match_states_call: + forall stk f rs m stk' + (STK: list_forall2 match_frames stk stk'), + match_states (Callstate stk f rs m) + (Callstate stk' (transf_fundef f) rs m) + | match_states_return: + forall stk rs m stk' + (STK: list_forall2 match_frames stk stk'), + match_states (Returnstate stk rs m) + (Returnstate stk' rs m). + +Definition measure (S: state) : nat := + match S with + | State s f sp c rs m => List.length c + | _ => 0%nat + end. + +Remark match_parent_locset: + forall stk stk', + list_forall2 match_frames stk stk' -> + return_regs (parent_locset stk') = return_regs (parent_locset stk). +Proof. + intros. inv H; auto. inv H0; auto. +Qed. + +Theorem transf_step_correct: + forall S1 t S2, step ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + (exists S2', step tge S1' t S2' /\ match_states S2 S2') + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. +Proof. +Opaque destroyed_at_move_regs. + induction 1; intros; inv MS; simpl. +(** getstack *) + simpl in SAFE. + assert (SAFE': sm = false \/ ~In r destroyed_at_move_regs /\ safe_move_insertion b = true). + destruct (in_dec mreg_eq r destroyed_at_move_regs); simpl in SAFE; intuition congruence. + destruct (is_incoming sl) as []_eqn. + (* 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. + repeat rewrite UGS. + apply match_states_regular with sm; auto. + apply kill_loc_hold. apply kill_loc_hold; auto. + rewrite (agree_slot _ _ _ sl AG). apply agree_set. apply agree_set. auto. + tauto. + (* not incoming *) + assert (UGS: forall rs, undef_getstack sl rs = rs). + destruct sl; simpl in Heqb0; discriminate || auto. + unfold contains_equation. + destruct (in_dec eq_equation (mkeq r sl) eqs); simpl. + (* eliminated *) + right. split. omega. split. auto. rewrite UGS. + exploit EQH; eauto. simpl. intro EQ. + assert (EQ1: rs' (S sl) = rs (S sl)) by (eapply agree_slot; eauto). + assert (EQ2: rs' (R r) = rs (R r)) by (eapply agree_reg; eauto; tauto). + rewrite <- EQ1; rewrite EQ; rewrite EQ2. rewrite locmap_set_reg_same. + apply match_states_regular with sm; auto. tauto. + (* found an equation *) + destruct (find_reg_containing sl eqs) as [r'|]_eqn. + exploit EQH. eapply find_reg_containing_sound; eauto. + simpl; intro EQ. + (* turned into a move *) + destruct (safe_move_insertion b) as []_eqn. + left; econstructor; split. 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. + 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. + repeat rewrite UGS. + apply match_states_regular with sm; auto. + apply eqs_getstack_hold; auto. + rewrite (agree_slot _ _ _ sl AG). apply agree_set. auto. + tauto. + +(* setstack *) + left; econstructor; split. 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. + instantiate (1 := v). rewrite <- H. + rewrite (agree_regs _ _ _ args AG). + apply eval_operation_preserved. exact symbols_preserved. + 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. + apply kill_loc_hold; apply kill_at_op_hold; auto. + apply agree_set. eapply agree_undef_op; eauto. + +(* load *) + left; econstructor; split. + 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. + eauto. + apply match_states_regular with false; auto. + apply kill_loc_hold; apply kill_temps_hold; auto. + apply agree_set. eapply agree_undef_temps; eauto. + +(* store *) +Opaque list_disjoint_dec. + simpl in SAFE. + assert (sm = false \/ ~In src destroyed_at_move_regs /\ list_disjoint args destroyed_at_move_regs). + destruct SAFE. auto. right. + 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 (agree_regs _ _ _ args AG). + apply eval_addressing_preserved. exact symbols_preserved. + tauto. + rewrite (agree_reg _ _ _ src AG). + eauto. + tauto. + apply match_states_regular with false; auto. + apply kill_temps_hold; auto. + eapply agree_undef_temps; eauto. + +(* call *) + 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. + symmetry; apply sig_preserved. + constructor. constructor; auto. constructor. + +(* tailcall *) + 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. + symmetry; apply sig_preserved. eauto. + rewrite (match_parent_locset _ _ STK). constructor; auto. + +(* builtin *) + left; econstructor; split. + constructor. + rewrite (agree_regs _ _ _ args AG). + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + 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. + apply kill_loc_hold; apply kill_temps_hold; auto. + apply agree_set. eapply agree_undef_temps; eauto. + +(* annot *) + 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. + exact symbols_preserved. exact varinfo_preserved. + apply match_states_regular with false; auto. + rewrite agree_false; auto. + +(* label *) + left; econstructor; split. 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. + apply match_states_regular with false; auto. + apply nil_hold. + simpl in SAFE. destruct SAFE. subst sm. auto. congruence. + +(* cond true *) + generalize (transl_find_label lbl (fn_code f) nil). rewrite H0. simpl. intros. + left; econstructor; split. + 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. + apply match_states_regular with false; auto. + apply nil_hold. + eapply agree_undef_temps; eauto. + +(* cond false *) + left; econstructor; split. 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. + apply kill_temps_hold; auto. + eapply agree_undef_temps; eauto. + +(* jumptable *) + generalize (transl_find_label lbl (fn_code f) nil). rewrite H1. simpl. intros. + left; econstructor; split. 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. + apply nil_hold. + eapply agree_undef_temps; eauto. + +(* return *) + simpl in SAFE. destruct SAFE; try discriminate. subst sm. rewrite agree_false in AG. subst rs'. + left; econstructor; split. + constructor. simpl. eauto. + rewrite (match_parent_locset _ _ STK). + constructor; auto. + +(* internal *) + left; econstructor; split. + constructor. simpl; eauto. + simpl. apply match_states_regular with false; auto. apply nil_hold. rewrite agree_false; auto. + +(* external *) + left; econstructor; split. + econstructor. eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + auto. eauto. + constructor; auto. + +(* return *) + inv STK. inv H1. left; econstructor; split. constructor. + apply match_states_regular with false; auto. + apply nil_hold. + rewrite agree_false; auto. +Qed. + +Lemma transf_initial_states: + forall st1, initial_state prog st1 -> + exists st2, initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inversion H. + econstructor; split. + econstructor. + apply Genv.init_mem_transf; eauto. + rewrite symbols_preserved. eauto. + apply function_ptr_translated; eauto. + rewrite sig_preserved. auto. + econstructor; eauto. constructor. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> final_state st1 r -> final_state st2 r. +Proof. + intros. inv H0. inv H. inv STK. econstructor. auto. +Qed. + +Theorem transf_program_correct: + forward_simulation (Linear.semantics prog) (Linear.semantics tprog). +Proof. + eapply forward_simulation_opt. + eexact symbols_preserved. + eexact transf_initial_states. + eexact transf_final_states. + eexact transf_step_correct. +Qed. + +End PRESERVATION. diff --git a/backend/RREtyping.v b/backend/RREtyping.v new file mode 100644 index 0000000..2501c7f --- /dev/null +++ b/backend/RREtyping.v @@ -0,0 +1,109 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Proof of type preservation for the [RRE] pass. *) + +Require Import Coqlib. +Require Import AST. +Require Import Locations. +Require Import Linear. +Require Import Lineartyping. +Require Import Conventions. +Require Import RRE. +Require Import RREproof. + +Remark wt_cons: + forall f c i, wt_instr f i -> wt_code f c -> wt_code f (i::c). +Proof. + intros; red; intros. simpl in H1; destruct H1. congruence. auto. +Qed. + +Hint Constructors wt_instr : linearty. +Hint Resolve wt_cons: linearty. + +Definition wt_eqs (eqs: equations) := + forall e, In e eqs -> slot_type (e_slot e) = mreg_type (e_reg e). + +Lemma wt_eqs_nil: + wt_eqs nil. +Proof. red; simpl; tauto. Qed. + +Lemma wt_eqs_cons: + forall r s eqs, + slot_type s = mreg_type r -> wt_eqs eqs -> wt_eqs (mkeq r s :: eqs). +Proof. + intros; red; simpl; intros. destruct H1. subst; simpl; auto. auto. +Qed. + +Lemma wt_kill_loc: + forall l eqs, + wt_eqs eqs -> wt_eqs (kill_loc l eqs). +Proof. + intros; red; intros. exploit In_kill_loc; eauto. intros [A B]. auto. +Qed. + +Lemma wt_kill_locs: + forall ll eqs, + wt_eqs eqs -> wt_eqs (kill_locs ll eqs). +Proof. + intros; red; intros. exploit In_kill_locs; eauto. intros [A B]. auto. +Qed. + +Lemma wt_kill_temps: + forall eqs, wt_eqs eqs -> wt_eqs (kill_temps eqs). +Proof. + exact (wt_kill_locs temporaries). +Qed. + +Lemma wt_kill_at_move: + forall eqs, wt_eqs eqs -> wt_eqs (kill_at_move eqs). +Proof. + exact (wt_kill_locs destroyed_at_move). +Qed. + +Hint Resolve wt_eqs_nil wt_eqs_cons wt_kill_loc wt_kill_locs + wt_kill_temps wt_kill_at_move: linearty. + +Lemma wt_kill_op: + forall op eqs, wt_eqs eqs -> wt_eqs (kill_op op eqs). +Proof. + intros; destruct op; simpl; apply wt_kill_locs; auto. +Qed. + +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). +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. + destruct (is_incoming s) as []_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. + destruct (safe_move_insertion c); auto 10 with linearty. +Qed. + +Lemma program_typing_preserved: + forall p, wt_program p -> wt_program (transf_program p). +Proof. + intros. red; intros. exploit transform_program_function; eauto. + intros [f0 [A B]]. subst f. exploit H; eauto. intros WTFD. + inv WTFD; simpl; constructor. red; simpl. + apply wt_transf_code; auto with linearty. +Qed. diff --git a/driver/Compiler.v b/driver/Compiler.v index 37a187e..abd3867 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -52,6 +52,7 @@ Require Tunneling. Require Linearize. Require CleanupLabels. Require Reload. +Require RRE. Require Stacking. Require Asmgen. (** Type systems. *) @@ -80,6 +81,8 @@ Require CleanupLabelsproof. Require CleanupLabelstyping. Require Reloadproof. Require Reloadtyping. +Require RREproof. +Require RREtyping. Require Stackingproof. Require Stackingtyping. Require Asmgenproof. @@ -150,6 +153,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := @@ CleanupLabels.transf_fundef @@ print print_LTLin @@ Reload.transf_fundef + @@ RRE.transf_fundef @@@ Stacking.transf_fundef @@ print print_Mach @@@ Asmgen.transf_fundef. @@ -327,13 +331,14 @@ Proof. unfold transf_rtl_program, transf_rtl_fundef in H. repeat TransfProgInv. repeat rewrite transform_program_print_identity in *. subst. - generalize (transform_partial_program_identity _ _ _ _ X0). intro EQ. subst. + generalize (transform_partial_program_identity _ _ _ _ X). intro EQ. subst. generalize Alloctyping.program_typing_preserved Tunnelingtyping.program_typing_preserved Linearizetyping.program_typing_preserved CleanupLabelstyping.program_typing_preserved Reloadtyping.program_typing_preserved + RREtyping.program_typing_preserved Stackingtyping.program_typing_preserved; intros. eapply compose_forward_simulation. apply Tailcallproof.transf_program_correct. @@ -345,6 +350,7 @@ Proof. eapply compose_forward_simulation. apply Linearizeproof.transf_program_correct. eassumption. eauto. eapply compose_forward_simulation. apply CleanupLabelsproof.transf_program_correct. eapply compose_forward_simulation. apply Reloadproof.transf_program_correct. eauto. + eapply compose_forward_simulation. apply RREproof.transf_program_correct. eauto. eapply compose_forward_simulation. apply Stackingproof.transf_program_correct. eassumption. eauto 8. apply Asmgenproof.transf_program_correct; eauto 10. split. auto. |