Hi Cristian, Thank you for your earlier replies regarding how to reproduce the Coreutils experiment. They are very helpful! Now we have set up the environment using Ubuntu 10.04 + LLVM 2.7 (I'd like to contribute to the upgrading to 2.9 after I finish this project). And we have some questions about replaying ktest and accumulating results. We use klee-replay to replay all the generated ktests in the obj-gcov directory and use gcov to get the line coverage on every single source file. Is that right?
And is there any possible way to replay in a sandbox? When testing some tools (e.g., chmod), it will do harm to the filesystem or encounter permission errors (which may hurt the coverage). Thank you in advance! Best regards, On Fri, Jan 25, 2013 at 10:40 AM, Cristian Cadar <[email protected]>wrote: > Hi Lei, > > Yes, we tested all utilities with --optimize, and this can have a > significant effect on the results. > > The problem you encounter is that KLEE does not support the llvm.trap > intrinsic, which I think was introduced in LLVM 2.9. You may want to try > LLVM 2.8, things might still work. Of course, we would like to have full > support for LLVM 2.9 (and ideally more recent versions of LLVM), so such > patches would be highly appreciated! > > Best, > Cristian > > > On 25/01/13 15:27, Lei Zhang wrote: > >> Hi Cristian, >> >> We are trying to reproduce the coreutils 6.10 result with KLEE r168798 >> (based on LLVM 2.9) using the parameter in >> http://klee.llvm.org/**CoreutilsExperiments.html<http://klee.llvm.org/CoreutilsExperiments.html>. >> It works fine for the >> majority of utilities but the following 6: >> >> cp, mv, who, pinky, hostid, shred >> >> They all failed because of "LLVM ERROR: Code generator does not support >> intrinsic function 'llvm.trap'!" >> >> This is caused by the '--optimize' option passed to KLEE. If I omit that >> option, everything goes smoothly. And 4 of them get coverage over 60%. >> So could you tell us whether or not these 6 utilities are tested with >> optimization in the OSDI'08 paper experiment? If so, any recommendation >> on how to solve this problem? I have searched a lot but didn't find any >> useful information. Any advise is highly appreciated. Thank you in >> advance! >> >> Best regards, >> >> On Mon, Jan 21, 2013 at 3:19 PM, Cristian Cadar <[email protected] >> <mailto:[email protected]**>> wrote: >> >> Hi Lei, >> >> Here are the symbolic arguments for those eight tools: >> >> dd: --sym-args 0 3 10 --sym-files 1 8 --sym-stdout >> dircolors: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout >> echo: --sym-args 0 4 300 --sym-files 2 30 --sym-stdout >> expr: --sym-args 0 1 10 --sym-args 0 3 2 --sym-stdout >> mknod: --sym-args 0 1 10 --sym-args 0 3 2 --sym-files 1 8 --sym-stdout >> od: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout >> pathchk: --sym-args 0 1 2 --sym-args 0 1 300 --sym-files 1 8 >> --sym-stdout >> printf: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout >> >> Hope this helps, >> Cristian >> >> >> On 14/01/13 18:28, Lei Zhang wrote: >> >> Hi Cristian, >> >> Thank you for your quick reply! :-) >> >> Besides, the paper mentions "For eight tools where the coverage >> results >> of these values were unsatisfactory, we consulted the man page and >> increased the number and size of arguments and files." Could you >> give us >> more details about that? Thanks! >> >> Best regards, >> >> On Mon, Jan 14, 2013 at 10:44 AM, Cristian Cadar >> <[email protected] <mailto:[email protected]**> >> <mailto:[email protected] >> >> <mailto:[email protected]**>__>> wrote: >> >> Hi Lei, >> >> Our choice was based on a high-level understanding of the >> Coreutils >> apps: most behavior can be triggered with no more than 2 >> short >> options, 1 long option, and 2 small files (one of which is >> stdin). >> >> Best wishes, >> Cristian >> >> >> On 14/01/13 14:58, Lei Zhang wrote: >> >> Hi All, >> >> We are working on a possible way to improve KLEE. So it >> would be >> nice to >> compare our method's results with the original KLEE's. >> For a fair >> comparison, we need to understand how the parameters >> used in your >> OSDI'08 paper were chosen. According to your reply on >> the KLEE >> mailing >> list >> >> (http://www.mail-archive.com/_**[email protected]/___** >> _msg00162.html<http://www.mail-archive.com/[email protected]/____msg00162.html> >> <http://www.mail-archive.com/_**[email protected]/__** >> msg00162.html<http://www.mail-archive.com/[email protected]/__msg00162.html> >> > >> >> >> <http://www.mail-archive.com/_**[email protected]/__** >> msg00162.html<http://www.mail-archive.com/[email protected]/__msg00162.html> >> <http://www.mail-archive.com/**[email protected]/** >> msg00162.html<http://www.mail-archive.com/[email protected]/msg00162.html> >> >>), >> >> your OSDI paper uses >> >> --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 2 8 >> --sym-stdout >> >> Could you unveil the rationale/intuition behind these >> settings, such >> like why 10 and 2 are used as the maximal lengths? Any >> help is >> highly >> appreciated. Thanks in advance! >> >> Best regards, >> >> -- >> Lei >> Department of Electrical and Computer Engineering >> University of Waterloo >> 200 University Avenue West >> Waterloo, Ontario, Canada N2L 3G1 >> >> >> ______________________________**_____________________ >> >> klee-dev mailing list >> [email protected] >> <mailto:[email protected].**uk<[email protected]> >> > >> <mailto:[email protected]._**_uk <mailto:[email protected]. >> **uk <[email protected]>>> >> >> https://mailman.ic.ac.uk/____**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/____mailman/listinfo/klee-dev> >> >> <https://mailman.ic.ac.uk/__**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev> >> > >> >> <https://mailman.ic.ac.uk/__**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev> >> >> <https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> >> >> >> >> >> ______________________________**_____________________ >> >> klee-dev mailing list >> [email protected] >> <mailto:[email protected].**uk<[email protected]> >> > >> <mailto:[email protected]._**_uk <mailto:[email protected]. >> **uk <[email protected]>>> >> >> https://mailman.ic.ac.uk/____**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/____mailman/listinfo/klee-dev> >> >> <https://mailman.ic.ac.uk/__**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev> >> > >> >> >> >> <https://mailman.ic.ac.uk/__**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev> >> >> <https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> >> >> >> >> >> >> >> -- >> Lei Zhang >> Department of Electrical and Computer Engineering >> University of Waterloo >> 200 University Avenue West >> Waterloo, Ontario, Canada N2L 3G1 >> >> >> >> >> -- >> Lei Zhang >> Department of Electrical and Computer Engineering >> University of Waterloo >> 200 University Avenue West >> Waterloo, Ontario, Canada N2L 3G1 >> > -- Lei Zhang Department of Electrical and Computer Engineering University of Waterloo 200 University Avenue West Waterloo, Ontario, Canada N2L 3G1
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
