18_LLVM Pass 작성 후 적용하기 (with Z3)

이번 주에는 Z3를 불러와서 사용하는 pass를 작성하여 C코드와 Python코드에 대해 적용해보았다.

 

1. Z3 설치 및 빌드

git clone https://github.com/Z3Prover/z3.git
python scripts/mk_make.py
cd build
make
sudo make install

 

2. 작성한 Pass

 

Z3Pass.cpp (llvm/lib/Transforms/Z3Pass/Z3Pass.cpp)

#include "llvm/Pass.h"
#include "llvm/IR/Function.h"
#include "llvm/Support/raw_ostream.h"
#include "z3++.h"

using namespace llvm;

namespace {
  struct Z3Pass : public FunctionPass {
    static char ID;
    z3::context context;

    Z3Pass() : FunctionPass(ID), context() {}

    virtual bool runOnFunction(Function &F) override {
      z3::expr x = context.int_const("x"); // 정수형 변수 x 생성
      z3::expr y = context.int_const("y"); // 정수형 변수 y 생성
      z3::solver s(context); // sover s 객체 생성
      s.add(x + y == 10); // 객체 s에 x + y == 10 이라는 조건 추가

      if (s.check() == z3::sat) { // 만약 s에 추가된 조건을 만족하는 해가 존재한다면
        outs() << "x + y == 10 is satisfiable\n";
      } else {
        outs() << "x + y == 10 is not satisfiable\n";
      }

      return false;
    }
  };
}

char Z3Pass::ID = 0;
static RegisterPass<Z3Pass> X("Z3Pass", "My custom LLVM pass with Z3");

- runOnFunction : LLVM에서 함수가 분석되거나 변환될 때 호출된다.

- Funtion &F : 현재 작업 중인 함수 변수

- Z3Pass:ID = 0 : Z3Pass의 ID 변수 초기화, 이 변수는 패스의 유니크한 식별자로 사용된다. 0은 임의의 값을 나타낸다.

- RegisterPass : LLVM Pass에 등록

 

해당 패스는 함수가 분석될 때마다 z3를 사용하여 정수형 변수 x, y를 생성하고 x+y==10인 조건을 추가하여 해당 조건을 만족하는 해가 있다면 "x + y == 10 is satisfiable" 라는 문구를 출력하고, 조건을 만족하는 해가 없다면  "x + y == 10 is not satisfiable" 라는 문구를 출력한다. Z3Pass의 ID를 0으로 초기화하고, RegisterPass 템플릿을 사용하여 Z3Pass 라는 이름의 패스를 LLVM에 등록한다.

이때 My custom LLVM pass with Z3은 패스에 대한 간단한 설명이다.

 

---

 

3. 패스 적용 과정

 

3-1. Pass를 적용시킬 C코드와 Python코드 작성

 

test.c : add 함수와 main 함수가 있는 간단한 코드

#include <stdio.h>

int add(int x, int y) {
	return x + y;
}

int main() {
	return add(1, 2);
}

 

test.py : main 함수가 있는 간단한 코드

#!/usr/bin/env python

import numba as nb

@nb.jit(nopython=True)
def main():
    sum = 0

    for number in [31, 63, 62, 87, 14]:
        sum += number

    print("sum:", sum)

if __name__ == "__main__":
    main()

---

3-2. CMakeLists.txt 작성 및 수정

(https://blueee.tistory.com/17 에서 1번, 2번 참고)

 

1. CMakeLists.txt (llvm/lib/Transforms/Z3Pass/CMakeLists.txt)

# Find Z3 package
find_package(Z3 REQUIRED)

# Include the Z3++ header directory
include_directories(/opt/homebrew/include)

add_compile_options(-fexceptions)
add_llvm_library(Z3Pass MODULE Z3Pass.cpp
 DEPENDS intrinsics_gen
 PLUGIN_TOOL opt
)

# Link against the Z3 library
target_link_libraries(Z3Pass ${Z3_LIBRARIES})

- find_package(Z3 REQUIRED) : 시스템에 Z3 패키지가 설치되어 있는지 확인하고 Z3 패키지가 없다면 에러를 발생시킨다.

- include_directories(/opt/homebrew/include) : C++ 코드에서 사용되는 Z3 헤더파일 위치를 추가하여 해당 디렉토리를 포함시킨다.

- add_compile_options(-fexceptions) : -fexceptions 컴파일 옵션을 추가하여 C++에서 예외 처리를 활성화한다.

- add_llvm_library(Z3Pass MODULE Z3Pass.cpp DEPENDS intrinsics_gen PLUGIN_TOOL opt) : Z3Pass.cpp을 사용하여 Z3Pass라는 LLVM 모듈을 생성한다. 

- target_link_libraries(Z3Pass ${Z3_LIBRARIES}) : Z3Pass 모듈을 빌드할 때, Z3 라이브러리를 링크한다.

 

2. CMakeLists.txt (llvm/lib/Transforms/CMakeLists.txt) 수정

add_subdirectory(폴더명)

llvm/lib/Transforms에 생성한 패스 디렉토리명을 추가해주면 된다.

---

3-3. 빌드 과정

1. llvm 프로젝트 재빌드 (참고 : https://blueee.tistory.com/15)

2. build/lib/Transforms/Z3Pass(추가한 패스 directory) 에서 make 진행 후 build/lib 에 Z3Pass.dylib (패스.dylib) 파일 생겼는지 확인

3. 패스를 적용할 C와 Python 파일을 .bc 파일로 변경한다.

 

test.c > test.bc

clang -c -emit-llvm test.c -o test.bc

 

test.py > test.bc (numba를 사용하기 때문에 numba를 설치한 후 진행)

numba test.py --dump-llvm test.ll
sudo llvm-as test.ll -o pythonTest.bc

---

3-4. 패스 적용

../build/bin/opt -load ../build/lib/Z3Pass.dylib -Z3Pass test.bc -o outZ3.bc

이때, opt는 경로를 지정해서 사용해준다.

 

C코드에는 함수가 add, main 두 개가 있었으므로 runOnFunction 함수가 두 번 실행되고, 문구가 두 번 출력된다.

 

python코드에는 함수가 main 한 개가 있었으므로 runOnFunction 함수가 한 번 실행되고, 문구가 한 번 출력된다.