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 --- arm/Asm.v | 213 +++---- arm/Asmgen.v | 456 ++++++++------ arm/Asmgenproof.v | 1648 ++++++++++++++++++++------------------------------- arm/Asmgenproof1.v | 1240 ++++++++++++-------------------------- arm/Asmgenretaddr.v | 217 ------- arm/PrintAsm.ml | 7 +- 6 files changed, 1412 insertions(+), 2369 deletions(-) delete mode 100644 arm/Asmgenretaddr.v (limited to 'arm') diff --git a/arm/Asm.v b/arm/Asm.v index 1e4bfa07..cad71884 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -89,8 +89,13 @@ End PregEq. Module Pregmap := EMap(PregEq). +(** Conventional names for stack pointer ([SP]) and return address ([RA]) *) + +Notation "'SP'" := IR13 (only parsing). +Notation "'RA'" := IR14 (only parsing). + (** The instruction set. Most instructions correspond exactly to - actual instructions of the PowerPC processor. See the PowerPC + actual instructions of the ARM processor. See the ARM reference manuals for more details. Some instructions, described below, are pseudo-instructions: they expand to canned instruction sequences during the printing of the assembly @@ -202,9 +207,9 @@ lbl: .word symbol stack pointer to the address of the bottom of this block. In the printed ASM assembly code, this allocation is: << - mov r12, sp + mov r10, sp sub sp, sp, #sz - str r12, [sp, #pos] + str r10, [sp, #pos] >> This cannot be expressed in our memory model, which does not reflect the fact that stack frames are adjacent and allocated/freed @@ -248,6 +253,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. *) @@ -285,13 +298,13 @@ Variable ge: genv. (** The semantics is purely small-step and defined as a function from the current state (a register set + a memory state) - to either [OK rs' m'] where [rs'] and [m'] are the updated register + to either [Next rs' m'] where [rs'] and [m'] are the updated register set and memory state after execution of the instruction at [rs#PC], - or [Error] if the processor is stuck. *) + or [Stuck] 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]). *) @@ -299,13 +312,13 @@ Inductive outcome: Type := Definition nextinstr (rs: regset) := rs#PC <- (Val.add rs#PC Vone). -Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) := - match label_pos lbl 0 c with - | None => Error +Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := + match label_pos lbl 0 (fn_code f) with + | 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. @@ -343,15 +356,15 @@ Definition eval_shift_addr (sa: shift_addr) (rs: regset) := Definition exec_load (chunk: memory_chunk) (addr: val) (r: preg) (rs: regset) (m: mem) := match Mem.loadv chunk m addr with - | None => Error - | Some v => OK (nextinstr (rs#r <- v)) m + | None => Stuck + | Some v => Next (nextinstr (rs#r <- v)) m end. Definition exec_store (chunk: memory_chunk) (addr: val) (r: preg) (rs: regset) (m: mem) := match Mem.storev chunk m addr (rs r) with - | None => Error - | Some m' => OK (nextinstr rs) m' + | None => Stuck + | Some m' => Next (nextinstr rs) m' end. (** Operations over condition bits. *) @@ -411,33 +424,33 @@ Definition symbol_offset (id: ident) (ofs: int) : val := | None => Vundef end. -Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome := +Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome := match i with | Padd r1 r2 so => - OK (nextinstr (rs#r1 <- (Val.add rs#r2 (eval_shift_op so rs)))) m + Next (nextinstr (rs#r1 <- (Val.add rs#r2 (eval_shift_op so rs)))) m | Pand r1 r2 so => - OK (nextinstr (rs#r1 <- (Val.and rs#r2 (eval_shift_op so rs)))) m + Next (nextinstr (rs#r1 <- (Val.and rs#r2 (eval_shift_op so rs)))) m | Pb lbl => - goto_label c lbl rs m + goto_label f lbl rs m | Pbc bit lbl => match rs#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 f lbl rs m + | _ => Stuck end | Pbsymb id sg => - OK (rs#PC <- (symbol_offset id Int.zero)) m + Next (rs#PC <- (symbol_offset id Int.zero)) m | Pbreg r sg => - OK (rs#PC <- (rs#r)) m + Next (rs#PC <- (rs#r)) m | Pblsymb id sg => - OK (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m + Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m | Pblreg r sg => - OK (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (rs#r)) m + Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (rs#r)) m | Pbic r1 r2 so => - OK (nextinstr (rs#r1 <- (Val.and rs#r2 (Val.notint (eval_shift_op so rs))))) m + Next (nextinstr (rs#r1 <- (Val.and rs#r2 (Val.notint (eval_shift_op so rs))))) m | Pcmp r1 so => - OK (nextinstr (compare_int rs rs#r1 (eval_shift_op so rs) m)) m + Next (nextinstr (compare_int rs rs#r1 (eval_shift_op so rs) m)) m | Peor r1 r2 so => - OK (nextinstr (rs#r1 <- (Val.xor rs#r2 (eval_shift_op so rs)))) m + Next (nextinstr (rs#r1 <- (Val.xor rs#r2 (eval_shift_op so rs)))) m | Pldr r1 r2 sa => exec_load Mint32 (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m | Pldrb r1 r2 sa => @@ -449,22 +462,22 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pldrsh r1 r2 sa => exec_load Mint16signed (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m | Pmov r1 so => - OK (nextinstr (rs#r1 <- (eval_shift_op so rs))) m + Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m | Pmovc bit r1 so => match rs#bit with | Vint n => if Int.eq n Int.zero - then OK (nextinstr rs) m - else OK (nextinstr (rs#r1 <- (eval_shift_op so rs))) m - | _ => OK (nextinstr (rs#r1 <- Vundef)) m + then Next (nextinstr rs) m + else Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m + | _ => Next (nextinstr (rs#r1 <- Vundef)) m end | Pmul r1 r2 r3 => - OK (nextinstr (rs#r1 <- (Val.mul rs#r2 rs#r3))) m + Next (nextinstr (rs#r1 <- (Val.mul rs#r2 rs#r3))) m | Pmvn r1 so => - OK (nextinstr (rs#r1 <- (Val.notint (eval_shift_op so rs)))) m + Next (nextinstr (rs#r1 <- (Val.notint (eval_shift_op so rs)))) m | Porr r1 r2 so => - OK (nextinstr (rs#r1 <- (Val.or rs#r2 (eval_shift_op so rs)))) m + Next (nextinstr (rs#r1 <- (Val.or rs#r2 (eval_shift_op so rs)))) m | Prsb r1 r2 so => - OK (nextinstr (rs#r1 <- (Val.sub (eval_shift_op so rs) rs#r2))) m + Next (nextinstr (rs#r1 <- (Val.sub (eval_shift_op so rs) rs#r2))) m | Pstr r1 r2 sa => exec_store Mint32 (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m | Pstrb r1 r2 sa => @@ -473,47 +486,47 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome exec_store Mint16unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m | Psdiv rd r1 r2 => match Val.divs rs#r1 rs#r2 with - | Some v => OK (nextinstr (rs#rd <- v)) m - | None => Error + | Some v => Next (nextinstr (rs#rd <- v)) m + | None => Stuck end | Psub r1 r2 so => - OK (nextinstr (rs#r1 <- (Val.sub rs#r2 (eval_shift_op so rs)))) m + Next (nextinstr (rs#r1 <- (Val.sub rs#r2 (eval_shift_op so rs)))) m | Pudiv rd r1 r2 => match Val.divu rs#r1 rs#r2 with - | Some v => OK (nextinstr (rs#rd <- v)) m - | None => Error + | Some v => Next (nextinstr (rs#rd <- v)) m + | None => Stuck end (* Floating-point coprocessor instructions *) | Pfcpyd r1 r2 => - OK (nextinstr (rs#r1 <- (rs#r2))) m + Next (nextinstr (rs#r1 <- (rs#r2))) m | Pfabsd r1 r2 => - OK (nextinstr (rs#r1 <- (Val.absf rs#r2))) m + Next (nextinstr (rs#r1 <- (Val.absf rs#r2))) m | Pfnegd r1 r2 => - OK (nextinstr (rs#r1 <- (Val.negf rs#r2))) m + Next (nextinstr (rs#r1 <- (Val.negf rs#r2))) m | Pfaddd r1 r2 r3 => - OK (nextinstr (rs#r1 <- (Val.addf rs#r2 rs#r3))) m + Next (nextinstr (rs#r1 <- (Val.addf rs#r2 rs#r3))) m | Pfdivd r1 r2 r3 => - OK (nextinstr (rs#r1 <- (Val.divf rs#r2 rs#r3))) m + Next (nextinstr (rs#r1 <- (Val.divf rs#r2 rs#r3))) m | Pfmuld r1 r2 r3 => - OK (nextinstr (rs#r1 <- (Val.mulf rs#r2 rs#r3))) m + Next (nextinstr (rs#r1 <- (Val.mulf rs#r2 rs#r3))) m | Pfsubd r1 r2 r3 => - OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m + Next (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m | Pflid r1 f => - OK (nextinstr (rs#r1 <- (Vfloat f))) m + Next (nextinstr (rs#r1 <- (Vfloat f))) m | Pfcmpd r1 r2 => - OK (nextinstr (compare_float rs rs#r1 rs#r2)) m + Next (nextinstr (compare_float rs rs#r1 rs#r2)) m | Pfcmpzd r1 => - OK (nextinstr (compare_float rs rs#r1 (Vfloat Float.zero))) m + Next (nextinstr (compare_float rs rs#r1 (Vfloat Float.zero))) m | Pfsitod r1 r2 => - OK (nextinstr (rs#r1 <- (Val.maketotal (Val.floatofint rs#r2)))) m + Next (nextinstr (rs#r1 <- (Val.maketotal (Val.floatofint rs#r2)))) m | Pfuitod r1 r2 => - OK (nextinstr (rs#r1 <- (Val.maketotal (Val.floatofintu rs#r2)))) m + Next (nextinstr (rs#r1 <- (Val.maketotal (Val.floatofintu rs#r2)))) m | Pftosizd r1 r2 => - OK (nextinstr (rs#r1 <- (Val.maketotal (Val.intoffloat rs#r2)))) m + Next (nextinstr (rs#r1 <- (Val.maketotal (Val.intoffloat rs#r2)))) m | Pftouizd r1 r2 => - OK (nextinstr (rs#r1 <- (Val.maketotal (Val.intuoffloat rs#r2)))) m + Next (nextinstr (rs#r1 <- (Val.maketotal (Val.intuoffloat rs#r2)))) m | Pfcvtsd r1 r2 => - OK (nextinstr (rs#r1 <- (Val.singleoffloat rs#r2))) m + Next (nextinstr (rs#r1 <- (Val.singleoffloat rs#r2))) m | Pfldd r1 r2 n => exec_load Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m | Pflds r1 r2 n => @@ -522,85 +535,63 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome exec_store Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m | Pfsts r1 r2 n => match exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m with - | OK rs' m' => OK (rs'#FR7 <- Vundef) m' - | Error => Error + | Next rs' m' => Next (rs'#FR7 <- Vundef) m' + | Stuck => Stuck end (* Pseudo-instructions *) | Pallocframe sz pos => 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 pos)) rs#IR13 with - | None => Error - | Some m2 => OK (nextinstr (rs #IR12 <- (rs#IR13) #IR13 <- sp)) m2 + | None => Stuck + | Some m2 => Next (nextinstr (rs #IR10 <- (rs#IR13) #IR13 <- sp)) m2 end | Pfreeframe sz pos => match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with - | None => Error + | None => Stuck | Some v => match rs#IR13 with | Vptr stk ofs => match Mem.free m stk 0 sz with - | None => Error - | Some m' => OK (nextinstr (rs#IR13 <- v)) m' + | None => Stuck + | Some m' => Next (nextinstr (rs#IR13 <- v)) m' end - | _ => Error + | _ => Stuck end end | Plabel lbl => - OK (nextinstr rs) m + Next (nextinstr rs) m | Ploadsymbol r1 lbl ofs => - OK (nextinstr (rs#r1 <- (symbol_offset lbl ofs))) m + Next (nextinstr (rs#r1 <- (symbol_offset lbl ofs))) m | Pbtbl r tbl => 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 m - end - else Error - | _ => Error + match list_nth_z tbl (Int.unsigned n) with + | None => Stuck + | Some lbl => goto_label f lbl (rs#IR14 <- Vundef) m + end + | _ => Stuck end - | Pbuiltin ef args res => Error (**r treated specially below *) - | Pannot ef args => Error (**r treated specially below *) + | Pbuiltin ef args res => Stuck (**r treated specially below *) + | Pannot ef args => Stuck (**r treated specially below *) end. (** Translation of the LTL/Linear/Mach view of machine registers - to the ARM view. ARM 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 [ARMgenproof] will show that this never happens. - - Note that no LTL register maps to [IR14]. + to the ARM view. Note that no LTL register maps to [IR14]. This register is reserved as temporary, to be used by the generated ARM code. *) -Definition ireg_of (r: mreg) : ireg := +Definition preg_of (r: mreg) : preg := match r with | R0 => IR0 | R1 => IR1 | R2 => IR2 | R3 => IR3 | R4 => IR4 | R5 => IR5 | R6 => IR6 | R7 => IR7 | R8 => IR8 | R9 => IR9 | R11 => IR11 | IT1 => IR10 | IT2 => IR12 - | _ => IR0 (* should not happen *) - end. - -Definition freg_of (r: mreg) : freg := - match r with | F0 => FR0 | F1 => FR1 | F2 => FR2 | F3 => FR3 | F4 => FR4 | F5 => FR5 | F8 => FR8 | F9 => FR9 | F10 => FR10 | F11 => FR11 | F12 => FR12 | F13 => FR13 | F14 => FR14 | F15 => FR15 | FT1 => FR6 | FT2 => FR7 - | _ => FR0 (* 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. @@ -651,7 +642,7 @@ Inductive step: state -> trace -> state -> Prop := rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_instr (Int.unsigned ofs) (fn_code f) = Some i -> - exec_instr (fn_code f) i rs m = OK rs' m' -> + exec_instr f i rs m = Next rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_builtin: forall b ofs f ef args res rs m t v m', @@ -765,3 +756,27 @@ 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 IR14 => false + | IR _ => true + | FR _ => true + | CR _ => false + | PC => false + end. + +Definition nontemp_preg (r: preg) : bool := + match r with + | IR IR14 => false + | IR IR10 => false + | IR IR12 => false + | IR _ => true + | FR FR6 => false + | FR FR7 => false + | FR _ => true + | CR _ => false + | PC => false + end. diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 05e7010e..562cf221 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -22,6 +22,17 @@ Require Import Locations. Require Import Mach. Require Import Asm. +Open Local Scope string_scope. +Open Local Scope error_monad_scope. + +(** 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. + (** Recognition of integer immediate arguments. - For arithmetic operations, immediates are 8-bit quantities zero-extended and rotated right by 0, 2, 4, ... 30 bits. @@ -130,33 +141,43 @@ Definition transl_cond (cond: condition) (args: list mreg) (k: code) := match cond, args with | Ccomp c, a1 :: a2 :: nil => - Pcmp (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp r1(SOreg r2) :: k) | Ccompu c, a1 :: a2 :: nil => - Pcmp (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp r1 (SOreg r2) :: k) | Ccompshift c s, a1 :: a2 :: nil => - Pcmp (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp r1 (transl_shift s r2) :: k) | Ccompushift c s, a1 :: a2 :: nil => - Pcmp (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp r1 (transl_shift s r2) :: k) | Ccompimm c n, a1 :: nil => - if is_immed_arith n then - Pcmp (ireg_of a1) (SOimm n) :: k - else - loadimm IR14 n (Pcmp (ireg_of a1) (SOreg IR14) :: k) + do r1 <- ireg_of a1; + OK (if is_immed_arith n then + Pcmp r1 (SOimm n) :: k + else + loadimm IR14 n (Pcmp r1 (SOreg IR14) :: k)) | Ccompuimm c n, a1 :: nil => - if is_immed_arith n then - Pcmp (ireg_of a1) (SOimm n) :: k - else - loadimm IR14 n (Pcmp (ireg_of a1) (SOreg IR14) :: k) + do r1 <- ireg_of a1; + OK (if is_immed_arith n then + Pcmp r1 (SOimm n) :: k + else + loadimm IR14 n (Pcmp r1 (SOreg IR14) :: k)) | Ccompf cmp, a1 :: a2 :: nil => - Pfcmpd (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmpd r1 r2 :: k) | Cnotcompf cmp, a1 :: a2 :: nil => - Pfcmpd (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmpd r1 r2 :: k) | Ccompfzero cmp, a1 :: nil => - Pfcmpzd (freg_of a1) :: k + do r1 <- freg_of a1; + OK (Pfcmpzd r1 :: k) | Cnotcompfzero cmp, a1 :: nil => - Pfcmpzd (freg_of a1) :: k + do r1 <- freg_of a1; + OK (Pfcmpzd r1 :: k) | _, _ => - k (**r never happens for well-typed code *) + Error(msg "Asmgen.transl_cond") end. Definition crbit_for_signed_cmp (cmp: comparison) := @@ -217,115 +238,159 @@ Definition crbit_for_cond (cond: condition) := 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 => Pmov (ireg_of r) (SOreg (ireg_of a1)) :: k - | Tfloat => Pfcpyd (freg_of r) (freg_of a1) :: k + match preg_of res, preg_of a1 with + | IR r, IR a => OK (Pmov r (SOreg a) :: k) + | FR r, FR a => OK (Pfcpyd 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 => - Pflid (freg_of r) f :: k + do r <- freg_of res; + OK (Pflid r f :: k) | Oaddrsymbol s ofs, nil => - Ploadsymbol (ireg_of r) s ofs :: k + do r <- ireg_of res; + OK (Ploadsymbol r s ofs :: k) | Oaddrstack n, nil => - addimm (ireg_of r) IR13 n k + do r <- ireg_of res; + OK (addimm r IR13 n k) | Oadd, a1 :: a2 :: nil => - Padd (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd r r1 (SOreg r2) :: k) | Oaddshift s, a1 :: a2 :: nil => - Padd (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd r r1 (transl_shift s r2) :: k) | Oaddimm n, a1 :: nil => - addimm (ireg_of r) (ireg_of a1) n k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (addimm r r1 n k) | Osub, a1 :: a2 :: nil => - Psub (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub r r1 (SOreg r2) :: k) | Osubshift s, a1 :: a2 :: nil => - Psub (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub r r1 (transl_shift s r2) :: k) | Orsubshift s, a1 :: a2 :: nil => - Prsb (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Prsb r r1 (transl_shift s r2) :: k) | Orsubimm n, a1 :: nil => - rsubimm (ireg_of r) (ireg_of a1) n k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (rsubimm r r1 n k) | Omul, a1 :: a2 :: nil => - if ireg_eq (ireg_of r) (ireg_of a1) - || ireg_eq (ireg_of r) (ireg_of a2) - then Pmul IR14 (ireg_of a1) (ireg_of a2) :: Pmov (ireg_of r) (SOreg IR14) :: k - else Pmul (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (if ireg_eq r r1 || ireg_eq r r2 + then Pmul IR14 r1 r2 :: Pmov r (SOreg IR14) :: k + else Pmul r r1 r2 :: k) | Odiv, a1 :: a2 :: nil => - Psdiv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psdiv r r1 r2 :: k) | Odivu, a1 :: a2 :: nil => - Pudiv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pudiv r r1 r2 :: k) | Oand, a1 :: a2 :: nil => - Pand (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand r r1 (SOreg r2) :: k) | Oandshift s, a1 :: a2 :: nil => - Pand (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand r r1 (transl_shift s r2) :: k) | Oandimm n, a1 :: nil => - andimm (ireg_of r) (ireg_of a1) n k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (andimm r r1 n k) | Oor, a1 :: a2 :: nil => - Porr (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr r r1 (SOreg r2) :: k) | Oorshift s, a1 :: a2 :: nil => - Porr (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr r r1 (transl_shift s r2) :: k) | Oorimm n, a1 :: nil => - orimm (ireg_of r) (ireg_of a1) n k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (orimm r r1 n k) | Oxor, a1 :: a2 :: nil => - Peor (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor r r1 (SOreg r2) :: k) | Oxorshift s, a1 :: a2 :: nil => - Peor (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor r r1 (transl_shift s r2) :: k) | Oxorimm n, a1 :: nil => - xorimm (ireg_of r) (ireg_of a1) n k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (xorimm r r1 n k) | Obic, a1 :: a2 :: nil => - Pbic (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic r r1 (SOreg r2) :: k) | Obicshift s, a1 :: a2 :: nil => - Pbic (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic r r1 (transl_shift s r2) :: k) | Onot, a1 :: nil => - Pmvn (ireg_of r) (SOreg (ireg_of a1)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (Pmvn r (SOreg r1) :: k) | Onotshift s, a1 :: nil => - Pmvn (ireg_of r) (transl_shift s (ireg_of a1)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (Pmvn r (transl_shift s r1) :: k) | Oshl, a1 :: a2 :: nil => - Pmov (ireg_of r) (SOlslreg (ireg_of a1) (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pmov r (SOlslreg r1 r2) :: k) | Oshr, a1 :: a2 :: nil => - Pmov (ireg_of r) (SOasrreg (ireg_of a1) (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pmov r (SOasrreg r1 r2) :: k) | Oshru, a1 :: a2 :: nil => - Pmov (ireg_of r) (SOlsrreg (ireg_of a1) (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pmov r (SOlsrreg r1 r2) :: k) | Oshift s, a1 :: nil => - Pmov (ireg_of r) (transl_shift s (ireg_of a1)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (Pmov r (transl_shift s r1) :: k) | Oshrximm n, a1 :: nil => - Pcmp (ireg_of a1) (SOimm Int.zero) :: - addimm IR14 (ireg_of a1) (Int.sub (Int.shl Int.one n) Int.one) - (Pmovc CRge IR14 (SOreg (ireg_of a1)) :: - Pmov (ireg_of r) (SOasrimm IR14 n) :: k) + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (Pcmp r1 (SOimm Int.zero) :: + addimm IR14 r1 (Int.sub (Int.shl Int.one n) Int.one) + (Pmovc CRge IR14 (SOreg r1) :: + Pmov r (SOasrimm IR14 n) :: k)) | Onegf, a1 :: nil => - Pfnegd (freg_of r) (freg_of a1) :: k + do r <- freg_of res; do r1 <- freg_of a1; + OK (Pfnegd r r1 :: k) | Oabsf, a1 :: nil => - Pfabsd (freg_of r) (freg_of a1) :: k + do r <- freg_of res; do r1 <- freg_of a1; + OK (Pfabsd r r1 :: k) | Oaddf, a1 :: a2 :: nil => - Pfaddd (freg_of r) (freg_of a1) (freg_of a2) :: k + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfaddd r r1 r2 :: k) | Osubf, a1 :: a2 :: nil => - Pfsubd (freg_of r) (freg_of a1) (freg_of a2) :: k + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfsubd r r1 r2 :: k) | Omulf, a1 :: a2 :: nil => - Pfmuld (freg_of r) (freg_of a1) (freg_of a2) :: k + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfmuld r r1 r2 :: k) | Odivf, a1 :: a2 :: nil => - Pfdivd (freg_of r) (freg_of a1) (freg_of a2) :: k + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfdivd r r1 r2 :: k) | Osingleoffloat, a1 :: nil => - Pfcvtsd (freg_of r) (freg_of a1) :: k + do r <- freg_of res; do r1 <- freg_of a1; + OK (Pfcvtsd r r1 :: k) | Ointoffloat, a1 :: nil => - Pftosizd (ireg_of r) (freg_of a1) :: k + do r <- ireg_of res; do r1 <- freg_of a1; + OK (Pftosizd r r1 :: k) | Ointuoffloat, a1 :: nil => - Pftouizd (ireg_of r) (freg_of a1) :: k + do r <- ireg_of res; do r1 <- freg_of a1; + OK (Pftouizd r r1 :: k) | Ofloatofint, a1 :: nil => - Pfsitod (freg_of r) (ireg_of a1) :: k + do r <- freg_of res; do r1 <- ireg_of a1; + OK (Pfsitod r r1 :: k) | Ofloatofintu, a1 :: nil => - Pfuitod (freg_of r) (ireg_of a1) :: k + do r <- freg_of res; do r1 <- ireg_of a1; + OK (Pfuitod r r1 :: k) | Ocmp cmp, _ => + do r <- ireg_of res; transl_cond cmp args - (Pmov (ireg_of r) (SOimm Int.zero) :: - Pmovc (crbit_for_cond cmp) (ireg_of r) (SOimm Int.one) :: + (Pmov r (SOimm Int.zero) :: + Pmovc (crbit_for_cond cmp) r (SOimm Int.one) :: 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 transl_shift_addr (s: shift) (r: ireg) : shift_addr := match s with @@ -335,62 +400,106 @@ Definition transl_shift_addr (s: shift) (r: ireg) : shift_addr := | Sror n => SAror r (s_amount n) end. -Definition transl_load_store +Definition transl_memory_access (mk_instr_imm: ireg -> int -> instruction) (mk_instr_gen: option (ireg -> shift_addr -> instruction)) (is_immed: int -> bool) - (addr: addressing) (args: list mreg) (k: code) : code := + (addr: addressing) (args: list mreg) (k: code) := match addr, args with | Aindexed n, a1 :: nil => - if is_immed n then - mk_instr_imm (ireg_of a1) n :: k - else - addimm IR14 (ireg_of a1) n - (mk_instr_imm IR14 Int.zero :: k) + do r1 <- ireg_of a1; + OK (if is_immed n then + mk_instr_imm r1 n :: k + else + addimm IR14 r1 n + (mk_instr_imm IR14 Int.zero :: k)) | Aindexed2, a1 :: a2 :: nil => - match mk_instr_gen with - | Some f => - f (ireg_of a1) (SAreg (ireg_of a2)) :: k - | None => - Padd IR14 (ireg_of a1) (SOreg (ireg_of a2)) :: - mk_instr_imm IR14 Int.zero :: k - end + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (match mk_instr_gen with + | Some f => + f r1 (SAreg r2) :: k + | None => + Padd IR14 r1 (SOreg r2) :: + mk_instr_imm IR14 Int.zero :: k + end) | Aindexed2shift s, a1 :: a2 :: nil => - match mk_instr_gen with - | Some f => - f (ireg_of a1) (transl_shift_addr s (ireg_of a2)) :: k - | None => - Padd IR14 (ireg_of a1) (transl_shift s (ireg_of a2)) :: - mk_instr_imm IR14 Int.zero :: k - end + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (match mk_instr_gen with + | Some f => + f r1 (transl_shift_addr s r2) :: k + | None => + Padd IR14 r1 (transl_shift s r2) :: + mk_instr_imm IR14 Int.zero :: k + end) | Ainstack n, nil => - if is_immed n then - mk_instr_imm IR13 n :: k - else - addimm IR14 IR13 n - (mk_instr_imm IR14 Int.zero :: k) + OK (if is_immed n then + mk_instr_imm IR13 n :: k + else + addimm IR14 IR13 n (mk_instr_imm IR14 Int.zero :: k)) | _, _ => - (* should not happen *) k + Error(msg "Asmgen.transl_memory_access") end. -Definition transl_load_store_int +Definition transl_memory_access_int (mk_instr: ireg -> ireg -> shift_addr -> instruction) (is_immed: int -> bool) - (rd: mreg) (addr: addressing) (args: list mreg) (k: code) := - transl_load_store - (fun r n => mk_instr (ireg_of rd) r (SAimm n)) - (Some (mk_instr (ireg_of rd))) + (dst: mreg) (addr: addressing) (args: list mreg) (k: code) := + do rd <- ireg_of dst; + transl_memory_access + (fun r n => mk_instr rd r (SAimm n)) + (Some (mk_instr rd)) is_immed addr args k. -Definition transl_load_store_float +Definition transl_memory_access_float (mk_instr: freg -> ireg -> int -> instruction) (is_immed: int -> bool) - (rd: mreg) (addr: addressing) (args: list mreg) (k: code) := - transl_load_store - (mk_instr (freg_of rd)) + (dst: mreg) (addr: addressing) (args: list mreg) (k: code) := + do rd <- freg_of dst; + transl_memory_access + (mk_instr rd) None is_immed addr args k. +Definition transl_load (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (dst: mreg) (k: code) := + match chunk with + | Mint8signed => + transl_memory_access_int Pldrsb is_immed_mem_small dst addr args k + | Mint8unsigned => + transl_memory_access_int Pldrb is_immed_mem_word dst addr args k + | Mint16signed => + transl_memory_access_int Pldrsh is_immed_mem_small dst addr args k + | Mint16unsigned => + transl_memory_access_int Pldrh is_immed_mem_small dst addr args k + | Mint32 => + transl_memory_access_int Pldr is_immed_mem_word dst addr args k + | Mfloat32 => + transl_memory_access_float Pflds is_immed_mem_float dst addr args k + | Mfloat64 | Mfloat64al32 => + transl_memory_access_float Pfldd is_immed_mem_float dst addr args k + end. + +Definition transl_store (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (src: mreg) (k: code) := + match chunk with + | Mint8signed => + transl_memory_access_int Pstrb is_immed_mem_small src addr args k + | Mint8unsigned => + transl_memory_access_int Pstrb is_immed_mem_word src addr args k + | Mint16signed => + transl_memory_access_int Pstrh is_immed_mem_small src addr args k + | Mint16unsigned => + transl_memory_access_int Pstrh is_immed_mem_small src addr args k + | Mint32 => + transl_memory_access_int Pstr is_immed_mem_word src addr args k + | Mfloat32 => + transl_memory_access_float Pfsts is_immed_mem_float src addr args k + | Mfloat64 | Mfloat64al32 => + transl_memory_access_float Pfstd is_immed_mem_float src addr args k + end. + +(** Accessing data in the stack frame. *) + Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) := if is_immed_mem_word ofs then Pldr dst base (SAimm ofs) :: k @@ -407,8 +516,8 @@ Definition loadind_float (base: ireg) (ofs: int) (dst: freg) (k: code) := Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := match ty with - | Tint => loadind_int base ofs (ireg_of dst) k - | Tfloat => loadind_float base ofs (freg_of dst) k + | Tint => do r <- ireg_of dst; OK (loadind_int base ofs r k) + | Tfloat => do r <- freg_of dst; OK (loadind_float base ofs r k) end. Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) := @@ -427,8 +536,8 @@ Definition storeind_float (src: freg) (base: ireg) (ofs: int) (k: code) := Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := match ty with - | Tint => storeind_int (ireg_of src) base ofs k - | Tfloat => storeind_float (freg_of src) base ofs k + | Tint => do r <- ireg_of src; OK (storeind_int r base ofs k) + | Tfloat => do r <- freg_of src; OK (storeind_float r base ofs k) end. (** Translation of arguments to annotations *) @@ -441,80 +550,71 @@ 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) + (r10_is_parent: bool) (k: code) := match i with | Mgetstack ofs ty dst => loadind IR13 ofs ty dst k | Msetstack src ofs ty => storeind src IR13 ofs ty k | Mgetparam ofs ty dst => - loadind_int IR13 f.(fn_link_ofs) IR14 (loadind IR14 ofs ty dst k) + do c <- loadind IR10 ofs ty dst k; + OK (if r10_is_parent + then c + else loadind_int IR13 f.(fn_link_ofs) IR10 c) | Mop op args res => transl_op op args res k | Mload chunk addr args dst => - match chunk with - | Mint8signed => - transl_load_store_int Pldrsb is_immed_mem_small dst addr args k - | Mint8unsigned => - transl_load_store_int Pldrb is_immed_mem_word dst addr args k - | Mint16signed => - transl_load_store_int Pldrsh is_immed_mem_small dst addr args k - | Mint16unsigned => - transl_load_store_int Pldrh is_immed_mem_small dst addr args k - | Mint32 => - transl_load_store_int Pldr is_immed_mem_word dst addr args k - | Mfloat32 => - transl_load_store_float Pflds is_immed_mem_float dst addr args k - | Mfloat64 | Mfloat64al32 => - transl_load_store_float Pfldd is_immed_mem_float dst addr args k - end + transl_load chunk addr args dst k | Mstore chunk addr args src => - match chunk with - | Mint8signed => - transl_load_store_int Pstrb is_immed_mem_small src addr args k - | Mint8unsigned => - transl_load_store_int Pstrb is_immed_mem_word src addr args k - | Mint16signed => - transl_load_store_int Pstrh is_immed_mem_small src addr args k - | Mint16unsigned => - transl_load_store_int Pstrh is_immed_mem_small src addr args k - | Mint32 => - transl_load_store_int Pstr is_immed_mem_word src addr args k - | Mfloat32 => - transl_load_store_float Pfsts is_immed_mem_float src addr args k - | Mfloat64 | Mfloat64al32 => - transl_load_store_float Pfstd is_immed_mem_float src addr args k - end - | Mcall sig (inl r) => - Pblreg (ireg_of r) sig :: k + transl_store chunk addr args src k + | Mcall sig (inl arg) => + do r <- ireg_of arg; OK (Pblreg r sig :: k) | Mcall sig (inr symb) => - Pblsymb symb sig :: k - | Mtailcall sig (inl r) => - loadind_int IR13 f.(fn_retaddr_ofs) IR14 - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg (ireg_of r) sig :: k) + OK (Pblsymb symb sig :: k) + | Mtailcall sig (inl arg) => + do r <- ireg_of arg; + OK (loadind_int IR13 f.(fn_retaddr_ofs) IR14 + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg r sig :: k)) | Mtailcall sig (inr symb) => - loadind_int IR13 f.(fn_retaddr_ofs) IR14 - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb sig :: k) + OK (loadind_int IR13 f.(fn_retaddr_ofs) IR14 + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb sig :: 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 => transl_cond cond args (Pbc (crbit_for_cond cond) lbl :: k) | Mjumptable arg tbl => - Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) :: - Pbtbl IR14 tbl :: k + do r <- ireg_of arg; + OK (Pbtbl r tbl :: k) | Mreturn => - loadind_int IR13 f.(fn_retaddr_ofs) IR14 - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 f.(Mach.fn_sig) :: k) + OK (loadind_int IR13 f.(fn_retaddr_ofs) IR14 + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pbreg IR14 f.(Mach.fn_sig) :: k)) end. -Definition transl_code (f: Mach.function) (il: list Mach.instruction) := - List.fold_right (transl_instr f) nil il. +(** Translation of a code sequence *) + +Definition r10_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. + +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (r10p: bool) := + match il with + | nil => OK nil + | i1 :: il' => + do k <- transl_code f il' (r10_is_parent r10p i1); + transl_instr f i1 r10p k + end. (** Translation of a whole function. Note that we must check that the generated code contains less than [2^32] instructions, @@ -522,24 +622,16 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) := around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - mkfunction f.(Mach.fn_sig) - (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) :: - transl_code f f.(Mach.fn_code)). - -Fixpoint code_size (c: code) : Z := - match c with - | nil => 0 - | instr :: c' => code_size c' + 1 - end. - -Open Local Scope string_scope. + do c <- transl_code f f.(Mach.fn_code) true; + OK (mkfunction f.(Mach.fn_sig) + (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) :: c)). Definition transf_function (f: Mach.function) : res Asm.function := - let tf := transl_function f in - if zlt Int.max_unsigned (code_size tf.(fn_code)) - then Errors.Error (msg "code size exceeded") - else Errors.OK tf. + do tf <- transl_function f; + if zlt Int.max_unsigned (list_length_z tf.(fn_code)) + then Error (msg "code size exceeded") + else OK tf. Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := transf_partial_fundef transf_function f. diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 365917cb..21becf12 100644 --- a/arm/Asmgenproof.v +++ b/arm/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. @@ -59,27 +57,14 @@ 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 (code_size (fn_code (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) -> - code_size (fn_code (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 (code_size (fn_code (transl_function f)))); simpl; intro. - congruence. intro; omega. + destruct (functions_translated _ _ H) as [tf' [A B]]. + rewrite A. monadInv B. f_equal. congruence. Qed. Lemma varinfo_preserved: @@ -92,191 +77,40 @@ 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_size_pos: - forall fn, code_size fn >= 0. +Lemma transf_function_no_overflow: + forall f tf, + transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned. Proof. - induction fn; simpl; omega. -Qed. - -Remark code_tail_bounds: - forall fn ofs i c, - code_tail ofs fn (i :: c) -> 0 <= ofs < code_size fn. -Proof. - assert (forall ofs fn c, code_tail ofs fn c -> - forall i c', c = i :: c' -> 0 <= ofs < code_size fn). - induction 1; intros; simpl. - rewrite H. simpl. generalize (code_size_pos c'). omega. - 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, - code_size 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 ARM 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) (fn_code (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 ARM 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_code fn) c rs m c' rs' m' -> - code_size (fn_code 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_code 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_code fn) c rs m c' rs' m' -> - code_size (fn_code 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_code fn) c -> - exists ofs', - rs'#PC = Vptr b ofs' - /\ code_tail (Int.unsigned ofs') (fn_code 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 (fn_code 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 (fn_code (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 (fn_code (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 - [ARMgen.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. *) @@ -293,7 +127,7 @@ Lemma label_pos_code_tail: exists pos', label_pos lbl pos c = Some pos' /\ code_tail (pos' - pos) c c' - /\ pos < pos' <= pos + code_size c. + /\ pos < pos' <= pos + list_length_z c. Proof. induction c. simpl; intros. discriminate. @@ -302,12 +136,12 @@ Proof. intro EQ; injection EQ; intro; subst c'. exists (pos + 1). split. auto. split. replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. - generalize (code_size_pos c). omega. + rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]]. exists pos'. split. auto. split. replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega. constructor. auto. - omega. + rewrite list_length_z_cons. omega. Qed. (** The following lemmas show that the translation from Mach to ARM @@ -399,9 +233,9 @@ Proof. Qed. 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 ty. + intros. destruct ty; monadInv H. apply loadind_int_label. unfold loadind_float. destruct (is_immed_mem_float ofs); autorewrite with labels; auto. @@ -415,102 +249,115 @@ Proof. Qed. Remark storeind_label: - forall base ofs ty src k, find_label lbl (storeind src base ofs ty k) = find_label lbl k. + forall base ofs ty src k c, storeind src base ofs ty k = OK c -> find_label lbl c = find_label lbl k. Proof. - intros; unfold storeind. destruct ty. + intros. destruct ty; monadInv H. apply storeind_int_label. unfold storeind_float. destruct (is_immed_mem_float ofs); autorewrite with labels; auto. Qed. + Hint Rewrite loadind_int_label loadind_label storeind_int_label storeind_label: labels. +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). + 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]]). + unfold transl_cond; intros; destruct cond; ArgsInv; auto. destruct (is_immed_arith i); autorewrite with labels; auto. destruct (is_immed_arith i); autorewrite with labels; auto. Qed. -Hint Rewrite transl_cond_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 (ireg_eq (ireg_of r) (ireg_of m) || ireg_eq (ireg_of r) (ireg_of m0)); reflexivity. - transitivity (find_label lbl - (addimm IR14 (ireg_of m) (Int.sub (Int.shl Int.one i) Int.one) - (Pmovc CRge IR14 (SOreg (ireg_of m)) - :: Pmov (ireg_of r) (SOasrimm IR14 i) :: k))). - unfold find_label; auto. autorewrite with labels. reflexivity. + unfold transl_op; intros; destruct op; ArgsInv; autorewrite with labels; auto. + destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; auto. + destruct (ireg_eq x x0 || ireg_eq x x1); auto. + simpl. autorewrite with labels; auto. + erewrite transl_cond_label by eauto; auto. Qed. -Hint Rewrite transl_op_label: labels. -Remark transl_load_store_label: +Remark transl_memory_access_label: forall (mk_instr_imm: ireg -> int -> instruction) (mk_instr_gen: option (ireg -> shift_addr -> instruction)) (is_immed: int -> bool) - (addr: addressing) (args: list mreg) (k: code), + (addr: addressing) (args: list mreg) c k, + transl_memory_access mk_instr_imm mk_instr_gen is_immed addr args k = OK c -> (forall r n, is_label lbl (mk_instr_imm r n) = false) -> (match mk_instr_gen with | None => True | Some f => forall r sa, is_label lbl (f r sa) = false end) -> - find_label lbl (transl_load_store mk_instr_imm mk_instr_gen is_immed addr args k) = find_label lbl k. + find_label lbl c = find_label lbl k. Proof. - intros; unfold transl_load_store. - destruct addr; destruct args; try (destruct args); try (destruct args); - try reflexivity. - destruct (is_immed i); autorewrite with labels; simpl; rewrite H; auto. - destruct mk_instr_gen. simpl. rewrite H0. auto. - simpl. rewrite H. auto. - destruct mk_instr_gen. simpl. rewrite H0. auto. - simpl. rewrite H. auto. - destruct (is_immed i); autorewrite with labels; simpl; rewrite H; auto. + unfold transl_memory_access; intros; destruct addr; ArgsInv; auto. + destruct (is_immed i); autorewrite with labels; simpl; rewrite H0; auto. + destruct mk_instr_gen. simpl. rewrite H1. auto. + simpl. rewrite H0. auto. + destruct mk_instr_gen. simpl. rewrite H1. auto. + simpl. rewrite H0. auto. + destruct (is_immed i); inv H; autorewrite with labels; 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. + 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. - 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. - unfold transl_load_store_int, transl_load_store_float. - destruct m; rewrite transl_load_store_label; intros; auto. - unfold transl_load_store_int, transl_load_store_float. - destruct m; rewrite transl_load_store_label; intros; auto. - destruct s0; reflexivity. - destruct s0; simpl; autorewrite with labels; reflexivity. - rewrite peq_false. auto. congruence. + unfold transl_instr, Mach.is_label; intros. destruct i; try (monadInv H). + eapply loadind_label; eauto. + eapply storeind_label; eauto. + destruct ep; autorewrite with labels; eapply loadind_label; eauto. + eapply transl_op_label; eauto. + destruct m; simpl in H; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. + destruct m; simpl in H; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. + destruct s0; monadInv H; auto. + destruct s0; monadInv H; autorewrite with labels; auto. + auto. + auto. + simpl. auto. + auto. + erewrite transl_cond_label. 2: eauto. auto. + auto. + autorewrite with labels; 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 (fn_code (transl_function f)) = - option_map (transl_code f) (Mach.find_label lbl (Mach.fn_code f)). + forall f tf, + transf_function f = OK tf -> + match Mach.find_label lbl f.(Mach.fn_code) with + | None => find_label lbl (fn_code tf) = None + | Some c => exists tc, find_label lbl (fn_code tf) = Some tc /\ transl_code f c false = OK tc + end. Proof. - intros. unfold transl_function. simpl. autorewrite with labels. apply transl_code_label. + intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. + monadInv EQ. simpl. + eapply transl_code_label; eauto. Qed. End TRANSL_LABEL. @@ -518,29 +365,30 @@ End TRANSL_LABEL. (** A valid branch in a piece of Mach code translates to a valid ``go to'' transition in the generated ARM code. *) +(** A valid branch in a piece of Mach code translates to a valid ``go to'' + 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 (Mach.fn_code f) = Some c' -> - exists rs', - goto_label (fn_code (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. unfold option_map. intro. - generalize (label_pos_code_tail lbl (fn_code (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. @@ -562,90 +410,92 @@ Qed. - Mach register values and ARM 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 (Mach.fn_code f) -> - 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 f m' - (STACKS: match_stack s) - (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) - (WTF: wt_function f) - (INCL: incl c (Mach.fn_code f)) - (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#IR10 = 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) + forall s fd ms m m' rs fb + (STACKS: match_stack ge s m m' rs#(IR IR14) (Mem.nextblock m)) + (MEXT: Mem.extends m m') (AG: agree ms (parent_sp s) rs) (ATPC: rs PC = Vptr fb Int.zero) - (ATLR: rs IR14 = parent_ra s) - (MEXT: Mem.extends m m'), - match_states (Machsem.Callstate s fb ms m) + (FUNCT: Genv.find_funct_ptr ge fb = Some fd) + (WTRA: Val.has_type rs#(IR IR14) 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) - (ATPC: rs PC = parent_ra s) - (MEXT: Mem.extends m m'), - match_states (Machsem.Returnstate s ms m) + forall s ms m m' rs + (STACKS: match_stack ge s m m' (rs PC) (Mem.nextblock m)) + (MEXT: Mem.extends m 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 m1' f c1 rs1 c2 m2 ms2, - match_stack s -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - wt_function f -> - incl c2 (Mach.fn_code f) -> - transl_code_at_pc (rs1 PC) fb f c1 -> - Mem.extends m1 m1' -> - (exists m2', - Mem.extends m2 m2' /\ - exists rs2, - exec_straight tge (fn_code (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 + /\ (r10_is_parent ep i = true -> rs2#IR10 = 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 H5 as [m2' [A [rs2 [B C]]]]. + 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 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. +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 -> + r10_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 (Mach.State s f (Vptr sp Int.zero) c' ms2 m2) st'. 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 @@ -656,381 +506,280 @@ 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_R10: forall r, negb (mreg_eq r IT1) = true -> IR IR10 <> preg_of r. Proof. - intros; red; intros; inv MS. - left; eapply exec_straight_steps; eauto with coqlib. - exists m'; split; auto. - exists (nextinstr rs); split. - simpl. apply exec_straight_one. reflexivity. reflexivity. - apply agree_nextinstr; auto. + intros. change (IR IR10) with (preg_of IT1). red; intros. + exploit preg_of_injective; eauto. intros; subst r. + unfold proj_sumbool in H; rewrite dec_eq_true in H; 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. inv WTI. - exploit Mem.loadv_extends; eauto. intros [v' [A B]]. - rewrite (sp_val _ _ _ AG) in A. - exploit loadind_correct. eexact A. reflexivity. - intros [rs2 [EX [RES OTH]]]. - left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. - exists m'; split; auto. - simpl. exists rs2; split. eauto. - apply agree_set_mreg with rs; auto. congruence. auto with ppcgen. -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. - exploit preg_val; eauto. instantiate (1 := src). intros A. - exploit Mem.storev_extends; eauto. intros [m2 [B C]]. - rewrite (sp_val _ _ _ AG) in B. - exploit storeind_correct. eexact B. reflexivity. congruence. - intros [rs2 [EX OTH]]. - left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. - exists m2; split; auto. - simpl. exists rs2; split. eauto. - apply agree_exten with rs; auto with ppcgen. -Qed. + induction 1; intros; inv MS. -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. auto. - unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H0. eauto. - intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. - assert (parent' = parent_sp s). inv B. auto. rewrite <- H3 in H1; discriminate. subst parent'. - exploit Mem.loadv_extends. eauto. eexact H1. eauto. - intros [v' [C D]]. - exploit (loadind_int_correct tge (fn_code (transl_function f)) IR13 f.(fn_link_ofs) IR14 - rs m' (parent_sp s) (loadind IR14 ofs (mreg_type dst) dst (transl_code f c))). - auto. - intros [rs1 [EX1 [RES1 OTH1]]]. - exploit (loadind_correct tge (fn_code (transl_function f)) IR14 ofs (mreg_type dst) dst - (transl_code f c) rs1 m' v'). - rewrite RES1. auto. auto. - intros [rs2 [EX2 [RES2 OTH2]]]. - left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. - exists m'; split; auto. - exists rs2; split; simpl. - eapply exec_straight_trans; eauto. - apply agree_set_mreg with rs1. - apply agree_set_mreg with rs. auto. auto. auto with ppcgen. - congruence. auto with ppcgen. -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. - exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. - intros [v' [A B]]. - assert (C: eval_operation tge sp op rs ## (preg_of ## args) m' = Some v'). - rewrite <- A. apply eval_operation_preserved. exact symbols_preserved. - rewrite (sp_val _ _ _ AG) in C. - exploit transl_op_correct; eauto. intros [rs' [P [Q R]]]. - left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. - exists m'; split; auto. - exists rs'; split. simpl. eexact P. - assert (agree (Regmap.set res v ms) sp rs'). - apply agree_set_mreg with rs; auto. eapply Val.lessdef_trans; eauto. - assert (agree (Regmap.set res v (undef_temps ms)) sp rs'). - apply agree_set_undef_mreg with rs; auto. eapply Val.lessdef_trans; eauto. - auto with ppcgen. - destruct op; assumption. -Qed. +- (* 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. -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; inv WTI. - assert (eval_addressing tge sp addr ms##args = Some a). +- (* Mgetstack *) + unfold load_stack in H. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ AG) in A. + 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. + +- (* 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 [v' [C D]]. +Opaque loadind. + left; eapply exec_straight_steps; eauto; intros. + destruct ep; monadInv TR. +(* R10 contains parent *) + exploit loadind_correct. eexact EQ. + instantiate (2 := rs0). rewrite DXP; eauto. + 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_R10; auto. +(* GPR11 does not contain parent *) + exploit loadind_int_correct. eexact A. instantiate (1 := IR10). intros [rs1 [P [Q R]]]. + exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. 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#IR10 <- (rs2#IR10)). intros. + rewrite Pregmap.gso; auto with asmgen. + congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' IR10). congruence. auto with asmgen. + simpl; intros. rewrite U; auto with asmgen. + apply preg_of_not_R10; 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]]]. + assert (S: Val.lessdef v (rs2 (preg_of res))) by (eapply Val.lessdef_trans; eauto). + exists rs2; split. eauto. split. + assert (agree (Regmap.set res v (undef_temps rs)) (Vptr sp0 Int.zero) rs2). + eapply agree_set_undef_mreg; eauto with asmgen. + unfold undef_op; destruct op; auto. + change (undef_move rs) with rs. eapply agree_set_mreg; eauto. + simpl. destruct op; try congruence. destruct ep; simpl; try congruence. intros. + rewrite R; auto. apply preg_of_not_R10; auto. + +- (* Mload *) + 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. - exists m'; split; auto. - destruct chunk; simpl; simpl in H6; - try (generalize (Mem.loadv_float64al32 _ _ _ H0); intros); - (eapply transl_load_int_correct || eapply transl_load_float_correct); - eauto; intros; reflexivity. -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. - assert (eval_addressing tge sp addr ms##args = Some a). + 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. + simpl; congruence. + +- (* 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. auto. eauto. auto. eauto with coqlib. eauto. eauto. - destruct chunk; simpl; simpl in H6; - try (rewrite storev_8_signed_unsigned in H0); - try (rewrite storev_16_signed_unsigned in H0); - try (generalize (Mem.storev_float64al32 _ _ _ _ H0); intros); - simpl; - (eapply transl_store_int_correct || eapply transl_store_float_correct); - eauto; intros; simpl; auto. - econstructor; split. rewrite H2. eauto. intros. apply Pregmap.gso; auto. -Qed. - -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 : Mach.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. inv WTI. + 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. + simpl; congruence. + +- (* Mcall *) inv AT. - assert (NOOV: code_size (fn_code (transl_function f)) <= Int.max_unsigned). - eapply functions_transl_no_overflow; eauto. - assert (CT: code_tail (Int.unsigned (Int.add ofs Int.one)) (fn_code (transl_function f)) (transl_code f c)). - destruct ros; simpl in H5; eapply code_tail_next_int; eauto. - set (rs2 := rs #IR14 <- (Val.add rs#PC Vone) #PC <- (Vptr f' Int.zero)). - exploit return_address_offset_correct; eauto. constructor; eauto. - intro RA_EQ. - assert (ATLR: rs2 IR14 = Vptr fb ra). - rewrite RA_EQ. - unfold rs2. rewrite <- H2. reflexivity. - assert (AG3: agree ms sp rs2). - unfold rs2. apply agree_set_other; auto. apply agree_set_other; auto. - left; exists (State rs2 m'); split. - apply plus_one. - destruct ros; simpl in H5. - econstructor. eauto. apply functions_transl. eexact H0. - eapply find_instr_tail. eauto. - simpl. - assert (rs (ireg_of m0) = Vptr f' Int.zero). - generalize (ireg_val _ _ _ m0 AG H3). intro LD. simpl in H. inv LD. - destruct (ms m0); try congruence. - generalize H. predSpec Int.eq Int.eq_spec i Int.zero; congruence. - rewrite <- H7 in H; congruence. - rewrite H6. auto. - econstructor. eauto. apply functions_transl. eexact H0. - eapply find_instr_tail. eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. - simpl in H. rewrite H. auto. + assert (NOOV: list_length_z (fn_code 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. + 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. eauto. + econstructor; eauto. econstructor; eauto. - econstructor; eauto with coqlib. - rewrite RA_EQ. econstructor; eauto. - eapply agree_sp_def; eauto. congruence. -Qed. - -Lemma agree_change_sp: - forall ms sp rs sp', - agree ms sp rs -> sp' <> Vundef -> - agree ms sp' (rs#IR13 <- sp'). -Proof. - intros. inv H. split. apply Pregmap.gss. auto. - intros. rewrite Pregmap.gso; auto with ppcgen. -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. inv WTI. - set (call_instr := - match ros with inl r => Pbreg (ireg_of r) sig | inr symb => Pbsymb symb sig end). - assert (TR: transl_code f (Mtailcall sig ros :: c) = - loadind_int IR13 (fn_retaddr_ofs f) IR14 - (Pfreeframe f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)). - unfold call_instr; destruct ros; auto. - unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H1. auto. - intros [parent' [A B]]. - exploit lessdef_parent_sp; eauto. intros. subst parent'. - exploit Mem.loadv_extends. eauto. eexact H2. auto. - intros [ra' [C D]]. - exploit lessdef_parent_ra; eauto. intros. subst ra'. - exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. - destruct (loadind_int_correct tge (fn_code (transl_function f)) IR13 f.(fn_retaddr_ofs) IR14 - rs m'0 (parent_ra s) - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c)) - as [rs1 [EXEC1 [RES1 OTH1]]]. - rewrite <- (sp_val ms (Vptr stk soff) rs); auto. - set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))). - assert (EXEC2: exec_straight tge (fn_code (transl_function f)) - (transl_code f (Mtailcall sig ros :: c)) rs m'0 - (call_instr :: transl_code f c) rs2 m2'). - rewrite TR. eapply exec_straight_trans. eexact EXEC1. - apply exec_straight_one. simpl. - rewrite OTH1; auto with ppcgen. - rewrite <- (sp_val ms (Vptr stk soff) rs); auto. - simpl chunk_of_type in A. rewrite A. - rewrite P. auto. auto. - set (rs3 := rs2#PC <- (Vptr f' Int.zero)). - left. exists (State rs3 m2'); split. - (* Execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - inv AT. exploit exec_straight_steps_2; eauto. - eapply functions_transl_no_overflow; eauto. - eapply functions_transl; eauto. - intros [ofs2 [RS2PC CT]]. + 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 (fn_code 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 SP) (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. + assert (X: forall k, exists rs2, + exec_straight tge tf + (loadind_int IR13 (fn_retaddr_ofs f) IR14 + (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k)) rs0 m'0 + k rs2 m2' + /\ rs2#SP = parent_sp s + /\ rs2#RA = ra + /\ forall r, r <> PC -> r <> SP -> r <> IR14 -> rs2#r = rs0#r). + { + intros. + exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. + econstructor; split. + eapply exec_straight_trans. eexact P. apply exec_straight_one. + simpl. rewrite R; auto with asmgen. rewrite A. + rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. + split. Simpl. + split. Simpl. + intros. Simpl. + } + 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. + destruct (X (Pbreg x0 sig :: x)) as [rs2 [P [Q [R S]]]]. + exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. + intros [ofs' [Y Z]]. + left; econstructor; split. + eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. eauto. eapply functions_transl; eauto. - eapply find_instr_tail; eauto. - unfold call_instr; destruct ros; simpl in H; simpl. - replace (rs2 (ireg_of m0)) with (Vptr f' Int.zero). auto. - unfold rs2. rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gso. rewrite OTH1; auto with ppcgen. - generalize (ireg_val _ _ _ m0 AG H7). intro LD. inv LD. - destruct (ms m0); try congruence. - generalize H. predSpec Int.eq Int.eq_spec i Int.zero; congruence. - rewrite <- H10 in H; congruence. - auto with ppcgen. - unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. + eapply find_instr_tail; eauto. + simpl. reflexivity. traceEq. - (* Match states *) - constructor; auto. - unfold rs3. apply agree_set_other; auto. - unfold rs2. apply agree_nextinstr. apply agree_change_sp with (Vptr stk soff). - apply agree_exten with rs; auto with ppcgen. - apply parent_sp_def. auto. -Qed. - -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. + econstructor; eauto. + Simpl. rewrite R; auto. + constructor; intros. Simpl. + Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. + Simpl. rewrite S; auto with asmgen. + rewrite <- (ireg_of_eq _ _ EQ1); auto with asmgen. + rewrite <- (ireg_of_eq _ _ EQ1); auto with asmgen. + Simpl. rewrite R. eapply retaddr_stored_at_type; eauto. ++ (* Direct call *) + destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. + destruct (X (Pbsymb fid sig :: x)) as [rs2 [P [Q [R S]]]]. + exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. + intros [ofs' [Y Z]]. + left; econstructor; split. + eapply plus_right'. eapply exec_straight_exec; eauto. + econstructor. eauto. eapply functions_transl; eauto. + eapply find_instr_tail; eauto. + simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. reflexivity. + traceEq. + econstructor; eauto. + Simpl. rewrite R; auto. + constructor; intros. Simpl. + Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. + Simpl. + Simpl. rewrite R. eapply retaddr_stored_at_type; eauto. + +- (* 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]]]]]. - inv AT. simpl in H3. - generalize (functions_transl _ _ FIND); intro FN. - generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. left. econstructor; split. apply plus_one. eapply exec_step_builtin. eauto. eauto. - eapply find_instr_tail; eauto. - eapply external_call_symbols_preserved; eauto. - eexact symbols_preserved. eexact varinfo_preserved. - econstructor; eauto with coqlib. - unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. - rewrite <- H0. simpl. constructor; auto. - eapply code_tail_next_int; eauto. - apply sym_not_equal. auto with ppcgen. + eapply find_instr_tail; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + 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. rewrite Pregmap.gso; auto. -Qed. - -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. + rewrite Pregmap.gss. auto. + intros. Simpl. + eapply retaddr_stored_at_extcall; eauto. + intros; eapply external_call_max_perm; eauto. + congruence. + +- (* 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]]]]]. @@ -1039,360 +788,220 @@ 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. - -Lemma exec_Mgoto_prop: - forall (s : list stackframe) (fb : block) (f : Mach.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 (Mach.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. + eapply retaddr_stored_at_extcall; eauto. + intros; eapply external_call_max_perm; eauto. + congruence. + +- (* 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 : Mach.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 (Mach.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. - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. - intros A. - exploit transl_cond_correct. eauto. eauto. - instantiate (1 := rs). instantiate (1 := m'). - rewrite A || (unfold PregEq.t; rewrite A). - intros [rs2 [EX [RES OTH]]]. - 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. + simpl; eauto. econstructor; eauto. - eapply find_instr_tail. eauto. - simpl. rewrite RES. simpl. auto. - traceEq. - econstructor; eauto. - eapply Mach.find_label_incl; eauto. - apply agree_exten_temps with rs; auto. intros. - rewrite INV3; 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. inv WTI. - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. - intros A. - exploit transl_cond_correct. eauto. - instantiate (1 := rs). instantiate (1 := m'). - rewrite A || (unfold PregEq.t; rewrite A). - intros [rs2 [EX [RES OTH]]]. - left; eapply exec_straight_steps; eauto with coqlib. - exists m'; split; auto. - exists (nextinstr rs2); split. - simpl. eapply exec_straight_trans. eexact EX. - apply exec_straight_one. simpl. rewrite RES. reflexivity. reflexivity. - apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen. -Qed. - -Lemma exec_Mjumptable_prop: - forall (s : list stackframe) (fb : block) (f : Mach.function) (sp : val) - (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction) - (ms : mreg -> val) (m : mem) (n : int) (lbl : Mach.label) - (c' : Mach.code), - ms 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 (Mach.fn_code f) = Some c' -> - exec_instr_prop - (Machsem.State s fb sp (Mjumptable arg tbl :: 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. - exploit list_nth_z_range; eauto. intro RANGE. - assert (SHIFT: Int.unsigned (Int.shl n (Int.repr 2)) = Int.unsigned n * 4). - rewrite Int.shl_mul. - unfold Int.mul. - apply Int.unsigned_repr. - omega. - inv AT. simpl in H7. - set (k1 := Pbtbl IR14 tbl :: transl_code f c). - set (rs1 := nextinstr (rs # IR14 <- (Vint (Int.shl n (Int.repr 2))))). - generalize (functions_transl _ _ H4); intro FN. - generalize (functions_transl_no_overflow _ _ H4); intro NOOV. - assert (rs (ireg_of arg) = Vint n). - exploit ireg_val; eauto. intros LD. inv LD. auto. congruence. - assert (exec_straight tge (fn_code (transl_function f)) - (Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) :: k1) rs m' - k1 rs1 m'). - apply exec_straight_one. - simpl. rewrite H8. reflexivity. reflexivity. - exploit exec_straight_steps_2; eauto. - intros [ofs' [PC1 CT1]]. - generalize (find_label_goto_label f lbl rs1 m' _ _ _ FIND PC1 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. - change (rs1 IR14) with (Vint (Int.shl n (Int.repr 2))). - 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. + eapply agree_exten; eauto with asmgen. + congruence. + +- (* 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 tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. + rewrite EC in B. + 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 tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. + rewrite EC in B. + econstructor; split. + eapply exec_straight_trans. eexact A. + 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#IR14 <- 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_exten with rs1; auto with ppcgen. - unfold rs1. apply agree_nextinstr. apply agree_set_other; auto with ppcgen. - apply agree_undef_temps; auto. -Qed. - -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. - unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H0. auto. - intros [parent' [A B]]. - exploit lessdef_parent_sp; eauto. intros. subst parent'. - exploit Mem.loadv_extends. eauto. eexact H1. auto. - intros [ra' [C D]]. - exploit lessdef_parent_ra; eauto. intros. subst ra'. - exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. - - exploit (loadind_int_correct tge (fn_code (transl_function f)) IR13 f.(fn_retaddr_ofs) IR14 - rs m'0 (parent_ra s) - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 f.(Mach.fn_sig) :: transl_code f c)). - rewrite <- (sp_val ms (Vptr stk soff) rs); auto. - intros [rs1 [EXEC1 [RES1 OTH1]]]. - set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))). - assert (EXEC2: exec_straight tge (fn_code (transl_function f)) - (loadind_int IR13 (fn_retaddr_ofs f) IR14 - (Pfreeframe f.(fn_stacksize) (fn_link_ofs f) :: Pbreg IR14 f.(Mach.fn_sig) :: transl_code f c)) - rs m'0 (Pbreg IR14 f.(Mach.fn_sig) :: transl_code f c) rs2 m2'). - eapply exec_straight_trans. eexact EXEC1. - apply exec_straight_one. simpl. rewrite OTH1; try congruence. - rewrite <- (sp_val ms (Vptr stk soff) rs); auto. - simpl chunk_of_type in A. rewrite A. rewrite E. auto. auto. - set (rs3 := rs2#PC <- (parent_ra s)). - left; exists (State rs3 m2'); split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - inv AT. exploit exec_straight_steps_2; eauto. - eapply functions_transl_no_overflow; eauto. - eapply functions_transl; eauto. - intros [ofs2 [RS2PC CT]]. + eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simpl. + congruence. + +- (* Mreturn *) + inversion AT; subst. + assert (NOOV: list_length_z (fn_code 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 SP) (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. + assert (X: forall k, exists rs2, + exec_straight tge tf + (loadind_int IR13 (fn_retaddr_ofs f) IR14 + (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k)) rs0 m'0 + k rs2 m2' + /\ rs2#SP = parent_sp s + /\ rs2#RA = ra + /\ forall r, r <> PC -> r <> SP -> r <> IR14 -> rs2#r = rs0#r). + { + intros. + exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. + econstructor; split. + eapply exec_straight_trans. eexact P. apply exec_straight_one. + simpl. rewrite R; auto with asmgen. rewrite A. + rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. + split. Simpl. + split. Simpl. + intros. Simpl. + } + destruct (X (Pbreg IR14 (Mach.fn_sig f) :: x)) as [rs2 [P [Q [R S]]]]. + exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. + intros [ofs' [Y Z]]. + left; econstructor; split. + eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. eauto. eapply functions_transl; eauto. - eapply find_instr_tail; eauto. - simpl. unfold rs3. decEq. decEq. unfold rs2. rewrite nextinstr_inv; auto with ppcgen. + eapply find_instr_tail; eauto. + simpl. reflexivity. traceEq. - (* match states *) - constructor. auto. - apply agree_exten with rs2. - unfold rs2. apply agree_nextinstr. apply agree_change_sp with (Vptr stk soff). - apply agree_exten with rs; auto with ppcgen. - apply parent_sp_def. auto. - intros. unfold rs3. apply Pregmap.gso; auto with ppcgen. - unfold rs3. apply Pregmap.gss. - auto. -Qed. - -Hypothesis wt_prog: wt_program prog. - -Lemma exec_function_internal_prop: - forall (s : list stackframe) (fb : block) (ms : Mach.regset) - (m : mem) (f : Mach.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 (Mach.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. - set (rs2 := nextinstr (rs#IR12 <- (rs#IR13) #IR13 <- sp)). - set (rs3 := nextinstr rs2). - exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. - intros [m1' [A B]]. - unfold store_stack in *; simpl chunk_of_type in *. - exploit Mem.storev_extends. eexact B. eauto. auto. auto. - intros [m2' [C D]]. - exploit Mem.storev_extends. eexact D. eauto. auto. auto. - intros [m3' [E F]]. + econstructor; eauto. + Simpl. rewrite R; auto. + constructor; intros. Simpl. + Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. + +- (* 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 (fn_code x0))); inversion EQ1. clear EQ1. + monadInv EQ0. + 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 *) + set (rs2 := nextinstr (rs0#IR10 <- (parent_sp s) #IR13 <- (Vptr stk Int.zero))). + set (rs3 := nextinstr rs2). assert (EXEC_PROLOGUE: - exec_straight tge (fn_code (transl_function f)) - (fn_code (transl_function f)) rs m' - (transl_code f f.(Mach.fn_code)) rs3 m3'). - unfold transl_function at 2. + exec_straight tge x + (fn_code x) rs0 m' + x1 rs3 m3'). + rewrite <- H5 at 2; unfold fn_code. apply exec_straight_two with rs2 m2'. - unfold exec_instr. rewrite A. fold sp. - rewrite (sp_val ms (parent_sp s) rs) in C; auto. rewrite C. auto. - unfold exec_instr. unfold eval_shift_addr. unfold exec_store. - change (rs2 IR13) with sp. change (rs2 IR14) with (rs IR14). rewrite ATLR. - rewrite E. auto. - auto. auto. - (* Agreement at end of prologue *) - assert (AT3: transl_code_at_pc rs3#PC fb f f.(Mach.fn_code)). - change (rs3 PC) with (Val.add (Val.add (rs PC) Vone) Vone). - rewrite ATPC. simpl. constructor. 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 (AG3: agree (undef_temps ms) sp rs3). - unfold rs3. apply agree_nextinstr. - unfold rs2. apply agree_nextinstr. - apply agree_change_sp with (parent_sp s). - apply agree_exten_temps with rs; auto. - intros. apply Pregmap.gso; auto with ppcgen. - unfold sp. congruence. + unfold exec_instr. rewrite C. fold sp. + rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. + simpl. auto. + simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). + rewrite Int.add_zero_l. simpl. rewrite P. auto. auto. auto. left; exists (State rs3 m3'); split. - (* execution *) - eapply exec_straight_steps_1; eauto. - change (Int.unsigned Int.zero) with 0. constructor. - (* match states *) - econstructor; eauto with coqlib. -Qed. - -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. + eapply exec_straight_steps_1; eauto. 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 (rs3 PC) with (Val.add (Val.add (rs0 PC) Vone) Vone). + rewrite ATPC. simpl. constructor; eauto. + subst x. eapply code_tail_next_int. omega. + eapply code_tail_next_int. omega. constructor. + unfold rs3, rs2. + apply agree_nextinstr. apply agree_nextinstr. + eapply agree_change_sp. + apply agree_exten_temps with rs0; eauto. + intros. Simpl. congruence. + +- (* external function *) exploit functions_translated; eauto. intros [tf [A B]]. simpl in B. inv B. exploit extcall_arguments_match; eauto. intros [args' [C D]]. - exploit external_call_mem_extends; eauto. - intros [vres' [m2' [P [Q [R S]]]]]. - left; exists (State (rs#(loc_external_result (ef_sig ef)) <- vres' #PC <- (rs IR14)) - m2'); split. - apply plus_one. eapply exec_step_external; eauto. - eapply external_call_symbols_preserved; eauto. + exploit external_call_mem_extends; eauto. + intros [res' [m2' [P [Q [R S]]]]]. + left; econstructor; split. + apply plus_one. eapply exec_step_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. - econstructor; eauto. - unfold loc_external_result. + econstructor; eauto. + 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 ppcgen. rewrite Pregmap.gss. auto. - intros. repeat rewrite Pregmap.gso; auto with ppcgen. -Qed. + rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. + intros; Simpl. -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 *. +- (* 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. + 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. intros. repeat rewrite Pregmap.gso; auto with ppcgen. - intros. unfold Regmap.init. auto. + 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. @@ -1400,21 +1009,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; eauto. instantiate (1 := R0); auto. - simpl. intros LD. inv LD; congruence. + intros. inv H0. inv H. inv STACKS. constructor. + auto. + compute in H1. + generalize (preg_val _ _ _ R0 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/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 658fc981..8fc8a7ee 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -12,8 +12,9 @@ (** Correctness proof for ARM code generation: auxiliary results. *) -Require Import Axioms. +(*Require Import Axioms.*) Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. @@ -24,455 +25,44 @@ 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. -(** * Correspondence between Mach registers and PPC registers *) +(** Useful properties of the R14 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. - -Lemma ireg_of_not_IR13: - forall r, ireg_of r <> IR13. -Proof. - destruct r; simpl; congruence. -Qed. - -Lemma ireg_of_not_IR14: - forall r, ireg_of r <> IR14. -Proof. - destruct r; simpl; congruence. -Qed. - -Lemma preg_of_not_IR13: - forall r, preg_of r <> IR13. -Proof. - unfold preg_of; intros. destruct (mreg_type r). - generalize (ireg_of_not_IR13 r); congruence. - congruence. -Qed. - -Lemma preg_of_not_IR14: - forall r, preg_of r <> IR14. -Proof. - unfold preg_of; intros. destruct (mreg_type r). - generalize (ireg_of_not_IR14 r); congruence. - congruence. -Qed. - -Lemma preg_of_not_PC: - forall r, preg_of r <> PC. -Proof. - intros. unfold preg_of. destruct (mreg_type r); congruence. -Qed. - -Lemma ireg_diff: - forall r1 r2, r1 <> r2 -> IR r1 <> IR r2. -Proof. intros; congruence. Qed. - -Hint Resolve ireg_of_not_IR13 ireg_of_not_IR14 - preg_of_not_IR13 preg_of_not_IR14 - preg_of_not_PC ireg_diff: ppcgen. - -(** Agreement between Mach register sets and ARM register sets. *) - -Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree { - agree_sp: rs#IR13 = 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. destruct H. auto. -Qed. - -Lemma preg_vals: - forall ms sp rs, agree ms sp rs -> - forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)). -Proof. - induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto. -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. generalize (preg_val _ _ _ r H). 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. generalize (preg_val _ _ _ r H). unfold preg_of. rewrite H0. auto. -Qed. - -Lemma sp_val: - forall ms sp rs, - agree ms sp rs -> - sp = rs#IR13. -Proof. - intros. destruct H; auto. -Qed. - -Hint Resolve preg_val ireg_val freg_val sp_val: ppcgen. - -Definition important_preg (r: preg) : bool := - match r with - | IR IR14 => false - | IR _ => true - | FR _ => true - | CR _ => false - | PC => false - end. - -Lemma preg_of_important: - forall r, important_preg (preg_of r) = true. -Proof. - intros. destruct r; reflexivity. -Qed. - -Lemma important_diff: - forall r r', - important_preg r = true -> important_preg r' = false -> r <> r'. -Proof. - congruence. -Qed. -Hint Resolve important_diff: ppcgen. - -Lemma agree_exten: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, important_preg r = true -> rs'#r = rs#r) -> - agree ms sp rs'. -Proof. - intros. destruct H. split. - rewrite H0; auto. auto. - intros. rewrite H0; auto. apply preg_of_important. -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', important_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros. destruct H. split. - rewrite H1; auto. apply sym_not_equal. apply preg_of_not_IR13. - auto. - intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. - rewrite H1. auto. apply preg_of_important. - red; intros; elim n. eapply preg_of_injective; eauto. -Qed. - -Lemma agree_set_other: - forall ms sp rs r v, - agree ms sp rs -> - important_preg r = false -> - agree ms sp (rs#r <- v). -Proof. - intros. apply agree_exten with rs. auto. - intros. apply Pregmap.gso. congruence. -Qed. - -Lemma agree_nextinstr: - forall ms sp rs, - agree ms sp rs -> agree ms sp (nextinstr rs). +Lemma ireg_of_not_R14: + forall m r, ireg_of m = OK r -> IR r <> IR IR14. Proof. - intros. unfold nextinstr. apply agree_set_other. auto. auto. + intros. erewrite <- ireg_of_eq; eauto with asmgen. Qed. +Hint Resolve ireg_of_not_R14: asmgen. -Definition nontemp_preg (r: preg) : bool := - match r with - | IR IR14 => false - | IR IR10 => false - | IR IR12 => false - | IR _ => true - | FR FR6 => false - | FR FR7 => false - | FR _ => true - | CR _ => false - | PC => false - end. - -Lemma nontemp_diff: - forall r r', - nontemp_preg r = true -> nontemp_preg r' = false -> r <> r'. -Proof. - congruence. -Qed. - -Hint Resolve nontemp_diff: ppcgen. - -Lemma nontemp_important: - forall r, nontemp_preg r = true -> important_preg r = true. +Lemma ireg_of_not_R14': + forall m r, ireg_of m = OK r -> r <> IR14. Proof. - unfold nontemp_preg, important_preg; destruct r; auto. destruct i; auto. + intros. generalize (ireg_of_not_R14 _ _ H). congruence. Qed. +Hint Resolve ireg_of_not_R14': asmgen. -Hint Resolve nontemp_important: ppcgen. +(** Useful simplification tactic *) -Remark undef_regs_1: - forall l ms r, ms r = Vundef -> Mach.undef_regs l ms r = Vundef. -Proof. - induction l; simpl; intros. auto. apply IHl. unfold Regmap.set. - destruct (RegEq.eq r a); congruence. -Qed. +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. -Remark undef_regs_2: - forall l ms r, In r l -> Mach.undef_regs l ms r = Vundef. -Proof. - induction l; simpl; intros. contradiction. - destruct H. subst. apply undef_regs_1. apply Regmap.gss. - auto. -Qed. - -Remark undef_regs_3: - forall l ms r, ~In r l -> Mach.undef_regs l ms r = ms r. -Proof. - induction l; simpl; intros. auto. - rewrite IHl. apply Regmap.gso. intuition. intuition. -Qed. - -Lemma agree_exten_temps: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, nontemp_preg r = true -> rs'#r = rs#r) -> - agree (undef_temps ms) sp rs'. -Proof. - intros. destruct H. split. - rewrite H0; auto. auto. - intros. unfold undef_temps. - destruct (In_dec mreg_eq r (int_temporaries ++ float_temporaries)). - rewrite undef_regs_2; auto. - rewrite undef_regs_3; auto. rewrite H0; auto. - simpl in n. destruct r; auto; intuition. -Qed. - -Lemma agree_set_undef_mreg: - forall ms sp rs r v rs', - agree ms sp rs -> - Val.lessdef v (rs'#(preg_of r)) -> - (forall r', nontemp_preg 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))); auto. - eapply agree_exten_temps; eauto. - intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). - congruence. auto. - intros. rewrite Pregmap.gso; auto. -Qed. +Ltac Simpl := repeat Simplif. -Lemma agree_undef_temps: - forall ms sp rs, - agree ms sp rs -> - agree (undef_temps ms) sp rs. -Proof. - intros. eapply agree_exten_temps; eauto. -Qed. - -(** Useful properties of the PC register. *) - -Lemma nextinstr_inv: - forall r rs, - r <> PC -> - (nextinstr rs)#r = rs#r. -Proof. - intros. unfold nextinstr. apply Pregmap.gso. red; intro; subst. auto. -Qed. - -Lemma nextinstr_inv2: - forall r rs, - nontemp_preg r = true -> - (nextinstr rs)#r = rs#r. -Proof. - intros. apply nextinstr_inv. red; intro; subst; discriminate. -Qed. - -Lemma nextinstr_set_preg: - forall rs m v, - (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone. -Proof. - intros. unfold nextinstr. rewrite Pregmap.gss. - rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC. -Qed. - -(** Connection between Mach and Asm calling conventions for external - functions. *) - -Lemma extcall_arg_match: - forall ms sp rs m m' l v, - agree ms sp rs -> - Machsem.extcall_arg ms m sp l v -> - Mem.extends m m' -> - exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'. -Proof. - intros. inv H0. - exists (rs#(preg_of r)); split. constructor. eauto with ppcgen. - 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; eauto. -Qed. - -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'. -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. -Qed. - -Lemma extcall_arguments_match: - forall ms m sp rs sg args m', - agree ms sp rs -> - Machsem.extcall_arguments ms m sp sg args -> - Mem.extends m m' -> - 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. - -(** Translation of arguments to annotations. *) - -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. - -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 ARM 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. - -Lemma exec_straight_four: - forall i1 i2 i3 i4 c rs1 m1 rs2 m2 rs3 m3 rs4 m4 rs5 m5, - 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 -> - exec_instr ge fn i4 rs4 m4 = OK rs5 m5 -> - rs2#PC = Val.add rs1#PC Vone -> - rs3#PC = Val.add rs2#PC Vone -> - rs4#PC = Val.add rs3#PC Vone -> - rs5#PC = Val.add rs4#PC Vone -> - exec_straight (i1 :: i2 :: i3 :: i4 :: c) rs1 m1 c rs5 m5. -Proof. - intros. apply exec_straight_step with rs2 m2; auto. - eapply exec_straight_three; eauto. -Qed. - -(** * Correctness of ARM constructor functions *) +Variable fn: function. (** Decomposition of an integer constant *) @@ -606,12 +196,12 @@ Lemma iterate_op_correct: forall op1 op2 (f: val -> int -> val) (rs: regset) (r: ireg) m v0 n k, (forall (rs:regset) n, exec_instr ge fn (op2 (SOimm n)) rs m = - OK (nextinstr (rs#r <- (f (rs#r) n))) m) -> + Next (nextinstr (rs#r <- (f (rs#r) n))) m) -> (forall n, exec_instr ge fn (op1 (SOimm n)) rs m = - OK (nextinstr (rs#r <- (f v0 n))) m) -> + Next (nextinstr (rs#r <- (f v0 n))) m) -> exists rs', - exec_straight (iterate_op op1 op2 (decompose_int n) k) rs m k rs' m + exec_straight ge fn (iterate_op op1 op2 (decompose_int n) k) rs m k rs' m /\ rs'#r = List.fold_left f (decompose_int n) v0 /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -623,8 +213,7 @@ Proof. (* base case *) intros; simpl. econstructor. split. apply exec_straight_one. rewrite SEM1. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. auto. - intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen. + intuition Simpl. (* inductive case *) intros. rewrite List.map_app. simpl. rewrite app_ass. simpl. @@ -632,9 +221,8 @@ Proof. econstructor. split. eapply exec_straight_trans. eexact A. apply exec_straight_one. rewrite SEM2. reflexivity. reflexivity. - split. rewrite fold_left_app; simpl. rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gss. rewrite B. auto. - intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen. + split. rewrite fold_left_app; simpl. Simpl. rewrite B. auto. + intros; Simpl. Qed. (** Loading a constant. *) @@ -642,7 +230,7 @@ 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. @@ -667,7 +255,7 @@ Qed. Lemma addimm_correct: forall r1 r2 n k rs m, 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. @@ -693,9 +281,8 @@ Qed. Lemma andimm_correct: forall r1 r2 n k rs m, - r2 <> IR14 -> 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': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -704,7 +291,7 @@ Proof. case (is_immed_arith n). exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))). split. apply exec_straight_one; auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. + split. rewrite nextinstr_inv; auto with asmgen. apply Pregmap.gss. intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. (* bic - bic* *) replace (Val.and (rs r2) (Vint n)) @@ -720,7 +307,7 @@ Qed. Lemma rsubimm_correct: forall r1 r2 n k rs m, exists rs', - exec_straight (rsubimm r1 r2 n k) rs m k rs' m + exec_straight ge fn (rsubimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = Val.sub (Vint n) rs#r2 /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -741,7 +328,7 @@ Qed. Lemma orimm_correct: forall r1 r2 n k rs m, 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 = Val.or rs#r2 (Vint n) /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -760,7 +347,7 @@ Qed. Lemma xorimm_correct: forall r1 r2 n k rs m, 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 = Val.xor rs#r2 (Vint n) /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -780,7 +367,7 @@ Lemma loadind_int_correct: forall (base: ireg) ofs dst (rs: regset) m v k, Mem.loadv Mint32 m (Val.add rs#base (Vint ofs)) = Some v -> exists rs', - exec_straight (loadind_int base ofs dst k) rs m k rs' m + exec_straight ge fn (loadind_int base ofs dst k) rs m k rs' m /\ rs'#dst = v /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. Proof. @@ -788,23 +375,21 @@ Proof. exists (nextinstr (rs#dst <- v)). split. apply exec_straight_one. simpl. unfold exec_load. rewrite H. auto. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + intuition Simpl. exploit addimm_correct. intros [rs' [A [B C]]]. exists (nextinstr (rs'#dst <- v)). split. eapply exec_straight_trans. eauto. apply exec_straight_one. simpl. unfold exec_load. rewrite B. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + intuition Simpl. Qed. Lemma loadind_float_correct: forall (base: ireg) ofs dst (rs: regset) m v k, Mem.loadv Mfloat64al32 m (Val.add rs#base (Vint ofs)) = Some v -> exists rs', - exec_straight (loadind_float base ofs dst k) rs m k rs' m + exec_straight ge fn (loadind_float base ofs dst k) rs m k rs' m /\ rs'#dst = v /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. Proof. @@ -812,33 +397,29 @@ Proof. exists (nextinstr (rs#dst <- v)). split. apply exec_straight_one. simpl. unfold exec_load. rewrite H. auto. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + intuition Simpl. exploit addimm_correct. eauto. intros [rs' [A [B C]]]. exists (nextinstr (rs'#dst <- v)). split. eapply exec_straight_trans. eauto. apply exec_straight_one. simpl. unfold exec_load. rewrite B. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + intuition Simpl. Qed. Lemma loadind_correct: - forall (base: ireg) ofs ty dst k (rs: regset) m v, + forall (base: ireg) ofs ty dst k c (rs: regset) m v, + 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 -> 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 <> IR14 -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros. unfold loadind. - assert (preg_of dst <> PC). - unfold preg_of. case (mreg_type dst); discriminate. - unfold preg_of. rewrite H0. destruct ty. - apply loadind_int_correct; auto. - apply loadind_float_correct; auto. + unfold loadind; intros. + destruct ty; monadInv H. + erewrite ireg_of_eq by eauto. apply loadind_int_correct; auto. + erewrite freg_of_eq by eauto. apply loadind_float_correct; auto. Qed. (** Indexed memory stores. *) @@ -848,37 +429,36 @@ Lemma storeind_int_correct: Mem.storev Mint32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' -> src <> IR14 -> exists rs', - exec_straight (storeind_int src base ofs k) rs m k rs' m' + exec_straight ge fn (storeind_int src base ofs k) rs m k rs' m' /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. Proof. intros; unfold storeind_int. destruct (is_immed_mem_word ofs). exists (nextinstr rs). split. apply exec_straight_one. simpl. unfold exec_store. rewrite H. auto. auto. - intros. rewrite nextinstr_inv; auto. + intuition Simpl. exploit addimm_correct. eauto. intros [rs' [A [B C]]]. exists (nextinstr rs'). split. eapply exec_straight_trans. eauto. apply exec_straight_one. simpl. unfold exec_store. rewrite B. rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. - congruence. auto with ppcgen. auto. - intros. rewrite nextinstr_inv; auto. + congruence. auto with asmgen. auto. + intuition Simpl. Qed. Lemma storeind_float_correct: forall (base: ireg) ofs (src: freg) (rs: regset) m m' k, Mem.storev Mfloat64al32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' -> - base <> IR14 -> exists rs', - exec_straight (storeind_float src base ofs k) rs m k rs' m' + exec_straight ge fn (storeind_float src base ofs k) rs m k rs' m' /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. Proof. intros; unfold storeind_float. destruct (is_immed_mem_float ofs). exists (nextinstr rs). split. apply exec_straight_one. simpl. unfold exec_store. rewrite H. auto. auto. - intros. rewrite nextinstr_inv; auto. + intuition Simpl. exploit addimm_correct. eauto. intros [rs' [A [B C]]]. exists (nextinstr rs'). split. eapply exec_straight_trans. eauto. apply exec_straight_one. @@ -886,22 +466,23 @@ Proof. rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. congruence. congruence. - auto with ppcgen. - intros. rewrite nextinstr_inv; auto. + auto with asmgen. + intuition Simpl. Qed. Lemma storeind_correct: - forall (base: ireg) ofs ty src k (rs: regset) m m', + forall (base: ireg) ofs ty src k c (rs: regset) m m', + 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 <> IR14 -> 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 <> IR14 -> rs'#r = rs#r. Proof. - intros. unfold storeind. unfold preg_of in H. rewrite H0 in H. destruct ty. - apply storeind_int_correct. auto. auto. auto with ppcgen. - apply storeind_float_correct. auto. auto. + unfold storeind; intros. + destruct ty; monadInv H. + erewrite ireg_of_eq in H0 by eauto. apply storeind_int_correct; auto. + assert (IR x <> IR IR14) by eauto with asmgen. congruence. + erewrite freg_of_eq in H0 by eauto. apply storeind_float_correct; auto. Qed. (** Translation of shift immediates *) @@ -935,11 +516,10 @@ Lemma compare_int_spec: /\ rs1#CRlt = (Val.cmp Clt v1 v2) /\ rs1#CRgt = (Val.cmp Cgt v1 v2) /\ rs1#CRle = (Val.cmp Cle v1 v2) - /\ forall r', important_preg r' = true -> rs1#r' = rs#r'. + /\ forall r', data_preg r' = true -> rs1#r' = rs#r'. Proof. - intros. unfold rs1. intuition; try reflexivity. - rewrite nextinstr_inv; auto with ppcgen. - unfold compare_int. repeat rewrite Pregmap.gso; auto with ppcgen. + intros. unfold rs1. intuition; try reflexivity. + unfold compare_int. Simpl. Qed. Lemma compare_float_spec: @@ -955,43 +535,43 @@ Lemma compare_float_spec: /\ rs'#CRlt = (Val.notbool (Val.cmpf Cge v1 v2)) /\ rs'#CRgt = (Val.cmpf Cgt v1 v2) /\ rs'#CRle = (Val.notbool (Val.cmpf Cgt v1 v2)) - /\ forall r', important_preg r' = true -> rs'#r' = rs#r'. -Proof. - intros. unfold rs'. intuition; try reflexivity. - rewrite nextinstr_inv; auto with ppcgen. - unfold compare_float. repeat rewrite Pregmap.gso; auto with ppcgen. -Qed. - -Ltac TypeInv1 := - match goal with - | H: (List.map ?f ?x = nil) |- _ => - destruct x; inv H; TypeInv1 - | H: (List.map ?f ?x = ?hd :: ?tl) |- _ => - destruct x; simpl in H; simplify_eq H; clear H; intros; TypeInv1 - | _ => idtac - end. - -Ltac TypeInv2 := - match goal with - | H: (mreg_type _ = Tint) |- _ => try (rewrite H in *); clear H; TypeInv2 - | H: (mreg_type _ = Tfloat) |- _ => try (rewrite H in *); clear H; TypeInv2 - | _ => idtac - end. - -Ltac TypeInv := TypeInv1; simpl in *; unfold preg_of in *; TypeInv2. + /\ forall r', data_preg r' = true -> rs'#r' = rs#r'. +Proof. + intros. unfold rs'. intuition; try reflexivity. + unfold compare_float. Simpl. +Qed. + +Definition lock {A: Type} (x: A) := x. + +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 ?x = OK ?y |- _ ] => + simpl in *; rewrite (ireg_of_eq _ _ H) in * +(*; change H with (lock (ireg_of x) = OK y)*) + | [ H: freg_of ?x = OK ?y |- _ ] => + simpl in *; rewrite (freg_of_eq _ _ H) in * +(*; change H with (lock (freg_of x) = OK y)*) + end). Lemma transl_cond_correct: - 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 /\ match eval_condition cond (map rs (map preg_of args)) m with | Some b => rs'#(CR (crbit_for_cond cond)) = Val.of_bool b | None => True end - /\ forall r, important_preg r = true -> rs'#r = rs r. + /\ forall r, data_preg r = true -> rs'#r = rs r. Proof. - intros until m; intros TY. + intros until c; intros TR. assert (MATCH: forall v ob, v = Val.of_optbool ob -> match ob with Some b => v = Val.of_bool b | None => True end). @@ -1006,268 +586,251 @@ Proof. intros. destruct v1; simpl; auto; destruct v2; simpl; auto. unfold Val.cmpu, Val.cmpu_bool in H. subst v. destruct H0; subst cmp; auto. - destruct cond; simpl in TY; TypeInv; simpl. - (* Ccomp *) - generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1)) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + unfold transl_cond in TR; destruct cond; ArgsInv. +- (* Ccomp *) + generalize (compare_int_spec rs (rs x) (rs x0) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto). + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). auto. - (* Ccompu *) - generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1)) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. +- (* Ccompu *) + generalize (compare_int_spec rs (rs x) (rs x0) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c; apply MATCH; assumption. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). auto. - (* Ccompshift *) - generalize (compare_int_spec rs (rs (ireg_of m0)) (eval_shift s (rs (ireg_of m1))) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. +- (* Ccompshift *) + generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite transl_shift_correct. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto). - rewrite transl_shift_correct. auto. - (* Ccompushift *) - generalize (compare_int_spec rs (rs (ireg_of m0)) (eval_shift s (rs (ireg_of m1))) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + rewrite transl_shift_correct. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). + auto. +- (* Ccompushift *) + generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite transl_shift_correct. destruct c; apply MATCH; assumption. - rewrite transl_shift_correct. auto. - (* Ccompimm *) + rewrite transl_shift_correct. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). + auto. +- (* Ccompimm *) destruct (is_immed_arith i). - generalize (compare_int_spec rs (rs (ireg_of m0)) (Vint i) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + generalize (compare_int_spec rs (rs x) (Vint i) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto). + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). auto. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. - generalize (compare_int_spec rs' (rs (ireg_of m0)) (Vint i) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + generalize (compare_int_spec rs' (rs x) (Vint i) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. - rewrite Q. rewrite R; eauto with ppcgen. auto. - split. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto). - intros. rewrite K; auto with ppcgen. - (* Ccompuimm *) + rewrite Q. rewrite R; eauto with asmgen. auto. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). + intros. rewrite C; auto with asmgen. +- (* Ccompuimm *) destruct (is_immed_arith i). - generalize (compare_int_spec rs (rs (ireg_of m0)) (Vint i) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + generalize (compare_int_spec rs (rs x) (Vint i) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c; apply MATCH; assumption. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). auto. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. - generalize (compare_int_spec rs' (rs (ireg_of m0)) (Vint i) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + generalize (compare_int_spec rs' (rs x) (Vint i) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. - rewrite Q. rewrite R; eauto with ppcgen. auto. - split. destruct c; apply MATCH; assumption. - intros. rewrite K; auto with ppcgen. - (* Ccompf *) - generalize (compare_float_spec rs (rs (freg_of m0)) (rs (freg_of m1))). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + rewrite Q. rewrite R; eauto with asmgen. auto. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). + intros. rewrite C; auto with asmgen. +- (* Ccompf *) + generalize (compare_float_spec rs (rs x) (rs x0)). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. case c; apply MATCH; assumption. + split. case c0; apply MATCH; assumption. auto. - (* Cnotcompf *) - generalize (compare_float_spec rs (rs (freg_of m0)) (rs (freg_of m1))). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. +- (* Cnotcompf *) + generalize (compare_float_spec rs (rs x) (rs x0)). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite <- Val.negate_cmpf_ne in B. rewrite <- Val.negate_cmpf_eq in A. - destruct c; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. + split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1. + destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. auto. - (* Ccompfzero *) - generalize (compare_float_spec rs (rs (freg_of m0)) (Vfloat Float.zero)). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. +- (* Ccompfzero *) + generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. case c; apply MATCH; assumption. + split. case c0; apply MATCH; assumption. auto. - (* Cnotcompf *) - generalize (compare_float_spec rs (rs (freg_of m0)) (Vfloat Float.zero)). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. +- (* Cnotcompf *) + generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite <- Val.negate_cmpf_ne in B. rewrite <- Val.negate_cmpf_eq in A. - destruct c; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. + split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1. + destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. auto. Qed. (** Translation of arithmetic operations. *) -Ltac Simpl := - match goal with - | [ |- context[nextinstr _ _] ] => rewrite nextinstr_inv; [auto | auto with ppcgen] - | [ |- context[Pregmap.get ?x (Pregmap.set ?x _ _)] ] => rewrite Pregmap.gss; auto - | [ |- context[Pregmap.set ?x _ _ ?x] ] => rewrite Pregmap.gss; auto - | [ |- context[Pregmap.get _ (Pregmap.set _ _ _)] ] => rewrite Pregmap.gso; [auto | auto with ppcgen] - | [ |- context[Pregmap.set _ _ _ _] ] => rewrite Pregmap.gso; [auto | auto with ppcgen] - end. - Ltac TranslOpSimpl := econstructor; split; [ apply exec_straight_one; [simpl; eauto | reflexivity ] | split; [try rewrite transl_shift_correct; repeat Simpl | intros; repeat Simpl] ]. Lemma transl_op_correct_same: - forall op args res k (rs: regset) m v, - wt_instr (Mop op args res) -> + forall op args res k c (rs: regset) m v, + transl_op op args res k = OK c -> eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v -> match op with Ocmp _ => False | _ => True end -> 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, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> r <> preg_of res -> rs'#r = rs#r. Proof. - intros. inv H. + intros until v; intros TR EV NOCMP. + unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; inv EV; try (TranslOpSimpl; fail). (* Omove *) - simpl in *. inv H0. - exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))). - split. unfold preg_of; rewrite <- H3. - destruct (mreg_type r1); apply exec_straight_one; auto. - split. Simpl. Simpl. - intros. Simpl. Simpl. - (* Other instructions *) - destruct op; simpl in H6; inv H6; TypeInv; simpl in H0; inv H0; try (TranslOpSimpl; fail). + exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of m0)))). + split. + destruct (preg_of res) eqn:RES; try discriminate; + destruct (preg_of m0) eqn:ARG; inv TR. + apply exec_straight_one; auto. + apply exec_straight_one; auto. + intuition Simpl. (* Ointconst *) - generalize (loadimm_correct (ireg_of res) i k rs m). intros [rs' [A [B C]]]. - exists rs'. split. auto. split. rewrite B; auto. intros. auto with ppcgen. + generalize (loadimm_correct x i k rs m). intros [rs' [A [B C]]]. + exists rs'; auto with asmgen. (* Oaddrstack *) - generalize (addimm_correct (ireg_of res) IR13 i k rs m). + generalize (addimm_correct x IR13 i k rs m). intros [rs' [EX [RES OTH]]]. - exists rs'. split. auto. split. auto. auto with ppcgen. + exists rs'; auto with asmgen. (* Oaddimm *) - generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m). + generalize (addimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. - exists rs'. split. auto. split. auto. auto with ppcgen. + exists rs'; auto with asmgen. (* Orsbimm *) - generalize (rsubimm_correct (ireg_of res) (ireg_of m0) i k rs m). + generalize (rsubimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. - exists rs'. - split. eauto. split. rewrite B. auto. - auto with ppcgen. + exists rs'; auto with asmgen. (* Omul *) - destruct (ireg_eq (ireg_of res) (ireg_of m0) || ireg_eq (ireg_of res) (ireg_of m1)). + destruct (ireg_eq x x0 || ireg_eq x x1). econstructor; split. eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split. repeat Simpl. - intros. repeat Simpl. + intuition Simpl. TranslOpSimpl. (* divs *) - econstructor. split. apply exec_straight_one. simpl. rewrite H2. reflexivity. auto. - split. repeat Simpl. intros. repeat Simpl. + econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. + intuition Simpl. (* divu *) - econstructor. split. apply exec_straight_one. simpl. rewrite H2. reflexivity. auto. - split. repeat Simpl. intros. repeat Simpl. + econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. + intuition Simpl. (* Oandimm *) - generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m - (ireg_of_not_IR14 m0)). + generalize (andimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. - exists rs'; auto with ppcgen. + exists rs'; auto with asmgen. (* Oorimm *) - generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m). + generalize (orimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. - exists rs'; auto with ppcgen. + exists rs'; auto with asmgen. (* Oxorimm *) - generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m). + generalize (xorimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. - exists rs'; auto with ppcgen. + exists rs'; auto with asmgen. (* Oshrximm *) exploit Val.shrx_shr; eauto. intros [n [i' [ARG1 [ARG2 RES]]]]. injection ARG2; intro ARG2'; subst i'; clear ARG2. set (islt := Int.lt n Int.zero) in *. set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero) m)). - assert (OTH1: forall r', important_preg r' = true -> rs1#r' = rs#r'). + assert (OTH1: forall r', data_preg r' = true -> rs1#r' = rs#r'). generalize (compare_int_spec rs (Vint n) (Vint Int.zero) m). fold rs1. intros [A B]. intuition. - exploit (addimm_correct IR14 (ireg_of m0) (Int.sub (Int.shl Int.one i) Int.one)). + exploit (addimm_correct IR14 x0 (Int.sub (Int.shl Int.one i) Int.one)). intros [rs2 [EXEC2 [RES2 OTH2]]]. set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))). - set (rs4 := nextinstr (rs3#(ireg_of res) <- (Val.shr rs3#IR14 (Vint i)))). + set (rs4 := nextinstr (rs3#x <- (Val.shr rs3#IR14 (Vint i)))). exists rs4; split. apply exec_straight_step with rs1 m. simpl. rewrite ARG1. auto. auto. eapply exec_straight_trans. eexact EXEC2. apply exec_straight_two with rs3 m. - simpl. rewrite OTH2. change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)). + simpl. rewrite OTH2; eauto with asmgen. + change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)). unfold Val.cmp, Val.cmp_bool. change (Int.cmp Cge n Int.zero) with (negb islt). - rewrite OTH2. rewrite OTH1. rewrite ARG1. + rewrite OTH2; eauto with asmgen. rewrite OTH1. rewrite ARG1. unfold rs3. case islt; reflexivity. - destruct m0; reflexivity. auto with ppcgen. auto with ppcgen. discriminate. discriminate. - simpl. auto. - auto. unfold rs3. case islt; auto. auto. - split. unfold rs4. repeat Simpl. unfold rs3. Simpl. destruct islt. - rewrite RES2. change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))). auto. - Simpl. rewrite <- ARG1; auto. - intros. unfold rs4; repeat Simpl. unfold rs3; repeat Simpl. - transitivity (rs2 r). destruct islt; auto. Simpl. - rewrite OTH2; auto with ppcgen. + rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen. + auto. + unfold rs3. destruct islt; auto. auto. + split. unfold rs4; Simpl. unfold rs3. destruct islt. + Simpl. rewrite RES2. unfold rs1. Simpl. + Simpl. congruence. + intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. (* intoffloat *) - econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto. - split; intros; repeat Simpl. + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + intuition Simpl. (* intuoffloat *) - econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto. - split; intros; repeat Simpl. + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + intuition Simpl. (* floatofint *) - econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto. - split; intros; repeat Simpl. + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + intuition Simpl. (* floatofintu *) - econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto. - split; intros; repeat Simpl. + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + intuition Simpl. (* Ocmp *) contradiction. Qed. Lemma transl_op_correct: - forall op args res k (rs: regset) m v, - wt_instr (Mop op args res) -> + forall op args res k c (rs: regset) m v, + transl_op op args res k = OK c -> eval_operation ge rs#IR13 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 /\ Val.lessdef v rs'#(preg_of res) - /\ forall r, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> r <> preg_of res -> rs'#r = rs#r. Proof. intros. assert (EITHER: match op with Ocmp _ => False | _ => True end \/ exists cmp, op = Ocmp cmp). - destruct op; auto. right; exists c; auto. - destruct EITHER as [A | [c A]]. + destruct op; auto. right; exists c0; auto. + destruct EITHER as [A | [cmp A]]. exploit transl_op_correct_same; eauto. intros [rs' [P [Q R]]]. subst v. exists rs'; eauto. (* Ocmp *) - subst op. inv H. simpl in H5. inv H5. simpl in H0. inv H0. - destruct (transl_cond_correct c args - (Pmov (ireg_of res) (SOimm Int.zero) - :: Pmovc (crbit_for_cond c) (ireg_of res) (SOimm Int.one) :: k) - rs m H1) - as [rs1 [A [B C]]]. - set (rs2 := nextinstr (rs1#(ireg_of res) <- (Vint Int.zero))). - set (v := match rs2#(crbit_for_cond c) with - | Vint n => if Int.eq n Int.zero then Vint Int.zero else Vint Int.one - | _ => Vundef - end). - set (rs3 := nextinstr (rs2#(ireg_of res) <- v)). + subst op. simpl in H. monadInv H. simpl in H0. inv H0. + rewrite (ireg_of_eq _ _ EQ). + exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]]. + set (rs2 := nextinstr (rs1#x <- (Vint Int.zero))). + set (rs3 := nextinstr (match rs2#(crbit_for_cond cmp) with + | Vint n => if Int.eq n Int.zero then rs2 else rs2#x <- Vone + | _ => rs2#x <- Vundef + end)). exists rs3; split. - eapply exec_straight_trans. eauto. - apply exec_straight_two with rs2 m; auto. - simpl. unfold rs3, v. - destruct (rs2 (crbit_for_cond c)) eqn:?; auto. - destruct (Int.eq i Int.zero); auto. - decEq. decEq. apply extensionality; intros. unfold Pregmap.set. - destruct (PregEq.eq x (ireg_of res)); auto. subst. - unfold rs2. Simpl. Simpl. - replace (preg_of res) with (IR (ireg_of res)). - split. unfold rs3. Simpl. Simpl. - destruct (eval_condition c rs ## (preg_of ## args) m); simpl; auto. - unfold v. unfold rs2. Simpl. Simpl. rewrite B. - destruct b; simpl; auto. - intros. unfold rs3. repeat Simpl. unfold rs2. repeat Simpl. - unfold preg_of; rewrite H2; auto. + eapply exec_straight_trans. eexact A. apply exec_straight_two with rs2 m. + auto. + simpl. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto. + auto. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto. + split. unfold rs3. Simpl. + replace (rs2 (crbit_for_cond cmp)) with (rs1 (crbit_for_cond cmp)). + destruct (eval_condition cmp rs##(preg_of##args) m) as [[]|]; simpl in *. + rewrite B. simpl. Simpl. + rewrite B. simpl. unfold rs2. Simpl. + auto. + destruct cmp; reflexivity. + intros. transitivity (rs2 r). + unfold rs3. destruct (rs2 (crbit_for_cond cmp)); Simpl. destruct (Int.eq i Int.zero); auto; Simpl. + unfold rs2. Simpl. Qed. Remark val_add_add_zero: @@ -1276,43 +839,40 @@ Proof. intros. destruct v1; destruct v2; simpl; auto; rewrite Int.add_zero; auto. Qed. -Lemma transl_load_store_correct: - forall (mk_instr_imm: ireg -> int -> instruction) +Lemma transl_memory_access_correct: + forall (P: regset -> Prop) (mk_instr_imm: ireg -> int -> instruction) (mk_instr_gen: option (ireg -> shift_addr -> instruction)) (is_immed: int -> bool) - addr args k ms sp rs m ms' m', + addr args k c (rs: regset) a m m', + transl_memory_access mk_instr_imm mk_instr_gen is_immed addr args k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> (forall (r1: ireg) (rs1: regset) n k, - eval_addressing ge sp addr (map rs (map preg_of args)) = Some(Val.add rs1#r1 (Vint n)) -> + Val.add rs1#r1 (Vint n) = a -> (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) -> exists rs', - exec_straight (mk_instr_imm r1 n :: k) rs1 m k rs' m' /\ - agree ms' sp rs') -> + exec_straight ge fn (mk_instr_imm r1 n :: k) rs1 m k rs' m' /\ P rs') -> match mk_instr_gen with | None => True | Some mk => (forall (r1: ireg) (sa: shift_addr) (rs1: regset) k, - eval_addressing ge sp addr (map rs (map preg_of args)) = Some(Val.add rs1#r1 (eval_shift_addr sa rs1)) -> + Val.add rs1#r1 (eval_shift_addr sa rs1) = a -> (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) -> exists rs', - exec_straight (mk r1 sa :: k) rs1 m k rs' m' /\ - agree ms' sp rs') + exec_straight ge fn (mk r1 sa :: k) rs1 m k rs' m' /\ P rs') end -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> exists rs', - exec_straight (transl_load_store mk_instr_imm mk_instr_gen is_immed addr args 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 EA MK1 MK2. + unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in EA; inv EA. (* Aindexed *) case (is_immed i). (* Aindexed, small displacement *) - apply H; auto. + apply MK1; auto. (* Aindexed, large displacement *) - destruct (addimm_correct IR14 (ireg_of m0) i (mk_instr_imm IR14 Int.zero :: k) rs m) + destruct (addimm_correct IR14 x i (mk_instr_imm IR14 Int.zero :: k) rs m) as [rs' [A [B C]]]. - exploit (H IR14 rs' Int.zero); eauto. + exploit (MK1 IR14 rs' Int.zero); eauto. rewrite B. rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity. intros [rs'' [D E]]. exists rs''; split. @@ -1320,13 +880,12 @@ Proof. (* Aindexed2 *) destruct mk_instr_gen as [mk | ]. (* binary form available *) - apply H0; auto. + apply MK2; auto. (* binary form not available *) - set (rs' := nextinstr (rs#IR14 <- (Val.add (rs (ireg_of m0)) (rs (ireg_of m1))))). - exploit (H IR14 rs' Int.zero); eauto. - unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - decEq. apply val_add_add_zero. - unfold rs'. intros. repeat Simpl. + set (rs' := nextinstr (rs#IR14 <- (Val.add (rs x) (rs x0)))). + exploit (MK1 IR14 rs' Int.zero); eauto. + unfold rs'. Simpl. symmetry. apply val_add_add_zero. + intros. unfold rs'. Simpl. intros [rs'' [A B]]. exists rs''; split. eapply exec_straight_step with (rs2 := rs'); eauto. @@ -1334,189 +893,172 @@ Proof. (* Aindexed2shift *) destruct mk_instr_gen as [mk | ]. (* binary form available *) - apply H0; auto. rewrite transl_shift_addr_correct. auto. + apply MK2; auto. rewrite transl_shift_addr_correct. auto. (* binary form not available *) - set (rs' := nextinstr (rs#IR14 <- (Val.add (rs (ireg_of m0)) (eval_shift s (rs (ireg_of m1)))))). - exploit (H IR14 rs' Int.zero); eauto. - unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - decEq. apply val_add_add_zero. - unfold rs'; intros; repeat Simpl. + set (rs' := nextinstr (rs#IR14 <- (Val.add (rs x) (eval_shift s (rs x0))))). + exploit (MK1 IR14 rs' Int.zero); eauto. + unfold rs'. Simpl. symmetry. apply val_add_add_zero. + intros; unfold rs'; Simpl. intros [rs'' [A B]]. exists rs''; split. eapply exec_straight_step with (rs2 := rs'); eauto. simpl. rewrite transl_shift_correct. auto. auto. (* Ainstack *) - destruct (is_immed i). + destruct (is_immed i); inv TR. (* Ainstack, short displacement *) - apply H; auto. rewrite (sp_val _ _ _ H1). auto. + apply MK1; auto. (* Ainstack, large displacement *) destruct (addimm_correct IR14 IR13 i (mk_instr_imm IR14 Int.zero :: k) rs m) as [rs' [A [B C]]]. - exploit (H IR14 rs' Int.zero); eauto. - rewrite (sp_val _ _ _ H1). rewrite B. rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. auto. + exploit (MK1 IR14 rs' Int.zero); eauto. + rewrite B. rewrite Val.add_assoc. f_equal. simpl. rewrite Int.add_zero; auto. intros [rs'' [D E]]. exists rs''; split. eapply exec_straight_trans. eexact A. eexact D. auto. Qed. Lemma transl_load_int_correct: - forall (mk_instr: ireg -> ireg -> shift_addr -> instruction) - (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m m' chunk a v, - (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset), - exec_instr ge c (mk_instr r1 r2 sa) rs1 m' = - exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m') -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - mreg_type rd = Tint -> - eval_addressing ge sp addr (map ms args) = Some a -> + forall mk_instr is_immed dst addr args k c (rs: regset) a chunk m v, + transl_memory_access_int mk_instr is_immed dst addr args k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> - Mem.extends m m' -> + (forall (r1 r2: ireg) (sa: shift_addr) (rs1: regset), + exec_instr ge fn (mk_instr r1 r2 sa) rs1 m = + exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) -> exists rs', - exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m' - k rs' m' - /\ agree (Regmap.set rd v (undef_temps ms)) sp rs'. + exec_straight ge fn c rs m k rs' m + /\ rs'#(preg_of dst) = v + /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros. unfold transl_load_store_int. - 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. - intros. - assert (Val.add (rs1 r1) (Vint n) = a') by congruence. - exists (nextinstr (rs1#(ireg_of rd) <- v')); split. - apply exec_straight_one. rewrite H. unfold exec_load. - simpl. rewrite H8. rewrite C. auto. auto. - apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. - unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. - unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen. - intros. - assert (Val.add (rs1 r1) (eval_shift_addr sa rs1) = a') by congruence. - exists (nextinstr (rs1#(ireg_of rd) <- v')); split. - apply exec_straight_one. rewrite H. unfold exec_load. - simpl. rewrite H8. rewrite C. auto. auto. - apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. - unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. - unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen. + intros. monadInv H. erewrite ireg_of_eq by eauto. + eapply transl_memory_access_correct; eauto. + intros; simpl. econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_load. simpl eval_shift_addr. rewrite H. rewrite H1. eauto. auto. + split. Simpl. intros; Simpl. + simpl; intros. + econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto. + split. Simpl. intros; Simpl. Qed. Lemma transl_load_float_correct: - forall (mk_instr: freg -> ireg -> int -> instruction) - (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m m' chunk a v, - (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset), - exec_instr ge c (mk_instr r1 r2 n) rs1 m' = - exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m') -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - mreg_type rd = Tfloat -> - eval_addressing ge sp addr (map ms args) = Some a -> + forall mk_instr is_immed dst addr args k c (rs: regset) a chunk m v, + transl_memory_access_float mk_instr is_immed dst addr args k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> - Mem.extends m m' -> + (forall (r1: freg) (r2: ireg) (n: int) (rs1: regset), + exec_instr ge fn (mk_instr r1 r2 n) rs1 m = + exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) -> exists rs', - exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m' - k rs' m' - /\ agree (Regmap.set rd v (undef_temps ms)) sp rs'. + exec_straight ge fn c rs m k rs' m + /\ rs'#(preg_of dst) = v + /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros. unfold transl_load_store_int. - 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. - intros. - assert (Val.add (rs1 r1) (Vint n) = a') by congruence. - exists (nextinstr (rs1#(freg_of rd) <- v')); split. - apply exec_straight_one. rewrite H. unfold exec_load. - simpl. rewrite H8. rewrite C. auto. auto. - apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. - unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. - unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen. + intros. monadInv H. erewrite freg_of_eq by eauto. + eapply transl_memory_access_correct; eauto. + intros; simpl. econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto. + split. Simpl. intros; Simpl. + simpl; auto. Qed. Lemma transl_store_int_correct: - forall (mk_instr: ireg -> ireg -> shift_addr -> instruction) - (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m1 chunk a m2 m1', - (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset), - exec_instr ge c (mk_instr r1 r2 sa) rs1 m1' = - exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m1') -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - mreg_type rd = Tint -> - eval_addressing ge sp addr (map ms args) = Some a -> - Mem.storev chunk m1 a (ms rd) = Some m2 -> - Mem.extends m1 m1' -> - exists m2', - Mem.extends m2 m2' /\ - exists rs', - exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m1' - k rs' m2' - /\ agree (undef_temps ms) sp rs'. -Proof. - intros. unfold transl_load_store_int. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. - unfold PregEq.t. - intros [a' [A B]]. - exploit preg_val; eauto. instantiate (1 := rd). intros C. - exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]]. - exists m2'; split; auto. - apply transl_load_store_correct with ms; auto. - intros. - assert (Val.add (rs1 r1) (Vint n) = a') by congruence. - exists (nextinstr rs1); split. - apply exec_straight_one. rewrite H. simpl. rewrite H8. - unfold exec_store. rewrite H7; auto with ppcgen. rewrite D. auto. auto. - apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen. - intros. - assert (Val.add (rs1 r1) (eval_shift_addr sa rs1) = a') by congruence. - exists (nextinstr rs1); split. - apply exec_straight_one. rewrite H. simpl. rewrite H8. - unfold exec_store. rewrite H7; auto with ppcgen. rewrite D. auto. auto. - apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen. + forall mk_instr is_immed src addr args k c (rs: regset) a chunk m m', + transl_memory_access_int mk_instr is_immed src addr args k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> + Mem.storev chunk m a rs#(preg_of src) = Some m' -> + (forall (r1 r2: ireg) (sa: shift_addr) (rs1: regset), + exec_instr ge fn (mk_instr r1 r2 sa) rs1 m = + exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) -> + exists rs', + exec_straight ge fn c rs m k rs' m' + /\ forall r, nontemp_preg r = true -> rs'#r = rs#r. +Proof. + intros. monadInv H. erewrite ireg_of_eq in * by eauto. + eapply transl_memory_access_correct; eauto. + intros; simpl. econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_store. simpl eval_shift_addr. rewrite H. rewrite H3; eauto with asmgen. + rewrite H1. eauto. auto. + intros; Simpl. + simpl; intros. + econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_store. rewrite H. rewrite H3; eauto with asmgen. + rewrite H1. eauto. auto. + intros; Simpl. Qed. Lemma transl_store_float_correct: - forall (mk_instr: freg -> ireg -> int -> instruction) - (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m1 chunk a m2 m1', - (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset) m2', - exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m1' = OK (nextinstr rs1) m2' -> - exists rs2, - exec_instr ge c (mk_instr r1 r2 n) rs1 m1' = OK rs2 m2' - /\ (forall (r: preg), r <> FR7 -> rs2 r = nextinstr rs1 r)) -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - mreg_type rd = Tfloat -> - eval_addressing ge sp addr (map ms args) = Some a -> - Mem.storev chunk m1 a (ms rd) = Some m2 -> - Mem.extends m1 m1' -> - exists m2', - Mem.extends m2 m2' /\ - exists rs', - exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m1' - k rs' m2' - /\ agree (undef_temps ms) sp rs'. -Proof. - intros. unfold transl_load_store_float. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. - unfold PregEq.t. - intros [a' [A B]]. - exploit preg_val; eauto. instantiate (1 := rd). intros C. - exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]]. - exists m2'; split; auto. - apply transl_load_store_correct with ms; auto. - intros. - assert (Val.add (rs1 r1) (Vint n) = a') by congruence. - exploit (H fn (freg_of rd) r1 n rs1 m2'). - unfold exec_store. rewrite H8. rewrite H7; auto with ppcgen. rewrite D. auto. - intros [rs2 [P Q]]. - exists rs2; split. apply exec_straight_one. auto. rewrite Q; auto with ppcgen. - apply agree_exten_temps with rs; auto. - intros. rewrite Q; auto with ppcgen. Simpl. apply H7; auto with ppcgen. -Qed. + forall mk_instr is_immed src addr args k c (rs: regset) a chunk m m', + transl_memory_access_float mk_instr is_immed src addr args k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> + Mem.storev chunk m a rs#(preg_of src) = Some m' -> + (forall (r1: freg) (r2: ireg) (n: int) (rs1: regset), + exec_instr ge fn (mk_instr r1 r2 n) rs1 m = + exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) -> + exists rs', + exec_straight ge fn c rs m k rs' m' + /\ forall r, nontemp_preg r = true -> rs'#r = rs#r. +Proof. + intros. monadInv H. erewrite freg_of_eq in * by eauto. + eapply transl_memory_access_correct; eauto. + intros; simpl. econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_store. rewrite H. rewrite H3; eauto with asmgen. + rewrite H1. eauto. auto. + intros; Simpl. + simpl; auto. +Qed. + +Lemma transl_load_correct: + forall chunk addr args dst k c (rs: regset) a m v, + transl_load chunk addr args dst k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> + Mem.loadv chunk m a = Some v -> + exists rs', + exec_straight ge fn c rs m k rs' m + /\ rs'#(preg_of dst) = v + /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. +Proof. + intros. destruct chunk; simpl in H. + eapply transl_load_int_correct; eauto. + eapply transl_load_int_correct; eauto. + eapply transl_load_int_correct; eauto. + eapply transl_load_int_correct; eauto. + eapply transl_load_int_correct; eauto. + eapply transl_load_float_correct; eauto. + apply Mem.loadv_float64al32 in H1. eapply transl_load_float_correct; eauto. + eapply transl_load_float_correct; eauto. +Qed. + +Lemma transl_store_correct: + forall chunk addr args src k c (rs: regset) a m m', + transl_store chunk addr args src k = OK c -> + eval_addressing ge (rs#SP) 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, nontemp_preg r = true -> rs'#r = rs#r. +Proof. + intros. destruct chunk; simpl in H. +- 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 transl_store_int_correct; eauto. +- eapply transl_store_int_correct; eauto. +- 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 transl_store_int_correct; eauto. +- eapply transl_store_int_correct; eauto. +- eapply transl_store_int_correct; eauto. +- unfold transl_memory_access_float in H. monadInv H. rewrite (freg_of_eq _ _ EQ) in *. + eapply transl_memory_access_correct; eauto. + intros. econstructor; split. apply exec_straight_one. + simpl. unfold exec_store. rewrite H. rewrite H2; eauto with asmgen. + rewrite H1. eauto. auto. intros. Simpl. + simpl; auto. +- apply Mem.storev_float64al32 in H1. eapply transl_store_float_correct; eauto. +- eapply transl_store_float_correct; eauto. +Qed. + +End CONSTRUCTORS. -End STRAIGHTLINE. diff --git a/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v deleted file mode 100644 index 2d3c72d3..00000000 --- a/arm/Asmgenretaddr.v +++ /dev/null @@ -1,217 +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 (fn_code (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 iterate_op_tail: - forall op1 op2 l k, is_tail k (iterate_op op1 op2 l k). -Proof. - intros. unfold iterate_op. - destruct l. - auto with coqlib. - constructor. revert l; induction l; simpl; auto with coqlib. -Qed. -Hint Resolve iterate_op_tail: ppcretaddr. - -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_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 rsubimm_tail: - forall r1 r2 n k, is_tail k (rsubimm r1 r2 n k). -Proof. unfold rsubimm; intros; IsTail. Qed. -Hint Resolve rsubimm_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 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_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 is_immed addr args k, - is_tail k (transl_load_store mk1 mk2 is_immed addr args k). -Proof. unfold transl_load_store; intros; destruct addr; IsTail. - destruct mk2; IsTail. destruct mk2; IsTail. Qed. -Hint Resolve transl_load_store_tail: ppcretaddr. - -Lemma transl_load_store_int_tail: - forall mk is_immed rd addr args k, - is_tail k (transl_load_store_int mk is_immed rd addr args k). -Proof. unfold transl_load_store_int; intros; IsTail. Qed. -Hint Resolve transl_load_store_int_tail: ppcretaddr. - -Lemma transl_load_store_float_tail: - forall mk is_immed rd addr args k, - is_tail k (transl_load_store_float mk is_immed rd addr args k). -Proof. unfold transl_load_store_float; intros; IsTail. Qed. -Hint Resolve transl_load_store_float_tail: ppcretaddr. - -Lemma loadind_int_tail: - forall base ofs dst k, is_tail k (loadind_int base ofs dst k). -Proof. unfold loadind_int; intros; IsTail. Qed. -Hint Resolve loadind_int_tail: ppcretaddr. - -Lemma loadind_tail: - forall base ofs ty dst k, is_tail k (loadind base ofs ty dst k). -Proof. unfold loadind, loadind_float; intros; IsTail. Qed. -Hint Resolve loadind_tail: ppcretaddr. - -Lemma storeind_int_tail: - forall src base ofs k, is_tail k (storeind_int src base ofs k). -Proof. unfold storeind_int; intros; IsTail. Qed. -Hint Resolve storeind_int_tail: ppcretaddr. - -Lemma storeind_tail: - forall src base ofs ty k, is_tail k (storeind src base ofs ty k). -Proof. unfold storeind, storeind_float; intros; IsTail. Qed. -Hint Resolve storeind_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.(Mach.fn_code) -> - exists ra, return_address_offset f c ra. -Proof. - intros. assert (is_tail (transl_code f c) (fn_code (transl_function f))). - unfold transl_function. simpl. 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/arm/PrintAsm.ml b/arm/PrintAsm.ml index 278b6b18..f5b04b54 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -593,14 +593,14 @@ let print_instruction oc = function fprintf oc " fsts %a, [%a, #%a]\n" freg_single FR6 ireg r2 coqint n; 2 (* Pseudo-instructions *) | Pallocframe(sz, ofs) -> - fprintf oc " mov r12, sp\n"; + fprintf oc " mov r10, sp\n"; let ninstr = ref 0 in List.iter (fun n -> fprintf oc " sub sp, sp, #%a\n" coqint n; incr ninstr) (Asmgen.decompose_int sz); - fprintf oc " str r12, [sp, #%a]\n" coqint ofs; + fprintf oc " str r10, [sp, #%a]\n" coqint ofs; 2 + !ninstr | Pfreeframe(sz, ofs) -> if Asmgen.is_immed_arith sz @@ -614,7 +614,8 @@ let print_instruction oc = function fprintf oc " ldr %a, .L%d @ %a\n" ireg r1 lbl print_symb_ofs (id, ofs); 1 | Pbtbl(r, tbl) -> - fprintf oc " ldr pc, [pc, %a]\n" ireg r; + fprintf oc " mov r14, %a, lsl #2\n"; + fprintf oc " ldr pc, [pc, r14]\n"; fprintf oc " mov r0, r0\n"; (* no-op *) List.iter (fun l -> fprintf oc " .word %a\n" print_label l) -- cgit