최적화 기회를 찾기
일반 최적화기가 처리하지 못한 작은 연산 조합에서도 더 간단한 표현이 가능할 수 있다. Souper는 비트코드에서 질의를 추출해 해결기에 전달한다. 조건을 만족하는 대체 표현을 찾아 기존 표현과 함께 제시하는 방식으로 활용할 수 있다.
탐색과 적용의 구분
찾은 최적화 기회를 출력해서 검토하거나 LLVM 패스를 통해 비트코드에 적용할 수 있다. Clang 계열 도구와 연동하는 경로도 제공한다. 최적화 후보를 찾는 도구와 이미 수행된 변환을 검증하는 도구는 관심 대상이 다르다.
캐시와 버전 관리
해결기 질의를 반복하는 비용을 줄이기 위해 캐시를 사용할 수 있다. 외부 캐시 구성은 Redis를 이용하며 도구 변경에 따른 캐시 호환성을 고려해야 한다. 결과를 비교할 때는 소스뿐 아니라 LLVM, 해결기, Souper의 구성도 함께 맞춘다.
관련 문서
Alive2 / Z3 / KLEE / Smt-Switch