Feature #11772
closedUpdate CPAchecker
0%
Description
Anton just rebased his branch on the latest trunk, so we need to update CPAchecker in Klever and test it thoroughly.
Updated by Evgeny Novikov 8 months ago
- Status changed from New to Resolved
I updated CPAchecker in branch update-cpachecker. Let's see on various testing results.
Updated by Evgeny Novikov 8 months ago
- Status changed from Resolved to Open
- Memory safety:
- 2 safes -> 2 timeouts.
- 2 unsafes (target bug and false alarm) -> 2 timeouts.
- Non-memory safety:
- 3 unsafes (target bug and 2 false alarms) -> 3 timeouts.
It is necessary to figure out reasons of bad regressions at least for memory safety and fix them if possible.
Updated by Evgeny Novikov 8 months ago
- Status changed from Open to Resolved
Anton has fixed some negative regressions, so I restarted CI.
Updated by Evgeny Novikov 8 months ago
- Status changed from Resolved to Open
CI demonstrated numerous degradations. It seems that many (all) of them are caused by the same reason, so I hope that some fix will get rid of them.
Updated by Evgeny Novikov 8 months ago
- Status changed from Open to Resolved
One more update of CPAchecker that should fix the issue is in the same branch. Let's see on testing results.
Updated by Evgeny Novikov 8 months ago
- Status changed from Resolved to Open
The old issue has gone, but CI revealed a new large group of degradations that seem to stem from the same root cause:
Exception in thread "main" java.lang.NullPointerException at java.base/java.util.ArrayList.<init>(Unknown Source) at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.evaluateArgumentValue(SMGTransferRelation.java:459) at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.evaluateArgumentValues(SMGTransferRelation.java:425) at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.handleFunctionCallEdge(SMGTransferRelation.java:342) at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.handleFunctionCallEdge(SMGTransferRelation.java:114) at org.sosy_lab.cpachecker.core.defaults.ForwardingTransferRelation.handleFunctionCallEdge(ForwardingTransferRelation.java:319) at org.sosy_lab.cpachecker.core.defaults.ForwardingTransferRelation.getAbstractSuccessorsForEdge(ForwardingTransferRelation.java:169) at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.callTransferRelation(CompositeTransferRelation.java:297) at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForSimpleEdge(CompositeTransferRelation.java:264) at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForEdge(CompositeTransferRelation.java:196) at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessors(CompositeTransferRelation.java:88) at org.sosy_lab.cpachecker.cpa.arg.ARGTransferRelation.getAbstractSuccessors(ARGTransferRelation.java:45) at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:334) at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(CPAAlgorithm.java:289) at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(CPAAlgorithm.java:260) at org.sosy_lab.cpachecker.core.algorithm.CounterexampleStoreAlgorithm.run(CounterexampleStoreAlgorithm.java:58) at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:512) at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:377) at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:170)
Updated by Evgeny Novikov 8 months ago
- Status changed from Open to Resolved
Anton has fixed the new issue, so I updated CPAchecker one more time and restarted CI.
Updated by Evgeny Novikov 8 months ago
- Status changed from Resolved to Closed
CI regressions are described in c8ffc39. Verification of a subset of Linux 5.19-rc7 drivers demonstrated a pretty good speedup. Now more safes and unsafes can be found instead of timeouts and suspicious false alarms. SMG can not reveal several hard-to-detect safes anymore, but improvements are more considerable. I merged the branch to master in c8ffc391c.
Updated by Evgeny Novikov 8 months ago
I forgot to mention that there is almost no changes for verification of those drivers against drivers:clk2.