From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asm.v | 24 ++-- powerpc/Asmgen.v | 8 +- powerpc/Asmgenproof.v | 64 ++++----- powerpc/Asmgenproof1.v | 54 +++---- powerpc/Asmgenretaddr.v | 4 +- powerpc/ConstpropOpproof.v | 83 +++++------ powerpc/Op.v | 327 ++++++++++++++++++++++++++++++------------- powerpc/PrintAsm.ml | 13 +- powerpc/SelectOp.v | 2 +- powerpc/SelectOpproof.v | 80 ++++++----- powerpc/eabi/Stacklayout.v | 85 +++++++++-- powerpc/macosx/Stacklayout.v | 85 +++++++++-- 12 files changed, 536 insertions(+), 293 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index e49986f6..d698524d 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -130,7 +130,7 @@ Inductive instruction : Type := | Paddi: ireg -> ireg -> constant -> instruction (**r add immediate *) | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) | Paddze: ireg -> ireg -> instruction (**r add Carry bit *) - | Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *) + | Pallocframe: Z -> int -> instruction (**r allocate new stack frame *) | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) @@ -154,7 +154,7 @@ Inductive instruction : Type := | Peqv: ireg -> ireg -> ireg -> instruction (**r bitwise not-xor *) | Pextsb: ireg -> ireg -> instruction (**r 8-bit sign extension *) | Pextsh: ireg -> ireg -> instruction (**r 16-bit sign extension *) - | Pfreeframe: Z -> Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) + | Pfreeframe: Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) | Pfabs: freg -> freg -> instruction (**r float absolute value *) | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) | Pfcmpu: freg -> freg -> instruction (**r float comparison *) @@ -249,19 +249,19 @@ lbl: .double floatcst lfd rdst, 0(r1) addi r1, r1, 8 >> -- [Pallocframe lo hi ofs]: in the formal semantics, this pseudo-instruction - allocates a memory block with bounds [lo] and [hi], stores the value +- [Pallocframe sz ofs]: in the formal semantics, this pseudo-instruction + allocates a memory block with bounds [0] and [sz], stores the value of register [r1] (the stack pointer, by convention) at offset [ofs] in this block, and sets [r1] to a pointer to the bottom of this block. In the printed PowerPC assembly code, this allocation is just a store-decrement of register [r1], assuming that [ofs = 0]: << - stwu r1, (lo - hi)(r1) + stwu r1, -sz(r1) >> This cannot be expressed in our memory model, which does not reflect the fact that stack frames are adjacent and allocated/freed following a stack discipline. -- [Pfreeframe lo hi ofs]: in the formal semantics, this pseudo-instruction +- [Pfreeframe sz ofs]: in the formal semantics, this pseudo-instruction reads the word at offset [ofs] in the block pointed by [r1] (the stack pointer), frees this block, and sets [r1] to the value of the word at offset [ofs]. In the printed PowerPC assembly code, this @@ -527,9 +527,9 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m | Paddze rd r1 => OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY))) m - | Pallocframe lo hi ofs => - let (m1, stk) := Mem.alloc m lo hi in - let sp := Vptr stk (Int.repr lo) in + | Pallocframe sz ofs => + let (m1, stk) := Mem.alloc m 0 sz in + let sp := Vptr stk Int.zero in match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with | None => Error | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)) m2 @@ -570,7 +570,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pbtbl r tbl => match gpr_or_zero rs r with | Vint n => - let pos := Int.signed n in + let pos := Int.unsigned n in if zeq (Zmod pos 4) 0 then match list_nth_z tbl (pos / 4) with | None => Error @@ -599,13 +599,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m | Pextsh rd r1 => OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m - | Pfreeframe lo hi ofs => + | Pfreeframe sz ofs => match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with | None => Error | Some v => match rs#GPR1 with | Vptr stk ofs => - match Mem.free m stk lo hi with + match Mem.free m stk 0 sz with | None => Error | Some m' => OK (nextinstr (rs#GPR1 <- v)) m' end diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 9c37c42f..5e3d39b3 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -466,12 +466,12 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Pmtctr (ireg_of r) :: Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR0 :: - Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: + Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbctr :: k | Mtailcall sig (inr symb) => Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR0 :: - Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: + Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbs symb :: k | Mbuiltin ef args res => Pbuiltin ef (map preg_of args) (preg_of res) :: k @@ -489,7 +489,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := | Mreturn => Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR0 :: - Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: + Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pblr :: k end. @@ -502,7 +502,7 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) := around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: + Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: Pmflr GPR0 :: Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: transl_code f f.(fn_code). diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 54e454e8..83193638 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -750,12 +750,12 @@ Proof. Qed. Lemma exec_Mgetparam_prop: - forall (s : list stackframe) (fb : block) (f: Mach.function) (sp parent : val) + 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 -> - load_stack m parent ty ofs = Some v -> + 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 (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0 (Machconcr.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m). Proof. @@ -792,7 +792,7 @@ 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 = Some v -> + eval_operation ge sp op ms ## args m = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0 (Machconcr.State s fb sp c (Regmap.set res v (undef_op op ms)) m). Proof. @@ -800,7 +800,7 @@ Proof. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. left; eapply exec_straight_steps; eauto with coqlib. - simpl. eapply transl_op_correct; auto. + simpl. eapply transl_op_correct; eauto. rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. Qed. @@ -810,8 +810,8 @@ Remark loadv_8_signed_unsigned: exists v', Mem.loadv Mint8unsigned m a = Some v' /\ v = Val.sign_ext 8 v'. Proof. unfold Mem.loadv; intros. destruct a; try congruence. - generalize (Mem.load_int8_signed_unsigned m b (Int.signed i)). - rewrite H. destruct (Mem.load Mint8unsigned m b (Int.signed i)). + generalize (Mem.load_int8_signed_unsigned m b (Int.unsigned i)). + rewrite H. destruct (Mem.load Mint8unsigned m b (Int.unsigned i)). simpl; intros. exists v0; split; congruence. simpl; congruence. Qed. @@ -987,7 +987,7 @@ Lemma exec_Mtailcall_prop: 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 (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 (Callstate s f' ms m'). @@ -1155,7 +1155,7 @@ Lemma exec_Mcond_true_prop: (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 = Some true -> + eval_condition cond ms ## args m = Some true -> Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 @@ -1168,8 +1168,7 @@ Proof. if snd (crbit_for_cond cond) then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c). - generalize (transl_cond_correct tge (transl_function f) - cond args k1 ms sp rs m' true H3 AG H). + exploit transl_cond_correct; eauto. simpl. intros [rs2 [EX [RES AG2]]]. inv AT. simpl in H5. generalize (functions_transl _ _ H4); intro FN. @@ -1198,29 +1197,22 @@ 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 = Some false -> + eval_condition cond ms ## args m = Some false -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 (Machconcr.State s fb sp c (undef_temps ms) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inversion WTI. - pose (k1 := - if snd (crbit_for_cond cond) - then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c - else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c). - generalize (transl_cond_correct tge (transl_function f) - cond args k1 ms sp rs m' false H1 AG H). + exploit transl_cond_correct; eauto. simpl. intros [rs2 [EX [RES AG2]]]. left; eapply exec_straight_steps; eauto with coqlib. exists (nextinstr rs2); split. simpl. eapply exec_straight_trans. eexact EX. caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES. - unfold k1; rewrite ISSET; apply exec_straight_one. - simpl. rewrite RES. reflexivity. + apply exec_straight_one. simpl. rewrite RES. reflexivity. reflexivity. - unfold k1; rewrite ISSET; apply exec_straight_one. - simpl. rewrite RES. reflexivity. + apply exec_straight_one. simpl. rewrite RES. reflexivity. reflexivity. auto with ppcgen. Qed. @@ -1231,7 +1223,7 @@ Lemma exec_Mjumptable_prop: (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label) (c' : Mach.code), rs arg = Vint n -> - list_nth_z tbl (Int.signed n) = Some lbl -> + list_nth_z tbl (Int.unsigned n) = Some lbl -> Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop @@ -1243,13 +1235,10 @@ Proof. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inv WTI. exploit list_nth_z_range; eauto. intro RANGE. - assert (SHIFT: Int.signed (Int.rolm n (Int.repr 2) (Int.repr (-4))) = Int.signed n * 4). + assert (SHIFT: Int.unsigned (Int.rolm n (Int.repr 2) (Int.repr (-4))) = Int.unsigned n * 4). replace (Int.repr (-4)) with (Int.shl Int.mone (Int.repr 2)). rewrite <- Int.shl_rolm. rewrite Int.shl_mul. - rewrite Int.mul_signed. - apply Int.signed_repr. - split. apply Zle_trans with 0. compute; congruence. omega. - omega. + unfold Int.mul. apply Int.unsigned_repr. omega. compute. reflexivity. apply Int.mkint_eq. compute. reflexivity. inv AT. simpl in H7. @@ -1274,11 +1263,10 @@ Proof. eapply exec_straight_steps_1; eauto. econstructor; eauto. eapply find_instr_tail. unfold k1 in CT1. eauto. - unfold exec_instr. + unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen. change (rs1 GPR12) with (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))). -Opaque Zmod. Opaque Zdiv. - simpl. rewrite SHIFT. rewrite Z_mod_mult. rewrite zeq_true. - rewrite Z_div_mult. + 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. econstructor; eauto. eapply Mach.find_label_incl; eauto. @@ -1295,7 +1283,7 @@ Lemma exec_Mreturn_prop: 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 (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 (Returnstate s ms m'). Proof. @@ -1356,12 +1344,12 @@ Lemma exec_function_internal_prop: forall (s : list stackframe) (fb : block) (ms : Mach.regset) (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block), Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mem.alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) -> - let sp := Vptr stk (Int.repr (- fn_framesize f)) in + 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 (Machconcr.Callstate s fb ms m) E0 - (Machconcr.State s fb sp (fn_code f) ms m3). + (Machconcr.State s fb sp (fn_code f) (undef_temps ms) m3). Proof. intros; red; intros; inv MS. assert (WTF: wt_function f). @@ -1405,7 +1393,7 @@ Proof. assert (AG2: agree ms sp rs2). split. reflexivity. unfold sp. congruence. intros. unfold rs2. rewrite nextinstr_inv. - repeat (rewrite Pregmap.gso). elim AG; auto. + repeat (rewrite Pregmap.gso). inv AG; auto. auto with ppcgen. auto with ppcgen. auto with ppcgen. assert (AG4: agree ms sp rs4). unfold rs4, rs3; auto with ppcgen. @@ -1414,7 +1402,7 @@ Proof. eapply exec_straight_steps_1; eauto. change (Int.unsigned Int.zero) with 0. constructor. (* match states *) - econstructor; eauto with coqlib. + econstructor; eauto with coqlib. auto with ppcgen. Qed. Lemma exec_function_external_prop: diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index d428543c..16dd923e 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1110,12 +1110,13 @@ Proof. Qed. Lemma transl_cond_correct: - forall cond args k ms sp rs m b, + forall cond args k ms sp rs m m' b, map mreg_type args = type_of_condition cond -> agree ms sp rs -> - eval_condition cond (map ms args) = Some b -> + eval_condition cond (map ms args) m = Some b -> + Mem.extends m m' -> exists rs', - exec_straight (transl_cond cond args k) rs m k rs' m + exec_straight (transl_cond cond args k) rs m' k rs' m' /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then Val.of_bool b @@ -1124,9 +1125,9 @@ Lemma transl_cond_correct: Proof. intros. assert (eval_condition_total cond rs ## (preg_of ## args) = Val.of_bool b). - apply eval_condition_weaken. eapply eval_condition_lessdef; eauto. + apply eval_condition_weaken with m'. eapply eval_condition_lessdef; eauto. eapply preg_vals; eauto. - rewrite <- H2. eapply transl_cond_correct_aux; eauto. + rewrite <- H3. eapply transl_cond_correct_aux; eauto. Qed. (** Translation of arithmetic operations. *) @@ -1155,21 +1156,22 @@ Ltac TranslOpSimpl := *) Lemma transl_op_correct: - forall op args res k ms sp rs m v, + forall op args res k ms sp rs m v m', wt_instr (Mop op args res) -> agree ms sp rs -> - eval_operation ge sp op (map ms args) = Some v -> + eval_operation ge sp op (map ms args) m = Some v -> + Mem.extends m m' -> exists rs', - exec_straight (transl_op op args res k) rs m k rs' m + exec_straight (transl_op op args res k) rs m' k rs' m' /\ agree (Regmap.set res v (undef_op op ms)) sp rs'. Proof. intros. assert (exists v', Val.lessdef v v' /\ eval_operation_total ge sp op (map rs (map preg_of args)) = v'). - exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. + exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. intros [v' [A B]]. exists v'; split; auto. - apply eval_operation_weaken; eauto. - destruct H2 as [v' [LD EQ]]. clear H1. + eapply eval_operation_weaken; eauto. + destruct H3 as [v' [LD EQ]]. clear H1 H2. inv H. (* Omove *) simpl in *. @@ -1183,7 +1185,7 @@ Proof. (* Omove again *) congruence. (* Ointconst *) - destruct (loadimm_correct (ireg_of res) i k rs m) + destruct (loadimm_correct (ireg_of res) i k rs m') as [rs' [A [B C]]]. exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. @@ -1198,7 +1200,7 @@ Proof. set (v' := symbol_offset ge i i0) in *. pose (rs1 := nextinstr (rs#GPR12 <- (high_half v'))). exists (nextinstr (rs1#(ireg_of res) <- v')). - split. apply exec_straight_two with rs1 m. + split. apply exec_straight_two with rs1 m'. unfold exec_instr. rewrite gpr_or_zero_zero. unfold const_high. rewrite Val.add_commut. rewrite high_half_zero. reflexivity. @@ -1213,7 +1215,7 @@ Proof. intros. apply Pregmap.gso; auto. (* Oaddrstack *) assert (GPR1 <> GPR0). discriminate. - generalize (addimm_correct (ireg_of res) GPR1 i k rs m (ireg_of_not_GPR0 res) H1). + generalize (addimm_correct (ireg_of res) GPR1 i k rs m' (ireg_of_not_GPR0 res) H1). intros [rs' [EX [RES OTH]]]. exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto with ppcgen. @@ -1235,7 +1237,7 @@ Proof. unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto. rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto. (* Oaddimm *) - generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m + generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m' (ireg_of_not_GPR0 res) (ireg_of_not_GPR0 m0)). intros [rs' [A [B C]]]. exists rs'. split. auto. @@ -1245,7 +1247,7 @@ Proof. econstructor; split. apply exec_straight_one. simpl; eauto. auto. auto 7 with ppcgen. - generalize (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m). + generalize (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m'). intros [rs1 [EX [RES OTH]]]. econstructor; split. eapply exec_straight_trans. eexact EX. @@ -1258,7 +1260,7 @@ Proof. econstructor; split. apply exec_straight_one. simpl; eauto. auto. auto with ppcgen. - generalize (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m). + generalize (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m'). intros [rs1 [EX [RES OTH]]]. assert (agree (undef_temps ms) sp rs1). eauto with ppcgen. econstructor; split. @@ -1275,22 +1277,22 @@ Proof. apply agree_exten_2 with rs1. unfold rs1; auto with ppcgen. auto. (* Oandimm *) - generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m + generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m' (ireg_of_not_GPR0 m0)). intros [rs' [A [B [C D]]]]. exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. (* Oorimm *) - generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m). + generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m'). intros [rs' [A [B C]]]. exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. (* Oxorimm *) - generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m). + generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m'). intros [rs' [A [B C]]]. exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. (* Oxhrximm *) pose (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shr (rs (ireg_of m0)) (Vint i)) #CARRY <- (Val.shr_carry (rs (ireg_of m0)) (Vint i)))). exists (nextinstr (rs1#(ireg_of res) <- (Val.shrx (rs (ireg_of m0)) (Vint i)))). - split. apply exec_straight_two with rs1 m. + split. apply exec_straight_two with rs1 m'. auto. simpl. decEq. decEq. decEq. unfold rs1. repeat (rewrite nextinstr_inv; try discriminate). rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. @@ -1312,7 +1314,7 @@ Proof. set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))). set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.xor (rs1#(ireg_of res)) (Vint Int.one)))). exists rs2. - split. apply exec_straight_two with rs1 m; auto. + split. apply exec_straight_two with rs1 m'; auto. rewrite <- Val.rolm_ge_zero in LD. unfold rs2. apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. fold rs1. @@ -1334,19 +1336,19 @@ Proof. (if isset then k else Pxori (ireg_of res) (ireg_of res) (Cint Int.one) :: k)). - generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m H1 H0). + generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m' H1 H0). fold bit; fold isset. intros [rs1 [EX1 [RES1 AG1]]]. set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#(reg_of_crbit bit)))). destruct isset. exists rs2. - split. apply exec_straight_trans with k1 rs1 m. assumption. + split. apply exec_straight_trans with k1 rs1 m'. assumption. unfold k1. apply exec_straight_one. reflexivity. reflexivity. unfold rs2. rewrite RES1. auto with ppcgen. econstructor. - split. apply exec_straight_trans with k1 rs1 m. assumption. - unfold k1. apply exec_straight_two with rs2 m. + split. apply exec_straight_trans with k1 rs1 m'. assumption. + unfold k1. apply exec_straight_two with rs2 m'. reflexivity. simpl. eauto. auto. auto. apply agree_nextinstr. unfold rs2 at 1. rewrite nextinstr_inv. rewrite Pregmap.gss. diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v index ae3c2bdb..a15bf736 100644 --- a/powerpc/Asmgenretaddr.v +++ b/powerpc/Asmgenretaddr.v @@ -179,11 +179,11 @@ Proof. Qed. Lemma return_address_exists: - forall f c, is_tail c f.(fn_code) -> + forall f sg ros c, is_tail (Mcall sg ros :: c) f.(fn_code) -> exists ra, return_address_offset f c ra. Proof. intros. assert (is_tail (transl_code f c) (transl_function f)). - unfold transl_function. IsTail. apply transl_code_tail; auto. + unfold transl_function. IsTail. apply transl_code_tail; eauto with coqlib. destruct (is_tail_code_tail _ _ H0) as [ofs A]. exists (Int.repr ofs). constructor. auto. Qed. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index ac15c0d3..bf065b78 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -88,10 +88,10 @@ Ltac InvVLMA := approximations returned by [eval_static_operation]. *) Lemma eval_static_condition_correct: - forall cond al vl b, + forall cond al vl m b, val_list_match_approx al vl -> eval_static_condition cond al = Some b -> - eval_condition cond vl = Some b. + eval_condition cond vl m = Some b. Proof. intros until b. unfold eval_static_condition. @@ -100,9 +100,9 @@ Proof. Qed. Lemma eval_static_operation_correct: - forall op sp al vl v, + forall op sp al vl m v, val_list_match_approx al vl -> - eval_operation ge sp op vl = Some v -> + eval_operation ge sp op vl m = Some v -> val_match_approx (eval_static_operation op al) v. Proof. intros until v. @@ -150,7 +150,7 @@ Proof. inv H4. destruct (Float.intoffloat f); simpl in H0; inv H0. red; auto. caseEq (eval_static_condition c vl0). - intros. generalize (eval_static_condition_correct _ _ _ _ H H1). + intros. generalize (eval_static_condition_correct _ _ _ m _ H H1). intro. rewrite H2 in H0. destruct b; injection H0; intro; subst v; simpl; auto. intros; simpl; auto. @@ -174,6 +174,7 @@ Section STRENGTH_REDUCTION. Variable app: reg -> approx. Variable sp: val. Variable rs: regset. +Variable m: mem. Hypothesis MATCH: forall r, val_match_approx (app r) rs#r. Lemma intval_correct: @@ -189,20 +190,20 @@ Qed. Lemma cond_strength_reduction_correct: forall cond args, let (cond', args') := cond_strength_reduction app cond args in - eval_condition cond' rs##args' = eval_condition cond rs##args. + eval_condition cond' rs##args' m = eval_condition cond rs##args m. Proof. intros. unfold cond_strength_reduction. case (cond_strength_reduction_match cond args); intros. caseEq (intval app r1); intros. simpl. rewrite (intval_correct _ _ H). destruct (rs#r2); auto. rewrite Int.swap_cmp. auto. - destruct c; reflexivity. caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H0). auto. auto. caseEq (intval app r1); intros. simpl. rewrite (intval_correct _ _ H). destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto. + destruct c; reflexivity. caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H0). auto. auto. @@ -212,8 +213,8 @@ Qed. Lemma make_addimm_correct: forall n r v, let (op, args) := make_addimm n r in - eval_operation ge sp Oadd (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oadd (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_addimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -225,8 +226,8 @@ Qed. Lemma make_shlimm_correct: forall n r v, let (op, args) := make_shlimm n r in - eval_operation ge sp Oshl (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshl (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shlimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -239,8 +240,8 @@ Qed. Lemma make_shrimm_correct: forall n r v, let (op, args) := make_shrimm n r in - eval_operation ge sp Oshr (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshr (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shrimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -251,8 +252,8 @@ Qed. Lemma make_shruimm_correct: forall n r v, let (op, args) := make_shruimm n r in - eval_operation ge sp Oshru (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshru (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shruimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -265,8 +266,8 @@ Qed. Lemma make_mulimm_correct: forall n r v, let (op, args) := make_mulimm n r in - eval_operation ge sp Omul (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Omul (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_mulimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -274,8 +275,8 @@ Proof. generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros. subst n. simpl in H1. simpl. FuncInv. rewrite Int.mul_one in H0. congruence. caseEq (Int.is_power2 n); intros. - replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil)) - with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)). + replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil) m) + with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil) m). apply make_shlimm_correct. simpl. generalize (Int.is_power2_range _ _ H1). change (Z_of_nat Int.wordsize) with 32. intro. rewrite H2. @@ -286,8 +287,8 @@ Qed. Lemma make_andimm_correct: forall n r v, let (op, args) := make_andimm n r in - eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oand (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_andimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -300,8 +301,8 @@ Qed. Lemma make_orimm_correct: forall n r v, let (op, args) := make_orimm n r in - eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oor (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_orimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -314,8 +315,8 @@ Qed. Lemma make_xorimm_correct: forall n r v, let (op, args) := make_xorimm n r in - eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oxor (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_xorimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -326,16 +327,16 @@ Qed. Lemma op_strength_reduction_correct: forall op args v, let (op', args') := op_strength_reduction app op args in - eval_operation ge sp op rs##args = Some v -> - eval_operation ge sp op' rs##args' = Some v. + eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op' rs##args' m = Some v. Proof. intros; unfold op_strength_reduction; case (op_strength_reduction_match op args); intros; simpl List.map. (* Oadd *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil) m). apply make_addimm_correct. simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto. caseEq (intval app r2); intros. @@ -346,16 +347,16 @@ Proof. rewrite (intval_correct _ _ H) in H0. assumption. caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). - replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)). + replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil) m). apply make_addimm_correct. simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. assumption. (* Omul *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil) m). apply make_mulimm_correct. simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto. caseEq (intval app r2); intros. @@ -375,8 +376,8 @@ Proof. caseEq (intval app r2); intros. caseEq (Int.is_power2 i); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)). + replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil) m). apply make_shruimm_correct. simpl. destruct rs#r1; auto. change 32 with (Z_of_nat Int.wordsize). @@ -389,8 +390,8 @@ Proof. (* Oand *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil) m). apply make_andimm_correct. simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto. caseEq (intval app r2); intros. @@ -399,8 +400,8 @@ Proof. (* Oor *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil) m). apply make_orimm_correct. simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto. caseEq (intval app r2); intros. @@ -409,8 +410,8 @@ Proof. (* Oxor *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil) m). apply make_xorimm_correct. simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto. caseEq (intval app r2); intros. diff --git a/powerpc/Op.v b/powerpc/Op.v index 6f05e550..d4669613 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -32,6 +32,7 @@ Require Import Values. Require Import Memdata. Require Import Memory. Require Import Globalenvs. +Require Import Events. Set Implicit Arguments. @@ -141,27 +142,30 @@ Definition eval_compare_mismatch (c: comparison) : option bool := Definition eval_compare_null (c: comparison) (n: int) : option bool := if Int.eq n Int.zero then eval_compare_mismatch c else None. -Definition eval_condition (cond: condition) (vl: list val): +Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with | Ccomp c, Vint n1 :: Vint n2 :: nil => Some (Int.cmp c n1 n2) - | Ccomp c, Vptr b1 n1 :: Vptr b2 n2 :: nil => - if eq_block b1 b2 - then Some (Int.cmp c n1 n2) - else eval_compare_mismatch c - | Ccomp c, Vptr b1 n1 :: Vint n2 :: nil => - eval_compare_null c n2 - | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil => - eval_compare_null c n1 | Ccompu c, Vint n1 :: Vint n2 :: nil => Some (Int.cmpu c n1 n2) + | Ccompu c, Vptr b1 n1 :: Vptr b2 n2 :: nil => + if Mem.valid_pointer m b1 (Int.unsigned n1) + && Mem.valid_pointer m b2 (Int.unsigned n2) then + if eq_block b1 b2 + then Some (Int.cmpu c n1 n2) + else eval_compare_mismatch c + else None + | Ccompu c, Vptr b1 n1 :: Vint n2 :: nil => + eval_compare_null c n2 + | Ccompu c, Vint n1 :: Vptr b2 n2 :: nil => + eval_compare_null c n1 | Ccompimm c n, Vint n1 :: nil => Some (Int.cmp c n1 n) - | Ccompimm c n, Vptr b1 n1 :: nil => - eval_compare_null c n | Ccompuimm c n, Vint n1 :: nil => Some (Int.cmpu c n1 n) + | Ccompuimm c n, Vptr b1 n1 :: nil => + eval_compare_null c n | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil => Some (Float.cmp c f1 f2) | Cnotcompf c, Vfloat f1 :: Vfloat f2 :: nil => @@ -182,7 +186,7 @@ Definition offset_sp (sp: val) (delta: int) : option val := Definition eval_operation (F V: Type) (genv: Genv.t F V) (sp: val) - (op: operation) (vl: list val): option val := + (op: operation) (vl: list val) (m: mem): option val := match op, vl with | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) @@ -251,7 +255,7 @@ Definition eval_operation | Ofloatofwords, Vint i1 :: Vint i2 :: nil => Some (Vfloat (Float.from_words i1 i2)) | Ocmp c, _ => - match eval_condition c vl with + match eval_condition c vl m with | None => None | Some false => Some Vfalse | Some true => Some Vtrue @@ -327,21 +331,23 @@ Proof. Qed. Lemma eval_negate_condition: - forall (cond: condition) (vl: list val) (b: bool), - eval_condition cond vl = Some b -> - eval_condition (negate_condition cond) vl = Some (negb b). + forall cond vl m b, + eval_condition cond vl m = Some b -> + eval_condition (negate_condition cond) vl m = Some (negb b). Proof. intros. destruct cond; simpl in H; FuncInv; try subst b; simpl. rewrite Int.negate_cmp. auto. + rewrite Int.negate_cmpu. auto. apply eval_negate_compare_null; auto. apply eval_negate_compare_null; auto. - destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence. + destruct (Mem.valid_pointer m b0 (Int.unsigned i) && + Mem.valid_pointer m b1 (Int.unsigned i0)); try congruence. + destruct (eq_block b0 b1). rewrite Int.negate_cmpu. congruence. apply eval_negate_compare_mismatch; auto. - rewrite Int.negate_cmpu. auto. rewrite Int.negate_cmp. auto. - apply eval_negate_compare_null; auto. rewrite Int.negate_cmpu. auto. + apply eval_negate_compare_null; auto. auto. rewrite negb_elim. auto. auto. @@ -362,8 +368,8 @@ Hypothesis agree_on_symbols: forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s. Lemma eval_operation_preserved: - forall sp op vl, - eval_operation ge2 sp op vl = eval_operation ge1 sp op vl. + forall sp op vl m, + eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m. Proof. intros. unfold eval_operation; destruct op; try rewrite agree_on_symbols; @@ -483,9 +489,9 @@ Variable A V: Type. Variable genv: Genv.t A V. Lemma type_of_operation_sound: - forall op vl sp v, + forall op vl sp v m, op <> Omove -> - eval_operation genv sp op vl = Some v -> + eval_operation genv sp op vl m = Some v -> Val.has_type v (snd (type_of_operation op)). Proof. intros. @@ -643,14 +649,16 @@ Proof. Qed. Lemma eval_condition_weaken: - forall c vl b, - eval_condition c vl = Some b -> + forall c vl b m, + eval_condition c vl m = Some b -> eval_condition_total c vl = Val.of_bool b. Proof. intros. unfold eval_condition in H; destruct c; FuncInv; try subst b; try reflexivity; simpl; try (apply eval_compare_null_weaken; auto). + destruct (Mem.valid_pointer m b0 (Int.unsigned i) && + Mem.valid_pointer m b1 (Int.unsigned i0)); try congruence. unfold eq_block in H. destruct (zeq b0 b1). congruence. apply eval_compare_mismatch_weaken; auto. @@ -659,8 +667,8 @@ Proof. Qed. Lemma eval_operation_weaken: - forall sp op vl v, - eval_operation genv sp op vl = Some v -> + forall sp op vl v m, + eval_operation genv sp op vl m = Some v -> eval_operation_total sp op vl = v. Proof. intros. @@ -680,7 +688,7 @@ Proof. destruct (Int.ltu i Int.iwordsize); congruence. destruct (Int.ltu i0 Int.iwordsize); congruence. destruct (Float.intoffloat f); inv H. auto. - caseEq (eval_condition c vl); intros; rewrite H0 in H. + caseEq (eval_condition c vl m); intros; rewrite H0 in H. replace v with (Val.of_bool b). eapply eval_condition_weaken; eauto. destruct b; simpl; congruence. @@ -746,12 +754,20 @@ Ltac InvLessdef := end. Lemma eval_condition_lessdef: - forall cond vl1 vl2 b, + forall cond vl1 vl2 b m1 m2, Val.lessdef_list vl1 vl2 -> - eval_condition cond vl1 = Some b -> - eval_condition cond vl2 = Some b. + Mem.extends m1 m2 -> + eval_condition cond vl1 m1 = Some b -> + eval_condition cond vl2 m2 = Some b. Proof. intros. destruct cond; simpl in *; FuncInv; InvLessdef; auto. + destruct (Mem.valid_pointer m1 b0 (Int.unsigned i) && + Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate. + destruct (andb_prop _ _ Heqb2) as [A B]. + assert (forall b ofs, Mem.valid_pointer m1 b ofs = true -> Mem.valid_pointer m2 b ofs = true). + intros until ofs. repeat rewrite Mem.valid_pointer_nonempty_perm. + apply Mem.perm_extends; auto. + rewrite (H _ _ A). rewrite (H _ _ B). auto. Qed. Ltac TrivialExists := @@ -762,33 +778,34 @@ Ltac TrivialExists := end. Lemma eval_operation_lessdef: - forall sp op vl1 vl2 v1, + forall sp op vl1 vl2 v1 m1 m2, Val.lessdef_list vl1 vl2 -> - eval_operation genv sp op vl1 = Some v1 -> - exists v2, eval_operation genv sp op vl2 = Some v2 /\ Val.lessdef v1 v2. + Mem.extends m1 m2 -> + eval_operation genv sp op vl1 m1 = Some v1 -> + exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2. Proof. intros. destruct op; simpl in *; FuncInv; InvLessdef; TrivialExists. exists v2; auto. - destruct (Genv.find_symbol genv i); inv H0. TrivialExists. + destruct (Genv.find_symbol genv i); inv H1. TrivialExists. exists v1; auto. exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto. exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto. exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto. exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto. - destruct (eq_block b b0); inv H0. TrivialExists. - destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. - destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. - destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. - destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. + destruct (eq_block b b0); inv H1. TrivialExists. + destruct (Int.eq i0 Int.zero); inv H1; TrivialExists. + destruct (Int.eq i0 Int.zero); inv H1; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists. + destruct (Int.ltu i Int.iwordsize); inv H1; TrivialExists. + destruct (Int.ltu i Int.iwordsize); inv H1; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists. exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto. - destruct (Float.intoffloat f); simpl in *; inv H0. TrivialExists. - caseEq (eval_condition c vl1); intros. rewrite H1 in H0. - rewrite (eval_condition_lessdef c H H1). - destruct b; inv H0; TrivialExists. - rewrite H1 in H0. discriminate. + destruct (Float.intoffloat f); simpl in *; inv H1. TrivialExists. + caseEq (eval_condition c vl1 m1); intros. rewrite H2 in H1. + rewrite (eval_condition_lessdef c H H0 H2). + destruct b; inv H1; TrivialExists. + rewrite H2 in H1. discriminate. Qed. Lemma eval_addressing_lessdef: @@ -805,6 +822,159 @@ Qed. End EVAL_LESSDEF. +(** Shifting stack-relative references. This is used in [Stacking]. *) + +Definition shift_stack_addressing (delta: int) (addr: addressing) := + match addr with + | Ainstack ofs => Ainstack (Int.add delta ofs) + | _ => addr + end. + +Definition shift_stack_operation (delta: int) (op: operation) := + match op with + | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) + | _ => op + end. + +Lemma type_shift_stack_addressing: + forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr. +Proof. + intros. destruct addr; auto. +Qed. + +Lemma type_shift_stack_operation: + forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. +Proof. + intros. destruct op; auto. +Qed. + +(** Compatibility of the evaluation functions with memory injections. *) + +Section EVAL_INJECT. + +Variable F V: Type. +Variable genv: Genv.t F V. +Variable f: meminj. +Hypothesis globals: meminj_preserves_globals genv f. +Variable sp1: block. +Variable sp2: block. +Variable delta: Z. +Hypothesis sp_inj: f sp1 = Some(sp2, delta). + +Ltac InvInject := + match goal with + | [ H: val_inject _ (Vint _) _ |- _ ] => + inv H; InvInject + | [ H: val_inject _ (Vfloat _) _ |- _ ] => + inv H; InvInject + | [ H: val_inject _ (Vptr _ _) _ |- _ ] => + inv H; InvInject + | [ H: val_list_inject _ nil _ |- _ ] => + inv H; InvInject + | [ H: val_list_inject _ (_ :: _) _ |- _ ] => + inv H; InvInject + | _ => idtac + end. + +Lemma eval_condition_inject: + forall cond vl1 vl2 b m1 m2, + val_list_inject f vl1 vl2 -> + Mem.inject f m1 m2 -> + eval_condition cond vl1 m1 = Some b -> + eval_condition cond vl2 m2 = Some b. +Proof. + intros. destruct cond; simpl in *; FuncInv; InvInject; auto. + destruct (Mem.valid_pointer m1 b0 (Int.unsigned i)) as [] _eqn; try discriminate. + destruct (Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate. + simpl in H1. + exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. + intros V1. rewrite V1. + exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb2. econstructor; eauto. + intros V2. rewrite V2. + simpl. + destruct (eq_block b0 b1); inv H1. + rewrite H3 in H5; inv H5. rewrite dec_eq_true. + decEq. apply Int.translate_cmpu. + eapply Mem.valid_pointer_inject_no_overflow; eauto. + eapply Mem.valid_pointer_inject_no_overflow; eauto. + exploit Mem.different_pointers_inject; eauto. intros P. + destruct (eq_block b3 b4); auto. + destruct P. contradiction. + destruct c; unfold eval_compare_mismatch in *; inv H2. + unfold Int.cmpu. rewrite Int.eq_false; auto. congruence. + unfold Int.cmpu. rewrite Int.eq_false; auto. congruence. +Qed. + +Ltac TrivialExists2 := + match goal with + | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] => + exists v1; split; [auto | econstructor; eauto] + | _ => idtac + end. + +Lemma eval_addressing_inject: + forall addr vl1 vl2 v1, + val_list_inject f vl1 vl2 -> + eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> + exists v2, + eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 + /\ val_inject f v1 v2. +Proof. + intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists2. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + destruct (Genv.find_symbol genv i) as [] _eqn; inv H0. + TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto. + destruct (Genv.find_symbol genv i) as [] _eqn; inv H0. + TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. +Qed. + +Lemma eval_operation_inject: + forall op vl1 vl2 v1 m1 m2, + val_list_inject f vl1 vl2 -> + Mem.inject f m1 m2 -> + eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> + exists v2, + eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 + /\ val_inject f v1 v2. +Proof. + intros. destruct op; simpl in *; FuncInv; InvInject; TrivialExists2. + exists v'; auto. + destruct (Genv.find_symbol genv i) as [] _eqn; inv H1. + TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + exists (Val.sign_ext 8 v'); split; auto. inv H4; simpl; auto. + exists (Val.zero_ext 8 v'); split; auto. inv H4; simpl; auto. + exists (Val.sign_ext 16 v'); split; auto. inv H4; simpl; auto. + exists (Val.zero_ext 16 v'); split; auto. inv H4; simpl; auto. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + rewrite Int.sub_add_l. auto. + destruct (eq_block b b0); inv H1. rewrite H3 in H5; inv H5. rewrite dec_eq_true. + rewrite Int.sub_shifted. TrivialExists2. + destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2. + destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2. + destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2. + destruct (Int.ltu i0 Int.iwordsize); inv H2. TrivialExists2. + destruct (Int.ltu i0 Int.iwordsize); inv H2. TrivialExists2. + destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2. + destruct (Int.ltu i Int.iwordsize); inv H1. TrivialExists2. + destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists2. + destruct (Int.ltu i Int.iwordsize); inv H2. TrivialExists2. + destruct (Int.ltu i Int.iwordsize); inv H2. TrivialExists2. + destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2. + exists (Val.singleoffloat v'); split; auto. inv H4; simpl; auto. + destruct (Float.intoffloat f0); simpl in *; inv H1. TrivialExists2. + destruct (eval_condition c vl1 m1) as [] _eqn; try discriminate. + exploit eval_condition_inject; eauto. intros EQ; rewrite EQ. + destruct b; inv H1; TrivialExists2. +Qed. + +End EVAL_INJECT. + (** Transformation of addressing modes with two operands or more into an equivalent arithmetic operation. This is used in the [Reload] pass when a store instruction cannot be reloaded directly because @@ -816,10 +986,10 @@ End EVAL_LESSDEF. Definition op_for_binary_addressing (addr: addressing) : operation := Oadd. Lemma eval_op_for_binary_addressing: - forall (F V: Type) (ge: Genv.t F V) sp addr args v, + forall (F V: Type) (ge: Genv.t F V) sp addr args v m, (length args >= 2)%nat -> eval_addressing ge sp addr args = Some v -> - eval_operation ge sp (op_for_binary_addressing addr) args = Some v. + eval_operation ge sp (op_for_binary_addressing addr) args m = Some v. Proof. intros. unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; @@ -849,57 +1019,20 @@ Definition is_trivial_op (op: operation) : bool := | _ => false end. -(** Shifting stack-relative references. This is used in [Stacking]. *) -Definition shift_stack_addressing (delta: int) (addr: addressing) := - match addr with - | Ainstack ofs => Ainstack (Int.add delta ofs) - | _ => addr - end. +(** Operations that depend on the memory state. *) -Definition shift_stack_operation (delta: int) (op: operation) := +Definition op_depends_on_memory (op: operation) : bool := match op with - | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) - | _ => op + | Ocmp (Ccompu _) => true + | _ => false end. -Lemma shift_stack_eval_addressing: - forall (F V: Type) (ge: Genv.t F V) sp addr args delta, - eval_addressing ge (Val.sub sp (Vint delta)) (shift_stack_addressing delta addr) args = - eval_addressing ge sp addr args. -Proof. - intros. destruct addr; simpl; auto. - destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. - decEq. decEq. rewrite <- Int.add_assoc. decEq. - rewrite Int.sub_add_opp. rewrite Int.add_assoc. - rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. - rewrite Int.sub_idem. apply Int.add_zero. -Qed. - -Lemma shift_stack_eval_operation: - forall (F V: Type) (ge: Genv.t F V) sp op args delta, - eval_operation ge (Val.sub sp (Vint delta)) (shift_stack_operation delta op) args = - eval_operation ge sp op args. +Lemma op_depends_on_memory_correct: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + op_depends_on_memory op = false -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. - intros. destruct op; simpl; auto. - destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. - decEq. decEq. rewrite <- Int.add_assoc. decEq. - rewrite Int.sub_add_opp. rewrite Int.add_assoc. - rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. - rewrite Int.sub_idem. apply Int.add_zero. + intros until m2. destruct op; simpl; try congruence. + destruct c; simpl; congruence. Qed. - -Lemma type_shift_stack_addressing: - forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr. -Proof. - intros. destruct addr; auto. -Qed. - -Lemma type_shift_stack_operation: - forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. -Proof. - intros. destruct op; auto. -Qed. - - - diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 60741975..c0f9294e 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -433,14 +433,11 @@ let print_instruction oc labels = function fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c | Paddze(r1, r2) -> fprintf oc " addze %a, %a\n" ireg r1 ireg r2 - | Pallocframe(lo, hi, ofs) -> - let lo = camlint_of_coqint lo - and hi = camlint_of_coqint hi + | Pallocframe(sz, ofs) -> + let sz = camlint_of_coqint sz and ofs = camlint_of_coqint ofs in - let sz = Int32.sub hi lo in assert (ofs = 0l); - (* Keep stack 16-aligned *) - let adj = Int32.neg (Int32.logand (Int32.add sz 15l) 0xFFFF_FFF0l) in + let adj = Int32.neg sz in if adj >= -0x8000l then fprintf oc " stwu %a, %ld(%a)\n" ireg GPR1 adj ireg GPR1 else begin @@ -509,8 +506,8 @@ let print_instruction oc labels = function fprintf oc " extsb %a, %a\n" ireg r1 ireg r2 | Pextsh(r1, r2) -> fprintf oc " extsh %a, %a\n" ireg r1 ireg r2 - | Pfreeframe(lo, hi, ofs) -> - (* Note: could also do an add on GPR1 using lo and hi *) + | Pfreeframe(sz, ofs) -> + (* Note: could also do an add on GPR1 using sz *) fprintf oc " lwz %a, %ld(%a)\n" ireg GPR1 (camlint_of_coqint ofs) ireg GPR1 | Pfabs(r1, r2) -> fprintf oc " fabs %a, %a\n" freg r1 freg r2 diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v index c421cdc5..b735fad0 100644 --- a/powerpc/SelectOp.v +++ b/powerpc/SelectOp.v @@ -146,7 +146,7 @@ Definition notint (e: expr) := (** ** Boolean negation *) Definition notbool_base (e: expr) := - Eop (Ocmp (Ccompimm Ceq Int.zero)) (e ::: Enil). + Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil). Fixpoint notbool (e: expr) {struct e} : expr := match e with diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 1f2c7362..6d1e3c5c 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -64,13 +64,13 @@ Ltac InvEval1 := Ltac InvEval2 := match goal with - | [ H: (eval_operation _ _ _ nil = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] => simpl in H; inv H - | [ H: (eval_operation _ _ _ (_ :: nil) = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] => simpl in H; FuncInv - | [ H: (eval_operation _ _ _ (_ :: _ :: nil) = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] => simpl in H; FuncInv - | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] => simpl in H; FuncInv | _ => idtac @@ -167,12 +167,12 @@ Proof. eapply eval_notbool_base; eauto. inv H. eapply eval_Eop; eauto. - simpl. assert (eval_condition c vl = Some b). + simpl. assert (eval_condition c vl m = Some b). generalize H6. simpl. - case (eval_condition c vl); intros. + case (eval_condition c vl m); intros. destruct b0; inv H1; inversion H0; auto; congruence. congruence. - rewrite (Op.eval_negate_condition _ _ H). + rewrite (Op.eval_negate_condition _ _ _ H). destruct b; reflexivity. inv H. eapply eval_Econdition; eauto. @@ -542,9 +542,9 @@ Qed. Lemma eval_mod_aux: forall divop semdivop, - (forall sp x y, + (forall sp x y m, y <> Int.zero -> - eval_operation ge sp divop (Vint x :: Vint y :: nil) = + eval_operation ge sp divop (Vint x :: Vint y :: nil) m = Some (Vint (semdivop x y))) -> forall le a b x y, eval_expr ge sp e m le a (Vint x) -> @@ -715,7 +715,7 @@ Theorem eval_singleoffloat: eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v). Proof. TrivialOp singleoffloat. Qed. -Theorem eval_comp_int: +Theorem eval_comp: forall le c a x b y, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vint y) -> @@ -728,6 +728,19 @@ Proof. EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. Qed. +Theorem eval_compu_int: + forall le c a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)). +Proof. + intros until y. + unfold compu; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. +Qed. + Remark eval_compare_null_transf: forall c x v, Cminor.eval_compare_null c x = Some v -> @@ -742,15 +755,15 @@ Proof. destruct c; try discriminate; auto. Qed. -Theorem eval_comp_ptr_int: +Theorem eval_compu_ptr_int: forall le c a x1 x2 b y v, eval_expr ge sp e m le a (Vptr x1 x2) -> eval_expr ge sp e m le b (Vint y) -> Cminor.eval_compare_null c y = Some v -> - eval_expr ge sp e m le (comp c a b) v. + eval_expr ge sp e m le (compu c a b) v. Proof. intros until v. - unfold comp; case (comp_match a b); intros; InvEval. + unfold compu; case (comp_match a b); intros; InvEval. EvalOp. simpl. apply eval_compare_null_transf; auto. EvalOp. simpl. apply eval_compare_null_transf; auto. Qed. @@ -764,58 +777,49 @@ Proof. destruct (Int.eq x Int.zero). destruct c; auto. auto. Qed. -Theorem eval_comp_int_ptr: +Theorem eval_compu_int_ptr: forall le c a x b y1 y2 v, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vptr y1 y2) -> Cminor.eval_compare_null c x = Some v -> - eval_expr ge sp e m le (comp c a b) v. + eval_expr ge sp e m le (compu c a b) v. Proof. intros until v. - unfold comp; case (comp_match a b); intros; InvEval. + unfold compu; case (comp_match a b); intros; InvEval. EvalOp. simpl. apply eval_compare_null_transf. rewrite eval_compare_null_swap; auto. EvalOp. simpl. apply eval_compare_null_transf. auto. Qed. -Theorem eval_comp_ptr_ptr: +Theorem eval_compu_ptr_ptr: forall le c a x1 x2 b y1 y2, eval_expr ge sp e m le a (Vptr x1 x2) -> eval_expr ge sp e m le b (Vptr y1 y2) -> + Mem.valid_pointer m x1 (Int.unsigned x2) + && Mem.valid_pointer m y1 (Int.unsigned y2) = true -> x1 = y1 -> - eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)). + eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x2 y2)). Proof. intros until y2. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. subst y1. rewrite dec_eq_true. - destruct (Int.cmp c x2 y2); reflexivity. + unfold compu; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. + destruct (Int.cmpu c x2 y2); reflexivity. Qed. -Theorem eval_comp_ptr_ptr_2: +Theorem eval_compu_ptr_ptr_2: forall le c a x1 x2 b y1 y2 v, eval_expr ge sp e m le a (Vptr x1 x2) -> eval_expr ge sp e m le b (Vptr y1 y2) -> + Mem.valid_pointer m x1 (Int.unsigned x2) + && Mem.valid_pointer m y1 (Int.unsigned y2) = true -> x1 <> y1 -> Cminor.eval_compare_mismatch c = Some v -> - eval_expr ge sp e m le (comp c a b) v. + eval_expr ge sp e m le (compu c a b) v. Proof. intros until y2. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite dec_eq_false; auto. - destruct c; simpl in H2; inv H2; auto. -Qed. - -Theorem eval_compu: - forall le c a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)). -Proof. - intros until y. unfold compu; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto. + destruct c; simpl in H3; inv H3; auto. Qed. Theorem eval_compf: diff --git a/powerpc/eabi/Stacklayout.v b/powerpc/eabi/Stacklayout.v index 0de1ccd6..22a28269 100644 --- a/powerpc/eabi/Stacklayout.v +++ b/powerpc/eabi/Stacklayout.v @@ -33,12 +33,6 @@ Require Import Bounds. - Saved values of float callee-save registers used by the function. - Space for the stack-allocated data declared in Cminor. -To facilitate some of the proofs, the Cminor stack-allocated data -starts at offset 0; the preceding areas in the activation record -therefore have negative offsets. This part (with negative offsets) -is called the ``frame'', by opposition with the ``Cminor stack data'' -which is the part with positive offsets. - The [frame_env] compilation environment records the positions of the boundaries between areas in the frame part. *) @@ -54,7 +48,8 @@ Record frame_env : Type := mk_frame_env { fe_num_int_callee_save: Z; fe_ofs_float_local: Z; fe_ofs_float_callee_save: Z; - fe_num_float_callee_save: Z + fe_num_float_callee_save: Z; + fe_stack_data: Z }. (** Computation of the frame environment from the bounds of the current @@ -67,17 +62,81 @@ Definition make_env (b: bounds) := let oendi := oics + 4 * b.(bound_int_callee_save) in let ofl := align oendi 8 in (* float locals *) let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *) - let sz := ofcs + 8 * b.(bound_float_callee_save) in (* total frame size *) + let ostkdata := ofcs + 8 * b.(bound_float_callee_save) in (* stack data *) + let sz := align (ostkdata + b.(bound_stack_data)) 16 in mk_frame_env sz 0 ora oil oics b.(bound_int_callee_save) - ofl ofcs b.(bound_float_callee_save). + ofl ofcs b.(bound_float_callee_save) + ostkdata. +(** Separation property *) -Remark align_float_part: +Remark frame_env_separated: forall b, - 8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 + 4 * bound_int_callee_save b <= - align (8 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 + 4 * bound_int_callee_save b) 8. + let fe := make_env b in + 0 <= fe.(fe_ofs_link) + /\ fe.(fe_ofs_link) + 4 <= fe_ofs_arg + /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_int_local) + /\ fe.(fe_ofs_int_local) + 4 * b.(bound_int_local) <= fe.(fe_ofs_retaddr) + /\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_ofs_int_callee_save) + /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_local) + /\ fe.(fe_ofs_float_local) + 8 * b.(bound_float_local) <= fe.(fe_ofs_float_callee_save) + /\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_stack_data) + /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size). Proof. - intros. apply align_le. omega. + intros. + generalize (align_le (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)). + generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 16 (refl_equal _)). + unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, + fe_ofs_int_local, fe_ofs_int_callee_save, + fe_num_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save, + fe_stack_data, fe_ofs_arg. + intros. + generalize (bound_int_local_pos b); intro; + generalize (bound_float_local_pos b); intro; + generalize (bound_int_callee_save_pos b); intro; + generalize (bound_float_callee_save_pos b); intro; + generalize (bound_outgoing_pos b); intro; + generalize (bound_stack_data_pos b); intro. + omega. Qed. +(** Alignment property *) + +Remark frame_env_aligned: + forall b, + let fe := make_env b in + (4 | fe.(fe_ofs_link)) + /\ (4 | fe.(fe_ofs_int_local)) + /\ (4 | fe.(fe_ofs_int_callee_save)) + /\ (8 | fe.(fe_ofs_float_local)) + /\ (8 | fe.(fe_ofs_float_callee_save)) + /\ (4 | fe.(fe_ofs_retaddr)) + /\ (4 | fe.(fe_stack_data)) + /\ (16 | fe.(fe_size)). +Proof. + intros. + unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, + fe_ofs_int_local, fe_ofs_int_callee_save, + fe_num_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save, + fe_stack_data. + set (x1 := 8 + 4 * bound_outgoing b). + assert (4 | x1). unfold x1; apply Zdivide_plus_r. exists 2; auto. exists (bound_outgoing b); ring. + set (x2 := x1 + 4 * bound_int_local b). + assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists (bound_int_local b); ring. + set (x3 := x2 + 4). + assert (4 | x3). unfold x3; apply Zdivide_plus_r; auto. exists 1; auto. + set (x4 := align (x3 + 4 * bound_int_callee_save b) 8). + assert (8 | x4). unfold x4. apply align_divides. omega. + set (x5 := x4 + 8 * bound_float_local b). + assert (8 | x5). unfold x5. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring. + set (x6 := x5 + 8 * bound_float_callee_save b). + assert (4 | x6). + apply Zdivides_trans with 8. exists 2; auto. + unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. + set (x7 := align (x6 + bound_stack_data b) 16). + assert (16 | x7). unfold x7; apply align_divides. omega. + intuition. +Qed. diff --git a/powerpc/macosx/Stacklayout.v b/powerpc/macosx/Stacklayout.v index c57f3f92..57592a8c 100644 --- a/powerpc/macosx/Stacklayout.v +++ b/powerpc/macosx/Stacklayout.v @@ -30,12 +30,6 @@ Require Import Bounds. - Saved values of float callee-save registers used by the function. - Space for the stack-allocated data declared in Cminor. -To facilitate some of the proofs, the Cminor stack-allocated data -starts at offset 0; the preceding areas in the activation record -therefore have negative offsets. This part (with negative offsets) -is called the ``frame'', by opposition with the ``Cminor stack data'' -which is the part with positive offsets. - The [frame_env] compilation environment records the positions of the boundaries between areas in the frame part. *) @@ -51,7 +45,8 @@ Record frame_env : Type := mk_frame_env { fe_num_int_callee_save: Z; fe_ofs_float_local: Z; fe_ofs_float_callee_save: Z; - fe_num_float_callee_save: Z + fe_num_float_callee_save: Z; + fe_stack_data: Z }. (** Computation of the frame environment from the bounds of the current @@ -63,17 +58,81 @@ Definition make_env (b: bounds) := let oendi := oics + 4 * b.(bound_int_callee_save) in let ofl := align oendi 8 in (* float locals *) let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *) - let sz := ofcs + 8 * b.(bound_float_callee_save) in (* total frame size *) + let ostkdata := ofcs + 8 * b.(bound_float_callee_save) in (* stack data *) + let sz := align (ostkdata + b.(bound_stack_data)) 16 in mk_frame_env sz 0 12 oil oics b.(bound_int_callee_save) - ofl ofcs b.(bound_float_callee_save). + ofl ofcs b.(bound_float_callee_save) + ostkdata. +(** Separation property *) -Remark align_float_part: +Remark frame_env_separated: forall b, - 24 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b <= - align (24 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8. + let fe := make_env b in + 0 <= fe.(fe_ofs_link) + /\ fe.(fe_ofs_link) + 4 <= fe.(fe_ofs_retaddr) + /\ fe.(fe_ofs_retaddr) + 4 <= fe_ofs_arg + /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_int_local) + /\ fe.(fe_ofs_int_local) + 4 * b.(bound_int_local) <= fe.(fe_ofs_int_callee_save) + /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_local) + /\ fe.(fe_ofs_float_local) + 8 * b.(bound_float_local) <= fe.(fe_ofs_float_callee_save) + /\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_stack_data) + /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size). Proof. - intros. apply align_le. omega. + intros. + generalize (align_le (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)). + generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 16 (refl_equal _)). + unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, + fe_ofs_int_local, fe_ofs_int_callee_save, + fe_num_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save, + fe_stack_data, fe_ofs_arg. + intros. + generalize (bound_int_local_pos b); intro; + generalize (bound_float_local_pos b); intro; + generalize (bound_int_callee_save_pos b); intro; + generalize (bound_float_callee_save_pos b); intro; + generalize (bound_outgoing_pos b); intro; + generalize (bound_stack_data_pos b); intro. + omega. Qed. +(** Alignment property *) + +Remark frame_env_aligned: + forall b, + let fe := make_env b in + (4 | fe.(fe_ofs_link)) + /\ (4 | fe.(fe_ofs_int_local)) + /\ (4 | fe.(fe_ofs_int_callee_save)) + /\ (8 | fe.(fe_ofs_float_local)) + /\ (8 | fe.(fe_ofs_float_callee_save)) + /\ (4 | fe.(fe_ofs_retaddr)) + /\ (4 | fe.(fe_stack_data)) + /\ (16 | fe.(fe_size)). +Proof. + intros. + unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, + fe_ofs_int_local, fe_ofs_int_callee_save, + fe_num_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save, + fe_stack_data. + set (x1 := 24 + 4 * bound_outgoing b). + assert (4 | x1). unfold x1; apply Zdivide_plus_r. exists 6; auto. exists (bound_outgoing b); ring. + set (x2 := x1 + 4 * bound_int_local b). + assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists (bound_int_local b); ring. + set (x3 := x2 + 4 * bound_int_callee_save b). + set (x4 := align x3 8). + assert (8 | x4). unfold x4. apply align_divides. omega. + set (x5 := x4 + 8 * bound_float_local b). + assert (8 | x5). unfold x5. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring. + set (x6 := x5 + 8 * bound_float_callee_save b). + assert (4 | x6). + apply Zdivides_trans with 8. exists 2; auto. + unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. + set (x7 := align (x6 + bound_stack_data b) 16). + assert (16 | x7). unfold x7; apply align_divides. omega. + intuition. + exists 3; auto. +Qed. -- cgit