Skip to content

Conversation

@jprotopopov-ut
Copy link
Collaborator

Adds a stub for __context__ builtin of Linux kernel Sparse semantic checker.

https://sparse.docs.kernel.org/en/latest/annotations.html#context-ctxt-entry-exit

@jprotopopov-ut jprotopopov-ut requested a review from sim642 January 14, 2026 08:12
Comment on lines +4438 to +4440
else if isSparseBuiltin then
let one = Const(CInt(cilint_of_int 1, IInt, None)) in
(empty, one, intType)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it really necessary to replace it with an arbitrary constant 1?
Why does it need to be handled in CIL? Couldn't it just remain as a normal function call that's added to Goblint's LibraryFunctions?

Or alternatively, wouldn't it be enough to introduce initSparseBuiltins like

cil/src/cil.ml

Line 2903 in e21285a

let initGccBuiltins () : unit =
if it needs an implicit declaration and a signature?
Most builtins are not specifically handled here, only the ones that really have to do something at compile time. But this __context__ doesn't seem to require anything like this.

@sim642 sim642 added this to the 2.1.0 milestone Jan 14, 2026
@jprotopopov-ut jprotopopov-ut marked this pull request as draft January 14, 2026 12:04
@jprotopopov-ut
Copy link
Collaborator Author

If I remember correctly, this built-in appeared in rather inconvenient places (e.g. function declarations), but at the moment I cannot find suitable examples. Once the other pull requests are dealt with, I will try to convert it into a library function to see whether it suffices. For now, converting into a draft.

@sim642
Copy link
Member

sim642 commented Jan 14, 2026

If I remember correctly, this built-in appeared in rather inconvenient places (e.g. function declarations), but at the moment I cannot find suitable examples.

From what I gathered, there's two flavors of this (https://elixir.bootlin.com/linux/v6.19-rc5/source/include/linux/compiler_types.h#L55-L61):

  1. Function declaration attributes. CIL should have no problem with these being present: they should be parsed by the general __attribute__ logic and just carried around.
  2. The __context__ "function" calls within function bodies. I guess __context__ is never declared/defined as anything but just supposed to directly stay around for Sparse. I suppose CIL might complain that __context__ is an undeclared identifier, in which case the builtins list might just help.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants