클레

Question

어떻게 상징적 인 매개 변수를 사용하여 루프의 경우 KLEE (상징적 실행 도구) 노력에 대한 질문이 : 우리는이 코드 클레을 실행하면

int loop(int data) { 
    int i, result=0; 
    for (i=0;i<data ;i++){ 
    result+= 1; 
    //printf("result%d\n", result); //-- With this line klee give different values for data 
} 
    return result; 
} 
void main() { 
    int n; 
    klee_make_symbolic(&n, sizeof(int),"n"); 
    int result=loop(n) ; 
} 

것은,이 줄을 단 하나의 테스트 케이스. 그러나 printf (...)의 주석을 제거하면 n에 대한 값을 생성하기 때문에 실행을 중지하는 데 필요한 유형의 컨트롤이 필요합니다. --max-depth = 200

클레어에게 왜 다른 행동이 필요한지 이해하고 싶습니다. 그것은 저에게 감각이 없습니다. 이 코드에 printf가 없으면 동일한 값을 생성하지 않습니다.

동일한 동작이없는 경우 --optimize 옵션이 사용 된 경우 이 발견되었습니다. 누가 Klee의 최적화 된 작업을하는지 알아?

다른 퀴스톤은 그들이 발행 한 논문에있는 경우, 그들이 발견 한 바에 따르면 휴리스틱 서치로 무한하지 않을 것입니다. (굶주림을 피합니다) 왜냐하면 나는 달리기를하지 않기 때문입니다. 이 루프의 경우에는 klee 실행을 완료해야합니다. 사전에

덕분에

Answer 1

내가 알고 싶은 것은 왜 옵션 --optimize이 다른 행동. 감사합니다

에서

C/C++ "정의되지 않은 동작"(참조의 개념이 : 모든 C 프로그래머가 정의되지 않은 동작 [#1/3]에 대해 알아야 할 C 및 C++, Part1, Part 2, Part 3에서 정의되지 않은 행동에 가이드는 [#2/3] , [#3/3]).

이 signed 정수 오버 플로우가 컴파일러는이 같은 물건을 최적화 할 수 있도록하기 위해 정의되지 않은 동작으로 정의된다

:

bool f(int x){ return x+1>x ? true : false ; } 

이의 생각하게하는 x + 1> X 일반 대수는 항상 true입니다 이 모듈 대수에가 (오버 플로우 한 경우를 제외하고) 거의 항상 사실이다, 그래서로 돌려 보자

true 

이러한 관행은 큰 최적화의 엄청난 금액을 수 있습니다. 오버플로시 동작을 정의하려면 unsigned 정수를 사용하십시오.이 기능은 암호화 알고리즘 구현에 광범위하게 사용됩니다. 한편

때때로이 코드처럼 놀라운 결과에 리드 :

int main(){ 
    int s=1, i=0; 
    while (s>0) { 
     ++i; 
     s=2*s; 
    } 
    return i; 
} 

이 무한 루프에 최적화되어있다. 그것은 버그가 아니야! 강력한 기능입니다! (다시 .. 정의 된 동작에 대해서는 unsigned을 사용하십시오).

의 위의 예제 어셈블리 코드를 생성하자 루프 부분의

$ g++ -O1 -S -o overflow_loop-O1.s overflow_loop.cpp 
$ g++ -O2 -S -o overflow_loop-O2.s overflow_loop.cpp 

확인이 다르게 컴파일 :

overflow_loop-O1.s을 :

(...) 
.L2: 
    addl $1, %eax 
    cmpl $31, %eax 
    jne .L2 
(...) 

overflow_loop-O2.s :

(...) 
.L2: 
    jmp .L2 
(...) 

다른 최적화 수준 (gcc -S -O0 대 gcc -S -O1 ... -O3)에서 코드 어셈블리를 확인하는 것이 좋습니다. 주제에 대한 그리고 다시, 좋은 게시물 : [1], [2], [3], [4], [5], [6].