[klee-dev] Using WLLVM together with overflow sanitizers

[Dingbao Xie]

I can do that by modifying the source code of whole-program-llvm.

In whole-program-llvm/driver/utils.py, the modified part is marked as red :

class ClangBuilder(BuilderBase):
    def __init__(self, cmd, isCxx, prefixPath=None):
        super(ClangBuilder, self).__init__(cmd, isCxx, prefixPath)

    def getBitcodeCompiler(self):
        cc = self.getCompiler()
        return cc + ['-emit-llvm', '-fsanitize=undefined', '-g']

    def getCompiler(self):
        if self.isCxx:
            return ['{0}clang++'.format(self.prefixPath),
'-fsanitize=undefined']
        else:
            return ['{0}clang'.format(self.prefixPath), '-fsanitize=undefined',
'-g']

On Thu, Mar 26, 2015 at 4:03 PM, Martin Hořeňovský <
martin.horenovsky at gmail.com> wrote:

> 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.)
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>



-- 
Dingbao Xie
-------------- next part --------------
HTML attachment scrubbed and removed