From b40e056328e183522b50c68aefdbff057bca29cc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 16 Jun 2013 06:56:02 +0000 Subject: Merge of the "princeton" branch: - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Asmgenproof0.v | 4 +- backend/Constpropproof.v | 10 ++-- backend/Inlining.v | 2 - backend/Inliningproof.v | 147 +++++++++++++++++++++++------------------------ backend/Inliningspec.v | 6 +- backend/Mach.v | 2 +- backend/Stackingproof.v | 143 ++++++++++++++++++++++----------------------- 7 files changed, 153 insertions(+), 161 deletions(-) (limited to 'backend') diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index f74fba8..3801a4f 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -844,10 +844,10 @@ Inductive match_stack: list Mach.stackframe -> Prop := match_stack (Stackframe fb sp ra c :: s). Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. -Proof. induction 1; simpl. congruence. auto. Qed. +Proof. induction 1; simpl. unfold Vzero; congruence. auto. Qed. Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. -Proof. induction 1; simpl. unfold Vzero. congruence. inv H0. congruence. Qed. +Proof. induction 1; simpl. unfold Vzero; congruence. inv H0. congruence. Qed. Lemma lessdef_parent_sp: forall s v, diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index a6385f4..2d11d94 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -255,7 +255,7 @@ Proof. intros. eapply Mem.load_alloc_unchanged; eauto. split. eauto with mem. intros; red; intros. exploit Mem.perm_alloc_inv; eauto. - rewrite zeq_false. apply C. eapply Mem.valid_not_valid_diff; eauto with mem. + rewrite dec_eq_false. apply C. eapply Mem.valid_not_valid_diff; eauto with mem. Qed. Lemma mem_match_approx_free: @@ -267,7 +267,7 @@ Proof. intros; red; intros. exploit H; eauto. intros [A [B C]]. split. apply Genv.load_store_init_data_invariant with m; auto. intros. eapply Mem.load_free; eauto. - destruct (zeq b0 b); auto. subst b0. + destruct (eq_block b0 b); auto. subst b0. right. destruct (zlt lo hi); auto. elim (C lo). apply Mem.perm_cur_max. exploit Mem.free_range_perm; eauto. instantiate (1 := lo); omega. @@ -323,10 +323,10 @@ Proof. unfold Genv.add_global, Genv.find_symbol, Genv.find_var_info in *; simpl in *. destruct EITHER as [[A B] | [A B]]. - subst id0. rewrite PTree.gss in H1. inv H1. rewrite ZMap.gss. auto. + subst id0. rewrite PTree.gss in H1. inv H1. rewrite PTree.gss. auto. rewrite PTree.gso in H1; auto. destruct gd. eapply H; eauto. - rewrite ZMap.gso. eapply H; eauto. - exploit Genv.genv_symb_range; eauto. unfold ZIndexed.t. omega. + rewrite PTree.gso. eapply H; eauto. + red; intros; subst b. eelim Plt_strict; eapply Genv.genv_symb_range; eauto. Qed. Theorem mem_match_approx_init: diff --git a/backend/Inlining.v b/backend/Inlining.v index 7b19f80..683d190 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -22,8 +22,6 @@ Require Import Op. Require Import Registers. Require Import RTL. -Ltac xomega := unfold Plt, Ple in *; zify; omega. - (** ** Environment of inlinable functions *) (** We maintain a mapping from function names to their definitions. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index ba61ed0..15d0b28 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -291,7 +291,7 @@ Proof. exploit (H ofs). generalize (Zmax2 sz 0). omega. intros [A B]. split; auto. intros; red; intros. exploit Mem.perm_alloc_inv; eauto. - destruct (zeq b sp); intros. + destruct (eq_block b sp); intros. subst b. rewrite H1 in H4; inv H4. rewrite Zmax_spec in H3. destruct (zlt 0 sz); omega. rewrite H2 in H4; auto. eelim B; eauto. @@ -331,7 +331,7 @@ Lemma range_private_extcall: range_private F m1 m1' sp base hi -> (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> - mem_unchanged_on (loc_out_of_reach F m1) m1' m2' -> + Mem.unchanged_on (loc_out_of_reach F m1) m1' m2' -> Mem.inject F m1 m1' -> inject_incr F F' -> inject_separated F F' m1 m1' -> @@ -340,26 +340,24 @@ Lemma range_private_extcall: Proof. intros until hi; intros RP PERM UNCH INJ INCR SEP VB. red; intros. exploit RP; eauto. intros [A B]. - destruct UNCH as [U1 U2]. - split. auto. + split. eapply Mem.perm_unchanged_on; eauto. intros. red in SEP. destruct (F b) as [[sp1 delta1] |] eqn:?. exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. red; intros; eelim B; eauto. eapply PERM; eauto. - red. destruct (zlt b (Mem.nextblock m1)); auto. + red. destruct (plt b (Mem.nextblock m1)); auto. exploit Mem.mi_freeblocks; eauto. congruence. exploit SEP; eauto. tauto. Qed. (** ** Relating global environments *) -Inductive match_globalenvs (F: meminj) (bound: Z): Prop := +Inductive match_globalenvs (F: meminj) (bound: block): Prop := | mk_match_globalenvs - (POS: bound > 0) - (DOMAIN: forall b, b < bound -> F b = Some(b, 0)) - (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) - (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound) - (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound) - (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). + (DOMAIN: forall b, Plt b bound -> F b = Some(b, 0)) + (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2) + (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound) + (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound) + (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound). Lemma find_function_agree: forall ros rs fd F ctx rs' bound, @@ -390,7 +388,7 @@ Inductive match_stacks (F: meminj) (m m': mem): list stackframe -> list stackframe -> block -> Prop := | match_stacks_nil: forall bound1 bound (MG: match_globalenvs F bound1) - (BELOW: bound1 <= bound), + (BELOW: Ple bound1 bound), match_stacks F m m' nil nil bound | match_stacks_cons: forall res f sp pc rs stk f' sp' rs' stk' bound ctx (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs') @@ -401,7 +399,7 @@ Inductive match_stacks (F: meminj) (m m': mem): (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned) (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)) (RES: Ple res ctx.(mreg)) - (BELOW: sp' < bound), + (BELOW: Plt sp' bound), match_stacks F m m' (Stackframe res f (Vptr sp Int.zero) pc rs :: stk) (Stackframe (sreg ctx res) f' (Vptr sp' Int.zero) (spc ctx pc) rs' :: stk') @@ -412,7 +410,7 @@ Inductive match_stacks (F: meminj) (m m': mem): (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned) (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)) (RET: ctx.(retinfo) = Some (rpc, res)) - (BELOW: sp' < bound), + (BELOW: Plt sp' bound), match_stacks F m m' stk (Stackframe res f' (Vptr sp' Int.zero) rpc rs' :: stk') @@ -474,13 +472,13 @@ Qed. Lemma match_stacks_bound: forall stk stk' bound bound1, match_stacks F m m' stk stk' bound -> - bound <= bound1 -> + Ple bound bound1 -> match_stacks F m m' stk stk' bound1. Proof. intros. inv H. - apply match_stacks_nil with bound0. auto. omega. - eapply match_stacks_cons; eauto. omega. - eapply match_stacks_untailcall; eauto. omega. + apply match_stacks_nil with bound0. auto. eapply Ple_trans; eauto. + eapply match_stacks_cons; eauto. eapply Plt_le_trans; eauto. + eapply match_stacks_untailcall; eauto. eapply Plt_le_trans; eauto. Qed. Variable F1: meminj. @@ -490,13 +488,13 @@ Hypothesis INCR: inject_incr F F1. Lemma match_stacks_invariant: forall stk stk' bound, match_stacks F m m' stk stk' bound -> forall (INJ: forall b1 b2 delta, - F1 b1 = Some(b2, delta) -> b2 < bound -> F b1 = Some(b2, delta)) + F1 b1 = Some(b2, delta) -> Plt b2 bound -> F b1 = Some(b2, delta)) (PERM1: forall b1 b2 delta ofs, - F1 b1 = Some(b2, delta) -> b2 < bound -> + F1 b1 = Some(b2, delta) -> Plt b2 bound -> Mem.perm m1 b1 ofs Max Nonempty -> Mem.perm m b1 ofs Max Nonempty) - (PERM2: forall b ofs, b < bound -> + (PERM2: forall b ofs, Plt b bound -> Mem.perm m' b ofs Cur Freeable -> Mem.perm m1' b ofs Cur Freeable) - (PERM3: forall b ofs k p, b < bound -> + (PERM3: forall b ofs k p, Plt b bound -> Mem.perm m1' b ofs k p -> Mem.perm m' b ofs k p), match_stacks F1 m1 m1' stk stk' bound @@ -506,13 +504,13 @@ with match_stacks_inside_invariant: forall rs2 (RS: forall r, Ple r ctx.(dreg) -> rs2#r = rs1#r) (INJ: forall b1 b2 delta, - F1 b1 = Some(b2, delta) -> b2 <= sp' -> F b1 = Some(b2, delta)) + F1 b1 = Some(b2, delta) -> Ple b2 sp' -> F b1 = Some(b2, delta)) (PERM1: forall b1 b2 delta ofs, - F1 b1 = Some(b2, delta) -> b2 <= sp' -> + F1 b1 = Some(b2, delta) -> Ple b2 sp' -> Mem.perm m1 b1 ofs Max Nonempty -> Mem.perm m b1 ofs Max Nonempty) - (PERM2: forall b ofs, b <= sp' -> + (PERM2: forall b ofs, Ple b sp' -> Mem.perm m' b ofs Cur Freeable -> Mem.perm m1' b ofs Cur Freeable) - (PERM3: forall b ofs k p, b <= sp' -> + (PERM3: forall b ofs k p, Ple b sp' -> Mem.perm m1' b ofs k p -> Mem.perm m' b ofs k p), match_stacks_inside F1 m1 m1' stk stk' f' ctx sp' rs2. @@ -521,34 +519,34 @@ Proof. (* nil *) apply match_stacks_nil with (bound1 := bound1). inv MG. constructor; auto. - intros. apply IMAGE with delta. eapply INJ; eauto. omega. auto. - omega. + intros. apply IMAGE with delta. eapply INJ; eauto. eapply Plt_le_trans; eauto. + auto. auto. (* cons *) apply match_stacks_cons with (ctx := ctx); auto. eapply match_stacks_inside_invariant; eauto. - intros; eapply INJ; eauto; omega. - intros; eapply PERM1; eauto; omega. - intros; eapply PERM2; eauto; omega. - intros; eapply PERM3; eauto; omega. + intros; eapply INJ; eauto; xomega. + intros; eapply PERM1; eauto; xomega. + intros; eapply PERM2; eauto; xomega. + intros; eapply PERM3; eauto; xomega. eapply agree_regs_incr; eauto. eapply range_private_invariant; eauto. (* untailcall *) apply match_stacks_untailcall with (ctx := ctx); auto. eapply match_stacks_inside_invariant; eauto. - intros; eapply INJ; eauto; omega. - intros; eapply PERM1; eauto; omega. - intros; eapply PERM2; eauto; omega. - intros; eapply PERM3; eauto; omega. + intros; eapply INJ; eauto; xomega. + intros; eapply PERM1; eauto; xomega. + intros; eapply PERM2; eauto; xomega. + intros; eapply PERM3; eauto; xomega. eapply range_private_invariant; eauto. induction 1; intros. (* base *) eapply match_stacks_inside_base; eauto. eapply match_stacks_invariant; eauto. - intros; eapply INJ; eauto; omega. - intros; eapply PERM1; eauto; omega. - intros; eapply PERM2; eauto; omega. - intros; eapply PERM3; eauto; omega. + intros; eapply INJ; eauto; xomega. + intros; eapply PERM1; eauto; xomega. + intros; eapply PERM2; eauto; xomega. + intros; eapply PERM3; eauto; xomega. (* inlined *) apply match_stacks_inside_inlined with (ctx' := ctx'); auto. apply IHmatch_stacks_inside; auto. @@ -557,8 +555,8 @@ Proof. apply agree_regs_invariant with rs'; auto. intros. apply RS. red in BELOW. xomega. eapply range_private_invariant; eauto. - intros. split. eapply INJ; eauto. omega. eapply PERM1; eauto. omega. - intros. eapply PERM2; eauto. omega. + intros. split. eapply INJ; eauto. xomega. eapply PERM1; eauto. xomega. + intros. eapply PERM2; eauto. xomega. Qed. Lemma match_stacks_empty: @@ -621,17 +619,17 @@ Proof. eapply match_stacks_inside_base; eauto. eapply match_stacks_invariant; eauto. intros. destruct (eq_block b1 b). - subst b1. rewrite H1 in H4; inv H4. omegaContradiction. + subst b1. rewrite H1 in H4; inv H4. eelim Plt_strict; eauto. rewrite H2 in H4; auto. - intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b1 b); intros; auto. - subst b1. rewrite H1 in H4. inv H4. omegaContradiction. + intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b1 b); intros; auto. + subst b1. rewrite H1 in H4. inv H4. eelim Plt_strict; eauto. (* inlined *) eapply match_stacks_inside_inlined; eauto. eapply IHmatch_stacks_inside; eauto. destruct SBELOW. omega. eapply agree_regs_incr; eauto. eapply range_private_invariant; eauto. - intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b0 b); intros. - subst b0. rewrite H2 in H5; inv H5. omegaContradiction. + intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b0 b); intros. + subst b0. rewrite H2 in H5; inv H5. elimtype False; xomega. rewrite H3 in H5; auto. Qed. @@ -654,7 +652,7 @@ Lemma match_stacks_free_right: match_stacks F m m1' stk stk' sp. Proof. intros. eapply match_stacks_invariant; eauto. - intros. eapply Mem.perm_free_1; eauto. left. unfold block; omega. + intros. eapply Mem.perm_free_1; eauto. intros. eapply Mem.perm_free_3; eauto. Qed. @@ -691,7 +689,7 @@ Variables F1 F2: meminj. Variables m1 m2 m1' m2': mem. Hypothesis MAXPERM: forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p. Hypothesis MAXPERM': forall b ofs p, Mem.valid_block m1' b -> Mem.perm m2' b ofs Max p -> Mem.perm m1' b ofs Max p. -Hypothesis UNCHANGED: mem_unchanged_on (loc_out_of_reach F1 m1) m1' m2'. +Hypothesis UNCHANGED: Mem.unchanged_on (loc_out_of_reach F1 m1) m1' m2'. Hypothesis INJ: Mem.inject F1 m1 m1'. Hypothesis INCR: inject_incr F1 F2. Hypothesis SEP: inject_separated F1 F2 m1 m1'. @@ -699,12 +697,12 @@ Hypothesis SEP: inject_separated F1 F2 m1 m1'. Lemma match_stacks_extcall: forall stk stk' bound, match_stacks F1 m1 m1' stk stk' bound -> - bound <= Mem.nextblock m1' -> + Ple bound (Mem.nextblock m1') -> match_stacks F2 m2 m2' stk stk' bound with match_stacks_inside_extcall: forall stk stk' f' ctx sp' rs', match_stacks_inside F1 m1 m1' stk stk' f' ctx sp' rs' -> - sp' < Mem.nextblock m1' -> + Plt sp' (Mem.nextblock m1') -> match_stacks_inside F2 m2 m2' stk stk' f' ctx sp' rs'. Proof. induction 1; intros. @@ -712,19 +710,19 @@ Proof. inv MG. constructor; intros; eauto. destruct (F1 b1) as [[b2' delta']|] eqn:?. exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eapply IMAGE; eauto. - exploit SEP; eauto. intros [A B]. elim B. red. omega. + exploit SEP; eauto. intros [A B]. elim B. red. xomega. eapply match_stacks_cons; eauto. - eapply match_stacks_inside_extcall; eauto. omega. + eapply match_stacks_inside_extcall; eauto. xomega. eapply agree_regs_incr; eauto. - eapply range_private_extcall; eauto. red; omega. - intros. apply SSZ2; auto. apply MAXPERM'; auto. red; omega. + eapply range_private_extcall; eauto. red; xomega. + intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega. eapply match_stacks_untailcall; eauto. - eapply match_stacks_inside_extcall; eauto. omega. - eapply range_private_extcall; eauto. red; omega. - intros. apply SSZ2; auto. apply MAXPERM'; auto. red; omega. + eapply match_stacks_inside_extcall; eauto. xomega. + eapply range_private_extcall; eauto. red; xomega. + intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega. induction 1; intros. eapply match_stacks_inside_base; eauto. - eapply match_stacks_extcall; eauto. omega. + eapply match_stacks_extcall; eauto. xomega. eapply match_stacks_inside_inlined; eauto. eapply agree_regs_incr; eauto. eapply range_private_extcall; eauto. @@ -952,9 +950,9 @@ Proof. eapply match_stacks_bound with (bound := sp'). eapply match_stacks_invariant; eauto. intros. eapply Mem.perm_free_3; eauto. - intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. + intros. eapply Mem.perm_free_1; eauto. intros. eapply Mem.perm_free_3; eauto. - erewrite Mem.nextblock_free; eauto. red in VB; omega. + erewrite Mem.nextblock_free; eauto. red in VB; xomega. eapply agree_val_regs; eauto. eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto. (* show that no valid location points into the stack block being freed *) @@ -1048,9 +1046,9 @@ Proof. eapply match_stacks_bound with (bound := sp'). eapply match_stacks_invariant; eauto. intros. eapply Mem.perm_free_3; eauto. - intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. + intros. eapply Mem.perm_free_1; eauto. intros. eapply Mem.perm_free_3; eauto. - erewrite Mem.nextblock_free; eauto. red in VB; omega. + erewrite Mem.nextblock_free; eauto. red in VB; xomega. destruct or; simpl. apply agree_val_reg; auto. auto. eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto. (* show that no valid location points into the stack block being freed *) @@ -1085,25 +1083,25 @@ Proof. rewrite <- SP in MS0. eapply match_stacks_invariant; eauto. intros. destruct (eq_block b1 stk). - subst b1. rewrite D in H7; inv H7. unfold block in *; omegaContradiction. + subst b1. rewrite D in H7; inv H7. subst b2. eelim Plt_strict; eauto. rewrite E in H7; auto. intros. exploit Mem.perm_alloc_inv. eexact H. eauto. - destruct (zeq b1 stk); intros; auto. - subst b1. rewrite D in H7; inv H7. unfold block in *; omegaContradiction. + destruct (eq_block b1 stk); intros; auto. + subst b1. rewrite D in H7; inv H7. subst b2. eelim Plt_strict; eauto. intros. eapply Mem.perm_alloc_1; eauto. intros. exploit Mem.perm_alloc_inv. eexact A. eauto. - rewrite zeq_false; auto. unfold block; omega. + rewrite dec_eq_false; auto. auto. auto. auto. rewrite H4. apply agree_regs_init_regs. eauto. auto. inv H0; auto. congruence. auto. eapply Mem.valid_new_block; eauto. red; intros. split. eapply Mem.perm_alloc_2; eauto. inv H0; xomega. intros; red; intros. exploit Mem.perm_alloc_inv. eexact H. eauto. - destruct (zeq b stk); intros. + destruct (eq_block b stk); intros. subst. rewrite D in H8; inv H8. inv H0; xomega. rewrite E in H8; auto. eelim Mem.fresh_block_alloc. eexact A. eapply Mem.mi_mappedblocks; eauto. auto. - intros. exploit Mem.perm_alloc_inv; eauto. rewrite zeq_true. omega. + intros. exploit Mem.perm_alloc_inv; eauto. rewrite dec_eq_true. omega. (* internal function, inlined *) inversion FB; subst. @@ -1156,7 +1154,7 @@ Proof. eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. intros; eapply external_call_max_perm; eauto. intros; eapply external_call_max_perm; eauto. - omega. + xomega. eapply external_call_nextblock; eauto. auto. auto. @@ -1217,13 +1215,12 @@ Proof. instantiate (1 := Mem.flat_inj (Mem.nextblock m0)). apply match_stacks_nil with (Mem.nextblock m0). constructor; intros. - apply Mem.nextblock_pos. - unfold Mem.flat_inj. apply zlt_true; auto. - unfold Mem.flat_inj in H. destruct (zlt b1 (Mem.nextblock m0)); congruence. + unfold Mem.flat_inj. apply pred_dec_true; auto. + unfold Mem.flat_inj in H. destruct (plt b1 (Mem.nextblock m0)); congruence. eapply Genv.find_symbol_not_fresh; eauto. eapply Genv.find_funct_ptr_not_fresh; eauto. eapply Genv.find_var_info_not_fresh; eauto. - omega. + apply Ple_refl. eapply Genv.initmem_inject; eauto. Qed. diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index e8dba67..f41f376 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -46,17 +46,17 @@ Proof. (* same *) subst id0. inv H1. destruct gd. destruct f0. destruct (should_inline id f0). - rewrite PTree.gss in H0. rewrite ZMap.gss. inv H0; auto. + rewrite PTree.gss in H0. rewrite PTree.gss. inv H0; auto. rewrite PTree.grs in H0; discriminate. rewrite PTree.grs in H0; discriminate. rewrite PTree.grs in H0; discriminate. (* different *) - destruct gd. rewrite ZMap.gso. eapply H; eauto. + destruct gd. rewrite PTree.gso. eapply H; eauto. destruct f0. destruct (should_inline id f0). rewrite PTree.gso in H0; auto. rewrite PTree.gro in H0; auto. rewrite PTree.gro in H0; auto. - exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega. + red; intros; subst b. eelim Plt_strict. eapply Genv.genv_symb_range; eauto. rewrite PTree.gro in H0; auto. eapply H; eauto. Qed. diff --git a/backend/Mach.v b/backend/Mach.v index 316e788..f0fb56a 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -273,7 +273,7 @@ Inductive state: Type := Definition parent_sp (s: list stackframe) : val := match s with - | nil => Vptr Mem.nullptr Int.zero + | nil => Vzero | Stackframe f sp ra c :: s' => sp end. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index dfa81d8..9b144cb 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -967,7 +967,7 @@ Lemma agree_frame_extcall_invariant: (Mem.valid_block m sp -> Mem.valid_block m1 sp) -> (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') -> - mem_unchanged_on (loc_out_of_reach j m) m' m1' -> + Mem.unchanged_on (loc_out_of_reach j m) m' m1' -> agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. Proof. intros. @@ -977,8 +977,8 @@ Proof. intros; red; intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst. red; intros. exploit agree_bounds; eauto. omega. eapply agree_frame_invariant; eauto. - intros. apply H3. intros. apply REACH. omega. auto. - intros. apply H3; auto. + intros. eapply Mem.load_unchanged_on; eauto. intros. apply REACH. omega. auto. + intros. eapply Mem.perm_unchanged_on; eauto with mem. auto. Qed. (** Preservation by parallel stores in the Linear and Mach codes *) @@ -1000,7 +1000,7 @@ Opaque Int.add. eauto with mem. eauto with mem. intros. rewrite <- H1. eapply Mem.load_store_other; eauto. - destruct (zeq sp' b2); auto. + destruct (eq_block sp' b2); auto. subst b2. right. exploit agree_inj_unique; eauto. intros [P Q]. subst b1 delta. exploit Mem.store_valid_access_3. eexact STORE1. intros [A B]. @@ -1462,13 +1462,13 @@ Proof. Qed. Lemma stores_in_frame_contents: - forall chunk b ofs sp, b < sp -> + forall chunk b ofs sp, Plt b sp -> forall m m', stores_in_frame sp m m' -> Mem.load chunk m' b ofs = Mem.load chunk m b ofs. Proof. induction 2. auto. rewrite IHstores_in_frame. eapply Mem.load_store_other; eauto. - left; unfold block; omega. + left. apply Plt_ne; auto. Qed. (** As a corollary of the previous lemmas, we obtain the following @@ -1512,7 +1512,7 @@ Proof. instantiate (1 := fe_stack_data fe). generalize stack_data_offset_valid (bound_stack_data_pos b) size_no_overflow; omega. intros; right. - exploit Mem.perm_alloc_inv. eexact ALLOC'. eauto. rewrite zeq_true. + exploit Mem.perm_alloc_inv. eexact ALLOC'. eauto. rewrite dec_eq_true. generalize size_no_overflow. omega. intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. @@ -1552,7 +1552,7 @@ Proof. rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; auto. red; auto. (* separation *) assert (SEP: forall b0 delta, j' b0 = Some(sp', delta) -> b0 = sp /\ delta = fe_stack_data fe). - intros. destruct (zeq b0 sp). + intros. destruct (eq_block b0 sp). subst b0. rewrite MAP1 in H; inv H; auto. rewrite MAP2 in H; auto. assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto. @@ -1619,7 +1619,7 @@ Proof. (* valid sp' *) eapply stores_in_frame_valid with (m := m2'); eauto with mem. (* bounds *) - exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto. + exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite dec_eq_true. auto. (* perms *) auto. (* wt *) @@ -1630,7 +1630,7 @@ Proof. split. eapply inject_alloc_separated; eauto with mem. (* inject *) split. eapply stores_in_frame_inject; eauto. - intros. exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto. + intros. exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite dec_eq_true. auto. (* stores in frame *) auto. Qed. @@ -1850,19 +1850,18 @@ End FRAME_PROPERTIES. (** * Call stack invariant *) -Inductive match_globalenvs (j: meminj) (bound: Z) : Prop := +Inductive match_globalenvs (j: meminj) (bound: block) : Prop := | match_globalenvs_intro - (POS: bound > 0) - (DOMAIN: forall b, b < bound -> j b = Some(b, 0)) - (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) - (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound) - (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound) - (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). + (DOMAIN: forall b, Plt b bound -> j b = Some(b, 0)) + (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2) + (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound) + (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound) + (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound). Inductive match_stacks (j: meminj) (m m': mem): - list Linear.stackframe -> list stackframe -> signature -> Z -> Z -> Prop := + list Linear.stackframe -> list stackframe -> signature -> block -> block -> Prop := | match_stacks_empty: forall sg hi bound bound', - hi <= bound -> hi <= bound' -> match_globalenvs j hi -> + Ple hi bound -> Ple hi bound' -> match_globalenvs j hi -> tailcall_possible sg -> match_stacks j m m' nil nil sg bound bound' | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg bound bound' trf @@ -1877,8 +1876,8 @@ Inductive match_stacks (j: meminj) (m m': mem): In (S Outgoing ofs ty) (loc_arguments sg) -> slot_within_bounds (function_bounds f) Outgoing ofs ty) (STK: match_stacks j m m' cs cs' (Linear.fn_sig f) sp sp') - (BELOW: sp < bound) - (BELOW': sp' < bound'), + (BELOW: Plt sp bound) + (BELOW': Plt sp' bound'), match_stacks j m m' (Linear.Stackframe f (Vptr sp Int.zero) ls c :: cs) (Stackframe fb (Vptr sp' Int.zero) ra c' :: cs') @@ -1890,12 +1889,12 @@ Lemma match_stacks_change_bounds: forall j m1 m' cs cs' sg bound bound', match_stacks j m1 m' cs cs' sg bound bound' -> forall xbound xbound', - bound <= xbound -> bound' <= xbound' -> + Ple bound xbound -> Ple bound' xbound' -> match_stacks j m1 m' cs cs' sg xbound xbound'. Proof. induction 1; intros. - apply match_stacks_empty with hi; auto. omega. omega. - econstructor; eauto. omega. omega. + apply match_stacks_empty with hi; auto. apply Ple_trans with bound; eauto. apply Ple_trans with bound'; eauto. + econstructor; eauto. eapply Plt_le_trans; eauto. eapply Plt_le_trans; eauto. Qed. (** Invariance with respect to change of [m]. *) @@ -1903,8 +1902,8 @@ Qed. Lemma match_stacks_change_linear_mem: forall j m1 m2 m' cs cs' sg bound bound', match_stacks j m1 m' cs cs' sg bound bound' -> - (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) -> - (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> + (forall b, Plt b bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) -> + (forall b ofs p, Plt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> match_stacks j m2 m' cs cs' sg bound bound'. Proof. induction 1; intros. @@ -1912,8 +1911,8 @@ Proof. econstructor; eauto. eapply agree_frame_invariant; eauto. apply IHmatch_stacks. - intros. apply H0; auto. omega. - intros. apply H1. omega. auto. + intros. apply H0; auto. apply Plt_trans with sp; auto. + intros. apply H1. apply Plt_trans with sp; auto. auto. Qed. (** Invariance with respect to change of [m']. *) @@ -1921,9 +1920,9 @@ Qed. Lemma match_stacks_change_mach_mem: forall j m m1' m2' cs cs' sg bound bound', match_stacks j m m1' cs cs' sg bound bound' -> - (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) -> - (forall b ofs k p, b < bound' -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) -> - (forall chunk b ofs v, b < bound' -> Mem.load chunk m1' b ofs = Some v -> Mem.load chunk m2' b ofs = Some v) -> + (forall b, Plt b bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) -> + (forall b ofs k p, Plt b bound' -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) -> + (forall chunk b ofs v, Plt b bound' -> Mem.load chunk m1' b ofs = Some v -> Mem.load chunk m2' b ofs = Some v) -> match_stacks j m m2' cs cs' sg bound bound'. Proof. induction 1; intros. @@ -1931,9 +1930,9 @@ Proof. econstructor; eauto. eapply agree_frame_invariant; eauto. apply IHmatch_stacks. - intros; apply H0; auto; omega. - intros; apply H1; auto; omega. - intros; apply H2; auto. omega. + intros; apply H0; auto. apply Plt_trans with sp'; auto. + intros; apply H1; auto. apply Plt_trans with sp'; auto. + intros; apply H2; auto. apply Plt_trans with sp'; auto. Qed. (** A variant of the latter, for use with external calls *) @@ -1941,10 +1940,10 @@ Qed. Lemma match_stacks_change_mem_extcall: forall j m1 m2 m1' m2' cs cs' sg bound bound', match_stacks j m1 m1' cs cs' sg bound bound' -> - (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) -> - (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> - (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) -> - mem_unchanged_on (loc_out_of_reach j m1) m1' m2' -> + (forall b, Plt b bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) -> + (forall b ofs p, Plt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> + (forall b, Plt b bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) -> + Mem.unchanged_on (loc_out_of_reach j m1) m1' m2' -> match_stacks j m2 m2' cs cs' sg bound bound'. Proof. induction 1; intros. @@ -1952,9 +1951,9 @@ Proof. econstructor; eauto. eapply agree_frame_extcall_invariant; eauto. apply IHmatch_stacks. - intros; apply H0; auto; omega. - intros; apply H1. omega. auto. - intros; apply H2; auto; omega. + intros; apply H0; auto. apply Plt_trans with sp; auto. + intros; apply H1. apply Plt_trans with sp; auto. auto. + intros; apply H2; auto. apply Plt_trans with sp'; auto. auto. Qed. @@ -1966,7 +1965,7 @@ Lemma match_stacks_change_meminj: inject_separated j j' m1 m1' -> forall cs cs' sg bound bound', match_stacks j m m' cs cs' sg bound bound' -> - bound' <= Mem.nextblock m1' -> + Ple bound' (Mem.nextblock m1') -> match_stacks j' m m' cs cs' sg bound bound'. Proof. induction 3; intros. @@ -1974,10 +1973,11 @@ Proof. inv H3. constructor; auto. intros. red in H0. case_eq (j b1). intros [b' delta'] EQ. rewrite (H _ _ _ EQ) in H3. inv H3. eauto. - intros EQ. exploit H0; eauto. intros [A B]. elim B. red. omega. + intros EQ. exploit H0; eauto. intros [A B]. elim B. red. + apply Plt_le_trans with hi. auto. apply Ple_trans with bound'; auto. econstructor; eauto. - eapply agree_frame_inject_incr; eauto. red; omega. - apply IHmatch_stacks. omega. + eapply agree_frame_inject_incr; eauto. red. eapply Plt_le_trans; eauto. + apply IHmatch_stacks. apply Ple_trans with bound'; auto. apply Plt_Ple; auto. Qed. (** Preservation by parallel stores in Linear and Mach. *) @@ -2007,17 +2007,17 @@ Lemma match_stack_change_extcall: external_call ec ge args' m1' t' res' m2' -> inject_incr j j' -> inject_separated j j' m1 m1' -> - mem_unchanged_on (loc_out_of_reach j m1) m1' m2' -> + Mem.unchanged_on (loc_out_of_reach j m1) m1' m2' -> forall cs cs' sg bound bound', match_stacks j m1 m1' cs cs' sg bound bound' -> - bound <= Mem.nextblock m1 -> bound' <= Mem.nextblock m1' -> + Ple bound (Mem.nextblock m1) -> Ple bound' (Mem.nextblock m1') -> match_stacks j' m2 m2' cs cs' sg bound bound'. Proof. intros. eapply match_stacks_change_meminj; eauto. eapply match_stacks_change_mem_extcall; eauto. intros; eapply external_call_valid_block; eauto. - intros; eapply external_call_max_perm; eauto. red; omega. + intros; eapply external_call_max_perm; eauto. red. eapply Plt_le_trans; eauto. intros; eapply external_call_valid_block; eauto. Qed. @@ -2318,7 +2318,7 @@ Variables m m': mem. Variable cs: list Linear.stackframe. Variable cs': list stackframe. Variable sg: signature. -Variables bound bound': Z. +Variables bound bound': block. Hypothesis MS: match_stacks j m m' cs cs' sg bound bound'. Variable ls: locset. Variable rs: regset. @@ -2574,7 +2574,7 @@ Proof. exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. omega. apply match_stacks_change_mach_mem with m'; auto. - eauto with mem. eauto with mem. intros. rewrite <- H3; eapply Mem.load_store_other; eauto. left; unfold block; omega. + eauto with mem. eauto with mem. intros. rewrite <- H3; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. eauto. eauto. auto. apply agree_regs_set_slot. apply agree_regs_undef_regs; auto. destruct sl. @@ -2687,11 +2687,11 @@ Proof. apply match_stacks_change_linear_mem with m. apply match_stacks_change_mach_mem with m'0. auto. - eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. - intros. rewrite <- H3. eapply Mem.load_free; eauto. left; unfold block; omega. + eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; apply Plt_ne; auto. + intros. rewrite <- H3. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. eauto with mem. intros. eapply Mem.perm_free_3; eauto. - apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. - apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. + apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. + apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. apply zero_size_arguments_tailcall_possible; auto. apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto. @@ -2707,8 +2707,8 @@ Proof. econstructor; eauto with coqlib. inversion H; inversion A; subst. eapply match_stack_change_extcall; eauto. - apply Zlt_le_weak. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. - apply Zlt_le_weak. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto. + apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. + apply Plt_Ple. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto. apply agree_regs_set_regs; auto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto. apply agree_frame_set_regs; auto. apply agree_frame_undef_regs; auto. eapply agree_frame_inject_incr; eauto. @@ -2733,8 +2733,8 @@ Proof. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto with coqlib. inv H; inv A. eapply match_stack_change_extcall; eauto. - apply Zlt_le_weak. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. - apply Zlt_le_weak. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto. + apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. + apply Plt_Ple. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto. eapply agree_regs_inject_incr; eauto. eapply agree_frame_inject_incr; eauto. apply agree_frame_extcall_invariant with m m'0; auto. @@ -2796,11 +2796,11 @@ Proof. apply match_stacks_change_linear_mem with m. apply match_stacks_change_mach_mem with m'0. eauto. - eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. - intros. rewrite <- H1. eapply Mem.load_free; eauto. left; unfold block; omega. + eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; apply Plt_ne; auto. + intros. rewrite <- H1. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. eauto with mem. intros. eapply Mem.perm_free_3; eauto. - apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. - apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. + apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. + apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto. (* internal function *) @@ -2821,9 +2821,9 @@ Proof. apply match_stacks_change_mach_mem with m'0. apply match_stacks_change_linear_mem with m. rewrite SP_EQ; rewrite SP'_EQ. - eapply match_stacks_change_meminj; eauto. omega. + eapply match_stacks_change_meminj; eauto. apply Ple_refl. eauto with mem. intros. exploit Mem.perm_alloc_inv. eexact H. eauto. - rewrite zeq_false. auto. omega. + rewrite dec_eq_false; auto. apply Plt_ne; auto. intros. eapply stores_in_frame_valid; eauto with mem. intros. eapply stores_in_frame_perm; eauto with mem. intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto. @@ -2843,11 +2843,9 @@ Proof. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. apply match_stacks_change_bounds with (Mem.nextblock m) (Mem.nextblock m'0). - inv H0; inv A. eapply match_stack_change_extcall; eauto. omega. omega. - exploit external_call_valid_block'. eexact H0. - instantiate (1 := (Mem.nextblock m - 1)). red; omega. unfold Mem.valid_block; omega. - exploit external_call_valid_block'. eexact A. - instantiate (1 := (Mem.nextblock m'0 - 1)). red; omega. unfold Mem.valid_block; omega. + inv H0; inv A. eapply match_stack_change_extcall; eauto. apply Ple_refl. apply Ple_refl. + eapply external_call_nextblock'; eauto. + eapply external_call_nextblock'; eauto. inv H0. apply wt_setlist_result. eapply external_call_well_typed; eauto. auto. apply agree_regs_set_regs; auto. apply agree_regs_inject_incr with j; auto. apply agree_callee_save_set_result; auto. @@ -2873,11 +2871,10 @@ Proof. rewrite symbols_preserved. eauto. econstructor; eauto. eapply Genv.initmem_inject; eauto. - apply match_stacks_empty with (Mem.nextblock m0). omega. omega. + apply match_stacks_empty with (Mem.nextblock m0). apply Ple_refl. apply Ple_refl. constructor. - apply Mem.nextblock_pos. - intros. unfold Mem.flat_inj. apply zlt_true; auto. - unfold Mem.flat_inj; intros. destruct (zlt b1 (Mem.nextblock m0)); congruence. + intros. unfold Mem.flat_inj. apply pred_dec_true; auto. + unfold Mem.flat_inj; intros. destruct (plt b1 (Mem.nextblock m0)); congruence. intros. change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto. intros. change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto. intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto. -- cgit v1.2.3