Project

General

Profile

LDV Validator » History » Version 2

Alexey Khoroshilov, 10/11/2013 08:23 PM

1 1 Evgeny Novikov
h1. LDV Validator
2
3 2 Alexey Khoroshilov
LDV Validator is a tool for validating LDV Tools verification system, in particular its back ends, i.e. verifiers like "BLAST":http://forge.ispras.ru/projects/blast/ or "CPAchecker":http://cpachecker.sosy-lab.org/. An approach, implemented in LDV Validator, is that LDV Tools are tried to find some known bugs in programs. If known bugs can be found using appropriate "specifications":http://forge.ispras.ru/projects/ldv-rules, then we prove that LDV Tools and corresponding verifiers work good. Otherwise we have reasons to revise LDV Tools or/and verifiers (sometimes we can have bugs in specifications as well), since this means that we can miss bugs during verification in production.
4 1 Evgeny Novikov
5
h2. Sources of programs with known bugs
6
7 2 Alexey Khoroshilov
One of the simplest approach to get programs with bugs is to introduce these bugs by ourselves. We used this approach very widely in preparing "test cases":http://forge.ispras.ru/projects/ldv/repository/revisions/master/show/ldv-tests/rule-models/drivers for LDV tools specifications. Obviously, we can''t cover all possible situations with these test cases. Thus we need other sources of programs with known bugs for validating LDV Tools.
8 1 Evgeny Novikov
9
We found out that programs with known nonartificial bugs can be efficiently obtained on the basis of the Linux kernel repositories. We have "analyzed":http://linuxtesting.org/downloads/ldv-commits-analysis-2012.zip about 3 thousands of commits made to "stable branches of the Linux kernel":http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/. This allowed us to find about 400 of nonfunctional bugs. And about 50% of these bugs were related with Linux kernel API misuse - exactly those bugs which can be found with help of LDV Tools. Information on those bugs (commit hashes, module names, specification identifiers, etc.) was put to a configuration file. LDV Validator gets that file as input and automatically launches LDV Tools with specified verifier, obtains verification results and generates a report where you can find summary information on all known bugs as well as details on whether a particular bug was detected or not. Besides LDV Validator automatically checks Linux kernel modules after fixing bugs. This aids to understand whether LDV Tools or/and a verifier did find a bug fixed in corresponding commit.