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 From 14f89bf9c397a4268d2b47418de234992b008d6c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Sun, 29 Mar 2020 11:35:58 +0200 Subject: Explicit error messages for ill-formed section attributes (#232) Introduce an error message for section attributes with non string arguments,and another for multiple, ambiguous section attributes. This is more consistent with the handling of other attributes, like packed, than the old behavior of silently ignoring them. --- common/Sections.ml | 29 +++++++++++++++++++++-------- common/Sections.mli | 4 ++-- 2 files changed, 23 insertions(+), 10 deletions(-) (limited to 'common') diff --git a/common/Sections.ml b/common/Sections.ml index 30be9e69..839128a5 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -160,9 +160,22 @@ let gcc_section name readonly exec = sec_writable = not readonly; sec_executable = exec; sec_access = Access_default } +(* Check and extract whether a section was given as attribute *) + +let get_attr_section loc attr = + match Cutil.find_custom_attributes ["section"; "__section__"] attr with + | [] -> None + | [[C.AString name]] -> Some name + | [[_]] -> + Diagnostics.error loc "'section' attribute requires a string"; + None + | _ -> + Diagnostics.error loc "ambiguous 'section' attribute"; + None + (* Determine section for a variable definition *) -let for_variable env id ty init = +let for_variable env loc id ty init = let attr = Cutil.attributes_of_type env ty in let readonly = List.mem C.AConst attr && not(List.mem C.AVolatile attr) in let si = @@ -170,11 +183,11 @@ let for_variable env id ty init = (* 1- Section explicitly associated with #use_section *) Hashtbl.find use_section_table id with Not_found -> - match Cutil.find_custom_attributes ["section"; "__section__"] attr with - | [[C.AString name]] -> + match get_attr_section loc attr with + | Some name -> (* 2- Section given as an attribute, gcc-style *) gcc_section name readonly false - | _ -> + | None -> (* 3- Default section appropriate for size and const-ness *) let size = match Cutil.sizeof env ty with Some sz -> sz | None -> max_int in @@ -190,17 +203,17 @@ let for_variable env id ty init = (* Determine sections for a function definition *) -let for_function env id attr = +let for_function env loc id attr = let si_code = try (* 1- Section explicitly associated with #use_section *) Hashtbl.find use_section_table id with Not_found -> - match Cutil.find_custom_attributes ["section"; "__section__"] attr with - | [[C.AString name]] -> + match get_attr_section loc attr with + | Some name -> (* 2- Section given as an attribute, gcc-style *) gcc_section name true true - | _ -> + | None -> (* 3- Default section *) try Hashtbl.find current_section_table "CODE" diff --git a/common/Sections.mli b/common/Sections.mli index bc97814d..d9fd9239 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -46,7 +46,7 @@ val define_section: -> ?writable:bool -> ?executable:bool -> ?access:access_mode -> unit -> unit val use_section_for: AST.ident -> string -> bool -val for_variable: Env.t -> AST.ident -> C.typ -> bool -> +val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> bool -> section_name * access_mode -val for_function: Env.t -> AST.ident -> C.attributes -> section_name list +val for_function: Env.t -> C.location -> AST.ident -> C.attributes -> section_name list val for_stringlit: unit -> section_name -- cgit