论文下载:https://www.comp.nus.edu.sg/~joxan/papers/testing.pdf
ABSTRACT && INTRODUCTION
- 优化concolic execution的工作
- 当前的优化方法:启发式搜索策略、简易功能缓存、动静结合
- 作者提出搜索剪枝的方法:如果一个test遍历了一条路径,当下次另一test遇到相同情况的时候就可实现剪枝
- concolic execution(我是传送门)
RUNNING EXAMPLE
- 假设两个read()都非0,程序执行到l_8,路径可达,没有bug
- 反转l_6的条件,发现不可达,所以l_6这个subtree搜索完成,条件是s <=3(这个例子有点违和,在符号执行里面放bug不可达)
- 回溯,到l_4,发现分支l’_6,但条件是s < = 1,满足刚才l_6的条件,所以不用再搜索
- l_4搜索完全,条件是s < = 1
- …
ALGORITHM
- 每当产生一条新的路径,就检查是否被搜索过
- 如果没有被搜索过,就执行concolic execution,但会记录每个分支的搜索条件和情况,即SymExec这个过程
- SymExec包括回溯的过程,对于回溯的搜索作了限定:每个program point只被搜索至多一次,当再次经过的时候,检查是否可以被剪枝,如果不行,放弃回溯
- 保证回溯是O(n)
Evaluation
- 4 programs from the ntdrivers-simplified category of SV-COMP’12
- 1000 – 2000 LOC
- 控制流复杂,有大量路径
Performance
- b明显说明回溯的作用
Subsumption
- 剪掉的路径数量百分比
Extra path-coverage
- 隐含福利,回溯的时候存在额外搜索,作为主搜索的补充
- (作者没有说明数据获取细节,但这个福利未免太大了)