5.4 정적 분석 — 실행하지 않고 프로그램을 추론하기

린터의 경고, 타입 체커의 오류, 컴파일러의 "이 변수는 초기화되지 않았을 수 있습니다"는 전부 같은 구조 위에 서 있다 — 프로그램을 실행하는 대신, 가능한 모든 실행을 근사하는 작은 세계를 만들어 그 위에서 결론을 낸다. 이 문서는 추상 상태·join·고정점이라는 그 근사의 공통 뼈대를 세우고, 도구의 경고를 건전성과 완전성의 교환 위에서 해석하는 — 어떤 침묵은 믿고 어떤 경고는 의심해야 하는지 판단하는 기준을 만든다.

학습 목표

• AST 수준의 구문 검사와 CFG 위의 데이터 흐름 분석이 각각 어떤 질문에 답할 수 있는지 구분한다.
• 추상 상태와 join의 정보 손실을 이해하고, worklist 알고리즘이 루프가 있는 CFG에서 고정점에 도달하는 과정을 추적한다.
• 대표 데이터 흐름 분석(도달 정의, 활성 변수, 상수 전파, definite assignment)을 방향·may/must의 프레임으로 비교한다.
• 건전성·완전성과 false positive·false negative의 관계를 설명하고, 도구별 경고 정책을 그 교환 위에서 해석한다.
• 분석이 조용한 것과 프로그램이 안전한 것을 구분하고, suppression의 비용을 판단한다.

배경: 왜 이것이 존재하는가

"이 코드는 초기화 안 된 변수를 읽는가?"에 정확히 답하는 일반적 방법은 존재하지 않는다 — 임의 프로그램의 임의 실행 경로에 대한 비자명한 질문은 결정 불가능하다는 것이 챕터 2(계산 이론)가 다루는 Rice의 정리의 귀결이다. 그런데 도구들은 매일 이 질문에 답하고 있다. 모순이 아니다 — 도구들은 다른 질문에 답한다: "내가 계산할 수 있는 근사 세계 안에서, 초기화 안 된 읽기가 가능해 보이는가?"

근사는 두 방향으로 틀릴 수 있다. 실제로는 안전한 코드를 위험하다고 하거나(false positive, 과잉 경고), 실제 결함을 놓치거나(false negative, 침묵). 결정 불가능성은 두 오류를 동시에 0으로 만들 수 없음을 보장한다. 따라서 모든 정적 분석 도구는 — 만든 사람이 의식했든 아니든 — 어느 쪽 오류를 얼마나 허용할지에 대한 정책을 갖는다. 이 문서의 목표는 그 정책을 읽는 눈이다. 도구가 "문제없음"이라 할 때 무엇을 보장하는 것이고, 경고할 때 얼마나 믿어야 하는가.

같은 뼈대가 도구 스펙트럼 전체에 깔려 있다. 컴파일러의 흐름 기반 경고, 린터, 타입 체커의 narrowing, 보안 취약점 스캐너까지 — 표면의 규칙은 달라도 "프로그램 상태의 근사를 제어 흐름을 따라 전파한다"는 기계는 같다. 그 기계는 5.2에서 세운 CFG 위에서 돈다 — 컴파일러 최적화의 분석과 도구의 분석은 같은 수학을 쓴다(사실 이 분야의 원전인 Kildall 1973은 최적화 논문이다).

핵심 개념

분석의 입력 — 구문 검사와 흐름 분석의 경계

AST만으로 답할 수 있는 질문이 있다: "== 대신 ===를 썼는가", "선언 안 된 이름을 참조하는가"(스코프 트리까지), "이 함수는 몇 줄인가". ESLint 규칙 대부분이 이 층이다 — AST 패턴 매칭과 스코프 분석으로 동작하고, 빠르고, 오진이 적다.

그러나 "이 변수는 읽히기 전에 모든 경로에서 대입되는가", "이 값은 이 지점에서 항상 상수인가"는 AST로 답할 수 없다. 실행 순서와 분기·합류·루프를 알아야 하므로 CFG가 필요하다. 이 층이 데이터 흐름 분석(data-flow analysis)이고, 이 문서의 중심이다.

