[klee-dev] using klee with Siemens Benchmarks

[Urmas Repinski]

Hello.

My name is Urmas Repinski, PhD student in Tallinn University of Technology, Estonia.

I am trying to generate inputs for Siemens Benchmarks with KLEE.

Siemens Benchmarks - C designs with various erroneous versions for testing error localization and error correction in C designs.
They can be located and downloaded from http://pleuma.cc.gatech.edu/aristotle/Tools/subjects/

I am testing KLEE with tcas design, it is smallest and simplest.

Siemens benchmarks provide their inputs, tcas/script/runall.sh script has 1607 lines of execution of the design, and it is easy extract 1607 various inputs for the design.
But i have no idea how the inputs were generated, attaching siemens benchmarks inputs to the letter (file INPUTS_tcas_Siemens_arg).

I want to compare Siemens inputs with inputs, generated by klee.

I had installed klee as it is written in documentation - http://klee.llvm.org/GetStarted.html - with uclibc support.

Installed llvm-gcc-4.2, llvm-gcc-4.5, originally provided by Linux Mint 12 uses too new version of gcc, and this generated error then used llvm-gcc, but ok, this error solved.

When i take tcas/v1/tcas.c design, adding corresponding modification to generate inputs with klee (tcas_original.c and tcas_modified.c are attached to the letter), i get 45 inputs generated, and after modifying klee output to suitable format i get klee outputs (file KLEE_OUTPUT_arg).

urmas-PBL21 src # llvm-gcc --emit-llvm -c -g tcas.c
urmas-PBL21 src # klee --libc=uclibc  --posix-runtime   tcas.o 
KLEE: NOTE: Using model: /home/urmas/forensic/thirdparty-install/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-143"
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 54549392)
KLEE: WARNING ONCE: calling __user_main with extra arguments.

KLEE: done: total instructions = 14790
KLEE: done: completed paths = 45
KLEE: done: generated tests = 45


This outputs have same coverage than Siemens Inputs, but most of errors in erroneous designs are simply not detected, while Simenes inputs detect all errors.

Inputs KLEE: Coverage - 92.5532%.  Total Inputs - 45 Detected Errors - 8/41
Inputs Siemens Benchmarks: Coverage - 93.0851%. Total Inputs - 1607, Detected Erroneous designs - 41/41

Maybe i have something wrong with KLEE arguments when i execute klee, can somebody help me with right klee execution?
I had tested klee with various options, but i still have 45 generated inputs. Is it possible to increase somehow number of generated inputs with klee?
Maybe WARNING KLEE: WARNING: undefined reference to function: fwrite aborts executions somewhere, but there is no fwrite function in tcas design.

Urmas Repinski

 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: INPUTS_tcas_Siemens_arg
Type: application/octet-stream
Size: 57724 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20130306/42edda24/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: tcas_original.c
Type: text/x-csrc
Size: 4621 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20130306/42edda24/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: tcas_modified.c
Type: text/x-csrc
Size: 5874 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20130306/42edda24/attachment-0001.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: KLEE_OUTPUT_arg
Type: application/octet-stream
Size: 3582 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20130306/42edda24/attachment-0001.obj>