search

markaduol / UROP

Using symbolic execution to identify semantic inconsistencies between implementations of the same function declaration across different repository revisions.
0 stars 1 forks source link

Add tutorial #3

Closed andreamattavelli closed 7 years ago

andreamattavelli commented 7 years ago

Some notes from our discussion:

src -> drivers for the experiments

llvm-passes -> passes

llvm-passes 
    ./build_script.sh to build the LLVM pass

third_party
    git submodule init
    git submodule update

upb https://github.com/google/upb
    export LLVM_COMPILER=clang
    CC=wllvm make
    cp -R pub upb-2
    cd upb-2
    git checkout 1aafd41
    CC=wllvm make clean all
    cd lib
    extract-bc -b libupb.a   // -b get bitcode
    extract-bc -b ../upb/lib/libupb.a
    cd $(MAIN)
    cp ../upb/lib/libupb.a.bc ../../../libupb1.a.bc
    cp ../upb-2/lib/libupb.a.bc ../../../libupb2.a.bc
    opt -load llvm-passes/build/functionrename/libFunctionRenamePass.so - functsionrename < libupb2.a.bc > libupb2.a.bc
    llvm-link -o libupb.a.bc libupb1.a.bc libupb2.a.bc
    cd src
    klee-clang -g -I third_party/upb src/td1.c
    klee -link-llvm-lib=../libupb.a.bc td1.bc
markaduol commented 7 years ago

Done.

andreamattavelli commented 7 years ago

Great thanks!