diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 11:57:02 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 11:57:02 +0000 |
| commit | bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc (patch) | |
| tree | 3efa5cb51e9bb3edc935f42dbd630fce9a170804 | |
| parent | cd2449aabe7b259b0fdb8aaa2af65c2b8957ab32 (diff) | |
| download | compcert-kvx-bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc.tar.gz compcert-kvx-bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc.zip | |
- Added alignment constraints to memory loads and stores.
- In Cminor and below, removed pointer validity check in semantics of
comparisons, so that evaluation of expressions is independent of
memory state.
- In Cminor and below, removed "alloc" instruction.
- Cleaned up commented-away parts.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
67 files changed, 719 insertions, 1488 deletions
@@ -145,7 +145,6 @@ Inductive instruction : Set := | Psufd: freg -> freg -> freg -> instruction (**r float subtraction *) (* Pseudo-instructions *) - | Pallocblock: instruction (**r dynamic allocation *) | Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *) | Pfreeframe: int -> instruction (**r deallocate stack frame and restore previous frame *) | Plabel: label -> instruction (**r define a code label *) @@ -232,11 +231,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. @@ -538,14 +532,6 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Psufd r1 r2 r3 => OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m (* Pseudo-instructions *) - | Pallocblock => - match rs#IR0 with - | Vint n => - let (m', b) := Mem.alloc m 0 (Int.signed n) in - OK (nextinstr (rs#IR0 <- (Vptr b Int.zero) - #IR14 <- (Val.add rs#PC Vone))) m' - | _ => Error - end | Pallocframe lo hi pos => let (m1, stk) := Mem.alloc m lo hi in let sp := (Vptr stk (Int.repr lo)) in diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 5e21e14e..7e40949a 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -477,8 +477,6 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := | Mtailcall sig (inr symb) => loadind_int IR13 f.(fn_retaddr_ofs) IR14 (Pfreeframe f.(fn_link_ofs) :: Pbsymb symb :: k) - | Malloc => - Pallocblock :: k | Mlabel lbl => Plabel lbl :: k | Mgoto lbl => diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 69a82dea..f9f4cd0f 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -523,50 +523,6 @@ Proof. intros. apply Pregmap.gso; auto. Qed. -(** * Memory properties *) - -(** We show that signed 8- and 16-bit stores can be performed - like unsigned stores. *) - -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 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 @@ -767,7 +723,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. @@ -940,21 +896,6 @@ Proof. intros. rewrite Pregmap.gso; auto. 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) @@ -984,7 +925,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 @@ -1020,7 +961,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. @@ -1197,7 +1138,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/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 32fedf31..b18ae914 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -431,60 +431,6 @@ Qed. (** * Correctness of ARM constructor functions *) -(** Properties of comparisons. *) -(* -Lemma compare_float_spec: - forall rs v1 v2, - let rs1 := nextinstr (compare_float rs v1 v2) in - rs1#CR0_0 = Val.cmpf Clt v1 v2 - /\ rs1#CR0_1 = Val.cmpf Cgt v1 v2 - /\ rs1#CR0_2 = Val.cmpf Ceq v1 v2 - /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> - r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. -Proof. - intros. unfold rs1. - split. reflexivity. - split. reflexivity. - split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_float. repeat (rewrite Pregmap.gso; auto). -Qed. - -Lemma compare_sint_spec: - forall rs v1 v2, - let rs1 := nextinstr (compare_sint rs v1 v2) in - rs1#CR0_0 = Val.cmp Clt v1 v2 - /\ rs1#CR0_1 = Val.cmp Cgt v1 v2 - /\ rs1#CR0_2 = Val.cmp Ceq v1 v2 - /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> - r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. -Proof. - intros. unfold rs1. - split. reflexivity. - split. reflexivity. - split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_sint. repeat (rewrite Pregmap.gso; auto). -Qed. - -Lemma compare_uint_spec: - forall rs v1 v2, - let rs1 := nextinstr (compare_uint rs v1 v2) in - rs1#CR0_0 = Val.cmpu Clt v1 v2 - /\ rs1#CR0_1 = Val.cmpu Cgt v1 v2 - /\ rs1#CR0_2 = Val.cmpu Ceq v1 v2 - /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> - r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. -Proof. - intros. unfold rs1. - split. reflexivity. - split. reflexivity. - split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_uint. repeat (rewrite Pregmap.gso; auto). -Qed. -*) - (** Loading a constant. *) Lemma loadimm_correct: @@ -868,14 +814,14 @@ 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'#(CR (crbit_for_cond cond)) = Val.of_bool b /\ agree ms sp rs'. Proof. intros. - rewrite <- (eval_condition_weaken _ _ _ H1). clear H1. + rewrite <- (eval_condition_weaken _ _ H1). clear H1. destruct cond; simpl in H; TypeInv; simpl. (* Ccomp *) generalize (compare_int_spec rs ms#m0 ms#m1). @@ -1008,12 +954,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))). @@ -1036,29 +982,6 @@ Proof. intros [rs' [A [B C]]]. exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto. -(* - (* Ofloatconst *) - exists (nextinstr (rs#(freg_of res) <- (Vfloat f))). - split. apply exec_straight_one. reflexivity. reflexivity. - auto with ppcgen. - (* Oaddrsymbol *) - change (find_symbol_offset ge i i0) with (symbol_offset ge i i0). - set (v := symbol_offset ge i i0). - pose (rs1 := nextinstr (rs#GPR2 <- (high_half v))). - exists (nextinstr (rs1#(ireg_of res) <- v)). - split. apply exec_straight_two with rs1 m. - unfold exec_instr. rewrite gpr_or_zero_zero. - unfold const_high. rewrite Val.add_commut. - rewrite high_half_zero. reflexivity. - simpl. rewrite gpr_or_zero_not_zero. 2: congruence. - unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gss. - fold v. rewrite Val.add_commut. unfold v. rewrite low_high_half. - reflexivity. reflexivity. reflexivity. - unfold rs1. apply agree_nextinstr. apply agree_set_mireg; auto. - apply agree_set_mreg. apply agree_nextinstr. - apply agree_set_other. auto. simpl. tauto. -*) (* Oaddrstack *) generalize (addimm_correct (ireg_of res) IR13 i k rs m). intros [rs' [EX [RES OTH]]]. @@ -1239,13 +1162,13 @@ Proof. repeat (rewrite (ireg_val ms sp rs); auto). reflexivity. auto 10 with ppcgen. (* Ocmp *) - assert (exists b, eval_condition c ms##args m = Some b /\ v = Val.of_bool b). - simpl in H1. destruct (eval_condition c ms##args m). + assert (exists b, eval_condition c ms##args = Some b /\ v = Val.of_bool b). + simpl in H1. destruct (eval_condition c ms##args). destruct b; inv H1. exists true; auto. exists false; auto. discriminate. destruct H5 as [b [EVC EQ]]. exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. - rewrite (eval_condition_weaken _ _ _ EVC). + rewrite (eval_condition_weaken _ _ EVC). set (rs1 := nextinstr (rs'#(ireg_of res) <- (Vint Int.zero))). set (rs2 := nextinstr (if b then (rs1#(ireg_of res) <- Vtrue) else rs1)). exists rs2; split. @@ -1477,31 +1400,5 @@ Proof. auto with ppcgen. 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#IR0 <- (Vptr blk Int.zero) #IR14 <- (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 IR0) with (preg_of Conventions.loc_alloc_result). - apply agree_set_mreg. auto. - simpl. tauto. -Qed. - End STRAIGHTLINE. diff --git a/arm/Constprop.v b/arm/Constprop.v index 7369012c..b51d974e 100644 --- a/arm/Constprop.v +++ b/arm/Constprop.v @@ -686,8 +686,6 @@ 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 => @@ -1206,8 +1204,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/arm/Constpropproof.v b/arm/Constpropproof.v index e85cadfe..7c7b8788 100644 --- a/arm/Constpropproof.v +++ b/arm/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. @@ -197,7 +197,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. @@ -270,9 +270,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. @@ -304,10 +304,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. @@ -317,10 +317,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. @@ -331,10 +331,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. @@ -345,10 +345,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. @@ -359,11 +359,11 @@ Proof. Qed. Lemma make_mulimm_correct: - forall n r r' m v, + forall n r r' v, rs#r' = Vint n -> let (op, args) := make_mulimm n r 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. @@ -371,8 +371,8 @@ Proof. generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros. subst n. simpl in H2. simpl. FuncInv. rewrite Int.mul_one in H1. 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 _ _ H2). change (Z_of_nat wordsize) with 32. intro. rewrite H3. @@ -381,10 +381,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. @@ -395,10 +395,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. @@ -409,10 +409,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. @@ -423,18 +423,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. @@ -443,8 +443,8 @@ Proof. (* Oaddshift *) caseEq (intval approx r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil) m) - with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil) m). + replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil)) + with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil)). apply make_addimm_correct. simpl. destruct rs#r1; auto. assumption. @@ -454,16 +454,16 @@ Proof. simpl in *. destruct rs#r2; auto. 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. (* Osubshift *) caseEq (intval approx r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil) m) - with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil) m). + replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil)) + with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil)). apply make_addimm_correct. simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. assumption. @@ -475,8 +475,8 @@ Proof. (* 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. apply intval_correct; auto. simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto. caseEq (intval approx r2); intros. @@ -487,8 +487,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). @@ -501,8 +501,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. @@ -511,15 +511,15 @@ Proof. (* Oandshift *) caseEq (intval approx r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil) m) - with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil) m). + replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil)) + with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil)). apply make_andimm_correct. reflexivity. assumption. (* 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. @@ -528,15 +528,15 @@ Proof. (* Oorshift *) caseEq (intval approx r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil) m) - with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil) m). + replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil)) + with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil)). apply make_orimm_correct. reflexivity. assumption. (* 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. @@ -545,22 +545,22 @@ Proof. (* Oxorshift *) caseEq (intval approx r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil) m) - with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil) m). + replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil)) + with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil)). apply make_xorimm_correct. reflexivity. assumption. (* Obic *) caseEq (intval approx r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil) m) - with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil) m). + replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil)) + with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil)). apply make_andimm_correct. reflexivity. assumption. (* Obicshift *) caseEq (intval approx r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil) m) - with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil) m). + replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil)) + with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil)). apply make_andimm_correct. reflexivity. assumption. (* Oshl *) @@ -779,13 +779,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; @@ -852,30 +852,20 @@ Proof. TransfInstr; intro. econstructor; split. 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. + constructor; 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. @@ -888,14 +878,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. @@ -165,9 +165,7 @@ Definition eval_compare_mismatch (c: comparison) : option bool := match c with Ceq => Some false | Cne => Some true | _ => None end. Definition eval_compare_null (c: comparison) (n: int) : option bool := - if Int.eq n Int.zero - then match c with Ceq => Some false | Cne => Some true | _ => None end - else None. + if Int.eq n Int.zero then eval_compare_mismatch c else None. Definition eval_shift (s: shift) (n: int) : int := match s with @@ -177,18 +175,15 @@ Definition eval_shift (s: shift) (n: int) : int := | Sror x => Int.ror n (s_amount x) end. -Definition eval_condition (cond: condition) (vl: list val) (m: mem): +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 => eval_compare_null c n2 | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil => @@ -223,7 +218,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) @@ -297,7 +292,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 @@ -358,20 +353,17 @@ Proof. 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. apply eval_negate_compare_null; auto. apply eval_negate_compare_null; auto. - destruct (valid_pointer m b0 (Int.signed i) && - valid_pointer m b1 (Int.signed i0)). destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence. destruct c; simpl in H; inv H; auto. - discriminate. rewrite Int.negate_cmpu. auto. rewrite Int.negate_cmp. auto. apply eval_negate_compare_null; auto. @@ -397,8 +389,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; @@ -418,74 +410,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 @@ -603,9 +527,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. @@ -771,25 +695,22 @@ Proof. 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); try congruence. apply eval_compare_mismatch_weaken; auto. - discriminate. 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. @@ -810,7 +731,7 @@ Proof. unfold Int.ltu. rewrite zlt_true. congruence. assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto. omega. discriminate. - 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. @@ -855,8 +776,6 @@ 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 @@ -876,15 +795,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 := @@ -897,8 +811,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. @@ -918,7 +832,7 @@ Proof. destruct (Int.ltu i0 (Int.repr 32)); inv H1; TrivialExists. destruct (Int.ltu i (Int.repr 31)); 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. @@ -986,10 +900,10 @@ Definition op_for_binary_addressing (addr: addressing) : operation := end. 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; simpl. diff --git a/arm/Selection.v b/arm/Selection.v index 1b5411b1..d04a4ca3 100644 --- a/arm/Selection.v +++ b/arm/Selection.v @@ -1359,7 +1359,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/arm/Selectionproof.v b/arm/Selectionproof.v index a307597a..10f93f3a 100644 --- a/arm/Selectionproof.v +++ b/arm/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 @@ -229,12 +229,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. @@ -591,9 +591,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) -> @@ -912,15 +912,12 @@ 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. simpl. - subst y1. rewrite dec_eq_true. + EvalOp. simpl. subst y1. rewrite dec_eq_true. destruct (Int.cmp c x2 y2); reflexivity. Qed. @@ -928,16 +925,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. @@ -1021,7 +1016,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. @@ -1041,7 +1036,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). @@ -1069,8 +1064,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. @@ -1195,7 +1190,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. @@ -1231,12 +1226,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. @@ -1417,10 +1409,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/arm/linux/Conventions.v b/arm/linux/Conventions.v index 03425213..a35162c2 100644 --- a/arm/linux/Conventions.v +++ b/arm/linux/Conventions.v @@ -852,7 +852,3 @@ Proof. intros; simpl. tauto. Qed. -(** ** Location of argument and result for dynamic memory allocation *) - -Definition loc_alloc_argument := R0. -Definition loc_alloc_result := R0. diff --git a/backend/Allocation.v b/backend/Allocation.v index 3a5960be..2389a331 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -101,8 +101,6 @@ Definition transfer (reg_sum_live ros (reg_dead res after)) | Itailcall sig ros args => reg_list_live args (reg_sum_live ros Regset.empty) - | Ialloc arg res s => - reg_live arg (reg_dead res after) | Icond cond args ifso ifnot => reg_list_live args after | Ireturn optarg => @@ -167,8 +165,6 @@ Definition transf_instr (assign res) s | Itailcall sig ros args => Ltailcall sig (sum_left_map assign ros) (List.map assign args) - | Ialloc arg res s => - Lalloc (assign arg) (assign res) s | Icond cond args ifso ifnot => Lcond cond (List.map assign args) ifso ifnot | Ireturn optarg => diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 5e389349..3971fb6d 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -601,7 +601,7 @@ Proof. rewrite <- H1. eapply agree_move_live; eauto. (* Not a move *) intros INMO CORR CODE. - assert (eval_operation tge sp op (map ls (map assign args)) m = Some v). + assert (eval_operation tge sp op (map ls (map assign args)) = Some v). replace (map ls (map assign args)) with (rs##args). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. eapply agree_eval_regs; eauto. @@ -671,25 +671,15 @@ Proof. rewrite (sig_function_translated _ _ TF). eauto. rewrite H1. econstructor; eauto. - (* Ialloc *) - assert (ls (assign arg) = Vint sz). - rewrite <- H0. symmetry. eapply agree_eval_reg; eauto. - econstructor; split. - eapply exec_Lalloc; eauto. TranslInstr. - generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). - unfold correct_alloc_instr. intros [CORR1 CORR2]. - MatchStates. - eapply agree_postcall with (args := arg :: nil) (ros := inr reg 1%positive); eauto. - (* Icond, true *) - assert (COND: eval_condition cond (map ls (map assign args)) m = Some true). + assert (COND: eval_condition cond (map ls (map assign args)) = Some true). replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Lcond_true; eauto. TranslInstr. MatchStates. eapply agree_reg_list_live. eauto. (* Icond, false *) - assert (COND: eval_condition cond (map ls (map assign args)) m = Some false). + assert (COND: eval_condition cond (map ls (map assign args)) = Some false). replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index d9ab17b0..aba96601 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -139,8 +139,6 @@ Proof. split. autorewrite with allocty; auto. split. auto with allocty. auto. rewrite transf_unroll; auto. - (* alloc *) - WT. (* cond *) WT. (* return *) diff --git a/backend/Bounds.v b/backend/Bounds.v index e5982450..d1ed28d5 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -26,8 +26,7 @@ Require Import Conventions. (** The [bounds] record capture how many local and outgoing stack slots and callee-save registers are used by a function. *) -(** We demand that all bounds are positive or null, - and moreover [bound_outgoing] is greater or equal to 6. +(** We demand that all bounds are positive or null. These properties are used later to reason about the layout of the activation record. *) @@ -104,7 +103,6 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil - | Lalloc => nil | Llabel lbl => nil | Lgoto lbl => nil | Lcond cond args lbl => nil diff --git a/backend/CSE.v b/backend/CSE.v index 49b84899..13e9be8e 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -260,7 +260,7 @@ Definition equation_holds (vres: valnum) (rh: rhs) : Prop := match rh with | Op op vl => - eval_operation ge sp op (List.map valuation vl) m = + eval_operation ge sp op (List.map valuation vl) = Some (valuation vres) | Load chunk addr vl => exists a, @@ -348,8 +348,6 @@ Definition transfer (f: function) (pc: node) (before: numbering) := empty_numbering | Itailcall sig ros args => empty_numbering - | Ialloc arg res s => - add_unknown before res | Icond cond args ifso ifnot => before | Ireturn optarg => diff --git a/backend/CSEproof.v b/backend/CSEproof.v index a87cd758..265bb20a 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -232,7 +232,7 @@ Proof. apply wf_kill_loads; auto. apply wf_empty_numbering. apply wf_empty_numbering. - apply wf_add_unknown; auto. +(* apply wf_add_unknown; auto. *) Qed. (** As a consequence, the numberings computed by the static analysis @@ -401,7 +401,7 @@ Definition rhs_evals_to (valu: valnum -> val) (rh: rhs) (v: val) : Prop := match rh with | Op op vl => - eval_operation ge sp op (List.map valu vl) m = Some v + eval_operation ge sp op (List.map valu vl) = Some v | Load chunk addr vl => exists a, eval_addressing ge sp addr (List.map valu vl) = Some a /\ @@ -482,7 +482,7 @@ Lemma add_op_satisfiable: forall n rs op args dst v, wf_numbering n -> numbering_satisfiable ge sp rs m n -> - eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op rs##args = Some v -> numbering_satisfiable ge sp (rs#dst <- v) m (add_op n dst op args). Proof. intros. inversion H0. @@ -559,7 +559,7 @@ Proof. intros. destruct H0 as [valu [A B]]. exists valu; split; intros. generalize (A _ _ H0). destruct rh; simpl. - intro. eapply eval_operation_alloc; eauto. + auto. intros [addr [C D]]. exists addr; split. auto. destruct addr; simpl in *; try discriminate. eapply Mem.load_alloc_other; eauto. @@ -595,7 +595,7 @@ Proof. generalize (kill_load_eqs_ops _ _ _ H5). destruct rh; simpl. intros. destruct addr; simpl in H; try discriminate. - eapply eval_operation_store; eauto. + auto. tauto. apply H3. assumption. Qed. @@ -651,7 +651,7 @@ Lemma find_op_correct: wf_numbering n -> numbering_satisfiable ge sp rs m n -> find_op n op args = Some r -> - eval_operation ge sp op rs##args m = Some rs#r. + eval_operation ge sp op rs##args = Some rs#r. Proof. intros until r. intros WF [valu NH]. unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND. @@ -841,14 +841,14 @@ Proof. (* Iop *) exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. - assert (eval_operation tge sp op rs##args m = Some v). + assert (eval_operation tge sp op rs##args = Some v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. generalize C; clear C. case (is_trivial_op op). intro. eapply exec_Iop'; eauto. caseEq (find_op (analyze f)!!pc op args). intros r FIND CODE. eapply exec_Iop'; eauto. simpl. - assert (eval_operation ge sp op rs##args m = Some rs#r). + assert (eval_operation ge sp op rs##args = Some rs#r). eapply find_op_correct; eauto. eapply wf_analyze; eauto. congruence. @@ -910,16 +910,6 @@ Proof. apply sig_preserved. econstructor; eauto. - (* Ialloc *) - 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 analysis_correct_1 with pc. - unfold successors; rewrite H; auto with coqlib. - unfold transfer; rewrite H. - apply add_unknown_satisfiable. apply wf_analyze; auto. - eapply alloc_satisfiable; eauto. - (* Icond true *) econstructor; split. eapply exec_Icond_true; eauto. diff --git a/backend/Cminor.v b/backend/Cminor.v index 16f7c3df..35bf3916 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -103,7 +103,6 @@ Inductive stmt : Set := | Sstore : memory_chunk -> expr -> expr -> stmt | Scall : option ident -> signature -> expr -> list expr -> stmt | Stailcall: signature -> expr -> list expr -> stmt - | Salloc : ident -> expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: expr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -251,8 +250,11 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := Definition eval_compare_mismatch (c: comparison) : option val := match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end. +Definition eval_compare_null (c: comparison) (n: int) : option val := + if Int.eq n Int.zero then eval_compare_mismatch c else None. + Definition eval_binop - (op: binary_operation) (arg1 arg2: val) (m: mem): option val := + (op: binary_operation) (arg1 arg2: val): option val := match op, arg1, arg2 with | Oadd, Vint n1, Vint n2 => Some (Vint (Int.add n1 n2)) | Oadd, Vint n1, Vptr b2 n2 => Some (Vptr b2 (Int.add n2 n1)) @@ -286,17 +288,13 @@ Definition eval_binop | Ocmp c, Vint n1, Vint n2 => Some (Val.of_bool(Int.cmp c n1 n2)) | Ocmp c, Vptr b1 n1, Vptr b2 n2 => - if valid_pointer m b1 (Int.signed n1) - && valid_pointer m b2 (Int.signed n2) then - if eq_block b1 b2 - then Some(Val.of_bool(Int.cmp c n1 n2)) - else eval_compare_mismatch c - else - None + if eq_block b1 b2 + then Some(Val.of_bool(Int.cmp c n1 n2)) + else eval_compare_mismatch c | Ocmp c, Vptr b1 n1, Vint n2 => - if Int.eq n2 Int.zero then eval_compare_mismatch c else None + eval_compare_null c n2 | Ocmp c, Vint n1, Vptr b2 n2 => - if Int.eq n1 Int.zero then eval_compare_mismatch c else None + eval_compare_null c n1 | Ocmpu c, Vint n1, Vint n2 => Some (Val.of_bool(Int.cmpu c n1 n2)) | Ocmpf c, Vfloat f1, Vfloat f2 => @@ -332,7 +330,7 @@ Inductive eval_expr: expr -> val -> Prop := | eval_Ebinop: forall op a1 a2 v1 v2 v, eval_expr a1 v1 -> eval_expr a2 v2 -> - eval_binop op v1 v2 m = Some v -> + eval_binop op v1 v2 = Some v -> eval_expr (Ebinop op a1 a2) v | eval_Eload: forall chunk addr vaddr v, eval_expr addr vaddr -> @@ -438,12 +436,6 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) (Mem.free m sp)) - | step_alloc: forall f id a k sp e m n m' b, - eval_expr sp e m a (Vint n) -> - Mem.alloc m 0 (Int.signed n) = (m', b) -> - step (State f (Salloc id a) k sp e m) - E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m') - | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) @@ -633,12 +625,6 @@ with exec_stmt: eval_funcall m f vargs t m' vres -> e' = set_optvar optid vres e -> exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal - | exec_Salloc: - forall sp e m id a n m' b, - eval_expr ge sp e m a (Vint n) -> - Mem.alloc m 0 (Int.signed n) = (m', b) -> - exec_stmt sp e m (Salloc id a) - E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal | exec_Sifthenelse: forall sp e m a s1 s2 v b t e' m' out, eval_expr ge sp e m a v -> @@ -805,10 +791,10 @@ Definition eval_funcall_exec_stmt_ind2 (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop) (P2: val -> env -> mem -> stmt -> trace -> env -> mem -> outcome -> Prop) := - fun a b c d e f g h i j k l m n o p q r => + fun a b c d e f g h i j k l m n o p q => conj - (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r) - (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r ). + (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q) + (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q). Inductive outcome_state_match (sp: val) (e: env) (m: mem) (f: function) (k: cont): @@ -918,11 +904,6 @@ Proof. constructor. reflexivity. traceEq. subst e'. constructor. -(* alloc *) - exists (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m'); split. - apply star_one. econstructor; eauto. - constructor. - (* ifthenelse *) destruct (H2 f k) as [S [A B]]. exists S; split. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 1d5c8c05..bfe92a40 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -68,7 +68,6 @@ Inductive stmt : Set := | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt | Scall : option ident -> signature -> expr -> exprlist -> stmt | Stailcall: signature -> expr -> exprlist -> stmt - | Salloc : ident -> expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -162,7 +161,7 @@ Inductive eval_expr: letenv -> expr -> val -> Prop := eval_expr le (Evar id) v | eval_Eop: forall le op al vl v, eval_exprlist le al vl -> - eval_operation ge sp op vl m = Some v -> + eval_operation ge sp op vl = Some v -> eval_expr le (Eop op al) v | eval_Eload: forall le chunk addr al vl vaddr v, eval_exprlist le al vl -> @@ -188,7 +187,7 @@ with eval_condexpr: letenv -> condexpr -> bool -> Prop := eval_condexpr le CEfalse false | eval_CEcond: forall le cond al vl b, eval_exprlist le al vl -> - eval_condition cond vl m = Some b -> + eval_condition cond vl = Some b -> eval_condexpr le (CEcond cond al) b | eval_CEcondition: forall le a b c vb1 vb2, eval_condexpr le a vb1 -> @@ -294,12 +293,6 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) (Mem.free m sp)) - | step_alloc: forall f id a k sp e m n m' b, - eval_expr sp e m nil a (Vint n) -> - Mem.alloc m 0 (Int.signed n) = (m', b) -> - step (State f (Salloc id a) k sp e m) - E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m') - | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) diff --git a/backend/Coloring.v b/backend/Coloring.v index 056aaa51..7204bc79 100644 --- a/backend/Coloring.v +++ b/backend/Coloring.v @@ -183,12 +183,6 @@ Definition add_edges_instr let largs := loc_arguments sig in add_prefs_call args largs (add_interf_call ros largs g) - | Ialloc arg res s => - add_pref_mreg arg loc_alloc_argument - (add_pref_mreg res loc_alloc_result - (add_interf_op res live - (add_interf_destroyed - (Regset.remove res live) destroyed_at_call_regs g))) | Ireturn (Some r) => add_pref_mreg r (loc_result sig) g | _ => g diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index ea31a29e..c86652a3 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -384,10 +384,6 @@ Proof. apply add_interf_destroyed_incl. eapply graph_incl_trans; [idtac|apply add_prefs_call_incl]. apply add_interfs_call_incl. - eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. - eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. - eapply graph_incl_trans; [idtac|apply add_interf_op_incl]. - apply add_interf_destroyed_incl. destruct o. apply add_pref_mreg_incl. apply graph_incl_refl. @@ -437,15 +433,6 @@ Definition correct_interf_instr interfere_mreg rfun mr g | inr idfun => True end - | Ialloc arg res s => - (forall r mr, - Regset.In r live -> - In mr destroyed_at_call_regs -> - r <> res -> - interfere_mreg r mr g) - /\ (forall r, - Regset.In r live -> - r <> res -> interfere r res g) | _ => True end. @@ -467,9 +454,6 @@ Proof. split. intros. eapply interfere_incl; eauto. destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. - intros [A B]. split. - intros. eapply interfere_mreg_incl; eauto. - intros. eapply interfere_incl; eauto. Qed. Lemma add_edges_instr_correct: @@ -516,20 +500,6 @@ Proof. eapply interfere_mreg_incl. apply add_prefs_call_incl. apply add_interfs_call_correct. auto. - - (* Ialloc *) - split; intros. - apply interfere_mreg_incl with - (add_interf_destroyed (Regset.remove r0 live) destroyed_at_call_regs g). - eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. - eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. - apply add_interf_op_incl. - apply add_interf_destroyed_correct; auto. - apply Regset.remove_2; auto. - - eapply interfere_incl. - eapply graph_incl_trans; apply add_pref_mreg_incl. - apply add_interf_op_correct; auto. Qed. Lemma add_edges_instrs_incl_aux: @@ -826,14 +796,6 @@ Definition correct_alloc_instr | inl rfun => ~(In (alloc rfun) (loc_arguments sig)) | inr idfun => True end) - | Ialloc arg res s => - (forall r, - Regset.In r live!!pc -> - r <> res -> - ~(In (alloc r) Conventions.destroyed_at_call)) - /\ (forall r, - Regset.In r live!!pc -> - r <> res -> alloc r <> alloc res) | _ => True end. @@ -927,15 +889,6 @@ Proof. caseEq (alloc r). intros. elim (ALL2 r m). apply H; auto. congruence. auto. destruct s0; auto. - (* Ialloc *) - intros [A B]. split. - intros; red; intros. - unfold destroyed_at_call in H1. - generalize (list_in_map_inv R _ _ H1). - intros [mr [EQ IN]]. - generalize (A r1 mr H IN H0). intro. - generalize (ALL2 _ _ H2). contradiction. - auto. Qed. Lemma regalloc_correct_1: diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index c9891c27..433c074d 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -52,12 +52,6 @@ Module OrderedRegReg := OrderedPair(OrderedReg)(OrderedReg). Module OrderedMreg := OrderedIndexed(IndexedMreg). Module OrderedRegMreg := OrderedPair(OrderedReg)(OrderedMreg). -(* -Module SetDepRegReg := FSetAVL.Make(OrderedRegReg). -Module SetRegReg := NodepOfDep(SetDepRegReg). -Module SetDepRegMreg := FSetAVL.Make(OrderedRegMreg). -Module SetRegMreg := NodepOfDep(SetDepRegMreg). -*) Module SetRegReg := FSetAVL.Make(OrderedRegReg). Module SetRegMreg := FSetAVL.Make(OrderedRegMreg). @@ -226,16 +220,6 @@ Definition all_interf_regs (g: graph) : Regset.t := g.(interf_reg_mreg) Regset.empty). -(* -Lemma mem_add_tail: - forall r r' u, - Regset.mem r u = true -> Regset.mem r (Regset.add r' u) = true. -Proof. - intros. case (Reg.eq r r'); intro. - subst r'. apply Regset.mem_add_same. - rewrite Regset.mem_add_other; auto. -Qed. -*) Lemma in_setregreg_fold: forall g r1 r2 u, SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u -> diff --git a/backend/LTL.v b/backend/LTL.v index 6ee07f73..0db5495e 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -41,7 +41,6 @@ Inductive instruction: Set := | Lstore: memory_chunk -> addressing -> list loc -> loc -> node -> instruction | Lcall: signature -> loc + ident -> list loc -> loc -> node -> instruction | Ltailcall: signature -> loc + ident -> list loc -> instruction - | Lalloc: loc -> loc -> node -> instruction | Lcond: condition -> list loc -> node -> node -> instruction | Lreturn: option loc -> instruction. @@ -165,7 +164,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_Lop: forall s f sp pc rs m op args res pc' v, (fn_code f)!pc = Some(Lop op args res pc') -> - eval_operation ge sp op (map rs args) m = Some v -> + eval_operation ge sp op (map rs args) = Some v -> step (State s f sp pc rs m) E0 (State s f sp pc' (Locmap.set res v rs) m) | exec_Lload: @@ -197,23 +196,16 @@ Inductive step: state -> trace -> state -> Prop := funsig f' = sig -> step (State s f (Vptr stk Int.zero) pc rs m) E0 (Callstate s f' (List.map rs args) (Mem.free m stk)) - | exec_Lalloc: - forall s f sp pc rs m pc' arg res sz m' b, - (fn_code f)!pc = Some(Lalloc arg res pc') -> - rs arg = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', b) -> - step (State s f sp pc rs m) - E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_locs rs)) m') | exec_Lcond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> - eval_condition cond (map rs args) m = Some true -> + eval_condition cond (map rs args) = Some true -> step (State s f sp pc rs m) E0 (State s f sp ifso rs m) | exec_Lcond_false: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> - eval_condition cond (map rs args) m = Some false -> + eval_condition cond (map rs args) = Some false -> step (State s f sp pc rs m) E0 (State s f sp ifnot rs m) | exec_Lreturn: @@ -275,7 +267,6 @@ Definition successors (f: function) (pc: node) : list node := | Lstore chunk addr args src s => s :: nil | Lcall sig ros args res s => s :: nil | Ltailcall sig ros args => nil - | Lalloc arg res s => s :: nil | Lcond cond args ifso ifnot => ifso :: ifnot :: nil | Lreturn optarg => nil end diff --git a/backend/LTLin.v b/backend/LTLin.v index fae64177..4c87c0d6 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -47,7 +47,6 @@ Inductive instruction: Set := | Lstore: memory_chunk -> addressing -> list loc -> loc -> instruction | Lcall: signature -> loc + ident -> list loc -> loc -> instruction | Ltailcall: signature -> loc + ident -> list loc -> instruction - | Lalloc: loc -> loc -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list loc -> label -> instruction @@ -157,7 +156,7 @@ Definition find_function (ros: loc + ident) (rs: locset) : option fundef := Inductive step: state -> trace -> state -> Prop := | exec_Lop: forall s f sp op args res b rs m v, - eval_operation ge sp op (map rs args) m = Some v -> + eval_operation ge sp op (map rs args) = Some v -> step (State s f sp (Lop op args res :: b) rs m) E0 (State s f sp b (Locmap.set res v rs) m) | exec_Lload: @@ -185,12 +184,6 @@ Inductive step: state -> trace -> state -> Prop := sig = funsig f' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m) E0 (Callstate s f' (List.map rs args) (Mem.free m stk)) - | exec_Lalloc: - forall s f sp arg res b rs m sz m' blk, - rs arg = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - step (State s f sp (Lalloc arg res :: b) rs m) - E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_locs rs)) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -202,13 +195,13 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp b' rs m) | exec_Lcond_true: forall s f sp cond args lbl b rs m b', - eval_condition cond (map rs args) m = Some true -> + eval_condition cond (map rs args) = Some true -> find_label lbl f.(fn_code) = Some b' -> step (State s f sp (Lcond cond args lbl :: b) rs m) E0 (State s f sp b' rs m) | exec_Lcond_false: forall s f sp cond args lbl b rs m, - eval_condition cond (map rs args) m = Some false -> + eval_condition cond (map rs args) = Some false -> step (State s f sp (Lcond cond args lbl :: b) rs m) E0 (State s f sp b rs m) | exec_Lreturn: diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 26ec066d..9f3f5896 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -67,11 +67,6 @@ Inductive wt_instr : instruction -> Prop := sig.(sig_res) = funsig.(sig_res) -> Conventions.tailcall_possible sig -> wt_instr (Ltailcall sig ros args) - | wt_Lalloc: - forall arg res, - Loc.type arg = Tint -> Loc.type res = Tint -> - loc_acceptable arg -> loc_acceptable res -> - wt_instr (Lalloc arg res) | wt_Llabel: forall lbl, wt_instr (Llabel lbl) | wt_Lgoto: forall lbl, diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 950154a1..0461c9af 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -88,12 +88,6 @@ Inductive wt_instr : instruction -> Prop := sig.(sig_res) = funct.(fn_sig).(sig_res) -> Conventions.tailcall_possible sig -> wt_instr (Ltailcall sig ros args) - | wt_Lalloc: - forall arg res s, - Loc.type arg = Tint -> Loc.type res = Tint -> - loc_acceptable arg -> loc_acceptable res -> - valid_successor s -> - wt_instr (Lalloc arg res s) | wt_Lcond: forall cond args s1 s2, List.map Loc.type args = type_of_condition cond -> diff --git a/backend/Linear.v b/backend/Linear.v index 629dcc53..34d6e5ce 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -43,7 +43,6 @@ Inductive instruction: Set := | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Lcall: signature -> mreg + ident -> instruction | Ltailcall: signature -> mreg + ident -> instruction - | Lalloc: instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list mreg -> label -> instruction @@ -247,7 +246,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp b (Locmap.set (S sl) (rs (R r)) rs) m) | exec_Lop: forall s f sp op args res b rs m v, - eval_operation ge sp op (reglist rs args) m = Some v -> + eval_operation ge sp op (reglist rs args) = Some v -> step (State s f sp (Lop op args res :: b) rs m) E0 (State s f sp b (Locmap.set (R res) v rs) m) | exec_Lload: @@ -274,15 +273,6 @@ Inductive step: state -> trace -> state -> Prop := sig = funsig f' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m) E0 (Callstate s f' (return_regs (parent_locset s) rs) (Mem.free m stk)) - | exec_Lalloc: - forall s f sp b rs m sz m' blk, - rs (R Conventions.loc_alloc_argument) = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - step (State s f sp (Lalloc :: b) rs m) - E0 (State s f sp b - (Locmap.set (R Conventions.loc_alloc_result) - (Vptr blk Int.zero) rs) - m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -294,13 +284,13 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp b' rs m) | exec_Lcond_true: forall s f sp cond args lbl b rs m b', - eval_condition cond (reglist rs args) m = Some true -> + eval_condition cond (reglist rs args) = Some true -> find_label lbl f.(fn_code) = Some b' -> step (State s f sp (Lcond cond args lbl :: b) rs m) E0 (State s f sp b' rs m) | exec_Lcond_false: forall s f sp cond args lbl b rs m, - eval_condition cond (reglist rs args) m = Some false -> + eval_condition cond (reglist rs args) = Some false -> step (State s f sp (Lcond cond args lbl :: b) rs m) E0 (State s f sp b rs m) | exec_Lreturn: diff --git a/backend/Linearize.v b/backend/Linearize.v index de372cc5..866d05b6 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -186,8 +186,6 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code := Lcall sig ros args res :: add_branch s k | LTL.Ltailcall sig ros args => Ltailcall sig ros args :: k - | LTL.Lalloc arg res s => - Lalloc arg res :: add_branch s k | LTL.Lcond cond args s1 s2 => if starts_with s1 k then Lcond (negate_condition cond) args s2 :: add_branch s1 k diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 8378332e..b3854291 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -604,22 +604,6 @@ Proof. destruct (Genv.find_symbol ge i); try discriminate. eapply Genv.find_funct_ptr_prop; eauto. - (* Lalloc *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - assert (REACH': (reachable f)!!pc' = true). - eapply reachable_successors; eauto. - unfold successors; rewrite H; auto with coqlib. - exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. - econstructor; split. - eapply plus_left'. - eapply exec_Lalloc; eauto. - eapply add_branch_correct; eauto. - eapply is_tail_add_branch. eapply is_tail_cons_left. - eapply is_tail_find_label. eauto. - traceEq. - econstructor; eauto. - (* Lcond true *) destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index ba547230..627c878f 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -55,7 +55,6 @@ Proof. apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. apply wt_add_instr. constructor; auto. auto. - apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. destruct (starts_with s1 k); apply wt_add_instr. constructor; auto. rewrite H. destruct cond; auto. apply wt_add_branch; auto. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 9ef6e317..33b570b9 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -85,8 +85,6 @@ Inductive wt_instr : instruction -> Prop := tailcall_possible sig -> match ros with inl r => r = IT1 | _ => True end -> wt_instr (Ltailcall sig ros) - | wt_Lalloc: - wt_instr Lalloc | wt_Llabel: forall lbl, wt_instr (Llabel lbl) diff --git a/backend/Mach.v b/backend/Mach.v index c64903b8..3f251373 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -58,7 +58,6 @@ Inductive instruction: Set := | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Mcall: signature -> mreg + ident -> instruction | Mtailcall: signature -> mreg + ident -> instruction - | Malloc: instruction | Mlabel: label -> instruction | Mgoto: label -> instruction | Mcond: condition -> list mreg -> label -> instruction diff --git a/backend/Machabstr.v b/backend/Machabstr.v index e145c896..25819f72 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -94,8 +94,9 @@ Section FRAME_ACCESSES. Variable f: function. (** A slot [(ty, ofs)] within a frame is valid in function [f] if it lies - within the bounds of [f]'s frame, and it does not overlap with - the slots reserved for the return address and the back link. *) + within the bounds of [f]'s frame, it does not overlap with + the slots reserved for the return address and the back link, + and it is aligned on a 4-byte boundary. *) Inductive slot_valid: typ -> Z -> Prop := slot_valid_intro: @@ -106,6 +107,7 @@ Inductive slot_valid: typ -> Z -> Prop := \/ Int.signed f.(fn_link_ofs) + 4 <= ofs) -> (ofs + AST.typesize ty <= Int.signed f.(fn_retaddr_ofs) \/ Int.signed f.(fn_retaddr_ofs) + 4 <= ofs) -> + (4 | ofs) -> slot_valid ty ofs. (** [get_slot f fr ty ofs v] holds if the frame [fr] contains value [v] @@ -239,7 +241,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp c (rs#dst <- v) fr m) | exec_Mop: forall s f sp op args res c rs fr m v, - eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op rs##args = Some v -> step (State s f sp (Mop op args res :: c) rs fr m) E0 (State s f sp c (rs#res <- v) fr m) | exec_Mload: @@ -264,15 +266,6 @@ Inductive step: state -> trace -> state -> Prop := find_function ros rs = Some f' -> step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs fr m) E0 (Callstate s f' rs (Mem.free m stk)) - - | exec_Malloc: - forall s f sp c rs fr m sz m' blk, - rs (Conventions.loc_alloc_argument) = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - step (State s f sp (Malloc :: c) rs fr m) - E0 (State s f sp c - (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero)) - fr m') | exec_Mgoto: forall s f sp lbl c rs fr m c', find_label lbl f.(fn_code) = Some c' -> @@ -280,13 +273,13 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp c' rs fr m) | exec_Mcond_true: forall s f sp cond args lbl c rs fr m c', - eval_condition cond rs##args m = Some true -> + eval_condition cond rs##args = Some true -> find_label lbl f.(fn_code) = Some c' -> step (State s f sp (Mcond cond args lbl :: c) rs fr m) E0 (State s f sp c' rs fr m) | exec_Mcond_false: forall s f sp cond args lbl c rs fr m, - eval_condition cond rs##args m = Some false -> + eval_condition cond rs##args = Some false -> step (State s f sp (Mcond cond args lbl :: c) rs fr m) E0 (State s f sp c rs fr m) | exec_Mreturn: diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 7eae610b..6e331f30 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -84,7 +84,7 @@ Inductive frame_match (fr: frame) high_bound ms sp >= 0 -> base = Int.repr (-f.(fn_framesize)) -> (forall ty ofs, - -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> + -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) -> load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) -> frame_match fr sp base mm ms. @@ -126,15 +126,16 @@ Lemma frame_match_load_stack: forall fr sp base mm ms ty ofs, frame_match fr sp base mm ms -> 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> + (4 | Int.signed ofs) -> load_stack ms (Vptr sp base) ty ofs = Some (fr ty (Int.signed ofs - f.(fn_framesize))). Proof. - intros. inv H. + intros. inv H. inv wt_f. unfold load_stack, Val.add, loadv. replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs)) with (Int.signed ofs - fn_framesize f). - apply H6. omega. omega. - inv wt_f. + apply H7. omega. omega. + apply Zdivide_minus_l; auto. assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f). apply Int.signed_repr. assert (0 <= Int.max_signed). compute; congruence. omega. @@ -150,8 +151,7 @@ Lemma frame_match_get_slot: get_slot f fr ty (Int.signed ofs) v -> load_stack ms (Vptr sp base) ty ofs = Some v. Proof. - intros. inversion H. inv H0. eapply frame_match_load_stack; eauto. - inv H7. auto. + intros. inversion H. inv H0. inv H7. eapply frame_match_load_stack; eauto. Qed. (** Assigning a value to a frame slot (in the abstract semantics) @@ -163,6 +163,7 @@ Lemma frame_match_store_stack: forall fr sp base mm ms ty ofs v, frame_match fr sp base mm ms -> 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> + (4 | Int.signed ofs) -> Val.has_type v ty -> Mem.extends mm ms -> exists ms', @@ -186,7 +187,10 @@ Proof. apply valid_access_store. constructor. auto. omega. rewrite size_type_chunk. omega. - destruct H7 as [ms' STORE]. + replace (align_chunk (chunk_of_type ty)) with 4. + apply Zdivide_minus_l; auto. + destruct ty; auto. + destruct H8 as [ms' STORE]. generalize (low_bound_store _ _ _ _ _ _ STORE sp). intro LB. generalize (high_bound_store _ _ _ _ _ _ STORE sp). intro HB. exists ms'. @@ -205,10 +209,10 @@ Proof. destruct ty; destruct ty0; simpl; congruence. destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)). (* disjoint *) - rewrite <- H8; auto. eapply load_store_other; eauto. + rewrite <- H9; auto. eapply load_store_other; eauto. right; left. rewrite size_type_chunk; auto. destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)). - rewrite <- H8; auto. eapply load_store_other; eauto. + rewrite <- H9; auto. eapply load_store_other; eauto. right; right. rewrite size_type_chunk; auto. (* overlap *) eapply load_store_overlap'; eauto with mem. @@ -230,8 +234,7 @@ Lemma frame_match_set_slot: frame_match fr' sp base mm ms' /\ Mem.extends mm ms'. Proof. - intros. inv H0. eapply frame_match_store_stack; eauto. - inv H3. auto. + intros. inv H0. inv H3. eapply frame_match_store_stack; eauto. Qed. (** Agreement is preserved by stores within blocks other than the @@ -277,7 +280,7 @@ Proof. destruct (zeq sp b). subst b. right. rewrite size_type_chunk. assert (valid_access mm chunk sp ofs) by eauto with mem. - inv H8. left. omega. + inv H9. left. omega. auto. Qed. @@ -310,6 +313,7 @@ Proof. intros. eapply load_alloc_same'; eauto. rewrite size_type_chunk. omega. + replace (align_chunk (chunk_of_type ty)) with 4; auto. destruct ty; auto. Qed. Lemma frame_match_alloc: @@ -435,6 +439,7 @@ Proof. replace (parent_sp cs) with (extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))). eapply frame_match_load_stack; eauto. + unfold extend_frame. rewrite update_other. apply update_same. simpl. omega. Qed. @@ -470,10 +475,10 @@ Proof. exploit frame_match_new. eauto. inv H. eexact H4. eauto. eauto. eauto. fold base. intros [C FM0]. destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ - FM0 wt_function_link H2 EXT0) + FM0 wt_function_link wt_function_link_aligned H2 EXT0) as [ms2 [STORE1 [FM1 EXT1]]]. destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ - FM1 wt_function_retaddr H3 EXT1) + FM1 wt_function_retaddr wt_function_retaddr_aligned H3 EXT1) as [ms3 [STORE2 [FM3 EXT3]]]. exists ms2; exists ms3; auto. Qed. @@ -783,8 +788,6 @@ Proof. (* Mop *) exists (State ts fb (Vptr sp0 base) c (rs#res <- v) ms); split. apply exec_Mop; auto. - eapply eval_operation_change_mem with (m := m); eauto. - intros. eapply Mem.valid_pointer_extends; eauto. econstructor; eauto with coqlib. (* Mload *) @@ -826,15 +829,6 @@ Proof. econstructor; eauto. eapply match_stacks_free; auto. apply free_extends; auto. - (* Malloc *) - caseEq (alloc ms 0 (Int.signed sz)). intros ms' blk' ALLOC. - exploit alloc_extends; eauto. omega. omega. intros [EQ MEXT']. subst blk'. - exists (State ts fb (Vptr sp0 base) c (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero)) ms'); split. - eapply exec_Malloc; eauto. - econstructor; eauto. - eapply match_stacks_alloc; eauto. inv MEXT; auto. - eapply frame_match_alloc with (mm := m) (ms := ms); eauto. inv MEXT; auto. - (* Mgoto *) econstructor; split. eapply exec_Mgoto; eauto. @@ -843,13 +837,9 @@ Proof. (* Mcond *) econstructor; split. eapply exec_Mcond_true; eauto. - eapply eval_condition_change_mem with (m := m); eauto. - intros. eapply Mem.valid_pointer_extends; eauto. econstructor; eauto. econstructor; split. eapply exec_Mcond_false; eauto. - eapply eval_condition_change_mem with (m := m); eauto. - intros. eapply Mem.valid_pointer_extends; eauto. econstructor; eauto. (* Mreturn *) diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 41216d25..4417cc6f 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -155,7 +155,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s fb sp c (rs#dst <- v) m) | exec_Mop: forall s f sp op args res c rs m v, - eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op rs##args = Some v -> step (State s f sp (Mop op args res :: c) rs m) E0 (State s f sp c (rs#res <- v) m) | exec_Mload: @@ -186,14 +186,6 @@ Inductive step: state -> trace -> state -> Prop := load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) E0 (Callstate s f' rs (Mem.free m stk)) - | exec_Malloc: - forall s f sp c rs m sz m' blk, - rs (Conventions.loc_alloc_argument) = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - step (State s f sp (Malloc :: c) rs m) - E0 (State s f sp c - (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero)) - m') | exec_Mgoto: forall s fb f sp lbl c rs m c', Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -202,14 +194,14 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s fb sp c' rs m) | exec_Mcond_true: forall s fb f sp cond args lbl c rs m c', - eval_condition cond rs##args m = Some true -> + eval_condition cond rs##args = Some true -> Genv.find_funct_ptr ge fb = Some (Internal f) -> find_label lbl f.(fn_code) = Some c' -> step (State s fb sp (Mcond cond args lbl :: c) rs m) E0 (State s fb sp c' rs m) | exec_Mcond_false: forall s f sp cond args lbl c rs m, - eval_condition cond rs##args m = Some false -> + eval_condition cond rs##args = Some false -> step (State s f sp (Mcond cond args lbl :: c) rs m) E0 (State s f sp c rs m) | exec_Mreturn: diff --git a/backend/Machtyping.v b/backend/Machtyping.v index f9f76d82..ef59e6f0 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -72,8 +72,6 @@ Inductive wt_instr : instruction -> Prop := Conventions.tailcall_possible sig -> match ros with inl r => mreg_type r = Tint | inr s => True end -> wt_instr (Mtailcall sig ros) - | wt_Malloc: - wt_instr Malloc | wt_Mgoto: forall lbl, wt_instr (Mgoto lbl) @@ -91,12 +89,18 @@ Record wt_function (f: function) : Prop := mk_wt_function { f.(fn_stacksize) >= 0; wt_function_framesize: 0 <= f.(fn_framesize) <= -Int.min_signed; + wt_function_framesize_aligned: + (4 | f.(fn_framesize)); wt_function_link: 0 <= Int.signed f.(fn_link_ofs) /\ Int.signed f.(fn_link_ofs) + 4 <= f.(fn_framesize); + wt_function_link_aligned: + (4 | Int.signed f.(fn_link_ofs)); wt_function_retaddr: 0 <= Int.signed f.(fn_retaddr_ofs) /\ Int.signed f.(fn_retaddr_ofs) + 4 <= f.(fn_framesize); + wt_function_retaddr_aligned: + (4 | Int.signed f.(fn_retaddr_ofs)); wt_function_link_retaddr: Int.signed f.(fn_retaddr_ofs) + 4 <= Int.signed f.(fn_link_ofs) \/ Int.signed f.(fn_link_ofs) + 4 <= Int.signed f.(fn_retaddr_ofs) @@ -250,7 +254,7 @@ Proof. simpl in H. rewrite <- H2. replace v with (rs r1). apply WTRS. congruence. replace (mreg_type res) with (snd (type_of_operation op)). - apply type_of_operation_sound with fundef ge rs##args sp m; auto. + apply type_of_operation_sound with fundef ge rs##args sp; auto. rewrite <- H5; reflexivity. apply wt_setreg; auto. inversion H1. rewrite H7. @@ -272,7 +276,7 @@ Proof. apply (Genv.find_funct_ptr_prop wt_fundef wt_p H). econstructor; eauto. - apply wt_setreg; auto. exact I. +(* apply wt_setreg; auto. exact I. *) apply is_tail_find_label with lbl; congruence. apply is_tail_find_label with lbl; congruence. @@ -293,17 +297,6 @@ Proof. econstructor; eauto. eauto with coqlib. Qed. -(* -Lemma subject_reduction_2: - forall s1 t s2, step ge s1 t s2 -> - forall (WTS: wt_state s1), wt_state s2. -Proof. - induction 1; intros. - auto. - eapply subject_reduction; eauto. - auto. -Qed. -*) End SUBJECT_REDUCTION. diff --git a/backend/RTL.v b/backend/RTL.v index abecd4a7..5fad2f27 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -68,10 +68,8 @@ Inductive instruction: Set := as arguments. It stores the return value in [dest] and branches to [succ]. *) | Itailcall: signature -> reg + ident -> list reg -> instruction - | Ialloc: reg -> reg -> node -> instruction - (** [Ialloc arg dest succ] allocates a fresh block of size - the contents of register [arg], stores a pointer to this - block in [dest], and branches to [succ]. *) + (** [Itailcall sig fn args] performs a function invocation + in tail-call position. *) | Icond: condition -> list reg -> node -> node -> instruction (** [Icond cond args ifso ifnot] evaluates the boolean condition [cond] over the values of registers [args]. If the condition @@ -213,7 +211,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_Iop: forall s c sp pc rs m op args res pc' v, c!pc = Some(Iop op args res pc') -> - eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op rs##args = Some v -> step (State s c sp pc rs m) E0 (State s c sp pc' (rs#res <- v) m) | exec_Iload: @@ -244,23 +242,16 @@ Inductive step: state -> trace -> state -> Prop := funsig f = sig -> step (State s c (Vptr stk Int.zero) pc rs m) E0 (Callstate s f rs##args (Mem.free m stk)) - | exec_Ialloc: - forall s c sp pc rs m pc' arg res sz m' b, - c!pc = Some(Ialloc arg res pc') -> - rs#arg = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', b) -> - step (State s c sp pc rs m) - E0 (State s c sp pc' (rs#res <- (Vptr b Int.zero)) m') | exec_Icond_true: forall s c sp pc rs m cond args ifso ifnot, c!pc = Some(Icond cond args ifso ifnot) -> - eval_condition cond rs##args m = Some true -> + eval_condition cond rs##args = Some true -> step (State s c sp pc rs m) E0 (State s c sp ifso rs m) | exec_Icond_false: forall s c sp pc rs m cond args ifso ifnot, c!pc = Some(Icond cond args ifso ifnot) -> - eval_condition cond rs##args m = Some false -> + eval_condition cond rs##args = Some false -> step (State s c sp pc rs m) E0 (State s c sp ifnot rs m) | exec_Ireturn: @@ -291,7 +282,7 @@ Inductive step: state -> trace -> state -> Prop := Lemma exec_Iop': forall s c sp pc rs m op args res pc' rs' v, c!pc = Some(Iop op args res pc') -> - eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op rs##args = Some v -> rs' = (rs#res <- v) -> step (State s c sp pc rs m) E0 (State s c sp pc' rs' m). @@ -352,7 +343,6 @@ Definition successors (f: function) (pc: node) : list node := | Istore chunk addr args src s => s :: nil | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil - | Ialloc arg res s => s :: nil | Icond cond args ifso ifnot => ifso :: ifnot :: nil | Ireturn optarg => nil end diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 5fde3d88..709dc78c 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -530,12 +530,6 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do n1 <- add_instr (Itailcall sig (inl _ rf) rargs); do n2 <- transl_exprlist map cl rargs n1; transl_expr map b rf n2 - | Salloc id a => - do ra <- alloc_reg map a; - do rr <- new_reg; - do n1 <- store_var map rr id nd; - do n2 <- add_instr (Ialloc ra rr n1); - transl_expr map a ra n2 | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 1074dddb..6d5cd8ea 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -568,7 +568,7 @@ Lemma transl_expr_Eop_correct: (vargs : list val) (v : val), eval_exprlist ge sp e m le args vargs -> transl_exprlist_prop le args vargs -> - eval_operation ge sp op vargs m = Some v -> + eval_operation ge sp op vargs = Some v -> transl_expr_prop le (Eop op args) v. Proof. intros; red; intros. inv TE. @@ -711,7 +711,7 @@ Lemma transl_condition_CEcond_correct: (vargs : list val) (b : bool), eval_exprlist ge sp e m le args vargs -> transl_exprlist_prop le args vargs -> - eval_condition cond vargs m = Some b -> + eval_condition cond vargs = Some b -> transl_condition_prop le (CEcond cond args) b. Proof. intros; red; intros; inv TE. @@ -1154,22 +1154,6 @@ Proof. apply sig_transl_function; auto. traceEq. rewrite G. constructor; auto. - - (* alloc *) - inv TS. - exploit transl_expr_correct; eauto. - intros [rs1 [A [B [C D]]]]. - set (rs2 := rs1#rd <- (Vptr b Int.zero)). - assert (match_env map e nil rs2). unfold rs2; eauto with rtlg. - exploit tr_store_var_correct. eauto. auto. eexact H1. - intros [rs3 [E F]]. - unfold rs2 in F. rewrite Regmap.gss in F. - econstructor; split. - left. apply plus_star_trans with E0 (State cs c sp n2 rs2 m') E0. - eapply plus_right. eexact A. unfold rs2. eapply exec_Ialloc; eauto. traceEq. - eexact E. traceEq. - econstructor; eauto. constructor. - (* seq *) inv TS. econstructor; split. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 59a5dd7e..e6adeb05 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -141,21 +141,6 @@ Proof. Qed. Hint Resolve instr_at_incr: rtlg. -(* -(** A useful tactic to reason over transitivity and reflexivity of [state_incr]. *) - -Ltac Show_state_incr := - eauto; - match goal with - | |- (state_incr ?c ?c) => - apply state_incr_refl - | |- (state_incr ?c1 ?c2) => - eapply state_incr_trans; [eauto; fail | idtac]; Show_state_incr - end. - -Hint Extern 2 (state_incr _ _) => Show_state_incr : rtlg. -*) - Hint Resolve state_incr_refl state_incr_trans: rtlg. (** * Validity and freshness of registers *) @@ -779,12 +764,6 @@ Inductive tr_stmt (c: code) (map: mapping): tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> c!n2 = Some (Itailcall sig (inl _ rf) rargs) -> tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret - | tr_Salloc: forall id a ns nd nexits ngoto nret rret rd n1 n2 r, - tr_expr c map nil a ns n1 r -> - c!n1 = Some (Ialloc r rd n2) -> - tr_store_var c map rd id n2 nd -> - ~reg_in_map map rd -> - tr_stmt c map (Salloc id a) ns nd nexits ngoto nret rret | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n, tr_stmt c map s2 n nd nexits ngoto nret rret -> tr_stmt c map s1 ns n nexits ngoto nret rret -> @@ -1197,11 +1176,6 @@ Proof. eapply A; eauto with rtlg. apply tr_exprlist_incr with s4; auto. eapply C; eauto with rtlg. - (* Salloc *) - econstructor; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. - apply tr_store_var_incr with s2; eauto with rtlg. - eapply store_var_charact; eauto with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index fa9dd210..60b1d72c 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -100,11 +100,6 @@ Inductive wt_instr : instruction -> Prop := List.map env args = sig.(sig_args) -> Conventions.tailcall_possible sig -> wt_instr (Itailcall sig ros args) - | wt_Ialloc: - forall arg res s, - env arg = Tint -> env res = Tint -> - valid_successor s -> - wt_instr (Ialloc arg res s) | wt_Icond: forall cond args s1 s2, List.map env args = type_of_condition cond -> @@ -225,10 +220,6 @@ Definition check_instr (i: instruction) : bool := && check_regs args sig.(sig_args) && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res) && Conventions.tailcall_is_possible sig - | Ialloc arg res s => - check_reg arg Tint - && check_reg res Tint - && check_successor s | Icond cond args s1 s2 => check_regs args (type_of_condition cond) && check_successor s1 @@ -331,11 +322,6 @@ Proof. eapply proj_sumbool_true; eauto. apply check_regs_correct; auto. apply Conventions.tailcall_is_possible_correct; auto. - (* alloc *) - constructor. - apply check_reg_correct; auto. - apply check_reg_correct; auto. - apply check_successor_correct; auto. (* cond *) constructor. apply check_regs_correct; auto. apply check_successor_correct; auto. @@ -524,7 +510,7 @@ Proof. econstructor; eauto. apply wt_regset_assign. auto. replace (env res) with (snd (type_of_operation op)). - apply type_of_operation_sound with fundef ge rs##args sp m; auto. + apply type_of_operation_sound with fundef ge rs##args sp; auto. rewrite <- H6. reflexivity. (* Iload *) econstructor; eauto. @@ -556,9 +542,6 @@ Proof. econstructor; eauto. rewrite H5; auto. rewrite <- H6. apply wt_regset_list. auto. - (* Ialloc *) - econstructor; eauto. - apply wt_regset_assign. auto. rewrite H6; exact I. (* Icond *) econstructor; eauto. econstructor; eauto. diff --git a/backend/Reload.v b/backend/Reload.v index 17664b63..621e75b5 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -235,9 +235,6 @@ Definition transf_instr parallel_move args largs (Ltailcall sig (inr _ id) :: k) end - | LTLin.Lalloc arg res => - add_reload arg loc_alloc_argument - (Lalloc :: add_spill loc_alloc_result res k) | LTLin.Llabel lbl => Llabel lbl :: k | LTLin.Lgoto lbl => diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 5a3acd31..ea7c5d19 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -178,10 +178,10 @@ Proof. Qed. Lemma not_enough_temporaries_addr: - forall (ge: genv) sp addr src args ls m v, + forall (ge: genv) sp addr src args ls v, enough_temporaries (src :: args) = false -> eval_addressing ge sp addr (List.map ls args) = Some v -> - eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) m = Some v. + eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) = Some v. Proof. intros. apply eval_op_for_binary_addressing; auto. @@ -631,21 +631,6 @@ Proof. apply temporaries_not_acceptable; auto. Qed. -Lemma agree_postcall_alloc: - forall rs ls ls2 v, - agree rs ls -> - (forall l, Loc.diff (R loc_alloc_argument) l -> ls2 l = ls l) -> - agree (LTL.postcall_locs rs) (Locmap.set (R loc_alloc_result) v ls2). -Proof. - intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto. - intros. destruct (Loc.eq l (R loc_alloc_result)). - subst l. elim H2. simpl. tauto. - rewrite Locmap.gso. apply H0. - red. destruct l; auto. red; intro. subst m. elim H2. - simpl. tauto. - apply Loc.diff_sym. apply loc_acceptable_noteq_diff; auto. -Qed. - Lemma agree_init_locs: forall ls dsts vl, locs_acceptable dsts -> @@ -991,9 +976,9 @@ Proof. eapply enough_temporaries_op_args; eauto. apply locs_acceptable_disj_temporaries; auto. intros [ls2 [A [B C]]]. instantiate (1 := ls) in B. - assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) tm = Some tv + assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) = Some tv /\ Val.lessdef v tv). - apply eval_operation_lessdef with m (map rs args); auto. + apply eval_operation_lessdef with (map rs args); auto. rewrite B. eapply agree_locs; eauto. rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. destruct H1 as [tv [P Q]]. @@ -1231,28 +1216,6 @@ Proof. exact (return_regs_preserve (parent_locset s') ls3). apply Mem.free_lessdef; auto. - (* Lalloc *) - ExploitWT; inv WTI. - caseEq (alloc tm 0 (Int.signed sz)). intros tm' blk' TALLOC. - assert (blk = blk' /\ Mem.lessdef m' tm'). - eapply Mem.alloc_lessdef; eauto. - exploit add_reload_correct. intros [ls2 [A [B C]]]. - exploit add_spill_correct. intros [ls3 [D [E F]]]. - destruct H1 as [P Q]. subst blk'. - assert (ls arg = Vint sz). - assert (Val.lessdef (rs arg) (ls arg)). eapply agree_loc; eauto. - rewrite H in H1; inversion H1; auto. - left; econstructor; split. - eapply star_plus_trans. eauto. - eapply plus_left. eapply exec_Lalloc; eauto. - rewrite B. eauto. - eauto. eauto. traceEq. - econstructor; eauto with coqlib. - apply agree_set with (Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) ls2). - auto. rewrite E. rewrite Locmap.gss. constructor. - auto. - apply agree_postcall_alloc with ls; auto. - (* Llabel *) left; econstructor; split. apply plus_one. apply exec_Llabel. @@ -1272,7 +1235,7 @@ Proof. intros [ls2 [A [B C]]]. left; econstructor; split. eapply plus_right. eauto. eapply exec_Lcond_true; eauto. - rewrite B. apply eval_condition_lessdef with m (map rs args); auto. + rewrite B. apply eval_condition_lessdef with (map rs args); auto. eapply agree_locs; eauto. apply find_label_transf_function; eauto. traceEq. @@ -1288,7 +1251,7 @@ Proof. intros [ls2 [A [B C]]]. left; econstructor; split. eapply plus_right. eauto. eapply exec_Lcond_false; eauto. - rewrite B. apply eval_condition_lessdef with m (map rs args); auto. + rewrite B. apply eval_condition_lessdef with (map rs args); auto. eapply agree_locs; eauto. traceEq. econstructor; eauto with coqlib. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index e531c548..375bbfde 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -34,7 +34,7 @@ Require Import Reloadproof. given sufficient typing and well-formedness hypotheses over the locations involved. *) Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove - wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lalloc + wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Llabel wt_Lgoto wt_Lcond wt_Lreturn: reloadty. Remark wt_code_cons: diff --git a/backend/Stacking.v b/backend/Stacking.v index 1cf010b4..158af8f6 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -179,8 +179,6 @@ Definition transl_instr | Ltailcall sig ros => restore_callee_save fe (Mtailcall sig ros :: k) - | Lalloc => - Malloc :: k | Llabel lbl => Mlabel lbl :: k | Lgoto lbl => diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index e17f67a6..a7560d03 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -172,6 +172,45 @@ Proof. assert (z <> z0). intuition auto. omega. Qed. +Remark aligned_4_4x: forall x, (4 | 4 * x). +Proof. intro. exists x; ring. Qed. + +Remark aligned_4_8x: forall x, (4 | 8 * x). +Proof. intro. exists (x * 2); ring. Qed. + +Remark aligned_4_align8: forall x, (4 | align x 8). +Proof. + intro. apply Zdivides_trans with 8. exists 2; auto. apply align_divides. omega. +Qed. + +Hint Resolve Zdivide_0 Zdivide_refl Zdivide_plus_r + aligned_4_4x aligned_4_8x aligned_4_align8: align_4. + +Hint Extern 4 (?X | ?Y) => (exists (Y/X); reflexivity) : align_4. + +Lemma offset_of_index_aligned: + forall idx, (4 | offset_of_index fe idx). +Proof. + intros. + destruct idx; + unfold offset_of_index, fe, make_env, + fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, + fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg; + auto with align_4. + destruct t; auto with align_4. +Qed. + +Lemma frame_size_aligned: + (4 | fe_size fe). +Proof. + unfold offset_of_index, fe, make_env, + fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, + fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg; + auto with align_4. +Qed. + (** The following lemmas give sufficient conditions for indices of various kinds to be valid. *) @@ -232,7 +271,7 @@ Proof. fe_ofs_float_local, fe_ofs_float_callee_save, fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg, type_of_index, typesize; - simpl in H5; + unfold index_valid in H5; simpl typesize in H5; omega. Qed. @@ -287,6 +326,7 @@ Proof. auto. exact I. red. destruct idx; auto || congruence. intro. rewrite typesize_typesize. assumption. exact I. + apply offset_of_index_aligned. Qed. Lemma get_slot_index: @@ -535,96 +575,6 @@ Proof. intros. rewrite get_set_index_val_other; eauto with stacking. red; auto. Qed. -(* -Lemma agree_set_int_callee_save: - forall ls ls0 rs fr r v, - agree ls ls0 rs fr -> - In r int_callee_save_regs -> - index_int_callee_save r < fe.(fe_num_int_callee_save) -> - exists fr', - set_slot tf fr Tint - (Int.signed (Int.repr - (offset_of_index fe (FI_saved_int (index_int_callee_save r))))) - v fr' /\ - agree ls (Locmap.set (R r) v ls0) rs fr'. -Proof. - intros. - set (idx := FI_saved_int (index_int_callee_save r)). - exists (set_index_val idx v fr); split. - change Tint with (type_of_index idx). - apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. - constructor; eauto with stacking. - (* agree_unused_reg *) - intros. rewrite Locmap.gso. eauto with stacking. - red; red; intro. subst r0. elim H2. red. - rewrite (int_callee_save_type r H0). auto. - (* agree_local *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_outgoing *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_incoming *) - intros. rewrite Locmap.gso. eauto with stacking. red. auto. - (* saved ints *) - intros. destruct (mreg_eq r r0). - subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. - rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking. - unfold idx. auto with stacking. auto with stacking. - unfold idx; red. apply index_int_callee_save_inj; auto. - red; auto. - (* saved floats *) - intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. - unfold idx. auto with stacking. - unfold idx; red; auto. - red. apply int_float_callee_save_disjoint; auto. -Qed. - -Lemma agree_set_float_callee_save: - forall ls ls0 rs fr r v, - agree ls ls0 rs fr -> - In r float_callee_save_regs -> - index_float_callee_save r < fe.(fe_num_float_callee_save) -> - exists fr', - set_slot tf fr Tfloat - (Int.signed (Int.repr - (offset_of_index fe (FI_saved_float (index_float_callee_save r))))) - v fr' /\ - agree ls (Locmap.set (R r) v ls0) rs fr'. -Proof. - intros. - set (idx := FI_saved_float (index_float_callee_save r)). - exists (set_index_val idx v fr); split. - change Tfloat with (type_of_index idx). - apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. - constructor; eauto with stacking. - (* agree_unused_reg *) - intros. rewrite Locmap.gso. eauto with stacking. - red; red; intro. subst r0. elim H2. red. - rewrite (float_callee_save_type r H0). auto. - (* agree_local *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_outgoing *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_incoming *) - intros. rewrite Locmap.gso. eauto with stacking. red. auto. - (* saved ints *) - intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. - unfold idx. auto with stacking. - unfold idx; red; auto. - red. apply sym_not_equal. apply int_float_callee_save_disjoint; auto. - (* saved floats *) - intros. destruct (mreg_eq r r0). - subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. - rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking. - unfold idx. auto with stacking. auto with stacking. - unfold idx; red. apply index_float_callee_save_inj; auto. - red; auto. -Qed. -*) - Lemma agree_return_regs: forall ls ls0 rs fr cs rs', agree ls ls0 rs fr cs -> @@ -1270,12 +1220,11 @@ Proof. Qed. Lemma shift_eval_operation: - forall f tf sp op args m v, + forall f tf sp op args v, transf_function f = OK tf -> - eval_operation ge sp op args m = Some v -> + eval_operation ge sp op args = Some v -> eval_operation tge (shift_sp tf sp) - (transl_op (make_env (function_bounds f)) op) args m = - Some v. + (transl_op (make_env (function_bounds f)) op) args = Some v. Proof. intros until v. destruct op; intros; auto. simpl in *. rewrite symbols_preserved. auto. @@ -1535,15 +1484,6 @@ Proof. intros. inv WTI. generalize (H3 _ H0). tauto. apply agree_callee_save_return_regs. - (* Lalloc *) - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) - (rs0#loc_alloc_result <- (Vptr blk Int.zero)) fr m'); split. - apply plus_one; eapply exec_Malloc; eauto. - rewrite (agree_eval_reg _ _ _ _ _ _ _ loc_alloc_argument AG). auto. - econstructor; eauto with coqlib. - apply agree_set_reg; auto. - red. simpl. generalize (max_over_regs_of_funct_pos f int_callee_save). omega. - (* Llabel *) econstructor; split. apply plus_one; apply exec_Mlabel. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index f1fe2cf0..b88dd50c 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -176,8 +176,6 @@ Proof. apply wt_restore_callee_save. apply wt_instrs_cons; auto. constructor; auto. destruct s0; auto. rewrite H5; auto. - (* alloc *) - apply wt_instrs_cons; auto. constructor. (* label *) apply wt_instrs_cons; auto. constructor. @@ -227,10 +225,13 @@ Proof. red; intros. elim H5. subst tf; simpl; auto. rewrite H2. generalize (size_pos f). fold b; fold fe; omega. + rewrite H1. change (4 | fe_size fe). unfold fe, b. apply frame_size_aligned. rewrite H3; rewrite H2. change 4 with (4 * typesize (type_of_index FI_link)). unfold fe, b; apply offset_of_index_valid. red; auto. + rewrite H3. unfold fe,b; apply offset_of_index_aligned. rewrite H4; rewrite H2. change 4 with (4 * typesize (type_of_index FI_retaddr)). unfold fe, b; apply offset_of_index_valid. red; auto. + rewrite H4. unfold fe,b; apply offset_of_index_aligned. rewrite H3; rewrite H4. apply (offset_of_index_disj f FI_retaddr FI_link); red; auto. Qed. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 2f520c61..32d1b595 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -112,8 +112,6 @@ Definition tunnel_instr (f: LTL.function) (b: instruction) : instruction := Lcall sig ros args res (branch_target f s) | Ltailcall sig ros args => Ltailcall sig ros args - | Lalloc arg res s => - Lalloc arg res (branch_target f s) | Lcond cond args s1 s2 => Lcond cond args (branch_target f s1) (branch_target f s2) | Lreturn or => diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 7ad75bae..49bf8942 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -297,12 +297,6 @@ Proof. rewrite sig_preserved. auto. apply find_function_translated; auto. econstructor; eauto. - (* Lalloc *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. - left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_locs rs)) m'); split. - eapply exec_Lalloc; eauto. - rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. - econstructor; eauto. (* cond *) rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. left; econstructor; split. diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 755aa28c..cc5e5ab3 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -287,8 +287,13 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := (** Layout of the Cminor stack data block and construction of the compilation environment. Csharpminor local variables that are arrays or whose address is taken are allocated a slot in the Cminor - stack data. While this is not important for correctness, sufficient - padding is inserted to ensure adequate alignment of addresses. *) + stack data. Sufficient padding is inserted to ensure adequate alignment + of addresses. *) + +Definition array_alignment (sz: Z) : Z := + if zlt sz 2 then 1 + else if zlt sz 4 then 2 + else if zlt sz 8 then 4 else 8. Definition assign_variable (atk: Identset.t) @@ -297,7 +302,7 @@ Definition assign_variable let (cenv, stacksize) := cenv_stacksize in match id_lv with | (id, Varray sz) => - let ofs := align stacksize 8 in + let ofs := align stacksize (array_alignment sz) in (PMap.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz) | (id, Vscalar chunk) => if Identset.mem id atk then diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index e1224bd1..5615eabe 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -484,7 +484,7 @@ Proof. intros. assert (exists v, load chunk m2 b 0 = Some v). apply valid_access_load. - eapply valid_access_alloc_same; eauto; omega. + eapply valid_access_alloc_same; eauto. omega. omega. apply Zdivide_0. destruct H0 as [v LOAD]. rewrite LOAD. decEq. eapply load_alloc_same; eauto. Qed. @@ -802,10 +802,10 @@ Qed. Remark val_inject_eval_compare_null: forall f i c v, - (if Int.eq i Int.zero then eval_compare_mismatch c else None) = Some v -> + eval_compare_null c i = Some v -> val_inject f v v. Proof. - intros. destruct (Int.eq i Int.zero). + unfold eval_compare_null. intros. destruct (Int.eq i Int.zero). eapply val_inject_eval_compare_mismatch; eauto. discriminate. Qed. @@ -871,12 +871,12 @@ Qed. Lemma eval_binop_compat: forall f op v1 tv1 v2 tv2 v m tm, - eval_binop op v1 v2 m = Some v -> + Csharpminor.eval_binop op v1 v2 m = Some v -> val_inject f v1 tv1 -> val_inject f v2 tv2 -> mem_inject f m tm -> exists tv, - eval_binop op tv1 tv2 tm = Some tv + Cminor.eval_binop op tv1 tv2 = Some tv /\ val_inject f v tv. Proof. destruct op; simpl; intros. @@ -919,10 +919,6 @@ Proof. caseEq (valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b0 (Int.signed ofs0)); intro EQ; rewrite EQ in H4; try discriminate. elim (andb_prop _ _ EQ); intros. - exploit (Mem.valid_pointer_inject f m tm b0 ofs0); eauto. - intro VP; rewrite VP; clear VP. - exploit (Mem.valid_pointer_inject f m tm b1 ofs1); eauto. - intro VP; rewrite VP; clear VP. destruct (eq_block b1 b0); inv H4. (* same blocks in source *) assert (b3 = b2) by congruence. subst b3. @@ -1318,6 +1314,15 @@ Qed. local variables, either as Cminor local variables or as sub-blocks of the Cminor stack data. This is the most difficult part of the proof. *) +Remark array_alignment_pos: + forall sz, array_alignment sz > 0. +Proof. + unfold array_alignment; intros. + destruct (zlt sz 2). omega. + destruct (zlt sz 4). omega. + destruct (zlt sz 8); omega. +Qed. + Remark assign_variables_incr: forall atk vars cenv sz cenv' sz', assign_variables atk vars (cenv, sz) = (cenv', sz') -> sz <= sz'. @@ -1329,12 +1334,56 @@ Proof. generalize (size_chunk_pos m). intro. generalize (align_le sz (size_chunk m) H0). omega. eauto. - intro. generalize (IHvars _ _ _ _ H). - assert (8 > 0). omega. generalize (align_le sz 8 H0). + intro. generalize (IHvars _ _ _ _ H). + generalize (align_le sz (array_alignment z) (array_alignment_pos z)). assert (0 <= Zmax 0 z). apply Zmax_bound_l. omega. omega. Qed. +Remark inj_offset_aligned_array: + forall stacksize sz, + inj_offset_aligned (align stacksize (array_alignment sz)) sz. +Proof. + intros; red; intros. + apply Zdivides_trans with (array_alignment sz). + unfold align_chunk. unfold array_alignment. + generalize Zone_divide; intro. + generalize Zdivide_refl; intro. + assert (2 | 4). exists 2; auto. + assert (2 | 8). exists 4; auto. + assert (4 | 8). exists 2; auto. + destruct (zlt sz 2). + destruct chunk; simpl in *; auto; omegaContradiction. + destruct (zlt sz 4). + destruct chunk; simpl in *; auto; omegaContradiction. + destruct (zlt sz 8). + destruct chunk; simpl in *; auto; omegaContradiction. + destruct chunk; simpl; auto. + apply align_divides. apply array_alignment_pos. +Qed. + +Remark inj_offset_aligned_array': + forall stacksize sz, + inj_offset_aligned (align stacksize (array_alignment sz)) (Zmax 0 sz). +Proof. + intros. + replace (array_alignment sz) with (array_alignment (Zmax 0 sz)). + apply inj_offset_aligned_array. + rewrite Zmax_spec. destruct (zlt sz 0); auto. + transitivity 1. reflexivity. unfold array_alignment. rewrite zlt_true. auto. omega. +Qed. + +Remark inj_offset_aligned_var: + forall stacksize chunk, + inj_offset_aligned (align stacksize (size_chunk chunk)) (size_chunk chunk). +Proof. + intros. + replace (align stacksize (size_chunk chunk)) + with (align stacksize (array_alignment (size_chunk chunk))). + apply inj_offset_aligned_array. + decEq. destruct chunk; reflexivity. +Qed. + Lemma match_callstack_alloc_variables_rec: forall tm sp cenv' sz' te lo cs atk, valid_block tm sp -> @@ -1388,7 +1437,9 @@ Proof. assert (Int.min_signed < 0). compute; auto. generalize (assign_variables_incr _ _ _ _ _ _ ASVS). intro. unfold f1; eapply alloc_mapped_inject; eauto. - omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. + omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. + rewrite Zminus_0_r. unfold ofs. rewrite LV. simpl. + apply inj_offset_aligned_var. intros. left. generalize (BOUND _ _ H5). omega. elim H3; intros MINJ1 INCR1; clear H3. exploit IHalloc_variables; eauto. @@ -1416,25 +1467,26 @@ Proof. (* 2. lv = LVarray dim, info = Var_stack_array *) intros dim LV EQ. injection EQ; clear EQ; intros. assert (0 <= Zmax 0 dim). apply Zmax1. - assert (8 > 0). omega. - generalize (align_le sz 8 H4). intro. - set (ofs := align sz 8) in *. + generalize (align_le sz (array_alignment dim) (array_alignment_pos dim)). intro. + set (ofs := align sz (array_alignment dim)) in *. set (f1 := extend_inject b1 (Some (sp, ofs)) f). assert (mem_inject f1 m1 tm /\ inject_incr f f1). assert (Int.min_signed < 0). compute; auto. generalize (assign_variables_incr _ _ _ _ _ _ ASVS). intro. unfold f1; eapply alloc_mapped_inject; eauto. - omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. - intros. left. generalize (BOUND _ _ H8). omega. - destruct H6 as [MINJ1 INCR1]. + omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. + rewrite Zminus_0_r. unfold ofs. rewrite LV. simpl. + apply inj_offset_aligned_array'. + intros. left. generalize (BOUND _ _ H7). omega. + destruct H5 as [MINJ1 INCR1]. exploit IHalloc_variables; eauto. unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. rewrite <- H1. omega. intros until delta; unfold f1, extend_inject, eq_block. rewrite (high_bound_alloc _ _ _ _ _ H b). case (zeq b b1); intros. - inversion H6. unfold sizeof; rewrite LV. omega. - generalize (BOUND _ _ H6). omega. + inversion H5. unfold sizeof; rewrite LV. omega. + generalize (BOUND _ _ H5). omega. intros [f' [INCR2 [MINJ2 MATCH2]]]. exists f'; intuition. eapply inject_incr_trans; eauto. Qed. diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index ce19f687..1aa536a1 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -181,7 +181,18 @@ Definition eval_constant (cst: constant) : option val := end. Definition eval_unop := Cminor.eval_unop. -Definition eval_binop := Cminor.eval_binop. + +Definition eval_binop (op: binary_operation) + (arg1 arg2: val) (m: mem): option val := + match op, arg1, arg2 with + | Cminor.Ocmp c, Vptr b1 n1, Vptr b2 n2 => + if valid_pointer m b1 (Int.signed n1) + && valid_pointer m b2 (Int.signed n2) + then Cminor.eval_binop op arg1 arg2 + else None + | _, _, _ => + Cminor.eval_binop op arg1 arg2 + end. (** Allocation of local variables at function entry. Each variable is bound to the reference to a fresh block of the appropriate size. *) diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index 98d057a4..e51533c3 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -313,10 +313,10 @@ Proof. simpl. rewrite H3. unfold eq_block. rewrite H9. auto. (* ipip ptr int *) inversion H9. eapply eval_Ebinop; eauto with cshm. - simpl. rewrite H8. auto. + simpl. unfold eval_compare_null. rewrite H8. auto. (* ipip int ptr *) inversion H9. eapply eval_Ebinop; eauto with cshm. - simpl. rewrite H8. auto. + simpl. unfold eval_compare_null. rewrite H8. auto. (* ff *) inversion H8. eauto with cshm. Qed. diff --git a/common/Mem.v b/common/Mem.v index 3db2ceba..de3e8c94 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -122,6 +122,51 @@ Proof. destruct chunk; auto. Qed. +Lemma size_chunk_pos: + forall chunk, size_chunk chunk > 0. +Proof. + intros. rewrite size_chunk_pred. omega. +Qed. + +(** Memory reads and writes must respect alignment constraints: + the byte offset of the location being addressed should be an exact + multiple of the natural alignment for the chunk being addressed. + This natural alignment is defined by the following + [align_chunk] function. Some target architectures + (e.g. the PowerPC) have no alignment constraints, which we could + reflect by taking [align_chunk chunk = 1]. However, other architectures + have stronger alignment requirements. The following definition is + appropriate for PowerPC and ARM. *) + +Definition align_chunk (chunk: memory_chunk) : Z := + match chunk with + | Mint8signed => 1 + | Mint8unsigned => 1 + | Mint16signed => 2 + | Mint16unsigned => 2 + | _ => 4 + end. + +Lemma align_chunk_pos: + forall chunk, align_chunk chunk > 0. +Proof. + intro. destruct chunk; simpl; omega. +Qed. + +Lemma align_size_chunk_divides: + forall chunk, (align_chunk chunk | size_chunk chunk). +Proof. + intros. destruct chunk; simpl; try apply Zdivide_refl. exists 2; auto. +Qed. + +Lemma align_chunk_compat: + forall chunk1 chunk2, + size_chunk chunk1 = size_chunk chunk2 -> align_chunk chunk1 = align_chunk chunk2. +Proof. + intros chunk1 chunk2. + destruct chunk1; destruct chunk2; simpl; congruence. +Qed. + (** The initial store. *) Remark one_pos: 1 > 0. @@ -376,13 +421,19 @@ Proof. Qed. (** [valid_access m chunk b ofs] holds if a memory access (load or store) - of the given chunk is possible in [m] at address [b, ofs]. *) + of the given chunk is possible in [m] at address [b, ofs]. + This means: +- The block [b] is valid. +- The range of bytes accessed is within the bounds of [b]. +- The offset [ofs] is aligned. +*) Inductive valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) : Prop := | valid_access_intro: valid_block m b -> low_bound m b <= ofs -> ofs + size_chunk chunk <= high_bound m b -> + (align_chunk chunk | ofs) -> valid_access m chunk b ofs. (** The following function checks whether accessing the given memory chunk @@ -395,7 +446,9 @@ Proof. destruct (zlt b m.(nextblock)). destruct (zle (low_bound m b) ofs). destruct (zle (ofs + size_chunk chunk) (high_bound m b)). + destruct (Zdivide_dec (align_chunk chunk) ofs (align_chunk_pos chunk)). left; constructor; auto. + right; red; intro V; inv V; contradiction. right; red; intro V; inv V; omega. right; red; intro V; inv V; omega. right; red; intro V; inv V; contradiction. @@ -577,7 +630,24 @@ Proof. intros. inv H; auto. Qed. -Hint Resolve valid_not_valid_diff valid_access_valid_block: mem. +Lemma valid_access_aligned: + forall m chunk b ofs, + valid_access m chunk b ofs -> (align_chunk chunk | ofs). +Proof. + intros. inv H; auto. +Qed. + +Lemma valid_access_compat: + forall m chunk1 chunk2 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. + rewrite <- (align_chunk_compat _ _ H). auto. +Qed. + +Hint Resolve valid_not_valid_diff valid_access_valid_block valid_access_aligned: mem. (** ** Properties related to [load] *) @@ -661,7 +731,7 @@ Lemma store_valid_access_1: forall chunk' b' ofs', valid_access m1 chunk' b' ofs' -> valid_access m2 chunk' b' ofs'. Proof. - intros. inv H. constructor. auto with mem. + intros. inv H. constructor; auto with mem. rewrite low_bound_store; auto. rewrite high_bound_store; auto. Qed. @@ -670,7 +740,7 @@ Lemma store_valid_access_2: forall chunk' b' ofs', valid_access m2 chunk' b' ofs' -> valid_access m1 chunk' b' ofs'. Proof. - intros. inv H. constructor. auto with mem. + intros. inv H. constructor; auto with mem. rewrite low_bound_store in H1; auto. rewrite high_bound_store in H2; auto. Qed. @@ -698,6 +768,7 @@ Proof. repeat rewrite size_chunk_pred in H. omega. apply store_valid_access_1. inv H0. constructor; auto. congruence. + rewrite (align_chunk_compat _ _ H). auto. Qed. Theorem load_store_same: @@ -801,12 +872,6 @@ Inductive load_store_cases b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 <> size_chunk chunk2 -> load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2. -Remark size_chunk_pos: - forall chunk1, size_chunk chunk1 > 0. -Proof. - destruct chunk1; simpl; omega. -Qed. - Definition load_store_classification: forall (chunk1: memory_chunk) (b1: block) (ofs1: Z) (chunk2: memory_chunk) (b2: block) (ofs2: Z), @@ -949,17 +1014,17 @@ Lemma valid_access_alloc_other: valid_access m1 chunk b' ofs -> valid_access m2 chunk b' ofs. Proof. - intros. inv H. constructor. auto with mem. + intros. inv H. constructor; auto with mem. rewrite low_bound_alloc_other; auto. rewrite high_bound_alloc_other; auto. Qed. Lemma valid_access_alloc_same: forall chunk ofs, - lo <= ofs -> ofs + size_chunk chunk <= hi -> + lo <= ofs -> ofs + size_chunk chunk <= hi -> (align_chunk chunk | ofs) -> valid_access m2 chunk b ofs. Proof. - intros. constructor. auto with mem. + intros. constructor; auto with mem. rewrite low_bound_alloc_same; auto. rewrite high_bound_alloc_same; auto. Qed. @@ -970,14 +1035,14 @@ Lemma valid_access_alloc_inv: forall chunk b' ofs, valid_access m2 chunk b' ofs -> valid_access m1 chunk b' ofs \/ - (b' = b /\ lo <= ofs /\ ofs + size_chunk chunk <= hi). + (b' = b /\ lo <= ofs /\ ofs + size_chunk chunk <= hi /\ (align_chunk chunk | ofs)). Proof. intros. inv H. elim (valid_block_alloc_inv _ H0); intro. subst b'. rewrite low_bound_alloc_same in H1. rewrite high_bound_alloc_same in H2. right. tauto. - left. constructor. auto. + left. constructor; auto. rewrite low_bound_alloc_other in H1; auto. rewrite high_bound_alloc_other in H2; auto. Qed. @@ -1020,14 +1085,14 @@ Qed. Theorem load_alloc_same': forall chunk ofs, - lo <= ofs -> ofs + size_chunk chunk <= hi -> + lo <= ofs -> ofs + size_chunk chunk <= hi -> (align_chunk chunk | ofs) -> load chunk m2 b ofs = Some Vundef. Proof. intros. assert (exists v, load chunk m2 b ofs = Some v). apply valid_access_load. constructor; eauto with mem. rewrite low_bound_alloc_same. auto. rewrite high_bound_alloc_same. auto. - destruct H1 as [v LOAD]. rewrite LOAD. decEq. + destruct H2 as [v LOAD]. rewrite LOAD. decEq. eapply load_alloc_same; eauto. Qed. @@ -1089,7 +1154,7 @@ Lemma valid_access_free_1: valid_access m chunk b ofs -> b <> bf -> valid_access (free m bf) chunk b ofs. Proof. - intros. inv H. constructor. auto with mem. + intros. inv H. constructor; auto with mem. rewrite low_bound_free; auto. rewrite high_bound_free; auto. Qed. @@ -1180,6 +1245,7 @@ Proof. eapply proj_sumbool_true; eauto. change (size_chunk Mint8unsigned) with 1. generalize (proj_sumbool_true _ H1). omega. + simpl. apply Zone_divide. inv H. unfold proj_sumbool. rewrite zlt_true; auto. rewrite zle_true; auto. change (size_chunk Mint8unsigned) with 1 in H2. @@ -1215,13 +1281,6 @@ Definition meminj : Set := block -> option (block * Z). Variable val_inj: meminj -> val -> val -> Prop. -(* -Hypothesis val_inj_ptr: - forall mi b1 ofs1 b2 ofs2, - val_inj mi (Vptr b1 ofs1) (Vptr b2 ofs2) <-> - exists delta, mi b1 = Some(b2, delta) /\ ofs2 = Int.repr (Int.signed ofs1 + delta). -*) - Hypothesis val_inj_undef: forall mi, val_inj mi Vundef Vundef. @@ -1350,6 +1409,9 @@ Proof. replace v with Vundef by congruence. subst v2'. apply val_inj_undef. Qed. +Definition inj_offset_aligned (delta: Z) (size: Z) : Prop := + forall chunk, size_chunk chunk <= size -> (align_chunk chunk | delta). + Lemma alloc_parallel_inj: forall mi m1 m2 lo1 hi1 m1' b1 lo2 hi2 m2' b2 delta, mem_inj mi m1 m2 -> @@ -1357,24 +1419,26 @@ Lemma alloc_parallel_inj: alloc m2 lo2 hi2 = (m2', b2) -> mi b1 = Some(b2, delta) -> lo2 <= lo1 + delta -> hi1 + delta <= hi2 -> + inj_offset_aligned delta (hi1 - lo1) -> mem_inj mi m1' m2'. Proof. intros; red; intros. exploit (valid_access_alloc_inv m1); eauto with mem. - intros [A | [A [B C]]]. + intros [A | [A [B [C D]]]]. assert (load chunk m1 b0 ofs = Some v1). - rewrite <- H6. symmetry. eapply load_alloc_unchanged; eauto with mem. + rewrite <- H7. symmetry. eapply load_alloc_unchanged; eauto with mem. exploit H; eauto. intros [v2 [LOAD2 VINJ]]. exists v2; split. rewrite <- LOAD2. eapply load_alloc_unchanged; eauto with mem. auto. - subst b0. rewrite H2 in H5. inversion H5. subst b3 delta0. + subst b0. rewrite H2 in H6. inversion H6. subst b3 delta0. assert (v1 = Vundef). eapply load_alloc_same with (m1 := m1); eauto. subst v1. assert (exists v2, load chunk m2' b2 (ofs + delta) = Some v2). apply valid_access_load. - eapply valid_access_alloc_same; eauto. omega. omega. - destruct H7 as [v2 LOAD2]. + eapply valid_access_alloc_same; eauto. omega. omega. + apply Zdivide_plus_r; auto. apply H5. omega. + destruct H8 as [v2 LOAD2]. assert (v2 = Vundef). eapply load_alloc_same with (m1 := m2); eauto. subst v2. exists Vundef; split. auto. apply val_inj_undef. @@ -1420,19 +1484,21 @@ Lemma alloc_left_mapped_inj: mi b1 = Some(b2, delta) -> valid_block m2 b2 -> low_bound m2 b2 <= lo + delta -> hi + delta <= high_bound m2 b2 -> + inj_offset_aligned delta (hi - lo) -> mem_inj mi m1' m2. Proof. intros; red; intros. exploit (valid_access_alloc_inv m1); eauto with mem. - intros [A | [A [B C]]]. + intros [A | [A [B [C D]]]]. eapply H; eauto. - rewrite <- H6. symmetry. eapply load_alloc_unchanged; eauto with mem. - subst b0. rewrite H1 in H5. inversion H5. subst b3 delta0. + rewrite <- H7. symmetry. eapply load_alloc_unchanged; eauto with mem. + subst b0. rewrite H1 in H6. inversion H6. subst b3 delta0. assert (v1 = Vundef). eapply load_alloc_same with (m1 := m1); eauto. subst v1. assert (exists v2, load chunk m2 b2 (ofs + delta) = Some v2). apply valid_access_load. constructor. auto. omega. omega. - destruct H7 as [v2 LOAD2]. exists v2; split. auto. + apply Zdivide_plus_r; auto. apply H5. omega. + destruct H8 as [v2 LOAD2]. exists v2; split. auto. apply val_inj_undef_any. Qed. @@ -1547,6 +1613,7 @@ Proof. unfold val_inj_id; auto. unfold inject_id; eauto. omega. omega. + red; intros. apply Zdivide_0. Qed. Theorem free_extends: @@ -1716,6 +1783,7 @@ Proof. unfold val_inj_lessdef; auto. unfold inject_id; eauto. omega. omega. + red; intros. apply Zdivide_0. Qed. Lemma free_lessdef: @@ -1887,7 +1955,7 @@ Proof. rewrite valid_pointer_valid_access in H2. rewrite (address_inject _ _ _ _ _ _ _ _ H H1 H3). rewrite (address_inject _ _ _ _ _ _ _ _ H H2 H4). - inv H1. simpl in H7. inv H2. simpl in H9. + inv H1. simpl in H7. inv H2. simpl in H10. exploit (mi_no_overlap _ _ _ H); eauto. intros [A | [A | [A | [A | A]]]]. auto. omegaContradiction. omegaContradiction. @@ -2256,6 +2324,7 @@ Lemma alloc_mapped_inject: high_bound m2 b' <= Int.max_signed -> low_bound m2 b' <= lo + ofs -> hi + ofs <= high_bound m2 b' -> + inj_offset_aligned ofs (hi-lo) -> (forall b0 ofs0, f b0 = Some (b', ofs0) -> high_bound m1 b0 + ofs0 <= lo + ofs \/ @@ -2270,34 +2339,34 @@ Proof. constructor. (* inj *) eapply alloc_left_mapped_inj; eauto. - red; intros. unfold extend_inject in H9. - rewrite zeq_false in H9. + red; intros. unfold extend_inject in H10. + rewrite zeq_false in H10. exploit mi_inj0; eauto. intros [v2 [LOAD VINJ]]. exists v2; split. auto. eapply val_inject_incr; eauto. eauto with mem. unfold extend_inject. apply zeq_true. (* freeblocks *) intros. unfold extend_inject. rewrite zeq_false. - apply mi_freeblocks0. red; intro. elim H9; eauto with mem. + apply mi_freeblocks0. red; intro. elim H10; eauto with mem. apply sym_not_equal; eauto with mem. (* mappedblocks *) unfold extend_inject; intros. - destruct (zeq b0 b). inv H9. auto. eauto. + destruct (zeq b0 b). inv H10. auto. eauto. (* overlap *) red; unfold extend_inject, update; intros. repeat rewrite (low_bound_alloc _ _ _ _ _ H0). repeat rewrite (high_bound_alloc _ _ _ _ _ H0). - destruct (zeq b1 b); [inv H10|idtac]; - (destruct (zeq b2 b); [inv H11|idtac]). + destruct (zeq b1 b); [inv H11|idtac]; + (destruct (zeq b2 b); [inv H12|idtac]). congruence. - destruct (zeq b1' b2'). subst b2'. generalize (H7 _ _ H11). tauto. auto. - destruct (zeq b1' b2'). subst b2'. generalize (H7 _ _ H10). tauto. auto. + destruct (zeq b1' b2'). subst b2'. generalize (H8 _ _ H12). tauto. auto. + destruct (zeq b1' b2'). subst b2'. generalize (H8 _ _ H11). tauto. auto. eauto. (* range *) unfold extend_inject; intros. - destruct (zeq b0 b). inv H9. auto. eauto. + destruct (zeq b0 b). inv H10. auto. eauto. unfold extend_inject; intros. - destruct (zeq b0 b). inv H9. auto. eauto. + destruct (zeq b0 b). inv H10. auto. eauto. Qed. Lemma alloc_parallel_inject: @@ -2318,6 +2387,7 @@ Proof. rewrite (high_bound_alloc_same _ _ _ _ _ H1). auto. rewrite (low_bound_alloc_same _ _ _ _ _ H1). omega. rewrite (high_bound_alloc_same _ _ _ _ _ H1). omega. + red; intros. apply Zdivide_0. intros. elimtype False. inv H. exploit mi_mappedblocks0; eauto. change (~ valid_block m2 b2). eauto with mem. @@ -2406,6 +2476,7 @@ Proof. unfold low_bound; rewrite <- B; simpl; rewrite A. rewrite update_o; auto. replace (high_bound m b0) with (high_bound m' b0). auto. unfold high_bound; rewrite <- B; simpl; rewrite A. rewrite update_o; auto. + auto. Qed. (** ** Memory shifting *) @@ -2415,21 +2486,6 @@ Qed. Definition memshift := block -> option Z. -(* -Inductive val_shift (mi: memshift): val -> val -> Prop := - | val_shift_int: - forall i, val_shift mi (Vint i) (Vint i) - | val_shift_float: - forall f, val_shift mi (Vfloat f) (Vfloat f) - | val_shift_ptr: - forall b ofs1 ofs2 x, - mi b = Some x -> - ofs2 = Int.add ofs1 (Int.repr x) -> - val_shift mi (Vptr b ofs1) (Vptr b ofs2) - | val_shift_undef: - val_shift mi Vundef Vundef. -*) - Definition meminj_of_shift (mi: memshift) : meminj := fun b => match mi b with None => None | Some x => Some (b, x) end. @@ -2688,6 +2744,7 @@ Lemma alloc_shift: lo2 <= lo1 + delta -> hi1 + delta <= hi2 -> Int.min_signed <= delta <= Int.max_signed -> Int.min_signed <= lo2 -> hi2 <= Int.max_signed -> + inj_offset_aligned delta (hi1-lo1) -> exists f', exists m2', alloc m2 lo2 hi2 = (m2', b) /\ mem_shift f' m1' m2' @@ -2719,7 +2776,7 @@ Proof. assert (mem_inj val_inject (meminj_of_shift f') m1 m2). red; intros. assert (meminj_of_shift f b1 = Some (b2, delta0)). - rewrite <- H7. unfold meminj_of_shift, f'. + rewrite <- H8. unfold meminj_of_shift, f'. destruct (zeq b1 b); auto. subst b1. assert (valid_block m1 b) by eauto with mem. @@ -2753,3 +2810,58 @@ Proof. unfold f'. apply zeq_true. Qed. +(** ** Relation between signed and unsigned loads and stores *) + +(** Target processors do not distinguish between signed and unsigned + stores of 8- and 16-bit quantities. We show these are equivalent. *) + +(** Signed 8- and 16-bit stores can be performed like unsigned stores. *) + +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_compat; eauto. + destruct (in_bounds m chunk2 b ofs); auto. + elim n. eapply valid_access_compat with (chunk1 := chunk2); eauto. +Qed. + +Lemma storev_8_signed_unsigned: + forall m a v, + storev Mint8signed m a v = 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, + storev Mint16signed m a v = storev Mint16unsigned m a v. +Proof. + intros. unfold storev. destruct a; auto. + unfold store. rewrite (in_bounds_equiv Mint16signed Mint16unsigned). + auto. auto. +Qed. + +(** Likewise, some target processors (e.g. the PowerPC) do not have + a ``load 8-bit signed integer'' instruction. + We show that it can be synthesized as a ``load 8-bit unsigned integer'' + followed by a sign extension. *) + +Lemma loadv_8_signed_unsigned: + forall m a, + loadv Mint8signed m a = option_map (Val.sign_ext 8) (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. + diff --git a/driver/Complements.v b/driver/Complements.v index fc2fa533..938c4888 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -240,26 +240,6 @@ Qed. (** ** Determinism for terminating executions. *) -(* -Lemma star_star_inv: - forall ge s t1 s1, star step ge s t1 s1 -> - forall t2 s2 w w1 w2, star step ge s t2 s2 -> - possible_trace w t1 w1 -> possible_trace w t2 w2 -> - exists t, (star step ge s1 t s2 /\ t2 = t1 ** t) - \/ (star step ge s2 t s1 /\ t1 = t2 ** t). -Proof. - induction 1; intros. - exists t2; left; split; auto. - inv H2. exists (t1 ** t2); right; split. econstructor; eauto. auto. - possibleTraceInv. - exploit step_deterministic. eexact H. eexact H5. eauto. eauto. - intros [U [V W]]. subst s5 t3 w3. - exploit IHstar; eauto. intros [t [ [Q R] | [Q R] ]]. - subst t4. exists t; left; split. auto. traceEq. - subst t2. exists t; right; split. auto. traceEq. -Qed. -*) - Lemma steps_deterministic: forall ge s0 t1 s1, star step ge s0 t1 s1 -> forall r1 r2 t2 s2 w0 w1 w2, star step ge s0 t2 s2 -> diff --git a/lib/Coqlib.v b/lib/Coqlib.v index ff6e9ae8..a79ea29c 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -18,6 +18,7 @@ library. *) Require Export ZArith. +Require Export Znumtheory. Require Export List. Require Export Bool. Require Import Wf_nat. @@ -526,6 +527,25 @@ Proof. omega. Qed. +(** Properties of divisibility. *) + +Lemma Zdivides_trans: + forall x y z, (x | y) -> (y | z) -> (x | z). +Proof. + intros. inv H. inv H0. exists (q0 * q). ring. +Qed. + +Definition Zdivide_dec: + forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }. +Proof. + intros. destruct (zeq (Zmod q p) 0). + left. exists (q / p). + transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto. + transitivity (p * (q / p)). omega. ring. + right; red; intros. elim n. apply Z_div_exact_1; auto. + inv H0. rewrite Z_div_mult; auto. ring. +Qed. + (** Alignment: [align n amount] returns the smallest multiple of [amount] greater than or equal to [n]. *) @@ -542,6 +562,11 @@ Proof. rewrite Zmult_comm. omega. Qed. +Lemma align_divides: forall x y, y > 0 -> (y | align x y). +Proof. + intros. unfold align. apply Zdivide_factor_l. +Qed. + (** * Definitions and theorems on the data types [option], [sum] and [list] *) Set Implicit Arguments. diff --git a/lib/Integers.v b/lib/Integers.v index a9644bcc..ff29d2a5 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -2252,59 +2252,6 @@ Proof. rewrite <- two_p_is_exp. unfold modulus. rewrite two_power_nat_two_p. decEq. omega. omega. omega. Qed. -(* -Lemma zero_ext_charact: - forall x y, - zero_ext n x = y <-> - 0 <= unsigned y < two_p n /\ eqmod (two_p n) (unsigned x) (unsigned y). -Proof. - intros. unfold zero_ext. set (x' := unsigned x). split; intros. - subst y. - assert (0 <= x' mod two_p n < two_p n). apply Z_mod_lt. apply two_p_n_pos. - rewrite unsigned_repr. split. auto. - apply eqmod_mod. apply two_p_n_pos. - generalize two_p_n_range. omega. - destruct H. destruct H0 as [k EQ]. - assert (x' mod two_p n = unsigned y). - apply Zmod_unique with k; auto. - rewrite H0. apply repr_unsigned. -Qed. - -Lemma sign_ext_charact: - forall x y, - sign_ext n x = y <-> - -(two_p (n-1)) <= signed y < two_p (n-1) - /\ eqmod (two_p n) (unsigned x) (signed y). -Proof. - intros. unfold sign_ext. set (x' := unsigned x). split; intros. - assert (0 <= x' mod two_p n < two_p n). apply Z_mod_lt. apply two_p_n_pos. - destruct (zlt (x' mod two_p n) (two_p (n - 1))); subst y. - rewrite signed_repr. split. omega. - apply eqmod_mod. apply two_p_n_pos. - assert (min_signed < 0). vm_compute; auto. - generalize two_p_n_range'. omega. - rewrite signed_repr. split. - assert (two_p n = 2 * two_p (n-1)). rewrite <- two_p_S. decEq. omega. omega. - omega. - apply eqmod_trans with (x' - 0). apply eqmod_refl2. omega. - apply eqmod_sub. apply eqmod_mod. apply two_p_n_pos. - exists (-1). ring. - split. generalize two_p_n_range'. - change (max_signed + 1) with (- min_signed). omega. - generalize two_p_n_range'. omega. - - destruct H. destruct H0 as [k EQ]. - assert (two_p n = 2 * two_p (n - 1)). rewrite <- two_p_S. decEq. omega. omega. - assert (signed y >= 0 \/ signed y < 0) by omega. destruct H1. - assert (x' mod two_p n = signed y). - apply Zmod_unique with k; auto. omega. - rewrite zlt_true. rewrite H2. apply repr_signed. omega. - assert (x' mod two_p n = signed y + two_p n). - apply Zmod_unique with (k-1). rewrite EQ. ring. omega. - rewrite zlt_false. replace (x' mod two_p n - two_p n) with (signed y) by omega. apply repr_signed. - omega. -Qed. -*) Lemma sign_ext_charact: forall x y, 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. |