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 >
