本研究の主題は,高い信頼性を持つCプログラム解析器の開発方法に関するものである.プログラムの実行時の振る舞いに関する性質を静的に調べるプログラム解析器は,コンパイラが生成する実行コードの性能を左右する主要な構成要素である.その不具合はコンパイラが生成する実行コードの不具合につながるため,その精度や効率と共に高い信頼性が求められている.

高信頼なプログラム解析器を開発する有力な方法のひとつに対象言語の形式的意味定義にもとづく方法が存在する.形式的意味定義は対象言語のプログラムの振る舞いを数学的な厳密さで定義したものである.形式的意味定義により,解析アルゴリズムがすべての場合に正しいことを数学的に証明することが可能となる.また,抽象解釈と呼ばれる手法を用いることで,正しさの証明しやすいアルゴリズムを系統的に設計することが可能である.Java等の理論的扱いの容易な一部の言語ではすでに実際の解析器の開発に用いられており,その有効性が報告されている.

しかしながら,C においては,このような形式的意味定義にもとづく開発は未だ実用に至っていない.最大の問題は,プログラム解析器の開発の基盤となりうる適切な形式的意味定義が存在しない点にある.Cは,型キャスト等の言語機能により具体的な実行環境に依存した記述を許している低レベル言語としての側面と,通常の高級言語のように抽象的な言語概念にもとづき意味が定められている高レベル言語としての側面が共存しているという特殊性を有している.既存のC の形式的意味定義は,低レベル言語としての側面にのみ着目し,型制約等の言語規格を無視しているもの,もしくは高レベル言語としての側面にのみ着目し,型キャスト等の低レベルな扱いが必要となる言語機能は対象外としているもの,のいずれかに分類される.前者の問題は,形式的意味定義に反映されていない言語規格の制約を前提とするプログラム解析器の正しさを証明することができない点である.後者の問題は,高信頼なプログラム解析器の開発において特に考慮の必要な言語機能が形式的意味定義に含まれておらず,そのような言語機能を用いるプログラムに対する解析の正しさが保証できない点である.

本研究の目的は,Cにおいても,形式的意味定義にもとづくプログラム解析器の開発を実現することである.我々はRML(Register Memory Language)と呼ぶ中間表現を設計し,その形式的意味定義を与える.RMLは,C プログラムの構文構造をほぼ維持したまま論理式で表す中間表現であり,その形式的意味をCの言語規格にもとづいて定義することで,高い信頼性を持つCプログラム解析器の開発基盤とすることができる.RMLの形式的意味定義は基本的にC の高レベルな側面に着目したもので,言語規格が定める型制約を忠実に反映している.Cの低レベルな側面が現れる型変換等の意味はパラメータ化されており,目的に応じた意味を高レベルな言語概念を用いて与えることができる.これにより,特にCの低レベルな側面に依存しないプログラムについては,既存の形式的意味定義では示すことのできない性質を示すことが可能である.

我々の定義が実用的なCプログラム解析器の開発に有用であることを示すため,代表的な解析器のひとつであるポインタ指示先解析器について,形式的意味定義にもとづきアルゴリズムを設計し,その正しさの証明を与えた.これは型変換と共用体を扱いうるポインタ指示先解析器の正しさに関するはじめての証明である.我々の枠組みでは,プログラムは基礎論理式の集合として表され,その意味は述語論理における理論(閉論理式の集合)として与えられる.解析器の仕様は,解析対象プログラムPの意味をcsem{P},解析によって判定したい性質を表す論理式を$phi$とするとき,$phi$がcsem{P}の論理的帰結になるかどうかの判定問題として定式化できる.我々は,この問題を抽象解釈にもとづき導出可能性問題に帰着し,その判定アルゴリズムを導く方法を示す.我々の知る限り,本手法は,形式的意味定義から抽象解釈を介してdeductive systemにもとづくアルゴリズムを導く最初のものである.

