Symbolic Execution심볼릭 실행

입력: x = α (기호값)

if (x > 0):          경로 조건: α > 0
  if (x * x == x):   경로 조건: α > 0 ∧ α² = α  → α = 1
    bug()            → 이 경로 도달 조건: x = 1

SMT 솔버(Z3 등)가 경로 조건 만족 입력 자동 생성:
  α > 0:            x = 1 가능
  α > 0 ∧ α² = α:  x = 1 → bug 경로 도달!

자동 생성 테스트 케이스: x = 1

초기 상태: σ = {}, π = True

코드:
  x = input()    → σ = {x: α}
  y = x + 1      → σ = {x: α, y: α+1}
  if (y > 10):
    then: π = (α+1 > 10) = (α > 9)
    else: π = (α+1 ≤ 10) = (α ≤ 9)

void func(int A) {
    int ret = 0;
    if (A == 1)
        ret = 100;
    else if (A == 2)
        ret = 200;
    else
        ret = -1;
}

         A = α (기호값)
              │
         A == 1 ?
        /         \
     [참]          [거짓]
   π: α=1         π: α≠1
   ret=100           │
                  A == 2 ?
                 /         \
              [참]          [거짓]
            π: α≠1,α=2    π: α≠1,α≠2
            ret=200        ret=-1

테스트 케이스:
  A=1  → ret=100  (π: A=1)
  A=2  → ret=200  (π: A≠1 ∧ A=2)
  A=3  → ret=-1   (π: A≠1 ∧ A≠2)

// test_me.c
# include <klee/klee.h>
# include <assert.h>

int test_me(int a, int b) {
  if (a == b) return 0;
  if (a + b > 10) {
    if (a > 5) return 1;   // 잠재적 버그 경로
    return 2;
  }
  return 3;
}

int main() {
  int a, b;
  klee_make_symbolic(&a, sizeof(a), "a");  // a를 기호 변수로 선언
  klee_make_symbolic(&b, sizeof(b), "b");  // b를 기호 변수로 선언
  test_me(a, b);
  return 0;
}

# 컴파일 및 실행
clang -emit-llvm -c test_me.c -o test_me.bc
klee test_me.bc

# KLEE가 자동 생성하는 테스트 케이스
# klee-out/test000001.ktest  → a=b (return 0 경로)
# klee-out/test000002.ktest  → a+b>10, a>5 (return 1 경로)
# klee-out/test000003.ktest  → a+b>10, a≤5 (return 2 경로)
# klee-out/test000004.ktest  → a+b≤10 (return 3 경로)

n개의 독립 if문 → 최대 2ⁿ 경로
while(N > 0)   → N값에 따라 임의로 많은 경로

예: 32개 독립 분기 → 4,294,967,296 경로

x = twice(y)  // 외부 함수 호출 → 기호 표현 불가
x * x = y     // 비선형 수식 → SMT 솔버 어려움

1. 초기 구체적 입력값으로 실행 (예: x=22, y=7)
2. 동시에 경로 제약 조건 수집
3. 미탐색 경로의 제약을 부정(Negate)하여 새 입력 생성
4. 새 입력으로 다시 실행 → 반복

장점:
- 비선형 함수는 구체적 값으로 처리
- 더 넓은 범위의 코드에 적용 가능
- 제약 풀이 실패 시 구체적 값으로 근사

목표 변수와 무관한 제약 조건 제거:
(x + y > 10) ∧ (z > 0) ∧ (y < 12) ∧ (z - x = 0)
→ x만 필요하다면: (x + y > 10) ∧ (z - x = 0)

이전 경로: π₁ = (a > 5) ∧ (b < 10)  → 해: a=6, b=9
다음 경로: π₂ = (a > 5) ∧ (b < 10) ∧ (a + b > 14)

기존 해(a=6, b=9)가 π₂를 만족하는지 확인 → 만족하면 재사용

from z3 import *

# 기호 변수 선언
a, b = Ints('a b')
solver = Solver()

# 경로 1: a == b
solver.push()
solver.add(a == b)
if solver.check() == sat:
    print("경로 1:", solver.model())  # a=0, b=0

# 경로 2: a != b, a+b > 10, a > 5
solver.pop(); solver.push()
solver.add(a != b, a + b > 10, a > 5)
if solver.check() == sat:
    print("경로 2:", solver.model())  # a=6, b=5

# 경로 3: a != b, a+b > 10, a <= 5
solver.pop(); solver.push()
solver.add(a != b, a + b > 10, a <= 5)
if solver.check() == sat:
    print("경로 3:", solver.model())  # a=1, b=10