Parsing failed when checking Linux 6.2 with -lockator-linux

[Tuo Li]

Hi,

I have tried to detect data races in Linux 6.2 with -lockator-linux, but I have got into some problems.

I first preprocessed source code of the Linux 6.2, and then I used the following command to detect data races in the preprocessed source code:

scripts/cpa.sh -lockator-linux linux_source/fs/crypto/fname.my.i

but I got the following Error:

Error: Parsing failed (lines 48893-48895: Initializer of global variable has side effect: struct kernfs_global_locks {
 struct mutex open_file_mutex[(1 << (2 * (( __builtin_constant_p(8192 < 32 ? 8192 : 32) ? ((8192 < 32 ? 8192 : 32) < 2 ? 0 : 63 - __builtin_clzll(8192 < 32 ? 8192 : 32)) : (sizeof(8192 < 32 ? 8192 : 32) <= 4) ? __ilog2_u32(8192 < 32 ? 8192 : 32) : __ilog2_u64(8192 < 32 ? 8192 : 32) ))))];
};) (EclipseCParser.buildCFA, SEVERE)

The file fname.my.i is attached in this email.

I wonder about the appropriate way to run CPAChecker on some projects such as Linux. Any feedback will be appreciated!

Thanks,

Tuo Li

[Pavel Andrianov]

Dear Tuo Li,

First of all, thank you for the interest in the CPAchecker framework and the CPALockator tool.

It is not so easy to run CPAchecker (or even other verification tool) on the Linux kernel code. Particularly, due to issues with EclipseCParser, which you also found. There is an LDV project [1], which applies verification techniques to the Linux kernel. And we are using the Klever framework [2] to prepare verification tasks for a verifier tool. Klever performs different steps, including code simplification and environment model generation. And its output verification task is usually successfully analyzed by CPAchecker. One more benefit from the Klever framework is its ability to visualize warnings, which are found by the verifiers.

Towards CPALockator (option -lockator-linux). The main functionality was not still merged into trunk. And the latest version can be found in [3], which significantly differs from the trunk version.

Actually, I could say nothing about the initial issue with EclipseCParser. Guess, this is just one more problem with the parser.

Best regards,
Pavel

1: https://linuxtesting.org
2: https://forge.ispras.ru/projects/klever
3: https://gitlab.ispras.ru/verification/cpachecker/-/tree/cpalockator-master

четверг, 21 сентября 2023 г. в 07:20:51 UTC+3, Tuo Li:

[Philipp Wendler]

Dear Tuo Li,

Am 21.09.23 um 06:20 schrieb Tuo Li:

> I first preprocessed source code of the Linux 6.2, and then I used the
> following command to detect data races in the preprocessed source code:
>
> scripts/cpa.sh -lockator-linux linux_source/fs/crypto/fname.my.i
>
> but I got the following Error:
>
> Error: Parsing failed (lines 48893-48895: Initializer of global variable
> has side effect: struct kernfs_global_locks {
> struct mutex open_file_mutex[(1 << (2 * (( __builtin_constant_p(8192 < 32
> ? 8192 : 32) ? ((8192 < 32 ? 8192 : 32) < 2 ? 0 : 63 - __builtin_clzll(8192
> < 32 ? 8192 : 32)) : (sizeof(8192 < 32 ? 8192 : 32) <= 4) ?
> __ilog2_u32(8192 < 32 ? 8192 : 32) : __ilog2_u64(8192 < 32 ? 8192 : 32)
> ))))];
> };) (EclipseCParser.buildCFA, SEVERE)
>
> The file fname.my.i is attached in this email.

The problem here is that function calls inside initializers of global
variables are typically not allowed, and it just works here because the
compiler evaluates the function call during compilation.
So we have to add support for __builtin_clzll, __ilog2_u32, and
__ilog2_u64 as well to CPAchecker (the other functions should already work).

This should not be too difficult, but I cannot promise that we get to
implement it soon. Would you be interested in contributing this? I can
provide a pointer where to start.

Kind regards
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181