c-parser: add support for _Static_assert statements #917

midnightveil · 2025-08-15T07:58:07Z

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).

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]( https://github.com/seL4/seL4/blob/13.0.0/include/assert.h#L45-L69). Signed-off-by: julia <midnight@trainwit.ch>

lsf37 · 2025-08-25T08:58:30Z

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?

lsf37 · 2025-08-25T09:00:10Z

tools/c-parser/program_analysis.ML

+  (* nothing to be done *)
+  (* XXX: like process_enumdecl, use const_eval on the condition to check it? *)
+  | StaticAssertion {...} => (puredecl d, e)


I guess this is the main question we have to decide on. I think we should stay with the "do nothing", but I'm keen to hear arguments for/against.

lsf37 · 2025-08-25T09:07:13Z

tools/c-parser/testfiles/static_assert.c

+_Static_assert(2 + 3 == 5, "Hello");
+
+// struct hello {
+//   _Static_assert(4 + 4 == 8, "Goodbye");
+// }


I'd like to see a few more tests, since the parser is correctness critical for architectures without binary verification.

If this can happen anywhere where we can have a declaration, we should at least add one inside a function body. Anything else that would make sense?

We're generally not so good with negative tests for the parser, but it would be worth adding a few to the testfiles/errors directory for this one. E.g. one where the _Static_assert has content that does not parse (in either of the arguments, maybe also 0, 1, and > 2 arguments), and one where _Static_assert as a whole occurs in a position it is not supposed to occur.

lsf37 · 2025-08-25T09:08:58Z

tools/c-parser/testfiles/static_assert.thy

+context static_assert
+begin
+
+end
+end


If we're adding a function body to the test, then we can add a thm f_body_def statement here to check that the function body has been defined. In this case it even make sense to state a lemma that shows that it is the expected function body so that the test confirms that the assert has been ignored (with a comment that this is what it does).

lsf37 · 2025-08-25T09:11:30Z

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.

lsf37 · 2025-08-25T09:17:42Z

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.

midnightveil · 2025-08-25T09:29:23Z

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.

midnightveil · 2025-08-25T09:45:08Z

tools/c-parser/StrictC.grm

+(* constant-expression is modelled as rexpression (c.f. "enumerator") *)
+static_assert_declaration
+: STATIC_ASSERT LPAREN rexpression YCOMMA cstring_literal RPAREN YSEMI
+                (wrap(StaticAssertion { condition = rexpression, message = cstring_literal }, eleft rexpression, eright rexpression))


I just realised that I forgot to go back and change this, the span for this should probably be STATIC_ASSERTleft and RPARENright not eleft/eright of the rexpression.

You're quoting from a C standard; you should say which one, otherwise people will expect C99.

Also, lines too long; this file tries to be 80 wide modulo minor spillage.

Xaphiosis · 2025-08-25T23:46:20Z

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.

Xaphiosis · 2025-08-25T23:56:47Z

tools/c-parser/StrictC.grm

                    sdecls)
                 end)
+(* per the C11 spec this should be allowed but let's not for simplicity *)
+(* | static_assert_declaration () *)


What is the issue here? If we're putting functionality in, but not putting in all of it, would be good to know why.

Nothing really, and it's probably pretty easy to do.

I was leaving it out because the kernel doesn't use _Static_assert in these positions (i.e. inside a struct) so I didn't see the point (I only learned that this was even possible reading the C spec last year or so, it's not commonly known either).

lsf37 reviewed Aug 25, 2025

View reviewed changes

lsf37 requested review from Xaphiosis and corlewis August 25, 2025 09:11

lsf37 added the C-parser anything about the C/Simpl parser label Aug 25, 2025

midnightveil commented Aug 25, 2025

View reviewed changes

Xaphiosis reviewed Aug 25, 2025

View reviewed changes

c-parser: add support for _Static_assert statements #917

Are you sure you want to change the base?

c-parser: add support for _Static_assert statements #917

Uh oh!

Conversation

midnightveil commented Aug 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

lsf37 commented Aug 25, 2025

Uh oh!

lsf37 Aug 25, 2025

Choose a reason for hiding this comment

Uh oh!

lsf37 Aug 25, 2025

Choose a reason for hiding this comment

Uh oh!

lsf37 Aug 25, 2025

Choose a reason for hiding this comment

Uh oh!

lsf37 commented Aug 25, 2025

Uh oh!

lsf37 commented Aug 25, 2025

Uh oh!

midnightveil commented Aug 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

midnightveil Aug 25, 2025

Choose a reason for hiding this comment

Uh oh!

Xaphiosis Aug 25, 2025

Choose a reason for hiding this comment

Uh oh!

Xaphiosis commented Aug 25, 2025

Uh oh!

Xaphiosis Aug 25, 2025

Choose a reason for hiding this comment

Uh oh!

midnightveil Aug 26, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

midnightveil commented Aug 15, 2025 •

edited

Loading

midnightveil commented Aug 25, 2025 •

edited

Loading