Project

General

Profile

Actions
Copy link

Feature #10488

closed

Develop models for devm memory allocating functions

Added by Evgeny Novikov about 4 years ago. Updated about 4 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Evgeny Novikov
Category:
Environment models
Target version:
3.0
Start date:
09/03/2020
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

At the moment there just models for devm_kzalloc and devm_iio_device_alloc used for checking memory safety. Those models are not accurate since allocated memory is not tracked by CPAchecker SMG.

I suggest to develop accurate models that will cause a verifier to track the memory. In addition, they will store pointers to allocated memory within a global list, but just for memory safety checking since lists are too complicated for reachability checking.

Actions
Copy link
 #1

Updated by Evgeny Novikov about 4 years ago

  • Status changed from New to Resolved

I implemented models in branch devm-alloc-models. Since they are quite important, I will perform several large experiments for evaluation.

Actions
Copy link
 #2

Updated by Evgeny Novikov about 4 years ago

  • Status changed from Resolved to Closed

Surprisingly new models demonstrated numerous problems with verifiers. Likely this is the case because of corresponding functions are quite popular in the Linux kernel.

CPAchecker BAM started to fail sometimes. Besides, it reported timeouts rather than finding some good results even when models do not affect corresponding verification tasks.

CPAchecker SMG works much worse. It started to produce plenty of new false alarms due to inaccurate analysis of predicates, lack of type attributes support and so on.

Despite bad verification results I merged the branch to master:018aa6a68 with hope that one day CPAchecker developers will fix crucial issues within their tool.

Actions
Copy link

Also available in: Atom PDF