0

C言語で書かれたターゲットプログラムのループをソースコードレベルで自動巻き戻ししたい(参考までにlinuxとgccコンパイラを使っています)。詳細な説明については、次の簡単なソース コードを見てみましょう。

1: int main(){
2:   int i = 0;
3:   while(i<3){
4:     printf("hi\n");
5:     i++;
6:   }
7: }

上記のソースコードを次のように変換したいと思います。

1: int main(){
2:   int i = 0;
3:   if (i<3){
4:     printf("hi\n");
5:     i++;
6:   }
7:   if (i<3){
8:     printf("hi\n");
9:     i++;
10:  }
11:  if (i<3){
12:    printf("hi\n");
13:    i++;
14:  }
15:}

CBMCがソフトウェア モデル チェックのためにループを自動的に巻き戻すことは知っていますが、ループを巻き戻すために CBMC がソース コードをソース コードに変換するかどうかはわかりません。すべてのループが巻き戻されたプログラム ソース コードを取得する必要があります。

そのためのツールや解決策を見つけようとしましたが、見つかりませんでした。提案やコメントをいただければ幸いです。ありがとう！

混乱させてすみません。私の最終目標である「ソースコードレベルでのループの巻き戻し」の詳細を説明します。ループの巻き戻しの最終的な目標は、ループの巻き戻しから生成されたステートメントを実行するテスト ケースの数を測定することです。次の例を参照してください。

1: void ex(int i){
2:   int i = 0;
3:   while(i<3){
4:     printf("hi\n");
5:     i++;
6:   }
7: }

上記のソースコードを変換すると、次のソースコードが得られます

1: void ex(int i){
2:   if (i<3){
3:     printf("hi\n");
4:     i++;
5:   }
6:   if (i<3){
7:     printf("hi\n");
8:     i++;
9:   }
10:  if (i<3){
11:    printf("hi\n");
12:    i++;
13:  }
14:}

そして、上記の変換されたソース コードから、「ループの巻き戻し」から生じる各ステートメントを実行するテスト ケースの数を測定します。たとえば、元のソース コードの 4 行目と 5 行目から変換された 3、4 行目、7、8 行目、または 11、12 行目を実行するテスト ケースの数は、1 行を実行するテスト ケースの数とは異なります。元のソース コードの #4,5。

参考までに、ループを巻き戻さずに最終目標を達成できる方法があれば、その方法も良いです! ありがとう！

4

3 に答える 3

1

ほとんどの場合、gcc は、あるコードがコードの展開に適しているかどうかを判断する際に、ユーザーよりも優れた仕事をします。私の経験では、gcc よりも優れた仕事ができることは非常にまれです。唯一の合理的なケースは、「奇妙な」ことを行う非常に複雑なコードがある場合であり、あなたの例ではそうではありません。

-S オプションを最適化とともに実際に使用して、コンパイラの動作を確認しましたか?

もちろん、printf() はすべてのループを合わせたものよりもはるかに重いため、コンパイラはこの特定のループを最適化しないことに意味があるかもしれませんが、それは少し別の問題です。

于 2012-12-31T08:21:41.323 に答える
0

ループ展開は、GCC によって (少なくとも-O2またはで-O3) 行われる (多くの) 最適化の 1 つにすぎず、それ自体には意味がありません。(定数伝播など、他の最適化を介してのみ役立ちます)。

また、ソース コードだけが必要なわけではありません (多くのマクロが、ループ展開されるforループに展開される可能性があることを想像してください)。

たとえば、GCC を拡張するための高レベルのドメイン固有言語であるMELTを使用して、GCC コンパイラを拡張することをお勧めします。

(または、時間がたくさんある場合は、GCC プラグインを C でコーディングするのが面倒です) .

次に、いくつかのループ展開 (およびその他の最適化) パスの後に、Gimple の内部表現を処理するパスを追加します (Gimple は、C に似た「最小限の」言語であり、基本的な操作x = y + z;や呼び出し、および のような単純なテストのみを備えていると理解できますif (x > y) goto l;) 。 .

しかし、私はあなたが結果をどうしたいのかまだ理解していません。さらに分析したい場合は、(おそらく MELT でコード化された別のパスを使用して) コンパイラー内の GCC 内部表現を処理します。その「展開された」コードを何らかの外部ツールにフィードしたい場合は、Gimple を適切な形式に変換する変換パスを記述します。

于 2012-12-31T08:15:51.640 に答える
0

アセンブラを調べて、コンパイラが実際にループのアンローリングでどの程度優れているかを確認する必要があります。しかし、コンパイラのプログラミングを少し改善することもできます。

for (unsigned i = 0; i < 3; ++i) {
  printf("hi\n");
}

これは、符号なし整数型をループ変数として使用し (size_t多くの場合、良い考えです)、ループ変数をローカルにします。-S -O3 -march=native次に、コンパイラ オプションなどを使用してアセンブラを検査します。

その後、結果に満足できない場合は、P99を調べてください。ループだけでなく、展開を行うための一連のマクロがあります。のようなものを探しP99_FORます。

于 2012-12-31T08:17:32.233 に答える