추상 상태 — 관심 있는 것만 남긴다

실행 하나를 정확히 따라가는 것은 그냥 실행이다(그것이 테스트다). 분석은 모든 실행을 한꺼번에 다뤄야 하므로, 구체적 값 대신 관심 속성만 남긴 추상 상태를 쓴다. "초기화 분석"이라면 변수마다 {대입됨, 안 됨} 두 값이면 충분하고, "상수 전파"라면 {아직 모름(⊤), 상수 c, 상수 아님(⊥)}이면 충분하다. 42인지 43인지는 버린다 — 버리기 때문에 상태 공간이 유한해지고, 유한하기 때문에 계산이 끝난다.

분기가 합류하는 지점에서는 두 경로의 추상 상태를 join으로 합친다. 규칙은 "둘 다와 모순되지 않는, 가장 정보가 많은 상태로"다. 한 경로에서 x = 1, 다른 경로에서 x = 2였다면 합류 후 x는 "상수 아님(⊥)"이다 — 어느 쪽이 실행될지 모르므로 안전하려면 정보를 버려야 한다. 두 경로 모두 x = 2였다면 합류 후에도 x = 2다. 이 "정보 순서"가 있는 값 공간이 lattice이고, join은 그 위에서 항상 같거나 더 보수적인 쪽으로만 움직인다. 이 단조성이 뒤에서 종료를 보장한다.

루프와 고정점 — worklist 추적

루프가 있으면 "한 번 훑기"로는 안 된다 — 루프 몸통의 결과가 루프 입구로 되돌아오기 때문이다. 해법은 변화가 멈출 때까지 반복이다. 다음 의사 코드(분석 예제용 — Toy 언어에는 루프가 없다)의 상수 전파를 추적해 보자.

fn demo(n) {                        CFG:
  let limit = 10;                     b0: limit←10; sum←0; i←0
  let sum = 0;                        b1: if (i < limit) → b2, else → b3
  let i = 0;                          b2: sum←sum+i; i←i+1; → b1  (back edge)
  while (i < limit) {                 b3: return sum * limit
    sum = sum + i;
    i = i + 1;
  }
  return sum * limit;
}

worklist 알고리즘: 블록을 큐에 넣고, 꺼내서 입구 상태(선행 블록 출구들의 join)에 블록의 효과(전달 함수, transfer function)를 적용하고, 출구 상태가 바뀌었으면 후속 블록들을 다시 큐에 넣는다.

단계	처리	b1 입구의 상태 (limit, sum, i)
1	b0 처리	b0에서: (10, 0, 0)
2	b1, b2 처리	b2 출구는 (10, 0, 1) — back edge로 b1에 되돌아옴
3	b1 재처리: join[(10,0,0), (10,0,1)]	(10, 0, ⊥) — i의 상수성 소실
4	b2 재처리: sum ← 0+⊥	b2 출구 (10, ⊥, ⊥) → b1 다시 큐에
5	b1 재처리: join	(10, ⊥, ⊥)
6	b2 재처리	출구 불변 — 고정점, 종료

종료가 보장되는 이유: 각 변수의 상태는 ⊤ → 상수 → ⊥로 한 방향으로만 내려가고(전달 함수와 join이 단조), lattice의 높이가 유한하므로 변화는 유한 번만 가능하다. 결과 읽기: sum과 i는 상수성을 잃었지만 limit은 루프를 통과해도 10으로 살아남았다 — return sum * limit의 limit은 상수로 접을 수 있고, i < limit는 i < 10이 된다. 분석이 "루프가 몇 번 도는지"를 전혀 몰라도 이만큼은 증명할 수 있다는 것, 그리고 실행 없이 모든 반복 횟수에 대해 성립하는 결론이라는 것이 요점이다.

대표 분석들 — 같은 기계, 다른 질문

분석	질문	방향	may/must
도달 정의 (reaching definitions)	이 사용 지점에 어느 대입들이 도달할 수 있나	순방향	may (하나라도 가능하면 포함)
활성 변수 (live variables)	이 값은 이후에 읽힐 가능성이 있나	역방향	may
상수 전파	이 지점에서 값이 항상 그 상수인가	순방향	must (모든 경로에서 같아야)
definite assignment	읽기 전에 모든 경로에서 대입됐나	순방향	must

