Add frontend support for some constructs used in the Linux kernel #1798

fbrausse · 2024-04-25T12:03:01Z

This PR adds a new command-line option --include-file mapping to the -include option for Clang (also supported by GCC), which the kernel uses to include certain headers before the actual source code being translated. For now I'm testing this on drivers/cxl/pci.c via the following command line, corresponding to the (relevant) flags used by kernel's build system itself:

esbmc /usr/src/linux/drivers/cxl/pci.c -I /usr/src/linux/arch/x86/include/ -I /usr/src/linux/arch/x86/include/generated/  -I /usr/src/linux/include -I /usr/src/linux/arch/x86/include/uapi -I /usr/src/linux/arch/x86/include/generated/uapi -I /usr/src/linux/include/uapi -I /usr/src/linux/include/generated/uapi --include-file /usr/src/linux/./include/linux/compiler-version.h --include-file /usr/src/linux/./include/linux/kconfig.h --include-file /usr/src/linux/./include/linux/compiler_types.h  -D__KERNEL__ -DMODULE -DKBUILD_BASENAME='"pci"' -DKBUILD_MODNAME='"cxl_pci"' -D__KBUILD_MODNAME=kmod_cxl_pc

Additionally clang-c frontend support for features used in that driver (and its included headers):

declared-only enum types as return value of function pointers (poorly, that's why I'd keep C Frontend fails to convert forward-declared enum type as part of fn-signature #1794 open for now),
__builtin_choose_expr(), fixes C frontend does not support clang::ChooseExpr #1796,
dynamic members in offsetof(), fixes C frontend does not support __builtin_offsetof() with dynamic member expression #1797, and
clang::AttributedStmt such as [[fallthrough]].

With these changes, I'm now finally getting

ERROR: main symbol `main' not found

i.e., the C frontend handles all constructs in the unmodified kernel's CXL driver's "pci.c" file.

src/clang-c-frontend/clang_c_convert.cpp

mikhailramalho

I would prefer the handling of the builtin offset to be done in the adjust code, but I guess we'll loose the information about the node, so LGTM

lucasccordeiro · 2024-04-25T13:09:07Z

Thanks, @fbrausse. Could you please run this PR over the SV-COMP benchmarks?

fbrausse · 2024-04-25T13:27:23Z

I would prefer the handling of the builtin offset to be done in the adjust code, but I guess we'll loose the information about the node, so LGTM

Indeed it would be better to have this as a separate exprt, not just in order to move it to the adjuster, but also because basically we already have this functionality implemented in the function compute_pointer_offset(). In addition, as the dynamic offsetof isn't handling the C++ base class member case right now, we could factor it out into a separate method so the C++ frontend can override it. Can we leave that for another PR, though? I'll add a TODO.

mikhailramalho · 2024-04-25T13:38:32Z

Yeah, and I think we merge base class methods/attributes to derived classes in our irep, so it might be tricky to get that working on compute_pointer_offset() Em qui., 25 de abr. de 2024 às 10:27, Franz Brauße ***@***.***> escreveu:

…

I would prefer the handling of the builtin offset to be done in the adjust code, but I guess we'll loose the information about the node, so LGTM Indeed it would be better to have this as a separate exprt, not just in order to move it to the adjuster, but also because basically we already have this functionality implemented in the function compute_pointer_offset(). In addition, as the dynamic offsetof isn't handling the C++ base class member case right now, we could factor it out into a separate method so the C++ frontend can override it. Can we leave that for another PR, though? I'll add a TODO. — Reply to this email directly, view it on GitHub <#1798 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKEJH2IJHVAOETZGWOFGULY7EAFFAVCNFSM6AAAAABGYXNBCWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANZXGE4DAMZZHA> . You are receiving this because your review was requested.Message ID: ***@***.***>

-- Mikhail R. Gadelha, Ph.D.

fbrausse · 2024-04-27T06:15:19Z

Master:

Statistics:          23805 Files
  correct:           15336
    correct true:     8701
    correct false:    6635
  incorrect:            50
    incorrect true:     18
    incorrect false:    32
  unknown:            8419
  Score:             22949 (max: 38482)

https://github.com/esbmc/esbmc/actions/runs/8849874090

This PR:

Statistics:          23805 Files
  correct:           15328
    correct true:     8702
    correct false:    6626
  incorrect:            50
    incorrect true:     18
    incorrect false:    32
  unknown:            8427
  Score:             22942 (max: 38482)

https://github.com/esbmc/esbmc/actions/runs/8852150400

…de' option

Addresses #1794.

Fixes #1796.

…_compatible_p()

Fixes #1797.

lucasccordeiro · 2024-04-27T06:20:06Z

Thanks for submitting this PR, @fbrausse.

fbrausse changed the title ~~Add support for some constructs used in the Linux kernel~~ Add frontend support for some constructs used in the Linux kernel Apr 25, 2024

lucasccordeiro requested review from mikhailramalho, rafaelsamenezes and XLiZHI April 25, 2024 12:38

rafaelsamenezes approved these changes Apr 25, 2024

View reviewed changes

src/clang-c-frontend/clang_c_convert.cpp Show resolved Hide resolved

mikhailramalho approved these changes Apr 25, 2024

View reviewed changes

lucasccordeiro approved these changes Apr 25, 2024

View reviewed changes

fbrausse force-pushed the fb/cxl branch 3 times, most recently from a545a5c to 77f3df8 Compare April 26, 2024 10:11

rafaelsamenezes force-pushed the fb/cxl branch from 77f3df8 to e7731d3 Compare April 26, 2024 17:38

fbrausse added 9 commits April 27, 2024 07:19

[options] add --include-file, which gets just mapped to Clang '-inclu…

513aaf1

…de' option

[clang-c] convert: handle enum decl-only types (poorly)

268f801

Addresses #1794.

[clang-c] convert: format comment

97bc3fe

[clang-c] convert: support __builtin_choose_expr()

41fa256

Fixes #1796.

[clang-c] type trait exprs can also return int, e.g., __builtin_types…

d3806b0

…_compatible_p()

[clang-c] convert: support offsetof() with dynamic member expression

1c451fb

Fixes #1797.

[clang-c] convert: support AttributedStmt such as [[fallthrough]]

d933a5c

[clang-c] convert: add docs for clang::ChooseExpr

f372e68

[clang-c] convert: document offsetof() conversion

6192e6b

lucasccordeiro force-pushed the fb/cxl branch from e7731d3 to 6192e6b Compare April 27, 2024 06:19

lucasccordeiro merged commit f0cca1a into master Apr 27, 2024
10 checks passed

lucasccordeiro deleted the fb/cxl branch April 27, 2024 06:19

fbrausse mentioned this pull request Apr 27, 2024

C Frontend fails to convert forward-declared enum type as part of fn-signature #1794

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add frontend support for some constructs used in the Linux kernel #1798

Add frontend support for some constructs used in the Linux kernel #1798

fbrausse commented Apr 25, 2024

mikhailramalho left a comment

lucasccordeiro commented Apr 25, 2024

fbrausse commented Apr 25, 2024

mikhailramalho commented Apr 25, 2024 via email

fbrausse commented Apr 27, 2024

lucasccordeiro commented Apr 27, 2024

Add frontend support for some constructs used in the Linux kernel #1798

Add frontend support for some constructs used in the Linux kernel #1798

Conversation

fbrausse commented Apr 25, 2024

mikhailramalho left a comment

Choose a reason for hiding this comment

lucasccordeiro commented Apr 25, 2024

fbrausse commented Apr 25, 2024

mikhailramalho commented Apr 25, 2024 via email

fbrausse commented Apr 27, 2024

lucasccordeiro commented Apr 27, 2024