A NullPointerException is thrown when detecting data races in Linux 4.0

[Tuo Li]

Hello all,

I have tried to detect data races in the Linux kernel with -lockator-linux for several days.

At first, I used CPAChecker to check Linux 6.2, but got an parsing error, and so I turned to an older version Linux 4.0. But I have got a new problem.

I first ran make allyesconfig at the root of the kernel tree, and then preprocessed the source file namei.c with make fs/ext2/namei.i, after which I tan the following command:

scripts/cpa.sh -lockator-linux fs/ext2/namei.i

but a NullPointerException is thrown:

Exception in thread "main" java.lang.NullPointerException: at index 0
at com.google.common.collect.ObjectArrays.checkElementNotNull(ObjectArrays.java:232)
at com.google.common.collect.ObjectArrays.checkElementsNotNull(ObjectArrays.java:222)
at com.google.common.collect.ObjectArrays.checkElementsNotNull(ObjectArrays.java:216)
at com.google.common.collect.ImmutableList.construct(ImmutableList.java:353)
at com.google.common.collect.ImmutableList.copyOf(ImmutableList.java:265)
at org.sosy_lab.cpachecker.cfa.ast.AFunctionCallExpression.<init>(AFunctionCallExpression.java:34)
at org.sosy_lab.cpachecker.cfa.ast.c.CFunctionCallExpression.<init>(CFunctionCallExpression.java:28)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convert(ASTConverter.java:1349)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convertExpressionWithSideEffectsNotSimplified(ASTConverter.java:464)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convertExpressionWithSideEffects(ASTConverter.java:437)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convertExpressionToStatement(ASTConverter.java:1745)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convert(ASTConverter.java:1741)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.handleExpressionStatement(CFAFunctionBuilder.java:691)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.visit(CFAFunctionBuilder.java:633)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTExpressionStatement.accept(CASTExpressionStatement.java:68)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTCompoundStatement.accept(CASTCompoundStatement.java:89)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTFunctionDefinition.accept(CASTFunctionDefinition.java:141)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFABuilder.handleFunctionDefinition(CFABuilder.java:407)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFABuilder.createCFA(CFABuilder.java:355)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.buildCFA(EclipseCParser.java:338)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.parseSomething(EclipseCParser.java:130)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.parseString(EclipseCParser.java:149)
at org.sosy_lab.cpachecker.cfa.CParserWithLocationMapper.parseFiles(CParserWithLocationMapper.java:215)
at org.sosy_lab.cpachecker.cfa.CFACreator.parseToCFAs(CFACreator.java:723)
at org.sosy_lab.cpachecker.cfa.CFACreator.parseFileAndCreateCFA(CFACreator.java:494)
at org.sosy_lab.cpachecker.core.CPAchecker.parse(CPAchecker.java:454)
at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:319)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:170)

I have no idea about what happend, and any feedback will be appreciated!

The preprocessed source file is attached with this email.

Sincerely,

Tuo Li

[Philipp Wendler]

Dear Tuo Li,

Am 21.09.23 um 13:09 schrieb Tuo Li:

> I tan the following command:
>
> scripts/cpa.sh -lockator-linux fs/ext2/namei.i
>
> but a NullPointerException is thrown:

Thank you for reporting this bug!
I have fixed it now in the latest development version of CPAchecker.

However, unfortunately CPAchecker is still not able to parse your
program due to this missing feature:
https://gitlab.com/sosy-lab/software/cpachecker/-/issues/1144
Furthermore, I have also noticed that the following feature is also
necessary for parsing your program:
https://gitlab.com/sosy-lab/software/cpachecker/-/issues/547

Are you interested in contributing to these?
I cannot promise that we get around to implementing them ourselves soon.

Kind regards
Philipp

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