diff options
Diffstat (limited to 'common')
| -rw-r--r-- | common/AST.v | 14 | ||||
| -rw-r--r-- | common/Events.v | 10 | ||||
| -rw-r--r-- | common/Globalenvs.v | 144 | ||||
| -rw-r--r-- | common/Linking.v | 126 | ||||
| -rw-r--r-- | common/Memdata.v | 2 | ||||
| -rw-r--r-- | common/Memory.v | 54 | ||||
| -rw-r--r-- | common/Separation.v | 142 | ||||
| -rw-r--r-- | common/Smallstep.v | 6 | ||||
| -rw-r--r-- | common/Values.v | 93 |
9 files changed, 320 insertions, 271 deletions
diff --git a/common/AST.v b/common/AST.v index 34f29bb3..8a46a153 100644 --- a/common/AST.v +++ b/common/AST.v @@ -111,7 +111,7 @@ Definition cc_default := Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}. Proof. - decide equality; apply bool_dec. + decide equality; apply bool_dec. Defined. Global Opaque calling_convention_eq. @@ -301,7 +301,7 @@ Lemma prog_defmap_unique: ~In id (map fst defs2) -> (prog_defmap p)!id = Some g. Proof. - unfold prog_defmap; intros. rewrite H. apply PTree_Properties.of_list_unique; auto. + unfold prog_defmap; intros. rewrite H. apply PTree_Properties.of_list_unique; auto. Qed. Lemma prog_defmap_norepet: @@ -408,7 +408,7 @@ Proof. OK (List.map (transform_program_globdef transf_fun) l)). { induction l as [ | [id g] l]; simpl. - auto. - - destruct g; simpl; rewrite IHl; simpl. auto. destruct v; auto. + - destruct g; simpl; rewrite IHl; simpl. auto. destruct v; auto. } rewrite EQ; simpl. auto. Qed. @@ -563,7 +563,7 @@ End TRANSF_PARTIAL_FUNDEF. Set Contextual Implicit. (** In some intermediate languages (LTL, Mach), 64-bit integers can be - split into two 32-bit halves and held in a pair of registers. + split into two 32-bit halves and held in a pair of registers. Syntactically, this is captured by the type [rpair] below. *) Inductive rpair (A: Type) : Type := @@ -589,7 +589,7 @@ Definition regs_of_rpair (A: Type) (p: rpair A): list A := end. Fixpoint regs_of_rpairs (A: Type) (l: list (rpair A)): list A := - match l with + match l with | nil => nil | p :: l => regs_of_rpair p ++ regs_of_rpairs l end. @@ -603,8 +603,8 @@ Qed. Lemma in_regs_of_rpairs_inv: forall (A: Type) (x: A) l, In x (regs_of_rpairs l) -> exists p, In p l /\ In x (regs_of_rpair p). Proof. - induction l; simpl; intros. contradiction. - rewrite in_app_iff in H; destruct H. + induction l; simpl; intros. contradiction. + rewrite in_app_iff in H; destruct H. exists a; auto. apply IHl in H. firstorder auto. Qed. diff --git a/common/Events.v b/common/Events.v index 97d4f072..14cd27c5 100644 --- a/common/Events.v +++ b/common/Events.v @@ -976,7 +976,7 @@ Proof. { intros. apply Mem.unchanged_on_implies with (fun b1 ofs1 => b1 <> b). - apply Mem.unchanged_on_trans with m'. + apply Mem.unchanged_on_trans with m'. eapply Mem.alloc_unchanged_on; eauto. eapply Mem.store_unchanged_on; eauto. intros. eapply Mem.valid_not_valid_diff; eauto with mem. @@ -997,7 +997,7 @@ Proof. (* mem extends *) - inv H. inv H1. inv H7. assert (SZ: v2 = Vptrofs sz). - { unfold Vptrofs in *. destruct Archi.ptr64; inv H5; auto. } + { unfold Vptrofs in *. destruct Archi.ptr64; inv H5; auto. } subst v2. exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. intros [m3' [A B]]. @@ -1009,7 +1009,7 @@ Proof. (* mem injects *) - inv H0. inv H2. inv H8. assert (SZ: v' = Vptrofs sz). - { unfold Vptrofs in *. destruct Archi.ptr64; inv H6; auto. } + { unfold Vptrofs in *. destruct Archi.ptr64; inv H6; auto. } subst v'. exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. @@ -1036,7 +1036,7 @@ Proof. rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence. rewrite <- (Ptrofs.of_int_to_int SF sz0), <- (Ptrofs.of_int_to_int SF sz). congruence. } - subst. + subst. split. constructor. intuition congruence. Qed. @@ -1093,7 +1093,7 @@ Proof. eapply Mem.free_range_perm; eauto. exploit Mem.address_inject; eauto. apply Mem.perm_implies with Freeable; auto with mem. - apply P. instantiate (1 := lo). + apply P. instantiate (1 := lo). generalize (size_chunk_pos Mptr); omega. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 9affd634..dd8a1eb9 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -259,7 +259,7 @@ Lemma add_globals_app: forall gl2 gl1 ge, add_globals ge (gl1 ++ gl2) = add_globals (add_globals ge gl1) gl2. Proof. - intros. apply fold_left_app. + intros. apply fold_left_app. Qed. Program Definition empty_genv (pub: list ident): t := @@ -429,17 +429,17 @@ Proof. { induction l as [ | [id1 g1] l]; intros; simpl. - auto. - apply IHl. unfold P, add_global, find_symbol, find_def; simpl. - rewrite ! PTree.gsspec. destruct (peq id id1). + rewrite ! PTree.gsspec. destruct (peq id id1). + subst id1. split; intros. inv H0. exists (genv_next ge); split; auto. apply PTree.gss. destruct H0 as (b & A & B). inv A. rewrite PTree.gss in B. auto. + red in H; rewrite H. split. - intros (b & A & B). exists b; split; auto. rewrite PTree.gso; auto. - apply Plt_ne. eapply genv_symb_range; eauto. - intros (b & A & B). rewrite PTree.gso in B. exists b; auto. - apply Plt_ne. eapply genv_symb_range; eauto. + intros (b & A & B). exists b; split; auto. rewrite PTree.gso; auto. + apply Plt_ne. eapply genv_symb_range; eauto. + intros (b & A & B). rewrite PTree.gso in B. exists b; auto. + apply Plt_ne. eapply genv_symb_range; eauto. } - apply REC. unfold P, find_symbol, find_def; simpl. + apply REC. unfold P, find_symbol, find_def; simpl. rewrite ! PTree.gempty. split. congruence. intros (b & A & B); congruence. @@ -770,12 +770,12 @@ Remark store_init_data_perm: store_init_data m b p i = Some m' -> (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. - intros. + intros. assert (forall chunk v, Mem.store chunk m b p v = Some m' -> (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm)). intros; split; eauto with mem. - destruct i; simpl in H; eauto. + destruct i; simpl in H; eauto. inv H; tauto. destruct (find_symbol ge i); try discriminate. eauto. Qed. @@ -788,7 +788,7 @@ Proof. induction idl as [ | i1 idl]; simpl; intros. - inv H; tauto. - destruct (store_init_data m b p i1) as [m1|] eqn:S1; try discriminate. - transitivity (Mem.perm m1 b' q k prm). + transitivity (Mem.perm m1 b' q k prm). eapply store_init_data_perm; eauto. eapply IHidl; eauto. Qed. @@ -849,8 +849,8 @@ Proof. intros until n. functional induction (store_zeros m b p n); intros. - inv H; apply Mem.unchanged_on_refl. - apply Mem.unchanged_on_trans with m'. -+ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega. -+ apply IHo; auto. intros; apply H0; omega. ++ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega. ++ apply IHo; auto. intros; apply H0; omega. - discriminate. Qed. @@ -878,7 +878,7 @@ Proof. - inv H. apply Mem.unchanged_on_refl. - destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. apply Mem.unchanged_on_trans with m1. - eapply store_init_data_unchanged; eauto. intros; apply H0; tauto. + eapply store_init_data_unchanged; eauto. intros; apply H0; tauto. eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); omega. Qed. @@ -947,8 +947,8 @@ Proof. intros; destruct i; simpl in H; try apply (Mem.loadbytes_store_same _ _ _ _ _ _ H). - inv H. simpl. assert (EQ: Z.of_nat (Z.to_nat z) = Z.max z 0). - { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } - rewrite <- EQ. apply H0. omega. simpl. omega. + { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } + rewrite <- EQ. apply H0. omega. simpl. omega. - rewrite init_data_size_addrof. simpl. destruct (find_symbol ge i) as [b'|]; try discriminate. rewrite (Mem.loadbytes_store_same _ _ _ _ _ _ H). @@ -976,14 +976,14 @@ Proof. eapply store_init_data_list_unchanged; eauto. intros; omega. intros; omega. - eapply store_init_data_loadbytes; eauto. + eapply store_init_data_loadbytes; eauto. red; intros; apply H0. omega. omega. apply IHil with m1; auto. - red; intros. + red; intros. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => p + init_data_size i1 <= ofs1). - eapply store_init_data_unchanged; eauto. + eapply store_init_data_unchanged; eauto. + intros; omega. intros; omega. - intros; omega. apply H0. omega. omega. auto. auto. Qed. @@ -1010,9 +1010,9 @@ Remark read_as_zero_unchanged: (forall i, ofs <= i < ofs + len -> P b i) -> read_as_zero m' b ofs len. Proof. - intros; red; intros. eapply Mem.load_unchanged_on; eauto. - intros; apply H1. omega. -Qed. + intros; red; intros. eapply Mem.load_unchanged_on; eauto. + intros; apply H1. omega. +Qed. Lemma store_zeros_read_as_zero: forall m b p n m', @@ -1078,7 +1078,7 @@ Proof. exploit IHil; eauto. set (P := fun (b': block) ofs' => p + init_data_size a <= ofs'). apply read_as_zero_unchanged with (m := m) (P := P). - red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega. + red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega. eapply store_init_data_unchanged with (P := P); eauto. intros; unfold P. omega. intros; unfold P. omega. @@ -1094,7 +1094,7 @@ Proof. set (P := fun (b': block) ofs' => ofs' < p + init_data_size (Init_space z)). inv Heqo. apply read_as_zero_unchanged with (m := m1) (P := P). red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega. - eapply store_init_data_list_unchanged; eauto. + eapply store_init_data_list_unchanged; eauto. intros; unfold P. omega. intros; unfold P. simpl; xomega. + rewrite init_data_size_addrof in *. @@ -1118,7 +1118,7 @@ Proof. apply Mem.unchanged_on_implies with Q. apply Mem.unchanged_on_trans with m1. eapply Mem.alloc_unchanged_on; eauto. - eapply Mem.drop_perm_unchanged_on; eauto. + eapply Mem.drop_perm_unchanged_on; eauto. intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem. - (* variable *) set (init := gvar_init v) in *. @@ -1133,8 +1133,8 @@ Proof. apply Mem.unchanged_on_trans with m2. eapply store_zeros_unchanged; eauto. apply Mem.unchanged_on_trans with m3. - eapply store_init_data_list_unchanged; eauto. - eapply Mem.drop_perm_unchanged_on; eauto. + eapply store_init_data_list_unchanged; eauto. + eapply Mem.drop_perm_unchanged_on; eauto. intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem. Qed. @@ -1147,7 +1147,7 @@ Proof. - inv H. apply Mem.unchanged_on_refl. - destruct (alloc_global m a) as [m''|] eqn:?; try discriminate. destruct a as [id g]. - apply Mem.unchanged_on_trans with m''. + apply Mem.unchanged_on_trans with m''. eapply alloc_global_unchanged; eauto. apply IHgl; auto. Qed. @@ -1196,7 +1196,7 @@ Proof. exploit Mem.alloc_result; eauto. intros RES. rewrite H, <- RES. split. eapply Mem.perm_drop_1; eauto. omega. - intros. + intros. assert (0 <= ofs < 1). { eapply Mem.perm_alloc_3; eauto. eapply Mem.perm_drop_4; eauto. } exploit Mem.perm_drop_2; eauto. intros ORD. split. omega. inv ORD; auto. @@ -1210,35 +1210,35 @@ Proof. split. red; intros. eapply Mem.perm_drop_1; eauto. split. intros. assert (0 <= ofs < sz). - { eapply Mem.perm_alloc_3; eauto. + { eapply Mem.perm_alloc_3; eauto. erewrite store_zeros_perm by eauto. - erewrite store_init_data_list_perm by eauto. + erewrite store_init_data_list_perm by eauto. eapply Mem.perm_drop_4; eauto. } split; auto. eapply Mem.perm_drop_2; eauto. split. intros NOTVOL. apply load_store_init_data_invariant with m3. - intros. eapply Mem.load_drop; eauto. right; right; right. + intros. eapply Mem.load_drop; eauto. right; right; right. unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem. - eapply store_init_data_list_charact; eauto. + eapply store_init_data_list_charact; eauto. eapply store_zeros_read_as_zero; eauto. - intros NOTVOL. - transitivity (Mem.loadbytes m3 b 0 sz). + intros NOTVOL. + transitivity (Mem.loadbytes m3 b 0 sz). eapply Mem.loadbytes_drop; eauto. right; right; right. unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem. eapply store_init_data_list_loadbytes; eauto. eapply store_zeros_loadbytes; eauto. + assert (U: Mem.unchanged_on (fun _ _ => True) m m') by (eapply alloc_global_unchanged; eauto). assert (VALID: Mem.valid_block m b). - { red. rewrite <- H. eapply genv_defs_range; eauto. } + { red. rewrite <- H. eapply genv_defs_range; eauto. } exploit H1; eauto. destruct gd0 as [f|v]. * intros [A B]; split; intros. eapply Mem.perm_unchanged_on; eauto. exact I. eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I. -* intros (A & B & C & D). split; [| split; [| split]]. +* intros (A & B & C & D). split; [| split; [| split]]. red; intros. eapply Mem.perm_unchanged_on; eauto. exact I. intros. eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I. - intros. apply load_store_init_data_invariant with m; auto. + intros. apply load_store_init_data_invariant with m; auto. intros. eapply Mem.load_unchanged_on_1; eauto. intros; exact I. intros. eapply Mem.loadbytes_unchanged_on; eauto. intros; exact I. - simpl. congruence. @@ -1312,7 +1312,7 @@ Lemma init_mem_characterization_gen: init_mem p = Some m -> globals_initialized (globalenv p) (globalenv p) m. Proof. - intros. apply alloc_globals_initialized with Mem.empty. + intros. apply alloc_globals_initialized with Mem.empty. auto. rewrite Mem.nextblock_empty. auto. red; intros. unfold find_def in H0; simpl in H0; rewrite PTree.gempty in H0; discriminate. @@ -1499,7 +1499,7 @@ Proof. { intros. apply Mem.store_valid_access_3 in H0. destruct H0. congruence. } destruct i; simpl in H; eauto. simpl. apply Z.divide_1_l. - destruct (find_symbol ge i); try discriminate. eapply DFL. eassumption. + destruct (find_symbol ge i); try discriminate. eapply DFL. eassumption. unfold Mptr, init_data_alignment; destruct Archi.ptr64; auto. Qed. @@ -1537,14 +1537,14 @@ Theorem init_mem_inversion: init_data_list_aligned 0 v.(gvar_init) /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol (globalenv p) i = Some b. Proof. - intros until v. unfold init_mem. set (ge := globalenv p). - revert m. generalize Mem.empty. generalize (prog_defs p). + intros until v. unfold init_mem. set (ge := globalenv p). + revert m. generalize Mem.empty. generalize (prog_defs p). induction l as [ | idg1 defs ]; simpl; intros m m'; intros. - contradiction. - destruct (alloc_global ge m idg1) as [m''|] eqn:A; try discriminate. destruct H0. -+ subst idg1; simpl in A. - set (il := gvar_init v) in *. set (sz := init_data_list_size il) in *. ++ subst idg1; simpl in A. + set (il := gvar_init v) in *. set (sz := init_data_list_size il) in *. destruct (Mem.alloc m 0 sz) as [m1 b]. destruct (store_zeros m1 b 0 sz) as [m2|]; try discriminate. destruct (store_init_data_list ge m2 b 0 il) as [m3|] eqn:B; try discriminate. @@ -1565,7 +1565,7 @@ Proof. - exists m; auto. - apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. omega. - destruct (Mem.valid_access_store m Mint8unsigned b p Vzero) as (m' & STORE). - split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega. + split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega. simpl. apply Z.divide_1_l. congruence. Qed. @@ -1577,17 +1577,17 @@ Lemma store_init_data_exists: (forall id ofs, i = Init_addrof id ofs -> exists b, find_symbol ge id = Some b) -> exists m', store_init_data ge m b p i = Some m'. Proof. - intros. + intros. assert (DFL: forall chunk v, init_data_size i = size_chunk chunk -> init_data_alignment i = align_chunk chunk -> exists m', Mem.store chunk m b p v = Some m'). { intros. destruct (Mem.valid_access_store m chunk b p v) as (m' & STORE). - split. rewrite <- H2; auto. rewrite <- H3; auto. + split. rewrite <- H2; auto. rewrite <- H3; auto. exists m'; auto. } destruct i; eauto. simpl. exists m; auto. - simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eapply DFL. + simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eapply DFL. unfold init_data_size, Mptr. destruct Archi.ptr64; auto. unfold init_data_alignment, Mptr. destruct Archi.ptr64; auto. Qed. @@ -1601,11 +1601,11 @@ Lemma store_init_data_list_exists: Proof. induction il as [ | i1 il ]; simpl; intros. - exists m; auto. -- destruct H0. +- destruct H0. destruct (@store_init_data_exists m b p i1) as (m1 & S1); eauto. red; intros. apply H. generalize (init_data_list_size_pos il); omega. - rewrite S1. - apply IHil; eauto. + rewrite S1. + apply IHil; eauto. red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); omega. Qed. @@ -1622,7 +1622,7 @@ Proof. intros m [id [f|v]]; intros; simpl. - destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC. destruct (Mem.range_perm_drop_2 m1 b 0 1 Nonempty) as [m2 DROP]. - red; intros; eapply Mem.perm_alloc_2; eauto. + red; intros; eapply Mem.perm_alloc_2; eauto. exists m2; auto. - destruct H as [P Q]. set (sz := init_data_list_size (gvar_init v)). @@ -1651,14 +1651,14 @@ Theorem init_mem_exists: /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol (globalenv p) i = Some b) -> exists m, init_mem p = Some m. Proof. - intros. set (ge := globalenv p) in *. + intros. set (ge := globalenv p) in *. unfold init_mem. revert H. generalize (prog_defs p) Mem.empty. induction l as [ | idg l]; simpl; intros. - exists m; auto. - destruct (@alloc_global_exists ge m idg) as [m1 A1]. destruct idg as [id [f|v]]; eauto. - fold ge. rewrite A1. eapply IHl; eauto. -Qed. + fold ge. rewrite A1. eapply IHl; eauto. +Qed. End GENV. @@ -1685,8 +1685,8 @@ Lemma add_global_match: Proof. intros. destruct H. constructor; simpl; intros. - congruence. -- rewrite mge_next0, ! PTree.gsspec. destruct (peq id0 id); auto. -- rewrite mge_next0, ! PTree.gsspec. destruct (peq b (genv_next ge1)). +- rewrite mge_next0, ! PTree.gsspec. destruct (peq id0 id); auto. +- rewrite mge_next0, ! PTree.gsspec. destruct (peq b (genv_next ge1)). constructor; auto. auto. Qed. @@ -1718,7 +1718,7 @@ Hypothesis progmatch: match_program_gen match_fundef match_varinfo ctx p tp. Lemma globalenvs_match: match_genvs (match_globdef match_fundef match_varinfo ctx) (globalenv p) (globalenv tp). Proof. - intros. apply add_globals_match. apply progmatch. + intros. apply add_globals_match. apply progmatch. constructor; simpl; intros; auto. rewrite ! PTree.gempty. constructor. Qed. @@ -1734,7 +1734,7 @@ Theorem find_def_match: find_def (globalenv tp) b = Some tg /\ match_globdef match_fundef match_varinfo ctx g tg. Proof. intros. generalize (find_def_match_2 b). rewrite H; intros R; inv R. - exists y; auto. + exists y; auto. Qed. Theorem find_funct_ptr_match: @@ -1743,8 +1743,8 @@ Theorem find_funct_ptr_match: exists cunit tf, find_funct_ptr (globalenv tp) b = Some tf /\ match_fundef cunit f tf /\ linkorder cunit ctx. Proof. - intros. rewrite find_funct_ptr_iff in *. apply find_def_match in H. - destruct H as (tg & P & Q). inv Q. + intros. rewrite find_funct_ptr_iff in *. apply find_def_match in H. + destruct H as (tg & P & Q). inv Q. exists ctx', f2; intuition auto. apply find_funct_ptr_iff; auto. Qed. @@ -1766,8 +1766,8 @@ Theorem find_var_info_match: exists tv, find_var_info (globalenv tp) b = Some tv /\ match_globvar match_varinfo v tv. Proof. - intros. rewrite find_var_info_iff in *. apply find_def_match in H. - destruct H as (tg & P & Q). inv Q. + intros. rewrite find_var_info_iff in *. apply find_def_match in H. + destruct H as (tg & P & Q). inv Q. exists v2; split; auto. apply find_var_info_iff; auto. Qed. @@ -1783,10 +1783,10 @@ Theorem senv_match: Proof. red; simpl. repeat split. - apply find_symbol_match. -- intros. unfold public_symbol. rewrite find_symbol_match. - rewrite ! globalenv_public. +- intros. unfold public_symbol. rewrite find_symbol_match. + rewrite ! globalenv_public. destruct progmatch as (P & Q & R). rewrite R. auto. -- intros. unfold block_is_volatile. +- intros. unfold block_is_volatile. destruct globalenvs_match as [P Q R]. specialize (R b). unfold find_var_info, find_def. inv R; auto. @@ -1820,7 +1820,7 @@ Proof. { destruct a1 as [id1 g1]; destruct b1 as [id2 g2]; destruct H; simpl in *. subst id2. inv H2. - auto. - - inv H; simpl in *. + - inv H; simpl in *. set (sz := init_data_list_size init) in *. destruct (Mem.alloc m 0 sz) as [m2 b] eqn:?. destruct (store_zeros m2 b 0 sz) as [m3|] eqn:?; try discriminate. @@ -1853,7 +1853,7 @@ Theorem find_funct_ptr_transf_partial: exists tf, find_funct_ptr (globalenv tp) b = Some tf /\ transf f = OK tf. Proof. - intros. exploit (find_funct_ptr_match progmatch); eauto. + intros. exploit (find_funct_ptr_match progmatch); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. @@ -1863,7 +1863,7 @@ Theorem find_funct_transf_partial: exists tf, find_funct (globalenv tp) v = Some tf /\ transf f = OK tf. Proof. - intros. exploit (find_funct_match progmatch); eauto. + intros. exploit (find_funct_match progmatch); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. @@ -1871,7 +1871,7 @@ Theorem find_symbol_transf_partial: forall (s : ident), find_symbol (globalenv tp) s = find_symbol (globalenv p) s. Proof. - intros. eapply (find_symbol_match progmatch). + intros. eapply (find_symbol_match progmatch). Qed. Theorem senv_transf_partial: @@ -1901,7 +1901,7 @@ Theorem find_funct_ptr_transf: find_funct_ptr (globalenv p) b = Some f -> find_funct_ptr (globalenv tp) b = Some (transf f). Proof. - intros. exploit (find_funct_ptr_match progmatch); eauto. + intros. exploit (find_funct_ptr_match progmatch); eauto. intros (cu & tf & P & Q & R). congruence. Qed. @@ -1910,7 +1910,7 @@ Theorem find_funct_transf: find_funct (globalenv p) v = Some f -> find_funct (globalenv tp) v = Some (transf f). Proof. - intros. exploit (find_funct_match progmatch); eauto. + intros. exploit (find_funct_match progmatch); eauto. intros (cu & tf & P & Q & R). congruence. Qed. diff --git a/common/Linking.v b/common/Linking.v index 52e774db..eaa95462 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -111,13 +111,13 @@ Inductive linkorder_varinit: list init_data -> list init_data -> Prop := Instance Linker_varinit : Linker (list init_data) := { link := link_varinit; - linkorder := linkorder_varinit + linkorder := linkorder_varinit }. Proof. - intros. constructor. - intros. inv H; inv H0; constructor; auto. congruence. - simpl. generalize (init_data_list_size_pos z). xomega. + simpl. generalize (init_data_list_size_pos z). xomega. - unfold link_varinit; intros until z. destruct (classify_init x) eqn:Cx, (classify_init y) eqn:Cy; intros E; inv E; try (split; constructor; fail). + destruct (zeq sz (Z.max sz0 0 + 0)); inv H0. @@ -159,7 +159,7 @@ Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := { linkorder := linkorder_vardef }. Proof. -- intros. destruct x; constructor; apply linkorder_refl. +- intros. destruct x; constructor; apply linkorder_refl. - intros. inv H; inv H0. constructor; eapply linkorder_trans; eauto. - unfold link_vardef; intros until z. destruct x as [f1 i1 r1 v1], y as [f2 i2 r2 v2]; simpl. @@ -214,7 +214,7 @@ Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F Proof. - intros. destruct x; constructor; apply linkorder_refl. - intros. inv H; inv H0; constructor; eapply linkorder_trans; eauto. -- unfold link_def; intros. +- unfold link_def; intros. destruct x as [f1|v1], y as [f2|v2]; try discriminate. + destruct (link f1 f2) as [f|] eqn:L; inv H. apply link_linkorder in L. split; constructor; tauto. @@ -229,7 +229,7 @@ Global Opaque Linker_def. a global definition in one unit but not in the other, this definition is left unchanged in the result of the link. If a name has global definitions in both units, and is public (not static) in both, - the two definitions are linked as per [Linker_def] above. + the two definitions are linked as per [Linker_def] above. If one or both definitions are static (not public), we should ideally rename it so that it can be kept unchanged in the result of the link. @@ -284,8 +284,8 @@ Proof. unfold link_prog; intros p E. destruct (ident_eq (prog_main p1) (prog_main p2)); try discriminate. destruct (PTree_Properties.for_all dm1 link_prog_check) eqn:C; inv E. - rewrite PTree_Properties.for_all_correct in C. - split; auto. split; auto. + rewrite PTree_Properties.for_all_correct in C. + split; auto. split; auto. intros. exploit C; eauto. unfold link_prog_check. rewrite H0. intros. destruct (in_dec peq id (prog_public p1)); try discriminate. destruct (in_dec peq id (prog_public p2)); try discriminate. @@ -303,7 +303,7 @@ Lemma link_prog_succeeds: prog_public := p1.(prog_public) ++ p2.(prog_public); prog_defs := PTree.elements (PTree.combine link_prog_merge dm1 dm2) |}. Proof. - intros. unfold link_prog. unfold proj_sumbool. rewrite H, dec_eq_true. simpl. + intros. unfold link_prog. unfold proj_sumbool. rewrite H, dec_eq_true. simpl. replace (PTree_Properties.for_all dm1 link_prog_check) with true; auto. symmetry. apply PTree_Properties.for_all_correct; intros. rename a into gd1. unfold link_prog_check. destruct dm2!x as [gd2|] eqn:G2; auto. @@ -334,29 +334,29 @@ Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program }. Proof. - intros; split; auto. split. apply incl_refl. intros. - exists gd1; split; auto. split; auto. apply linkorder_refl. + exists gd1; split; auto. split; auto. apply linkorder_refl. -- intros x y z (A1 & B1 & C1) (A2 & B2 & C2). - split. congruence. split. red; eauto. - intros. exploit C1; eauto. intros (gd2 & P & Q & R). - exploit C2; eauto. intros (gd3 & U & X & Y). - exists gd3. split; auto. split. eapply linkorder_trans; eauto. - intros. transitivity gd2. apply Y. auto. apply R. red; intros; elim H0; auto. +- intros x y z (A1 & B1 & C1) (A2 & B2 & C2). + split. congruence. split. red; eauto. + intros. exploit C1; eauto. intros (gd2 & P & Q & R). + exploit C2; eauto. intros (gd3 & U & X & Y). + exists gd3. split; auto. split. eapply linkorder_trans; eauto. + intros. transitivity gd2. apply Y. auto. apply R. red; intros; elim H0; auto. - intros. apply link_prog_inv in H. destruct H as (L1 & L2 & L3). subst z; simpl. intuition auto. + red; intros; apply in_app_iff; auto. -+ rewrite prog_defmap_elements, PTree.gcombine, H by auto. ++ rewrite prog_defmap_elements, PTree.gcombine, H by auto. destruct (prog_defmap y)!id as [gd2|] eqn:GD2; simpl. * exploit L2; eauto. intros (P & Q & gd & R). - exists gd; split. auto. split. apply link_linkorder in R; tauto. + exists gd; split. auto. split. apply link_linkorder in R; tauto. rewrite in_app_iff; tauto. * exists gd1; split; auto. split. apply linkorder_refl. auto. + red; intros; apply in_app_iff; auto. -+ rewrite prog_defmap_elements, PTree.gcombine, H by auto. ++ rewrite prog_defmap_elements, PTree.gcombine, H by auto. destruct (prog_defmap x)!id as [gd2|] eqn:GD2; simpl. * exploit L2; eauto. intros (P & Q & gd & R). - exists gd; split. auto. split. apply link_linkorder in R; tauto. + exists gd; split. auto. split. apply link_linkorder in R; tauto. rewrite in_app_iff; tauto. * exists gd1; split; auto. split. apply linkorder_refl. auto. Defined. @@ -417,24 +417,24 @@ Theorem match_program_defmap: forall ctx p1 p2, match_program_gen ctx p1 p2 -> forall id, option_rel (match_globdef ctx) (prog_defmap p1)!id (prog_defmap p2)!id. Proof. - intros. apply PTree_Properties.of_list_related. apply H. + intros. apply PTree_Properties.of_list_related. apply H. Qed. Lemma match_program_gen_main: forall ctx p1 p2, match_program_gen ctx p1 p2 -> p2.(prog_main) = p1.(prog_main). Proof. - intros. apply H. + intros. apply H. Qed. Lemma match_program_public: forall ctx p1 p2, match_program_gen ctx p1 p2 -> p2.(prog_public) = p1.(prog_public). Proof. - intros. apply H. + intros. apply H. Qed. End MATCH_PROGRAM_GENERIC. -(** In many cases, the context for [match_program_gen] is the source program or +(** In many cases, the context for [match_program_gen] is the source program or source compilation unit itself. We provide a specialized definition for this case. *) Definition match_program {F1 V1 F2 V2: Type} {LF: Linker F1} {LV: Linker V1} @@ -464,7 +464,7 @@ Lemma match_program_implies: (forall v w, match_varinfo1 v w -> match_varinfo2 v w) -> match_program match_fundef2 match_varinfo2 p p'. Proof. - intros. destruct H as [P Q]. split; auto. + intros. destruct H as [P Q]. split; auto. eapply list_forall2_imply; eauto. intros. inv H3. split; auto. inv H5. econstructor; eauto. @@ -488,12 +488,12 @@ Theorem match_transform_partial_program2: match_program_gen match_fundef match_varinfo ctx p tp. Proof. unfold transform_partial_program2; intros. monadInv H. - red; simpl; split; auto. - revert x EQ. generalize (prog_defs p). + red; simpl; split; auto. + revert x EQ. generalize (prog_defs p). induction l as [ | [i g] l]; simpl; intros. - monadInv EQ. constructor. - destruct g as [f|v]. -+ destruct (transf_fun i f) as [tf|?] eqn:TF; monadInv EQ. ++ destruct (transf_fun i f) as [tf|?] eqn:TF; monadInv EQ. constructor; auto. split; simpl; auto. econstructor. apply linkorder_refl. eauto. + destruct (transf_globvar transf_var i v) as [tv|?] eqn:TV; monadInv EQ. constructor; auto. split; simpl; auto. constructor. @@ -509,7 +509,7 @@ Theorem match_transform_partial_program_contextual: (forall f tf, transf_fun f = OK tf -> match_fundef p f tf) -> match_program match_fundef eq p tp. Proof. - intros. + intros. eapply match_transform_partial_program2. eexact H. auto. simpl; intros. congruence. @@ -523,8 +523,8 @@ Theorem match_transform_program_contextual: (forall f, match_fundef p f (transf_fun f)) -> match_program match_fundef eq p (transform_program transf_fun p). Proof. - intros. - eapply match_transform_partial_program_contextual. + intros. + eapply match_transform_partial_program_contextual. apply transform_program_partial_program with (transf_fun := transf_fun). simpl; intros. inv H0. auto. Qed. @@ -582,11 +582,11 @@ Lemma link_match_globvar: match_globvar match_varinfo v1 tv1 -> match_globvar match_varinfo v2 tv2 -> exists tv, link tv1 tv2 = Some tv /\ match_globvar match_varinfo v tv. Proof. - simpl; intros. unfold link_vardef in *. inv H0; inv H1; simpl in *. + simpl; intros. unfold link_vardef in *. inv H0; inv H1; simpl in *. destruct (link i1 i0) as [info'|] eqn:LINFO; try discriminate. destruct (link init init0) as [init'|] eqn:LINIT; try discriminate. destruct (eqb ro ro0 && eqb vo vo0); inv H. - exploit link_match_varinfo; eauto. intros (tinfo & P & Q). rewrite P. + exploit link_match_varinfo; eauto. intros (tinfo & P & Q). rewrite P. econstructor; split. eauto. constructor. auto. Qed. @@ -603,7 +603,7 @@ Proof. exploit link_match_fundef; eauto. intros (tf & P & Q). assert (X: exists ctx', linkorder ctx' ctx /\ match_fundef ctx' f tf). { destruct Q as [Q|Q]; econstructor; (split; [|eassumption]). - apply linkorder_trans with ctx1; auto. + apply linkorder_trans with ctx1; auto. apply linkorder_trans with ctx2; auto. } destruct X as (cu & X & Y). exists (Gfun tf); split. rewrite P; auto. econstructor; eauto. @@ -618,7 +618,7 @@ Lemma match_globdef_linkorder: linkorder ctx ctx' -> match_globdef match_fundef match_varinfo ctx' g tg. Proof. - intros. inv H. + intros. inv H. - econstructor. eapply linkorder_trans; eauto. auto. - constructor; auto. Qed. @@ -635,25 +635,25 @@ Proof. generalize H0; intros (A1 & B1 & C1). generalize H1; intros (A2 & B2 & C2). econstructor; split. -- apply link_prog_succeeds. -+ congruence. -+ intros. +- apply link_prog_succeeds. ++ congruence. ++ intros. generalize (match_program_defmap _ _ _ _ _ H0 id) (match_program_defmap _ _ _ _ _ H1 id). rewrite H4, H5. intros R1 R2; inv R1; inv R2. exploit Q; eauto. intros (X & Y & gd & Z). - exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto. + exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto. intros (tg & TL & _). intuition congruence. - split; [|split]. -+ rewrite R. apply PTree.elements_canonical_order'. intros id. ++ rewrite R. apply PTree.elements_canonical_order'. intros id. rewrite ! PTree.gcombine by auto. generalize (match_program_defmap _ _ _ _ _ H0 id) (match_program_defmap _ _ _ _ _ H1 id). clear R. intros R1 R2; inv R1; inv R2; unfold link_prog_merge. * constructor. -* constructor. apply match_globdef_linkorder with ctx2; auto. +* constructor. apply match_globdef_linkorder with ctx2; auto. * constructor. apply match_globdef_linkorder with ctx1; auto. * exploit Q; eauto. intros (X & Y & gd & Z). - exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto. - intros (tg & TL & MG). rewrite Z, TL. constructor; auto. + exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto. + intros (tg & TL & MG). rewrite Z, TL. constructor; auto. + rewrite R; simpl; auto. + rewrite R; simpl. congruence. Qed. @@ -674,7 +674,7 @@ Remark link_transf_partial_fundef: link f1 f2 = Some f -> transf_partial_fundef tr1 f1 = OK tf1 -> transf_partial_fundef tr2 f2 = OK tf2 -> - exists tf, + exists tf, link tf1 tf2 = Some tf /\ (transf_partial_fundef tr1 f = OK tf \/ transf_partial_fundef tr2 f = OK tf). Proof. @@ -683,7 +683,7 @@ Local Transparent Linker_fundef. - discriminate. - destruct ef2; inv H. exists (Internal x); split; auto. left; simpl; rewrite EQ; auto. - destruct ef1; inv H. exists (Internal x); split; auto. right; simpl; rewrite EQ; auto. -- destruct (external_function_eq ef1 ef2); inv H. exists (External ef2); split; auto. simpl. rewrite dec_eq_true; auto. +- destruct (external_function_eq ef1 ef2); inv H. exists (External ef2); split; auto. simpl. rewrite dec_eq_true; auto. Qed. Instance TransfPartialContextualLink @@ -697,8 +697,8 @@ Instance TransfPartialContextualLink Proof. red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. eapply link_match_program; eauto. -- intros. eapply link_transf_partial_fundef; eauto. -- intros; subst. exists v; auto. +- intros. eapply link_transf_partial_fundef; eauto. +- intros; subst. exists v; auto. Qed. Instance TransfPartialLink @@ -711,8 +711,8 @@ Instance TransfPartialLink Proof. red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. eapply link_match_program; eauto. -- intros. eapply link_transf_partial_fundef; eauto. -- intros; subst. exists v; auto. +- intros. eapply link_transf_partial_fundef; eauto. +- intros; subst. exists v; auto. Qed. Instance TransfTotallContextualLink @@ -726,12 +726,12 @@ Instance TransfTotallContextualLink Proof. red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. eapply link_match_program; eauto. -- intros. subst. destruct f1, f2; simpl in *. +- intros. subst. destruct f1, f2; simpl in *. + discriminate. -+ destruct e; inv H2. econstructor; eauto. -+ destruct e; inv H2. econstructor; eauto. -+ destruct (external_function_eq e e0); inv H2. econstructor; eauto. -- intros; subst. exists v; auto. ++ destruct e; inv H2. econstructor; eauto. ++ destruct e; inv H2. econstructor; eauto. ++ destruct (external_function_eq e e0); inv H2. econstructor; eauto. +- intros; subst. exists v; auto. Qed. Instance TransfTotalLink @@ -744,12 +744,12 @@ Instance TransfTotalLink Proof. red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. eapply link_match_program; eauto. -- intros. subst. destruct f1, f2; simpl in *. +- intros. subst. destruct f1, f2; simpl in *. + discriminate. -+ destruct e; inv H2. econstructor; eauto. -+ destruct e; inv H2. econstructor; eauto. -+ destruct (external_function_eq e e0); inv H2. econstructor; eauto. -- intros; subst. exists v; auto. ++ destruct e; inv H2. econstructor; eauto. ++ destruct e; inv H2. econstructor; eauto. ++ destruct (external_function_eq e e0); inv H2. econstructor; eauto. +- intros; subst. exists v; auto. Qed. (** * Linking a set of compilation units *) @@ -794,7 +794,7 @@ Theorem link_list_match: exists b, link_list bl = Some b /\ prog_match a b. Proof. induction 1; simpl; intros a' L. -- inv L. exists b; auto. +- inv L. exists b; auto. - destruct (link_list l) as [a1|] eqn:LL; try discriminate. exploit IHnlist_forall2; eauto. intros (b' & P & Q). red in TL. exploit TL; eauto. intros (b'' & U & V). @@ -829,7 +829,7 @@ Program Definition pass_identity (l: Language): Pass l l := {| pass_match := fun p1 p2 => p1 = p2; pass_match_link := _ |}. Next Obligation. - red; intros. subst. exists p; auto. + red; intros. subst. exists p; auto. Defined. Program Definition pass_compose {l1 l2 l3: Language} (pass: Pass l1 l2) (pass': Pass l2 l3) : Pass l1 l3 := @@ -875,7 +875,7 @@ Lemma nlist_forall2_compose_inv: exists lb: nlist B, nlist_forall2 R1 la lb /\ nlist_forall2 R2 lb lc. Proof. induction 1. -- rename b into c. destruct H as (b & P & Q). +- rename b into c. destruct H as (b & P & Q). exists (nbase b); split; constructor; auto. - rename b into c. destruct H as (b & P & Q). destruct IHnlist_forall2 as (lb & U & V). exists (ncons b lb); split; constructor; auto. @@ -898,8 +898,8 @@ Proof. - apply nlist_forall2_compose_inv in F2. destruct F2 as (interm_units & P & Q). edestruct (@link_list_match _ _ (lang_link l1) (lang_link l2) (pass_match p)) as (interm_prog & U & V). - apply pass_match_link. eauto. eauto. + apply pass_match_link. eauto. eauto. exploit IHpasses; eauto. intros (tgt_prog & X & Y). - exists tgt_prog; split; auto. exists interm_prog; auto. + exists tgt_prog; split; auto. exists interm_prog; auto. Qed. diff --git a/common/Memdata.v b/common/Memdata.v index 87547e1e..0aed4644 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -1062,7 +1062,7 @@ Lemma encode_val_int64: encode_val Mint32 (if Archi.big_endian then Val.hiword v else Val.loword v) ++ encode_val Mint32 (if Archi.big_endian then Val.loword v else Val.hiword v). Proof. - intros. unfold encode_val. rewrite H. + intros. unfold encode_val. rewrite H. destruct v; destruct Archi.big_endian eqn:BI; try reflexivity; unfold Val.loword, Val.hiword, encode_val. unfold inj_bytes. rewrite <- map_app. f_equal. diff --git a/common/Memory.v b/common/Memory.v index 764fdc26..8bb69c02 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -912,7 +912,7 @@ Proof. rewrite Ptrofs.add_unsigned. replace (Ptrofs.unsigned (Ptrofs.of_int (Int.repr 4))) with (Int.unsigned (Int.repr 4)) by (symmetry; apply Ptrofs.agree32_of_int; auto). - change (Int.unsigned (Int.repr 4)) with 4. + change (Int.unsigned (Int.repr 4)) with 4. apply Ptrofs.unsigned_repr. exploit (Zdivide_interval (Ptrofs.unsigned i) Ptrofs.modulus 8). omega. apply Ptrofs.unsigned_range. auto. @@ -934,7 +934,7 @@ Proof. exploit load_int64_split; eauto. intros (v1 & v2 & L1 & L2 & EQ). unfold Val.add; rewrite H0. assert (NV: Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4). - { apply addressing_int64_split; auto. + { apply addressing_int64_split; auto. exploit load_valid_access. eexact H2. intros [P Q]. auto. } exists v1, v2. Opaque Ptrofs.repr. @@ -1519,7 +1519,7 @@ Qed. Theorem loadbytes_storebytes_same: loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes. Proof. - intros. assert (STORE2:=STORE). unfold storebytes in STORE2. unfold loadbytes. + intros. assert (STORE2:=STORE). unfold storebytes in STORE2. unfold loadbytes. destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); try discriminate. rewrite pred_dec_true. @@ -1829,7 +1829,7 @@ Proof. intros. exploit load_result; eauto. intro. rewrite H0. injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1. rewrite PMap.gss. destruct (size_chunk_nat_pos chunk) as [n E]. rewrite E. simpl. - rewrite ZMap.gi. apply decode_val_undef. + rewrite ZMap.gi. apply decode_val_undef. Qed. Theorem load_alloc_same': @@ -2930,7 +2930,7 @@ Proof. rewrite (nextblock_store _ _ _ _ _ _ H0). auto. eapply store_outside_inj; eauto. unfold inject_id; intros. inv H2. eapply H1; eauto. omega. - intros. eauto using perm_store_2. + intros. eauto using perm_store_2. Qed. Theorem storev_extends: @@ -2982,7 +2982,7 @@ Proof. rewrite (nextblock_storebytes _ _ _ _ _ H0). auto. eapply storebytes_outside_inj; eauto. unfold inject_id; intros. inv H2. eapply H1; eauto. omega. - intros. eauto using perm_storebytes_2. + intros. eauto using perm_storebytes_2. Qed. Theorem alloc_extends: @@ -3017,7 +3017,7 @@ Proof. intros. eapply perm_alloc_inv in H; eauto. generalize (perm_alloc_inv _ _ _ _ _ H0 b0 ofs Max Nonempty); intros PERM. destruct (eq_block b0 b). - subst b0. + subst b0. assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by omega. destruct EITHER. left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. @@ -3034,7 +3034,7 @@ Proof. intros. inv H. constructor. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_left_inj; eauto. - intros. exploit mext_perm_inv0; eauto. intros [A|A]. + intros. exploit mext_perm_inv0; eauto. intros [A|A]. eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto. subst b0. right; eapply perm_free_2; eauto. intuition eauto using perm_free_3. @@ -3051,7 +3051,7 @@ Proof. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_right_inj; eauto. unfold inject_id; intros. inv H. eapply H1; eauto. omega. - intros. eauto using perm_free_3. + intros. eauto using perm_free_3. Qed. Theorem free_parallel_extends: @@ -3498,7 +3498,7 @@ Proof. intros. eapply mi_representable; try eassumption. destruct H4; eauto with mem. (* perm inv *) - intros. exploit mi_perm_inv0; eauto using perm_store_2. + intros. exploit mi_perm_inv0; eauto using perm_store_2. intuition eauto using perm_store_1, perm_store_2. Qed. @@ -3523,7 +3523,7 @@ Proof. intros. eapply mi_representable; try eassumption. destruct H3; eauto with mem. (* perm inv *) - intros. exploit mi_perm_inv0; eauto using perm_store_2. + intros. exploit mi_perm_inv0; eauto using perm_store_2. intuition eauto using perm_store_1, perm_store_2. Qed. @@ -3594,7 +3594,7 @@ Proof. intros. eapply mi_representable0; eauto. destruct H4; eauto using perm_storebytes_2. (* perm inv *) - intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. + intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. @@ -3668,7 +3668,7 @@ Proof. intros. eapply mi_representable0; eauto. destruct H3; eauto using perm_storebytes_2. (* perm inv *) - intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. + intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. @@ -3694,7 +3694,7 @@ Proof. auto. (* perm inv *) intros. eapply perm_alloc_inv in H2; eauto. destruct (eq_block b0 b2). - subst b0. eelim fresh_block_alloc; eauto. + subst b0. eelim fresh_block_alloc; eauto. eapply mi_perm_inv0; eauto. Qed. @@ -3741,7 +3741,7 @@ Proof. destruct H4; eauto using perm_alloc_4. (* perm inv *) intros. unfold f' in H3; destruct (eq_block b0 b1); try discriminate. - exploit mi_perm_inv0; eauto. + exploit mi_perm_inv0; eauto. intuition eauto using perm_alloc_1, perm_alloc_4. (* incr *) split. auto. @@ -3892,7 +3892,7 @@ Proof. (* perm inv *) intros. exploit mi_perm_inv0; eauto. intuition eauto using perm_free_3. eapply perm_free_inv in H4; eauto. destruct H4 as [[A B] | A]; auto. - subst b1. right; eapply perm_free_2; eauto. + subst b1. right; eapply perm_free_2; eauto. Qed. Lemma free_list_left_inject: @@ -4080,7 +4080,7 @@ Proof. destruct H0; eauto using perm_inj. rewrite H. omega. (* perm inv *) - intros. + intros. destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. destruct (f' b') as [[b'' delta''] |] eqn:?; try discriminate. inversion H; clear H; subst b'' delta. @@ -4163,7 +4163,7 @@ Proof. eapply mem_inj_compose; eauto. apply extensionality; intros. unfold compose_meminj, inject_id. auto. (* perm inv *) - exploit mext_perm_inv1; eauto. intros [A|A]. + exploit mext_perm_inv1; eauto. intros [A|A]. eapply mext_perm_inv0; eauto. right; red; intros; elim A. eapply perm_extends; eauto. Qed. @@ -4305,7 +4305,7 @@ Lemma perm_unchanged_on: unchanged_on m m' -> P b ofs -> perm m b ofs k p -> perm m' b ofs k p. Proof. - intros. destruct H. apply unchanged_on_perm0; auto. eapply perm_valid_block; eauto. + intros. destruct H. apply unchanged_on_perm0; auto. eapply perm_valid_block; eauto. Qed. Lemma perm_unchanged_on_2: @@ -4324,7 +4324,7 @@ Proof. - intros. transitivity (perm m2 b ofs k p); apply unchanged_on_perm; auto. eapply valid_block_unchanged_on; eauto. - intros. transitivity (ZMap.get ofs (mem_contents m2)#b); apply unchanged_on_contents; auto. - eapply perm_unchanged_on; eauto. + eapply perm_unchanged_on; eauto. Qed. Lemma loadbytes_unchanged_on_1: @@ -4462,13 +4462,13 @@ Proof. - rewrite (nextblock_drop _ _ _ _ _ _ H). apply Ple_refl. - split; intros. eapply perm_drop_3; eauto. destruct (eq_block b0 b); auto. - subst b0. + subst b0. assert (~ (lo <= ofs < hi)). { red; intros; eelim H0; eauto. } right; omega. - eapply perm_drop_4; eauto. -- unfold drop_perm in H. + eapply perm_drop_4; eauto. +- unfold drop_perm in H. destruct (range_perm_dec m b lo hi Cur Freeable); inv H; simpl. auto. -Qed. +Qed. End UNCHANGED_ON. @@ -4480,9 +4480,9 @@ Lemma unchanged_on_implies: Proof. intros. destruct H. constructor; intros. - auto. -- apply unchanged_on_perm0; auto. -- apply unchanged_on_contents0; auto. - apply H0; auto. eapply perm_valid_block; eauto. +- apply unchanged_on_perm0; auto. +- apply unchanged_on_contents0; auto. + apply H0; auto. eapply perm_valid_block; eauto. Qed. End Mem. diff --git a/common/Separation.v b/common/Separation.v index c0a3c9cf..c27148aa 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -18,7 +18,7 @@ (** This library defines a number of useful logical assertions about CompCert memory states, such as "block [b] at offset [ofs] contains value [v]". Assertions can be grouped using a separating conjunction - operator in the style of separation logic. + operator in the style of separation logic. Currently, this library is used only in module [Stackingproof] to reason about the shapes of stack frames generated during the @@ -84,7 +84,7 @@ Qed. Remark massert_eqv_trans: forall p q r, massert_eqv p q -> massert_eqv q r -> massert_eqv p r. Proof. - unfold massert_eqv, massert_imp; intros. firstorder auto. + unfold massert_eqv, massert_imp; intros. firstorder auto. Qed. (** Record [massert_eqv] and [massert_imp] as relations so that they can be used by rewriting tactics. *) @@ -139,7 +139,7 @@ Add Morphism sepconj Proof. intros P1 P2 [A B] Q1 Q2 [C D]. red; simpl; split; intros. -- intuition auto. red; intros. apply (H2 b ofs); auto. +- intuition auto. red; intros. apply (H2 b ofs); auto. - intuition auto. Qed. @@ -147,7 +147,7 @@ Add Morphism sepconj with signature massert_eqv ==> massert_eqv ==> massert_eqv as sepconj_morph_2. Proof. - intros. destruct H, H0. split; apply sepconj_morph_1; auto. + intros. destruct H, H0. split; apply sepconj_morph_1; auto. Qed. Infix "**" := sepconj (at level 60, right associativity) : sep_scope. @@ -155,7 +155,7 @@ Infix "**" := sepconj (at level 60, right associativity) : sep_scope. Local Open Scope sep_scope. Lemma sep_imp: - forall P P' Q Q' m, + forall P P' Q Q' m, m |= P ** Q -> massert_imp P P' -> massert_imp Q Q' -> m |= P' ** Q'. Proof. intros. rewrite <- H0, <- H1; auto. @@ -249,7 +249,7 @@ Lemma sep_drop2: forall P Q R m, m |= P ** Q ** R -> m |= P ** R. Proof. intros. rewrite sep_swap in H. eapply sep_drop; eauto. -Qed. +Qed. Lemma sep_proj1: forall Q P m, m |= P ** Q -> m |= P. @@ -263,25 +263,25 @@ Proof sep_drop. Definition sep_pick1 := sep_proj1. -Lemma sep_pick2: +Lemma sep_pick2: forall P Q R m, m |= P ** Q ** R -> m |= Q. Proof. intros. eapply sep_proj1; eapply sep_proj2; eauto. Qed. -Lemma sep_pick3: +Lemma sep_pick3: forall P Q R S m, m |= P ** Q ** R ** S -> m |= R. Proof. intros. eapply sep_pick2; eapply sep_proj2; eauto. Qed. -Lemma sep_pick4: +Lemma sep_pick4: forall P Q R S T m, m |= P ** Q ** R ** S ** T -> m |= S. Proof. intros. eapply sep_pick3; eapply sep_proj2; eauto. Qed. -Lemma sep_pick5: +Lemma sep_pick5: forall P Q R S T U m, m |= P ** Q ** R ** S ** T ** U -> m |= T. Proof. intros. eapply sep_pick4; eapply sep_proj2; eauto. @@ -337,7 +337,7 @@ Lemma alloc_rule: m |= P -> m' |= range b lo hi ** P. Proof. - intros; simpl. split; [|split]. + intros; simpl. split; [|split]. - split; auto. split; auto. intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. @@ -352,7 +352,7 @@ Lemma range_split: m |= range b lo hi ** P -> m |= range b lo mid ** range b mid hi ** P. Proof. - intros. rewrite <- sep_assoc. eapply sep_imp; eauto. + intros. rewrite <- sep_assoc. eapply sep_imp; eauto. split; simpl; intros. - intuition auto. + omega. @@ -425,8 +425,8 @@ Next Obligation. - exists v. split; auto. eapply Mem.load_unchanged_on; eauto. simpl; auto. Qed. Next Obligation. - eauto with mem. -Qed. + eauto with mem. +Qed. Lemma contains_no_overflow: forall spec m chunk b ofs, @@ -466,10 +466,10 @@ Proof. destruct (Mem.valid_access_store _ _ _ _ v H) as [m' STORE]. exists m'; split; auto. simpl. intuition auto. - eapply Mem.store_valid_access_1; eauto. -- exists (Val.load_result chunk v); split; auto. eapply Mem.load_store_same; eauto. -- apply (m_invar P) with m; auto. - eapply Mem.store_unchanged_on; eauto. - intros; red; intros. apply (C b i); simpl; auto. +- exists (Val.load_result chunk v); split; auto. eapply Mem.load_store_same; eauto. +- apply (m_invar P) with m; auto. + eapply Mem.store_unchanged_on; eauto. + intros; red; intros. apply (C b i); simpl; auto. Qed. Lemma storev_rule: @@ -523,7 +523,7 @@ Lemma store_rule': exists m', Mem.store chunk m b ofs v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P. Proof. - intros. eapply store_rule; eauto. + intros. eapply store_rule; eauto. Qed. Lemma storev_rule': @@ -542,7 +542,7 @@ Program Definition mconj (P Q: massert) : massert := {| m_footprint := fun b ofs => m_footprint P b ofs \/ m_footprint Q b ofs |}. Next Obligation. - split. + split. apply (m_invar P) with m; auto. eapply Mem.unchanged_on_implies; eauto. simpl; auto. apply (m_invar Q) with m; auto. eapply Mem.unchanged_on_implies; eauto. simpl; auto. Qed. @@ -586,7 +586,7 @@ Lemma frame_mconj: Proof. intros. destruct H as (A & B & C); simpl in A. destruct H0 as (D & E & F). - simpl. intuition auto. + simpl. intuition auto. red; simpl; intros. destruct H2. eapply F; eauto. eapply C; simpl; eauto. Qed. @@ -602,7 +602,7 @@ Add Morphism mconj with signature massert_eqv ==> massert_eqv ==> massert_eqv as mconj_morph_2. Proof. - intros. destruct H, H0. split; apply mconj_morph_1; auto. + intros. destruct H, H0. split; apply mconj_morph_1; auto. Qed. (** The image of a memory injection *) @@ -615,8 +615,8 @@ Next Obligation. set (img := fun b' ofs => exists b delta, j b = Some(b', delta) /\ Mem.perm m0 b (ofs - delta) Max Nonempty) in *. assert (IMG: forall b1 b2 delta ofs k p, j b1 = Some (b2, delta) -> Mem.perm m0 b1 ofs k p -> img b2 (ofs + delta)). - { intros. red. exists b1, delta; split; auto. - replace (ofs + delta - delta) with ofs by omega. + { intros. red. exists b1, delta; split; auto. + replace (ofs + delta - delta) with ofs by omega. eauto with mem. } destruct H. constructor. - destruct mi_inj. constructor; intros. @@ -624,11 +624,11 @@ Next Obligation. + eauto. + rewrite (Mem.unchanged_on_contents _ _ _ H0); eauto. - assumption. -- intros. eapply Mem.valid_block_unchanged_on; eauto. +- intros. eapply Mem.valid_block_unchanged_on; eauto. - assumption. - assumption. - intros. destruct (Mem.perm_dec m0 b1 ofs Max Nonempty); auto. - eapply mi_perm_inv; eauto. + eapply mi_perm_inv; eauto. eapply Mem.perm_unchanged_on_2; eauto. Qed. Next Obligation. @@ -666,8 +666,8 @@ Proof. - apply (m_invar P) with m2; auto. eapply Mem.store_unchanged_on; eauto. intros; red; intros. eelim C; eauto. simpl. - exists b1, delta; split; auto. destruct VALID as [V1 V2]. - apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. + exists b1, delta; split; auto. destruct VALID as [V1 V2]. + apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. apply V1. omega. - red; simpl; intros. destruct H1 as (b0 & delta0 & U & V). eelim C; eauto. simpl. exists b0, delta0; eauto with mem. @@ -695,41 +695,41 @@ Proof. assert (FRESH2: ~Mem.valid_block m2 b2) by (eapply Mem.fresh_block_alloc; eauto). destruct SEP as (INJ & SP & DISJ). simpl in INJ. exploit Mem.alloc_left_mapped_inject. -- eapply Mem.alloc_right_inject; eauto. +- eapply Mem.alloc_right_inject; eauto. - eexact ALLOC1. - instantiate (1 := b2). eauto with mem. - instantiate (1 := delta). xomega. - intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). omega. -- intros. apply Mem.perm_implies with Freeable; auto with mem. +- intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. xomega. -- red; intros. apply Zdivides_trans with 8; auto. +- red; intros. apply Zdivides_trans with 8; auto. exists (8 / align_chunk chunk). destruct chunk; reflexivity. -- intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. +- intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. - intros (j' & INJ' & J1 & J2 & J3). exists j'; split; auto. rewrite <- ! sep_assoc. split; [|split]. + simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; omega). * apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. omega. + eapply Mem.perm_alloc_2; eauto. omega. * apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. omega. + eapply Mem.perm_alloc_2; eauto. omega. * red; simpl; intros. destruct H1, H2. omega. * red; simpl; intros. assert (b = b2) by tauto. subst b. assert (0 <= ofs < lo \/ hi <= ofs < sz2) by tauto. clear H1. destruct H2 as (b0 & delta0 & D & E). - eapply Mem.perm_alloc_inv in E; eauto. + eapply Mem.perm_alloc_inv in E; eauto. destruct (eq_block b0 b1). subst b0. rewrite J2 in D. inversion D; clear D; subst delta0. xomega. - rewrite J3 in D by auto. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. -+ apply (m_invar P) with m2; auto. eapply Mem.alloc_unchanged_on; eauto. + rewrite J3 in D by auto. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. ++ apply (m_invar P) with m2; auto. eapply Mem.alloc_unchanged_on; eauto. + red; simpl; intros. assert (VALID: Mem.valid_block m2 b) by (eapply (m_valid P); eauto). destruct H as [A | (b0 & delta0 & A & B)]. * assert (b = b2) by tauto. subst b. contradiction. -* eelim DISJ; eauto. simpl. - eapply Mem.perm_alloc_inv in B; eauto. +* eelim DISJ; eauto. simpl. + eapply Mem.perm_alloc_inv in B; eauto. destruct (eq_block b0 b1). subst b0. rewrite J2 in A. inversion A; clear A; subst b delta0. contradiction. rewrite J3 in A by auto. exists b0, delta0; auto. @@ -745,19 +745,19 @@ Lemma free_parallel_rule: Mem.free m2 b2 0 sz2 = Some m2' /\ m2' |= minjection j m1' ** P. Proof. - intros. rewrite <- ! sep_assoc in H. + intros. rewrite <- ! sep_assoc in H. destruct H as (A & B & C). destruct A as (D & E & F). destruct D as (J & K & L). destruct J as (_ & _ & J). destruct K as (_ & _ & K). simpl in E. assert (PERM: Mem.range_perm m2 b2 0 sz2 Cur Freeable). - { red; intros. + { red; intros. destruct (zlt ofs lo). apply J; omega. destruct (zle hi ofs). apply K; omega. replace ofs with ((ofs - delta) + delta) by omega. - eapply Mem.perm_inject; eauto. - eapply Mem.free_range_perm; eauto. xomega. + eapply Mem.perm_inject; eauto. + eapply Mem.free_range_perm; eauto. xomega. } destruct (Mem.range_perm_free _ _ _ _ PERM) as [m2' FREE]. exists m2'; split; auto. split; [|split]. @@ -765,33 +765,33 @@ Proof. intros. apply (F b2 (ofs + delta0)). + simpl. destruct (zlt (ofs + delta0) lo). intuition auto. - destruct (zle hi (ofs + delta0)). intuition auto. + destruct (zle hi (ofs + delta0)). intuition auto. destruct (eq_block b0 b1). * subst b0. rewrite H1 in H; inversion H; clear H; subst delta0. eelim (Mem.perm_free_2 m1); eauto. xomega. -* exploit Mem.mi_no_overlap; eauto. - apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. +* exploit Mem.mi_no_overlap; eauto. + apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. eapply Mem.perm_free_3; eauto. - apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - eapply (Mem.free_range_perm m1); eauto. - instantiate (1 := ofs + delta0 - delta). xomega. - intros [X|X]. congruence. omega. -+ simpl. exists b0, delta0; split; auto. + apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. + eapply (Mem.free_range_perm m1); eauto. + instantiate (1 := ofs + delta0 - delta). xomega. + intros [X|X]. congruence. omega. ++ simpl. exists b0, delta0; split; auto. replace (ofs + delta0 - delta0) with ofs by omega. - apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. + apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. eapply Mem.perm_free_3; eauto. -- apply (m_invar P) with m2; auto. - eapply Mem.free_unchanged_on; eauto. - intros; red; intros. eelim C; eauto. simpl. +- apply (m_invar P) with m2; auto. + eapply Mem.free_unchanged_on; eauto. + intros; red; intros. eelim C; eauto. simpl. destruct (zlt i lo). intuition auto. destruct (zle hi i). intuition auto. - right; exists b1, delta; split; auto. + right; exists b1, delta; split; auto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.free_range_perm; eauto. xomega. -- red; simpl; intros. eelim C; eauto. - simpl. right. destruct H as (b0 & delta0 & U & V). - exists b0, delta0; split; auto. - eapply Mem.perm_free_3; eauto. + eapply Mem.free_range_perm; eauto. xomega. +- red; simpl; intros. eelim C; eauto. + simpl. right. destruct H as (b0 & delta0 & U & V). + exists b0, delta0; split; auto. + eapply Mem.perm_free_3; eauto. Qed. (** Preservation of a global environment by a memory injection *) @@ -836,7 +836,7 @@ Lemma globalenv_inject_incr: Proof. intros. destruct H1 as (A & B & C). destruct A as (bound & D & E). split; [|split]; auto. - exists bound; split; auto. + exists bound; split; auto. inv E; constructor; intros. - eauto. - destruct (j b1) as [[b0 delta0]|] eqn:JB1. @@ -860,7 +860,7 @@ Lemma external_call_parallel_rule: /\ inject_separated j j' m1 m2. Proof. intros until vargs2; intros CALL SEP ARGS. - destruct SEP as (A & B & C). simpl in A. + destruct SEP as (A & B & C). simpl in A. exploit external_call_mem_inject; eauto. eapply globalenv_inject_preserves_globals. eapply sep_pick1; eauto. intros (j' & vres2 & m2' & CALL' & RES & INJ' & UNCH1 & UNCH2 & INCR & ISEP). @@ -877,11 +877,11 @@ Proof. eelim C; eauto. simpl. exists b0, delta; auto. - red; intros. destruct H as (b0 & delta & J' & E). destruct (j b0) as [[b' delta'] | ] eqn:J. -+ erewrite INCR in J' by eauto. inv J'. - eelim C; eauto. simpl. exists b0, delta; split; auto. apply MAXPERMS; auto. ++ erewrite INCR in J' by eauto. inv J'. + eelim C; eauto. simpl. exists b0, delta; split; auto. apply MAXPERMS; auto. eapply Mem.valid_block_inject_1; eauto. + exploit ISEP; eauto. intros (X & Y). elim Y. eapply m_valid; eauto. -Qed. +Qed. Lemma alloc_parallel_rule_2: forall (F V: Type) (ge: Genv.t F V) m1 sz1 m1' b1 m2 sz2 m2' b2 P j lo hi delta, @@ -898,19 +898,19 @@ Lemma alloc_parallel_rule_2: /\ inject_incr j j' /\ j' b1 = Some(b2, delta). Proof. - intros. + intros. set (j1 := fun b => if eq_block b b1 then Some(b2, delta) else j b). assert (X: inject_incr j j1). - { unfold j1; red; intros. destruct (eq_block b b1); auto. - subst b. eelim Mem.fresh_block_alloc. eexact H0. + { unfold j1; red; intros. destruct (eq_block b b1); auto. + subst b. eelim Mem.fresh_block_alloc. eexact H0. eapply Mem.valid_block_inject_1. eauto. apply sep_proj1 in H. eexact H. } assert (Y: inject_separated j j1 m1 m2). - { unfold j1; red; intros. destruct (eq_block b0 b1). + { unfold j1; red; intros. destruct (eq_block b0 b1). - inversion H9; clear H9; subst b3 delta0 b0. split; eapply Mem.fresh_block_alloc; eauto. - congruence. } rewrite sep_swap in H. eapply globalenv_inject_incr with (j' := j1) in H; eauto. rewrite sep_swap in H. clear X Y. - exploit alloc_parallel_rule; eauto. + exploit alloc_parallel_rule; eauto. intros (j' & A & B & C & D). exists j'; split; auto. rewrite sep_swap4 in A. rewrite sep_swap4. apply globalenv_inject_incr with j1 m1; auto. diff --git a/common/Smallstep.v b/common/Smallstep.v index 9c91243a..c269013b 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -786,7 +786,7 @@ End SIMULATION_SEQUENCES. Lemma compose_forward_simulations: forall L1 L2 L3, forward_simulation L1 L2 -> forward_simulation L2 L3 -> forward_simulation L1 L3. Proof. - intros L1 L2 L3 S12 S23. + intros L1 L2 L3 S12 S23. destruct S12 as [index order match_states props]. destruct S23 as [index' order' match_states' props']. @@ -1632,7 +1632,7 @@ Theorem factor_forward_simulation: forward_simulation L1 L2 -> single_events L2 -> forward_simulation (atomic L1) L2. Proof. - intros L1 L2 FS L2single. + intros L1 L2 FS L2single. destruct FS as [index order match_states sim]. apply Forward_simulation with order (ffs_match L1 L2 match_states); constructor. - (* wf *) @@ -1727,7 +1727,7 @@ Theorem factor_backward_simulation: backward_simulation L1 L2 -> single_events L1 -> well_behaved_traces L2 -> backward_simulation L1 (atomic L2). Proof. - intros L1 L2 BS L1single L2wb. + intros L1 L2 BS L1single L2wb. destruct BS as [index order match_states sim]. apply Backward_simulation with order (fbs_match L1 L2 match_states); constructor. - (* wf *) diff --git a/common/Values.v b/common/Values.v index cfabb7a5..d086c69f 100644 --- a/common/Values.v +++ b/common/Values.v @@ -16,7 +16,6 @@ (** This module defines the type of values that is used in the dynamic semantics of all our intermediate languages. *) -Require Archi. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -668,6 +667,12 @@ Definition modlu (v1 v2: val): option val := | _, _ => None end. +Definition addl_carry (v1 v2 cin: val): val := + match v1, v2, cin with + | Vlong n1, Vlong n2, Vlong c => Vlong(Int64.add_carry n1 n2 c) + | _, _, _ => Vundef + end. + Definition subl_overflow (v1 v2: val) : val := match v1, v2 with | Vlong n1, Vlong n2 => Vint (Int.repr (Int64.unsigned (Int64.sub_overflow n1 n2 Int64.zero))) @@ -734,6 +739,15 @@ Definition shrxl (v1 v2: val): option val := | _, _ => None end. +Definition shrl_carry (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vint n2 => + if Int.ltu n2 Int64.iwordsize' + then Vlong(Int64.shr_carry' n1 n2) + else Vundef + | _, _ => Vundef + end. + Definition roll (v1 v2: val): val := match v1, v2 with | Vlong n1, Vint n2 => Vlong(Int64.rol n1 (Int64.repr (Int.unsigned n2))) @@ -746,9 +760,9 @@ Definition rorl (v1 v2: val): val := | _, _ => Vundef end. -Definition rolml (v: val) (amount mask: int64): val := +Definition rolml (v: val) (amount: int) (mask: int64): val := match v with - | Vlong n => Vlong(Int64.rolm n amount mask) + | Vlong n => Vlong(Int64.rolm n (Int64.repr (Int.unsigned amount)) mask) | _ => Vundef end. @@ -1073,7 +1087,7 @@ Proof. symmetry. auto with ptrofs. symmetry. rewrite Int.add_commut. auto with ptrofs. - destruct (eq_block b b0); auto. - f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs. + f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs. Qed. Theorem mul_commut: forall x y, mul x y = mul y x. @@ -1133,6 +1147,28 @@ Proof. generalize (Int.eq_spec i0 Int.zero). rewrite Heqb; auto. Qed. +Theorem modls_divls: + forall x y z, + modls x y = Some z -> exists v, divls x y = Some v /\ z = subl x (mull v y). +Proof. + intros. destruct x; destruct y; simpl in *; try discriminate. + destruct (Int64.eq i0 Int64.zero + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H. + exists (Vlong (Int64.divs i i0)); split; auto. + simpl. rewrite Int64.mods_divs. auto. +Qed. + +Theorem modlu_divlu: + forall x y z, + modlu x y = Some z -> exists v, divlu x y = Some v /\ z = subl x (mull v y). +Proof. + intros. destruct x; destruct y; simpl in *; try discriminate. + destruct (Int64.eq i0 Int64.zero) eqn:?; inv H. + exists (Vlong (Int64.divu i i0)); split; auto. + simpl. rewrite Int64.modu_divu. auto. + generalize (Int64.eq_spec i0 Int64.zero). rewrite Heqb; auto. +Qed. + Theorem divs_pow2: forall x n logn y, Int.is_power2 n = Some logn -> Int.ltu logn (Int.repr 31) = true -> @@ -1282,7 +1318,7 @@ Proof. symmetry; apply zlt_true. change (Int.unsigned n < 32); omega. symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32. assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } - rewrite Int.unsigned_repr. + rewrite Int.unsigned_repr. change (Int.unsigned Int.iwordsize) with 32; omega. assert (32 < Int.max_unsigned) by reflexivity. omega. Qed. @@ -1384,7 +1420,7 @@ Proof. symmetry. auto with ptrofs. symmetry. rewrite Int64.add_commut. auto with ptrofs. - destruct (eq_block b b0); auto. - simpl; f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs. + simpl; f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs. - rewrite Int64.add_commut. rewrite Int64.sub_add_r. auto. Qed. @@ -1462,7 +1498,7 @@ Proof. || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n Int64.mone); inv H3. simpl. rewrite H0. decEq. decEq. generalize (Int64.is_power2'_correct _ _ H); intro. - unfold Int64.shrx'. rewrite Int64.shl'_mul_two_p. rewrite <- H1. + unfold Int64.shrx'. rewrite Int64.shl'_mul_two_p. rewrite <- H1. rewrite Int64.mul_commut. rewrite Int64.mul_one. rewrite Int64.repr_unsigned. auto. Qed. @@ -1491,6 +1527,19 @@ Proof. simpl. decEq. symmetry. eapply Int64.modu_and; eauto. Qed. +Theorem shrxl_carry: + forall x y z, + shrxl x y = Some z -> + addl (shrl x y) (shrl_carry x y) = z. +Proof. + intros. destruct x; destruct y; simpl in H; inv H. + destruct (Int.ltu i0 (Int.repr 63)) eqn:?; inv H1. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63. intros. + assert (Int.ltu i0 Int64.iwordsize' = true). + unfold Int.ltu. apply zlt_true. change (Int.unsigned Int64.iwordsize') with 64. omega. + simpl. rewrite H0. simpl. decEq. rewrite Int64.shrx'_carry; auto. +Qed. + Theorem shrxl_shrl_2: forall n x z, shrxl x (Vint n) = Some z -> @@ -1511,7 +1560,7 @@ Proof. symmetry; apply zlt_true. change (Int.unsigned n < 64); omega. symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64. assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } - rewrite Int.unsigned_repr. + rewrite Int.unsigned_repr. change (Int.unsigned Int64.iwordsize') with 64; omega. assert (64 < Int.max_unsigned) by reflexivity. omega. Qed. @@ -1603,7 +1652,7 @@ Theorem swap_cmpu_bool: Proof. assert (E: forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c). { destruct c; auto. } - intros; unfold cmpu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto. + intros; unfold cmpu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto. - rewrite Int.swap_cmpu. auto. - rewrite Int.swap_cmpu. auto. - destruct (eq_block b b0); subst. @@ -1630,7 +1679,7 @@ Theorem swap_cmplu_bool: Proof. assert (E: forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c). { destruct c; auto. } - intros; unfold cmplu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto. + intros; unfold cmplu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto. - rewrite Int64.swap_cmpu. auto. - destruct (eq_block b b0); subst. rewrite dec_eq_true. @@ -1937,7 +1986,7 @@ Qed. Lemma offset_ptr_assoc: forall v d1 d2, offset_ptr (offset_ptr v d1) d2 = offset_ptr v (Ptrofs.add d1 d2). Proof. - intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc. + intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc. Qed. (** * Values and memory injections *) @@ -1988,7 +2037,7 @@ Hint Resolve inject_list_nil inject_list_cons. Lemma inject_ptrofs: forall mi i, inject mi (Vptrofs i) (Vptrofs i). Proof. - unfold Vptrofs; intros. destruct Archi.ptr64; auto. + unfold Vptrofs; intros. destruct Archi.ptr64; auto. Qed. Hint Resolve inject_ptrofs. @@ -2002,7 +2051,7 @@ Lemma load_result_inject: inject f v1 v2 -> inject f (Val.load_result chunk v1) (Val.load_result chunk v2). Proof. - intros. inv H; destruct chunk; simpl; try constructor; destruct Archi.ptr64; econstructor; eauto. + intros. inv H; destruct chunk; simpl; try constructor; destruct Archi.ptr64; econstructor; eauto. Qed. Remark add_inject: @@ -2012,11 +2061,11 @@ Remark add_inject: inject f (Val.add v1 v2) (Val.add v1' v2'). Proof. intros. unfold Val.add. destruct Archi.ptr64 eqn:SF. -- inv H; inv H0; constructor. +- inv H; inv H0; constructor. - inv H; inv H0; simpl; auto. -+ econstructor; eauto. ++ econstructor; eauto. rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. -+ econstructor; eauto. ++ econstructor; eauto. rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. Qed. @@ -2029,7 +2078,7 @@ Proof. intros. unfold Val.sub. destruct Archi.ptr64 eqn:SF. - inv H; inv H0; constructor. - inv H; inv H0; simpl; auto. -+ econstructor; eauto. ++ econstructor; eauto. rewrite Ptrofs.sub_add_l. auto. + destruct (eq_block b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite dec_eq_true. @@ -2044,11 +2093,11 @@ Remark addl_inject: Proof. intros. unfold Val.addl. destruct Archi.ptr64 eqn:SF. - inv H; inv H0; simpl; auto. -+ econstructor; eauto. ++ econstructor; eauto. rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. -+ econstructor; eauto. ++ econstructor; eauto. rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. -- inv H; inv H0; constructor. +- inv H; inv H0; constructor. Qed. Remark subl_inject: @@ -2059,7 +2108,7 @@ Remark subl_inject: Proof. intros. unfold Val.subl. destruct Archi.ptr64 eqn:SF. - inv H; inv H0; simpl; auto. -+ econstructor; eauto. ++ econstructor; eauto. rewrite Ptrofs.sub_add_l. auto. + destruct (eq_block b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite dec_eq_true. @@ -2126,7 +2175,7 @@ Lemma cmpu_bool_inject: Proof. Local Opaque Int.add Ptrofs.add. intros. - unfold cmpu_bool in *; destruct Archi.ptr64; + unfold cmpu_bool in *; destruct Archi.ptr64; inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. - fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1. fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))). |