[ldv-project] CIL-OCaml Linux Driver testing - usbkbd.c and usbmouse.c

[Vadim Mutilin]

Hi Iyer!

Replacing CC for the Linux kernel didn't worked for us.
For collecting make commands we are patching kernel makefiles.
For compiler command you can change file scripts/Makefile.build

Somethere about line 243 you can find
  define rule_cc_o_c
At that point you can insert a command which will do preprocessing by 
gcc, and then can be passed to CIL.
+       $(CC) $(c_flags) -O0 -E -o $@.i $< ;       \

The better way to get extracted drivers is to use LDV framework.
To verify device drivers with your own static analysis tool you need to 
write wrapper as described in ldv-tools/VerifierDevelopersHowTo

Best,
Vadim

01.07.2015 17:12, Iyer,Naveen R ?????:
>
> Hi all !
>
>
> I am trying to use C Intermediate Language (CIL) to test usbkbd.c and 
> usbmouse.c drivers.
>
> For normal .c source codes, I do the following:
>
>
> From the /cil-1.7.3 location:
>
> bin/cilly --dologcalls --save-temps -D HAPPY_MOOD -I myincludes 
> hello.c -o hello.exe
>
>
> And it works.
>
> However, my primary aim is to test usbkbd.c and usbmouse.c.
>
> I have compiled the linux kernel and have tried to modify the drivers 
> by adding few comments and commenting few lines and then "insmod"'ing 
> them.
>
> However, now if I want to use "cilly" to "make" these driver files, I 
> do the following:
>
>
> From the /linux-3.13.0 location:
>
> make CC=/home/naveen/cil-1.7.3/bin/cilly SUBDIRS=drivers/hid/usbhid/ 
> CONFIG_USB_MOUSE=m modules
>
>
> And running the above command I get the following error:
>
> root at naveen-VirtualBox:/home/naveen/linux-3.13.0# make 
> CC=/home/naveen/cil-1.7.3/bin/cilly SUBDIRS=drivers/hid/usbhid/ 
> CONFIG_USB_MOUSE=m modules
> /home/naveen/linux-3.13.0/arch/x86/Makefile:98: stack protector 
> enabled but no compiler support
> /home/naveen/linux-3.13.0/arch/x86/Makefile:113: CONFIG_X86_X32 
> enabled but no binutils support
> gcc -D_GNUCC -E -print-file-name=include
>   CC [M]  drivers/hid/usbhid/hid-core.o
> Warning: Unknown argument -Wframe-larger-than=1024
> Warning: Unknown argument -Werror=implicit-int
> Warning: Unknown argument -Werror=strict-prototypes
> gcc -D_GNUCC -E -Wp,-MD,drivers/hid/usbhid/.hid-core.o.d -include 
> /home/naveen/linux-3.13.0/include/linux/kconfig.h -nostdinc -isystem 
> /usr/lib/gcc/x86_64-linux-gnu/4.8/include 
> -I/home/naveen/linux-3.13.0/arch/x86/include 
> -Iarch/x86/include/generated -Iinclude 
> -I/home/naveen/linux-3.13.0/arch/x86/include/uapi 
> -Iarch/x86/include/generated/uapi 
> -I/home/naveen/linux-3.13.0/include/uapi -Iinclude/generated/uapi 
> -Iubuntu/include -D__KERNEL__ -fno-strict-aliasing -fno-common 
> -fno-delete-null-pointer-checks -O2 -m64 -mno-mmx -mno-sse 
> -mpreferred-stack-boundary=3 -mtune=generic -mno-red-zone 
> -mcmodel=kernel -funit-at-a-time -maccumulate-outgoing-args 
> -DCONFIG_AS_CFI=1 -DCONFIG_AS_CFI_SIGNAL_FRAME=1 
> -DCONFIG_AS_CFI_SECTIONS=1 -DCONFIG_AS_FXSAVEQ=1 -DCONFIG_AS_AVX=1 
> -DCONFIG_AS_AVX2=1 -pipe -fno-asynchronous-unwind-tables -mno-sse 
> -mno-mmx -mno-sse2 -mno-3dnow -mno-avx -fno-omit-frame-pointer 
> -fno-optimize-sibling-calls -fno-var-tracking-assignments -g -mfentry 
> -DCC_USING_FENTRY -fno-strict-overflow -fconserve-stack 
> -DCC_HAVE_ASM_GOTO -I myincludes -DMODULE -DKBUILD_STR(s)=#s 
> -DKBUILD_BASENAME=KBUILD_STR(hid_core) 
> -DKBUILD_MODNAME=KBUILD_STR(usbhid) -DCIL=1 
> drivers/hid/usbhid/hid-core.c -o ./hid-core.i
> /home/naveen/cil-1.7.3/bin/cilly.native --out ./hid-core.cil.c 
> --warnall --envmachine --dologcalls ./hid-core.i
> /home/naveen/linux-3.13.0/arch/x86/include/asm/cpufeature.h[396:7-7] : 
> syntax error
> Parsing errorFatal error: exception Frontc.ParseError("Parse error")
> make[1]: *** [drivers/hid/usbhid/hid-core.o] Error 2
> make: *** [_module_drivers/hid/usbhid] Error 2
>
>
> Could anyone please guide me on this?
>
>
> Thanks
>
> Regards
> *Naveen R. Iyer*
> Graduate Student (Research Division: Computer Engineering)
> Dept. of Electrical & Computer Engineering
> University of Florida
>
>
> _______________________________________________
> ldv-project mailing list
> ldv-project at linuxtesting.org
> http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20150703/937527a4/attachment.html>