Skip to content

sdasgup3/symbolic-analysis

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

sudo yum install g++ curl dejagnu subversion bison flex bc libcap-devel
export PATH=$PATH:/home/sdasgup3/llvm/llvm-gcc4.2-2.9-x86_64-linux/bin/
/*To Find the tarball @
http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
*/

Build llvm 2.9

tar zxvf llvm-2.9.tgz
cd llvm-2.9
./configure --enable-optimized --enable-assertions
make

Build stp

tar xzfv stp-r940.tgz /*Find the tarball http://www.doc.ic.ac.uk/~cristic/klee/stp.html */
cd stp-r940
./scripts/configure --with-prefix=`pwd`/install --with-cryptominisat2
make OPTIMIZE=-O2 CFLAGS_M32= install
ulimit -s unlimited

Build uclibc

git clone --depth 1 --branch klee_0_9_29 https://github.com/ccadar/klee-uclibc.git
/*
In case u want to do some dev oin uclibc then use the following:
git clone --branch klee_0_9_29 https://github.com/ccadar/klee-uclibc.git
*/
cd klee-uclibc/
export PATH=$PATH:/home/sdasgup3/llvm/llvm-2.9/Release+Asserts/bin/
/* or
export PATH=$PATH:/home/sdasgup3/llvm/llvm-3.4.2/llvm-build/Release+Asserts/bin/
module load gcc
*/
./configure -l  
/*  
./configure --make-llvm-lib
https://github.com/klee/klee-uclibc/wiki/Getting-started
*/
make -j2

Build llvmpa

setenv LD_LIBRARY_PATH /software/gcc-4.8.2/lib64:/software/gcc-4.8.2/lib:/usr/lib64
module load gcc
../llvmpa/configure --with-llvmsrc=/home/sdasgup3/llvm/llvm-3.4.2/llvm-src/ --with-llvmobj=/home/sdasgup3/llvm/llvm-3.4.2/llvm-build --with-gcc-toolchain=/software/gcc-4.8.2 --with-extra-options=-std=c++11 --with-extra-ld-options="-Wl,-rpath,/software/gcc-4.8.2/lib64" --enable-optimized --enable-assertions
make

Build poolalloc

../SymbolicAnalysis/poolalloc/configure --with-llvmsrc=/home/kasampa2/Documents/llvm/llvm.src --with-llvmobj=/home/kasampa2/Documents/llvm/llvm.obj --with-gcc-toolchain=/home/kasampa2/Documents/gcc/gcc-4.8.2.inst --with-extra-options=-std=c++11 --with-extra-ld-options=-Wl,-rpath,/home/kasampa2/Documents/gcc/gcc-4.8.2.inst/lib64 --disable-optimized --enable-assertions

make CXXFLAGS+=-std=c++11 ENABLE_OPTIMIZED=1

Build klee/zesti

git clone https://github.com/ccadar/klee.git //for klee
tar -xvf zesti.tar.gz
cd klee/zesti
./configure --with-llvm=/home/sdasgup3/llvm/llvm-2.9/ --with-stp=/home/sdasgup3/klee/stp-r940/install/ --with-uclibc=/home/sdasgup3/klee/klee-uclibc/ --enable-posix-runtime

/*
or
./configure --with-llvmsrc=/home/sdasgup3/llvm/llvm-3.4.2/llvm-src/ --with-llvmobj=/home/sdasgup3/llvm/llvm-3.4.2/llvm-build/ --with-stp=/home/sdasgup3/SymbolicAnalysis/stp-r940/install/ --with-uclibc=/home/sdasgup3/SymbolicAnalysis/klee-uclibc/ --enable-posix-runtime
*/

When building zesti add these options to configure to help it find llvmpa:
--with-llvmpasrc=/path/to/llvmpa/src/tree
--with-llvmpaobj=/path/to/llvmpa/obj/tree
Ex:
./configure --with-llvmsrc=/home/sdasgup3/llvm/llvm-3.4.2/llvm-src/ --with-llvmobj=/home/sdasgup3/llvm/llvm-3.4.2/llvm-build/ --with-stp=/home/sdasgup3/zesti_utils//stp-r940/install/ --with-uclibc=/home/sdasgup3/zesti_utils/klee-uclibc/ --with-llvmpasrc=/home/sdasgup3/llvmpa/ --with-llvmpaobj=/home/sdasgup3/llvmpa-build/ --enable-posix-runtime

Also, add these options to configure to help it find poolalloc:
--with-poolallocsrc=/path/to/poolalloc/src/tree
--with-poolallocobj=/path/to/poolalloc/obj/tree

/* In case stuck in problems
sudo ln -s /usr/include/x86_64-linux-gnu/asm/ /usr/include/asm
In case of prblms like C compiler not working
sudo apt-get remove gcc
sudo apt-get install gcc
sudo apt-get install g++
*/
make ENABLE_OPTIMIZED=1 
make check  //optional
make unittests  //optional

Running Testcase with checker

// The detailed commands can be viewed from Scripts/build.pl. Also find the Makefiles required from Scripts folder.

make clean
make $test LLVM_BIN=$llvm_bin_3_4 LLVMPALIB=$llvmpalib KLEEINCLUDE=$kleeincl
make $test-kleecheck LLVM_BIN=$llvm_bin_3_4 LLVMPALIB=$llvmpalib
cat $test-kleecheck.ll | sed 's/target datalayout.*//' | sed 's/\!llvm.ident =.*//' | sed 's/\!0 = metadata.*//' | sed 's/^attributes \#[0-9]*.*//' | sed 's/\#[0-9][0-9]*//' >  temp
mv temp $test-kleecheck.ll
$clang2_9 -emit-llvm -c $SCRIPTDIR/jf_checker_map.cpp -I $SCRIPTDIR -o jf_checker_map.bc
$llvmas2_9 < $test-kleecheck.ll  > a.bc
$llvmld2_9 -disable-opt a.bc  jf_checker_map.bc
$llvmdis2_9 < a.out.bc  > a.out.ll
cp a.out.bc $test.a.out.bc
zesti --zest --zest-depth-offset=$offset  --use-symbex=2 --symbex-for=10 --search=zest --zest-search-heuristic=br --zest-discard-far-states=false  ./$test.a.out.bc

Running withOUT checker (the llvm used must be compatible with klee build)

/home/sdasgup3/llvm/llvm-3.4.2/llvm-build//Release+Asserts/bin/clang -O0 -emit-llvm -I /home/sdasgup3/SymbolicAnalysis/zesti//include/klee -I ./ -c zesti_test_6.c -o zesti_test_6.a.out.bc 
/home/sdasgup3/llvm/llvm-3.4.2/llvm-build//Release+Asserts/bin/llvm-dis zesti_test_6.a.out.bc -o a.out.ll 
/home/sdasgup3/SymbolicAnalysis/zesti//Release+Asserts/bin/klee  --zest      -debug-print-instructions         --use-symbex=2 --symbex-for=10 --search=zest --zest-search-heuristic=br --zest-discard-far-states=false ./zesti_test_6.a.out.bc

Build libffi used for running lli

Follow the steps in http://www.linuxfromscratch.org/blfs/view/svn/general/libffi.html
to install libffi and then
1. export CPPFLAGS='-I/pathto/libffiinckude/'
2. export LDFLAGS='-L/pathto/libffilibs/'
3. export LD_LIBRARY_PATH to  point to the libffi libs
run confugure and make llvm




About

Customized symbolic analysis to find pointer analysis bugs

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 2

  •  
  •