From 85b01868ba454e4aa0d44b1be0126496dc16ee0f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 15 Aug 2026 09:48:09 +0200 Subject: [PATCH 1/2] Memory model: ensure injections do not make metadata accessible normally The modeling of `malloc` and `free` uses a negative block offset to store the size of the allocated block. This ensures that user code cannot modify the size using an ordinary store. More generally, metadata can be stored at negative block offsets to hide it from user code. However, a memory injection could map this negative offset to a nonnegative offset, manipulable by the user code. In turn, this makes `free` more lenient than it should be, e.g. it is possible to free a pointer that was not returned by `malloc`. This commit adds one condition to memory injections: if a block has negative lower bound (i.e. valid negative offsets), its injection must have delta = 0. This condition is trivially satisfied by CompCert's uses of memory injections: the only blocks that are injected with delta <> 0 are stack blocks, which have lower bound 0. --- backend/Inliningproof.v | 2 + backend/Unusedglobproof.v | 1 + backend/ValueDomain.v | 3 + cfrontend/Cminorgenproof.v | 15 +- common/Memory.v | 351 +++++++++++++++++++++---------------- common/Separation.v | 2 + 6 files changed, 218 insertions(+), 156 deletions(-) diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index c28b57e45..0706d9e65 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -1177,6 +1177,8 @@ Proof. instantiate (1 := sp'). auto. (* offset is representable *) instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). lia. + (* negative offsets are not revealed *) + right; lia. (* size of target block is representable *) intros. right. exploit SSZ2; eauto with mem. inv FB; lia. (* we have full permissions on sp' at and above dstk ctx *) diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index c741e96fc..406a1b9a9 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -1196,6 +1196,7 @@ Proof. apply Q2 in H0. destruct H0. subst. left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. apply P1. lia. +- apply init_meminj_invert in H. tauto. Qed. End INIT_MEM. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 165540777..7f2fc39ce 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -5035,6 +5035,9 @@ Proof. - (* perm inv *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Z.add_0_r in H2. auto. +- (* metadata *) + intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. + auto. Qed. Lemma inj_of_bc_preserves_globals: diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index c02b05c57..4bad1b9c3 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -817,24 +817,23 @@ Lemma match_callstack_alloc_variables_rec: Proof. intros until cs; intros VALID REPRES STKSIZE STKPERMS. induction 1; intros f1 NOREPET COMPAT SEP1 SEP2 UNBOUND MCS MINJ. - (* base case *) +- (* base case *) simpl in MCS. exists f1; auto. - (* inductive case *) +- (* inductive case *) simpl in NOREPET. inv NOREPET. -(* exploit Mem.alloc_result; eauto. intros RES. - exploit Mem.nextblock_alloc; eauto. intros NB.*) exploit (COMPAT id sz). auto with coqlib. intros [ofs [CENV [ALIGNED [LOB HIB]]]]. exploit Mem.alloc_left_mapped_inject. eexact MINJ. eexact H. eexact VALID. - instantiate (1 := ofs). zify. lia. + instantiate (1 := ofs). lia. + right; lia. intros. exploit STKSIZE; eauto. lia. - intros. apply STKPERMS. zify. lia. + intros. apply STKPERMS. lia. replace (sz - 0) with sz by lia. auto. intros. eapply SEP2. eauto with coqlib. eexact CENV. eauto. eauto. lia. - intros [f2 [A [B [C D]]]]. - exploit (IHalloc_variables f2); eauto. + intros (f2 & A & B & C & D). + eapply (IHalloc_variables f2); eauto. red; intros. eapply COMPAT. auto with coqlib. red; intros. eapply SEP1; eauto with coqlib. red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b b1); intros P. diff --git a/common/Memory.v b/common/Memory.v index 54def2786..a6276dd08 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -3138,7 +3138,10 @@ Qed. - distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2]; - the sizes of [m2]'s blocks are representable with unsigned machine integers; - pointers that could be represented using unsigned machine integers remain - representable after the injection. + representable after the injection; +- "metadata" (data stored at negative offsets within a block, making it + inaccessible to user code) is not revealed (at positive offsets) after + the injection. *) Record inject' (f: meminj) (m1 m2: mem) : Prop := @@ -3160,7 +3163,12 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop := forall b1 ofs b2 delta k p, f b1 = Some(b2, delta) -> perm m2 b2 (ofs + delta) k p -> - perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty + perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty; + mi_metadata: forall b b' delta ofs, + f b = Some(b', delta) -> + perm m1 b ofs Max Nonempty -> + ofs < 0 -> + delta = 0 }. Definition inject := inject'. @@ -3529,20 +3537,22 @@ Proof. intros. inversion H. exploit store_mapped_inj; eauto. intros [n2 [STORE MI]]. exists n2; split. eauto. constructor. -(* inj *) +- (* inj *) auto. -(* freeblocks *) +- (* freeblocks *) eauto with mem. -(* mappedblocks *) +- (* mappedblocks *) eauto with mem. -(* no overlap *) +- (* no overlap *) red; intros. eauto with mem. -(* representable *) +- (* representable *) intros. eapply mi_representable; try eassumption. destruct H4; eauto with mem. -(* perm inv *) +- (* perm inv *) intros. exploit mi_perm_inv0; eauto using perm_store_2. intuition eauto using perm_store_1, perm_store_2. +- (* metadata *) + intros. eauto using perm_store_2. Qed. Theorem store_unmapped_inject: @@ -3554,20 +3564,22 @@ Theorem store_unmapped_inject: Proof. intros. inversion H. constructor. -(* inj *) +- (* inj *) eapply store_unmapped_inj; eauto. -(* freeblocks *) +- (* freeblocks *) eauto with mem. -(* mappedblocks *) +- (* mappedblocks *) eauto with mem. -(* no overlap *) +- (* no overlap *) red; intros. eauto with mem. -(* representable *) +- (* representable *) intros. eapply mi_representable; try eassumption. destruct H3; eauto with mem. -(* perm inv *) +- (* perm inv *) intros. exploit mi_perm_inv0; eauto using perm_store_2. intuition eauto using perm_store_1, perm_store_2. +- (* metadata *) + intros. eauto using perm_store_2. Qed. Theorem store_outside_inject: @@ -3581,17 +3593,19 @@ Theorem store_outside_inject: inject f m1 m2'. Proof. intros. inversion H. constructor. -(* inj *) +- (* inj *) eapply store_outside_inj; eauto. -(* freeblocks *) +- (* freeblocks *) auto. -(* mappedblocks *) +- (* mappedblocks *) eauto with mem. -(* no overlap *) +- (* no overlap *) auto. -(* representable *) +- (* representable *) eauto with mem. -(* perm inv *) +- (* perm inv *) + intros. eauto using perm_store_2. +- (* metadata *) intros. eauto using perm_store_2. Qed. @@ -3627,20 +3641,22 @@ Proof. intros. inversion H. exploit storebytes_mapped_inj; eauto. intros [n2 [STORE MI]]. exists n2; split. eauto. constructor. -(* inj *) +- (* inj *) auto. -(* freeblocks *) +- (* freeblocks *) intros. apply mi_freeblocks0. red; intros; elim H3; eapply storebytes_valid_block_1; eauto. -(* mappedblocks *) +- (* mappedblocks *) intros. eapply storebytes_valid_block_1; eauto. -(* no overlap *) +- (* no overlap *) red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. -(* representable *) +- (* representable *) intros. eapply mi_representable0; eauto. destruct H4; eauto using perm_storebytes_2. -(* perm inv *) +- (* perm inv *) intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. intuition eauto using perm_storebytes_1, perm_storebytes_2. +- (* metadata *) + intros. eauto using perm_storebytes_2. Qed. Theorem storebytes_unmapped_inject: @@ -3652,20 +3668,22 @@ Theorem storebytes_unmapped_inject: Proof. intros. inversion H. constructor. -(* inj *) +- (* inj *) eapply storebytes_unmapped_inj; eauto. -(* freeblocks *) +- (* freeblocks *) intros. apply mi_freeblocks0. red; intros; elim H2; eapply storebytes_valid_block_1; eauto. -(* mappedblocks *) +- (* mappedblocks *) eauto with mem. -(* no overlap *) +- (* no overlap *) red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. -(* representable *) +- (* representable *) intros. eapply mi_representable0; eauto. destruct H3; eauto using perm_storebytes_2. -(* perm inv *) +- (* perm inv *) intros. exploit mi_perm_inv0; eauto. intuition eauto using perm_storebytes_1, perm_storebytes_2. +- (* metadata *) + intros. eauto using perm_storebytes_2. Qed. Theorem storebytes_outside_inject: @@ -3679,18 +3697,20 @@ Theorem storebytes_outside_inject: inject f m1 m2'. Proof. intros. inversion H. constructor. -(* inj *) +- (* inj *) eapply storebytes_outside_inj; eauto. -(* freeblocks *) +- (* freeblocks *) auto. -(* mappedblocks *) +- (* mappedblocks *) intros. eapply storebytes_valid_block_1; eauto. -(* no overlap *) +- (* no overlap *) auto. -(* representable *) +- (* representable *) auto. -(* perm inv *) +- (* perm inv *) intros. eapply mi_perm_inv0; eauto using perm_storebytes_2. +- (* metadata *) + intros. eauto using perm_storebytes_2. Qed. Theorem storebytes_empty_inject: @@ -3701,20 +3721,22 @@ Theorem storebytes_empty_inject: inject f m1' m2'. Proof. intros. inversion H. constructor; intros. -(* inj *) +- (* inj *) eapply storebytes_empty_inj; eauto. -(* freeblocks *) +- (* freeblocks *) intros. apply mi_freeblocks0. red; intros; elim H2; eapply storebytes_valid_block_1; eauto. -(* mappedblocks *) +- (* mappedblocks *) intros. eapply storebytes_valid_block_1; eauto. -(* no overlap *) +- (* no overlap *) red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. -(* representable *) +- (* representable *) intros. eapply mi_representable0; eauto. destruct H3; eauto using perm_storebytes_2. -(* perm inv *) +- (* perm inv *) intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. intuition eauto using perm_storebytes_1, perm_storebytes_2. +- (* metadata *) + intros. eauto using perm_storebytes_2. Qed. (* Preservation of allocations *) @@ -3727,20 +3749,22 @@ Theorem alloc_right_inject: Proof. intros. injection H0. intros NEXT MEM. inversion H. constructor. -(* inj *) +- (* inj *) eapply alloc_right_inj; eauto. -(* freeblocks *) +- (* freeblocks *) auto. -(* mappedblocks *) +- (* mappedblocks *) eauto with mem. -(* no overlap *) +- (* no overlap *) auto. -(* representable *) +- (* representable *) auto. -(* perm inv *) +- (* perm inv *) intros. eapply perm_alloc_inv in H2; eauto. destruct (eq_block b0 b2). subst b0. eelim fresh_block_alloc; eauto. eapply mi_perm_inv0; eauto. +- (* metadata *) + auto. Qed. Theorem alloc_left_unmapped_inject: @@ -3765,34 +3789,37 @@ Proof. unfold f'; intros. destruct (eq_block b0 b1). congruence. eauto. unfold f'; intros. destruct (eq_block b0 b1). congruence. apply memval_inject_incr with f; auto. - exists f'; split. constructor. -(* inj *) + exists f'; split; [constructor|split; [|split]]. +- (* inj *) eapply alloc_left_unmapped_inj; eauto. unfold f'; apply dec_eq_true. -(* freeblocks *) +- (* freeblocks *) intros. unfold f'. destruct (eq_block b b1). auto. apply mi_freeblocks0. red; intro; elim H3. eauto with mem. -(* mappedblocks *) +- (* mappedblocks *) unfold f'; intros. destruct (eq_block b b1). congruence. eauto. -(* no overlap *) +- (* no overlap *) unfold f'; red; intros. destruct (eq_block b0 b1); destruct (eq_block b2 b1); try congruence. eapply mi_no_overlap0. eexact H3. eauto. eauto. exploit perm_alloc_inv. eauto. eexact H6. rewrite dec_eq_false; auto. exploit perm_alloc_inv. eauto. eexact H7. rewrite dec_eq_false; auto. -(* representable *) +- (* representable *) unfold f'; intros. destruct (eq_block b b1); try discriminate. eapply mi_representable0; try eassumption. destruct H4; eauto using perm_alloc_4. -(* perm inv *) +- (* perm inv *) intros. unfold f' in H3; destruct (eq_block b0 b1); try discriminate. exploit mi_perm_inv0; eauto. intuition eauto using perm_alloc_1, perm_alloc_4. -(* incr *) - split. auto. -(* image *) - split. unfold f'; apply dec_eq_true. -(* incr *) +- (* metadata *) + intros. unfold f' in H3; destruct (eq_block b b1); try discriminate. + eauto using perm_alloc_4. +- (* incr *) + auto. +- (* image *) + unfold f'; apply dec_eq_true. +- (* incr *) intros; unfold f'; apply dec_eq_false; auto. Qed. @@ -3802,6 +3829,7 @@ Theorem alloc_left_mapped_inject: alloc m1 lo hi = (m1', b1) -> valid_block m2 b2 -> 0 <= delta <= Ptrofs.max_unsigned -> + delta = 0 \/ 0 <= lo -> (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Ptrofs.max_unsigned) -> (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) -> inj_offset_aligned delta (hi-lo) -> @@ -3815,7 +3843,8 @@ Theorem alloc_left_mapped_inject: /\ f' b1 = Some(b2, delta) /\ (forall b, b <> b1 -> f' b = f b). Proof. - intros. inversion H. + intros until delta; intros INJ ALLOC VALID RANGE1 RANGE2 RANGE3 PERM ALIGN SEP. + inversion INJ. set (f' := fun b => if eq_block b b1 then Some(b2, delta) else f b). assert (inject_incr f f'). { red; unfold f'; intros. destruct (eq_block b b1). subst b. @@ -3824,66 +3853,70 @@ Proof. assert (mem_inj f' m1 m2). { inversion mi_inj0; constructor; eauto with mem. + unfold f'; intros. destruct (eq_block b0 b1). - inversion H8. subst b0 b3 delta0. - elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. + inversion H0. subst b0 b3 delta0. + elim (fresh_block_alloc _ _ _ _ _ ALLOC). eauto with mem. eauto. + unfold f'; intros. destruct (eq_block b0 b1). - inversion H8. subst b0 b3 delta0. - elim (fresh_block_alloc _ _ _ _ _ H0). - eapply perm_valid_block with (ofs := ofs). apply H10. lia. + inversion H0. subst b0 b3 delta0. + elim (fresh_block_alloc _ _ _ _ _ ALLOC). + eapply perm_valid_block with (ofs := ofs). apply H2. lia. eauto. + unfold f'; intros. destruct (eq_block b0 b1). - inversion H8. subst b0 b3 delta0. - elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. + inversion H0. subst b0 b3 delta0. + elim (fresh_block_alloc _ _ _ _ _ ALLOC). eauto with mem. apply memval_inject_incr with f; auto. } - exists f'. split. constructor. -(* inj *) + exists f'; split; [constructor|split; [|split]]. +- (* inj *) eapply alloc_left_mapped_inj; eauto. unfold f'; apply dec_eq_true. -(* freeblocks *) +- (* freeblocks *) unfold f'; intros. destruct (eq_block b b1). subst b. - elim H9. eauto with mem. + elim H1. eauto with mem. eauto with mem. -(* mappedblocks *) +- (* mappedblocks *) unfold f'; intros. destruct (eq_block b b1). congruence. eauto. -(* overlap *) +- (* overlap *) unfold f'; red; intros. - exploit perm_alloc_inv. eauto. eexact H12. intros P1. - exploit perm_alloc_inv. eauto. eexact H13. intros P2. + exploit perm_alloc_inv. eauto. eexact H4. intros P1. + exploit perm_alloc_inv. eauto. eexact H5. intros P2. destruct (eq_block b0 b1); destruct (eq_block b3 b1). congruence. - inversion H10; subst b0 b1' delta1. + inversion H2; subst b0 b1' delta1. destruct (eq_block b2 b2'); auto. subst b2'. right; red; intros. - eapply H6; eauto. lia. - inversion H11; subst b3 b2' delta2. + eapply SEP; eauto. lia. + inversion H3; subst b3 b2' delta2. destruct (eq_block b1' b2); auto. subst b1'. right; red; intros. - eapply H6; eauto. lia. + eapply SEP; eauto. lia. eauto. -(* representable *) +- (* representable *) unfold f'; intros. destruct (eq_block b b1). - subst. injection H9; intros; subst b' delta0. destruct H10. - exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. - exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. - generalize (Ptrofs.unsigned_range_2 ofs). lia. - exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. - exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. - generalize (Ptrofs.unsigned_range_2 ofs). lia. - eapply mi_representable0; try eassumption. - destruct H10; eauto using perm_alloc_4. -(* perm inv *) - intros. unfold f' in H9; destruct (eq_block b0 b1). - inversion H9; clear H9; subst b0 b3 delta0. - assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by lia. - destruct EITHER. - left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. - right; intros A. eapply perm_alloc_inv in A; eauto. rewrite dec_eq_true in A. tauto. - exploit mi_perm_inv0; eauto. intuition eauto using perm_alloc_1, perm_alloc_4. -(* incr *) - split. auto. -(* image of b1 *) - split. unfold f'; apply dec_eq_true. -(* image of others *) + + subst. injection H1; intros; subst b' delta0. destruct H2. + * exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. + exploit RANGE3. apply PERM with (k := Max) (p := Nonempty); eauto. + generalize (Ptrofs.unsigned_range_2 ofs). lia. + * exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. + exploit RANGE3. apply PERM with (k := Max) (p := Nonempty); eauto. + generalize (Ptrofs.unsigned_range_2 ofs). lia. + + eapply mi_representable0; try eassumption. + destruct H2; eauto using perm_alloc_4. +- (* perm inv *) + intros. unfold f' in H1; destruct (eq_block b0 b1). + + inversion H1; clear H1; subst b0 b3 delta0. + assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by lia. + destruct EITHER. + * left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. + * right; intros A. eapply perm_alloc_inv in A; eauto. rewrite dec_eq_true in A. tauto. + + exploit mi_perm_inv0; eauto. intuition eauto using perm_alloc_1, perm_alloc_4. +- (* metadata *) + intros. unfold f' in H1; destruct (eq_block b b1). + + inv H1. rename delta0 into delta. eapply perm_alloc_3 in H2; eauto. lia. + + eauto using perm_alloc_4. +- (* incr *) + auto. +- (* image of b1 *) + unfold f'; apply dec_eq_true. +- (* image of others *) intros. unfold f'; apply dec_eq_false; auto. Qed. @@ -3900,13 +3933,14 @@ Theorem alloc_parallel_inject: /\ (forall b, b <> b1 -> f' b = f b). Proof. intros. - case_eq (alloc m2 lo2 hi2). intros m2' b2 ALLOC. + destruct (alloc m2 lo2 hi2) as [m2' b2] eqn:ALLOC. exploit alloc_left_mapped_inject. eapply alloc_right_inject; eauto. eauto. instantiate (1 := b2). eauto with mem. instantiate (1 := 0). unfold Ptrofs.max_unsigned. generalize Ptrofs.modulus_pos; lia. auto. + auto. intros. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. lia. red; intros. apply Z.divide_0_r. @@ -3924,21 +3958,23 @@ Lemma free_left_inject: inject f m1' m2. Proof. intros. inversion H. constructor. -(* inj *) +- (* inj *) eapply free_left_inj; eauto. -(* freeblocks *) +- (* freeblocks *) eauto with mem. -(* mappedblocks *) +- (* mappedblocks *) auto. -(* no overlap *) +- (* no overlap *) red; intros. eauto with mem. -(* representable *) +- (* representable *) intros. eapply mi_representable0; try eassumption. destruct H2; eauto with mem. -(* perm inv *) +- (* 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. +- (* metadata *) + intros. eauto using perm_free_3. Qed. Lemma free_list_left_inject: @@ -3964,17 +4000,19 @@ Lemma free_right_inject: inject f m1 m2'. Proof. intros. inversion H. constructor. -(* inj *) +- (* inj *) eapply free_right_inj; eauto. -(* freeblocks *) +- (* freeblocks *) auto. -(* mappedblocks *) +- (* mappedblocks *) eauto with mem. -(* no overlap *) +- (* no overlap *) auto. -(* representable *) +- (* representable *) auto. -(* perm inv *) +- (* perm inv *) + intros. eauto using perm_free_3. +- (* metadata *) intros. eauto using perm_free_3. Qed. @@ -4088,16 +4126,16 @@ Theorem inject_compose: Proof. unfold compose_meminj; intros. inv H; inv H0. constructor. -(* inj *) +- (* inj *) eapply mem_inj_compose; eauto. -(* unmapped *) +- (* unmapped *) intros. erewrite mi_freeblocks0; eauto. -(* mapped *) +- (* mapped *) intros. destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate. destruct (f' b1) as [[b2 delta2] |] eqn:?; inv H. eauto. -(* no overlap *) +- (* no overlap *) red; intros. destruct (f b1) as [[b1x delta1x] |] eqn:?; try discriminate. destruct (f' b1x) as [[b1y delta1y] |] eqn:?; inv H0. @@ -4111,7 +4149,7 @@ Proof. eapply perm_inj. eauto. eexact H2. eauto. eapply perm_inj. eauto. eexact H3. eauto. intuition lia. -(* representable *) +- (* representable *) intros. destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate. destruct (f' b1) as [[b2 delta2] |] eqn:?; inv H. @@ -4125,7 +4163,7 @@ Proof. ((Ptrofs.unsigned ofs - 1) + delta1) by lia. destruct H0; eauto using perm_inj. rewrite H. lia. -(* perm inv *) +- (* perm inv *) intros. destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. destruct (f' b') as [[b'' delta''] |] eqn:?; try discriminate. @@ -4134,6 +4172,15 @@ Proof. exploit mi_perm_inv1; eauto. intros [A|A]. eapply mi_perm_inv0; eauto. right; red; intros. elim A. eapply perm_inj; eauto. +- (* metadata *) + intros. + destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate. + destruct (f' b1) as [[b2 delta2] |] eqn:?; try discriminate. + inversion H; clear H; subst b2 delta. + assert (delta1 = 0) by eauto. + eapply perm_inj in H0; eauto. subst delta1. rewrite Z.add_0_r in H0. + assert (delta2 = 0) by eauto. + lia. Qed. Lemma val_lessdef_inject_compose: @@ -4155,23 +4202,25 @@ Lemma extends_inject_compose: extends m1 m2 -> inject f m2 m3 -> inject f m1 m3. Proof. intros. inversion H; inv H0. constructor; intros. -(* inj *) +- (* inj *) replace f with (compose_meminj inject_id f). eapply mem_inj_compose; eauto. apply extensionality; intros. unfold compose_meminj, inject_id. destruct (f x) as [[y delta] | ]; auto. -(* unmapped *) +- (* unmapped *) eapply mi_freeblocks0. erewrite <- valid_block_extends; eauto. -(* mapped *) +- (* mapped *) eauto. -(* no overlap *) +- (* no overlap *) red; intros. eapply mi_no_overlap0; eauto; eapply perm_extends; eauto. -(* representable *) +- (* representable *) eapply mi_representable0; eauto. destruct H1; eauto using perm_extends. -(* perm inv *) +- (* perm inv *) exploit mi_perm_inv0; eauto. intros [A|A]. eapply mext_perm_inv0; eauto. right; red; intros; elim A. eapply perm_extends; eauto. +- (* metadata *) + eauto using perm_extends. Qed. Lemma inject_extends_compose: @@ -4179,22 +4228,24 @@ Lemma inject_extends_compose: inject f m1 m2 -> extends m2 m3 -> inject f m1 m3. Proof. intros. inv H; inversion H0. constructor; intros. -(* inj *) +- (* inj *) replace f with (compose_meminj f inject_id). eapply mem_inj_compose; eauto. apply extensionality; intros. unfold compose_meminj, inject_id. destruct (f x) as [[y delta] | ]; auto. decEq. decEq. lia. -(* unmapped *) +- (* unmapped *) eauto. -(* mapped *) +- (* mapped *) erewrite <- valid_block_extends; eauto. -(* no overlap *) +- (* no overlap *) red; intros. eapply mi_no_overlap0; eauto. -(* representable *) +- (* representable *) eapply mi_representable0; eauto. -(* perm inv *) +- (* perm inv *) exploit mext_perm_inv0; eauto. intros [A|A]. eapply mi_perm_inv0; eauto. right; red; intros; elim A. eapply perm_inj; eauto. +- (* metadata *) + eauto. Qed. Lemma extends_extends_compose: @@ -4202,13 +4253,13 @@ Lemma extends_extends_compose: extends m1 m2 -> extends m2 m3 -> extends m1 m3. Proof. intros. inversion H; subst; inv H0; constructor; intros. - (* nextblock *) +- (* nextblock *) congruence. - (* meminj *) +- (* meminj *) replace inject_id with (compose_meminj inject_id inject_id). eapply mem_inj_compose; eauto. apply extensionality; intros. unfold compose_meminj, inject_id. auto. - (* perm inv *) +- (* perm inv *) exploit mext_perm_inv1; eauto. intros [A|A]. eapply mext_perm_inv0; eauto. right; red; intros; elim A. eapply perm_extends; eauto. @@ -4235,35 +4286,39 @@ Theorem neutral_inject: forall m, inject_neutral (nextblock m) m -> inject (flat_inj (nextblock m)) m m. Proof. intros. constructor. -(* meminj *) +- (* meminj *) auto. -(* freeblocks *) +- (* freeblocks *) unfold flat_inj, valid_block; intros. apply pred_dec_false. auto. -(* mappedblocks *) +- (* mappedblocks *) unfold flat_inj, valid_block; intros. destruct (plt b (nextblock m)); inversion H0; subst. auto. -(* no overlap *) +- (* no overlap *) apply flat_inj_no_overlap. -(* range *) +- (* range *) unfold flat_inj; intros. destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); lia. -(* perm inv *) +- (* perm inv *) unfold flat_inj; intros. destruct (plt b1 (nextblock m)); inv H0. rewrite Z.add_0_r in H1; auto. +- (* metadata *) + unfold flat_inj; intros. + destruct (plt b (nextblock m)); inv H0. + auto. Qed. Theorem empty_inject_neutral: forall thr, inject_neutral thr empty. Proof. intros; red; constructor. -(* perm *) +- (* perm *) unfold flat_inj; intros. destruct (plt b1 thr); inv H. replace (ofs + 0) with ofs by lia; auto. -(* align *) +- (* align *) unfold flat_inj; intros. destruct (plt b1 thr); inv H. apply Z.divide_0_r. -(* mem_contents *) +- (* mem_contents *) intros; simpl. rewrite ! PMap.gi. rewrite ! ZMap.gi. constructor. Qed. diff --git a/common/Separation.v b/common/Separation.v index 465adfa48..deba792d3 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -639,6 +639,7 @@ Next Obligation. - intros. destruct (Mem.perm_dec m0 b1 ofs Max Nonempty); auto. eapply mi_perm_inv; eauto. eapply Mem.perm_unchanged_on_2; eauto. +- eauto using Mem.perm_unchanged_on_2. Qed. Next Obligation. eapply Mem.valid_block_inject_2; eauto. @@ -708,6 +709,7 @@ Proof. - eexact ALLOC1. - instantiate (1 := b2). eauto with mem. - instantiate (1 := delta). extlia. +- right; lia. - intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). lia. - intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. extlia. From e2efe163a820386cad882501638a69f2898681af Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 15 Aug 2026 11:25:07 +0200 Subject: [PATCH 2/2] Tigthen the semantics of `free` Require that the argument `p` of `free(p)` points to the beginning of a block (offset is 0). Before, for compatibility with memory injections, `p` pointing in the middle of a block was accepted, provided that the word before `p` contains a valid length. This is not ISO C, of course. With the new definition of memory injections (previous commit), `free` can fail on pointers in the middle of a block while remaining compatible with memory injections. --- cfrontend/Cexec.v | 19 +++++++++---------- common/Events.v | 27 ++++++++++++--------------- 2 files changed, 21 insertions(+), 25 deletions(-) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index b66abfeb3..8d129dcfb 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -505,18 +505,17 @@ Definition do_ef_free (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match vargs with | Vptr b lo :: nil => - do vsz <- Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr); + check (Ptrofs.eq_dec lo Ptrofs.zero); + do vsz <- Mem.load Mptr m b (- size_chunk Mptr); do sz <- do_alloc_size vsz; - do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz); + do m' <- Mem.free m b (- size_chunk Mptr) (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 + check (Int.eq_dec n Int.zero && negb Archi.ptr64); + Some(w, E0, Vundef, m) | Vlong n :: nil => - if Int64.eq_dec n Int64.zero && Archi.ptr64 - then Some(w, E0, Vundef, m) - else None + check (Int64.eq_dec n Int64.zero && Archi.ptr64); + Some(w, E0, Vundef, m) | _ => None end. @@ -628,7 +627,7 @@ Proof with try congruence. replace (Vlong Int64.zero) with Vnullptr. split; constructor. unfold Vnullptr; rewrite H0; auto. + destruct vargs... mydestr. - split. apply SIZE in Heqo0. econstructor; eauto. congruence. + split. apply SIZE in Heqo0. subst v. econstructor; eauto. constructor. - (* EF_memcpy *) unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... @@ -685,7 +684,7 @@ Proof. inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto. - (* EF_free *) inv H; unfold do_ef_free. -+ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite H2. auto. ++ inv H0. rewrite dec_eq_true. rewrite H1. erewrite SIZE by eauto. rewrite H2. auto. + inv H0. unfold Vnullptr; destruct Archi.ptr64; auto. - (* EF_memcpy *) inv H; unfold do_ef_memcpy. diff --git a/common/Events.v b/common/Events.v index 38cf6139d..6cc9f025d 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1060,10 +1060,10 @@ Qed. Inductive extcall_free_sem (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := - | extcall_free_sem_ptr: forall b lo sz m m', - Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr) = Some (Vptrofs sz) -> - 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_ptr: forall b sz m m', + Mem.load Mptr m b (- size_chunk Mptr) = Some (Vptrofs sz) -> + Mem.free m b (- size_chunk Mptr) (Ptrofs.unsigned sz) = Some m' -> + extcall_free_sem ge (Vptr b Ptrofs.zero :: nil) m E0 Vundef m' | extcall_free_sem_null: forall m, extcall_free_sem ge (Vnullptr :: nil) m E0 Vundef m. @@ -1115,25 +1115,22 @@ Proof. assert (v' = Vptrofs sz). { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. } subst v'. - assert (P: Mem.range_perm m1 b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) Cur Freeable). - eapply Mem.free_range_perm; eauto. - assert (EQ: Ptrofs.unsigned (Ptrofs.add lo (Ptrofs.repr delta)) = Ptrofs.unsigned lo + delta). - { eapply Mem.address_inject_gen with (p := Freeable); eauto. - right. apply P. - generalize (size_chunk_pos Mptr), (Ptrofs.unsigned_range sz); lia. } + assert (delta = 0). + { eapply Mem.mi_metadata; eauto. + instantiate (1 := - size_chunk Mptr). eauto with mem. + generalize (size_chunk_pos Mptr). lia. } + subst delta. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). + rewrite ! Z.add_0_r in *. exists f, Vundef, m2'; split. - apply extcall_free_sem_ptr with (sz := sz) (m' := m2'). - rewrite EQ. rewrite <- A. f_equal. lia. - auto. auto. - rewrite ! EQ. rewrite <- C. f_equal; lia. + apply extcall_free_sem_ptr with (sz := sz) (m' := m2'); auto. split. auto. split. auto. split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence. split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach. intros. red; intros. eelim H2; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - apply P. lia. + eapply Mem.free_range_perm; eauto. lia. split. auto. red; intros. congruence. + inv H2. inv H6. replace v' with Vnullptr.