On Oct 20, 2009, at 12:47 AM, Daniel Dunbar wrote: > On Mon, Oct 19, 2009 at 2:16 PM, Cristian Zamfir > <cristian.zamfir at epfl.ch> wrote: >> >> Hi, >> >> I am trying to reproduce the bugs from the OSDI paper. >> >> I managed to reproduce 7 bugs on the native binaries: using the >> instructions in the paper, it worked for paste, mkdir, mknod, mkfifo, >> tac, seq and "ptx -F\\ abcdefghijklmnopqrstuvwxyz" >> >> There are 3 bugs I cannot reproduce with the content of the files >> described in the paper: >> ./pr -e t2.txt >> ./md5sum -c t1.txt >> ./ptx x t4.txt >> >> Do you happen to have at hand the content of those files (t1.txt, >> t2.txt and t4.txt)? > > I don't have it handy, but there are longer descriptions here: > http://www.mail-archive.com/coreutils-announce at gnu.org/msg00038.html > >> I also tried to use KLEE to find the bugs that I could reproduce on >> the binaries. I tried so far paste, tac and seq. >> I ran KLEE for an hour with the parameters I found in an earlier >> post. >> I use a version of KLEE from July 2008. I assume this version should >> work too. >> >> Unfortunately, KLEE did not find the bugs. I am not sure if this is >> because of my version of KLEE or due to the parameters I use. Do you >> happen to know the exact parameters I should pass to KLEE for these >> particular coreutils? > > I don't have this stuff handy and my memory is fuzzy. May Cristian > C. remembers? >
Hi, here is the line we used to run KLEE on paste (taken from the info file on our archives). However, this is from an old version of KLEE, and some options might need to be adapted to work with the current version. klee --simplify-sym-indices --write-cvcs --write-cov --output-module -- max-memory=1000 --disable-inlining --optimize --use-forked-stp --use- cex-cache --with-libc --with-file-model=release --allow-external-sym- calls --only-output-states-covering-new --exclude-libc-cov --exclude- cov-file=./../lib/functions.txt --environ=test.env --run-in=/tmp/ sandbox --output-dir=nrp-1h/paste-data --max-sym-array-size=4096 --max- instruction-time=10. --max-time=3600. --watchdog --max-memory- inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1 --max- static-cpfork-pct=1 --switch-type=internal --randomize-fork --use- random-path --use-interleaved-covnew-NURS --use-batching-search -- batch-instructions 10000 --init-env ./paste.bc --sym-args 0 1 10 --sym- args 0 2 2 --sym-files 1 8 --sym-stdout Hope this helps, Cristian > - Daniel > >> Thank you, >> Cristi >> >> _______________________________________________ >> klee-dev mailing list >> klee-dev at keeda.stanford.edu >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >> -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20091021/0fadea3d/attachment.html
