[klee-dev] Using WLLVM together with overflow sanitizers

[Martin Hořeňovský]

Hello,

I've been trying to use wllvm to create bitcode archive for klee, but
I ran into some trouble when trying to use it together with overflow
sanitizers.

I tried a minimal test case overflow.c:
#include "klee/klee.h"

int main(){
    int a, b;
    volatile int c;
    klee_make_symbolic(&a, sizeof(a), "a");
    klee_make_symbolic(&b, sizeof(b), "b");

   c = a + b;
   c = a - b;
   c = a * b;

   return 0;
}

if I use clang (version 3.3, compiled from sources on llvm project
website) like this:
clang -c -emit-llvm -fsanitize=integer overflow.c
I can feed the resulting .o file into klee and get expected result.
(Which is 4 paths, three of them leading to error.)

and if I use wllvm (after setting LLVM_COMPILER to clang) without
sanitizers, this works:

wllvm -lkleeRuntest overflow.c
extract-bc a.out
klee a.out.bc

but the results from klee is a single path and no overflow checking.

However, if I use wllvm:
wllvm -fsanitize=integer overflow.c -lkleeRuntest
I get undefined reference to '__ubsan_handle_mul_overflow'  (and to
the other two handlers)

and after changing wllvm invocation to
wllvm -fsanitize=integer overflow.c -lkleeRuntest -llvm
-fsanitize=integer overflow.c -lkleeRuntest -lclang_rt.ubsan-x86_64 -L
/home/martin/.aux/lib/clang/3.3/lib/linux/

I get a massive wall of errors that boils down to multiple definitions
of various ubsan functions. (Full error text dump is here:
http://pastebin.com/DC404z8U)

So I wonder, has anyone successfully used wllvm with sanitizers?

(I need to use wllvm because I have a rather large library that is
nontrivial to build, that I want to check against overflows as well.)