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.ca...@imperial.ac.uk
<mailto:c.ca...@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.ca...@imperial.ac.uk <mailto:c.ca...@imperial.ac.uk>
<mailto:c.ca...@imperial.ac.uk
<mailto:c.ca...@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@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
<mailto:klee-...@imperial.ac.__uk <mailto:klee-dev@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@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
<mailto:klee-...@imperial.ac.__uk <mailto:klee-dev@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
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
