Hi, just a short note to say that this is now fixed in the mainline.
Cristian
On 09/08/17 16:55, Cristian Cadar wrote:
Yes, the right way to replay tests generated with --posix-runtime is via
klee-replay. As Yude said, it is possible in some circumstances for
KLEE to explore paths that triggers errors in programs using symbolic
files, but here there is actually a bug in KLEE that I plan to fix very
soon. In the meantime, please use the option --readable-posix-inputs
when generating tests with KLEE.
Best,
Cristian
On 05/08/17 07:24, Yude Lin wrote:
Hi Daniel,
I think the first method doesn't understand symbolic inputs specified
by '--posix-runtime', so you're right.
Isn't it an expected result for the second method? If 'A' doesn't
exist or is unreadable then the program crashes on fclose(NULL);
test000001 probably specifies an unreadable case. If there is an
test000002, it should be the not-null case.
Regards,
Yude
On Fri, Aug 4, 2017 at 7:35 AM, Daniel Schwartz
<d.schwa...@columbia.edu <mailto:d.schwa...@columbia.edu>> wrote:
Hi,
I'm struggling to figure out how to replay generated test cases with
symbolic files.
I see in the documentation that there are two ways to replay test
cases.
1. (As shown in: https://klee.github.io/tutorials/testing-function/
<https://klee.github.io/tutorials/testing-function/>) is to run the
executable with the KTEST_FILE flag set to a .ktest file.
2. (As shown in: https://klee.github.io/tutorials/testing-coreutils/
<https://klee.github.io/tutorials/testing-coreutils/>) is to use
klee-replay
My intuition is that the KTEST_FILE method won't work since there is
no call to klee_make_symbolic to intercept. I'm not sure why the
second method fails. I've included my attempt at both methods.
I've included a tester file for reproduction, the command I used to
launch KLEE and KLEE-replay, and the behavior I saw.
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------
Here is the tester I wrote up:
#include <stdio.h>
#include <stdlib.h>
#include <klee/klee.h>
int main(int argc, char **argv) {
char buf[1];
FILE *file = fopen(argv[1], "r");
if ( file != NULL ) {
fread(buf, 1, 1, file);
}
fclose(file);
printf("%d", buf[0]);
return 0;
}
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------
I generate files with the following command:
$ klee --libc=uclibc --posix-runtime --min-query-time-to-log=-1
--max-solver-time=10 --max-time=21600 --max-memory=4096
--simplify-sym-indices --write-cvcs --write-cov
--dump-states-on-halt=false --disable-inlining --use-forked-solver
--use-cex-cache --allow-external-sym-calls -write-test-info
--max-instruction-time=30. --watchdog test5-cov-outputs-klee.bc A
-sym-files 1 32
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------
And I get the following behavior:
$ KTEST_FILE=./klee-last/test000001.ktest ./tester
Segmentation fault
$ klee-replay ./tester klee-last/test000001.ktest
klee-replay: TEST CASE: klee-last/test000001.ktest
klee-replay: ARGS: "./tester" "A"
warning: check_file A: dev mismatch: 2049 vs 0
warning: check_file A: mode mismatch: 0100000 vs 0
warning: check_file A: nlink mismatch: 1 vs 0
warning: check_file A: blksize mismatch: 4096 vs 0
klee-replay: EXIT STATUS: CRASHED signal 11 (0 seconds)
Thanks,
Daniel Schwartz
_______________________________________________
klee-dev mailing list
klee-dev@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>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
