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

[Yude Lin]

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>
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/) 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/) 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
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed