rationale behind the parameters used in the KLEE OSDI paper

Discussion:

Lei Zhang

2013-01-14 14:58:31 UTC

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-AQ/***@public.gmane.org/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

Cristian Cadar

2013-01-14 15:44:03 UTC

Permalink

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

Post by Lei Zhang
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
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Lei Zhang

2013-01-14 18:28:32 UTC

Permalink

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,

Post by Cristian Cadar
Hi Lei,
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

Post by Lei Zhang
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
),
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
https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>

______________________________**_________________
klee-dev mailing list
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

Cristian Cadar

2013-01-21 20:19:13 UTC

Permalink

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

Post by Lei Zhang
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,
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
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
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
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
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

2013-01-21 20:26:46 UTC

Permalink

Hi Cristian,

Thank you very much!

Post by Cristian Cadar
Hi Lei,
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

--
Lei Zhang
Department of Electrical and Computer Engineering
University of Waterloo
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1

Lei Zhang

2013-01-25 15:27:57 UTC

Permalink

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

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,

Hi Lei,
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

--
Lei Zhang
Department of Electrical and Computer Engineering
University of Waterloo
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1

Cristian Cadar

2013-01-25 15:40:39 UTC

Permalink

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

Post by 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
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,
Hi Lei,
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
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
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
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
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
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
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

2013-02-05 03:35:00 UTC

Permalink

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,

Post by Cristian Cadar
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

Post by 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<http://klee.llvm.org/CoreutilsExperiments.html>.
It works fine for the
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,
Hi Lei,
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
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
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
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

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
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
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

Cristian Cadar

2013-02-07 11:03:04 UTC

Permalink

Hi Lei,

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).

That would be useful, thanks.

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?

Yes, that's correct. You might want to use a tool that Daniel wrote,
zcov, to visualize the results: http://minormatter.com/zcov/

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!

Yes, the right thing to do would be to replay every test in a new
instance of a virtual machine (or something similar). But we didn't do
this, we just made sure that the replay process doesn't have permissions
to do too much harm :) In any case, what's important to remember is to
replay each test case in a fresh sandbox directory (I'm referring here
to the "sandbox" discussed at
http://klee.llvm.org/CoreutilsExperiments.html) and to set the same
environment variables as the ones set during symbolic execution (the
ones in test.env).

Hope this helps,
Cristian

Lei Zhang

2013-02-08 14:44:53 UTC

Permalink

Hi Cristian,

Thank you very much for your direction!

Post by Cristian Cadar
Hi Lei,

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).

That would be useful, thanks.
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?

Yes, that's correct. You might want to use a tool that Daniel wrote,
zcov, to visualize the results: http://minormatter.com/zcov/
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!

Yes, the right thing to do would be to replay every test in a new instance
of a virtual machine (or something similar). But we didn't do this, we
just made sure that the replay process doesn't have permissions to do too
much harm :) In any case, what's important to remember is to replay each
test case in a fresh sandbox directory (I'm referring here to the "sandbox"
discussed at http://klee.llvm.org/**CoreutilsExperiments.html<http://klee.llvm.org/CoreutilsExperiments.html>)
and to set the same environment variables as the ones set during symbolic
execution (the ones in test.env).

So this means before replay a ktest, I should remove the old sanbox
directory and uncompress sandbox.tgz to create a new one, and then copy the
native utility compiled with gcov support to the new sandbox directory and
then reply the ktest?

Post by Cristian Cadar
Hope this helps,
Cristian
______________________________**_________________
klee-dev mailing list
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

Cristian Cadar

2013-02-11 18:12:08 UTC

Permalink

Post by Lei Zhang
So this means before replay a ktest, I should remove the old sanbox
directory and uncompress sandbox.tgz to create a new one, and then
copy the native utility compiled with gcov support to the new sandbox
directory and then reply the ktest?

Lei Zhang

2013-02-24 15:34:08 UTC

Permalink

Post by Cristian Cadar

Hi Cristian,
Thank you for your detailed instruction. Now we do like that. And, another
question, I think there are actually only 88 stand-alone utilities in
coreutils, unless considering "false" or "test/[" as stand-alone. I skipped
"dir", "vdir", "ginstall", "groups", "sha*sum", "false", and only test one
of the "test" and "[" pair. Should I consider "false" or "test/[" as
stand-alone?

Besides, how did you modify the buffer used by "sort"? Thank you very much!

Best regards,

Post by Cristian Cadar
Best wishes,
Cristian
______________________________**_________________
klee-dev mailing list
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

Cristian Cadar

2013-03-06 23:29:09 UTC

Permalink

Hi Lei,

Post by Lei Zhang
Thank you for your detailed instruction. Now we do like that. And,
another question, I think there are actually only 88 stand-alone
utilities in coreutils, unless considering "false" or "test/[" as
stand-alone. I skipped "dir", "vdir", "ginstall", "groups", "sha*sum",
"false", and only test one of the "test" and "[" pair. Should I consider
"false" or "test/[" as stand-alone?

You need to consider ginstall. But you need to skip arch, which as we
mention in the paper is just a wrapper for uname -m. I updated the
Coreutils experiments webpage with the list of the 89 utilities that we
considered.

Post by Lei Zhang
Besides, how did you modify the buffer used by "sort"? Thank you very much!

I've just looked, and we changed
#define INPUT_FILE_SIZE_GUESS (1024 * 1024)
to
#define INPUT_FILE_SIZE_GUESS 1024

Looking over our archives, I noticed two more changes that we had to do
during our experiments:
(1) We had to change some _exit calls during replay, since otherwise
gcov will not record any coverage on those paths. Of course, note that
this is a problem when you run the manual test suite too (and gcov in
general)
(2) We had to disable buffered I/O, as otherwise the sequence of system
calls issued by some programs is nondeterministic, which is a problem in
failure mode.

I will try to document these issues -- and any other I encounter while
looking at our archives -- on the KLEE website as soon as I get a chance.

BTW, I remember you mentioned a patch that addresses the issues you
encountered while running KLEE with more recent versions of LLVM (incl.
2.9)? It would be great if you could contribute it to the mainline.

Best,
Cristian

Lei Zhang

2013-02-25 15:56:59 UTC

Permalink

Hi Cristian,

Just another question about the KLEE paper. In footnote 7 you said that "We
ran the test suite using the commands: env RUN_EXPENSIVE_TESTS=YES
RUN_VERY_EXPENSIVE_TESTS=YES make check and make check-root (as root). A
small number of tests (14 out of 393) which require special configuration
were not run; from manual inspection we do not expect these to have a
significant impact on our results." How did you calculated the number of
393? We run this command too, but the number reported by "make check" and
"make check-root" is totally about 150. Besides, we have also tried using
Linux audit <http://linux.die.net/man/8/auditd> to record every invocation
of the compiled binaries. The total number of invocations is 8056. In order
to guarantee our evaluation's sanity, we need your help about this
discrepancy. Could you tell us how the number of 393 is calculated? Thank
you in advance!

Best regards,

Post by Cristian Cadar

Hi Lei, yes, this is essentially correct; however, to better mimic the
symbolic execution environment, what we did was to invoke klee-replay from
within the sandbox directory, but without copying the native executable in
the sandbox directory. Finally, don't forget to reset the environment
variables before you replay a test.
Best wishes,
Cristian
______________________________**_________________
klee-dev mailing list
https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>

--
Lei Zhang,
Department of Computer Science & Technology,
School of Electronics Engineering and Computer Science,
Peking University,
No.5 Yiheyuan Road Haidian District,
Beijing, 100871, P.R.China