GSE

这篇paper的完整题目是 Generalized Symbolic Execution for Model Checking and Testing

下载链接

摘要

本文给出新的symbolic execution模型，用来自动化的检查软件。两个步骤：

• 1、instrument程序
• 2、使用新算法（lazy initialization）操作数组、树以及concurrency。

Motivation

当代的软件系统需要极度可靠地处理concurrency和复杂数据结构，比如动态生成的树、链表

之前常用的方法是testing和model checking，但是testing是人工测试，很难测concurrency。Model checking会出现路径爆炸，所以需要非常有限的环境和输入值。

1、intro

本文使用symbolic execution自动生成测试用例，对concurrent程序进行model checking时可以无限制输入复杂结构。减少路径爆炸。

两个步骤

• 1) instrument程序
  • instrument之后提供给标准model checker
  • 这样就不用为每一类程序定制一个checker
  • model checker自动化的探索different program heap configurations，并且manipulating logical formulae on program data values？？？
• 2) lazy initialization
  • 以“按需”为原则对变量进行初始化
  • 无需预先限制输入大小

• 自动化生成“非同构(non-isomorphic)”测试用例？
• 使用 Java PathFinder 进行 model checking
• 使用 Omega library 作为 decision procedure
• 使用 Korat 进行 program instrumentation

2、实例程序

编辑链表前两个node的排序。其中swapNode破坏性的改变输入链表的结构。

class Node {
	int elem;
	Node next;
}

Node swapNode() {
	if(this.next != null) {
		if(this.elem > next.elem){
			Node t = this.next;
			this.next = t.next;
			t.next = this;
			return t;
		}	// 保证 root <= root.next
		return this;
	}
}

• 使用prototype implementation (Section 6)来分析7种symbolic execution
  • 其中4种情况对应root.next.next的值
  • 每种情况包含一组Input list + Constraint
    • 每种情况(partition)被称为是“同构(isomorphism)”的
  • 问号“？”和云表示未访问
  • 可以设置相应的precondition，比如“链表不许有cycle”

3、背景：Symbolic execution

• 使用符号值，而不是具体值，作为input
  • 用符号表示程序中的变量
• 符号执行程序的状态(state)包括
  • （符号化的）程序变量
  • path condition (PC)
    • 表示限定条件累积量
    • 是一个boolean表达式
  • program counter
    • 下一个要被执行的语句
• 通过symbolic execution tree可以判定哪些语句是“无法到达”的

4、算法

本节关注单线程的程序

4.1 Lazy initialization

• 程序开始执行前，所有变量都没初始化
• 只有被执行到的时候才被初始化
  • 这使得input不需要被预先限定

抽象例子

• 为了执行classC中的methodm
  • 算法先创造一个C的实例objecto，其中o的值都没初始化
  • 之后程序调用o.m()
• 除了uninitialized的部分外，其他过程与静态的symbolic execution相同。

if ( f is uninitialized ) {
	if ( f is reference field of type T ) {
		nondeterministically initialize f to
			1. null
			2. a new object of class T (with uninitialized field values)
			3. an object created during a prior initialization of a field of type T
		if ( method precondition is violated )
		backtrack();
	}
	if ( f is primitive (or string) field )
		initialize f to a new symbolic value of appropriate type
}

• 当程序遇到 uninitialized 值
  • 对于 reference field，执行recursion：
    • 试试null
    • 试试new
    • 试试各种old （检查是否满足precondition，比如链表cycle）
  • 对于 primitive field
    • initialize 为新符号
• 当程序遇到 primitive field 的 branching condition
  • 执行传统的 symbolic execution

执行完程序后，使用 PC 来生成相应的input值/范围

4.2 实例

• 每个node表示一个state
  • 记录了heap的状态和累积的PC值
• 连接两个node的过程称为transition
  • 有数字N：表示执行程序的第N条语句
    • 可能是1对多 比如if带来的 path condition
  • 没数字：表示进行 lazy initialization
    • 图中X号表示不被 precondition 允许，abort path 比如“链表不允许出现 cycle”
• reference field 只有在“被读取”的时候才会被 initialized

5、Framework

• 使用 Korat 进行 program instrumentation
• 使用 Java PathFinder 进行 model checking
• 使用 Omega library 作为 decision procedure

• 首先对原程序进行 source-to-source instrumentation
  • 这可以帮助任一 model checker 对程序进行 symbolic execution 的时候，进行 backtracking 和 nondeterministic choice 的操作
  • 添加 pre- 和 post-condition checking
• 然后是 section 4 里面描述的算法
• 之后用 model checker 探索上面生成的 symbolic execution tree
  • 检查每一个 state
    • 包括 heap configuration，path condition on primitive fields 和 thread scheduling
• 同时对每一个更新过的 path condition 进行检查
  • 使用 Omega library 作为 decision procedure
  • 如果不满足条件，则 backtrack

本框架支持多种程序功能：多线程、loop、recursion、method调用。但是，这首先需要 model checker 支持测试这些功能。

6、实现细节

本节介绍 instrumentation、JPF 以及 对本方法的讨论

6.1 instrumentation

这一节的操作没有实现自动化，而且细节给的太少了，很艰涩，基本没看懂

6.3 局限

• 本工具分析的方式比较保守，只能根据预先给定的precondition进行排除，所以有时无法排除特定的 无法到达的path
• 无法分析 array

Questions

• predicate
• isomorph
• 6、instrument

• Previous
  Daikon安装
• Next
  DART