seL4
c-parser: add support for _Static_assert statements
The kernel AST now produces statements like:
##StaticAssertion: long_is_32bits
StaticAssertion [
"long_is_32bits"
BinOp [
"=="
SizeofTy [
Unsigned [
"long"
],
],
Constant [
NUMCONST [
"4"
""
"DEC"
],
],
],
],
This should allow the horrible array size hack to be removed from the kernel source code, i.e. include/assert.h.
Was this necessary? No Was this interesting? Yes Was this fun? Uhhh well I want to do more of it
It doesn't seem like any of the kernel proofs actually proved anything against the static asserts, so this should be fine. (I ran the proofs locally after making all the static assertions false and they still succeeded, so I think only the compiler checks these).
I've no idea how to write an appropriate test, aside from that it parses.
I also have a similar one for offsetof, but I don't want to trigger the CI builds unnecessarily by making another PR (for the moment, at least).
Hm, I'm not sure about this one. On the one hand it'd be nice to not just fail on _Static_assert and to be able to use it in the kernel. From that direction, yes, we should do this. On the other hand, the parser is for C99 and the verification also does not see any of the other C assertions, so adding a non-C99 construct and in particular an assertion into the parser is strange.
For one, it immediately throws up the question that you hit what to do with those assertions. Do we prove them? Do we evaluate them in the parser? Do we error on the parse because a static assertion failed? Compilation is quick, translating seL4 into Isabelle is not quick, so failing can become extremely annoying.
I guess the most consistent approach would be to allow the parse, and then ignore the assert. If I understand the PR correctly, this is what it is currently doing (parse as declaration, but not adding any types).
(Also, I'm impressed that you managed to add this without too much trouble, people seem to be very afraid of touching this code in general :))
@Xaphiosis @corlewis What are your opinions?
If we add this, we should also add a remark to doc/ctranslation.tex that the parser handles and ignores _StaticAssert. Probably needs a new section somewhere close to the GCC attributes.
I also have a similar one for offsetof, but I don't want to trigger the CI builds unnecessarily by making another PR (for the moment, at least).
Does clang support the same attribute the same way? Our own requirements are GCC first, clang later, but there are other people using the parser mostly on clang code. We don't have much attribute support currently, but if we add more that might become relevant.
Does clang support the same attribute the same way?
Yeah, it does (or at least recent-ish clang do); the API is basically that of the C11 offsetof header.
Broadly speaking, yeah I agree with your concerns.
I mostly did this for fun, but it would be nice to bring in more of the used subset into the parser; this is the only use of CONFIG_VERIFICATION_BUILD in seL4's c code itself (iirc)
And I think there's an open issue regarding what to support on the parser. we have quirks like tb SEL4_LONG_ENUM which aren't technically c99 compatible, but there's some things regarding "do the compilers support it anyway" that was discussed. But I don't think that was resolved.
Impressive you felt like doing this, and even more so that you got something to work.
Gerwin's covered the main areas, especially tests. Nitpicks: when dealing with other code bases, try to blend in with comment style etc, and if we're going to keep this and the tests, it would be good if they were more targeted/informative (e.g. "False assertion in global scope" / "Commented out" instead of "Hello").
The main thing to discuss is what this gives us. We'd be including a part of C11 into the C parser, arguing that in C99 gcc/clang implement it already, and doing so most likely so that verification can ignore it. The benefit is that an seL4 include file won't need the funky assert.h dance, nicer assertions will appear in the source code of the verified kernel, and (of dubious benefit) in the AST.
We have had (sometimes fiery) discussions about the C parser supporting a subset of C99 vs becoming some kind of Frankenstein's monster, with C99 usually winning. We do have the --underscore_idents C parser option, but that is gated behind an option. I think if we are to violate the C99 standard, it should also be gated behind an option (--static-asserts / --drop-static-asserts?). Also, this is also not the only branch of the C parser in existence, given AutoCorres2 is out there, but I don't know if they'd be interested in picking these up.
When it comes to what do we do with the assertions, I'm on the side of discarding them in verification. The "ideal" thing to have is the C parser checking them during a parse (also so that standalone-parser would be able to do it, and verification never picks them up), but that's way too much work. It makes more sense to compile the code instead, and don't bother with verification if it doesn't compile. I don't think it benefits us in CRefine to have any of these assertions around (in function scope, do we have to prove them? assume them? step over them with csymbr? eliminate them with ccorres_rewrite?).
In summary, I'm reluctantly ok with this if it's gated behind an option and we don't need to prove or step over function-scope static asserts, provided it's properly documented+tested.
For offsetof it's going to be the same story (sanctifying an implementation-defined macro with a specific definition not in the standard). The C parser should have all the type info, but I'd want to make sure it's quite stable, e.g. that it doesn't barf on a forward-declared struct etc, and we'd need to put in a proof or two to show it actually calculates the correct result.
