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 --- cfrontend/Cexec.v | 73 +++++++++++++++++++++++++++++++++---------------------- common/Events.v | 44 ++++++++++++++++++++++----------- 2 files changed, 74 insertions(+), 43 deletions(-) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 2942080b..b08c3ad7 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -460,6 +460,14 @@ Definition do_ef_free check (zlt 0 (Ptrofs.unsigned sz)); do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz); Some(w, E0, Vundef, m') + | Vint n :: nil => + if Int.eq_dec n Int.zero && negb Archi.ptr64 + then Some(w, E0, Vundef, m) + else None + | Vlong n :: nil => + if Int64.eq_dec n Int64.zero && Archi.ptr64 + then Some(w, E0, Vundef, m) + else None | _ => None end. @@ -544,45 +552,51 @@ Proof with try congruence. - eapply do_external_function_sound; eauto. } destruct ef; simpl. -(* EF_external *) +- (* EF_external *) eapply do_external_function_sound; eauto. -(* EF_builtin *) +- (* EF_builtin *) eapply BF_EX; eauto. -(* EF_runtime *) +- (* EF_runtime *) eapply BF_EX; eauto. -(* EF_vload *) +- (* EF_vload *) unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... mydestr. destruct p as [[w'' t''] v]; mydestr. exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. - auto. -(* EF_vstore *) +- (* EF_vstore *) unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... mydestr. destruct p as [[w'' t''] m'']. mydestr. exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto. - auto. -(* EF_malloc *) +- (* EF_malloc *) unfold do_ef_malloc. destruct vargs... destruct vargs... mydestr. destruct (Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned i)) as [m1 b] eqn:?. mydestr. split. apply SIZE in Heqo. subst v. econstructor; eauto. constructor. -(* EF_free *) - unfold do_ef_free. destruct vargs... destruct v... destruct vargs... - mydestr. split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. constructor. -(* EF_memcpy *) +- (* EF_free *) + unfold do_ef_free. destruct vargs... destruct v... ++ destruct vargs... mydestr; InvBooleans; subst i. + replace (Vint Int.zero) with Vnullptr. split; constructor. + apply negb_true_iff in H0. unfold Vnullptr; rewrite H0; auto. ++ destruct vargs... mydestr; InvBooleans; subst i. + replace (Vlong Int64.zero) with Vnullptr. split; constructor. + unfold Vnullptr; rewrite H0; auto. ++ destruct vargs... mydestr. + split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. + constructor. +- (* EF_memcpy *) unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... destruct v... destruct vargs... mydestr. apply Decidable_sound in Heqb1. red in Heqb1. split. econstructor; eauto; tauto. constructor. -(* EF_annot *) +- (* EF_annot *) unfold do_ef_annot. mydestr. split. constructor. apply list_eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. -(* EF_annot_val *) +- (* EF_annot_val *) unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. split. constructor. apply eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. -(* EF_inline_asm *) +- (* EF_inline_asm *) eapply do_inline_assembly_sound; eauto. -(* EF_debug *) +- (* EF_debug *) unfold do_ef_debug. mydestr. split; constructor. Qed. @@ -605,37 +619,38 @@ Proof. - eapply do_external_function_complete; eauto. } destruct ef; simpl in *. -(* EF_external *) +- (* EF_external *) eapply do_external_function_complete; eauto. -(* EF_builtin *) +- (* EF_builtin *) eapply BF_EX; eauto. -(* EF_runtime *) +- (* EF_runtime *) eapply BF_EX; eauto. -(* EF_vload *) +- (* EF_vload *) inv H; unfold do_ef_volatile_load. exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto. -(* EF_vstore *) +- (* EF_vstore *) inv H; unfold do_ef_volatile_store. exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto. -(* EF_malloc *) +- (* EF_malloc *) inv H; unfold do_ef_malloc. inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto. -(* EF_free *) +- (* EF_free *) inv H; unfold do_ef_free. - inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega. -(* EF_memcpy *) ++ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega. ++ inv H0. unfold Vnullptr; destruct Archi.ptr64; auto. +- (* EF_memcpy *) inv H; unfold do_ef_memcpy. inv H0. rewrite Decidable_complete. rewrite H7; rewrite H8; auto. red. tauto. -(* EF_annot *) +- (* EF_annot *) inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. rewrite (list_eventval_of_val_complete _ _ _ H1). auto. -(* EF_annot_val *) +- (* EF_annot_val *) inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. rewrite (eventval_of_val_complete _ _ _ H1). auto. -(* EF_inline_asm *) +- (* EF_inline_asm *) eapply do_inline_assembly_complete; eauto. -(* EF_debug *) +- (* EF_debug *) inv H. inv H0. reflexivity. Qed. 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