diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-06-16 06:56:02 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-06-16 06:56:02 +0000 |
| commit | b40e056328e183522b50c68aefdbff057bca29cc (patch) | |
| tree | b05fd2f0490e979e68ea06e1931bfcfba9b35771 | |
| parent | 0648e79b98cc8d79e1942d15dbf05ba7b9eaaa8c (diff) | |
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
35 files changed, 1237 insertions, 1040 deletions
@@ -689,7 +689,7 @@ Inductive initial_state (p: program): state -> Prop := (Pregmap.init Vundef) # PC <- (symbol_offset ge p.(prog_main) Int.zero) # IR14 <- Vzero - # IR13 <- (Vptr Mem.nullptr Int.zero) in + # IR13 <- Vzero in Genv.init_mem p = Some m0 -> initial_state p (State rs0 m0). diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 18f905a..19f5687 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -949,7 +949,7 @@ Proof. econstructor; eauto. constructor. apply Mem.extends_refl. - split. auto. simpl. congruence. intros. rewrite Regmap.gi. auto. + split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. unfold symbol_offset. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. @@ -390,9 +390,9 @@ Proof with (try exact I). destruct v0; destruct v1... generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; tauto. destruct v0... - destruct v0; destruct v1... simpl. destruct (zeq b b0)... - generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; intuition. destruct (zeq b b0)... - generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; intuition. destruct (zeq b0 b)... + destruct v0; destruct v1... simpl. destruct (eq_block b b0)... + generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; intuition. destruct (eq_block b b0)... + generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; intuition. destruct (eq_block b0 b)... destruct v0... destruct v0; destruct v1... destruct v0... destruct v1... destruct v2... 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. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 2df8b93..d6b99ed 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -204,7 +204,7 @@ Inductive match_var (f: meminj) (sp: block): option (block * Z) -> option Z -> P Record match_env (f: meminj) (cenv: compilenv) (e: Csharpminor.env) (sp: block) - (lo hi: Z) : Prop := + (lo hi: block) : Prop := mk_match_env { (** C#minor local variables match sub-blocks of the Cminor stack data block. *) @@ -213,12 +213,12 @@ Record match_env (f: meminj) (cenv: compilenv) (** [lo, hi] is a proper interval. *) me_low_high: - lo <= hi; + Ple lo hi; (** Every block appearing in the C#minor environment [e] must be in the range [lo, hi]. *) me_bounded: - forall id b sz, PTree.get id e = Some(b, sz) -> lo <= b < hi; + forall id b sz, PTree.get id e = Some(b, sz) -> Ple lo b /\ Plt b hi; (** All blocks mapped to sub-blocks of the Cminor stack data must be images of variables from the C#minor environment [e] *) @@ -232,7 +232,7 @@ Record match_env (f: meminj) (cenv: compilenv) (i.e. allocated before the stack data for the current Cminor function). *) me_incr: forall b tb delta, - f b = Some(tb, delta) -> b < lo -> tb < sp + f b = Some(tb, delta) -> Plt b lo -> Plt tb sp }. Ltac geninv x := @@ -243,7 +243,7 @@ Lemma match_env_invariant: match_env f1 cenv e sp lo hi -> inject_incr f1 f2 -> (forall b delta, f2 b = Some(sp, delta) -> f1 b = Some(sp, delta)) -> - (forall b, b < lo -> f2 b = f1 b) -> + (forall b, Plt b lo -> f2 b = f1 b) -> match_env f2 cenv e sp lo hi. Proof. intros. destruct H. constructor; auto. @@ -285,12 +285,12 @@ Lemma match_env_external_call: match_env f1 cenv e sp lo hi -> inject_incr f1 f2 -> inject_separated f1 f2 m1 m1' -> - hi <= Mem.nextblock m1 -> sp < Mem.nextblock m1' -> + Ple hi (Mem.nextblock m1) -> Plt sp (Mem.nextblock m1') -> match_env f2 cenv e sp lo hi. Proof. intros. apply match_env_invariant with f1; auto. intros. eapply inject_incr_separated_same'; eauto. - intros. eapply inject_incr_separated_same; eauto. red. destruct H. omega. + intros. eapply inject_incr_separated_same; eauto. red. destruct H. xomega. Qed. (** [match_env] and allocations *) @@ -320,18 +320,18 @@ Proof. constructor; eauto. constructor. (* low-high *) - rewrite NEXTBLOCK; omega. + rewrite NEXTBLOCK; xomega. (* bounded *) intros. rewrite PTree.gsspec in H. destruct (peq id0 id). - inv H. rewrite NEXTBLOCK; omega. - exploit me_bounded0; eauto. rewrite NEXTBLOCK; omega. + inv H. rewrite NEXTBLOCK; xomega. + exploit me_bounded0; eauto. rewrite NEXTBLOCK; xomega. (* inv *) - intros. destruct (zeq b (Mem.nextblock m1)). + intros. destruct (eq_block b (Mem.nextblock m1)). subst b. rewrite SAME in H; inv H. exists id; exists sz. apply PTree.gss. rewrite OTHER in H; auto. exploit me_inv0; eauto. intros [id1 [sz1 EQ]]. exists id1; exists sz1. rewrite PTree.gso; auto. congruence. (* incr *) - intros. rewrite OTHER in H. eauto. unfold block in *; omega. + intros. rewrite OTHER in H. eauto. unfold block in *; xomega. Qed. (** The sizes of blocks appearing in [e] are respected. *) @@ -371,7 +371,7 @@ Lemma padding_freeable_invariant: padding_freeable f1 e tm1 sp sz -> match_env f1 cenv e sp lo hi -> (forall ofs, Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) -> - (forall b, b < hi -> f2 b = f1 b) -> + (forall b, Plt b hi -> f2 b = f1 b) -> padding_freeable f2 e tm2 sp sz. Proof. intros; red; intros. @@ -424,14 +424,13 @@ Qed. (** Global environments match if the memory injection [f] leaves unchanged the references to global symbols and functions. *) -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). Remark inj_preserves_globals: forall f hi, @@ -459,7 +458,7 @@ Inductive frame : Type := (le: Csharpminor.temp_env) (te: Cminor.env) (sp: block) - (lo hi: Z). + (lo hi: block). Definition callstack : Type := list frame. @@ -473,16 +472,16 @@ Definition callstack : Type := list frame. *) Inductive match_callstack (f: meminj) (m: mem) (tm: mem): - callstack -> Z -> Z -> Prop := + callstack -> block -> block -> Prop := | mcs_nil: forall hi bound tbound, match_globalenvs f hi -> - hi <= bound -> hi <= tbound -> + Ple hi bound -> Ple hi tbound -> match_callstack f m tm nil bound tbound | mcs_cons: forall cenv tf e le te sp lo hi cs bound tbound - (BOUND: hi <= bound) - (TBOUND: sp < tbound) + (BOUND: Ple hi bound) + (TBOUND: Plt sp tbound) (MTMP: match_temps f le te) (MENV: match_env f cenv e sp lo hi) (BOUND: match_bounds e m) @@ -506,44 +505,44 @@ Lemma match_callstack_invariant: forall f1 m1 tm1 f2 m2 tm2 cs bound tbound, match_callstack f1 m1 tm1 cs bound tbound -> inject_incr f1 f2 -> - (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> - (forall sp ofs, sp < tbound -> Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) -> - (forall b, b < bound -> f2 b = f1 b) -> - (forall b b' delta, f2 b = Some(b', delta) -> b' < tbound -> f1 b = Some(b', delta)) -> + (forall b ofs p, Plt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> + (forall sp ofs, Plt sp tbound -> Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) -> + (forall b, Plt b bound -> f2 b = f1 b) -> + (forall b b' delta, f2 b = Some(b', delta) -> Plt b' tbound -> f1 b = Some(b', delta)) -> match_callstack f2 m2 tm2 cs bound tbound. Proof. induction 1; intros. (* base case *) econstructor; eauto. inv H. constructor; intros; eauto. - eapply IMAGE; eauto. eapply H6; eauto. omega. + eapply IMAGE; eauto. eapply H6; eauto. xomega. (* inductive case *) - assert (lo <= hi) by (eapply me_low_high; eauto). + assert (Ple lo hi) by (eapply me_low_high; eauto). econstructor; eauto. eapply match_temps_invariant; eauto. eapply match_env_invariant; eauto. - intros. apply H3. omega. + intros. apply H3. xomega. eapply match_bounds_invariant; eauto. intros. eapply H1; eauto. - exploit me_bounded; eauto. omega. + exploit me_bounded; eauto. xomega. eapply padding_freeable_invariant; eauto. - intros. apply H3. omega. + intros. apply H3. xomega. eapply IHmatch_callstack; eauto. - intros. eapply H1; eauto. omega. - intros. eapply H2; eauto. omega. - intros. eapply H3; eauto. omega. - intros. eapply H4; eauto. omega. + intros. eapply H1; eauto. xomega. + intros. eapply H2; eauto. xomega. + intros. eapply H3; eauto. xomega. + intros. eapply H4; eauto. xomega. Qed. Lemma match_callstack_incr_bound: forall f m tm cs bound tbound bound' tbound', match_callstack f m tm cs bound tbound -> - bound <= bound' -> tbound <= tbound' -> + Ple bound bound' -> Ple tbound tbound' -> match_callstack f m tm cs bound' tbound'. Proof. intros. inv H. - econstructor; eauto. omega. omega. - constructor; auto. omega. omega. + econstructor; eauto. xomega. xomega. + constructor; auto. xomega. xomega. Qed. (** Assigning a temporary variable. *) @@ -610,7 +609,7 @@ Proof. apply match_callstack_incr_bound with lo sp; try omega. apply match_callstack_invariant with f m tm; auto. intros. eapply perm_freelist; eauto. - intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. + intros. eapply Mem.perm_free_1; eauto. left; unfold block; xomega. xomega. xomega. eapply Mem.free_inject; eauto. intros. exploit me_inv0; eauto. intros [id [sz A]]. exists 0; exists sz; split. @@ -622,52 +621,52 @@ Qed. Lemma match_callstack_external_call: forall f1 f2 m1 m2 m1' m2', - mem_unchanged_on (loc_unmapped f1) m1 m2 -> - mem_unchanged_on (loc_out_of_reach f1 m1) m1' m2' -> + Mem.unchanged_on (loc_unmapped f1) m1 m2 -> + Mem.unchanged_on (loc_out_of_reach f1 m1) m1' m2' -> inject_incr f1 f2 -> inject_separated f1 f2 m1 m1' -> (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> forall cs bound tbound, match_callstack f1 m1 m1' cs bound tbound -> - bound <= Mem.nextblock m1 -> tbound <= Mem.nextblock m1' -> + Ple bound (Mem.nextblock m1) -> Ple tbound (Mem.nextblock m1') -> match_callstack f2 m2 m2' cs bound tbound. Proof. intros until m2'. intros UNMAPPED OUTOFREACH INCR SEPARATED MAXPERMS. - destruct OUTOFREACH as [OUTOFREACH1 OUTOFREACH2]. induction 1; intros. (* base case *) apply mcs_nil with hi; auto. inv H. constructor; auto. intros. case_eq (f1 b1). intros [b2' delta'] EQ. rewrite (INCR _ _ _ EQ) in H. inv H. eauto. - intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. omega. + intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. xomega. (* inductive case *) constructor. auto. auto. eapply match_temps_invariant; eauto. eapply match_env_invariant; eauto. red in SEPARATED. intros. destruct (f1 b) as [[b' delta']|] eqn:?. exploit INCR; eauto. congruence. - exploit SEPARATED; eauto. intros [A B]. elim B. red. omega. - intros. assert (lo <= hi) by (eapply me_low_high; eauto). + exploit SEPARATED; eauto. intros [A B]. elim B. red. xomega. + intros. assert (Ple lo hi) by (eapply me_low_high; eauto). destruct (f1 b) as [[b' delta']|] eqn:?. apply INCR; auto. destruct (f2 b) as [[b' delta']|] eqn:?; auto. - exploit SEPARATED; eauto. intros [A B]. elim A. red. omega. + exploit SEPARATED; eauto. intros [A B]. elim A. red. xomega. eapply match_bounds_invariant; eauto. - intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. omega. + intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. xomega. (* padding-freeable *) red; intros. destruct (is_reachable_from_env_dec f1 e sp ofs). inv H3. right. apply is_reachable_intro with id b sz delta; auto. exploit PERM; eauto. intros [A|A]; try contradiction. - left. apply OUTOFREACH1; auto. red; intros. - red; intros; elim H3. + left. eapply Mem.perm_unchanged_on; eauto. + red; intros; red; intros. elim H3. exploit me_inv; eauto. intros [id [lv B]]. exploit BOUND0; eauto. intros C. apply is_reachable_intro with id b0 lv delta; auto; omega. + eauto with mem. (* induction *) - eapply IHmatch_callstack; eauto. inv MENV; omega. omega. + eapply IHmatch_callstack; eauto. inv MENV; xomega. xomega. Qed. (** [match_callstack] and allocations *) @@ -687,12 +686,12 @@ Proof. exploit Mem.nextblock_alloc; eauto. intros NEXTBLOCK. exploit Mem.alloc_result; eauto. intros RES. constructor. - omega. - unfold block in *; omega. + xomega. + unfold block in *; xomega. auto. constructor; intros. rewrite H3. rewrite PTree.gempty. constructor. - omega. + xomega. rewrite PTree.gempty in H4; discriminate. eelim Mem.fresh_block_alloc; eauto. eapply Mem.valid_block_inject_2; eauto. rewrite RES. change (Mem.valid_block tm tb). eapply Mem.valid_block_inject_2; eauto. @@ -721,25 +720,25 @@ Proof. intros. inv H. exploit Mem.nextblock_alloc; eauto. intros NEXTBLOCK. exploit Mem.alloc_result; eauto. intros RES. - assert (LO: lo <= Mem.nextblock m1) by (eapply me_low_high; eauto). + assert (LO: Ple lo (Mem.nextblock m1)) by (eapply me_low_high; eauto). constructor. - omega. + xomega. auto. eapply match_temps_invariant; eauto. eapply match_env_alloc; eauto. red; intros. rewrite PTree.gsspec in H. destruct (peq id0 id). inversion H. subst b0 sz0 id0. eapply Mem.perm_alloc_3; eauto. eapply BOUND0; eauto. eapply Mem.perm_alloc_4; eauto. - exploit me_bounded; eauto. unfold block in *; omega. + exploit me_bounded; eauto. unfold block in *; xomega. red; intros. exploit PERM; eauto. intros [A|A]. auto. right. inv A. apply is_reachable_intro with id0 b0 sz0 delta; auto. rewrite PTree.gso. auto. congruence. eapply match_callstack_invariant with (m1 := m1); eauto. intros. eapply Mem.perm_alloc_4; eauto. - unfold block in *; omega. - intros. apply H4. unfold block in *; omega. - intros. destruct (zeq b0 b). - subst b0. rewrite H3 in H. inv H. omegaContradiction. + unfold block in *; xomega. + intros. apply H4. unfold block in *; xomega. + intros. destruct (eq_block b0 b). + subst b0. rewrite H3 in H. inv H. xomegaContradiction. rewrite H4 in H; auto. Qed. @@ -841,7 +840,7 @@ Proof. exploit (IHalloc_variables f2); eauto. red; intros. eapply COMPAT. auto with coqlib. red; intros. eapply SEP1; eauto with coqlib. - red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b b1); intros P. + red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b b1); intros P. subst b. rewrite C in H5; inv H5. exploit SEP1. eapply in_eq. eapply in_cons; eauto. eauto. eauto. red; intros; subst id0. elim H3. change id with (fst (id, sz0)). apply in_map; auto. @@ -1553,9 +1552,9 @@ Proof. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. inv H; inv H0; inv H1; TrivialExists. apply Int.sub_add_l. - simpl. destruct (zeq b1 b0); auto. + simpl. destruct (eq_block b1 b0); auto. subst b1. rewrite H in H0; inv H0. - rewrite zeq_true. rewrite Int.sub_shifted. auto. + rewrite dec_eq_true. rewrite Int.sub_shifted. auto. inv H; inv H0; inv H1; TrivialExists. inv H0; try discriminate; inv H1; try discriminate. simpl in *. destruct (Int.eq i0 Int.zero @@ -2575,7 +2574,7 @@ Proof. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. intros. eapply external_call_max_perm; eauto. - omega. omega. + xomega. xomega. eapply external_call_nextblock; eauto. eapply external_call_nextblock; eauto. econstructor; eauto. @@ -2725,7 +2724,7 @@ Opaque PTree.set. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. intros. eapply external_call_max_perm; eauto. - omega. omega. + xomega. xomega. eapply external_call_nextblock; eauto. eapply external_call_nextblock; eauto. @@ -2743,10 +2742,9 @@ Lemma match_globalenvs_init: match_globalenvs (Mem.flat_inj (Mem.nextblock m)) (Mem.nextblock m). Proof. intros. constructor. - apply Mem.nextblock_pos. - intros. unfold Mem.flat_inj. apply zlt_true; auto. + intros. unfold Mem.flat_inj. apply pred_dec_true; auto. intros. unfold Mem.flat_inj in H0. - destruct (zlt b1 (Mem.nextblock m)); congruence. + destruct (plt b1 (Mem.nextblock m)); congruence. intros. eapply Genv.find_symbol_not_fresh; eauto. intros. eapply Genv.find_funct_ptr_not_fresh; eauto. intros. eapply Genv.find_var_info_not_fresh; eauto. @@ -2770,7 +2768,7 @@ Proof. eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame) (cenv := PTree.empty Z). auto. eapply Genv.initmem_inject; eauto. - apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. omega. omega. + apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. xomega. xomega. constructor. red; auto. constructor. Qed. diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index e7ffc89..4932bad 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -604,7 +604,7 @@ Definition sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := | sub_case_pp ty => (**r pointer minus pointer *) match v1,v2 with | Vptr b1 ofs1, Vptr b2 ofs2 => - if zeq b1 b2 then + if eq_block b1 b2 then if Int.eq (Int.repr (sizeof ty)) Int.zero then None else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty)))) else None @@ -1059,8 +1059,8 @@ Proof. + inv H0; inv H1; inv H. TrivialInject. econstructor. eauto. rewrite Int.sub_add_l. auto. + inv H0; inv H1; inv H. TrivialInject. - destruct (zeq b1 b0); try discriminate. subst b1. - rewrite H0 in H2; inv H2. rewrite zeq_true. + destruct (eq_block b1 b0); try discriminate. subst b1. + rewrite H0 in H2; inv H2. rewrite dec_eq_true. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H3. rewrite Int.sub_shifted. TrivialInject. + inv H0; inv H1; inv H. TrivialInject. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 953e690..11f8011 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -437,8 +437,8 @@ Proof. destruct (classify_sub tya tyb); inv MAKE. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - destruct va; try discriminate; destruct vb; inv SEM. - destruct (zeq b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero) eqn:E; inv H0. - econstructor; eauto with cshm. rewrite zeq_true. simpl. rewrite E; auto. + destruct (eq_block b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero) eqn:E; inv H0. + econstructor; eauto with cshm. rewrite dec_eq_true. simpl. rewrite E; auto. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - eapply make_binarith_correct; eauto; intros; auto. Qed. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index cb2f132..e7debfc 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -30,7 +30,7 @@ Open Scope error_monad_scope. (** To evaluate constant expressions at compile-time, we use the same [value] type and the same [sem_*] functions that are used in CompCert C's semantics (module [Csem]). However, we interpret pointer values symbolically: - [Vptr (Zpos id) ofs] represents the address of global variable [id] + [Vptr id ofs] represents the address of global variable [id] plus byte offset [ofs]. *) (** [constval a] evaluates the constant expression [a]. @@ -111,7 +111,7 @@ Fixpoint constval (a: expr) : res val := | Ecomma r1 r2 ty => do v1 <- constval r1; constval r2 | Evar x ty => - OK(Vptr (Zpos x) Int.zero) + OK(Vptr x Int.zero) | Ederef r ty => constval r | Efield l f ty => @@ -155,9 +155,9 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data := | Vlong n, Tlong _ _ => OK(Init_int64 n) | Vfloat f, Tfloat F32 _ => OK(Init_float32 f) | Vfloat f, Tfloat F64 _ => OK(Init_float64 f) - | Vptr (Zpos id) ofs, Tint I32 sg _ => OK(Init_addrof id ofs) - | Vptr (Zpos id) ofs, Tpointer _ _ => OK(Init_addrof id ofs) - | Vptr (Zpos id) ofs, Tcomp_ptr _ _ => OK(Init_addrof id ofs) + | Vptr id ofs, Tint I32 sg _ => OK(Init_addrof id ofs) + | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs) + | Vptr id ofs, Tcomp_ptr _ _ => OK(Init_addrof id ofs) | Vundef, _ => Error(msg "undefined operation in initializer") | _, _ => Error (msg "type mismatch in initializer") end. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 2f29514..f3de05c 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -334,17 +334,13 @@ Qed. (** * Soundness of the compile-time evaluator *) (** A global environment [ge] induces a memory injection mapping - our symbolic pointers [Vptr (Zpos id) ofs] to run-time pointers + our symbolic pointers [Vptr id ofs] to run-time pointers [Vptr b ofs] where [Genv.find_symbol ge id = Some b]. *) Definition inj (b: block) := - match b with - | Zpos id => - match Genv.find_symbol ge id with - | Some b' => Some (b', 0) - | None => None - end - | _ => None + match Genv.find_symbol ge b with + | Some b' => Some (b', 0) + | None => None end. Lemma mem_empty_not_valid_pointer: @@ -512,11 +508,11 @@ Proof. destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. (* pointer *) - unfold inj in H. destruct b1; try discriminate. - assert (data = Init_addrof p ofs1 /\ chunk = Mint32). + unfold inj in H. + assert (data = Init_addrof b1 ofs1 /\ chunk = Mint32). destruct ty; inv EQ2; inv H2. destruct i; inv H5. intuition congruence. auto. - destruct H4; subst. destruct (Genv.find_symbol ge p); inv H. + destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H. rewrite Int.add_zero in H3. auto. (* undef *) discriminate. @@ -538,7 +534,6 @@ Proof. destruct ty; inv EQ2; reflexivity. destruct ty; try discriminate. destruct f0; inv EQ2; reflexivity. - destruct b; try discriminate. destruct ty; try discriminate. destruct i0; inv EQ2; reflexivity. inv EQ2; reflexivity. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 8e6bc9f..854d345 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -90,6 +90,14 @@ Definition gensym (ty: type): mon ident := (mkgenerator (Psucc (gen_next g)) ((gen_next g, ty) :: gen_trail g)) (Ple_succ (gen_next g)). +Definition reset_trail: mon unit := + fun (g: generator) => + Res tt (mkgenerator (gen_next g) nil) (Ple_refl (gen_next g)). + +Definition get_trail: mon (list (ident * type)) := + fun (g: generator) => + Res (gen_trail g) g (Ple_refl (gen_next g)). + (** Construct a sequence from a list of statements. To facilitate the proof, the sequence is nested to the left and starts with a [Sskip]. *) @@ -491,34 +499,43 @@ with transl_lblstmt (ls: Csyntax.labeled_statements) : mon labeled_statements := (** Translation of a function *) -Definition transl_function (f: Csyntax.function) : res function := - match transl_stmt f.(Csyntax.fn_body) (initial_generator tt) with - | Err msg => - Error msg - | Res tbody g i => - OK (mkfunction +Definition transl_function (f: Csyntax.function) : mon function := + do x <- reset_trail; + do tbody <- transl_stmt f.(Csyntax.fn_body); + do temps <- get_trail; + ret (mkfunction f.(Csyntax.fn_return) f.(Csyntax.fn_params) f.(Csyntax.fn_vars) - g.(gen_trail) - tbody) - end. + temps + tbody). -Local Open Scope error_monad_scope. - -Definition transl_fundef (fd: Csyntax.fundef) : res fundef := +Definition transl_fundef (fd: Csyntax.fundef) : mon fundef := match fd with | Csyntax.Internal f => - do tf <- transl_function f; OK (Internal tf) + do tf <- transl_function f; ret (Internal tf) | Csyntax.External ef targs tres => - OK (External ef targs tres) + ret (External ef targs tres) end. -Definition transl_program (p: Csyntax.program) : res program := - transform_partial_program transl_fundef p. - - - - +Local Open Scope error_monad_scope. +Fixpoint transl_globdefs + (l: list (ident * globdef Csyntax.fundef type)) + (g: generator) : res (list (ident * globdef Clight.fundef type)) := + match l with + | nil => OK nil + | (id, Gfun f) :: l' => + match transl_fundef f g with + | Err msg => + Error (MSG "In function " :: CTX id :: MSG ": " :: msg) + | Res tf g' _ => + do tl' <- transl_globdefs l' g'; OK ((id, Gfun tf) :: tl') + end + | (id, Gvar v) :: l' => + do tl' <- transl_globdefs l' g; OK ((id, Gvar v) :: tl') + end. +Definition transl_program (p: Csyntax.program) : res program := + do gl' <- transl_globdefs p.(prog_defs) (initial_generator tt); + OK (mkprogram gl' p.(prog_main)). diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index a2b8e61..dfe1c8a 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -44,29 +44,44 @@ Let tge := Genv.globalenv tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof - (Genv.find_symbol_transf_partial transl_fundef _ TRANSL). +Proof. + intros. eapply Genv.find_symbol_match. eapply transl_program_spec; eauto. + simpl. tauto. +Qed. Lemma function_ptr_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. -Proof - (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL). + Genv.find_funct_ptr tge b = Some tf /\ tr_fundef f tf. +Proof. + intros. eapply Genv.find_funct_ptr_match. + eapply transl_program_spec; eauto. + assumption. +Qed. Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. -Proof - (Genv.find_funct_transf_partial transl_fundef _ TRANSL). + Genv.find_funct tge v = Some tf /\ tr_fundef f tf. +Proof. + intros. eapply Genv.find_funct_match. + eapply transl_program_spec; eauto. + assumption. +Qed. Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof - (Genv.find_var_info_transf_partial transl_fundef _ TRANSL). +Proof. + intros. destruct (Genv.find_var_info ge b) as [v|] eqn:V. +- exploit Genv.find_var_info_match. eapply transl_program_spec; eauto. eassumption. + intros [tv [A B]]. inv B. assumption. +- destruct (Genv.find_var_info tge b) as [v'|] eqn:V'; auto. + exploit Genv.find_var_info_rev_match. eapply transl_program_spec; eauto. eassumption. + simpl. destruct (plt b (Genv.genv_next (Genv.globalenv prog))); try tauto. + intros [v [A B]]. inv B. fold ge in A. congruence. +Qed. Lemma block_is_volatile_preserved: forall b, block_is_volatile tge b = block_is_volatile ge b. @@ -75,22 +90,19 @@ Proof. Qed. Lemma type_of_fundef_preserved: - forall f tf, transl_fundef f = OK tf -> + forall f tf, tr_fundef f tf -> type_of_fundef tf = Csyntax.type_of_fundef f. Proof. - intros. destruct f; monadInv H. - exploit transl_function_spec; eauto. intros [A [B [C D]]]. - simpl. unfold type_of_function, Csyntax.type_of_function. congruence. + intros. inv H. + inv H0; simpl. unfold type_of_function, Csyntax.type_of_function. congruence. auto. Qed. Lemma function_return_preserved: - forall f tf, transl_function f = OK tf -> + forall f tf, tr_function f tf -> fn_return tf = Csyntax.fn_return f. Proof. - intros. unfold transl_function in H. - destruct (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); inv H. - auto. + intros. inv H; auto. Qed. Lemma type_of_global_preserved: @@ -893,7 +905,7 @@ Inductive match_cont : Csem.cont -> cont -> Prop := match_cont k tk -> match_cont (Csem.Kswitch2 k) (Kswitch tk) | match_Kcall: forall f e C ty k optid tf le sl tk a dest tmps, - transl_function f = Errors.OK tf -> + tr_function f tf -> leftcontext RV RV C -> (forall v m, tr_top tge e (set_opttemp optid v le) m dest (C (Csyntax.Eval v ty)) sl a tmps) -> match_cont_exp dest a k tk -> @@ -961,19 +973,19 @@ Qed. Inductive match_states: Csem.state -> state -> Prop := | match_exprstates: forall f r k e m tf sl tk le dest a tmps, - transl_function f = Errors.OK tf -> + tr_function f tf -> tr_top tge e le m dest r sl a tmps -> match_cont_exp dest a k tk -> match_states (Csem.ExprState f r k e m) (State tf Sskip (Kseqlist sl tk) e le m) | match_regularstates: forall f s k e m tf ts tk le, - transl_function f = Errors.OK tf -> + tr_function f tf -> tr_stmt s ts -> match_cont k tk -> match_states (Csem.State f s k e m) (State tf ts tk e le m) | match_callstates: forall fd args k m tfd tk, - transl_fundef fd = Errors.OK tfd -> + tr_fundef fd tfd -> match_cont k tk -> match_states (Csem.Callstate fd args k m) (Callstate tfd args tk m) @@ -2089,8 +2101,7 @@ Proof. inv H9. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. econstructor; split. left. eapply plus_two. constructor. econstructor. eauto. - replace (fn_return tf) with (Csyntax.fn_return f). eauto. - exploit transl_function_spec; eauto. intuition congruence. + erewrite function_return_preserved; eauto. eauto. traceEq. constructor. apply match_cont_call; auto. (* skip return *) @@ -2133,8 +2144,8 @@ Proof. (* goto *) inv H7. - exploit transl_function_spec; eauto. intros [A [B [C D]]]. - exploit tr_find_label. eexact A. apply match_cont_call. eauto. + inversion H6; subst. + exploit tr_find_label. eauto. apply match_cont_call. eauto. instantiate (1 := lbl). rewrite H. intros [ts' [tk' [P [Q R]]]]. econstructor; split. @@ -2142,18 +2153,17 @@ Proof. econstructor; eauto. (* internal function *) - monadInv H7. - exploit transl_function_spec; eauto. intros [A [B [C D]]]. + inv H7. inversion H3; subst. econstructor; split. left; apply plus_one. eapply step_internal_function. econstructor. - rewrite C; rewrite D; auto. - rewrite C; rewrite D. eapply alloc_variables_preserved; eauto. - rewrite C. eapply bind_parameters_preserved; eauto. + rewrite H5; rewrite H6; auto. + rewrite H5; rewrite H6. eapply alloc_variables_preserved; eauto. + rewrite H5. eapply bind_parameters_preserved; eauto. eauto. constructor; auto. (* external function *) - monadInv H5. + inv H5. econstructor; split. left; apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. @@ -2188,14 +2198,13 @@ Lemma transl_initial_states: exists S', Clight.initial_state tprog S' /\ match_states S S'. Proof. intros. inv H. + exploit transl_program_spec; eauto. intros MP. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. econstructor; split. econstructor. - apply (Genv.init_mem_transf_partial _ _ TRANSL). eauto. + exploit Genv.init_mem_match; eauto. simpl. fold tge. rewrite symbols_preserved. - replace (prog_main tprog) with (prog_main prog). eexact H1. - symmetry. unfold transl_program in TRANSL. - eapply transform_partial_program_main; eauto. + destruct MP as [A B]. rewrite B; eexact H1. eexact FIND. rewrite <- H3. apply type_of_fundef_preserved. auto. constructor. auto. constructor. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index d063c4e..a424261 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -1085,17 +1085,67 @@ Opaque transl_expression transl_expr_stmt. monadInv TR; constructor; eauto. Qed. -Theorem transl_function_spec: - forall f tf, - transl_function f = OK tf -> - tr_stmt f.(Csyntax.fn_body) tf.(fn_body) - /\ fn_return tf = Csyntax.fn_return f - /\ fn_params tf = Csyntax.fn_params f - /\ fn_vars tf = Csyntax.fn_vars f. +(** Relational presentation for the transformation of functions, fundefs, and variables. *) + +Inductive tr_function: Csyntax.function -> Clight.function -> Prop := + | tr_function_intro: forall f tf, + tr_stmt f.(Csyntax.fn_body) tf.(fn_body) -> + fn_return tf = Csyntax.fn_return f -> + fn_params tf = Csyntax.fn_params f -> + fn_vars tf = Csyntax.fn_vars f -> + tr_function f tf. + +Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop := + | tr_internal: forall f tf, + tr_function f tf -> + tr_fundef (Csyntax.Internal f) (Clight.Internal tf) + | tr_external: forall ef targs tres, + tr_fundef (Csyntax.External ef targs tres) (External ef targs tres). + +Lemma transl_function_spec: + forall f tf g g' i, + transl_function f g = Res tf g' i -> + tr_function f tf. Proof. - intros until tf. unfold transl_function. - case_eq (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); intros; inv H0. - simpl. intuition. eapply transl_stmt_meets_spec; eauto. + unfold transl_function; intros. monadInv H. + constructor; auto. simpl. eapply transl_stmt_meets_spec; eauto. +Qed. + +Lemma transl_fundef_spec: + forall fd tfd g g' i, + transl_fundef fd g = Res tfd g' i -> + tr_fundef fd tfd. +Proof. + unfold transl_fundef; intros. + destruct fd; monadInv H. ++ constructor. eapply transl_function_spec; eauto. ++ constructor. +Qed. + +Lemma transl_globdefs_spec: + forall l g l', + transl_globdefs l g = OK l' -> + list_forall2 (match_globdef tr_fundef (fun v1 v2 => v1 = v2)) l l'. +Proof. + induction l; simpl; intros. +- inv H. constructor. +- destruct a as [id gd]. destruct gd. + + destruct (transl_fundef f g) as [? | tf g' ?] eqn:E1; try discriminate. + destruct (transl_globdefs l g') eqn:E2; simpl in H; inv H. + constructor; eauto. constructor. eapply transl_fundef_spec; eauto. + + destruct (transl_globdefs l g) eqn:E2; simpl in H; inv H. + constructor; eauto. destruct v; constructor; auto. +Qed. + +Theorem transl_program_spec: + forall p tp, + transl_program p = OK tp -> + match_program tr_fundef (fun v1 v2 => v1 = v2) nil p.(prog_main) p tp. +Proof. + unfold transl_program; intros. + destruct (transl_globdefs (prog_defs p) (initial_generator tt)) eqn:E; simpl in H; inv H. + split; auto. exists l; split. eapply transl_globdefs_spec; eauto. + rewrite <- app_nil_end; auto. Qed. End SPEC. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 38660c6..515049a 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -114,8 +114,8 @@ Inductive match_var (f: meminj) (cenv: compilenv) (e: env) (m: mem) (te: env) (t match_var f cenv e m te tle id. Record match_envs (f: meminj) (cenv: compilenv) - (e: env) (le: temp_env) (m: mem) (lo hi: Z) - (te: env) (tle: temp_env) (tlo thi: Z) : Prop := + (e: env) (le: temp_env) (m: mem) (lo hi: block) + (te: env) (tle: temp_env) (tlo thi: block) : Prop := mk_match_envs { me_vars: forall id, match_var f cenv e m te tle id; @@ -127,9 +127,9 @@ Record match_envs (f: meminj) (cenv: compilenv) me_inj: forall id1 b1 ty1 id2 b2 ty2, e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2; me_range: - forall id b ty, e!id = Some(b, ty) -> lo <= b < hi; + forall id b ty, e!id = Some(b, ty) -> Ple lo b /\ Plt b hi; me_trange: - forall id b ty, te!id = Some(b, ty) -> tlo <= b < thi; + forall id b ty, te!id = Some(b, ty) -> Ple tlo b /\ Plt b thi; me_mapped: forall id b' ty, te!id = Some(b', ty) -> exists b, f b = Some(b', 0) /\ e!id = Some(b, ty); @@ -137,9 +137,9 @@ Record match_envs (f: meminj) (cenv: compilenv) forall id b' ty b delta, te!id = Some(b', ty) -> f b = Some(b', delta) -> e!id = Some(b, ty) /\ delta = 0; me_incr: - lo <= hi; + Ple lo hi; me_tincr: - tlo <= thi + Ple tlo thi }. (** Invariance by change of memory and injection *) @@ -148,10 +148,10 @@ Lemma match_envs_invariant: forall f cenv e le m lo hi te tle tlo thi f' m', match_envs f cenv e le m lo hi te tle tlo thi -> (forall b chunk v, - f b = None -> lo <= b < hi -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) -> + f b = None -> Ple lo b /\ Plt b hi -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) -> inject_incr f f' -> - (forall b, lo <= b < hi -> f' b = f b) -> - (forall b b' delta, f' b = Some(b', delta) -> tlo <= b' < thi -> f' b = f b) -> + (forall b, Ple lo b /\ Plt b hi -> f' b = f b) -> + (forall b b' delta, f' b = Some(b', delta) -> Ple tlo b' /\ Plt b' thi -> f' b = f b) -> match_envs f' cenv e le m' lo hi te tle tlo thi. Proof. intros until m'; intros ME LD INCR INV1 INV2. @@ -175,22 +175,22 @@ Qed. Lemma match_envs_extcall: forall f cenv e le m lo hi te tle tlo thi tm f' m', match_envs f cenv e le m lo hi te tle tlo thi -> - mem_unchanged_on (loc_unmapped f) m m' -> + Mem.unchanged_on (loc_unmapped f) m m' -> inject_incr f f' -> inject_separated f f' m tm -> - hi <= Mem.nextblock m -> thi <= Mem.nextblock tm -> + Ple hi (Mem.nextblock m) -> Ple thi (Mem.nextblock tm) -> match_envs f' cenv e le m' lo hi te tle tlo thi. Proof. intros. eapply match_envs_invariant; eauto. - intros. destruct H0. eapply H8. intros; red. auto. auto. + intros. eapply Mem.load_unchanged_on; eauto. red in H2. intros. destruct (f b) as [[b' delta]|] eqn:?. eapply H1; eauto. destruct (f' b) as [[b' delta]|] eqn:?; auto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. - omegaContradiction. + xomegaContradiction. intros. destruct (f b) as [[b'' delta']|] eqn:?. eauto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. - omegaContradiction. + xomegaContradiction. Qed. (** Properties of values obtained by casting to a given type. *) @@ -591,33 +591,34 @@ Hint Resolve compat_cenv_union_l compat_cenv_union_r compat_cenv_empty: compat. Lemma alloc_variables_nextblock: forall e m vars e' m', - alloc_variables e m vars e' m' -> Mem.nextblock m <= Mem.nextblock m'. + alloc_variables e m vars e' m' -> Ple (Mem.nextblock m) (Mem.nextblock m'). Proof. induction 1. - omega. - exploit Mem.nextblock_alloc; eauto. unfold block. omega. + apply Ple_refl. + eapply Ple_trans; eauto. exploit Mem.nextblock_alloc; eauto. intros EQ; rewrite EQ. apply Ple_succ. Qed. Lemma alloc_variables_range: forall id b ty e m vars e' m', alloc_variables e m vars e' m' -> - e'!id = Some(b, ty) -> e!id = Some(b, ty) \/ Mem.nextblock m <= b < Mem.nextblock m'. + e'!id = Some(b, ty) -> e!id = Some(b, ty) \/ Ple (Mem.nextblock m) b /\ Plt b (Mem.nextblock m'). Proof. induction 1; intros. auto. exploit IHalloc_variables; eauto. rewrite PTree.gsspec. intros [A|A]. destruct (peq id id0). inv A. - right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. unfold block. - generalize (alloc_variables_nextblock _ _ _ _ _ H0). omega. + right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. + generalize (alloc_variables_nextblock _ _ _ _ _ H0). intros A B C. + subst b. split. apply Ple_refl. eapply Plt_le_trans; eauto. rewrite B. apply Plt_succ. auto. - right. exploit Mem.nextblock_alloc; eauto. unfold block. omega. + right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. xomega. Qed. Lemma alloc_variables_injective: forall id1 b1 ty1 id2 b2 ty2 e m vars e' m', alloc_variables e m vars e' m' -> (e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2) -> - (forall id b ty, e!id = Some(b, ty) -> b < Mem.nextblock m) -> + (forall id b ty, e!id = Some(b, ty) -> Plt b (Mem.nextblock m)) -> (e'!id1 = Some(b1, ty1) -> e'!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2). Proof. induction 1; intros. @@ -626,12 +627,12 @@ Proof. repeat rewrite PTree.gsspec; intros. destruct (peq id1 id); destruct (peq id2 id). congruence. - inv H6. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; omega. - inv H7. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; omega. + inv H6. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; xomega. + inv H7. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; xomega. eauto. intros. rewrite PTree.gsspec in H6. destruct (peq id0 id). inv H6. - exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; omega. - exploit H2; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; omega. + exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; xomega. + exploit H2; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; xomega. Qed. Lemma match_alloc_variables: @@ -714,16 +715,16 @@ Proof. destruct (eq_block b b1); auto. subst. assert (j' b1 = j1 b1). apply M. eapply Mem.valid_new_block; eauto. rewrite H4 in H1. rewrite D in H1. inv H1. eelim Mem.fresh_block_alloc; eauto. - split. intros. destruct (zeq b' tb1). + split. intros. destruct (eq_block b' tb1). subst b'. rewrite (N _ _ _ H1) in H1. - destruct (zeq b b1). subst b. rewrite D in H1; inv H1. + destruct (eq_block b b1). subst b. rewrite D in H1; inv H1. exploit (P id); auto. intros [X Y]. exists id; exists ty. rewrite X; rewrite Y. repeat rewrite PTree.gss. auto. rewrite E in H1; auto. elim H3. eapply Mem.mi_mappedblocks; eauto. eapply Mem.valid_new_block; eauto. eapply Q; eauto. unfold Mem.valid_block in *. exploit Mem.nextblock_alloc. eexact A. exploit Mem.alloc_result. eexact A. - unfold block; omega. + unfold block; xomega. split. intros. destruct (ident_eq id0 id). (* same var *) subst id0. @@ -983,7 +984,7 @@ Proof. (* flat *) exploit alloc_variables_range. eexact A. eauto. rewrite PTree.gempty. intros [P|P]. congruence. - exploit K; eauto. unfold Mem.valid_block. omega. + exploit K; eauto. unfold Mem.valid_block. xomega. intros [id0 [ty0 [U [V W]]]]. split; auto. destruct (ident_eq id id0). congruence. assert (b' <> b'). @@ -1262,7 +1263,7 @@ Proof. eapply Mem.range_perm_inject; eauto. eapply free_blocks_of_env_perm_2; eauto. (* no repetitions *) - set (F := fun id => match te!id with Some(b, ty) => b | None => 0 end). + set (F := fun id => match te!id with Some(b, ty) => b | None => xH end). replace (map (fun b_lo_hi : block * Z * Z => fst (fst b_lo_hi)) (blocks_of_env te)) with (map F (map (fun x => fst x) (PTree.elements te))). apply list_map_norepet. apply PTree.elements_keys_norepet. @@ -1297,14 +1298,13 @@ Qed. (** Matching 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 match_globalenvs_preserves_globals: forall f, @@ -1324,7 +1324,7 @@ Variables le tle: temp_env. Variables m tm: mem. Variable f: meminj. Variable cenv: compilenv. -Variables lo hi tlo thi: Z. +Variables lo hi tlo thi: block. Hypothesis MATCH: match_envs f cenv e le m lo hi te tle tlo thi. Hypothesis MEMINJ: Mem.inject f m tm. Hypothesis GLOB: exists bound, match_globalenvs f bound. @@ -1472,9 +1472,9 @@ End EVAL_EXPR. (** Matching continuations *) -Inductive match_cont (f: meminj): compilenv -> cont -> cont -> mem -> Z -> Z -> Prop := +Inductive match_cont (f: meminj): compilenv -> cont -> cont -> mem -> block -> block -> Prop := | match_Kstop: forall cenv m bound tbound hi, - match_globalenvs f hi -> hi <= bound -> hi <= tbound -> + match_globalenvs f hi -> Ple hi bound -> Ple hi tbound -> match_cont f cenv Kstop Kstop m bound tbound | match_Kseq: forall cenv s k ts tk m bound tbound, simpl_stmt cenv s = OK ts -> @@ -1501,7 +1501,7 @@ Inductive match_cont (f: meminj): compilenv -> cont -> cont -> mem -> Z -> Z -> match_envs f (cenv_for fn) e le m lo hi te tle tlo thi -> match_cont f (cenv_for fn) k tk m lo tlo -> check_opttemp (cenv_for fn) optid = OK x -> - hi <= bound -> thi <= tbound -> + Ple hi bound -> Ple thi tbound -> match_cont f cenv (Kcall optid fn e le k) (Kcall optid tfn te tle tk) m bound tbound. @@ -1511,26 +1511,26 @@ Lemma match_cont_invariant: forall f' m' f cenv k tk m bound tbound, match_cont f cenv k tk m bound tbound -> (forall b chunk v, - f b = None -> b < bound -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) -> + f b = None -> Plt b bound -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) -> inject_incr f f' -> - (forall b, b < bound -> f' b = f b) -> - (forall b b' delta, f' b = Some(b', delta) -> b' < tbound -> f' b = f b) -> + (forall b, Plt b bound -> f' b = f b) -> + (forall b b' delta, f' b = Some(b', delta) -> Plt b' tbound -> f' b = f b) -> match_cont f' cenv k tk m' bound tbound. Proof. induction 1; intros LOAD INCR INJ1 INJ2; econstructor; eauto. (* globalenvs *) inv H. constructor; intros; eauto. - assert (f b1 = Some (b2, delta)). rewrite <- H; symmetry; eapply INJ2; eauto. omega. + assert (f b1 = Some (b2, delta)). rewrite <- H; symmetry; eapply INJ2; eauto. xomega. eapply IMAGE; eauto. (* call *) eapply match_envs_invariant; eauto. - intros. apply LOAD; auto. omega. - intros. apply INJ1; auto; omega. - intros. eapply INJ2; eauto; omega. + intros. apply LOAD; auto. xomega. + intros. apply INJ1; auto; xomega. + intros. eapply INJ2; eauto; xomega. eapply IHmatch_cont; eauto. - intros; apply LOAD; auto. inv H0; omega. - intros; apply INJ1. inv H0; omega. - intros; eapply INJ2; eauto. inv H0; omega. + intros; apply LOAD; auto. inv H0; xomega. + intros; apply INJ1. inv H0; xomega. + intros; eapply INJ2; eauto. inv H0; xomega. Qed. (** Invariance by assignment to location "above" *) @@ -1539,15 +1539,15 @@ Lemma match_cont_assign_loc: forall f cenv k tk m bound tbound ty loc ofs v m', match_cont f cenv k tk m bound tbound -> assign_loc ty m loc ofs v m' -> - bound <= loc -> + Ple bound loc -> match_cont f cenv k tk m' bound tbound. Proof. intros. eapply match_cont_invariant; eauto. intros. rewrite <- H4. inv H0. (* scalar *) - simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; omega. + simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; xomega. (* block copy *) - eapply Mem.load_storebytes_other; eauto. left. unfold block; omega. + eapply Mem.load_storebytes_other; eauto. left. unfold block; xomega. Qed. (** Invariance by external calls *) @@ -1555,19 +1555,19 @@ Qed. Lemma match_cont_extcall: forall f cenv k tk m bound tbound tm f' m', match_cont f cenv k tk m bound tbound -> - mem_unchanged_on (loc_unmapped f) m m' -> + Mem.unchanged_on (loc_unmapped f) m m' -> inject_incr f f' -> inject_separated f f' m tm -> - bound <= Mem.nextblock m -> tbound <= Mem.nextblock tm -> + Ple bound (Mem.nextblock m) -> Ple tbound (Mem.nextblock tm) -> match_cont f' cenv k tk m' bound tbound. Proof. intros. eapply match_cont_invariant; eauto. - destruct H0. intros. eapply H5; eauto. + intros. eapply Mem.load_unchanged_on; eauto. red in H2. intros. destruct (f b) as [[b' delta] | ] eqn:?. auto. destruct (f' b) as [[b' delta] | ] eqn:?; auto. - exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction. + exploit H2; eauto. unfold Mem.valid_block. intros [A B]. xomegaContradiction. red in H2. intros. destruct (f b) as [[b'' delta''] | ] eqn:?. auto. - exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction. + exploit H2; eauto. unfold Mem.valid_block. intros [A B]. xomegaContradiction. Qed. (** Invariance by change of bounds *) @@ -1576,10 +1576,10 @@ Lemma match_cont_incr_bounds: forall f cenv k tk m bound tbound, match_cont f cenv k tk m bound tbound -> forall bound' tbound', - bound <= bound' -> tbound <= tbound' -> + Ple bound bound' -> Ple tbound tbound' -> match_cont f cenv k tk m bound' tbound'. Proof. - induction 1; intros; econstructor; eauto; omega. + induction 1; intros; econstructor; eauto; xomega. Qed. (** [match_cont] and call continuations. *) @@ -1626,22 +1626,22 @@ Qed. Remark free_list_load: forall chunk b' l m m', Mem.free_list m l = Some m' -> - (forall b lo hi, In (b, lo, hi) l -> b' < b) -> + (forall b lo hi, In (b, lo, hi) l -> Plt b' b) -> Mem.load chunk m' b' 0 = Mem.load chunk m b' 0. Proof. induction l; simpl; intros. inv H; auto. destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate. transitivity (Mem.load chunk m1 b' 0). eauto. - eapply Mem.load_free. eauto. left. assert (b' < b) by eauto. unfold block; omega. + eapply Mem.load_free. eauto. left. assert (Plt b' b) by eauto. unfold block; xomega. Qed. Lemma match_cont_free_env: forall f cenv e le m lo hi te tle tm tlo thi k tk m' tm', match_envs f cenv e le m lo hi te tle tlo thi -> match_cont f cenv k tk m lo tlo -> - hi <= Mem.nextblock m -> - thi <= Mem.nextblock tm -> + Ple hi (Mem.nextblock m) -> + Ple thi (Mem.nextblock tm) -> Mem.free_list m (blocks_of_env e) = Some m' -> Mem.free_list tm (blocks_of_env te) = Some tm' -> match_cont f cenv k tk m' (Mem.nextblock m') (Mem.nextblock tm'). @@ -1651,9 +1651,9 @@ Proof. intros. rewrite <- H7. eapply free_list_load; eauto. unfold blocks_of_env; intros. exploit list_in_map_inv; eauto. intros [[id [b1 ty]] [P Q]]. simpl in P. inv P. - exploit me_range; eauto. eapply PTree.elements_complete; eauto. omega. - rewrite (free_list_nextblock _ _ _ H3). inv H; omega. - rewrite (free_list_nextblock _ _ _ H4). inv H; omega. + exploit me_range; eauto. eapply PTree.elements_complete; eauto. xomega. + rewrite (free_list_nextblock _ _ _ H3). inv H; xomega. + rewrite (free_list_nextblock _ _ _ H4). inv H; xomega. Qed. (** Matching of global environments *) @@ -1695,8 +1695,8 @@ Inductive match_states: state -> state -> Prop := (MCONT: match_cont j (cenv_for f) k tk m lo tlo) (MINJ: Mem.inject j m tm) (COMPAT: compat_cenv (addr_taken_stmt s) (cenv_for f)) - (BOUND: hi <= Mem.nextblock m) - (TBOUND: thi <= Mem.nextblock tm), + (BOUND: Ple hi (Mem.nextblock m)) + (TBOUND: Ple thi (Mem.nextblock tm)), match_states (State f s k e le m) (State tf ts tk te tle tm) | match_call_state: @@ -1900,7 +1900,7 @@ Proof. apply plus_one. econstructor. eapply make_cast_correct. eexact A. rewrite typeof_simpl_expr. eexact C. econstructor; eauto with compat. eapply match_envs_assign_lifted; eauto. eapply cast_val_is_casted; eauto. - eapply match_cont_assign_loc; eauto. exploit me_range; eauto. omega. + eapply match_cont_assign_loc; eauto. exploit me_range; eauto. xomega. inv MV; try congruence. inv H2; try congruence. unfold Mem.storev in H3. eapply Mem.store_unmapped_inject; eauto. congruence. erewrite assign_loc_nextblock; eauto. @@ -1951,9 +1951,9 @@ Proof. eapply match_envs_set_opttemp; eauto. eapply match_envs_extcall; eauto. eapply match_cont_extcall; eauto. - inv MENV; omega. inv MENV; omega. - eapply Zle_trans; eauto. eapply external_call_nextblock; eauto. - eapply Zle_trans; eauto. eapply external_call_nextblock; eauto. + inv MENV; xomega. inv MENV; xomega. + eapply Ple_trans; eauto. eapply external_call_nextblock; eauto. + eapply Ple_trans; eauto. eapply external_call_nextblock; eauto. (* sequence *) econstructor; split. apply plus_one. econstructor. @@ -2085,11 +2085,11 @@ Proof. eapply bind_parameters_load; eauto. intros. exploit alloc_variables_range. eexact H1. eauto. unfold empty_env. rewrite PTree.gempty. intros [?|?]. congruence. - red; intros; subst b'. omega. + red; intros; subst b'. xomega. eapply alloc_variables_load; eauto. apply compat_cenv_for. - rewrite (bind_parameters_nextblock _ _ _ _ _ H2). omega. - rewrite T; omega. + rewrite (bind_parameters_nextblock _ _ _ _ _ H2). xomega. + rewrite T; xomega. (* external function *) monadInv TRFD. inv FUNTY. @@ -2101,7 +2101,7 @@ Proof. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm). - eapply match_cont_extcall; eauto. omega. omega. + eapply match_cont_extcall; eauto. xomega. xomega. eapply external_call_nextblock; eauto. eapply external_call_nextblock; eauto. @@ -2130,13 +2130,12 @@ Proof. intros. instantiate (1 := Mem.flat_inj (Mem.nextblock m0)). econstructor. instantiate (1 := 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)); inv H. auto. + unfold Mem.flat_inj. apply pred_dec_true; auto. + unfold Mem.flat_inj in H. destruct (plt b1 (Mem.nextblock m0)); inv H. auto. eapply Genv.find_symbol_not_fresh; eauto. eapply Genv.find_funct_ptr_not_fresh; eauto. eapply Genv.find_var_info_not_fresh; eauto. - omega. omega. + xomega. xomega. eapply Genv.initmem_inject; eauto. constructor. Qed. diff --git a/common/Events.v b/common/Events.v index be1915a..3082503 100644 --- a/common/Events.v +++ b/common/Events.v @@ -582,14 +582,6 @@ Definition extcall_sem : Type := (** We now specify the expected properties of this predicate. *) -Definition mem_unchanged_on (P: block -> Z -> Prop) (m_before m_after: mem): Prop := - (forall b ofs k p, - P b ofs -> Mem.perm m_before b ofs k p -> Mem.perm m_after b ofs k p) -/\(forall chunk b ofs v, - (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) -> - Mem.load chunk m_before b ofs = Some v -> - Mem.load chunk m_after b ofs = Some v). - Definition loc_out_of_bounds (m: mem) (b: block) (ofs: Z) : Prop := ~Mem.perm m b ofs Max Nonempty. @@ -663,7 +655,7 @@ Record extcall_properties (sem: extcall_sem) sem F V ge vargs' m1' t vres' m2' /\ Val.lessdef vres vres' /\ Mem.extends m2 m2' - /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'; + /\ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'; (** External calls must commute with memory injections, in the following sense. *) @@ -677,8 +669,8 @@ Record extcall_properties (sem: extcall_sem) sem F V ge vargs' m1' t vres' m2' /\ val_inject f' vres vres' /\ Mem.inject f' m2 m2' - /\ mem_unchanged_on (loc_unmapped f) m1 m2 - /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2' + /\ Mem.unchanged_on (loc_unmapped f) m1 m2 + /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' /\ inject_incr f f' /\ inject_separated f f' m1 m1'; @@ -797,12 +789,12 @@ Proof. (* mem extends *) inv H. inv H1. inv H6. inv H4. exploit volatile_load_extends; eauto. intros [v' [A B]]. - exists v'; exists m1'; intuition. constructor; auto. red; auto. + exists v'; exists m1'; intuition. constructor; auto. (* mem injects *) inv H0. inv H2. inv H7. inversion H5; subst. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. constructor; auto. - red; auto. red; auto. red; intros. congruence. + red; intros. congruence. (* trace length *) inv H; inv H0; simpl; omega. (* receptive *) @@ -821,7 +813,6 @@ Proof. split. constructor. intuition congruence. Qed. - Inductive volatile_load_global_sem (chunk: memory_chunk) (id: ident) (ofs: int) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := @@ -861,14 +852,14 @@ Proof. inv H; auto. (* extends *) inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]]. - exists v'; exists m1'; intuition. econstructor; eauto. red; auto. + exists v'; exists m1'; intuition. econstructor; eauto. (* inject *) inv H0. inv H2. assert (val_inject f (Vptr b ofs) (Vptr b ofs)). exploit (proj1 H); eauto. intros EQ. econstructor. eauto. rewrite Int.add_zero; auto. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. econstructor; eauto. - red; auto. red; auto. red; intros; congruence. + red; intros; congruence. (* trace length *) inv H; inv H1; simpl; omega. (* receptive *) @@ -933,25 +924,20 @@ Lemma volatile_store_extends: exists m2', volatile_store ge chunk m1' b ofs v' t m2' /\ Mem.extends m2 m2' - /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'. + /\ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'. Proof. intros. inv H. - econstructor; split. econstructor; eauto. eapply eventval_match_lessdef; eauto. - split. auto. red; auto. - exploit Mem.store_within_extends; eauto. intros [m2' [A B]]. - exists m2'; intuition. econstructor; eauto. - red; split; intros. - eapply Mem.perm_store_1; eauto. - rewrite <- H4. eapply Mem.load_store_other; eauto. - destruct (eq_block b0 b); auto. subst b0; right. - apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) - (Int.unsigned ofs, Int.unsigned ofs + size_chunk chunk)). - red; intros; red; intros. - exploit (H x H5). exploit Mem.store_valid_access_3. eexact H3. intros [E G]. - apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. - auto. - simpl. generalize (size_chunk_pos chunk0). omega. - simpl. generalize (size_chunk_pos chunk). omega. +- econstructor; split. econstructor; eauto. eapply eventval_match_lessdef; eauto. + auto with mem. +- exploit Mem.store_within_extends; eauto. intros [m2' [A B]]. + exists m2'; intuition. ++ econstructor; eauto. ++ eapply Mem.store_unchanged_on; eauto. + unfold loc_out_of_bounds; intros. + assert (Mem.perm m1 b i Max Nonempty). + { apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. + exploit Mem.store_valid_access_3. eexact H3. intros [P Q]. eauto. } + tauto. Qed. Lemma volatile_store_inject: @@ -964,37 +950,28 @@ Lemma volatile_store_inject: exists m2', volatile_store ge chunk m1' b' ofs' v' t m2' /\ Mem.inject f m2 m2' - /\ mem_unchanged_on (loc_unmapped f) m1 m2 - /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2'. + /\ Mem.unchanged_on (loc_unmapped f) m1 m2 + /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'. Proof. intros. inv H0. - inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H9 in EQ; inv EQ. - rewrite Int.add_zero. exists m1'. - split. constructor; auto. eapply eventval_match_inject; eauto. - split. auto. split. red; auto. red; auto. - assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. +- inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H9 in EQ; inv EQ. + rewrite Int.add_zero. exists m1'. intuition. + constructor; auto. eapply eventval_match_inject; eauto. +- assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]]. inv H1. exists m2'; intuition. - constructor; auto. rewrite <- H4. eapply meminj_preserves_block_is_volatile; eauto. - split; intros. eapply Mem.perm_store_1; eauto. - rewrite <- H6. eapply Mem.load_store_other; eauto. - left. exploit (H1 ofs0). generalize (size_chunk_pos chunk0). omega. - unfold loc_unmapped. congruence. - split; intros. eapply Mem.perm_store_1; eauto. - rewrite <- H6. eapply Mem.load_store_other; eauto. - destruct (eq_block b0 b'); auto. subst b0; right. - assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta). - eapply Mem.address_inject; eauto with mem. - unfold Mem.storev in A. rewrite EQ in A. rewrite EQ. - apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) - (Int.unsigned ofs + delta, Int.unsigned ofs + delta + size_chunk chunk)). - red; intros; red; intros. exploit (H1 x H7). eauto. - exploit Mem.store_valid_access_3. eexact H0. intros [C D]. - apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. - apply C. red in H8; simpl in H8. omega. - auto. - simpl. generalize (size_chunk_pos chunk0). omega. - simpl. generalize (size_chunk_pos chunk). omega. ++ constructor; auto. rewrite <- H4. eapply meminj_preserves_block_is_volatile; eauto. ++ eapply Mem.store_unchanged_on; eauto. + unfold loc_unmapped; intros. congruence. ++ eapply Mem.store_unchanged_on; eauto. + unfold loc_out_of_reach; intros. red; intros. simpl in A. + assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta) + by (eapply Mem.address_inject; eauto with mem). + rewrite EQ in *. + eelim H6; eauto. + exploit Mem.store_valid_access_3. eexact H5. intros [P Q]. + apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. + apply P. omega. Qed. Lemma volatile_store_receptive: @@ -1120,13 +1097,15 @@ Proof. forall (P: block -> Z -> Prop) m n m' b m'', Mem.alloc m (-4) (Int.unsigned n) = (m', b) -> Mem.store Mint32 m' b (-4) (Vint n) = Some m'' -> - mem_unchanged_on P m m''). - intros; split; intros. - eauto with mem. - transitivity (Mem.load chunk m' b0 ofs). - eapply Mem.load_store_other; eauto. left. - apply Mem.valid_not_valid_diff with m; eauto with mem. - eapply Mem.load_alloc_other; eauto. + Mem.unchanged_on P m m''). + { + intros; constructor; intros. + - split; intros; eauto with mem. + - assert (b0 <> b) by (eapply Mem.valid_not_valid_diff; eauto with mem). + erewrite Mem.store_mem_contents; eauto. rewrite Maps.PMap.gso by auto. + Local Transparent Mem.alloc. unfold Mem.alloc in H. injection H; intros A B. + rewrite <- B; simpl. rewrite A. rewrite Maps.PMap.gso by auto. auto. + } constructor; intros. (* well typed *) @@ -1139,7 +1118,7 @@ Proof. inv H. eauto with mem. (* perms *) inv H. exploit Mem.perm_alloc_inv. eauto. eapply Mem.perm_store_2; eauto. - rewrite zeq_false. auto. + rewrite dec_eq_false. auto. apply Mem.valid_not_valid_diff with m1; eauto with mem. (* readonly *) inv H. transitivity (Mem.load chunk m' b ofs). @@ -1194,6 +1173,7 @@ Lemma extcall_free_ok: extcall_properties extcall_free_sem (mksignature (Tint :: nil) None). Proof. +(* assert (UNCHANGED: forall (P: block -> Z -> Prop) m b lo hi m', Mem.free m b lo hi = Some m' -> @@ -1201,13 +1181,16 @@ Proof. (forall b' ofs, P b' ofs -> b' <> b \/ ofs < lo \/ hi <= ofs) -> mem_unchanged_on P m m'). intros; split; intros. + split; intros. eapply Mem.perm_free_1; eauto. + eapply Mem.perm_free_3; eauto. rewrite <- H3. eapply Mem.load_free; eauto. destruct (eq_block b0 b); auto. right. right. apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) (lo, hi)). red; intros. apply Intv.notin_range. simpl. exploit H1; eauto. intuition. simpl; generalize (size_chunk_pos chunk); omega. simpl; omega. +*) constructor; intros. (* well typed *) @@ -1239,12 +1222,12 @@ Proof. exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]]. exists Vundef; exists m2'; intuition. econstructor; eauto. - eapply UNCHANGED; eauto. omega. - intros. destruct (eq_block b' b); auto. subst b; right. - assert (~(Int.unsigned lo - 4 <= ofs < Int.unsigned lo + Int.unsigned sz)). - red; intros; elim H. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.free_range_perm. eexact H4. auto. - omega. + eapply Mem.free_unchanged_on; eauto. + unfold loc_out_of_bounds; intros. + assert (Mem.perm m1 b i Max Nonempty). + { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. + eapply Mem.free_range_perm. eexact H4. eauto. } + tauto. (* mem inject *) inv H0. inv H2. inv H7. inv H9. exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. @@ -1278,18 +1261,15 @@ Proof. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. apply H0. omega. eapply Mem.perm_max. eauto with mem. - unfold block; omega. + intuition. - eapply UNCHANGED; eauto. omega. intros. - red in H7. left. congruence. + eapply Mem.free_unchanged_on; eauto. + unfold loc_unmapped; intros. congruence. - eapply UNCHANGED; eauto. omega. intros. - destruct (eq_block b' b2); auto. subst b'. right. - assert (~(Int.unsigned lo + delta - 4 <= ofs < Int.unsigned lo + delta + Int.unsigned sz)). - red; intros. elim (H7 _ _ H6). - apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - apply H0. omega. - omega. + eapply Mem.free_unchanged_on; eauto. + unfold loc_out_of_reach; intros. red; intros. eelim H8; eauto. + apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. + apply H0. omega. red; intros. congruence. (* trace length *) @@ -1351,21 +1331,12 @@ Proof. split. econstructor; eauto. split. constructor. split. auto. - red; split; intros. - eauto with mem. - exploit Mem.loadbytes_length. eexact H8. intros. - rewrite <- H1. eapply Mem.load_storebytes_other; eauto. - destruct (eq_block b bdst); auto. subst b; right. - exploit list_forall2_length; eauto. intros R. - apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) - (Int.unsigned odst, Int.unsigned odst + Z_of_nat (length bytes2))); simpl. - red; unfold Intv.In; simpl; intros; red; intros. - eapply (H x H11). + eapply Mem.storebytes_unchanged_on; eauto. unfold loc_out_of_bounds; intros. + assert (Mem.perm m1 bdst i Max Nonempty). apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. - eapply Mem.storebytes_range_perm. eexact H9. - rewrite R. auto. - generalize (size_chunk_pos chunk). omega. - rewrite <- R. rewrite H10. rewrite nat_of_Z_eq. omega. omega. + eapply Mem.storebytes_range_perm; eauto. + erewrite list_forall2_length; eauto. + tauto. (* injections *) intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12. exploit Mem.loadbytes_length; eauto. intros LEN. @@ -1392,20 +1363,13 @@ Proof. apply Mem.range_perm_max with Cur; auto. split. constructor. split. auto. - split. red; split; intros. eauto with mem. - rewrite <- H2. eapply Mem.load_storebytes_other; eauto. - destruct (eq_block b bdst); auto. subst b. - assert (loc_unmapped f bdst ofs). apply H0. generalize (size_chunk_pos chunk); omega. - red in H12. congruence. - split. red; split; intros. eauto with mem. - rewrite <- H2. eapply Mem.load_storebytes_other; eauto. - destruct (eq_block b b0); auto. subst b0; right. - rewrite <- (list_forall2_length B). rewrite LEN. rewrite nat_of_Z_eq; try omega. - apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) - (Int.unsigned odst + delta0, Int.unsigned odst + delta0 + sz)); simpl. - red; unfold Intv.In; simpl; intros; red; intros. - eapply (H0 x H12). eauto. apply Mem.perm_cur_max. apply RPDST. omega. - generalize (size_chunk_pos chunk); omega. + split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. + congruence. + split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros. + eelim H2; eauto. + apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. + eapply Mem.storebytes_range_perm; eauto. + erewrite list_forall2_length; eauto. omega. split. apply inject_incr_refl. red; intros; congruence. @@ -1452,15 +1416,12 @@ Proof. exists vres; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_lessdef; eauto. - red; auto. (* mem injects *) inv H0. exists f; exists vres; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_inject; eauto. eapply eventval_match_inject_2; eauto. - red; auto. - red; auto. red; intros; congruence. (* trace length *) inv H; simpl; omega. @@ -1518,14 +1479,11 @@ Proof. exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_lessdef; eauto. - red; auto. (* mem injects *) inv H0. exists f; exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_inject; eauto. - red; auto. - red; auto. red; intros; congruence. (* trace length *) inv H; simpl; omega. @@ -1567,14 +1525,11 @@ Proof. exists v2; exists m1'; intuition. econstructor; eauto. eapply eventval_match_lessdef; eauto. - red; auto. inv H0. inv H2. inv H7. exists f; exists v'; exists m1'; intuition. econstructor; eauto. eapply eventval_match_inject; eauto. - red; auto. - red; auto. red; intros; congruence. inv H; simpl; omega. @@ -1687,12 +1642,12 @@ Qed. Lemma external_call_nextblock: forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2, external_call ef ge vargs m1 t vres m2 -> - Mem.nextblock m1 <= Mem.nextblock m2. + Ple (Mem.nextblock m1) (Mem.nextblock m2). Proof. - intros. - exploit external_call_valid_block; eauto. - instantiate (1 := Mem.nextblock m1 - 1). red; omega. - unfold Mem.valid_block. omega. + intros. destruct (plt (Mem.nextblock m2) (Mem.nextblock m1)). + exploit external_call_valid_block; eauto. intros. + eelim Plt_strict; eauto. + unfold Plt, Ple in *; zify; omega. Qed. (** Corollaries of [external_call_determ]. *) @@ -1822,6 +1777,14 @@ Proof. intros. inv H. eapply external_call_valid_block; eauto. Qed. +Lemma external_call_nextblock': + forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2, + external_call' ef ge vargs m1 t vres m2 -> + Ple (Mem.nextblock m1) (Mem.nextblock m2). +Proof. + intros. inv H. eapply external_call_nextblock; eauto. +Qed. + Lemma external_call_mem_extends': forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2 m1' vargs', external_call' ef ge vargs m1 t vres m2 -> @@ -1831,7 +1794,7 @@ Lemma external_call_mem_extends': external_call' ef ge vargs' m1' t vres' m2' /\ Val.lessdef_list vres vres' /\ Mem.extends m2 m2' - /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'. + /\ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'. Proof. intros. inv H. exploit external_call_mem_extends; eauto. @@ -1852,8 +1815,8 @@ Lemma external_call_mem_inject': external_call' ef ge vargs' m1' t vres' m2' /\ val_list_inject f' vres vres' /\ Mem.inject f' m2 m2' - /\ mem_unchanged_on (loc_unmapped f) m1 m2 - /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2' + /\ Mem.unchanged_on (loc_unmapped f) m1 m2 + /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' /\ inject_incr f f' /\ inject_separated f f' m1 m1'. Proof. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index a082819..4e155e3 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -83,15 +83,14 @@ Variable V: Type. (**r The type of information attached to variables *) Record t: Type := mkgenv { genv_symb: PTree.t block; (**r mapping symbol -> block *) - genv_funs: ZMap.t (option F); (**r mapping function pointer -> definition *) - genv_vars: ZMap.t (option (globvar V)); (**r mapping variable pointer -> info *) + genv_funs: PTree.t F; (**r mapping function pointer -> definition *) + genv_vars: PTree.t (globvar V); (**r mapping variable pointer -> info *) genv_next: block; (**r next symbol pointer *) - genv_next_pos: genv_next > 0; - genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> 0 < b < genv_next; - genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> 0 < b < genv_next; - genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_next; + genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> Plt b genv_next; + genv_funs_range: forall b f, PTree.get b genv_funs = Some f -> Plt b genv_next; + genv_vars_range: forall b v, PTree.get b genv_vars = Some v -> Plt b genv_next; genv_funs_vars: forall b1 b2 f v, - ZMap.get b1 genv_funs = Some f -> ZMap.get b2 genv_vars = Some v -> b1 <> b2; + PTree.get b1 genv_funs = Some f -> PTree.get b2 genv_vars = Some v -> b1 <> b2; genv_vars_inj: forall id1 id2 b, PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2 }. @@ -107,7 +106,7 @@ Definition find_symbol (ge: t) (id: ident) : option block := the given address. *) Definition find_funct_ptr (ge: t) (b: block) : option F := - ZMap.get b ge.(genv_funs). + PTree.get b ge.(genv_funs). (** [find_funct] is similar to [find_funct_ptr], but the function address is given as a value, which must be a pointer with offset 0. *) @@ -129,7 +128,7 @@ Definition invert_symbol (ge: t) (b: block) : option ident := at address [b]. *) Definition find_var_info (ge: t) (b: block) : option (globvar V) := - ZMap.get b ge.(genv_vars). + PTree.get b ge.(genv_vars). (** ** Constructing the global environment *) @@ -137,48 +136,46 @@ Program Definition add_global (ge: t) (idg: ident * globdef F V) : t := @mkgenv (PTree.set idg#1 ge.(genv_next) ge.(genv_symb)) (match idg#2 with - | Gfun f => ZMap.set ge.(genv_next) (Some f) ge.(genv_funs) + | Gfun f => PTree.set ge.(genv_next) f ge.(genv_funs) | Gvar v => ge.(genv_funs) end) (match idg#2 with | Gfun f => ge.(genv_vars) - | Gvar v => ZMap.set ge.(genv_next) (Some v) ge.(genv_vars) + | Gvar v => PTree.set ge.(genv_next) v ge.(genv_vars) end) - (ge.(genv_next) + 1) - _ _ _ _ _ _. -Next Obligation. - destruct ge; simpl; omega. -Qed. + (Psucc ge.(genv_next)) + _ _ _ _ _. Next Obligation. destruct ge; simpl in *. - rewrite PTree.gsspec in H. destruct (peq id i). inv H. unfold block; omega. - exploit genv_symb_range0; eauto. unfold block; omega. + rewrite PTree.gsspec in H. destruct (peq id i). inv H. apply Plt_succ. + apply Plt_trans_succ; eauto. Qed. Next Obligation. destruct ge; simpl in *. destruct g. - rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b genv_next0). subst; omega. - exploit genv_funs_range0; eauto. omega. - exploit genv_funs_range0; eauto. omega. + rewrite PTree.gsspec in H. + destruct (peq b genv_next0). inv H. apply Plt_succ. + apply Plt_trans_succ; eauto. + apply Plt_trans_succ; eauto. Qed. Next Obligation. destruct ge; simpl in *. - destruct g. - exploit genv_vars_range0; eauto. omega. - rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b genv_next0). subst; omega. - exploit genv_vars_range0; eauto. omega. + destruct g. + apply Plt_trans_succ; eauto. + rewrite PTree.gsspec in H. + destruct (peq b genv_next0). inv H. apply Plt_succ. + apply Plt_trans_succ; eauto. Qed. Next Obligation. - destruct ge; simpl in *. destruct g. - rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b1 genv_next0). inv H. - exploit genv_vars_range0; eauto. unfold ZIndexed.t; omega. + destruct ge; simpl in *. + destruct g. + rewrite PTree.gsspec in H. + destruct (peq b1 genv_next0). inv H. + apply sym_not_equal; apply Plt_ne; eauto. eauto. - rewrite ZMap.gsspec in H0. - destruct (ZIndexed.eq b2 genv_next0). inv H. - exploit genv_funs_range0; eauto. unfold ZIndexed.t; omega. + rewrite PTree.gsspec in H0. + destruct (peq b2 genv_next0). inv H0. + apply Plt_ne; eauto. eauto. Qed. Next Obligation. @@ -186,8 +183,8 @@ Next Obligation. rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. destruct (peq id1 i); destruct (peq id2 i). congruence. - exploit genv_symb_range0; eauto. intros [A B]. inv H. omegaContradiction. - exploit genv_symb_range0; eauto. intros [A B]. inv H0. omegaContradiction. + inv H. eelim Plt_strict. eapply genv_symb_range0; eauto. + inv H0. eelim Plt_strict. eapply genv_symb_range0; eauto. eauto. Qed. @@ -202,21 +199,18 @@ Proof. Qed. Program Definition empty_genv : t := - @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) 1 _ _ _ _ _ _. -Next Obligation. - omega. -Qed. + @mkgenv (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _. Next Obligation. rewrite PTree.gempty in H. discriminate. Qed. Next Obligation. - rewrite ZMap.gi in H. discriminate. + rewrite PTree.gempty in H. discriminate. Qed. Next Obligation. - rewrite ZMap.gi in H. discriminate. + rewrite PTree.gempty in H. discriminate. Qed. Next Obligation. - rewrite ZMap.gi in H. discriminate. + rewrite PTree.gempty in H. discriminate. Qed. Next Obligation. rewrite PTree.gempty in H. discriminate. @@ -317,12 +311,12 @@ Proof. intros. unfold find_symbol, find_funct_ptr in *; simpl. destruct H1 as [b [A B]]. exists b; split. rewrite PTree.gso; auto. - destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto. - exploit genv_funs_range; eauto. unfold ZIndexed.t; omega. + destruct g1 as [f1 | v1]. rewrite PTree.gso. auto. + apply Plt_ne. eapply genv_funs_range; eauto. auto. (* ensures *) intros. unfold find_symbol, find_funct_ptr in *; simpl. - exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. + exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. Qed. Theorem find_var_exists: @@ -338,11 +332,11 @@ Proof. intros. unfold find_symbol, find_var_info in *; simpl. destruct H1 as [b [A B]]. exists b; split. rewrite PTree.gso; auto. - destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto. - exploit genv_vars_range; eauto. unfold ZIndexed.t; omega. + destruct g1 as [f1 | v1]. auto. rewrite PTree.gso. auto. + apply Plt_ne. eapply genv_vars_range; eauto. (* ensures *) intros. unfold find_symbol, find_var_info in *; simpl. - exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. + exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. Qed. Lemma find_symbol_inversion : forall p x b, @@ -366,11 +360,11 @@ Proof. intros until f. unfold globalenv. apply add_globals_preserves. (* preserves *) unfold find_funct_ptr; simpl; intros. destruct g; auto. - rewrite ZMap.gsspec in H1. destruct (ZIndexed.eq b (genv_next ge)). + rewrite PTree.gsspec in H1. destruct (peq b (genv_next ge)). inv H1. exists id; auto. auto. (* base *) - unfold find_funct_ptr; simpl; intros. rewrite ZMap.gi in H. discriminate. + unfold find_funct_ptr; simpl; intros. rewrite PTree.gempty in H. discriminate. Qed. Theorem find_funct_inversion: @@ -410,22 +404,15 @@ Proof. intros until f. unfold globalenv, find_symbol, find_funct_ptr. apply add_globals_preserves. (* preserves *) intros. simpl in *. rewrite PTree.gsspec in H1. destruct (peq id id0). - inv H1. destruct g as [f1|v1]. rewrite ZMap.gss in H2. inv H2. auto. - exploit genv_funs_range; eauto. intros. omegaContradiction. - destruct g as [f1|v1]. rewrite ZMap.gso in H2. auto. - exploit genv_symb_range; eauto. unfold ZIndexed.t; omega. + inv H1. destruct g as [f1|v1]. rewrite PTree.gss in H2. inv H2. auto. + eelim Plt_strict. eapply genv_funs_range; eauto. + destruct g as [f1|v1]. rewrite PTree.gso in H2. auto. + apply Plt_ne. eapply genv_symb_range; eauto. auto. (* initial *) intros. simpl in *. rewrite PTree.gempty in H. discriminate. Qed. -Theorem find_symbol_not_nullptr: - forall p id b, - find_symbol (globalenv p) id = Some b -> b <> Mem.nullptr. -Proof. - intros until b. unfold find_symbol. destruct (globalenv p); simpl. - intros. exploit genv_symb_range0; eauto. unfold Mem.nullptr, block. omega. -Qed. Theorem global_addresses_distinct: forall ge id1 id2 b1 b2, @@ -470,14 +457,16 @@ Proof. congruence. Qed. +Definition advance_next (gl: list (ident * globdef F V)) (x: positive) := + List.fold_left (fun n g => Psucc n) gl x. + Remark genv_next_add_globals: forall gl ge, - genv_next (add_globals ge gl) = genv_next ge + Z_of_nat (length gl). + genv_next (add_globals ge gl) = advance_next gl (genv_next ge). Proof. - induction gl; intros. - simpl. unfold block; omega. - simpl add_globals; simpl length; rewrite inj_S. - rewrite IHgl. simpl. unfold block; omega. + induction gl; simpl; intros. + auto. + rewrite IHgl. auto. Qed. (** * Construction of the initial memory state *) @@ -609,7 +598,7 @@ Qed. Remark alloc_global_nextblock: forall g m m', alloc_global m g = Some m' -> - Mem.nextblock m' = Zsucc(Mem.nextblock m). + Mem.nextblock m' = Psucc(Mem.nextblock m). Proof. unfold alloc_global. intros. destruct g as [id [f|v]]. @@ -631,13 +620,12 @@ Qed. Remark alloc_globals_nextblock: forall gl m m', alloc_globals m gl = Some m' -> - Mem.nextblock m' = Mem.nextblock m + Z_of_nat(List.length gl). + Mem.nextblock m' = advance_next gl (Mem.nextblock m). Proof. - induction gl. - simpl; intros. inv H; unfold block; omega. - simpl length; rewrite inj_S; simpl; intros. + induction gl; simpl; intros. + congruence. destruct (alloc_global m a) as [m1|] eqn:?; try discriminate. - erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto. unfold block; omega. + erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto. Qed. (** Permissions *) @@ -712,7 +700,8 @@ Proof. simpl; intros. inv H. tauto. simpl; intros. destruct (alloc_global m a) as [m1|] eqn:?; try discriminate. erewrite alloc_global_perm; eauto. eapply IHgl; eauto. - unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. omega. + unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. + apply Plt_trans_succ; auto. Qed. (** Data preservation properties *) @@ -727,8 +716,8 @@ Proof. intros until n. functional induction (store_zeros m b p n); intros. inv H; auto. transitivity (Mem.load chunk m' b' p'). - apply IHo. auto. unfold block in *; omega. - eapply Mem.load_store_other; eauto. simpl. unfold block in *; omega. + apply IHo. auto. intuition omega. + eapply Mem.load_store_other; eauto. simpl. intuition omega. discriminate. Qed. @@ -847,7 +836,8 @@ Proof. destruct (alloc_global m a) as [m''|] eqn:?; try discriminate. transitivity (Mem.load chunk m'' b p). apply IHgl; auto. unfold Mem.valid_block in *. - erewrite alloc_global_nextblock; eauto. omega. + erewrite alloc_global_nextblock; eauto. + apply Plt_trans with (Mem.nextblock m); auto. apply Plt_succ. destruct a as [id g]. eapply load_alloc_global; eauto. Qed. @@ -894,14 +884,14 @@ Proof. red; intros. unfold find_var_info in H3. simpl in H3. exploit H1; eauto. intros [A [B C]]. assert (D: Mem.valid_block m b). - red. exploit genv_vars_range; eauto. rewrite H; omega. + red. exploit genv_vars_range; eauto. rewrite H; auto. split. red; intros. erewrite <- alloc_global_perm; eauto. split. intros. eapply B. erewrite alloc_global_perm; eauto. intros. apply load_store_init_data_invariant with m; auto. intros. eapply load_alloc_global; eauto. (* variable *) - red; intros. unfold find_var_info in H3. simpl in H3. rewrite ZMap.gsspec in H3. - destruct (ZIndexed.eq b (genv_next ge0)). + red; intros. unfold find_var_info in H3. simpl in H3. rewrite PTree.gsspec in H3. + destruct (peq b (genv_next ge0)). (* same *) inv H3. simpl in H0. set (init := gvar_init gv) in *. @@ -927,7 +917,7 @@ Proof. (* older var *) exploit H1; eauto. intros [A [B C]]. assert (D: Mem.valid_block m b). - red. exploit genv_vars_range; eauto. rewrite H; omega. + red. exploit genv_vars_range; eauto. rewrite H; auto. split. red; intros. erewrite <- alloc_global_perm; eauto. split. intros. eapply B. erewrite alloc_global_perm; eauto. intros. apply load_store_init_data_invariant with m; auto. @@ -935,8 +925,8 @@ Proof. (* functions-initialized *) split. destruct g as [f|v]. (* function *) - red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite ZMap.gsspec in H3. - destruct (ZIndexed.eq b (genv_next ge0)). + red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite PTree.gsspec in H3. + destruct (peq b (genv_next ge0)). (* same *) inv H3. simpl in H0. destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. @@ -951,18 +941,18 @@ Proof. (* older function *) exploit H2; eauto. intros [A B]. assert (D: Mem.valid_block m b). - red. exploit genv_funs_range; eauto. rewrite H; omega. + red. exploit genv_funs_range; eauto. rewrite H; auto. split. erewrite <- alloc_global_perm; eauto. intros. eapply B. erewrite alloc_global_perm; eauto. (* variables *) red; intros. unfold find_funct_ptr in H3. simpl in H3. exploit H2; eauto. intros [A B]. assert (D: Mem.valid_block m b). - red. exploit genv_funs_range; eauto. rewrite H; omega. + red. exploit genv_funs_range; eauto. rewrite H; auto. split. erewrite <- alloc_global_perm; eauto. intros. eapply B. erewrite alloc_global_perm; eauto. (* nextblock *) - rewrite NB. simpl. rewrite H. unfold block; omega. + rewrite NB. simpl. rewrite H. auto. Qed. Lemma alloc_globals_initialized: @@ -1001,7 +991,7 @@ Theorem find_symbol_not_fresh: find_symbol (globalenv p) id = Some b -> Mem.valid_block m b. Proof. intros. red. erewrite <- init_mem_genv_next; eauto. - exploit genv_symb_range; eauto. omega. + eapply genv_symb_range; eauto. Qed. Theorem find_funct_ptr_not_fresh: @@ -1010,7 +1000,7 @@ Theorem find_funct_ptr_not_fresh: find_funct_ptr (globalenv p) b = Some f -> Mem.valid_block m b. Proof. intros. red. erewrite <- init_mem_genv_next; eauto. - exploit genv_funs_range; eauto. omega. + eapply genv_funs_range; eauto. Qed. Theorem find_var_info_not_fresh: @@ -1019,7 +1009,7 @@ Theorem find_var_info_not_fresh: find_var_info (globalenv p) b = Some gv -> Mem.valid_block m b. Proof. intros. red. erewrite <- init_mem_genv_next; eauto. - exploit genv_vars_range; eauto. omega. + eapply genv_vars_range; eauto. Qed. Theorem init_mem_characterization: @@ -1033,8 +1023,8 @@ Theorem init_mem_characterization: Proof. intros. eapply alloc_globals_initialized; eauto. rewrite Mem.nextblock_empty. auto. - red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction. - red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction. + red; intros. unfold find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence. + red; intros. unfold find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence. Qed. Theorem init_mem_characterization_2: @@ -1045,9 +1035,9 @@ Theorem init_mem_characterization_2: /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p). Proof. intros. unfold init_mem in H0. eapply alloc_globals_initialized; eauto. - rewrite Mem.nextblock_empty. auto. - red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction. - red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction. + rewrite Mem.nextblock_empty. auto. + red; intros. unfold find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence. + red; intros. unfold find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence. Qed. (** ** Compatibility with memory injections *) @@ -1056,12 +1046,12 @@ Section INITMEM_INJ. Variable ge: t. Variable thr: block. -Hypothesis symb_inject: forall id b, find_symbol ge id = Some b -> b < thr. +Hypothesis symb_inject: forall id b, find_symbol ge id = Some b -> Plt b thr. Lemma store_zeros_neutral: forall m b p n m', Mem.inject_neutral thr m -> - b < thr -> + Plt b thr -> store_zeros m b p n = Some m' -> Mem.inject_neutral thr m'. Proof. @@ -1074,30 +1064,29 @@ Qed. Lemma store_init_data_neutral: forall m b p id m', Mem.inject_neutral thr m -> - b < thr -> + Plt b thr -> store_init_data ge m b p id = Some m' -> Mem.inject_neutral thr m'. Proof. intros. destruct id; simpl in H1; try (eapply Mem.store_inject_neutral; eauto; fail). congruence. - revert H1. caseEq (find_symbol ge i); try congruence. intros b' FS ST. + destruct (find_symbol ge i) as [b'|] eqn:E; try discriminate. eapply Mem.store_inject_neutral; eauto. - econstructor. unfold Mem.flat_inj. apply zlt_true; eauto. + econstructor. unfold Mem.flat_inj. apply pred_dec_true; auto. eauto. rewrite Int.add_zero. auto. Qed. Lemma store_init_data_list_neutral: forall b idl m p m', Mem.inject_neutral thr m -> - b < thr -> + Plt b thr -> store_init_data_list ge m b p idl = Some m' -> Mem.inject_neutral thr m'. Proof. - induction idl; simpl. - intros; congruence. - intros until m'; intros INJ FB. - caseEq (store_init_data ge m b p a); try congruence. intros. + induction idl; simpl; intros. + congruence. + destruct (store_init_data ge m b p a) as [m1|] eqn:E; try discriminate. eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto. Qed. @@ -1105,13 +1094,13 @@ Lemma alloc_global_neutral: forall idg m m', alloc_global ge m idg = Some m' -> Mem.inject_neutral thr m -> - Mem.nextblock m < thr -> + Plt (Mem.nextblock m) thr -> Mem.inject_neutral thr m'. Proof. intros. destruct idg as [id [f|v]]; simpl in H. (* function *) destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. - assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. + assert (Plt b thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. eapply Mem.drop_inject_neutral; eauto. eapply Mem.alloc_inject_neutral; eauto. (* variable *) @@ -1120,27 +1109,35 @@ Proof. destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?. destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate. destruct (store_init_data_list ge m2 b 0 init) as [m3|] eqn:?; try discriminate. - assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. + assert (Plt b thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. eapply Mem.drop_inject_neutral; eauto. eapply store_init_data_list_neutral with (m := m2) (b := b); eauto. eapply store_zeros_neutral with (m := m1); eauto. eapply Mem.alloc_inject_neutral; eauto. Qed. +Remark advance_next_le: forall gl x, Ple x (advance_next gl x). +Proof. + induction gl; simpl; intros. + apply Ple_refl. + apply Ple_trans with (Psucc x). apply Ple_succ. eauto. +Qed. + Lemma alloc_globals_neutral: forall gl m m', alloc_globals ge m gl = Some m' -> Mem.inject_neutral thr m -> - Mem.nextblock m' <= thr -> + Ple (Mem.nextblock m') thr -> Mem.inject_neutral thr m'. Proof. - induction gl; simpl. - intros. congruence. - intros until m'. caseEq (alloc_global ge m a); try congruence. intros. - assert (Mem.nextblock m' = Mem.nextblock m + Z_of_nat(length (a :: gl))). - eapply alloc_globals_nextblock with ge. simpl. rewrite H. auto. - simpl length in H3. rewrite inj_S in H3. - exploit alloc_global_neutral; eauto. unfold block in *; omega. + induction gl; intros. + simpl in *. congruence. + exploit alloc_globals_nextblock; eauto. intros EQ. + simpl in *. destruct (alloc_global ge m a) as [m1|] eqn:E; try discriminate. + exploit alloc_global_neutral; eauto. + assert (Ple (Psucc (Mem.nextblock m)) (Mem.nextblock m')). + { rewrite EQ. apply advance_next_le. } + unfold Plt, Ple in *; zify; omega. Qed. End INITMEM_INJ. @@ -1155,7 +1152,7 @@ Proof. eapply alloc_globals_neutral; eauto. intros. exploit find_symbol_not_fresh; eauto. apply Mem.empty_inject_neutral. - omega. + apply Ple_refl. Qed. Section INITMEM_AUGMENT_INJ. @@ -1166,23 +1163,23 @@ Variable thr: block. Lemma store_zeros_augment: forall m1 m2 b p n m2', Mem.inject (Mem.flat_inj thr) m1 m2 -> - b >= thr -> + Ple thr b -> store_zeros m2 b p n = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2'. Proof. intros until n. functional induction (store_zeros m2 b p n); intros. inv H1; auto. apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. - intros. exfalso. unfold Mem.flat_inj in H2. destruct (zlt b' thr). - inversion H2; subst; omega. - discriminate. - inv H1. + intros. exfalso. unfold Mem.flat_inj in H2. destruct (plt b' thr). + inv H2. unfold Plt, Ple in *. zify; omega. + discriminate. + discriminate. Qed. Lemma store_init_data_augment: forall m1 m2 b p id m2', Mem.inject (Mem.flat_inj thr) m1 m2 -> - b >= thr -> + Ple thr b -> store_init_data ge m2 b p id = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2'. Proof. @@ -1192,7 +1189,7 @@ Proof. Mem.inject (Mem.flat_inj thr) m1 m2'). intros. eapply Mem.store_outside_inject; eauto. intros. unfold Mem.flat_inj in H0. - destruct (zlt b' thr); inversion H0; subst. omega. + destruct (plt b' thr); inv H0. unfold Plt, Ple in *. zify; omega. destruct id; simpl in ST; try (eapply P; eauto; fail). congruence. revert ST. caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. @@ -1201,7 +1198,7 @@ Qed. Lemma store_init_data_list_augment: forall b idl m1 m2 p m2', Mem.inject (Mem.flat_inj thr) m1 m2 -> - b >= thr -> + Ple thr b -> store_init_data_list ge m2 b p idl = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2'. Proof. @@ -1216,37 +1213,37 @@ Lemma alloc_global_augment: forall idg m1 m2 m2', alloc_global ge m2 idg = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2 -> - Mem.nextblock m2 >= thr -> + Ple thr (Mem.nextblock m2) -> Mem.inject (Mem.flat_inj thr) m1 m2'. Proof. intros. destruct idg as [id [f|v]]; simpl in H. (* function *) destruct (Mem.alloc m2 0 1) as [m3 b] eqn:?. - assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. + assert (Ple thr b). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. eapply Mem.drop_outside_inject. 2: eauto. eapply Mem.alloc_right_inject; eauto. - intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3. - subst; exfalso; omega. + intros. unfold Mem.flat_inj in H3. destruct (plt b' thr); inv H3. + unfold Plt, Ple in *. zify; omega. (* variable *) set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. destruct (Mem.alloc m2 0 sz) as [m3 b] eqn:?. destruct (store_zeros m3 b 0 sz) as [m4|] eqn:?; try discriminate. destruct (store_init_data_list ge m4 b 0 init) as [m5|] eqn:?; try discriminate. - assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. + assert (Ple thr b). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. eapply Mem.drop_outside_inject. 2: eauto. eapply store_init_data_list_augment. 3: eauto. 2: eauto. eapply store_zeros_augment. 3: eauto. 2: eauto. eapply Mem.alloc_right_inject; eauto. - intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3. - subst; exfalso; omega. + intros. unfold Mem.flat_inj in H3. destruct (plt b' thr); inv H3. + unfold Plt, Ple in *. zify; omega. Qed. Lemma alloc_globals_augment: forall gl m1 m2 m2', alloc_globals ge m2 gl = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2 -> - Mem.nextblock m2 >= thr -> + Ple thr (Mem.nextblock m2) -> Mem.inject (Mem.flat_inj thr) m1 m2'. Proof. induction gl; simpl. @@ -1255,7 +1252,7 @@ Proof. eapply IHgl with (m2 := m); eauto. eapply alloc_global_augment; eauto. rewrite (alloc_global_nextblock _ _ _ H). - unfold block in *; omega. + apply Ple_trans with (Mem.nextblock m2); auto. apply Ple_succ. Qed. End INITMEM_AUGMENT_INJ. @@ -1280,26 +1277,26 @@ Inductive match_globvar: globvar V -> globvar W -> Prop := Record match_genvs (new_globs : list (ident * globdef B W)) (ge1: t A V) (ge2: t B W): Prop := { mge_next: - genv_next ge2 = genv_next ge1 + Z_of_nat(length new_globs); + genv_next ge2 = advance_next new_globs (genv_next ge1); mge_symb: forall id, ~ In id (map fst new_globs) -> PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1); mge_funs: - forall b f, ZMap.get b (genv_funs ge1) = Some f -> - exists tf, ZMap.get b (genv_funs ge2) = Some tf /\ match_fun f tf; + forall b f, PTree.get b (genv_funs ge1) = Some f -> + exists tf, PTree.get b (genv_funs ge2) = Some tf /\ match_fun f tf; mge_rev_funs: - forall b tf, ZMap.get b (genv_funs ge2) = Some tf -> - if zlt b (genv_next ge1) then - exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf + forall b tf, PTree.get b (genv_funs ge2) = Some tf -> + if plt b (genv_next ge1) then + exists f, PTree.get b (genv_funs ge1) = Some f /\ match_fun f tf else In (Gfun tf) (map snd new_globs); mge_vars: - forall b v, ZMap.get b (genv_vars ge1) = Some v -> - exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_globvar v tv; + forall b v, PTree.get b (genv_vars ge1) = Some v -> + exists tv, PTree.get b (genv_vars ge2) = Some tv /\ match_globvar v tv; mge_rev_vars: - forall b tv, ZMap.get b (genv_vars ge2) = Some tv -> - if zlt b (genv_next ge1) then - exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv + forall b tv, PTree.get b (genv_vars ge2) = Some tv -> + if plt b (genv_next ge1) then + exists v, PTree.get b (genv_vars ge1) = Some v /\ match_globvar v tv else In (Gvar tv) (map snd new_globs) }. @@ -1310,50 +1307,49 @@ Lemma add_global_match: match_globdef match_fun match_varinfo idg1 idg2 -> match_genvs nil (add_global ge1 idg1) (add_global ge2 idg2). Proof. - intros. destruct H. - simpl in mge_next0. rewrite Zplus_0_r in mge_next0. + intros. destruct H. simpl in mge_next0. inv H0. (* two functions *) constructor; simpl. - rewrite Zplus_0_r. congruence. + congruence. intros. rewrite mge_next0. repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. - rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_next ge1)). + rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. + destruct (peq b (genv_next ge1)). exists f2; split; congruence. eauto. - rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_next ge1)). - subst b. rewrite zlt_true. exists f1; split; congruence. omega. + rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. + destruct (peq b (genv_next ge1)). + subst b. rewrite pred_dec_true. exists f1; split; congruence. apply Plt_succ. pose proof (mge_rev_funs0 b tf H0). - destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto. contradiction. eauto. intros. pose proof (mge_rev_vars0 b tv H0). - destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. + apply Plt_trans with (genv_next ge1); auto. apply Plt_succ. contradiction. (* two variables *) constructor; simpl. - rewrite Zplus_0_r. congruence. + congruence. intros. rewrite mge_next0. repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. eauto. intros. pose proof (mge_rev_funs0 b tf H0). - destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto. contradiction. - rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_next ge1)). + rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. + destruct (peq b (genv_next ge1)). econstructor; split. eauto. inv H0. constructor; auto. eauto. - rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_next ge1)). - subst b. rewrite zlt_true. - econstructor; split. eauto. inv H0. constructor; auto. - omega. + rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. + destruct (peq b (genv_next ge1)). + subst b. rewrite pred_dec_true. + econstructor; split. eauto. inv H0. constructor; auto. apply Plt_succ. pose proof (mge_rev_vars0 b tv H0). - destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto. contradiction. Qed. @@ -1372,31 +1368,36 @@ Lemma add_global_augment_match: match_genvs new_globs ge1 ge2 -> match_genvs (new_globs ++ (idg :: nil)) ge1 (add_global ge2 idg). Proof. - intros. destruct H. constructor; simpl. - rewrite mge_next0. rewrite app_length. - simpl. rewrite inj_plus. change (Z_of_nat 1) with 1. unfold block; omega. + intros. destruct H. + assert (LE: Ple (genv_next ge1) (genv_next ge2)). + { rewrite mge_next0; apply advance_next_le. } + constructor; simpl. + rewrite mge_next0. unfold advance_next. rewrite fold_left_app. simpl. auto. intros. rewrite map_app in H. rewrite in_app in H. simpl in H. destruct (peq id idg#1). subst. intuition. rewrite PTree.gso. apply mge_symb0. intuition. auto. intros. destruct idg as [id1 [f1|v1]]; simpl; eauto. - rewrite ZMap.gso. eauto. exploit genv_funs_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega. + rewrite PTree.gso. eauto. + exploit genv_funs_range; eauto. intros. + unfold Plt, Ple in *; zify; omega. intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H. - rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)). - rewrite zlt_false. rewrite in_app. simpl; right; left. congruence. - subst b. rewrite mge_next0. omega. - exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto. + rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). + rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence. + subst b. unfold Plt, Ple in *; zify; omega. + exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. rewrite in_app. tauto. - exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto. + exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. rewrite in_app. tauto. intros. destruct idg as [id1 [f1|v1]]; simpl; eauto. - rewrite ZMap.gso. eauto. exploit genv_vars_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega. + rewrite PTree.gso. eauto. exploit genv_vars_range; eauto. + unfold Plt, Ple in *; zify; omega. intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H. - exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto. + exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. rewrite in_app. tauto. - rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)). - rewrite zlt_false. rewrite in_app. simpl; right; left. congruence. - subst b. rewrite mge_next0. omega. - exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto. + rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). + rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence. + subst b. unfold Plt, Ple in *; zify; omega. + exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. rewrite in_app. tauto. Qed. @@ -1427,7 +1428,7 @@ Proof. change new_globs with (nil ++ new_globs) at 1. apply add_globals_augment_match. apply add_globals_match; auto. - constructor; simpl; auto; intros; rewrite ZMap.gi in H; congruence. + constructor; simpl; auto; intros; rewrite PTree.gempty in H; congruence. Qed. Theorem find_funct_ptr_match: @@ -1440,7 +1441,7 @@ Proof (mge_funs globalenvs_match). Theorem find_funct_ptr_rev_match: forall (b : block) (tf : B), find_funct_ptr (globalenv p') b = Some tf -> - if zlt b (genv_next (globalenv p)) then + if plt b (genv_next (globalenv p)) then exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf else In (Gfun tf) (map snd new_globs). @@ -1467,7 +1468,7 @@ Proof. rewrite find_funct_find_funct_ptr in H. rewrite find_funct_find_funct_ptr. apply find_funct_ptr_rev_match in H. - destruct (zlt b (genv_next (globalenv p))); auto. + destruct (plt b (genv_next (globalenv p))); auto. Qed. Theorem find_var_info_match: @@ -1480,7 +1481,7 @@ Proof (mge_vars globalenvs_match). Theorem find_var_info_rev_match: forall (b : block) (tv : globvar W), find_var_info (globalenv p') b = Some tv -> - if zlt b (genv_next (globalenv p)) then + if plt b (genv_next (globalenv p)) then exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv else In (Gvar tv) (map snd new_globs). @@ -1597,18 +1598,18 @@ Proof. intros. unfold find_symbol, find_funct_ptr in *; simpl. destruct H1 as [b [X Y]]. exists b; split. rewrite PTree.gso; auto. - destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto. - exploit genv_funs_range; eauto. unfold ZIndexed.t; omega. + destruct g1 as [f1 | v1]. rewrite PTree.gso. auto. + apply Plt_ne. eapply genv_funs_range; eauto. auto. (* ensures *) intros. unfold find_symbol, find_funct_ptr in *; simpl. - exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. + exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. Qed. Theorem find_funct_ptr_rev_transf_augment: forall (b: block) (tf: B), find_funct_ptr (globalenv p') b = Some tf -> - if zlt b (genv_next (globalenv p)) then + if plt b (genv_next (globalenv p)) then (exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf) else In (Gfun tf) (map snd new_globs). @@ -1662,24 +1663,24 @@ Proof. intros. unfold find_symbol, find_var_info in *; simpl. destruct H1 as [b [X Y]]. exists b; split. rewrite PTree.gso; auto. - destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto. - exploit genv_vars_range; eauto. unfold ZIndexed.t; omega. + destruct g1 as [f1 | v1]. auto. rewrite PTree.gso. auto. + red; intros; subst b. eelim Plt_strict. eapply genv_vars_range; eauto. (* ensures *) intros. unfold find_symbol, find_var_info in *; simpl. - exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. + exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. Qed. Theorem find_var_info_rev_transf_augment: forall (b: block) (v': globvar W), find_var_info (globalenv p') b = Some v' -> - if zlt b (genv_next (globalenv p)) then + if plt b (genv_next (globalenv p)) then (exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v') else (In (Gvar v') (map snd new_globs)). Proof. intros. exploit find_var_info_rev_match. eexact prog_match. eauto. - destruct (zlt b (genv_next (globalenv p))); auto. + destruct (plt b (genv_next (globalenv p))); auto. intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl. rewrite H0; simpl. auto. Qed. @@ -1711,7 +1712,7 @@ Proof. intros. pose proof (initmem_inject p H0). erewrite init_mem_transf_augment in H1; eauto. - eapply alloc_globals_augment; eauto. omega. + eapply alloc_globals_augment; eauto. apply Ple_refl. Qed. End TRANSF_PROGRAM_AUGMENT. @@ -1748,7 +1749,7 @@ Theorem find_funct_ptr_rev_transf_partial2: Proof. pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). intros. pose proof (H b tf H0). - destruct (zlt b (genv_next (globalenv p))). auto. contradiction. + destruct (plt b (genv_next (globalenv p))). auto. contradiction. Qed. Theorem find_funct_transf_partial2: @@ -1787,7 +1788,7 @@ Theorem find_var_info_rev_transf_partial2: Proof. pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). intros. pose proof (H b v' H0). - destruct (zlt b (genv_next (globalenv p))). auto. contradiction. + destruct (plt b (genv_next (globalenv p))). auto. contradiction. Qed. Theorem find_symbol_transf_partial2: diff --git a/common/Memory.v b/common/Memory.v index 54d50f7..ca8b490 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -41,7 +41,7 @@ Require Export Memtype. Local Unset Elimination Schemes. Local Unset Case Analysis Schemes. -Local Notation "a # b" := (ZMap.get b a) (at level 1). +Local Notation "a # b" := (PMap.get b a) (at level 1). Module Mem <: MEM. @@ -59,15 +59,16 @@ Definition perm_order'' (po1 po2: option permission) := end. Record mem' : Type := mkmem { - mem_contents: ZMap.t (ZMap.t memval); (**r [block -> offset -> memval] *) - mem_access: ZMap.t (Z -> perm_kind -> option permission); + mem_contents: PMap.t (ZMap.t memval); (**r [block -> offset -> memval] *) + mem_access: PMap.t (Z -> perm_kind -> option permission); (**r [block -> offset -> kind -> option permission] *) nextblock: block; - nextblock_pos: nextblock > 0; access_max: forall b ofs, perm_order'' (mem_access#b ofs Max) (mem_access#b ofs Cur); nextblock_noaccess: - forall b ofs k, b >= nextblock -> mem_access#b ofs k = None + forall b ofs k, ~(Plt b nextblock) -> mem_access#b ofs k = None; + contents_default: + forall b, fst mem_contents#b = Undef }. Definition mem := mem'. @@ -85,8 +86,7 @@ Qed. (** A block address is valid if it was previously allocated. It remains valid even after being freed. *) -Definition valid_block (m: mem) (b: block) := - b < nextblock m. +Definition valid_block (m: mem) (b: block) := Plt b (nextblock m). Theorem valid_not_valid_diff: forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'. @@ -142,7 +142,7 @@ Theorem perm_valid_block: forall m b ofs k p, perm m b ofs k p -> valid_block m b. Proof. unfold perm; intros. - destruct (zlt b m.(nextblock)). + destruct (plt b m.(nextblock)). auto. assert (m.(mem_access)#b ofs k = None). eapply nextblock_noaccess; eauto. @@ -340,48 +340,47 @@ Qed. (** The initial store *) Program Definition empty: mem := - mkmem (ZMap.init (ZMap.init Undef)) - (ZMap.init (fun ofs k => None)) - 1 _ _ _. + mkmem (PMap.init (ZMap.init Undef)) + (PMap.init (fun ofs k => None)) + 1%positive _ _ _. Next Obligation. - omega. + repeat rewrite PMap.gi. red; auto. Qed. Next Obligation. - repeat rewrite ZMap.gi. red; auto. + rewrite PMap.gi. auto. Qed. Next Obligation. - rewrite ZMap.gi. auto. + rewrite PMap.gi. auto. Qed. -Definition nullptr: block := 0. - (** Allocation of a fresh block with the given bounds. Return an updated memory state and the address of the fresh block, which initially contains undefined cells. Note that allocation never fails: we model an infinite memory. *) Program Definition alloc (m: mem) (lo hi: Z) := - (mkmem (ZMap.set m.(nextblock) + (mkmem (PMap.set m.(nextblock) (ZMap.init Undef) m.(mem_contents)) - (ZMap.set m.(nextblock) + (PMap.set m.(nextblock) (fun ofs k => if zle lo ofs && zlt ofs hi then Some Freeable else None) m.(mem_access)) - (Zsucc m.(nextblock)) + (Psucc m.(nextblock)) _ _ _, m.(nextblock)). Next Obligation. - generalize (nextblock_pos m). omega. -Qed. -Next Obligation. - repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextblock m)). + repeat rewrite PMap.gsspec. destruct (peq b (nextblock m)). subst b. destruct (zle lo ofs && zlt ofs hi); red; auto with mem. apply access_max. Qed. Next Obligation. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextblock m)). - subst b. generalize (nextblock_pos m). intros. omegaContradiction. - apply nextblock_noaccess. omega. + rewrite PMap.gsspec. destruct (peq b (nextblock m)). + subst b. elim H. apply Plt_succ. + apply nextblock_noaccess. red; intros; elim H. + apply Plt_trans_succ; auto. +Qed. +Next Obligation. + rewrite PMap.gsspec. destruct (peq b (nextblock m)). auto. apply contents_default. Qed. (** Freeing a block between the given bounds. @@ -391,23 +390,23 @@ Qed. Program Definition unchecked_free (m: mem) (b: block) (lo hi: Z): mem := mkmem m.(mem_contents) - (ZMap.set b + (PMap.set b (fun ofs k => if zle lo ofs && zlt ofs hi then None else m.(mem_access)#b ofs k) m.(mem_access)) m.(nextblock) _ _ _. Next Obligation. - apply nextblock_pos. -Qed. -Next Obligation. - repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). + repeat rewrite PMap.gsspec. destruct (peq b0 b). destruct (zle lo ofs && zlt ofs hi). red; auto. apply access_max. apply access_max. Qed. Next Obligation. - repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst. + repeat rewrite PMap.gsspec. destruct (peq b0 b). subst. destruct (zle lo ofs && zlt ofs hi). auto. apply nextblock_noaccess; auto. apply nextblock_noaccess; auto. Qed. +Next Obligation. + apply contents_default. +Qed. Definition free (m: mem) (b: block) (lo hi: Z): option mem := if range_perm_dec m b lo hi Cur Freeable @@ -431,7 +430,7 @@ Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem := Fixpoint getN (n: nat) (p: Z) (c: ZMap.t memval) {struct n}: list memval := match n with | O => nil - | S n' => c#p :: getN n' (p + 1) c + | S n' => ZMap.get p c :: getN n' (p + 1) c end. (** [load chunk m b ofs] perform a read in memory state [m], at address @@ -475,12 +474,12 @@ Fixpoint setN (vl: list memval) (p: Z) (c: ZMap.t memval) {struct vl}: ZMap.t me Remark setN_other: forall vl c p q, (forall r, p <= r < p + Z_of_nat (length vl) -> r <> q) -> - (setN vl p c)#q = c#q. + ZMap.get q (setN vl p c) = ZMap.get q c. Proof. induction vl; intros; simpl. auto. simpl length in H. rewrite inj_S in H. - transitivity ((ZMap.set p a c)#q). + transitivity (ZMap.get q (ZMap.set p a c)). apply IHvl. intros. apply H. omega. apply ZMap.gso. apply not_eq_sym. apply H. omega. Qed. @@ -488,7 +487,7 @@ Qed. Remark setN_outside: forall vl c p q, q < p \/ q >= p + Z_of_nat (length vl) -> - (setN vl p c)#q = c#q. + ZMap.get q (setN vl p c) = ZMap.get q c. Proof. intros. apply setN_other. intros. omega. @@ -507,7 +506,7 @@ Qed. Remark getN_exten: forall c1 c2 n p, - (forall i, p <= i < p + Z_of_nat n -> c1#i = c2#i) -> + (forall i, p <= i < p + Z_of_nat n -> ZMap.get i c1 = ZMap.get i c2) -> getN n p c1 = getN n p c2. Proof. induction n; intros. auto. rewrite inj_S in H. simpl. decEq. @@ -522,23 +521,34 @@ Proof. intros. apply getN_exten. intros. apply setN_outside. omega. Qed. +Remark setN_default: + forall vl q c, fst (setN vl q c) = fst c. +Proof. + induction vl; simpl; intros. auto. rewrite IHvl. auto. +Qed. + (** [store chunk m b ofs v] perform a write in memory state [m]. Value [v] is stored at address [b] and offset [ofs]. Return the updated memory store, or [None] if the accessed bytes are not writable. *) -Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val): option mem := +Program Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val): option mem := if valid_access_dec m chunk b ofs Writable then - Some (mkmem (ZMap.set b + Some (mkmem (PMap.set b (setN (encode_val chunk v) ofs (m.(mem_contents)#b)) m.(mem_contents)) m.(mem_access) m.(nextblock) - m.(nextblock_pos) - m.(access_max) - m.(nextblock_noaccess)) + _ _ _) else None. +Next Obligation. apply access_max. Qed. +Next Obligation. apply nextblock_noaccess; auto. Qed. +Next Obligation. + rewrite PMap.gsspec. destruct (peq b0 b). + rewrite setN_default. apply contents_default. + apply contents_default. +Qed. (** [storev chunk m addr v] is similar, but the address and offset are given as a single value [addr], which must be a pointer value. *) @@ -553,17 +563,22 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := starting at location [(b, ofs)]. Returns updated memory state or [None] if the accessed locations are not writable. *) -Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem := +Program Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem := if range_perm_dec m b ofs (ofs + Z_of_nat (length bytes)) Cur Writable then Some (mkmem - (ZMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents)) + (PMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents)) m.(mem_access) m.(nextblock) - m.(nextblock_pos) - m.(access_max) - m.(nextblock_noaccess)) + _ _ _) else None. +Next Obligation. apply access_max. Qed. +Next Obligation. apply nextblock_noaccess; auto. Qed. +Next Obligation. + rewrite PMap.gsspec. destruct (peq b0 b). + rewrite setN_default. apply contents_default. + apply contents_default. +Qed. (** [drop_perm m b lo hi p] sets the max permissions of the byte range [(b, lo) ... (b, hi - 1)] to [p]. These bytes must have current permissions @@ -573,38 +588,38 @@ Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option Program Definition drop_perm (m: mem) (b: block) (lo hi: Z) (p: permission): option mem := if range_perm_dec m b lo hi Cur Freeable then Some (mkmem m.(mem_contents) - (ZMap.set b + (PMap.set b (fun ofs k => if zle lo ofs && zlt ofs hi then Some p else m.(mem_access)#b ofs k) m.(mem_access)) m.(nextblock) _ _ _) else None. Next Obligation. - apply nextblock_pos. -Qed. -Next Obligation. - repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst b0. + repeat rewrite PMap.gsspec. destruct (peq b0 b). subst b0. destruct (zle lo ofs && zlt ofs hi). red; auto with mem. apply access_max. apply access_max. Qed. Next Obligation. specialize (nextblock_noaccess m b0 ofs k H0). intros. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst b0. + rewrite PMap.gsspec. destruct (peq b0 b). subst b0. destruct (zle lo ofs). destruct (zlt ofs hi). assert (perm m b ofs k Freeable). apply perm_cur. apply H; auto. unfold perm in H2. rewrite H1 in H2. contradiction. auto. auto. auto. Qed. +Next Obligation. + apply contents_default. +Qed. (** * Properties of the memory operations *) (** Properties of the empty store. *) -Theorem nextblock_empty: nextblock empty = 1. +Theorem nextblock_empty: nextblock empty = 1%positive. Proof. reflexivity. Qed. Theorem perm_empty: forall b ofs k p, ~perm empty b ofs k p. Proof. - intros. unfold perm, empty; simpl. rewrite ZMap.gi. simpl. tauto. + intros. unfold perm, empty; simpl. rewrite PMap.gi. simpl. tauto. Qed. Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p. @@ -838,7 +853,7 @@ Qed. Theorem load_rep: forall ch m1 m2 b ofs v1 v2, - (forall z, 0 <= z < size_chunk ch -> m1.(mem_contents)#b#(ofs+z) = m2.(mem_contents)#b#(ofs+z)) -> + (forall z, 0 <= z < size_chunk ch -> ZMap.get (ofs + z) m1.(mem_contents)#b = ZMap.get (ofs + z) m2.(mem_contents)#b) -> load ch m1 b ofs = Some v1 -> load ch m2 b ofs = Some v2 -> v1 = v2. @@ -948,9 +963,9 @@ Proof. Qed. Lemma store_mem_contents: - mem_contents m2 = ZMap.set b (setN (encode_val chunk v) ofs m1.(mem_contents)#b) m1.(mem_contents). + mem_contents m2 = PMap.set b (setN (encode_val chunk v) ofs m1.(mem_contents)#b) m1.(mem_contents). Proof. - unfold store in STORE. destruct ( valid_access_dec m1 chunk b ofs Writable); inv STORE. + unfold store in STORE. destruct (valid_access_dec m1 chunk b ofs Writable); inv STORE. auto. Qed. @@ -1028,7 +1043,7 @@ Proof. exists v'; split; auto. exploit load_result; eauto. intros B. rewrite B. rewrite store_mem_contents; simpl. - rewrite ZMap.gss. + rewrite PMap.gss. replace (size_chunk_nat chunk') with (length (encode_val chunk v)). rewrite getN_setN_same. apply decode_encode_val_general. rewrite encode_val_length. repeat rewrite size_chunk_conv in H. @@ -1063,7 +1078,7 @@ Proof. destruct (valid_access_dec m1 chunk' b' ofs' Readable). rewrite pred_dec_true. decEq. decEq. rewrite store_mem_contents; simpl. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. + rewrite PMap.gsspec. destruct (peq b' b). subst b'. apply getN_setN_outside. rewrite encode_val_length. repeat rewrite <- size_chunk_conv. intuition. auto. @@ -1078,7 +1093,7 @@ Proof. intros. assert (valid_access m2 chunk b ofs Readable) by eauto with mem. unfold loadbytes. rewrite pred_dec_true. rewrite store_mem_contents; simpl. - rewrite ZMap.gss. + rewrite PMap.gss. replace (nat_of_Z (size_chunk chunk)) with (length (encode_val chunk v)). rewrite getN_setN_same. auto. rewrite encode_val_length. auto. @@ -1097,7 +1112,7 @@ Proof. destruct (range_perm_dec m1 b' ofs' (ofs' + n) Cur Readable). rewrite pred_dec_true. decEq. rewrite store_mem_contents; simpl. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. + rewrite PMap.gsspec. destruct (peq b' b). subst b'. destruct H. congruence. destruct (zle n 0) as [z | n0]. rewrite (nat_of_Z_neg _ z). auto. @@ -1114,7 +1129,7 @@ Lemma setN_property: forall (P: memval -> Prop) vl p q c, (forall v, In v vl -> P v) -> p <= q < p + Z_of_nat (length vl) -> - P((setN vl p c)#q). + P(ZMap.get q (setN vl p c)). Proof. induction vl; intros. simpl in H0. omegaContradiction. @@ -1127,7 +1142,7 @@ Qed. Lemma getN_in: forall c q n p, p <= q < p + Z_of_nat n -> - In (c#q) (getN n p c). + In (ZMap.get q c) (getN n p c). Proof. induction n; intros. simpl in H; omegaContradiction. @@ -1143,7 +1158,7 @@ Theorem load_pointer_store: \/ (b' <> b \/ ofs' + size_chunk chunk' <= ofs \/ ofs + size_chunk chunk <= ofs'). Proof. intros. exploit load_result; eauto. rewrite store_mem_contents; simpl. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b); auto. subst b'. intro DEC. + rewrite PMap.gsspec. destruct (peq b' b); auto. subst b'. intro DEC. destruct (zle (ofs' + size_chunk chunk') ofs); auto. destruct (zle (ofs + size_chunk chunk) ofs'); auto. destruct (size_chunk_nat_pos chunk) as [sz SZ]. @@ -1176,9 +1191,9 @@ Proof. For the read to return a pointer, it must satisfy ~memval_valid_cont. *) elimtype False. - assert (~memval_valid_cont (c'#ofs')). + assert (~memval_valid_cont (ZMap.get ofs' c')). rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. auto. - assert (memval_valid_cont (c'#ofs')). + assert (memval_valid_cont (ZMap.get ofs' c')). inv VSHAPE. unfold c'. rewrite <- H1. simpl. apply setN_property. auto. assert (length mvl = sz). @@ -1197,10 +1212,10 @@ Proof. For the read to return a pointer, it must satisfy ~memval_valid_first. *) elimtype False. - assert (memval_valid_first (c'#ofs)). + assert (memval_valid_first (ZMap.get ofs c')). inv VSHAPE. unfold c'. rewrite <- H0. simpl. rewrite setN_outside. rewrite ZMap.gss. auto. omega. - assert (~memval_valid_first (c'#ofs)). + assert (~memval_valid_first (ZMap.get ofs c')). rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. apply H4. apply getN_in. rewrite size_chunk_conv in *. rewrite SZ' in *. rewrite inj_S in *. omega. @@ -1229,7 +1244,7 @@ Proof. rewrite LD; clear LD. Opaque encode_val. rewrite ST; simpl. - rewrite ZMap.gss. + rewrite PMap.gss. set (c := m1.(mem_contents)#b). set (c' := setN (encode_val chunk (Vptr v_b v_o)) ofs c). destruct (decode_val_shape chunk' (getN (size_chunk_nat chunk') ofs' c')) @@ -1257,9 +1272,9 @@ Opaque encode_val. The byte at ofs' is Undef or not memval_valid_first (because write of pointer). The byte at ofs' must be memval_valid_first and not Undef (otherwise load returns Vundef). *) - assert (memval_valid_first (c'#ofs') /\ c'#ofs' <> Undef). + assert (memval_valid_first (ZMap.get ofs' c') /\ ZMap.get ofs' c' <> Undef). rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. auto. - assert (~memval_valid_first (c'#ofs') \/ c'#ofs' = Undef). + assert (~memval_valid_first (ZMap.get ofs' c') \/ ZMap.get ofs' c' = Undef). unfold c'. destruct ENC. right. apply setN_property. rewrite H5. intros. eapply in_list_repeat; eauto. rewrite encode_val_length. rewrite <- size_chunk_conv. omega. @@ -1277,11 +1292,11 @@ Opaque encode_val. The byte at ofs is Undef or not memval_valid_cont (because write of pointer). The byte at ofs must be memval_valid_cont and not Undef (otherwise load returns Vundef). *) - assert (memval_valid_cont (c'#ofs) /\ c'#ofs <> Undef). + assert (memval_valid_cont (ZMap.get ofs c') /\ ZMap.get ofs c' <> Undef). rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. apply H8. apply getN_in. rewrite size_chunk_conv in H2. rewrite SZ' in H2. rewrite inj_S in H2. omega. - assert (~memval_valid_cont (c'#ofs) \/ c'#ofs = Undef). + assert (~memval_valid_cont (ZMap.get ofs c') \/ ZMap.get ofs c' = Undef). elim ENC. rewrite <- GET. rewrite SZ. simpl. intros. right; congruence. rewrite <- GET. rewrite SZ. simpl. intros. inv H5. auto. @@ -1301,7 +1316,7 @@ Proof. rewrite LD; clear LD. Opaque encode_val. rewrite ST; simpl. - rewrite ZMap.gss. + rewrite PMap.gss. set (c1 := m1.(mem_contents)#b). set (e := encode_val chunk (Vptr v_b v_o)). destruct (size_chunk_nat_pos chunk) as [sz SZ]. @@ -1334,11 +1349,10 @@ Proof. rewrite <- (encode_val_length chunk2 v2). congruence. unfold store. - destruct (valid_access_dec m chunk1 b ofs Writable). - rewrite pred_dec_true. - f_equal. apply mkmem_ext; auto. congruence. - apply valid_access_compat with chunk1; auto. omega. + destruct (valid_access_dec m chunk1 b ofs Writable); destruct (valid_access_dec m chunk2 b ofs Writable); auto. + f_equal. apply mkmem_ext; auto. congruence. + elim n. apply valid_access_compat with chunk1; auto. omega. elim n. apply valid_access_compat with chunk2; auto. omega. Qed. @@ -1392,8 +1406,9 @@ Theorem store_float64al32: Proof. unfold store; intros. destruct (valid_access_dec m Mfloat64 b ofs Writable); try discriminate. - rewrite pred_dec_true. rewrite <- H. auto. - apply valid_access_compat with Mfloat64; auto. simpl; omega. + destruct (valid_access_dec m Mfloat64al32 b ofs Writable). + rewrite <- H. f_equal. apply mkmem_ext; auto. + elim n. apply valid_access_compat with Mfloat64; auto. simpl; omega. Qed. Theorem storev_float64al32: @@ -1410,9 +1425,9 @@ Theorem range_perm_storebytes: range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable -> { m2 : mem | storebytes m1 b ofs bytes = Some m2 }. Proof. - intros. econstructor. unfold storebytes. + intros. unfold storebytes. destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable). - reflexivity. + econstructor; reflexivity. contradiction. Defined. @@ -1425,7 +1440,7 @@ Proof. unfold storebytes, store. intros. destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable); inv H. destruct (valid_access_dec m1 chunk b ofs Writable). - auto. + f_equal. apply mkmem_ext; auto. elim n. constructor; auto. rewrite encode_val_length in r. rewrite size_chunk_conv. auto. Qed. @@ -1438,7 +1453,7 @@ Proof. unfold storebytes, store. intros. destruct (valid_access_dec m1 chunk b ofs Writable); inv H. destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable). - auto. + f_equal. apply mkmem_ext; auto. destruct v0. elim n. rewrite encode_val_length. rewrite <- size_chunk_conv. auto. Qed. @@ -1460,7 +1475,7 @@ Proof. Qed. Lemma storebytes_mem_contents: - mem_contents m2 = ZMap.set b (setN bytes ofs m1.(mem_contents)#b) m1.(mem_contents). + mem_contents m2 = PMap.set b (setN bytes ofs m1.(mem_contents)#b) m1.(mem_contents). Proof. unfold storebytes in STORE. destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); @@ -1539,7 +1554,7 @@ Proof. destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); try discriminate. rewrite pred_dec_true. - decEq. inv STORE; simpl. rewrite ZMap.gss. rewrite nat_of_Z_of_nat. + decEq. inv STORE; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat. apply getN_setN_same. red; eauto with mem. Qed. @@ -1556,7 +1571,7 @@ Proof. destruct (range_perm_dec m1 b' ofs' (ofs' + len) Cur Readable). rewrite pred_dec_true. rewrite storebytes_mem_contents. decEq. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. + rewrite PMap.gsspec. destruct (peq b' b). subst b'. apply getN_setN_outside. rewrite nat_of_Z_eq; auto. intuition congruence. auto. red; auto with mem. @@ -1575,7 +1590,7 @@ Proof. destruct (valid_access_dec m1 chunk b' ofs' Readable). rewrite pred_dec_true. rewrite storebytes_mem_contents. decEq. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. + rewrite PMap.gsspec. destruct (peq b' b). subst b'. rewrite getN_setN_outside. auto. rewrite <- size_chunk_conv. intuition congruence. auto. destruct v; split; auto. red; auto with mem. @@ -1606,7 +1621,7 @@ Proof. destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) Cur Writable); try congruence. destruct (range_perm_dec m b ofs (ofs + Z_of_nat (length (bytes1 ++ bytes2))) Cur Writable). inv ST1; inv ST2; simpl. decEq. apply mkmem_ext; auto. - rewrite ZMap.gss. rewrite setN_concat. symmetry. apply ZMap.set2. + rewrite PMap.gss. rewrite setN_concat. symmetry. apply PMap.set2. elim n. rewrite app_length. rewrite inj_plus. red; intros. destruct (zlt ofs0 (ofs + Z_of_nat(length bytes1))). @@ -1684,7 +1699,7 @@ Variable b: block. Hypothesis ALLOC: alloc m1 lo hi = (m2, b). Theorem nextblock_alloc: - nextblock m2 = Zsucc (nextblock m1). + nextblock m2 = Psucc (nextblock m1). Proof. injection ALLOC; intros. rewrite <- H0; auto. Qed. @@ -1698,19 +1713,20 @@ Qed. Theorem valid_block_alloc: forall b', valid_block m1 b' -> valid_block m2 b'. Proof. - unfold valid_block; intros. rewrite nextblock_alloc. omega. + unfold valid_block; intros. rewrite nextblock_alloc. + apply Plt_trans_succ; auto. Qed. Theorem fresh_block_alloc: ~(valid_block m1 b). Proof. - unfold valid_block. rewrite alloc_result. omega. + unfold valid_block. rewrite alloc_result. apply Plt_strict. Qed. Theorem valid_new_block: valid_block m2 b. Proof. - unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. omega. + unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. apply Plt_succ. Qed. Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. @@ -1720,32 +1736,32 @@ Theorem valid_block_alloc_inv: Proof. unfold valid_block; intros. rewrite nextblock_alloc in H. rewrite alloc_result. - unfold block; omega. + exploit Plt_succ_inv; eauto. tauto. Qed. Theorem perm_alloc_1: forall b' ofs k p, perm m1 b' ofs k p -> perm m2 b' ofs k p. Proof. unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl. - subst b. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' (nextblock m1)); auto. - rewrite nextblock_noaccess in H. contradiction. omega. + subst b. rewrite PMap.gsspec. destruct (peq b' (nextblock m1)); auto. + rewrite nextblock_noaccess in H. contradiction. subst b'. apply Plt_strict. Qed. Theorem perm_alloc_2: forall ofs k, lo <= ofs < hi -> perm m2 b ofs k Freeable. Proof. unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl. - subst b. rewrite ZMap.gss. unfold proj_sumbool. rewrite zle_true. + subst b. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. auto with mem. omega. omega. Qed. Theorem perm_alloc_inv: forall b' ofs k p, perm m2 b' ofs k p -> - if zeq b' b then lo <= ofs < hi else perm m1 b' ofs k p. + if eq_block b' b then lo <= ofs < hi else perm m1 b' ofs k p. Proof. intros until p; unfold perm. inv ALLOC. simpl. - rewrite ZMap.gsspec. unfold ZIndexed.eq. destruct (zeq b' (nextblock m1)); intros. + rewrite PMap.gsspec. unfold eq_block. destruct (peq b' (nextblock m1)); intros. destruct (zle lo ofs); try contradiction. destruct (zlt ofs hi); try contradiction. split; auto. auto. @@ -1754,13 +1770,13 @@ Qed. Theorem perm_alloc_3: forall ofs k p, perm m2 b ofs k p -> lo <= ofs < hi. Proof. - intros. exploit perm_alloc_inv; eauto. rewrite zeq_true; auto. + intros. exploit perm_alloc_inv; eauto. rewrite dec_eq_true; auto. Qed. Theorem perm_alloc_4: forall b' ofs k p, perm m2 b' ofs k p -> b' <> b -> perm m1 b' ofs k p. Proof. - intros. exploit perm_alloc_inv; eauto. rewrite zeq_false; auto. + intros. exploit perm_alloc_inv; eauto. rewrite dec_eq_false; auto. Qed. Local Hint Resolve perm_alloc_1 perm_alloc_2 perm_alloc_3 perm_alloc_4: mem. @@ -1794,14 +1810,14 @@ Theorem valid_access_alloc_inv: Proof. intros. inv H. generalize (size_chunk_pos chunk); intro. - unfold eq_block. destruct (zeq b' b). subst b'. + destruct (eq_block b' b). subst b'. assert (perm m2 b ofs Cur p). apply H0. omega. assert (perm m2 b (ofs + size_chunk chunk - 1) Cur p). apply H0. omega. - exploit perm_alloc_inv. eexact H2. rewrite zeq_true. intro. - exploit perm_alloc_inv. eexact H3. rewrite zeq_true. intro. + exploit perm_alloc_inv. eexact H2. rewrite dec_eq_true. intro. + exploit perm_alloc_inv. eexact H3. rewrite dec_eq_true. intro. intuition omega. split; auto. red; intros. - exploit perm_alloc_inv. apply H0. eauto. rewrite zeq_false; auto. + exploit perm_alloc_inv. apply H0. eauto. rewrite dec_eq_false; auto. Qed. Theorem load_alloc_unchanged: @@ -1815,7 +1831,7 @@ Proof. subst b'. elimtype False. eauto with mem. rewrite pred_dec_true; auto. injection ALLOC; intros. rewrite <- H2; simpl. - rewrite ZMap.gso. auto. rewrite H1. apply sym_not_equal; eauto with mem. + rewrite PMap.gso. auto. rewrite H1. apply sym_not_equal; eauto with mem. rewrite pred_dec_false. auto. eauto with mem. Qed. @@ -1835,7 +1851,7 @@ Theorem load_alloc_same: Proof. intros. exploit load_result; eauto. intro. rewrite H0. injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1. - rewrite ZMap.gss. destruct chunk; simpl; repeat rewrite ZMap.gi; reflexivity. + rewrite PMap.gss. destruct chunk; simpl; repeat rewrite ZMap.gi; reflexivity. Qed. Theorem load_alloc_same': @@ -1914,7 +1930,7 @@ Theorem perm_free_1: perm m2 b ofs k p. Proof. intros. rewrite free_result. unfold perm, unchecked_free; simpl. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b. + rewrite PMap.gsspec. destruct (peq b bf). subst b. destruct (zle lo ofs); simpl. destruct (zlt ofs hi); simpl. elimtype False; intuition. @@ -1926,7 +1942,7 @@ Theorem perm_free_2: forall ofs k p, lo <= ofs < hi -> ~ perm m2 bf ofs k p. Proof. intros. rewrite free_result. unfold perm, unchecked_free; simpl. - rewrite ZMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. + rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. tauto. omega. omega. Qed. @@ -1935,7 +1951,7 @@ Theorem perm_free_3: perm m2 b ofs k p -> perm m1 b ofs k p. Proof. intros until p. rewrite free_result. unfold perm, unchecked_free; simpl. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b. + rewrite PMap.gsspec. destruct (peq b bf). subst b. destruct (zle lo ofs); simpl. destruct (zlt ofs hi); simpl. tauto. auto. auto. auto. @@ -1947,7 +1963,7 @@ Theorem perm_free_inv: (b = bf /\ lo <= ofs < hi) \/ perm m2 b ofs k p. Proof. intros. rewrite free_result. unfold perm, unchecked_free; simpl. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf); auto. subst b. + rewrite PMap.gsspec. destruct (peq b bf); auto. subst b. destruct (zle lo ofs); simpl; auto. destruct (zlt ofs hi); simpl; auto. Qed. @@ -1985,7 +2001,7 @@ Proof. intros. destruct H. split; auto. red; intros. generalize (H ofs0 H1). rewrite free_result. unfold perm, unchecked_free; simpl. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b. + rewrite PMap.gsspec. destruct (peq b bf). subst b. destruct (zle lo ofs0); simpl. destruct (zlt ofs0 hi); simpl. tauto. auto. auto. auto. @@ -2072,7 +2088,7 @@ Theorem perm_drop_1: Proof. intros. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. - unfold perm. simpl. rewrite ZMap.gss. unfold proj_sumbool. + unfold perm. simpl. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. constructor. omega. omega. Qed. @@ -2082,7 +2098,7 @@ Theorem perm_drop_2: Proof. intros. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. - revert H0. unfold perm; simpl. rewrite ZMap.gss. unfold proj_sumbool. + revert H0. unfold perm; simpl. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. auto. omega. omega. Qed. @@ -2092,7 +2108,7 @@ Theorem perm_drop_3: Proof. intros. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. - unfold perm; simpl. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. + unfold perm; simpl. rewrite PMap.gsspec. destruct (peq b' b). subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi). byContradiction. intuition omega. auto. auto. auto. @@ -2103,7 +2119,7 @@ Theorem perm_drop_4: Proof. intros. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. - revert H. unfold perm; simpl. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). + revert H. unfold perm; simpl. rewrite PMap.gsspec. destruct (peq b' b). subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi). simpl. intros. apply perm_implies with p. apply perm_implies with Freeable. apply perm_cur. apply r. tauto. auto with mem. auto. @@ -2117,7 +2133,7 @@ Lemma valid_access_drop_1: Proof. intros. destruct H0. split; auto. red; intros. - destruct (zeq b' b). subst b'. + destruct (eq_block b' b). subst b'. destruct (zlt ofs0 lo). eapply perm_drop_3; eauto. destruct (zle hi ofs0). eapply perm_drop_3; eauto. apply perm_implies with p. eapply perm_drop_1; eauto. omega. @@ -2133,20 +2149,6 @@ Proof. red; intros. eapply perm_drop_4; eauto. Qed. -(* -Lemma valid_access_drop_3: - forall chunk b' ofs p', - valid_access m' chunk b' ofs p' -> - b' <> b \/ Intv.disjoint (lo, hi) (ofs, ofs + size_chunk chunk) \/ perm_order p p'. -Proof. - intros. destruct H. - destruct (zeq b' b); auto. subst b'. - destruct (Intv.disjoint_dec (lo, hi) (ofs, ofs + size_chunk chunk)); auto. - exploit intv_not_disjoint; eauto. intros [x [A B]]. - right; right. apply perm_drop_2 with x. auto. apply H. auto. -Qed. -*) - Theorem load_drop: forall chunk b' ofs, b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p Readable -> @@ -2190,7 +2192,7 @@ Record mem_inj (f: meminj) (m1 m2: mem) : Prop := forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> perm m1 b1 ofs Cur Readable -> - memval_inject f (m1.(mem_contents)#b1#ofs) (m2.(mem_contents)#b2#(ofs + delta)) + memval_inject f (ZMap.get ofs m1.(mem_contents)#b1) (ZMap.get (ofs+delta) m2.(mem_contents)#b2) }. (** Preservation of permissions *) @@ -2280,9 +2282,9 @@ Lemma setN_inj: forall (access: Z -> Prop) delta f vl1 vl2, list_forall2 (memval_inject f) vl1 vl2 -> forall p c1 c2, - (forall q, access q -> memval_inject f (c1#q) (c2#(q + delta))) -> - (forall q, access q -> memval_inject f ((setN vl1 p c1)#q) - ((setN vl2 (p + delta) c2)#(q + delta))). + (forall q, access q -> memval_inject f (ZMap.get q c1) (ZMap.get (q + delta) c2)) -> + (forall q, access q -> memval_inject f (ZMap.get q (setN vl1 p c1)) + (ZMap.get (q + delta) (setN vl2 (p + delta) c2))). Proof. induction 1; intros; simpl. auto. @@ -2331,15 +2333,15 @@ Proof. intros. rewrite (store_mem_contents _ _ _ _ _ _ H0). rewrite (store_mem_contents _ _ _ _ _ _ STORE). - repeat rewrite ZMap.gsspec. - destruct (ZIndexed.eq b0 b1). subst b0. + rewrite ! PMap.gsspec. + destruct (peq b0 b1). subst b0. (* block = b1, block = b2 *) assert (b3 = b2) by congruence. subst b3. assert (delta0 = delta) by congruence. subst delta0. - rewrite zeq_true. + rewrite peq_true. apply setN_inj with (access := fun ofs => perm m1 b1 ofs Cur Readable). apply encode_val_inject; auto. intros. eapply mi_memval; eauto. eauto with mem. - destruct (ZIndexed.eq b3 b2). subst b3. + destruct (peq b3 b2). subst b3. (* block <> b1, block = b2 *) rewrite setN_other. eapply mi_memval; eauto. eauto with mem. rewrite encode_val_length. rewrite <- size_chunk_conv. intros. @@ -2367,7 +2369,7 @@ Proof. (* mem_contents *) intros. rewrite (store_mem_contents _ _ _ _ _ _ H0). - rewrite ZMap.gso. eapply mi_memval; eauto with mem. + rewrite PMap.gso. eapply mi_memval; eauto with mem. congruence. Qed. @@ -2389,7 +2391,7 @@ Proof. (* mem_contents *) intros. rewrite (store_mem_contents _ _ _ _ _ _ H1). - rewrite ZMap.gsspec. destruct (ZIndexed.eq b2 b). subst b2. + rewrite PMap.gsspec. destruct (peq b2 b). subst b2. rewrite setN_outside. auto. rewrite encode_val_length. rewrite <- size_chunk_conv. destruct (zlt (ofs0 + delta) ofs); auto. @@ -2434,13 +2436,13 @@ Proof. assert (perm m1 b0 ofs0 Cur Readable). eapply perm_storebytes_2; eauto. rewrite (storebytes_mem_contents _ _ _ _ _ H0). rewrite (storebytes_mem_contents _ _ _ _ _ STORE). - repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b1). subst b0. + rewrite ! PMap.gsspec. destruct (peq b0 b1). subst b0. (* block = b1, block = b2 *) assert (b3 = b2) by congruence. subst b3. assert (delta0 = delta) by congruence. subst delta0. - rewrite zeq_true. + rewrite peq_true. apply setN_inj with (access := fun ofs => perm m1 b1 ofs Cur Readable); auto. - destruct (ZIndexed.eq b3 b2). subst b3. + destruct (peq b3 b2). subst b3. (* block <> b1, block = b2 *) rewrite setN_other. auto. intros. @@ -2471,7 +2473,7 @@ Proof. (* mem_contents *) intros. rewrite (storebytes_mem_contents _ _ _ _ _ H0). - rewrite ZMap.gso. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto. + rewrite PMap.gso. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto. congruence. Qed. @@ -2493,7 +2495,7 @@ Proof. (* mem_contents *) intros. rewrite (storebytes_mem_contents _ _ _ _ _ H1). - rewrite ZMap.gsspec. destruct (ZIndexed.eq b2 b). subst b2. + rewrite PMap.gsspec. destruct (peq b2 b). subst b2. rewrite setN_outside. auto. destruct (zlt (ofs0 + delta) ofs); auto. destruct (zle (ofs + Z_of_nat (length bytes2)) (ofs0 + delta)). omega. @@ -2520,7 +2522,7 @@ Proof. assert (perm m2 b0 (ofs + delta) Cur Readable). eapply mi_perm0; eauto. assert (valid_block m2 b0) by eauto with mem. - rewrite <- MEM; simpl. rewrite ZMap.gso. eauto with mem. + rewrite <- MEM; simpl. rewrite PMap.gso. eauto with mem. rewrite NEXT. eauto with mem. Qed. @@ -2534,15 +2536,15 @@ Proof. intros. inversion H. constructor. (* perm *) intros. exploit perm_alloc_inv; eauto. intros. - destruct (zeq b0 b1). congruence. eauto. + destruct (eq_block b0 b1). congruence. eauto. (* access *) - intros. exploit valid_access_alloc_inv; eauto. unfold eq_block. intros. - destruct (zeq b0 b1). congruence. eauto. + intros. exploit valid_access_alloc_inv; eauto. intros. + destruct (eq_block b0 b1). congruence. eauto. (* mem_contents *) injection H0; intros NEXT MEM. intros. rewrite <- MEM; simpl. rewrite NEXT. exploit perm_alloc_inv; eauto. intros. - rewrite ZMap.gsspec. unfold ZIndexed.eq. destruct (zeq b0 b1). + rewrite PMap.gsspec. unfold eq_block in H4. destruct (peq b0 b1). rewrite ZMap.gi. constructor. eauto. Qed. @@ -2562,12 +2564,12 @@ Proof. intros. inversion H. constructor. (* perm *) intros. - exploit perm_alloc_inv; eauto. intros. destruct (zeq b0 b1). subst b0. + exploit perm_alloc_inv; eauto. intros. destruct (eq_block b0 b1). subst b0. rewrite H4 in H5; inv H5. eauto. eauto. (* access *) intros. - exploit valid_access_alloc_inv; eauto. unfold eq_block. intros. - destruct (zeq b0 b1). subst b0. rewrite H4 in H5. inv H5. + exploit valid_access_alloc_inv; eauto. intros. + destruct (eq_block b0 b1). subst b0. rewrite H4 in H5. inv H5. split. red; intros. replace ofs0 with ((ofs0 - delta0) + delta0) by omega. apply H3. omega. @@ -2577,8 +2579,8 @@ Proof. injection H0; intros NEXT MEM. intros. rewrite <- MEM; simpl. rewrite NEXT. exploit perm_alloc_inv; eauto. intros. - rewrite ZMap.gsspec. unfold ZIndexed.eq. - destruct (zeq b0 b1). rewrite ZMap.gi. constructor. eauto. + rewrite PMap.gsspec. unfold eq_block in H7. + destruct (peq b0 b1). rewrite ZMap.gi. constructor. eauto. Qed. Lemma free_left_inj: @@ -2612,7 +2614,7 @@ Proof. perm m1 b1 ofs k p -> perm m2' b2 (ofs + delta) k p). intros. intros. eapply perm_free_1; eauto. - destruct (zeq b2 b); auto. subst b. right. + destruct (eq_block b2 b); auto. subst b. right. assert (~ (lo <= ofs + delta < hi)). red; intros; eapply H1; eauto. omega. constructor. @@ -2643,7 +2645,7 @@ Proof. eapply valid_access_drop_2; eauto. (* contents *) intros. - replace (m1'.(mem_contents)#b1#ofs) with (m1.(mem_contents)#b1#ofs). + replace (ZMap.get ofs m1'.(mem_contents)#b1) with (ZMap.get ofs m1.(mem_contents)#b1). apply mi_memval0; auto. eapply perm_drop_4; eauto. unfold drop_perm in H0; destruct (range_perm_dec m1 b lo hi Cur Freeable); inv H0; auto. Qed. @@ -2668,10 +2670,11 @@ Proof. assert (PERM: forall b0 b3 delta0 ofs k p0, f b0 = Some (b3, delta0) -> perm m1' b0 ofs k p0 -> perm m2' b3 (ofs + delta0) k p0). + { intros. assert (perm m2 b3 (ofs + delta0) k p0). eapply mi_perm0; eauto. eapply perm_drop_4; eauto. - destruct (zeq b1 b0). + destruct (eq_block b1 b0). (* b1 = b0 *) subst b0. rewrite H2 in H; inv H. destruct (zlt (ofs + delta0) (lo + delta0)). eapply perm_drop_3; eauto. @@ -2682,7 +2685,7 @@ Proof. eapply perm_drop_1. eauto. omega. (* b1 <> b0 *) eapply perm_drop_3; eauto. - destruct (zeq b3 b2); auto. + destruct (eq_block b3 b2); auto. destruct (zlt (ofs + delta0) (lo + delta)); auto. destruct (zle (hi + delta) (ofs + delta0)); auto. exploit H1; eauto. @@ -2691,7 +2694,8 @@ Proof. eapply range_perm_drop_1; eauto. omega. auto with mem. eapply perm_drop_4; eauto. eapply perm_max. apply perm_implies with p0. eauto. eauto with mem. - unfold block. omega. + intuition. + } constructor. (* perm *) auto. @@ -2723,7 +2727,7 @@ Proof. f b0 = Some (b3, delta0) -> perm m1 b0 ofs k p0 -> perm m2' b3 (ofs + delta0) k p0). intros. eapply perm_drop_3; eauto. - destruct (zeq b3 b); auto. subst b3. right. + destruct (eq_block b3 b); auto. subst b3. right. destruct (zlt (ofs + delta0) lo); auto. destruct (zle hi (ofs + delta0)); auto. byContradiction. exploit H1; eauto. omega. @@ -2973,7 +2977,7 @@ Theorem valid_block_extends: extends m1 m2 -> (valid_block m1 b <-> valid_block m2 b). Proof. - intros. inv H. unfold valid_block. rewrite mext_next0. omega. + intros. inv H. unfold valid_block. rewrite mext_next0. tauto. Qed. Theorem perm_extends: @@ -3039,7 +3043,7 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop := mi_representable: forall b b' delta ofs, f b = Some(b', delta) -> - weak_valid_pointer m1 b (Int.unsigned ofs) = true -> + perm m1 b (Int.unsigned ofs) Max Nonempty \/ perm m1 b (Int.unsigned ofs - 1) Max Nonempty -> delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned }. Definition inject := inject'. @@ -3054,7 +3058,7 @@ Theorem valid_block_inject_1: inject f m1 m2 -> valid_block m1 b1. Proof. - intros. inv H. destruct (zlt b1 (nextblock m1)). auto. + intros. inv H. destruct (plt b1 (nextblock m1)). auto. assert (f b1 = None). eapply mi_freeblocks; eauto. congruence. Qed. @@ -3125,21 +3129,6 @@ Qed. (** The following lemmas establish the absence of machine integer overflow during address computations. *) -(* -Lemma address_no_overflow: - forall f m1 m2 b1 b2 delta ofs1 k p, - inject f m1 m2 -> - perm m1 b1 (Int.unsigned ofs1) k p -> - f b1 = Some (b2, delta) -> - 0 <= Int.unsigned ofs1 + Int.unsigned (Int.repr delta) <= Int.max_unsigned. -Proof. - intros. exploit mi_representable; eauto. intros [A | [A B]]. - subst delta. change (Int.unsigned (Int.repr 0)) with 0. - rewrite Zplus_0_r. apply Int.unsigned_range_2. - rewrite Int.unsigned_repr; auto. -Qed. -*) - Lemma address_inject: forall f m1 m2 b1 ofs1 b2 delta p, inject f m1 m2 -> @@ -3147,9 +3136,8 @@ Lemma address_inject: f b1 = Some (b2, delta) -> Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta. Proof. - intros. apply (perm_implies _ _ _ _ _ Nonempty) in H0; [| constructor]. - rewrite <-valid_pointer_nonempty_perm in H0. - apply valid_pointer_implies in H0. + intros. + assert (perm m1 b1 (Int.unsigned ofs1) Max Nonempty) by eauto with mem. exploit mi_representable; eauto. intros [A B]. assert (0 <= delta <= Int.max_unsigned). generalize (Int.unsigned_range ofs1). omega. @@ -3174,7 +3162,10 @@ Theorem weak_valid_pointer_inject_no_overflow: f b = Some(b', delta) -> 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. Proof. - intros. exploit mi_representable; eauto. intros. + intros. rewrite weak_valid_pointer_spec in H0. + rewrite ! valid_pointer_nonempty_perm in H0. + exploit mi_representable; eauto. destruct H0; eauto with mem. + intros [A B]. pose proof (Int.unsigned_range ofs). rewrite Int.unsigned_repr; omega. Qed. @@ -3209,9 +3200,13 @@ Theorem weak_valid_pointer_inject_val: val_inject f (Vptr b ofs) (Vptr b' ofs') -> weak_valid_pointer m2 b' (Int.unsigned ofs') = true. Proof. - intros. inv H1. exploit mi_representable; try eassumption. intros. + intros. inv H1. + exploit weak_valid_pointer_inject; eauto. intros W. + rewrite weak_valid_pointer_spec in H0. + rewrite ! valid_pointer_nonempty_perm in H0. + exploit mi_representable; eauto. destruct H0; eauto with mem. + intros [A B]. pose proof (Int.unsigned_range ofs). - exploit weak_valid_pointer_inject; eauto. unfold Int.add. repeat rewrite Int.unsigned_repr; auto; omega. Qed. @@ -3279,7 +3274,7 @@ Proof. exploit mi_no_overlap; eauto. instantiate (1 := x - delta1). apply H2. omega. instantiate (1 := x - delta2). apply H3. omega. - unfold block; omega. + intuition. Qed. Theorem aligned_area_inject: @@ -3371,8 +3366,6 @@ Proof. red; intros. eauto with mem. (* representable *) intros. eapply mi_representable; try eassumption. - rewrite weak_valid_pointer_spec in *. - rewrite !valid_pointer_nonempty_perm in H4 |- *. destruct H4; eauto with mem. Qed. @@ -3395,8 +3388,6 @@ Proof. red; intros. eauto with mem. (* representable *) intros. eapply mi_representable; try eassumption. - rewrite weak_valid_pointer_spec in *. - rewrite !valid_pointer_nonempty_perm in H3 |- *. destruct H3; eauto with mem. Qed. @@ -3463,8 +3454,6 @@ Proof. red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. (* representable *) intros. eapply mi_representable0; eauto. - rewrite weak_valid_pointer_spec in *. - rewrite !valid_pointer_nonempty_perm in H4 |- *. destruct H4; eauto using perm_storebytes_2. Qed. @@ -3487,8 +3476,6 @@ Proof. red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. (* representable *) intros. eapply mi_representable0; eauto. - rewrite weak_valid_pointer_spec in *. - rewrite !valid_pointer_nonempty_perm in H3 |- *. destruct H3; eauto using perm_storebytes_2. Qed. @@ -3548,44 +3535,42 @@ Theorem alloc_left_unmapped_inject: /\ (forall b, b <> b1 -> f' b = f b). Proof. intros. inversion H. - set (f' := fun b => if zeq b b1 then None else f b). + set (f' := fun b => if eq_block b b1 then None else f b). assert (inject_incr f f'). - red; unfold f'; intros. destruct (zeq b b1). subst b. + red; unfold f'; intros. destruct (eq_block b b1). subst b. assert (f b1 = None). eauto with mem. congruence. auto. assert (mem_inj f' m1 m2). inversion mi_inj0; constructor; eauto with mem. - unfold f'; intros. destruct (zeq b0 b1). congruence. eauto. - unfold f'; intros. destruct (zeq b0 b1). congruence. eauto. - unfold f'; intros. destruct (zeq b0 b1). congruence. + unfold f'; intros. destruct (eq_block b0 b1). congruence. eauto. + unfold f'; intros. destruct (eq_block b0 b1). congruence. eauto. + unfold f'; intros. destruct (eq_block b0 b1). congruence. apply memval_inject_incr with f; auto. exists f'; split. constructor. (* inj *) - eapply alloc_left_unmapped_inj; eauto. unfold f'; apply zeq_true. + eapply alloc_left_unmapped_inj; eauto. unfold f'; apply dec_eq_true. (* freeblocks *) - intros. unfold f'. destruct (zeq b b1). auto. + intros. unfold f'. destruct (eq_block b b1). auto. apply mi_freeblocks0. red; intro; elim H3. eauto with mem. (* mappedblocks *) - unfold f'; intros. destruct (zeq b b1). congruence. eauto. + unfold f'; intros. destruct (eq_block b b1). congruence. eauto. (* no overlap *) unfold f'; red; intros. - destruct (zeq b0 b1); destruct (zeq b2 b1); try congruence. + destruct (eq_block b0 b1); destruct (eq_block b2 b1); try congruence. eapply mi_no_overlap0. eexact H3. eauto. eauto. - exploit perm_alloc_inv. eauto. eexact H6. rewrite zeq_false; auto. - exploit perm_alloc_inv. eauto. eexact H7. rewrite zeq_false; auto. + exploit perm_alloc_inv. eauto. eexact H6. rewrite dec_eq_false; auto. + exploit perm_alloc_inv. eauto. eexact H7. rewrite dec_eq_false; auto. (* representable *) unfold f'; intros. - destruct (zeq b b1); try discriminate. + destruct (eq_block b b1); try discriminate. eapply mi_representable0; try eassumption. - rewrite weak_valid_pointer_spec in *. - rewrite !valid_pointer_nonempty_perm in H4 |- *. destruct H4; eauto using perm_alloc_4. (* incr *) split. auto. (* image *) - split. unfold f'; apply zeq_true. + split. unfold f'; apply dec_eq_true. (* incr *) - intros; unfold f'; apply zeq_false; auto. + intros; unfold f'; apply dec_eq_false; auto. Qed. Theorem alloc_left_mapped_inject: @@ -3608,68 +3593,65 @@ Theorem alloc_left_mapped_inject: /\ (forall b, b <> b1 -> f' b = f b). Proof. intros. inversion H. - set (f' := fun b => if zeq b b1 then Some(b2, delta) else f b). + set (f' := fun b => if eq_block b b1 then Some(b2, delta) else f b). assert (inject_incr f f'). - red; unfold f'; intros. destruct (zeq b b1). subst b. + red; unfold f'; intros. destruct (eq_block b b1). subst b. assert (f b1 = None). eauto with mem. congruence. auto. assert (mem_inj f' m1 m2). inversion mi_inj0; constructor; eauto with mem. - unfold f'; intros. destruct (zeq b0 b1). + unfold f'; intros. destruct (eq_block b0 b1). inversion H8. subst b0 b3 delta0. elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. eauto. - unfold f'; intros. destruct (zeq b0 b1). + unfold f'; intros. destruct (eq_block b0 b1). inversion H8. subst b0 b3 delta0. elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. eauto. - unfold f'; intros. destruct (zeq b0 b1). + unfold f'; intros. destruct (eq_block b0 b1). inversion H8. subst b0 b3 delta0. elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. apply memval_inject_incr with f; auto. exists f'. split. constructor. (* inj *) - eapply alloc_left_mapped_inj; eauto. unfold f'; apply zeq_true. + eapply alloc_left_mapped_inj; eauto. unfold f'; apply dec_eq_true. (* freeblocks *) - unfold f'; intros. destruct (zeq b b1). subst b. + unfold f'; intros. destruct (eq_block b b1). subst b. elim H9. eauto with mem. eauto with mem. (* mappedblocks *) - unfold f'; intros. destruct (zeq b b1). congruence. eauto. + unfold f'; intros. destruct (eq_block b b1). congruence. eauto. (* overlap *) unfold f'; red; intros. exploit perm_alloc_inv. eauto. eexact H12. intros P1. exploit perm_alloc_inv. eauto. eexact H13. intros P2. - destruct (zeq b0 b1); destruct (zeq b3 b1). + destruct (eq_block b0 b1); destruct (eq_block b3 b1). congruence. inversion H10; subst b0 b1' delta1. - destruct (zeq b2 b2'); auto. subst b2'. right; red; intros. + destruct (eq_block b2 b2'); auto. subst b2'. right; red; intros. eapply H6; eauto. omega. inversion H11; subst b3 b2' delta2. - destruct (zeq b1' b2); auto. subst b1'. right; red; intros. + destruct (eq_block b1' b2); auto. subst b1'. right; red; intros. eapply H6; eauto. omega. eauto. (* representable *) unfold f'; intros. - rewrite weak_valid_pointer_spec in *. - rewrite !valid_pointer_nonempty_perm in H10. - destruct (zeq b b1). + destruct (eq_block b b1). subst. injection H9; intros; subst b' delta0. destruct H10. - exploit perm_alloc_inv; eauto; rewrite zeq_true; intro. - exploit H3. apply H4 with (k := Cur) (p := Nonempty); eauto. + exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. + exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. generalize (Int.unsigned_range_2 ofs). omega. - exploit perm_alloc_inv; eauto; rewrite zeq_true; intro. - exploit H3. apply H4 with (k := Cur) (p := Nonempty); eauto. + exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. + exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. generalize (Int.unsigned_range_2 ofs). omega. eapply mi_representable0; try eassumption. - rewrite !weak_valid_pointer_spec, !valid_pointer_nonempty_perm. destruct H10; eauto using perm_alloc_4. (* incr *) split. auto. (* image of b1 *) - split. unfold f'; apply zeq_true. + split. unfold f'; apply dec_eq_true. (* image of others *) - intros. unfold f'; apply zeq_false; auto. + intros. unfold f'; apply dec_eq_false; auto. Qed. Theorem alloc_parallel_inject: @@ -3719,8 +3701,6 @@ Proof. red; intros. eauto with mem. (* representable *) intros. eapply mi_representable0; try eassumption. - rewrite weak_valid_pointer_spec in *. - rewrite !valid_pointer_nonempty_perm in H2 |- *. destruct H2; eauto with mem. Qed. @@ -3732,9 +3712,9 @@ Lemma free_list_left_inject: Proof. induction l; simpl; intros. inv H0. auto. - destruct a as [[b lo] hi]. generalize H0. case_eq (free m1 b lo hi); intros. - apply IHl with m; auto. eapply free_left_inject; eauto. - congruence. + destruct a as [[b lo] hi]. + destruct (free m1 b lo hi) as [m11|] eqn:E; try discriminate. + apply IHl with m11; auto. eapply free_left_inject; eauto. Qed. Lemma free_right_inject: @@ -3766,14 +3746,14 @@ Lemma perm_free_list: perm m b ofs k p /\ (forall lo hi, In (b, lo, hi) l -> lo <= ofs < hi -> False). Proof. - induction l; intros until p; simpl. - intros. inv H. split; auto. + induction l; simpl; intros. + inv H. auto. destruct a as [[b1 lo1] hi1]. - case_eq (free m b1 lo1 hi1); intros; try congruence. + destruct (free m b1 lo1 hi1) as [m1|] eqn:E; try discriminate. exploit IHl; eauto. intros [A B]. split. eauto with mem. - intros. destruct H2. inv H2. - elim (perm_free_2 _ _ _ _ _ H ofs k p). auto. auto. + intros. destruct H1. inv H1. + elim (perm_free_2 _ _ _ _ _ E ofs k p). auto. auto. eauto. Qed. @@ -3861,7 +3841,7 @@ Proof. exploit mi_no_overlap1. eauto. eauto. eauto. eapply perm_inj. eauto. eexact H2. eauto. eapply perm_inj. eauto. eexact H3. eauto. - unfold block; omega. + intuition omega. (* representable *) intros. destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate. @@ -3872,7 +3852,6 @@ Proof. unfold ofs'; apply Int.unsigned_repr. auto. exploit mi_representable1. eauto. instantiate (1 := ofs'). rewrite H. - rewrite weak_valid_pointer_spec, !valid_pointer_nonempty_perm in *. replace (Int.unsigned ofs + delta1 - 1) with ((Int.unsigned ofs - 1) + delta1) by omega. destruct H0; eauto using perm_inj. @@ -3910,7 +3889,6 @@ Proof. red; intros. eapply mi_no_overlap0; eauto; eapply perm_extends; eauto. (* representable *) eapply mi_representable0; eauto. - rewrite weak_valid_pointer_spec, !valid_pointer_nonempty_perm in *. destruct H1; eauto using perm_extends. Qed. @@ -3949,7 +3927,7 @@ Qed. (** Injecting a memory into itself. *) Definition flat_inj (thr: block) : meminj := - fun (b: block) => if zlt b thr then Some(b, 0) else None. + fun (b: block) => if plt b thr then Some(b, 0) else None. Definition inject_neutral (thr: block) (m: mem) := mem_inj (flat_inj thr) m m. @@ -3958,8 +3936,8 @@ Remark flat_inj_no_overlap: forall thr m, meminj_no_overlap (flat_inj thr) m. Proof. unfold flat_inj; intros; red; intros. - destruct (zlt b1 thr); inversion H0; subst. - destruct (zlt b2 thr); inversion H1; subst. + destruct (plt b1 thr); inversion H0; subst. + destruct (plt b2 thr); inversion H1; subst. auto. Qed. @@ -3971,15 +3949,15 @@ Proof. auto. (* freeblocks *) unfold flat_inj, valid_block; intros. - apply zlt_false. omega. + apply pred_dec_false. auto. (* mappedblocks *) unfold flat_inj, valid_block; intros. - destruct (zlt b (nextblock m)); inversion H0; subst. auto. + destruct (plt b (nextblock m)); inversion H0; subst. auto. (* no overlap *) apply flat_inj_no_overlap. (* range *) unfold flat_inj; intros. - destruct (zlt b (nextblock m)); inv H0. generalize (Int.unsigned_range_2 ofs); omega. + destruct (plt b (nextblock m)); inv H0. generalize (Int.unsigned_range_2 ofs); omega. Qed. Theorem empty_inject_neutral: @@ -3987,20 +3965,20 @@ Theorem empty_inject_neutral: Proof. intros; red; constructor. (* perm *) - unfold flat_inj; intros. destruct (zlt b1 thr); inv H. + unfold flat_inj; intros. destruct (plt b1 thr); inv H. replace (ofs + 0) with ofs by omega; auto. (* access *) - unfold flat_inj; intros. destruct (zlt b1 thr); inv H. + unfold flat_inj; intros. destruct (plt b1 thr); inv H. replace (ofs + 0) with ofs by omega; auto. (* mem_contents *) - intros; simpl. repeat rewrite ZMap.gi. constructor. + intros; simpl. rewrite ! PMap.gi. rewrite ! ZMap.gi. constructor. Qed. Theorem alloc_inject_neutral: forall thr m lo hi b m', alloc m lo hi = (m', b) -> inject_neutral thr m -> - nextblock m < thr -> + Plt (nextblock m) thr -> inject_neutral thr m'. Proof. intros; red. @@ -4010,7 +3988,7 @@ Proof. intros. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. omega. - unfold flat_inj. apply zlt_true. + unfold flat_inj. apply pred_dec_true. rewrite (alloc_result _ _ _ _ _ H). auto. Qed. @@ -4018,13 +3996,13 @@ Theorem store_inject_neutral: forall chunk m b ofs v m' thr, store chunk m b ofs v = Some m' -> inject_neutral thr m -> - b < thr -> + Plt b thr -> val_inject (flat_inj thr) v v -> inject_neutral thr m'. Proof. intros; red. exploit store_mapped_inj. eauto. eauto. apply flat_inj_no_overlap. - unfold flat_inj. apply zlt_true; auto. eauto. + unfold flat_inj. apply pred_dec_true; auto. eauto. replace (ofs + 0) with ofs by omega. intros [m'' [A B]]. congruence. Qed. @@ -4033,15 +4011,152 @@ Theorem drop_inject_neutral: forall m b lo hi p m' thr, drop_perm m b lo hi p = Some m' -> inject_neutral thr m -> - b < thr -> + Plt b thr -> inject_neutral thr m'. Proof. unfold inject_neutral; intros. exploit drop_mapped_inj; eauto. apply flat_inj_no_overlap. - unfold flat_inj. apply zlt_true; eauto. + unfold flat_inj. apply pred_dec_true; eauto. repeat rewrite Zplus_0_r. intros [m'' [A B]]. congruence. Qed. +(** * Invariance properties between two memory states *) + +Section UNCHANGED_ON. + +Variable P: block -> Z -> Prop. + +Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on { + unchanged_on_perm: + forall b ofs k p, + P b ofs -> valid_block m_before b -> + (perm m_before b ofs k p <-> perm m_after b ofs k p); + unchanged_on_contents: + forall b ofs, + P b ofs -> perm m_before b ofs Cur Readable -> + ZMap.get ofs (PMap.get b m_after.(mem_contents)) = + ZMap.get ofs (PMap.get b m_before.(mem_contents)) +}. + +Lemma unchanged_on_refl: + forall m, unchanged_on m m. +Proof. + intros; constructor; tauto. +Qed. + +Lemma perm_unchanged_on: + forall m m' b ofs k p, + unchanged_on m m' -> P b ofs -> valid_block m b -> + perm m b ofs k p -> perm m' b ofs k p. +Proof. + intros. destruct H. apply unchanged_on_perm0; auto. +Qed. + +Lemma perm_unchanged_on_2: + forall m m' b ofs k p, + unchanged_on m m' -> P b ofs -> valid_block m b -> + perm m' b ofs k p -> perm m b ofs k p. +Proof. + intros. destruct H. apply unchanged_on_perm0; auto. +Qed. + +Lemma loadbytes_unchanged_on: + forall m m' b ofs n bytes, + unchanged_on m m' -> + (forall i, ofs <= i < ofs + n -> P b i) -> + loadbytes m b ofs n = Some bytes -> + loadbytes m' b ofs n = Some bytes. +Proof. + intros. + destruct (zle n 0). ++ erewrite loadbytes_empty in * by assumption. auto. ++ unfold loadbytes in *. destruct H. + destruct (range_perm_dec m b ofs (ofs + n) Cur Readable); inv H1. + assert (valid_block m b). + { eapply perm_valid_block. apply (r ofs). omega. } + assert (range_perm m' b ofs (ofs + n) Cur Readable). + { red; intros. apply unchanged_on_perm0; auto. } + rewrite pred_dec_true by assumption. f_equal. + apply getN_exten. intros. rewrite nat_of_Z_eq in H2 by omega. + apply unchanged_on_contents0; auto. +Qed. + +Lemma load_unchanged_on: + forall m m' chunk b ofs v, + unchanged_on m m' -> + (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) -> + load chunk m b ofs = Some v -> + load chunk m' b ofs = Some v. +Proof. + intros. + exploit load_valid_access; eauto. intros [A B]. + exploit load_loadbytes; eauto. intros [bytes [C D]]. + subst v. apply loadbytes_load; auto. eapply loadbytes_unchanged_on; eauto. +Qed. + +Lemma store_unchanged_on: + forall chunk m b ofs v m', + store chunk m b ofs v = Some m' -> + (forall i, ofs <= i < ofs + size_chunk chunk -> ~ P b i) -> + unchanged_on m m'. +Proof. + intros; constructor; intros. +- split; intros; eauto with mem. +- erewrite store_mem_contents; eauto. rewrite PMap.gsspec. + destruct (peq b0 b); auto. subst b0. apply setN_outside. + rewrite encode_val_length. rewrite <- size_chunk_conv. + destruct (zlt ofs0 ofs); auto. + destruct (zlt ofs0 (ofs + size_chunk chunk)); auto. + elim (H0 ofs0). omega. auto. +Qed. + +Lemma storebytes_unchanged_on: + forall m b ofs bytes m', + storebytes m b ofs bytes = Some m' -> + (forall i, ofs <= i < ofs + Z_of_nat (length bytes) -> ~ P b i) -> + unchanged_on m m'. +Proof. + intros; constructor; intros. +- split; intros. eapply perm_storebytes_1; eauto. eapply perm_storebytes_2; eauto. +- erewrite storebytes_mem_contents; eauto. rewrite PMap.gsspec. + destruct (peq b0 b); auto. subst b0. apply setN_outside. + destruct (zlt ofs0 ofs); auto. + destruct (zlt ofs0 (ofs + Z_of_nat (length bytes))); auto. + elim (H0 ofs0). omega. auto. +Qed. + +Lemma alloc_unchanged_on: + forall m lo hi m' b, + alloc m lo hi = (m', b) -> + unchanged_on m m'. +Proof. + intros; constructor; intros. +- split; intros. + eapply perm_alloc_1; eauto. + eapply perm_alloc_4; eauto. + eapply valid_not_valid_diff; eauto with mem. +- injection H; intros A B. rewrite <- B; simpl. + rewrite PMap.gso; auto. rewrite A. eapply valid_not_valid_diff; eauto with mem. +Qed. + +Lemma free_unchanged_on: + forall m b lo hi m', + free m b lo hi = Some m' -> + (forall i, lo <= i < hi -> ~ P b i) -> + unchanged_on m m'. +Proof. + intros; constructor; intros. +- split; intros. + eapply perm_free_1; eauto. + destruct (eq_block b0 b); auto. destruct (zlt ofs lo); auto. destruct (zle hi ofs); auto. + subst b0. elim (H0 ofs). omega. auto. + eapply perm_free_3; eauto. +- unfold free in H. destruct (range_perm_dec m b lo hi Cur Freeable); inv H. + simpl. auto. +Qed. + +End UNCHANGED_ON. + End Mem. Notation mem := Mem.mem. @@ -4105,4 +4220,5 @@ Hint Resolve Mem.valid_access_free_2 Mem.valid_access_free_inv_1 Mem.valid_access_free_inv_2 + Mem.unchanged_on_refl : mem. diff --git a/common/Memtype.v b/common/Memtype.v index 59dc7a3..37ab33c 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -88,8 +88,6 @@ Module Type MEM. (** The abstract type of memory states. *) Parameter mem: Type. -Definition nullptr: block := 0. - (** * Operations on memory states *) (** [empty] is the initial memory state. *) @@ -176,11 +174,9 @@ Parameter drop_perm: forall (m: mem) (b: block) (lo hi: Z) (p: permission), opti block. *) Parameter nextblock: mem -> block. -Axiom nextblock_pos: - forall m, nextblock m > 0. -Definition valid_block (m: mem) (b: block) := - b < nextblock m. +Definition valid_block (m: mem) (b: block) := Plt b (nextblock m). + Axiom valid_not_valid_diff: forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'. @@ -279,7 +275,7 @@ Axiom valid_pointer_implies: (** ** Properties of the initial memory state. *) -Axiom nextblock_empty: nextblock empty = 1. +Axiom nextblock_empty: nextblock empty = 1%positive. Axiom perm_empty: forall b ofs k p, ~perm empty b ofs k p. Axiom valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p. @@ -607,7 +603,7 @@ Axiom alloc_result: Axiom nextblock_alloc: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> - nextblock m2 = Zsucc (nextblock m1). + nextblock m2 = Psucc (nextblock m1). Axiom valid_block_alloc: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> @@ -640,7 +636,7 @@ Axiom perm_alloc_inv: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> forall b' ofs k p, perm m2 b' ofs k p -> - if zeq b' b then lo <= ofs < hi else perm m1 b' ofs k p. + if eq_block b' b then lo <= ofs < hi else perm m1 b' ofs k p. (** Effect of [alloc] on access validity. *) @@ -1191,7 +1187,7 @@ Axiom drop_outside_inject: (** Memory states that inject into themselves. *) Definition flat_inj (thr: block) : meminj := - fun (b: block) => if zlt b thr then Some(b, 0) else None. + fun (b: block) => if plt b thr then Some(b, 0) else None. Parameter inject_neutral: forall (thr: block) (m: mem), Prop. @@ -1206,14 +1202,14 @@ Axiom alloc_inject_neutral: forall thr m lo hi b m', alloc m lo hi = (m', b) -> inject_neutral thr m -> - nextblock m < thr -> + Plt (nextblock m) thr -> inject_neutral thr m'. Axiom store_inject_neutral: forall chunk m b ofs v m' thr, store chunk m b ofs v = Some m' -> inject_neutral thr m -> - b < thr -> + Plt b thr -> val_inject (flat_inj thr) v v -> inject_neutral thr m'. @@ -1221,7 +1217,7 @@ Axiom drop_inject_neutral: forall m b lo hi p m' thr, drop_perm m b lo hi p = Some m' -> inject_neutral thr m -> - b < thr -> + Plt b thr -> inject_neutral thr m'. End MEM. diff --git a/common/Values.v b/common/Values.v index bb97cdc..7caf551 100644 --- a/common/Values.v +++ b/common/Values.v @@ -21,8 +21,8 @@ Require Import AST. Require Import Integers. Require Import Floats. -Definition block : Type := Z. -Definition eq_block := zeq. +Definition block : Type := positive. +Definition eq_block := peq. (** A value is either: - a machine integer; @@ -212,7 +212,7 @@ Definition sub (v1 v2: val): val := | Vint n1, Vint n2 => Vint(Int.sub n1 n2) | Vptr b1 ofs1, Vint n2 => Vptr b1 (Int.sub ofs1 n2) | Vptr b1 ofs1, Vptr b2 ofs2 => - if zeq b1 b2 then Vint(Int.sub ofs1 ofs2) else Vundef + if eq_block b1 b2 then Vint(Int.sub ofs1 ofs2) else Vundef | _, _ => Vundef end. @@ -568,7 +568,7 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool := | Vint n1, Vptr b2 ofs2 => if Int.eq n1 Int.zero then cmp_different_blocks c else None | Vptr b1 ofs1, Vptr b2 ofs2 => - if zeq b1 b2 then + if eq_block b1 b2 then if weak_valid_ptr b1 (Int.unsigned ofs1) && weak_valid_ptr b2 (Int.unsigned ofs2) then Some (Int.cmpu c ofs1 ofs2) @@ -785,7 +785,7 @@ Proof. destruct v1; destruct v2; intros; simpl; auto. rewrite Int.sub_add_l. auto. rewrite Int.sub_add_l. auto. - case (zeq b b0); intro. rewrite Int.sub_add_l. auto. reflexivity. + case (eq_block b b0); intro. rewrite Int.sub_add_l. auto. reflexivity. Qed. Theorem sub_add_r: @@ -797,7 +797,7 @@ Proof. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. decEq. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq. apply Int.neg_add_distr. - case (zeq b b0); intro. simpl. decEq. + case (eq_block b b0); intro. simpl. decEq. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq. apply Int.neg_add_distr. reflexivity. @@ -1037,7 +1037,7 @@ Proof. rewrite Int.negate_cmpu. auto. destruct (Int.eq i Int.zero); auto. destruct (Int.eq i0 Int.zero); auto. - destruct (zeq b b0). + destruct (eq_block b b0). destruct ((valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1)) && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))). rewrite Int.negate_cmpu. auto. @@ -1084,13 +1084,13 @@ Proof. rewrite Int.swap_cmpu. auto. case (Int.eq i Int.zero); auto. case (Int.eq i0 Int.zero); auto. - destruct (zeq b b0); subst. - rewrite zeq_true. + destruct (eq_block b b0); subst. + rewrite dec_eq_true. destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)); destruct (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1)); simpl; auto. rewrite Int.swap_cmpu. auto. - rewrite zeq_false by auto. + rewrite dec_eq_false by auto. destruct (valid_ptr b (Int.unsigned i)); destruct (valid_ptr b0 (Int.unsigned i0)); simpl; auto. Qed. @@ -1286,7 +1286,7 @@ Proof. destruct v1; simpl in H2; try discriminate; destruct v2; simpl in H2; try discriminate; inv H0; inv H1; simpl; auto. - destruct (zeq b0 b1). + destruct (eq_block b0 b1). assert (forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). intros until ofs. rewrite ! orb_true_iff. intuition. @@ -1401,7 +1401,7 @@ Remark val_sub_inject: Proof. intros. inv H; inv H0; simpl; auto. econstructor; eauto. rewrite Int.sub_add_l. auto. - destruct (zeq b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite zeq_true. + destruct (eq_block b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite dec_eq_true. rewrite Int.sub_shifted. auto. Qed. @@ -1461,15 +1461,15 @@ Proof. fold (weak_valid_ptr1 b0 (Int.unsigned ofs0)) in H1. fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))). - destruct (zeq b1 b0); subst. - rewrite H in H2. inv H2. rewrite zeq_true. + destruct (eq_block b1 b0); subst. + rewrite H in H2. inv H2. rewrite dec_eq_true. destruct (weak_valid_ptr1 b0 (Int.unsigned ofs1)) eqn:?; try discriminate. destruct (weak_valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate. erewrite !weak_valid_ptr_inj by eauto. simpl. rewrite <-H1. simpl. decEq. apply Int.translate_cmpu; eauto. destruct (valid_ptr1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate. destruct (valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate. - destruct (zeq b2 b3); subst. + destruct (eq_block b2 b3); subst. assert (valid_ptr_implies: forall b ofs, valid_ptr1 b ofs = true -> weak_valid_ptr1 b ofs = true). intros. unfold weak_valid_ptr1. rewrite H0; auto. erewrite !weak_valid_ptr_inj by eauto using valid_ptr_implies. simpl. diff --git a/driver/Interp.ml b/driver/Interp.ml index 662baa2..6f9336e 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -155,7 +155,7 @@ let compare_mem m1 m2 = (* Comparing continuations *) -let some_expr = Eval(Vptr(Mem.nullptr, Int.zero), Tvoid) +let some_expr = Eval(Vint Int.zero, Tvoid) let rank_cont = function | Kstop -> 0 @@ -234,7 +234,7 @@ let mem_state = function let compare_state s1 s2 = if s1 == s2 then 0 else - let c = Z.compare (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock in + let c = P.compare (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock in if c <> 0 then c else begin match s1, s2 with | State(f1,s1,k1,e1,m1), State(f2,s2,k2,e2,m2) -> @@ -275,7 +275,7 @@ let rec purge_seen nextblock seen = match min with | None -> seen | Some((s, w) as sw) -> - if Z.le (mem_state s).Mem.nextblock nextblock + if P.le (mem_state s).Mem.nextblock nextblock then purge_seen nextblock (StateSet.remove sw seen) else seen @@ -514,7 +514,7 @@ module PrioQueue = struct let singleton elt = Node(elt, Empty, Empty) let higher_prio (time1, (s1, w1)) (time2, (s2, w2)) = - Z.lt (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock + P.lt (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock let rec insert queue elt = match queue with diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 04f170d..9027f86 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -60,11 +60,20 @@ let sanitize s = done; s' +module StringSet = Set.Make(String) + +let temp_names : (ident, string) Hashtbl.t = Hashtbl.create 17 +let all_temp_names : StringSet.t ref = ref StringSet.empty + let ident p id = try let s = Hashtbl.find string_of_atom id in fprintf p "_%s" (sanitize s) with Not_found | Not_an_identifier -> + try + let s = Hashtbl.find temp_names id in + fprintf p "%s" s + with Not_found -> fprintf p "%ld%%positive" (P.to_int32 id) let define_idents p = @@ -76,8 +85,33 @@ let define_idents p = with Not_an_identifier -> ()) string_of_atom; + Hashtbl.iter + (fun id name -> + fprintf p "Definition %s : ident := %ld%%positive.@ " + name (P.to_int32 id)) + temp_names; fprintf p "@ " +let rec find_temp_name name counter = + let name' = + if counter = 0 then name ^ "'" else sprintf "%s'%d" name counter in + if StringSet.mem name' !all_temp_names + then find_temp_name name (counter + 1) + else name' + +let name_temporary t v = + (* Try to give "t" a name that is the name of "v" with a prime + plus a number to disambiguate if needed. *) + if not (Hashtbl.mem string_of_atom t || Hashtbl.mem temp_names t) then begin + try + let vname = "_" ^ sanitize (Hashtbl.find string_of_atom v) in + let tname = find_temp_name vname 0 in + Hashtbl.add temp_names t tname; + all_temp_names := StringSet.add tname !all_temp_names + with Not_found | Not_an_identifier -> + () + end + (* Numbers *) let coqint p n = @@ -163,7 +197,11 @@ and fieldlist p = function let asttype p t = fprintf p "%s" - (match t with AST.Tint -> "AST.Tint" | AST.Tfloat -> "AST.Tfloat" | AST.Tlong -> "AST.Tlong") + (match t with + | AST.Tint -> "AST.Tint" + | AST.Tfloat -> "AST.Tfloat" + | AST.Tlong -> "AST.Tlong" + | AST.Tsingle -> "AST.Tsingle") let name_of_chunk = function | Mint8signed -> "Mint8signed" @@ -413,10 +451,20 @@ let rec collect_exprlist = function | [] -> () | r1 :: rl -> collect_expr r1; collect_exprlist rl +let rec temp_of_expr = function + | Etempvar(tmp, _) -> Some tmp + | Ecast(e, _) -> temp_of_expr e + | _ -> None + let rec collect_stmt = function | Sskip -> () | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 - | Sset(id, e2) -> collect_expr e2 + | Sset(id, e2) -> + begin match temp_of_expr e2 with + | Some tmp -> name_temporary tmp id + | None -> () + end; + collect_expr e2 | Scall(optid, e1, el) -> collect_expr e1; collect_exprlist el | Sbuiltin(optid, ef, tyl, el) -> collect_exprlist el | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 @@ -454,8 +502,6 @@ let define_struct p ty = | _ -> assert false let define_structs p prog = - struct_unions := TypeSet.empty; - List.iter collect_globdef prog.prog_defs; use_struct_names := false; TypeSet.iter (define_struct p) !struct_unions; use_struct_names := true; @@ -534,6 +580,10 @@ Local Open Scope Z_scope. let print_program p prog = fprintf p "@[<v 0>"; fprintf p "%s" prologue; + Hashtbl.clear temp_names; + all_temp_names := StringSet.empty; + struct_unions := TypeSet.empty; + List.iter collect_globdef prog.prog_defs; define_idents p; define_structs p prog; List.iter (print_globdef p) prog.prog_defs; @@ -797,7 +797,7 @@ Inductive initial_state (p: program): state -> Prop := (Pregmap.init Vundef) # PC <- (symbol_offset ge p.(prog_main) Int.zero) # RA <- Vzero - # ESP <- (Vptr Mem.nullptr Int.zero) in + # ESP <- Vzero in initial_state p (State rs0 m0). Inductive final_state: state -> int -> Prop := diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index f6eefbd..df09ca7 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -905,7 +905,7 @@ Proof. econstructor; eauto. constructor. apply Mem.extends_refl. - split. auto. simpl. congruence. intros. rewrite Regmap.gi. auto. + split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. unfold symbol_offset. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 00b706c..0bf030c 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -550,7 +550,7 @@ Proof. simpl. fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *. fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *. - destruct (zeq b0 b1). + destruct (eq_block b0 b1). destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) && Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1. destruct c; simpl; auto. @@ -384,7 +384,7 @@ Proof with (try exact I). destruct v0... destruct v0... destruct v0... - destruct v0; destruct v1... simpl. destruct (zeq b b0)... + destruct v0; destruct v1... simpl. destruct (eq_block b b0)... destruct v0; destruct v1... destruct v0... destruct v0; destruct v1; simpl in *; inv H0. @@ -792,7 +792,7 @@ Proof. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. econstructor; eauto. rewrite Int.sub_add_l. auto. - destruct (zeq b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite zeq_true. + destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. rewrite Int.sub_shifted. auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 58c9572..35d5385 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -177,6 +177,9 @@ Proof (Pos.lt_irrefl). Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. +Ltac xomega := unfold Plt, Ple in *; zify; omega. +Ltac xomegaContradiction := exfalso; xomega. + (** Peano recursion over positive numbers. *) Section POSITIVE_ITERATION. diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 55a23f2..bbe2d3e 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -889,7 +889,7 @@ Inductive initial_state (p: program): state -> Prop := (Pregmap.init Vundef) # PC <- (symbol_offset ge p.(prog_main) Int.zero) # LR <- Vzero - # GPR1 <- (Vptr Mem.nullptr Int.zero) in + # GPR1 <- Vzero in initial_state p (State rs0 m0). Inductive final_state: state -> int -> Prop := diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 2c155ea..869fab3 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -973,7 +973,7 @@ Proof. econstructor; eauto. constructor. apply Mem.extends_refl. - split. auto. simpl. congruence. intros. rewrite Regmap.gi. auto. + split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. unfold symbol_offset. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. diff --git a/powerpc/Op.v b/powerpc/Op.v index 3963c6b..1952304 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -347,7 +347,7 @@ Proof with (try exact I). destruct v0... destruct v0; destruct v1... destruct v0... - destruct v0; destruct v1... simpl. destruct (zeq b b0)... + destruct v0; destruct v1... simpl. destruct (eq_block b b0)... destruct v0... destruct v0; destruct v1... destruct v0... @@ -754,7 +754,7 @@ Proof. apply Values.val_add_inject; auto. inv H4; inv H2; simpl; auto. econstructor; eauto. rewrite Int.sub_add_l. auto. - destruct (zeq b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite zeq_true. + destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. rewrite Int.sub_shifted. auto. inv H4; auto. inv H4; inv H2; simpl; auto. diff --git a/runtime/Makefile b/runtime/Makefile index 81df4ea..668e365 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -7,7 +7,11 @@ OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \ i64_udivmod.o i64_udiv.o i64_umod.o i64_utod.o i64_utof.o LIB=libcompcert.a +ifeq ($(strip $(HAS_RUNTIME_LIB)),true) all: $(LIB) $(INCLUDES) +else +all: +endif $(LIB): $(OBJS) rm -f $(LIB) @@ -22,9 +26,13 @@ $(LIB): $(OBJS) clean:: rm -f *.o $(LIB) +ifeq ($(strip $(HAS_RUNTIME_LIB)),true) install: install -d $(LIBDIR) install -c $(LIB) $(INCLUDES) $(LIBDIR) +else +install: +endif test/test_int64: test/test_int64.c $(LIB) $(CC) -o $@ test/test_int64.c $(LIB) |