KLEE nicht findet nicht initialisierten Variablen Fehler

Question

ich KLEE jetzt lerne und ich schrieb einen einfachen 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; 
} 

Zuerst erzeugen ich LLVM Bitcode, und dann an den Bitcode ich ausführen KLEE. Im Anschluss ist die gesamte Ausgabe:

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 

Ich nehme an, dass KLEE mir einen Fehler geben soll, dass der q-Zeiger nicht initialisiert wird, aber es funktioniert nicht. Warum gibt mir KLEE keinen Fehler oder eine Warnung? KLEE kann diesen Fehler nicht erkennen? Danke im Voraus!

Answer 1

TLTR: KLEE hat diese Funktion nicht implementiert. Clang kann dies direkt überprüfen.

KLEE unterstützt derzeit die Überprüfung von Add/Sub/Mul/Div-Überläufen. Um diese Funktion nutzen zu können, müssen Sie den Quellcode mit clang -fsanitize = signed-integer-overflow oder clang -fsanitize = unsigned-integer-overflow kompilieren.

Die Idee ist, dass ein Funktionsaufruf in den Bytecode eingefügt wird (z. B. __ubsan_handle_add_overflow), wenn Sie den Clang-Desinfektor verwenden. Dann behandelt KLEE die Überlaufüberprüfung, sobald es den Funktionsaufruf erfüllt.

Clang-Unterstützung MemorySanitizer, AddressSanitizerUndefinedBehaviorSanitizer. Sie sind im Verzeichnis projects/compiler-rt/lib definiert. MemorySanitizer ist derjenige, nach dem Sie suchen, der ein Detektor nicht initialisierter Lesevorgänge ist.

Sie können den KLEE-Funktionsaufruf entfernen und direkt mit clang überprüfen.

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