diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Asm.v | 14 | ||||
-rw-r--r-- | powerpc/Asmgen.v | 2 | ||||
-rw-r--r-- | powerpc/Asmgenproof.v | 84 | ||||
-rw-r--r-- | powerpc/Asmgenproof1.v | 33 | ||||
-rw-r--r-- | powerpc/Constprop.v | 4 | ||||
-rw-r--r-- | powerpc/Constpropproof.v | 128 | ||||
-rw-r--r-- | powerpc/Op.v | 164 | ||||
-rw-r--r-- | powerpc/Selection.v | 1 | ||||
-rw-r--r-- | powerpc/Selectionproof.v | 91 | ||||
-rw-r--r-- | powerpc/eabi/Conventions.v | 4 | ||||
-rw-r--r-- | powerpc/macosx/Conventions.v | 4 |
11 files changed, 162 insertions, 367 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index b4490afe..69085aa9 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -100,7 +100,6 @@ Inductive instruction : Set := | 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 *) - | Pallocblock: instruction (**r allocate new heap block *) | Pallocframe: Z -> 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 *) @@ -293,11 +292,6 @@ lbl: .long 0x43300000, 0x00000000 >> Again, our memory model cannot comprehend that this operation frees (logically) the current stack frame. -- [Pallocheap]: in the formal semantics, this pseudo-instruction - allocates a heap block of size the contents of [GPR3], and leaves - a pointer to this block in [GPR3]. In the generated assembly code, - it is turned into a call to the allocation function of the run-time - system. *) Definition code := list instruction. @@ -554,14 +548,6 @@ 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 - | Pallocblock => - match rs#GPR3 with - | Vint n => - let (m', b) := Mem.alloc m 0 (Int.signed n) in - OK (nextinstr (rs#GPR3 <- (Vptr b Int.zero) - #LR <- (Val.add rs#PC Vone))) m' - | _ => Error - end | Pallocframe lo hi ofs => let (m1, stk) := Mem.alloc m lo hi in let sp := Vptr stk (Int.repr lo) in diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 2ddaa6d0..1dcc3990 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -457,8 +457,6 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Pmtlr GPR12 :: Pfreeframe f.(fn_link_ofs) :: Pbs symb :: k - | Malloc => - Pallocblock :: k | Mlabel lbl => Plabel lbl :: k | Mgoto lbl => diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 980925bd..a96125a2 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -537,68 +537,6 @@ Proof. intros. apply Pregmap.gso; auto. Qed. -(** * Memory properties *) - -(** The PowerPC has no instruction for ``load 8-bit signed integer''. - We show that it can be synthesized as a ``load 8-bit unsigned integer'' - followed by a sign extension. *) - -Remark valid_access_equiv: - forall chunk1 chunk2 m b ofs, - size_chunk chunk1 = size_chunk chunk2 -> - valid_access m chunk1 b ofs -> - valid_access m chunk2 b ofs. -Proof. - intros. inv H0. rewrite H in H3. constructor; auto. -Qed. - -Remark in_bounds_equiv: - forall chunk1 chunk2 m b ofs (A: Set) (a1 a2: A), - size_chunk chunk1 = size_chunk chunk2 -> - (if in_bounds m chunk1 b ofs then a1 else a2) = - (if in_bounds m chunk2 b ofs then a1 else a2). -Proof. - intros. destruct (in_bounds m chunk1 b ofs). - rewrite in_bounds_true. auto. eapply valid_access_equiv; eauto. - destruct (in_bounds m chunk2 b ofs); auto. - elim n. eapply valid_access_equiv with (chunk1 := chunk2); eauto. -Qed. - -Lemma loadv_8_signed_unsigned: - forall m a, - Mem.loadv Mint8signed m a = - option_map (Val.sign_ext 8) (Mem.loadv Mint8unsigned m a). -Proof. - intros. unfold Mem.loadv. destruct a; try reflexivity. - unfold load. rewrite (in_bounds_equiv Mint8signed Mint8unsigned). - destruct (in_bounds m Mint8unsigned b (Int.signed i)); auto. - simpl. - destruct (getN 0 (Int.signed i) (contents (blocks m b))); auto. - simpl. rewrite Int.sign_ext_zero_ext. auto. compute; auto. - auto. -Qed. - -(** Similarly, we show that signed 8- and 16-bit stores can be performed - like unsigned stores. *) - -Lemma storev_8_signed_unsigned: - forall m a v, - Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. -Proof. - intros. unfold storev. destruct a; auto. - unfold store. rewrite (in_bounds_equiv Mint8signed Mint8unsigned). - auto. auto. -Qed. - -Lemma storev_16_signed_unsigned: - forall m a v, - Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. -Proof. - intros. unfold storev. destruct a; auto. - unfold store. rewrite (in_bounds_equiv Mint16signed Mint16unsigned). - auto. auto. -Qed. - (** * Proof of semantic preservation *) (** Semantic preservation is proved using simulation diagrams @@ -805,7 +743,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 m = Some v -> + eval_operation ge sp op ms ## args = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0 (Machconcr.State s fb sp c (Regmap.set res v ms) m). Proof. @@ -1069,21 +1007,6 @@ Proof. unfold rs5; auto with ppcgen. Qed. -Lemma exec_Malloc_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (c : list Mach.instruction) (ms : mreg -> val) (m : mem) (sz : int) - (m' : mem) (blk : block), - ms Conventions.loc_alloc_argument = Vint sz -> - alloc m 0 (Int.signed sz) = (m', blk) -> - exec_instr_prop (Machconcr.State s fb sp (Malloc :: c) ms m) E0 - (Machconcr.State s fb sp c - (Regmap.set (Conventions.loc_alloc_result) (Vptr blk Int.zero) ms) m'). -Proof. - intros; red; intros; inv MS. - left; eapply exec_straight_steps; eauto with coqlib. - simpl. eapply transl_alloc_correct; eauto. -Qed. - Lemma exec_Mgoto_prop: forall (s : list stackframe) (fb : block) (f : function) (sp : val) (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) @@ -1113,7 +1036,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 m = Some true -> + eval_condition cond ms ## args = 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 @@ -1156,7 +1079,7 @@ Lemma exec_Mcond_false_prop: forall (s : list stackframe) (fb : block) (sp : val) (cond : condition) (args : list mreg) (lbl : Mach.label) (c : list Mach.instruction) (ms : mreg -> val) (m : mem), - eval_condition cond ms ## args m = Some false -> + eval_condition cond ms ## args = Some false -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 (Machconcr.State s fb sp c ms m). Proof. @@ -1345,7 +1268,6 @@ Proof exec_Mstore_prop exec_Mcall_prop exec_Mtailcall_prop - exec_Malloc_prop exec_Mgoto_prop exec_Mcond_true_prop exec_Mcond_false_prop diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index c17cb737..fdb48bec 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1122,7 +1122,7 @@ Lemma transl_cond_correct: forall cond args k ms sp rs m b, map mreg_type args = type_of_condition cond -> agree ms sp rs -> - eval_condition cond (map ms args) m = Some b -> + eval_condition cond (map ms args) = Some b -> exists rs', exec_straight (transl_cond cond args k) rs m k rs' m /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = @@ -1131,7 +1131,7 @@ Lemma transl_cond_correct: else Val.notbool (Val.of_bool b)) /\ agree ms sp rs'. Proof. - intros. rewrite <- (eval_condition_weaken _ _ _ H1). + intros. rewrite <- (eval_condition_weaken _ _ H1). apply transl_cond_correct_aux; auto. Qed. @@ -1161,12 +1161,12 @@ Lemma transl_op_correct: forall op args res k ms sp rs m v, wt_instr (Mop op args res) -> agree ms sp rs -> - eval_operation ge sp op (map ms args) m = Some v -> + eval_operation ge sp op (map ms args) = Some v -> exists rs', exec_straight (transl_op op args res k) rs m k rs' m /\ agree (Regmap.set res v ms) sp rs'. Proof. - intros. rewrite <- (eval_operation_weaken _ _ _ _ _ H1). clear H1; clear v. + intros. rewrite <- (eval_operation_weaken _ _ _ _ H1). clear H1; clear v. inversion H. (* Omove *) simpl. exists (nextinstr (rs#(preg_of res) <- (ms r1))). @@ -1602,31 +1602,6 @@ Proof. auto. auto. Qed. -(** Translation of allocations *) - -Lemma transl_alloc_correct: - forall ms sp rs sz m m' blk k, - agree ms sp rs -> - ms Conventions.loc_alloc_argument = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - let ms' := Regmap.set Conventions.loc_alloc_result (Vptr blk Int.zero) ms in - exists rs', - exec_straight (Pallocblock :: k) rs m k rs' m' - /\ agree ms' sp rs'. -Proof. - intros. - pose (rs' := nextinstr (rs#GPR3 <- (Vptr blk Int.zero) #LR <- (Val.add rs#PC Vone))). - exists rs'; split. - apply exec_straight_one. unfold exec_instr. - generalize (preg_val _ _ _ Conventions.loc_alloc_argument H). - unfold preg_of; intro. simpl in H2. rewrite <- H2. rewrite H0. - rewrite H1. reflexivity. - reflexivity. - unfold ms', rs'. apply agree_nextinstr. apply agree_set_other. - change (IR GPR3) with (preg_of Conventions.loc_alloc_result). - apply agree_set_mreg. auto. - simpl. tauto. -Qed. End STRAIGHTLINE. diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v index 75fb1486..6ec27a3f 100644 --- a/powerpc/Constprop.v +++ b/powerpc/Constprop.v @@ -654,8 +654,10 @@ Definition transfer (f: function) (pc: node) (before: D.t) := D.set res Unknown before | Itailcall sig ros args => before +(* | Ialloc arg res s => D.set res Unknown before +*) | Icond cond args ifso ifnot => before | Ireturn optarg => @@ -1045,8 +1047,6 @@ Definition transf_instr (approx: D.t) (instr: instruction) := Icall sig (transf_ros approx ros) args res s | Itailcall sig ros args => Itailcall sig (transf_ros approx ros) args - | Ialloc arg res s => - Ialloc arg res s | Icond cond args s1 s2 => match eval_static_condition cond (approx_regs args approx) with | Some b => diff --git a/powerpc/Constpropproof.v b/powerpc/Constpropproof.v index e16f322e..dbd498f9 100644 --- a/powerpc/Constpropproof.v +++ b/powerpc/Constpropproof.v @@ -143,10 +143,10 @@ Ltac InvVLMA := approximations returned by [eval_static_operation]. *) Lemma eval_static_condition_correct: - forall cond al vl m b, + forall cond al vl b, val_list_match_approx al vl -> eval_static_condition cond al = Some b -> - eval_condition cond vl m = Some b. + eval_condition cond vl = Some b. Proof. intros until b. unfold eval_static_condition. @@ -155,9 +155,9 @@ Proof. Qed. Lemma eval_static_operation_correct: - forall op sp al vl m v, + forall op sp al vl v, val_list_match_approx al vl -> - eval_operation ge sp op vl m = Some v -> + eval_operation ge sp op vl = Some v -> val_match_approx (eval_static_operation op al) v. Proof. intros until v. @@ -203,7 +203,7 @@ Proof. rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence. caseEq (eval_static_condition c vl0). - intros. generalize (eval_static_condition_correct _ _ _ m _ H H1). + intros. generalize (eval_static_condition_correct _ _ _ _ H H1). intro. rewrite H2 in H0. destruct b; injection H0; intro; subst v; simpl; auto. intros; simpl; auto. @@ -276,9 +276,9 @@ Proof. Qed. Lemma cond_strength_reduction_correct: - forall cond args m, + forall cond args, let (cond', args') := cond_strength_reduction approx cond args in - eval_condition cond' rs##args' m = eval_condition cond rs##args m. + eval_condition cond' rs##args' = eval_condition cond rs##args. Proof. intros. unfold cond_strength_reduction. case (cond_strength_reduction_match cond args); intros. @@ -299,10 +299,10 @@ Proof. Qed. Lemma make_addimm_correct: - forall n r m v, + forall n r v, let (op, args) := make_addimm n r in - eval_operation ge sp Oadd (rs#r :: Vint n :: nil) m = Some v -> - eval_operation ge sp op rs##args m = Some v. + eval_operation ge sp Oadd (rs#r :: Vint n :: nil) = Some v -> + eval_operation ge sp op rs##args = Some v. Proof. intros; unfold make_addimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -312,10 +312,10 @@ Proof. Qed. Lemma make_shlimm_correct: - forall n r m v, + forall n r v, let (op, args) := make_shlimm n r in - eval_operation ge sp Oshl (rs#r :: Vint n :: nil) m = Some v -> - eval_operation ge sp op rs##args m = Some v. + eval_operation ge sp Oshl (rs#r :: Vint n :: nil) = Some v -> + eval_operation ge sp op rs##args = Some v. Proof. intros; unfold make_shlimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -326,10 +326,10 @@ Proof. Qed. Lemma make_shrimm_correct: - forall n r m v, + forall n r v, let (op, args) := make_shrimm n r in - eval_operation ge sp Oshr (rs#r :: Vint n :: nil) m = Some v -> - eval_operation ge sp op rs##args m = Some v. + eval_operation ge sp Oshr (rs#r :: Vint n :: nil) = Some v -> + eval_operation ge sp op rs##args = Some v. Proof. intros; unfold make_shrimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -338,10 +338,10 @@ Proof. Qed. Lemma make_shruimm_correct: - forall n r m v, + forall n r v, let (op, args) := make_shruimm n r in - eval_operation ge sp Oshru (rs#r :: Vint n :: nil) m = Some v -> - eval_operation ge sp op rs##args m = Some v. + eval_operation ge sp Oshru (rs#r :: Vint n :: nil) = Some v -> + eval_operation ge sp op rs##args = Some v. Proof. intros; unfold make_shruimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -352,10 +352,10 @@ Proof. Qed. Lemma make_mulimm_correct: - forall n r m v, + forall n r v, let (op, args) := make_mulimm n r in - eval_operation ge sp Omul (rs#r :: Vint n :: nil) m = Some v -> - eval_operation ge sp op rs##args m = Some v. + eval_operation ge sp Omul (rs#r :: Vint n :: nil) = Some v -> + eval_operation ge sp op rs##args = Some v. Proof. intros; unfold make_mulimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -363,8 +363,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) m) - with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil) m). + replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil)) + with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)). apply make_shlimm_correct. simpl. generalize (Int.is_power2_range _ _ H1). change (Z_of_nat wordsize) with 32. intro. rewrite H2. @@ -373,10 +373,10 @@ Proof. Qed. Lemma make_andimm_correct: - forall n r m v, + forall n r v, let (op, args) := make_andimm n r in - eval_operation ge sp Oand (rs#r :: Vint n :: nil) m = Some v -> - eval_operation ge sp op rs##args m = Some v. + eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v -> + eval_operation ge sp op rs##args = Some v. Proof. intros; unfold make_andimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -387,10 +387,10 @@ Proof. Qed. Lemma make_orimm_correct: - forall n r m v, + forall n r v, let (op, args) := make_orimm n r in - eval_operation ge sp Oor (rs#r :: Vint n :: nil) m = Some v -> - eval_operation ge sp op rs##args m = Some v. + eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v -> + eval_operation ge sp op rs##args = Some v. Proof. intros; unfold make_orimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -401,10 +401,10 @@ Proof. Qed. Lemma make_xorimm_correct: - forall n r m v, + forall n r v, let (op, args) := make_xorimm n r in - eval_operation ge sp Oxor (rs#r :: Vint n :: nil) m = Some v -> - eval_operation ge sp op rs##args m = Some v. + eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v -> + eval_operation ge sp op rs##args = Some v. Proof. intros; unfold make_xorimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -413,18 +413,18 @@ Proof. Qed. Lemma op_strength_reduction_correct: - forall op args m v, + forall op args v, let (op', args') := op_strength_reduction approx op args in - eval_operation ge sp op rs##args m = Some v -> - eval_operation ge sp op' rs##args' m = Some v. + eval_operation ge sp op rs##args = Some v -> + eval_operation ge sp op' rs##args' = Some v. Proof. intros; unfold op_strength_reduction; case (op_strength_reduction_match op args); intros; simpl List.map. (* Oadd *) caseEq (intval approx r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil) m) - with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil) m). + replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil)) + with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)). apply make_addimm_correct. simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto. caseEq (intval approx r2); intros. @@ -435,16 +435,16 @@ Proof. rewrite (intval_correct _ _ H) in H0. assumption. caseEq (intval approx r2); intros. rewrite (intval_correct _ _ H0). - 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). + replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil)) + with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)). apply make_addimm_correct. simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. assumption. (* Omul *) caseEq (intval approx r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil) m) - with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil) m). + replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil)) + with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)). apply make_mulimm_correct. simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto. caseEq (intval approx r2); intros. @@ -464,8 +464,8 @@ Proof. caseEq (intval approx r2); intros. caseEq (Int.is_power2 i); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil) m) - with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil) m). + replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil)) + with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)). apply make_shruimm_correct. simpl. destruct rs#r1; auto. change 32 with (Z_of_nat wordsize). @@ -478,8 +478,8 @@ Proof. (* Oand *) caseEq (intval approx r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil) m) - with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil) m). + replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil)) + with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)). apply make_andimm_correct. simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto. caseEq (intval approx r2); intros. @@ -488,8 +488,8 @@ Proof. (* Oor *) caseEq (intval approx r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil) m) - with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil) m). + replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil)) + with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)). apply make_orimm_correct. simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto. caseEq (intval approx r2); intros. @@ -498,8 +498,8 @@ Proof. (* Oxor *) caseEq (intval approx r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil) m) - with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil) m). + replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil)) + with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)). apply make_xorimm_correct. simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto. caseEq (intval approx r2); intros. @@ -763,13 +763,13 @@ Proof. exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. TransfInstr. caseEq (op_strength_reduction (analyze f)!!pc op args); intros op' args' OSR. - assert (eval_operation tge sp op' rs##args' m = Some v). + assert (eval_operation tge sp op' rs##args' = Some v). rewrite (eval_operation_preserved symbols_preserved). generalize (op_strength_reduction_correct ge (analyze f)!!pc sp rs - MATCH op args m v). + MATCH op args v). rewrite OSR; simpl. auto. generalize (eval_static_operation_correct ge op sp - (approx_regs args (analyze f)!!pc) rs##args m v + (approx_regs args (analyze f)!!pc) rs##args v (approx_regs_val_list _ _ _ args MATCH) H0). case (eval_static_operation op (approx_regs args (analyze f)!!pc)); intros; simpl in H2; @@ -838,28 +838,18 @@ Proof. eapply exec_Itailcall; eauto. apply sig_function_translated; auto. constructor; auto. - (* Ialloc *) - TransfInstr; intro. - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- (Vptr b Int.zero)) m'); split. - eapply exec_Ialloc; eauto. - econstructor; eauto. - apply analyze_correct_1 with pc; auto. - unfold successors; rewrite H; auto with coqlib. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. simpl; auto. - (* Icond, true *) exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. caseEq (cond_strength_reduction (analyze f)!!pc cond args); intros cond' args' CSR. - assert (eval_condition cond' rs##args' m = Some true). + assert (eval_condition cond' rs##args' = Some true). generalize (cond_strength_reduction_correct - ge (analyze f)!!pc rs MATCH cond args m). + ge (analyze f)!!pc rs MATCH cond args). rewrite CSR. intro. congruence. TransfInstr. rewrite CSR. caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)). intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ m _ + generalize (eval_static_condition_correct ge cond _ _ _ (approx_regs_val_list _ _ _ args MATCH) ESC); intro. replace b with true. intro; eapply exec_Inop; eauto. congruence. intros. eapply exec_Icond_true; eauto. @@ -872,14 +862,14 @@ Proof. exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. caseEq (cond_strength_reduction (analyze f)!!pc cond args); intros cond' args' CSR. - assert (eval_condition cond' rs##args' m = Some false). + assert (eval_condition cond' rs##args' = Some false). generalize (cond_strength_reduction_correct - ge (analyze f)!!pc rs MATCH cond args m). + ge (analyze f)!!pc rs MATCH cond args). rewrite CSR. intro. congruence. TransfInstr. rewrite CSR. caseEq (eval_static_condition cond (approx_regs args (analyze f)!!pc)). intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ m _ + generalize (eval_static_condition_correct ge cond _ _ _ (approx_regs_val_list _ _ _ args MATCH) ESC); intro. replace b with false. intro; eapply exec_Inop; eauto. congruence. intros. eapply exec_Icond_false; eauto. diff --git a/powerpc/Op.v b/powerpc/Op.v index 20ebf705..300a8043 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -139,28 +139,28 @@ Qed. Definition eval_compare_mismatch (c: comparison) : option bool := match c with Ceq => Some false | Cne => Some true | _ => None end. -Definition eval_condition (cond: condition) (vl: list val) (m: mem): +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): 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 valid_pointer m b1 (Int.signed n1) - && valid_pointer m b2 (Int.signed n2) then - if eq_block b1 b2 - then Some (Int.cmp c n1 n2) - else eval_compare_mismatch c - else None + 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 => - if Int.eq n2 Int.zero then eval_compare_mismatch c else None + eval_compare_null c n2 | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil => - if Int.eq n1 Int.zero then eval_compare_mismatch c else None + eval_compare_null c n1 | Ccompu c, Vint n1 :: Vint n2 :: nil => Some (Int.cmpu c n1 n2) | Ccompimm c n, Vint n1 :: nil => Some (Int.cmp c n1 n) | Ccompimm c n, Vptr b1 n1 :: nil => - if Int.eq n Int.zero then eval_compare_mismatch c else None + eval_compare_null c n | Ccompuimm c n, Vint n1 :: nil => Some (Int.cmpu c n1 n) | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil => @@ -183,7 +183,7 @@ Definition offset_sp (sp: val) (delta: int) : option val := Definition eval_operation (F: Set) (genv: Genv.t F) (sp: val) - (op: operation) (vl: list val) (m: mem): option val := + (op: operation) (vl: list val): option val := match op, vl with | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) @@ -256,7 +256,7 @@ Definition eval_operation | Ofloatofintu, Vint n1 :: nil => Some (Vfloat (Float.floatofintu n1)) | Ocmp c, _ => - match eval_condition c vl m with + match eval_condition c vl with | None => None | Some false => Some Vfalse | Some true => Some Vtrue @@ -322,24 +322,30 @@ Proof. destruct c; intro EQ; inv EQ; auto. Qed. +Remark eval_negate_compare_null: + forall c i b, + eval_compare_null c i = Some b -> + eval_compare_null (negate_comparison c) i = Some (negb b). +Proof. + unfold eval_compare_null; intros. + destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. congruence. +Qed. + Lemma eval_negate_condition: - 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). + forall (cond: condition) (vl: list val) (b: bool), + eval_condition cond vl = Some b -> + eval_condition (negate_condition cond) vl = Some (negb b). Proof. intros. destruct cond; simpl in H; FuncInv; try subst b; simpl. rewrite Int.negate_cmp. auto. - destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. discriminate. - destruct (Int.eq i0 Int.zero). apply eval_negate_compare_mismatch; auto. discriminate. - destruct (valid_pointer m b0 (Int.signed i) && - valid_pointer m b1 (Int.signed i0)). + apply eval_negate_compare_null; auto. + apply eval_negate_compare_null; auto. destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence. apply eval_negate_compare_mismatch; auto. - discriminate. rewrite Int.negate_cmpu. auto. rewrite Int.negate_cmp. auto. - destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. discriminate. + apply eval_negate_compare_null; auto. rewrite Int.negate_cmpu. auto. auto. rewrite negb_elim. auto. @@ -361,8 +367,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 m, - eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m. + forall sp op vl, + eval_operation ge2 sp op vl = eval_operation ge1 sp op vl. Proof. intros. unfold eval_operation; destruct op; try rewrite agree_on_symbols; @@ -380,74 +386,6 @@ Qed. End GENV_TRANSF. -(** [eval_condition] and [eval_operation] depend on a memory store - (to check pointer validity in pointer comparisons). - We show that their results are preserved by a change of - memory if this change preserves pointer validity. - In particular, this holds in case of a memory allocation - or a memory store. *) - -Lemma eval_condition_change_mem: - forall m m' c args b, - (forall b ofs, valid_pointer m b ofs = true -> valid_pointer m' b ofs = true) -> - eval_condition c args m = Some b -> eval_condition c args m' = Some b. -Proof. - intros until b. intro INV. destruct c; simpl; auto. - destruct args; auto. destruct v; auto. destruct args; auto. - destruct v; auto. destruct args; auto. - caseEq (valid_pointer m b0 (Int.signed i)); intro. - caseEq (valid_pointer m b1 (Int.signed i0)); intro. - simpl. rewrite (INV _ _ H). rewrite (INV _ _ H0). auto. - simpl; congruence. simpl; congruence. -Qed. - -Lemma eval_operation_change_mem: - forall (F: Set) m m' (ge: Genv.t F) sp op args v, - (forall b ofs, valid_pointer m b ofs = true -> valid_pointer m' b ofs = true) -> - eval_operation ge sp op args m = Some v -> eval_operation ge sp op args m' = Some v. -Proof. - intros until v; intro INV. destruct op; simpl; auto. - caseEq (eval_condition c args m); intros. - rewrite (eval_condition_change_mem _ _ _ _ INV H). auto. - discriminate. -Qed. - -Lemma eval_condition_alloc: - forall m lo hi m' b c args v, - Mem.alloc m lo hi = (m', b) -> - eval_condition c args m = Some v -> eval_condition c args m' = Some v. -Proof. - intros. apply eval_condition_change_mem with m; auto. - intros. eapply valid_pointer_alloc; eauto. -Qed. - -Lemma eval_operation_alloc: - forall (F: Set) m lo hi m' b (ge: Genv.t F) sp op args v, - Mem.alloc m lo hi = (m', b) -> - eval_operation ge sp op args m = Some v -> eval_operation ge sp op args m' = Some v. -Proof. - intros. apply eval_operation_change_mem with m; auto. - intros. eapply valid_pointer_alloc; eauto. -Qed. - -Lemma eval_condition_store: - forall chunk m b ofs v' m' c args v, - Mem.store chunk m b ofs v' = Some m' -> - eval_condition c args m = Some v -> eval_condition c args m' = Some v. -Proof. - intros. apply eval_condition_change_mem with m; auto. - intros. eapply valid_pointer_store; eauto. -Qed. - -Lemma eval_operation_store: - forall (F: Set) chunk m b ofs v' m' (ge: Genv.t F) sp op args v, - Mem.store chunk m b ofs v' = Some m' -> - eval_operation ge sp op args m = Some v -> eval_operation ge sp op args m' = Some v. -Proof. - intros. apply eval_operation_change_mem with m; auto. - intros. eapply valid_pointer_store; eauto. -Qed. - (** Recognition of move operations. *) Definition is_move_operation @@ -563,9 +501,9 @@ Variable A: Set. Variable genv: Genv.t A. Lemma type_of_operation_sound: - forall op vl sp v m, + forall op vl sp v, op <> Omove -> - eval_operation genv sp op vl m = Some v -> + eval_operation genv sp op vl = Some v -> Val.has_type v (snd (type_of_operation op)). Proof. intros. @@ -716,35 +654,33 @@ Qed. Lemma eval_compare_null_weaken: forall n c b, - (if Int.eq n Int.zero then eval_compare_mismatch c else None) = Some b -> + eval_compare_null c n = Some b -> (if Int.eq n Int.zero then Val.cmp_mismatch c else Vundef) = Val.of_bool b. Proof. + unfold eval_compare_null. intros. destruct (Int.eq n Int.zero). apply eval_compare_mismatch_weaken. auto. discriminate. Qed. Lemma eval_condition_weaken: - forall c vl m b, - eval_condition c vl m = Some b -> + forall c vl b, + eval_condition c vl = 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 (valid_pointer m b0 (Int.signed i) && - valid_pointer m b1 (Int.signed i0)). unfold eq_block in H. destruct (zeq b0 b1). congruence. apply eval_compare_mismatch_weaken; auto. - discriminate. symmetry. apply Val.notbool_negb_1. symmetry. apply Val.notbool_negb_1. Qed. Lemma eval_operation_weaken: - forall sp op vl m v, - eval_operation genv sp op vl m = Some v -> + forall sp op vl v, + eval_operation genv sp op vl = Some v -> eval_operation_total sp op vl = v. Proof. intros. @@ -763,7 +699,7 @@ Proof. destruct (Int.ltu i (Int.repr 32)); congruence. destruct (Int.ltu i (Int.repr 32)); congruence. destruct (Int.ltu i0 (Int.repr 32)); congruence. - caseEq (eval_condition c vl m); intros; rewrite H0 in H. + caseEq (eval_condition c vl); intros; rewrite H0 in H. replace v with (Val.of_bool b). eapply eval_condition_weaken; eauto. destruct b; simpl; congruence. @@ -806,14 +742,12 @@ Qed. End EVAL_OP_TOTAL. (** Compatibility of the evaluation functions with the - ``is less defined'' relation over values and memory states. *) + ``is less defined'' relation over values. *) Section EVAL_LESSDEF. Variable F: Set. Variable genv: Genv.t F. -Variables m1 m2: mem. -Hypothesis MEM: Mem.lessdef m1 m2. Ltac InvLessdef := match goal with @@ -833,16 +767,10 @@ Ltac InvLessdef := Lemma eval_condition_lessdef: forall cond vl1 vl2 b, Val.lessdef_list vl1 vl2 -> - eval_condition cond vl1 m1 = Some b -> - eval_condition cond vl2 m2 = Some b. + eval_condition cond vl1 = Some b -> + eval_condition cond vl2 = Some b. Proof. intros. destruct cond; simpl in *; FuncInv; InvLessdef; auto. - generalize H0. - caseEq (valid_pointer m1 b0 (Int.signed i)); intro; simpl; try congruence. - caseEq (valid_pointer m1 b1 (Int.signed i0)); intro; simpl; try congruence. - rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H1). - rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H). simpl. - auto. Qed. Ltac TrivialExists := @@ -855,8 +783,8 @@ Ltac TrivialExists := Lemma eval_operation_lessdef: forall sp op vl1 vl2 v1, Val.lessdef_list vl1 vl2 -> - eval_operation genv sp op vl1 m1 = Some v1 -> - exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2. + eval_operation genv sp op vl1 = Some v1 -> + exists v2, eval_operation genv sp op vl2 = Some v2 /\ Val.lessdef v1 v2. Proof. intros. destruct op; simpl in *; FuncInv; InvLessdef; TrivialExists. exists v2; auto. @@ -875,7 +803,7 @@ Proof. destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists. destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto. - caseEq (eval_condition c vl1 m1); intros. rewrite H1 in H0. + 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. @@ -906,10 +834,10 @@ End EVAL_LESSDEF. Definition op_for_binary_addressing (addr: addressing) : operation := Oadd. Lemma eval_op_for_binary_addressing: - forall (F: Set) (ge: Genv.t F) sp addr args m v, + forall (F: Set) (ge: Genv.t F) sp addr args v, (length args >= 2)%nat -> eval_addressing ge sp addr args = Some v -> - eval_operation ge sp (op_for_binary_addressing addr) args m = Some v. + eval_operation ge sp (op_for_binary_addressing addr) args = Some v. Proof. intros. unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; diff --git a/powerpc/Selection.v b/powerpc/Selection.v index 1de6ae3c..f1c5a73b 100644 --- a/powerpc/Selection.v +++ b/powerpc/Selection.v @@ -1161,7 +1161,6 @@ Fixpoint sel_stmt (s: Cminor.stmt) : stmt := Scall optid sg (sel_expr fn) (sel_exprlist args) | Cminor.Stailcall sg fn args => Stailcall sg (sel_expr fn) (sel_exprlist args) - | Cminor.Salloc id b => Salloc id (sel_expr b) | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2) | Cminor.Sifthenelse e ifso ifnot => Sifthenelse (condexpr_of_expr (sel_expr e)) diff --git a/powerpc/Selectionproof.v b/powerpc/Selectionproof.v index 5e0b2b27..b6e838cd 100644 --- a/powerpc/Selectionproof.v +++ b/powerpc/Selectionproof.v @@ -149,13 +149,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 @@ -234,12 +234,12 @@ Proof. eapply eval_notbool_base; eauto. inv H. eapply eval_Eop; eauto. - simpl. assert (eval_condition c vl m = Some b). + simpl. assert (eval_condition c vl = Some b). generalize H6. simpl. - case (eval_condition c vl m); intros. + 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. @@ -545,9 +545,9 @@ Qed. Lemma eval_mod_aux: forall divop semdivop, - (forall sp x y m, + (forall sp x y, y <> Int.zero -> - eval_operation ge sp divop (Vint x :: Vint y :: nil) m = + eval_operation ge sp divop (Vint x :: Vint y :: nil) = Some (Vint (semdivop x y))) -> forall le a b x y, eval_expr ge sp e m le a (Vint x) -> @@ -812,52 +812,66 @@ Proof. EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. Qed. +Remark eval_compare_null_transf: + forall c x v, + Cminor.eval_compare_null c x = Some v -> + match eval_compare_null c x with + | Some true => Some Vtrue + | Some false => Some Vfalse + | None => None (A:=val) + end = Some v. +Proof. + unfold Cminor.eval_compare_null, eval_compare_null; intros. + destruct (Int.eq x Int.zero); try discriminate. + destruct c; try discriminate; auto. +Qed. + Theorem eval_comp_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) -> - (if Int.eq y Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> + Cminor.eval_compare_null c y = Some v -> eval_expr ge sp e m le (comp c a b) v. Proof. intros until v. unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. destruct (Int.eq y Int.zero); try discriminate. - unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. - destruct c; try discriminate; auto. - EvalOp. simpl. destruct (Int.eq y Int.zero); try discriminate. - unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. - destruct c; try discriminate; auto. + EvalOp. simpl. apply eval_compare_null_transf; auto. + EvalOp. simpl. apply eval_compare_null_transf; auto. +Qed. + +Remark eval_compare_null_swap: + forall c x, + Cminor.eval_compare_null (swap_comparison c) x = + Cminor.eval_compare_null c x. +Proof. + intros. unfold Cminor.eval_compare_null. + destruct (Int.eq x Int.zero). destruct c; auto. auto. Qed. Theorem eval_comp_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) -> - (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> + Cminor.eval_compare_null c x = Some v -> eval_expr ge sp e m le (comp c a b) v. Proof. intros until v. unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. destruct (Int.eq x Int.zero); try discriminate. - unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. - destruct c; try discriminate; auto. - EvalOp. simpl. destruct (Int.eq x Int.zero); try discriminate. - unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. - destruct c; try discriminate; auto. + 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: 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) -> - valid_pointer m x1 (Int.signed x2) && - valid_pointer m y1 (Int.signed y2) = true -> x1 = y1 -> eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)). Proof. intros until y2. unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. + EvalOp. simpl. subst y1. rewrite dec_eq_true. destruct (Int.cmp c x2 y2); reflexivity. Qed. @@ -865,16 +879,14 @@ Theorem eval_comp_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) -> - valid_pointer m x1 (Int.signed x2) && - valid_pointer m y1 (Int.signed y2) = true -> x1 <> y1 -> Cminor.eval_compare_mismatch c = Some v -> eval_expr ge sp e m le (comp c a b) v. Proof. intros until y2. unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto. - destruct c; simpl in H3; inv H3; auto. + EvalOp. simpl. rewrite dec_eq_false; auto. + destruct c; simpl in H2; inv H2; auto. Qed. Theorem eval_compu: @@ -955,7 +967,7 @@ Qed. Lemma is_compare_neq_zero_correct: forall c v b, is_compare_neq_zero c = true -> - eval_condition c (v :: nil) m = Some b -> + eval_condition c (v :: nil) = Some b -> Val.bool_of_val v b. Proof. intros. @@ -975,7 +987,7 @@ Qed. Lemma is_compare_eq_zero_correct: forall c v b, is_compare_eq_zero c = true -> - eval_condition c (v :: nil) m = Some b -> + eval_condition c (v :: nil) = Some b -> Val.bool_of_val v (negb b). Proof. intros. apply is_compare_neq_zero_correct with (negate_condition c). @@ -1003,8 +1015,8 @@ Proof. eapply eval_base_condition_of_expr; eauto. inv H0. simpl in H7. - assert (eval_condition c vl m = Some b). - destruct (eval_condition c vl m); try discriminate. + assert (eval_condition c vl = Some b). + destruct (eval_condition c vl); try discriminate. destruct b0; inv H7; inversion H1; congruence. assert (eval_condexpr ge sp e m le (CEcond c e0) b). eapply eval_CEcond; eauto. @@ -1119,7 +1131,7 @@ Lemma eval_sel_binop: forall le op a1 a2 v1 v2 v, eval_expr ge sp e m le a1 v1 -> eval_expr ge sp e m le a2 v2 -> - eval_binop op v1 v2 m = Some v -> + eval_binop op v1 v2 = Some v -> eval_expr ge sp e m le (sel_binop op a1 a2) v. Proof. destruct op; simpl; intros; FuncInv; try subst v. @@ -1154,12 +1166,9 @@ Proof. apply eval_comp_int; auto. eapply eval_comp_int_ptr; eauto. eapply eval_comp_ptr_int; eauto. - generalize H1; clear H1. - case_eq (valid_pointer m b (Int.signed i) && valid_pointer m b0 (Int.signed i0)); intros. - destruct (eq_block b b0); inv H2. + destruct (eq_block b b0); inv H1. eapply eval_comp_ptr_ptr; eauto. eapply eval_comp_ptr_ptr_2; eauto. - discriminate. eapply eval_compu; eauto. eapply eval_compf; eauto. Qed. @@ -1340,10 +1349,6 @@ Proof. apply functions_translated; eauto. apply sig_function_translated. constructor; auto. apply call_cont_commut. - (* Salloc *) - exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id (Vptr b Int.zero) e) m'); split. - econstructor; eauto with evalexpr. - constructor; auto. (* Sifthenelse *) exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split. constructor. eapply eval_condition_of_expr; eauto with evalexpr. diff --git a/powerpc/eabi/Conventions.v b/powerpc/eabi/Conventions.v index 6e27b9d2..90e14a0a 100644 --- a/powerpc/eabi/Conventions.v +++ b/powerpc/eabi/Conventions.v @@ -792,7 +792,3 @@ Proof. intros; simpl. tauto. Qed. -(** ** Location of argument and result for dynamic memory allocation *) - -Definition loc_alloc_argument := R3. -Definition loc_alloc_result := R3. diff --git a/powerpc/macosx/Conventions.v b/powerpc/macosx/Conventions.v index 4f06b415..6d1ccb13 100644 --- a/powerpc/macosx/Conventions.v +++ b/powerpc/macosx/Conventions.v @@ -799,7 +799,3 @@ Proof. intros; simpl. tauto. Qed. -(** ** Location of argument and result for dynamic memory allocation *) - -Definition loc_alloc_argument := R3. -Definition loc_alloc_result := R3. |