Feature #11444
closed
Added by Evgeny Novikov about 2 years ago.
Updated almost 2 years ago.
Description
We had several updates of CPAchecker SMG in Klever 3.4 (#10998), but we could not switch to trunk since Anton did not transfer all changes from his development branch to trunk. Let's hope that this will be done for Klever 3.5.
SMGCPA will provide ability to specify names of functions with behavior of mem*() functions to solve problem with definitions in new versions of the Linux kernel (for instance, you can see at include/linux/fortify-string.h of Linux 5.17). Estimation time for implementation is 2 days.
Merge development branch to trunk of CPAChecker is temporary unavailable.
Problem with definitions of mem*() functions is solved with new configuration options for SMGCPA:
cpa.smg.allocaFunctions = {"__builtin_alloca"}
cpa.smg.memcpyFunctions = {"memcpy"}
cpa.smg.memsetFunctions = {"memset"}
with combination of previous options:
cpa.smg.memoryAllocationFunctions = {"malloc", "__kmalloc", "kmalloc", "realloc"}
cpa.smg.arrayAllocationFunctions = {"calloc"}
cpa.smg.externalAllocationFunction = {"ext_allocation"}
cpa.smg.deallocationFunctions = {"free"}
cpa.smg.zeroingMemoryAllocation = {"calloc", "kzalloc"}
- Status changed from New to Resolved
Preliminary tests demonstrated that it works! So I updated CPAchecker SMG and added necessary models in the same branch support-linux-5.17 as for blocked issue #11459. Let's see on testing results.
- Status changed from Resolved to Open
Further testing confirmed that it does work. So I merged the mentioned branch to master in 1633a0f37. We still may want to update CPAchecker for Klever 3.5 since Anton promised to optimize it substantially.
- Status changed from Open to Resolved
After Anton optimized CPAchecker, I updated it in branch update-cpachecker and launched CI tests as well as extended testing on ~2000 drivers of Linux 5.5/5.17. Let's see on results.
- Status changed from Resolved to Closed
CI did not demonstrate any noticeable changes except for some small speedup, but SMG related verification tasks constitute a relatively small share of all verification tasks there.
There were such changes at verification of ~2000 drivers of Linux 5.5:
- The overall CPU time consumption almost did not change. BTW, ~70% of it comprises timeouts while there are a lot of timeouts still (448 instead of former 462).
- 12 timeouts became safes and 3 timeouts became unsafes. It took much CPU time (near the limit) to find those safes and unsafes.
Almost the same changes happened at verification of ~2000 drivers of Linux 5.17-rc1. The only important difference that there are more timeouts by some unknown reason (596 and 610 before and after update of CPAchecker correspondingly) and the overall CPU time consumption is ~1.2 times more in comparison with Linux 5.5. But that's another story.
I merged branch update-cpachecker to master in d18298301.
Also available in: Atom
PDF