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

Reply via email to