[ldv-project] [rule-instrument] How to find the intermediate files produced by CIF ?

[Evgeny Novikov]

 Hi MA Lele.

11.09.2013, 09:48, "Tu Pipa" <tupipa0929 at gmail.com>:
> On Tue, Nov 6, 2012 at 11:18 PM, Evgeny Novikov <eugenenovikov at yandex.ru> wrote:
>> On 11/06/2012 01:02 PM, Ma Lele wrote:
>>
>>> Hello Evegeny Novikov,
>>> I have just finished reading your paper <<One Approach to Aspect-Oriented Programming Implementation for the C programming language >>. Your works is so excellent and please accept my best wishes for you to get more and more development in this domain in the future :-)
>>
>> Thank you for wishes, I will try to continue research :)
>>> I have installed the ldv , which seems that it can verify some kernel driver successfully (like usb/storage dirver I have mentioned in the last e-mail).
>>>
>>> But I failed to find the four kinds of files you mentioned in this paper( *.c.p , *.c.p.mw , or *.c.p.mw.aw). Are they all cleaned during the process ? If so, how can I get these files  when running the ldv ?
>>
>> First of all, you need to verify drivers against models ending with "a" suffix (I have explained the difference between different models before), e.g. 32_7a.
>>
>> Also from the time when I have written that paper much time has gone. These files are named more properly now and they are kept automatically if you use LDV_DEBUG>=30. These names correspond to 5 stages that you can find in my presentation. Assume that "diro" is output directory, "a" is aspect file, "c" is input C file, "o" is output file then you will obtain at these stages respectively:
>> 1. "diro/a.i".
>> 2. "diro/c.prepared".
>> 3. "diro/c.macroinstrumented".
>> 4. "diro/c.instrumented".
>> 5. "diro/о.c".
>>
>> For instance, here is the content of directory work/current--X--drivers/cdrom--X--defaultlinux-2.6.39--X--32_7a/linux-2.6.39/csd_deg_dscv/10/dscv_tempdir/dscv/ri/32_7a/drivers/cdrom/ at my computer:
>> 0032.tmpl.aspect.i  cdrom.c  cdrom.c.instrumented  cdrom.c.macroinstrumented  cdrom.c.prepared  cdrom.ko  cdrom.o  cdrom.o.c
>>> Thank you for your time reading my message. Eager for your response.
>>
>> Thank you for your user experience - it helps us very much.> --
>>> Best Regards,
>>> MA Lele
>>
>> -- Best regards, Evgeny Novikov.
>
> Hi, Evgeny Novikov,
> I still have a question about the file like cdrom.o.c which is fianlly genetated by the CIF.
> I know it's used as an input source file to be verified for the blast. Now I want to compile it using GCC compiler in order to use some other tools to verify the code. But it always give me some error like
> "../inst/current/envs/linux-2.6.36/linux-2.6.36/arch/x86/include/asm/thread_info.h:179: error: register name not specified for ‘current_stack_pointer’".
I know that instrumented source code (like in cdrom.o.c) isn't perfect. It looks to be rather good for tools like CIL, BLAST, CPAchecker, UFO, CBMC and many others. But for a very strict compiler that tries to produce object/binary code on the basis of instrumented source code it isn't enough.
The error is presented from 171 to 179 lines of arch/x86/include/asm/thread_info.h file (http://lxr.free-electrons.com/source/arch/x86/include/asm/thread_info.h#L171). I can suggest that instead of:
  register unsigned long current_stack_pointer asm("esp") __used;
something like:
  register unsigned long current_stack_pointer;
was generated by CIF. And due to absence of asm("esp") GCC says: "register name not specified for ‘current_stack_pointer’". I guess that the most of static verification tools don't perform such sort of checks, or just warn in case of such problems (BTW, what tool do you use?). But nevertheless this doesn't allow CIF to produce incorrect instrumented source code that doesn't correspond to the original one. 
I will be very grateful to you if you will open an appropriate issue at CIF project page http://forge.ispras.ru/projects/cif. It will be great if you will attach *.macroinstrumented file and an aspect file that leads to the error there. I can't guarantee that I will fix it quickly, but I will fix it one day.
> It may need some more gcc options to compile this kind of files. But I don't know where to find it out.
> Can you help me with this?
No extra options are needed since these files are based on files that were preprocessed with all required options. Simple workaround for you is to manually (or with patch) replace:
  register unsigned long current_stack_pointer;
with:
  register unsigned long current_stack_pointer asm("esp");
If there will be other errors, you can post more bugs to http://forge.ispras.ru/projects/cif or/and make some extra manual patches. 
> Thank you in advance!
>
> --
> Best Regards,
> MA Lele


-- 
Best regards, Evgeny Novikov.