[klee-dev] KLEE symbolic file input

[Shehbaz Jaffer]

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