2

シンボリック パラメーターを使用したループの場合、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) ;
}

このコードで klee を実行すると、テスト ケースは 1 つだけになります。ただし、printf(...) のコメントを削除すると、klee は実行を停止するための何らかの制御が必要になります。これは、n の値を生成するためです: --max-depth= 200

クレーがこのように異なる振る舞いをする理由を理解したいのですが、それは私には意味がありません。このコードに printf がない場合、同じ値が生成されないのはなぜですか。

オプション --optimize が使用されていない場合に同じ動作が発生することがわかりました。Klee の --optimize がどのように機能しているか知っている人はいますか?

同じことについての別の疑問は、彼らが公開した論文の場合、私が理解しているように、彼らのヒューリスティック検索では無限にならないと言われていることです (彼らは飢餓を回避します)。このループの場合、クレーの実行を終了する必要がありますか?

前もって感謝します

4

1 に答える 1

0

私が知りたいのは、オプション --optimize を使用した場合のこの異なる動作の理由です。ありがとう

C/C++ には、「未定義の動作」の概念があります (参照: C および C++ における未定義の動作のガイド、第 1 部、第 2 部、第 3 部、すべての C プログラマーが未定義の動作について知っておくべきこと[#1/3]、[ #2/3] , [#3/3] )。

signed整数のオーバーフローは、コンパイラが次のような最適化を実行できるようにするために、未定義の動作として定義されています。

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

考えてみましょう... 通常の代数では x+1>x は常に真ですが、このモジュロ代数ではほとんどの場合真です (オーバーフローの 1 つのケースを除く)。

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
(...)

オーバーフローループ-O2.s:

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

コードのアセンブリをさまざまな最適化レベル ( gcc -S -O0vs gcc -S -O1... -O3) でチェックすることをお勧めします。また、トピックに関する素敵な投稿: [1] , [2] , [3] , [4] , [5] , [6] .

于 2012-10-18T10:46:32.843 に答える