From 8587b8310a91702e2635a689e1622a87b7bf8985 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 2 Mar 2020 10:32:07 +0100 Subject: Weaker ec_readonly condition over external calls (#225) Currently we require the memory to be unchanged on readonly locations. This is too strong. For example, current permissions could decrease from readonly to none. This commit weakens the ec_readonly condition to the strict minimum needed to show the correctness of value analysis for const globals. --- common/Events.v | 48 +++++++++++++++++++++++++++++++++--------------- 1 file changed, 33 insertions(+), 15 deletions(-) (limited to 'common') diff --git a/common/Events.v b/common/Events.v index 10e0c232..4431b0b7 100644 --- a/common/Events.v +++ b/common/Events.v @@ -649,9 +649,12 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := (** External call cannot modify memory unless they have [Max, Writable] permissions. *) ec_readonly: - forall ge vargs m1 t vres m2, + forall ge vargs m1 t vres m2 b ofs n bytes, sem ge vargs m1 t vres m2 -> - Mem.unchanged_on (loc_not_writable m1) m1 m2; + Mem.valid_block m1 b -> + Mem.loadbytes m2 b ofs n = Some bytes -> + (forall i, ofs <= i < ofs + n -> ~Mem.perm m1 b i Max Writable) -> + Mem.loadbytes m1 b ofs n = Some bytes; (** External calls must commute with memory extensions, in the following sense. *) @@ -784,7 +787,7 @@ Proof. (* max perms *) - inv H; auto. (* readonly *) -- inv H. apply Mem.unchanged_on_refl. +- inv H; auto. (* mem extends *) - inv H. inv H1. inv H6. inv H4. exploit volatile_load_extends; eauto. intros [v' [A B]]. @@ -833,14 +836,27 @@ Proof. rewrite C; auto. Qed. +Lemma unchanged_on_readonly: + forall m1 m2 b ofs n bytes, + Mem.unchanged_on (loc_not_writable m1) m1 m2 -> + Mem.valid_block m1 b -> + Mem.loadbytes m2 b ofs n = Some bytes -> + (forall i, ofs <= i < ofs + n -> ~Mem.perm m1 b i Max Writable) -> + Mem.loadbytes m1 b ofs n = Some bytes. +Proof. + intros. + rewrite <- H1. symmetry. + apply Mem.loadbytes_unchanged_on_1 with (P := loc_not_writable m1); auto. +Qed. + Lemma volatile_store_readonly: forall ge chunk1 m1 b1 ofs1 v t m2, volatile_store ge chunk1 m1 b1 ofs1 v t m2 -> Mem.unchanged_on (loc_not_writable m1) m1 m2. Proof. intros. inv H. - apply Mem.unchanged_on_refl. - eapply Mem.store_unchanged_on; eauto. +- apply Mem.unchanged_on_refl. +- eapply Mem.store_unchanged_on; eauto. exploit Mem.store_valid_access_3; eauto. intros [P Q]. intros. unfold loc_not_writable. red; intros. elim H2. apply Mem.perm_cur_max. apply P. auto. @@ -934,7 +950,7 @@ Proof. (* perms *) - inv H. inv H2. auto. eauto with mem. (* readonly *) -- inv H. eapply volatile_store_readonly; eauto. +- inv H. eapply unchanged_on_readonly; eauto. eapply volatile_store_readonly; eauto. (* mem extends*) - inv H. inv H1. inv H6. inv H7. inv H4. exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. @@ -994,7 +1010,7 @@ Proof. rewrite dec_eq_false. auto. apply Mem.valid_not_valid_diff with m1; eauto with mem. (* readonly *) -- inv H. eapply UNCHANGED; eauto. +- inv H. eapply unchanged_on_readonly; eauto. (* mem extends *) - inv H. inv H1. inv H7. assert (SZ: v2 = Vptrofs sz). @@ -1065,8 +1081,9 @@ Proof. (* perms *) - inv H. eapply Mem.perm_free_3; eauto. (* readonly *) -- inv H. eapply Mem.free_unchanged_on; eauto. - intros. red; intros. elim H3. +- inv H. eapply unchanged_on_readonly; eauto. + eapply Mem.free_unchanged_on; eauto. + intros. red; intros. elim H6. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.free_range_perm; eauto. (* mem extends *) @@ -1159,8 +1176,9 @@ Proof. - (* perms *) intros. inv H. eapply Mem.perm_storebytes_2; eauto. - (* readonly *) - intros. inv H. eapply Mem.storebytes_unchanged_on; eauto. - intros; red; intros. elim H8. + intros. inv H. eapply unchanged_on_readonly; eauto. + eapply Mem.storebytes_unchanged_on; eauto. + intros; red; intros. elim H11. apply Mem.perm_cur_max. eapply Mem.storebytes_range_perm; eauto. - (* extensions *) intros. inv H. @@ -1271,7 +1289,7 @@ Proof. (* perms *) - inv H; auto. (* readonly *) -- inv H. apply Mem.unchanged_on_refl. +- inv H; auto. (* mem extends *) - inv H. exists Vundef; exists m1'; intuition. @@ -1316,7 +1334,7 @@ Proof. (* perms *) - inv H; auto. (* readonly *) -- inv H. apply Mem.unchanged_on_refl. +- inv H; auto. (* mem extends *) - inv H. inv H1. inv H6. exists v2; exists m1'; intuition. @@ -1359,7 +1377,7 @@ Proof. (* perms *) - inv H; auto. (* readonly *) -- inv H. apply Mem.unchanged_on_refl. +- inv H; auto. (* mem extends *) - inv H. exists Vundef; exists m1'; intuition. @@ -1406,7 +1424,7 @@ Proof. (* perms *) - inv H; auto. (* readonly *) -- inv H. apply Mem.unchanged_on_refl. +- inv H; auto. (* mem extends *) - inv H. fold bsem in H2. apply val_inject_list_lessdef in H1. specialize (bs_inject _ bsem _ _ _ H1). -- cgit From f8d3d265f6ef967acf6eea017cb472809096a135 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 2 Mar 2020 10:41:11 +0100 Subject: Define the semantics of `free(NULL)` (#226) According to ISO C, `free(NULL)` is correct and does nothing. This commit updates accordingly the formal semantics of the `free` external function and the reference interpreter. Closes: #334 --- common/Events.v | 44 ++++++++++++++++++++++++++++++-------------- 1 file changed, 30 insertions(+), 14 deletions(-) (limited to 'common') diff --git a/common/Events.v b/common/Events.v index 4431b0b7..022adaef 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1061,11 +1061,13 @@ Qed. Inductive extcall_free_sem (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := - | extcall_free_sem_intro: forall b lo sz m m', + | extcall_free_sem_ptr: forall b lo sz m m', Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr) = Some (Vptrofs sz) -> Ptrofs.unsigned sz > 0 -> Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) = Some m' -> - extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'. + extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m' + | extcall_free_sem_null: forall m, + extcall_free_sem ge (Vnullptr :: nil) m E0 Vundef m. Lemma extcall_free_ok: extcall_properties extcall_free_sem @@ -1073,27 +1075,29 @@ Lemma extcall_free_ok: Proof. constructor; intros. (* well typed *) -- inv H. simpl. auto. +- inv H; simpl; auto. (* symbols preserved *) - inv H0; econstructor; eauto. (* valid block *) -- inv H. eauto with mem. +- inv H; eauto with mem. (* perms *) -- inv H. eapply Mem.perm_free_3; eauto. +- inv H; eauto using Mem.perm_free_3. (* readonly *) -- inv H. eapply unchanged_on_readonly; eauto. - eapply Mem.free_unchanged_on; eauto. +- eapply unchanged_on_readonly; eauto. inv H. ++ eapply Mem.free_unchanged_on; eauto. intros. red; intros. elim H6. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.free_range_perm; eauto. ++ apply Mem.unchanged_on_refl. (* mem extends *) -- inv H. inv H1. inv H8. inv H6. +- inv H. ++ inv H1. inv H8. inv H6. exploit Mem.load_extends; eauto. intros [v' [A B]]. assert (v' = Vptrofs sz). { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. } subst v'. exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]]. - exists Vundef; exists m2'; intuition. + exists Vundef; exists m2'; intuition auto. econstructor; eauto. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_bounds; intros. @@ -1101,8 +1105,14 @@ Proof. { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.free_range_perm. eexact H4. eauto. } tauto. ++ inv H1. inv H5. replace v2 with Vnullptr. + exists Vundef; exists m1'; intuition auto. + constructor. + apply Mem.unchanged_on_refl. + unfold Vnullptr in *; destruct Archi.ptr64; inv H3; auto. (* mem inject *) -- inv H0. inv H2. inv H7. inv H9. +- inv H0. ++ inv H2. inv H7. inv H9. exploit Mem.load_inject; eauto. intros [v' [A B]]. assert (v' = Vptrofs sz). { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. } @@ -1116,7 +1126,7 @@ Proof. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). exists f, Vundef, m2'; split. - apply extcall_free_sem_intro with (sz := sz) (m' := m2'). + apply extcall_free_sem_ptr with (sz := sz) (m' := m2'). rewrite EQ. rewrite <- A. f_equal. omega. auto. auto. rewrite ! EQ. rewrite <- C. f_equal; omega. @@ -1129,14 +1139,19 @@ Proof. apply P. omega. split. auto. red; intros. congruence. ++ inv H2. inv H6. replace v' with Vnullptr. + exists f, Vundef, m1'; intuition auto using Mem.unchanged_on_refl. + constructor. + red; intros; congruence. + unfold Vnullptr in *; destruct Archi.ptr64; inv H4; auto. (* trace length *) - inv H; simpl; omega. (* receptive *) -- assert (t1 = t2). inv H; inv H0; auto. subst t2. +- assert (t1 = t2) by (inv H; inv H0; auto). subst t2. exists vres1; exists m1; auto. (* determ *) -- inv H; inv H0. - assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence. +- inv H; inv H0; try (unfold Vnullptr in *; discriminate). ++ assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence. assert (EQ2: sz0 = sz). { unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF. rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence. @@ -1144,6 +1159,7 @@ Proof. } subst sz0. split. constructor. intuition congruence. ++ split. constructor. intuition auto. Qed. (** ** Semantics of [memcpy] operations. *) -- cgit From 94558ecb3e48261f12c644045d40c7d0784415e0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 2 Mar 2020 11:39:06 +0100 Subject: Define the semantics of `free(NULL)`, continued The proof script for Events.excall_free_ok was incomplete if Archi.ptr64 is unknown (as in the RISC-V case). --- common/Events.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'common') diff --git a/common/Events.v b/common/Events.v index 022adaef..28bb992a 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1150,7 +1150,7 @@ Proof. - assert (t1 = t2) by (inv H; inv H0; auto). subst t2. exists vres1; exists m1; auto. (* determ *) -- inv H; inv H0; try (unfold Vnullptr in *; discriminate). +- inv H; inv H0; try (unfold Vnullptr in *; destruct Archi.ptr64; discriminate). + assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence. assert (EQ2: sz0 = sz). { unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF. -- cgit From 6af8f4275f7f9572d4d0783818cbfb85357807c6 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Mar 2020 13:17:54 +0100 Subject: loadv_storev_same --- common/Memory.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'common') diff --git a/common/Memory.v b/common/Memory.v index b68a5049..89b920b3 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -1169,6 +1169,24 @@ Local Hint Resolve store_valid_block_1 store_valid_block_2: mem. Local Hint Resolve store_valid_access_1 store_valid_access_2 store_valid_access_3: mem. + +Section STOREV. +Variable chunk: memory_chunk. +Variable m1: mem. +Variables addr v: val. +Variable m2: mem. +Hypothesis STORE: storev chunk m1 addr v = Some m2. + + +Theorem loadv_storev_same: + loadv chunk m2 addr = Some (Val.load_result chunk v). +Proof. + destruct addr; simpl in *; try discriminate. + eapply load_store_same. + eassumption. +Qed. +End STOREV. + Lemma load_store_overlap: forall chunk m1 b ofs v m2 chunk' ofs' v', store chunk m1 b ofs v = Some m2 -> -- cgit From 74efac13484e4767f793cf9ccc94835825ca30ba Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 12:27:58 +0100 Subject: CSE2 alias analysis for Risc-V --- common/Memdata.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'common') diff --git a/common/Memdata.v b/common/Memdata.v index f3016efe..a09b90f5 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -44,6 +44,13 @@ Definition size_chunk (chunk: memory_chunk) : Z := | Many64 => 8 end. +Definition largest_size_chunk := 8. + +Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8. +Proof. + destruct chunk; simpl; omega. +Qed. + Lemma size_chunk_pos: forall chunk, size_chunk chunk > 0. Proof. -- cgit