既存のコンパイラで用いるプログラム解析器を開発する場合,その対象となる中間表現は所与のものを用いる必要がある.しかしながら,多くのコンパイラにおいて中間表現の仕様は明確に定義されておらず,高信頼なプログラム解析器を開発する上で障害となっている.この問題に対し,我々はIIR(Identifier-based Intermediate Representation data model)と呼ぶデータモデルにもとづく中間表現の仕様記述方法を提案する.IIRは関係データモデルに一定の制限を加えたデータモデルであり,プログラムの中間表現をデータベース(関係の集合)としてモデル化することができる.中間表現の仕様は,スキーマおよび制約を表すHorn論理式によって記述される.後者の制約を論理型言語を用いて記述することで,実行可能仕様として利用することができる.提案手法を用いることで,製品Cコンパイラの中間表現の仕様を,実装と整合する仕様を形式的に記述することが可能となった.

本論文は5つのPartにより構成されている.主要部はPart IIからIVの3部である.Part IIおよびIIIでは,高い信頼性を持つCプログラム解析器の開発基盤となる中間表現RMLを導入し,それにもとづき高信頼なポインタ解析器の開発を行う.Part IVでは,中間表現の仕様記述に適したデータモデルであるIIRを導入し,それを用いて既存のCコンパイラの中間表現の仕様を記述する.RMLとIIRの関係は相補的である.RMLがCプログラムの抽象的な論理式表現であるのに対し,IIRは,RMLの具体的な表現を定義する際の仕様記述方法を与える.

各Partの内容は以下の通りである.

Part Iは導入部である.1章では,本研究の対象,動機,目的,方法を明らかにする.また,本研究に関連する従来研究の問題を指摘する.2章では,本論文で用いる基本的な用語,表記法を定義する.

Part IIでは,中間表現RMLの定義を行う.3章では,Cの標準言語規格を分析し,形式的意味を定義する際に生じる問題をあきらかにする.4章では,RMLの形式的意味定義の概要を示す.5章および6章では,RMLの静的・動的な形式的意味を定義する.7章は,本Partのまとめである.関連研究との比較を行い,その利点・欠点を議論する.

Part IIIでは,Part IIの成果をCプログラム解析器のひとつであるポインタ解析器の開発に適用した結果を示す.最初に,8章において,ポインタ解析について,その目的,関連研究,研究課題を説明する.また,Part IIの形式的意味を用いて,ポインタ解析問題を形式的に定義する.9章と10章では,8章で与えた問題定義にもとづき,その解析アルゴリズムを設計する方法を示す.9章では,形式的意味をその構造に沿って抽象化した抽象的意味を定義する.10章では,抽象的意味から解析アルゴリズムを導出する方法を示す.11章は,本Partのまとめである.

Part IVでは,中間表現の仕様記述を支援するための手法を提案する.12章では,本編の動機,これまでの問題点,および提案手法の概要を示す.13章では,提案する中間表現データモデルIIRを定義する.14章では,提案手法の適用事例として,製品Cコンパイラで用いている中間表現の仕様記述を行った結果を示す.15章では,IIRの応用可能性を示す.IIRではプログラムを関係の集合としてモデル化するが,この特徴は,仕様記述以外に,論理型言語を用いた宣言的なプログラム解析や永続化にも有用であることを示す.16章と17章では,提案手法を関連研究と比較し,その利点・欠点を議論する.18章は,本Partのまとめである.

Part Vは本論文の結論部である.19章では,本研究の成果をまとめ,今後の課題について述べる.

プログラムの実行時の振る舞いに関する性質を静的に調べるプログラム解析器は、コンパイラが生成する実行コードの性能を左右する主要な構成要素である。その不具合はコンパイラが生成する実行コードの不具合につながるため、その精度や効率とともに高い信頼性が求められている。信頼性の高いプログラム解析器を開発する有力な方法のひとつに対象言語の形式的意味定義に基づく方法が存在するが、C言語に対しては、このような開発は未だ行われるに至っていない。その最大の問題点は、プログラム解析器の開発の基盤となりうる適切な形式的意味定義が存在しない点にある。

本研究の主な貢献は、Cに対する形式的意味定義に基づくプログラム解析器の開発を実現したことである。そこでは、形式的意味定義に適した中間表現を提案し、それが実用的な Cプログラム解析器の開発に有用であることを示している。また、既存のコンパイラで用いる既存の中間表現の仕様記述法を提案し、コンパイラと整合性のある解析器の構成手法を与えている。