같은 worklist 기계에 질문(lattice와 전달 함수)만 갈아 끼운 것이다. may 분석은 "가능성 하나라도"를 모으므로 join이 합집합 쪽이고, must 분석은 "모든 경로에서"를 요구하므로 join이 교집합 쪽이다. 활성 변수처럼 "이후"를 묻는 질문은 흐름을 거슬러 역방향으로 전파한다 — 죽은 대입 제거(5.2의 DCE)가 이 분석의 소비자다.

민감도 — 정밀도의 가격표

분석이 무엇을 구분하는가에 따라 정밀도와 비용이 갈린다.

• flow-sensitive: 문장 순서를 구분한다. "대입 전"과 "대입 후"가 다른 상태다. 위의 데이터 흐름 분석은 모두 여기 속하고, TypeScript의 narrowing("이 if 안에서 v는 string")도 흐름 민감 분석이다.
• path-sensitive: 어떤 조건으로 여기 왔는지까지 구분한다. 경로 조건의 조합은 분기 수에 지수적으로 늘어나므로(경로 폭발) 전면 적용은 비싸고, 실전 도구는 제한된 형태만 쓴다.
• context-sensitive: 함수를 호출 지점별로 구분해 분석한다. "f(1)의 반환"과 "f(2)의 반환"을 섞지 않는 대신, 호출 그래프 크기만큼 비용이 는다.

join에서 정밀도가 사라지는 지점을 실제 도구로 확인해 보자(TypeScript 5.9, --strict 기준으로 아래 오류 발생을 확인했다).

function correlated(cond: boolean) {
  let x: number | undefined;
  if (cond) x = 1;
  if (cond) return x.toFixed(); // error TS18048: 'x' is possibly 'undefined'.
  return 'none';
}

실행 관점에서 x.toFixed()에 도달하는 경로는 반드시 첫 if도 통과했으므로 x는 항상 1이다. 그러나 흐름 민감·경로 비민감 분석은 첫 if 뒤의 합류에서 x: number | undefined로 join하고, 두 cond 검사가 상관되어 있다는 사실을 추적하지 않는다. 경고는 분석기의 버그가 아니라 근사의 정직한 출력이다 — 그리고 이 근사를 아는 개발자는 코드를 분석기가 증명할 수 있는 형태(한 if로 합치기)로 바꾸는 것이 우회임을 안다.

건전성과 완전성 — 도구의 정책을 읽는다

분석이 "위험 없음"이라 말할 때 실제로 위험이 없다면 그 분석은 건전(sound)하다 — 놓침(false negative)이 없다. 분석이 "위험"이라 말할 때 실제로 항상 위험하다면 완전(complete)하다 — 오진(false positive)이 없다. 결정 불가능성 때문에 비자명한 속성에 대해 둘 다는 불가능하므로, 도구는 선택한다.

• 건전성을 지향하는 도구는 확신할 수 없으면 경고한다. 정보 부족이 위험으로 근사된다 — 위의 TS18048이 정확히 그것이다. "false positive는 분석기의 버그"라는 통념이 틀리는 지점이다: 높은 건전성을 산 대가로 지불한 의도된 비용일 수 있다.
• 소음 억제를 지향하는 도구(대부분의 린터, 많은 보안 스캐너)는 확신 있는 패턴만 보고한다. 조용하다고 안전한 것이 아니다 — 침묵은 "내가 아는 패턴은 없었다"까지만 의미한다.
• 실전 도구는 순수하게 어느 한쪽이 아니다. TypeScript는 공식적으로 건전성을 절대 목표로 삼지 않는다고 명시한다 — 실용성을 위해 알려진 unsound 지점(예: 배열 인덱스 접근의 기본 타입)을 남겨 둔 설계다. 도구의 보장을 과대평가하지 않으려면 이 정책 문서를 읽어야 한다.

진단 정책 — 분석과 제품 사이의 계층

