diff options
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/Asm.v | 18 | ||||
| -rw-r--r-- | ia32/Asmgen.v | 43 | ||||
| -rw-r--r-- | ia32/Asmgenproof.v | 176 | ||||
| -rw-r--r-- | ia32/Asmgenproof1.v | 105 | ||||
| -rw-r--r-- | ia32/Asmgenretaddr.v | 40 | ||||
| -rw-r--r-- | ia32/ConstpropOpproof.v | 55 | ||||
| -rw-r--r-- | ia32/Op.v | 330 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 20 | ||||
| -rw-r--r-- | ia32/SelectOp.v | 2 | ||||
| -rw-r--r-- | ia32/SelectOpproof.v | 74 | ||||
| -rw-r--r-- | ia32/standard/Conventions1.v | 2 | ||||
| -rw-r--r-- | ia32/standard/Stacklayout.v | 102 |
12 files changed, 626 insertions, 341 deletions
@@ -184,8 +184,8 @@ Inductive instruction: Type := | Pret (** Pseudo-instructions *) | Plabel(l: label) - | Pallocframe(lo hi: Z)(ofs_ra ofs_link: int) - | Pfreeframe(lo hi: Z)(ofs_ra ofs_link: int) + | Pallocframe(sz: Z)(ofs_ra ofs_link: int) + | Pfreeframe(sz: Z)(ofs_ra ofs_link: int) | Pbuiltin(ef: external_function)(args: list preg)(res: preg). Definition code := list instruction. @@ -601,7 +601,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pjmptbl r tbl => match rs#r with | Vint n => - match list_nth_z tbl (Int.signed n) with + match list_nth_z tbl (Int.unsigned n) with | None => Stuck | Some lbl => goto_label c lbl (rs #ECX <- Vundef #EDX <- Vundef) m end @@ -616,18 +616,18 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome (** Pseudo-instructions *) | Plabel lbl => Next (nextinstr rs) m - | Pallocframe lo hi ofs_ra ofs_link => - let (m1, stk) := Mem.alloc m lo hi in - let sp := Vptr stk (Int.repr lo) in + | Pallocframe sz ofs_ra ofs_link => + 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_link)) rs#ESP with | None => Stuck | Some m2 => match Mem.storev Mint32 m2 (Val.add sp (Vint ofs_ra)) rs#RA with | None => Stuck - | Some m3 => Next (nextinstr (rs#ESP <- sp)) m3 + | Some m3 => Next (nextinstr (rs #EDX <- (rs#ESP) #ESP <- sp)) m3 end end - | Pfreeframe lo hi ofs_ra ofs_link => + | Pfreeframe sz ofs_ra ofs_link => match Mem.loadv Mint32 m (Val.add rs#ESP (Vint ofs_ra)) with | None => Stuck | Some ra => @@ -636,7 +636,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Some sp => match rs#ESP with | Vptr stk ofs => - match Mem.free m stk lo hi with + match Mem.free m stk 0 sz with | None => Stuck | Some m' => Next (nextinstr (rs#ESP <- sp #RA <- ra)) m' end diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index f53ec81..0e14dee 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -215,10 +215,10 @@ Definition transl_cond | Ccompu c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmp_rr r1 r2 :: k) | Ccompimm c n, a1 :: nil => - do r1 <- ireg_of a1; OK (Pcmp_ri r1 n :: k) - | Ccompuimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if Int.eq_dec n Int.zero then Ptest_rr r1 r1 :: k else Pcmp_ri r1 n :: k) + | Ccompuimm c n, a1 :: nil => + do r1 <- ireg_of a1; OK (Pcmp_ri r1 n :: k) | Ccompf cmp, a1 :: a2 :: nil => do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k) | Cnotcompf cmp, a1 :: a2 :: nil => @@ -443,15 +443,19 @@ Definition transl_store (chunk: memory_chunk) (** 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) + (edx_is_parent: bool) (k: code) := match i with | Mgetstack ofs ty dst => loadind ESP ofs ty dst k | Msetstack src ofs ty => storeind src ESP ofs ty k | Mgetparam ofs ty dst => - do k1 <- loadind EDX ofs ty dst k; - loadind ESP f.(fn_link_ofs) Tint IT1 k1 + if edx_is_parent then + loadind EDX ofs ty dst k + else + (do k1 <- loadind EDX ofs ty dst k; + loadind ESP f.(fn_link_ofs) Tint IT1 k1) | Mop op args res => transl_op op args res k | Mload chunk addr args dst => @@ -464,12 +468,10 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := OK (Pcall_s symb :: k) | Mtailcall sig (inl reg) => do r <- ireg_of reg; - OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) - f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: Pjmp_r r :: k) | Mtailcall sig (inr symb) => - OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) - f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: Pjmp_s symb :: k) | Mlabel lbl => OK(Plabel lbl :: k) @@ -480,17 +482,27 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := | Mjumptable arg tbl => do r <- ireg_of arg; OK (Pjmptbl r tbl :: k) | Mreturn => - OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) - f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: Pret :: k) | Mbuiltin ef args res => OK (Pbuiltin ef (List.map preg_of args) (preg_of res) :: k) end. -Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) := +(** Translation of a code sequence *) + +Definition edx_preserved (before: bool) (i: Mach.instruction) : bool := + match i with + | Msetstack src ofs ty => before + | Mgetparam ofs ty dst => negb (mreg_eq dst IT1) + | _ => false + end. + +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (edx_is_parent: bool) := match il with | nil => OK nil - | i1 :: il' => do k <- transl_code f il'; transl_instr f i1 k + | i1 :: il' => + do k <- transl_code f il' (edx_preserved edx_is_parent i1); + transl_instr f i1 edx_is_parent k end. (** Translation of a whole function. Note that we must check @@ -499,10 +511,9 @@ Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) := around, leading to incorrect executions. *) Definition transf_function (f: Mach.function) : res Asm.code := - do c <- transl_code f f.(fn_code); + do c <- transl_code f f.(fn_code) true; if zlt (list_length_z c) Int.max_unsigned - then OK (Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) - f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c) + then OK (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c) else Error (msg "code size exceeded"). Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 543028f..f596f66 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Correctness proof for PPC generation: main proof. *) +(** Correctness proof for x86 generation: main proof. *) Require Import Coqlib. Require Import Maps. @@ -150,15 +150,15 @@ Qed. 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 -> +Inductive transl_code_at_pc: val -> block -> Mach.function -> Mach.code -> bool -> Asm.code -> Asm.code -> Prop := transl_code_at_pc_intro: - forall b ofs f c tf tc, + forall b ofs f c ep tf tc, Genv.find_funct_ptr ge b = Some (Internal f) -> transf_function f = OK tf -> - transl_code f c = OK tc -> + transl_code f c ep = OK tc -> code_tail (Int.unsigned ofs) tf tc -> - transl_code_at_pc (Vptr b ofs) b f c tf tc. + transl_code_at_pc (Vptr b ofs) b f c ep tf tc. (** The following lemmas show that straight-line executions (predicate [exec_straight]) correspond to correct PPC executions @@ -210,8 +210,8 @@ Proof. Qed. Lemma exec_straight_exec: - forall fb f c tf tc c' rs m rs' m', - transl_code_at_pc (rs PC) fb f c tf tc -> + forall fb f c ep tf tc c' rs m rs' m', + transl_code_at_pc (rs PC) fb 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. @@ -222,11 +222,11 @@ Proof. Qed. Lemma exec_straight_at: - forall fb f c tf tc c' tc' rs m rs' m', - transl_code_at_pc (rs PC) fb f c tf tc -> - transl_code f c' = OK tc' -> + forall fb f c ep tf tc c' ep' tc' rs m rs' m', + transl_code_at_pc (rs PC) fb 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 (rs' PC) fb f c' tf tc'. + transl_code_at_pc (rs' PC) fb f c' ep' tf tc'. Proof. intros. inv H. exploit exec_straight_steps_2; eauto. @@ -257,12 +257,12 @@ Qed. Lemma return_address_offset_correct: forall b ofs fb f c tf tc ofs', - transl_code_at_pc (Vptr b ofs) fb f c tf tc -> + transl_code_at_pc (Vptr b ofs) fb f c false tf tc -> return_address_offset f c ofs' -> ofs' = ofs. Proof. intros. inv H0. inv H. - exploit code_tail_unique. eexact H11. eapply H1; eauto. intro. + exploit code_tail_unique. eexact H12. eapply H1; eauto. intro. subst ofs0. apply Int.repr_unsigned. Qed. @@ -461,8 +461,8 @@ Proof. Qed. Lemma transl_instr_label: - forall f i k c, - transl_instr f i k = OK c -> + 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). @@ -472,7 +472,7 @@ Opaque loadind. destruct i; simpl in H. eapply loadind_label; eauto. eapply storeind_label; eauto. - monadInv H. eapply trans_eq; eapply loadind_label; eauto. + destruct ep. eapply loadind_label; eauto. monadInv H. eapply trans_eq; eapply loadind_label; eauto. eapply transl_op_label; eauto. eapply transl_load_label; eauto. eapply transl_store_label; eauto. @@ -487,17 +487,20 @@ Opaque loadind. Qed. Lemma transl_code_label: - forall f c tc, - transl_code f c = OK tc -> + 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' = OK tc' + | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc' end. Proof. induction c; simpl; intros. inv H. auto. - monadInv H. rewrite (transl_instr_label _ _ _ _ EQ0). - destruct (Mach.is_label lbl a). exists x; auto. apply IHc. 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: @@ -505,11 +508,11 @@ Lemma transl_find_label: transf_function f = OK tf -> match Mach.find_label lbl f.(fn_code) with | None => find_label lbl tf = None - | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c = OK tc + | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc end. Proof. intros. monadInv H. destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0. - simpl. apply transl_code_label; auto. + simpl. eapply transl_code_label; eauto. Qed. End TRANSL_LABEL. @@ -525,7 +528,7 @@ Lemma find_label_goto_label: Mach.find_label lbl f.(fn_code) = Some c' -> exists tc', exists rs', goto_label tf lbl rs m = Next rs' m - /\ transl_code_at_pc (rs' PC) b f c' tf tc' + /\ transl_code_at_pc (rs' PC) b f c' false tf tc' /\ forall r, r <> PC -> rs'#r = rs#r. Proof. intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. @@ -564,19 +567,20 @@ Inductive match_stack: list Machconcr.stackframe -> Prop := match_stack nil | match_stack_cons: forall fb sp ra c s f tf tc, Genv.find_funct_ptr ge fb = Some (Internal f) -> - transl_code_at_pc ra fb f c tf tc -> + transl_code_at_pc ra fb f c false tf tc -> sp <> Vundef -> ra <> Vundef -> match_stack s -> match_stack (Stackframe fb sp ra c :: s). Inductive match_states: Machconcr.state -> Asm.state -> Prop := | match_states_intro: - forall s fb sp c ms m m' rs f tf tc + forall s fb sp c ep ms m m' rs f tf tc (STACKS: match_stack s) (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) (MEXT: Mem.extends m m') - (AT: transl_code_at_pc (rs PC) fb f c tf tc) - (AG: agree ms sp rs), + (AT: transl_code_at_pc (rs PC) fb f c ep tf tc) + (AG: agree ms sp rs) + (DXP: ep = true -> rs#EDX = parent_sp s), match_states (Machconcr.State s fb sp c ms m) (Asm.State rs m') | match_states_call: @@ -598,19 +602,22 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop := (Asm.State rs m'). Lemma exec_straight_steps: - forall s fb f rs1 i c tf tc m1' m2 m2' sp ms2, + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2, match_stack s -> Mem.extends m2 m2' -> Genv.find_funct_ptr ge fb = Some (Internal f) -> - transl_code_at_pc (rs1 PC) fb f (i :: c) tf tc -> - (forall k c, transl_instr f i k = OK c -> - exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' /\ agree ms2 sp rs2) -> + transl_code_at_pc (rs1 PC) fb f (i :: c) ep tf tc -> + (forall k c, transl_instr f i ep k = OK c -> + exists rs2, + exec_straight tge tf c rs1 m1' k rs2 m2' + /\ agree ms2 sp rs2 + /\ (edx_preserved ep i = true -> rs2#EDX = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ match_states (Machconcr.State s fb sp c ms2 m2) st'. Proof. intros. inversion H2. subst. monadInv H7. - exploit H3; eauto. intros [rs2 [A B]]. + exploit H3; eauto. intros [rs2 [A [B C]]]. exists (State rs2 m2'); split. eapply exec_straight_exec; eauto. econstructor; eauto. eapply exec_straight_at; eauto. @@ -671,7 +678,7 @@ Proof. intros; red; intros; inv MS. left; eapply exec_straight_steps; eauto; intros. monadInv H. econstructor; split. apply exec_straight_one. simpl; eauto. auto. - apply agree_nextinstr; auto. + split. apply agree_nextinstr; auto. simpl; congruence. Qed. Lemma exec_Mgetstack_prop: @@ -688,7 +695,9 @@ Proof. rewrite (sp_val _ _ _ AG) in A. left; eapply exec_straight_steps; eauto. intros. simpl in H0. exploit loadind_correct; eauto. intros [rs' [P [Q R]]]. - exists rs'; split. eauto. eapply agree_set_mreg; eauto. congruence. + exists rs'; split. eauto. + split. eapply agree_set_mreg; eauto. congruence. + simpl; congruence. Qed. Lemma exec_Msetstack_prop: @@ -706,16 +715,18 @@ Proof. rewrite (sp_val _ _ _ AG) in A. left; eapply exec_straight_steps; eauto. intros. simpl in H1. exploit storeind_correct; eauto. intros [rs' [P Q]]. - exists rs'; split. eauto. eapply agree_exten; eauto. + exists rs'; split. eauto. + split. eapply agree_exten; eauto. + simpl; intros. rewrite Q; auto with ppcgen. 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. @@ -724,38 +735,55 @@ Proof. unfold load_stack in *. exploit Mem.loadv_extends. eauto. eexact H0. auto. intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. - assert (parent' = parent). inv B. auto. simpl in H1. congruence. + assert (parent' = parent_sp s). inv B. auto. rewrite <- H3 in H1. simpl in H1. congruence. subst parent'. exploit Mem.loadv_extends. eauto. eexact H1. auto. intros [v' [C D]]. Opaque loadind. - left; eapply exec_straight_steps; eauto; intros. monadInv H2. + left; eapply exec_straight_steps; eauto; intros. + assert (DIFF: negb (mreg_eq dst IT1) = true -> IR EDX <> preg_of dst). + intros. change (IR EDX) with (preg_of IT1). red; intros. + exploit preg_of_injective; eauto. intros. subst dst. + unfold proj_sumbool in H3. rewrite dec_eq_true in H3. simpl in H3. congruence. + destruct ep; simpl in H2. +(* EDX contains parent *) + exploit loadind_correct. eexact H2. + instantiate (2 := rs). rewrite DXP; eauto. + intros [rs1 [P [Q R]]]. + exists rs1; split. eauto. + split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto. + simpl; intros. rewrite R; auto. +(* EDX does not contain parent *) + monadInv H2. exploit loadind_correct. eexact EQ0. eauto. intros [rs1 [P [Q R]]]. simpl in Q. exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. intros [rs2 [S [T U]]]. exists rs2; split. eapply exec_straight_trans; eauto. - eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto. + split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto. + simpl; intros. rewrite U; auto. 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 = 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. intros; red; intros; inv MS. - assert (eval_operation tge sp op ms##args = Some v). + assert (eval_operation tge sp op ms##args m = Some v). rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. - exploit eval_operation_lessdef. eapply preg_vals; eauto. eexact H0. + 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 H1. exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. exists rs2; split. eauto. - rewrite <- Q in B. + split. rewrite <- Q in B. unfold undef_op. - destruct op; try (eapply agree_set_undef_mreg; eauto). eapply agree_set_mreg; eauto. + destruct op; try (eapply agree_set_undef_mreg; eauto). + eapply agree_set_mreg; eauto. + simpl; congruence. Qed. Lemma exec_Mload_prop: @@ -776,7 +804,9 @@ Proof. exploit Mem.loadv_extends; eauto. intros [v' [C D]]. left; eapply exec_straight_steps; eauto; intros. simpl in H2. exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. - exists rs2; split. eauto. eapply agree_set_undef_mreg; eauto. congruence. + exists rs2; split. eauto. + split. eapply agree_set_undef_mreg; eauto. congruence. + simpl; congruence. Qed. Lemma exec_Mstore_prop: @@ -798,7 +828,9 @@ Proof. exploit Mem.storev_extends; eauto. intros [m2' [C D]]. left; eapply exec_straight_steps; eauto; intros. simpl in H3. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. - exists rs2; split. eauto. eapply agree_exten_temps; eauto. + exists rs2; split. eauto. + split. eapply agree_exten_temps; eauto. + simpl; congruence. Qed. Lemma exec_Mcall_prop: @@ -824,7 +856,7 @@ Proof. generalize (Int.eq_spec i Int.zero); destruct (Int.eq i Int.zero); congruence. clear H. generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. - assert (TCA: transl_code_at_pc (Vptr fb (Int.add ofs Int.one)) fb f c tf x). + assert (TCA: transl_code_at_pc (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). econstructor; eauto. exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. @@ -838,7 +870,7 @@ Proof. rewrite <- H2. auto. (* Direct call *) generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. - assert (TCA: transl_code_at_pc (Vptr fb (Int.add ofs Int.one)) fb f c tf x). + assert (TCA: transl_code_at_pc (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). econstructor; eauto. exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. @@ -868,7 +900,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'). @@ -942,6 +974,7 @@ Proof. simpl; eauto. econstructor; eauto. eapply agree_exten; eauto with ppcgen. + congruence. Qed. Lemma exec_Mbuiltin_prop: @@ -968,11 +1001,12 @@ Proof. instantiate (2 := tf); instantiate (1 := x). unfold nextinstr_nf, nextinstr. rewrite Pregmap.gss. simpl undef_regs. repeat rewrite Pregmap.gso; auto with ppcgen. - rewrite <- H0. simpl. constructor; auto. + rewrite <- H0. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. apply agree_nextinstr_nf. eapply agree_set_undef_mreg; eauto. rewrite Pregmap.gss. auto. - intros. repeat rewrite Pregmap.gso; auto with ppcgen. + intros. repeat rewrite Pregmap.gso; auto with ppcgen. + congruence. Qed. Lemma exec_Mcond_true_prop: @@ -980,14 +1014,14 @@ 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 (Machconcr.State s fb sp c' (undef_temps ms) m). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros EC. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. inv AT. monadInv H5. exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. generalize (functions_transl _ _ _ FIND H4); intro FN. @@ -1003,24 +1037,26 @@ Proof. eapply find_instr_tail. eauto. simpl. rewrite B. eauto. traceEq. econstructor; eauto. eapply agree_exten_temps; eauto. intros. rewrite INV3; auto with ppcgen. + congruence. 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 = 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. - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros EC. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. left; eapply exec_straight_steps; eauto. intros. simpl in H0. exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl. rewrite B. eauto. auto. - apply agree_nextinstr. eapply agree_exten_temps; eauto. + split. apply agree_nextinstr. eapply agree_exten_temps; eauto. + simpl; congruence. Qed. Lemma exec_Mjumptable_prop: @@ -1029,7 +1065,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 @@ -1052,6 +1088,7 @@ Proof. econstructor; eauto. eapply agree_exten_temps; eauto. intros. rewrite C; auto with ppcgen. repeat rewrite Pregmap.gso; auto with ppcgen. + congruence. Qed. Lemma exec_Mreturn_prop: @@ -1060,7 +1097,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. @@ -1094,12 +1131,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. exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. @@ -1118,11 +1155,17 @@ Proof. simpl. rewrite C. simpl in E. rewrite (sp_val _ _ _ AG) in E. rewrite E. rewrite ATLR. simpl in P. rewrite P. eauto. econstructor; eauto. - unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with ppcgen. + unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with ppcgen. rewrite ATPC. simpl. constructor; eauto. subst x. eapply code_tail_next_int. rewrite list_length_z_cons. omega. constructor. - apply agree_nextinstr. eapply agree_change_sp; eauto. congruence. + apply agree_nextinstr. eapply agree_change_sp; eauto. + apply agree_exten_temps with rs; eauto. + intros. apply Pregmap.gso; auto with ppcgen. + congruence. + intros. rewrite nextinstr_inv; auto with ppcgen. + rewrite Pregmap.gso; auto with ppcgen. + rewrite Pregmap.gss. eapply agree_sp; eauto. Qed. Lemma exec_function_external_prop: @@ -1163,6 +1206,7 @@ Proof. intros; red; intros; inv MS. inv STACKS. simpl in *. right. split. omega. split. auto. econstructor; eauto. rewrite ATPC; eauto. + congruence. Qed. Theorem transf_instr_correct: diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index aef03db..81154f9 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -1009,10 +1009,29 @@ Proof. destruct (Int.lt n1 n2); auto. Qed. -Lemma testcond_for_signed_comparison_correct_pi: +Lemma testcond_for_unsigned_comparison_correct_ii: + forall c n1 n2 rs, + eval_testcond (testcond_for_unsigned_comparison c) + (nextinstr (compare_ints (Vint n1) (Vint n2) rs)) = + Some(Int.cmpu c n1 n2). +Proof. + intros. generalize (compare_ints_spec rs (Vint n1) (Vint n2)). + set (rs' := nextinstr (compare_ints (Vint n1) (Vint n2) rs)). + intros [A [B [C D]]]. + unfold eval_testcond. rewrite A; rewrite B; rewrite C. + destruct c; simpl. + destruct (Int.eq n1 n2); auto. + destruct (Int.eq n1 n2); auto. + destruct (Int.ltu n1 n2); auto. + rewrite int_not_ltu. destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto. + rewrite (int_ltu_not n1 n2). destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto. + destruct (Int.ltu n1 n2); auto. +Qed. + +Lemma testcond_for_unsigned_comparison_correct_pi: forall c blk n1 n2 rs b, eval_compare_null c n2 = Some b -> - eval_testcond (testcond_for_signed_comparison c) + eval_testcond (testcond_for_unsigned_comparison c) (nextinstr (compare_ints (Vptr blk n1) (Vint n2) rs)) = Some b. Proof. intros. @@ -1028,10 +1047,10 @@ Proof. rewrite <- H0; auto. Qed. -Lemma testcond_for_signed_comparison_correct_ip: +Lemma testcond_for_unsigned_comparison_correct_ip: forall c blk n1 n2 rs b, eval_compare_null c n1 = Some b -> - eval_testcond (testcond_for_signed_comparison c) + eval_testcond (testcond_for_unsigned_comparison c) (nextinstr (compare_ints (Vint n1) (Vptr blk n2) rs)) = Some b. Proof. intros. @@ -1047,14 +1066,18 @@ Proof. rewrite <- H0; auto. Qed. -Lemma testcond_for_signed_comparison_correct_pp: - forall c b1 n1 b2 n2 rs b, - (if eq_block b1 b2 then Some (Int.cmp c n1 n2) else eval_compare_mismatch c) = Some b -> - eval_testcond (testcond_for_signed_comparison c) +Lemma testcond_for_unsigned_comparison_correct_pp: + forall c b1 n1 b2 n2 rs m b, + (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) = Some b -> + eval_testcond (testcond_for_unsigned_comparison c) (nextinstr (compare_ints (Vptr b1 n1) (Vptr b2 n2) rs)) = Some b. Proof. - intros. generalize (compare_ints_spec rs (Vptr b1 n1) (Vptr b2 n2)). + intros. + destruct (Mem.valid_pointer m b1 (Int.unsigned n1) && Mem.valid_pointer m b2 (Int.unsigned n2)); try discriminate. + generalize (compare_ints_spec rs (Vptr b1 n1) (Vptr b2 n2)). set (rs' := nextinstr (compare_ints (Vptr b1 n1) (Vptr b2 n2) rs)). intros [A [B [C D]]]. unfold eq_block in H. unfold eval_testcond. rewrite A; rewrite B; rewrite C. @@ -1063,37 +1086,18 @@ Proof. rewrite <- H; auto. destruct (zeq b1 b2). inversion H. destruct (Int.eq n1 n2); auto. rewrite <- H; auto. - destruct (zeq b1 b2). inversion H. destruct (Int.lt n1 n2); auto. + destruct (zeq b1 b2). inversion H. destruct (Int.ltu n1 n2); auto. discriminate. destruct (zeq b1 b2). inversion H. - rewrite int_not_lt. destruct (Int.lt n1 n2); destruct (Int.eq n1 n2); auto. + rewrite int_not_ltu. destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto. discriminate. destruct (zeq b1 b2). inversion H. - rewrite (int_lt_not n1 n2). destruct (Int.lt n1 n2); destruct (Int.eq n1 n2); auto. + rewrite (int_ltu_not n1 n2). destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto. discriminate. - destruct (zeq b1 b2). inversion H. destruct (Int.lt n1 n2); auto. + destruct (zeq b1 b2). inversion H. destruct (Int.ltu n1 n2); auto. discriminate. Qed. -Lemma testcond_for_unsigned_comparison_correct: - forall c n1 n2 rs, - eval_testcond (testcond_for_unsigned_comparison c) - (nextinstr (compare_ints (Vint n1) (Vint n2) rs)) = - Some(Int.cmpu c n1 n2). -Proof. - intros. generalize (compare_ints_spec rs (Vint n1) (Vint n2)). - set (rs' := nextinstr (compare_ints (Vint n1) (Vint n2) rs)). - intros [A [B [C D]]]. - unfold eval_testcond. rewrite A; rewrite B; rewrite C. - destruct c; simpl. - destruct (Int.eq n1 n2); auto. - destruct (Int.eq n1 n2); auto. - destruct (Int.ltu n1 n2); auto. - rewrite int_not_ltu. destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto. - rewrite (int_ltu_not n1 n2). destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto. - destruct (Int.ltu n1 n2); auto. -Qed. - Lemma compare_floats_spec: forall rs n1 n2, let rs' := nextinstr (compare_floats (Vfloat n1) (Vfloat n2) rs) in @@ -1214,7 +1218,7 @@ Qed. Lemma transl_cond_correct: forall cond args k c rs m b, transl_cond cond args k = OK c -> - eval_condition cond (map rs (map preg_of args)) = Some b -> + eval_condition cond (map rs (map preg_of args)) m = Some b -> exists rs', exec_straight c rs m k rs' m /\ eval_testcond (testcond_for_condition cond) rs' = Some b @@ -1227,32 +1231,33 @@ Proof. econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. simpl in H0. FuncInv. subst b. apply testcond_for_signed_comparison_correct_ii. - apply testcond_for_signed_comparison_correct_ip; auto. - apply testcond_for_signed_comparison_correct_pi; auto. - apply testcond_for_signed_comparison_correct_pp; auto. intros. unfold compare_ints. repeat SOther. (* compu *) - simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0. rewrite (ireg_of_eq _ _ EQ1) in H0. + simpl map in H0. + rewrite (ireg_of_eq _ _ EQ) in H0. rewrite (ireg_of_eq _ _ EQ1) in H0. econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. simpl in H0. FuncInv. - subst b. apply testcond_for_unsigned_comparison_correct. + subst b. apply testcond_for_unsigned_comparison_correct_ii. + apply testcond_for_unsigned_comparison_correct_ip; auto. + apply testcond_for_unsigned_comparison_correct_pi; auto. + eapply testcond_for_unsigned_comparison_correct_pp; eauto. intros. unfold compare_ints. repeat SOther. (* compimm *) simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0. - econstructor. split. apply exec_straight_one. simpl; eauto. auto. - split. simpl in H0. FuncInv. - subst b. apply testcond_for_signed_comparison_correct_ii. - apply testcond_for_signed_comparison_correct_pi; auto. - intros. unfold compare_ints. repeat SOther. -(* compuimm *) - simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0. exists (nextinstr (compare_ints (rs x) (Vint i) rs)). split. destruct (Int.eq_dec i Int.zero). apply exec_straight_one. subst i. simpl. simpl in H0. FuncInv. simpl. rewrite Int.and_idem. auto. auto. apply exec_straight_one; auto. split. simpl in H0. FuncInv. - subst b. apply testcond_for_unsigned_comparison_correct. + subst b. apply testcond_for_signed_comparison_correct_ii. + intros. unfold compare_ints. repeat SOther. +(* compuimm *) + simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0. + econstructor. split. apply exec_straight_one. simpl; eauto. auto. + split. simpl in H0. FuncInv. + subst b. apply testcond_for_unsigned_comparison_correct_ii. + apply testcond_for_unsigned_comparison_correct_pi; auto. intros. unfold compare_ints. repeat SOther. (* compf *) simpl map in H0. rewrite (freg_of_eq _ _ EQ) in H0. rewrite (freg_of_eq _ _ EQ1) in H0. @@ -1333,7 +1338,7 @@ Ltac TranslOp := Lemma transl_op_correct: forall op args res k c (rs: regset) m v, transl_op op args res k = OK c -> - eval_operation ge (rs#ESP) op (map rs (map preg_of args)) = Some v -> + eval_operation ge (rs#ESP) op (map rs (map preg_of args)) m = Some v -> exists rs', exec_straight c rs m k rs' m /\ rs'#(preg_of res) = v @@ -1342,7 +1347,7 @@ Lemma transl_op_correct: r <> preg_of res -> rs' r = rs r. Proof. intros until v; intros TR EV. - rewrite <- (eval_operation_weaken _ _ _ _ EV). + rewrite <- (eval_operation_weaken _ _ _ _ _ EV). destruct op; simpl in TR; ArgsInv; try (TranslOp; fail). (* move *) exploit mk_mov_correct; eauto. intros [rs2 [A [B C]]]. @@ -1383,8 +1388,8 @@ Proof. rewrite (eval_addressing_weaken _ _ _ _ EV). rewrite <- EA. TranslOp. (* condition *) - remember (eval_condition c0 rs ## (preg_of ## args)) as ob. destruct ob; inv EV. - rewrite (eval_condition_weaken _ _ (sym_equal Heqob)). + remember (eval_condition c0 rs ## (preg_of ## args) m) as ob. destruct ob; inv EV. + rewrite (eval_condition_weaken _ _ _ (sym_equal Heqob)). exploit transl_cond_correct; eauto. intros [rs2 [P [Q R]]]. exists (nextinstr (rs2#ECX <- Vundef #EDX <- Vundef #x <- v)). split. eapply exec_straight_trans. eauto. diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v index 048f5a2..95df712 100644 --- a/ia32/Asmgenretaddr.v +++ b/ia32/Asmgenretaddr.v @@ -71,7 +71,7 @@ Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop := forall f c ofs, (forall tf tc, transf_function f = OK tf -> - transl_code f c = OK tc -> + transl_code f c false = OK tc -> code_tail ofs tf tc) -> return_address_offset f c (Int.repr ofs). @@ -202,7 +202,7 @@ Proof. Qed. Lemma transl_instr_tail: - forall f i k c, transl_instr f i k = OK c -> is_tail k c. + forall f i ep k c, transl_instr f i ep k = OK c -> is_tail k c. Proof. unfold transl_instr; intros. destruct i; IsTail. eapply is_tail_trans; eapply loadind_tail; eauto. @@ -213,32 +213,40 @@ Proof. destruct s0; IsTail. eapply is_tail_trans. 2: eapply transl_cond_tail; eauto. IsTail. Qed. - + Lemma transl_code_tail: forall f c1 c2, is_tail c1 c2 -> - forall tc1 tc2, transl_code f c1 = OK tc1 -> transl_code f c2 = OK tc2 -> - is_tail tc1 tc2. + forall tc2 ep2, transl_code f c2 ep2 = OK tc2 -> + exists tc1, exists ep1, transl_code f c1 ep1 = OK tc1 /\ is_tail tc1 tc2. Proof. induction 1; simpl; intros. - replace tc2 with tc1 by congruence. constructor. - IsTail. apply is_tail_trans with x. eauto. eapply transl_instr_tail; eauto. + exists tc2; exists ep2; split; auto with coqlib. + monadInv H0. exploit IHis_tail; eauto. intros [tc1 [ep1 [A B]]]. + exists tc1; exists ep1; split. auto. + apply is_tail_trans with x. auto. eapply transl_instr_tail; eauto. 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. - caseEq (transf_function f). intros tf TF. - caseEq (transl_code f c). intros tc TC. - assert (is_tail tc tf). - unfold transf_function in TF. monadInv TF. - destruct (zlt (list_length_z x) Int.max_unsigned); monadInv EQ0. - IsTail. eapply transl_code_tail; eauto. - destruct (is_tail_code_tail _ _ H0) as [ofs A]. + caseEq (transf_function f). intros tf TF. + assert (exists tc1, transl_code f (fn_code f) true = OK tc1 /\ is_tail tc1 tf). + monadInv TF. + destruct (zlt (list_length_z x) Int.max_unsigned); monadInv EQ0. + econstructor; eauto with coqlib. + destruct H0 as [tc2 [A B]]. + exploit transl_code_tail; eauto. intros [tc1 [ep [C D]]]. +Opaque transl_instr. + monadInv C. + assert (is_tail x tf). + apply is_tail_trans with tc2; auto. + apply is_tail_trans with tc1; auto. + eapply transl_instr_tail; eauto. + exploit is_tail_code_tail. eexact H0. intros [ofs C]. exists (Int.repr ofs). constructor; intros. congruence. intros. exists (Int.repr 0). constructor; intros; congruence. - intros. exists (Int.repr 0). constructor; intros; congruence. Qed. diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index 105a7bd..79e1537 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/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. @@ -120,9 +120,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. @@ -181,7 +181,7 @@ Proof. inv H4. destruct (Float.intoffloat f); 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. @@ -202,6 +202,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: @@ -217,20 +218,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. @@ -303,8 +304,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. @@ -315,8 +316,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. @@ -327,8 +328,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. @@ -339,8 +340,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. @@ -348,8 +349,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. @@ -360,8 +361,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. @@ -374,8 +375,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. @@ -388,8 +389,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. @@ -400,8 +401,8 @@ 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. @@ -432,8 +433,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. rewrite (Int.is_power2_range _ _ H0). @@ -32,6 +32,7 @@ Require Import Values. Require Import Memdata. Require Import Memory. Require Import Globalenvs. +Require Import Events. Set Implicit Arguments. @@ -147,27 +148,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 => @@ -228,7 +232,7 @@ Definition eval_addressing 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) @@ -289,7 +293,7 @@ Definition eval_operation | Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1)) | 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 @@ -340,21 +344,24 @@ 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: condition) (vl: list val) (b: bool) (m: mem), + 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 discriminate. + destruct (eq_block b0 b1); try discriminate. + 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. @@ -384,8 +391,8 @@ Proof. Qed. 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; auto. @@ -507,9 +514,9 @@ Proof. Qed. 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. @@ -570,7 +577,7 @@ End SOUNDNESS. (** Alternate definition of [eval_condition], [eval_op], [eval_addressing] as total functions that return [Vundef] when not applicable - (instead of [None]). Used in the proof of [PPCgen]. *) + (instead of [None]). Used in the proof of [Asmgen]. *) Section EVAL_OP_TOTAL. @@ -675,14 +682,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 discriminate. unfold eq_block in H. destruct (zeq b0 b1). congruence. apply eval_compare_mismatch_weaken; auto. @@ -705,8 +714,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. @@ -729,7 +738,7 @@ Proof. destruct (Int.ltu i Int.iwordsize); congruence. apply eval_addressing_weaken; auto. destruct (Float.intoffloat f); simpl in H; 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. @@ -779,12 +788,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 := @@ -808,10 +825,11 @@ Proof. Qed. 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. @@ -819,30 +837,182 @@ Proof. 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.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 i 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.repr 31)); 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 (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.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 i 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.repr 31)); 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. eapply eval_addressing_lessdef; eauto. exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto. exists v1; split; auto. - 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 (eval_condition c vl1 m1) as [] _eqn. + rewrite (eval_condition_lessdef c H H0 Heqo). + destruct b; inv H1; TrivialExists. + discriminate. 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 + | Olea addr => Olea (shift_stack_addressing delta addr) + | _ => 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. simpl. decEq. apply type_shift_stack_addressing. +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. rewrite Int.add_commut. apply Int.add_assoc. + repeat rewrite Int.add_assoc. decEq. rewrite Int.add_commut. apply Int.add_assoc. + repeat rewrite Int.add_assoc. decEq. rewrite Int.add_commut. apply Int.add_assoc. + 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. + destruct (Genv.find_symbol genv i0) as [] _eqn; inv H0. + TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto. + 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. + 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. + 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.eq i0 Int.zero); inv H1. TrivialExists2. + destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2. + destruct (Int.ltu i Int.iwordsize); inv H1. 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 i0 Int.iwordsize); inv H1. TrivialExists2. + destruct (Int.ltu i Int.iwordsize); inv H1. TrivialExists2. + destruct (Int.ltu i Int.iwordsize); inv H1. TrivialExists2. + eapply eval_addressing_inject; eauto. + 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 @@ -851,10 +1021,10 @@ End EVAL_LESSDEF. Definition op_for_binary_addressing (addr: addressing) : operation := Olea addr. 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. simpl. auto. Qed. @@ -925,53 +1095,21 @@ Definition is_trivial_op (op: operation) : bool := | _ => false end. -(** Shifting stack-relative references. This is used in [Stacking]. *) +(** Operations that depend on the memory state. *) -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) := +Definition op_depends_on_memory (op: operation) : bool := match op with - | Olea addr => Olea (shift_stack_addressing delta addr) - | _ => 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. +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 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. + intros until m2. destruct op; simpl; try congruence. + destruct c; simpl; congruence. Qed. -Lemma shift_stack_eval_operation: - forall (F V: Type) (ge: Genv.t F V) sp op args delta, - eval_operation ge (Val.sub sp (Vint delta)) (shift_stack_operation delta op) args = - eval_operation ge sp op args. -Proof. - intros. destruct op; simpl; auto. - apply shift_stack_eval_addressing. -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. simpl. decEq. apply type_shift_stack_addressing. -Qed. - - diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index e4c2ea1..e4de2a3 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -165,12 +165,12 @@ let int32_align n a = then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a)) else Int32.logand n (Int32.of_int (-a)) -let sp_adjustment lo hi = - let lo = camlint_of_coqint lo and hi = camlint_of_coqint hi in - let sz = Int32.sub hi lo in -(* Enforce stack alignment, noting that 4 bytes are already allocated - by the call *) - let sz = Int32.sub (int32_align (Int32.add sz 4l) stack_alignment) 4l in +let sp_adjustment sz = + let sz = camlint_of_coqint sz in + (* Preserve proper alignment of the stack *) + let sz = int32_align sz stack_alignment in + (* The top 4 bytes have already been allocated by the "call" instruction. *) + let sz = Int32.sub sz 4l in assert (sz >= 0l); sz @@ -549,14 +549,14 @@ let print_instruction oc labels = function | Plabel(l) -> if Labelset.mem l labels then fprintf oc "%a:\n" label (transl_label l) - | Pallocframe(lo, hi, ofs_ra, ofs_link) -> - let sz = sp_adjustment lo hi in + | Pallocframe(sz, ofs_ra, ofs_link) -> + let sz = sp_adjustment sz in let ofs_link = camlint_of_coqint ofs_link in fprintf oc " subl $%ld, %%esp\n" sz; fprintf oc " leal %ld(%%esp), %%edx\n" (Int32.add sz 4l); fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link - | Pfreeframe(lo, hi, ofs_ra, ofs_link) -> - let sz = sp_adjustment lo hi in + | Pfreeframe(sz, ofs_ra, ofs_link) -> + let sz = sp_adjustment sz in fprintf oc " addl $%ld, %%esp\n" sz | Pbuiltin(ef, args, res) -> let name = extern_atom ef.ef_id in diff --git a/ia32/SelectOp.v b/ia32/SelectOp.v index 4a4d9e1..c1f5703 100644 --- a/ia32/SelectOp.v +++ b/ia32/SelectOp.v @@ -61,7 +61,7 @@ Definition addrstack (ofs: int) := (** ** 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/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 3d6a667..82bca26 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/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 @@ -150,12 +150,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. 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. @@ -667,7 +667,7 @@ Proof. EvalOp. simpl. rewrite H1. auto. 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) -> @@ -680,6 +680,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 -> @@ -694,15 +707,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. @@ -716,58 +729,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/ia32/standard/Conventions1.v b/ia32/standard/Conventions1.v index a2d7aba..781617e 100644 --- a/ia32/standard/Conventions1.v +++ b/ia32/standard/Conventions1.v @@ -62,7 +62,7 @@ Definition dummy_float_reg := X0. (**r Used in [Coloring]. *) Definition index_int_callee_save (r: mreg) := match r with - | BX => 1 | SI => 2 | DI => 3 | BP => 4 | _ => -1 + | BX => 0 | SI => 1 | DI => 2 | BP => 3 | _ => -1 end. Definition index_float_callee_save (r: mreg) := -1. diff --git a/ia32/standard/Stacklayout.v b/ia32/standard/Stacklayout.v index 135aba1..1fa3fb3 100644 --- a/ia32/standard/Stacklayout.v +++ b/ia32/standard/Stacklayout.v @@ -19,21 +19,15 @@ Require Import Bounds. from bottom (lowest offsets) to top: - Space for outgoing arguments to function calls. - Back link to parent frame -- Return address (formally; it's actually pushed elsewhere) - Local stack slots of integer type. - Saved values of integer callee-save registers used by the function. - Local stack slots of float type. - 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. +- Space for the stack-allocated data declared in Cminor +- Return address. The [frame_env] compilation environment records the positions of -the boundaries between areas in the frame part. +the boundaries between these areas of the activation record. *) Definition fe_ofs_arg := 0. @@ -47,7 +41,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 @@ -55,22 +50,101 @@ Record frame_env : Type := mk_frame_env { Definition make_env (b: bounds) := let olink := 4 * b.(bound_outgoing) in (* back link *) - let oretaddr := olink + 4 in (* return address *) - let oil := oretaddr + 4 in (* integer locals *) + let oil := olink + 4 in (* integer locals *) let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *) 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 oretaddr := align (ostkdata + b.(bound_stack_data)) 4 in (* return address *) + let sz := oretaddr + 4 in (* total size *) mk_frame_env sz olink oretaddr 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 frame_env_separated: + forall b, + let fe := make_env b in + 0 <= fe_ofs_arg + /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_link) + /\ fe.(fe_ofs_link) + 4 <= 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_ofs_retaddr) + /\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_size). +Proof. + 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)) 4 (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)) + /\ (4 | 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 := 4 * bound_outgoing b). + assert (4 | x1). unfold x1; exists (bound_outgoing b); ring. + set (x2 := x1 + 4). + assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists 1; auto. + set (x3 := x2 + 4 * bound_int_local b). + assert (4 | x3). unfold x2; apply Zdivide_plus_r; auto. exists (bound_int_local b); ring. + set (x4 := x3 + 4 * bound_int_callee_save b). + set (x5 := align x4 8). + assert (8 | x5). unfold x5. apply align_divides. omega. + set (x6 := x5 + 8 * bound_float_local b). + assert (8 | x6). unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring. + set (x7 := x6 + 8 * bound_float_callee_save b). + assert (4 | x7). + apply Zdivides_trans with 8. exists 2; auto. + unfold x7. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. + set (x8 := align (x7 + bound_stack_data b) 4). + assert (4 | x8). apply align_divides. omega. + set (x9 := x8 + 4). + assert (4 | x9). unfold x8; apply Zdivide_plus_r; auto. exists 1; auto. + tauto. +Qed. + +(* Remark align_float_part: forall b, 4 * bound_outgoing b + 4 + 4 + 4 * bound_int_local b + 4 * bound_int_callee_save b <= align (4 * bound_outgoing b + 4 + 4 + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8. + Proof. intros. apply align_le. omega. Qed. +*)
\ No newline at end of file |