I have been recently going through Volume 5 of Software Foundations on Verifiable C and encountered
free() in the third chapter. The specification of
free() takes a pointer with an associated
malloc_token in the precondition and "disposes" of it, presumably freeing the memory under the pointer; however, according to my understanding, a function that takes in such a pointer and does nothing would also satisfy this specification (correct me if I am wrong). If so, does that mean that there is no easy way to prove that a particular C program is free of memory leaks using VST (alone)?
VST is a linear logic, so there's no immediate way to throw away resources. However, @Ralf Jung has written on this https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf#page92
In personal conversation, we got confirmation that this [a certain use of impredicative invariants] is likely sufficient to “leak” resources in VST, in the same vein as Theorem 2. And indeed, VST does not have a theorem stating that memory-leak freedom can be established by showing a Hoare triple with postcondition Emp.
Interesting read, thanks for sharing!
a function that takes in such a pointer and does nothing would also satisfy this specification (correct me if I am wrong)
If it does literally nothing, I think it might not be possible to satisfy the spec. But if it creates a lock and is creative about making the lock invariant self-referential, I think it is possible to satisfy the
free spec without actually freeing anything. (That's what I referred to in the quote above.)
I haven't literally tried to do this in Coq though as that I am not a VST expert. Could be a fun exercise for someone with more VST knowledge. :)
see in particular https://www.cs.princeton.edu/~appel/papers/hobor.pdf#page=92, the "unlock" rule -- which has postcondition
Last updated: Sep 25 2023 at 14:01 UTC