[ldv-project] [cif of ldv] -- does the cif deal with the system calls or interrupts?

[Evgeny Novikov]

Hello Lele and Jian,

this is actually the case, LDV does need a Linux operating system model 
as well as SDV. At the moment we have implemented just a small part of 
this model. The rest part of the model is considered as undefined. For 
instance, here 
(http://linuxtesting.ru/ldv/online?action=detailed_report&trace_id=195&number=22) 
you can see that call to spi_register_driver isn't actually "executed" 
inside wl12xx_init. So all possible return values of spi_register_driver 
are analyzed. The error trace visualized corresponds to the case when 
spi_register_driver returns 0 that allows to continue driver 
initialization and following processing.
Now we are actively investigated an approach to automatically extract 
Linux operating system model for some of our rules. For instance, this 
will allow to check might sleep functions in spinlock context. IMHO this 
is almost impossible to write full Linux operating system model since 
Linux API isn't stable and it's huge in comparison with the Microsoft 
Windows one.
As for CIF it just does what it's asked for, i.e. it applies aspects to 
driver source code. Nevertheless one can use CIF to obtain some 
knowledge about, say, Linux kernel source code, e.g. about whether a 
given function is might sleep or not.

Thank you for greetings! I also wish you Merry Christmas!

On 12/25/2012 12:29 PM, Jian Liu/ISCAS wrote:
> Lele,
>
>     To my knowledge, it should be needed to model some interfaces for driver
> routine function for static analysis Linux drivers, just like you said
> system calls or interrupts etc. For example, according to Microsoft's static
> driver verifier (SDV) team, they built ~39,170 lines of C code to implement
> an operating system model. I think LDV should contain such a model in their
> tool releases. But I do not know where is code and how to build such
> modeling interfaces automatically (maybe not automatically) in LDV. Wish
> Evgeny could help you.
>
>     Jian
>
>> -----Original Message-----
>> From: MA Lele [mailto:tupipa0929 at 126.com]
>> Sent: Tuesday, December 25, 2012 5:06 PM
>> To: Evgeny Novikov
>> Cc: ldv-project; Jian Liu
>> Subject: [cif of ldv] -- does the cif deal with the system calls or
> interrupts?
>>
>> Dear Evegeny Novikov,
>>
>> I'm very interested in how to deal with the system calls or interrupts when
> doing
>> instrumentation of a driver's source code.
>> Almost all drivers needs to do I/O or other kinds of communications with
> system
>> or other devices. So , there exists lots of systems calls or interrupt code
> in the
>> driver source . And some bugs may be occurred depending the different
> return
>> value of these external calls.
>> So, does the CIF have some simulation strategy to deal with the system
> calls or
>> interrupts? If so, how does it complete this ?
>>
>> Merry Christmas to you :-) and eager for your response!
>>
>>
>> Best Regards,
>> MA Lele,
>> Institute of Software, Chinese Academy of Sciences
>>


-- 
Best regards, Evgeny Novikov.