Project

General

Profile

Edit History

LDV Validator » History » Version 6

Vadim Mutilin, 02/12/2014 01:03 PM

1 1 Evgeny Novikov 
h1. LDV Validator
2 





    3
    5
    Evgeny Novikov
    
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 can miss bugs during verification in production. So we have reasons to revise LDV Tools or/and verifiers (sometimes we can have bugs in specifications as well).





    4
    1
    Evgeny Novikov
    





    5
    
    
    
h2. Sources of programs with known bugs





    6
    
    
    





    7
    3
    Alexey Khoroshilov
    
One of the simplest approaches 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
    6
    Vadim Mutilin
    
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 thousand commits made to "stable branches of the Linux kernel":http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/ since 26-10-2010 till 26-10-2011. This allowed us to find about 200 bugs 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. 





    10
    4
    Evgeny Novikov
    





    11
    
    
    
h2. LDV Validator workflow





    12
    
    
    





    13
    
    
    
LDV Validator gets a configuration file as input and automatically launches LDV Tools with specified verifier, obtains verification results and generates a report where one can find summary information 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.