Symbolic file inputs

[Unknown]

Hi,

I'm trying to run KLEE with tar 1.19. I have managed to compile tar
with KLEE, and I'm trying to generate one symbolic file input to
represent/simulate an input tar file.

I'm currently running KLEE with the following command line call:
$ klee --libc=uclibc --posix-runtime --max-time 30 --init-env
./src/a.out.bc -xz --sym-files 1 100000

I have two questions regarding symbolic file inputs:

1. Is the first symbolic file input always passed to stdin of the
program being called?

2. For the subsequent symbolic input files beyond the first, how do
these get passed to the program/how does the program access these
files? Or are the multiple symbolic input files passed to the program
one after another, with as many runs of the program as there are
symbolic input files specified?

Also, I got this error from (the LLVM-compiled version of) tar:

===== BEGIN OUTPUT =====
KLEE: WARNING: pipe: ignoring (ENFILE)
interprocess channel: Cannot pipeKLEE: WARNING: calling external:
vprintf(188424464, 202253304)

Error is not recoverable: exiting now
: Too many open files in system
KLEE: done: total instructions = 690302
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
===== END OUTPUT =====

Any ideas what this means?

Thanks,
Jiaqi Tan

[Unknown]

Hi Jiaqi,

Post by Unknown
Hi,
I'm trying to run KLEE with tar 1.19. I have managed to compile tar
with KLEE, and I'm trying to generate one symbolic file input to
represent/simulate an input tar file.

Ok.

Post by Unknown
$ klee --libc=uclibc --posix-runtime --max-time 30 --init-env
./src/a.out.bc -xz --sym-files 1 100000

And by the way, 100000 bytes is a whole lot from a symbolic execution
perspective. This will kill the constraint solver in no time. I would
be happy if 256 works. :)

Post by Unknown
1. Is the first symbolic file input always passed to stdin of the
program being called?

The --sym-files argument implies creating a symbolic stdin. There
isn't really any such thing as the "first symbolic file", rather the
limit passed to --sym-files controls how many *different* symbolic
files a program could theoretically access.

Post by Unknown
2. For the subsequent symbolic input files beyond the first, how do
these get passed to the program/how does the program access these
files? Or are the multiple symbolic input files passed to the program
one after another, with as many runs of the program as there are
symbolic input files specified?

Symbolic files are essentially made visible as files named 'A', 'B',
... for as many as are available. This is a crude but simple way of
ensuring that a program which passes a symbolic string to open() will
end up accessing a symbolic file.

Post by Unknown
===== BEGIN OUTPUT =====
KLEE: WARNING: pipe: ignoring (ENFILE)
vprintf(188424464, 202253304)
Error is not recoverable: exiting now
: Too many open files in system
KLEE: done: total instructions = 690302
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
===== END OUTPUT =====
Any ideas what this means?
KLEE: WARNING: pipe: ignoring (ENFILE)

is KLEE saying that it doesn't implement pipe, and it is just going to
return ENFILE, after which tar is bailing.

- Daniel

- Daniel

Post by Unknown
Thanks,
Jiaqi Tan
_______________________________________________
klee-dev mailing list
klee-dev at keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev