detect and handle attribute `packed`

[lsf37]

The seL4 C code uses the GCC attributed packed for some structs that are not used in the proofs.

The C parser accepts and ignores the attribute. This is dangerous, because if the attribute is at some point accidentally used for a struct that is relevant for verification, the memory layout generated by the parser will be wrong (wrong offsets, overall size, and alignment, because the compiler will not add padding and the C parser will). Tom found the same issue during binary verification before: https://sel4.atlassian.net/browse/SELFOUR-1590

We should have some kind of check/mechanism for making sure packed is not used accidentally. We could try to forbid it completely, but that will conflict with existing code behind the machine interface and may not always be possible.

Maybe we C parser could recognise the attribute and make the structure unusable in Isabelle by not deriving any of the UMM properties. That would mean the corresponding functions are still translatable and will not fail the build, but we will not be able to prove anything about them unless we derive those properties manually. I'm not clear on what this would do to binary verification -- it would likely fail those functions, but they would have been failing before if the memory layout is not the same as the compiler has.

The other option would be to model packed properly, but that would mean a fairly large change, probably another type class for those kinds of structs, and all that for structs that we explicitly do not want to use in the proofs.

[Indanz]

Am I right in understanding that the main problem is that the proofs can't deal with unaligned accesses and memory layouts, even if the architecture supports it?

[lsf37]

Am I right in understanding that the main problem is that the proofs can't deal with unaligned accesses and memory layouts, even if the architecture supports it?

The proofs could relax/modify alignment conditions, although that would also be extremely annoying since they are currently uniform. The main problem is that the layout is just different and that would need to be modelled.

[Indanz]

The main problem is that the layout is just different and that would need to be modelled.

That is surprising to me, because we currently need to manually pad to avoid compiler padding, so I would have thought that the C parser takes the code as-is, exactly because it doesn't add padding itself.

[lsf37]

That is surprising to me, because we currently need to manually pad to avoid compiler padding, so I would have thought that the C parser takes the code as-is, exactly because it doesn't add padding itself.

It does add padding, but the semantics of C does not allow you to say much about what that padding does, in particular the compiler is allowed to write or not to write padding as it pleases with whatever content it pleases. This means that writing to a field via pointer to the field and writing to a field via pointer to the structure is not the same, and that is very unpleasant to work with. If the struct naturally has no padding, we can prove that it is the same.