Stricter formal semantics for free - #592
Open
xavierleroy wants to merge 2 commits into
Open
Conversation
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.
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
As currently modeled in the CompCert semantics, the
freefunction accepts as arguments some pointers that were not returned bymalloc, including pointers in the middle of a block. The reason for this tolerance is to make the semantics offreecompatible with memory injections, which can transform a pointer returned bymallocinto a pointer in the middle of a block. (At least conceptually; this is never necessary in CompCert's correctness proofs.)This PR tightens the formal semantics of
freeso that it fails when given a pointer that does not point to the beginning of a block allocated bymalloc. Compatibility with memory injections is ensured by an extra condition on memory injections.Conceptually, we could associate a kind (global, stack, heap) with every memory block and require that blocks tagged "heap" are injected with offset 0. Instead, I chose to express the extra requirement on memory injections in terms of permissions and of metadata associated with heap blocks. The formal model of
mallocandfreeuses negative offsets to store metadata (the size of the block), so that user code cannot read or write this metadata. In this PR, we require that valid negative offsets are injected with offset 0 and therefore cannot end up at nonnegative offsets. In other words, metadata should remain inaccessible to user code after memory injection.