Hello!
I have looked at previous discussions on symbolic file inputs [1][2][3], but I
am unable to run an example for how KLEE could be run for symbolic file inputs.
Please consider the sample program which opens a file, seeks to start of file,
reads 64 bytes of data, and seeks back to start of file, and then exits.
int main(int argc, char *argv[])
{
int sock;
FILE *dev;
long pos;
char blocks[64];
if ((sock = open(argv[1], O_RDWR)) < 0) {
// tried replacing argv[1] with 'A', 'A-data'
// but none seem to work?
EXIT("open failed\n");
}else if((dev = fdopen(sock, "r+")) == NULL){
EXIT("open read mode failed\n");
}
if ((pos = ftell(dev)) < 0) {
EXIT("ftell");
}
if (fseek(dev, 0 , SEEK_SET) < 0) {
EXIT("fseek");
}
if (fread(blocks, 64, 1 , dev) != 1) {
EXIT("freed");
}
if (fseek(dev, pos, SEEK_SET) < 0) {
EXIT("fseek");
}
printf ("PASS\n");
}
If I run the program with a concrete file input:
./sock /tmp/testfile
OUTPUT: PASS
However, if I try KLEE with --sym-file argument:
klee --libc=uclibc --posix-runtime sock.bc --sym-file 1000
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 52082608)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: calling external: printf(52815248, 47655712)
open failed // OPEN FAILS!!
KLEE: done: total instructions = 6402
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
I have also looked at POSIX/runtime/fd_init.c and it looks like a symbolic file
"A-data" is created (for 1 symbolic file) but the contents of the file are
malloc'ed and marked symbolic using klee_mark_symbolic on a fixed sized
in-memory buffer of size specified by user. The actual file is not created on
disk. Is this the reason why a call to open() of argv[1] fails? What is the
alternative method to ensure argv[1] corresponds to symbolic file created using
--symfile 1000 option? I also tried instrumenting code and replacing argv[1]
with "A" and "A-data". Still, open call fails and KLEE does not successfully
execute open command.
Thanks and Regards,
Shehbaz
[1] http://mailman.ic.ac.uk/pipermail/klee-dev/2013-April/000156.html
[2] https://www.cs.purdue.edu/homes/kim1051/cs490/proj3/description.html
[3] http://klee-dev.keeda.stanford.narkive.com/5t9M1H0i/symbolic-file-inputs
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
