1. How do you define 'design structure'?
2. You might be criticising an apple for not being a good orange. KLEE is
designed to tests the program it's being executed on, and if one also wants to
test 41 variants, he/she will run KLEE again on the variants. I'm not sure what
you would expect, even in a simple scenario like
if (input = 100) {
//something
}
You would need to generate 2^sizeof(input) inputs to take into account all
possible mutations to the literal 100 using regression testing.
Paul
On 7 Mar 2013, at 05:06, Urmas Repinski <[email protected]> wrote:
> Hello.
>
> Yes.
>
> So KLEE takes into account only the coverage, if all paths are covered, but
> does not take into account entire design structure.
>
> The errors provided by siemens benchmarks are in the operators (+ -> -, > ->
> <, etc) and in numbers (2 -> 3, 70 -> 80), and with klee inputs even if
> corresponding nodes in the design's model representation are activated, error
> is not propagated to the output.
>
> Its a pity, if it is possible to test the entire structure with klee inputs
> (activate different bits in variables with inputs, confirm that operators
> values take influence on the output) then klee generated inputs will be more
> useful for practical imlementation.
>
> It is possible to investigate error types, found in siemens benchmarks, and
> improve test generation with klee.
>
> I am writing one article about the errors in the designs at the moment, it
> will be published in the september, and then i will send it to the list too.
>
> Maybe this will make possible to improve input generation and make klee more
> usable in actual industry.
>
> Urmas Repinski
>
> Subject: Re: [klee-dev] using klee with Siemens Benchmarks
> From: [email protected]
> Date: Wed, 6 Mar 2013 21:19:54 +0000
> CC: [email protected]
> To: [email protected]
>
> Hello Urmas,
> It's not that clear what you're trying to do but I assume you want to use the
> inputs generated by KLEE on one program version to test 41 variants. I'm
> afraid this might not be that easy.
>
> KLEE actually gets nearly 100% statement and branch coverage on the original
> program ('nearly' because there's some unreachable code). You should run it
> without the POSIX runtime and uclibc because you're not using them anyway.
> What you get is:
>
> --------------------------------------------------------------------------
> | Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount | Solver(%) |
> --------------------------------------------------------------------------
> | klee-out-0 | 5951 | 0.26 | 99.36 | 94.44 | 311 | 91.92 |
> --------------------------------------------------------------------------
>
> From what I can tell, the path coverage is also 100%, counting just feasible
> paths, so there are no other inputs to generate as far as KLEE is concerned.
>
> Paul
>
> On 6 Mar 2013, at 12:31, Urmas Repinski <[email protected]> wrote:
>
> 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
> <INPUTS_tcas_Siemens_arg><tcas_original.c><tcas_modified.c><KLEE_OUTPUT_arg>_______________________________________________
> klee-dev mailing list
> [email protected]
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> _______________________________________________
> klee-dev mailing list
> [email protected]
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
