[klee-dev] rationale behind the parameters used in the KLEE OSDI paper
Lei Zhang
lei.zhang at uwaterloo.ca
Tue Feb 5 03:35:00 GMT 2013
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 <c.cadar at imperial.ac.uk>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 <c.cadar at imperial.ac.uk
>> <mailto:c.cadar at imperial.ac.uk**>> 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
>> <c.cadar at imperial.ac.uk <mailto:c.cadar at imperial.ac.uk**>
>> <mailto:c.cadar at imperial.ac.uk
>>
>> <mailto:c.cadar at imperial.ac.uk**>__>> 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/_**___klee-dev@imperial.ac.uk/___**
>> _msg00162.html<http://www.mail-archive.com/____klee-dev@imperial.ac.uk/____msg00162.html>
>> <http://www.mail-archive.com/_**_klee-dev@imperial.ac.uk/__**
>> msg00162.html<http://www.mail-archive.com/__klee-dev@imperial.ac.uk/__msg00162.html>
>> >
>>
>>
>> <http://www.mail-archive.com/_**_klee-dev@imperial.ac.uk/__**
>> msg00162.html<http://www.mail-archive.com/__klee-dev@imperial.ac.uk/__msg00162.html>
>> <http://www.mail-archive.com/**klee-dev@imperial.ac.uk/**
>> msg00162.html<http://www.mail-archive.com/klee-dev@imperial.ac.uk/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
>> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.**uk<klee-dev at imperial.ac.uk>
>> >
>> <mailto:klee-dev at imperial.ac._**_uk <mailto:klee-dev at imperial.ac.
>> **uk <klee-dev at imperial.ac.uk>>>
>> 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
>> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.**uk<klee-dev at imperial.ac.uk>
>> >
>> <mailto:klee-dev at imperial.ac._**_uk <mailto:klee-dev at imperial.ac.
>> **uk <klee-dev at imperial.ac.uk>>>
>> 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
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list