Dynamically Inferring Data Preconditions over Predicates by Tree LearningSriram Sankaranarayanan Swarat Chaudhuri, Franjo Ivancic, and Aarti Gupta |
|
We present a technique to learn data preconditions for procedures
written in an imperative programming language. Given a procedure
and an 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
provided by the user and/or automatically produced from the program
description using heuristics. The enumeration of truth assignments
is performed by using randomized SAT solvers with a theory
satisfiability checker capable of generating unsatisfiable cores.
For each combination of truth values chosen by our sampler, the corresponding set of test cases are generated and exectued. Based on the result of the execution, the truth combination is classified as safe or buggy. Finally, a decision tree classifier is used to generate a boolean formula over the input predicates that explains the truth table generated in this process. The resulting boolean formula forms a precondition for the function under test.
We apply our techniques on a wide variety of functions, including
functions in the standard C library. Our experiments show that the
proposed learning technique is quite robust. In many cases, it
successfully learns a precondition that captures a safe and
permissive calling environment required for the execution of the
function.
|
| Intl. Symp. on Software Testing and Analysis (ISSTA'08), pp. 295-306, ACM Press. |
| Copyright (C) Association For Computer Machinery (ACM). See first page of paper for copyright notice. Copy has been made available online for personal use only. Do not redistribute without permission. |