KLEE does not find uninitialized variable error

Question

I am learning KLEE now and I wrote a simple code:

#include "klee/klee.h"
#include <stdio.h>
#include <stdlib.h>

int test(int *p)
{
    int *q = (int *) malloc(sizeof(int));

    if ((*p) == (*q)) {
       printf("reading uninitialized heap memory");
    }
    return 0;
}


int main()
{
    int *p = (int *) malloc(sizeof(int));
    test(p);
    return 0;
}

First, I generate LLVM bitcode, and then I execute KLEE to the bitcode. Following is all output:

KLEE: output directory is "/Users/yjy/WorkSpace/Test/klee-out-13"
Using STP solver backend
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING ONCE: calling external: printf(140351601907424)
reading uninitialized heap memory
KLEE: done: total instructions = 61
KLEE: done: completed paths = 4
KLEE: done: generated tests = 4

I suppose that KLEE should give me an error that the q pointer is not initialized, but it doesn't. Why KLEE does not give me an error or warning about this? KLEE can not detect this error? Thanks in advance!

Answer 1

TLTR: KLEE has not implemented this feature. Clang can check this directly.

KLEE currently support add/sub/mul/div overflow checking. To use this feature, you have to compile the source code with clang -fsanitize=signed-integer-overflow or clang -fsanitize=unsigned-integer-overflow .

The idea is that a function call is inserted into the bytecode (e.g. __ubsan_handle_add_overflow) when you use the clang sanitizer. Then KLEE will handle the overflow checking once it meets the function call.

Clang support MemorySanitizer, AddressSanitizer UndefinedBehaviorSanitizer. They are defined in projects/compiler-rt/lib directory. MemorySanitizer is the one you are looking for, which is a detector of uninitialized reads.

You can remove the KLEE function call and check with clang directly.

➜  ~ clang -g -fsanitize=memory st.cpp
➜  ~ ./a.out
==16031==WARNING: MemorySanitizer: use-of-uninitialized-value
    #0 0x490954  (/home/hailin/a.out+0x490954)
    #1 0x7f21b72f382f  (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #2 0x41a1d8  (/home/hailin/a.out+0x41a1d8)

SUMMARY: MemorySanitizer: use-of-uninitialized-value (/home/hailin/a.out+0x490954)
Exiting