diff options
-rw-r--r-- | .depend | 8 | ||||
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | arm/ConstpropOp.v (renamed from arm/Constprop.v) | 213 | ||||
-rw-r--r-- | arm/ConstpropOpproof.v (renamed from arm/Constpropproof.v) | 502 | ||||
-rw-r--r-- | backend/Constprop.v | 235 | ||||
-rw-r--r-- | backend/Constpropproof.v | 445 | ||||
-rw-r--r-- | powerpc/ConstpropOp.v (renamed from powerpc/Constprop.v) | 220 | ||||
-rw-r--r-- | powerpc/ConstpropOpproof.v (renamed from powerpc/Constpropproof.v) | 478 |
8 files changed, 776 insertions, 1327 deletions
@@ -25,8 +25,8 @@ $(ARCH)/Asmgenproof.vo: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/E $(ARCH)/Asmgenretaddr.vo: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.vo: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asm.vo: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Conventions.vo -$(ARCH)/Constpropproof.vo: $(ARCH)/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/Constprop.vo -$(ARCH)/Constprop.vo: $(ARCH)/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo +$(ARCH)/ConstpropOpproof.vo: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo +$(ARCH)/ConstpropOp.vo: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo $(ARCH)/Machregs.vo: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/SelectOpproof.vo: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo @@ -39,6 +39,8 @@ backend/CminorSel.vo: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.v backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Mem.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo backend/Coloringproof.vo: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo backend/Coloring.vo: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/InterfGraph.vo +backend/Constpropproof.vo: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo +backend/Constprop.vo: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo backend/CSEproof.vo: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/CSE.vo backend/CSE.vo: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/InterfGraph.vo: backend/InterfGraph.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo backend/Registers.vo backend/Locations.vo @@ -88,5 +90,5 @@ cfrontend/Cshmgenproof3.vo: cfrontend/Cshmgenproof3.v lib/Coqlib.vo common/Error cfrontend/Cshmgen.vo: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csyntax.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Csyntax.vo: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Ctyping.vo: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo cfrontend/Csyntax.vo -driver/Compiler.vo: driver/Compiler.v 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/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo $(ARCH)/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/Ctyping.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/Cshmgenproof3.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo $(ARCH)/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2concr.vo $(ARCH)/Asmgenproof.vo +driver/Compiler.vo: driver/Compiler.v 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/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/Ctyping.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/Cshmgenproof3.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.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/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2concr.vo $(ARCH)/Asmgenproof.vo driver/Complements.vo: 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/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo @@ -53,7 +53,7 @@ BACKEND=\ Tailcall.v Tailcallproof.v \ RTLtyping.v \ Kildall.v \ - Constprop.v Constpropproof.v \ + ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ CSE.v CSEproof.v \ Machregs.v Locations.v Conventions.v LTL.v LTLtyping.v \ InterfGraph.v Coloring.v Coloringproof.v \ diff --git a/arm/Constprop.v b/arm/ConstpropOp.v index 154a5fc1..b5e5a03b 100644 --- a/arm/Constprop.v +++ b/arm/ConstpropOp.v @@ -10,22 +10,16 @@ (* *) (* *********************************************************************) -(** Constant propagation over RTL. This is the first of the two - optimizations performed at RTL level. It proceeds by a standard - dataflow analysis and the corresponding code transformation. *) +(** Static analysis and strength reduction for operators + and conditions. This is the machine-dependent part of [Constprop]. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Registers. -Require Import RTL. -Require Import Lattice. -Require Import Kildall. (** * Static analysis *) @@ -42,77 +36,6 @@ Inductive approx : Type := (** The value is the address of the given global symbol plus the given integer offset. *) -(** We equip this set of approximations with a semi-lattice structure. - The ordering is inclusion between the sets of values denoted by - the approximations. *) - -Module Approx <: SEMILATTICE_WITH_TOP. - Definition t := approx. - Definition eq (x y: t) := (x = y). - Definition eq_refl: forall x, eq x x := (@refl_equal t). - Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). - Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). - Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}. - Proof. - decide equality. - apply Int.eq_dec. - apply Float.eq_dec. - apply Int.eq_dec. - apply ident_eq. - Qed. - Definition beq (x y: t) := if eq_dec x y then true else false. - Lemma beq_correct: forall x y, beq x y = true -> x = y. - Proof. - unfold beq; intros. destruct (eq_dec x y). auto. congruence. - Qed. - Definition ge (x y: t) : Prop := - x = Unknown \/ y = Novalue \/ x = y. - Lemma ge_refl: forall x y, eq x y -> ge x y. - Proof. - unfold eq, ge; tauto. - Qed. - Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Proof. - unfold ge; intuition congruence. - Qed. - Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. - Proof. - unfold eq, ge; intros; congruence. - Qed. - Definition bot := Novalue. - Definition top := Unknown. - Lemma ge_bot: forall x, ge x bot. - Proof. - unfold ge, bot; tauto. - Qed. - Lemma ge_top: forall x, ge top x. - Proof. - unfold ge, bot; tauto. - Qed. - Definition lub (x y: t) : t := - if eq_dec x y then x else - match x, y with - | Novalue, _ => y - | _, Novalue => x - | _, _ => Unknown - end. - Lemma lub_commut: forall x y, eq (lub x y) (lub y x). - Proof. - unfold lub, eq; intros. - case (eq_dec x y); case (eq_dec y x); intros; try congruence. - destruct x; destruct y; auto. - Qed. - Lemma ge_lub_left: forall x y, ge (lub x y) x. - Proof. - unfold lub; intros. - case (eq_dec x y); intro. - apply ge_refl. apply eq_refl. - destruct x; destruct y; unfold ge; tauto. - Qed. -End Approx. - -Module D := LPMap Approx. - (** We now define the abstract interpretations of conditions and operators over this set of approximations. For instance, the abstract interpretation of the operator [Oaddf] applied to two expressions [a] and [b] is @@ -658,59 +581,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) := Unknown end. - -(** The transfer function for the dataflow analysis is straightforward: - for [Iop] instructions, we set the approximation of the destination - register to the result of executing abstractly the operation; - for [Iload] and [Icall], we set the approximation of the destination - to [Unknown]. *) - -Definition approx_regs (rl: list reg) (approx: D.t) := - List.map (fun r => D.get r approx) rl. - -Definition transfer (f: function) (pc: node) (before: D.t) := - match f.(fn_code)!pc with - | None => before - | Some i => - match i with - | Inop s => - before - | Iop op args res s => - let a := eval_static_operation op (approx_regs args before) in - D.set res a before - | Iload chunk addr args dst s => - D.set dst Unknown before - | Istore chunk addr args src s => - before - | Icall sig ros args res s => - D.set res Unknown before - | Itailcall sig ros args => - before - | Icond cond args ifso ifnot => - before - | Ireturn optarg => - before - end - 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 - to approximations. It can fail to reach a fixpoint in a reasonable - number of iterations, in which case [None] is returned. *) - -Module DS := Dataflow_Solver(D)(NodeSetForward). - -Definition analyze (f: RTL.function): PMap.t D.t := - match DS.fixpoint (successors f) (transfer f) - ((f.(fn_entrypoint), D.top) :: nil) with - | None => PMap.init D.top - | Some res => res - end. - -(** * Code transformation *) - -(** ** Operator strength reduction *) +(** * Operator strength reduction *) (** We now define auxiliary functions for strength reduction of operators and addressing modes: replacing an operator with a cheaper @@ -719,10 +590,10 @@ Definition analyze (f: RTL.function): PMap.t D.t := Section STRENGTH_REDUCTION. -Variable approx: D.t. +Variable app: reg -> approx. Definition intval (r: reg) : option int := - match D.get r approx with I n => Some n | _ => None end. + match app r with I n => Some n | _ => None end. (* Definition cond_strength_reduction (cond: condition) (args: list reg) := @@ -1159,77 +1030,3 @@ Definition addr_strength_reduction (addr: addressing) (args: list reg) := end. End STRENGTH_REDUCTION. - -(** ** Code transformation *) - -(** The code transformation proceeds instruction by instruction. - Operators whose arguments are all statically known are turned - into ``load integer constant'', ``load float constant'' or - ``load symbol address'' operations. Operators for which some - but not all arguments are known are subject to strength reduction, - and similarly for the addressing modes of load and store instructions. - Other instructions are unchanged. *) - -Definition transf_ros (approx: D.t) (ros: reg + ident) : reg + ident := - match ros with - | inl r => - match D.get r approx with - | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros - | _ => ros - end - | inr s => ros - end. - -Definition transf_instr (approx: D.t) (instr: instruction) := - match instr with - | Iop op args res s => - match eval_static_operation op (approx_regs args approx) with - | I n => - Iop (Ointconst n) nil res s - | F n => - Iop (Ofloatconst n) nil res s - | S symb ofs => - Iop (Oaddrsymbol symb ofs) nil res s - | _ => - let (op', args') := op_strength_reduction approx op args in - Iop op' args' res s - end - | Iload chunk addr args dst s => - let (addr', args') := addr_strength_reduction approx addr args in - Iload chunk addr' args' dst s - | Istore chunk addr args src s => - let (addr', args') := addr_strength_reduction approx addr args in - Istore chunk addr' args' src s - | Icall sig ros args res s => - Icall sig (transf_ros approx ros) args res s - | Itailcall sig ros args => - Itailcall sig (transf_ros approx ros) args - | Icond cond args s1 s2 => - match eval_static_condition cond (approx_regs args approx) with - | Some b => - if b then Inop s1 else Inop s2 - | None => - let (cond', args') := cond_strength_reduction approx cond args in - Icond cond' args' s1 s2 - end - | _ => - instr - end. - -Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code := - PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs. - -Definition transf_function (f: function) : function := - let approxs := analyze f in - mkfunction - f.(fn_sig) - f.(fn_params) - f.(fn_stacksize) - (transf_code approxs f.(fn_code)) - f.(fn_entrypoint). - -Definition transf_fundef (fd: fundef) : fundef := - AST.transf_fundef transf_function fd. - -Definition transf_program (p: program) : program := - transform_program transf_fundef p. diff --git a/arm/Constpropproof.v b/arm/ConstpropOpproof.v index a3e2b82b..70fc606c 100644 --- a/arm/Constpropproof.v +++ b/arm/ConstpropOpproof.v @@ -10,23 +10,19 @@ (* *) (* *********************************************************************) -(** Correctness proof for constant propagation. *) +(** Correctness proof for constant propagation (processor-dependent part). *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Events. Require Import Mem. Require Import Globalenvs. -Require Import Smallstep. Require Import Op. Require Import Registers. Require Import RTL. -Require Import Lattice. -Require Import Kildall. +Require Import ConstpropOp. Require Import Constprop. (** * Correctness of the static analysis *) @@ -51,16 +47,6 @@ Definition val_match_approx (a: approx) (v: val) : Prop := | _ => False end. -Definition regs_match_approx (a: D.t) (rs: regset) : Prop := - forall r, val_match_approx (D.get r a) rs#r. - -Lemma regs_match_approx_top: - forall rs, regs_match_approx D.top rs. -Proof. - intros. red; intros. simpl. rewrite PTree.gempty. - unfold Approx.top, val_match_approx. auto. -Qed. - Lemma val_match_approx_increasing: forall a1 a2 v, Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v. @@ -72,26 +58,6 @@ Proof. subst a2. auto. Qed. -Lemma regs_match_approx_increasing: - forall a1 a2 rs, - D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs. -Proof. - unfold D.ge, regs_match_approx. intros. - apply val_match_approx_increasing with (D.get r a2); auto. -Qed. - -Lemma regs_match_approx_update: - forall ra rs a v r, - val_match_approx a v -> - regs_match_approx ra rs -> - regs_match_approx (D.set r a ra) (rs#r <- v). -Proof. - intros; red; intros. rewrite Regmap.gsspec. - case (peq r0 r); intro. - subst r0. rewrite D.gss. auto. - rewrite D.gso; auto. -Qed. - Inductive val_list_match_approx: list approx -> list val -> Prop := | vlma_nil: val_list_match_approx nil nil @@ -101,16 +67,6 @@ Inductive val_list_match_approx: list approx -> list val -> Prop := val_list_match_approx al vl -> val_list_match_approx (a :: al) (v :: vl). -Lemma approx_regs_val_list: - forall ra rs rl, - regs_match_approx ra rs -> - val_list_match_approx (approx_regs rl ra) rs##rl. -Proof. - induction rl; simpl; intros. - constructor. - constructor. apply H. auto. -Qed. - Ltac SimplVMA := match goal with | H: (val_match_approx (I _) ?v) |- _ => @@ -208,42 +164,6 @@ Proof. auto. Qed. -(** The correctness of the static analysis follows from the results - above and the fact that the result of the static analysis is - a solution of the forward dataflow inequations. *) - -Lemma analyze_correct_1: - forall f pc rs pc' i, - f.(fn_code)!pc = Some i -> - In pc' (successors_instr i) -> - regs_match_approx (transfer f pc (analyze f)!!pc) rs -> - regs_match_approx (analyze f)!!pc' rs. -Proof. - intros until i. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. - apply regs_match_approx_increasing with (transfer f pc approxs!!pc). - eapply DS.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto. - auto. - intros. rewrite PMap.gi. apply regs_match_approx_top. -Qed. - -Lemma analyze_correct_3: - forall f rs, - regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs. -Proof. - intros. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. - apply regs_match_approx_increasing with D.top. - eapply DS.fixpoint_entry; eauto. auto with coqlib. - apply regs_match_approx_top. - intros. rewrite PMap.gi. apply regs_match_approx_top. -Qed. - (** * Correctness of strength reduction *) (** We now show that strength reduction over operators and addressing @@ -254,49 +174,49 @@ Qed. Section STRENGTH_REDUCTION. -Variable approx: D.t. +Variable app: reg -> approx. Variable sp: val. Variable rs: regset. -Hypothesis MATCH: regs_match_approx approx rs. +Hypothesis MATCH: forall r, val_match_approx (app r) rs#r. Lemma intval_correct: forall r n, - intval approx r = Some n -> rs#r = Vint n. + intval app r = Some n -> rs#r = Vint n. Proof. intros until n. - unfold intval. caseEq (D.get r approx); intros; try discriminate. + unfold intval. caseEq (app r); intros; try discriminate. generalize (MATCH r). unfold val_match_approx. rewrite H. congruence. Qed. Lemma cond_strength_reduction_correct: forall cond args, - let (cond', args') := cond_strength_reduction approx cond args in + let (cond', args') := cond_strength_reduction app cond args in eval_condition cond' rs##args' = eval_condition cond rs##args. Proof. intros. unfold cond_strength_reduction. case (cond_strength_reduction_match cond args); intros. - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. simpl. rewrite (intval_correct _ _ H). destruct (rs#r2); auto. rewrite Int.swap_cmp. auto. destruct c; reflexivity. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H0). auto. auto. - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. simpl. rewrite (intval_correct _ _ H). destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H0). auto. auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H). auto. auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H). auto. auto. @@ -424,24 +344,24 @@ Qed. Lemma op_strength_reduction_correct: forall op args v, - let (op', args') := op_strength_reduction approx op args in + let (op', args') := op_strength_reduction app op args in eval_operation ge sp op rs##args = Some v -> eval_operation ge sp op' rs##args' = Some v. Proof. intros; unfold op_strength_reduction; case (op_strength_reduction_match op args); intros; simpl List.map. (* Oadd *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil)) with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)). apply make_addimm_correct. simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). apply make_addimm_correct. assumption. (* Oaddshift *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil)) with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil)). @@ -449,10 +369,10 @@ Proof. simpl. destruct rs#r1; auto. assumption. (* Osub *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H) in H0. simpl in *. destruct rs#r2; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil)) with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)). @@ -460,7 +380,7 @@ Proof. simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. assumption. (* Osubshift *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil)) with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil)). @@ -468,23 +388,23 @@ Proof. simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. assumption. (* Orsubshift *) - caseEq (intval approx r2). intros n H. + caseEq (intval app r2). intros n H. rewrite (intval_correct _ _ H). simpl. destruct rs#r1; auto. auto. (* Omul *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil)) with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)). apply make_mulimm_correct. apply intval_correct; auto. simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). apply make_mulimm_correct. apply intval_correct; auto. assumption. (* Odivu *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. caseEq (Int.is_power2 i); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil)) @@ -499,107 +419,99 @@ Proof. assumption. assumption. (* Oand *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil)) with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)). apply make_andimm_correct. simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). apply make_andimm_correct. assumption. (* Oandshift *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil)) with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil)). apply make_andimm_correct. reflexivity. assumption. (* Oor *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil)) with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)). apply make_orimm_correct. simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). apply make_orimm_correct. assumption. (* Oorshift *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil)) with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil)). apply make_orimm_correct. reflexivity. assumption. (* Oxor *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil)) with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)). apply make_xorimm_correct. simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). apply make_xorimm_correct. assumption. (* Oxorshift *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil)) with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil)). apply make_xorimm_correct. reflexivity. assumption. (* Obic *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil)) with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil)). apply make_andimm_correct. reflexivity. assumption. (* Obicshift *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil)) with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil)). apply make_andimm_correct. reflexivity. assumption. (* Oshl *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. caseEq (Int.ltu i (Int.repr 32)); intros. rewrite (intval_correct _ _ H). apply make_shlimm_correct. assumption. assumption. (* Oshr *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. caseEq (Int.ltu i (Int.repr 32)); intros. rewrite (intval_correct _ _ H). apply make_shrimm_correct. assumption. assumption. (* Oshru *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. caseEq (Int.ltu i (Int.repr 32)); intros. rewrite (intval_correct _ _ H). apply make_shruimm_correct. assumption. assumption. (* Ocmp *) generalize (cond_strength_reduction_correct c rl). - destruct (cond_strength_reduction approx c rl). + destruct (cond_strength_reduction app c rl). simpl. intro. rewrite H. auto. (* default *) assumption. Qed. - -Ltac KnownApprox := - match goal with - | MATCH: (regs_match_approx ?approx ?rs), - H: (D.get ?r ?approx = ?a) |- _ => - generalize (MATCH r); rewrite H; intro; clear H; KnownApprox - | _ => idtac - end. Lemma addr_strength_reduction_correct: forall addr args, - let (addr', args') := addr_strength_reduction approx addr args in + let (addr', args') := addr_strength_reduction app addr args in eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args. Proof. intros. @@ -608,15 +520,15 @@ Proof. case (addr_strength_reduction_match addr args); intros. (* Aindexed2 *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. simpl; rewrite (intval_correct _ _ H). destruct rs#r2; auto. rewrite Int.add_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. simpl; rewrite (intval_correct _ _ H0). auto. auto. (* Aindexed2shift *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. simpl; rewrite (intval_correct _ _ H). auto. auto. @@ -627,331 +539,3 @@ Qed. End STRENGTH_REDUCTION. End ANALYSIS. - -(** * Correctness of the code transformation *) - -(** We now show that the transformed code after constant propagation - has the same semantics as the original code. *) - -Section PRESERVATION. - -Variable prog: program. -Let tprog := transf_program prog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.find_symbol_transf. -Qed. - -Lemma functions_translated: - forall (v: val) (f: fundef), - Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (transf_fundef f). -Proof. - intros. - exact (Genv.find_funct_transf transf_fundef H). -Qed. - -Lemma function_ptr_translated: - forall (b: block) (f: fundef), - Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (transf_fundef f). -Proof. - intros. - exact (Genv.find_funct_ptr_transf transf_fundef H). -Qed. - -Lemma sig_function_translated: - forall f, - funsig (transf_fundef f) = funsig f. -Proof. - intros. destruct f; reflexivity. -Qed. - -Lemma transf_ros_correct: - forall ros rs f approx, - regs_match_approx ge approx rs -> - find_function ge ros rs = Some f -> - find_function tge (transf_ros approx ros) rs = Some (transf_fundef f). -Proof. - intros until approx; intro MATCH. - destruct ros; simpl. - intro. - exploit functions_translated; eauto. intro FIND. - caseEq (D.get r approx); intros; auto. - generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto. - generalize (MATCH r). rewrite H0. intros [b [A B]]. - rewrite <- symbols_preserved in A. - rewrite B in FIND. rewrite H1 in FIND. - rewrite Genv.find_funct_find_funct_ptr in FIND. - simpl. rewrite A. auto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i). - intro. apply function_ptr_translated. auto. - congruence. -Qed. - -(** The proof of semantic preservation is a simulation argument - based on diagrams of the following form: -<< - st1 --------------- st2 - | | - t| |t - | | - v v - st1'--------------- st2' ->> - The left vertical arrow represents a transition in the - original RTL code. The top horizontal bar is the [match_states] - invariant between the initial state [st1] in the original RTL code - and an initial state [st2] in the transformed code. - This invariant expresses that all code fragments appearing in [st2] - are obtained by [transf_code] transformation of the corresponding - fragments in [st1]. Moreover, the values of registers in [st1] - must match their compile-time approximations at the current program - point. - These two parts of the diagram are the hypotheses. In conclusions, - we want to prove the other two parts: the right vertical arrow, - which is a transition in the transformed RTL code, and the bottom - horizontal bar, which means that the [match_state] predicate holds - between the final states [st1'] and [st2']. *) - -Inductive match_stackframes: stackframe -> stackframe -> Prop := - match_stackframe_intro: - forall res c sp pc rs f, - c = f.(RTL.fn_code) -> - (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) -> - match_stackframes - (Stackframe res c sp pc rs) - (Stackframe res (transf_code (analyze f) c) sp pc rs). - -Inductive match_states: state -> state -> Prop := - | match_states_intro: - forall s c sp pc rs m f s' - (CF: c = f.(RTL.fn_code)) - (MATCH: regs_match_approx ge (analyze f)!!pc rs) - (STACKS: list_forall2 match_stackframes s s'), - match_states (State s c sp pc rs m) - (State s' (transf_code (analyze f) c) sp pc rs m) - | match_states_call: - forall s f args m s', - list_forall2 match_stackframes s s' -> - match_states (Callstate s f args m) - (Callstate s' (transf_fundef f) args m) - | match_states_return: - forall s s' v m, - list_forall2 match_stackframes s s' -> - match_states (Returnstate s v m) - (Returnstate s' v m). - -Ltac TransfInstr := - match goal with - | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ => - cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr)); - [ simpl - | unfold transf_code; rewrite PTree.gmap; - unfold option_map; rewrite H1; reflexivity ] - end. - -(** The proof of simulation proceeds by case analysis on the transition - taken in the source code. *) - -Lemma 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'. -Proof. - induction 1; intros; inv MS. - - (* Inop *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split. - TransfInstr; intro. eapply exec_Inop; eauto. - econstructor; eauto. - eapply analyze_correct_1 with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. auto. - - (* Iop *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. - TransfInstr. caseEq (op_strength_reduction (analyze f)!!pc op args); - intros op' args' OSR. - assert (eval_operation tge sp op' rs##args' = Some v). - rewrite (eval_operation_preserved symbols_preserved). - generalize (op_strength_reduction_correct ge (analyze f)!!pc sp rs - MATCH op args v). - rewrite OSR; simpl. auto. - generalize (eval_static_operation_correct ge op sp - (approx_regs args (analyze f)!!pc) rs##args v - (approx_regs_val_list _ _ _ args MATCH) H0). - case (eval_static_operation op (approx_regs args (analyze f)!!pc)); intros; - simpl in H2; - eapply exec_Iop; eauto; simpl. - congruence. - congruence. - elim H2; intros b [A B]. rewrite symbols_preserved. - rewrite A; rewrite B; auto. - econstructor; eauto. - eapply analyze_correct_1 with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. - eapply eval_static_operation_correct; eauto. - apply approx_regs_val_list; auto. - - (* Iload *) - caseEq (addr_strength_reduction (analyze f)!!pc addr args); - intros addr' args' ASR. - assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved symbols_preserved). - generalize (addr_strength_reduction_correct ge (analyze f)!!pc sp rs - MATCH addr args). - rewrite ASR; simpl. congruence. - TransfInstr. rewrite ASR. intro. - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split. - eapply exec_Iload; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. simpl; auto. - - (* Istore *) - caseEq (addr_strength_reduction (analyze f)!!pc addr args); - intros addr' args' ASR. - assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved symbols_preserved). - generalize (addr_strength_reduction_correct ge (analyze f)!!pc sp rs - MATCH addr args). - rewrite ASR; simpl. congruence. - TransfInstr. rewrite ASR. intro. - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split. - eapply exec_Istore; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. auto. - - (* Icall *) - exploit transf_ros_correct; eauto. intro FIND'. - TransfInstr; intro. - econstructor; split. - eapply exec_Icall; eauto. apply sig_function_translated; auto. - constructor; auto. constructor; auto. - econstructor; eauto. - intros. eapply analyze_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. simpl. auto. - - (* Itailcall *) - exploit transf_ros_correct; eauto. intros FIND'. - TransfInstr; intro. - econstructor; split. - eapply exec_Itailcall; eauto. apply sig_function_translated; auto. - constructor; auto. - - (* Icond, true *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. - caseEq (cond_strength_reduction (analyze f)!!pc cond args); - intros cond' args' CSR. - assert (eval_condition cond' rs##args' = Some true). - generalize (cond_strength_reduction_correct - ge (analyze f)!!pc rs MATCH cond args). - rewrite CSR. intro. congruence. - TransfInstr. rewrite CSR. - caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)). - intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ _ - (approx_regs_val_list _ _ _ args MATCH) ESC); intro. - replace b with true. intro; eapply exec_Inop; eauto. congruence. - intros. eapply exec_Icond_true; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. - - (* Icond, false *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. - caseEq (cond_strength_reduction (analyze f)!!pc cond args); - intros cond' args' CSR. - assert (eval_condition cond' rs##args' = Some false). - generalize (cond_strength_reduction_correct - ge (analyze f)!!pc rs MATCH cond args). - rewrite CSR. intro. congruence. - TransfInstr. rewrite CSR. - caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)). - intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ _ - (approx_regs_val_list _ _ _ args MATCH) ESC); intro. - replace b with false. intro; eapply exec_Inop; eauto. congruence. - intros. eapply exec_Icond_false; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. - - (* Ireturn *) - exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split. - eapply exec_Ireturn; eauto. TransfInstr; auto. - constructor; auto. - - (* internal function *) - simpl. unfold transf_function. - econstructor; split. - eapply exec_function_internal; simpl; eauto. - simpl. econstructor; eauto. - apply analyze_correct_3; auto. - - (* external function *) - simpl. econstructor; split. - eapply exec_function_external; eauto. - constructor; auto. - - (* return *) - inv H3. inv H1. - econstructor; split. - eapply exec_return; eauto. - econstructor; eauto. -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. - exploit function_ptr_translated; eauto. intro FIND. - exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. - econstructor; eauto. - replace (prog_main tprog) with (prog_main prog). - rewrite symbols_preserved. eauto. - reflexivity. - rewrite <- H2. apply sig_function_translated. - replace (Genv.init_mem tprog) with (Genv.init_mem prog). - constructor. constructor. auto. - symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. -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 H4. constructor. -Qed. - -(** The preservation of the observable behavior of the program then - follows, using the generic preservation theorem - [Smallstep.simulation_step_preservation]. *) - -Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - exec_program prog beh -> exec_program tprog beh. -Proof. - unfold exec_program; intros. - eapply simulation_step_preservation; eauto. - eexact transf_initial_states. - eexact transf_final_states. - exact transf_step_correct. -Qed. - -End PRESERVATION. diff --git a/backend/Constprop.v b/backend/Constprop.v new file mode 100644 index 00000000..cccce9a3 --- /dev/null +++ b/backend/Constprop.v @@ -0,0 +1,235 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Constant propagation over RTL. This is one of the optimizations + performed at RTL level. It proceeds by a standard dataflow analysis + and the corresponding code rewriting. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Globalenvs. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import Lattice. +Require Import Kildall. +Require Import ConstpropOp. + +(** * Static analysis *) + +(** The type [approx] of compile-time approximations of values is + defined in the machine-dependent part [ConstpropOp]. *) + +(** We equip this type of approximations with a semi-lattice structure. + The ordering is inclusion between the sets of values denoted by + the approximations. *) + +Module Approx <: SEMILATTICE_WITH_TOP. + Definition t := approx. + Definition eq (x y: t) := (x = y). + Definition eq_refl: forall x, eq x x := (@refl_equal t). + Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). + Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}. + Proof. + decide equality. + apply Int.eq_dec. + apply Float.eq_dec. + apply Int.eq_dec. + apply ident_eq. + Qed. + Definition beq (x y: t) := if eq_dec x y then true else false. + Lemma beq_correct: forall x y, beq x y = true -> x = y. + Proof. + unfold beq; intros. destruct (eq_dec x y). auto. congruence. + Qed. + Definition ge (x y: t) : Prop := + x = Unknown \/ y = Novalue \/ x = y. + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge; tauto. + Qed. + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge; intuition congruence. + Qed. + Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. + Proof. + unfold eq, ge; intros; congruence. + Qed. + Definition bot := Novalue. + Definition top := Unknown. + Lemma ge_bot: forall x, ge x bot. + Proof. + unfold ge, bot; tauto. + Qed. + Lemma ge_top: forall x, ge top x. + Proof. + unfold ge, bot; tauto. + Qed. + Definition lub (x y: t) : t := + if eq_dec x y then x else + match x, y with + | Novalue, _ => y + | _, Novalue => x + | _, _ => Unknown + end. + Lemma lub_commut: forall x y, eq (lub x y) (lub y x). + Proof. + unfold lub, eq; intros. + case (eq_dec x y); case (eq_dec y x); intros; try congruence. + destruct x; destruct y; auto. + Qed. + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold lub; intros. + case (eq_dec x y); intro. + apply ge_refl. apply eq_refl. + destruct x; destruct y; unfold ge; tauto. + Qed. +End Approx. + +Module D := LPMap Approx. + +(** The transfer function for the dataflow analysis is straightforward: + for [Iop] instructions, we set the approximation of the destination + register to the result of executing abstractly the operation; + for [Iload] and [Icall], we set the approximation of the destination + to [Unknown]. *) + +Definition approx_reg (app: D.t) (r: reg) := + D.get r app. + +Definition approx_regs (app: D.t) (rl: list reg):= + List.map (approx_reg app) rl. + +Definition transfer (f: function) (pc: node) (before: D.t) := + match f.(fn_code)!pc with + | None => before + | Some i => + match i with + | Inop s => + before + | Iop op args res s => + let a := eval_static_operation op (approx_regs before args) in + D.set res a before + | Iload chunk addr args dst s => + D.set dst Unknown before + | Istore chunk addr args src s => + before + | Icall sig ros args res s => + D.set res Unknown before + | Itailcall sig ros args => + before +(* + | Ialloc arg res s => + D.set res Unknown before +*) + | Icond cond args ifso ifnot => + before + | Ireturn optarg => + before + end + 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 + to approximations. It can fail to reach a fixpoint in a reasonable + number of iterations, in which case [None] is returned. *) + +Module DS := Dataflow_Solver(D)(NodeSetForward). + +Definition analyze (f: RTL.function): PMap.t D.t := + match DS.fixpoint (successors f) (transfer f) + ((f.(fn_entrypoint), D.top) :: nil) with + | None => PMap.init D.top + | Some res => res + end. + +(** * Code transformation *) + +(** The code transformation proceeds instruction by instruction. + Operators whose arguments are all statically known are turned + into ``load integer constant'', ``load float constant'' or + ``load symbol address'' operations. Operators for which some + but not all arguments are known are subject to strength reduction, + and similarly for the addressing modes of load and store instructions. + Other instructions are unchanged. *) + +Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident := + match ros with + | inl r => + match D.get r app with + | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros + | _ => ros + end + | inr s => ros + end. + +Definition transf_instr (app: D.t) (instr: instruction) := + match instr with + | Iop op args res s => + match eval_static_operation op (approx_regs app args) with + | I n => + Iop (Ointconst n) nil res s + | F n => + Iop (Ofloatconst n) nil res s + | S symb ofs => + Iop (Oaddrsymbol symb ofs) nil res s + | _ => + let (op', args') := op_strength_reduction (approx_reg app) op args in + Iop op' args' res s + end + | Iload chunk addr args dst s => + let (addr', args') := addr_strength_reduction (approx_reg app) addr args in + Iload chunk addr' args' dst s + | Istore chunk addr args src s => + let (addr', args') := addr_strength_reduction (approx_reg app) addr args in + Istore chunk addr' args' src s + | Icall sig ros args res s => + Icall sig (transf_ros app ros) args res s + | Itailcall sig ros args => + Itailcall sig (transf_ros app ros) args + | Icond cond args s1 s2 => + match eval_static_condition cond (approx_regs app args) with + | Some b => + if b then Inop s1 else Inop s2 + | None => + let (cond', args') := cond_strength_reduction (approx_reg app) cond args in + Icond cond' args' s1 s2 + end + | _ => + instr + end. + +Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code := + PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs. + +Definition transf_function (f: function) : function := + let approxs := analyze f in + mkfunction + f.(fn_sig) + f.(fn_params) + f.(fn_stacksize) + (transf_code approxs f.(fn_code)) + f.(fn_entrypoint). + +Definition transf_fundef (fd: fundef) : fundef := + AST.transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v new file mode 100644 index 00000000..e628d426 --- /dev/null +++ b/backend/Constpropproof.v @@ -0,0 +1,445 @@ +(* *********************************************************************) +(* *) +(* 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 constant propagation. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Events. +Require Import Mem. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import Lattice. +Require Import Kildall. +Require Import ConstpropOp. +Require Import Constprop. +Require Import ConstpropOpproof. + +(** * Correctness of the static analysis *) + +Section ANALYSIS. + +Variable ge: genv. + +Definition regs_match_approx (a: D.t) (rs: regset) : Prop := + forall r, val_match_approx ge (D.get r a) rs#r. + +Lemma regs_match_approx_top: + forall rs, regs_match_approx D.top rs. +Proof. + intros. red; intros. simpl. rewrite PTree.gempty. + unfold Approx.top, val_match_approx. auto. +Qed. + +Lemma regs_match_approx_increasing: + forall a1 a2 rs, + D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs. +Proof. + unfold D.ge, regs_match_approx. intros. + apply val_match_approx_increasing with (D.get r a2); auto. +Qed. + +Lemma regs_match_approx_update: + forall ra rs a v r, + val_match_approx ge a v -> + regs_match_approx ra rs -> + regs_match_approx (D.set r a ra) (rs#r <- v). +Proof. + intros; red; intros. rewrite Regmap.gsspec. + case (peq r0 r); intro. + subst r0. rewrite D.gss. auto. + rewrite D.gso; auto. +Qed. + +Lemma approx_regs_val_list: + forall ra rs rl, + regs_match_approx ra rs -> + val_list_match_approx ge (approx_regs ra rl) rs##rl. +Proof. + induction rl; simpl; intros. + constructor. + constructor. apply H. 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. *) + +Lemma analyze_correct_1: + forall f pc rs pc' i, + f.(fn_code)!pc = Some i -> + In pc' (successors_instr i) -> + regs_match_approx (transfer f pc (analyze f)!!pc) rs -> + regs_match_approx (analyze f)!!pc' rs. +Proof. + intros until i. unfold analyze. + caseEq (DS.fixpoint (successors f) (transfer f) + ((fn_entrypoint f, D.top) :: nil)). + intros approxs; intros. + apply regs_match_approx_increasing with (transfer f pc approxs!!pc). + eapply DS.fixpoint_solution; eauto. + unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto. + auto. + intros. rewrite PMap.gi. apply regs_match_approx_top. +Qed. + +Lemma analyze_correct_3: + forall f rs, + regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs. +Proof. + intros. unfold analyze. + caseEq (DS.fixpoint (successors f) (transfer f) + ((fn_entrypoint f, D.top) :: nil)). + intros approxs; intros. + apply regs_match_approx_increasing with D.top. + eapply DS.fixpoint_entry; eauto. auto with coqlib. + apply regs_match_approx_top. + intros. rewrite PMap.gi. apply regs_match_approx_top. +Qed. + +End ANALYSIS. + +(** * Correctness of the code transformation *) + +(** We now show that the transformed code after constant propagation + has the same semantics as the original code. *) + +Section PRESERVATION. + +Variable prog: program. +Let tprog := transf_program prog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + intros; unfold ge, tge, tprog, transf_program. + apply Genv.find_symbol_transf. +Qed. + +Lemma functions_translated: + forall (v: val) (f: fundef), + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof. + intros. + exact (Genv.find_funct_transf transf_fundef H). +Qed. + +Lemma function_ptr_translated: + forall (b: block) (f: fundef), + Genv.find_funct_ptr ge b = Some f -> + Genv.find_funct_ptr tge b = Some (transf_fundef f). +Proof. + intros. + exact (Genv.find_funct_ptr_transf transf_fundef H). +Qed. + +Lemma sig_function_translated: + forall f, + funsig (transf_fundef f) = funsig f. +Proof. + intros. destruct f; reflexivity. +Qed. + +Lemma transf_ros_correct: + forall ros rs f approx, + regs_match_approx ge approx rs -> + find_function ge ros rs = Some f -> + find_function tge (transf_ros approx ros) rs = Some (transf_fundef f). +Proof. + intros until approx; intro MATCH. + destruct ros; simpl. + intro. + exploit functions_translated; eauto. intro FIND. + caseEq (D.get r approx); intros; auto. + generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto. + generalize (MATCH r). rewrite H0. intros [b [A B]]. + rewrite <- symbols_preserved in A. + rewrite B in FIND. rewrite H1 in FIND. + rewrite Genv.find_funct_find_funct_ptr in FIND. + simpl. rewrite A. auto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge i). + intro. apply function_ptr_translated. auto. + congruence. +Qed. + +(** The proof of semantic preservation is a simulation argument + based on diagrams of the following form: +<< + st1 --------------- st2 + | | + t| |t + | | + v v + st1'--------------- st2' +>> + The left vertical arrow represents a transition in the + original RTL code. The top horizontal bar is the [match_states] + invariant between the initial state [st1] in the original RTL code + and an initial state [st2] in the transformed code. + This invariant expresses that all code fragments appearing in [st2] + are obtained by [transf_code] transformation of the corresponding + fragments in [st1]. Moreover, the values of registers in [st1] + must match their compile-time approximations at the current program + point. + These two parts of the diagram are the hypotheses. In conclusions, + we want to prove the other two parts: the right vertical arrow, + which is a transition in the transformed RTL code, and the bottom + horizontal bar, which means that the [match_state] predicate holds + between the final states [st1'] and [st2']. *) + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + match_stackframe_intro: + forall res c sp pc rs f, + c = f.(RTL.fn_code) -> + (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) -> + match_stackframes + (Stackframe res c sp pc rs) + (Stackframe res (transf_code (analyze f) c) sp pc rs). + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall s c sp pc rs m f s' + (CF: c = f.(RTL.fn_code)) + (MATCH: regs_match_approx ge (analyze f)!!pc rs) + (STACKS: list_forall2 match_stackframes s s'), + match_states (State s c sp pc rs m) + (State s' (transf_code (analyze f) c) sp pc rs m) + | match_states_call: + forall s f args m s', + list_forall2 match_stackframes s s' -> + match_states (Callstate s f args m) + (Callstate s' (transf_fundef f) args m) + | match_states_return: + forall s s' v m, + list_forall2 match_stackframes s s' -> + match_states (Returnstate s v m) + (Returnstate s' v m). + +Ltac TransfInstr := + match goal with + | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ => + cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr)); + [ simpl + | unfold transf_code; rewrite PTree.gmap; + unfold option_map; rewrite H1; reflexivity ] + end. + +(** The proof of simulation proceeds by case analysis on the transition + taken in the source code. *) + +Lemma 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'. +Proof. + induction 1; intros; inv MS. + + (* Inop *) + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split. + TransfInstr; intro. eapply exec_Inop; eauto. + econstructor; eauto. + eapply analyze_correct_1 with (pc := pc); eauto. + simpl; auto. + unfold transfer; rewrite H. auto. + + (* Iop *) + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. + TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args); + intros op' args' OSR. + assert (eval_operation tge sp op' rs##args' = Some v). + rewrite (eval_operation_preserved symbols_preserved). + generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs + MATCH op args v). + rewrite OSR; simpl. auto. + generalize (eval_static_operation_correct ge op sp + (approx_regs (analyze f)!!pc args) rs##args v + (approx_regs_val_list _ _ _ args MATCH) H0). + case (eval_static_operation op (approx_regs (analyze f)!!pc args)); intros; + simpl in H2; + eapply exec_Iop; eauto; simpl. + congruence. + congruence. + elim H2; intros b [A B]. rewrite symbols_preserved. + rewrite A; rewrite B; auto. + econstructor; eauto. + eapply analyze_correct_1 with (pc := pc); eauto. + simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. + eapply eval_static_operation_correct; eauto. + apply approx_regs_val_list; auto. + + (* Iload *) + caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); + intros addr' args' ASR. + assert (eval_addressing tge sp addr' rs##args' = Some a). + rewrite (eval_addressing_preserved symbols_preserved). + generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs + MATCH addr args). + rewrite ASR; simpl. congruence. + TransfInstr. rewrite ASR. intro. + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split. + eapply exec_Iload; eauto. + econstructor; eauto. + eapply analyze_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. simpl; auto. + + (* Istore *) + caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); + intros addr' args' ASR. + assert (eval_addressing tge sp addr' rs##args' = Some a). + rewrite (eval_addressing_preserved symbols_preserved). + generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs + MATCH addr args). + rewrite ASR; simpl. congruence. + TransfInstr. rewrite ASR. intro. + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split. + eapply exec_Istore; eauto. + econstructor; eauto. + eapply analyze_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. auto. + + (* Icall *) + exploit transf_ros_correct; eauto. intro FIND'. + TransfInstr; intro. + econstructor; split. + eapply exec_Icall; eauto. apply sig_function_translated; auto. + constructor; auto. constructor; auto. + econstructor; eauto. + intros. eapply analyze_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. simpl. auto. + + (* Itailcall *) + exploit transf_ros_correct; eauto. intros FIND'. + TransfInstr; intro. + econstructor; split. + eapply exec_Itailcall; eauto. apply sig_function_translated; auto. + constructor; auto. + + (* Icond, true *) + exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. + caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); + intros cond' args' CSR. + assert (eval_condition cond' rs##args' = Some true). + generalize (cond_strength_reduction_correct + ge (approx_reg (analyze f)!!pc) rs MATCH cond args). + rewrite CSR. intro. congruence. + TransfInstr. rewrite CSR. + caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)). + intros b ESC. + generalize (eval_static_condition_correct ge cond _ _ _ + (approx_regs_val_list _ _ _ args MATCH) ESC); intro. + replace b with true. intro; eapply exec_Inop; eauto. congruence. + intros. eapply exec_Icond_true; eauto. + econstructor; eauto. + eapply analyze_correct_1; eauto. + simpl; auto. + unfold transfer; rewrite H; auto. + + (* Icond, false *) + exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. + caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); + intros cond' args' CSR. + assert (eval_condition cond' rs##args' = Some false). + generalize (cond_strength_reduction_correct + ge (approx_reg (analyze f)!!pc) rs MATCH cond args). + rewrite CSR. intro. congruence. + TransfInstr. rewrite CSR. + caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)). + intros b ESC. + generalize (eval_static_condition_correct ge cond _ _ _ + (approx_regs_val_list _ _ _ args MATCH) ESC); intro. + replace b with false. intro; eapply exec_Inop; eauto. congruence. + intros. eapply exec_Icond_false; eauto. + econstructor; eauto. + eapply analyze_correct_1; eauto. + simpl; auto. + unfold transfer; rewrite H; auto. + + (* Ireturn *) + exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split. + eapply exec_Ireturn; eauto. TransfInstr; auto. + constructor; auto. + + (* internal function *) + simpl. unfold transf_function. + econstructor; split. + eapply exec_function_internal; simpl; eauto. + simpl. econstructor; eauto. + apply analyze_correct_3; auto. + + (* external function *) + simpl. econstructor; split. + eapply exec_function_external; eauto. + constructor; auto. + + (* return *) + inv H3. inv H1. + econstructor; split. + eapply exec_return; eauto. + econstructor; eauto. +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. + exploit function_ptr_translated; eauto. intro FIND. + exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. + econstructor; eauto. + replace (prog_main tprog) with (prog_main prog). + rewrite symbols_preserved. eauto. + reflexivity. + rewrite <- H2. apply sig_function_translated. + replace (Genv.init_mem tprog) with (Genv.init_mem prog). + constructor. constructor. auto. + symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. +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 H4. constructor. +Qed. + +(** The preservation of the observable behavior of the program then + follows, using the generic preservation theorem + [Smallstep.simulation_step_preservation]. *) + +Theorem transf_program_correct: + forall (beh: program_behavior), not_wrong beh -> + exec_program prog beh -> exec_program tprog beh. +Proof. + unfold exec_program; intros. + eapply simulation_step_preservation; eauto. + eexact transf_initial_states. + eexact transf_final_states. + exact transf_step_correct. +Qed. + +End PRESERVATION. diff --git a/powerpc/Constprop.v b/powerpc/ConstpropOp.v index 109125c3..87b2cfa4 100644 --- a/powerpc/Constprop.v +++ b/powerpc/ConstpropOp.v @@ -10,22 +10,16 @@ (* *) (* *********************************************************************) -(** Constant propagation over RTL. This is the first of the two - optimizations performed at RTL level. It proceeds by a standard - dataflow analysis and the corresponding code transformation. *) +(** Static analysis and strength reduction for operators + and conditions. This is the machine-dependent part of [Constprop]. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Registers. -Require Import RTL. -Require Import Lattice. -Require Import Kildall. (** * Static analysis *) @@ -42,77 +36,6 @@ Inductive approx : Type := (** The value is the address of the given global symbol plus the given integer offset. *) -(** We equip this set of approximations with a semi-lattice structure. - The ordering is inclusion between the sets of values denoted by - the approximations. *) - -Module Approx <: SEMILATTICE_WITH_TOP. - Definition t := approx. - Definition eq (x y: t) := (x = y). - Definition eq_refl: forall x, eq x x := (@refl_equal t). - Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). - Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). - Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}. - Proof. - decide equality. - apply Int.eq_dec. - apply Float.eq_dec. - apply Int.eq_dec. - apply ident_eq. - Qed. - Definition beq (x y: t) := if eq_dec x y then true else false. - Lemma beq_correct: forall x y, beq x y = true -> x = y. - Proof. - unfold beq; intros. destruct (eq_dec x y). auto. congruence. - Qed. - Definition ge (x y: t) : Prop := - x = Unknown \/ y = Novalue \/ x = y. - Lemma ge_refl: forall x y, eq x y -> ge x y. - Proof. - unfold eq, ge; tauto. - Qed. - Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Proof. - unfold ge; intuition congruence. - Qed. - Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. - Proof. - unfold eq, ge; intros; congruence. - Qed. - Definition bot := Novalue. - Definition top := Unknown. - Lemma ge_bot: forall x, ge x bot. - Proof. - unfold ge, bot; tauto. - Qed. - Lemma ge_top: forall x, ge top x. - Proof. - unfold ge, bot; tauto. - Qed. - Definition lub (x y: t) : t := - if eq_dec x y then x else - match x, y with - | Novalue, _ => y - | _, Novalue => x - | _, _ => Unknown - end. - Lemma lub_commut: forall x y, eq (lub x y) (lub y x). - Proof. - unfold lub, eq; intros. - case (eq_dec x y); case (eq_dec y x); intros; try congruence. - destruct x; destruct y; auto. - Qed. - Lemma ge_lub_left: forall x y, ge (lub x y) x. - Proof. - unfold lub; intros. - case (eq_dec x y); intro. - apply ge_refl. apply eq_refl. - destruct x; destruct y; unfold ge; tauto. - Qed. -End Approx. - -Module D := LPMap Approx. - (** We now define the abstract interpretations of conditions and operators over this set of approximations. For instance, the abstract interpretation of the operator [Oaddf] applied to two expressions [a] and [b] is @@ -627,62 +550,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) := Unknown end. -(** The transfer function for the dataflow analysis is straightforward: - for [Iop] instructions, we set the approximation of the destination - register to the result of executing abstractly the operation; - for [Iload] and [Icall], we set the approximation of the destination - to [Unknown]. *) - -Definition approx_regs (rl: list reg) (approx: D.t) := - List.map (fun r => D.get r approx) rl. - -Definition transfer (f: function) (pc: node) (before: D.t) := - match f.(fn_code)!pc with - | None => before - | Some i => - match i with - | Inop s => - before - | Iop op args res s => - let a := eval_static_operation op (approx_regs args before) in - D.set res a before - | Iload chunk addr args dst s => - D.set dst Unknown before - | Istore chunk addr args src s => - before - | Icall sig ros args res s => - D.set res Unknown before - | Itailcall sig ros args => - before -(* - | Ialloc arg res s => - D.set res Unknown before -*) - | Icond cond args ifso ifnot => - before - | Ireturn optarg => - before - end - 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 - to approximations. It can fail to reach a fixpoint in a reasonable - number of iterations, in which case [None] is returned. *) - -Module DS := Dataflow_Solver(D)(NodeSetForward). - -Definition analyze (f: RTL.function): PMap.t D.t := - match DS.fixpoint (successors f) (transfer f) - ((f.(fn_entrypoint), D.top) :: nil) with - | None => PMap.init D.top - | Some res => res - end. - -(** * Code transformation *) - -(** ** Operator strength reduction *) +(** * Operator strength reduction *) (** We now define auxiliary functions for strength reduction of operators and addressing modes: replacing an operator with a cheaper @@ -691,10 +559,10 @@ Definition analyze (f: RTL.function): PMap.t D.t := Section STRENGTH_REDUCTION. -Variable approx: D.t. +Variable app: reg -> approx. Definition intval (r: reg) : option int := - match D.get r approx with I n => Some n | _ => None end. + match app r with I n => Some n | _ => None end. Inductive cond_strength_reduction_cases: condition -> list reg -> Type := | csr_case1: @@ -978,7 +846,7 @@ Definition addr_strength_reduction_match (addr: addressing) (args: list reg) := Definition addr_strength_reduction (addr: addressing) (args: list reg) := match addr_strength_reduction_match addr args with | addr_strength_reduction_case1 r1 r2 => (* Aindexed2 *) - match D.get r1 approx, D.get r2 approx with + match app r1, app r2 with | S symb n1, I n2 => (Aglobal symb (Int.add n1 n2), nil) | S symb n1, _ => (Abased symb n1, r2 :: nil) | I n1, S symb n2 => (Aglobal symb (Int.add n1 n2), nil) @@ -993,7 +861,7 @@ Definition addr_strength_reduction (addr: addressing) (args: list reg) := | _ => (addr, args) end | addr_strength_reduction_case3 n r1 => (* Aindexed *) - match D.get r1 approx with + match app r1 with | S symb ofs => (Aglobal symb (Int.add ofs n), nil) | _ => (addr, args) end @@ -1002,77 +870,3 @@ Definition addr_strength_reduction (addr: addressing) (args: list reg) := end. End STRENGTH_REDUCTION. - -(** ** Code transformation *) - -(** The code transformation proceeds instruction by instruction. - Operators whose arguments are all statically known are turned - into ``load integer constant'', ``load float constant'' or - ``load symbol address'' operations. Operators for which some - but not all arguments are known are subject to strength reduction, - and similarly for the addressing modes of load and store instructions. - Other instructions are unchanged. *) - -Definition transf_ros (approx: D.t) (ros: reg + ident) : reg + ident := - match ros with - | inl r => - match D.get r approx with - | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros - | _ => ros - end - | inr s => ros - end. - -Definition transf_instr (approx: D.t) (instr: instruction) := - match instr with - | Iop op args res s => - match eval_static_operation op (approx_regs args approx) with - | I n => - Iop (Ointconst n) nil res s - | F n => - Iop (Ofloatconst n) nil res s - | S symb ofs => - Iop (Oaddrsymbol symb ofs) nil res s - | _ => - let (op', args') := op_strength_reduction approx op args in - Iop op' args' res s - end - | Iload chunk addr args dst s => - let (addr', args') := addr_strength_reduction approx addr args in - Iload chunk addr' args' dst s - | Istore chunk addr args src s => - let (addr', args') := addr_strength_reduction approx addr args in - Istore chunk addr' args' src s - | Icall sig ros args res s => - Icall sig (transf_ros approx ros) args res s - | Itailcall sig ros args => - Itailcall sig (transf_ros approx ros) args - | Icond cond args s1 s2 => - match eval_static_condition cond (approx_regs args approx) with - | Some b => - if b then Inop s1 else Inop s2 - | None => - let (cond', args') := cond_strength_reduction approx cond args in - Icond cond' args' s1 s2 - end - | _ => - instr - end. - -Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code := - PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs. - -Definition transf_function (f: function) : function := - let approxs := analyze f in - mkfunction - f.(fn_sig) - f.(fn_params) - f.(fn_stacksize) - (transf_code approxs f.(fn_code)) - f.(fn_entrypoint). - -Definition transf_fundef (fd: fundef) : fundef := - AST.transf_fundef transf_function fd. - -Definition transf_program (p: program) : program := - transform_program transf_fundef p. diff --git a/powerpc/Constpropproof.v b/powerpc/ConstpropOpproof.v index 6e17f307..3fd81a6b 100644 --- a/powerpc/Constpropproof.v +++ b/powerpc/ConstpropOpproof.v @@ -13,20 +13,16 @@ (** Correctness proof for constant propagation. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Events. Require Import Mem. Require Import Globalenvs. -Require Import Smallstep. Require Import Op. Require Import Registers. Require Import RTL. -Require Import Lattice. -Require Import Kildall. +Require Import ConstpropOp. Require Import Constprop. (** * Correctness of the static analysis *) @@ -51,16 +47,6 @@ Definition val_match_approx (a: approx) (v: val) : Prop := | _ => False end. -Definition regs_match_approx (a: D.t) (rs: regset) : Prop := - forall r, val_match_approx (D.get r a) rs#r. - -Lemma regs_match_approx_top: - forall rs, regs_match_approx D.top rs. -Proof. - intros. red; intros. simpl. rewrite PTree.gempty. - unfold Approx.top, val_match_approx. auto. -Qed. - Lemma val_match_approx_increasing: forall a1 a2 v, Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v. @@ -72,26 +58,6 @@ Proof. subst a2. auto. Qed. -Lemma regs_match_approx_increasing: - forall a1 a2 rs, - D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs. -Proof. - unfold D.ge, regs_match_approx. intros. - apply val_match_approx_increasing with (D.get r a2); auto. -Qed. - -Lemma regs_match_approx_update: - forall ra rs a v r, - val_match_approx a v -> - regs_match_approx ra rs -> - regs_match_approx (D.set r a ra) (rs#r <- v). -Proof. - intros; red; intros. rewrite Regmap.gsspec. - case (peq r0 r); intro. - subst r0. rewrite D.gss. auto. - rewrite D.gso; auto. -Qed. - Inductive val_list_match_approx: list approx -> list val -> Prop := | vlma_nil: val_list_match_approx nil nil @@ -101,16 +67,6 @@ Inductive val_list_match_approx: list approx -> list val -> Prop := val_list_match_approx al vl -> val_list_match_approx (a :: al) (v :: vl). -Lemma approx_regs_val_list: - forall ra rs rl, - regs_match_approx ra rs -> - val_list_match_approx (approx_regs rl ra) rs##rl. -Proof. - induction rl; simpl; intros. - constructor. - constructor. apply H. auto. -Qed. - Ltac SimplVMA := match goal with | H: (val_match_approx (I _) ?v) |- _ => @@ -214,42 +170,6 @@ Proof. auto. Qed. -(** The correctness of the static analysis follows from the results - above and the fact that the result of the static analysis is - a solution of the forward dataflow inequations. *) - -Lemma analyze_correct_1: - forall f pc rs pc' i, - f.(fn_code)!pc = Some i -> - In pc' (successors_instr i) -> - regs_match_approx (transfer f pc (analyze f)!!pc) rs -> - regs_match_approx (analyze f)!!pc' rs. -Proof. - intros until i. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. - apply regs_match_approx_increasing with (transfer f pc approxs!!pc). - eapply DS.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto. - auto. - intros. rewrite PMap.gi. apply regs_match_approx_top. -Qed. - -Lemma analyze_correct_3: - forall f rs, - regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs. -Proof. - intros. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. - apply regs_match_approx_increasing with D.top. - eapply DS.fixpoint_entry; eauto. auto with coqlib. - apply regs_match_approx_top. - intros. rewrite PMap.gi. apply regs_match_approx_top. -Qed. - (** * Correctness of strength reduction *) (** We now show that strength reduction over operators and addressing @@ -260,39 +180,39 @@ Qed. Section STRENGTH_REDUCTION. -Variable approx: D.t. +Variable app: reg -> approx. Variable sp: val. Variable rs: regset. -Hypothesis MATCH: regs_match_approx approx rs. +Hypothesis MATCH: forall r, val_match_approx (app r) rs#r. Lemma intval_correct: forall r n, - intval approx r = Some n -> rs#r = Vint n. + intval app r = Some n -> rs#r = Vint n. Proof. intros until n. - unfold intval. caseEq (D.get r approx); intros; try discriminate. + unfold intval. caseEq (app r); intros; try discriminate. generalize (MATCH r). unfold val_match_approx. rewrite H. congruence. Qed. Lemma cond_strength_reduction_correct: forall cond args, - let (cond', args') := cond_strength_reduction approx cond args in + let (cond', args') := cond_strength_reduction app cond args in eval_condition cond' rs##args' = eval_condition cond rs##args. Proof. intros. unfold cond_strength_reduction. case (cond_strength_reduction_match cond args); intros. - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. simpl. rewrite (intval_correct _ _ H). destruct (rs#r2); auto. rewrite Int.swap_cmp. auto. destruct c; reflexivity. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H0). auto. auto. - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. simpl. rewrite (intval_correct _ _ H). destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H0). auto. auto. auto. @@ -414,26 +334,26 @@ Qed. Lemma op_strength_reduction_correct: forall op args v, - let (op', args') := op_strength_reduction approx op args in + let (op', args') := op_strength_reduction app op args in eval_operation ge sp op rs##args = Some v -> eval_operation ge sp op' rs##args' = Some v. Proof. intros; unfold op_strength_reduction; case (op_strength_reduction_match op args); intros; simpl List.map. (* Oadd *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil)) with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)). apply make_addimm_correct. simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). apply make_addimm_correct. assumption. (* Osub *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H) in H0. assumption. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil)) with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)). @@ -441,17 +361,17 @@ Proof. simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. assumption. (* Omul *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil)) with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)). apply make_mulimm_correct. simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). apply make_mulimm_correct. assumption. (* Odiv *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. caseEq (Int.is_power2 i); intros. rewrite (intval_correct _ _ H) in H1. simpl in *; FuncInv. destruct (Int.eq i Int.zero). congruence. @@ -461,7 +381,7 @@ Proof. assumption. assumption. (* Odivu *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. caseEq (Int.is_power2 i); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil)) @@ -476,56 +396,56 @@ Proof. assumption. assumption. (* Oand *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil)) with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)). apply make_andimm_correct. simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). apply make_andimm_correct. assumption. (* Oor *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil)) with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)). apply make_orimm_correct. simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). apply make_orimm_correct. assumption. (* Oxor *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil)) with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)). apply make_xorimm_correct. simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto. - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). apply make_xorimm_correct. assumption. (* Oshl *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. caseEq (Int.ltu i (Int.repr 32)); intros. rewrite (intval_correct _ _ H). apply make_shlimm_correct. assumption. assumption. (* Oshr *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. caseEq (Int.ltu i (Int.repr 32)); intros. rewrite (intval_correct _ _ H). apply make_shrimm_correct. assumption. assumption. (* Oshru *) - caseEq (intval approx r2); intros. + caseEq (intval app r2); intros. caseEq (Int.ltu i (Int.repr 32)); intros. rewrite (intval_correct _ _ H). apply make_shruimm_correct. assumption. assumption. (* Ocmp *) generalize (cond_strength_reduction_correct c rl). - destruct (cond_strength_reduction approx c rl). + destruct (cond_strength_reduction app c rl). simpl. intro. rewrite H. auto. (* default *) assumption. @@ -533,15 +453,14 @@ Qed. Ltac KnownApprox := match goal with - | MATCH: (regs_match_approx ?approx ?rs), - H: (D.get ?r ?approx = ?a) |- _ => + | H: ?approx ?r = ?a |- _ => generalize (MATCH r); rewrite H; intro; clear H; KnownApprox | _ => idtac end. Lemma addr_strength_reduction_correct: forall addr args, - let (addr', args') := addr_strength_reduction approx addr args in + let (addr', args') := addr_strength_reduction app addr args in eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args. Proof. intros. @@ -589,18 +508,18 @@ Proof. case (addr_strength_reduction_match addr args); intros. (* Aindexed2 *) - caseEq (D.get r1 approx); intros; - caseEq (D.get r2 approx); intros; + caseEq (app r1); intros; + caseEq (app r2); intros; try reflexivity; KnownApprox; auto. rewrite A0. rewrite Int.add_commut. apply A5; auto. (* Abased *) - caseEq (intval approx r1); intros. + caseEq (intval app r1); intros. simpl; rewrite (intval_correct _ _ H). auto. auto. (* Aindexed *) - caseEq (D.get r1 approx); intros; auto. + caseEq (app r1); intros; auto. simpl; KnownApprox. elim H0. intros b [A B]. rewrite A; rewrite B. auto. @@ -612,330 +531,3 @@ End STRENGTH_REDUCTION. End ANALYSIS. -(** * Correctness of the code transformation *) - -(** We now show that the transformed code after constant propagation - has the same semantics as the original code. *) - -Section PRESERVATION. - -Variable prog: program. -Let tprog := transf_program prog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.find_symbol_transf. -Qed. - -Lemma functions_translated: - forall (v: val) (f: fundef), - Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (transf_fundef f). -Proof. - intros. - exact (Genv.find_funct_transf transf_fundef H). -Qed. - -Lemma function_ptr_translated: - forall (b: block) (f: fundef), - Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (transf_fundef f). -Proof. - intros. - exact (Genv.find_funct_ptr_transf transf_fundef H). -Qed. - -Lemma sig_function_translated: - forall f, - funsig (transf_fundef f) = funsig f. -Proof. - intros. destruct f; reflexivity. -Qed. - -Lemma transf_ros_correct: - forall ros rs f approx, - regs_match_approx ge approx rs -> - find_function ge ros rs = Some f -> - find_function tge (transf_ros approx ros) rs = Some (transf_fundef f). -Proof. - intros until approx; intro MATCH. - destruct ros; simpl. - intro. - exploit functions_translated; eauto. intro FIND. - caseEq (D.get r approx); intros; auto. - generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto. - generalize (MATCH r). rewrite H0. intros [b [A B]]. - rewrite <- symbols_preserved in A. - rewrite B in FIND. rewrite H1 in FIND. - rewrite Genv.find_funct_find_funct_ptr in FIND. - simpl. rewrite A. auto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i). - intro. apply function_ptr_translated. auto. - congruence. -Qed. - -(** The proof of semantic preservation is a simulation argument - based on diagrams of the following form: -<< - st1 --------------- st2 - | | - t| |t - | | - v v - st1'--------------- st2' ->> - The left vertical arrow represents a transition in the - original RTL code. The top horizontal bar is the [match_states] - invariant between the initial state [st1] in the original RTL code - and an initial state [st2] in the transformed code. - This invariant expresses that all code fragments appearing in [st2] - are obtained by [transf_code] transformation of the corresponding - fragments in [st1]. Moreover, the values of registers in [st1] - must match their compile-time approximations at the current program - point. - These two parts of the diagram are the hypotheses. In conclusions, - we want to prove the other two parts: the right vertical arrow, - which is a transition in the transformed RTL code, and the bottom - horizontal bar, which means that the [match_state] predicate holds - between the final states [st1'] and [st2']. *) - -Inductive match_stackframes: stackframe -> stackframe -> Prop := - match_stackframe_intro: - forall res c sp pc rs f, - c = f.(RTL.fn_code) -> - (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) -> - match_stackframes - (Stackframe res c sp pc rs) - (Stackframe res (transf_code (analyze f) c) sp pc rs). - -Inductive match_states: state -> state -> Prop := - | match_states_intro: - forall s c sp pc rs m f s' - (CF: c = f.(RTL.fn_code)) - (MATCH: regs_match_approx ge (analyze f)!!pc rs) - (STACKS: list_forall2 match_stackframes s s'), - match_states (State s c sp pc rs m) - (State s' (transf_code (analyze f) c) sp pc rs m) - | match_states_call: - forall s f args m s', - list_forall2 match_stackframes s s' -> - match_states (Callstate s f args m) - (Callstate s' (transf_fundef f) args m) - | match_states_return: - forall s s' v m, - list_forall2 match_stackframes s s' -> - match_states (Returnstate s v m) - (Returnstate s' v m). - -Ltac TransfInstr := - match goal with - | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ => - cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr)); - [ simpl - | unfold transf_code; rewrite PTree.gmap; - unfold option_map; rewrite H1; reflexivity ] - end. - -(** The proof of simulation proceeds by case analysis on the transition - taken in the source code. *) - -Lemma 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'. -Proof. - induction 1; intros; inv MS. - - (* Inop *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split. - TransfInstr; intro. eapply exec_Inop; eauto. - econstructor; eauto. - eapply analyze_correct_1 with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. auto. - - (* Iop *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. - TransfInstr. caseEq (op_strength_reduction (analyze f)!!pc op args); - intros op' args' OSR. - assert (eval_operation tge sp op' rs##args' = Some v). - rewrite (eval_operation_preserved symbols_preserved). - generalize (op_strength_reduction_correct ge (analyze f)!!pc sp rs - MATCH op args v). - rewrite OSR; simpl. auto. - generalize (eval_static_operation_correct ge op sp - (approx_regs args (analyze f)!!pc) rs##args v - (approx_regs_val_list _ _ _ args MATCH) H0). - case (eval_static_operation op (approx_regs args (analyze f)!!pc)); intros; - simpl in H2; - eapply exec_Iop; eauto; simpl. - congruence. - congruence. - elim H2; intros b [A B]. rewrite symbols_preserved. - rewrite A; rewrite B; auto. - econstructor; eauto. - eapply analyze_correct_1 with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. - eapply eval_static_operation_correct; eauto. - apply approx_regs_val_list; auto. - - (* Iload *) - caseEq (addr_strength_reduction (analyze f)!!pc addr args); - intros addr' args' ASR. - assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved symbols_preserved). - generalize (addr_strength_reduction_correct ge (analyze f)!!pc sp rs - MATCH addr args). - rewrite ASR; simpl. congruence. - TransfInstr. rewrite ASR. intro. - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split. - eapply exec_Iload; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. simpl; auto. - - (* Istore *) - caseEq (addr_strength_reduction (analyze f)!!pc addr args); - intros addr' args' ASR. - assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved symbols_preserved). - generalize (addr_strength_reduction_correct ge (analyze f)!!pc sp rs - MATCH addr args). - rewrite ASR; simpl. congruence. - TransfInstr. rewrite ASR. intro. - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split. - eapply exec_Istore; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. auto. - - (* Icall *) - exploit transf_ros_correct; eauto. intro FIND'. - TransfInstr; intro. - econstructor; split. - eapply exec_Icall; eauto. apply sig_function_translated; auto. - constructor; auto. constructor; auto. - econstructor; eauto. - intros. eapply analyze_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. simpl. auto. - - (* Itailcall *) - exploit transf_ros_correct; eauto. intros FIND'. - TransfInstr; intro. - econstructor; split. - eapply exec_Itailcall; eauto. apply sig_function_translated; auto. - constructor; auto. - - (* Icond, true *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. - caseEq (cond_strength_reduction (analyze f)!!pc cond args); - intros cond' args' CSR. - assert (eval_condition cond' rs##args' = Some true). - generalize (cond_strength_reduction_correct - ge (analyze f)!!pc rs MATCH cond args). - rewrite CSR. intro. congruence. - TransfInstr. rewrite CSR. - caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)). - intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ _ - (approx_regs_val_list _ _ _ args MATCH) ESC); intro. - replace b with true. intro; eapply exec_Inop; eauto. congruence. - intros. eapply exec_Icond_true; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. - - (* Icond, false *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. - caseEq (cond_strength_reduction (analyze f)!!pc cond args); - intros cond' args' CSR. - assert (eval_condition cond' rs##args' = Some false). - generalize (cond_strength_reduction_correct - ge (analyze f)!!pc rs MATCH cond args). - rewrite CSR. intro. congruence. - TransfInstr. rewrite CSR. - caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)). - intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ _ - (approx_regs_val_list _ _ _ args MATCH) ESC); intro. - replace b with false. intro; eapply exec_Inop; eauto. congruence. - intros. eapply exec_Icond_false; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. - - (* Ireturn *) - exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split. - eapply exec_Ireturn; eauto. TransfInstr; auto. - constructor; auto. - - (* internal function *) - simpl. unfold transf_function. - econstructor; split. - eapply exec_function_internal; simpl; eauto. - simpl. econstructor; eauto. - apply analyze_correct_3; auto. - - (* external function *) - simpl. econstructor; split. - eapply exec_function_external; eauto. - constructor; auto. - - (* return *) - inv H3. inv H1. - econstructor; split. - eapply exec_return; eauto. - econstructor; eauto. -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. - exploit function_ptr_translated; eauto. intro FIND. - exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. - econstructor; eauto. - replace (prog_main tprog) with (prog_main prog). - rewrite symbols_preserved. eauto. - reflexivity. - rewrite <- H2. apply sig_function_translated. - replace (Genv.init_mem tprog) with (Genv.init_mem prog). - constructor. constructor. auto. - symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. -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 H4. constructor. -Qed. - -(** The preservation of the observable behavior of the program then - follows, using the generic preservation theorem - [Smallstep.simulation_step_preservation]. *) - -Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - exec_program prog beh -> exec_program tprog beh. -Proof. - unfold exec_program; intros. - eapply simulation_step_preservation; eauto. - eexact transf_initial_states. - eexact transf_final_states. - exact transf_step_correct. -Qed. - -End PRESERVATION. |