Project

General

Profile

Actions

Feature #1037

open

Why the LDV needs to compile drivers?

Added by Andrey Ponomarenko over 13 years ago. Updated over 13 years ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Start date:
04/06/2011
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

The LDV is a "static verification suite" according to the project description. Why it need to compile drivers? Is it possible to implement a special mode of the analysis without the drivers compilation? The ideal solution in my mind is to get all the *.c and *.h files from the driver package and statically check the source code for faults.

Actions #1

Updated by Evgeny Novikov over 13 years ago

My opinion is that at present and near future we won't do this. Instead we suggest that a developer checks a driver against a "correct" kernel with which the driver should be compilable.
Nevertheless we should keep in mind such the ability to check statically driver without any compilation and even without all kernel sources at all. However, I don't understand clearly how to do the last.

Actions #2

Updated by Pavel Shved over 13 years ago

Why stop at discarding kernel sources? Let's check the driver without its own source code! While I do not understand how to do it as well, with such feature implemented our framework would have an extremely easy-to-use interface!

Requiring a "correct kernel" is not what we do. We want the program to be built, and we watch the build process closely to extract the build commands from it. Without these commands, it's impossible to tell what exactly is executed when the program runs, preprocessing and modularization contributing to this implausibility the most. And it's the correctness of execution of the program we try to verify! We can't know what the final source looks like unless we follow the build process the driver developer intended.

As for compiling without the kernel, driver relies on kernel data structures as well as kernel functions. While the calls to the latter could just be ignored (like any unresolved function call is at the moment), inference of data structures by source code of the using program is beyond the scope of current work, and would require a lot of change into BLAST frontend. But it's not only BLAST what requires the input to be a correct C program: Aspectator, core of which are C code transformations, naturally require the program it instruments to be correct and full.

I think that static analysis tools will remain integrated with build process in the future, and we should to tighten this integration instead of trying to drop it.

Actions

Also available in: Atom PDF