[klee-dev] KLEE symbolic file input

[Cristian Cadar]

Hi,

If you run instead
klee --libc=uclibc --posix-runtime sock.bc A --sym-file 1000

the test should behave as expected.

As briefly documented at 
http://klee.github.io/docs/options/#symbolic-environment, the symbolic 
files are called A, B, C, etc.

Best,
Cristian


On 20/06/17 14:26, Shehbaz Jaffer wrote:
> 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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>