抽象実行 そのフレームワークと実例（その１）

抽象実行とは，プログラムの様々な性質を解析するために提案され た理論的なフレームワークである．これは，プログラムのデータ領域 や計算動作などの意味を抽象化した有限抽象領域を設計し，その上で プログラムを不動点計算と呼ばれる手法で「実行」することにより， プログラムの性質を求める．
そこで，本チュートリアルでは，プログラム解析のごく初歩的な知 識を持つ読者を対象にして，抽象実行の基本概念，分類，具体的設計 法、仕様記述への展望などを説明する． 対象言語としては，遅延評価型の関数型言語を取り上げる。ただし仕 様記述への展望は、手続き型言語における様相論理や時相論理による 仕様記述をベースに説明する。

抽象実行 そのフレームワークと実例（その２）

関数型言語の抽象実行のフレームワークとして， 領域抽象化による順方向実行と逆方向実行について ストリクトネス解析を例として説明する. さらにそれらを統一的に扱う４つのパラメータについて説明し 計算経路解析をそのパラメータ表現に基づきあらわす（１章）. 次に逆方向実行であるプロジェクション解析を説明し計算経路解析 と比較する（２章）. 最後に Per (Partial Equivalence Relation) による順方向実行の抽象実行 を説明し, プロジェクション解析や計算経路解析と比較する（３章）.

抽象実行 そのフレームワークと実例（その３）

