Project

General

Profile

Actions
Copy link

Feature #11444

closed

Update CPAchecker SMG

Added by Evgeny Novikov about 2 years ago. Updated almost 2 years ago.

Status:
Closed
Priority:
High
Assignee:
Evgeny Novikov
Category:
Addons
Target version:
3.5
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
Copy link
 #1

Updated by Evgeny Novikov about 2 years ago

Actions
Copy link
 #2

Updated by Anton Vasilyev about 2 years 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
Copy link
 #3

Updated by Anton Vasilyev about 2 years 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
Copy link
 #4

Updated by Evgeny Novikov about 2 years 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
Copy link
 #5

Updated by Evgeny Novikov almost 2 years ago

Actions
Copy link
 #6

Updated by Evgeny Novikov almost 2 years 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
Copy link
 #7

Updated by Evgeny Novikov almost 2 years 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
Copy link
 #8

Updated by Evgeny Novikov almost 2 years 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
Copy link

Also available in: Atom PDF