approach six

#pragma loop bounded 64
for (int i = 0; i < n; ++i) { ... }

Another kind of pragmas may be useful to make compiling verified code more practical. Let's call them "must-pragmas". For example:

#pragma loop must bound 0, 64
for (int i = 0; i < n; ++i) { ... }

That pragma would make the compiler to fail at compile time if it is not able to determine with 100% certainty, all the stages of compilation considered, that the bounds of the loop are indeed 0 and 64.

The idea is that if the compiler can figure out the loop bounds, then it may be possible to emit BPF code in a form from which the verifier can also determine the same bounds, and therefore there is a chance the compiler can produce a verifiable program.

On the other hand, if the compiler cannot determine the loop bounds, using all the information it has about the program being compiled (from source code to the several intermediate representations in their respective abstraction levels) then there is little or no hope for a low-level verifier, that only has access to the compiled instructions, to do so. A compile-time error is in order in that case, pointing to the specific "non-verifiable" source code construct.

Other example of that kind of pragmas could be `#pragma loop must unroll' and, in general, annotations that make the compiler to fail if some particular optimization has not been successfully applied to some particular source code construct.

So approach six may still contribute to the solution... perhaps 8-)

We plan to continue and expand the discussion on how to make compiling to BPF and verified targets more practical at the LPC Toolchains Track in November, along with the clang/llvm and kernel chaps. It will be fun, interesting and hopefully useful.