14-4 화이트박스 테스트(동적 심볼릭 테스트)

동적 심볼릭 테스트 기법은 소스 코드를 기반으로 하는 테스트 케이스를 선정하여 프로그램 내에 존재하는 버그를 찾아내는 데 목적이 있다. 심볼릭 테스트는 콘콜릭 테스트라고도 하는데 Concolic은 전통적 실행(concrete execution) 기반 테스트와 기호 실행(symbolic execution) 기반 테스트를 혼합한 기법이다.

🔢 기호 실행

입력값을 대신하여 기호(미지수)를 사용한다.
이 방식을 적용하면 특정 문장을 만족하는 입력값을 쉽게 알 수 있다.

📌 예시

int foo(int x) {
    if (x > 10) {
        return 1;
    } else {
        return 0;
    }
}

• 기호 실행에서는 x를 실제 값이 아닌 기호 X로 둔다.
• 분기 조건은 X > 10이라는 제약식으로 기록된다.
• SMT 솔버는 이 제약식을 만족하는 값(예: x = 11)을 찾아낸다.

(이모지) 콘콜릭 실행

SMT는 어떤 제약 사항이 주어졌을 때 모든 가능한 조합을 고려하여 만족할 만한 해를 결정해주는 기능이다.
콘콜릭 테스트를 수행하려면 SMT이 필요하다.

CS(Concrete Store)

코드의 특정 지점에 있는 실제 값을 저장하는 변수

SS(Symbolic Store)

코드의 특정 지점에 있는 심볼 값을 저장하는 함수

PC(Path Constraints)

특정 지점에서 만족되어야 하는 분기 조건을 저장하는 변수

🔍 콘콜릭 실행 예시

프로그램

int test(int a, int b) {
    if (a > 5) {
        if (b == a) {
            return 1;
        }
    }
    return 0;
}

① 첫 실행(Concrete Execution)

• 입력: (a=3, b=2)
• 실행 경로: a > 5 → 거짓 → return 0
• Path Constraint(PC): [a ≤ 5]

② SMT Solver가 새로운 입력 생성

• 기존 제약식의 부정을 사용하여 새로운 입력을 생성:
  a > 5 → 예: (a=6, b=2)

③ 두 번째 실행

• 입력: (a=6, b=2)
• 실행 경로: a > 5 → 참, b == a → 거짓 → return 0
• PC: [a > 5, b ≠ a]

④ SMT Solver가 또 다른 입력 생성

• 제약식 부정: b == a → 예: (a=6, b=6)
• 새로운 실행에서 return 1을 탐지

✅ 결과적으로, 모든 분기 조건을 만족하는 입력 세트가 자동으로 생성되어 테스트 커버리지가 높아진다.