같은 분석 결과라도 도구는 severity(error/warning/info), confidence(확실/추정), suppression(억제 주석, baseline)이라는 정책 계층을 거쳐 사용자에게 낸다. 이 분리를 알면 두 가지가 명확해진다. 첫째, "warning을 error로 올리기"는 분석을 바꾸는 게 아니라 정책을 바꾸는 것이다 — 오진율은 그대로인데 차단력만 올라가므로, 오진 처리 비용(suppression 절차)을 함께 설계해야 한다. 둘째, suppression은 분석의 눈을 가리는 것이므로 그 자체가 관리 대상이다 — 사유 없는 일괄 억제가 쌓이면 도구의 실효 건전성이 조용히 무너진다.

실무 관점

도구 세 개를 같은 프레임으로 읽기

• ESLint는 파일 단위 AST + 스코프 분석 위의 규칙 엔진이다. 타입 정보가 없으므로 "이 메서드는 이 타입에 없다" 같은 질문은 원리적으로 밖이고(typescript-eslint가 타입 체커를 결합해야 가능해진다), 강점은 싸고 오진 적은 구문·스코프 규칙이다. 규칙별 문서가 "왜 이 패턴이 문제인가"를 설명하는 것도 이 층의 특성이다 — 패턴 자체가 결론이기 때문이다.
• TypeScript의 흐름 기반 narrowing은 이 문서의 데이터 흐름 분석이 제품화된 것이다. typeof v === 'string' 분기 안에서 v: string이 되는 것(흐름 민감), 위의 TS18048(경로 비민감), let label: string이 일부 경로에서만 대입되면 error TS2454: Variable 'label' is used before being assigned(definite assignment — must 분석)까지, 이 문서의 어휘로 전부 위치가 찍힌다.
• 컴파일러 경고(미초기화 변수, 도달 불가능 코드)는 같은 분석의 컴파일러 내장판이고, 대개 "확신 있는 것만 기본 경고, 나머지는 옵션 플래그"라는 정책을 갖는다.

경고를 받았을 때의 판단 절차

경고 앞에서 물을 것은 "코드가 틀렸나"가 아니라 순서대로: (1) 분석기가 본 것이 무엇인가 — 어느 경로·어느 join에서 이 결론이 나왔나. (2) 그 경로가 실제로 가능한가 — 가능하면 진짜 결함이다. (3) 불가능하다면 왜 분석기는 배제하지 못했나 — 대개 경로 상관관계, 함수 경계 밖의 불변식, 동적 값처럼 분석의 민감도 밖에 있는 사실이다. 이때 선택지는 suppression이 아니라 증명 가능한 형태로의 리팩터링이 먼저다 — 분석기가 증명할 수 있는 코드는 대체로 사람에게도 추론하기 쉬운 코드이기 때문이다.

통념: "린터와 타입 체커가 조용하면 프로그램은 안전하다"

침묵의 보장 범위는 도구가 선택한 추상화와 민감도 안이다. 구체적으로 침묵이 보장하지 않는 것들: 값의 범위가 만드는 오류(0으로 나누기, 배열 경계 — 타입은 number로 동일하다), 동시성·시간 순서, 비즈니스 로직의 정합성, 그리고 도구가 unsound하기로 선택한 지점들. 정적 분석은 테스트를 대체하는 것이 아니라 다른 축을 검사한다 — 분석은 모든 경로에 대한 얕은 속성을, 테스트는 소수 경로에 대한 깊은 속성을 본다. 두 축이 직교하므로 함께 쓰는 것이다.

더 깊이

분석을 무력화하는 언어 기능

worklist가 도는 CFG와 호출 그래프는 코드가 정적으로 읽힐 수 있다는 전제 위에 있다. reflection, 동적 속성 접근(obj[key]), eval, 런타임 코드 로딩, 외부 I/O로 들어오는 값은 그 전제를 깬다 — 분석기는 모르는 것을 ⊥(무엇이든 가능)로 근사하고, ⊥는 닿는 모든 것을 ⊥로 만든다. 5.3에서 같은 기능들이 JIT의 추측을 무력화했던 것과 정확히 같은 구조다 — 실행 전 추론과 실행 중 추측 모두 "코드가 정적으로 예측 가능하다"는 같은 자원을 소비한다. 동적 기능의 비용을 계산할 때 성능과 분석 가능성을 함께 계상해야 하는 이유다.

