[klee-dev] rationale behind the parameters used in the KLEE OSDI paper
Cristian Cadar
c.cadar at imperial.ac.uk
Fri Jan 25 15:40:39 GMT 2013
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. 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>>),
>
> 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>
> <mailto:klee-dev at imperial.ac.__uk <mailto: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>
> <mailto:klee-dev at imperial.ac.__uk <mailto: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
More information about the klee-dev
mailing list