[klee-dev] rationale behind the parameters used in the KLEE OSDI paper

[Lei Zhang]

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. 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>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**>> 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>
>> >),
>>
>>         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>
>> >
>>         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>
>> >
>>     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
-------------- next part --------------
HTML attachment scrubbed and removed