CREST: Concolic test generation tool for C programs

https://github.com/ARISE-Handong/crest/

ARISE-Handong/crest

아래의 소스코드는 triangle을 판별하는 코드이다. 

이 소스코드를 CREST Concolic test generation을 이용하여 coverage를 살펴볼 것이다. 

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

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

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

	if (a <= 0 || b<= 0 || c<= 0) {
		printf("@L0\n") ;
		exit(0);  
	}

    // printf("%d %d %d", a, b, c) ;
    //0: Equilateral, 1:Isosceles, 
	// 2: Not a traiangle, 3:Scalene

	int result = -1 ;

	if(a == b) 
		match = match + 1 ;
	if(a == c) 
		match = match + 2 ;
	if(b == c) 
		match = match + 3 ;
	if(match == 0) {
		if(a + b <= c) {
			result = 2 ;
			printf("@L1\n") ;
		}
		else if (b + c <= a) {
			result = 2 ;
			printf("@L2\n") ;
		}
		else if (a + c <= b) {
			result = 2 ;
			printf("@L3\n") ;
		}
		else {
			result = 3 ;
			printf("@L4\n") ;
		}
	} 
	else {
		if(match == 1) {
			if(a + b <= c) {
				result = 2 ;
				printf("@L5\n") ;
			}
			else {
				result = 1 ;
				printf("@L6\n") ;
			}
		} 
		else {
			if (match == 2) {
				if (a + c <= b) {
					result = 2 ;
					printf("L7\n") ;
				}
				else {
					result = 1 ;
					printf("L8\n") ;
            	}
			} 
			else {
				if (match == 3) {
					if(b + c <= a) {
						result = 2 ;
						printf("@L9\n") ;
					}
					else {
						result = 1 ;
						printf("@L10\n") ;
					}
				} 
				else {
					result = 0;
					printf("@L11\n") ;
				}
			}
		}
	}
	printf("result=%d\n",result);
}

crestc로 symbolic execution이 삽입된 코드를 컴파일한다. 

crestc triangle.c

crest를 이용하여 최대 100 iteration까지 DFS를 이용하여 실험한다. 

mck427@peace:~/CREST_HW/crest/test/triangle$ run_crest ./triangle 100 -pdfs
Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Total Elapsed Time: 0.000152917
  Search Time: 0.000152917
  Solving Time: 0
  Program Time: 0
0
0
0
@L0
Iteration 1 (0s): covered 1 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.0108058
  Search Time: 0.00399314
  Solving Time: 0.00270821
  Program Time: 0.00410445
1
0
0
@L0
Iteration 2 (0s): covered 3 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.0197076
  Search Time: 0.00745641
  Solving Time: 0.00415976
  Program Time: 0.00809147
1
1
0
@L0
Iteration 3 (0s): covered 5 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.0285032
  Search Time: 0.011048
  Solving Time: 0.00531351
  Program Time: 0.0121418
1
1
1
@L11
result=0
Iteration 4 (0s): covered 13 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.0389599
  Search Time: 0.0146172
  Solving Time: 0.00806087
  Program Time: 0.0162818
1
1
2
@L5
result=2
Iteration 5 (0s): covered 17 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.0482902
  Search Time: 0.0179812
  Solving Time: 0.009909
  Program Time: 0.0204
2
2
3
@L6
result=1
Iteration 6 (0s): covered 18 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.0586903
  Search Time: 0.0215317
  Solving Time: 0.0125576
  Program Time: 0.024601
1
2
1
L7
result=2
Iteration 7 (0s): covered 21 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.0680405
  Search Time: 0.02501
  Solving Time: 0.0142708
  Program Time: 0.0287597
2
1
2
L8
result=1
Iteration 8 (0s): covered 22 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.0790816
  Search Time: 0.029269
  Solving Time: 0.0169328
  Program Time: 0.0328798
2
1
3
@L1
result=2
Iteration 9 (0s): covered 24 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.0882815
  Search Time: 0.0328593
  Solving Time: 0.0185566
  Program Time: 0.0368657
2
3
4
@L4
result=3
Iteration 10 (0s): covered 27 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.0976706
  Search Time: 0.0363636
  Solving Time: 0.0203117
  Program Time: 0.0409954
1
3
2
@L3
result=2
Iteration 11 (0s): covered 28 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.107074
  Search Time: 0.0397363
  Solving Time: 0.0220659
  Program Time: 0.0452714
3
1
2
@L2
result=2
Iteration 12 (0s): covered 29 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.115946
  Search Time: 0.0432186
  Solving Time: 0.023587
  Program Time: 0.0491402
2
1
1
@L9
result=2
Iteration 13 (0s): covered 31 branches [1 reach funs, 32 reach branches].
Total Elapsed Time: 0.125123
  Search Time: 0.046569
  Solving Time: 0.0253051
  Program Time: 0.0532484
1
2
2
@L10
result=1
Iteration 14 (0s): covered 32 branches [1 reach funs, 32 reach branches].