추상 해석 — 이 문서의 일반 이론

이 문서의 lattice·전달 함수·고정점은 추상 해석(abstract interpretation, Cousot & Cousot 1977)이라는 일반 이론의 사례다. 이론의 핵심 주장은 "구체 의미론과 추상 의미론을 잇는 사상이 특정 조건을 만족하면, 추상 세계의 고정점이 구체 세계의 모든 실행을 안전하게 덮는다"는 건전성 정리다. 수학적 전개는 이 챕터의 범위 밖이지만, 존재를 알아 둘 가치가 있다 — 산업용 정적 분석기(Astrée, Infer 등)의 보장이 "휴리스틱이 아니라 정리 위에 서 있다"는 말의 의미가 이것이다.

타입 체커는 어디까지 같은 기계인가

타입 검사의 본체(선언·추론된 타입과 사용의 정합성)는 챕터 4(타입 시스템)의 주제이고, 이 문서와의 접점은 흐름 기반 narrowing이다 — 선언된 타입 집합을 lattice로, 가드를 전달 함수로 쓰는 데이터 흐름 분석. TypeScript가 union 타입 위에서 narrowing을 하는 구조와, 그 건전성의 한계(공식 설계 목표 문서가 명시하는 unsound 지점들)를 이 문서의 프레임으로 읽으면, "타입이 통과했는데 런타임 오류"의 상당수가 분류 가능해진다 — 분석 밖의 값(외부 입력의 as 단언), unsound 지점, 또는 narrowing이 추적 못 하는 상관관계다.

정리

• 정적 분석은 결정 불가능한 질문을 "계산 가능한 근사 세계 안의 질문"으로 바꾼다. 근사인 이상 오진과 놓침의 교환은 피할 수 없고, 그 배분이 도구의 정책이다.
• 기계의 뼈대는 추상 상태(관심 속성만), join(합류에서 보수적으로 합침), 전달 함수, 그리고 worklist로 도달하는 고정점이다. 유한 높이 lattice와 단조성이 종료를 보장한다.
• 대표 분석들은 같은 기계에 방향(순/역)과 may/must만 갈아 끼운 것이고, 컴파일러 최적화와 도구 경고가 이 기계를 공유한다.
• 정밀도는 민감도(flow/path/context)로 사고, 비용은 지수적으로 는다. join에서 사라진 경로 상관관계가 흔한 false positive의 출처다.
• 건전한 도구의 경고는 "증명 실패"를 포함하고, 소음을 억제한 도구의 침묵은 "아는 패턴 없음"까지만 의미한다. 침묵을 안전으로 읽지 않는 것이 분석 도구 사용의 제1 규율이다.

확인 문제

1. 다음 코드에 TypeScript(strict)는 error TS2454: Variable 'label' is used before being assigned를 낸다. 이 경고를 만든 분석을 이 문서의 어휘(방향, may/must, join)로 설명하고, kind가 실제로는 항상 0 이상이라는 사실을 팀이 알고 있을 때의 올바른 대응을 논하라.

function pickLabel(kind: number) {
  let label: string;
  if (kind === 0) label = 'zero';
  else if (kind > 0) label = 'positive';
  return label;
}

정답과 해설

definite assignment는 순방향 must 분석이다 — "모든 유입 경로에서 대입됨"이어야 '대입됨'으로 판정하므로, join은 교집합 쪽으로 동작한다. if/else if는 어느 조건도 참이 아닌 제3의 경로(둘 다 거짓)를 남기고, 그 경로에서 label은 미대입이므로 합류 지점의 상태는 "미대입 가능"이 된다. kind >= 0이라는 도메인 불변식은 타입에 표현되지 않았으므로 분석은 쓸 수 없다. 대응: (1) 불변식을 코드로 증명 가능하게 만든다 — 마지막 가지를 else로 바꿔 모든 경로에서 대입하거나, 남는 경로에서 명시적으로 throw한다(도달하면 불변식 위반이므로 오히려 올바른 방어다). (2) 단순 suppression(! 단언)은 불변식이 깨졌을 때 오류를 조용한 오동작으로 바꾸므로 열등하다. 분석기의 오진처럼 보이는 것이 사실 "불변식이 코드에 없다"는 신호인 사례다.

