CNUproject/코드 동일성 검사 도구
24_Python IR에 KLEE 함수 직접 추가해보기
YUMMMM
2023. 11. 2. 00:30
1. Python 코드
#!/usr/bin/env python
import numba as nb
@nb.jit(nopython=True)
def add(num):
num += num
return num
@nb.jit(nopython=True)
def mul(num):
num *= 2
return num
@nb.jit(nopython=True)
def main():
num = 10
add_result = add(num)
mul_result = mul(num)
if __name__ == "__main__":
main()
2. .py를 .ll로 변경
numba KleeTest.py --dump-llvm > KleeTest.ll
3. KLEE 함수 삽입
수정 전
--------------------LLVM DUMP <function descriptor 'add$2'>---------------------
; ModuleID = "add$2"
target triple = "arm64-apple-darwin22.6.0"
target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
@"_ZN08NumbaEnv8__main__3addB2v2B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29" = common global i8* null
define i32 @"_ZN8__main__3addB2v2B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29"(i64* noalias nocapture %"retptr", {i8*, i32, i8*, i8*, i32}** noalias nocapture %"excinfo", i64 %"arg.num")
{
entry:
br label %"B0"
B0:
%".5" = add nsw i64 10, 10
store i64 %".5", i64* %"retptr"
ret i32 0
}
================================================================================
--------------------LLVM DUMP <function descriptor 'mul$3'>---------------------
; ModuleID = "mul$3"
target triple = "arm64-apple-darwin22.6.0"
target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
@"_ZN08NumbaEnv8__main__3mulB2v3B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29" = common global i8* null
define i32 @"_ZN8__main__3mulB2v3B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29"(i64* noalias nocapture %"retptr", {i8*, i32, i8*, i8*, i32}** noalias nocapture %"excinfo", i64 %"arg.num")
{
entry:
br label %"B0"
B0:
%".5" = mul nsw i64 10, 2
store i64 %".5", i64* %"retptr"
ret i32 0
}
================================================================================
--------------------LLVM DUMP <function descriptor 'main$1'>--------------------
; ModuleID = "main$1"
target triple = "arm64-apple-darwin22.6.0"
target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
@"_ZN08NumbaEnv8__main__4mainB2v1B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE" = common global i8* null
define i32 @"_ZN8__main__4mainB2v1B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE"(i8** noalias nocapture %"retptr", {i8*, i32, i8*, i8*, i32}** noalias nocapture %"excinfo")
{
entry:
%".5" = alloca i64
store i64 0, i64* %".5"
%"excinfo.1" = alloca {i8*, i32, i8*, i8*, i32}*
store {i8*, i32, i8*, i8*, i32}* null, {i8*, i32, i8*, i8*, i32}** %"excinfo.1"
%"try_state" = alloca i64
store i64 0, i64* %"try_state"
%".32" = alloca i64
store i64 0, i64* %".32"
%"excinfo.2" = alloca {i8*, i32, i8*, i8*, i32}*
store {i8*, i32, i8*, i8*, i32}* null, {i8*, i32, i8*, i8*, i32}** %"excinfo.2"
br label %"B0"
B0:
%".4" = load i8*, i8** @"numba.dynamic.globals.11a315f80"
store i64 0, i64* %".5"
%".9" = call i32 @"_ZN8__main__3addB2v2B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29"(i64* %".5", {i8*, i32, i8*, i8*, i32}** %"excinfo.1", i64 10)
%".10" = load {i8*, i32, i8*, i8*, i32}*, {i8*, i32, i8*, i8*, i32}** %"excinfo.1"
%".11" = icmp eq i32 %".9", 0
%".12" = icmp eq i32 %".9", -2
%".13" = icmp eq i32 %".9", -1
%".14" = icmp eq i32 %".9", -3
%".15" = or i1 %".11", %".12"
%".16" = xor i1 %".15", -1
%".17" = icmp sge i32 %".9", 1
%".18" = select i1 %".17", {i8*, i32, i8*, i8*, i32}* %".10", {i8*, i32, i8*, i8*, i32}* undef
%".19" = load i64, i64* %".5"
br i1 %".16", label %"B0.if", label %"B0.endif", !prof !0
B0.if:
store i64 0, i64* %"try_state"
%".23" = load i64, i64* %"try_state"
%".24" = icmp ugt i64 %".23", 0
%".25" = load {i8*, i32, i8*, i8*, i32}*, {i8*, i32, i8*, i8*, i32}** %"excinfo"
store {i8*, i32, i8*, i8*, i32}* %".18", {i8*, i32, i8*, i8*, i32}** %"excinfo"
%".27" = xor i1 %".24", -1
br i1 %".27", label %"B0.if.if", label %"B0.if.endif"
B0.endif:
%".31" = load i8*, i8** @"numba.dynamic.globals.11a316020"
store i64 0, i64* %".32"
%".36" = call i32 @"_ZN8__main__3mulB2v3B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29"(i64* %".32", {i8*, i32, i8*, i8*, i32}** %"excinfo.2", i64 10)
%".37" = load {i8*, i32, i8*, i8*, i32}*, {i8*, i32, i8*, i8*, i32}** %"excinfo.2"
%".38" = icmp eq i32 %".36", 0
%".39" = icmp eq i32 %".36", -2
%".40" = icmp eq i32 %".36", -1
%".41" = icmp eq i32 %".36", -3
%".42" = or i1 %".38", %".39"
%".43" = xor i1 %".42", -1
%".44" = icmp sge i32 %".36", 1
%".45" = select i1 %".44", {i8*, i32, i8*, i8*, i32}* %".37", {i8*, i32, i8*, i8*, i32}* undef
%".46" = load i64, i64* %".32"
br i1 %".43", label %"B0.endif.if", label %"B0.endif.endif", !prof !0
B0.if.if:
ret i32 %".9"
B0.if.endif:
br label %"B0.endif"
B0.endif.if:
%".48" = load i64, i64* %"try_state"
%".49" = icmp ugt i64 %".48", 0
%".50" = load {i8*, i32, i8*, i8*, i32}*, {i8*, i32, i8*, i8*, i32}** %"excinfo"
store {i8*, i32, i8*, i8*, i32}* %".45", {i8*, i32, i8*, i8*, i32}** %"excinfo"
%".52" = xor i1 %".49", -1
br i1 %".52", label %"B0.endif.if.if", label %"B0.endif.if.endif"
B0.endif.endif:
store i8* null, i8** %"retptr"
ret i32 0
B0.endif.if.if:
ret i32 %".36"
B0.endif.if.endif:
br label %"B0.endif.endif"
}
@"numba.dynamic.globals.11a315f80" = linkonce global i8* inttoptr (i64 4734410624 to i8*)
declare i32 @"_ZN8__main__3addB2v2B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29"(i64* noalias nocapture %"retptr", {i8*, i32, i8*, i8*, i32}** noalias nocapture %"excinfo", i64 %"arg.num")
@"numba.dynamic.globals.11a316020" = linkonce global i8* inttoptr (i64 4734410784 to i8*)
declare i32 @"_ZN8__main__3mulB2v3B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29"(i64* noalias nocapture %"retptr", {i8*, i32, i8*, i8*, i32}** noalias nocapture %"excinfo", i64 %"arg.num")
!0 = !{ !"branch_weights", i32 1, i32 99 }
================================================================================
수정 후
; ModuleID = "add$2"
target triple = "arm64-apple-darwin22.6.0"
target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
declare dso_local void @klee_make_symbolic(i64*, i64, i8*)
declare dso_local void @klee_assume(i1)
@"_ZN08NumbaEnv8__main__3addB2v2B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29" = common global i8* null
define i32 @"_ZN8__main__3addB2v2B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29"(i64* noalias nocapture %"retptr", {i8*, i32, i8*, i8*, i32}** noalias nocapture %"excinfo", i64 %"arg.num")
{
entry:
br label %"B0"
B0:
%".5" = add nsw i64 10, 10
store i64 %".5", i64* %"retptr"
ret i32 0
}
; ModuleID = "mul$3"
@"_ZN08NumbaEnv8__main__3mulB2v3B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29" = common global i8* null
define i32 @"_ZN8__main__3mulB2v3B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29"(i64* noalias nocapture %"retptr", {i8*, i32, i8*, i8*, i32}** noalias nocapture %"excinfo", i64 %"arg.num")
{
entry:
br label %"B0"
B0:
%".5" = mul nsw i64 10, 2
store i64 %".5", i64* %"retptr"
ret i32 0
}
; ModuleID = "main$1"
@"numba.dynamic.globals.11e015f80" = linkonce global i8* inttoptr (i64 4798373760 to i8*)
@"numba.dynamic.globals.11e016020" = linkonce global i8* inttoptr (i64 4798373920 to i8*)
define i32 @"main"(i8** noalias nocapture %"retptr", {i8*, i32, i8*, i8*, i32}** noalias nocapture %"excinfo")
{
entry:
%".5" = alloca i64
call void @klee_make_symbolic(i64* %".5", i64 8, i8* null)
store i64 0, i64* %".5"
%"excinfo.1" = alloca {i8*, i32, i8*, i8*, i32}*
store {i8*, i32, i8*, i8*, i32}* null, {i8*, i32, i8*, i8*, i32}** %"excinfo.1"
%"try_state" = alloca i64
store i64 0, i64* %"try_state"
%".32" = alloca i64
store i64 0, i64* %".32"
%"excinfo.2" = alloca {i8*, i32, i8*, i8*, i32}*
store {i8*, i32, i8*, i8*, i32}* null, {i8*, i32, i8*, i8*, i32}** %"excinfo.2"
%add_result = alloca i32
%mul_result = alloca i32
br label %"B0"
B0:
%".4" = load i8*, i8** @"numba.dynamic.globals.11e015f80"
store i64 0, i64* %".5"
%".9" = call i32 @"_ZN8__main__3addB2v2B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29"(i64* %".5", {i8*, i32, i8*, i8*, i32}** %"excinfo.1", i64 10)
store i32 %".9", i32* %add_result
%".10" = load {i8*, i32, i8*, i8*, i32}*, {i8*, i32, i8*, i8*, i32}** %"excinfo.1"
%".11" = icmp eq i32 %".9", 0
%".12" = icmp eq i32 %".9", -2
%".13" = icmp eq i32 %".9", -1
%".14" = icmp eq i32 %".9", -3
%".15" = or i1 %".11", %".12"
%".16" = xor i1 %".15", -1
%".17" = icmp sge i32 %".9", 1
%".18" = select i1 %".17", {i8*, i32, i8*, i8*, i32}* %".10", {i8*, i32, i8*, i8*, i32}* undef
%".19" = load i64, i64* %".5"
br i1 %".16", label %"B0.if", label %"B0.endif", !prof !0
B0.if:
store i64 0, i64* %"try_state"
%".23" = load i64, i64* %"try_state"
%".24" = icmp ugt i64 %".23", 0
%".25" = load {i8*, i32, i8*, i8*, i32}*, {i8*, i32, i8*, i8*, i32}** %"excinfo"
store {i8*, i32, i8*, i8*, i32}* %".18", {i8*, i32, i8*, i8*, i32}** %"excinfo"
%".27" = xor i1 %".24", -1
br i1 %".27", label %"B0.if.if", label %"B0.if.endif"
B0.endif:
%".31" = load i8*, i8** @"numba.dynamic.globals.11e016020"
store i64 0, i64* %".32"
%".36" = call i32 @"_ZN8__main__3mulB2v3B38c8tJTIcFKzyF2ILShI4CrgQElQb6HczSBAA_3dE24Literal_5bint_5d_2810_29"(i64* %".32", {i8*, i32, i8*, i8*, i32}** %"excinfo.2", i64 10)
store i32 %".36", i32* %mul_result
%add_value = load i32, i32* %add_result, align 4
%mul_value = load i32, i32* %mul_result, align 4
%cmp = icmp ne i32 %add_value, %mul_value
call void @klee_assume(i1 %cmp)
%".37" = load {i8*, i32, i8*, i8*, i32}*, {i8*, i32, i8*, i8*, i32}** %"excinfo.2"
%".38" = icmp eq i32 %".36", 0
%".39" = icmp eq i32 %".36", -2
%".40" = icmp eq i32 %".36", -1
%".41" = icmp eq i32 %".36", -3
%".42" = or i1 %".38", %".39"
%".43" = xor i1 %".42", -1
%".44" = icmp sge i32 %".36", 1
%".45" = select i1 %".44", {i8*, i32, i8*, i8*, i32}* %".37", {i8*, i32, i8*, i8*, i32}* undef
%".46" = load i64, i64* %".32"
br i1 %".43", label %"B0.endif.if", label %"B0.endif.endif", !prof !0
B0.if.if:
ret i32 %".9"
B0.if.endif:
br label %"B0.endif"
B0.endif.if:
%".48" = load i64, i64* %"try_state"
%".49" = icmp ugt i64 %".48", 0
%".50" = load {i8*, i32, i8*, i8*, i32}*, {i8*, i32, i8*, i8*, i32}** %"excinfo"
store {i8*, i32, i8*, i8*, i32}* %".45", {i8*, i32, i8*, i8*, i32}** %"excinfo"
%".52" = xor i1 %".49", -1
br i1 %".52", label %"B0.endif.if.if", label %"B0.endif.if.endif"
B0.endif.endif:
store i8* null, i8** %"retptr"
ret i32 0
B0.endif.if.if:
ret i32 %".36"
B0.endif.if.endif:
br label %"B0.endif.endif"
}
!0 = !{ !"branch_weights", i32 1, i32 99 }
%".5" : name 역할
main 함수에서 klee_make_symbolic 함수로 전달
%".9" : add함수의 반환값
%".32" : mul함수의 반환값
두 값을 비교하고, klee_assume 함수로 전달
4. .ll 파일을 .bc 파일로 변환
llvm-as KleeTest.ll -o KleeTest.bc
5. 결과
klee KleeTest.bc