symbolic execution 이란 무엇인가?

Symbolic Execution은 대부분의 낯선 것들이 그렇듯 관념적으로 이해하게 된다.

이 글에서는 Symbolic Execution 을 만든 사람들이 어떤 고민을 했는지를 생각해보는 과정을 통해 그리고 몇 가지 예시를 통해

 

 

수학에서는 함수를 f 로 표기하고 함수=function이라고 부른다.

공교롭게도 이 함수는 프로그래밍에서 함수=function이라고 부르는 것과 일치한다 .

 

f(x) = x + 4  인 함수를 C로 작성한다면?

int f(int x) {
  return x+4;
}

너무 쉬워서 더 생각할 필요도 없는것 같지만 Symbolic Execution은 우리가 간과하는 것을 고민한다.

대표적인게, "위에서 작성한 코드를 어떻게 테스트 할 수 있을까?"에 대한 고민이 그것이다.

내 생각에 고민은 크게 두 방향인 것 같다.

1. 작성된 함수 f에 대해 옳바른 검증을 할 수 있는가?

2. 작성된 함수 f에 대해 효율적인 검증을 할 수 있는가?

 

 

1. 작성된 함수 f에 대해 옳바른 검증을 할 수 있는가? 를 생각해보자.

위 코드를 테스트하는 간단한 테스트 함수를 만들어본다.

#include <stdio.h>                         
#include <limits.h>                        
#include <assert.h>                        
                                           
int f(int x) {                             
  return x+4;                        
}                                          
                                           
int test() {                               
  for(int i = 0; i < INT_MAX; i++)   
    assert((i+4) == f(i));     
}                                          
                              
int bug() {
  printf("%d + %d = %d\n", INT_MAX, f(INT_MAX), INT_MAX+f(INT_MAX));
}                                                        
                                  
int main()                                 
{     
  test();
  bug();               
}

위 함수는 test()를 호출했을때 문제가 발생하지 않는다 .

 

하지만, bug 함수를 호출한 결과는 그렇지 않다.

2147483647 + -2147483645 = 2

INT_MAX=2147483647 에서 정수오버플로우가 발생해 INT_MAX+4=-2147483645 가 되고,
두 값을 더한 값이 -2가 되버렸다.

 

우리가 기대한 값은 이렇다.

2147483647 + 2147483651 = 4294967298

 

그러므로 올바른 테스트는 아래처럼 작성되어야 했을 것이다.

int 의 값의 범위는 –2,147,483,648 ~ 2,147,483,647 의 min/max을 테스트하는 예제이다.

#include <stdio.h>
#include <limits.h>
#include <assert.h>

int f(int x) {
  return x+4;
}

int test() {
 int low = -2147483648;
 int max = 2147483647;
 assert(f(low) == -2147483644);
 assert(f(max) == 2147483651);
}

int bug() {
  printf("%d + %d = %d\n", INT_MAX, f(INT_MAX), INT_MAX+f(INT_MAX));
}

int main()
{
  test();
  bug();
}

그리고 이 테스트는 문제를 검출할 수 있었다.

test.c:13: test: Assertion `f(max) == 2147483651' failed. Aborted

 

2. 작성된 함수 f에 대해 효율적인 검증을 할 수 있는가?

f(x) 가 처음 작성됐을때는 x+4를 반환하는 간단한 함수였으나, 이후 여러가지 예외와 조건이 붙기 시작했다.

이런 상황에서 어떻게 효율적인 검증을 할 수 있을까?

 

예를 들어 다음의 조건들이 f(x)에 추가된다.

1. 값 1000의 마다 4를 추가로 더한다.

2. x가 3의 배수이면 3번째 4를 더할때마다 1을 추가로 더한다.

3. x가 4의 배수이면 4번째 4를 더할때마다 1을 추가로 더한다.

4. x가 3의 배수이면서 4의 배수이면 12번째 4를 더할때마다 12를 추가로 더한다.

 

(TODO:: 몇 가지 조건이 추가된 f(x)의 테스트 코드 작성. 값의 범위 선정. 테스트 시간)

 

 

 

위의 1, 2 과정을 통해 버그 수정이나 기능 추가와 같은 유지보수 과정 속에서 코드 품질을 유지하기 위해 우리가 사용했던 방식을 Symbolic Execution이 등장하며 Concrete Execution 이라고 부르게 된다. 이는 검증을 위한 "고정된 값과 고정된 경로의 테스트 방식"을 뜻한다.

 

Concrete Execution

검증을 위한 "고정된 값과 고정된 경로의 테스트 방식"을 뜻한다.

 

그렇다면 Symbolic Execution은 무엇이 다를까?

 

 

(TODO:: Symbolic Execution 1, 2 답습)

 

 

Concolic Execution aka Dynamic Symbolic Execution