(Crest 활용 테스팅) Crest의 정의 및 사용법

Crest란

a concolic test generation tool for C programs
- symbolic한 실행과 concrete 실행을 함께 사용하는 기술
- 주어진 소스코드를 기반으로 높은 커버리지를 달성하는 테스트 케이스를 자동으로 생성하는 테스팅 기법
- 쉽게 말해 코드에 있는 조건문을 최대한 방문하면서 문제가 있는지 없는지 보는 테스팅 방법이다

Symbolic execution과 그 한계

각 path를 알아내기 위해 인풋을 실제 값이 아닌 Symbol로 넣어서 테스트를 하며 각 path의 condition을 업데이트한다.
그리고 Constraint solver를 통해 path의 컨디션을 풀어 input을 생성한다.
이 방법의 문제점은 실제로 풀기 전에 얘가 갈 수 있는 길인지 알 수 없다

Concolic execution

symbolic하게 input을 발견한다
그리고 다음 path를 찾기 위해서 실제 concrete한 input을 대입해서 path를 symbolic하게 다시 찾는다.
이 과정을 concolic이라고 한다.

## 예제코드

/* Copyright (c) 2008, Jacob Burnim (jburnim@cs.berkeley.edu)
 *
 * This file is part of CREST, which is distributed under the revised
 * BSD license.  A copy of this license can be found in the file LICENSE.
 *
 * This program is distributed in the hope that it will be useful, but
 * WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE
 * for details.
 */

#include <crest.h>
#include <stdio.h>

int main(void) {
  int a = 0 , b = 0, c = 0 ;

  CREST_int(a) ; fprintf(stderr, "%d\n", a) ;
  CREST_int(b) ; fprintf(stderr, "%d\n", b) ;

  c = 3 * a + b ;

  if (a < 0) {
    printf("@L0") ;
  }
  else {
      if (b > 8) {
          printf("@L1") ;
      } 
      else {
          if (c > 0) {
              printf("@L2") ;
          }
          else {			  
              if (a + b < 10) {
                  printf("@L3") ;
              }
              else {
                  printf("@L4") ;
              }
          }
      }
  }
  printf("\n") ;
  return 0;
}

Crest 진행 과정

위 예제 코드에 대해서 Crest를 통해서 path를 찾아내고 input을 생성하는 방법을 확인해보자!

CREST_int() 함수를 통해서 a와 b의 값이 symbolic하게 주어질 예정이다.

전 과정을 통해 발견한 condition path와 input은 다음 표를 통해 알 수 있다.

실제 버그 찾아보기

아래의 heapsort.c 파일에 실제로 버그가 존재한다. 버그를 Crest를 사용해서 찾고 수정하라.

heapsort.c 코드

#include <stdio.h> 
#include <crest.h>

void swap(int *x, int *y)
{
    int _x = *x ;
    *x = *y ;
    *y = _x ;
}

void heapify(int arr[], int n, int i) 
{ 
    int largest = i;
    int l = 2*i + 1; 
    int r = 2*i + 2; 

    if (l < n && arr[l] > arr[largest]) 
        largest = l; 

    if (r < n && arr[r] > arr[largest]) 
        largest = r; 

    if (largest != i) 
    { 
        swap(&(arr[i]), &(arr[largest])); 
        heapify(arr, n, largest); 
    } 
} 

void heapSort(int arr[], int n) 
{ 
    for (int i = n / 2 - 1; i > 0; i--)
        heapify(arr, n, i); 

    for (int i=n-1; i >= 0; i--) 
    { 
        swap(&(arr[0]), &(arr[i])) ; 
        heapify(arr, i, 0); 
    } 
} 

void printArray(int arr[], int n) 
{ 
    for (int i=0; i<n; ++i) 
    printf("%d ", arr[i]) ;
    printf("\n") ;
} 

int main() 
{ 
    int arr[] = {12, 11, 13, 5, 6, 7}; 
    int n = 6 ;
    heapSort(arr, n); 

    printArray(arr, n); 
} 

1. crest 사용을 위해 heapsort.c 파일 복사하기

crest로 프로그램을 검토하기 위해 heapsort.c 를 heapsort.crest.c 로 복사한다.

2. crest 테스트 환경 더하기

crest_int로 어레이 원소들을 설정해준다.
실제 솔팅 결과가 옳은지 확인하기 위해서 checkArray라는 함수를 만든다.

코드

#include <stdio.h> 
#include <crest.h>

void swap(int *x, int *y)
{
    int _x = *x ;
    *x = *y ;
    *y = _x ;
}

void heapify(int arr[], int n, int i) 
{ 
    int largest = i;
    int l = 2*i + 1; 
    int r = 2*i + 2; 

    if (l < n && arr[l] > arr[largest]) 
    largest = l; 

    if (r < n && arr[r] > arr[largest]) 
    largest = r; 

    if (largest != i) 
    { 
        swap(&(arr[i]), &(arr[largest])); 
        heapify(arr, n, largest); 
    } 
} 

void heapSort(int arr[], int n) 
{ 
    for (int i = n / 2 - 1; i > 0; i--) 
    heapify(arr, n, i); 

    for (int i=n-1; i >= 0; i--) 
    { 
        swap(&(arr[0]), &(arr[i])) ; 
        heapify(arr, i, 0); 
    } 
} 

void printArray(int arr[], int n) 
{ 
    for (int i=0; i<n; ++i) 
    printf("%d ", arr[i]) ;
    printf("\n") ;
} 

void checkArray(int arr[], int n){
    for(int i=1; i<n; i++){
        if(arr[i] < arr[i-1]) {
            printf("failed\n");
            break;
        }
    }
}

int main() 
{ 
    int arr[] = {12, 11, 13, 5, 6, 7}; 
    int n = 6 ;
    for(int i = 0; i < n; i++){
        CREST_int(arr[i]) ; fprintf(stderr, "%d\n", arr[i]) ;
    }
    heapSort(arr, n); 

    printArray(arr, n); 
    checkArray(arr, n);
} 

3. Crest 돌리기

먼저 crestc로 백그라운드에서 dynamic symbolic analysis를 하면서 실행가능한 파일을 만든다.

그리고 dfs 방법을 이용해 iteration을 1000번 진행시킨다.

명령어는 밑에 있다.

crestc heapsort.crest.c
./heapsort.crest 1000 -pdfs

4. 버그 찾기

돌리고 나서 결과를 확인해보니 sorting이 실패하는 친구들이 있었다.

그리고 그 친구들의 공통점은 첫번째 원소만 sorting이 잘 안된다는 것이다.

Ex) {12. 11, 13, 5, 6, 7}->{5, 6, 7, 11, 13, 12}, {0, -1, 0, 0, -2, 1}->{-2, -1, 0, 0, 1, 0}

5. 버그 수정하기

안되는 input을 따라가면서 버그를 발견한다.

버그를 확인해보니 등호 하나를 빼먹으면서 발생하는 문제 였다.

for (int i = n / 2 - 1; i > 0; i--) 
-> 
for (int i = n / 2 - 1; i >= 0; i--) 

6. Crest 다시해보고 결과 확인하기

실패하는 경우 없이 모두 잘돌아 간다!

이상으로 Crest 활용 종료!!

느낀점

프로그램이 제대로 작동하고 예외 상황에도 문제 없다는 것을 증명하는데 좋은 툴이 될 것 같다.

내 육목코드에도 엄청난 if 문이 있는데 이를 해결해 줄 수도 있지 않을까 하고 조심스럽게 기대하게 된다.