KLEE는 초기화되지 않은 변수 오류를 지금 KLEE을 배우고

Question

를 찾을 수없는 나는 간단한 코드 작성 :

#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 나에게 질문 포인터가 초기화되지 않는다는 오류를 제공해야한다고 생각하지만 그렇지 않습니다. 왜 KLEE이 나에게이 오류나 경고를주지 않는 이유가 무엇입니까? KLEE이 오류를 감지 할 수 없습니까? 미리 감사드립니다!

Answer 1

TLTR : KLEE은이 기능을 구현하지 않았습니다. Clang이 직접 확인할 수 있습니다.

KLEE은 현재 add/sub/mul/div 오버 플로우 검사를 지원합니다. 이 기능을 사용하려면 clang -fsanitize = signed-integer-overflow 또는 clang -fsanitize = unsigned-integer-overflow를 사용하여 소스 코드를 컴파일해야합니다.

clang 위생 처리기를 사용할 때 함수 호출이 바이트 코드 (예 : __ubsan_handle_add_overflow)에 삽입된다는 아이디어가 있습니다. 그런 다음 KLEE은 함수 호출을 충족하면 오버플로 검사를 처리합니다.

clang support MemorySanitizer, AddressSanitizerUndefinedBehaviorSanitizer. 그것들은 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