design: outputting bitwidth-generic code?

[andres-erbsen]

We may want a story for generating C code that can run in both 32-bit and 64-bit environments. Currently most functions are only proven for a single width. While some current functions have have generic proofs, extrapolating the current strategy would lead to width-parametrized bedrock2 code in Coq that would need to be instantiated with a width before output. If we wanted to output a single C file, we'd probably need a way to access UINTPTR_SIZE in bedrock2 expressions and stack-allocation calls. And we'd need to use width-parametrized memory-representation predicates for structures that contain pointers.

[samuelgruetter]

We already have several separation logic library files containing width-parametrized memory-representation predicates, so I'd expect this part should just work.
Parameterizing source syntax over the bitwidth parameter feels a bit wrong, because so far we always tried to say the bitwidth is a semantics thing and keep it separate from syntax (even though in my live verif stuff, if I start parameterizing over the bitwidth, the source code will be paramerized over it too).
Outputting bitwidth-generic code using the Gallina pretty-printer would be nice, but doesn't seem possible at the moment because the AST being fed to the pretty-printer needs to be fully concrete. I guess I wouldn't oppose adding a special expr.bytes_per_word or expr.word_sz (or whatever name you come up with) node and a notation UINTPTR_SIZE for it, and it should also be easy to replace that by a literal in the flattening phase of the compiler.

[andres-erbsen]

Cool. Would you be happy with having stackalloc sizes be expr, but evaluated in an empty environment?

[samuelgruetter]

Aah I see why you want this... A little awkward, supporting arbitrary expressions evaluated with full access to the locals and memory would be nicer, but can't really work in general with the static stack usage analyzer. But we could probably say the programs still have defined behavior according to the semantics, but the compiler just fails with an error if the stackalloc size isn't a constant.
Or maybe a simpler approach: Add an access_size argument to stackalloc?

[andres-erbsen]

Multiplying by an access_size is not enough for sizing structs that contain both bytes and words. Allowing runtime-sized stack allocation in the semantics but not in the compiler could also work, yes. Would you prefer this solution? (I believe naive translation to C would summon C variable-length arrays for code we didn't intend to support, but these would probably still have the right semantics until UB from stack overflow.)

[samuelgruetter]

Multiplying by an access_size is not enough for sizing structs that contain both bytes and words.

Ah good point, so that doesn't work.

Not sure whether it's better to disallow variable-sized stackalloc in the semantics (by evaluating the expr in an empty env) or in the compiler's stack usage analyzer, but at least now we've "considered" more than one option 🤷‍♂️ 😉
Do you think, like Linus, that variable-length arrays are "ACTIVELY STUPID"?

[andres-erbsen]

I don't intend to use VLAs, but with appropriate memory-safety proofs I don't see it as my duty to stop others from using them. 🤷. I think the interesting cases in this LKML thread have a bounded but variable allocation, and the desired behavior is to allocate up to the bound without considering runtime variation. If we wanted to have really nice support for this case, we'd generate a <= obligation and then have mStack have the runtime size from the perspective of the program logic. I don't feel particularly called to implement this either.

Perhaps the n mod bytes_per_word = 0 restriction also belongs to the compiler-specific precondition?

[samuelgruetter]

Perhaps the n mod bytes_per_word = 0 restriction also belongs to the compiler-specific precondition?

Ah yes, that would make more sense, but actually, at this point, it would probably be a similar amount of work to simply lift this restriction altogether...