abstract interpretation은 엔지니어가 탭을 닫게 만드는 유형의 용어다. 이해하려면 격자 이론을 한 학기 배워야 할 것처럼 들린다. 대부분의 개발자는 이것이 연구 논문에나 나오는 것이지 풀 리퀘스트에는 관련 없는 것으로 생각한다.

그 가정은 비싼 대가를 치른다. abstract interpretation은 코드를 실행하지 않고 코드에 대해 무언가를 증명하는 방법일 뿐이다. 이를 기반으로 구축된 도구는 타입 검사기와 린터가 놓치는 null reference, memory leak, race condition을 잡아낼 수 있다. 좋은 소식은: 이를 사용하기 위해 갈루아 연결을 이해할 필요가 없다는 것이다. 작동하는 CI 설정과 약 20분이면 충분하다.

abstract interpretation이 실제로 하는 일

핵심적으로 abstract interpretation은 자동화된 증명 기법이다. 프로그램을 실행하지만 실제 값 대신 근사치를 사용한다.

변수 x를 생각해 보자. 일반적인 실행에서 x는 42를 가질 수 있다. abstract interpretation에서 x는 “양의 정수”를 가질 수 있다. 분석은 이러한 추상 값을 모든 가능한 코드 경로를 통해 추적한다. 어떤 경로도 null reference으로 이어지지 않음을 증명할 수 있다면 안전하다. 반대로, x가 참조 지점에서 널이 될 수 있는 경로를 발견하면 잠재적 버그를 보고한다.

마법은 이것이 루프와 조건문에서도 작동한다는 것이다. 분석기는 추상 상태에 대한 고정점을 계산하여 실제로 영원히 반복하지 않고도 무한 반복에 대해 추론할 수 있다. 이것이 루프에 어려움을 겪는 더 단순한 기호 실행 도구와 abstract interpretation을 구분하는 것이다.

Facebook의 Infer는 이 기술을 사용하는 가장 접근하기 쉬운 프로덕션 도구다. Java, C, C++, Objective-C를 분석하기 위해 코드를 중간 표현으로 컴파일하고 각 함수에 대해 구성적 abstract interpretation을 실행한다. Infer는 함수별로 결과를 캐시하므로 증분 빌드가 빠르다. 이것이 CI에서 실행 가능하게 하는 비결이다.

왜 린터만으로는 부족한가

린터는 구문을 본다. 타입 검사기는 타입을 본다. abstract interpretation은 경로를 가로지르는 동작을 본다.

린터는 널 체크를 잊었다고 지적할 수 있다. 타입 검사기는 함수가 Optional<T>를 반환하도록 강제할 수 있다. 하지만 둘 다 복잡한 분기 후에 한 경로에서 초기화되지 않은 채로 남은 포인터를 47번째 줄에서 참조하는 것을 확실히 잡아낼 수는 없다. abstract interpretation은 해당 포인터의 가능한 상태를 모든 분기점과 병합점을 통해 추적한다.

트레이드오프는 노이즈다. abstract interpretation은 false positive을 생성한다. 비즈니스 로직이 절대 일어나지 않는다고 보장하는 null reference을 보고할 수 있다. 분석기는 불변 조건을 모른다. 코드가 문자 그대로 허용하는 것만 안다.

Infer의 기본 체커는 대부분의 코드베이스에서 false positive률을 10~15% 정도로 낮게 유지하도록 조정되어 있다. 타입 검사기보다 높지만, 찾는 버그는 종종 코드 리뷰와 테스트를 빠져나가는 것들이다.

CI 파이프라인에 Infer 추가하기

Infer를 소스에서 빌드할 필요는 없다. Facebook은 Docker 이미지를 공개한다. 다음은 Java 프로젝트를 분석하는 작동하는 GitHub Actions 워크플로우다:

# .github/workflows/infer.yml
name: Abstract Interpretation

on: [pull_request]

jobs:
  infer:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Run Infer
        uses: docker://ghcr.io/facebook/infer:main
        with:
          args: >
            infer run
            --make-command "mvn compile"
            --
            mvn compile

      - name: Upload report
        uses: actions/upload-artifact@v4
        with:
          name: infer-report
          path: infer-out/report.json

Node.js나 Python 프로젝트의 경우 빌드 명령을 교체하라. Infer는 네이티브로 JavaScript나 Python을 분석하지 않지만, 이러한 프로젝트가 종종 의존하는 C/C++ 확장에 대해 실행할 수 있다. 순수한 관리 언어 환경에 있는 경우에도 CodeQL이나 SonarQube와 같은 도구에서 유사한 경로에 민감한 분석을 얻을 수 있지만, 기반 엔진은 다르다.

C나 C++ 프로젝트의 경우 설정은 더 간단하다:

# .github/workflows/infer-cpp.yml
name: Infer C++ Analysis

on: [pull_request]

jobs:
  infer:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Build with Infer
        uses: docker://ghcr.io/facebook/infer:main
        with:
          args: >
            infer run
            --make-command "make"
            --
            make

infer run --make-command 패턴은 일반적인 빌드 프로세스 중에 컴파일러 호출을 가로챈다. Infer는 중간 표현을 추출하고, 분석하고, 결과를 infer-out/에 기록한다. 실제 빌드 산출물은 영향을 받지 않는다.

출력 읽기와 false positive 조정

