Hi Jiaqi, On Mon, Mar 15, 2010 at 1:49 AM, Jiaqi Tan <tanjiaqi at gmail.com> wrote: > 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. > 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 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. :) > > I have two questions regarding symbolic file inputs: > > 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. > 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. > 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? Covered in previous message -- for what its worth, this message: > 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 > Thanks, > Jiaqi Tan > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
