Dynamic Symbolic Execution의 다른 종류인, Execution Generated Testing에 대해 알아보자 !
🌳 Execution-Generated Testing의 동작 방식
state집합을 유지한다.
state를 반복적으로고르고,실행하고,fork하는 프로세스를 반복한다.
이 과정에서 state 집합을 유지하면서 특정 state를 고르고, 실행하고, fork한다.
state S는 tuple (instr, store, PC)이다.
instr : 이 state가 실행할 다음 명령어
store : 프로그램 변수를 symbolic value로 맵핑하는 store이다 . concolic testing의 symbolic state이다.
pc : symbolic branch condition의 conjunction이다.
첫 줄이므로 initial State S0는 위와 같다.
🔔 Error 지점에 도달하고자 할 때, 어떻게 테스트케이스를 generate할 수 있을까?
1) Initial State
Initial State 이후,
Candidate State는 처음에 S0 하나 뿐이다.
2) 따라서 다시 S0을 실행해야 한다. (이 때, 다음 명령어였던 if문을 실행하게 될 것이다)
이 때 만약 다음에 실행할 명령어 instr이 조건문인 경우에는, 그 조건문의 두 브랜치가 statisfiable한지 체크한다.
-> 두 브랜치 모두 satisfiable함을 확인했다.
3) 두 브랜치가 모두 statisfiable한 경우, state fork를 한다.
하나였던 state s0를 두개의 state로 만든다.
기존의 s0은 업데이트하여 path condition이 (a == 2b) 된다. 다음 실행할 명령어는 if (x==y+10)이 된다.
두 번째 fork된 s1은 path condition이 (a != 2b) 이 된다. 따라서 해당 조건문 밖으로 빠지게 되어 프로그램 종료지점에 도달했으므로 halt이다.
4) s0를 다시 선택했다고 가정하자.
이 때 만약 다음에 실행할 명령어 instr이 조건문인 경우에는, 그 조건문의 두 브랜치가 statisfiable한지 체크한다.
if x == y+10에 대해서,
1. a == 2b ∩ a == b + 10이 satisfiable 한가?
2. a == 2b ∩ a != b + 10이 satisfiable 한가?
-> 모두 satisfiable 하다.
5) state fork를 한다.
s0은 true branch로 가게 되면 error 지점에 도달한다.
s2는 false branch로 가게 되면 프로그램 종료지점에 도달하므로 halt가 된다.
6) state 3개 중에 s0를 선택했다고 가정하자.
s0에서 error 지점을 실행하게 된다.
그리고 error 지점 이후에는 조건문이 아니니까 fork 등을 고려하지 않고 다음 줄로 넘어가게 된다.
다음 줄은 프로그램 종료 지점으로, halt가 된다.
7) SMT 에 path condition 전달 후 testcase generate
프로그램의 끝 지점에 도달했으므로 더 이상 업데이트할 path condition이 없는 상태다.
따라서, 이 condition을 SMT Solver에게 전달하여 satisfiable한지 체크한다. 그리고 satisfiable 하다면, 해를 리턴한다.
8) 해당 해를 리턴했으므로, s0은 state에서 사라진다.
9) s1도 path condition을 SMT에 전달하여, testcase generate
10) s1도 state 집합에서 사라진다.
11) s2를 선택하여 SMT에 path condition 전달하여, testcase generate
🌳 EGT Algorithm
1: 초기 state를 가진 집합 S를 정의한다.
3: state 집합에서 state를 선택한다.
4: state를 선택한 후, 전체 집합에서 제거한다.
5: 해당 state의 instruction를 실행한다. 그러면 isntruction, store, pathcondition이 업데이트된다.
6: 다음 명령어가 if else statement인 경우
7: 기존 path condition ∩ if문 true 브랜치 조건이 satisfiable하면, instruction1을 업데이트한다. path condition도 업데이트된다
8: 기존 path condition ∩ if문 false 브랜치 조건이 satisfiable하면, instruction2을 업데이트한다. path condition도 업데이트된다
9: 만약 다음 명령어가 halt 라면
10: 해당 condition을 통해서 testcase v를 generate한다.
11: 이 과정을 반복해서 state 집합이 공집합이 될 때까지 반복한다.
