Dynamic inference of likely data preconditions over predicates by tree learning
Dynamic inference of likely data preconditions over predicates by tree learning
复制标题
通过树学习动态推断谓词上可能的数据先决条件
DOI：
10.1145/1390630.1390666
复制
发表时间：
2008
影响因子：
0.8
通讯作者：
Aarti Gupta
中科院分区：
文献类型：
--
作者：
S. Sankaranarayanan;Swarat Chaudhuri;Franjo Ivancic;Aarti Gupta
我们提出了一种技术来推断可能的数据先决条件forprocedures写在一个命令式编程语言。给定一个过程和一组谓词在其输入，我们的技术列举了不同的真值分配的谓词，从每个可行的真值分配派生测试用例。谓词本身是使用简单的语法自动派生的。真值赋值的枚举是使用命题SAT求解器以及能够生成不可满足核的理论可满足性检查器沿着执行的。
对于每个真值的分配，生成并执行一组相应的测试用例。基于执行的结果，真值分配被分类为安全的或有缺陷的。最后，使用决策树分类器在输入谓词上生成布尔公式，该布尔公式解释从测试用例获得的数据。实际上，所得到的布尔公式是所考虑的程序的可能的数据先决条件。
我们将我们的技术应用于标准C库中的各种函数。我们的实验表明，该技术是相当强大的。在大多数情况下，它成功地学习了一个先决条件，捕获了一个安全和宽松的呼叫环境。
We present a technique to infer likely data preconditions forprocedures written in an imperative programming language. Given a procedure and a set of predicates over its inputs, our technique enumerates different truth assignments to the predicates, deriving test cases from each feasible truth assignment. The predicates themselves are derived automatically using simple heuristics. The enumeration of truth assignments is performed using a propositional SAT solver along with a theory satisfiability checker capable of generating unsatisfiable cores.
For each assignment of truth values, a corresponding set of test cases are generated and executed. Based on the result of the execution, the truth assignment is classified as being safe or buggy. Finally, a decision tree classifier is used to generate a Boolean formula over the input predicates that explains the data obtained from the test cases. The resulting Boolean formula is, in effect, a likely data precondition for the procedure under consideration.
We apply our techniques on a wide variety of functions from the standard C library. Our experiments show that the proposed technique is quite robust. For most cases, it successfully learns a precondition that captures a safe and permissive calling environment.