Why was the decision made to not support function pointers? about bedrock2 HOT 2 CLOSED

I don't know of any easy-to-read resource, we have been reading up on bedrock1/VST and talking to users of these systems to figure out what to do. The primary reason behind of omitting function pointer support for now was to focus efforts elsewhere. I think it that a similar system could likely be built with function-pointer support, and we might even add it once everything else is working. But for now, the plan is to use C++-style templates (implemented as coq functions) for code reuse across types instead of runtime function pointers. We realize this is limiting in some cases, but the judgement call was that improving the quality of the toolchain for function-pointer-free code is more important than allowing function pointers.

The fundamental source of difficulty in verifying code with function pointers is as follows:
To verify a function f that takes in a function pointer g, the precondition of f needs to say something about when it is safe to call g. However, defining what it means for g to satisfy its precondition is tricky because g could in principle call f, and circular definitions are no good. Thus we would need to either have some discipline to rule out the possibility of g calling f, or create some technical distinction between the top-level call to f and each following call through g. http://flint.cs.yale.edu/flint/publications/xcap.pdf section 2.3 discusses possible approaches for dealing this in more detail.

The XCAP style is perhaps the cleanest, but proof automation for it in bedrock1 was painfully slow on non-trivial examples. As far as we understand, this was due to technical debt in Coq, not because it fundamentally has to be slow, so likely either working around or fixing some coq asymptotic performance surprises (or here) could make this usable. For code without function pointers, the proof-by-reflection technique is a standard workaround.

from bedrock2.

answered

from bedrock2.