From b40e056328e183522b50c68aefdbff057bca29cc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 16 Jun 2013 06:56:02 +0000 Subject: Merge of the "princeton" branch: - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgenproof.v | 144 ++++++++++++++++++++++----------------------- 1 file changed, 71 insertions(+), 73 deletions(-) (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 2df8b932..d6b99edd 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. -- cgit