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

[Cristian Cadar]

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