i'm happy to create a package if someone can give me ssh access to a machine that has klee setup to run the osdi experiments :) in theory, it should be as easy as figuring out which klee svn version and coreutils version was used for the experiments, right? but i'm sure reality is less ideal.
pg On Thu, May 26, 2011 at 2:36 PM, Dawson Engler <engler at csl.stanford.edu>wrote: > perhaps it's wortwhile to run the actual osdi code and package it up so > other people can replicate? > > > > On Thu, 26 May 2011, Cristian Cadar wrote: > > Hi Philip, >> >> Thanks a lot for the CDE package, it's really helpful. I just added >> your instructions to the Getting Started webpage. >> >> Best, >> Cristian >> >> On 26/05/2011 00:42, Philip Guo wrote: >> >>> With the help of Cristian, I've put together an improved version of the >>> Klee package: >>> >>> http://keeda.stanford.edu/~pgbovine/klee-cde-package.v2.tar.bz2 (200MB) >>> >>> Now you're able to run the Klee regression tests AND also replicate the >>> world-famous coreutils case study from: >>> http://klee.llvm.org/TestingCoreutils.html >>> >>> See the README file in the package for detailed instructions. >>> >>> >>> On Wed, May 25, 2011 at 11:47 AM, Philip Guo <pg at cs.stanford.edu >>> <mailto:pg at cs.stanford.edu>> wrote: >>> >>> Hi everyone, >>> >>> I'm helping someone who's struggling to compile Klee right now, and >>> I've used my CDE tool (http://www.stanford.edu/~pgbovine/cde.html) >>> to create a completely self-contained package so that new Klee users >>> can get up-and-running without first installing any of its pesky >>> dependencies. The package is 151MB and located here: >>> >>> http://keeda.stanford.edu/~pgbovine/klee-cde-package.v1.tar.bz2 >>> >>> Feedback and testing would be greatly appreciated :) >>> >>> Daniel - if you think this is useful, that would be awesome to get >>> this uploaded to the official Klee webpage. >>> >>> Thanks, >>> Philip >>> >>> >>> Here is the README file from the package: >>> --- >>> This package contains a self-contained distribution of Klee and all of >>> its associated dependencies (e.g., llvm-2.7, llvm-gcc, uClibc, svn). >>> Using this package, you can: >>> >>> 1.) Compile target programs using llvm-gcc >>> 2.) Run Klee on target programs compiled with llvm-gcc >>> 3.) Hack on Klee's source code and re-compile it to build a new Klee >>> binary >>> 4.) Pull the latest Klee source code updates from SVN >>> >>> ... all without compiling or installing anything on your Linux >>> machine! >>> >>> The only requirement is that you are running a reasonably-modern >>> x86-Linux distro that can execute 32-bit ELF binaries. >>> >>> --- >>> >>> Instructions: >>> >>> 1.) Compile a target program using llvm-gcc >>> >>> I've put an example program in: >>> cde-root/home/pgbovine/test-programs/islower.c >>> >>> To compile it into LLVM object code, run: >>> >>> cd cde-root/home/pgbovine/test-programs/ >>> ./llvm-gcc.cde -I../klee/include --emit-llvm -c -g islower.c >>> >>> This will create a file called islower.o, which is ready to be run >>> through Klee. >>> >>> >>> 2.) Run Klee on the compiled target program >>> >>> cd cde-root/home/pgbovine/test-programs/ >>> ./klee.cde islower.o >>> >>> This should create klee-out-* and klee-last sub-directories, which >>> contain the output of Klee from running on islower.o >>> >>> To see all of the myriad of Klee options, run: >>> ./klee.cde --help >>> >>> >>> 3.) Hacking on Klee source code >>> >>> The Klee source code is located in: cde-root/home/pgbovine/klee/ >>> >>> You can freely edit the source code, and then to compile, run: >>> cd cde-root/home/pgbovine/klee/ >>> ./make.cde >>> >>> (Note that running your system's native 'make' will NOT work; you must >>> run make.cde!) >>> >>> This will create a new Klee binary in: >>> cde-root/home/pgbovine/klee/Release+Asserts/bin/klee >>> >>> >>> ("./make.cde clean" doesn't seem to work too well right now, though.) >>> >>> >>> 4.) Updating to the latest Klee source from SVN >>> >>> cd cde-root/home/pgbovine/klee/ >>> ./svn.cde up >>> >>> (Note that running 'svn' might not work if you have an incompatible >>> version of SVN installed, but './svn.cde' should always work since it >>> runs the version of svn in the package, which exactly matches the >>> format >>> of the .svn/ directories within cde-root/home/pgbovine/klee/.) >>> >>> >>> >>> >>> _______________________________________________ >>> klee-dev mailing list >>> klee-dev at keeda.stanford.edu >>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >>> >> _______________________________________________ >> 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/20110526/124e7fbd/attachment.html
