Lightweight Data-flow Analysis for Execution-driven Constraint Solving

Presentation on theme: "Lightweight Data-flow Analysis for Execution-driven Constraint Solving"— Presentation transcript:

1 Lightweight Data-flow Analysis for Execution-driven Constraint Solving
Junaid Haroon Siddiqui Darko Marinov Sarfraz Khurshid

2 背景 Constraint-based testing Key challenge-valid inputs generation
execution-driven solving Wasteful Repeated predicate execution, predicate result

3 贡献 Lightweight static data-flow analysis for constraint solving
Multi-value comparisons Implementation Evaluation

4 Traditional Korat 1，建立一个要测试的初始结构，执行repok算法；
2，当repok算法执行完后，将field domain中最后一个输入域中的数值改成一个新数值，然后重新执行repok算法； 3，如果最后一个field domain中的数值没有更多的数值，则到前一个field domain中； 4，一直所有的field domain中的数值都执行完。

5

6 Koratmulti: multi-value comparisons
A multi-value comparison compares a given value against all values in the field domain of a field not yet accessed in the repOk predicate. If a field has already been accessed, the given value can only be compared against its ssigned value and no multi-value comparison can take place.

7 Koratmulti: multi-value comparisons
条件： 至少有一个可能的结果能够决定哪个repOk predicate能够返回。

8 Koratmulti: multi-value comparisons

9 Koratmulti: multi-value comparisons

10 Technique 主要思路： 对candidate进行判断是否为marked，如果是marked，则不需要执行repOk， repOk的结果就可以知道。 主要方法： 结合Data-flow analysis和Multi-value comparisons，在Multi-value comparisons中使用数据流分析方法，然后用Multi-value comparisons将candidate分为marked和unmarked。

11

12 1,followUseChain the accessed value is directly used as one argument of a comparison. 2,br The comparison is used inside an if statement. 3,ret determines if a constant is returned.

13

14 Evaloution 1,the number of repOk executions
2,the time it takes to generate valid inputs.

15 Evaloution

16