Project

General

Profile

Actions

Feature #11444

closed

Update CPAchecker SMG

Added by Evgeny Novikov 6 months ago. Updated 4 months ago.

Status:
Closed
Priority:
High
Category:
Addons
Target version:
Start date:
02/22/2022
Due date:
% Done:

0%

Estimated time:
Published in build:

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.

Actions #1

Updated by Evgeny Novikov 4 months ago

Actions #2

Updated by Anton Vasilyev 4 months ago

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.

Actions #3

Updated by Anton Vasilyev 4 months ago

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"}

Actions #4

Updated by Evgeny Novikov 4 months ago

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

Actions #5

Updated by Evgeny Novikov 4 months ago

Actions #6

Updated by Evgeny Novikov 4 months ago

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

Actions #7

Updated by Evgeny Novikov 4 months ago

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

Actions #8

Updated by Evgeny Novikov 4 months ago

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

Actions

Also available in: Atom PDF