6 posts
Infer를 사용하여 CI 파이프라인에서 형식적 정적 분석을 실행하는 방법. 작동하는 설정과 현실적인 트레이드오프를 소개한다.
abstract interpretation은 엔지니어가 탭을 닫게 만드는 유형의 용어다. 이해하려면 격자 이론을 한 학기 배워야 할 것처럼 들린다. 대부분의 개발자는 이것이 연구 논문에나 나오는 것이지 풀 리퀘스트에는 관련 없는 것으로 생각한다. 그 가정은 비싼 대가를 치른다.…
대규모 언어 모델은 정적 분석의 false positive을 선별하는 데 도움이 되지만, abstract interpretation처럼 프로그램의 의미론을 이해하는 것은 아니다. 두 가지를 결합하는 방법을 설명한다.
당신의 정적 분석기가 금요일 오후에 847개의 경고를 출력했다. 통계적으로 그중 5%에서 15%가 실제 버그다. 나머지는 false positive이다: 생성된 코드의 데드 스토어, 도구에게는 의심스러워 보이지만 사람에게는 분명한 널 체크, 중요하지 않은 해시 함수의 정수 오버플로.…
Facebook이 어떻게 abstract interpretation과 의도적인 unsoundness를 사용하여 수백만 줄의 Android 코드에서 race condition을 대규모로 발견했는가.
Facebook의 Android 앱에는 성능 문제가 있었다. UI 스레드가 작업에 압도당했지만, 코드를 백그라운드 스레드로 이동하면 race condition이 발생했다. 프로덕션의 크래시. 화난 사용자. 그들은 더 나은 코드 리뷰나 더 많은 테스트로 이를 해결하지 않았다. 그들은…
Meta의 Infer는 abstract interpretation과 양방향 추론을 사용해 코드 구조를 분석하여 null reference, memory leak, race condition을 발견한다. 실행은 필요 없다. 작동 방식과 자체 코드베이스에서의 활용법을 설명한다.
Meta는 코드가 사용자에게 도달하기 전에 정적 분석기가 포착한 10만 건 이상의 버그 수정을 배포했다. 이 도구의 이름은 Infer이며 오픈 소스이고 코드를 실행하지 않는다. 코드를 읽어 코드가 할 수 있는 동작의 수학적 모델을 구축하고, 특정한 나쁜 일이 일어날 수 없음을…
추상 해석은 모든 가능한 프로그램 상태를 과대 근사합니다. 추상화 안에서 0으로 나누기에 도달할 수 없다면, 실제 코드에서도 도달할 수 없습니다. 다음은 그 작동 원리와 한계입니다.
정적 분석은 비행기가 추락하지 않음을 증명할 수 없습니다. 하지만 고도계 제어 루프가 0으로 나누기를 절대 하지 않고, 배열 범위를 벗어나는 인덱싱을 절대 하지 않으며, 고정 소수점 누산기에서 오버플로우가 절대 발생하지 않음은 증명할 수 있습니다. 이 둘의 차이가 중요한 이유는,…
추상 해석은 실행 전에 런타임 에러가 불가능함을 증명하게 해줍니다. 실제로 어떻게 작동하는지, 왜 어려운지, 그리고 도구 체인의 어디에 맞는지 알아봅니다.
테스트 스위트는 통과했다. 타입 체커는 초록불이다. 배포했다. 두 시간 후, 프로덕션에서 아묏도 테스트하지 않은 엣지 케이스에서 가 발생했다. 테스트는 버그를 찾는다. 타입은 일부를 방지한다. 둘 다 프로그램이 런타임 에러로부터 자유롭다는 것을 증명하지는 못한다. 그것을 위해서는 더…