前回までに抽象実行および広域解析のフレームワークを説明してきた. さて, では抽象実行や広域解析は本当に役に立つのだろうか？ また今後, 研究として興味が持たれるであろうか？ 最終回では, 筆者らの主観に基づく抽象実行の研究の今後の展望について説明する.
第１章では, いくつかの決定可能な様相論理の体系を紹介する. さらに, 応用として, 手続き型言語における二つの解析自動生成手法を紹介する. 一つは, 仕様記述として正規表現を用いたアクション履歴抽象化による 変則性解析の自動生成, もう一つは, 仕様記述として命題不動点論理を用いたアクション抽象化による 広域解析の自動生成を説明する.
第２章では, 命題不動点論理 $L_{\mu}$ と等価な表現力をもつ 単項二階論理 SnS について説明する. SnS は単項関数記号と単項述語記号のみを持つ二階述語論理である. さらに, 応用として, 関数型プログラムのストリクト性と類似した概念である 項書換え系の逐次性を紹介し, その決定可能性について説明する(Comon, LICS'95).
第３章では, 不動点計算に対する推論機構の部分的導入について説明する. ここでは無限領域上の不動点計算を, プログラム対応に lazy に抽象領域を生成する 手法に注目し, 再帰データ型上へのプロジェクション解析の自動拡張, および二項述語に対する自動検証法 (Le Metayer, ACM PEPM'95) を紹介する.
第４章は, $L_{\mu}$ や SnS に含まれない, 決定可能なその他の体系（集合制約, 非正規動的論理など）を簡単に紹介し, このチュートリアルを終る.

最小不動点計算に基づくプログラムの帰納的性質の導出

本論文では，時相論理式によって仕様が記述されたプログラム解析をモデル検査技術の 利用によって行うツールについて述べる．本ツールは，対象プログラム言語は Jimple， プログラム解析の仕様記述言語は時相論理 CTL-FV である．
Jimple は Java と相互変換可能な３番地コードからなる中間言語であり，Java に比べ プログラム解析や最適化が適用しやすい．また，CTL-FV は CTL（Computation Tree Logic）を拡張した時相論理であり，プログラム中の情報を述語に引用することを 許したところに大きな特徴がある．CTL-FV によって多くのプログラム解析が記述 できるため，本ツールを使用すると Jimple プログラムに対し様々な解析を自動的に おこなうことができるようになる．
今回，モデル検査を既存のモデル検査ツール SMV をそのまま利用することによって 実装が非常に簡単になり，Java 言語で約500行（コメント除く）のプログラムでこれ が実現できた．また，標準ライブラリのいくつかのクラスに対して無用命令の検出を 本ツールにより実行したところ，比較的大きなサイズのクラスに対しても数分で解析 することができた．ここでは，主に本ツールの設計と実装について説明する．

最小不動点計算に基づくプログラムの帰納的性質の導出

本論文では, 関数型プログラムの帰納的性質を最小不動点計算に基づき求める 手法について論じる. この手法は, 検証したい性質に対応して有限抽象領域を 定め, 自動生成系により広域解析プログラム(最小不動点計算系)を生成する. そして, 解析対象プログラムの抽象領域上の最小不動点を求め, 性質を検証する. 本手法は, 検証系の停止性が保証され全自動の機械的検証が可能なほか, 検証系 の自動生成が可能という特徴を持つ.

Transformation of strictness-related analyses based on abstract interpretation

This paper newly proposes HOMomorphic Transformer (HOMT) in order to formalize relations among strictness-related analyses (SRAs) on first-order functional programs. A HOMT is defined to be a composition of special instances of abstract interpretation, and has enough ability to treat known SRAs including head/tail/total strictness detection on nonflat domains. A set of HOMTs, furthermore, is an algebraic space such that some composition of HOMTs can be reduced to a simpler HOMT. This structure gives a transformational mechanism between various SRAs, and further clarifies the equivalence and the hierarchy among them.
First, we show a construction of a HOMT as a composition of Unit-HOMTs (U-HOMTs) which are specified by quadruplet representations. Second, algebraic relations among HOMTs are shown as reduction rules among specific pairs of quadruplet representations. Thus, hierarchy among HOMTs can be clarified by finding some adequate quadruplet representation which bridges a HOMT to the other. Third, various SRAs are formalized as HOMTs in either forward or backward manners. They are also shown to be safe under unified discussions. Finally, their equivalence and hierarchy are examined in terms of an algebraic structure of HOMTs.

広域データフロー解析に基づく関数型プログラムの変則性検出

一階の関数型言語を対象として、広域データフロー解析に基づく新たな変則性 検出アルゴリズムを提案する。変則性検出は、評価しても結果に影響を与える ことのない不要オブジェクト、および評価すると無限ループに陥り停止しない 発散オブジェクトの二点について行なう。この検出アルゴリズムは、計算結果 を与える計算経路を求める関数間広域解析技術に基づいている。このため、単 に構文的な定義・参照関係を追跡するクロスレファレンス型解析より高い検出 能力を持っている。本アルゴリズムを用いると、概念的には無限長リストとな るストリームを用いたプログラムにおいて生じやすい、計算が発散するバグの 自動検出に有効である。

Interprocedural Program Analysis for Java based on Weighted Pushdown Model Checking

Based on the observation that ``{\em program analysis is abstraction plus model checking}'', this paper investigates pushdown model checking based approach on interprocedural program analyses for mono-thread Java. The running example is an interprocedual dead code detection under PER (partial equivalence relation) based abstraction. The prototype implementation combines SOOT as preprocessing to convert Java to Jimple and the Weighted PDS (pushdown system) library as the back-end model checking engine. With these existing tools, we developed an interprocedural dead code analyzer for mono-thread Java with around 1500 lines of Java codes. This analysis framework enables us a rapid prototyping for an interprocedual analysis design.

Automatic verification based on abstract interpretation

This paper extends the automatic verification technique of Le M\'{e}tayer, Proving properties of programs defined over recursive data structures (ACM PEPM '95). Extensions of the range of both programming and specification languages are achieved by (1) the use of the input variable in function properties, (2) introducing new predicate constructors, and (3) the use of uninterpreted function/predicate symbols. The termination and soundness proofs are given by the formalization as a backward abstract interpretation.
To show the effectiveness, we demonstrate two examples of the declarative specifications of the sorting and formatting programs, which are directly and concisely expressed in our specification language.

Abstract interpretation over infinite abstract domains

Abstract interpretation is the technique to detect properties of programs by approximating their executions to those that over abstract domains, and is used to formalize various analyses and verifications. Two important requirements are soundness and termination. Roughly speaking, soundness means that the property detected by an abstract interpretation is always correct. This is usually guaranteed by continuity of the abstraction and concretization maps. Termination is needed for analyses/verification to be done in compile time. Termination is usually guaranteed by the finiteness of abstract domains. However, if one wants to extend the ability of analyses/verification, one always faces to this limitation. Some effort to this direction can be found in literatures, but the use of induction makes termination uncertain and/or requires strong limitation on a class to solve. Recently, the termination of symbolic model checking over infinite states have been discussed in terms of well-quasi-Order (WQO), and several new applications are obtained. We borrow this idea for termination of abstract interpretation. In this report, a sufficient condition for termination of a backward abstract interpretation over infinite abstract domains is presented in terms of better-quasi-order (BQO). The key observations are,
  1. classification of abstract interpretations by their direction (i.e., forward/backward) and their approximation (i.e., necessary/sufficient) decide their power domain constructions (in Section 2),
  2. extensions $\sqsubseteq_0$, $\sqsubseteq_1$ (over powersets) of a better-quasi-order are again better-quasi-orders (in Section 4).

and they lead the main statement that if a (possibly infinite) abstract domain is better-quasi-ordered then a backward abstract interpretation terminates.