2. 보안 스캐너 A는 "확실한 취약점만 보고합니다(오진 거의 없음)"를, 스캐너 B는 "의심스러운 것은 모두 보고합니다"를 표방한다. 두 도구가 모두 조용할 때 각각의 침묵이 의미하는 바를 건전성·완전성으로 구분하고, "A만 통과하면 배포"라는 정책의 위험과 "B의 경고 전부 수정"이라는 정책의 위험을 각각 설명하라.

정답과 해설

A는 완전성(경고하면 진짜) 지향이므로 건전성을 포기했다 — A의 침묵은 "확실한 패턴은 없었다"일 뿐 false negative가 구조적으로 존재한다. B는 건전성 지향이므로 침묵의 보장은 더 강하지만(그 분석 범위 안에서), 대신 오진이 많다. "A만 통과하면 배포"의 위험: A가 놓치도록 설계된 회색 지대(정보 부족으로 확신 못 하는 취약점)가 검사 없이 통과한다 — 놓침이 도구의 정책이었음을 잊은 것이다. "B 경고 전부 수정"의 위험: 오진 수정에 자원이 소모되고, 개발자들이 경고를 소음으로 학습해 일괄 suppression이 쌓이면 B의 건전성이 실질적으로 무너진다 — 정책 계층(우선순위, 확신도 필터, suppression 사유 관리) 없이 분석 결과를 제품 게이트로 직결한 것이 원인이다.

3. 위 worklist 예제에서 while (i < limit)의 limit이 루프 안에서 limit = limit - 1로 갱신된다고 하자. 고정점에 도달했을 때 limit의 추상 상태가 어떻게 달라지는지 추적하고, 그 결과가 return sum * limit의 상수 접기에 미치는 영향과 "분석은 루프 횟수를 모른다"는 사실이 이 결론의 정확성에 왜 문제가 되지 않는지 설명하라.

정답과 해설

첫 반복에서 b2가 limit ← 10 - 1 = 9를 만들고, back edge로 b1에 돌아온 상태 (…, limit=9)가 b0의 (…, limit=10)과 join되면서 limit은 ⊥(상수 아님)로 내려간다. 이후 전달 함수는 ⊥ - 1 = ⊥이므로 고정점에서 limit = ⊥다. 따라서 sum * limit도 i < limit도 접을 수 없다. 정확성에 문제가 없는 이유: 상수 전파의 결론은 "모든 실행에서 이 값은 이 상수"라는 must 주장인데, limit은 반복 횟수에 따라 10, 9, 8…로 실제로 달라지므로 "상수 아님"이 참이다. 분석은 루프가 몇 번 도는지 몰라도 되도록 설계됐다 — 고정점은 "몇 번을 돌든 성립하는" 상태이고, 그 대가로 특정 실행에서의 구체적 값(첫 반복에서는 10이다 같은 사실)을 표현하지 못할 뿐이다. 근사의 방향이 안전 쪽(정보 포기)으로만 무너지는 것을 확인하는 문제다.

참고 자료

• Gary A. Kildall, A Unified Approach to Global Program Optimization (POPL 1973) — lattice·전달 함수·고정점으로 데이터 흐름 분석을 통일한 원전. 이 문서의 worklist 기계가 여기서 나왔다.
• Flemming Nielson, Hanne Riis Nielson, Chris Hankin, Principles of Program Analysis (1999) — 데이터 흐름 분석과 추상 해석의 표준 교과서. may/must, 민감도의 형식적 정의를 확인한다.
• TypeScript Handbook, Narrowing — 흐름 기반 좁히기의 공식 서술. 이 문서의 TS 예제(5.9 기준)가 어떤 가드를 인식하는지의 기준 문서다.
• Microsoft, TypeScript Design Goals — "건전성을 목표로 하지 않는다"를 명시한 공식 문서. 도구의 보장 범위를 정책 문서로 확인하는 습관의 예다.
• ESLint, Architecture — AST(ESTree) 기반 규칙 엔진과 스코프 분석의 구조. 린터가 어느 층에서 동작하는지 공식 문서로 확인한다.