테스트 스위트는 통과했다. 타입 체커는 초록불이다. 배포했다. 두 시간 후, 프로덕션에서 아묏도 테스트하지 않은 엣지 케이스에서 IndexError가 발생했다.
테스트는 버그를 찾는다. 타입은 일부를 방지한다. 둘 다 프로그램이 런타임 에러로부터 자유롭다는 것을 증명하지는 못한다. 그것을 위해서는 더 강력한 무언가가 필요하다: 코드를 실행하지 않고, 모든 가능한 실행을 한 번에 추론할 수 있는 방법.
추상 해석이 바로 이것을 가능하게 하는 기법이다. Astrée, Facebook의 Infer, 그리고 Rust의 대여 체커 내부의 건전성 보장에 쓰이는 정적 분석기의 핵심이다. 또한 대부분의 “오탐 없음”이라는 정적 분석 마케팅이 거짓말인 이유도 설명해 준다.
런타임 에러는 도달 가능성 문제다
런타임 에러는 그저 잘못된 상태에 도달하는 연산이다. 0으로 나누기, 널 참조, 버퍼 오버플로우, 인덱스 범위 초과. 각각은 실행이 해당 연산이 안전하지 않은 프로그램 지점에 도달했기 때문에 발생한다.
런타임 에러가 존재하지 않음을 증명하려면, 모든 가능한 실행에서 모든 안전하지 않은 연산이 도달 불가능함을 증명해야 한다. 모든 입력. 모든 분기. 모든 루프 반복.
완전한 테스트는 장난감 프로그램이 아니면 불가능하다. 기호 실행은 경로 폭발 때문에 확장성이 떨어진다. 추상 해석은 다른 길을 택한다: 정확한 값을 아는 것을 포기하고, 대신 모든 실제 실행을 보장하는 방식으로 근사 속성을 추적한다.
추상 해석이 실제로 하는 일
추상 해석은 Patrick과 Radhia Cousot이 1976년에 도입했다. 핵심 아이디어는 아름답게도 단순하다: 프로그램을 실행하되, 실제 숫자, 문자열, 포인터로 계산하는 대신 실제 값을 과대 근사하는 추상 표현으로 계산한다.
이를 구체적 실행을 관심 있는 속성을 추적하는 “그림자” 실행으로 대체한다고 생각하면 된다. x = 42를 아는 대신, x > 0을 알 수 있다. arr의 길이가 10이라는 것을 아는 대신, arr이 비어 있지 않다는 것을 알 수 있다.
핵심 제약은 건전성이다. 모든 구체적 상태는 어떤 추상 상태로 표현되어야 한다. 추상 실행이 어떤 연산이 안전하다고 말하면, 그것이 표현하는 모든 구체적 실행은 안전하다. 대가는 정확도다: 추상 상태가 너무 모호하면 거짓 긍정(안전한 연산에 대한 허위 경고)이 발생한다.
구체적 예시: 구간 분석
다음은 0으로 나누기가 불가능함을 증명하는 최소한의 추상 해석기다. 각 변수의 가능한 범위를 구간으로 추적한다.
# 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]이므로 0을 제외하여 안전함을 증명한다. 두 번째 경우는 x가 -1일 때 t가 0이 될 수 있으므로 위험을 정확히 표시한다.
if 처리기는 두 분기를 구간의 합집합을 취해 병합한다. while 처리기는 구간이 더 이상 커지지 않을 때까지 반복한다(고정점). 이것이 추상 해석의 핵심이다: 정확한 값을 보장된 과대 근사와 교환하고, 잘못된 상태가 근사 밖에 있음을 보여 안전함을 증명한다.
어디서 무너지는가: 정확도의 벽
위 예시는 장난감 수준이다. 실제 프로그램에는 별칭 지정, 재귀, 힙 할당, 데이터 의존적 범위를 가진 루프가 있다. 각각은 예측 가능한 방식으로 정확도를 파괴한다.
i를 0부터 100까지 증가시키는 루프를 생각해 보자. 단순한 구간 분석은 i를 [0, +inf)로 확장하고 상한을 절대 회복하지 못할 수 있다. i <= 100을 추적하려면 관계형 도메인(다면체나 팔각형 같은)이 필요하다. 이러한 도메인은 변수 개수에 대해 3차 또는 지수적이다. 변수가 1,000개인 프로그램에서 다면체 분석은 실행할 수 없다.
이것이 상용 도구가 다른 선택을 하는 이유다. Astrée는 임베디드 C에 맞게 세심하게 조정된 추상 도메인의 격자를 사용한다. Infer는 분리 논리와 쌍방향 추론을 사용해 수백만 줄의 모바일 코드까지 확장하지만, 일부 언어 기능에 대해선 건전성을 포기한다. Rust의 대여 체커는 본질적으로 소유권이라는 단 하나의 극도로 정확한 도메인을 가진 추상 해석기다.
피할 수 없는 트레이드오프
건전성, 정확도, 확장성. 둘만 고를 수 있다.
건전하고 정확도 높은 분석기는 small modules을 넘어 확장되지 않는다. 확장 가능하고 건전한 분석기는 거짓 긍정에 당신을 끝없이 고통스럽게 할 것이다. 확장 가능하고 정확도 높은 분석기는 실제 버그를 놓칠 것이다.
추상 도메인의 선택이 조절 손잡이다. 구간은 빠르지만 정확도가 떨어진다. 다면체는 정확하지만 느리다. 술어 추상화는 중간에 위치하며 대부분의 소프트웨어 모델 검증기를 구동한다.
실제로 이것을 어떻게 사용하는가
아마도 당신은 직접 추상 해석기를 작성하지 않을 것이다. 이미 존재하는 것을 사용할 것이다.
C와 임베디드 시스템의 경우, Astrée와 Frama-C가 성숙한 옵션이다. Frama-C의 EVA 플러그인은 실제 C 코드에 대해 구간 및 메모리 분석을 수행한다.
Rust의 경우, 타입 시스템이 이미 소유권 추상 도메인을 인코딩하고 있다. Miri는 해석기이지 추상 해석기는 아니지만, 타입 시스템이 놓치는 정의되지 않은 동작을 잡아낸다.
범용 코드의 경우, Meta의 Infer가 Java, C++, Objective-C에 가장 확장 가능한 추상 해석기에 가깝다. 프로덕션 codebases에서 실제 널 참조와 메모리 누수 버그를 찾아낸다.
실험해 보고 싶다면, 직접 파싱하는 언어에서 간단한 부호 분석이나 구간 분석부터 시작하라. Dragon Book은 데이터 흐름 분석을 다룬다. Nielson과 Nielson의 Principles of Program Analysis는 추상 해석 자체에 대한 표준 참고서다.
부정을 증명하기
추상 해석이 당신의 코드를 버그 없게 만들지는 않는다. 그것이 주는 것은 특정 클래스의 런타임 에러가 불가능함을 증명하는 수학적 프레임워크다. 그 증명은 추상 도메인, 확장 전략, 그리고 거짓 긍정을 감수할 의지만큼만 좋다.
대부분의 팀은 좋은 테스트와 건전한 타입 시스템에서 더 많은 가치를 얻는다. 하지만 런타임 에러가 곧 위성이 하늘에서 떨어지는 코드를 작성할 때, 추상 해석이 밤에 잠들게 해 주는 방법이다.