[klee-dev] Trouble replaying test cases with symbolic files

[Cristian Cadar]

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.schwartz at columbia.edu 
> <mailto:d.schwartz at 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 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>
> 
> 
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>