Alive2 검증 도구에서 놓친 경보 버그를 찾는 방법

Looking for Missed Alarm Bugs in a Formal Verification Tool

Alive2는 LLVM 최적화의 정확성을 검증하는 도구로, 컴파일러 엔지니어들이 널리 사용합니다. 이 글에서는 Alive2가 실제 버그를 놓치는 'missed alarm' 결함을 찾기 위한 두 가지 방법을 소개합니다. 첫째, YARPGen을 변형하여 무작위로 생성한 함수 쌍이 서로 다른 동작을 하도록 하고 Alive2가 이를 감지하는지 확인합니다. 둘째, Minotaur 슈퍼옵티마이저가 생성하는 수많은 후보를 검증하는 과정에서 Alive2가 잘못 통과시키는 경우를 찾습니다. 현재까지는 큰 문제가 발견되지 않았지만, 함수 속성 등 특정 영역에 대한 추가 테스트가 필요하다고 저자는 말합니다.