From 5020a5a07da3fd690f5d171a48d0c73ef48f9430 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 1 Mar 2013 15:32:13 +0000 Subject: Revised Stacking and Asmgen passes and Mach semantics: - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asm.v | 263 ++++---- powerpc/Asmgen.v | 503 ++++++++------ powerpc/Asmgenproof.v | 1723 +++++++++++++++++------------------------------ powerpc/Asmgenproof1.v | 1424 ++++++++++++++------------------------- powerpc/Asmgenretaddr.v | 204 ------ powerpc/PrintAsm.ml | 3 +- 6 files changed, 1554 insertions(+), 2566 deletions(-) delete mode 100644 powerpc/Asmgenretaddr.v (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 5d815fda..27e801a7 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -84,6 +84,11 @@ End PregEq. Module Pregmap := EMap(PregEq). +(** Conventional names for stack pointer ([SP]) and return address ([RA]) *) + +Notation "'SP'" := GPR1 (only parsing). +Notation "'RA'" := LR (only parsing). + (** Symbolic constants. Immediate operands to an arithmetic instruction or an indexed memory access can be either integer literals, or the low or high 16 bits of a symbolic reference (the address @@ -291,7 +296,9 @@ lbl: .long table[0], table[1], ... *) Definition code := list instruction. -Definition fundef := AST.fundef code. +Definition function := code. +Definition fn_code (f: function) : code := f. +Definition fundef := AST.fundef function. Definition program := AST.program fundef unit. (** * Operational semantics *) @@ -309,6 +316,14 @@ Definition genv := Genv.t fundef unit. Notation "a # b" := (a b) (at level 1, only parsing). Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level). +(** Undefining some registers *) + +Fixpoint undef_regs (l: list preg) (rs: regset) : regset := + match l with + | nil => rs + | r :: l' => undef_regs l' (rs#r <- Vundef) + end. + Section RELSEM. (** Looking up instructions in a code sequence by position. *) @@ -428,8 +443,8 @@ Definition const_high (c: constant) := or [Error] if the processor is stuck. *) Inductive outcome: Type := - | OK: regset -> mem -> outcome - | Error: outcome. + | Next: regset -> mem -> outcome + | Stuck: outcome. (** Manipulations over the [PC] register: continuing with the next instruction ([nextinstr]) or branching to a label ([goto_label]). *) @@ -439,11 +454,11 @@ Definition nextinstr (rs: regset) := Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) := match label_pos lbl 0 c with - | None => Error + | None => Stuck | Some pos => match rs#PC with - | Vptr b ofs => OK (rs#PC <- (Vptr b (Int.repr pos))) m - | _ => Error + | Vptr b ofs => Next (rs#PC <- (Vptr b (Int.repr pos))) m + | _ => Stuck end end. @@ -453,29 +468,29 @@ Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) := Definition load1 (chunk: memory_chunk) (rd: preg) (cst: constant) (r1: ireg) (rs: regset) (m: mem) := match Mem.loadv chunk m (Val.add (gpr_or_zero rs r1) (const_low cst)) with - | None => Error - | Some v => OK (nextinstr (rs#rd <- v)) m + | None => Stuck + | Some v => Next (nextinstr (rs#rd <- v)) m end. Definition load2 (chunk: memory_chunk) (rd: preg) (r1 r2: ireg) (rs: regset) (m: mem) := match Mem.loadv chunk m (Val.add rs#r1 rs#r2) with - | None => Error - | Some v => OK (nextinstr (rs#rd <- v)) m + | None => Stuck + | Some v => Next (nextinstr (rs#rd <- v)) m end. Definition store1 (chunk: memory_chunk) (r: preg) (cst: constant) (r1: ireg) (rs: regset) (m: mem) := match Mem.storev chunk m (Val.add (gpr_or_zero rs r1) (const_low cst)) (rs#r) with - | None => Error - | Some m' => OK (nextinstr rs) m' + | None => Stuck + | Some m' => Next (nextinstr rs) m' end. Definition store2 (chunk: memory_chunk) (r: preg) (r1 r2: ireg) (rs: regset) (m: mem) := match Mem.storev chunk m (Val.add rs#r1 rs#r2) (rs#r) with - | None => Error - | Some m' => OK (nextinstr rs) m' + | None => Stuck + | Some m' => Next (nextinstr rs) m' end. (** Operations over condition bits. *) @@ -521,127 +536,124 @@ Definition compare_float (rs: regset) (v1 v2: val) := Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome := match i with | Padd rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m | Padde rd r1 r2 => - OK (nextinstr (rs #rd <- (Val.add (Val.add rs#r1 rs#r2) rs#CARRY) + Next (nextinstr (rs #rd <- (Val.add (Val.add rs#r1 rs#r2) rs#CARRY) #CARRY <- (Val.add_carry rs#r1 rs#r2 rs#CARRY))) m | Paddi rd r1 cst => - OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)))) m + Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)))) m | Paddic rd r1 cst => - OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)) + Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)) #CARRY <- (Val.add_carry (gpr_or_zero rs r1) (const_low cst) Vzero))) m | Paddis rd r1 cst => - OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m + Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m | Paddze rd r1 => - OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY) + Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY) #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m | Pallocframe sz ofs => let (m1, stk) := Mem.alloc m 0 sz in let sp := Vptr stk Int.zero in match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with - | None => Error - | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)) m2 + | None => Stuck + | Some m2 => Next (nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)) m2 end | Pand_ rd r1 r2 => let v := Val.and rs#r1 rs#r2 in - OK (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m + Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m | Pandc rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.and rs#r1 (Val.notint rs#r2)))) m + Next (nextinstr (rs#rd <- (Val.and rs#r1 (Val.notint rs#r2)))) m | Pandi_ rd r1 cst => let v := Val.and rs#r1 (const_low cst) in - OK (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m + Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m | Pandis_ rd r1 cst => let v := Val.and rs#r1 (const_high cst) in - OK (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m + Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m | Pb lbl => goto_label c lbl rs m | Pbctr => - OK (rs#PC <- (rs#CTR)) m + Next (rs#PC <- (rs#CTR)) m | Pbctrl => - OK (rs#LR <- (Val.add rs#PC Vone) #PC <- (rs#CTR)) m + Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (rs#CTR)) m | Pbf bit lbl => match rs#(reg_of_crbit bit) with - | Vint n => if Int.eq n Int.zero then goto_label c lbl rs m else OK (nextinstr rs) m - | _ => Error + | Vint n => if Int.eq n Int.zero then goto_label c lbl rs m else Next (nextinstr rs) m + | _ => Stuck end | Pbl ident => - OK (rs#LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset ident Int.zero)) m + Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset ident Int.zero)) m | Pbs ident => - OK (rs#PC <- (symbol_offset ident Int.zero)) m + Next (rs#PC <- (symbol_offset ident Int.zero)) m | Pblr => - OK (rs#PC <- (rs#LR)) m + Next (rs#PC <- (rs#LR)) m | Pbt bit lbl => match rs#(reg_of_crbit bit) with - | Vint n => if Int.eq n Int.zero then OK (nextinstr rs) m else goto_label c lbl rs m - | _ => Error + | Vint n => if Int.eq n Int.zero then Next (nextinstr rs) m else goto_label c lbl rs m + | _ => Stuck end | Pbtbl r tbl => - match gpr_or_zero rs r with + match rs r with | Vint n => - let pos := Int.unsigned n in - if zeq (Zmod pos 4) 0 then - match list_nth_z tbl (pos / 4) with - | None => Error - | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m - end - else Error - | _ => Error + match list_nth_z tbl (Int.unsigned n) with + | None => Stuck + | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m + end + | _ => Stuck end | Pcmplw r1 r2 => - OK (nextinstr (compare_uint rs m rs#r1 rs#r2)) m + Next (nextinstr (compare_uint rs m rs#r1 rs#r2)) m | Pcmplwi r1 cst => - OK (nextinstr (compare_uint rs m rs#r1 (const_low cst))) m + Next (nextinstr (compare_uint rs m rs#r1 (const_low cst))) m | Pcmpw r1 r2 => - OK (nextinstr (compare_sint rs rs#r1 rs#r2)) m + Next (nextinstr (compare_sint rs rs#r1 rs#r2)) m | Pcmpwi r1 cst => - OK (nextinstr (compare_sint rs rs#r1 (const_low cst))) m + Next (nextinstr (compare_sint rs rs#r1 (const_low cst))) m | Pcror bd b1 b2 => - OK (nextinstr (rs#(reg_of_crbit bd) <- (Val.or rs#(reg_of_crbit b1) rs#(reg_of_crbit b2)))) m + Next (nextinstr (rs#(reg_of_crbit bd) <- (Val.or rs#(reg_of_crbit b1) rs#(reg_of_crbit b2)))) m | Pdivw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.maketotal (Val.divs rs#r1 rs#r2)))) m + Next (nextinstr (rs#rd <- (Val.maketotal (Val.divs rs#r1 rs#r2)))) m | Pdivwu rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.maketotal (Val.divu rs#r1 rs#r2)))) m + Next (nextinstr (rs#rd <- (Val.maketotal (Val.divu rs#r1 rs#r2)))) m | Peqv rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.notint (Val.xor rs#r1 rs#r2)))) m + Next (nextinstr (rs#rd <- (Val.notint (Val.xor rs#r1 rs#r2)))) m | Pextsb rd r1 => - OK (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m + Next (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m | Pextsh rd r1 => - OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m + Next (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m | Pfreeframe sz ofs => match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with - | None => Error + | None => Stuck | Some v => match rs#GPR1 with | Vptr stk ofs => match Mem.free m stk 0 sz with - | None => Error - | Some m' => OK (nextinstr (rs#GPR1 <- v)) m' + | None => Stuck + | Some m' => Next (nextinstr (rs#GPR1 <- v)) m' end - | _ => Error + | _ => Stuck end end | Pfabs rd r1 => - OK (nextinstr (rs#rd <- (Val.absf rs#r1))) m + Next (nextinstr (rs#rd <- (Val.absf rs#r1))) m | Pfadd rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m | Pfcmpu r1 r2 => - OK (nextinstr (compare_float rs rs#r1 rs#r2)) m + Next (nextinstr (compare_float rs rs#r1 rs#r2)) m | Pfcti rd r1 => - OK (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m + Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m | Pfdiv rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m | Pfmake rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m | Pfmr rd r1 => - OK (nextinstr (rs#rd <- (rs#r1))) m + Next (nextinstr (rs#rd <- (rs#r1))) m | Pfmul rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m | Pfneg rd r1 => - OK (nextinstr (rs#rd <- (Val.negf rs#r1))) m + Next (nextinstr (rs#rd <- (Val.negf rs#r1))) m | Pfrsp rd r1 => - OK (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m + Next (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m | Pfsub rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m | Plbz rd cst r1 => load1 Mint8unsigned rd cst r1 rs m | Plbzx rd r1 r2 => @@ -663,50 +675,50 @@ 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 #GPR12 <- Vundef #rd <- (Vfloat f))) m + Next (nextinstr (rs #GPR12 <- Vundef #rd <- (Vfloat f))) m | Plwz rd cst r1 => load1 Mint32 rd cst r1 rs m | Plwzx rd r1 r2 => load2 Mint32 rd r1 r2 rs m | Pmfcrbit rd bit => - OK (nextinstr (rs#rd <- (rs#(reg_of_crbit bit)))) m + Next (nextinstr (rs#rd <- (rs#(reg_of_crbit bit)))) m | Pmflr rd => - OK (nextinstr (rs#rd <- (rs#LR))) m + Next (nextinstr (rs#rd <- (rs#LR))) m | Pmr rd r1 => - OK (nextinstr (rs#rd <- (rs#r1))) m + Next (nextinstr (rs#rd <- (rs#r1))) m | Pmtctr r1 => - OK (nextinstr (rs#CTR <- (rs#r1))) m + Next (nextinstr (rs#CTR <- (rs#r1))) m | Pmtlr r1 => - OK (nextinstr (rs#LR <- (rs#r1))) m + Next (nextinstr (rs#LR <- (rs#r1))) m | Pmulli rd r1 cst => - OK (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m + Next (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m | Pmullw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.mul rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.mul rs#r1 rs#r2))) m | Pnand rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.notint (Val.and rs#r1 rs#r2)))) m + Next (nextinstr (rs#rd <- (Val.notint (Val.and rs#r1 rs#r2)))) m | Pnor rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.notint (Val.or rs#r1 rs#r2)))) m + Next (nextinstr (rs#rd <- (Val.notint (Val.or rs#r1 rs#r2)))) m | Por rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.or rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.or rs#r1 rs#r2))) m | Porc rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.or rs#r1 (Val.notint rs#r2)))) m + Next (nextinstr (rs#rd <- (Val.or rs#r1 (Val.notint rs#r2)))) m | Pori rd r1 cst => - OK (nextinstr (rs#rd <- (Val.or rs#r1 (const_low cst)))) m + Next (nextinstr (rs#rd <- (Val.or rs#r1 (const_low cst)))) m | Poris rd r1 cst => - OK (nextinstr (rs#rd <- (Val.or rs#r1 (const_high cst)))) m + Next (nextinstr (rs#rd <- (Val.or rs#r1 (const_high cst)))) m | Prlwinm rd r1 amount mask => - OK (nextinstr (rs#rd <- (Val.rolm rs#r1 amount mask))) m + Next (nextinstr (rs#rd <- (Val.rolm rs#r1 amount mask))) m | Prlwimi rd r1 amount mask => - OK (nextinstr (rs#rd <- (Val.or (Val.and rs#rd (Vint (Int.not mask))) + Next (nextinstr (rs#rd <- (Val.or (Val.and rs#rd (Vint (Int.not mask))) (Val.rolm rs#r1 amount mask)))) m | Pslw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m | Psraw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2) #CARRY <- (Val.shr_carry rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2) #CARRY <- (Val.shr_carry rs#r1 rs#r2))) m | Psrawi rd r1 n => - OK (nextinstr (rs#rd <- (Val.shr rs#r1 (Vint n)) #CARRY <- (Val.shr_carry rs#r1 (Vint n)))) m + Next (nextinstr (rs#rd <- (Val.shr rs#r1 (Vint n)) #CARRY <- (Val.shr_carry rs#r1 (Vint n)))) m | Psrw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.shru rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.shru rs#r1 rs#r2))) m | Pstb rd cst r1 => store1 Mint8unsigned rd cst r1 rs m | Pstbx rd r1 r2 => @@ -717,13 +729,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome store2 Mfloat64al32 rd r1 r2 rs m | Pstfs rd cst r1 => match store1 Mfloat32 rd cst r1 rs m with - | OK rs' m' => OK (rs'#FPR13 <- Vundef) m' - | Error => Error + | Next rs' m' => Next (rs'#FPR13 <- Vundef) m' + | Stuck => Stuck end | Pstfsx rd r1 r2 => match store2 Mfloat32 rd r1 r2 rs m with - | OK rs' m' => OK (rs'#FPR13 <- Vundef) m' - | Error => Error + | Next rs' m' => Next (rs'#FPR13 <- Vundef) m' + | Stuck => Stuck end | Psth rd cst r1 => store1 Mint16unsigned rd cst r1 rs m @@ -734,41 +746,34 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pstwx rd r1 r2 => store2 Mint32 rd r1 r2 rs m | Psubfc rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1) + Next (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1) #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) Vone))) m | Psubfe rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.add (Val.add rs#r2 (Val.notint rs#r1)) rs#CARRY) + Next (nextinstr (rs#rd <- (Val.add (Val.add rs#r2 (Val.notint rs#r1)) rs#CARRY) #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) rs#CARRY))) m | Psubfic rd r1 cst => - OK (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1) + Next (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1) #CARRY <- (Val.add_carry (const_low cst) (Val.notint rs#r1) Vone))) m | Pxor rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.xor rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.xor rs#r1 rs#r2))) m | Pxori rd r1 cst => - OK (nextinstr (rs#rd <- (Val.xor rs#r1 (const_low cst)))) m + Next (nextinstr (rs#rd <- (Val.xor rs#r1 (const_low cst)))) m | Pxoris rd r1 cst => - OK (nextinstr (rs#rd <- (Val.xor rs#r1 (const_high cst)))) m + Next (nextinstr (rs#rd <- (Val.xor rs#r1 (const_high cst)))) m | Plabel lbl => - OK (nextinstr rs) m + Next (nextinstr rs) m | Pbuiltin ef args res => - Error (**r treated specially below *) + Stuck (**r treated specially below *) | Pannot ef args => - Error (**r treated specially below *) + Stuck (**r treated specially below *) end. (** Translation of the LTL/Linear/Mach view of machine registers - to the PPC view. PPC has two different types for registers - (integer and float) while LTL et al have only one. The - [ireg_of] and [freg_of] are therefore partial in principle. - To keep things simpler, we make them return nonsensical - 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 [GPR0]. + to the PPC view. 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 := +Definition preg_of (r: mreg) : preg := match r with | R3 => GPR3 | R4 => GPR4 | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9 | R10 => GPR10 @@ -778,11 +783,6 @@ Definition ireg_of (r: mreg) : ireg := | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29 | R30 => GPR30 | R31 => GPR31 | 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 | F11 => FPR11 @@ -792,13 +792,6 @@ Definition freg_of (r: mreg) : freg := | F24 => FPR24 | F25 => FPR25 | F26 => FPR26 | F27 => FPR27 | F28 => FPR28 | F29 => FPR29 | F30 => FPR30 | F31 => FPR31 | FT1 => FPR0 | FT2 => FPR12 | FT3 => FPR13 - | _ => FPR0 (* should not happen *) - end. - -Definition preg_of (r: mreg) := - match mreg_type r with - | Tint => IR (ireg_of r) - | Tfloat => FR (freg_of r) end. (** Extract the values of the arguments of an external call. @@ -849,7 +842,7 @@ Inductive step: state -> trace -> state -> Prop := rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal c) -> find_instr (Int.unsigned ofs) c = Some i -> - exec_instr c i rs m = OK rs' m' -> + exec_instr c i rs m = Next rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_builtin: forall b ofs c ef args res rs m t v m', @@ -968,3 +961,25 @@ Ltac Equalities := (* final states *) inv H; inv H0. congruence. Qed. + +(** Classification functions for processor registers (used in Asmgenproof). *) + +Definition data_preg (r: preg) : bool := + match r with + | IR GPR0 => false + | PC => false | LR => false | CTR => false + | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false + | CARRY => false + | _ => true + end. + +Definition nontemp_preg (r: preg) : bool := + match r with + | IR GPR0 => false | IR GPR11 => false | IR GPR12 => false + | FR FPR0 => false | FR FPR12 => false | FR FPR13 => false + | PC => false | LR => false | CTR => false + | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false + | CARRY => false + | _ => true + end. + diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 8ef249dd..0035dff8 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -22,6 +22,23 @@ Require Import Locations. Require Import Mach. Require Import Asm. +Open Local Scope string_scope. +Open Local Scope error_monad_scope. + +(** The code generation functions take advantage of several + characteristics of the [Mach] code generated by earlier passes of the + compiler, mostly that argument and result registers are of the correct + types. These properties are true by construction, but it's easier to + recheck them during code generation and fail if they do not hold. *) + +(** Extracting integer or float registers. *) + +Definition ireg_of (r: mreg) : res ireg := + match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end. + +Definition freg_of (r: mreg) : res freg := + match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end. + (** Decomposition of integer constants. As noted in file [Asm], immediate arguments to PowerPC instructions must fit into 16 bits, and are interpreted after zero extension, sign extension, or @@ -106,30 +123,36 @@ Definition rolm (r1 r2: ireg) (amount mask: int) (k: code) := (** 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 - match ty with - | Tint => Plwz (ireg_of dst) (Cint ofs) base :: k - | Tfloat => Plfd (freg_of dst) (Cint ofs) base :: k - end - else - loadimm GPR0 ofs - (match ty with - | Tint => Plwzx (ireg_of dst) base GPR0 :: k - | Tfloat => Plfdx (freg_of dst) base GPR0 :: k - end). + match ty with + | Tint => + do r <- ireg_of dst; + OK (if Int.eq (high_s ofs) Int.zero then + Plwz r (Cint ofs) base :: k + else + loadimm GPR0 ofs (Plwzx r base GPR0 :: k)) + | Tfloat => + do r <- freg_of dst; + OK (if Int.eq (high_s ofs) Int.zero then + Plfd r (Cint ofs) base :: k + else + loadimm GPR0 ofs (Plfdx r 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 - match ty with - | Tint => Pstw (ireg_of src) (Cint ofs) base :: k - | Tfloat => Pstfd (freg_of src) (Cint ofs) base :: k - end - else - loadimm GPR0 ofs - (match ty with - | Tint => Pstwx (ireg_of src) base GPR0 :: k - | Tfloat => Pstfdx (freg_of src) base GPR0 :: k - end). + match ty with + | Tint => + do r <- ireg_of src; + OK (if Int.eq (high_s ofs) Int.zero then + Pstw r (Cint ofs) base :: k + else + loadimm GPR0 ofs (Pstwx r base GPR0 :: k)) + | Tfloat => + do r <- freg_of src; + OK (if Int.eq (high_s ofs) Int.zero then + Pstfd r (Cint ofs) base :: k + else + loadimm GPR0 ofs (Pstfdx r base GPR0 :: k)) + end. (** Constructor for a floating-point comparison. The PowerPC has a single [fcmpu] instruction to compare floats, which sets @@ -156,29 +179,31 @@ Definition transl_cond (cond: condition) (args: list mreg) (k: code) := match cond, args with | Ccomp c, a1 :: a2 :: nil => - Pcmpw (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmpw r1 r2 :: k) | Ccompu c, a1 :: a2 :: nil => - Pcmplw (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmplw r1 r2 :: k) | Ccompimm c n, a1 :: nil => + do r1 <- ireg_of a1; if Int.eq (high_s n) Int.zero then - Pcmpwi (ireg_of a1) (Cint n) :: k + OK (Pcmpwi r1 (Cint n) :: k) else - loadimm GPR0 n (Pcmpw (ireg_of a1) GPR0 :: k) + OK (loadimm GPR0 n (Pcmpw r1 GPR0 :: k)) | Ccompuimm c n, a1 :: nil => + do r1 <- ireg_of a1; if Int.eq (high_u n) Int.zero then - Pcmplwi (ireg_of a1) (Cint n) :: k + OK (Pcmplwi r1 (Cint n) :: k) else - loadimm GPR0 n (Pcmplw (ireg_of a1) GPR0 :: k) + OK (loadimm GPR0 n (Pcmplw r1 GPR0 :: k)) | Ccompf cmp, a1 :: a2 :: nil => - floatcomp cmp (freg_of a1) (freg_of a2) k + do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 k) | Cnotcompf cmp, a1 :: a2 :: nil => - floatcomp cmp (freg_of a1) (freg_of a2) k + do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 k) | Cmaskzero n, a1 :: nil => - andimm_base GPR0 (ireg_of a1) n k + do r1 <- ireg_of a1; OK (andimm_base GPR0 r1 n k) | Cmasknotzero n, a1 :: nil => - andimm_base GPR0 (ireg_of a1) n k + do r1 <- ireg_of a1; OK (andimm_base GPR0 r1 n k) | _, _ => - k (**r never happens for well-typed code *) + Error(msg "Asmgen.transl_cond") end. (* CRbit_0 = Less @@ -264,180 +289,267 @@ Definition classify_condition (c: condition) (args: list mreg): condition_class Definition transl_cond_op (cond: condition) (args: list mreg) (r: mreg) (k: code) := + do r' <- ireg_of r; match classify_condition cond args with | condition_eq0 _ a _ => - Psubfic GPR0 (ireg_of a) (Cint Int.zero) :: - Padde (ireg_of r) GPR0 (ireg_of a) :: k + do a' <- ireg_of a; + OK (Psubfic GPR0 a' (Cint Int.zero) :: + Padde r' GPR0 a' :: k) | condition_ne0 _ a _ => - Paddic GPR0 (ireg_of a) (Cint Int.mone) :: - Psubfe (ireg_of r) GPR0 (ireg_of a) :: k + do a' <- ireg_of a; + OK (Paddic GPR0 a' (Cint Int.mone) :: + Psubfe r' GPR0 a' :: k) | condition_ge0 _ a _ => - Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: - Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k + do a' <- ireg_of a; + OK (Prlwinm r' a' Int.one Int.one :: + Pxori r' r' (Cint Int.one) :: k) | condition_lt0 _ a _ => - Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: k + do a' <- ireg_of a; + OK (Prlwinm r' a' Int.one Int.one :: k) | condition_default _ _ => let p := crbit_for_cond cond in transl_cond cond args - (Pmfcrbit (ireg_of r) (fst p) :: + (Pmfcrbit r' (fst p) :: if snd p then k - else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k) + else Pxori r' r' (Cint Int.one) :: k) end. (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) Definition transl_op - (op: operation) (args: list mreg) (r: mreg) (k: code) := + (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with | Omove, a1 :: nil => - match mreg_type a1 with - | Tint => Pmr (ireg_of r) (ireg_of a1) :: k - | Tfloat => Pfmr (freg_of r) (freg_of a1) :: k + match preg_of res, preg_of a1 with + | IR r, IR a => OK (Pmr r a :: k) + | FR r, FR a => OK (Pfmr r a :: k) + | _ , _ => Error(msg "Asmgen.Omove") end | Ointconst n, nil => - loadimm (ireg_of r) n k + do r <- ireg_of res; OK (loadimm r n k) | Ofloatconst f, nil => - Plfi (freg_of r) f :: k + do r <- freg_of res; OK (Plfi r f :: k) | Oaddrsymbol s ofs, nil => - if symbol_is_small_data s ofs then - Paddi (ireg_of r) GPR0 (Csymbol_sda s ofs) :: k - else - Paddis GPR12 GPR0 (Csymbol_high s ofs) :: - Paddi (ireg_of r) GPR12 (Csymbol_low s ofs) :: k + do r <- ireg_of res; + OK (if symbol_is_small_data s ofs then + Paddi r GPR0 (Csymbol_sda s ofs) :: k + else + Paddis GPR12 GPR0 (Csymbol_high s ofs) :: + Paddi r GPR12 (Csymbol_low s ofs) :: k) | Oaddrstack n, nil => - addimm (ireg_of r) GPR1 n k + do r <- ireg_of res; OK (addimm r GPR1 n k) | Ocast8signed, a1 :: nil => - Pextsb (ireg_of r) (ireg_of a1) :: k + do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pextsb r r1 :: k) | Ocast16signed, a1 :: nil => - Pextsh (ireg_of r) (ireg_of a1) :: k + do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pextsh r r1 :: k) | Oadd, a1 :: a2 :: nil => - Padd (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Padd r r1 r2 :: k) | Oaddimm n, a1 :: nil => - addimm (ireg_of r) (ireg_of a1) n k + do r1 <- ireg_of a1; do r <- ireg_of res; OK (addimm r r1 n k) | Osub, a1 :: a2 :: nil => - Psubfc (ireg_of r) (ireg_of a2) (ireg_of a1) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Psubfc r r2 r1 :: k) | Osubimm n, a1 :: nil => - if Int.eq (high_s n) Int.zero then - Psubfic (ireg_of r) (ireg_of a1) (Cint n) :: k - else - loadimm GPR0 n (Psubfc (ireg_of r) (ireg_of a1) GPR0 :: k) + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (if Int.eq (high_s n) Int.zero then + Psubfic r r1 (Cint n) :: k + else + loadimm GPR0 n (Psubfc r r1 GPR0 :: k)) | Omul, a1 :: a2 :: nil => - Pmullw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pmullw r r1 r2 :: 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 GPR0 n (Pmullw (ireg_of r) (ireg_of a1) GPR0 :: k) + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (if Int.eq (high_s n) Int.zero then + Pmulli r r1 (Cint n) :: k + else + loadimm GPR0 n (Pmullw r r1 GPR0 :: k)) | Odiv, a1 :: a2 :: nil => - Pdivw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pdivw r r1 r2 :: k) | Odivu, a1 :: a2 :: nil => - Pdivwu (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pdivwu r r1 r2 :: k) | Oand, a1 :: a2 :: nil => - Pand_ (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pand_ r r1 r2 :: k) | Oandimm n, a1 :: nil => - andimm (ireg_of r) (ireg_of a1) n k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (andimm r r1 n k) | Oor, a1 :: a2 :: nil => - Por (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Por r r1 r2 :: k) | Oorimm n, a1 :: nil => - orimm (ireg_of r) (ireg_of a1) n k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (orimm r r1 n k) | Oxor, a1 :: a2 :: nil => - Pxor (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pxor r r1 r2 :: k) | Oxorimm n, a1 :: nil => - xorimm (ireg_of r) (ireg_of a1) n k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (xorimm r r1 n k) | Onot, a1 :: nil => - Pnor (ireg_of r) (ireg_of a1) (ireg_of a1) :: k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Pnor r r1 r1 :: k) | Onand, a1 :: a2 :: nil => - Pnand (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pnand r r1 r2 :: k) | Onor, a1 :: a2 :: nil => - Pnor (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pnor r r1 r2 :: k) | Onxor, a1 :: a2 :: nil => - Peqv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Peqv r r1 r2 :: k) | Oandc, a1 :: a2 :: nil => - Pandc (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pandc r r1 r2 :: k) | Oorc, a1 :: a2 :: nil => - Porc (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Porc r r1 r2 :: k) | Oshl, a1 :: a2 :: nil => - Pslw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pslw r r1 r2 :: k) | Oshr, a1 :: a2 :: nil => - Psraw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Psraw r r1 r2 :: k) | Oshrimm n, a1 :: nil => - Psrawi (ireg_of r) (ireg_of a1) n :: k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Psrawi r r1 n :: k) | Oshrximm n, a1 :: nil => - Psrawi (ireg_of r) (ireg_of a1) n :: - Paddze (ireg_of r) (ireg_of r) :: k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Psrawi r r1 n :: Paddze r r :: k) | Oshru, a1 :: a2 :: nil => - Psrw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Psrw r r1 r2 :: k) | Orolm amount mask, a1 :: nil => - rolm (ireg_of r) (ireg_of a1) amount mask k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (rolm r r1 amount mask k) | Oroli amount mask, a1 :: a2 :: nil => - if mreg_eq a1 r then (**r should always be true *) - Prlwimi (ireg_of r) (ireg_of a2) amount mask :: k - else - Pmr GPR0 (ireg_of a1) :: - Prlwimi GPR0 (ireg_of a2) amount mask :: - Pmr (ireg_of r) GPR0 :: k + do x <- assertion (mreg_eq a1 res); + do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Prlwimi r r2 amount mask :: k) | Onegf, a1 :: nil => - Pfneg (freg_of r) (freg_of a1) :: k + do r1 <- freg_of a1; do r <- freg_of res; + OK (Pfneg r r1 :: k) | Oabsf, a1 :: nil => - Pfabs (freg_of r) (freg_of a1) :: k + do r1 <- freg_of a1; do r <- freg_of res; + OK (Pfabs r r1 :: k) | Oaddf, a1 :: a2 :: nil => - Pfadd (freg_of r) (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfadd r r1 r2 :: k) | Osubf, a1 :: a2 :: nil => - Pfsub (freg_of r) (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfsub r r1 r2 :: k) | Omulf, a1 :: a2 :: nil => - Pfmul (freg_of r) (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfmul r r1 r2 :: k) | Odivf, a1 :: a2 :: nil => - Pfdiv (freg_of r) (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfdiv r r1 r2 :: k) | Osingleoffloat, a1 :: nil => - Pfrsp (freg_of r) (freg_of a1) :: k + do r1 <- freg_of a1; do r <- freg_of res; + OK (Pfrsp r r1 :: k) | Ointoffloat, a1 :: nil => - Pfcti (ireg_of r) (freg_of a1) :: k + do r1 <- freg_of a1; do r <- ireg_of res; + OK (Pfcti r r1 :: k) | Ofloatofwords, a1 :: a2 :: nil => - Pfmake (freg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res; + OK (Pfmake r r1 r2 :: k) | Ocmp cmp, _ => - transl_cond_op cmp args r k + transl_cond_op cmp args res k | _, _ => - k (**r never happens for well-typed code *) + Error(msg "Asmgen.transl_op") end. -(** Common code to translate [Mload] and [Mstore] instructions. *) +(** Translation of memory accesses: loads, and stores. *) Definition int_temp_for (r: mreg) := if mreg_eq r IT2 then GPR11 else GPR12. -Definition transl_load_store +Definition transl_memory_access (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) (addr: addressing) (args: list mreg) (temp: ireg) (k: code) := match addr, args with | Aindexed ofs, a1 :: nil => - if Int.eq (high_s ofs) Int.zero then - mk1 (Cint ofs) (ireg_of a1) :: k - else - Paddis temp (ireg_of a1) (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) temp :: k + do r1 <- ireg_of a1; + OK (if Int.eq (high_s ofs) Int.zero then + mk1 (Cint ofs) r1 :: k + else + Paddis temp r1 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) temp :: k) | Aindexed2, a1 :: a2 :: nil => - mk2 (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (mk2 r1 r2 :: k) | Aglobal symb ofs, nil => - if symbol_is_small_data symb ofs then - mk1 (Csymbol_sda symb ofs) GPR0 :: k - else - Paddis temp GPR0 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) temp :: k + OK (if symbol_is_small_data symb ofs then + mk1 (Csymbol_sda symb ofs) GPR0 :: k + else + Paddis temp GPR0 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) temp :: k) | Abased symb ofs, a1 :: nil => - Paddis temp (ireg_of a1) (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) temp :: k + do r1 <- ireg_of a1; + OK (Paddis temp r1 (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 temp GPR1 (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) temp :: k + OK (if Int.eq (high_s ofs) Int.zero then + mk1 (Cint ofs) GPR1 :: k + else + Paddis temp GPR1 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) temp :: k) | _, _ => - (* should not happen *) k + Error(msg "Asmgen.transl_memory_access") + end. + +Definition transl_load (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (dst: mreg) (k: code) := + match chunk with + | Mint8signed => + do r <- ireg_of dst; + transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 (Pextsb r r :: k) + | Mint8unsigned => + do r <- ireg_of dst; + transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 k + | Mint16signed => + do r <- ireg_of dst; + transl_memory_access (Plha r) (Plhax r) addr args GPR12 k + | Mint16unsigned => + do r <- ireg_of dst; + transl_memory_access (Plhz r) (Plhzx r) addr args GPR12 k + | Mint32 => + do r <- ireg_of dst; + transl_memory_access (Plwz r) (Plwzx r) addr args GPR12 k + | Mfloat32 => + do r <- freg_of dst; + transl_memory_access (Plfs r) (Plfsx r) addr args GPR12 k + | Mfloat64 | Mfloat64al32 => + do r <- freg_of dst; + transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k + end. + +Definition transl_store (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (src: mreg) (k: code) := + let temp := int_temp_for src in + match chunk with + | Mint8signed | Mint8unsigned => + do r <- ireg_of src; + transl_memory_access (Pstb r) (Pstbx r) addr args temp k + | Mint16signed | Mint16unsigned => + do r <- ireg_of src; + transl_memory_access (Psth r) (Psthx r) addr args temp k + | Mint32 => + do r <- ireg_of src; + transl_memory_access (Pstw r) (Pstwx r) addr args temp k + | Mfloat32 => + do r <- freg_of src; + transl_memory_access (Pstfs r) (Pstfsx r) addr args temp k + | Mfloat64 | Mfloat64al32 => + do r <- freg_of src; + transl_memory_access (Pstfd r) (Pstfdx r) addr args temp k end. (** Translation of arguments to annotations *) @@ -450,105 +562,80 @@ Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param := (** Translation of a Mach instruction. *) -Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := +Definition transl_instr (f: Mach.function) (i: Mach.instruction) + (r11_is_parent: bool) (k: code) := match i with | Mgetstack ofs ty dst => loadind GPR1 ofs ty dst k | Msetstack src ofs ty => storeind src GPR1 ofs ty k | Mgetparam ofs ty dst => - Plwz GPR11 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR11 ofs ty dst k + if r11_is_parent then + loadind GPR11 ofs ty dst k + else + (do k1 <- loadind GPR11 ofs ty dst k; + loadind GPR1 f.(fn_link_ofs) Tint IT1 k1) | 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 GPR12 - (Pextsb (ireg_of dst) (ireg_of dst) :: k) - | Mint8unsigned => - transl_load_store - (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 GPR12 k - | Mint16unsigned => - transl_load_store - (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 GPR12 k - | Mfloat32 => - transl_load_store - (Plfs (freg_of dst)) (Plfsx (freg_of dst)) addr args GPR12 k - | Mfloat64 | Mfloat64al32 => - transl_load_store - (Plfd (freg_of dst)) (Plfdx (freg_of dst)) addr args GPR12 k - end + transl_load chunk addr args dst k | 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 temp k - | Mint8unsigned => - transl_load_store - (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 temp k - | Mint16unsigned => - transl_load_store - (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 temp k - | Mfloat32 => - transl_load_store - (Pstfs (freg_of src)) (Pstfsx (freg_of src)) addr args temp k - | Mfloat64 | Mfloat64al32 => - transl_load_store - (Pstfd (freg_of src)) (Pstfdx (freg_of src)) addr args temp k - end + transl_store chunk addr args src k | Mcall sig (inl r) => - Pmtctr (ireg_of r) :: Pbctrl :: k + do r1 <- ireg_of r; OK (Pmtctr r1 :: Pbctrl :: k) | Mcall sig (inr symb) => - Pbl symb :: k + OK (Pbl symb :: k) | Mtailcall sig (inl r) => - Pmtctr (ireg_of r) :: - Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR0 :: - Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pbctr :: k + do r1 <- ireg_of r; + OK (Pmtctr r1 :: + Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR0 :: + Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pbctr :: k) | Mtailcall sig (inr symb) => - Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR0 :: - Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pbs symb :: k + OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR0 :: + Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pbs symb :: k) | Mbuiltin ef args res => - Pbuiltin ef (map preg_of args) (preg_of res) :: k + OK (Pbuiltin ef (map preg_of args) (preg_of res) :: k) | Mannot ef args => - Pannot ef (map transl_annot_param args) :: k + OK (Pannot ef (map transl_annot_param args) :: k) | Mlabel lbl => - Plabel lbl :: k + OK (Plabel lbl :: k) | Mgoto lbl => - Pb lbl :: k + OK (Pb lbl :: k) | Mcond cond args lbl => let p := crbit_for_cond cond in transl_cond cond args (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k) | Mjumptable arg tbl => - Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: - Pbtbl GPR12 tbl :: k + do r <- ireg_of arg; + OK (Pbtbl r tbl :: k) | Mreturn => - Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR0 :: - Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pblr :: k + OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR0 :: + Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pblr :: k) + end. + +(** Translation of a code sequence *) + +Definition r11_is_parent (before: bool) (i: Mach.instruction) : bool := + match i with + | Msetstack src ofs ty => before + | Mgetparam ofs ty dst => negb (mreg_eq dst IT1) + | Mop Omove args res => before && negb (mreg_eq res IT1) + | _ => false end. -Definition transl_code (f: Mach.function) (il: list Mach.instruction) := - List.fold_right (transl_instr f) nil il. +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (r11p: bool) := + match il with + | nil => OK nil + | i1 :: il' => + do k <- transl_code f il' (r11_is_parent r11p i1); + transl_instr f i1 r11p k + end. (** Translation of a whole function. Note that we must check that the generated code contains less than [2^32] instructions, @@ -556,18 +643,16 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) := around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pmflr GPR0 :: - Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: - transl_code f f.(fn_code). - -Open Local Scope string_scope. + do c <- transl_code f f.(Mach.fn_code) false; + OK (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pmflr GPR0 :: + Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: c). Definition transf_function (f: Mach.function) : res Asm.code := - let c := transl_function f in + do c <- transl_function f; if zlt Int.max_unsigned (list_length_z c) - then Errors.Error (msg "code size exceeded") - else Errors.OK c. + then Error (msg "code size exceeded") + else OK c. Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := transf_partial_fundef transf_function f. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index de9decbd..6c95744a 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -27,11 +27,9 @@ Require Import Op. Require Import Locations. Require Import Conventions. Require Import Mach. -Require Import Machsem. -Require Import Machtyping. Require Import Asm. Require Import Asmgen. -Require Import Asmgenretaddr. +Require Import Asmgenproof0. Require Import Asmgenproof1. Section PRESERVATION. @@ -67,210 +65,53 @@ Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). Lemma functions_transl: - forall f b, + forall f b tf, Genv.find_funct_ptr ge b = Some (Internal f) -> - Genv.find_funct_ptr tge b = Some (Internal (transl_function f)). + transf_function f = OK tf -> + Genv.find_funct_ptr tge b = Some (Internal tf). Proof. intros. - destruct (functions_translated _ _ H) as [tf [A B]]. - rewrite A. generalize B. unfold transf_fundef, transf_partial_fundef, transf_function. - case (zlt Int.max_unsigned (list_length_z (transl_function f))); simpl; intro. - congruence. intro. inv B0. auto. -Qed. - -Lemma functions_transl_no_overflow: - forall b f, - Genv.find_funct_ptr ge b = Some (Internal f) -> - list_length_z (transl_function f) <= Int.max_unsigned. -Proof. - intros. - destruct (functions_translated _ _ H) as [tf [A B]]. - generalize B. unfold transf_fundef, transf_partial_fundef, transf_function. - case (zlt Int.max_unsigned (list_length_z (transl_function f))); simpl; intro. - congruence. intro; omega. + destruct (functions_translated _ _ H) as [tf' [A B]]. + rewrite A. monadInv B. f_equal. congruence. Qed. (** * Properties of control flow *) -Lemma find_instr_in: - forall c pos i, - find_instr pos c = Some i -> In i c. -Proof. - induction c; simpl. intros; discriminate. - intros until i. case (zeq pos 0); intros. - left; congruence. right; eauto. -Qed. - -Lemma find_instr_tail: - forall c1 i c2 pos, - code_tail pos c1 (i :: c2) -> - find_instr pos c1 = Some i. -Proof. - induction c1; simpl; intros. - inv H. - destruct (zeq pos 0). subst pos. - inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction. - inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega. - eauto. -Qed. - -Remark code_tail_bounds: - forall fn ofs i c, - code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn. +Lemma transf_function_no_overflow: + forall f tf, + transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned. Proof. - assert (forall ofs fn c, code_tail ofs fn c -> - forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn). - induction 1; intros; simpl. - rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega. - rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega. - eauto. -Qed. - -Lemma code_tail_next: - forall fn ofs i c, - code_tail ofs fn (i :: c) -> - code_tail (ofs + 1) fn c. -Proof. - assert (forall ofs fn c, code_tail ofs fn c -> - forall i c', c = i :: c' -> code_tail (ofs + 1) fn c'). - induction 1; intros. - subst c. constructor. constructor. - constructor. eauto. - eauto. -Qed. - -Lemma code_tail_next_int: - forall fn ofs i c, - list_length_z fn <= Int.max_unsigned -> - code_tail (Int.unsigned ofs) fn (i :: c) -> - code_tail (Int.unsigned (Int.add ofs Int.one)) fn c. -Proof. - intros. rewrite Int.add_unsigned. - change (Int.unsigned Int.one) with 1. - rewrite Int.unsigned_repr. apply code_tail_next with i; auto. - generalize (code_tail_bounds _ _ _ _ H0). omega. -Qed. - -(** [transl_code_at_pc pc fn c] holds if the code pointer [pc] points - within the PPC code generated by translating Mach function [fn], - and [c] is the tail of the generated code at the position corresponding - to the code pointer [pc]. *) - -Inductive transl_code_at_pc: val -> block -> Mach.function -> Mach.code -> Prop := - transl_code_at_pc_intro: - forall b ofs f c, - Genv.find_funct_ptr ge b = Some (Internal f) -> - code_tail (Int.unsigned ofs) (transl_function f) (transl_code f c) -> - transl_code_at_pc (Vptr b ofs) b f c. - -(** The following lemmas show that straight-line executions - (predicate [exec_straight]) correspond to correct PPC executions - (predicate [exec_steps]) under adequate [transl_code_at_pc] hypotheses. *) - -Lemma exec_straight_steps_1: - forall fn c rs m c' rs' m', - exec_straight tge fn c rs m c' rs' m' -> - list_length_z fn <= Int.max_unsigned -> - forall b ofs, - rs#PC = Vptr b ofs -> - Genv.find_funct_ptr tge b = Some (Internal fn) -> - code_tail (Int.unsigned ofs) fn c -> - plus step tge (State rs m) E0 (State rs' m'). -Proof. - induction 1; intros. - apply plus_one. - econstructor; eauto. - eapply find_instr_tail. eauto. - eapply plus_left'. - econstructor; eauto. - eapply find_instr_tail. eauto. - apply IHexec_straight with b (Int.add ofs Int.one). - auto. rewrite H0. rewrite H3. reflexivity. - auto. - apply code_tail_next_int with i; auto. - traceEq. -Qed. - -Lemma exec_straight_steps_2: - forall fn c rs m c' rs' m', - exec_straight tge fn c rs m c' rs' m' -> - list_length_z fn <= Int.max_unsigned -> - forall b ofs, - rs#PC = Vptr b ofs -> - Genv.find_funct_ptr tge b = Some (Internal fn) -> - code_tail (Int.unsigned ofs) fn c -> - exists ofs', - rs'#PC = Vptr b ofs' - /\ code_tail (Int.unsigned ofs') fn c'. -Proof. - induction 1; intros. - exists (Int.add ofs Int.one). split. - rewrite H0. rewrite H2. auto. - apply code_tail_next_int with i1; auto. - apply IHexec_straight with (Int.add ofs Int.one). - auto. rewrite H0. rewrite H3. reflexivity. auto. - apply code_tail_next_int with i; auto. + intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. + omega. Qed. Lemma exec_straight_exec: - forall fb f c c' rs m rs' m', - transl_code_at_pc (rs PC) fb f c -> - exec_straight tge (transl_function f) - (transl_code f c) rs m c' rs' m' -> + forall f c ep tf tc c' rs m rs' m', + transl_code_at_pc ge (rs PC) f c ep tf tc -> + exec_straight tge tf tc rs m c' rs' m' -> plus step tge (State rs m) E0 (State rs' m'). Proof. - intros. inversion H. subst. + intros. inv H. eapply exec_straight_steps_1; eauto. - eapply functions_transl_no_overflow; eauto. - eapply functions_transl; eauto. + eapply transf_function_no_overflow; eauto. + eapply functions_transl; eauto. Qed. Lemma exec_straight_at: - forall fb f c c' rs m rs' m', - transl_code_at_pc (rs PC) fb f c -> - exec_straight tge (transl_function f) - (transl_code f c) rs m (transl_code f c') rs' m' -> - transl_code_at_pc (rs' PC) fb f c'. + forall f c ep tf tc c' ep' tc' rs m rs' m', + transl_code_at_pc ge (rs PC) f c ep tf tc -> + transl_code f c' ep' = OK tc' -> + exec_straight tge tf tc rs m tc' rs' m' -> + transl_code_at_pc ge (rs' PC) f c' ep' tf tc'. Proof. - intros. inversion H. subst. - generalize (functions_transl_no_overflow _ _ H2). intro. - generalize (functions_transl _ _ H2). intro. - generalize (exec_straight_steps_2 _ _ _ _ _ _ _ - H0 H4 _ _ (sym_equal H1) H5 H3). + intros. inv H. + exploit exec_straight_steps_2; eauto. + eapply transf_function_no_overflow; eauto. + eapply functions_transl; eauto. intros [ofs' [PC' CT']]. rewrite PC'. constructor; auto. Qed. -(** Correctness of the return addresses predicted by - [PPCgen.return_address_offset]. *) - -Remark code_tail_no_bigger: - forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat. -Proof. - induction 1; simpl; omega. -Qed. - -Remark code_tail_unique: - forall fn c pos pos', - code_tail pos fn c -> code_tail pos' fn c -> pos = pos'. -Proof. - induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - f_equal. eauto. -Qed. - -Lemma return_address_offset_correct: - forall b ofs fb f c ofs', - transl_code_at_pc (Vptr b ofs) fb f c -> - return_address_offset f c ofs' -> - ofs' = ofs. -Proof. - intros. inv H0. inv H. - generalize (code_tail_unique _ _ _ _ H1 H7). intro. rewrite H. - apply Int.repr_unsigned. -Qed. - (** The [find_label] function returns the code tail starting at the given label. A connection with [code_tail] is then established. *) @@ -391,119 +232,137 @@ Qed. Hint Rewrite rolm_label: labels. Remark loadind_label: - forall base ofs ty dst k, find_label lbl (loadind base ofs ty dst k) = find_label lbl k. + forall base ofs ty dst k c, + loadind base ofs ty dst k = OK c -> + find_label lbl c = find_label lbl k. Proof. - intros; unfold loadind. - destruct (Int.eq (high_s ofs) Int.zero); destruct ty; autorewrite with labels; auto. + unfold loadind; intros. + destruct ty; destruct (Int.eq (high_s ofs) Int.zero); monadInv H; + autorewrite with labels; auto. Qed. -Hint Rewrite loadind_label: labels. Remark storeind_label: - forall base ofs ty src k, find_label lbl (storeind base src ofs ty k) = find_label lbl k. + forall base ofs ty src k c, + storeind base src ofs ty k = OK c -> + find_label lbl c = find_label lbl k. Proof. - intros; unfold storeind. - destruct (Int.eq (high_s ofs) Int.zero); destruct ty; autorewrite with labels; auto. + unfold storeind; intros. + destruct ty; destruct (Int.eq (high_s ofs) Int.zero); monadInv H; + 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. intros; unfold floatcomp. destruct cmp; reflexivity. Qed. +Hint Rewrite floatcomp_label: labels. Remark transl_cond_label: - forall cond args k, find_label lbl (transl_cond cond args k) = find_label lbl k. + forall cond args k c, + transl_cond cond args k = OK c -> find_label lbl c = find_label lbl k. Proof. - intros; unfold transl_cond. - destruct cond; (destruct args; - [try reflexivity | destruct args; - [try reflexivity | destruct args; try reflexivity]]). - case (Int.eq (high_s i) Int.zero). reflexivity. - autorewrite with labels; reflexivity. - case (Int.eq (high_u i) Int.zero). reflexivity. - autorewrite with labels; reflexivity. - apply floatcomp_label. apply floatcomp_label. - apply andimm_base_label. apply andimm_base_label. + unfold transl_cond; intros; destruct cond; + (destruct args; + [try discriminate | destruct args; + [try discriminate | destruct args; try discriminate]]); + monadInv H; autorewrite with labels; auto. + destruct (Int.eq (high_s i) Int.zero); inv EQ0; autorewrite with labels; auto. + destruct (Int.eq (high_u i) Int.zero); inv EQ0; autorewrite with labels; auto. Qed. -Hint Rewrite transl_cond_label: labels. Remark transl_cond_op_label: - forall c args r k, - find_label lbl (transl_cond_op c args r k) = find_label lbl k. + forall cond args r k c, + transl_cond_op cond args r k = OK c -> find_label lbl c = find_label lbl k. Proof. - intros c args. - unfold transl_cond_op. destruct (classify_condition c args); intros; auto. - autorewrite with labels. destruct (snd (crbit_for_cond c)); auto. + unfold transl_cond_op; intros; destruct (classify_condition cond args); + monadInv H; auto. + erewrite transl_cond_label. 2: eauto. + destruct (snd (crbit_for_cond c0)); auto. Qed. -Hint Rewrite transl_cond_op_label: labels. Remark transl_op_label: - forall op args r k, find_label lbl (transl_op op args r k) = find_label lbl k. + forall op args r k c, + transl_op op args r k = OK c -> find_label lbl c = find_label lbl k. Proof. - intros; unfold transl_op; - destruct op; destruct args; try (destruct args); try (destruct args); try (destruct args); - try reflexivity; autorewrite with labels; try reflexivity. - case (mreg_type m); reflexivity. - case (symbol_is_small_data i i0); reflexivity. - case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. - case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. - destruct (mreg_eq m r); reflexivity. + unfold transl_op; intros; destruct op; try (eapply transl_cond_op_label; eauto; fail); + (destruct args; + [try discriminate | destruct args; + [try discriminate | destruct args; try discriminate]]); + try (monadInv H); autorewrite with labels; auto. + destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; auto. + destruct (symbol_is_small_data i i0); auto. + destruct (Int.eq (high_s i) Int.zero); autorewrite with labels; auto. + destruct (Int.eq (high_s i) Int.zero); autorewrite with labels; auto. Qed. -Hint Rewrite transl_op_label: labels. -Remark transl_load_store_label: +Remark transl_memory_access_label: forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - addr args temp k, + addr args temp k c, + transl_memory_access mk1 mk2 addr args temp k = OK c -> (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 temp k) = find_label lbl k. -Proof. - intros; unfold transl_load_store. - destruct addr; destruct args; try (destruct args); try (destruct args); - try reflexivity. - destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto. + find_label lbl c = find_label lbl k. +Proof. + unfold transl_memory_access; intros; destruct addr; + (destruct args; + [try discriminate | destruct args; + [try discriminate | destruct args; try discriminate]]); + monadInv H; autorewrite with labels; auto. + destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H0; auto. + simpl; rewrite H1; auto. + destruct (symbol_is_small_data i i0); simpl; rewrite H0; auto. simpl; rewrite H0; auto. - destruct (symbol_is_small_data i i0); simpl; rewrite H; auto. - simpl; rewrite H; auto. - destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto. + destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H0; auto. Qed. -Hint Rewrite transl_load_store_label: labels. Lemma transl_instr_label: - forall f i k, - find_label lbl (transl_instr f i k) = - if Mach.is_label lbl i then Some k else find_label lbl k. -Proof. - intros. generalize (Mach.is_label_correct lbl i). - case (Mach.is_label lbl i); intro. - subst i. simpl. rewrite peq_true. auto. - destruct i; simpl; autorewrite with labels; try reflexivity. - destruct m; rewrite transl_load_store_label; intros; reflexivity. - destruct m; rewrite transl_load_store_label; intros; reflexivity. - destruct s0; reflexivity. - destruct s0; reflexivity. - rewrite peq_false. auto. congruence. - case (snd (crbit_for_cond c)); reflexivity. + forall f i ep k c, + transl_instr f i ep k = OK c -> + find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. +Proof. + unfold transl_instr, Mach.is_label; intros; destruct i; try (monadInv H); + autorewrite with labels; auto. + eapply loadind_label; eauto. + eapply storeind_label; eauto. + destruct ep. eapply loadind_label; eauto. + monadInv H. transitivity (find_label lbl x); eapply loadind_label; eauto. + eapply transl_op_label; eauto. + destruct m; monadInv H; rewrite (transl_memory_access_label _ _ _ _ _ _ _ EQ0); auto. + destruct m; monadInv H; rewrite (transl_memory_access_label _ _ _ _ _ _ _ EQ0); auto. + destruct s0; monadInv H; auto. + destruct s0; monadInv H; auto. + erewrite transl_cond_label. 2: eauto. destruct (snd (crbit_for_cond c0)); auto. Qed. Lemma transl_code_label: - forall f c, - find_label lbl (transl_code f c) = - option_map (transl_code f) (Mach.find_label lbl c). + forall f c ep tc, + transl_code f c ep = OK tc -> + match Mach.find_label lbl c with + | None => find_label lbl tc = None + | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc' + end. Proof. induction c; simpl; intros. - auto. rewrite transl_instr_label. - case (Mach.is_label lbl a). reflexivity. - auto. + inv H. auto. + monadInv H. rewrite (transl_instr_label _ _ _ _ _ EQ0). + generalize (Mach.is_label_correct lbl a). + destruct (Mach.is_label lbl a); intros. + subst a. simpl in EQ. exists x; auto. + eapply IHc; eauto. Qed. Lemma transl_find_label: - forall f, - find_label lbl (transl_function f) = - option_map (transl_code f) (Mach.find_label lbl f.(fn_code)). + forall f tf, + transf_function f = OK tf -> + match Mach.find_label lbl f.(Mach.fn_code) with + | None => find_label lbl tf = None + | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc + end. Proof. - intros. unfold transl_function. simpl. apply transl_code_label. + intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. + monadInv EQ. simpl. + eapply transl_code_label; eauto. Qed. End TRANSL_LABEL. @@ -512,28 +371,26 @@ End TRANSL_LABEL. transition in the generated PPC code. *) Lemma find_label_goto_label: - forall f lbl rs m c' b ofs, + forall f tf lbl rs m c' b ofs, Genv.find_funct_ptr ge b = Some (Internal f) -> + transf_function f = OK tf -> rs PC = Vptr b ofs -> - Mach.find_label lbl f.(fn_code) = Some c' -> - exists rs', - goto_label (transl_function f) lbl rs m = OK rs' m - /\ transl_code_at_pc (rs' PC) b f c' + Mach.find_label lbl f.(Mach.fn_code) = Some c' -> + exists tc', exists rs', + goto_label tf lbl rs m = Next rs' m + /\ transl_code_at_pc ge (rs' PC) f c' false tf tc' /\ forall r, r <> PC -> rs'#r = rs#r. Proof. - intros. - generalize (transl_find_label lbl f). - rewrite H1; simpl. intro. - generalize (label_pos_code_tail lbl (transl_function f) 0 - (transl_code f c') H2). - intros [pos' [A [B C]]]. - exists (rs#PC <- (Vptr b (Int.repr pos'))). - split. unfold goto_label. rewrite A. rewrite H0. auto. + intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. + intros [tc [A B]]. + exploit label_pos_code_tail; eauto. instantiate (1 := 0). + intros [pos' [P [Q R]]]. + exists tc; exists (rs#PC <- (Vptr b (Int.repr pos'))). + split. unfold goto_label. rewrite P. rewrite H1. auto. split. rewrite Pregmap.gss. constructor; auto. - rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in B. - auto. omega. - generalize (functions_transl_no_overflow _ _ H). - omega. + rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in Q. + auto. omega. + generalize (transf_function_no_overflow _ _ H0). omega. intros. apply Pregmap.gso; auto. Qed. @@ -555,108 +412,92 @@ Qed. - Mach register values and PPC register values agree. *) -Inductive match_stack: list Machsem.stackframe -> Prop := - | match_stack_nil: - match_stack nil - | match_stack_cons: forall fb sp ra c s f, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - 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: Machsem.state -> Asm.state -> Prop := +Inductive match_states: Mach.state -> Asm.state -> Prop := | match_states_intro: - 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) - (MEXT: Mem.extends m m'), - match_states (Machsem.State s fb sp c ms m) + forall s f sp c ep ms m m' rs tf tc ra + (STACKS: match_stack ge s m m' ra sp) + (MEXT: Mem.extends m m') + (AT: transl_code_at_pc ge (rs PC) f c ep tf tc) + (AG: agree ms (Vptr sp Int.zero) rs) + (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra) + (DXP: ep = true -> rs#GPR11 = parent_sp s), + match_states (Mach.State s f (Vptr sp Int.zero) c ms m) (Asm.State rs m') | match_states_call: - forall s fb ms m rs m' - (STACKS: match_stack s) - (AG: agree ms (parent_sp s) rs) + forall s fd ms m m' rs fb + (STACKS: match_stack ge s m m' (rs LR) (Mem.nextblock m)) (MEXT: Mem.extends m m') + (AG: agree ms (parent_sp s) rs) (ATPC: rs PC = Vptr fb Int.zero) - (ATLR: rs LR = parent_ra s), - match_states (Machsem.Callstate s fb ms m) + (FUNCT: Genv.find_funct_ptr ge fb = Some fd) + (WTRA: Val.has_type (rs LR) Tint), + match_states (Mach.Callstate s fd ms m) (Asm.State rs m') | match_states_return: - forall s ms m rs m' - (STACKS: match_stack s) - (AG: agree ms (parent_sp s) rs) + forall s ms m m' rs + (STACKS: match_stack ge s m m' (rs PC) (Mem.nextblock m)) (MEXT: Mem.extends m m') - (ATPC: rs PC = parent_ra s), - match_states (Machsem.Returnstate s ms m) + (AG: agree ms (parent_sp s) rs), + match_states (Mach.Returnstate s ms m) (Asm.State rs m'). Lemma exec_straight_steps: - 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' - /\ agree ms2 sp rs2) -> + forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 ra, + match_stack ge s m2 m2' ra sp -> Mem.extends m2 m2' -> + retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra -> + transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc -> + (forall k c (TR: transl_instr f i ep k = OK c), + exists rs2, + exec_straight tge tf c rs1 m1' k rs2 m2' + /\ agree ms2 (Vptr sp Int.zero) rs2 + /\ (r11_is_parent ep i = true -> rs2#GPR11 = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ - match_states (Machsem.State s fb sp c2 ms2 m2) st'. + match_states (Mach.State s f (Vptr sp Int.zero) c ms2 m2) st'. Proof. - intros. destruct H4 as [rs2 [A B]]. + intros. inversion H2; subst. monadInv H7. + exploit H3; eauto. intros [rs2 [A [B C]]]. exists (State rs2 m2'); split. - eapply exec_straight_exec; eauto. + 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) -> +Lemma exec_straight_steps_goto: + forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c' ra, + match_stack ge s m2 m2' ra sp -> + Mem.extends m2 m2' -> + retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra -> + Mach.find_label lbl f.(Mach.fn_code) = Some c' -> + transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc -> + r11_is_parent ep i = false -> + (forall k c (TR: transl_instr f i ep k = OK c), + exists jmp, exists k', exists rs2, + exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' + /\ agree ms2 (Vptr sp Int.zero) rs2 + /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') -> exists st', plus step tge (State rs1 m1') E0 st' /\ - match_states (Machsem.State s fb sp c2 ms2 m2) st'. + match_states (Mach.State s f (Vptr sp Int.zero) c' 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. + intros. inversion H3; subst. monadInv H9. + exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]]. + generalize (functions_transl _ _ _ H7 H8); intro FN. + generalize (transf_function_no_overflow _ _ H8); intro NOOV. + exploit exec_straight_steps_2; eauto. + intros [ofs' [PC2 CT2]]. + exploit find_label_goto_label; eauto. + intros [tc' [rs3 [GOTO [AT' OTH]]]]. + exists (State rs3 m2'); split. + eapply plus_right'. + eapply exec_straight_steps_1; eauto. + econstructor; eauto. + eapply find_instr_tail. eauto. + rewrite C. eexact GOTO. + traceEq. + econstructor; eauto. + apply agree_exten with rs2; auto with asmgen. + congruence. Qed. (** We need to show that, in the simulation diagram, we cannot @@ -667,448 +508,285 @@ Qed. So, the following integer measure will suffice to rule out the unwanted behaviour. *) -Definition measure (s: Machsem.state) : nat := +Definition measure (s: Mach.state) : nat := match s with - | Machsem.State _ _ _ _ _ _ => 0%nat - | Machsem.Callstate _ _ _ _ => 0%nat - | Machsem.Returnstate _ _ _ => 1%nat + | Mach.State _ _ _ _ _ _ => 0%nat + | Mach.Callstate _ _ _ _ => 0%nat + | Mach.Returnstate _ _ _ => 1%nat end. -(** We show the simulation diagram by case analysis on the Mach transition - on the left. Since the proof is large, we break it into one lemma - per transition. *) - -Definition exec_instr_prop (s1: Machsem.state) (t: trace) (s2: Machsem.state) : Prop := - forall s1' (MS: match_states s1 s1'), - (exists s2', plus step tge s1' t s2' /\ match_states s2 s2') - \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat. - - -Lemma exec_Mlabel_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) - (m : mem), - exec_instr_prop (Machsem.State s fb sp (Mlabel lbl :: c) ms m) E0 - (Machsem.State s fb sp c ms m). +Remark preg_of_not_GPR11: forall r, negb (mreg_eq r IT1) = true -> IR GPR11 <> preg_of r. Proof. - intros; red; intros; inv MS. - left; eapply exec_straight_steps; eauto with coqlib. - exists (nextinstr rs); split. - simpl. apply exec_straight_one. reflexivity. reflexivity. - apply agree_nextinstr; auto. + intros. change (IR GPR11) with (preg_of IT1). red; intros. + exploit preg_of_injective; eauto. intros; subst r; discriminate. Qed. -Lemma exec_Mgetstack_prop: - forall (s : list stackframe) (fb : block) (sp : val) (ofs : int) - (ty : typ) (dst : mreg) (c : list Mach.instruction) - (ms : Mach.regset) (m : mem) (v : val), - load_stack m sp ty ofs = Some v -> - exec_instr_prop (Machsem.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0 - (Machsem.State s fb sp c (Regmap.set dst v ms) m). -Proof. - intros; red; intros; inv MS. - unfold load_stack in H. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - 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_set_mreg with rs; auto with ppcgen. congruence. -Qed. +(** This is the simulation diagram. We prove it by case analysis on the Mach transition. *) -Lemma exec_Msetstack_prop: - forall (s : list stackframe) (fb : block) (sp : val) (src : mreg) - (ofs : int) (ty : typ) (c : list Mach.instruction) - (ms : mreg -> val) (m m' : mem), - store_stack m sp ty ofs (ms src) = Some m' -> - exec_instr_prop (Machsem.State s fb sp (Msetstack src ofs ty :: c) ms m) E0 - (Machsem.State s fb sp c ms m'). +Theorem step_simulation: + forall S1 t S2, Mach.step ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. Proof. - intros; red; intros; inv MS. - unfold store_stack in H. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inv WTI. - generalize (preg_val ms sp rs src AG). intro. - exploit Mem.storev_extends; eauto. - intros [m2' [A B]]. + induction 1; intros; inv MS. + +- (* Mlabel *) + left; eapply exec_straight_steps; eauto; intros. + monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split. apply agree_nextinstr; auto. simpl; congruence. + +- (* Mgetstack *) + unfold load_stack in H. + exploit Mem.loadv_extends; eauto. intros [v' [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. - apply agree_exten with rs; auto with ppcgen. -Qed. + left; eapply exec_straight_steps; eauto. intros. simpl in TR. + exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]]. + exists rs'; split. eauto. + split. eapply agree_set_mreg; eauto with asmgen. congruence. + simpl; congruence. -Lemma exec_Mgetparam_prop: - forall (s : list stackframe) (fb : block) (f: Mach.function) (sp : val) - (ofs : int) (ty : typ) (dst : mreg) (c : list Mach.instruction) - (ms : Mach.regset) (m : mem) (v : val), - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (parent_sp s) ty ofs = Some v -> - exec_instr_prop (Machsem.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0 - (Machsem.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. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inv WTI. - unfold load_stack in *. simpl in H0. +- (* Msetstack *) + unfold store_stack in H. + assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. + exploit Mem.storev_extends; eauto. intros [m2' [A B]]. + left; eapply exec_straight_steps; eauto. + eapply match_stack_storev; eauto. + eapply retaddr_stored_at_storev; eauto. + rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. + exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]]. + exists rs'; split. eauto. + split. change (undef_setstack rs) with rs. apply agree_exten with rs0; auto with asmgen. + simpl; intros. rewrite Q; auto with asmgen. + +- (* Mgetparam *) + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H. auto. + intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. + exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'. 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. - apply agree_set_mreg with rs1; auto with ppcgen. - unfold rs1. change (IR GPR11) with (preg_of IT1). - apply agree_nextinstr. apply agree_set_mreg with rs; auto with ppcgen. - intros. apply Pregmap.gso; auto with ppcgen. - congruence. -Qed. - -Lemma exec_Mop_prop: - forall (s : list stackframe) (fb : block) (sp : val) (op : operation) - (args : list mreg) (res : mreg) (c : list Mach.instruction) - (ms : mreg -> val) (m : mem) (v : val), - eval_operation ge sp op ms ## args m = Some v -> - exec_instr_prop (Machsem.State s fb sp (Mop op args res :: c) ms m) E0 - (Machsem.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 _ _))). - intro WTI. - left; eapply exec_straight_steps; eauto with coqlib. - simpl. eapply transl_op_correct; eauto. - rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. -Qed. - -Remark loadv_8_signed_unsigned: - forall m a v, - Mem.loadv Mint8signed m a = Some v -> - exists v', Mem.loadv Mint8unsigned m a = Some v' /\ v = Val.sign_ext 8 v'. -Proof. - unfold Mem.loadv; intros. destruct a; try congruence. - generalize (Mem.load_int8_signed_unsigned m b (Int.unsigned i)). - rewrite H. destruct (Mem.load Mint8unsigned m b (Int.unsigned i)). - simpl; intros. exists v0; split; congruence. +Opaque loadind. + left; eapply exec_straight_steps; eauto; intros. + destruct ep; simpl in TR. +(* GPR11 contains parent *) + exploit loadind_correct. eexact TR. + instantiate (2 := rs0). rewrite DXP; eauto. congruence. + intros [rs1 [P [Q R]]]. + exists rs1; split. eauto. + split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. + simpl; intros. rewrite R; auto with asmgen. + apply preg_of_not_GPR11; auto. +(* GPR11 does not contain parent *) + monadInv TR. + exploit loadind_correct. eexact EQ0. eauto. congruence. intros [rs1 [P [Q R]]]. simpl in Q. + exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. congruence. + intros [rs2 [S [T U]]]. + exists rs2; split. eapply exec_straight_trans; eauto. + split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto. + instantiate (1 := rs1#GPR11 <- (rs2#GPR11)). intros. + rewrite Pregmap.gso; auto with asmgen. + congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' GPR11). congruence. auto with asmgen. + simpl; intros. rewrite U; auto with asmgen. + apply preg_of_not_GPR11; auto. + +- (* Mop *) + assert (eval_operation tge (Vptr sp0 Int.zero) op rs##args m = Some v). + rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. + exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0. + intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. + left; eapply exec_straight_steps; eauto; intros. simpl in TR. + exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. + exists rs2; split. eauto. split. auto. + simpl. destruct op; try congruence. destruct ep; simpl; try congruence. intros. + rewrite R; auto. apply preg_of_not_GPR11; auto. + +- (* Mload *) + assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. + intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. + exploit Mem.loadv_extends; eauto. intros [v' [C D]]. + left; eapply exec_straight_steps; eauto; intros. simpl in TR. + exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. + exists rs2; split. eauto. + split. eapply agree_set_undef_mreg; eauto. congruence. + intros; auto with asmgen. simpl; congruence. -Qed. -Lemma exec_Mload_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (chunk : memory_chunk) (addr : addressing) (args : list mreg) - (dst : mreg) (c : list Mach.instruction) (ms : mreg -> val) - (m : mem) (a v : val), - eval_addressing ge sp addr ms ## args = Some a -> - Mem.loadv chunk m a = Some v -> - exec_instr_prop (Machsem.State s fb sp (Mload chunk addr args dst :: c) ms m) - E0 (Machsem.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 _ _))). - intro WTI; inversion WTI. - assert (eval_addressing tge sp addr ms##args = Some a). +- (* Mstore *) + assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. - left; eapply exec_straight_steps; eauto with coqlib; - destruct chunk; simpl; simpl in H6; - (* all cases but Mint8signed and Mfloat64 *) - try (eapply transl_load_correct; eauto; - intros; simpl; unfold preg_of; rewrite H6; auto; fail). - (* 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'). - 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. - exploit transl_load_correct; eauto. - intros [rs2 [EX1 AG1]]. - 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. - (* Mfloat64 *) - exploit Mem.loadv_float64al32; eauto. intros. clear H0. - eapply transl_load_correct; eauto; - intros; simpl; unfold preg_of; rewrite H6; auto. -Qed. - -Lemma storev_8_signed_unsigned: - forall m a v, - Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. -Proof. - intros. unfold Mem.storev. destruct a; auto. - apply Mem.store_signed_unsigned_8. -Qed. - -Lemma storev_16_signed_unsigned: - forall m a v, - Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. -Proof. - intros. unfold Mem.storev. destruct a; auto. - apply Mem.store_signed_unsigned_16. -Qed. - -Lemma exec_Mstore_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (chunk : memory_chunk) (addr : addressing) (args : list mreg) - (src : mreg) (c : list Mach.instruction) (ms : mreg -> val) - (m m' : mem) (a : val), - eval_addressing ge sp addr ms ## args = Some a -> - Mem.storev chunk m a (ms src) = Some m' -> - exec_instr_prop (Machsem.State s fb sp (Mstore chunk addr args src :: c) ms m) E0 - (Machsem.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; inv WTI. - rewrite <- (eval_addressing_preserved _ _ symbols_preserved) in H. - left; eapply exec_straight_steps_bis; eauto with coqlib. - destruct chunk; simpl; simpl in H6; - try (generalize (Mem.storev_float64al32 _ _ _ _ H0); intros); - try (rewrite storev_8_signed_unsigned in H0); - try (rewrite storev_16_signed_unsigned in H0); - simpl; eapply transl_store_correct; eauto; - (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. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. + intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. + assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. + exploit Mem.storev_extends; eauto. intros [m2' [C D]]. + left; eapply exec_straight_steps; eauto. + eapply match_stack_storev; eauto. + eapply retaddr_stored_at_storev; eauto. + intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. + exists rs2; split. eauto. + split. eapply agree_exten_temps; eauto. intros; auto with asmgen. + simpl; congruence. -Lemma exec_Mcall_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (sig : signature) (ros : mreg + ident) (c : Mach.code) - (ms : Mach.regset) (m : mem) (f : function) (f' : block) - (ra : int), - find_function_ptr ge ros ms = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - return_address_offset f c ra -> - exec_instr_prop (Machsem.State s fb sp (Mcall sig ros :: c) ms m) E0 - (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' ms m). -Proof. - intros; red; intros; inv MS. - assert (f0 = f) by congruence. subst f0. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. +- (* Mcall *) inv AT. - assert (NOOV: list_length_z (transl_function f) <= Int.max_unsigned). - eapply functions_transl_no_overflow; eauto. - destruct ros; simpl in H; simpl transl_code in H7. - (* Indirect call *) - generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1. + assert (NOOV: list_length_z tf <= Int.max_unsigned). + eapply transf_function_no_overflow; eauto. + destruct ros as [rf|fid]; simpl in H; monadInv H3. ++ (* Indirect call *) + exploit Genv.find_funct_inv; eauto. intros [bf EQ2]. + rewrite EQ2 in H; rewrite Genv.find_funct_find_funct_ptr in H. + assert (rs0 x0 = Vptr bf Int.zero). + exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto. + generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1. generalize (code_tail_next_int _ _ _ _ NOOV CT1). intro CT2. - 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). - rewrite RA_EQ. - change (rs3 LR) with (Val.add (Val.add (rs PC) Vone) Vone). - 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. - econstructor. eauto. apply functions_transl. eexact H0. - eapply find_instr_tail. eauto. - simpl. rewrite P2. auto. - apply star_one. econstructor. - change (rs2 PC) with (Val.add (rs PC) Vone). rewrite <- H5. - simpl. auto. - apply functions_transl. eexact H0. - eapply find_instr_tail. eauto. - simpl. reflexivity. + assert (TCA: transl_code_at_pc ge (Vptr b (Int.add (Int.add ofs Int.one) Int.one)) f c false tf x). + econstructor; eauto. + left; econstructor; split. + eapply plus_left. eapply exec_step_internal. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. eauto. + apply star_one. eapply exec_step_internal. Simpl. rewrite <- H0; simpl; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. eauto. traceEq. + econstructor; eauto. 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)). - assert (ATPC: rs2 PC = Vptr f' Int.zero). - change (rs2 PC) with (symbol_offset tge i Int.zero). - unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. - exploit return_address_offset_correct; eauto. constructor; eauto. - intro RA_EQ. - assert (ATLR: rs2 LR = Vptr fb ra). - rewrite RA_EQ. - change (rs2 LR) with (Val.add (rs PC) Vone). - rewrite <- H5. reflexivity. - assert (AG2: agree ms sp rs2). - unfold rs2; auto 8 with ppcgen. - left; exists (State rs2 m'); split. - apply plus_one. econstructor. - eauto. - apply functions_transl. eexact H0. - eapply find_instr_tail. eauto. - simpl. reflexivity. - econstructor; eauto with coqlib. - econstructor; eauto with coqlib. - rewrite RA_EQ. econstructor; eauto. - eapply agree_sp_def; eauto. congruence. -Qed. - -Lemma exec_Mtailcall_prop: - forall (s : list stackframe) (fb stk : block) (soff : int) - (sig : signature) (ros : mreg + ident) (c : list Mach.instruction) - (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m', - find_function_ptr ge ros ms = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> - Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - exec_instr_prop - (Machsem.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 - (Callstate s f' ms m'). -Proof. - intros; red; intros; inv MS. - assert (f0 = f) by congruence. subst f0. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - 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 *) - 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))). + Simpl. rewrite <- H0; eexact TCA. + change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. + simpl. eapply agree_exten; eauto. intros. Simpl. + Simpl. rewrite <- H0. exact I. ++ (* Direct call *) + destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. + generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1. + assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x). + econstructor; eauto. + left; econstructor; split. + apply plus_one. eapply exec_step_internal. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. eauto. + econstructor; eauto. + econstructor; eauto. + rewrite <- H0. eexact TCA. + change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. + simpl. eapply agree_exten; eauto. intros. Simpl. + auto. + rewrite <- H0. exact I. + +- (* Mtailcall *) + inversion AT; subst. + assert (NOOV: list_length_z tf <= Int.max_unsigned). + eapply transf_function_no_overflow; eauto. + rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. + exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. + assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 GPR1) (Vint (fn_retaddr_ofs f))) = Some ra). +Opaque Int.repr. + erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l. + eapply rsa_contains; eauto. + exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]]. + assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')). + apply match_stack_change_bound with stk. + eapply match_stack_free_left; eauto. + eapply match_stack_free_left; eauto. + eapply match_stack_free_right; eauto. + omega. + apply Z.lt_le_incl. change (Mem.valid_block m'' stk). + eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. + eapply retaddr_stored_at_valid; eauto. + destruct ros as [rf|fid]; simpl in H; monadInv H6. ++ (* Indirect call *) + exploit Genv.find_funct_inv; eauto. intros [bf EQ2]. + rewrite EQ2 in H; rewrite Genv.find_funct_find_funct_ptr in H. + assert (rs0 x0 = Vptr bf Int.zero). + exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto. + set (rs2 := nextinstr (rs0#CTR <- (Vptr bf Int.zero))). + set (rs3 := nextinstr (rs2#GPR0 <- ra)). + set (rs4 := nextinstr (rs3#LR <- ra)). 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'0 - (Pbctr :: transl_code f c) rs5 m2'). - simpl. apply exec_straight_step with rs2 m'0. - simpl. rewrite P2. auto. auto. + assert (exec_straight tge tf + (Pmtctr x0 :: Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0 + :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbctr :: x) + rs0 m'0 + (Pbctr :: x) rs5 m2'). + apply exec_straight_step with rs2 m'0. + simpl. rewrite H6. 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. rewrite LOAD2. auto. congruence. auto. + change (rs2 GPR1) with (rs0 GPR1). rewrite C. 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). - simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity. + simpl. change (rs4 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG). + rewrite E. reflexivity. reflexivity. left; exists (State rs6 m2'); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. - change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone) Vone). - rewrite <- H8; simpl. eauto. + change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone). + rewrite <- H3; simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. repeat (eapply code_tail_next_int; auto). eauto. simpl. reflexivity. traceEq. (* match states *) econstructor; eauto. - assert (AG4: agree ms (Vptr stk soff) rs4). - unfold rs4, rs3, rs2; auto 10 with ppcgen. - assert (AG5: agree ms (parent_sp s) rs5). - unfold rs5. apply agree_nextinstr. - split. reflexivity. apply parent_sp_def; auto. - intros. inv AG4. rewrite Pregmap.gso; auto with ppcgen. - unfold rs6; auto with ppcgen. - (* direct call *) - set (rs2 := nextinstr (rs#GPR0 <- (parent_ra s))). - set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). +Hint Resolve agree_nextinstr agree_set_other: asmgen. + assert (AG4: agree rs (Vptr stk Int.zero) rs4). + unfold rs4, rs3, rs2; auto 10 with asmgen. + assert (AG5: agree rs (parent_sp s) rs5). + unfold rs5. apply agree_nextinstr. eapply agree_change_sp. eauto. + eapply parent_sp_def; eauto. + unfold rs6, rs5; auto 10 with asmgen. + reflexivity. + change (rs6 LR) with ra. eapply retaddr_stored_at_type; eauto. ++ (* Direct call *) + destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. + set (rs2 := nextinstr (rs0#GPR0 <- ra)). + set (rs3 := nextinstr (rs2#LR <- ra)). 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'0 - (Pbs i :: transl_code f c) rs4 m2'). - simpl. apply exec_straight_step with rs2 m'0. + set (rs5 := rs4#PC <- (Vptr bf Int.zero)). + assert (exec_straight tge tf + (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0 + :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid :: x) + rs0 m'0 + (Pbs fid :: x) rs4 m2'). + 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. rewrite LOAD2. auto. discriminate. auto. + rewrite C. auto. congruence. 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). - simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity. + simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG). + rewrite E. reflexivity. reflexivity. left; exists (State rs5 m2'); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. - change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). - rewrite <- H8; simpl. eauto. + change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). + rewrite <- H3; simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. repeat (eapply code_tail_next_int; auto). eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. - reflexivity. traceEq. + simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. auto. traceEq. (* match states *) econstructor; eauto. - assert (AG3: agree ms (Vptr stk soff) rs3). - unfold rs3, rs2; auto 10 with ppcgen. - assert (AG4: agree ms (parent_sp s) rs4). - unfold rs4. apply agree_nextinstr. - split. reflexivity. - apply parent_sp_def; auto. - intros. inv AG3. rewrite Pregmap.gso; auto with ppcgen. - unfold rs5; auto with ppcgen. -Qed. +Hint Resolve agree_nextinstr agree_set_other: asmgen. + assert (AG3: agree rs (Vptr stk Int.zero) rs3). + unfold rs3, rs2; auto 10 with asmgen. + assert (AG4: agree rs (parent_sp s) rs4). + unfold rs4. apply agree_nextinstr. eapply agree_change_sp. eauto. + eapply parent_sp_def; eauto. + unfold rs5; auto 10 with asmgen. + reflexivity. + change (rs5 LR) with ra. eapply retaddr_stored_at_type; eauto. -Lemma exec_Mbuiltin_prop: - forall (s : list stackframe) (f : block) (sp : val) - (ms : Mach.regset) (m : mem) (ef : external_function) - (args : list mreg) (res : mreg) (b : list Mach.instruction) - (t : trace) (v : val) (m' : mem), - external_call ef ge ms ## args m t v m' -> - exec_instr_prop (Machsem.State s f sp (Mbuiltin ef args res :: b) ms m) t - (Machsem.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 _ _))). - intro WTI. inv WTI. - inv AT. simpl in H3. - generalize (functions_transl _ _ FIND); intro FN. - generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. +- (* Mbuiltin *) + inv AT. monadInv H3. + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H2); 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. @@ -1116,30 +794,23 @@ Proof. eapply find_instr_tail; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. - econstructor; eauto with coqlib. - 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. - apply agree_nextinstr. apply agree_set_mreg_undef_temps with rs; auto. - rewrite Pregmap.gss. auto. - intros. repeat rewrite Pregmap.gso; auto with ppcgen. -Qed. + econstructor; eauto. + eapply match_stack_extcall; eauto. + intros; eapply external_call_max_perm; eauto. + instantiate (2 := tf); instantiate (1 := x). + Simpl. rewrite <- H0. simpl. econstructor; eauto. + eapply code_tail_next_int; eauto. + apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. + rewrite Pregmap.gss. auto. + intros. Simpl. + eapply retaddr_stored_at_extcall; eauto. + intros; eapply external_call_max_perm; eauto. + congruence. -Lemma exec_Mannot_prop: - forall (s : list stackframe) (f : block) (sp : val) - (ms : Mach.regset) (m : mem) (ef : external_function) - (args : list Mach.annot_param) (b : list Mach.instruction) - (vargs: list val) (t : trace) (v : val) (m' : mem), - Machsem.annot_arguments ms m sp args vargs -> - external_call ef ge vargs m t v m' -> - exec_instr_prop (Machsem.State s f sp (Mannot ef args :: b) ms m) t - (Machsem.State s f sp b ms m'). -Proof. - intros; red; intros; inv MS. - inv AT. simpl in H3. - generalize (functions_transl _ _ FIND); intro FN. - generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. +- (* Mannot *) + inv AT. monadInv H4. + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H3); intro NOOV. exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. exploit external_call_mem_extends; eauto. intros [vres' [m2' [A [B [C D]]]]]. @@ -1148,373 +819,238 @@ Proof. eapply find_instr_tail; eauto. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. - econstructor; eauto with coqlib. + eapply match_states_intro with (ep := false); eauto with coqlib. + eapply match_stack_extcall; eauto. + intros; eapply external_call_max_perm; eauto. unfold nextinstr. rewrite Pregmap.gss. - rewrite <- H1; simpl. econstructor; auto. + rewrite <- H1; simpl. econstructor; eauto. eapply code_tail_next_int; eauto. apply agree_nextinstr. auto. -Qed. + eapply retaddr_stored_at_extcall; eauto. + intros; eapply external_call_max_perm; eauto. + congruence. -Lemma exec_Mgoto_prop: - forall (s : list stackframe) (fb : block) (f : function) (sp : val) - (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) - (m : mem) (c' : Mach.code), - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl (fn_code f) = Some c' -> - exec_instr_prop (Machsem.State s fb sp (Mgoto lbl :: c) ms m) E0 - (Machsem.State s fb sp c' ms m). -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). - intros [rs2 [GOTO [AT2 INV]]]. - left; exists (State rs2 m'); split. +- (* Mgoto *) + inv AT. monadInv H3. + exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. + left; exists (State rs' m'); split. apply plus_one. econstructor; eauto. - apply functions_transl; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl; auto. - econstructor; eauto. - eapply Mach.find_label_incl; eauto. - apply agree_exten with rs; auto with ppcgen. -Qed. - -Lemma exec_Mcond_true_prop: - forall (s : list stackframe) (fb : block) (f : function) (sp : val) - (cond : condition) (args : list mreg) (lbl : Mach.label) - (c : list Mach.instruction) (ms : mreg -> val) (m : mem) - (c' : Mach.code), - eval_condition cond ms ## args m = Some true -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl (fn_code f) = Some c' -> - exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machsem.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 _ _))). - intro WTI. inv WTI. - pose (k1 := - if snd (crbit_for_cond cond) - then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c - else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c). - exploit transl_cond_correct; eauto. - 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). - intros [rs3 [GOTO [AT3 INV3]]]. - 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. - econstructor; eauto. - eapply find_instr_tail. unfold k1 in CT2; rewrite ISSET in CT2. eauto. - simpl. rewrite RES. simpl. auto. + simpl; eauto. econstructor; eauto. - eapply find_instr_tail. unfold k1 in CT2; rewrite ISSET in CT2. eauto. - simpl. rewrite RES. simpl. auto. - traceEq. - econstructor; eauto. - eapply Mach.find_label_incl; eauto. - apply agree_undef_temps with rs2; auto with ppcgen. -Qed. - -Lemma exec_Mcond_false_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (cond : condition) (args : list mreg) (lbl : Mach.label) - (c : list Mach.instruction) (ms : mreg -> val) (m : mem), - eval_condition cond ms ## args m = Some false -> - exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machsem.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. - exploit transl_cond_correct; eauto. - simpl. intros [rs2 [EX [RES AG2]]]. - left; eapply exec_straight_steps; eauto with coqlib. - exists (nextinstr rs2); split. - simpl. eapply exec_straight_trans. eexact EX. - caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES. - apply exec_straight_one. simpl. rewrite RES. reflexivity. - reflexivity. - apply exec_straight_one. simpl. rewrite RES. reflexivity. - reflexivity. - apply agree_nextinstr. apply agree_undef_temps with rs2; auto. -Qed. + eapply agree_exten; eauto with asmgen. + congruence. -Lemma exec_Mjumptable_prop: - forall (s : list stackframe) (fb : block) (f : function) (sp : val) - (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction) - (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label) - (c' : Mach.code), - rs arg = Vint n -> - list_nth_z tbl (Int.unsigned n) = Some lbl -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl (fn_code f) = Some c' -> - exec_instr_prop - (Machsem.State s fb sp (Mjumptable arg tbl :: c) rs m) E0 - (Machsem.State s fb sp c' (undef_temps rs) m). -Proof. - intros; red; intros; inv MS. - assert (f0 = f) by congruence. subst f0. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inv WTI. - exploit list_nth_z_range; eauto. intro RANGE. - assert (SHIFT: Int.unsigned (Int.rolm n (Int.repr 2) (Int.repr (-4))) = Int.unsigned n * 4). - replace (Int.repr (-4)) with (Int.shl Int.mone (Int.repr 2)). - rewrite <- Int.shl_rolm. rewrite Int.shl_mul. - unfold Int.mul. apply Int.unsigned_repr. omega. - compute. reflexivity. - apply Int.mkint_eq. compute. reflexivity. - inv AT. simpl in H7. - set (k1 := Pbtbl GPR12 tbl :: transl_code f c). - set (rs1 := nextinstr (rs0 # GPR12 <- (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))))). - 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'). - apply exec_straight_one. - 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). - intros [rs3 [GOTO [AT3 INV3]]]. - left; exists (State rs3 m'); split. - eapply plus_right'. - eapply exec_straight_steps_1; eauto. - econstructor; eauto. - eapply find_instr_tail. unfold k1 in CT1. eauto. - unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen. - change (rs1 GPR12) with (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))). - lazy iota beta. rewrite SHIFT. rewrite Z_mod_mult. rewrite zeq_true. - rewrite Z_div_mult. - change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq. +- (* Mcond true *) + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. + left; eapply exec_straight_steps_goto; eauto. + intros. simpl in TR. + destruct (transl_cond_correct_1 tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. + rewrite EC in B. + destruct (snd (crbit_for_cond cond)). + (* Pbt, taken *) + econstructor; econstructor; econstructor; split. eexact A. + split. eapply agree_exten_temps; eauto with asmgen. + simpl. rewrite B. reflexivity. + (* Pbf, taken *) + econstructor; econstructor; econstructor; split. eexact A. + split. eapply agree_exten_temps; eauto with asmgen. + simpl. rewrite B. reflexivity. + +- (* Mcond false *) + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. + left; eapply exec_straight_steps; eauto. intros. simpl in TR. + destruct (transl_cond_correct_1 tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. + rewrite EC in B. + econstructor; split. + eapply exec_straight_trans. eexact A. + destruct (snd (crbit_for_cond cond)). + apply exec_straight_one. simpl. rewrite B. reflexivity. auto. + apply exec_straight_one. simpl. rewrite B. reflexivity. auto. + split. eapply agree_exten_temps; eauto with asmgen. + intros; Simpl. + simpl. congruence. + +- (* Mjumptable *) + inv AT. monadInv H5. + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H4); intro NOOV. + exploit find_label_goto_label. eauto. eauto. + instantiate (2 := rs0#GPR12 <- Vundef #CTR <- Vundef). + Simpl. eauto. + eauto. + intros [tc' [rs' [A [B C]]]]. + exploit ireg_val; eauto. rewrite H. intros LD; inv LD. + left; econstructor; split. + apply plus_one. econstructor; eauto. + eapply find_instr_tail; eauto. + simpl. rewrite <- H8. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. econstructor; eauto. - eapply Mach.find_label_incl; eauto. - apply agree_undef_temps with rs0; auto. - intros. rewrite INV3; auto with ppcgen. - unfold rs2. repeat rewrite Pregmap.gso; auto with ppcgen. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. - apply Pregmap.gso; auto with ppcgen. -Qed. + eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simpl. + congruence. -Lemma exec_Mreturn_prop: - forall (s : list stackframe) (fb stk : block) (soff : int) - (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m', - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> - Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - exec_instr_prop (Machsem.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 - (Returnstate s ms m'). -Proof. - intros; red; intros; inv MS. - assert (f0 = f) by congruence. subst f0. - 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))). +- (* Mreturn *) + inversion AT; subst. + assert (NOOV: list_length_z tf <= Int.max_unsigned). + eapply transf_function_no_overflow; eauto. + rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H. auto. simpl. intros [parent' [A B]]. + exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. + assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 GPR1) (Vint (fn_retaddr_ofs f))) = Some ra). +Opaque Int.repr. + erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l. + eapply rsa_contains; eauto. + exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]]. + assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')). + apply match_stack_change_bound with stk. + eapply match_stack_free_left; eauto. + eapply match_stack_free_left; eauto. + eapply match_stack_free_right; eauto. omega. + apply Z.lt_le_incl. change (Mem.valid_block m'' stk). + eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. + eapply retaddr_stored_at_valid; eauto. + monadInv H5. + set (rs2 := nextinstr (rs0#GPR0 <- ra)). + set (rs3 := nextinstr (rs2#LR <- ra)). 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'0 - (Pblr :: transl_code f c) rs4 m2'). + set (rs5 := rs4#PC <- ra). + assert (exec_straight tge tf + (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 + :: Pmtlr GPR0 + :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pblr :: x) rs0 m'0 + (Pblr :: x) 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. - rewrite <- (sp_val _ _ _ AG). simpl. rewrite LOAD2. - reflexivity. discriminate. - unfold rs3. reflexivity. - simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. rewrite LOAD1. rewrite FREE'. reflexivity. - reflexivity. reflexivity. reflexivity. + simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. rewrite C. auto. congruence. + simpl. auto. + simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A. + rewrite <- (sp_val _ _ _ AG). rewrite E. auto. + auto. auto. auto. left; exists (State rs5 m2'); split. (* execution *) 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). - rewrite <- H4. simpl. eauto. - apply functions_transl; eauto. - generalize (functions_transl_no_overflow _ _ H5); intro NOOV. - simpl in H6. eapply find_instr_tail. + econstructor. + change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). + rewrite <- H2. simpl. eauto. + eapply functions_transl; eauto. + eapply find_instr_tail. eapply code_tail_next_int; auto. eapply code_tail_next_int; auto. eapply code_tail_next_int; eauto. reflexivity. traceEq. (* match states *) econstructor; eauto. - 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. 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. -Qed. - -Hypothesis wt_prog: wt_program prog. - -Lemma exec_function_internal_prop: - forall (s : list stackframe) (fb : block) (ms : Mach.regset) - (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block), - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mem.alloc m 0 (fn_stacksize f) = (m1, stk) -> - let sp := Vptr stk Int.zero in - store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 -> - store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> - exec_instr_prop (Machsem.Callstate s fb ms m) E0 - (Machsem.State s fb sp (fn_code f) (undef_temps ms) m3). -Proof. - intros; red; intros; inv MS. - assert (WTF: wt_function f). - generalize (Genv.find_funct_ptr_prop wt_fundef _ _ wt_prog H); intro TY. - inversion TY; auto. - exploit functions_transl; eauto. intro TFIND. - generalize (functions_transl_no_overflow _ _ H); intro NOOV. - 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). + assert (AG3: agree rs (Vptr stk Int.zero) rs3). + unfold rs3, rs2; auto 10 with asmgen. + assert (AG4: agree rs (parent_sp s) rs4). + unfold rs4. apply agree_nextinstr. eapply agree_change_sp; eauto. + eapply parent_sp_def; eauto. + unfold rs5; auto with asmgen. + +- (* internal function *) + exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. + generalize EQ; intros EQ'. monadInv EQ'. + destruct (zlt Int.max_unsigned (list_length_z x0)); inversion EQ1. clear EQ1. + unfold store_stack in *. + exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + intros [m1' [C D]]. + assert (E: Mem.extends m2 m1') by (eapply Mem.free_left_extends; eauto). + exploit Mem.storev_extends. eexact E. eexact H1. eauto. eauto. + intros [m2' [F G]]. + exploit retaddr_stored_at_can_alloc. eexact H. eauto. eauto. eauto. eauto. + auto. auto. auto. auto. eauto. + intros [m3' [P [Q R]]]. (* Execution of function prologue *) + monadInv EQ0. + set (rs2 := nextinstr (rs0#GPR1 <- sp #GPR0 <- Vundef)). + set (rs3 := nextinstr (rs2#GPR0 <- (rs0#LR))). + set (rs4 := nextinstr rs3). assert (EXEC_PROLOGUE: - exec_straight tge (transl_function f) - (transl_function f) rs m' - (transl_code f (fn_code f)) rs4 m3'). - unfold transl_function at 2. + exec_straight tge x + x rs0 m' + x1 rs4 m3'). + rewrite <- H5 at 2. 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. + unfold exec_instr. rewrite C. fold sp. + rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. + simpl. auto. simpl. unfold store1. rewrite gpr_or_zero_not_zero. - 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)). - change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). - rewrite ATPC. simpl. constructor. auto. - eapply code_tail_next_int; auto. - eapply code_tail_next_int; auto. - eapply code_tail_next_int; auto. - change (Int.unsigned Int.zero) with 0. - unfold transl_function. constructor. - assert (AG2: agree ms sp rs2). - split. reflexivity. unfold sp. congruence. - intros. unfold rs2. rewrite nextinstr_inv. - repeat (rewrite Pregmap.gso). inv AG; auto. - auto with ppcgen. auto with ppcgen. auto with ppcgen. - assert (AG4: agree ms sp rs4). - unfold rs4, rs3; auto with ppcgen. + change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). simpl. + rewrite Int.add_zero_l. rewrite P. auto. congruence. + auto. auto. auto. left; exists (State rs4 m3'); split. - (* execution *) - eapply exec_straight_steps_1; eauto. - change (Int.unsigned Int.zero) with 0. constructor. - (* match states *) - econstructor; eauto with coqlib. apply agree_undef_temps with rs4; auto. -Qed. + eapply exec_straight_steps_1; eauto. unfold fn_code; omega. constructor. + econstructor; eauto. + assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto). + rewrite <- STK in STACKS. simpl in F. simpl in H1. + eapply match_stack_invariant; eauto. + intros. eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_free_3; eauto. + eapply Mem.perm_store_2; eauto. unfold block; omega. + intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. + eapply Mem.perm_alloc_1; eauto. + intros. erewrite Mem.load_store_other. 2: eauto. + erewrite Mem.load_store_other. 2: eauto. + eapply Mem.load_alloc_other; eauto. + left; unfold block; omega. + left; unfold block; omega. + change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). + rewrite ATPC. simpl. constructor; eauto. + subst x. unfold fn_code. eapply code_tail_next_int. omega. + eapply code_tail_next_int. omega. + eapply code_tail_next_int. omega. + constructor. + unfold rs4, rs3, rs2. + apply agree_nextinstr. apply agree_set_other; auto. apply agree_set_other; auto. + apply agree_nextinstr. apply agree_set_other; auto. + eapply agree_change_sp; eauto. apply agree_exten_temps with rs0; eauto. + unfold sp; congruence. + congruence. -Lemma exec_function_external_prop: - forall (s : list stackframe) (fb : block) (ms : Mach.regset) - (m : mem) (t0 : trace) (ms' : RegEq.t -> val) - (ef : external_function) (args : list val) (res : val) (m': mem), - Genv.find_funct_ptr ge fb = Some (External ef) -> - external_call ef ge args m t0 res m' -> - Machsem.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> - ms' = Regmap.set (loc_result (ef_sig ef)) res ms -> - exec_instr_prop (Machsem.Callstate s fb ms m) - t0 (Machsem.Returnstate s ms' m'). -Proof. - intros; red; intros; inv MS. +- (* external function *) exploit functions_translated; eauto. - intros [tf [A B]]. simpl in B. inv B. + intros [tf [A B]]. simpl in B. inv B. exploit extcall_arguments_match; eauto. intros [args' [C D]]. - exploit external_call_mem_extends; eauto. + 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. + left; econstructor; split. apply plus_one. eapply exec_step_external; eauto. - eapply external_call_symbols_preserved; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - unfold loc_external_result. - apply agree_set_other; auto with ppcgen. - apply agree_set_mreg with rs; auto. - rewrite Pregmap.gss; auto. - intros; apply Pregmap.gso; auto. -Qed. - -Lemma exec_return_prop: - forall (s : list stackframe) (fb : block) (sp ra : val) - (c : Mach.code) (ms : Mach.regset) (m : mem), - exec_instr_prop (Machsem.Returnstate (Stackframe fb sp ra c :: s) ms m) E0 - (Machsem.State s fb sp c ms m). -Proof. - intros; red; intros; inv MS. inv STACKS. simpl in *. + rewrite Pregmap.gss. apply match_stack_change_bound with (Mem.nextblock m). + eapply match_stack_extcall; eauto. + intros. eapply external_call_max_perm; eauto. + eapply external_call_nextblock; eauto. + unfold loc_external_result. + eapply agree_set_mreg; eauto. + rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. + intros; Simpl. + +- (* return *) + inv STACKS. simpl in *. right. split. omega. split. auto. - econstructor; eauto. rewrite ATPC; auto. + econstructor; eauto. congruence. Qed. -Theorem transf_instr_correct: - forall s1 t s2, Machsem.step ge s1 t s2 -> - exec_instr_prop s1 t s2. -Proof - (Machsem.step_ind ge exec_instr_prop - exec_Mlabel_prop - exec_Mgetstack_prop - exec_Msetstack_prop - exec_Mgetparam_prop - exec_Mop_prop - exec_Mload_prop - exec_Mstore_prop - exec_Mcall_prop - exec_Mtailcall_prop - exec_Mbuiltin_prop - exec_Mannot_prop - exec_Mgoto_prop - exec_Mcond_true_prop - exec_Mcond_false_prop - exec_Mjumptable_prop - exec_Mreturn_prop - exec_function_internal_prop - exec_function_external_prop - exec_return_prop). - Lemma transf_initial_states: - forall st1, Machsem.initial_state prog st1 -> + forall st1, Mach.initial_state prog st1 -> exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. unfold ge0 in *. + exploit functions_translated; eauto. intros [tf [A B]]. econstructor; split. econstructor. eapply Genv.init_mem_transf_partial; eauto. replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero) - with (Vptr fb Int.zero). - econstructor; eauto. constructor. - split. auto. simpl. congruence. - intros. repeat rewrite Pregmap.gso; auto with ppcgen. + with (Vptr b Int.zero). + econstructor; eauto. + constructor. apply Mem.extends_refl. + split. auto. intros. rewrite Regmap.gi. auto. + reflexivity. + exact I. unfold symbol_offset. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. unfold ge; rewrite H1. auto. @@ -1522,21 +1058,22 @@ Qed. Lemma transf_final_states: forall st1 st2 r, - match_states st1 st2 -> Machsem.final_state st1 r -> Asm.final_state st2 r. + match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r. Proof. - intros. inv H0. inv H. constructor. auto. - compute in H1. - exploit (ireg_val _ _ _ R3 AG). auto. rewrite H1; intro. inv H. auto. + intros. inv H0. inv H. inv STACKS. constructor. + auto. + compute in H1. + generalize (preg_val _ _ _ R3 AG). rewrite H1. intros LD; inv LD. auto. Qed. Theorem transf_program_correct: - forward_simulation (Machsem.semantics prog) (Asm.semantics tprog). + forward_simulation (Mach.semantics prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. - exact transf_instr_correct. + exact step_simulation. Qed. End PRESERVATION. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 56cb2240..1e16a0d4 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -13,6 +13,7 @@ (** Correctness proof for PPC generation: auxiliary results. *) Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. @@ -23,11 +24,10 @@ Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. -Require Import Machsem. -Require Import Machtyping. Require Import Asm. Require Import Asmgen. Require Import Conventions. +Require Import Asmgenproof0. (** * Properties of low half/high half decomposition *) @@ -103,308 +103,7 @@ Proof. rewrite Int.sub_idem. apply Int.add_zero. Qed. -(** * Correspondence between Mach registers and PPC registers *) - -Hint Extern 2 (_ <> _) => discriminate: ppcgen. - -(** Mapping from Mach registers to PPC registers. *) - -Lemma preg_of_injective: - forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. -Proof. - destruct r1; destruct r2; simpl; intros; reflexivity || discriminate. -Qed. - -(** Characterization of PPC registers that correspond to Mach registers. *) - -Definition is_data_reg (r: preg) : bool := - match r with - | IR GPR0 => false - | PC => false | LR => false | CTR => false - | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false - | CARRY => false - | _ => true - end. - -Lemma ireg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r) = true. -Proof. - destruct r; reflexivity. -Qed. - -Lemma freg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r) = true. -Proof. - destruct r; reflexivity. -Qed. - -Lemma preg_of_is_data_reg: - forall (r: mreg), is_data_reg (preg_of r) = true. -Proof. - destruct r; reflexivity. -Qed. - -Lemma data_reg_diff: - forall r r', is_data_reg r = true -> is_data_reg r' = false -> r <> r'. -Proof. - intros. congruence. -Qed. - -Lemma ireg_diff: - forall r r', r <> r' -> IR r <> IR r'. -Proof. - intros. congruence. -Qed. - -Lemma diff_ireg: - forall r r', IR r <> IR r' -> r <> r'. -Proof. - intros. congruence. -Qed. - -Hint Resolve ireg_of_is_data_reg freg_of_is_data_reg preg_of_is_data_reg - data_reg_diff ireg_diff diff_ireg: ppcgen. - -Definition is_nontemp_reg (r: preg) : bool := - match r with - | IR GPR0 => false | IR GPR11 => false | IR GPR12 => false - | FR FPR0 => false | FR FPR12 => false | FR FPR13 => false - | PC => false | LR => false | CTR => false - | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false - | CARRY => false - | _ => true - end. - -Remark is_nontemp_is_data: - forall r, is_nontemp_reg r = true -> is_data_reg r = true. -Proof. - destruct r; simpl; try congruence. destruct i; congruence. -Qed. - -Lemma nontemp_reg_diff: - forall r r', is_nontemp_reg r = true -> is_nontemp_reg r' = false -> r <> r'. -Proof. - intros. congruence. -Qed. - -Hint Resolve is_nontemp_is_data nontemp_reg_diff: ppcgen. - -Lemma ireg_of_not_GPR1: - forall r, ireg_of r <> GPR1. -Proof. - intro. case r; discriminate. -Qed. - -Lemma preg_of_not_GPR1: - forall r, preg_of r <> GPR1. -Proof. - intro. case r; discriminate. -Qed. -Hint Resolve ireg_of_not_GPR1 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. *) - -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 -> Val.lessdef (ms r) rs#(preg_of r). -Proof. - 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 -> - Val.lessdef (ms r) rs#(ireg_of r). -Proof. - 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 -> - Val.lessdef (ms r) rs#(freg_of r). -Proof. - intros. replace (FR (freg_of r)) with (preg_of r). eapply preg_val; eauto. - unfold preg_of. rewrite H0. auto. -Qed. - -Lemma sp_val: - forall ms sp rs, - agree ms sp rs -> - sp = rs#GPR1. -Proof. - intros. elim H; auto. -Qed. - -Lemma agree_exten: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, is_data_reg r = true -> rs'#r = rs#r) -> - agree ms sp rs'. -Proof. - intros. inv H. constructor; auto. - intros. rewrite H0; auto with ppcgen. -Qed. - -(** Preservation of register agreement under various assignments. *) - -Lemma agree_set_mreg: - forall ms sp rs r v rs', - agree ms sp rs -> - Val.lessdef v (rs'#(preg_of r)) -> - (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros. inv H. constructor; auto with ppcgen. - intros. unfold Regmap.set. destruct (RegEq.eq r0 r). - subst r0. auto. - rewrite H1; auto with ppcgen. red; intros; elim n; apply preg_of_injective; auto. -Qed. -Hint Resolve agree_set_mreg: ppcgen. - -Lemma agree_set_mireg: - forall ms sp rs r v (rs': regset), - agree ms sp rs -> - Val.lessdef v (rs'#(ireg_of r)) -> - mreg_type r = Tint -> - (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros. eapply agree_set_mreg; eauto. unfold preg_of; rewrite H1; auto. -Qed. -Hint Resolve agree_set_mireg: ppcgen. - -Lemma agree_set_mfreg: - forall ms sp rs r v (rs': regset), - agree ms sp rs -> - Val.lessdef v (rs'#(freg_of r)) -> - mreg_type r = Tfloat -> - (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros. eapply agree_set_mreg; eauto. unfold preg_of; rewrite H1; auto. -Qed. - -Lemma agree_set_other: - forall ms sp rs r v, - agree ms sp rs -> - is_data_reg r = false -> - agree ms sp (rs#r <- v). -Proof. - intros. apply agree_exten with rs. - auto. intros. apply Pregmap.gso. congruence. -Qed. -Hint Resolve agree_set_other: ppcgen. - -Lemma agree_nextinstr: - forall ms sp rs, - agree ms sp rs -> agree ms sp (nextinstr rs). -Proof. - intros. unfold nextinstr. apply agree_set_other. auto. auto. -Qed. -Hint Resolve agree_nextinstr: ppcgen. - -Lemma agree_undef_regs: - forall rl ms sp rs rs', - agree ms sp rs -> - (forall r, is_data_reg r = true -> ~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 with rs; auto. - apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))). - apply agree_set_mreg with rs; auto with ppcgen. - intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of a)). - congruence. 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, is_nontemp_reg r = true -> 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. intuition. - apply H0. destruct r; simpl in *; auto. - destruct i; intuition. destruct f; intuition. -Qed. -Hint Resolve agree_undef_temps: ppcgen. - -Lemma agree_set_mreg_undef_temps: - forall ms sp rs r v rs', - agree ms sp rs -> - Val.lessdef v (rs'#(preg_of r)) -> - (forall r', is_nontemp_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v (undef_temps ms)) sp rs'. -Proof. - intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))). - apply agree_undef_temps with rs; auto. - intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). - congruence. apply H1; auto. - auto. - intros. rewrite Pregmap.gso; auto. -Qed. - -Lemma agree_set_twice_mireg: - forall ms sp rs r v v1 v', - agree (Regmap.set r v1 ms) sp rs -> - mreg_type r = Tint -> - Val.lessdef v v' -> - agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v'). -Proof. - intros. inv H. - split. rewrite Pregmap.gso. auto. - generalize (ireg_of_not_GPR1 r); congruence. - 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. - repeat rewrite Regmap.gso; auto. - rewrite Pregmap.gso. auto. - replace (IR (ireg_of r)) with (preg_of r). - red; intros. elim n. apply preg_of_injective; auto. - unfold preg_of. rewrite H0. auto. -Qed. - -(** Useful properties of the PC and GPR0 registers. *) - -Lemma nextinstr_inv: - forall r rs, r <> PC -> (nextinstr rs)#r = rs#r. -Proof. - intros. unfold nextinstr. apply Pregmap.gso. auto. -Qed. -Hint Resolve nextinstr_inv: ppcgen. +(** Useful properties of the GPR0 registers. *) Lemma gpr_or_zero_not_zero: forall rs r, r <> GPR0 -> gpr_or_zero rs r = rs#r. @@ -416,154 +115,40 @@ Lemma gpr_or_zero_zero: Proof. intros. reflexivity. Qed. -Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: ppcgen. - -(** Connection between Mach and Asm calling conventions for external - functions. *) +Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: asmgen. -Lemma extcall_arg_match: - forall ms sp rs m m' l v, - agree ms sp rs -> - Mem.extends m m' -> - Machsem.extcall_arg ms m sp l v -> - exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'. +Lemma ireg_of_not_GPR0: + forall m r, ireg_of m = OK r -> IR r <> IR GPR0. Proof. - 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. + intros. erewrite <- ireg_of_eq; eauto with asmgen. Qed. +Hint Resolve ireg_of_not_GPR0: asmgen. -Lemma extcall_args_match: - forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> - forall ll vl, - list_forall2 (Machsem.extcall_arg ms m sp) ll vl -> - exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'. +Lemma ireg_of_not_GPR0': + forall m r, ireg_of m = OK r -> r <> GPR0. Proof. - induction 3; intros. - exists (@nil val); split. constructor. constructor. - exploit extcall_arg_match; eauto. intros [v1' [A B]]. - destruct IHlist_forall2 as [vl' [C D]]. - exists (v1' :: vl'); split; constructor; auto. + intros. generalize (ireg_of_not_GPR0 _ _ H). congruence. Qed. +Hint Resolve ireg_of_not_GPR0': asmgen. -Lemma extcall_arguments_match: - forall ms m m' sp rs sg args, - agree ms sp rs -> Mem.extends m m' -> - Machsem.extcall_arguments ms m sp sg args -> - exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'. -Proof. - unfold Machsem.extcall_arguments, Asm.extcall_arguments; intros. - eapply extcall_args_match; eauto. -Qed. +(** Useful simplification tactic *) -(** Translation of arguments to annotations. *) +Ltac Simplif := + ((rewrite nextinstr_inv by eauto with asmgen) + || (rewrite nextinstr_inv1 by eauto with asmgen) + || (rewrite Pregmap.gss) + || (rewrite nextinstr_pc) + || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen. -Lemma annot_arg_match: - forall ms sp rs m m' p v, - agree ms sp rs -> - Mem.extends m m' -> - Machsem.annot_arg ms m sp p v -> - exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'. -Proof. - intros. inv H1; simpl. -(* reg *) - exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto. -(* stack *) - exploit Mem.load_extends; eauto. intros [v' [A B]]. - exists v'; split; auto. - inv H. econstructor; eauto. -Qed. +Ltac Simpl := repeat Simplif. -Lemma annot_arguments_match: - forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> - forall pl vl, - Machsem.annot_arguments ms m sp pl vl -> - exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl' - /\ Val.lessdef_list vl vl'. -Proof. - induction 3; intros. - exists (@nil val); split. constructor. constructor. - exploit annot_arg_match; eauto. intros [v1' [A B]]. - destruct IHlist_forall2 as [vl' [C D]]. - exists (v1' :: vl'); split; constructor; auto. -Qed. - -(** * Execution of straight-line code *) +(** * Correctness of PowerPC constructor functions *) -Section STRAIGHTLINE. +Section CONSTRUCTORS. Variable ge: genv. Variable fn: code. -(** Straight-line code is composed of PPC instructions that execute - in sequence (no branches, no function calls and returns). - The following inductive predicate relates the machine states - before and after executing a straight-line sequence of instructions. - Instructions are taken from the first list instead of being fetched - from memory. *) - -Inductive exec_straight: code -> regset -> mem -> - code -> regset -> mem -> Prop := - | exec_straight_one: - forall i1 c rs1 m1 rs2 m2, - exec_instr ge fn i1 rs1 m1 = OK rs2 m2 -> - rs2#PC = Val.add rs1#PC Vone -> - exec_straight (i1 :: c) rs1 m1 c rs2 m2 - | exec_straight_step: - forall i c rs1 m1 rs2 m2 c' rs3 m3, - exec_instr ge fn i rs1 m1 = OK rs2 m2 -> - rs2#PC = Val.add rs1#PC Vone -> - exec_straight c rs2 m2 c' rs3 m3 -> - exec_straight (i :: c) rs1 m1 c' rs3 m3. - -Lemma exec_straight_trans: - forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, - exec_straight c1 rs1 m1 c2 rs2 m2 -> - exec_straight c2 rs2 m2 c3 rs3 m3 -> - exec_straight c1 rs1 m1 c3 rs3 m3. -Proof. - induction 1; intros. - apply exec_straight_step with rs2 m2; auto. - apply exec_straight_step with rs2 m2; auto. -Qed. - -Lemma exec_straight_two: - forall i1 i2 c rs1 m1 rs2 m2 rs3 m3, - exec_instr ge fn i1 rs1 m1 = OK rs2 m2 -> - exec_instr ge fn i2 rs2 m2 = OK rs3 m3 -> - rs2#PC = Val.add rs1#PC Vone -> - rs3#PC = Val.add rs2#PC Vone -> - exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3. -Proof. - intros. apply exec_straight_step with rs2 m2; auto. - apply exec_straight_one; auto. -Qed. - -Lemma exec_straight_three: - forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4, - exec_instr ge fn i1 rs1 m1 = OK rs2 m2 -> - exec_instr ge fn i2 rs2 m2 = OK rs3 m3 -> - exec_instr ge fn i3 rs3 m3 = OK rs4 m4 -> - rs2#PC = Val.add rs1#PC Vone -> - rs3#PC = Val.add rs2#PC Vone -> - rs4#PC = Val.add rs3#PC Vone -> - exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4. -Proof. - intros. apply exec_straight_step with rs2 m2; auto. - eapply exec_straight_two; eauto. -Qed. - -(** * Correctness of PowerPC constructor functions *) - -Ltac SIMP := - (rewrite nextinstr_inv || rewrite Pregmap.gss || rewrite Pregmap.gso); auto with ppcgen. - (** Properties of comparisons. *) Lemma compare_float_spec: @@ -578,7 +163,7 @@ Proof. split. reflexivity. split. reflexivity. split. reflexivity. - intros. unfold compare_float. repeat SIMP. + intros. unfold compare_float. Simpl. Qed. Lemma compare_sint_spec: @@ -593,7 +178,7 @@ Proof. split. reflexivity. split. reflexivity. split. reflexivity. - intros. unfold compare_sint. repeat SIMP. + intros. unfold compare_sint. Simpl. Qed. Lemma compare_uint_spec: @@ -608,7 +193,7 @@ Proof. split. reflexivity. split. reflexivity. split. reflexivity. - intros. unfold compare_uint. repeat SIMP. + intros. unfold compare_uint. Simpl. Qed. (** Loading a constant. *) @@ -616,35 +201,25 @@ Qed. Lemma loadimm_correct: forall r n k rs m, exists rs', - exec_straight (loadimm r n k) rs m k rs' m + exec_straight ge fn (loadimm r n k) rs m k rs' m /\ rs'#r = Vint n /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'. Proof. intros. unfold loadimm. case (Int.eq (high_s n) Int.zero). (* addi *) - exists (nextinstr (rs#r <- (Vint n))). - split. apply exec_straight_one. - simpl. rewrite Int.add_zero_l. auto. - reflexivity. - split. repeat SIMP. intros; repeat SIMP. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + rewrite Int.add_zero_l. intuition Simpl. (* addis *) generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro. - exists (nextinstr (rs#r <- (Vint n))). - split. apply exec_straight_one. - simpl. rewrite Int.add_commut. - rewrite <- H. rewrite low_high_s. reflexivity. - reflexivity. - split. repeat SIMP. intros; repeat SIMP. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + rewrite <- H. rewrite Int.add_commut. rewrite low_high_s. + intuition Simpl. (* addis + ori *) - pose (rs1 := nextinstr (rs#r <- (Vint (Int.shl (high_u n) (Int.repr 16))))). - exists (nextinstr (rs1#r <- (Vint n))). - split. eapply exec_straight_two. - simpl. rewrite Int.add_zero_l. reflexivity. - simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - unfold Val.or. rewrite low_high_u. reflexivity. - reflexivity. reflexivity. - unfold rs1. split. repeat SIMP. intros; repeat SIMP. + econstructor; split. eapply exec_straight_two. + simpl; eauto. simpl; eauto. auto. auto. + split. Simpl. rewrite Int.add_zero_l. unfold Val.or. rewrite low_high_u. auto. + intros; Simpl. Qed. (** Add integer immediate. *) @@ -654,37 +229,31 @@ Lemma addimm_correct: r1 <> GPR0 -> r2 <> GPR0 -> exists rs', - exec_straight (addimm r1 r2 n k) rs m k rs' m + exec_straight ge fn (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. (* addi *) case (Int.eq (high_s n) Int.zero). - exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))). - split. apply exec_straight_one. - simpl. rewrite gpr_or_zero_not_zero; auto. - reflexivity. - split. repeat SIMP. intros. repeat SIMP. + econstructor; split. apply exec_straight_one. + simpl. rewrite gpr_or_zero_not_zero; eauto. + reflexivity. + intuition Simpl. (* addis *) generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro. - exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))). - split. apply exec_straight_one. - simpl. rewrite gpr_or_zero_not_zero; auto. - generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. intro. - rewrite H2. auto. - reflexivity. - split. repeat SIMP. intros; repeat SIMP. + econstructor; split. apply exec_straight_one. + simpl. rewrite gpr_or_zero_not_zero; auto. auto. + split. Simpl. + generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. congruence. + intros; Simpl. (* addis + addi *) - pose (rs1 := nextinstr (rs#r1 <- (Val.add rs#r2 (Vint (Int.shl (high_s n) (Int.repr 16)))))). - exists (nextinstr (rs1#r1 <- (Val.add rs#r2 (Vint n)))). - split. apply exec_straight_two with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; auto. - simpl. rewrite gpr_or_zero_not_zero; auto. - unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. - reflexivity. reflexivity. - unfold rs1; split. repeat SIMP. intros; repeat SIMP. + econstructor; split. eapply exec_straight_two. + simpl. rewrite gpr_or_zero_not_zero; eauto. + simpl. rewrite gpr_or_zero_not_zero; eauto. + auto. auto. + split. Simpl. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. + intros; Simpl. Qed. (** And integer immediate. *) @@ -694,10 +263,10 @@ Lemma andimm_base_correct: r2 <> GPR0 -> let v := Val.and rs#r2 (Vint n) in exists rs', - exec_straight (andimm_base r1 r2 n k) rs m k rs' m + exec_straight ge fn (andimm_base r1 r2 n k) rs m k rs' m /\ rs'#r1 = v /\ rs'#CR0_2 = Val.cmp Ceq v Vzero - /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'. + /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold andimm_base. case (Int.eq (high_u n) Int.zero). @@ -706,9 +275,9 @@ Proof. generalize (compare_sint_spec (rs#r1 <- v) v Vzero). intros [A [B [C D]]]. split. apply exec_straight_one. reflexivity. reflexivity. - split. rewrite D; auto with ppcgen. SIMP. + split. rewrite D; auto with asmgen. Simpl. split. auto. - intros. rewrite D; auto with ppcgen. SIMP. + intros. rewrite D; auto with asmgen. Simpl. (* andis *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. @@ -718,9 +287,9 @@ Proof. split. apply exec_straight_one. simpl. generalize (low_high_u n). rewrite H0. rewrite Int.or_zero. intro. rewrite H1. reflexivity. reflexivity. - split. rewrite D; auto with ppcgen. SIMP. + split. rewrite D; auto with asmgen. Simpl. split. auto. - intros. rewrite D; auto with ppcgen. SIMP. + intros. rewrite D; auto with asmgen. Simpl. (* loadimm + and *) generalize (loadimm_correct GPR0 n (Pand_ r1 r2 GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTHER1]]]. @@ -731,25 +300,24 @@ Proof. apply exec_straight_one. simpl. rewrite RES1. rewrite (OTHER1 r2). reflexivity. congruence. congruence. reflexivity. - split. rewrite D; auto with ppcgen. SIMP. + split. rewrite D; auto with asmgen. Simpl. split. auto. - intros. rewrite D; auto with ppcgen. SIMP. + intros. rewrite D; auto with asmgen. Simpl. Qed. Lemma andimm_correct: forall r1 r2 n k (rs : regset) m, r2 <> GPR0 -> exists rs', - exec_straight (andimm r1 r2 n k) rs m k rs' m + exec_straight ge fn (andimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = Val.and rs#r2 (Vint n) - /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'. + /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold andimm. destruct (is_rlw_mask n). (* turned into rlw *) - exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))). - split. apply exec_straight_one. simpl. rewrite Val.rolm_zero. auto. reflexivity. - split. SIMP. apply Pregmap.gss. - intros. SIMP. apply Pregmap.gso; auto with ppcgen. + econstructor; split. eapply exec_straight_one. + simpl. rewrite Val.rolm_zero. eauto. auto. + intuition Simpl. (* andimm_base *) destruct (andimm_base_correct r1 r2 n k rs m) as [rs' [A [B [C D]]]]; auto. exists rs'; auto. @@ -761,7 +329,7 @@ Lemma orimm_correct: forall r1 (r2: ireg) n k (rs : regset) m, let v := Val.or rs#r2 (Vint n) in exists rs', - exec_straight (orimm r1 r2 n k) rs m k rs' m + exec_straight ge fn (orimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = v /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -770,8 +338,7 @@ Proof. (* ori *) exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. reflexivity. reflexivity. - split. repeat SIMP. - intros. repeat SIMP. + intuition Simpl. (* oris *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. @@ -779,12 +346,11 @@ Proof. split. apply exec_straight_one. simpl. generalize (low_high_u n). rewrite H. rewrite Int.or_zero. intro. rewrite H0. reflexivity. reflexivity. - split. repeat SIMP. - intros. repeat SIMP. + intuition Simpl. (* oris + ori *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss. rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. - intros. repeat SIMP. + intuition Simpl. + rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. Qed. (** Xor integer immediate. *) @@ -793,7 +359,7 @@ Lemma xorimm_correct: forall r1 (r2: ireg) n k (rs : regset) m, let v := Val.xor rs#r2 (Vint n) in exists rs', - exec_straight (xorimm r1 r2 n k) rs m k rs' m + exec_straight ge fn (xorimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = v /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -802,20 +368,19 @@ Proof. (* xori *) exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. reflexivity. reflexivity. - split. repeat SIMP. intros. repeat SIMP. + intuition Simpl. (* xoris *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. simpl. - generalize (low_high_u_xor n). rewrite H. rewrite Int.xor_zero. + generalize (low_high_u n). rewrite H. rewrite Int.or_zero. intro. rewrite H0. reflexivity. reflexivity. - split. repeat SIMP. intros. repeat SIMP. + intuition Simpl. (* xoris + xori *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss. + intuition Simpl. rewrite Val.xor_assoc. simpl. rewrite low_high_u_xor. reflexivity. - intros. repeat SIMP. Qed. (** Rotate and mask. *) @@ -824,95 +389,108 @@ Lemma rolm_correct: forall r1 r2 amount mask k (rs : regset) m, r1 <> GPR0 -> exists rs', - exec_straight (rolm r1 r2 amount mask k) rs m k rs' m + exec_straight ge fn (rolm r1 r2 amount mask k) rs m k rs' m /\ rs'#r1 = Val.rolm rs#r2 amount mask - /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'. + /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold rolm. destruct (is_rlw_mask mask). (* rlwinm *) - exists (nextinstr (rs#r1 <- (Val.rolm rs#r2 amount mask))). - split. apply exec_straight_one; auto. - split. SIMP. apply Pregmap.gss. - intros. SIMP. apply Pregmap.gso; auto. + econstructor; split. eapply exec_straight_one; simpl; eauto. + intuition Simpl. (* rlwinm ; andimm *) set (rs1 := nextinstr (rs#r1 <- (Val.rolm rs#r2 amount Int.mone))). destruct (andimm_base_correct r1 r1 mask k rs1 m) as [rs' [A [B [C D]]]]; auto. exists rs'. split. eapply exec_straight_step; eauto. auto. auto. - split. rewrite B. unfold rs1. SIMP. rewrite Pregmap.gss. - destruct (rs r2); simpl; auto. unfold Int.rolm. rewrite Int.and_assoc. + split. rewrite B. unfold rs1. rewrite nextinstr_inv; auto with asmgen. + rewrite Pregmap.gss. destruct (rs r2); simpl; auto. + unfold Int.rolm. rewrite Int.and_assoc. decEq; decEq; decEq. rewrite Int.and_commut. apply Int.and_mone. - intros. rewrite D; auto. unfold rs1; SIMP. apply Pregmap.gso; auto. + intros. rewrite D; auto. unfold rs1; Simpl. Qed. (** Indexed memory loads. *) Lemma loadind_correct: - forall (base: ireg) ofs ty dst k (rs: regset) m v, + forall (base: ireg) ofs ty dst k (rs: regset) m v c, + loadind base ofs ty dst k = OK c -> Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v -> - mreg_type dst = ty -> base <> GPR0 -> exists rs', - exec_straight (loadind base ofs ty dst k) rs m k rs' m + exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v /\ forall r, r <> PC -> r <> preg_of dst -> r <> GPR0 -> rs'#r = rs#r. Proof. - intros. unfold loadind. destruct (Int.eq (high_s ofs) Int.zero). -(* one load *) - exists (nextinstr (rs#(preg_of dst) <- v)); split. - unfold preg_of. rewrite H0. - destruct ty; apply exec_straight_one; auto with ppcgen; simpl. - unfold load1. rewrite gpr_or_zero_not_zero; auto. - simpl in *. rewrite H. auto. - unfold load1. rewrite gpr_or_zero_not_zero; auto. - simpl in *. rewrite H. auto. - split. repeat SIMP. intros. repeat SIMP. -(* loadimm + one load *) +Opaque Int.eq. + unfold loadind; intros. destruct ty; monadInv H; simpl in H0. +(* integer *) + rewrite (ireg_of_eq _ _ EQ). + destruct (Int.eq (high_s ofs) Int.zero). + (* one load *) + econstructor; split. apply exec_straight_one. simpl. + unfold load1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. + intuition Simpl. + (* loadimm + load *) + exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. + exists (nextinstr (rs'#x <- v)); split. + eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. + simpl. unfold load2. rewrite C; auto with asmgen. rewrite B. rewrite H0. auto. + intuition Simpl. +(* float *) + rewrite (freg_of_eq _ _ EQ). + destruct (Int.eq (high_s ofs) Int.zero). + (* one load *) + econstructor; split. apply exec_straight_one. simpl. + unfold load1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. + intuition Simpl. + (* loadimm + 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. - unfold preg_of. rewrite H0. - destruct ty; apply exec_straight_one; auto with ppcgen; simpl. - unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto. - unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto. - split. repeat SIMP. - intros. repeat SIMP. + exists (nextinstr (rs'#x <- v)); split. + eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. + simpl. unfold load2. rewrite C; auto with asmgen. rewrite B. rewrite H0. auto. + intuition Simpl. Qed. (** Indexed memory stores. *) Lemma storeind_correct: - forall (base: ireg) ofs ty src k (rs: regset) m m', + forall (base: ireg) ofs ty src k (rs: regset) m m' c, + storeind src base ofs ty k = OK c -> 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 -> exists rs', - exec_straight (storeind src base ofs ty k) rs m k rs' m' + exec_straight ge fn c rs m k rs' m' /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r. Proof. - 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 *) + unfold storeind; intros. + assert (preg_of src <> GPR0) by auto with asmgen. + destruct ty; monadInv H; simpl in H0. +(* integer *) + rewrite (ireg_of_eq _ _ EQ) in *. + destruct (Int.eq (high_s ofs) Int.zero). + (* one store *) + econstructor; split. apply exec_straight_one. simpl. + unfold store1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. + intros; Simpl. + (* loadimm + store *) + exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. + exists (nextinstr rs'); split. + eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. + simpl. unfold store2. rewrite B. rewrite ! C; auto with asmgen. rewrite H0. auto. + intuition Simpl. +(* float *) + rewrite (freg_of_eq _ _ EQ) in *. + destruct (Int.eq (high_s ofs) Int.zero). + (* one store *) + econstructor; split. apply exec_straight_one. simpl. + unfold store1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. + intuition Simpl. + (* loadimm + store *) exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. - assert (rs' base = rs base). apply C; auto with ppcgen. - 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. + exists (nextinstr rs'); split. + eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. + simpl. unfold store2. rewrite B. rewrite ! C; auto with asmgen. rewrite H0. auto. + intuition Simpl. Qed. (** Float comparisons. *) @@ -920,7 +498,7 @@ Qed. Lemma floatcomp_correct: forall cmp (r1 r2: freg) k rs m, exists rs', - exec_straight (floatcomp cmp r1 r2 k) rs m k rs' m + exec_straight ge fn (floatcomp cmp r1 r2 k) rs m k rs' m /\ rs'#(reg_of_crbit (fst (crbit_for_fcmp cmp))) = (if snd (crbit_for_fcmp cmp) then Val.cmpf cmp rs#r1 rs#r2 @@ -938,10 +516,10 @@ Proof. case cmp; tauto. unfold floatcomp. elim H; intro; clear H. exists rs1. - split. generalize H0; intros [EQ|[EQ|[EQ|EQ]]]; subst cmp; + split. destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; apply exec_straight_one; reflexivity. split. - generalize H0; intros [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. + destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. rewrite Val.negate_cmpf_eq. auto. auto. (* two instrs *) @@ -958,155 +536,132 @@ Proof. split. elim H0; intro; subst cmp; simpl. reflexivity. reflexivity. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + intros. Simpl. Qed. -Ltac TypeInv := - match goal with - | H: (List.map ?f ?x = nil) |- _ => - destruct x; [clear H | simpl in H; discriminate] - | H: (List.map ?f ?x = ?hd :: ?tl) |- _ => - destruct x; simpl in H; - [ discriminate | - injection H; clear H; let T := fresh "T" in ( - intros H T; 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. *) +Ltac ArgsInv := + repeat (match goal with + | [ H: Error _ = OK _ |- _ ] => discriminate + | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args + | [ H: bind _ _ = OK _ |- _ ] => monadInv H + | [ H: assertion _ = OK _ |- _ ] => monadInv H + end); + subst; + repeat (match goal with + | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in * + | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in * + end). + Lemma transl_cond_correct_1: - forall cond args k rs m, - map mreg_type args = type_of_condition cond -> + forall cond args k rs m c, + transl_cond cond args k = OK c -> exists rs', - exec_straight (transl_cond cond args k) rs m k rs' m + exec_straight ge fn c rs m k rs' m /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) else Val.notbool (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m))) - /\ forall r, is_data_reg r = true -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. intros. Opaque Int.eq. - destruct cond; simpl in H; TypeInv; simpl; UseTypeInfo. + unfold transl_cond in H; destruct cond; ArgsInv; simpl. (* Ccomp *) - fold (Val.cmp c (rs (ireg_of m0)) (rs (ireg_of m1))). - destruct (compare_sint_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))) - as [A [B [C D]]]. + fold (Val.cmp c0 (rs x) (rs x0)). + destruct (compare_sint_spec rs (rs x) (rs x0)) 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. - auto with ppcgen. + case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. + auto with asmgen. (* Ccompu *) - fold (Val.cmpu (Mem.valid_pointer m) c (rs (ireg_of m0)) (rs (ireg_of m1))). - destruct (compare_uint_spec rs m (rs (ireg_of m0)) (rs (ireg_of m1))) - as [A [B [C D]]]. + fold (Val.cmpu (Mem.valid_pointer m) c0 (rs x) (rs x0)). + destruct (compare_uint_spec rs m (rs x) (rs x0)) 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. - auto with ppcgen. + case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. + auto with asmgen. (* Ccompimm *) - fold (Val.cmp c (rs (ireg_of m0)) (Vint i)). - case (Int.eq (high_s i) Int.zero). - destruct (compare_sint_spec rs (rs (ireg_of m0)) (Vint i)) - as [A [B [C D]]]. + fold (Val.cmp c0 (rs x) (Vint i)). + destruct (Int.eq (high_s i) Int.zero); inv EQ0. + destruct (compare_sint_spec rs (rs x) (Vint i)) as [A [B [C D]]]. econstructor; split. - apply exec_straight_one. simpl. eauto. reflexivity. + apply exec_straight_one. simpl; reflexivity. reflexivity. split. - case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - auto with ppcgen. - generalize (loadimm_correct GPR0 i (Pcmpw (ireg_of m0) GPR0 :: k) rs m). - intros [rs1 [EX1 [RES1 OTH1]]]. - 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. - exists (nextinstr (compare_sint rs1 (rs1 (ireg_of m0)) (Vint i))). + case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. + auto with asmgen. + destruct (loadimm_correct GPR0 i (Pcmpw x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]]. + destruct (compare_sint_spec rs1 (rs x) (Vint i)) as [A [B [C D]]]. + assert (SAME: rs1 x = rs x) by (apply OTH1; eauto with asmgen). + exists (nextinstr (compare_sint rs1 (rs1 x) (Vint i))). split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto. + apply exec_straight_one. simpl. rewrite RES1; rewrite SAME; auto. reflexivity. - split. rewrite H. - case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - intros. rewrite H; rewrite D; auto with ppcgen. + split. rewrite SAME. + case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. + intros. rewrite SAME; rewrite D; auto with asmgen. (* Ccompuimm *) - fold (Val.cmpu (Mem.valid_pointer m) c (rs (ireg_of m0)) (Vint i)). - case (Int.eq (high_u i) Int.zero). - destruct (compare_uint_spec rs m (rs (ireg_of m0)) (Vint i)) - as [A [B [C D]]]. + fold (Val.cmpu (Mem.valid_pointer m) c0 (rs x) (Vint i)). + destruct (Int.eq (high_u i) Int.zero); inv EQ0. + destruct (compare_uint_spec rs m (rs x) (Vint i)) as [A [B [C D]]]. econstructor; split. - apply exec_straight_one. simpl. eauto. reflexivity. + apply exec_straight_one. simpl; reflexivity. reflexivity. split. - case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - auto with ppcgen. - generalize (loadimm_correct GPR0 i (Pcmplw (ireg_of m0) GPR0 :: k) rs m). - intros [rs1 [EX1 [RES1 OTH1]]]. - destruct (compare_uint_spec rs1 m (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. - exists (nextinstr (compare_uint rs1 m (rs1 (ireg_of m0)) (Vint i))). + case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. + auto with asmgen. + destruct (loadimm_correct GPR0 i (Pcmplw x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]]. + destruct (compare_uint_spec rs1 m (rs x) (Vint i)) as [A [B [C D]]]. + assert (SAME: rs1 x = rs x) by (apply OTH1; eauto with asmgen). + exists (nextinstr (compare_uint rs1 m (rs1 x) (Vint i))). split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto. + apply exec_straight_one. simpl. rewrite RES1; rewrite SAME; auto. reflexivity. - split. rewrite H. - case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - intros. rewrite H; rewrite D; auto with ppcgen. + split. rewrite SAME. + case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. + intros. rewrite SAME; rewrite D; auto with asmgen. (* Ccompf *) - fold (Val.cmpf c (rs (freg_of m0)) (rs (freg_of m1))). - destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m) - as [rs' [EX [RES OTH]]]. + fold (Val.cmpf c0 (rs x) (rs x0)). + destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]]. exists rs'. split. auto. split. apply RES. - auto with ppcgen. + auto with asmgen. (* Cnotcompf *) rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. - fold (Val.cmpf c (rs (freg_of m0)) (rs (freg_of m1))). - destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m) - as [rs' [EX [RES OTH]]]. + fold (Val.cmpf c0 (rs x) (rs x0)). + destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]]. exists rs'. split. auto. - split. rewrite RES. destruct (snd (crbit_for_fcmp c)); auto. - auto with ppcgen. + split. rewrite RES. destruct (snd (crbit_for_fcmp c0)); auto. + auto with asmgen. (* Cmaskzero *) - destruct (andimm_base_correct GPR0 (ireg_of m0) i k rs m) - as [rs' [A [B [C D]]]]. auto with ppcgen. + destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]]. + eauto with asmgen. exists rs'. split. assumption. - split. rewrite C. destruct (rs (ireg_of m0)); auto. - auto with ppcgen. + split. rewrite C. destruct (rs x); auto. + auto with asmgen. (* Cmasknotzero *) - destruct (andimm_base_correct GPR0 (ireg_of m0) i k rs m) - as [rs' [A [B [C D]]]]. auto with ppcgen. + destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]]. + eauto with asmgen. exists rs'. split. assumption. - split. rewrite C. destruct (rs (ireg_of m0)); auto. + split. rewrite C. destruct (rs x); auto. fold (option_map negb (Some (Int.eq (Int.and i0 i) Int.zero))). rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. auto. - auto with ppcgen. + auto with asmgen. Qed. Lemma transl_cond_correct_2: - forall cond args k rs m b, - map mreg_type args = type_of_condition cond -> + forall cond args k rs m b c, + transl_cond cond args k = OK c -> eval_condition cond (map rs (map preg_of args)) m = Some b -> exists rs', - exec_straight (transl_cond cond args k) rs m k rs' m + exec_straight ge fn c rs m k rs' m /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then Val.of_bool b else Val.notbool (Val.of_bool b)) - /\ forall r, is_data_reg r = true -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. intros. replace (Val.of_bool b) @@ -1115,14 +670,14 @@ Proof. rewrite H0; auto. Qed. -Lemma transl_cond_correct: - forall cond args k ms sp rs m b m', - map mreg_type args = type_of_condition cond -> +Lemma transl_cond_correct_3: + forall cond args k ms sp rs m b m' c, + transl_cond cond args k = OK c -> agree ms sp rs -> eval_condition cond (map ms args) m = Some b -> Mem.extends m m' -> exists rs', - exec_straight (transl_cond cond args k) rs m' k rs' m' + exec_straight ge fn c rs m' k rs' m' /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then Val.of_bool b @@ -1184,66 +739,60 @@ Transparent Int.eq. Qed. Lemma transl_cond_op_correct: - forall cond args r k rs m, - mreg_type r = Tint -> - map mreg_type args = type_of_condition cond -> + forall cond args r k rs m c, + transl_cond_op cond args r k = OK c -> exists rs', - exec_straight (transl_cond_op cond args r k) rs m k rs' m - /\ rs'#(ireg_of r) = Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) - /\ forall r', is_data_reg r' = true -> r' <> ireg_of r -> rs'#r' = rs#r'. + exec_straight ge fn c rs m k rs' m + /\ rs'#(preg_of r) = Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) + /\ forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r'. Proof. intros until args. unfold transl_cond_op. - destruct (classify_condition cond args); - intros until m; intros TY1 TY2; simpl in TY2. + destruct (classify_condition cond args); intros; monadInv H; simpl; + erewrite ! ireg_of_eq; eauto. (* eq 0 *) - inv TY2. simpl. unfold preg_of; rewrite H0. econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. destruct (rs (ireg_of r)); simpl; auto. + split. Simpl. destruct (rs x0); simpl; auto. apply add_carry_eq0. - intros; repeat SIMP. + intros; Simpl. (* ne 0 *) - inv TY2. simpl. unfold preg_of; rewrite H0. econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. rewrite gpr_or_zero_not_zero; auto with ppcgen. - destruct (rs (ireg_of r)); simpl; auto. + rewrite gpr_or_zero_not_zero; eauto with asmgen. + split. Simpl. destruct (rs x0); simpl; auto. apply add_carry_ne0. - intros; repeat SIMP. + intros; Simpl. (* ge 0 *) - inv TY2. simpl. unfold preg_of; rewrite H0. econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. rewrite Val.rolm_ge_zero. auto. - intros; repeat SIMP. + split. Simpl. rewrite Val.rolm_ge_zero. auto. + intros; Simpl. (* lt 0 *) - inv TY2. simpl. unfold preg_of; rewrite H0. econstructor; split. apply exec_straight_one; simpl; reflexivity. - split. repeat SIMP. rewrite Val.rolm_lt_zero. auto. - intros; repeat SIMP. + split. Simpl. rewrite Val.rolm_lt_zero. auto. + intros; Simpl. (* default *) - set (bit := fst (crbit_for_cond c)). - set (isset := snd (crbit_for_cond c)). + set (bit := fst (crbit_for_cond c)) in *. + set (isset := snd (crbit_for_cond c)) in *. set (k1 := - Pmfcrbit (ireg_of r) bit :: + Pmfcrbit x bit :: (if isset then k - else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)). - generalize (transl_cond_correct_1 c rl k1 rs m TY2). + else Pxori x x (Cint Int.one) :: k)). + generalize (transl_cond_correct_1 c rl k1 rs m c0 EQ0). fold bit; fold isset. intros [rs1 [EX1 [RES1 AG1]]]. destruct isset. (* bit set *) econstructor; split. eapply exec_straight_trans. eexact EX1. - unfold k1. apply exec_straight_one; simpl; reflexivity. - split. repeat SIMP. intros; repeat SIMP. + unfold k1. apply exec_straight_one; simpl; reflexivity. + intuition Simpl. (* bit clear *) econstructor; split. eapply exec_straight_trans. eexact EX1. - unfold k1. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. rewrite RES1. - destruct (eval_condition c rs ## (preg_of ## rl) m). destruct b; auto. auto. - intros; repeat SIMP. + unfold k1. eapply exec_straight_two; simpl; reflexivity. + intuition Simpl. + rewrite RES1. destruct (eval_condition c rs ## (preg_of ## rl) m). destruct b; auto. auto. Qed. (** Translation of arithmetic operations. *) @@ -1251,137 +800,123 @@ Qed. Ltac TranslOpSimpl := econstructor; split; [ apply exec_straight_one; [simpl; eauto | reflexivity] - | split; intros; (repeat SIMP; fail) ]. + | split; intros; Simpl; fail ]. Lemma transl_op_correct_aux: - forall op args res k (rs: regset) m v, - wt_instr (Mop op args res) -> + forall op args res k (rs: regset) m v c, + transl_op op args res k = OK c -> eval_operation ge (rs#GPR1) op (map rs (map preg_of args)) m = Some v -> exists rs', - exec_straight (transl_op op args res k) rs m k rs' m + exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of res) = v /\ forall r, - match op with Omove => is_data_reg r = true | _ => is_nontemp_reg r = true end -> + match op with Omove => data_preg r = true | _ => nontemp_preg r = true end -> r <> preg_of res -> rs'#r = rs#r. Proof. - intros until v; intros WT EV. - inv WT. +Opaque Int.eq. Opaque Int.repr. + intros. unfold transl_op in H; destruct op; ArgsInv; simpl in H0; try (inv H0); try TranslOpSimpl. (* Omove *) - simpl in *. inv EV. - exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))). - split. unfold preg_of. rewrite <- H0. - destruct (mreg_type r1); apply exec_straight_one; auto. - split. repeat SIMP. intros; repeat SIMP. - (* Other instructions *) -Opaque Int.eq. - destruct op; simpl; simpl in H3; injection H3; clear H3; intros; - TypeInv; simpl in *; UseTypeInfo; inv EV; try (TranslOpSimpl). + destruct (preg_of res) eqn:RES; destruct (preg_of m0) eqn:ARG; inv H. + TranslOpSimpl. + TranslOpSimpl. (* Ointconst *) - destruct (loadimm_correct (ireg_of res) i k rs m) as [rs' [A [B C]]]. - exists rs'. split. auto. split. auto. auto with ppcgen. + destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]]. + exists rs'. auto with asmgen. (* Oaddrsymbol *) change (symbol_address ge i i0) with (symbol_offset ge i i0). set (v' := symbol_offset ge i i0). - caseEq (symbol_is_small_data i i0); intro SD. + destruct (symbol_is_small_data i i0) eqn:SD. (* small data *) econstructor; split. apply exec_straight_one; simpl; reflexivity. - split. repeat SIMP. - rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. + split. Simpl. rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero; auto. - intros; repeat SIMP. + intros; Simpl. (* not small data *) Opaque Val.add. econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. rewrite gpr_or_zero_zero. - rewrite gpr_or_zero_not_zero; auto with ppcgen. repeat SIMP. + split. Simpl. rewrite gpr_or_zero_zero. + rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. rewrite (Val.add_commut Vzero). rewrite high_half_zero. rewrite Val.add_commut. rewrite low_high_half. auto. - intros; repeat SIMP. + intros; Simpl. (* Oaddrstack *) - destruct (addimm_correct (ireg_of res) GPR1 i k rs m) as [rs' [EX [RES OTH]]]. - auto with ppcgen. congruence. - exists rs'; auto with ppcgen. + destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen. + exists rs'; auto with asmgen. (* Oaddimm *) - destruct (addimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]; auto with ppcgen. - exists rs'; auto with ppcgen. + destruct (addimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. + exists rs'; auto with asmgen. (* Osubimm *) case (Int.eq (high_s i) Int.zero). TranslOpSimpl. - destruct (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. + destruct (loadimm_correct GPR0 i (Psubfc x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. econstructor; split. eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. - split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. - intros; repeat SIMP. + split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. + intros; Simpl. (* Omulimm *) case (Int.eq (high_s i) Int.zero). TranslOpSimpl. - destruct (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. + destruct (loadimm_correct GPR0 i (Pmullw x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. econstructor; split. eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. - split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. - intros; repeat SIMP. + split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. + intros; Simpl. (* Odivs *) - replace v with (Val.maketotal (Val.divs (rs (ireg_of m0)) (rs (ireg_of m1)))). + replace v with (Val.maketotal (Val.divs (rs x) (rs x0))). TranslOpSimpl. - rewrite H2; auto. + rewrite H1; auto. (* Odivu *) - replace v with (Val.maketotal (Val.divu (rs (ireg_of m0)) (rs (ireg_of m1)))). + replace v with (Val.maketotal (Val.divu (rs x) (rs x0))). TranslOpSimpl. - rewrite H2; auto. + rewrite H1; auto. (* Oand *) - 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]]]. + set (v' := Val.and (rs x) (rs x0)) in *. + pose (rs1 := rs#x1 <- v'). + destruct (compare_sint_spec rs1 v' Vzero) as [A [B [C D]]]. econstructor; split. apply exec_straight_one; simpl; reflexivity. - split. rewrite D; auto with ppcgen. unfold rs1. SIMP. - intros. rewrite D; auto with ppcgen. unfold rs1. SIMP. + split. rewrite D; auto with asmgen. unfold rs1; Simpl. + intros. rewrite D; auto with asmgen. unfold rs1; Simpl. (* Oandimm *) - destruct (andimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]; auto with ppcgen. - exists rs'; auto with ppcgen. + destruct (andimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. + exists rs'; auto with asmgen. (* Oorimm *) - destruct (orimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. - exists rs'; auto with ppcgen. + destruct (orimm_correct x0 x i k rs m) as [rs' [A [B C]]]. + exists rs'; auto with asmgen. (* Oxorimm *) - destruct (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. - exists rs'; auto with ppcgen. + destruct (xorimm_correct x0 x i k rs m) as [rs' [A [B C]]]. + exists rs'; auto with asmgen. (* Onor *) - replace (Val.notint (rs (ireg_of m0))) - with (Val.notint (Val.or (rs (ireg_of m0)) (rs (ireg_of m0)))). + replace (Val.notint (rs x)) + with (Val.notint (Val.or (rs x) (rs x))). TranslOpSimpl. - destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.or_idem. auto. + destruct (rs x); simpl; auto. rewrite Int.or_idem. auto. (* Oshrximm *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. apply Val.shrx_carry. auto. - intros; repeat SIMP. + split. Simpl. apply Val.shrx_carry. auto. + intros; Simpl. (* Orolm *) - destruct (rolm_correct (ireg_of res) (ireg_of m0) i i0 k rs m) as [rs' [A [B C]]]; auto with ppcgen. - exists rs'; auto with ppcgen. - (* Oroli *) - destruct (mreg_eq m0 res). subst m0. - TranslOpSimpl. - econstructor; split. - eapply exec_straight_three; simpl; reflexivity. - split. repeat SIMP. intros; repeat SIMP. + destruct (rolm_correct x0 x i i0 k rs m) as [rs' [A [B C]]]; eauto with asmgen. + exists rs'; auto with asmgen. (* Ointoffloat *) - replace v with (Val.maketotal (Val.intoffloat (rs (freg_of m0)))). + replace v with (Val.maketotal (Val.intoffloat (rs x))). TranslOpSimpl. - rewrite H2; auto. + rewrite H1; auto. (* Ocmp *) - destruct (transl_cond_op_correct c args res k rs m) as [rs' [A [B C]]]; auto. - exists rs'; auto with ppcgen. + destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto. + exists rs'; auto with asmgen. Qed. Lemma transl_op_correct: - forall op args res k ms sp rs m v m', - wt_instr (Mop op args res) -> + forall op args res k ms sp rs m v m' c, + transl_op op args res k = OK c -> agree ms sp rs -> eval_operation ge sp op (map ms args) m = Some v -> Mem.extends m m' -> exists 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'. + exec_straight ge fn c rs m' k rs' m' + /\ agree (Regmap.set res v (undef_op op ms)) sp rs' + /\ forall r, op = Omove -> data_preg r = true -> r <> preg_of res -> rs'#r = rs#r. Proof. intros. exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. @@ -1389,74 +924,67 @@ Proof. exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]]. rewrite <- Q in B. exists rs'; split. eexact P. - unfold undef_op. destruct op; - (apply agree_set_mreg_undef_temps with rs || apply agree_set_mreg with rs); + split. unfold undef_op. destruct op; + (apply agree_set_undef_mreg with rs || apply agree_set_mreg with rs); auto. + intros. subst op. auto. Qed. -Lemma transl_load_store_correct: - forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - addr args (temp: ireg) k ms sp rs m ms' m', +(** Translation of memory accesses *) + +Lemma transl_memory_access_correct: + forall (P: regset -> Prop) mk1 mk2 addr args temp k c (rs: regset) a m m', + transl_memory_access mk1 mk2 addr args temp k = OK c -> + eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a -> + temp <> GPR0 -> (forall cst (r1: ireg) (rs1: regset) k, - eval_addressing ge sp addr (map rs (map preg_of args)) = - Some(Val.add (gpr_or_zero rs1 r1) (const_low ge cst)) -> - (forall (r: preg), r <> PC -> r <> temp -> rs1 r = rs r) -> + Val.add (gpr_or_zero rs1 r1) (const_low ge cst) = a -> + (forall r, 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) k, - eval_addressing ge sp addr (map rs (map preg_of args)) = Some(Val.add rs#r1 rs#r2) -> + exec_straight ge fn (mk1 cst r1 :: k) rs1 m k rs' m' /\ P rs') -> + (forall (r1 r2: ireg) (rs1: regset) k, + Val.add rs1#r1 rs1#r2 = a -> + (forall r, r <> PC -> r <> temp -> rs1 r = rs r) -> exists rs', - 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 -> + exec_straight ge fn (mk2 r1 r2 :: k) rs1 m k rs' m' /\ P rs') -> exists rs', - exec_straight (transl_load_store mk1 mk2 addr args temp k) rs m - k rs' m' - /\ agree ms' sp rs'. + exec_straight ge fn c rs m k rs' m' /\ P rs'. Proof. - intros. destruct addr; simpl in H2; TypeInv; simpl. + intros until m'; intros TR ADDR TEMP MK1 MK2. + unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in ADDR; inv ADDR. (* Aindexed *) case (Int.eq (high_s i) Int.zero). (* Aindexed short *) - apply H. - simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto with ppcgen. - auto. + apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. (* Aindexed long *) - 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; repeat SIMP. rewrite Val.add_assoc. + set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))). + exploit (MK1 (Cint (low_s i)) temp rs1 k). + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. + unfold rs1; Simpl. rewrite Val.add_assoc. Transparent Val.add. simpl. rewrite low_high_s. auto. - intros; unfold rs1; repeat SIMP. + intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto. + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. auto. auto. (* Aindexed2 *) - apply H0. - simpl. UseTypeInfo; auto. + apply MK2; auto. (* Aglobal *) - case_eq (symbol_is_small_data i i0); intro SISD. + destruct (symbol_is_small_data i i0) eqn:SISD; inv TR. (* Aglobal from small data *) - apply H. rewrite gpr_or_zero_zero. simpl const_low. - rewrite small_data_area_addressing; auto. simpl. + apply MK1. simpl. rewrite small_data_area_addressing; auto. unfold symbol_address, symbol_offset. destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero. auto. auto. (* Aglobal general case *) 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. rewrite low_high_half. auto. - discriminate. - intros; unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + exploit (MK1 (Csymbol_low i i0) temp rs1 k). + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. + unfold rs1. Simpl. + unfold const_high, const_low. + rewrite Val.add_commut. rewrite low_high_half. auto. + intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. unfold exec_instr. rewrite gpr_or_zero_zero. @@ -1465,27 +993,24 @@ Transparent Val.add. reflexivity. reflexivity. assumption. assumption. (* Abased *) - 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. + set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (const_high ge (Csymbol_high i i0))))). + exploit (MK1 (Csymbol_low i i0) temp rs1 k). + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. + unfold rs1. Simpl. rewrite Val.add_assoc. unfold const_high, const_low. - set (v := symbol_offset ge i i0). - symmetry. rewrite Val.add_commut. decEq. decEq. - unfold v. rewrite Val.add_commut. rewrite low_high_half. auto. - UseTypeInfo. auto. discriminate. - intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + symmetry. rewrite Val.add_commut. f_equal. f_equal. + rewrite Val.add_commut. rewrite low_high_half. auto. + intros; unfold rs1; Simpl. 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. + unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. assumption. assumption. (* 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#temp <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))). - exploit (H (Cint (low_s i)) temp rs1 k). + destruct (Int.eq (high_s i) Int.zero); inv TR. + apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. + set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s i) (Int.repr 16)))))). + exploit (MK1 (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. simpl. rewrite low_high_s. auto. @@ -1493,120 +1018,149 @@ Transparent Val.add. 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. - rewrite <- (sp_val ms sp rs); auto. auto. + unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. assumption. assumption. Qed. -(** Translation of memory loads. *) +(** Translation of loads *) Lemma transl_load_correct: - forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - 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') -> - (forall (r1 r2: ireg) (rs1: regset), - 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 -> + forall chunk addr args dst k c (rs: regset) m a v, + transl_load chunk addr args dst k = OK c -> + eval_addressing ge (rs#GPR1) addr (map rs (map preg_of 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 GPR12 k) rs m' - k rs' m' - /\ agree (Regmap.set dst v (undef_temps ms)) sp rs'. + exec_straight ge fn c rs m k rs' m + /\ rs'#(preg_of dst) = v + /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs' r = rs r. Proof. intros. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. - unfold PregEq.t. - intros [a' [A B]]. - exploit Mem.loadv_extends; eauto. intros [v' [C D]]. - 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 A in H6. inv H6. rewrite C. auto. - unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen. - apply agree_set_mreg with rs1. - apply agree_undef_temps with rs; auto with ppcgen. - repeat SIMP. - intros; repeat SIMP. -(* mk2 *) - intros. exists (nextinstr (rs#(preg_of dst) <- v')). - split. apply exec_straight_one. rewrite H0. - unfold load2. rewrite A in H6. inv H6. rewrite C. auto. - unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen. - apply agree_set_mreg with rs. - apply agree_undef_temps with rs; auto with ppcgen. - repeat SIMP. - intros; repeat SIMP. -(* not GPR0 *) - congruence. -Qed. - -(** Translation of memory stores. *) + assert (BASE: forall mk1 mk2 k' chunk' v', + transl_memory_access mk1 mk2 addr args GPR12 k' = OK c -> + Mem.loadv chunk' m a = Some 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) -> + (forall (r1 r2: ireg) (rs1: regset), + exec_instr ge fn (mk2 r1 r2) rs1 m = + load2 chunk' (preg_of dst) r1 r2 rs1 m) -> + exists rs', + exec_straight ge fn c rs m k' rs' m + /\ rs'#(preg_of dst) = v' + /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs' r = rs r). + { + intros. eapply transl_memory_access_correct; eauto. congruence. + intros. econstructor; split. apply exec_straight_one. + rewrite H4. unfold load1. rewrite H6. rewrite H3. eauto. + unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen. + intuition Simpl. + intros. econstructor; split. apply exec_straight_one. + rewrite H5. unfold load2. rewrite H6. rewrite H3. eauto. + unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen. + intuition Simpl. + } + destruct chunk; monadInv H. +- (* Mint8signed *) + assert (exists v1, Mem.loadv Mint8unsigned m a = Some v1 /\ v = Val.sign_ext 8 v1). + { + destruct a; simpl in *; try discriminate. + rewrite Mem.load_int8_signed_unsigned in H1. + destruct (Mem.load Mint8unsigned m b (Int.unsigned i)); simpl in H1; inv H1. + exists v0; auto. + } + destruct H as [v1 [LD SG]]. clear H1. + exploit BASE; eauto; erewrite ireg_of_eq by eauto; auto. + intros [rs1 [A [B C]]]. + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. + split. Simpl. congruence. intros. Simpl. +- (* Mint8unsigned *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint816signed *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint16unsigned *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint32 *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mfloat32 *) + eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. +- (* Mfloat64 *) + apply Mem.loadv_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. +- (* Mfloat64al32 *) + eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. +Qed. + +(** Translation of 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' 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' -> - 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'. + forall chunk addr args src k c (rs: regset) m a m', + transl_store chunk addr args src k = OK c -> + eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a -> + Mem.storev chunk m a (rs (preg_of src)) = Some m' -> + exists rs', + exec_straight ge fn c rs m k rs' m' + /\ forall r, r <> PC -> r <> GPR11 -> r <> GPR12 -> r <> FPR13 -> rs' r = rs r. Proof. intros. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. - unfold PregEq.t. - 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]]. - 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 A in H6. inv 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. - apply agree_undef_temps with rs. auto. - intros. rewrite V; auto with ppcgen. SIMP. apply H7; auto with ppcgen. - unfold int_temp_for. destruct (mreg_eq src IT2); auto with ppcgen. -(* mk2 *) - intros. - exploit (H0 r1 r2 rs (nextinstr rs) m1'). - unfold store2. rewrite A in H6. inv 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 with ppcgen. - unfold int_temp_for. destruct (mreg_eq src IT2); congruence. -Qed. - -End STRAIGHTLINE. + assert (TEMP0: int_temp_for src = GPR11 \/ int_temp_for src = GPR12). + unfold int_temp_for. destruct (mreg_eq src IT2); auto. + assert (TEMP1: int_temp_for src <> GPR0). + destruct TEMP0; congruence. + assert (TEMP2: IR (int_temp_for src) <> preg_of src). + unfold int_temp_for. destruct (mreg_eq src IT2). + subst src; simpl; congruence. + change (IR GPR12) with (preg_of IT2). red; intros; elim n. + eapply preg_of_injective; eauto. + assert (BASE: forall mk1 mk2 chunk', + transl_memory_access mk1 mk2 addr args (int_temp_for src) k = OK c -> + Mem.storev chunk' m a (rs (preg_of src)) = Some m' -> + (forall cst (r1: ireg) (rs1: regset), + exec_instr ge fn (mk1 cst r1) rs1 m = + store1 ge chunk' (preg_of src) cst r1 rs1 m) -> + (forall (r1 r2: ireg) (rs1: regset), + exec_instr ge fn (mk2 r1 r2) rs1 m = + store2 chunk' (preg_of src) r1 r2 rs1 m) -> + exists rs', + exec_straight ge fn c rs m k rs' m' + /\ forall r, r <> PC -> r <> GPR11 -> r <> GPR12 -> r <> FPR13 -> rs' r = rs r). + { + intros. eapply transl_memory_access_correct; eauto. + intros. econstructor; split. apply exec_straight_one. + rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. + intros; Simpl. apply H7; auto. destruct TEMP0; congruence. + intros. econstructor; split. apply exec_straight_one. + rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. + intros; Simpl. apply H7; auto. destruct TEMP0; congruence. + } + destruct chunk; monadInv H. +- (* Mint8signed *) + assert (Mem.storev Mint8unsigned m a (rs (preg_of src)) = Some m'). + rewrite <- H1. destruct a; simpl; auto. symmetry. apply Mem.store_signed_unsigned_8. + clear H1. eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint8unsigned *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint16signed *) + assert (Mem.storev Mint16unsigned m a (rs (preg_of src)) = Some m'). + rewrite <- H1. destruct a; simpl; auto. symmetry. apply Mem.store_signed_unsigned_16. + clear H1. eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint16unsigned *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint32 *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mfloat32 *) + rewrite (freg_of_eq _ _ EQ) in H1. + eapply transl_memory_access_correct. eauto. eauto. eauto. + intros. econstructor; split. apply exec_straight_one. + simpl. unfold store1. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. + intros. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. + intros. econstructor; split. apply exec_straight_one. + simpl. unfold store2. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. + intros. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. +- (* Mfloat64 *) + apply Mem.storev_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. +- (* Mfloat64al32 *) + eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. +Qed. + +End CONSTRUCTORS. diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v deleted file mode 100644 index ddbfda65..00000000 --- a/powerpc/Asmgenretaddr.v +++ /dev/null @@ -1,204 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Predictor for return addresses in generated PPC code. - - The [return_address_offset] predicate defined here is used in the - semantics for Mach (module [Machsem]) to determine the - return addresses that are stored in activation records. *) - -Require Import Coqlib. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import Locations. -Require Import Mach. -Require Import Asm. -Require Import Asmgen. - -(** The ``code tail'' of an instruction list [c] is the list of instructions - starting at PC [pos]. *) - -Inductive code_tail: Z -> code -> code -> Prop := - | code_tail_0: forall c, - code_tail 0 c c - | code_tail_S: forall pos i c1 c2, - code_tail pos c1 c2 -> - code_tail (pos + 1) (i :: c1) c2. - -Lemma code_tail_pos: - forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. -Proof. - induction 1. omega. omega. -Qed. - -(** Consider a Mach function [f] and a sequence [c] of Mach instructions - representing the Mach code that remains to be executed after a - function call returns. The predicate [return_address_offset f c ofs] - holds if [ofs] is the integer offset of the PPC instruction - following the call in the PPC code obtained by translating the - code of [f]. Graphically: -<< - Mach function f |--------- Mcall ---------| - Mach code c | |--------| - | \ \ - | \ \ - | \ \ - PPC code | |--------| - PPC function |--------------- Pbl ---------| - - <-------- ofs -------> ->> -*) - -Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop := - | return_address_offset_intro: - forall c f ofs, - code_tail ofs (transl_function f) (transl_code f c) -> - return_address_offset f c (Int.repr ofs). - -(** We now show that such an offset always exists if the Mach code [c] - is a suffix of [f.(fn_code)]. This holds because the translation - from Mach to PPC is compositional: each Mach instruction becomes - zero, one or several PPC instructions, but the order of instructions - is preserved. *) - -Lemma is_tail_code_tail: - forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1. -Proof. - induction 1. exists 0; constructor. - destruct IHis_tail as [ofs CT]. exists (ofs + 1); constructor; auto. -Qed. - -Hint Resolve is_tail_refl: ppcretaddr. - -Ltac IsTail := - auto with ppcretaddr; - match goal with - | [ |- is_tail _ (_ :: _) ] => constructor; IsTail - | [ |- is_tail _ (match ?x with true => _ | false => _ end) ] => destruct x; IsTail - | [ |- is_tail _ (match ?x with left _ => _ | right _ => _ end) ] => destruct x; IsTail - | [ |- is_tail _ (match ?x with nil => _ | _ :: _ => _ end) ] => destruct x; IsTail - | [ |- is_tail _ (match ?x with Tint => _ | Tfloat => _ end) ] => destruct x; IsTail - | [ |- is_tail _ (?f _ _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail - | [ |- is_tail _ (?f _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail - | [ |- is_tail _ (?f _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail - | [ |- is_tail _ (?f _ _ _ ?k) ] => apply is_tail_trans with k; IsTail - | [ |- is_tail _ (?f _ _ ?k) ] => apply is_tail_trans with k; IsTail - | _ => idtac - end. - -Lemma loadimm_tail: - forall r n k, is_tail k (loadimm r n k). -Proof. unfold loadimm; intros; IsTail. Qed. -Hint Resolve loadimm_tail: ppcretaddr. - -Lemma addimm_tail: - forall r1 r2 n k, is_tail k (addimm r1 r2 n k). -Proof. unfold addimm; intros; IsTail. Qed. -Hint Resolve addimm_tail: ppcretaddr. - -Lemma andimm_base_tail: - forall r1 r2 n k, is_tail k (andimm_base r1 r2 n k). -Proof. unfold andimm_base; intros; IsTail. Qed. -Hint Resolve andimm_base_tail: ppcretaddr. - -Lemma andimm_tail: - forall r1 r2 n k, is_tail k (andimm r1 r2 n k). -Proof. unfold andimm; intros; IsTail. Qed. -Hint Resolve andimm_tail: ppcretaddr. - -Lemma orimm_tail: - forall r1 r2 n k, is_tail k (orimm r1 r2 n k). -Proof. unfold orimm; intros; IsTail. Qed. -Hint Resolve orimm_tail: ppcretaddr. - -Lemma xorimm_tail: - forall r1 r2 n k, is_tail k (xorimm r1 r2 n k). -Proof. unfold xorimm; intros; IsTail. Qed. -Hint Resolve xorimm_tail: ppcretaddr. - -Lemma rolm_tail: - forall r1 r2 amount mask k, is_tail k (rolm r1 r2 amount mask k). -Proof. unfold rolm; intros; IsTail. Qed. -Hint Resolve rolm_tail: ppcretaddr. - -Lemma loadind_tail: - forall base ofs ty dst k, is_tail k (loadind base ofs ty dst k). -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. destruct ty; IsTail. Qed. -Hint Resolve storeind_tail: ppcretaddr. - -Lemma floatcomp_tail: - forall cmp r1 r2 k, is_tail k (floatcomp cmp r1 r2 k). -Proof. unfold floatcomp; intros; destruct cmp; IsTail. Qed. -Hint Resolve floatcomp_tail: ppcretaddr. - -Lemma transl_cond_tail: - forall cond args k, is_tail k (transl_cond cond args k). -Proof. unfold transl_cond; intros; destruct cond; IsTail. Qed. -Hint Resolve transl_cond_tail: ppcretaddr. - -Lemma transl_cond_op_tail: - forall cond args r k, is_tail k (transl_cond_op cond args r k). -Proof. - unfold transl_cond_op; intros. - destruct (classify_condition cond args); IsTail. -Qed. -Hint Resolve transl_cond_op_tail: ppcretaddr. - -Lemma transl_op_tail: - forall op args r k, is_tail k (transl_op op args r k). -Proof. - unfold transl_op; intros; destruct op; IsTail. -Qed. -Hint Resolve transl_op_tail: ppcretaddr. - -Lemma transl_load_store_tail: - 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. - -Lemma transl_instr_tail: - forall f i k, is_tail k (transl_instr f i k). -Proof. - unfold transl_instr; intros; destruct i; IsTail. - destruct m; IsTail. - destruct m; IsTail. - destruct s0; IsTail. - destruct s0; IsTail. -Qed. -Hint Resolve transl_instr_tail: ppcretaddr. - -Lemma transl_code_tail: - forall f c1 c2, is_tail c1 c2 -> is_tail (transl_code f c1) (transl_code f c2). -Proof. - induction 1; simpl. constructor. eapply is_tail_trans; eauto with ppcretaddr. -Qed. - -Lemma return_address_exists: - forall f sg ros c, is_tail (Mcall sg ros :: c) f.(fn_code) -> - exists ra, return_address_offset f c ra. -Proof. - intros. assert (is_tail (transl_code f c) (transl_function f)). - unfold transl_function. IsTail. apply transl_code_tail; eauto with coqlib. - destruct (is_tail_code_tail _ _ H0) as [ofs A]. - exists (Int.repr ofs). constructor. auto. -Qed. - - diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index c9203ec6..152a4f7c 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -536,7 +536,8 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc "%s jumptable [ " comment; List.iter (fun l -> fprintf oc "%a " label (transl_label l)) tbl; fprintf oc "]\n"; - fprintf oc " addis %a, %a, %a\n" ireg GPR12 ireg r label_high lbl; + fprintf oc " slwi %a, %a, 2\n" ireg GPR12 ireg r; + fprintf oc " addis %a, %a, %a\n" ireg GPR12 ireg GPR12 label_high lbl; fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12; fprintf oc " mtctr %a\n" ireg GPR12; fprintf oc " bctr\n"; -- cgit