Infer는 결과를 infer-out/report.json과 사람이 읽을 수 있는 infer-out/report.txt에 출력한다. 전형적인 발견은 다음과 같다:

src/parser.c:142: error: NULL_DEREFERENCE
  pointer `node` last assigned on line 138 could be null and is dereferenced at line 142, column 5

메시지는 변수, 할당된 위치, 참조가 발생한 위치를 알려준다. 에디터에서 경로를 추적할 수 있다.

Infer가 너무 시끄러우면 특정 체커를 억제하거나 분석을 건너뛰도록 코드에 주석을 달 수 있다:

// src/parser.c
// infer-ignore: the parent check guarantees node is non-null here
node->value = parsed;

또는 특정 체커를 전역적으로 비활성화할 수 있다:

infer run --make-command "make" --no-bufferoverrun --

buffer overrun 체커는 복잡한 포인터 산술이 있는 코드에서 특히 false positive을 일으키기 쉽다. 나는 보통 레거시 C 코드베이스에서는 이를 비활성화하고 null reference 및 memory leak 체커를 활성 상태로 둔다. 이 두 가지는 검토 시간을 정당화할 비율로 실제 버그를 발견한다.

빌드 시간 트레이드오프

abstract interpretation은 공짜가 아니다. 중형 C++ 프로젝트에서 Infer 전체 실행은 일반 빌드보다 24배 더 오래 걸릴 수 있다. 증분 분석이 도움이 된다: 후속 실행에서는 Infer가 변경된 함수와 그 의존성만 재분석한다. 실제로 이는 10분 빌드가 깨끗한 CI 실행에서는 1520분이 될 수 있지만, 증분 실행에서는 3~5분이 된다는 것을 의미한다.

CI 예산이 빠듯하다면 풀 리퀘스트에서는 Infer를 실행하지만 main에 대한 모든 푸시에서는 실행하지 마라. 또는 매일 밤 실행하라. 발견하는 버그는 보통 지연 시간만한 가치가 있지만, 적절한 빈도는 팀의 CI 시간에 대한 허용도에 달려 있다.

또 다른 선택은 푸시하기 전에 로컬에서 Infer를 실행하는 것이다. 동일한 Docker 이미지는 Docker가 설치된 모든 머신에서 작동한다:

docker run --rm -v $(pwd):/workspace -w /workspace \
  ghcr.io/facebook/infer:main \
  infer run --make-command "make" --

Infer가 잡아내지 못하는 것

Infer는 구성적이다. 함수를 분리하여 분석하고 요약을 사용하여 호출자와 피호출자를 모델링한다. 이것이 확장성을 제공하지만, 전체 호출 그래프 분석을 필요로 하는 교차 함수, 경로에 민감한 버그가 빠져나갈 수 있음을 의미한다.

또한 논리 버그도 찾지 못한다. 코드가 포인터를 안전하게 참조하지만 잘못된 값을 사용하는 경우 Infer는 조용하다. 이는 안전성 검사기이지, 정확성의 오라클은 아니다.

동시성 버그는 제한적이다. Infer에는 race condition 검사기가 있지만 이는 실험적이며 대부분의 팀이 끄는 만큼의 false positive을 생성한다.

다음에 할 일

작게 시작하라. 컴파일 언어로 된 프로젝트 하나를 선택하고 위의 GitHub Actions 워크플로우를 추가하라. 다음 몇 번의 풀 리퀘스트에서 실행하게 하라. 팀과 함께 발견 사항을 검토하고 노이즈에 대한 억제 목록을 구축하라.

1주일 후에는 신호가 CI 시간을 감당할 가치가 있는지 감이 잡힐 것이다. 내 경험으로는 기존 C나 Java 코드베이스의 첫 실행은 항상 코드 리뷰가 놓친 적어도 하나의 null reference을 발견한다. 보통 이것만으로도 유지할 가치가 충분하다.

더 깊이 들어가고 싶다면 Infer 문서에는 OCaml로 사용자 정의 체커를 작성하는 내용이 담겨 있다. 거기서 박사 학위가 유용하다. 그 외의 모든 것에는 기본 체커와 Docker 이미지로 충분하다.

FAQ

간단히 말해 abstract interpretation이란 무엇인가? 코드를 실제로 실행하지 않고 “이 포인터는 절대 널이 아니다”와 같은 속성을 증명하기 위해 프로그램의 동작을 근사화하는 정적 분석 기법이다.

Infer는 무료로 사용할 수 있나? 예. Infer는 MIT 라이선스 하에 오픈소스이며 Meta가 유지보수한다.

Infer와 SonarQube를 비교하면 어떤가? SonarQube는 패턴 매칭, 오염 분석, 언어에 따라 더 깊은 분석의 혼합을 사용한다. Infer는 구체적으로 abstract interpretation에 기반하여 구축되었으며 SonarQube가 일반적으로 C, C++, Java, Objective-C에서 하지 않는 방식으로 경로에 민감하다.

Infer를 JavaScript나 Python에서 실행할 수 있나? 직접적으로는 안 된다. Infer는 컴파일 언어를 분석한다. JavaScript와 Python의 경우 CodeQL이나 엄격한 규칙을 가진 ESLint나 Pyright와 같은 타입 인식 린터를 고려하라.

Infer가 CI를 현저히 느리게 하나? 전체 분석은 빌드 시간의 2~4배가 소요된다. 풀 리퀘스트의 증분 분석은 훨씬 빠르고, 보통 몇 분 추가된다.