本論文は、 A Logic-Based Approach to Developing Analysers for C Programs (論理にもとづくCプログラム解析器の開発に関する研究) と題し、5部より構成され、主要部は第II部から第IV部である。第II部と第III部では、高い信頼性を持つCプログラム解析器の開発基盤となる中間表現 RML (Register Memory Language) を導入し、それに基づく信頼性の高いポインタ解析器の開発法を扱っている。第 IV部では、中間表現の仕様記述に適したデータモデルIIR (Identifier-based Intermediate Representation data model) を導入し、それを用いて既存のCコンパイラの中間表現の仕様を記述している。これら各部で中心的な役割を果たすRMLとIIRの関係は相補的であり、RMLがCプログラムの抽象的な論理式表現であるのに対して、 IIRはRMLの具体的表現を定義する際の仕様記述方法を与えるものであり、本論文ではその関連を明確に述べている。

第I部 Introductionは導入部である。

第1章 Introductionでは、本研究の対象、動機、目的、方法を明らかにし、関連する従来研究の問題点を指摘している。

第2章 Preliminariesでは、本論文で用いる基本的な用語、表記法を定義している。

第II部 Definition of RMLでは、中間表現RMLの定義を行っている。

第3章 The C Standardでは、Cの標準言語規格を分析し、形式的意味を定義する際に生じる問題点を明確にしている。

第4章 Overview of RML では、以下の章で扱うRMLの形式的意味定義の概要を示している。

第5章 Static Semantics および 第6章 Dynamic Semantics では、それぞれRMLの静的、および動的な形式的意味の定義を与えている。

第7章 Discussion and Related Work は第II部のまとめとして、関連研究との比較を行い、その利点・欠点を議論している。

第III部 Systematic Development of a Pointer Analyser では、第II部の成果を Cプログラムのポインタ解析器の開発に適用して得られた結果を示している。

第8章 Pointer Analysis Problem では、ポインタ解析の目的、関連研究、研究課題を述べている。また、第II部で与えた形式的意味記述を用いて、ポインタ解析問題を形式的に定義している。

第9章 Abstract Semantics では、第8章で与えた問題定義に基づき、形式的意味をその構造に沿って抽象化した抽象的意味を定義している。

第10章 Algorithmでは、第9章で得られた抽象的意味から解析アルゴリズムを導出する方法を示している。

第11章 Concluding Remarks では第III部をまとめて、ポインタ解析問題への本手法の適用の優位性を論じている。

第IV部Method for Specifying Static Semantics of IRでは、プログラムの中間表現(Intermediate Representation)の仕様記述を支援する手法を扱っている。

第12章 Introduction では、プログラムの中間表現に関する問題点、およびここで提案する手法の概要を示している。

第13章 IIR では中間表現データモデルIIRを定義している。

第14章 Case Study では、提案手法の適用事例として、製品Cコンパイラで用いている中間表現の仕様を記述した結果を示している。

第15章 Other Applications では、IIRのさらなる応用可能性を示し、プログラムを関係の集合としてモデル化するIIRの特徴が仕様記述以外にも、論理型言語を用いた宣言的なプログラム解析に有用であることを主張している。

第16章 Discussionと第17章 Related Work では、提案手法を関連研究と比較してその利点・欠点を議論している。

第18章は第IV部のまとめとして、IIRの有効性を述べている。

第V部 Conclusion は本論文の結論部である。

第19章 Conclusions and Future Works では、本研究の成果をまとめ、今後の課題について述べている。

本論文において提案したCの形式的意味定義に基づくプログラム解析器の開発例であるポインタ指示先解析器の設計とその正しさの証明は、型変換と共用体を扱いうる解析器に関する初めてのものである。また、既存のコンパイラで用いるプログラム解析器を開発する上で障害となっている中間表現の仕様記述方法を提案して、既存のCコンパイラの中間表現の仕様を形式的に記述できることを示した成果は、実用的なプログラム解析器の開発に有用な視点を与えるものである。

以上のように、本論文はこれまで十分ではなかったC言語に対する形式的意味記述に基づくプログラム解析器の開発手法を提案してその有効性を例示するとともに、既存のコンパイラで用いられている中間表現の仕様記述法を与えて実用的な解析器の構成法を実証的に明らかにしたものとして、この分野に少なくない貢献を果している。すなわち、本研究は情報理工学に関する研究的意義とともに、情報理工学における創造的実践に関し価値が認められる。よって本論文は博士(情報理工学)の学位請求論文として合格と認められる。