テストスイートは通過した。型チェッカーも緑色だ。リリースする。2時間後、本番環境で誰もテストしようとしなかったエッジケースで IndexError が発生する。
テストはバグを見つける。型はいくつかを防ぐ。どちらもプログラムにランタイムエラーがないことを証明するわけではない。それを実現するには、もっと強力なものが必要だ：コードを実行せずに、すべての可能な実行を一度に推論する方法。
抽象解釈はそれを可能にする技術だ。Astrée、FacebookのInfer、Rustの借用チェッカーの健全性保証の根底にある静的解析を支えている。そして、「誤検出ゼロ」という静的解析のマーケティングの多くがなぜ嘘なのかも説明する。
ランタイムエラーは到達可能性の問題だ
ランタイムエラーとは、ただの悪い状態に到達してしまう操作のことだ。ゼロ除算、nullの逆参照、バッファオーバーフロー、配列の範囲外アクセス。すべて、実行が安全でないプログラムの箇所に到達したために起こる。
ランタイムエラーが存在しないことを証明するには、すべての可能な実行において、すべての安全でない操作が到達不可能であることを証明する必要がある。すべての入力。すべての分岐。すべてのループの繰り返し。
網羅的なテストは、おもちゃのプログラム以外では不可能だ。記号的実行はパス爆発で破綻するためスケールが悪い。抽象解釈は別の道を選ぶ：正確な値を知ることを諦め、代わりにすべての実際の実行を保証してカバーする近似の性質を追跡する。
抽象解釈が実際に行うこと
抽象解釈は、1976年にPatrick CousotとRadhia Cousotによって導入された。核心的なアイデアは美しくシンプルだ：プログラムを実行するが、実際の数値や文字列、ポインタを使って計算するのではなく、実際の値を過近似する抽象表現を使って計算する。
これを、関心のある性質を追跡する「影」の実行に置き換えると考えてほしい。x = 42 であることを知る代わりに、x > 0 であることを知るかもしれない。arr の長さが10であることを知る代わりに、arr が空でないことを知るかもしれない。
重要な制約は健全性だ。すべての具体的な状態は、何らかの抽象状態によって表現されなければならない。抽象実行がある操作が安全だと言えば、それが表現するすべての具体的な実行も安全である。代償は精度だ：抽象状態が曖昧すぎると、誤検出（安全な操作に対する虚偽の警告）が出る。
具体例：区間解析
ここに、ゼロ除算が不可能であることを証明する最小の抽象インタープリタを示す。これは各変数の可能な範囲を区間を使って追跡する。
# A tiny abstract interpreter for interval analysis
from dataclasses import dataclass
from typing import Dict
@dataclass(frozen=True)
class Interval:
lo: float
hi: float
def __contains__(self, val: float) -> bool:
return self.lo <= val <= self.hi
TOP = Interval(float("-inf"), float("inf"))
def eval_expr(env: Dict[str, Interval], expr) -> Interval:
if isinstance(expr, int):
return Interval(float(expr), float(expr))
if isinstance(expr, str):
return env.get(expr, TOP)
if expr[0] == "+":
l = eval_expr(env, expr[1])
r = eval_expr(env, expr[2])
return Interval(l.lo + r.lo, l.hi + r.hi)
if expr[0] == "-":
l = eval_expr(env, expr[1])
r = eval_expr(env, expr[2])
return Interval(l.lo - r.hi, l.hi - r.lo)
if expr[0] == "*":
l = eval_expr(env, expr[1])
r = eval_expr(env, expr[2])
products = [l.lo * r.lo, l.lo * r.hi, l.hi * r.lo, l.hi * r.hi]
return Interval(min(products), max(products))
if expr[0] == "/":
l = eval_expr(env, expr[1])
r = eval_expr(env, expr[2])
if r.lo <= 0 <= r.hi:
raise ValueError("Possible division by zero")
return TOP
raise ValueError(f"Unknown expr: {expr}")
def merge_envs(env1: Dict[str, Interval], env2: Dict[str, Interval]) -> Dict[str, Interval]:
keys = set(env1) | set(env2)
result = {}
for k in keys:
a = env1.get(k, TOP)
b = env2.get(k, TOP)
result[k] = Interval(min(a.lo, b.lo), max(a.hi, b.hi))
return result
def analyze(program, env: Dict[str, Interval]) -> Dict[str, Interval]:
env = dict(env)
for stmt in program:
if stmt[0] == "assign":
_, var, expr = stmt
env[var] = eval_expr(env, expr)
elif stmt[0] == "if":
_, cond, true_branch, false_branch = stmt
t_env = analyze(true_branch, dict(env))
f_env = analyze(false_branch, dict(env))
env = merge_envs(t_env, f_env)
elif stmt[0] == "while":
_, cond, body = stmt
old = dict(env)
for _ in range(10):
new = analyze(body, dict(old))
changed = False
for k in set(old) | set(new):
prev = old.get(k, TOP)
curr = new.get(k, TOP)
widened = Interval(min(prev.lo, curr.lo), max(prev.hi, curr.hi))
if widened.lo != prev.lo or widened.hi != prev.hi:
changed = True
old[k] = widened
if not changed:
break
env = old
return env
# Example program: y = 10 / (x + 1) where x >= 0
program = [
("assign", "t", ("+", "x", 1)),
("assign", "y", ("/", 10, "t")),
]
# This should pass: x >= 0 means t >= 1, so no division by zero
safe_env = analyze(program, {"x": Interval(0, 100)})
print("Safe env:", safe_env)
# This should fail: x could be -1
try:
bad_env = analyze(program, {"x": Interval(-5, 5)})
except ValueError as e:
print("Caught:", e)実行してみよう。最初のケースでは、t の区間が [1.0, 101.0] となりゼロを除外するため、安全性が証明される。2番目のケースでは、x が -1 のとき t がゼロになりうるため、正しくリスクを警告する。
if のハンドラは両方の分岐をマージする際に区間の和集合を取る。while のハンドラは区間が成長しなくなるまで反復する（不動点）。これが抽象解釈の核心だ：正確な値と引き換えに、保証された過近似を得る。そして、悪い状態が近似の外側にあることを示すことで安全性を証明する。
どこで破綻するのか：精度の壁
上記の例はおもちゃサイズだ。実際のプログラムにはエイリアシング、再帰、ヒープ割り当て、データ依存の境界を持つループがある。それぞれが予測可能な方法で精度を破壊する。
i を0から100まで増やすループを考えてみよう。単純な区間解析では、i を [0, +inf) に拡張してしまい、上限を回復できないかもしれない。i <= 100 を追跡するには、多面体や八角形のような関係ドメインが必要だ。これらのドメインは変数の数に対して3次または指数的である。1,000個の変数を持つプログラムで多面体解析を実行するのは現実的ではない。
これが、商用ツールが異なる選択をする理由だ。Astrée は、組み込みC用に慎重に選ばれた抽象ドメインの束を使う。Infer は分離論理と双アブダクションを使って数百万行のモバイルコードにスケールするが、一部の言語機能に対して健全性を諦めている。Rustの借用チェッカーは本質的に、所有権という1つの極めて精度の高いドメインを持つ抽象インタープリタだ。
避けられないトレードオフ
健全性、精度、スケーラビリティ。2つを選べ。
健全で精度の高い解析は、small modulesを超えてスケールしない。スケーラブルで健全な解析は、誤検出に溺れる。スケーラブルで精度の高い解析は、本当のバグを見逃す。
抽象ドメインの選択が調整ノブだ。区間は速く精度が低い。多面体は精度が高く遅い。述語抽象はその中間に位置し、ほとんどのソフトウェアモデル検査を支えている。
実際にどう使うか
おそらく、独自の抽象インタープリタを書くことはない。既存のものを使うことになるだろう。
Cや組み込みシステム向けには、Astrée と Frama-C が成熟した選択肢だ。Frama-C の EVA プラグインは、実世界のCコードに対して区間解析とメモリ解析を実行する。
Rust では、型システムが既に所有権の抽象ドメインをエンコードしている。Miri はインタープリタであり抽象インタープリタではないが、型システムが見逃す未定義動作を捕捉する。
汎用コード向けには、Meta の Infer が Java、C++、Objective-C に対するスケーラブルな抽象インタープリタに最も近い。本番codebasesで本当の null 逆参照やメモリリークのバグを見つける。
実験したい場合は、自分でパースする言語に対して、単純な符号解析や区間解析から始めるのがよい。ドラゴンブックではデータフロー解析が扱われている。Nielson と Nielson の Principles of Program Analysis は、抽象解釈そのものの標準的な参考文献だ。
否定的な証明
抽象解釈はコードをバグフリーにするわけではない。与えてくれるのは、特定のクラスのランタイムエラーが不可能であることを証明する数学的枠組みだ。その証明の信頼性は、抽象ドメイン、拡張戦略、そして誤検出を許容する覚悟に依存する。
ほとんどのチームにとって、優れたテストと健全な型システムの方が価値がある。しかし、ランタイムエラーが意味するのが人工衛星が空から落ちるようなコードを書いているとき、抽象解釈があってこそ夜も安く眠れる。