静的解析を通じて結合型をタグ付き結合型に変換する
静的解析を使って、ユニオンをタグ付きユニオンに変換する系統的なアプローチ。
― 1 分で読む
このセクションでは、タグ付き共用体にタグを持つ共用体を変えるのを助ける「静的解析」と呼ばれる方法について話すよ。この解析の目的は、共用体内のタグフィールドを特定して、それぞれの共用体フィールドに割り当てられたタグ値を見つけること。プロセスは主に4つのステップから成り立ってるよ:候補構造体の探査、プログラム内の異なる領域を指すポイントの確認、特定の関数の分析、そして最後に結果を解釈すること。
候補の特定
最初のステップは、共用体が含まれている可能性のある構造体と、タグとして使えるフィールドを見つけることだよ。これらの構造体を基に、どの関数を調べるかも決めるよ。適合する構造体が見つからなければ、解析は終わりで、タグ付き共用体に変える共用体はないと結論するんだ。
候補構造体を特定するために、まずタグに適したフィールドの定義をするよ。これはタグフィールドとして使えるフィールドだ。そして、フィールドがタグに適していると見なされるためには、3つの基準を満たす必要があるよ:
- 整数型であること。
- 割り当てに使われるときは、等号(=)を使うこと、+=のような他の演算子を使ってはいけない。
- ポインタで参照されないこと。
2つ目と3つ目の基準は重要で、タグ付き共用体は整数をタグとして使うことができなく、フィールドとして参照されることもできないから。だから、こうした使い方をするフィールドはタグ付き共用体に変えられないんだ。
次に、候補共用体が何かを定義するよ。共用体は次の条件を満たすと候補だ:
- 1つ以上のタグに適したフィールドを持つ構造体のフィールドであること。
- 名前が「C2RustUnnamed」で始まること。これは元のコードで匿名の共用体だから。共用体に名前がある場合、それはその構造体の外に独立して存在できるので、タグ付き共用体としては不適切なんだ。
最終的に候補構造体は、少なくとも1つの候補共用体を持っているものだよ。
それじゃ、どの関数を分析すべきかを決めるよ。共用体のためのタグフィールドとその値を見つけるためには、候補構造体のフィールドにある可能性のある値を知る必要があるんだ。もし関数がフィールドを読み書きしないと、そのフィールドの値についての情報は得られないから、候補構造体のフィールドにアクセスする関数だけに焦点を当てるよ。
可能性のポイント指向分析
次のステップは、プログラム全体に対する可能性のポイント指向分析を行うこと。これは次の「必須ポイント指向分析」の信頼性のために必要不可欠なステップだよ。
この分析にはフィールド感度のアプローチを適用するよ。つまり、コードの順序に影響されない形でフィールドがどのように関連しているかを見るんだ。他の可能性のポイント指向分析もあるけど、それらはそこまで精度が高くなく、必須ポイント指向分析には信頼できない結果をもたらすんだ。
必須ポイント指向分析
次は必須ポイント指向分析に焦点を当てるよ。これは選択した関数ごとに行う。その方法は、他の研究に見られる典型的な必須ポイント指向分析に似ているよ。各ポイントのプログラムの状態はグラフで示され、ノードがメモリの位置を表し、エッジがそれらの関係を示すんだ。
分析は、システムが安定点に達するまで各ポイントでの状態を更新していくよ。各状態は、前の状態と現在の命令の効果を組み合わせて作成されるんだ。
これらのグラフを視覚化するために、ローカル変数の名前からメモリ位置を表すノードへの矢印を描くよ。ここで重要なのは、変数名そのものはノードではなく、矢印は単に接続を示すものだということ。
例えば、x = y
があったとすると、グラフにはx
とy
のノードがあって、x
がy
が格納されている場所を指していることがわかるんだ。
必須ポイント指向関係を分析する際には、ノードにタグ@
を付けてフィールドの整数値を追跡するよ。このラベルは、その場所に格納されている可能性のある整数値について教えてくれるんだ。ノードにラベルがなければ、通常のCの値を保持しているってことだよ。
この方法は、整数値を効率的に伝播するのに役立つよ。例えば、もしx = 1
で、その後y = x
があった場合、直接確認することなくy
も1であると結論付けることができるんだ。
共用体を使ったコードの分析
次に、共用体を使用したコードを分析する方法を考えてみよう。例えば、式を評価する関数を見てみると、特定のコード行の後に異なるフィールド間の関係を視覚化できるんだ。
数行のチェック後、kind
の値に基づいて共用体の特定のフィールドがアクセスされていることがわかるかもしれない。それによって、これらの共用体で作業する際に可能な値を追跡できるって結論に至るんだ。
グラフの結合
もっと複雑な状況では、2つのグラフを結合する必要が出てくるかもしれない。例えば、コードの一つのブランチが特定の値にkind
を設定し、別のブランチが異なることをしている場合、これらのグラフを組み合わせて共用体フィールドが取る可能性のあるすべての値を見る必要があるんだ。
結合する際は、必須のポイント指向関係を維持し、それらのエッジに関連する整数値を結合するよ。こうすることで、グラフは現在のプログラム状態を正確に反映するんだ。
必須ポイント指向分析における可能性のポイント指向の利用
時々、ポインタが異なる場所を指していることがおわかりかもしれない。そういう場合、ポインタがどこに導くかを追跡する必要があるんだ。例えば、ポインタが2つの異なる場所を指している場合、その不確実性を反映するようにグラフを調整しなければならないんだ。
分析の中で、現在の実行に対して成立しない関係を削除するよ。可能性のポイント指向関係に依存することで、変数の値について誤った仮定を避けられる。これにより、値の書き込みと読み取りの間に起こる変更にもかかわらず、分析は正確に保たれるんだ。
結果の解釈
最後のステップは、必須ポイント指向分析から得られた結果を解釈することだよ。まず、共用体のフィールドに対するタグ値を特定するところから始めるよ。ここでの目標は、特定のフィールドが共用体のタグフィールドとして使えるかどうかを確認し、もしそうならそのタグ値が何であるかを判断することなんだ。
分析した関数内の各プログラムポイントをチェックして、アクセスされているフィールドがあるかどうかを探すよ。もしフィールドがアクセスされていたら、以前の分析に基づいて可能な値を確認するんだ。
このステップを通じて、共用体フィールドに関連するタグ値に関する情報を集めるよ。もし値が複数の場所で現れたら、それはフィールドがタグとして使われるのを妨げるから、捨てるんだ。
最後に、すべての可能なタグ値を集め、共用体フィールドに既に関連付けられているものを取り除くよ。最終的には、各候補構造体について、そのフィールドが関連する値に基づいてタグフィールドとして使えるかどうかを確認するためにプロセスを適用するんだ。
最終的な目標は、最も異なるタグ値を提供するフィールドを探すこと。そして、その要件を満たすものがタグ付き共用体のタグフィールドとして選ばれるんだ。
これらのステップを完了することで、タグを持つ共用体をタグ付き共用体に効果的に変換できるし、プログラム分析全体で正確さを保つことができるんだ。
タイトル: To Tag, or Not to Tag: Translating C's Unions to Rust's Tagged Unions
概要: Automatic C-to-Rust translation is a promising way to enhance the reliability of legacy system software. However, C2Rust, an industrially developed translator, generates Rust code with unsafe features, undermining the translation's objective. While researchers have proposed techniques to remove unsafe features in C2Rust-generated code, these efforts have targeted only a limited subset of unsafe features. One important unsafe feature remaining unaddressed is a union, a type consisting of multiple fields sharing the same memory storage. Programmers often place a union with a tag in a struct to record the last-written field, but they can still access wrong fields. In contrast, Rust's tagged unions combine tags and unions at the language level, ensuring correct value access. In this work, we propose techniques to replace unions with tagged unions during C-to-Rust translation. We develop a static analysis that facilitates such replacement by identifying tag fields and the corresponding tag values. The analysis involves a must-points-to analysis computing struct field values and a heuristic interpreting these results. To enhance efficiency, we adopt intraprocedural function-wise analysis, allowing selective analysis of functions. Our evaluation on 36 real-world C programs shows that the proposed approach is (1) precise, identifying 74 tag fields with no false positives and only five false negatives, (2) mostly correct, with 17 out of 23 programs passing tests post-transformation, and (3) efficient, capable of analyzing and transforming 141k LOC in 4,910 seconds.
著者: Jaemin Hong, Sukyoung Ryu
最終更新: 2024-09-16 00:00:00
言語: English
ソースURL: https://arxiv.org/abs/2408.11418
ソースPDF: https://arxiv.org/pdf/2408.11418
ライセンス: https://creativecommons.org/licenses/by/4.0/
変更点: この要約はAIの助けを借りて作成されており、不正確な場合があります。正確な情報については、ここにリンクされている元のソース文書を参照してください。
オープンアクセスの相互運用性を利用させていただいた arxiv に感謝します。