__bool__ 오버로딩을 통한 심볼릭 실행
2024-12-24
이 글에서는 Z3 Python 라이브러리에서 __bool__ 함수를 오버로딩하여 Python 코드의 심볼릭 실행을 수행하는 영리한 기법을 소개합니다. 저자는 Z3의 기능을 활용하여 Python 조건문을 Z3 표현식으로 변환하여 경로 탐색 및 결과 분석을 가능하게 합니다. 이러한 접근 방식은 복잡한 AST 순회를 피하고 Python 코드 내에서 직접 사용할 수 있으므로 심볼릭 실행을 간소화합니다.