diff options
| -rw-r--r-- | .depend | 8 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | arm/SelectOp.v (renamed from arm/Selection.v) | 259 | ||||
| -rw-r--r-- | arm/SelectOpproof.v (renamed from arm/Selectionproof.v) | 601 | ||||
| -rw-r--r-- | backend/CminorSel.v | 122 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 4 | ||||
| -rw-r--r-- | powerpc/SelectOp.v (renamed from powerpc/Selection.v) | 261 | ||||
| -rw-r--r-- | powerpc/SelectOpproof.v (renamed from powerpc/Selectionproof.v) | 616 |
8 files changed, 325 insertions, 1548 deletions
@@ -29,8 +29,8 @@ $(ARCH)/Constpropproof.vo: $(ARCH)/Constpropproof.v lib/Coqlib.vo lib/Maps.vo co $(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)/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)/Selectionproof.vo: $(ARCH)/Selectionproof.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)/Selection.vo -$(ARCH)/Selection.vo: $(ARCH)/Selection.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 backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.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 +$(ARCH)/SelectOp.vo: $(ARCH)/SelectOp.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 backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/Allocation.vo: backend/Allocation.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Coloring.vo backend/LTL.vo backend/Allocproof.vo: backend/Allocproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/LTL.vo backend/Alloctyping.vo: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo $(ARCH)/$(VARIANT)/Conventions.vo @@ -68,6 +68,8 @@ backend/RTLgenspec.vo: backend/RTLgenspec.v lib/Coqlib.vo common/Errors.vo lib/M backend/RTLgen.vo: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo common/Mem.vo lib/Integers.vo common/Events.vo common/Smallstep.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo +backend/Selectionproof.vo: backend/Selectionproof.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 backend/Selection.vo $(ARCH)/SelectOpproof.vo +backend/Selection.vo: backend/Selection.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 backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/Stackingproof.vo: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machabstr.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingtyping.vo: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingproof.vo backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo @@ -86,5 +88,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 $(ARCH)/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 $(ARCH)/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 $(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/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 @@ -47,7 +47,7 @@ COMMON=Errors.v AST.v Events.v Globalenvs.v Mem.v Values.v \ BACKEND=\ Cminor.v Op.v CminorSel.v \ - Selection.v Selectionproof.v \ + SelectOp.v Selection.v SelectOpproof.v Selectionproof.v \ Registers.v RTL.v \ RTLgen.v RTLgenspec.v RTLgenproof.v \ Tailcall.v Tailcallproof.v \ diff --git a/arm/Selection.v b/arm/SelectOp.v index 12cc1b27..8ac4ea51 100644 --- a/arm/Selection.v +++ b/arm/SelectOp.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Instruction selection *) +(** Instruction selection for operators *) (** The instruction selection pass recognizes opportunities for using combined arithmetic and logical operations and addressing modes @@ -19,8 +19,22 @@ and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned into a "rotate and mask" instruction. - Instruction selection proceeds by bottom-up rewriting over expressions. - The source language is Cminor and the target language is CminorSel. *) + This file defines functions for building CminorSel expressions and + statements, especially expressions consisting of operator + applications. These functions examine their arguments to choose + cheaper forms of operators whenever possible. + + For instance, [add e1 e2] will return a CminorSel expression semantically + equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a + [Oaddimm] operator if one of the arguments is an integer constant, + or suppress the addition altogether if one of the arguments is the + null integer. In passing, we perform operator reassociation + ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount + of constant propagation. + + On top of the "smart constructor" functions defined below, + module [Selection] implements the actual instruction selection pass. +*) Require Import Coqlib. Require Import Maps. @@ -34,61 +48,7 @@ Require Cminor. Require Import Op. Require Import CminorSel. -Infix ":::" := Econs (at level 60, right associativity) : selection_scope. - -Open Local Scope selection_scope. - -(** * Lifting of let-bound variables *) - -(** Some of the instruction functions generate [Elet] constructs to - share the evaluation of a subexpression. Owing to the use of de - Bruijn indices for let-bound variables, we need to shift de Bruijn - indices when an expression [b] is put in a [Elet a b] context. *) - -Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr := - match a with - | Evar id => Evar id - | Eop op bl => Eop op (lift_exprlist p bl) - | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl) - | Econdition b c d => - Econdition (lift_condexpr p b) (lift_expr p c) (lift_expr p d) - | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c) - | Eletvar n => - if le_gt_dec p n then Eletvar (S n) else Eletvar n - end - -with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr := - match a with - | CEtrue => CEtrue - | CEfalse => CEfalse - | CEcond cond bl => CEcond cond (lift_exprlist p bl) - | CEcondition b c d => - CEcondition (lift_condexpr p b) (lift_condexpr p c) (lift_condexpr p d) - end - -with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist := - match a with - | Enil => Enil - | Econs b cl => Econs (lift_expr p b) (lift_exprlist p cl) - end. - -Definition lift (a: expr): expr := lift_expr O a. - -(** * Smart constructors for operators *) - -(** This section defines functions for building CminorSel expressions - and statements, especially expressions consisting of operator - applications. These functions examine their arguments to choose - cheaper forms of operators whenever possible. - - For instance, [add e1 e2] will return a CminorSel expression semantically - equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a - [Oaddimm] operator if one of the arguments is an integer constant, - or suppress the addition altogether if one of the arguments is the - null integer. In passing, we perform operator reassociation - ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount - of constant propagation. -*) +Open Local Scope cminorsel_scope. (** ** Integer logical negation *) @@ -1146,50 +1106,19 @@ Definition compu (c: comparison) (e1: expr) (e2: expr) := Definition compf (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). -(** ** Conditional expressions *) - -Fixpoint negate_condexpr (e: condexpr): condexpr := - match e with - | CEtrue => CEfalse - | CEfalse => CEtrue - | CEcond c el => CEcond (negate_condition c) el - | CEcondition e1 e2 e3 => - CEcondition e1 (negate_condexpr e2) (negate_condexpr e3) - end. +(** ** Other operators, not optimized. *) - -Definition is_compare_neq_zero (c: condition) : bool := - match c with - | Ccompimm Cne n => Int.eq n Int.zero - | Ccompuimm Cne n => Int.eq n Int.zero - | _ => false - end. - -Definition is_compare_eq_zero (c: condition) : bool := - match c with - | Ccompimm Ceq n => Int.eq n Int.zero - | Ccompuimm Ceq n => Int.eq n Int.zero - | _ => false - end. - -Fixpoint condexpr_of_expr (e: expr) : condexpr := - match e with - | Eop (Ointconst n) Enil => - if Int.eq n Int.zero then CEfalse else CEtrue - | Eop (Ocmp c) (e1 ::: Enil) => - if is_compare_neq_zero c then - condexpr_of_expr e1 - else if is_compare_eq_zero c then - negate_condexpr (condexpr_of_expr e1) - else - CEcond c (e1 ::: Enil) - | Eop (Ocmp c) el => - CEcond c el - | Econdition ce e1 e2 => - CEcondition ce (condexpr_of_expr e1) (condexpr_of_expr e2) - | _ => - CEcond (Ccompimm Cne Int.zero) (e:::Enil) - end. +Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil). +Definition negf (e: expr) := Eop Onegf (e ::: Enil). +Definition absf (e: expr) := Eop Oabsf (e ::: Enil). +Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). +Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). +Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). +Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil). +Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). +Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). +Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). +Definition divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). (** ** Recognition of addressing modes for load and store operations *) @@ -1264,131 +1193,3 @@ Definition addressing (chunk: memory_chunk) (e: expr) := (Aindexed Int.zero, e:::Enil) end. -Definition load (chunk: memory_chunk) (e1: expr) := - match addressing chunk e1 with - | (mode, args) => Eload chunk mode args - end. - -Definition store (chunk: memory_chunk) (e1 e2: expr) := - match addressing chunk e1 with - | (mode, args) => Sstore chunk mode args e2 - end. - -(** * Translation from Cminor to CminorSel *) - -(** Instruction selection for operator applications *) - -Definition sel_constant (cst: Cminor.constant) : expr := - match cst with - | Cminor.Ointconst n => Eop (Ointconst n) Enil - | Cminor.Ofloatconst f => Eop (Ofloatconst f) Enil - | Cminor.Oaddrsymbol id ofs => Eop (Oaddrsymbol id ofs) Enil - | Cminor.Oaddrstack ofs => Eop (Oaddrstack ofs) Enil - end. - -Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := - match op with - | Cminor.Ocast8unsigned => cast8unsigned arg - | Cminor.Ocast8signed => cast8signed arg - | Cminor.Ocast16unsigned => cast16unsigned arg - | Cminor.Ocast16signed => cast16signed arg - | Cminor.Onegint => Eop (Orsubimm Int.zero) (arg ::: Enil) - | Cminor.Onotbool => notbool arg - | Cminor.Onotint => notint arg - | Cminor.Onegf => Eop Onegf (arg ::: Enil) - | Cminor.Oabsf => Eop Oabsf (arg ::: Enil) - | Cminor.Osingleoffloat => singleoffloat arg - | Cminor.Ointoffloat => Eop Ointoffloat (arg ::: Enil) - | Cminor.Ointuoffloat => Eop Ointuoffloat (arg ::: Enil) - | Cminor.Ofloatofint => Eop Ofloatofint (arg ::: Enil) - | Cminor.Ofloatofintu => Eop Ofloatofintu (arg ::: Enil) - end. - -Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := - match op with - | Cminor.Oadd => add arg1 arg2 - | Cminor.Osub => sub arg1 arg2 - | Cminor.Omul => mul arg1 arg2 - | Cminor.Odiv => divs arg1 arg2 - | Cminor.Odivu => divu arg1 arg2 - | Cminor.Omod => mods arg1 arg2 - | Cminor.Omodu => modu arg1 arg2 - | Cminor.Oand => and arg1 arg2 - | Cminor.Oor => or arg1 arg2 - | Cminor.Oxor => xor arg1 arg2 - | Cminor.Oshl => shl arg1 arg2 - | Cminor.Oshr => shr arg1 arg2 - | Cminor.Oshru => shru arg1 arg2 - | Cminor.Oaddf => Eop Oaddf (arg1 ::: arg2 ::: Enil) - | Cminor.Osubf => Eop Osubf (arg1 ::: arg2 ::: Enil) - | Cminor.Omulf => Eop Omulf (arg1 ::: arg2 ::: Enil) - | Cminor.Odivf => Eop Odivf (arg1 ::: arg2 ::: Enil) - | Cminor.Ocmp c => comp c arg1 arg2 - | Cminor.Ocmpu c => compu c arg1 arg2 - | Cminor.Ocmpf c => compf c arg1 arg2 - end. - -(** Conversion from Cminor expression to Cminorsel expressions *) - -Fixpoint sel_expr (a: Cminor.expr) : expr := - match a with - | Cminor.Evar id => Evar id - | Cminor.Econst cst => sel_constant cst - | Cminor.Eunop op arg => sel_unop op (sel_expr arg) - | Cminor.Ebinop op arg1 arg2 => sel_binop op (sel_expr arg1) (sel_expr arg2) - | Cminor.Eload chunk addr => load chunk (sel_expr addr) - | Cminor.Econdition cond ifso ifnot => - Econdition (condexpr_of_expr (sel_expr cond)) - (sel_expr ifso) (sel_expr ifnot) - end. - -Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist := - match al with - | nil => Enil - | a :: bl => Econs (sel_expr a) (sel_exprlist bl) - end. - -(** Conversion from Cminor statements to Cminorsel statements. *) - -Fixpoint sel_stmt (s: Cminor.stmt) : stmt := - match s with - | Cminor.Sskip => Sskip - | Cminor.Sassign id e => Sassign id (sel_expr e) - | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs) - | Cminor.Scall optid sg fn args => - Scall optid sg (sel_expr fn) (sel_exprlist args) - | Cminor.Stailcall sg fn args => - Stailcall sg (sel_expr fn) (sel_exprlist args) - | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2) - | Cminor.Sifthenelse e ifso ifnot => - Sifthenelse (condexpr_of_expr (sel_expr e)) - (sel_stmt ifso) (sel_stmt ifnot) - | Cminor.Sloop body => Sloop (sel_stmt body) - | Cminor.Sblock body => Sblock (sel_stmt body) - | Cminor.Sexit n => Sexit n - | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl - | Cminor.Sreturn None => Sreturn None - | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e)) - | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body) - | Cminor.Sgoto lbl => Sgoto lbl - end. - -(** Conversion of functions and programs. *) - -Definition sel_function (f: Cminor.function) : function := - mkfunction - f.(Cminor.fn_sig) - f.(Cminor.fn_params) - f.(Cminor.fn_vars) - f.(Cminor.fn_stackspace) - (sel_stmt f.(Cminor.fn_body)). - -Definition sel_fundef (f: Cminor.fundef) : fundef := - transf_fundef sel_function f. - -Definition sel_program (p: Cminor.program) : program := - transform_program sel_fundef p. - -(** For compatibility with PowerPC *) - -Parameter use_fused_mul: unit -> bool. diff --git a/arm/Selectionproof.v b/arm/SelectOpproof.v index cf7613b6..68b49fd8 100644 --- a/arm/Selectionproof.v +++ b/arm/SelectOpproof.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Correctness of instruction selection *) +(** Correctness of instruction selection for operators *) Require Import Coqlib. Require Import Maps. @@ -25,9 +25,9 @@ Require Import Smallstep. Require Import Cminor. Require Import Op. Require Import CminorSel. -Require Import Selection. +Require Import SelectOp. -Open Local Scope selection_scope. +Open Local Scope cminorsel_scope. Section CMCONSTR. @@ -36,91 +36,6 @@ Variable sp: val. Variable e: env. Variable m: mem. -(** * Lifting of let-bound variables *) - -Inductive insert_lenv: letenv -> nat -> val -> letenv -> Prop := - | insert_lenv_0: - forall le v, - insert_lenv le O v (v :: le) - | insert_lenv_S: - forall le p w le' v, - insert_lenv le p w le' -> - insert_lenv (v :: le) (S p) w (v :: le'). - -Lemma insert_lenv_lookup1: - forall le p w le', - insert_lenv le p w le' -> - forall n v, - nth_error le n = Some v -> (p > n)%nat -> - nth_error le' n = Some v. -Proof. - induction 1; intros. - omegaContradiction. - destruct n; simpl; simpl in H0. auto. - apply IHinsert_lenv. auto. omega. -Qed. - -Lemma insert_lenv_lookup2: - forall le p w le', - insert_lenv le p w le' -> - forall n v, - nth_error le n = Some v -> (p <= n)%nat -> - nth_error le' (S n) = Some v. -Proof. - induction 1; intros. - simpl. assumption. - simpl. destruct n. omegaContradiction. - apply IHinsert_lenv. exact H0. omega. -Qed. - -Hint Resolve eval_Evar eval_Eop eval_Eload eval_Econdition - eval_Elet eval_Eletvar - eval_CEtrue eval_CEfalse eval_CEcond - eval_CEcondition eval_Enil eval_Econs: evalexpr. - -Lemma eval_lift_expr: - forall w le a v, - eval_expr ge sp e m le a v -> - forall p le', insert_lenv le p w le' -> - eval_expr ge sp e m le' (lift_expr p a) v. -Proof. - intro w. - apply (eval_expr_ind3 ge sp e m - (fun le a v => - forall p le', insert_lenv le p w le' -> - eval_expr ge sp e m le' (lift_expr p a) v) - (fun le a v => - forall p le', insert_lenv le p w le' -> - eval_condexpr ge sp e m le' (lift_condexpr p a) v) - (fun le al vl => - forall p le', insert_lenv le p w le' -> - eval_exprlist ge sp e m le' (lift_exprlist p al) vl)); - simpl; intros; eauto with evalexpr. - - destruct v1; eapply eval_Econdition; - eauto with evalexpr; simpl; eauto with evalexpr. - - eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. - - case (le_gt_dec p n); intro. - apply eval_Eletvar. eapply insert_lenv_lookup2; eauto. - apply eval_Eletvar. eapply insert_lenv_lookup1; eauto. - - destruct vb1; eapply eval_CEcondition; - eauto with evalexpr; simpl; eauto with evalexpr. -Qed. - -Lemma eval_lift: - forall le a v w, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m (w::le) (lift a) v. -Proof. - intros. unfold lift. eapply eval_lift_expr. - eexact H. apply insert_lenv_0. -Qed. - -Hint Resolve eval_lift: evalexpr. - (** * Useful lemmas and tactics *) (** The following are trivial lemmas and custom tactics that help @@ -961,132 +876,75 @@ Proof. destruct (Float.cmp c x y); reflexivity. Qed. -Lemma negate_condexpr_correct: - forall le a b, - eval_condexpr ge sp e m le a b -> - eval_condexpr ge sp e m le (negate_condexpr a) (negb b). -Proof. - induction 1; simpl. - constructor. - constructor. - econstructor. eauto. apply eval_negate_condition. auto. - econstructor. eauto. destruct vb1; auto. -Qed. +Theorem eval_negint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (negint a) (Vint (Int.neg x)). +Proof. intros; unfold negint; EvalOp. Qed. -Scheme expr_ind2 := Induction for expr Sort Prop - with exprlist_ind2 := Induction for exprlist Sort Prop. +Theorem eval_negf: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (negf a) (Vfloat (Float.neg x)). +Proof. intros; unfold negf; EvalOp. Qed. -Fixpoint forall_exprlist (P: expr -> Prop) (el: exprlist) {struct el}: Prop := - match el with - | Enil => True - | Econs e el' => P e /\ forall_exprlist P el' - end. +Theorem eval_absf: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (absf a) (Vfloat (Float.abs x)). +Proof. intros; unfold absf; EvalOp. Qed. -Lemma expr_induction_principle: - forall (P: expr -> Prop), - (forall i : ident, P (Evar i)) -> - (forall (o : operation) (e : exprlist), - forall_exprlist P e -> P (Eop o e)) -> - (forall (m : memory_chunk) (a : Op.addressing) (e : exprlist), - forall_exprlist P e -> P (Eload m a e)) -> - (forall (c : condexpr) (e : expr), - P e -> forall e0 : expr, P e0 -> P (Econdition c e e0)) -> - (forall e : expr, P e -> forall e0 : expr, P e0 -> P (Elet e e0)) -> - (forall n : nat, P (Eletvar n)) -> - forall e : expr, P e. -Proof. - intros. apply expr_ind2 with (P := P) (P0 := forall_exprlist P); auto. - simpl. auto. - intros. simpl. auto. -Qed. +Theorem eval_intoffloat: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)). +Proof. intros; unfold intoffloat; EvalOp. Qed. -Lemma eval_base_condition_of_expr: - forall le a v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_condexpr ge sp e m le - (CEcond (Ccompimm Cne Int.zero) (a ::: Enil)) - b. -Proof. - intros. - eapply eval_CEcond. eauto with evalexpr. - inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto. -Qed. +Theorem eval_intuoffloat: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)). +Proof. intros; unfold intuoffloat; EvalOp. Qed. -Lemma is_compare_neq_zero_correct: - forall c v b, - is_compare_neq_zero c = true -> - eval_condition c (v :: nil) = Some b -> - Val.bool_of_val v b. -Proof. - intros. - destruct c; simpl in H; try discriminate; - destruct c; simpl in H; try discriminate; - generalize (Int.eq_spec i Int.zero); rewrite H; intro; subst i. - - simpl in H0. destruct v; inv H0. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. - subst i; constructor. constructor; auto. constructor. - - simpl in H0. destruct v; inv H0. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. - subst i; constructor. constructor; auto. -Qed. +Theorem eval_floatofint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)). +Proof. intros; unfold floatofint; EvalOp. Qed. -Lemma is_compare_eq_zero_correct: - forall c v b, - is_compare_eq_zero c = true -> - eval_condition c (v :: nil) = Some b -> - Val.bool_of_val v (negb b). -Proof. - intros. apply is_compare_neq_zero_correct with (negate_condition c). - destruct c; simpl in H; simpl; try discriminate; - destruct c; simpl; try discriminate; auto. - apply eval_negate_condition; auto. -Qed. +Theorem eval_floatofintu: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)). +Proof. intros; unfold floatofintu; EvalOp. Qed. -Lemma eval_condition_of_expr: - forall a le v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_condexpr ge sp e m le (condexpr_of_expr a) b. -Proof. - intro a0; pattern a0. - apply expr_induction_principle; simpl; intros; - try (eapply eval_base_condition_of_expr; eauto; fail). - - destruct o; try (eapply eval_base_condition_of_expr; eauto; fail). +Theorem eval_addf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (addf a b) (Vfloat (Float.add x y)). +Proof. intros; unfold addf; EvalOp. Qed. - destruct e0. InvEval. - inversion H1. - rewrite Int.eq_false; auto. constructor. - subst i; rewrite Int.eq_true. constructor. - eapply eval_base_condition_of_expr; eauto. - - inv H0. simpl in H7. - assert (eval_condition c vl = Some b). - destruct (eval_condition c vl); try discriminate. - destruct b0; inv H7; inversion H1; congruence. - assert (eval_condexpr ge sp e m le (CEcond c e0) b). - eapply eval_CEcond; eauto. - destruct e0; auto. destruct e1; auto. - simpl in H. destruct H. - inv H5. inv H11. - - case_eq (is_compare_neq_zero c); intros. - eapply H; eauto. - apply is_compare_neq_zero_correct with c; auto. - - case_eq (is_compare_eq_zero c); intros. - replace b with (negb (negb b)). apply negate_condexpr_correct. - eapply H; eauto. - apply is_compare_eq_zero_correct with c; auto. - apply negb_involutive. - - auto. - - inv H1. destruct v1; eauto with evalexpr. -Qed. +Theorem eval_subf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (subf a b) (Vfloat (Float.sub x y)). +Proof. intros; unfold subf; EvalOp. Qed. + +Theorem eval_mulf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (mulf a b) (Vfloat (Float.mul x y)). +Proof. intros; unfold mulf; EvalOp. Qed. + +Theorem eval_divf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (divf a b) (Vfloat (Float.div x y)). +Proof. intros; unfold divf; EvalOp. Qed. Lemma eval_addressing: forall le chunk a v b ofs, @@ -1125,335 +983,4 @@ Proof. subst v. simpl. rewrite Int.add_zero. auto. Qed. -Lemma eval_load: - forall le a v chunk v', - eval_expr ge sp e m le a v -> - Mem.loadv chunk m v = Some v' -> - eval_expr ge sp e m le (load chunk a) v'. -Proof. - intros. generalize H0; destruct v; simpl; intro; try discriminate. - unfold load. - generalize (eval_addressing _ chunk _ _ _ _ H (refl_equal _)). - destruct (addressing chunk a). intros [vl [EV EQ]]. - eapply eval_Eload; eauto. -Qed. - -Lemma eval_store: - forall chunk a1 a2 v1 v2 f k m', - eval_expr ge sp e m nil a1 v1 -> - eval_expr ge sp e m nil a2 v2 -> - Mem.storev chunk m v1 v2 = Some m' -> - step ge (State f (store chunk a1 a2) k sp e m) - E0 (State f Sskip k sp e m'). -Proof. - intros. generalize H1; destruct v1; simpl; intro; try discriminate. - unfold store. - generalize (eval_addressing _ chunk _ _ _ _ H (refl_equal _)). - destruct (addressing chunk a1). intros [vl [EV EQ]]. - eapply step_store; eauto. -Qed. - -(** * Correctness of instruction selection for operators *) - -(** We now prove a semantic preservation result for the [sel_unop] - and [sel_binop] selection functions. The proof exploits - the results of the previous section. *) - -Lemma eval_sel_unop: - forall le op a1 v1 v, - eval_expr ge sp e m le a1 v1 -> - eval_unop op v1 = Some v -> - eval_expr ge sp e m le (sel_unop op a1) v. -Proof. - destruct op; simpl; intros; FuncInv; try subst v. - apply eval_cast8unsigned; auto. - apply eval_cast8signed; auto. - apply eval_cast16unsigned; auto. - apply eval_cast16signed; auto. - EvalOp. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro. - change true with (negb false). eapply eval_notbool; eauto. subst i; constructor. - change false with (negb true). eapply eval_notbool; eauto. constructor; auto. - change Vfalse with (Val.of_bool (negb true)). - eapply eval_notbool; eauto. constructor. - apply eval_notint; auto. - EvalOp. - EvalOp. - apply eval_singleoffloat; auto. - EvalOp. - EvalOp. - EvalOp. - EvalOp. -Qed. - -Lemma eval_sel_binop: - forall le op a1 a2 v1 v2 v, - eval_expr ge sp e m le a1 v1 -> - eval_expr ge sp e m le a2 v2 -> - eval_binop op v1 v2 = Some v -> - eval_expr ge sp e m le (sel_binop op a1 a2) v. -Proof. - destruct op; simpl; intros; FuncInv; try subst v. - apply eval_add; auto. - apply eval_add_ptr_2; auto. - apply eval_add_ptr; auto. - apply eval_sub; auto. - apply eval_sub_ptr_int; auto. - destruct (eq_block b b0); inv H1. - eapply eval_sub_ptr_ptr; eauto. - apply eval_mul; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_divs; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_divu; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_mods; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_modu; eauto. - apply eval_and; auto. - apply eval_or; auto. - apply eval_xor; auto. - caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - apply eval_shl; auto. - caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - apply eval_shr; auto. - caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - apply eval_shru; auto. - EvalOp. - EvalOp. - EvalOp. - EvalOp. - apply eval_comp_int; auto. - eapply eval_comp_int_ptr; eauto. - eapply eval_comp_ptr_int; eauto. - destruct (eq_block b b0); inv H1. - eapply eval_comp_ptr_ptr; eauto. - eapply eval_comp_ptr_ptr_2; eauto. - eapply eval_compu; eauto. - eapply eval_compf; eauto. -Qed. - End CMCONSTR. - -(** * Semantic preservation for instruction selection. *) - -Section PRESERVATION. - -Variable prog: Cminor.program. -Let tprog := sel_program prog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -(** Relationship between the global environments for the original - CminorSel program and the generated RTL program. *) - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, sel_program. - apply Genv.find_symbol_transf. -Qed. - -Lemma functions_translated: - forall (v: val) (f: Cminor.fundef), - Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (sel_fundef f). -Proof. - intros. - exact (Genv.find_funct_transf sel_fundef H). -Qed. - -Lemma function_ptr_translated: - forall (b: block) (f: Cminor.fundef), - Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (sel_fundef f). -Proof. - intros. - exact (Genv.find_funct_ptr_transf sel_fundef H). -Qed. - -Lemma sig_function_translated: - forall f, - funsig (sel_fundef f) = Cminor.funsig f. -Proof. - intros. destruct f; reflexivity. -Qed. - -(** Semantic preservation for expressions. *) - -Lemma sel_expr_correct: - forall sp e m a v, - Cminor.eval_expr ge sp e m a v -> - forall le, - eval_expr tge sp e m le (sel_expr a) v. -Proof. - induction 1; intros; simpl. - (* Evar *) - constructor; auto. - (* Econst *) - destruct cst; simpl; simpl in H; (econstructor; [constructor|simpl;auto]). - rewrite symbols_preserved. auto. - (* Eunop *) - eapply eval_sel_unop; eauto. - (* Ebinop *) - eapply eval_sel_binop; eauto. - (* Eload *) - eapply eval_load; eauto. - (* Econdition *) - econstructor; eauto. eapply eval_condition_of_expr; eauto. - destruct b1; auto. -Qed. - -Hint Resolve sel_expr_correct: evalexpr. - -Lemma sel_exprlist_correct: - forall sp e m a v, - Cminor.eval_exprlist ge sp e m a v -> - forall le, - eval_exprlist tge sp e m le (sel_exprlist a) v. -Proof. - induction 1; intros; simpl; constructor; auto with evalexpr. -Qed. - -Hint Resolve sel_exprlist_correct: evalexpr. - -(** Semantic preservation for terminating function calls and statements. *) - -Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont := - match k with - | Cminor.Kstop => Kstop - | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1) - | Cminor.Kblock k1 => Kblock (sel_cont k1) - | Cminor.Kcall id f sp e k1 => - Kcall id (sel_function f) sp e (sel_cont k1) - end. - -Inductive match_states: Cminor.state -> CminorSel.state -> Prop := - | match_state: forall f s k s' k' sp e m, - s' = sel_stmt s -> - k' = sel_cont k -> - match_states - (Cminor.State f s k sp e m) - (State (sel_function f) s' k' sp e m) - | match_callstate: forall f args k k' m, - k' = sel_cont k -> - match_states - (Cminor.Callstate f args k m) - (Callstate (sel_fundef f) args k' m) - | match_returnstate: forall v k k' m, - k' = sel_cont k -> - match_states - (Cminor.Returnstate v k m) - (Returnstate v k' m). - -Remark call_cont_commut: - forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k). -Proof. - induction k; simpl; auto. -Qed. - -Remark find_label_commut: - forall lbl s k, - find_label lbl (sel_stmt s) (sel_cont k) = - option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk))) - (Cminor.find_label lbl s k). -Proof. - induction s; intros; simpl; auto. - unfold store. destruct (addressing m (sel_expr e)); auto. - change (Kseq (sel_stmt s2) (sel_cont k)) - with (sel_cont (Cminor.Kseq s2 k)). - rewrite IHs1. rewrite IHs2. - destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto. - rewrite IHs1. rewrite IHs2. - destruct (Cminor.find_label lbl s1 k); auto. - change (Kseq (Sloop (sel_stmt s)) (sel_cont k)) - with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)). - auto. - change (Kblock (sel_cont k)) - with (sel_cont (Cminor.Kblock k)). - auto. - destruct o; auto. - destruct (ident_eq lbl l); auto. -Qed. - -Lemma sel_step_correct: - forall S1 t S2, Cminor.step ge S1 t S2 -> - forall T1, match_states S1 T1 -> - exists T2, step tge T1 t T2 /\ match_states S2 T2. -Proof. - induction 1; intros T1 ME; inv ME; simpl; - try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail). - - (* skip call *) - econstructor; split. - econstructor. destruct k; simpl in H; simpl; auto. - rewrite <- H0; reflexivity. - constructor; auto. - (* store *) - econstructor; split. - eapply eval_store; eauto with evalexpr. - constructor; auto. - (* Scall *) - econstructor; split. - econstructor; eauto with evalexpr. - apply functions_translated; eauto. - apply sig_function_translated. - constructor; auto. - (* Stailcall *) - econstructor; split. - econstructor; eauto with evalexpr. - apply functions_translated; eauto. - apply sig_function_translated. - constructor; auto. apply call_cont_commut. - (* Sifthenelse *) - exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split. - constructor. eapply eval_condition_of_expr; eauto with evalexpr. - constructor; auto. destruct b; auto. - (* Sreturn None *) - econstructor; split. - econstructor. - constructor; auto. apply call_cont_commut. - (* Sreturn Some *) - econstructor; split. - econstructor. simpl. eauto with evalexpr. - constructor; auto. apply call_cont_commut. - (* Sgoto *) - econstructor; split. - econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut. - rewrite H. simpl. reflexivity. - constructor; auto. -Qed. - -Lemma sel_initial_states: - forall S, Cminor.initial_state prog S -> - exists R, initial_state tprog R /\ match_states S R. -Proof. - induction 1. - econstructor; split. - econstructor. - simpl. fold tge. rewrite symbols_preserved. eexact H. - apply function_ptr_translated. eauto. - rewrite <- H1. apply sig_function_translated; auto. - unfold tprog, sel_program. rewrite Genv.init_mem_transf. - constructor; auto. -Qed. - -Lemma sel_final_states: - forall S R r, - match_states S R -> Cminor.final_state S r -> final_state R r. -Proof. - intros. inv H0. inv H. simpl. constructor. -Qed. - -Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. -Proof. - unfold CminorSel.exec_program, Cminor.exec_program; intros. - eapply simulation_step_preservation; eauto. - eexact sel_initial_states. - eexact sel_final_states. - exact sel_step_correct. -Qed. - -End PRESERVATION. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 1e798b5f..85338720 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -58,6 +58,8 @@ with exprlist : Type := | Enil: exprlist | Econs: expr -> exprlist -> exprlist. +Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope. + (** Statements are as in Cminor, except that the condition of an if/then/else conditional is a [condexpr], and the [Sstore] construct uses a machine-dependent addressing mode. *) @@ -373,3 +375,123 @@ Inductive final_state: state -> int -> Prop := Definition exec_program (p: program) (beh: program_behavior) : Prop := program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. + +Hint Constructors eval_expr eval_condexpr eval_exprlist: evalexpr. + +(** * Lifting of let-bound variables *) + +(** Instruction selection sometimes generate [Elet] constructs to + share the evaluation of a subexpression. Owing to the use of de + Bruijn indices for let-bound variables, we need to shift de Bruijn + indices when an expression [b] is put in a [Elet a b] context. *) + +Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr := + match a with + | Evar id => Evar id + | Eop op bl => Eop op (lift_exprlist p bl) + | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl) + | Econdition b c d => + Econdition (lift_condexpr p b) (lift_expr p c) (lift_expr p d) + | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c) + | Eletvar n => + if le_gt_dec p n then Eletvar (S n) else Eletvar n + end + +with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr := + match a with + | CEtrue => CEtrue + | CEfalse => CEfalse + | CEcond cond bl => CEcond cond (lift_exprlist p bl) + | CEcondition b c d => + CEcondition (lift_condexpr p b) (lift_condexpr p c) (lift_condexpr p d) + end + +with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist := + match a with + | Enil => Enil + | Econs b cl => Econs (lift_expr p b) (lift_exprlist p cl) + end. + +Definition lift (a: expr): expr := lift_expr O a. + +(** We now relate the evaluation of a lifted expression with that + of the original expression. *) + +Inductive insert_lenv: letenv -> nat -> val -> letenv -> Prop := + | insert_lenv_0: + forall le v, + insert_lenv le O v (v :: le) + | insert_lenv_S: + forall le p w le' v, + insert_lenv le p w le' -> + insert_lenv (v :: le) (S p) w (v :: le'). + +Lemma insert_lenv_lookup1: + forall le p w le', + insert_lenv le p w le' -> + forall n v, + nth_error le n = Some v -> (p > n)%nat -> + nth_error le' n = Some v. +Proof. + induction 1; intros. + omegaContradiction. + destruct n; simpl; simpl in H0. auto. + apply IHinsert_lenv. auto. omega. +Qed. + +Lemma insert_lenv_lookup2: + forall le p w le', + insert_lenv le p w le' -> + forall n v, + nth_error le n = Some v -> (p <= n)%nat -> + nth_error le' (S n) = Some v. +Proof. + induction 1; intros. + simpl. assumption. + simpl. destruct n. omegaContradiction. + apply IHinsert_lenv. exact H0. omega. +Qed. + +Lemma eval_lift_expr: + forall ge sp e m w le a v, + eval_expr ge sp e m le a v -> + forall p le', insert_lenv le p w le' -> + eval_expr ge sp e m le' (lift_expr p a) v. +Proof. + intros until w. + apply (eval_expr_ind3 ge sp e m + (fun le a v => + forall p le', insert_lenv le p w le' -> + eval_expr ge sp e m le' (lift_expr p a) v) + (fun le a v => + forall p le', insert_lenv le p w le' -> + eval_condexpr ge sp e m le' (lift_condexpr p a) v) + (fun le al vl => + forall p le', insert_lenv le p w le' -> + eval_exprlist ge sp e m le' (lift_exprlist p al) vl)); + simpl; intros; eauto with evalexpr. + + destruct v1; eapply eval_Econdition; + eauto with evalexpr; simpl; eauto with evalexpr. + + eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. + + case (le_gt_dec p n); intro. + apply eval_Eletvar. eapply insert_lenv_lookup2; eauto. + apply eval_Eletvar. eapply insert_lenv_lookup1; eauto. + + destruct vb1; eapply eval_CEcondition; + eauto with evalexpr; simpl; eauto with evalexpr. +Qed. + +Lemma eval_lift: + forall ge sp e m le a v w, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m (w::le) (lift a) v. +Proof. + intros. unfold lift. eapply eval_lift_expr. + eexact H. apply insert_lenv_0. +Qed. + +Hint Resolve eval_lift: evalexpr. + diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index aa327731..e86b7dc4 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -182,8 +182,8 @@ let (text, data, const_data, float_literal) = | Diab -> (".text", ".data", - ".const", (* to check *) - ".const") (* to check *) + ".data", (* to check *) + ".data") (* to check *) (* Encoding masks for rlwinm instructions *) diff --git a/powerpc/Selection.v b/powerpc/SelectOp.v index 286517ef..ef55b8bb 100644 --- a/powerpc/Selection.v +++ b/powerpc/SelectOp.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Instruction selection *) +(** Instruction selection for operators *) (** The instruction selection pass recognizes opportunities for using combined arithmetic and logical operations and addressing modes @@ -19,8 +19,22 @@ and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned into a "rotate and mask" instruction. - Instruction selection proceeds by bottom-up rewriting over expressions. - The source language is Cminor and the target language is CminorSel. *) + This file defines functions for building CminorSel expressions and + statements, especially expressions consisting of operator + applications. These functions examine their arguments to choose + cheaper forms of operators whenever possible. + + For instance, [add e1 e2] will return a CminorSel expression semantically + equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a + [Oaddimm] operator if one of the arguments is an integer constant, + or suppress the addition altogether if one of the arguments is the + null integer. In passing, we perform operator reassociation + ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount + of constant propagation. + + On top of the "smart constructor" functions defined below, + module [Selection] implements the actual instruction selection pass. +*) Require Import Coqlib. Require Import Maps. @@ -34,61 +48,7 @@ Require Cminor. Require Import Op. Require Import CminorSel. -Infix ":::" := Econs (at level 60, right associativity) : selection_scope. - -Open Local Scope selection_scope. - -(** * Lifting of let-bound variables *) - -(** Some of the instruction functions generate [Elet] constructs to - share the evaluation of a subexpression. Owing to the use of de - Bruijn indices for let-bound variables, we need to shift de Bruijn - indices when an expression [b] is put in a [Elet a b] context. *) - -Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr := - match a with - | Evar id => Evar id - | Eop op bl => Eop op (lift_exprlist p bl) - | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl) - | Econdition b c d => - Econdition (lift_condexpr p b) (lift_expr p c) (lift_expr p d) - | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c) - | Eletvar n => - if le_gt_dec p n then Eletvar (S n) else Eletvar n - end - -with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr := - match a with - | CEtrue => CEtrue - | CEfalse => CEfalse - | CEcond cond bl => CEcond cond (lift_exprlist p bl) - | CEcondition b c d => - CEcondition (lift_condexpr p b) (lift_condexpr p c) (lift_condexpr p d) - end - -with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist := - match a with - | Enil => Enil - | Econs b cl => Econs (lift_expr p b) (lift_exprlist p cl) - end. - -Definition lift (a: expr): expr := lift_expr O a. - -(** * Smart constructors for operators *) - -(** This section defines functions for building CminorSel expressions - and statements, especially expressions consisting of operator - applications. These functions examine their arguments to choose - cheaper forms of operators whenever possible. - - For instance, [add e1 e2] will return a CminorSel expression semantically - equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a - [Oaddimm] operator if one of the arguments is an integer constant, - or suppress the addition altogether if one of the arguments is the - null integer. In passing, we perform operator reassociation - ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount - of constant propagation. -*) +Open Local Scope cminorsel_scope. (** ** Integer logical negation *) @@ -984,50 +944,19 @@ Definition compu (c: comparison) (e1: expr) (e2: expr) := Definition compf (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). -(** ** Conditional expressions *) +(** ** Other operators, not optimized. *) -Fixpoint negate_condexpr (e: condexpr): condexpr := - match e with - | CEtrue => CEfalse - | CEfalse => CEtrue - | CEcond c el => CEcond (negate_condition c) el - | CEcondition e1 e2 e3 => - CEcondition e1 (negate_condexpr e2) (negate_condexpr e3) - end. - - -Definition is_compare_neq_zero (c: condition) : bool := - match c with - | Ccompimm Cne n => Int.eq n Int.zero - | Ccompuimm Cne n => Int.eq n Int.zero - | _ => false - end. - -Definition is_compare_eq_zero (c: condition) : bool := - match c with - | Ccompimm Ceq n => Int.eq n Int.zero - | Ccompuimm Ceq n => Int.eq n Int.zero - | _ => false - end. - -Fixpoint condexpr_of_expr (e: expr) : condexpr := - match e with - | Eop (Ointconst n) Enil => - if Int.eq n Int.zero then CEfalse else CEtrue - | Eop (Ocmp c) (e1 ::: Enil) => - if is_compare_neq_zero c then - condexpr_of_expr e1 - else if is_compare_eq_zero c then - negate_condexpr (condexpr_of_expr e1) - else - CEcond c (e1 ::: Enil) - | Eop (Ocmp c) el => - CEcond c el - | Econdition ce e1 e2 => - CEcondition ce (condexpr_of_expr e1) (condexpr_of_expr e2) - | _ => - CEcond (Ccompimm Cne Int.zero) (e:::Enil) - end. +Definition negint (e: expr) := Eop (Osubimm Int.zero) (e ::: Enil). +Definition negf (e: expr) := Eop Onegf (e ::: Enil). +Definition absf (e: expr) := Eop Oabsf (e ::: Enil). +Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). +Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). +Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). +Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil). +Definition xor (e1 e2: expr) := Eop Oxor (e1 ::: e2 ::: Enil). +Definition shr (e1 e2: expr) := Eop Oshr (e1 ::: e2 ::: Enil). +Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). +Definition divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). (** ** Recognition of addressing modes for load and store operations *) @@ -1080,7 +1009,7 @@ Definition addressing_match (e: expr) := addressing_default e end. -Definition addressing (e: expr) := +Definition addressing (chunk: memory_chunk) (e: expr) := match addressing_match e with | addressing_case1 s n => (Aglobal s n, Enil) @@ -1095,131 +1024,3 @@ Definition addressing (e: expr) := | addressing_default e => (Aindexed Int.zero, e:::Enil) end. - -Definition load (chunk: memory_chunk) (e1: expr) := - match addressing e1 with - | (mode, args) => Eload chunk mode args - end. - -Definition store (chunk: memory_chunk) (e1 e2: expr) := - match addressing e1 with - | (mode, args) => Sstore chunk mode args e2 - end. - -(** * Translation from Cminor to CminorSel *) - -(** Instruction selection for operator applications *) - -Definition sel_constant (cst: Cminor.constant) : expr := - match cst with - | Cminor.Ointconst n => Eop (Ointconst n) Enil - | Cminor.Ofloatconst f => Eop (Ofloatconst f) Enil - | Cminor.Oaddrsymbol id ofs => Eop (Oaddrsymbol id ofs) Enil - | Cminor.Oaddrstack ofs => Eop (Oaddrstack ofs) Enil - end. - -Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := - match op with - | Cminor.Ocast8unsigned => cast8unsigned arg - | Cminor.Ocast8signed => cast8signed arg - | Cminor.Ocast16unsigned => cast16unsigned arg - | Cminor.Ocast16signed => cast16signed arg - | Cminor.Onegint => Eop (Osubimm Int.zero) (arg ::: Enil) - | Cminor.Onotbool => notbool arg - | Cminor.Onotint => notint arg - | Cminor.Onegf => Eop Onegf (arg ::: Enil) - | Cminor.Oabsf => Eop Oabsf (arg ::: Enil) - | Cminor.Osingleoffloat => singleoffloat arg - | Cminor.Ointoffloat => Eop Ointoffloat (arg ::: Enil) - | Cminor.Ointuoffloat => Eop Ointuoffloat (arg ::: Enil) - | Cminor.Ofloatofint => Eop Ofloatofint (arg ::: Enil) - | Cminor.Ofloatofintu => Eop Ofloatofintu (arg ::: Enil) - end. - -Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := - match op with - | Cminor.Oadd => add arg1 arg2 - | Cminor.Osub => sub arg1 arg2 - | Cminor.Omul => mul arg1 arg2 - | Cminor.Odiv => divs arg1 arg2 - | Cminor.Odivu => divu arg1 arg2 - | Cminor.Omod => mods arg1 arg2 - | Cminor.Omodu => modu arg1 arg2 - | Cminor.Oand => and arg1 arg2 - | Cminor.Oor => or arg1 arg2 - | Cminor.Oxor => Eop Oxor (arg1 ::: arg2 ::: Enil) - | Cminor.Oshl => shl arg1 arg2 - | Cminor.Oshr => Eop Oshr (arg1 ::: arg2 ::: Enil) - | Cminor.Oshru => shru arg1 arg2 - | Cminor.Oaddf => addf arg1 arg2 - | Cminor.Osubf => subf arg1 arg2 - | Cminor.Omulf => Eop Omulf (arg1 ::: arg2 ::: Enil) - | Cminor.Odivf => Eop Odivf (arg1 ::: arg2 ::: Enil) - | Cminor.Ocmp c => comp c arg1 arg2 - | Cminor.Ocmpu c => compu c arg1 arg2 - | Cminor.Ocmpf c => compf c arg1 arg2 - end. - -(** Conversion from Cminor expression to Cminorsel expressions *) - -Fixpoint sel_expr (a: Cminor.expr) : expr := - match a with - | Cminor.Evar id => Evar id - | Cminor.Econst cst => sel_constant cst - | Cminor.Eunop op arg => sel_unop op (sel_expr arg) - | Cminor.Ebinop op arg1 arg2 => sel_binop op (sel_expr arg1) (sel_expr arg2) - | Cminor.Eload chunk addr => load chunk (sel_expr addr) - | Cminor.Econdition cond ifso ifnot => - Econdition (condexpr_of_expr (sel_expr cond)) - (sel_expr ifso) (sel_expr ifnot) - end. - -Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist := - match al with - | nil => Enil - | a :: bl => Econs (sel_expr a) (sel_exprlist bl) - end. - -(** Conversion from Cminor statements to Cminorsel statements. *) - -Fixpoint sel_stmt (s: Cminor.stmt) : stmt := - match s with - | Cminor.Sskip => Sskip - | Cminor.Sassign id e => Sassign id (sel_expr e) - | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs) - | Cminor.Scall optid sg fn args => - Scall optid sg (sel_expr fn) (sel_exprlist args) - | Cminor.Stailcall sg fn args => - Stailcall sg (sel_expr fn) (sel_exprlist args) - | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2) - | Cminor.Sifthenelse e ifso ifnot => - Sifthenelse (condexpr_of_expr (sel_expr e)) - (sel_stmt ifso) (sel_stmt ifnot) - | Cminor.Sloop body => Sloop (sel_stmt body) - | Cminor.Sblock body => Sblock (sel_stmt body) - | Cminor.Sexit n => Sexit n - | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl - | Cminor.Sreturn None => Sreturn None - | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e)) - | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body) - | Cminor.Sgoto lbl => Sgoto lbl - end. - -(** Conversion of functions and programs. *) - -Definition sel_function (f: Cminor.function) : function := - mkfunction - f.(Cminor.fn_sig) - f.(Cminor.fn_params) - f.(Cminor.fn_vars) - f.(Cminor.fn_stackspace) - (sel_stmt f.(Cminor.fn_body)). - -Definition sel_fundef (f: Cminor.fundef) : fundef := - transf_fundef sel_function f. - -Definition sel_program (p: Cminor.program) : program := - transform_program sel_fundef p. - - - diff --git a/powerpc/Selectionproof.v b/powerpc/SelectOpproof.v index 27e9ee47..77bca504 100644 --- a/powerpc/Selectionproof.v +++ b/powerpc/SelectOpproof.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Correctness of instruction selection *) +(** Correctness of instruction selection for operators *) Require Import Coqlib. Require Import Maps. @@ -25,9 +25,9 @@ Require Import Smallstep. Require Import Cminor. Require Import Op. Require Import CminorSel. -Require Import Selection. +Require Import SelectOp. -Open Local Scope selection_scope. +Open Local Scope cminorsel_scope. Section CMCONSTR. @@ -36,91 +36,6 @@ Variable sp: val. Variable e: env. Variable m: mem. -(** * Lifting of let-bound variables *) - -Inductive insert_lenv: letenv -> nat -> val -> letenv -> Prop := - | insert_lenv_0: - forall le v, - insert_lenv le O v (v :: le) - | insert_lenv_S: - forall le p w le' v, - insert_lenv le p w le' -> - insert_lenv (v :: le) (S p) w (v :: le'). - -Lemma insert_lenv_lookup1: - forall le p w le', - insert_lenv le p w le' -> - forall n v, - nth_error le n = Some v -> (p > n)%nat -> - nth_error le' n = Some v. -Proof. - induction 1; intros. - omegaContradiction. - destruct n; simpl; simpl in H0. auto. - apply IHinsert_lenv. auto. omega. -Qed. - -Lemma insert_lenv_lookup2: - forall le p w le', - insert_lenv le p w le' -> - forall n v, - nth_error le n = Some v -> (p <= n)%nat -> - nth_error le' (S n) = Some v. -Proof. - induction 1; intros. - simpl. assumption. - simpl. destruct n. omegaContradiction. - apply IHinsert_lenv. exact H0. omega. -Qed. - -Hint Resolve eval_Evar eval_Eop eval_Eload eval_Econdition - eval_Elet eval_Eletvar - eval_CEtrue eval_CEfalse eval_CEcond - eval_CEcondition eval_Enil eval_Econs: evalexpr. - -Lemma eval_lift_expr: - forall w le a v, - eval_expr ge sp e m le a v -> - forall p le', insert_lenv le p w le' -> - eval_expr ge sp e m le' (lift_expr p a) v. -Proof. - intro w. - apply (eval_expr_ind3 ge sp e m - (fun le a v => - forall p le', insert_lenv le p w le' -> - eval_expr ge sp e m le' (lift_expr p a) v) - (fun le a v => - forall p le', insert_lenv le p w le' -> - eval_condexpr ge sp e m le' (lift_condexpr p a) v) - (fun le al vl => - forall p le', insert_lenv le p w le' -> - eval_exprlist ge sp e m le' (lift_exprlist p al) vl)); - simpl; intros; eauto with evalexpr. - - destruct v1; eapply eval_Econdition; - eauto with evalexpr; simpl; eauto with evalexpr. - - eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. - - case (le_gt_dec p n); intro. - apply eval_Eletvar. eapply insert_lenv_lookup2; eauto. - apply eval_Eletvar. eapply insert_lenv_lookup1; eauto. - - destruct vb1; eapply eval_CEcondition; - eauto with evalexpr; simpl; eauto with evalexpr. -Qed. - -Lemma eval_lift: - forall le a v w, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m (w::le) (lift a) v. -Proof. - intros. unfold lift. eapply eval_lift_expr. - eexact H. apply insert_lenv_0. -Qed. - -Hint Resolve eval_lift: evalexpr. - (** * Useful lemmas and tactics *) (** The following are trivial lemmas and custom tactics that help @@ -166,9 +81,9 @@ Ltac InvEval := InvEval1; InvEval2; InvEval2. (** * Correctness of the smart constructors *) (** We now show that the code generated by "smart constructor" functions - such as [Selection.notint] behaves as expected. Continuing the + such as [SelectOp.notint] behaves as expected. Continuing the [notint] example, we show that if the expression [e] - evaluates to some integer value [Vint n], then [Selection.notint e] + evaluates to some integer value [Vint n], then [SelectOp.notint e] evaluates to a value [Vint (Int.not n)] which is indeed the integer negation of the value of [e]. @@ -940,138 +855,82 @@ Proof. destruct (Float.cmp c x y); reflexivity. Qed. -Lemma negate_condexpr_correct: - forall le a b, - eval_condexpr ge sp e m le a b -> - eval_condexpr ge sp e m le (negate_condexpr a) (negb b). -Proof. - induction 1; simpl. - constructor. - constructor. - econstructor. eauto. apply eval_negate_condition. auto. - econstructor. eauto. destruct vb1; auto. -Qed. +Theorem eval_negint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (negint a) (Vint (Int.neg x)). +Proof. intros; unfold negint; EvalOp. Qed. -Scheme expr_ind2 := Induction for expr Sort Prop - with exprlist_ind2 := Induction for exprlist Sort Prop. +Theorem eval_negf: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (negf a) (Vfloat (Float.neg x)). +Proof. intros; unfold negf; EvalOp. Qed. -Fixpoint forall_exprlist (P: expr -> Prop) (el: exprlist) {struct el}: Prop := - match el with - | Enil => True - | Econs e el' => P e /\ forall_exprlist P el' - end. +Theorem eval_absf: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (absf a) (Vfloat (Float.abs x)). +Proof. intros; unfold absf; EvalOp. Qed. -Lemma expr_induction_principle: - forall (P: expr -> Prop), - (forall i : ident, P (Evar i)) -> - (forall (o : operation) (e : exprlist), - forall_exprlist P e -> P (Eop o e)) -> - (forall (m : memory_chunk) (a : Op.addressing) (e : exprlist), - forall_exprlist P e -> P (Eload m a e)) -> - (forall (c : condexpr) (e : expr), - P e -> forall e0 : expr, P e0 -> P (Econdition c e e0)) -> - (forall e : expr, P e -> forall e0 : expr, P e0 -> P (Elet e e0)) -> - (forall n : nat, P (Eletvar n)) -> - forall e : expr, P e. -Proof. - intros. apply expr_ind2 with (P := P) (P0 := forall_exprlist P); auto. - simpl. auto. - intros. simpl. auto. -Qed. +Theorem eval_intoffloat: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)). +Proof. intros; unfold intoffloat; EvalOp. Qed. -Lemma eval_base_condition_of_expr: - forall le a v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_condexpr ge sp e m le - (CEcond (Ccompimm Cne Int.zero) (a ::: Enil)) - b. -Proof. - intros. - eapply eval_CEcond. eauto with evalexpr. - inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto. -Qed. +Theorem eval_intuoffloat: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)). +Proof. intros; unfold intuoffloat; EvalOp. Qed. -Lemma is_compare_neq_zero_correct: - forall c v b, - is_compare_neq_zero c = true -> - eval_condition c (v :: nil) = Some b -> - Val.bool_of_val v b. -Proof. - intros. - destruct c; simpl in H; try discriminate; - destruct c; simpl in H; try discriminate; - generalize (Int.eq_spec i Int.zero); rewrite H; intro; subst i. - - simpl in H0. destruct v; inv H0. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. - subst i; constructor. constructor; auto. constructor. - - simpl in H0. destruct v; inv H0. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. - subst i; constructor. constructor; auto. -Qed. +Theorem eval_floatofint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)). +Proof. intros; unfold floatofint; EvalOp. Qed. -Lemma is_compare_eq_zero_correct: - forall c v b, - is_compare_eq_zero c = true -> - eval_condition c (v :: nil) = Some b -> - Val.bool_of_val v (negb b). -Proof. - intros. apply is_compare_neq_zero_correct with (negate_condition c). - destruct c; simpl in H; simpl; try discriminate; - destruct c; simpl; try discriminate; auto. - apply eval_negate_condition; auto. -Qed. +Theorem eval_floatofintu: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)). +Proof. intros; unfold floatofintu; EvalOp. Qed. -Lemma eval_condition_of_expr: - forall a le v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_condexpr ge sp e m le (condexpr_of_expr a) b. -Proof. - intro a0; pattern a0. - apply expr_induction_principle; simpl; intros; - try (eapply eval_base_condition_of_expr; eauto; fail). - - destruct o; try (eapply eval_base_condition_of_expr; eauto; fail). +Theorem eval_xor: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (xor a b) (Vint (Int.xor x y)). +Proof. intros; unfold xor; EvalOp. Qed. - destruct e0. InvEval. - inversion H1. - rewrite Int.eq_false; auto. constructor. - subst i; rewrite Int.eq_true. constructor. - eapply eval_base_condition_of_expr; eauto. - - inv H0. simpl in H7. - assert (eval_condition c vl = Some b). - destruct (eval_condition c vl); try discriminate. - destruct b0; inv H7; inversion H1; congruence. - assert (eval_condexpr ge sp e m le (CEcond c e0) b). - eapply eval_CEcond; eauto. - destruct e0; auto. destruct e1; auto. - simpl in H. destruct H. - inv H5. inv H11. - - case_eq (is_compare_neq_zero c); intros. - eapply H; eauto. - apply is_compare_neq_zero_correct with c; auto. - - case_eq (is_compare_eq_zero c); intros. - replace b with (negb (negb b)). apply negate_condexpr_correct. - eapply H; eauto. - apply is_compare_eq_zero_correct with c; auto. - apply negb_involutive. - - auto. - - inv H1. destruct v1; eauto with evalexpr. -Qed. +Theorem eval_shr: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + Int.ltu y (Int.repr 32) = true -> + eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)). +Proof. intros; unfold shr; EvalOp. simpl. rewrite H1. auto. Qed. -Lemma eval_addressing: - forall le a v b ofs, +Theorem eval_mulf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (mulf a b) (Vfloat (Float.mul x y)). +Proof. intros; unfold mulf; EvalOp. Qed. + +Theorem eval_divf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (divf a b) (Vfloat (Float.div x y)). +Proof. intros; unfold divf; EvalOp. Qed. + +Theorem eval_addressing: + forall le chunk a v b ofs, eval_expr ge sp e m le a v -> v = Vptr b ofs -> - match addressing a with (mode, args) => + match addressing chunk a with (mode, args) => exists vl, eval_exprlist ge sp e m le args vl /\ eval_addressing ge sp mode vl = Some v @@ -1094,340 +953,5 @@ Proof. subst v. simpl. rewrite Int.add_zero. auto. Qed. -Lemma eval_load: - forall le a v chunk v', - eval_expr ge sp e m le a v -> - Mem.loadv chunk m v = Some v' -> - eval_expr ge sp e m le (load chunk a) v'. -Proof. - intros. generalize H0; destruct v; simpl; intro; try discriminate. - unfold load. - generalize (eval_addressing _ _ _ _ _ H (refl_equal _)). - destruct (addressing a). intros [vl [EV EQ]]. - eapply eval_Eload; eauto. -Qed. - -Lemma eval_store: - forall chunk a1 a2 v1 v2 f k m', - eval_expr ge sp e m nil a1 v1 -> - eval_expr ge sp e m nil a2 v2 -> - Mem.storev chunk m v1 v2 = Some m' -> - step ge (State f (store chunk a1 a2) k sp e m) - E0 (State f Sskip k sp e m'). -Proof. - intros. generalize H1; destruct v1; simpl; intro; try discriminate. - unfold store. - generalize (eval_addressing _ _ _ _ _ H (refl_equal _)). - destruct (addressing a1). intros [vl [EV EQ]]. - eapply step_store; eauto. -Qed. - -(** * Correctness of instruction selection for operators *) - -(** We now prove a semantic preservation result for the [sel_unop] - and [sel_binop] selection functions. The proof exploits - the results of the previous section. *) - -Lemma eval_sel_unop: - forall le op a1 v1 v, - eval_expr ge sp e m le a1 v1 -> - eval_unop op v1 = Some v -> - eval_expr ge sp e m le (sel_unop op a1) v. -Proof. - destruct op; simpl; intros; FuncInv; try subst v. - apply eval_cast8unsigned; auto. - apply eval_cast8signed; auto. - apply eval_cast16unsigned; auto. - apply eval_cast16signed; auto. - EvalOp. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro. - change true with (negb false). eapply eval_notbool; eauto. subst i; constructor. - change false with (negb true). eapply eval_notbool; eauto. constructor; auto. - change Vfalse with (Val.of_bool (negb true)). - eapply eval_notbool; eauto. constructor. - apply eval_notint; auto. - EvalOp. - EvalOp. - apply eval_singleoffloat; auto. - EvalOp. - EvalOp. - EvalOp. - EvalOp. -Qed. - -Lemma eval_sel_binop: - forall le op a1 a2 v1 v2 v, - eval_expr ge sp e m le a1 v1 -> - eval_expr ge sp e m le a2 v2 -> - eval_binop op v1 v2 = Some v -> - eval_expr ge sp e m le (sel_binop op a1 a2) v. -Proof. - destruct op; simpl; intros; FuncInv; try subst v. - apply eval_add; auto. - apply eval_add_ptr_2; auto. - apply eval_add_ptr; auto. - apply eval_sub; auto. - apply eval_sub_ptr_int; auto. - destruct (eq_block b b0); inv H1. - eapply eval_sub_ptr_ptr; eauto. - apply eval_mul; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_divs; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_divu; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_mods; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_modu; eauto. - apply eval_and; auto. - apply eval_or; auto. - EvalOp. - caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - apply eval_shl; auto. - EvalOp. - caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - apply eval_shru; auto. - apply eval_addf; auto. - apply eval_subf; auto. - EvalOp. - EvalOp. - apply eval_comp_int; auto. - eapply eval_comp_int_ptr; eauto. - eapply eval_comp_ptr_int; eauto. - destruct (eq_block b b0); inv H1. - eapply eval_comp_ptr_ptr; eauto. - eapply eval_comp_ptr_ptr_2; eauto. - eapply eval_compu; eauto. - eapply eval_compf; eauto. -Qed. - End CMCONSTR. -(** * Semantic preservation for instruction selection. *) - -Section PRESERVATION. - -Variable prog: Cminor.program. -Let tprog := sel_program prog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -(** Relationship between the global environments for the original - CminorSel program and the generated RTL program. *) - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, sel_program. - apply Genv.find_symbol_transf. -Qed. - -Lemma functions_translated: - forall (v: val) (f: Cminor.fundef), - Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (sel_fundef f). -Proof. - intros. - exact (Genv.find_funct_transf sel_fundef H). -Qed. - -Lemma function_ptr_translated: - forall (b: block) (f: Cminor.fundef), - Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (sel_fundef f). -Proof. - intros. - exact (Genv.find_funct_ptr_transf sel_fundef H). -Qed. - -Lemma sig_function_translated: - forall f, - funsig (sel_fundef f) = Cminor.funsig f. -Proof. - intros. destruct f; reflexivity. -Qed. - -(** Semantic preservation for expressions. *) - -Lemma sel_expr_correct: - forall sp e m a v, - Cminor.eval_expr ge sp e m a v -> - forall le, - eval_expr tge sp e m le (sel_expr a) v. -Proof. - induction 1; intros; simpl. - (* Evar *) - constructor; auto. - (* Econst *) - destruct cst; simpl; simpl in H; (econstructor; [constructor|simpl;auto]). - rewrite symbols_preserved. auto. - (* Eunop *) - eapply eval_sel_unop; eauto. - (* Ebinop *) - eapply eval_sel_binop; eauto. - (* Eload *) - eapply eval_load; eauto. - (* Econdition *) - econstructor; eauto. eapply eval_condition_of_expr; eauto. - destruct b1; auto. -Qed. - -Hint Resolve sel_expr_correct: evalexpr. - -Lemma sel_exprlist_correct: - forall sp e m a v, - Cminor.eval_exprlist ge sp e m a v -> - forall le, - eval_exprlist tge sp e m le (sel_exprlist a) v. -Proof. - induction 1; intros; simpl; constructor; auto with evalexpr. -Qed. - -Hint Resolve sel_exprlist_correct: evalexpr. - -(** Semantic preservation for terminating function calls and statements. *) - -Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont := - match k with - | Cminor.Kstop => Kstop - | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1) - | Cminor.Kblock k1 => Kblock (sel_cont k1) - | Cminor.Kcall id f sp e k1 => - Kcall id (sel_function f) sp e (sel_cont k1) - end. - -Inductive match_states: Cminor.state -> CminorSel.state -> Prop := - | match_state: forall f s k s' k' sp e m, - s' = sel_stmt s -> - k' = sel_cont k -> - match_states - (Cminor.State f s k sp e m) - (State (sel_function f) s' k' sp e m) - | match_callstate: forall f args k k' m, - k' = sel_cont k -> - match_states - (Cminor.Callstate f args k m) - (Callstate (sel_fundef f) args k' m) - | match_returnstate: forall v k k' m, - k' = sel_cont k -> - match_states - (Cminor.Returnstate v k m) - (Returnstate v k' m). - -Remark call_cont_commut: - forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k). -Proof. - induction k; simpl; auto. -Qed. - -Remark find_label_commut: - forall lbl s k, - find_label lbl (sel_stmt s) (sel_cont k) = - option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk))) - (Cminor.find_label lbl s k). -Proof. - induction s; intros; simpl; auto. - unfold store. destruct (addressing (sel_expr e)); auto. - change (Kseq (sel_stmt s2) (sel_cont k)) - with (sel_cont (Cminor.Kseq s2 k)). - rewrite IHs1. rewrite IHs2. - destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto. - rewrite IHs1. rewrite IHs2. - destruct (Cminor.find_label lbl s1 k); auto. - change (Kseq (Sloop (sel_stmt s)) (sel_cont k)) - with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)). - auto. - change (Kblock (sel_cont k)) - with (sel_cont (Cminor.Kblock k)). - auto. - destruct o; auto. - destruct (ident_eq lbl l); auto. -Qed. - -Lemma sel_step_correct: - forall S1 t S2, Cminor.step ge S1 t S2 -> - forall T1, match_states S1 T1 -> - exists T2, step tge T1 t T2 /\ match_states S2 T2. -Proof. - induction 1; intros T1 ME; inv ME; simpl; - try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail). - - (* skip call *) - econstructor; split. - econstructor. destruct k; simpl in H; simpl; auto. - rewrite <- H0; reflexivity. - constructor; auto. -(* - (* assign *) - exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split. - constructor. auto with evalexpr. - constructor; auto. -*) - (* store *) - econstructor; split. - eapply eval_store; eauto with evalexpr. - constructor; auto. - (* Scall *) - econstructor; split. - econstructor; eauto with evalexpr. - apply functions_translated; eauto. - apply sig_function_translated. - constructor; auto. - (* Stailcall *) - econstructor; split. - econstructor; eauto with evalexpr. - apply functions_translated; eauto. - apply sig_function_translated. - constructor; auto. apply call_cont_commut. - (* Sifthenelse *) - exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split. - constructor. eapply eval_condition_of_expr; eauto with evalexpr. - constructor; auto. destruct b; auto. - (* Sreturn None *) - econstructor; split. - econstructor. - constructor; auto. apply call_cont_commut. - (* Sreturn Some *) - econstructor; split. - econstructor. simpl. eauto with evalexpr. - constructor; auto. apply call_cont_commut. - (* Sgoto *) - econstructor; split. - econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut. - rewrite H. simpl. reflexivity. - constructor; auto. -Qed. - -Lemma sel_initial_states: - forall S, Cminor.initial_state prog S -> - exists R, initial_state tprog R /\ match_states S R. -Proof. - induction 1. - econstructor; split. - econstructor. - simpl. fold tge. rewrite symbols_preserved. eexact H. - apply function_ptr_translated. eauto. - rewrite <- H1. apply sig_function_translated; auto. - unfold tprog, sel_program. rewrite Genv.init_mem_transf. - constructor; auto. -Qed. - -Lemma sel_final_states: - forall S R r, - match_states S R -> Cminor.final_state S r -> final_state R r. -Proof. - intros. inv H0. inv H. simpl. constructor. -Qed. - -Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. -Proof. - unfold CminorSel.exec_program, Cminor.exec_program; intros. - eapply simulation_step_preservation; eauto. - eexact sel_initial_states. - eexact sel_final_states. - exact sel_step_correct. -Qed. - -End PRESERVATION. |