Klever

I updated CPAchecker in branch update-cpachecker. Let's see on various testing results.

• 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.

Anton has fixed some negative regressions, so I restarted CI.

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.

One more update of CPAchecker that should fix the issue is in the same branch. Let's see on testing results.

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)

Anton has fixed the new issue, so I updated CPAchecker one more time and restarted CI.

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.