1
$\begingroup$

I apologize if this is not the right site to ask this, as the question is not about a proof assistant per se, but about a particular formalization.

In the semantics of the RTL intermediate language in CompCert, memory blocks are allocated and freed. At function start, the stack frame is allocated in memory, and it is freed at the end.

Assuming no external calls, it seems feasible to me (though I've not done it) to show that the stack frames that are on the current stack are still currently allocated in memory (until the stack is popped and the block freed as expected).

I however do not see how to prove that if a stack frame is allocated prior to an external call, it stays allocated. (In real life, of course, it is impossible to deallocate a caller's stackframe unless one does something like longjmp() or other dark magic, but I'm discussing this particular formalization here.)

There are a number of semantic definitions in Events.v that say what an external call is allowed to do, but I don't see anything preventing it from freeing a stack block.

Am I missing something?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

There is nothing that ensures that the stack frames are not freed. However, return (or tail call) will succeed only if the stack frames are still freeable, so execution would stop at that point in the formal semantics if the block has been freed before.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.