KLEE не находит ошибку неинициализированной переменной

Question

Сейчас я изучаю KLEE и написал простой код:

#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;
}

Сначала я генерирую битовый код LLVM, а затем выполняю KLEE для битового кода. Следующее - все выходные данные:

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

Я предполагаю, что KLEE должен дать мне ошибку, что указатель q не инициализирован, но это не так. Почему KLEE не дает мне ошибки или предупреждения об этом? KLEE не может обнаружить эту ошибку? Заранее спасибо!

Answer 1

TLTR: KLEE не реализовал эту функцию. Clang может проверить это напрямую.

В настоящее время KLEE поддерживает проверку переполнения add/sub/mul/div. Чтобы использовать эту функцию, вы должны скомпилировать исходный код с помощью clang -fsanitize=signature-integer-overflow или clang -fsanitize=unsigned-integer-overflow .

Идея заключается в том, что вызов функции вставляется в байт-код (например, __ubsan_handle_add_overflow), когда вы используете дезинфицирующее средство clang. Затем KLEE обработает проверку переполнения, как только встретит вызов функции.

Clang поддержка MemorySanitizer, AddressSanitizer https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html. Они определены в каталоге projects/compiler-rt/lib. MemorySanitizer - это то, что вы ищете, это детектор неинициализированных операций чтения.

Вы можете удалить вызов функции KLEE и проверить с помощью clang напрямую.

➜  ~ 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