Rubyプログラムの制御フロー解析とその健全性の証明

IPSJ Web Site

Bibliographic Information

Other Title
  • Ruby プログラム ノ セイギョ フロー カイセキ ト ソノ ケンゼンセイ ノ ショウメイ
  • Control Flow Analysis of Ruby Programs and Its Soundness

Search this article

Abstract

Rubyプログラムの制御フロー解析を設計し，その健全性を操作的意味論に基づき証明する．Ruby などのスクリプト言語に関する静的プログラム解析は多く提案されているが，その健全性について言語の意味論に基づき証明がなされたものは少ない．本研究では，Ruby のコア言語について操作的意味論を定義し，その意味論に基づき制御フロー解析の健全性を証明する．Ruby のコア言語は，ruby 1.9 処理系の構文解析器によって得られる中間言語をモデルとし，メソッドの動的な定義・イテレータブロック・大域脱出などを含む．Ruby では，クラス・メソッドの定義は，宣言ではなく動的に評価される式であり，さらにメソッド定義の上書きが可能である．そのため，プログラムの実行時の制御フローによって，異なるクラス定義・メソッド定義が得られる可能性がある．本研究では，メソッド定義が評価されたかどうかについて，制御フローを区別する解析を行う．これにより，特に多く見られる，トップレベルでクラス・メソッドの定義を行うプログラムについては，メソッド呼び出しの正確な解析が可能となる．

We design a semi-flow-sensitive control flow analysis for Ruby, and prove its soundness. Static analysis of scripting languages including Ruby has been actively studied recently, but few of the analysis proved their correctness with respect to language semantics. We formalize an operational semantics of the core of Ruby. It is designed based on the intermediate language obtained by the parser of ruby-1.9, and supports dynamic method definition, iterator blocks, and non-local exits. Our analysis is semi-flow-sensitive in the sense that it is not sensitive on the values of a variable at each program point, but on which method definitions have been evaluated. This sensitivity makes it possible to precisely analyze typical Ruby programs where the definition of a class is split into several top-level class definitions.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

Report a problem

Back to top