Error when using LLVM frontend

[Yoel Kim]

Hi CPAchecker team,

I used -clang option to use LLVM frontend and executed CPAchecker with this option like:

```

$ bash scripts/cpa.sh -predicateAnalysis -clang doc/examples/example_bug.c
Running CPAchecker with default heap size (1200M). Specify a larger value with -heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed.
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 2.3.1-svn / predicateAnalysis (OpenJDK 64-Bit Server VM 17.0.10) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "doc/examples/example_bug.c" (CPAchecker.parse, INFO)

Exception in thread "main" java.lang.AssertionError: Unhandled cast of array type (const char)[56] to (signed int : 8)*
        at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.castToExpectedType(CFABuilder.java:1518)
        at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.getExpression(CFABuilder.java:1186)
        at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.handleCall(CFABuilder.java:816)
        at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.visitInstruction(CFABuilder.java:705)
        at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.handleInstructions(CFABuilder.java:585)
        at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.iterateOverBasicBlocks(CFABuilder.java:341)
        at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.iterateOverFunctions(CFABuilder.java:260)
        at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.visit(CFABuilder.java:180)
        at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.build(CFABuilder.java:163)
        at org.sosy_lab.cpachecker.cfa.parser.llvm.LlvmParser.buildCfa(LlvmParser.java:102)
        at org.sosy_lab.cpachecker.cfa.parser.llvm.LlvmParser.parseFile(LlvmParser.java:64)
        at org.sosy_lab.cpachecker.cfa.LlvmParserWithClang.parse0(LlvmParserWithClang.java:89)
        at org.sosy_lab.cpachecker.cfa.LlvmParserWithClang.parseSingleFile(LlvmParserWithClang.java:76)
        at org.sosy_lab.cpachecker.cfa.LlvmParserWithClang.parseFiles(LlvmParserWithClang.java:53)
        at org.sosy_lab.cpachecker.cfa.CFACreator.parseToCFAs(CFACreator.java:741)
        at org.sosy_lab.cpachecker.cfa.CFACreator.parseFileAndCreateCFA(CFACreator.java:505)
        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:171)

```
I also run $ clang-9 -S -emit-llvm doc/examples/example_bug.c -o example_bug.ll
and found that standard library calls with several arguments such as "assert(0)" and "printf("any")" lead to the same error above.

Is there any solution to avoid this error? (by configuring some options of clang?)

Regards,
Yoel Kim

[Thomas Lemberger]

Hi Yoel,

Thanks for your interest in CPAchecker and the report!

I fixed this issue in the latest trunk of CPAchecker: https://gitlab.com/sosy-lab/software/cpachecker

Can you please retry to check that it also works on your side?

Best,

Thomas

Am 20.03.2024 um 09:52 schrieb Yoel Kim <kimyo...@gmail.com>:

Hi CPAchecker team,

--
You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cpachecker-users/39c39ae3-2988-4e2e-9659-072438841d83n%40googlegroups.com.

<example_bug.ll>

[Yoel Kim]

Hi Thomas,

Yes, it works! 

Thank you.

Yoel Kim

2024년 3월 21일 목요일 오전 2시 58분 28초 UTC+9에 Thomas Lemberger님이 작성:

[Yoel Kim]

Hi Thomas,

I found another error while using LLVM.
Here is the code "test.c" that calls an external function "check".

When I ran CPAchecker with the following command $ bash scripts/cpa.sh -predicateAnalysis -preprocess test.c
then the result was valid.

However, when I ran it with the command  $ bash scripts/cpa.sh -predicateAnalysis test.ll
the result was

```
Inconsistent replayed error path! No variable values will be available. (PredicateCPA:PathChecker.createCounterexample, WARNING)

Exception in thread "main" java.lang.AssertionError: Found imprecise counterexample in PredicateCPA. If this is expected for this configuration (e.g., because of UF-based heap encoding), set counterexample.export.allowImpreciseCounterexamples=true. Otherwise please report this as a bug.
        at org.sosy_lab.cpachecker.util.predicates.PathChecker.createImpreciseCounterexample(PathChecker.java:255)
        at org.sosy_lab.cpachecker.util.predicates.PathChecker.createCounterexample(PathChecker.java:224)
        at org.sosy_lab.cpachecker.util.predicates.PathChecker.handleFeasibleCounterexample(PathChecker.java:179)
        at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performRefinementForPath(PredicateCPARefiner.java:314)
        at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performRefinementForPath(PredicateStaticRefiner.java:183)
        at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:158)
        at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:104)
        at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:310)
        at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:256)
        at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:507)
        at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:369)
        at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:172)

```


Regards,
Yoel 

2024년 3월 21일 목요일 오후 3시 35분 9초 UTC+9에 Yoel Kim님이 작성:

[Yoel Kim]

Here are the files

2024년 4월 9일 화요일 오후 9시 54분 13초 UTC+9에 Yoel Kim님이 작성:

[Thomas Lemberger]

Hi Yoel,

sorry for the late reply. CPAchecker's SMT-based analyses on LLVM use some more memory handling than the analysis of pure C code.
You can avoid your error by setting `-setprop counterexample.export.allowImpreciseCounterexamples=true`.

This _may_ produce invalid counterexamples in the output folder, but currently we have no better solution.

Hope this still helps.

Best,

Thomas