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

[Tu Pipa]

On Thu, Sep 12, 2013 at 1:44 PM, Evgeny Novikov <novikov at ispras.ru> wrote:

>  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.
>

Thank you so much! The error is gone when the instruction being replaced.
But another error comes then...
I have opened an  issue at CIF project http://forge.ispras.ru/issues/4467 .
And I hope we can solve this problem very soon.
Thank you again for your help !

-- 
Best Regards,
MA Lele
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130912/a6c9aad7/attachment.html>