From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asm.v | 112 ++--- powerpc/Asmgen.v | 157 +++--- powerpc/Asmgenproof.v | 472 ++++++++++-------- powerpc/Asmgenproof1.v | 1074 +++++++++++++++++++---------------------- powerpc/Asmgenretaddr.v | 10 +- powerpc/ConstpropOp.v | 30 +- powerpc/Machregs.v | 27 +- powerpc/Machregsaux.ml | 7 +- powerpc/Op.v | 90 +++- powerpc/PrintAsm.ml | 62 +-- powerpc/PrintOp.ml | 6 +- powerpc/SelectOp.v | 179 ++----- powerpc/SelectOpproof.v | 106 ++-- powerpc/eabi/Conventions1.v | 5 +- powerpc/macosx/Conventions1.v | 10 +- 15 files changed, 1080 insertions(+), 1267 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 9da58710..e49986f6 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -159,17 +159,15 @@ Inductive instruction : Type := | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) | Pfcmpu: freg -> freg -> instruction (**r float comparison *) | Pfcti: ireg -> freg -> instruction (**r float-to-signed-int conversion *) - | Pfctiu: ireg -> freg -> instruction (**r float-to-unsigned-int conversion *) | Pfdiv: freg -> freg -> freg -> instruction (**r float division *) | Pfmadd: freg -> freg -> freg -> freg -> instruction (**r float multiply-add *) + | Pfmake: freg -> ireg -> ireg -> instruction (**r build a float from 2 ints *) | Pfmr: freg -> freg -> instruction (**r float move *) | Pfmsub: freg -> freg -> freg -> freg -> instruction (**r float multiply-sub *) | Pfmul: freg -> freg -> freg -> instruction (**r float multiply *) | Pfneg: freg -> freg -> instruction (**r float negation *) | Pfrsp: freg -> freg -> instruction (**r float round to single precision *) | Pfsub: freg -> freg -> freg -> instruction (**r float subtraction *) - | Pictf: freg -> ireg -> instruction (**r int-to-float conversion *) - | Piuctf: freg -> ireg -> instruction (**r unsigned int-to-float conversion *) | Plbz: ireg -> constant -> ireg -> instruction (**r load 8-bit unsigned int *) | Plbzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plfd: freg -> constant -> ireg -> instruction (**r load 64-bit float *) @@ -235,72 +233,21 @@ lbl: .double floatcst Initialized data in the constant data section are not modeled here, which is why we use a pseudo-instruction for this purpose. - [Pfcti]: convert a float to a signed integer. This requires a transfer - via memory of a 32-bit integer from a float register to an int register, - which our memory model cannot express. Expands to: + via memory of a 32-bit integer from a float register to an int register. + Expands to: << fctiwz f13, rsrc stfdu f13, -8(r1) lwz rdst, 4(r1) addi r1, r1, 8 >> -- [Pfctiu]: convert a float to an unsigned integer. The PowerPC way - to do this is to compare the argument against the floating-point - constant [2^31], subtract [2^31] if bigger, then convert to a signed - integer as above, then add back [2^31] if needed. Expands to: +- [Pfmake]: build a double float from two 32-bit integers. This also + requires a transfer via memory. Expands to: << - addis r12, 0, ha16(lbl1) - lfd f13, lo16(lbl1)(r12) - fcmpu cr7, rsrc, f13 - cror 30, 29, 30 - beq cr7, lbl2 - fctiwz f13, rsrc - stfdu f13, -8(r1) - lwz rdst, 4(r1) - b lbl3 -lbl2: fsub f13, rsrc, f13 - fctiwz f13, f13 - stfdu f13, -8(r1) - lwz rdst, 4(r1) - addis rdst, rdst, 0x8000 -lbl3: addi r1, r1, 8 - .const_data -lbl1: .long 0x41e00000, 0x00000000 # 2^31 in double precision - .text ->> -- [Pictf]: convert a signed integer to a float. This requires complicated - bit-level manipulations of IEEE floats through mixed float and integer - arithmetic over a memory word, which our memory model and axiomatization - of floats cannot express. Expands to: -<< - addis r12, 0, 0x4330 - stwu r12, -8(r1) - addis r12, rsrc, 0x8000 - stw r12, 4(r1) - addis r12, 0, ha16(lbl) - lfd f13, lo16(lbl)(r12) + stwu rsrc1, -8(r1) + stw rsrc2, 4(r1) lfd rdst, 0(r1) addi r1, r1, 8 - fsub rdst, rdst, f13 - .const_data -lbl: .long 0x43300000, 0x80000000 - .text ->> - (Don't worry if you do not understand this instruction sequence: intimate - knowledge of IEEE float arithmetic is necessary.) -- [Piuctf]: convert an unsigned integer to a float. The expansion is close - to that [Pictf], and equally obscure. -<< - addis r12, 0, 0x4330 - stwu r12, -8(r1) - stw rsrc, 4(r1) - addis r12, 0, ha16(lbl) - lfd f13, lo16(lbl)(r12) - lfd rdst, 0(r1) - addi r1, r1, 8 - fsub rdst, rdst, f13 - .const_data -lbl: .long 0x43300000, 0x00000000 - .text >> - [Pallocframe lo hi ofs]: in the formal semantics, this pseudo-instruction allocates a memory block with bounds [lo] and [hi], stores the value @@ -585,7 +532,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome let sp := Vptr stk (Int.repr lo) in match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with | None => Error - | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR12 <- Vundef)) m2 + | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)) m2 end | Pand_ rd r1 r2 => let v := Val.and rs#r1 rs#r2 in @@ -621,7 +568,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | _ => Error end | Pbtbl r tbl => - match rs#r with + match gpr_or_zero rs r with | Vint n => let pos := Int.signed n in if zeq (Zmod pos 4) 0 then @@ -672,13 +619,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pfcmpu r1 r2 => OK (nextinstr (compare_float rs rs#r1 rs#r2)) m | Pfcti rd r1 => - OK (nextinstr (rs#rd <- (Val.intoffloat rs#r1) #FPR13 <- Vundef)) m - | Pfctiu rd r1 => - OK (nextinstr (rs#rd <- (Val.intuoffloat rs#r1) #FPR13 <- Vundef)) m + OK (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.intoffloat rs#r1))) m | Pfdiv rd r1 r2 => OK (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m | Pfmadd rd r1 r2 r3 => OK (nextinstr (rs#rd <- (Val.addf (Val.mulf rs#r1 rs#r2) rs#r3))) m + | Pfmake rd r1 r2 => + OK (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m | Pfmr rd r1 => OK (nextinstr (rs#rd <- (rs#r1))) m | Pfmsub rd r1 r2 r3 => @@ -691,10 +638,6 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m | Pfsub rd r1 r2 => OK (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m - | Pictf rd r1 => - OK (nextinstr (rs#rd <- (Val.floatofint rs#r1) #GPR12 <- Vundef #FPR13 <- Vundef)) m - | Piuctf rd r1 => - OK (nextinstr (rs#rd <- (Val.floatofintu rs#r1) #GPR12 <- Vundef #FPR13 <- Vundef)) m | Plbz rd cst r1 => load1 Mint8unsigned rd cst r1 rs m | Plbzx rd r1 r2 => @@ -716,7 +659,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Plhzx rd r1 r2 => load2 Mint16unsigned rd r1 r2 rs m | Plfi rd f => - OK (nextinstr (rs#rd <- (Vfloat f) #GPR12 <- Vundef)) m + OK (nextinstr (rs #GPR12 <- Vundef #rd <- (Vfloat f))) m | Plwz rd cst r1 => load1 Mint32 rd cst r1 rs m | Plwzx rd r1 r2 => @@ -766,9 +709,15 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pstfdx rd r1 r2 => store2 Mfloat64 rd r1 r2 rs m | Pstfs rd cst r1 => - store1 Mfloat32 rd cst r1 (rs#FPR13 <- Vundef) m + match store1 Mfloat32 rd cst r1 rs m with + | OK rs' m' => OK (rs'#FPR13 <- Vundef) m' + | Error => Error + end | Pstfsx rd r1 r2 => - store2 Mfloat32 rd r1 r2 (rs#FPR13 <- Vundef) m + match store2 Mfloat32 rd r1 r2 rs m with + | OK rs' m' => OK (rs'#FPR13 <- Vundef) m' + | Error => Error + end | Psth rd cst r1 => store1 Mint16unsigned rd cst r1 rs m | Psthx rd r1 r2 => @@ -801,8 +750,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome results when applied to a LTL register of the wrong type. The proof in [Asmgenproof] will show that this never happens. - Note that no LTL register maps to [GPR12] nor [FPR13]. - These two registers are reserved as temporaries, to be used + Note that no LTL register maps to [GPR0]. + This register is reserved as a temporary to be used by the generated PPC code. *) Definition ireg_of (r: mreg) : ireg := @@ -814,20 +763,21 @@ Definition ireg_of (r: mreg) : ireg := | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24 | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29 | R30 => GPR30 | R31 => GPR31 - | IT1 => GPR11 | IT2 => GPR0 - | _ => GPR0 (* should not happen *) + | IT1 => GPR11 | IT2 => GPR12 + | _ => GPR12 (* should not happen *) end. Definition freg_of (r: mreg) : freg := match r with | F1 => FPR1 | F2 => FPR2 | F3 => FPR3 | F4 => FPR4 | F5 => FPR5 | F6 => FPR6 | F7 => FPR7 | F8 => FPR8 - | F9 => FPR9 | F10 => FPR10 | F14 => FPR14 | F15 => FPR15 + | F9 => FPR9 | F10 => FPR10 | F11 => FPR11 + | F14 => FPR14 | F15 => FPR15 | F16 => FPR16 | F17 => FPR17 | F18 => FPR18 | F19 => FPR19 | F20 => FPR20 | F21 => FPR21 | F22 => FPR22 | F23 => FPR23 | F24 => FPR24 | F25 => FPR25 | F26 => FPR26 | F27 => FPR27 | F28 => FPR28 | F29 => FPR29 | F30 => FPR30 | F31 => FPR31 - | FT1 => FPR0 | FT2 => FPR11 | FT3 => FPR12 + | FT1 => FPR0 | FT2 => FPR12 | FT3 => FPR13 | _ => FPR0 (* should not happen *) end. @@ -886,7 +836,11 @@ Inductive step: state -> trace -> state -> Prop := Genv.find_funct_ptr ge b = Some (Internal c) -> find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) -> external_call ef ge (map rs args) m t v m' -> - step (State rs m) t (State (nextinstr(rs # res <- v)) m') + step (State rs m) t + (State (nextinstr(rs #GPR11 <- Vundef #GPR12 <- Vundef + #FPR12 <- Vundef #FPR13 <- Vundef + #FPR0 <- Vundef #CTR <- Vundef + #res <- v)) m') | exec_step_external: forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index b1b1245b..9c37c42f 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -60,7 +60,7 @@ Definition loadimm (r: ireg) (n: int) (k: code) := Paddis r GPR0 (Cint (high_u n)) :: Pori r r (Cint (low_u n)) :: k. -Definition addimm_1 (r1 r2: ireg) (n: int) (k: code) := +Definition addimm (r1 r2: ireg) (n: int) (k: code) := if Int.eq (high_s n) Int.zero then Paddi r1 r2 (Cint n) :: k else if Int.eq (low_s n) Int.zero then @@ -69,24 +69,13 @@ Definition addimm_1 (r1 r2: ireg) (n: int) (k: code) := Paddis r1 r2 (Cint (high_s n)) :: Paddi r1 r1 (Cint (low_s n)) :: k. -Definition addimm_2 (r1 r2: ireg) (n: int) (k: code) := - loadimm GPR12 n (Padd r1 r2 GPR12 :: k). - -Definition addimm (r1 r2: ireg) (n: int) (k: code) := - if ireg_eq r1 GPR0 then - addimm_2 r1 r2 n k - else if ireg_eq r2 GPR0 then - addimm_2 r1 r2 n k - else - addimm_1 r1 r2 n k. - Definition andimm (r1 r2: ireg) (n: int) (k: code) := if Int.eq (high_u n) Int.zero then Pandi_ r1 r2 (Cint n) :: k else if Int.eq (low_u n) Int.zero then Pandis_ r1 r2 (Cint (high_u n)) :: k else - loadimm GPR12 n (Pand_ r1 r2 GPR12 :: k). + loadimm GPR0 n (Pand_ r1 r2 GPR0 :: k). Definition orimm (r1 r2: ireg) (n: int) (k: code) := if Int.eq (high_u n) Int.zero then @@ -106,36 +95,34 @@ Definition xorimm (r1 r2: ireg) (n: int) (k: code) := Pxoris r1 r2 (Cint (high_u n)) :: Pxori r1 r1 (Cint (low_u n)) :: k. -(** Smart constructors for indexed loads and stores, - where the address is the contents of a register plus - an integer literal. *) - -Definition loadind_aux (base: ireg) (ofs: int) (ty: typ) (dst: mreg) := - match ty with - | Tint => Plwz (ireg_of dst) (Cint ofs) base - | Tfloat => Plfd (freg_of dst) (Cint ofs) base - end. +(** Accessing slots in the stack frame. *) Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := if Int.eq (high_s ofs) Int.zero then - loadind_aux base ofs ty dst :: k + match ty with + | Tint => Plwz (ireg_of dst) (Cint ofs) base :: k + | Tfloat => Plfd (freg_of dst) (Cint ofs) base :: k + end else - Paddis GPR12 base (Cint (high_s ofs)) :: - loadind_aux GPR12 (low_s ofs) ty dst :: k. - -Definition storeind_aux (src: mreg) (base: ireg) (ofs: int) (ty: typ) := - match ty with - | Tint => Pstw (ireg_of src) (Cint ofs) base - | Tfloat => Pstfd (freg_of src) (Cint ofs) base - end. + loadimm GPR0 ofs + (match ty with + | Tint => Plwzx (ireg_of dst) base GPR0 :: k + | Tfloat => Plfdx (freg_of dst) base GPR0 :: k + end). Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := if Int.eq (high_s ofs) Int.zero then - storeind_aux src base ofs ty :: k + match ty with + | Tint => Pstw (ireg_of src) (Cint ofs) base :: k + | Tfloat => Pstfd (freg_of src) (Cint ofs) base :: k + end else - Paddis GPR12 base (Cint (high_s ofs)) :: - storeind_aux src GPR12 (low_s ofs) ty :: k. - + loadimm GPR0 ofs + (match ty with + | Tint => Pstwx (ireg_of src) base GPR0 :: k + | Tfloat => Pstfdx (freg_of src) base GPR0 :: k + end). + (** Constructor for a floating-point comparison. The PowerPC has a single [fcmpu] instruction to compare floats, which sets bits 0, 1 and 2 of the condition register to reflect ``less'', @@ -168,20 +155,20 @@ Definition transl_cond if Int.eq (high_s n) Int.zero then Pcmpwi (ireg_of a1) (Cint n) :: k else - loadimm GPR12 n (Pcmpw (ireg_of a1) GPR12 :: k) + loadimm GPR0 n (Pcmpw (ireg_of a1) GPR0 :: k) | Ccompuimm c n, a1 :: nil => if Int.eq (high_u n) Int.zero then Pcmplwi (ireg_of a1) (Cint n) :: k else - loadimm GPR12 n (Pcmplw (ireg_of a1) GPR12 :: k) + loadimm GPR0 n (Pcmplw (ireg_of a1) GPR0 :: k) | Ccompf cmp, a1 :: a2 :: nil => floatcomp cmp (freg_of a1) (freg_of a2) k | Cnotcompf cmp, a1 :: a2 :: nil => floatcomp cmp (freg_of a1) (freg_of a2) k | Cmaskzero n, a1 :: nil => - andimm GPR12 (ireg_of a1) n k + andimm GPR0 (ireg_of a1) n k | Cmasknotzero n, a1 :: nil => - andimm GPR12 (ireg_of a1) n k + andimm GPR0 (ireg_of a1) n k | _, _ => k (**r never happens for well-typed code *) end. @@ -287,14 +274,14 @@ Definition transl_op if Int.eq (high_s n) Int.zero then Psubfic (ireg_of r) (ireg_of a1) (Cint n) :: k else - loadimm GPR12 n (Psubfc (ireg_of r) (ireg_of a1) GPR12 :: k) + loadimm GPR0 n (Psubfc (ireg_of r) (ireg_of a1) GPR0 :: k) | Omul, a1 :: a2 :: nil => Pmullw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k | Omulimm n, a1 :: nil => if Int.eq (high_s n) Int.zero then Pmulli (ireg_of r) (ireg_of a1) (Cint n) :: k else - loadimm GPR12 n (Pmullw (ireg_of r) (ireg_of a1) GPR12 :: k) + loadimm GPR0 n (Pmullw (ireg_of r) (ireg_of a1) GPR0 :: k) | Odiv, a1 :: a2 :: nil => Pdivw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k | Odivu, a1 :: a2 :: nil => @@ -350,12 +337,8 @@ Definition transl_op Pfrsp (freg_of r) (freg_of a1) :: k | Ointoffloat, a1 :: nil => Pfcti (ireg_of r) (freg_of a1) :: k - | Ointuoffloat, a1 :: nil => - Pfctiu (ireg_of r) (freg_of a1) :: k - | Ofloatofint, a1 :: nil => - Pictf (freg_of r) (ireg_of a1) :: k - | Ofloatofintu, a1 :: nil => - Piuctf (freg_of r) (ireg_of a1) :: k + | Ofloatofwords, a1 :: a2 :: nil => + Pfmake (freg_of r) (ireg_of a1) (ireg_of a2) :: k | Ocmp cmp, _ => match classify_condition cmp args with | condition_ge0 _ a _ => @@ -377,43 +360,38 @@ Definition transl_op (** Common code to translate [Mload] and [Mstore] instructions. *) +Definition int_temp_for (r: mreg) := + if mreg_eq r IT2 then GPR11 else GPR12. + Definition transl_load_store (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - (addr: addressing) (args: list mreg) (k: code) := + (addr: addressing) (args: list mreg) + (temp: ireg) (k: code) := match addr, args with | Aindexed ofs, a1 :: nil => - if ireg_eq (ireg_of a1) GPR0 then - Pmr GPR12 (ireg_of a1) :: - Paddis GPR12 GPR12 (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) GPR12 :: k - else if Int.eq (high_s ofs) Int.zero then + if Int.eq (high_s ofs) Int.zero then mk1 (Cint ofs) (ireg_of a1) :: k else - Paddis GPR12 (ireg_of a1) (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) GPR12 :: k + Paddis temp (ireg_of a1) (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) temp :: k | Aindexed2, a1 :: a2 :: nil => mk2 (ireg_of a1) (ireg_of a2) :: k | Aglobal symb ofs, nil => if symbol_is_small_data symb ofs then mk1 (Csymbol_sda symb ofs) GPR0 :: k else - Paddis GPR12 GPR0 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) GPR12 :: k + Paddis temp GPR0 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) temp :: k | Abased symb ofs, a1 :: nil => - if ireg_eq (ireg_of a1) GPR0 then - Pmr GPR12 (ireg_of a1) :: - Paddis GPR12 GPR12 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) GPR12 :: k - else - Paddis GPR12 (ireg_of a1) (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) GPR12 :: k + Paddis temp (ireg_of a1) (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) temp :: k | Ainstack ofs, nil => if Int.eq (high_s ofs) Int.zero then mk1 (Cint ofs) GPR1 :: k else - Paddis GPR12 GPR1 (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) GPR12 :: k + Paddis temp GPR1 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) temp :: k | _, _ => (* should not happen *) k end. @@ -427,57 +405,58 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := | Msetstack src ofs ty => storeind src GPR1 ofs ty k | Mgetparam ofs ty dst => - Plwz GPR12 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR12 ofs ty dst k + Plwz GPR11 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR11 ofs ty dst k | Mop op args res => transl_op op args res k | Mload chunk addr args dst => match chunk with | Mint8signed => transl_load_store - (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args + (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args GPR12 (Pextsb (ireg_of dst) (ireg_of dst) :: k) | Mint8unsigned => transl_load_store - (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args k + (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args GPR12 k | Mint16signed => transl_load_store - (Plha (ireg_of dst)) (Plhax (ireg_of dst)) addr args k + (Plha (ireg_of dst)) (Plhax (ireg_of dst)) addr args GPR12 k | Mint16unsigned => transl_load_store - (Plhz (ireg_of dst)) (Plhzx (ireg_of dst)) addr args k + (Plhz (ireg_of dst)) (Plhzx (ireg_of dst)) addr args GPR12 k | Mint32 => transl_load_store - (Plwz (ireg_of dst)) (Plwzx (ireg_of dst)) addr args k + (Plwz (ireg_of dst)) (Plwzx (ireg_of dst)) addr args GPR12 k | Mfloat32 => transl_load_store - (Plfs (freg_of dst)) (Plfsx (freg_of dst)) addr args k + (Plfs (freg_of dst)) (Plfsx (freg_of dst)) addr args GPR12 k | Mfloat64 => transl_load_store - (Plfd (freg_of dst)) (Plfdx (freg_of dst)) addr args k + (Plfd (freg_of dst)) (Plfdx (freg_of dst)) addr args GPR12 k end | Mstore chunk addr args src => + let temp := int_temp_for src in match chunk with | Mint8signed => transl_load_store - (Pstb (ireg_of src)) (Pstbx (ireg_of src)) addr args k + (Pstb (ireg_of src)) (Pstbx (ireg_of src)) addr args temp k | Mint8unsigned => transl_load_store - (Pstb (ireg_of src)) (Pstbx (ireg_of src)) addr args k + (Pstb (ireg_of src)) (Pstbx (ireg_of src)) addr args temp k | Mint16signed => transl_load_store - (Psth (ireg_of src)) (Psthx (ireg_of src)) addr args k + (Psth (ireg_of src)) (Psthx (ireg_of src)) addr args temp k | Mint16unsigned => transl_load_store - (Psth (ireg_of src)) (Psthx (ireg_of src)) addr args k + (Psth (ireg_of src)) (Psthx (ireg_of src)) addr args temp k | Mint32 => transl_load_store - (Pstw (ireg_of src)) (Pstwx (ireg_of src)) addr args k + (Pstw (ireg_of src)) (Pstwx (ireg_of src)) addr args temp k | Mfloat32 => transl_load_store - (Pstfs (freg_of src)) (Pstfsx (freg_of src)) addr args k + (Pstfs (freg_of src)) (Pstfsx (freg_of src)) addr args temp k | Mfloat64 => transl_load_store - (Pstfd (freg_of src)) (Pstfdx (freg_of src)) addr args k + (Pstfd (freg_of src)) (Pstfdx (freg_of src)) addr args temp k end | Mcall sig (inl r) => Pmtctr (ireg_of r) :: Pbctrl :: k @@ -485,13 +464,13 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Pbl symb :: k | Mtailcall sig (inl r) => Pmtctr (ireg_of r) :: - Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR12 :: + Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR0 :: Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbctr :: k | Mtailcall sig (inr symb) => - Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR12 :: + Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR0 :: Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbs symb :: k | Mbuiltin ef args res => @@ -508,8 +487,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: Pbtbl GPR12 tbl :: k | Mreturn => - Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR12 :: + Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR0 :: Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pblr :: k end. @@ -524,8 +503,8 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) := Definition transl_function (f: Mach.function) := Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: - Pmflr GPR12 :: - Pstw GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmflr GPR0 :: + Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: transl_code f f.(fn_code). Open Local Scope string_scope. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index fc14830c..65c831e7 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -342,25 +342,12 @@ Proof. Qed. Hint Rewrite loadimm_label: labels. -Remark addimm_1_label: - forall r1 r2 n k, find_label lbl (addimm_1 r1 r2 n k) = find_label lbl k. -Proof. - intros; unfold addimm_1. - case (Int.eq (high_s n) Int.zero). reflexivity. - case (Int.eq (low_s n) Int.zero). reflexivity. reflexivity. -Qed. -Remark addimm_2_label: - forall r1 r2 n k, find_label lbl (addimm_2 r1 r2 n k) = find_label lbl k. -Proof. - intros; unfold addimm_2. autorewrite with labels. reflexivity. -Qed. Remark addimm_label: forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k. Proof. intros; unfold addimm. - case (ireg_eq r1 GPR0); intro. apply addimm_2_label. - case (ireg_eq r2 GPR0); intro. apply addimm_2_label. - apply addimm_1_label. + case (Int.eq (high_s n) Int.zero). reflexivity. + case (Int.eq (low_s n) Int.zero). reflexivity. reflexivity. Qed. Hint Rewrite addimm_label: labels. @@ -392,36 +379,22 @@ Proof. Qed. Hint Rewrite xorimm_label: labels. -Remark loadind_aux_label: - forall base ofs ty dst k, find_label lbl (loadind_aux base ofs ty dst :: k) = find_label lbl k. -Proof. - intros; unfold loadind_aux. - case ty; reflexivity. -Qed. Remark loadind_label: forall base ofs ty dst k, find_label lbl (loadind base ofs ty dst k) = find_label lbl k. Proof. intros; unfold loadind. - case (Int.eq (high_s ofs) Int.zero). apply loadind_aux_label. - transitivity (find_label lbl (loadind_aux GPR12 (low_s ofs) ty dst :: k)). - reflexivity. apply loadind_aux_label. + destruct (Int.eq (high_s ofs) Int.zero); destruct ty; autorewrite with labels; auto. Qed. Hint Rewrite loadind_label: labels. -Remark storeind_aux_label: - forall base ofs ty dst k, find_label lbl (storeind_aux base ofs ty dst :: k) = find_label lbl k. -Proof. - intros; unfold storeind_aux. - case dst; reflexivity. -Qed. + Remark storeind_label: forall base ofs ty src k, find_label lbl (storeind base src ofs ty k) = find_label lbl k. Proof. - intros; unfold storeind. - case (Int.eq (high_s ofs) Int.zero). apply storeind_aux_label. - transitivity (find_label lbl (storeind_aux base GPR12 (low_s ofs) ty :: k)). - reflexivity. apply storeind_aux_label. + intros; unfold storeind. + destruct (Int.eq (high_s ofs) Int.zero); destruct ty; autorewrite with labels; auto. Qed. Hint Rewrite storeind_label: labels. + Remark floatcomp_label: forall cmp r1 r2 k, find_label lbl (floatcomp cmp r1 r2 k) = find_label lbl k. Proof. @@ -481,22 +454,19 @@ Hint Rewrite transl_op_label: labels. Remark transl_load_store_label: forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - addr args k, + addr args temp k, (forall c r, is_label lbl (mk1 c r) = false) -> (forall r1 r2, is_label lbl (mk2 r1 r2) = false) -> - find_label lbl (transl_load_store mk1 mk2 addr args k) = find_label lbl k. + find_label lbl (transl_load_store mk1 mk2 addr args temp k) = find_label lbl k. Proof. intros; unfold transl_load_store. destruct addr; destruct args; try (destruct args); try (destruct args); try reflexivity. - case (ireg_eq (ireg_of m) GPR0); intro. - simpl. rewrite H. auto. - case (Int.eq (high_s i) Int.zero). simpl; rewrite H; auto. - simpl; rewrite H; auto. + destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto. simpl; rewrite H0; auto. destruct (symbol_is_small_data i i0); simpl; rewrite H; auto. - case (ireg_eq (ireg_of m) GPR0); intro; simpl; rewrite H; auto. - case (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto. + simpl; rewrite H; auto. + destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto. Qed. Hint Rewrite transl_load_store_label: labels. @@ -593,56 +563,102 @@ Inductive match_stack: list Machconcr.stackframe -> Prop := wt_function f -> incl c f.(fn_code) -> transl_code_at_pc ra fb f c -> + sp <> Vundef -> + ra <> Vundef -> match_stack s -> match_stack (Stackframe fb sp ra c :: s). Inductive match_states: Machconcr.state -> Asm.state -> Prop := | match_states_intro: - forall s fb sp c ms m rs f + forall s fb sp c ms m rs m' f (STACKS: match_stack s) (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) (WTF: wt_function f) (INCL: incl c f.(fn_code)) (AT: transl_code_at_pc (rs PC) fb f c) - (AG: agree ms sp rs), + (AG: agree ms sp rs) + (MEXT: Mem.extends m m'), match_states (Machconcr.State s fb sp c ms m) - (Asm.State rs m) + (Asm.State rs m') | match_states_call: - forall s fb ms m rs + forall s fb ms m rs m' (STACKS: match_stack s) (AG: agree ms (parent_sp s) rs) + (MEXT: Mem.extends m m') (ATPC: rs PC = Vptr fb Int.zero) (ATLR: rs LR = parent_ra s), match_states (Machconcr.Callstate s fb ms m) - (Asm.State rs m) + (Asm.State rs m') | match_states_return: - forall s ms m rs + forall s ms m rs m' (STACKS: match_stack s) (AG: agree ms (parent_sp s) rs) + (MEXT: Mem.extends m m') (ATPC: rs PC = parent_ra s), match_states (Machconcr.Returnstate s ms m) - (Asm.State rs m). + (Asm.State rs m'). Lemma exec_straight_steps: - forall s fb sp m1 f c1 rs1 c2 m2 ms2, + forall s fb sp m1' f c1 rs1 c2 m2 m2' ms2, match_stack s -> Genv.find_funct_ptr ge fb = Some (Internal f) -> wt_function f -> incl c2 f.(fn_code) -> transl_code_at_pc (rs1 PC) fb f c1 -> (exists rs2, - exec_straight tge (transl_function f) (transl_code f c1) rs1 m1 (transl_code f c2) rs2 m2 + exec_straight tge (transl_function f) (transl_code f c1) rs1 m1' (transl_code f c2) rs2 m2' /\ agree ms2 sp rs2) -> + Mem.extends m2 m2' -> exists st', - plus step tge (State rs1 m1) E0 st' /\ + plus step tge (State rs1 m1') E0 st' /\ match_states (Machconcr.State s fb sp c2 ms2 m2) st'. Proof. intros. destruct H4 as [rs2 [A B]]. - exists (State rs2 m2); split. + exists (State rs2 m2'); split. eapply exec_straight_exec; eauto. econstructor; eauto. eapply exec_straight_at; eauto. Qed. +Lemma exec_straight_steps_bis: + forall s fb sp m1' f c1 rs1 c2 m2 ms2, + match_stack s -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + wt_function f -> + incl c2 f.(fn_code) -> + transl_code_at_pc (rs1 PC) fb f c1 -> + (exists m2', + Mem.extends m2 m2' + /\ exists rs2, + exec_straight tge (transl_function f) (transl_code f c1) rs1 m1' (transl_code f c2) rs2 m2' + /\ agree ms2 sp rs2) -> + exists st', + plus step tge (State rs1 m1') E0 st' /\ + match_states (Machconcr.State s fb sp c2 ms2 m2) st'. +Proof. + intros. destruct H4 as [m2' [A B]]. + eapply exec_straight_steps; eauto. +Qed. + +Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. +Proof. induction 1; simpl. congruence. auto. Qed. + +Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. +Proof. induction 1; simpl. unfold Vzero. congruence. auto. Qed. + +Lemma lessdef_parent_sp: + forall s v, + match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s. +Proof. + intros. inv H0. auto. exploit parent_sp_def; eauto. tauto. +Qed. + +Lemma lessdef_parent_ra: + forall s v, + match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s. +Proof. + intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. +Qed. + (** We need to show that, in the simulation diagram, we cannot take infinitely many Mach transitions that correspond to zero transitions on the PPC side. Actually, all Mach transitions @@ -694,18 +710,18 @@ Proof. unfold load_stack in H. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inversion WTI. - rewrite (sp_val _ _ _ AG) in H. - assert (NOTE: GPR1 <> GPR0). congruence. - generalize (loadind_correct tge (transl_function f) GPR1 ofs ty - dst (transl_code f c) rs m v H H1 NOTE). + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ AG) in A. + exploit (loadind_correct tge (transl_function f) GPR1 ofs ty dst (transl_code f c) rs m' v'). + auto. auto. congruence. intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. simpl. exists rs2; split. auto. - apply agree_exten_2 with (rs#(preg_of dst) <- v). + apply agree_exten_2 with (rs#(preg_of dst) <- v'). auto with ppcgen. - intros. case (preg_eq r0 (preg_of dst)); intro. - subst r0. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso; auto. + intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of dst)). + subst r0. auto. + apply OTH; auto. Qed. Lemma exec_Msetstack_prop: @@ -719,12 +735,14 @@ Proof. intros; red; intros; inv MS. unfold store_stack in H. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - rewrite (sp_val _ _ _ AG) in H. - rewrite (preg_val ms sp rs) in H; auto. - assert (NOTE: GPR1 <> GPR0). congruence. - generalize (storeind_correct tge (transl_function f) GPR1 ofs ty - src (transl_code f c) rs m m' H H1 NOTE). + intro WTI. inv WTI. + generalize (preg_val ms sp rs src AG). intro. + exploit Mem.storev_extends; eauto. + intros [m2' [A B]]. + rewrite (sp_val _ _ _ AG) in A. + exploit (storeind_correct tge (transl_function f) GPR1 ofs (mreg_type src) + src (transl_code f c) rs). + eauto. auto. congruence. intros [rs2 [EX OTH]]. left; eapply exec_straight_steps; eauto with coqlib. exists rs2; split; auto. @@ -739,34 +757,35 @@ Lemma exec_Mgetparam_prop: load_stack m sp Tint f.(fn_link_ofs) = Some parent -> load_stack m parent ty ofs = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0 - (Machconcr.State s fb sp c (Regmap.set dst v ms) m). + (Machconcr.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. - set (rs2 := nextinstr (rs#GPR12 <- parent)). - assert (EX1: exec_straight tge (transl_function f) - (transl_code f (Mgetparam ofs ty dst :: c)) rs m - (loadind GPR12 ofs ty dst (transl_code f c)) rs2 m). - simpl. apply exec_straight_one. - simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto with ppcgen. - unfold const_low. rewrite <- (sp_val ms sp rs); auto. - unfold load_stack in H0. simpl chunk_of_type in H0. - rewrite H0. reflexivity. reflexivity. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - unfold load_stack in H1. change parent with rs2#GPR12 in H1. - assert (NOTE: GPR12 <> GPR0). congruence. - generalize (loadind_correct tge (transl_function f) GPR12 ofs ty - dst (transl_code f c) rs2 m v H1 H3 NOTE). - intros [rs3 [EX2 [RES OTH]]]. - left; eapply exec_straight_steps; eauto with coqlib. - exists rs3; split; simpl. - eapply exec_straight_trans; eauto. - apply agree_exten_2 with (rs2#(preg_of dst) <- v). - unfold rs2; auto with ppcgen. - intros. case (preg_eq r0 (preg_of dst)); intro. - subst r0. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso; auto. + intro WTI. inv WTI. + unfold load_stack in *. simpl in H0. + exploit Mem.loadv_extends. eauto. eexact H0. auto. + intros [parent' [A B]]. + exploit Mem.loadv_extends. eauto. eexact H1. + instantiate (1 := (Val.add parent' (Vint ofs))). + inv B. auto. simpl; auto. + intros [v' [C D]]. + left; eapply exec_straight_steps; eauto with coqlib. simpl. + set (rs1 := nextinstr (rs#GPR11 <- parent')). + exploit (loadind_correct tge (transl_function f) GPR11 ofs (mreg_type dst) dst (transl_code f c) rs1 m' v'). + unfold rs1. rewrite nextinstr_inv; auto with ppcgen. auto. congruence. + intros [rs2 [U [V W]]]. + exists rs2; split. + apply exec_straight_step with rs1 m'. + simpl. unfold load1. simpl. rewrite gpr_or_zero_not_zero. + rewrite <- (sp_val _ _ _ AG). rewrite A. auto. congruence. auto. + auto. + assert (agree (Regmap.set IT1 Vundef ms) sp rs1). + unfold rs1. eauto with ppcgen. + apply agree_exten_2 with (rs1#(preg_of dst) <- v'). + auto with ppcgen. + intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of dst)). + congruence. auto. Qed. Lemma exec_Mop_prop: @@ -775,7 +794,7 @@ Lemma exec_Mop_prop: (ms : mreg -> val) (m : mem) (v : val), eval_operation ge sp op ms ## args = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0 - (Machconcr.State s fb sp c (Regmap.set res v ms) m). + (Machconcr.State s fb sp c (Regmap.set res v (undef_op op ms)) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). @@ -805,7 +824,7 @@ Lemma exec_Mload_prop: eval_addressing ge sp addr ms ## args = Some a -> Mem.loadv chunk m a = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mload chunk addr args dst :: c) ms m) - E0 (Machconcr.State s fb sp c (Regmap.set dst v ms) m). + E0 (Machconcr.State s fb sp c (Regmap.set dst v (undef_temps ms)) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). @@ -820,26 +839,22 @@ Proof. (* Mint8signed *) exploit loadv_8_signed_unsigned; eauto. intros [v' [LOAD EQ]]. assert (X1: forall (cst : constant) (r1 : ireg) (rs1 : regset), - exec_instr tge (transl_function f) (Plbz (ireg_of dst) cst r1) rs1 m = - load1 tge Mint8unsigned (preg_of dst) cst r1 rs1 m). + exec_instr tge (transl_function f) (Plbz (ireg_of dst) cst r1) rs1 m' = + load1 tge Mint8unsigned (preg_of dst) cst r1 rs1 m'). intros. unfold preg_of; rewrite H6. reflexivity. assert (X2: forall (r1 r2 : ireg) (rs1 : regset), - exec_instr tge (transl_function f) (Plbzx (ireg_of dst) r1 r2) rs1 m = - load2 Mint8unsigned (preg_of dst) r1 r2 rs1 m). - intros. unfold preg_of; rewrite H6. reflexivity. - generalize (transl_load_correct tge (transl_function f) - (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) - Mint8unsigned addr args - (Pextsb (ireg_of dst) (ireg_of dst) :: transl_code f c) - ms sp rs m dst a v' - X1 X2 AG H3 H7 LOAD). + exec_instr tge (transl_function f) (Plbzx (ireg_of dst) r1 r2) rs1 m' = + load2 Mint8unsigned (preg_of dst) r1 r2 rs1 m'). + intros. unfold preg_of; rewrite H6. reflexivity. + exploit transl_load_correct; eauto. intros [rs2 [EX1 AG1]]. - exists (nextinstr (rs2#(ireg_of dst) <- v)). - split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. - rewrite <- (ireg_val _ _ _ dst AG1);auto. rewrite Regmap.gss. - rewrite EQ. reflexivity. reflexivity. - eauto with ppcgen. + econstructor; split. + eapply exec_straight_trans. eexact EX1. + apply exec_straight_one. simpl. eauto. auto. + apply agree_nextinstr. + eapply agree_set_twice_mireg; eauto. + rewrite EQ. apply Val.sign_ext_lessdef. + generalize (ireg_val _ _ _ dst AG1 H6). rewrite Regmap.gss. auto. Qed. Lemma storev_8_signed_unsigned: @@ -866,20 +881,20 @@ Lemma exec_Mstore_prop: eval_addressing ge sp addr ms ## args = Some a -> Mem.storev chunk m a (ms src) = Some m' -> exec_instr_prop (Machconcr.State s fb sp (Mstore chunk addr args src :: c) ms m) E0 - (Machconcr.State s fb sp c ms m'). + (Machconcr.State s fb sp c (undef_temps ms) m'). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI; inversion WTI. + intro WTI; inv WTI. rewrite <- (eval_addressing_preserved _ _ symbols_preserved) in H. - left; eapply exec_straight_steps; eauto with coqlib. + left; eapply exec_straight_steps_bis; eauto with coqlib. destruct chunk; simpl; simpl in H6; try (rewrite storev_8_signed_unsigned in H0); try (rewrite storev_16_signed_unsigned in H0); simpl; eapply transl_store_correct; eauto; - intros; (econstructor; split; [unfold preg_of; rewrite H6; reflexivity | auto]). - intros. apply Pregmap.gso; auto. - intros. apply Pregmap.gso; auto. + (unfold preg_of; rewrite H6; intros; econstructor; eauto). + split. simpl. rewrite H1. eauto. intros; apply Pregmap.gso; auto. + split. simpl. rewrite H1. eauto. intros; apply Pregmap.gso; auto. Qed. Lemma exec_Mcall_prop: @@ -904,12 +919,15 @@ Proof. (* Indirect call *) generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1. generalize (code_tail_next_int _ _ _ _ NOOV CT1). intro CT2. - set (rs2 := nextinstr (rs#CTR <- (ms m0))). - set (rs3 := rs2 #LR <- (Val.add rs2#PC Vone) #PC <- (ms m0)). - assert (ATPC: rs3 PC = Vptr f' Int.zero). - change (rs3 PC) with (ms m0). - destruct (ms m0); try discriminate. + assert (P1: ms m0 = Vptr f' Int.zero). + destruct (ms m0); try congruence. generalize H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. + assert (P2: rs (ireg_of m0) = Vptr f' Int.zero). + generalize (ireg_val _ _ _ m0 AG H3). + rewrite P1. intro. inv H2. auto. + set (rs2 := nextinstr (rs#CTR <- (Vptr f' Int.zero))). + set (rs3 := rs2 #LR <- (Val.add rs2#PC Vone) #PC <- (Vptr f' Int.zero)). + assert (ATPC: rs3 PC = Vptr f' Int.zero). reflexivity. exploit return_address_offset_correct; eauto. constructor; eauto. intro RA_EQ. assert (ATLR: rs3 LR = Vptr fb ra). @@ -918,11 +936,11 @@ Proof. rewrite <- H5. reflexivity. assert (AG3: agree ms sp rs3). unfold rs3, rs2; auto 8 with ppcgen. - left; exists (State rs3 m); split. - apply plus_left with E0 (State rs2 m) E0. + left; exists (State rs3 m'); split. + apply plus_left with E0 (State rs2 m') E0. econstructor. eauto. apply functions_transl. eexact H0. eapply find_instr_tail. eauto. - simpl. rewrite <- (ireg_val ms sp rs); auto. + simpl. rewrite P2. auto. apply star_one. econstructor. change (rs2 PC) with (Val.add (rs PC) Vone). rewrite <- H5. simpl. auto. @@ -933,6 +951,8 @@ Proof. econstructor; eauto. econstructor; eauto with coqlib. rewrite RA_EQ. econstructor; eauto. + eapply agree_sp_def; eauto. congruence. + (* Direct call *) generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1. set (rs2 := rs #LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset tge i Int.zero)). @@ -947,7 +967,7 @@ Proof. rewrite <- H5. reflexivity. assert (AG2: agree ms sp rs2). unfold rs2; auto 8 with ppcgen. - left; exists (State rs2 m); split. + left; exists (State rs2 m'); split. apply plus_one. econstructor. eauto. apply functions_transl. eexact H0. @@ -956,6 +976,7 @@ Proof. econstructor; eauto with coqlib. econstructor; eauto with coqlib. rewrite RA_EQ. econstructor; eauto. + eapply agree_sp_def; eauto. congruence. Qed. Lemma exec_Mtailcall_prop: @@ -978,30 +999,43 @@ Proof. inversion AT. subst b f0 c0. assert (NOOV: list_length_z (transl_function f) <= Int.max_unsigned). eapply functions_transl_no_overflow; eauto. + exploit Mem.free_parallel_extends; eauto. + intros [m2' [FREE' EXT']]. + unfold load_stack in *. simpl in H1; simpl in H2. + exploit Mem.load_extends. eexact MEXT. eexact H1. + intros [parent' [LOAD1 LD1]]. + rewrite (lessdef_parent_sp s parent' STACKS LD1) in LOAD1. + exploit Mem.load_extends. eexact MEXT. eexact H2. + intros [ra' [LOAD2 LD2]]. + rewrite (lessdef_parent_ra s ra' STACKS LD2) in LOAD2. destruct ros; simpl in H; simpl in H9. (* Indirect call *) - set (rs2 := nextinstr (rs#CTR <- (ms m0))). - set (rs3 := nextinstr (rs2#GPR12 <- (parent_ra s))). + assert (P1: ms m0 = Vptr f' Int.zero). + destruct (ms m0); try congruence. + generalize H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. + assert (P2: rs (ireg_of m0) = Vptr f' Int.zero). + generalize (ireg_val _ _ _ m0 AG H7). + rewrite P1. intro. inv H11. auto. + set (rs2 := nextinstr (rs#CTR <- (Vptr f' Int.zero))). + set (rs3 := nextinstr (rs2#GPR0 <- (parent_ra s))). set (rs4 := nextinstr (rs3#LR <- (parent_ra s))). set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))). set (rs6 := rs5#PC <- (rs5 CTR)). assert (exec_straight tge (transl_function f) - (transl_code f (Mtailcall sig (inl ident m0) :: c)) rs m - (Pbctr :: transl_code f c) rs5 m'). - simpl. apply exec_straight_step with rs2 m. - simpl. rewrite <- (ireg_val _ _ _ _ AG H7). reflexivity. reflexivity. - apply exec_straight_step with rs3 m. + (transl_code f (Mtailcall sig (inl ident m0) :: c)) rs m'0 + (Pbctr :: transl_code f c) rs5 m2'). + simpl. apply exec_straight_step with rs2 m'0. + simpl. rewrite P2. auto. auto. + apply exec_straight_step with rs3 m'0. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. change (rs2 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. unfold load_stack in H2. simpl in H2. rewrite H2. - reflexivity. discriminate. reflexivity. - apply exec_straight_step with rs4 m. + simpl. rewrite LOAD2. auto. congruence. auto. + apply exec_straight_step with rs4 m'0. simpl. reflexivity. reflexivity. apply exec_straight_one. simpl. change (rs4 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - unfold load_stack in H1; simpl in H1. - simpl. rewrite H1. rewrite H3. reflexivity. reflexivity. - left; exists (State rs6 m'); split. + simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity. + left; exists (State rs6 m2'); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. @@ -1017,32 +1051,27 @@ Proof. unfold rs4, rs3, rs2; auto 10 with ppcgen. assert (AG5: agree ms (parent_sp s) rs5). unfold rs5. apply agree_nextinstr. - split. reflexivity. intros. inv AG4. rewrite H13. - rewrite Pregmap.gso; auto with ppcgen. + split. reflexivity. apply parent_sp_def; auto. + intros. inv AG4. rewrite Pregmap.gso; auto with ppcgen. unfold rs6; auto with ppcgen. - change (rs6 PC) with (ms m0). - generalize H. destruct (ms m0); try congruence. - predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. (* direct call *) - set (rs2 := nextinstr (rs#GPR12 <- (parent_ra s))). + set (rs2 := nextinstr (rs#GPR0 <- (parent_ra s))). set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). set (rs5 := rs4#PC <- (Vptr f' Int.zero)). assert (exec_straight tge (transl_function f) - (transl_code f (Mtailcall sig (inr mreg i) :: c)) rs m - (Pbs i :: transl_code f c) rs4 m'). - simpl. apply exec_straight_step with rs2 m. + (transl_code f (Mtailcall sig (inr mreg i) :: c)) rs m'0 + (Pbs i :: transl_code f c) rs4 m2'). + simpl. apply exec_straight_step with rs2 m'0. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. rewrite <- (sp_val _ _ _ AG). - simpl. unfold load_stack in H2. simpl in H2. rewrite H2. - reflexivity. discriminate. reflexivity. - apply exec_straight_step with rs3 m. + simpl. rewrite LOAD2. auto. discriminate. auto. + apply exec_straight_step with rs3 m'0. simpl. reflexivity. reflexivity. apply exec_straight_one. simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - unfold load_stack in H1; simpl in H1. - simpl. rewrite H1. rewrite H3. reflexivity. reflexivity. - left; exists (State rs5 m'); split. + simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity. + left; exists (State rs5 m2'); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. @@ -1059,8 +1088,9 @@ Proof. unfold rs3, rs2; auto 10 with ppcgen. assert (AG4: agree ms (parent_sp s) rs4). unfold rs4. apply agree_nextinstr. - split. reflexivity. intros. inv AG3. rewrite H13. - rewrite Pregmap.gso; auto with ppcgen. + split. reflexivity. + apply parent_sp_def; auto. + intros. inv AG3. rewrite Pregmap.gso; auto with ppcgen. unfold rs5; auto with ppcgen. Qed. @@ -1071,7 +1101,7 @@ Lemma exec_Mbuiltin_prop: (t : trace) (v : val) (m' : mem), external_call ef ge ms ## args m t v m' -> exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t - (Machconcr.State s f sp b (Regmap.set res v ms) m'). + (Machconcr.State s f sp b (Regmap.set res v (undef_temps ms)) m'). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). @@ -1079,20 +1109,21 @@ Proof. inv AT. simpl in H3. generalize (functions_transl _ _ FIND); intro FN. generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. + exploit external_call_mem_extends; eauto. eapply preg_vals; eauto. + intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_builtin. eauto. eauto. - eapply find_instr_tail; eauto. - replace (rs##(preg_of##args)) with (ms##args). + eapply find_instr_tail; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. - rewrite list_map_compose. apply list_map_exten. intros. - symmetry. eapply preg_val; eauto. econstructor; eauto with coqlib. - unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. + unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with ppcgen. rewrite <- H0. simpl. constructor; auto. eapply code_tail_next_int; eauto. - apply sym_not_equal. auto with ppcgen. - auto with ppcgen. + apply sym_not_equal. auto with ppcgen. + apply agree_nextinstr. apply agree_set_mreg; auto. + eapply agree_undef_temps; eauto. + intros. repeat rewrite Pregmap.gso; auto. Qed. Lemma exec_Mgoto_prop: @@ -1107,9 +1138,9 @@ Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. inv AT. simpl in H3. - generalize (find_label_goto_label f lbl rs m _ _ _ FIND (sym_equal H1) H0). + generalize (find_label_goto_label f lbl rs m' _ _ _ FIND (sym_equal H1) H0). intros [rs2 [GOTO [AT2 INV]]]. - left; exists (State rs2 m); split. + left; exists (State rs2 m'); split. apply plus_one. econstructor; eauto. apply functions_transl; eauto. eapply find_instr_tail; eauto. @@ -1128,7 +1159,7 @@ Lemma exec_Mcond_true_prop: Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machconcr.State s fb sp c' ms m). + (Machconcr.State s fb sp c' (undef_temps ms) m). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). @@ -1138,16 +1169,16 @@ Proof. then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c). generalize (transl_cond_correct tge (transl_function f) - cond args k1 ms sp rs m true H3 AG H). + cond args k1 ms sp rs m' true H3 AG H). simpl. intros [rs2 [EX [RES AG2]]]. inv AT. simpl in H5. generalize (functions_transl _ _ H4); intro FN. generalize (functions_transl_no_overflow _ _ H4); intro NOOV. exploit exec_straight_steps_2; eauto. intros [ofs' [PC2 CT2]]. - generalize (find_label_goto_label f lbl rs2 m _ _ _ FIND PC2 H1). + generalize (find_label_goto_label f lbl rs2 m' _ _ _ FIND PC2 H1). intros [rs3 [GOTO [AT3 INV3]]]. - left; exists (State rs3 m); split. + left; exists (State rs3 m'); split. eapply plus_right'. eapply exec_straight_steps_1; eauto. caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES. @@ -1160,7 +1191,7 @@ Proof. traceEq. econstructor; eauto. eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs2; auto. + apply agree_exten_2 with rs2; auto with ppcgen. Qed. Lemma exec_Mcond_false_prop: @@ -1169,7 +1200,7 @@ Lemma exec_Mcond_false_prop: (c : list Mach.instruction) (ms : mreg -> val) (m : mem), eval_condition cond ms ## args = Some false -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machconcr.State s fb sp c ms m). + (Machconcr.State s fb sp c (undef_temps ms) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). @@ -1179,7 +1210,7 @@ Proof. then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c). generalize (transl_cond_correct tge (transl_function f) - cond args k1 ms sp rs m false H1 AG H). + cond args k1 ms sp rs m' false H1 AG H). simpl. intros [rs2 [EX [RES AG2]]]. left; eapply exec_straight_steps; eauto with coqlib. exists (nextinstr rs2); split. @@ -1205,7 +1236,7 @@ Lemma exec_Mjumptable_prop: Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop (Machconcr.State s fb sp (Mjumptable arg tbl :: c) rs m) E0 - (Machconcr.State s fb sp c' rs m). + (Machconcr.State s fb sp c' (undef_temps rs) m). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. @@ -1227,17 +1258,18 @@ Proof. generalize (functions_transl _ _ H4); intro FN. generalize (functions_transl_no_overflow _ _ H4); intro NOOV. assert (exec_straight tge (transl_function f) - (Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: k1) rs0 m - k1 rs1 m). + (Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: k1) rs0 m' + k1 rs1 m'). apply exec_straight_one. - simpl. rewrite <- (ireg_val _ _ _ _ AG H5). rewrite H. reflexivity. reflexivity. + simpl. generalize (ireg_val _ _ _ arg AG H5). rewrite H. intro. inv H8. + reflexivity. reflexivity. exploit exec_straight_steps_2; eauto. intros [ofs' [PC1 CT1]]. set (rs2 := rs1 # GPR12 <- Vundef # CTR <- Vundef). assert (PC2: rs2 PC = Vptr fb ofs'). rewrite <- PC1. reflexivity. - generalize (find_label_goto_label f lbl rs2 m _ _ _ FIND PC2 H2). + generalize (find_label_goto_label f lbl rs2 m' _ _ _ FIND PC2 H2). intros [rs3 [GOTO [AT3 INV3]]]. - left; exists (State rs3 m); split. + left; exists (State rs3 m'); split. eapply plus_right'. eapply exec_straight_steps_1; eauto. econstructor; eauto. @@ -1251,7 +1283,10 @@ Opaque Zmod. Opaque Zdiv. econstructor; eauto. eapply Mach.find_label_incl; eauto. apply agree_exten_2 with rs2; auto. - unfold rs2, rs1. repeat apply agree_set_other; auto with ppcgen. + unfold rs2, rs1. apply agree_set_other; auto with ppcgen. + apply agree_undef_temps with rs0; auto. + intros. rewrite Pregmap.gso; auto. rewrite nextinstr_inv; auto. + rewrite Pregmap.gso; auto. Qed. Lemma exec_Mreturn_prop: @@ -1266,27 +1301,33 @@ Lemma exec_Mreturn_prop: Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. - set (rs2 := nextinstr (rs#GPR12 <- (parent_ra s))). + exploit Mem.free_parallel_extends; eauto. + intros [m2' [FREE' EXT']]. + unfold load_stack in *. simpl in H0; simpl in H1. + exploit Mem.load_extends. eexact MEXT. eexact H0. + intros [parent' [LOAD1 LD1]]. + rewrite (lessdef_parent_sp s parent' STACKS LD1) in LOAD1. + exploit Mem.load_extends. eexact MEXT. eexact H1. + intros [ra' [LOAD2 LD2]]. + rewrite (lessdef_parent_ra s ra' STACKS LD2) in LOAD2. + set (rs2 := nextinstr (rs#GPR0 <- (parent_ra s))). set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). set (rs5 := rs4#PC <- (parent_ra s)). assert (exec_straight tge (transl_function f) - (transl_code f (Mreturn :: c)) rs m - (Pblr :: transl_code f c) rs4 m'). - simpl. apply exec_straight_three with rs2 m rs3 m. + (transl_code f (Mreturn :: c)) rs m'0 + (Pblr :: transl_code f c) rs4 m2'). + simpl. apply exec_straight_three with rs2 m'0 rs3 m'0. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - unfold load_stack in H1. simpl in H1. - rewrite <- (sp_val _ _ _ AG). simpl. rewrite H1. + rewrite <- (sp_val _ _ _ AG). simpl. rewrite LOAD2. reflexivity. discriminate. - unfold rs3. change (parent_ra s) with rs2#GPR12. reflexivity. + unfold rs3. reflexivity. simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. - unfold load_stack in H0. simpl in H0. - rewrite H0. rewrite H2. reflexivity. + simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity. reflexivity. reflexivity. - left; exists (State rs5 m'); split. + left; exists (State rs5 m2'); split. (* execution *) - apply plus_right' with E0 (State rs4 m') E0. + apply plus_right' with E0 (State rs4 m2') E0. eapply exec_straight_exec; eauto. inv AT. econstructor. change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). @@ -1303,7 +1344,7 @@ Proof. assert (AG3: agree ms (Vptr stk soff) rs3). unfold rs3, rs2; auto 10 with ppcgen. assert (AG4: agree ms (parent_sp s) rs4). - split. reflexivity. intros. unfold rs4. + split. reflexivity. apply parent_sp_def; auto. intros. unfold rs4. rewrite nextinstr_inv. rewrite Pregmap.gso. elim AG3; auto. auto with ppcgen. auto with ppcgen. unfold rs5; auto with ppcgen. @@ -1328,23 +1369,29 @@ Proof. inversion TY; auto. exploit functions_transl; eauto. intro TFIND. generalize (functions_transl_no_overflow _ _ H); intro NOOV. - set (rs2 := nextinstr (rs#GPR1 <- sp #GPR12 <- Vundef)). - set (rs3 := nextinstr (rs2#GPR12 <- (parent_ra s))). + unfold store_stack in *; simpl in *. + exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + intros [m1' [ALLOC' MEXT1]]. + exploit Mem.store_within_extends. eexact MEXT1. eexact H1. auto. + intros [m2' [STORE2 MEXT2]]. + exploit Mem.store_within_extends. eexact MEXT2. eexact H2. auto. + intros [m3' [STORE3 MEXT3]]. + set (rs2 := nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)). + set (rs3 := nextinstr (rs2#GPR0 <- (parent_ra s))). set (rs4 := nextinstr rs3). (* Execution of function prologue *) assert (EXEC_PROLOGUE: exec_straight tge (transl_function f) - (transl_function f) rs m - (transl_code f (fn_code f)) rs4 m3). + (transl_function f) rs m' + (transl_code f (fn_code f)) rs4 m3'). unfold transl_function at 2. - apply exec_straight_three with rs2 m2 rs3 m2. - unfold exec_instr. rewrite H0. fold sp. - unfold store_stack in H1. simpl chunk_of_type in H1. - rewrite <- (sp_val _ _ _ AG). rewrite H1. reflexivity. + apply exec_straight_three with rs2 m2' rs3 m2'. + unfold exec_instr. rewrite ALLOC'. fold sp. + rewrite <- (sp_val _ _ _ AG). unfold sp; simpl; rewrite STORE2. reflexivity. simpl. change (rs2 LR) with (rs LR). rewrite ATLR. reflexivity. simpl. unfold store1. rewrite gpr_or_zero_not_zero. - unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR12) with (parent_ra s). - unfold store_stack in H2. simpl chunk_of_type in H2. rewrite H2. reflexivity. + unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR0) with (parent_ra s). + simpl. rewrite STORE3. reflexivity. discriminate. reflexivity. reflexivity. reflexivity. (* Agreement at end of prologue *) assert (AT4: transl_code_at_pc rs4#PC fb f f.(fn_code)). @@ -1356,13 +1403,13 @@ Proof. change (Int.unsigned Int.zero) with 0. unfold transl_function. constructor. assert (AG2: agree ms sp rs2). - split. reflexivity. + split. reflexivity. unfold sp. congruence. intros. unfold rs2. rewrite nextinstr_inv. repeat (rewrite Pregmap.gso). elim AG; auto. auto with ppcgen. auto with ppcgen. auto with ppcgen. assert (AG4: agree ms sp rs4). unfold rs4, rs3; auto with ppcgen. - left; exists (State rs4 m3); split. + left; exists (State rs4 m3'); split. (* execution *) eapply exec_straight_steps_1; eauto. change (Int.unsigned Int.zero) with 0. constructor. @@ -1384,12 +1431,15 @@ Proof. intros; red; intros; inv MS. exploit functions_translated; eauto. intros [tf [A B]]. simpl in B. inv B. - left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs LR)) - m'); split. + exploit extcall_arguments_match; eauto. + intros [args' [C D]]. + exploit external_call_mem_extends; eauto. + intros [res' [m2' [P [Q [R S]]]]]. + left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res' #PC <- (rs LR)) + m2'); split. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. - eapply extcall_arguments_match; eauto. econstructor; eauto. unfold loc_external_result. auto with ppcgen. Qed. @@ -1440,7 +1490,9 @@ Proof. replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero) with (Vptr fb Int.zero). econstructor; eauto. constructor. - split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen. + split. auto. simpl. congruence. + intros. repeat rewrite Pregmap.gso; auto with ppcgen. + apply Mem.extends_refl. unfold symbol_offset. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. unfold ge; rewrite H1. auto. @@ -1451,8 +1503,8 @@ Lemma transf_final_states: match_states st1 st2 -> Machconcr.final_state st1 r -> Asm.final_state st2 r. Proof. intros. inv H0. inv H. constructor. auto. - compute in H1. - rewrite (ireg_val _ _ _ R3 AG) in H1. auto. auto. + compute in H1. + exploit (ireg_val _ _ _ R3 AG). auto. rewrite H1; intro. inv H. auto. Qed. Theorem transf_program_correct: diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 0b146daa..d428543c 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -117,8 +117,7 @@ Qed. Definition is_data_reg (r: preg) : Prop := match r with - | IR GPR12 => False - | FR FPR13 => False + | IR GPR0 => False | PC => False | LR => False | CTR => False | CR0_0 => False | CR0_1 => False | CR0_2 => False | CR0_3 => False | CARRY => False @@ -148,17 +147,12 @@ Lemma ireg_of_not_GPR1: Proof. intro. case r; discriminate. Qed. -Lemma ireg_of_not_GPR12: - forall r, ireg_of r <> GPR12. +Lemma ireg_of_not_GPR0: + forall r, ireg_of r <> GPR0. Proof. intro. case r; discriminate. Qed. -Lemma freg_of_not_FPR13: - forall r, freg_of r <> FPR13. -Proof. - intro. case r; discriminate. -Qed. -Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR12 freg_of_not_FPR13: ppcgen. +Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR0: ppcgen. Lemma preg_of_not: forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2. @@ -174,36 +168,57 @@ Proof. Qed. Hint Resolve preg_of_not_GPR1: ppcgen. +Lemma int_temp_for_diff: + forall r, IR(int_temp_for r) <> preg_of r. +Proof. + intros. unfold int_temp_for. destruct (mreg_eq r IT2). + subst r. compute. congruence. + change (IR GPR12) with (preg_of IT2). red; intros; elim n. + apply preg_of_injective; auto. +Qed. + (** Agreement between Mach register sets and PPC register sets. *) -Definition agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) := - rs#GPR1 = sp /\ forall r: mreg, ms r = rs#(preg_of r). +Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree { + agree_sp: rs#GPR1 = sp; + agree_sp_def: sp <> Vundef; + agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r)) +}. Lemma preg_val: forall ms sp rs r, - agree ms sp rs -> ms r = rs#(preg_of r). + agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r). Proof. - intros. elim H. auto. + intros. eapply agree_mregs; eauto. Qed. - + +Lemma preg_vals: + forall ms sp rs rl, + agree ms sp rs -> Val.lessdef_list (List.map ms rl) (List.map rs (List.map preg_of rl)). +Proof. + induction rl; intros; simpl. + constructor. + constructor. eapply preg_val; eauto. eauto. +Qed. + Lemma ireg_val: forall ms sp rs r, agree ms sp rs -> mreg_type r = Tint -> - ms r = rs#(ireg_of r). + Val.lessdef (ms r) rs#(ireg_of r). Proof. - intros. elim H; intros. - generalize (H2 r). unfold preg_of. rewrite H0. auto. + intros. replace (IR (ireg_of r)) with (preg_of r). eapply preg_val; eauto. + unfold preg_of. rewrite H0. auto. Qed. Lemma freg_val: forall ms sp rs r, agree ms sp rs -> mreg_type r = Tfloat -> - ms r = rs#(freg_of r). + Val.lessdef (ms r) rs#(freg_of r). Proof. - intros. elim H; intros. - generalize (H2 r). unfold preg_of. rewrite H0. auto. + intros. replace (FR (freg_of r)) with (preg_of r). eapply preg_val; eauto. + unfold preg_of. rewrite H0. auto. Qed. Lemma sp_val: @@ -220,8 +235,9 @@ Lemma agree_exten_1: (forall r, is_data_reg r -> rs'#r = rs#r) -> agree ms sp rs'. Proof. - unfold agree; intros. elim H; intros. - split. rewrite H0. auto. exact I. + intros. inv H. constructor. + apply H0. exact I. + auto. intros. rewrite H0. auto. apply preg_of_is_data_reg. Qed. @@ -229,7 +245,7 @@ Lemma agree_exten_2: forall ms sp rs rs', agree ms sp rs -> (forall r, - r <> IR GPR12 -> r <> FR FPR13 -> + r <> IR GPR0 -> r <> PC -> r <> LR -> r <> CTR -> r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 -> r <> CARRY -> @@ -243,12 +259,14 @@ Qed. (** Preservation of register agreement under various assignments. *) Lemma agree_set_mreg: - forall ms sp rs r v, + forall ms sp rs r v v', agree ms sp rs -> - agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v). + Val.lessdef v v' -> + agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v'). Proof. - unfold agree; intros. elim H; intros; clear H. - split. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR1. + intros. inv H. constructor. + rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR1. + auto. intros. unfold Regmap.set. case (RegEq.eq r0 r); intro. subst r0. rewrite Pregmap.gss. auto. rewrite Pregmap.gso. auto. red; intro. @@ -296,13 +314,14 @@ Qed. Hint Resolve agree_nextinstr: ppcgen. Lemma agree_set_mireg_twice: - forall ms sp rs r v v', + forall ms sp rs r v v' v1, agree ms sp rs -> mreg_type r = Tint -> - agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v' #(ireg_of r) <- v). + Val.lessdef v v' -> + agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v1 #(ireg_of r) <- v'). Proof. - intros. replace (IR (ireg_of r)) with (preg_of r). elim H; intros. - split. repeat (rewrite Pregmap.gso; auto with ppcgen). + intros. replace (IR (ireg_of r)) with (preg_of r). inv H. + split. repeat (rewrite Pregmap.gso; auto with ppcgen). auto. intros. case (mreg_eq r r0); intro. subst r0. rewrite Regmap.gss. rewrite Pregmap.gss. auto. assert (preg_of r <> preg_of r0). @@ -314,15 +333,17 @@ Qed. Hint Resolve agree_set_mireg_twice: ppcgen. Lemma agree_set_twice_mireg: - forall ms sp rs r v v', - agree (Regmap.set r v' ms) sp rs -> + forall ms sp rs r v v1 v', + agree (Regmap.set r v1 ms) sp rs -> mreg_type r = Tint -> - agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v). + Val.lessdef v v' -> + agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v'). Proof. - intros. elim H; intros. + intros. inv H. split. rewrite Pregmap.gso. auto. generalize (ireg_of_not_GPR1 r); congruence. - intros. generalize (H2 r0). + auto. + intros. generalize (agree_mregs0 r0). case (mreg_eq r0 r); intro. subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0. rewrite Pregmap.gss. auto. @@ -367,20 +388,66 @@ Lemma agree_set_mireg_exten: forall ms sp rs r v (rs': regset), agree ms sp rs -> mreg_type r = Tint -> - rs'#(ireg_of r) = v -> + Val.lessdef v rs'#(ireg_of r) -> (forall r', - r' <> IR GPR12 -> r' <> FR FPR13 -> + r' <> IR GPR0 -> r' <> PC -> r' <> LR -> r' <> CTR -> r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> CARRY -> r' <> IR (ireg_of r) -> rs'#r' = rs#r') -> agree (Regmap.set r v ms) sp rs'. Proof. - intros. apply agree_exten_2 with (rs#(ireg_of r) <- v). + intros. set (v' := rs'#(ireg_of r)). + apply agree_exten_2 with (rs#(ireg_of r) <- v'). auto with ppcgen. intros. unfold Pregmap.set. case (PregEq.eq r0 (ireg_of r)); intro. subst r0. auto. apply H2; auto. Qed. +Hint Resolve agree_set_mireg_exten: ppcgen. + +Lemma agree_undef_regs: + forall rl ms sp rs rs', + agree ms sp rs -> + (forall r, is_data_reg r -> ~In r (List.map preg_of rl) -> rs'#r = rs#r) -> + agree (undef_regs rl ms) sp rs'. +Proof. + induction rl; simpl; intros. + apply agree_exten_1 with rs; auto. + apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))). + apply agree_set_mreg; auto. + intros. unfold Pregmap.set. + destruct (PregEq.eq r (preg_of a)). + congruence. + apply H0. auto. intuition congruence. +Qed. + +Lemma agree_undef_temps: + forall ms sp rs rs', + agree ms sp rs -> + (forall r, + r <> IR GPR0 -> + r <> PC -> r <> LR -> r <> CTR -> + r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 -> + r <> CARRY -> + r <> IR GPR11 -> r <> IR GPR12 -> + r <> FR FPR0 -> r <> FR FPR12 -> r <> FR FPR13 -> + rs'#r = rs#r) -> + agree (undef_temps ms) sp rs'. +Proof. + unfold undef_temps. intros. apply agree_undef_regs with rs; auto. + simpl. unfold preg_of; simpl. intros. + apply H0; (red; intro; subst; simpl in H1; intuition congruence). +Qed. +Hint Resolve agree_undef_temps: ppcgen. + +Lemma agree_undef_temps_2: + forall ms sp rs, + agree ms sp rs -> + agree (undef_temps ms) sp rs. +Proof. + intros. apply agree_undef_temps with rs; auto. +Qed. +Hint Resolve agree_undef_temps_2: ppcgen. (** Useful properties of the PC and GPR0 registers. *) @@ -416,33 +483,41 @@ Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: ppcgen. functions. *) Lemma extcall_arg_match: - forall ms sp rs m l v, + forall ms sp rs m m' l v, agree ms sp rs -> + Mem.extends m m' -> Machconcr.extcall_arg ms m sp l v -> - Asm.extcall_arg rs m l v. + exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'. Proof. - intros. inv H0. - rewrite (preg_val _ _ _ r H). constructor. - rewrite (sp_val _ _ _ H) in H1. - destruct ty; unfold load_stack in H1. - econstructor. reflexivity. assumption. - econstructor. reflexivity. assumption. + intros. inv H1. + exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto. + unfold load_stack in H2. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ H) in A. + exists v'; split; auto. + destruct ty; econstructor. + reflexivity. assumption. + reflexivity. assumption. Qed. Lemma extcall_args_match: - forall ms sp rs m, agree ms sp rs -> + forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> forall ll vl, Machconcr.extcall_args ms m sp ll vl -> - Asm.extcall_args rs m ll vl. + exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'. Proof. - induction 2; constructor; auto. eapply extcall_arg_match; eauto. + induction 3; intros. + exists (@nil val); split. constructor. constructor. + exploit extcall_arg_match; eauto. intros [v1' [A B]]. + exploit IHextcall_args; eauto. intros [vl' [C D]]. + exists (v1' :: vl'); split; constructor; auto. Qed. Lemma extcall_arguments_match: - forall ms m sp rs sg args, - agree ms sp rs -> + forall ms m m' sp rs sg args, + agree ms sp rs -> Mem.extends m m' -> Machconcr.extcall_arguments ms m sp sg args -> - Asm.extcall_arguments rs m sg args. + exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'. Proof. unfold Machconcr.extcall_arguments, Asm.extcall_arguments; intros. eapply extcall_args_match; eauto. @@ -611,16 +686,16 @@ Qed. (** Add integer immediate. *) -Lemma addimm_1_correct: +Lemma addimm_correct: forall r1 r2 n k rs m, r1 <> GPR0 -> r2 <> GPR0 -> exists rs', - exec_straight (addimm_1 r1 r2 n k) rs m k rs' m + exec_straight (addimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = Val.add rs#r2 (Vint n) /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. - intros. unfold addimm_1. + intros. unfold addimm. (* addi *) case (Int.eq (high_s n) Int.zero). exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))). @@ -653,55 +728,18 @@ Proof. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. Qed. -Lemma addimm_2_correct: - forall r1 r2 n k rs m, - r2 <> GPR12 -> - exists rs', - exec_straight (addimm_2 r1 r2 n k) rs m k rs' m - /\ rs'#r1 = Val.add rs#r2 (Vint n) - /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'. -Proof. - intros. unfold addimm_2. - generalize (loadimm_correct GPR12 n (Padd r1 r2 GPR12 :: k) rs m). - intros [rs1 [EX [RES OTHER]]]. - exists (nextinstr (rs1#r1 <- (Val.add rs#r2 (Vint n)))). - split. eapply exec_straight_trans. eexact EX. - apply exec_straight_one. simpl. rewrite RES. rewrite OTHER. - auto. congruence. discriminate. - reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. -Qed. - -Lemma addimm_correct: - forall r1 r2 n k rs m, - r2 <> GPR12 -> - exists rs', - exec_straight (addimm r1 r2 n k) rs m k rs' m - /\ rs'#r1 = Val.add rs#r2 (Vint n) - /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'. -Proof. - intros. unfold addimm. - case (ireg_eq r1 GPR0); intro. - apply addimm_2_correct; auto. - case (ireg_eq r2 GPR0); intro. - apply addimm_2_correct; auto. - generalize (addimm_1_correct r1 r2 n k rs m n0 n1). - intros [rs' [EX [RES OTH]]]. exists rs'. intuition. -Qed. - (** And integer immediate. *) Lemma andimm_correct: forall r1 r2 n k (rs : regset) m, - r2 <> GPR12 -> + r2 <> GPR0 -> let v := Val.and rs#r2 (Vint n) in exists rs', exec_straight (andimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = v /\ rs'#CR0_2 = Val.cmp Ceq v Vzero /\ forall r': preg, - r' <> r1 -> r' <> GPR12 -> r' <> PC -> + r' <> r1 -> r' <> GPR0 -> r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> rs'#r' = rs#r'. Proof. @@ -728,7 +766,7 @@ Proof. split. auto. intros. rewrite D; auto. apply Pregmap.gso; auto. (* loadimm + and *) - generalize (loadimm_correct GPR12 n (Pand_ r1 r2 GPR12 :: k) rs m). + generalize (loadimm_correct GPR0 n (Pand_ r1 r2 GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTHER1]]]. exists (nextinstr (compare_sint (rs1#r1 <- v) v Vzero)). generalize (compare_sint_spec (rs1#r1 <- v) v Vzero). @@ -823,21 +861,6 @@ Qed. (** Indexed memory loads. *) -Lemma loadind_aux_correct: - forall (base: ireg) ofs ty dst (rs: regset) m v, - Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v -> - mreg_type dst = ty -> - base <> GPR0 -> - exec_instr ge fn (loadind_aux base ofs ty dst) rs m = - OK (nextinstr (rs#(preg_of dst) <- v)) m. -Proof. - intros. unfold loadind_aux. unfold preg_of. rewrite H0. destruct ty. - simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto. - unfold const_low. simpl in H. rewrite H. auto. - simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto. - unfold const_low. simpl in H. rewrite H. auto. -Qed. - Lemma loadind_correct: forall (base: ireg) ofs ty dst k (rs: regset) m v, Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v -> @@ -846,50 +869,33 @@ Lemma loadind_correct: exists rs', exec_straight (loadind base ofs ty dst k) rs m k rs' m /\ rs'#(preg_of dst) = v - /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> preg_of dst -> r <> GPR0 -> rs'#r = rs#r. Proof. - intros. unfold loadind. - assert (preg_of dst <> PC). - unfold preg_of. case (mreg_type dst); discriminate. - (* short offset *) - case (Int.eq (high_s ofs) Int.zero). - exists (nextinstr (rs#(preg_of dst) <- v)). - split. apply exec_straight_one. apply loadind_aux_correct; auto. - unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. auto. auto. - split. rewrite nextinstr_inv; auto. apply Pregmap.gss. + intros. unfold loadind. destruct (Int.eq (high_s ofs) Int.zero). +(* one load *) + exists (nextinstr (rs#(preg_of dst) <- v)); split. + destruct ty; apply exec_straight_one; auto with ppcgen; simpl. + unfold load1. rewrite gpr_or_zero_not_zero; auto. + simpl in *. rewrite H. unfold preg_of; rewrite H0. auto. + unfold load1. rewrite gpr_or_zero_not_zero; auto. + simpl in *. rewrite H. unfold preg_of; rewrite H0. auto. + split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - (* long offset *) - pose (rs1 := nextinstr (rs#GPR12 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). - exists (nextinstr (rs1#(preg_of dst) <- v)). - split. apply exec_straight_two with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; auto. - apply loadind_aux_correct. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - rewrite Val.add_assoc. simpl. rewrite low_high_s. assumption. - auto. discriminate. reflexivity. - unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. auto. auto. - split. rewrite nextinstr_inv; auto. apply Pregmap.gss. +(* loadimm + one load *) + exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. + exists (nextinstr (rs'#(preg_of dst) <- v)); split. + eapply exec_straight_trans. eexact A. + destruct ty; apply exec_straight_one; auto with ppcgen; simpl. + unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. + unfold preg_of; rewrite H0. auto. congruence. + unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. + unfold preg_of; rewrite H0. auto. congruence. + split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. Qed. (** Indexed memory stores. *) -Lemma storeind_aux_correct: - forall (base: ireg) ofs ty src (rs: regset) m m', - Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' -> - mreg_type src = ty -> - base <> GPR0 -> - exec_instr ge fn (storeind_aux src base ofs ty) rs m = - OK (nextinstr rs) m'. -Proof. - intros. unfold storeind_aux. unfold preg_of in H. rewrite H0 in H. destruct ty. - simpl. unfold store1. rewrite gpr_or_zero_not_zero; auto. - unfold const_low. simpl in H. rewrite H. auto. - simpl. unfold store1. rewrite gpr_or_zero_not_zero; auto. - unfold const_low. simpl in H. rewrite H. auto. -Qed. - Lemma storeind_correct: forall (base: ireg) ofs ty src k (rs: regset) m m', Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' -> @@ -897,28 +903,31 @@ Lemma storeind_correct: base <> GPR0 -> exists rs', exec_straight (storeind src base ofs ty k) rs m k rs' m' - /\ forall r, r <> PC -> r <> GPR12 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r. Proof. - intros. unfold storeind. - (* short offset *) - case (Int.eq (high_s ofs) Int.zero). - exists (nextinstr rs). - split. apply exec_straight_one. apply storeind_aux_correct; auto. - reflexivity. + intros. unfold storeind. destruct (Int.eq (high_s ofs) Int.zero). +(* one store *) + exists (nextinstr rs); split. + destruct ty; apply exec_straight_one; auto with ppcgen; simpl. + unfold store1. rewrite gpr_or_zero_not_zero; auto. + simpl in *. unfold preg_of in H; rewrite H0 in H. rewrite H. auto. + unfold store1. rewrite gpr_or_zero_not_zero; auto. + simpl in *. unfold preg_of in H; rewrite H0 in H. rewrite H. auto. + intros. apply nextinstr_inv; auto. +(* loadimm + one store *) + exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. + assert (rs' base = rs base). apply C; auto with ppcgen. congruence. + assert (rs' (preg_of src) = rs (preg_of src)). apply C; auto with ppcgen. + exists (nextinstr rs'). + split. eapply exec_straight_trans. eexact A. + destruct ty; apply exec_straight_one; auto with ppcgen; simpl. + unfold store2. replace (IR (ireg_of src)) with (preg_of src). + rewrite H2; rewrite H3. rewrite B. simpl in H. rewrite H. auto. + unfold preg_of; rewrite H0; auto. + unfold store2. replace (FR (freg_of src)) with (preg_of src). + rewrite H2; rewrite H3. rewrite B. simpl in H. rewrite H. auto. + unfold preg_of; rewrite H0; auto. intros. rewrite nextinstr_inv; auto. - (* long offset *) - pose (rs1 := nextinstr (rs#GPR12 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). - exists (nextinstr rs1). - split. apply exec_straight_two with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; auto. - apply storeind_aux_correct; auto with ppcgen. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gso; auto with ppcgen. - rewrite Val.add_assoc. simpl. rewrite low_high_s. assumption. - reflexivity. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. Qed. (** Float comparisons. *) @@ -979,6 +988,19 @@ Ltac TypeInv := | _ => idtac end. +Ltac UseTypeInfo := + match goal with + | T: (mreg_type ?r = ?t), H: context[preg_of ?r] |- _ => + unfold preg_of in H; UseTypeInfo + | T: (mreg_type ?r = ?t), H: context[mreg_type ?r] |- _ => + rewrite T in H; UseTypeInfo + | T: (mreg_type ?r = ?t) |- context[preg_of ?r] => + unfold preg_of; UseTypeInfo + | T: (mreg_type ?r = ?t) |- context[mreg_type ?r] => + rewrite T; UseTypeInfo + | _ => idtac + end. + (** Translation of conditions. *) Lemma transl_cond_correct_aux: @@ -989,116 +1011,101 @@ Lemma transl_cond_correct_aux: exec_straight (transl_cond cond args k) rs m k rs' m /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) - then eval_condition_total cond (map ms args) - else Val.notbool (eval_condition_total cond (map ms args))) + then eval_condition_total cond (map rs (map preg_of args)) + else Val.notbool (eval_condition_total cond (map rs (map preg_of args)))) /\ agree ms sp rs'. Proof. - intros. destruct cond; simpl in H; TypeInv. + intros. + destruct cond; simpl in H; TypeInv; simpl; UseTypeInfo. (* Ccomp *) - simpl. - generalize (compare_sint_spec rs ms#m0 ms#m1). - intros [A [B [C D]]]. - exists (nextinstr (compare_sint rs ms#m0 ms#m1)). - split. apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs); auto). - reflexivity. + destruct (compare_sint_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))) + as [A [B [C D]]]. + econstructor; split. + apply exec_straight_one. simpl; reflexivity. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. apply agree_exten_2 with rs; auto. (* Ccompu *) - simpl. - generalize (compare_uint_spec rs ms#m0 ms#m1). - intros [A [B [C D]]]. - exists (nextinstr (compare_uint rs ms#m0 ms#m1)). - split. apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs); auto). - reflexivity. + destruct (compare_uint_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))) + as [A [B [C D]]]. + econstructor; split. + apply exec_straight_one. simpl; reflexivity. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. apply agree_exten_2 with rs; auto. (* Ccompimm *) - simpl. case (Int.eq (high_s i) Int.zero). - generalize (compare_sint_spec rs ms#m0 (Vint i)). - intros [A [B [C D]]]. - exists (nextinstr (compare_sint rs ms#m0 (Vint i))). - split. apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs); auto). - reflexivity. + destruct (compare_sint_spec rs (rs (ireg_of m0)) (Vint i)) + as [A [B [C D]]]. + econstructor; split. + apply exec_straight_one. simpl. eauto. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. apply agree_exten_2 with rs; auto. - generalize (loadimm_correct GPR12 i (Pcmpw (ireg_of m0) GPR12 :: k) rs m). + generalize (loadimm_correct GPR0 i (Pcmpw (ireg_of m0) GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTH1]]]. - assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. - generalize (compare_sint_spec rs1 ms#m0 (Vint i)). - intros [A [B [C D]]]. - exists (nextinstr (compare_sint rs1 ms#m0 (Vint i))). + destruct (compare_sint_spec rs1 (rs (ireg_of m0)) (Vint i)) + as [A [B [C D]]]. + assert (rs1 (ireg_of m0) = rs (ireg_of m0)). + apply OTH1; auto with ppcgen. decEq. auto with ppcgen. + exists (nextinstr (compare_sint rs1 (rs1 (ireg_of m0)) (Vint i))). split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs1); auto). rewrite RES1. - reflexivity. reflexivity. - split. + apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto. + reflexivity. + split. rewrite H. case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - apply agree_exten_2 with rs1; auto. + apply agree_exten_2 with rs; auto. + intros. rewrite H; rewrite D; auto. (* Ccompuimm *) - simpl. case (Int.eq (high_u i) Int.zero). - generalize (compare_uint_spec rs ms#m0 (Vint i)). - intros [A [B [C D]]]. - exists (nextinstr (compare_uint rs ms#m0 (Vint i))). - split. apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs); auto). - reflexivity. + destruct (compare_uint_spec rs (rs (ireg_of m0)) (Vint i)) + as [A [B [C D]]]. + econstructor; split. + apply exec_straight_one. simpl. eauto. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. apply agree_exten_2 with rs; auto. - generalize (loadimm_correct GPR12 i (Pcmplw (ireg_of m0) GPR12 :: k) rs m). + generalize (loadimm_correct GPR0 i (Pcmplw (ireg_of m0) GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTH1]]]. - assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. - generalize (compare_uint_spec rs1 ms#m0 (Vint i)). - intros [A [B [C D]]]. - exists (nextinstr (compare_uint rs1 ms#m0 (Vint i))). + destruct (compare_uint_spec rs1 (rs (ireg_of m0)) (Vint i)) + as [A [B [C D]]]. + assert (rs1 (ireg_of m0) = rs (ireg_of m0)). + apply OTH1; auto with ppcgen. decEq. auto with ppcgen. + exists (nextinstr (compare_uint rs1 (rs1 (ireg_of m0)) (Vint i))). split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs1); auto). rewrite RES1. - reflexivity. reflexivity. - split. + apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto. + reflexivity. + split. rewrite H. case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - apply agree_exten_2 with rs1; auto. + apply agree_exten_2 with rs; auto. + intros. rewrite H; rewrite D; auto. (* Ccompf *) - simpl. - generalize (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m). - intros [rs' [EX [RES OTH]]]. + destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m) + as [rs' [EX [RES OTH]]]. exists rs'. split. auto. - split. rewrite RES. repeat (rewrite <- (freg_val ms sp rs); auto). + split. apply RES. apply agree_exten_2 with rs; auto. (* Cnotcompf *) - simpl. - generalize (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m). - intros [rs' [EX [RES OTH]]]. + destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m) + as [rs' [EX [RES OTH]]]. exists rs'. split. auto. - split. rewrite RES. repeat (rewrite <- (freg_val ms sp rs); auto). + split. rewrite RES. assert (forall v1 v2, Val.notbool (Val.notbool (Val.cmpf c v1 v2)) = Val.cmpf c v1 v2). intros v1 v2; unfold Val.cmpf; destruct v1; destruct v2; auto. apply Val.notbool_idem2. - rewrite H. - generalize RES. case (snd (crbit_for_fcmp c)); simpl; auto. + rewrite H. case (snd (crbit_for_fcmp c)); simpl; auto. apply agree_exten_2 with rs; auto. (* Cmaskzero *) - simpl. - generalize (andimm_correct GPR12 (ireg_of m0) i k rs m (ireg_of_not_GPR12 m0)). - intros [rs' [A [B [C D]]]]. + destruct (andimm_correct GPR0 (ireg_of m0) i k rs m (ireg_of_not_GPR0 m0)) + as [rs' [A [B [C D]]]]. exists rs'. split. assumption. - split. rewrite C. rewrite <- (ireg_val ms sp rs); auto. + split. rewrite C. auto. apply agree_exten_2 with rs; auto. (* Cmasknotzero *) - simpl. - generalize (andimm_correct GPR12 (ireg_of m0) i k rs m (ireg_of_not_GPR12 m0)). - intros [rs' [A [B [C D]]]]. + destruct (andimm_correct GPR0 (ireg_of m0) i k rs m (ireg_of_not_GPR0 m0)) + as [rs' [A [B [C D]]]]. exists rs'. split. assumption. - split. rewrite C. rewrite <- (ireg_val ms sp rs); auto. - rewrite Val.notbool_idem3. reflexivity. + split. rewrite C. rewrite Val.notbool_idem3. reflexivity. apply agree_exten_2 with rs; auto. Qed. @@ -1115,31 +1122,37 @@ Lemma transl_cond_correct: else Val.notbool (Val.of_bool b)) /\ agree ms sp rs'. Proof. - intros. rewrite <- (eval_condition_weaken _ _ H1). - apply transl_cond_correct_aux; auto. + intros. + assert (eval_condition_total cond rs ## (preg_of ## args) = Val.of_bool b). + apply eval_condition_weaken. eapply eval_condition_lessdef; eauto. + eapply preg_vals; eauto. + rewrite <- H2. eapply transl_cond_correct_aux; eauto. Qed. (** Translation of arithmetic operations. *) Ltac TranslOpSimpl := + econstructor; split; + [ apply exec_straight_one; [simpl; eauto | reflexivity] + | auto 7 with ppcgen; fail ]. +(* match goal with - | |- exists rs' : regset, + | H: (Val.lessdef ?v ?v') |- + exists rs' : regset, exec_straight ?c ?rs ?m ?k rs' ?m /\ agree (Regmap.set ?res ?v ?ms) ?sp rs' => - (exists (nextinstr (rs#(ireg_of res) <- v)); + + (exists (nextinstr (rs#(ireg_of res) <- v')); split; - [ apply exec_straight_one; - [ repeat (rewrite (ireg_val ms sp rs); auto); reflexivity - | reflexivity ] + [ apply exec_straight_one; auto; fail | auto with ppcgen ]) || - (exists (nextinstr (rs#(freg_of res) <- v)); + (exists (nextinstr (rs#(freg_of res) <- v')); split; - [ apply exec_straight_one; - [ repeat (rewrite (freg_val ms sp rs); auto); reflexivity - | reflexivity ] + [ apply exec_straight_one; auto; fail | auto with ppcgen ]) end. +*) Lemma transl_op_correct: forall op args res k ms sp rs m v, @@ -1147,41 +1160,44 @@ Lemma transl_op_correct: agree ms sp rs -> eval_operation ge sp op (map ms args) = Some v -> exists rs', - exec_straight (transl_op op args res k) rs m k rs' m - /\ agree (Regmap.set res v ms) sp rs'. + exec_straight (transl_op op args res k) rs m k rs' m + /\ agree (Regmap.set res v (undef_op op ms)) sp rs'. Proof. - intros. rewrite <- (eval_operation_weaken _ _ _ _ H1). clear H1; clear v. - inversion H. + intros. + assert (exists v', Val.lessdef v v' /\ + eval_operation_total ge sp op (map rs (map preg_of args)) = v'). + exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. + intros [v' [A B]]. exists v'; split; auto. + apply eval_operation_weaken; eauto. + destruct H2 as [v' [LD EQ]]. clear H1. + inv H. (* Omove *) - simpl. exists (nextinstr (rs#(preg_of res) <- (ms r1))). - split. caseEq (mreg_type r1); intro. - apply exec_straight_one. simpl. rewrite (ireg_val ms sp rs); auto. - simpl. unfold preg_of. rewrite <- H2. rewrite H5. reflexivity. - auto with ppcgen. - apply exec_straight_one. simpl. rewrite (freg_val ms sp rs); auto. - simpl. unfold preg_of. rewrite <- H2. rewrite H5. reflexivity. - auto with ppcgen. - auto with ppcgen. + simpl in *. + exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))). + split. unfold preg_of. rewrite <- H2. + destruct (mreg_type r1); apply exec_straight_one; auto. + auto with ppcgen. (* Other instructions *) - clear H1; clear H2; clear H4. - destruct op; simpl in H5; injection H5; clear H5; intros; - TypeInv; simpl; try (TranslOpSimpl). + destruct op; simpl; simpl in H5; injection H5; clear H5; intros; + TypeInv; simpl in *; UseTypeInfo; try (TranslOpSimpl). (* Omove again *) congruence. (* Ointconst *) - generalize (loadimm_correct (ireg_of res) i k rs m). - intros [rs' [A [B C]]]. + destruct (loadimm_correct (ireg_of res) i k rs m) + as [rs' [A [B C]]]. exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto. + rewrite <- B in LD. eauto with ppcgen. (* Ofloatconst *) - exists (nextinstr (rs#(freg_of res) <- (Vfloat f) #GPR12 <- Vundef)). + exists (nextinstr (rs #GPR12 <- Vundef #(freg_of res) <- (Vfloat f))). split. apply exec_straight_one. reflexivity. reflexivity. - auto with ppcgen. + apply agree_nextinstr. apply agree_set_mfreg; auto. apply agree_set_mreg; auto. + eapply agree_undef_temps; eauto. + intros. apply Pregmap.gso; auto. (* Oaddrsymbol *) - change (find_symbol_offset ge i i0) with (symbol_offset ge i i0). - set (v := symbol_offset ge i i0). - pose (rs1 := nextinstr (rs#GPR12 <- (high_half v))). - exists (nextinstr (rs1#(ireg_of res) <- v)). + change (find_symbol_offset ge i i0) with (symbol_offset ge i i0) in LD. + set (v' := symbol_offset ge i i0) in *. + pose (rs1 := nextinstr (rs#GPR12 <- (high_half v'))). + exists (nextinstr (rs1#(ireg_of res) <- v')). split. apply exec_straight_two with rs1 m. unfold exec_instr. rewrite gpr_or_zero_zero. unfold const_high. rewrite Val.add_commut. @@ -1189,173 +1205,127 @@ Proof. simpl. rewrite gpr_or_zero_not_zero. 2: congruence. unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - fold v. rewrite Val.add_commut. unfold v. rewrite low_high_half. + fold v'. rewrite Val.add_commut. unfold v'. rewrite low_high_half. reflexivity. reflexivity. reflexivity. unfold rs1. apply agree_nextinstr. apply agree_set_mireg; auto. - apply agree_set_mreg. apply agree_nextinstr. - apply agree_set_other. auto. simpl. tauto. + apply agree_set_mreg; auto. apply agree_nextinstr. + eapply agree_undef_temps; eauto. + intros. apply Pregmap.gso; auto. (* Oaddrstack *) - assert (GPR1 <> GPR12). discriminate. - generalize (addimm_correct (ireg_of res) GPR1 i k rs m H2). + assert (GPR1 <> GPR0). discriminate. + generalize (addimm_correct (ireg_of res) GPR1 i k rs m (ireg_of_not_GPR0 res) H1). intros [rs' [EX [RES OTH]]]. exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto. - rewrite (sp_val ms sp rs). auto. auto. + apply agree_set_mireg_exten with rs; auto with ppcgen. + rewrite (sp_val ms sp rs) in LD; auto. rewrite RES; auto. (* Ocast8unsigned *) - exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 255)))). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity. - replace (Val.zero_ext 8 (ms m0)) - with (Val.rolm (ms m0) Int.zero (Int.repr 255)). + econstructor; split. + apply exec_straight_one. simpl; reflexivity. reflexivity. + replace (Val.zero_ext 8 (rs (ireg_of m0))) + with (Val.rolm (rs (ireg_of m0)) Int.zero (Int.repr 255)) in LD. auto with ppcgen. - unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto. + unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto. rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto. (* Ocast16unsigned *) - exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 65535)))). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity. - replace (Val.zero_ext 16 (ms m0)) - with (Val.rolm (ms m0) Int.zero (Int.repr 65535)). + econstructor; split. + apply exec_straight_one. simpl; reflexivity. reflexivity. + replace (Val.zero_ext 16 (rs (ireg_of m0))) + with (Val.rolm (rs (ireg_of m0)) Int.zero (Int.repr 65535)) in LD. auto with ppcgen. - unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto. + unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto. rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto. (* Oaddimm *) generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m - (ireg_of_not_GPR12 m0)). + (ireg_of_not_GPR0 res) (ireg_of_not_GPR0 m0)). intros [rs' [A [B C]]]. exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto. - rewrite (ireg_val ms sp rs); auto. - (* Osub *) - exists (nextinstr (rs#(ireg_of res) <- (Val.sub (ms m0) (ms m1)) #CARRY <- Vundef)). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). - simpl. reflexivity. auto with ppcgen. + rewrite <- B in LD. eauto with ppcgen. (* Osubimm *) case (Int.eq (high_s i) Int.zero). - exists (nextinstr (rs#(ireg_of res) <- (Val.sub (Vint i) (ms m0)) #CARRY <- Vundef)). - split. apply exec_straight_one. rewrite (ireg_val ms sp rs); auto. - reflexivity. simpl. auto with ppcgen. - generalize (loadimm_correct GPR12 i (Psubfc (ireg_of res) (ireg_of m0) GPR12 :: k) rs m). + econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + auto 7 with ppcgen. + generalize (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m). intros [rs1 [EX [RES OTH]]]. - assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. - exists (nextinstr (rs1#(ireg_of res) <- (Val.sub (Vint i) (ms m0)) #CARRY <- Vundef)). - split. eapply exec_straight_trans. eexact EX. - apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). - simpl. rewrite RES. rewrite OTH. reflexivity. - generalize (ireg_of_not_GPR12 m0); congruence. - discriminate. - reflexivity. simpl; auto with ppcgen. + econstructor; split. + eapply exec_straight_trans. eexact EX. + apply exec_straight_one. simpl; eauto. auto. + rewrite RES. rewrite OTH; auto with ppcgen. + assert (agree (undef_temps ms) sp rs1). eauto with ppcgen. + auto with ppcgen. decEq; auto with ppcgen. (* Omulimm *) case (Int.eq (high_s i) Int.zero). - exists (nextinstr (rs#(ireg_of res) <- (Val.mul (ms m0) (Vint i)))). - split. apply exec_straight_one. rewrite (ireg_val ms sp rs); auto. - reflexivity. auto with ppcgen. - generalize (loadimm_correct GPR12 i (Pmullw (ireg_of res) (ireg_of m0) GPR12 :: k) rs m). + econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + auto with ppcgen. + generalize (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m). intros [rs1 [EX [RES OTH]]]. - assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. - exists (nextinstr (rs1#(ireg_of res) <- (Val.mul (ms m0) (Vint i)))). - split. eapply exec_straight_trans. eexact EX. - apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). - simpl. rewrite RES. rewrite OTH. reflexivity. - generalize (ireg_of_not_GPR12 m0); congruence. - discriminate. - reflexivity. simpl; auto with ppcgen. + assert (agree (undef_temps ms) sp rs1). eauto with ppcgen. + econstructor; split. + eapply exec_straight_trans. eexact EX. + apply exec_straight_one. simpl; eauto. auto. + rewrite RES. rewrite OTH; auto with ppcgen. decEq; auto with ppcgen. (* Oand *) - pose (v := Val.and (ms m0) (ms m1)). - pose (rs1 := rs#(ireg_of res) <- v). - generalize (compare_sint_spec rs1 v Vzero). + set (v' := Val.and (rs (ireg_of m0)) (rs (ireg_of m1))) in *. + pose (rs1 := rs#(ireg_of res) <- v'). + generalize (compare_sint_spec rs1 v' Vzero). intros [A [B [C D]]]. - exists (nextinstr (compare_sint rs1 v Vzero)). - split. apply exec_straight_one. - unfold rs1, v. repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. - apply agree_exten_2 with rs1. unfold rs1, v; auto with ppcgen. + exists (nextinstr (compare_sint rs1 v' Vzero)). + split. apply exec_straight_one. auto. auto. + apply agree_exten_2 with rs1. unfold rs1; auto with ppcgen. auto. (* Oandimm *) generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m - (ireg_of_not_GPR12 m0)). + (ireg_of_not_GPR0 m0)). intros [rs' [A [B [C D]]]]. - exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto. - rewrite (ireg_val ms sp rs); auto. + exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. (* Oorimm *) generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m). intros [rs' [A [B C]]]. - exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto. - rewrite (ireg_val ms sp rs); auto. + exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. (* Oxorimm *) generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m). intros [rs' [A [B C]]]. - exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto. - rewrite (ireg_val ms sp rs); auto. - (* Oshr *) - exists (nextinstr (rs#(ireg_of res) <- (Val.shr (ms m0) (ms m1)) #CARRY <- (Val.shr_carry (ms m0) (ms m1)))). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. auto with ppcgen. - (* Oshrimm *) - exists (nextinstr (rs#(ireg_of res) <- (Val.shr (ms m0) (Vint i)) #CARRY <- (Val.shr_carry (ms m0) (Vint i)))). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. auto with ppcgen. + exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. (* Oxhrximm *) - pose (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shr (ms m0) (Vint i)) #CARRY <- (Val.shr_carry (ms m0) (Vint i)))). - exists (nextinstr (rs1#(ireg_of res) <- (Val.shrx (ms m0) (Vint i)))). + pose (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shr (rs (ireg_of m0)) (Vint i)) #CARRY <- (Val.shr_carry (rs (ireg_of m0)) (Vint i)))). + exists (nextinstr (rs1#(ireg_of res) <- (Val.shrx (rs (ireg_of m0)) (Vint i)))). split. apply exec_straight_two with rs1 m. - unfold rs1; rewrite (ireg_val ms sp rs); auto. - simpl; unfold rs1; repeat rewrite <- (ireg_val ms sp rs); auto. - repeat (rewrite nextinstr_inv; try discriminate). - repeat rewrite Pregmap.gss. decEq. decEq. - apply (f_equal3 (@Pregmap.set val)); auto. - rewrite Pregmap.gso. rewrite Pregmap.gss. apply Val.shrx_carry. - discriminate. reflexivity. reflexivity. - apply agree_exten_2 with (rs#(ireg_of res) <- (Val.shrx (ms m0) (Vint i))). - auto with ppcgen. - intros. rewrite nextinstr_inv; auto. - case (preg_eq (ireg_of res) r); intro. - subst r. repeat rewrite Pregmap.gss. auto. - repeat rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. - repeat rewrite Pregmap.gso; auto. + auto. simpl. decEq. decEq. decEq. + unfold rs1. repeat (rewrite nextinstr_inv; try discriminate). + rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. + apply Val.shrx_carry. auto with ppcgen. auto. auto. + apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. + apply agree_set_commut. auto with ppcgen. + apply agree_set_other. apply agree_set_mireg_twice; auto with ppcgen. + compute; auto. auto with ppcgen. (* Ointoffloat *) - exists (nextinstr (rs#(ireg_of res) <- (Val.intoffloat (ms m0)) #FPR13 <- Vundef)). - split. apply exec_straight_one. - repeat (rewrite (freg_val ms sp rs); auto). - reflexivity. auto with ppcgen. - (* Ointuoffloat *) - exists (nextinstr (rs#(ireg_of res) <- (Val.intuoffloat (ms m0)) #FPR13 <- Vundef)). - split. apply exec_straight_one. - repeat (rewrite (freg_val ms sp rs); auto). - reflexivity. auto with ppcgen. - (* Ofloatofint *) - exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)) #GPR12 <- Vundef #FPR13 <- Vundef)). - split. apply exec_straight_one. - repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. auto 10 with ppcgen. - (* Ofloatofintu *) - exists (nextinstr (rs#(freg_of res) <- (Val.floatofintu (ms m0)) #GPR12 <- Vundef #FPR13 <- Vundef)). - split. apply exec_straight_one. - repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. auto 10 with ppcgen. + econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + apply agree_nextinstr. apply agree_set_mireg; auto. apply agree_set_mreg; auto. + apply agree_undef_temps with rs; auto. intros. + repeat rewrite Pregmap.gso; auto. (* Ocmp *) - generalize H2; case (classify_condition c args); intros. + revert H1 LD; case (classify_condition c args); intros. (* Optimization: compimm Cge 0 *) - subst n. simpl in H4. simpl. - set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.rolm (ms r) Int.one Int.one))). + subst n. simpl in *. inv H1. UseTypeInfo. + set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))). set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.xor (rs1#(ireg_of res)) (Vint Int.one)))). exists rs2. - split. apply exec_straight_two with rs1 m. - simpl. unfold rs1. rewrite (ireg_val ms sp rs); auto. congruence. - auto. auto. auto. - rewrite <- Val.rolm_ge_zero. + split. apply exec_straight_two with rs1 m; auto. + rewrite <- Val.rolm_ge_zero in LD. unfold rs2. apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. fold rs1. - replace (rs1 (ireg_of res)) with (Val.rolm (ms r) Int.one Int.one). - apply agree_set_mireg_twice; auto. + replace (rs1 (ireg_of res)) with (Val.rolm (rs (ireg_of r)) Int.one Int.one). + apply agree_set_mireg_twice; auto with ppcgen. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. auto. auto with ppcgen. auto with ppcgen. (* Optimization: compimm Clt 0 *) - subst n. simpl in H4. simpl. - exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms r) Int.one Int.one))). - split. apply exec_straight_one. simpl. rewrite (ireg_val ms sp rs); auto. congruence. - auto. - apply agree_nextinstr. apply agree_set_mireg. - rewrite Val.rolm_lt_zero. apply agree_set_mreg. auto. congruence. + subst n. simpl in *. inv H1. UseTypeInfo. + exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))). + split. apply exec_straight_one; auto. + rewrite <- Val.rolm_lt_zero in LD. + auto with ppcgen. (* General case *) set (bit := fst (crbit_for_cond c0)). set (isset := snd (crbit_for_cond c0)). @@ -1364,7 +1334,7 @@ Proof. (if isset then k else Pxori (ireg_of res) (ireg_of res) (Cint Int.one) :: k)). - generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m H4 H0). + generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m H1 H0). fold bit; fold isset. intros [rs1 [EX1 [RES1 AG1]]]. set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#(reg_of_crbit bit)))). @@ -1374,89 +1344,63 @@ Proof. unfold k1. apply exec_straight_one. reflexivity. reflexivity. unfold rs2. rewrite RES1. auto with ppcgen. - exists (nextinstr (rs2#(ireg_of res) <- (eval_condition_total c0 ms##rl))). + econstructor. split. apply exec_straight_trans with k1 rs1 m. assumption. unfold k1. apply exec_straight_two with rs2 m. - reflexivity. simpl. - replace (Val.xor (rs2 (ireg_of res)) (Vint Int.one)) - with (eval_condition_total c0 ms##rl). - reflexivity. - unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - rewrite RES1. apply Val.notbool_xor. apply eval_condition_total_is_bool. - reflexivity. reflexivity. - unfold rs2. auto with ppcgen. + reflexivity. simpl. eauto. auto. auto. + apply agree_nextinstr. + unfold rs2 at 1. rewrite nextinstr_inv. rewrite Pregmap.gss. + rewrite RES1. rewrite <- Val.notbool_xor. + unfold rs2. auto 7 with ppcgen. + apply eval_condition_total_is_bool. + auto with ppcgen. Qed. Lemma transl_load_store_correct: forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - addr args k ms sp rs m ms' m', + addr args (temp: ireg) k ms sp rs m ms' m', (forall cst (r1: ireg) (rs1: regset) k, - eval_addressing_total ge sp addr (map ms args) = + eval_addressing_total ge sp addr (map rs (map preg_of args)) = Val.add (gpr_or_zero rs1 r1) (const_low ge cst) -> - agree ms sp rs1 -> + (forall (r: preg), r <> PC -> r <> temp -> rs1 r = rs r) -> exists rs', exec_straight (mk1 cst r1 :: k) rs1 m k rs' m' /\ agree ms' sp rs') -> - (forall (r1 r2: ireg) (rs1: regset) k, - eval_addressing_total ge sp addr (map ms args) = Val.add rs1#r1 rs1#r2 -> - agree ms sp rs1 -> + (forall (r1 r2: ireg) k, + eval_addressing_total ge sp addr (map rs (map preg_of args)) = Val.add rs#r1 rs#r2 -> exists rs', - exec_straight (mk2 r1 r2 :: k) rs1 m k rs' m' /\ + exec_straight (mk2 r1 r2 :: k) rs m k rs' m' /\ agree ms' sp rs') -> agree ms sp rs -> map mreg_type args = type_of_addressing addr -> + temp <> GPR0 -> exists rs', - exec_straight (transl_load_store mk1 mk2 addr args k) rs m + exec_straight (transl_load_store mk1 mk2 addr args temp k) rs m k rs' m' /\ agree ms' sp rs'. Proof. intros. destruct addr; simpl in H2; TypeInv; simpl. (* Aindexed *) - case (ireg_eq (ireg_of t) GPR0); intro. - (* Aindexed from GPR0 *) - set (rs1 := nextinstr (rs#GPR12 <- (ms t))). - set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))). - assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) = - Val.add (gpr_or_zero rs2 GPR12) (const_low ge (Cint (low_s i)))). - simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. - unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss. - rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. - discriminate. - assert (AG: agree ms sp rs2). unfold rs2, rs1; auto 6 with ppcgen. - destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']]. - exists rs'. split. - apply exec_straight_trans with (mk1 (Cint (low_s i)) GPR12 :: k) rs2 m. - apply exec_straight_two with rs1 m. - unfold rs1. rewrite (ireg_val ms sp rs); auto. - unfold rs2. replace (ms t) with (rs1#GPR12). auto. - unfold rs1. rewrite nextinstr_inv. apply Pregmap.gss. discriminate. - reflexivity. reflexivity. - assumption. assumption. - (* Aindexed short *) case (Int.eq (high_s i) Int.zero). - assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) = - Val.add (gpr_or_zero rs (ireg_of t)) (const_low ge (Cint i))). - simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. - rewrite (ireg_val ms sp rs); auto. - destruct (H _ _ _ k ADDR H1) as [rs' [EX' AG']]. - exists rs'. split. auto. auto. + (* Aindexed short *) + apply H. + simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto with ppcgen. + auto. (* Aindexed long *) - set (rs1 := nextinstr (rs#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))). - assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) = - Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Cint (low_s i)))). - simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. - unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. + set (rs1 := nextinstr (rs#temp <- (Val.add (rs (ireg_of m0)) (Vint (Int.shl (high_s i) (Int.repr 16)))))). + exploit (H (Cint (low_s i)) temp rs1 k). + simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto. + unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. discriminate. - assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen. - destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']]. + intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; auto. - rewrite <- (ireg_val ms sp rs); auto. reflexivity. - assumption. assumption. + simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto. + auto. auto. (* Aindexed2 *) apply H0. - simpl. repeat (rewrite (ireg_val ms sp rs); auto). auto. + simpl. UseTypeInfo; auto. (* Aglobal *) case_eq (symbol_is_small_data i i0); intro SISD. (* Aglobal from small data *) @@ -1466,17 +1410,16 @@ Proof. destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero. auto. auto. (* Aglobal general case *) - set (rs1 := nextinstr (rs#GPR12 <- (const_high ge (Csymbol_high i i0)))). - assert (ADDR: eval_addressing_total ge sp (Aglobal i i0) ms##nil = - Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Csymbol_low i i0))). + set (rs1 := nextinstr (rs#temp <- (const_high ge (Csymbol_high i i0)))). + exploit (H (Csymbol_low i i0) temp rs1 k). simpl. rewrite gpr_or_zero_not_zero; auto. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. unfold const_high, const_low. set (v := symbol_offset ge i i0). symmetry. rewrite Val.add_commut. unfold v. apply low_high_half. - discriminate. discriminate. - assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen. - destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']]. + discriminate. + intros; unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. unfold exec_instr. rewrite gpr_or_zero_zero. rewrite Val.add_commut. unfold const_high. @@ -1484,153 +1427,142 @@ Proof. reflexivity. reflexivity. assumption. assumption. (* Abased *) - assert (COMMON: - forall (rs1: regset) r, - r <> GPR0 -> - ms t = rs1#r -> - agree ms sp rs1 -> - exists rs', - exec_straight - (Paddis GPR12 r (Csymbol_high i i0) - :: mk1 (Csymbol_low i i0) GPR12 :: k) rs1 m k rs' m' - /\ agree ms' sp rs'). - intros. - set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (const_high ge (Csymbol_high i i0))))). - assert (ADDR: eval_addressing_total ge sp (Abased i i0) ms##(t::nil) = - Val.add (gpr_or_zero rs2 GPR12) (const_low ge (Csymbol_low i i0))). - simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. - unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss. - unfold const_high. - set (v := symbol_offset ge i i0). + set (rs1 := nextinstr (rs#temp <- (Val.add (rs (ireg_of m0)) (const_high ge (Csymbol_high i i0))))). + exploit (H (Csymbol_low i i0) temp rs1 k). + simpl. rewrite gpr_or_zero_not_zero; auto. + unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. rewrite Val.add_assoc. - rewrite (Val.add_commut (high_half v)). - unfold v. rewrite low_high_half. apply Val.add_commut. - discriminate. - assert (AG: agree ms sp rs2). unfold rs2; auto with ppcgen. - destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']]. - exists rs'. split. apply exec_straight_step with rs2 m. - unfold exec_instr. rewrite gpr_or_zero_not_zero; auto. - rewrite <- H3. reflexivity. reflexivity. - assumption. assumption. - case (ireg_eq (ireg_of t) GPR0); intro. - set (rs1 := nextinstr (rs#GPR12 <- (ms t))). - assert (R1: GPR12 <> GPR0). discriminate. - assert (R2: ms t = rs1 GPR12). - unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss; auto. - discriminate. - assert (R3: agree ms sp rs1). unfold rs1; auto with ppcgen. - generalize (COMMON rs1 GPR12 R1 R2 R3). intros [rs' [EX' AG']]. - exists rs'. split. - apply exec_straight_step with rs1 m. - unfold rs1. rewrite (ireg_val ms sp rs); auto. reflexivity. + unfold const_high, const_low. + set (v := symbol_offset ge i i0). + symmetry. rewrite Val.add_commut. decEq. + unfold v. rewrite Val.add_commut. apply low_high_half. + UseTypeInfo. auto. discriminate. + intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + intros [rs' [EX' AG']]. + exists rs'. split. apply exec_straight_step with rs1 m. + unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto. assumption. assumption. - apply COMMON; auto. eapply ireg_val; eauto. (* Ainstack *) case (Int.eq (high_s i) Int.zero). apply H. simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. rewrite (sp_val ms sp rs); auto. auto. - set (rs1 := nextinstr (rs#GPR12 <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))). - assert (ADDR: eval_addressing_total ge sp (Ainstack i) ms##nil = - Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Cint (low_s i)))). - simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. + set (rs1 := nextinstr (rs#temp <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))). + exploit (H (Cint (low_s i)) temp rs1 k). + simpl. rewrite gpr_or_zero_not_zero; auto. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. - rewrite Val.add_assoc. decEq. simpl. rewrite low_high_s. auto. - discriminate. - assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen. - destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']]. + rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. + congruence. + intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. - simpl. rewrite gpr_or_zero_not_zero. - unfold rs1. rewrite (sp_val ms sp rs). reflexivity. - auto. discriminate. reflexivity. assumption. assumption. + unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen. + rewrite <- (sp_val ms sp rs); auto. auto. + assumption. assumption. Qed. (** Translation of memory loads. *) Lemma transl_load_correct: forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - chunk addr args k ms sp rs m dst a v, + chunk addr args k ms sp rs m m' dst a v, (forall cst (r1: ireg) (rs1: regset), - exec_instr ge fn (mk1 cst r1) rs1 m = - load1 ge chunk (preg_of dst) cst r1 rs1 m) -> + exec_instr ge fn (mk1 cst r1) rs1 m' = + load1 ge chunk (preg_of dst) cst r1 rs1 m') -> (forall (r1 r2: ireg) (rs1: regset), - exec_instr ge fn (mk2 r1 r2) rs1 m = - load2 chunk (preg_of dst) r1 r2 rs1 m) -> + exec_instr ge fn (mk2 r1 r2) rs1 m' = + load2 chunk (preg_of dst) r1 r2 rs1 m') -> agree ms sp rs -> map mreg_type args = type_of_addressing addr -> eval_addressing ge sp addr (map ms args) = Some a -> Mem.loadv chunk m a = Some v -> + Mem.extends m m' -> exists rs', - exec_straight (transl_load_store mk1 mk2 addr args k) rs m - k rs' m - /\ agree (Regmap.set dst v ms) sp rs'. + exec_straight (transl_load_store mk1 mk2 addr args GPR12 k) rs m' + k rs' m' + /\ agree (Regmap.set dst v (undef_temps ms)) sp rs'. Proof. - intros. apply transl_load_store_correct with ms. - intros. exists (nextinstr (rs1#(preg_of dst) <- v)). - split. apply exec_straight_one. rewrite H. - unfold load1. rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4. - rewrite H5 in H4. rewrite H4. auto. - auto with ppcgen. auto with ppcgen. - intros. exists (nextinstr (rs1#(preg_of dst) <- v)). + intros. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + intros [a' [A B]]. + exploit Mem.loadv_extends; eauto. intros [v' [C D]]. + exploit eval_addressing_weaken. eexact A. intro E. rewrite <- E in C. + apply transl_load_store_correct with ms; auto. +(* mk1 *) + intros. exists (nextinstr (rs1#(preg_of dst) <- v')). + split. apply exec_straight_one. rewrite H. + unfold load1. rewrite <- H6. rewrite C. auto. + auto with ppcgen. + eauto with ppcgen. +(* mk2 *) + intros. exists (nextinstr (rs#(preg_of dst) <- v')). split. apply exec_straight_one. rewrite H0. - unfold load2. - rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4. - rewrite H5 in H4. rewrite H4. auto. - auto with ppcgen. auto with ppcgen. - auto. auto. + unfold load2. rewrite <- H6. rewrite C. auto. + auto with ppcgen. + eauto with ppcgen. +(* not GPR0 *) + congruence. Qed. (** Translation of memory stores. *) Lemma transl_store_correct: forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - chunk addr args k ms sp rs m src a m', - (forall cst (r1: ireg) (rs1: regset), - exists rs2, - exec_instr ge fn (mk1 cst r1) rs1 m = - store1 ge chunk (preg_of src) cst r1 rs2 m - /\ (forall (r: preg), r <> FPR13 -> rs2 r = rs1 r)) -> - (forall (r1 r2: ireg) (rs1: regset), - exists rs2, - exec_instr ge fn (mk2 r1 r2) rs1 m = - store2 chunk (preg_of src) r1 r2 rs2 m - /\ (forall (r: preg), r <> FPR13 -> rs2 r = rs1 r)) -> + chunk addr args k ms sp rs m src a m' m1, + (forall cst (r1: ireg) (rs1 rs2: regset) (m2: mem), + store1 ge chunk (preg_of src) cst r1 rs1 m1 = OK rs2 m2 -> + exists rs3, + exec_instr ge fn (mk1 cst r1) rs1 m1 = OK rs3 m2 + /\ (forall (r: preg), r <> FPR13 -> rs3 r = rs2 r)) -> + (forall (r1 r2: ireg) (rs1 rs2: regset) (m2: mem), + store2 chunk (preg_of src) r1 r2 rs1 m1 = OK rs2 m2 -> + exists rs3, + exec_instr ge fn (mk2 r1 r2) rs1 m1 = OK rs3 m2 + /\ (forall (r: preg), r <> FPR13 -> rs3 r = rs2 r)) -> agree ms sp rs -> map mreg_type args = type_of_addressing addr -> eval_addressing ge sp addr (map ms args) = Some a -> Mem.storev chunk m a (ms src) = Some m' -> - exists rs', - exec_straight (transl_load_store mk1 mk2 addr args k) rs m - k rs' m' - /\ agree ms sp rs'. + Mem.extends m m1 -> + exists m1', + Mem.extends m' m1' + /\ exists rs', + exec_straight (transl_load_store mk1 mk2 addr args (int_temp_for src) k) rs m1 + k rs' m1' + /\ agree (undef_temps ms) sp rs'. Proof. - intros. apply transl_load_store_correct with ms. - intros. destruct (H cst r1 rs1) as [rs2 [A B]]. - exists (nextinstr rs2). - split. apply exec_straight_one. rewrite A. - unfold store1. rewrite B. replace (gpr_or_zero rs2 r1) with (gpr_or_zero rs1 r1). - rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4. - rewrite H5 in H4. elim H6; intros. rewrite H8 in H4. - rewrite H4. auto. - unfold gpr_or_zero. destruct (ireg_eq r1 GPR0); auto. symmetry. apply B. discriminate. - apply preg_of_not. simpl. tauto. - rewrite <- B. auto. discriminate. - apply agree_nextinstr. eapply agree_exten_2; eauto. - - intros. destruct (H0 r1 r2 rs1) as [rs2 [A B]]. - exists (nextinstr rs2). - split. apply exec_straight_one. rewrite A. - unfold store2. repeat rewrite B. - rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4. - rewrite H5 in H4. elim H6; intros. rewrite H8 in H4. - rewrite H4. auto. - apply preg_of_not. simpl. tauto. - discriminate. discriminate. - rewrite <- B. auto. discriminate. - apply agree_nextinstr. eapply agree_exten_2; eauto. - - auto. auto. + intros. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + intros [a' [A B]]. + assert (Z: Val.lessdef (ms src) (rs (preg_of src))). eapply preg_val; eauto. + exploit Mem.storev_extends; eauto. intros [m1' [C D]]. + exploit eval_addressing_weaken. eexact A. intro E. rewrite <- E in C. + exists m1'; split; auto. + apply transl_load_store_correct with ms; auto. +(* mk1 *) + intros. + exploit (H cst r1 rs1 (nextinstr rs1) m1'). + unfold store1. rewrite <- H6. + replace (rs1 (preg_of src)) with (rs (preg_of src)). + rewrite C. auto. + symmetry. apply H7. auto with ppcgen. + apply sym_not_equal. apply int_temp_for_diff. + intros [rs3 [U V]]. + exists rs3; split. + apply exec_straight_one. auto. rewrite V; auto with ppcgen. + eapply agree_undef_temps; eauto. intros. + rewrite V; auto. rewrite nextinstr_inv; auto. apply H7; auto. + unfold int_temp_for. destruct (mreg_eq src IT2); auto. +(* mk2 *) + intros. + exploit (H0 r1 r2 rs (nextinstr rs) m1'). + unfold store2. rewrite <- H6. rewrite C. auto. + intros [rs3 [U V]]. + exists rs3; split. + apply exec_straight_one. auto. rewrite V; auto with ppcgen. + eapply agree_undef_temps; eauto. intros. + rewrite V; auto. rewrite nextinstr_inv; auto. + unfold int_temp_for. destruct (mreg_eq src IT2); congruence. Qed. - End STRAIGHTLINE. diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v index d55635b1..ae3c2bdb 100644 --- a/powerpc/Asmgenretaddr.v +++ b/powerpc/Asmgenretaddr.v @@ -109,7 +109,7 @@ Hint Resolve loadimm_tail: ppcretaddr. Lemma addimm_tail: forall r1 r2 n k, is_tail k (addimm r1 r2 n k). -Proof. unfold addimm, addimm_1, addimm_2; intros; IsTail. Qed. +Proof. unfold addimm; intros; IsTail. Qed. Hint Resolve addimm_tail: ppcretaddr. Lemma andimm_tail: @@ -129,12 +129,12 @@ Hint Resolve xorimm_tail: ppcretaddr. Lemma loadind_tail: forall base ofs ty dst k, is_tail k (loadind base ofs ty dst k). -Proof. unfold loadind; intros; IsTail. Qed. +Proof. unfold loadind; intros. destruct ty; IsTail. Qed. Hint Resolve loadind_tail: ppcretaddr. Lemma storeind_tail: forall src base ofs ty k, is_tail k (storeind src base ofs ty k). -Proof. unfold storeind; intros; IsTail. Qed. +Proof. unfold storeind; intros. destruct ty; IsTail. Qed. Hint Resolve storeind_tail: ppcretaddr. Lemma floatcomp_tail: @@ -156,8 +156,8 @@ Qed. Hint Resolve transl_op_tail: ppcretaddr. Lemma transl_load_store_tail: - forall mk1 mk2 addr args k, - is_tail k (transl_load_store mk1 mk2 addr args k). + forall mk1 mk2 addr args temp k, + is_tail k (transl_load_store mk1 mk2 addr args temp k). Proof. unfold transl_load_store; intros; destruct addr; IsTail. Qed. Hint Resolve transl_load_store_tail: ppcretaddr. diff --git a/powerpc/ConstpropOp.v b/powerpc/ConstpropOp.v index ededce07..b6eecc74 100644 --- a/powerpc/ConstpropOp.v +++ b/powerpc/ConstpropOp.v @@ -182,9 +182,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) := | Omulsubf, F n1 :: F n2 :: F n3 :: nil => F(Float.sub (Float.mul n1 n2) n3) | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1) | Ointoffloat, F n1 :: nil => I(Float.intoffloat n1) - | Ointuoffloat, F n1 :: nil => I(Float.intuoffloat n1) - | Ofloatofint, I n1 :: nil => F(Float.floatofint n1) - | Ofloatofintu, I n1 :: nil => F(Float.floatofintu n1) + | Ofloatofwords, I n1 :: I n2 :: nil => F(Float.from_words n1 n2) | Ocmp c, vl => match eval_static_condition c vl with | None => Unknown @@ -322,11 +320,8 @@ Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), forall n1, eval_static_operation_cases (Ointoffloat) (F n1 :: nil) | eval_static_operation_case45: - forall n1, - eval_static_operation_cases (Ofloatofint) (I n1 :: nil) - | eval_static_operation_case46: - forall n1, - eval_static_operation_cases (Ofloatofintu) (I n1 :: nil) + forall n1 n2, + eval_static_operation_cases (Ofloatofwords) (I n1 :: I n2 :: nil) | eval_static_operation_case47: forall c vl, eval_static_operation_cases (Ocmp c) (vl) @@ -336,9 +331,6 @@ Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), | eval_static_operation_case49: forall n1, eval_static_operation_cases (Ocast16unsigned) (I n1 :: nil) - | eval_static_operation_case50: - forall n1, - eval_static_operation_cases (Ointuoffloat) (F n1 :: nil) | eval_static_operation_default: forall (op: operation) (vl: list approx), eval_static_operation_cases op vl. @@ -429,18 +421,14 @@ Definition eval_static_operation_match (op: operation) (vl: list approx) := eval_static_operation_case43 n1 | Ointoffloat, F n1 :: nil => eval_static_operation_case44 n1 - | Ofloatofint, I n1 :: nil => - eval_static_operation_case45 n1 - | Ofloatofintu, I n1 :: nil => - eval_static_operation_case46 n1 + | Ofloatofwords, I n1 :: I n2 :: nil => + eval_static_operation_case45 n1 n2 | Ocmp c, vl => eval_static_operation_case47 c vl | Ocast8unsigned, I n1 :: nil => eval_static_operation_case48 n1 | Ocast16unsigned, I n1 :: nil => eval_static_operation_case49 n1 - | Ointuoffloat, F n1 :: nil => - eval_static_operation_case50 n1 | op, vl => eval_static_operation_default op vl end. @@ -531,10 +519,8 @@ Definition eval_static_operation (op: operation) (vl: list approx) := F(Float.singleoffloat n1) | eval_static_operation_case44 n1 => I(Float.intoffloat n1) - | eval_static_operation_case45 n1 => - F(Float.floatofint n1) - | eval_static_operation_case46 n1 => - F(Float.floatofintu n1) + | eval_static_operation_case45 n1 n2 => + F(Float.from_words n1 n2) | eval_static_operation_case47 c vl => match eval_static_condition c vl with | None => Unknown @@ -544,8 +530,6 @@ Definition eval_static_operation (op: operation) (vl: list approx) := I(Int.zero_ext 8 n1) | eval_static_operation_case49 n1 => I(Int.zero_ext 16 n1) - | eval_static_operation_case50 n1 => - I(Float.intuoffloat n1) | eval_static_operation_default op vl => Unknown end. diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 88b70c1d..632a55df 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -41,18 +41,19 @@ Inductive mreg: Type := (** Allocatable float regs *) | F1: mreg | F2: mreg | F3: mreg | F4: mreg | F5: mreg | F6: mreg | F7: mreg | F8: mreg - | F9: mreg | F10: mreg | F14: mreg | F15: mreg + | F9: mreg | F10: mreg | F11: mreg + | F14: mreg | F15: mreg | F16: mreg | F17: mreg | F18: mreg | F19: mreg | F20: mreg | F21: mreg | F22: mreg | F23: mreg | F24: mreg | F25: mreg | F26: mreg | F27: mreg | F28: mreg | F29: mreg | F30: mreg | F31: mreg (** Integer temporaries *) - | IT1: mreg (* R11 *) | IT2: mreg (* R0 *) + | IT1: mreg (* R11 *) | IT2: mreg (* R12 *) (** Float temporaries *) - | FT1: mreg (* F11 *) | FT2: mreg (* F12 *) | FT3: mreg (* F0 *). + | FT1: mreg (* F0 *) | FT2: mreg (* F12 *) | FT3: mreg (* F13 *). Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. -Proof. decide equality. Qed. +Proof. decide equality. Defined. Definition mreg_type (r: mreg): typ := match r with @@ -65,7 +66,8 @@ Definition mreg_type (r: mreg): typ := | R29 => Tint | R30 => Tint | R31 => Tint | F1 => Tfloat | F2 => Tfloat | F3 => Tfloat | F4 => Tfloat | F5 => Tfloat | F6 => Tfloat | F7 => Tfloat | F8 => Tfloat - | F9 => Tfloat | F10 => Tfloat | F14 => Tfloat | F15 => Tfloat + | F9 => Tfloat | F10 => Tfloat | F11 => Tfloat + | F14 => Tfloat | F15 => Tfloat | F16 => Tfloat | F17 => Tfloat | F18 => Tfloat | F19 => Tfloat | F20 => Tfloat | F21 => Tfloat | F22 => Tfloat | F23 => Tfloat | F24 => Tfloat | F25 => Tfloat | F26 => Tfloat | F27 => Tfloat @@ -90,13 +92,14 @@ Module IndexedMreg <: INDEXED_TYPE. | R29 => 24 | R30 => 25 | R31 => 26 | F1 => 28 | F2 => 29 | F3 => 30 | F4 => 31 | F5 => 32 | F6 => 33 | F7 => 34 | F8 => 35 - | F9 => 36 | F10 => 37 | F14 => 38 | F15 => 39 - | F16 => 40 | F17 => 41 | F18 => 42 | F19 => 43 - | F20 => 44 | F21 => 45 | F22 => 46 | F23 => 47 - | F24 => 48 | F25 => 49 | F26 => 50 | F27 => 51 - | F28 => 52 | F29 => 53 | F30 => 54 | F31 => 55 - | IT1 => 56 | IT2 => 57 - | FT1 => 58 | FT2 => 59 | FT3 => 60 + | F9 => 36 | F10 => 37 | F11 => 38 + | F14 => 39 | F15 => 40 + | F16 => 41 | F17 => 42 | F18 => 43 | F19 => 44 + | F20 => 45 | F21 => 46 | F22 => 47 | F23 => 48 + | F24 => 49 | F25 => 50 | F26 => 51 | F27 => 52 + | F28 => 53 | F29 => 54 | F30 => 55 | F31 => 56 + | IT1 => 57 | IT2 => 58 + | FT1 => 59 | FT2 => 60 | FT3 => 61 end. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml index 87800be1..713e14d1 100644 --- a/powerpc/Machregsaux.ml +++ b/powerpc/Machregsaux.ml @@ -24,13 +24,14 @@ let register_names = [ ("R29", R29); ("R30", R30); ("R31", R31); ("F1", F1); ("F2", F2); ("F3", F3); ("F4", F4); ("F5", F5); ("F6", F6); ("F7", F7); ("F8", F8); - ("F9", F9); ("F10", F10); ("F14", F14); ("F15", F15); + ("F9", F9); ("F10", F10); ("F11", F11); + ("F14", F14); ("F15", F15); ("F16", F16); ("F17", F17); ("F18", F18); ("F19", F19); ("F20", F20); ("F21", F21); ("F22", F22); ("F23", F23); ("F24", F24); ("F25", F25); ("F26", F26); ("F27", F27); ("F28", F28); ("F29", F29); ("F30", F30); ("F31", F31); - ("R11", IT1); ("R0", IT2); - ("F11", FT1); ("F12", FT2); ("F0", FT3) + ("R11", IT1); ("R12", IT2); + ("F0", FT1); ("F12", FT2); ("F13", FT3) ] let name_of_register r = diff --git a/powerpc/Op.v b/powerpc/Op.v index 7a9aa500..902fc025 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -96,9 +96,7 @@ Inductive operation : Type := | Osingleoffloat: operation (**r [rd] is [r1] truncated to single-precision float *) (*c Conversions between int and float: *) | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *) - | Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] *) - | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] *) - | Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] *) + | Ofloatofwords: operation (**r [rd = float_of_words(r1,r2)] *) (*c Boolean tests: *) | Ocmp: condition -> operation. (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) @@ -250,12 +248,8 @@ Definition eval_operation Some (Val.singleoffloat v1) | Ointoffloat, Vfloat f1 :: nil => Some (Vint (Float.intoffloat f1)) - | Ointuoffloat, Vfloat f1 :: nil => - Some (Vint (Float.intuoffloat f1)) - | Ofloatofint, Vint n1 :: nil => - Some (Vfloat (Float.floatofint n1)) - | Ofloatofintu, Vint n1 :: nil => - Some (Vfloat (Float.floatofintu n1)) + | Ofloatofwords, Vint i1 :: Vint i2 :: nil => + Some (Vfloat (Float.from_words i1 i2)) | Ocmp c, _ => match eval_condition c vl with | None => None @@ -466,9 +460,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Omulsubf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat) | Osingleoffloat => (Tfloat :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) - | Ointuoffloat => (Tfloat :: nil, Tint) - | Ofloatofint => (Tint :: nil, Tfloat) - | Ofloatofintu => (Tint :: nil, Tfloat) + | Ofloatofwords => (Tint :: Tint :: nil, Tfloat) | Ocmp c => (type_of_condition c, Tint) end. @@ -615,9 +607,7 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val : | Omulsubf, v1::v2::v3::nil => Val.subf (Val.mulf v1 v2) v3 | Osingleoffloat, v1::nil => Val.singleoffloat v1 | Ointoffloat, v1::nil => Val.intoffloat v1 - | Ointuoffloat, v1::nil => Val.intuoffloat v1 - | Ofloatofint, v1::nil => Val.floatofint v1 - | Ofloatofintu, v1::nil => Val.floatofintu v1 + | Ofloatofwords, v1::v2::nil => Val.floatofwords v1 v2 | Ocmp c, _ => eval_condition_total c vl | _, _ => Vundef end. @@ -840,3 +830,73 @@ Lemma type_op_for_binary_addressing: Proof. intros. destruct addr; simpl in H; reflexivity || omegaContradiction. Qed. + +(** Two-address operations. There are none in the PowerPC architecture. *) + +Definition two_address_op (op: operation) : bool := false. + +(** Operations that are so cheap to recompute that CSE should not factor them out. *) + +Definition is_trivial_op (op: operation) : bool := + match op with + | Omove => true + | Ointconst _ => true + | Oaddrsymbol _ _ => true + | Oaddrstack _ => true + | _ => false + end. + +(** Shifting stack-relative references. This is used in [Stacking]. *) + +Definition shift_stack_addressing (delta: int) (addr: addressing) := + match addr with + | Ainstack ofs => Ainstack (Int.add delta ofs) + | _ => addr + end. + +Definition shift_stack_operation (delta: int) (op: operation) := + match op with + | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) + | _ => op + end. + +Lemma shift_stack_eval_addressing: + forall (F V: Type) (ge: Genv.t F V) sp addr args delta, + eval_addressing ge (Val.sub sp (Vint delta)) (shift_stack_addressing delta addr) args = + eval_addressing ge sp addr args. +Proof. + intros. destruct addr; simpl; auto. + destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. + decEq. decEq. rewrite <- Int.add_assoc. decEq. + rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. + rewrite Int.sub_idem. apply Int.add_zero. +Qed. + +Lemma shift_stack_eval_operation: + forall (F V: Type) (ge: Genv.t F V) sp op args delta, + eval_operation ge (Val.sub sp (Vint delta)) (shift_stack_operation delta op) args = + eval_operation ge sp op args. +Proof. + intros. destruct op; simpl; auto. + destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. + decEq. decEq. rewrite <- Int.add_assoc. decEq. + rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. + rewrite Int.sub_idem. apply Int.add_zero. +Qed. + +Lemma type_shift_stack_addressing: + forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr. +Proof. + intros. destruct addr; auto. +Qed. + +Lemma type_shift_stack_operation: + forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. +Proof. + intros. destruct op; auto. +Qed. + + + diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 9df9cc0a..ef50795a 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -263,14 +263,15 @@ let rec log2 n = (* Built-ins. They come in two flavors: - inlined by the compiler: take their arguments in arbitrary - registers; preserve all registers except GPR12 and FPR13 + registers; preserve all registers except the temporaries + (GPR0, GPR11, GPR12, FPR0, FPR12, FPR13); - inlined while printing asm code; take their arguments in locations dictated by the calling conventions; preserve callee-save regs only. *) let print_builtin_inlined oc name args res = fprintf oc "%s begin builtin %s\n" comment name; - (* Can use as temporaries: GPR12, FPR13 *) + (* Can use as temporaries: GPR0, GPR11, GPR12, FPR0, FPR12, FPR13 *) begin match name, args, res with (* Volatile reads *) | "__builtin_volatile_read_int8unsigned", [IR addr], IR res -> @@ -524,32 +525,18 @@ let print_instruction oc labels = function fprintf oc " lwz %a, 4(%a)\n" ireg r1 ireg GPR1; fprintf oc " addi %a, %a, 8\n" ireg GPR1 ireg GPR1; fprintf oc "%s end pseudoinstr fcti\n" comment - | Pfctiu(r1, r2) -> - let lbl1 = new_label() in - let lbl2 = new_label() in - let lbl3 = new_label() in - fprintf oc "%s begin pseudoinstr %a = fctiu(%a)\n" comment ireg r1 freg r2; - fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl1; - fprintf oc " lfd %a, %a(%a)\n" freg FPR13 label_low lbl1 ireg GPR12; - fprintf oc " fcmpu %a, %a, %a\n" creg 7 freg r2 freg FPR13; - fprintf oc " cror 30, 29, 30\n"; - fprintf oc " beq %a, %a\n" creg 7 label lbl2; - fprintf oc " fctiwz %a, %a\n" freg FPR13 freg r2; - fprintf oc " stfdu %a, -8(%a)\n" freg FPR13 ireg GPR1; - fprintf oc " lwz %a, 4(%a)\n" ireg r1 ireg GPR1; - fprintf oc " b %a\n" label lbl3; - fprintf oc "%a: fsub %a, %a, %a\n" label lbl2 freg FPR13 freg r2 freg FPR13; - fprintf oc " fctiwz %a, %a\n" freg FPR13 freg FPR13; - fprintf oc " stfdu %a, -8(%a)\n" freg FPR13 ireg GPR1; - fprintf oc " lwz %a, 4(%a)\n" ireg r1 ireg GPR1; - fprintf oc " addis %a, %a, 0x8000\n" ireg r1 ireg r1; - fprintf oc "%a: addi %a, %a, 8\n" label lbl3 ireg GPR1 ireg GPR1; - float_literals := (lbl1, 0x41e0_0000_0000_0000L) :: !float_literals; - fprintf oc "%s end pseudoinstr fctiu\n" comment | Pfdiv(r1, r2, r3) -> fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfmadd(r1, r2, r3, r4) -> fprintf oc " fmadd %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pfmake(rd, r1, r2) -> + fprintf oc "%s begin pseudoinstr %a = fmake(%a, %a)\n" + comment freg rd ireg r1 ireg r2; + fprintf oc " stwu %a, -8(%a)\n" ireg r1 ireg GPR1; + fprintf oc " stw %a, 4(%a)\n" ireg r2 ireg GPR1; + fprintf oc " lfd %a, 0(%a)\n" freg rd ireg GPR1; + fprintf oc " addi %a, %a, 8\n" ireg GPR1 ireg GPR1; + fprintf oc "%s end pseudoinstr fmake\n" comment | Pfmr(r1, r2) -> fprintf oc " fmr %a, %a\n" freg r1 freg r2 | Pfmsub(r1, r2, r3, r4) -> @@ -562,33 +549,6 @@ let print_instruction oc labels = function fprintf oc " frsp %a, %a\n" freg r1 freg r2 | Pfsub(r1, r2, r3) -> fprintf oc " fsub %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pictf(r1, r2) -> - let lbl = new_label() in - fprintf oc "%s begin pseudoinstr %a = ictf(%a)\n" comment freg r1 ireg r2; - fprintf oc " addis %a, 0, 0x4330\n" ireg GPR12; - fprintf oc " stwu %a, -8(%a)\n" ireg GPR12 ireg GPR1; - fprintf oc " addis %a, %a, 0x8000\n" ireg GPR12 ireg r2; - fprintf oc " stw %a, 4(%a)\n" ireg GPR12 ireg GPR1; - fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " lfd %a, %a(%a)\n" freg FPR13 label_low lbl ireg GPR12; - fprintf oc " lfd %a, 0(%a)\n" freg r1 ireg GPR1; - fprintf oc " addi %a, %a, 8\n" ireg GPR1 ireg GPR1; - fprintf oc " fsub %a, %a, %a\n" freg r1 freg r1 freg FPR13; - float_literals := (lbl, 0x4330_0000_8000_0000L) :: !float_literals; - fprintf oc "%s end pseudoinstr ictf\n" comment - | Piuctf(r1, r2) -> - let lbl = new_label() in - fprintf oc "%s begin pseudoinstr %a = iuctf(%a)\n" comment freg r1 ireg r2; - fprintf oc " addis %a, 0, 0x4330\n" ireg GPR12; - fprintf oc " stwu %a, -8(%a)\n" ireg GPR12 ireg GPR1; - fprintf oc " stw %a, 4(%a)\n" ireg r2 ireg GPR1; - fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " lfd %a, %a(%a)\n" freg FPR13 label_low lbl ireg GPR12; - fprintf oc " lfd %a, 0(%a)\n" freg r1 ireg GPR1; - fprintf oc " addi %a, %a, 8\n" ireg GPR1 ireg GPR1; - fprintf oc " fsub %a, %a, %a\n" freg r1 freg r1 freg FPR13; - float_literals := (lbl, 0x4330_0000_0000_0000L) :: !float_literals; - fprintf oc "%s end pseudoinstr ictf\n" comment | Plbz(r1, c, r2) -> fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2 | Plbzx(r1, r2, r3) -> diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index 31de8d1a..4eb95bf3 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -92,9 +92,7 @@ let print_operation reg pp = function | Omulsubf, [r1;r2;r3] -> fprintf pp "%a *f %a -f %a" reg r1 reg r2 reg r3 | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 - | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1 - | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 - | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1 + | Ofloatofwords, [r1;r2] -> fprintf pp "floatofwords(%a,%a)" reg r1 reg r2 | Ocmp c, args -> print_condition reg pp (c, args) | _ -> fprintf pp "" @@ -105,5 +103,3 @@ let print_addressing reg pp = function | Abased(id, ofs), [r1] -> fprintf pp "%s + %ld + %a" (extern_atom id) (camlint_of_coqint ofs) reg r1 | Ainstack ofs, [] -> fprintf pp "stack(%ld)" (camlint_of_coqint ofs) | _ -> fprintf pp "" - - diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v index e6a281b2..c421cdc5 100644 --- a/powerpc/SelectOp.v +++ b/powerpc/SelectOp.v @@ -50,6 +50,14 @@ Require Import CminorSel. Open Local Scope cminorsel_scope. +(** ** Constants **) + +Definition addrsymbol (id: ident) (ofs: int) := + Eop (Oaddrsymbol id ofs) Enil. + +Definition addrstack (ofs: int) := + Eop (Oaddrstack ofs) Enil. + (** ** Integer logical negation *) (** The natural way to write smart constructors is by pattern-matching @@ -846,148 +854,6 @@ Definition subf (e1: expr) (e2: expr) := end else Eop Osubf (e1:::e2:::Enil). -(** ** Truncations and sign extensions *) - -Inductive cast8signed_cases: forall (e1: expr), Type := - | cast8signed_case1: - forall (e2: expr), - cast8signed_cases (Eop Ocast8signed (e2 ::: Enil)) - | cast8signed_case2: - forall mode args, - cast8signed_cases (Eload Mint8signed mode args) - | cast8signed_default: - forall (e1: expr), - cast8signed_cases e1. - -Definition cast8signed_match (e1: expr) := - match e1 as z1 return cast8signed_cases z1 with - | Eop Ocast8signed (e2 ::: Enil) => - cast8signed_case1 e2 - | Eload Mint8signed mode args => - cast8signed_case2 mode args - | e1 => - cast8signed_default e1 - end. - -Definition cast8signed (e: expr) := - match cast8signed_match e with - | cast8signed_case1 e1 => e - | cast8signed_case2 mode args => e - | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil) - end. - -Inductive cast8unsigned_cases: forall (e1: expr), Type := - | cast8unsigned_case1: - forall (e2: expr), - cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil)) - | cast8unsigned_case2: - forall mode args, - cast8unsigned_cases (Eload Mint8unsigned mode args) - | cast8unsigned_default: - forall (e1: expr), - cast8unsigned_cases e1. - -Definition cast8unsigned_match (e1: expr) := - match e1 as z1 return cast8unsigned_cases z1 with - | Eop Ocast8unsigned (e2 ::: Enil) => - cast8unsigned_case1 e2 - | Eload Mint8unsigned mode args => - cast8unsigned_case2 mode args - | e1 => - cast8unsigned_default e1 - end. - -Definition cast8unsigned (e: expr) := - match cast8unsigned_match e with - | cast8unsigned_case1 e1 => e - | cast8unsigned_case2 mode args => e - | cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil) - end. - -Inductive cast16signed_cases: forall (e1: expr), Type := - | cast16signed_case1: - forall (e2: expr), - cast16signed_cases (Eop Ocast16signed (e2 ::: Enil)) - | cast16signed_case2: - forall mode args, - cast16signed_cases (Eload Mint16signed mode args) - | cast16signed_default: - forall (e1: expr), - cast16signed_cases e1. - -Definition cast16signed_match (e1: expr) := - match e1 as z1 return cast16signed_cases z1 with - | Eop Ocast16signed (e2 ::: Enil) => - cast16signed_case1 e2 - | Eload Mint16signed mode args => - cast16signed_case2 mode args - | e1 => - cast16signed_default e1 - end. - -Definition cast16signed (e: expr) := - match cast16signed_match e with - | cast16signed_case1 e1 => e - | cast16signed_case2 mode args => e - | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil) - end. - -Inductive cast16unsigned_cases: forall (e1: expr), Type := - | cast16unsigned_case1: - forall (e2: expr), - cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil)) - | cast16unsigned_case2: - forall mode args, - cast16unsigned_cases (Eload Mint16unsigned mode args) - | cast16unsigned_default: - forall (e1: expr), - cast16unsigned_cases e1. - -Definition cast16unsigned_match (e1: expr) := - match e1 as z1 return cast16unsigned_cases z1 with - | Eop Ocast16unsigned (e2 ::: Enil) => - cast16unsigned_case1 e2 - | Eload Mint16unsigned mode args => - cast16unsigned_case2 mode args - | e1 => - cast16unsigned_default e1 - end. - -Definition cast16unsigned (e: expr) := - match cast16unsigned_match e with - | cast16unsigned_case1 e1 => e - | cast16unsigned_case2 mode args => e - | cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil) - end. - -Inductive singleoffloat_cases: forall (e1: expr), Type := - | singleoffloat_case1: - forall (e2: expr), - singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil)) - | singleoffloat_case2: - forall mode args, - singleoffloat_cases (Eload Mfloat32 mode args) - | singleoffloat_default: - forall (e1: expr), - singleoffloat_cases e1. - -Definition singleoffloat_match (e1: expr) := - match e1 as z1 return singleoffloat_cases z1 with - | Eop Osingleoffloat (e2 ::: Enil) => - singleoffloat_case1 e2 - | Eload Mfloat32 mode args => - singleoffloat_case2 mode args - | e1 => - singleoffloat_default e1 - end. - -Definition singleoffloat (e: expr) := - match singleoffloat_match e with - | singleoffloat_case1 e1 => e - | singleoffloat_case2 mode args => e - | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil) - end. - (** ** Comparisons *) Inductive comp_cases: forall (e1: expr) (e2: expr), Type := @@ -1034,15 +900,36 @@ Definition compu (c: comparison) (e1: expr) (e2: expr) := Definition compf (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). +(** ** Floating-point conversions *) + +Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). + +Definition intuoffloat (e: expr) := + let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in + Elet e + (Econdition (CEcond (Ccompf Clt) (Eletvar O ::: f ::: Enil)) + (intoffloat (Eletvar O)) + (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar O) f)))). + +Definition floatofintu (e: expr) := + subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) + (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil). + +Definition floatofint (e: expr) := + subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil + ::: addimm Float.ox8000_0000 e ::: Enil)) + (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil). + (** ** Other operators, not optimized. *) +Definition cast8unsigned (e: expr) := Eop Ocast8unsigned (e ::: Enil). +Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil). +Definition cast16unsigned (e: expr) := Eop Ocast16unsigned (e ::: Enil). +Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil). +Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). 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). diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 2fc13273..8a06433f 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -100,6 +100,24 @@ Ltac InvEval := InvEval1; InvEval2; InvEval2. by the smart constructor. *) +Theorem eval_addrsymbol: + forall le id ofs b, + Genv.find_symbol ge id = Some b -> + eval_expr ge sp e m le (addrsymbol id ofs) (Vptr b ofs). +Proof. + intros. unfold addrsymbol. econstructor. constructor. + simpl. rewrite H. auto. +Qed. + +Theorem eval_addrstack: + forall le ofs b n, + sp = Vptr b n -> + eval_expr ge sp e m le (addrstack ofs) (Vptr b (Int.add n ofs)). +Proof. + intros. unfold addrstack. econstructor. constructor. + simpl. unfold offset_sp. rewrite H. auto. +Qed. + Theorem eval_notint: forall le a x, eval_expr ge sp e m le a (Vint x) -> @@ -667,80 +685,35 @@ Proof. intros. EvalOp. Qed. -Lemma loadv_cast: - forall chunk addr v, - Mem.loadv chunk m addr = Some v -> - match chunk with - | Mint8signed => v = Val.sign_ext 8 v - | Mint8unsigned => v = Val.zero_ext 8 v - | Mint16signed => v = Val.sign_ext 16 v - | Mint16unsigned => v = Val.zero_ext 16 v - | Mfloat32 => v = Val.singleoffloat v - | _ => True - end. -Proof. - intros. destruct addr; simpl in H; try discriminate. - eapply Mem.load_cast. eauto. -Qed. - Theorem eval_cast8signed: forall le a v, eval_expr ge sp e m le a v -> eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v). -Proof. - intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.sign_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). - EvalOp. -Qed. +Proof. TrivialOp cast8signed. Qed. Theorem eval_cast8unsigned: forall le a v, eval_expr ge sp e m le a v -> eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v). -Proof. - intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.zero_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). - EvalOp. -Qed. +Proof. TrivialOp cast8unsigned. Qed. Theorem eval_cast16signed: forall le a v, eval_expr ge sp e m le a v -> eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v). -Proof. - intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.sign_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). - EvalOp. -Qed. +Proof. TrivialOp cast16signed. Qed. Theorem eval_cast16unsigned: forall le a v, eval_expr ge sp e m le a v -> eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v). -Proof. - intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.zero_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). - EvalOp. -Qed. +Proof. TrivialOp cast16unsigned. Qed. Theorem eval_singleoffloat: forall le a v, eval_expr ge sp e m le a v -> eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v). -Proof. - intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. - inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). - EvalOp. -Qed. +Proof. TrivialOp singleoffloat. Qed. Theorem eval_comp_int: forall le c a x b y, @@ -883,19 +856,46 @@ 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. +Proof. + intros. unfold intuoffloat. + econstructor. eauto. + set (fm := Float.floatofintu Float.ox8000_0000). + assert (eval_expr ge sp e m (Vfloat x :: le) (Eletvar O) (Vfloat x)). constructor. auto. + apply eval_Econdition with (v1 := Float.cmp Clt x fm). + econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. + simpl. auto. + caseEq (Float.cmp Clt x fm); intros. + rewrite Float.intuoffloat_intoffloat_1; auto. + EvalOp. + rewrite Float.intuoffloat_intoffloat_2; auto. + apply eval_addimm. apply eval_intoffloat. apply eval_subf; auto. EvalOp. +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. +Proof. + intros. unfold floatofint. rewrite Float.floatofint_from_words. + apply eval_subf. + EvalOp. constructor. EvalOp. simpl; eauto. + constructor. apply eval_addimm. eauto. constructor. + simpl. auto. + EvalOp. +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. +Proof. + intros. unfold floatofintu. rewrite Float.floatofintu_from_words. + apply eval_subf. + EvalOp. constructor. EvalOp. simpl; eauto. + constructor. eauto. constructor. + simpl. auto. + EvalOp. +Qed. Theorem eval_xor: forall le a x b y, diff --git a/powerpc/eabi/Conventions1.v b/powerpc/eabi/Conventions1.v index 60eaaa5e..b25f2a5d 100644 --- a/powerpc/eabi/Conventions1.v +++ b/powerpc/eabi/Conventions1.v @@ -35,7 +35,7 @@ Definition int_caller_save_regs := R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: nil. Definition float_caller_save_regs := - F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: nil. + F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: F11 :: nil. Definition int_callee_save_regs := R31 :: R30 :: R29 :: R28 :: R27 :: R26 :: R25 :: R24 :: R23 :: @@ -58,6 +58,9 @@ Definition float_temporaries := FT1 :: FT2 :: FT3 :: nil. Definition temporaries := R IT1 :: R IT2 :: R FT1 :: R FT2 :: R FT3 :: nil. +Definition dummy_int_reg := R3. (**r Used in [Coloring]. *) +Definition dummy_float_reg := F1. (**r Used in [Coloring]. *) + (** The [index_int_callee_save] and [index_float_callee_save] associate a unique positive integer to callee-save registers. This integer is used in [Stacking] to determine where to save these registers in diff --git a/powerpc/macosx/Conventions1.v b/powerpc/macosx/Conventions1.v index a5741e1c..2a0f2336 100644 --- a/powerpc/macosx/Conventions1.v +++ b/powerpc/macosx/Conventions1.v @@ -35,7 +35,7 @@ Definition int_caller_save_regs := R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: nil. Definition float_caller_save_regs := - F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: nil. + F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: F11 :: nil. Definition int_callee_save_regs := R14 :: R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 :: @@ -58,6 +58,9 @@ Definition float_temporaries := FT1 :: FT2 :: FT3 :: nil. Definition temporaries := R IT1 :: R IT2 :: R FT1 :: R FT2 :: R FT3 :: nil. +Definition dummy_int_reg := R3. (**r Used in [Coloring]. *) +Definition dummy_float_reg := F1. (**r Used in [Coloring]. *) + (** The [index_int_callee_save] and [index_float_callee_save] associate a unique positive integer to callee-save registers. This integer is used in [Stacking] to determine where to save these registers in @@ -291,7 +294,7 @@ Qed. (** The PowerPC ABI states the following convention for passing arguments to a function: - The first 8 integer arguments are passed in registers [R3] to [R10]. -- The first 10 float arguments are passed in registers [F1] to [F10]. +- The first 11 float arguments are passed in registers [F1] to [F11]. - Each float argument passed in a float register ``consumes'' two integer arguments. - Extra arguments are passed on the stack, in [Outgoing] slots, consecutively @@ -327,7 +330,7 @@ Fixpoint loc_arguments_rec Definition int_param_regs := R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: nil. Definition float_param_regs := - F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: nil. + F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: F11 :: nil. (** [loc_arguments s] returns the list of locations where to store arguments when calling a function with signature [s]. *) @@ -589,4 +592,3 @@ Proof. intro; simpl. ElimOrEq; reflexivity. intro; simpl. ElimOrEq; reflexivity. Qed. - -- cgit