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

[Daniel Schwartz]

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
-------------- next part --------------
HTML attachment scrubbed and removed