Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Francesco Logozzo
We consider the problem of automatic precondition inference. We argue that the common notion of sufficient precondition inference (i.e., under which precondition is the program correct?) imposes too large a burden on callers, and hence it is unfit for automatic program analysis. Therefore, we define the problem of necessary precondition inference (i.e., under which precondition, if violated, will the program always be incorrect?). We designed and implemented several new abstract interpretation-based analyses to infer atomic, disjunctive, universally and existentially quantified necessary preconditions.
We experimentally validated the analyses on large scale industrial code. For unannotated code, the inference algorithms find necessary preconditions for almost 64% of methods which contained warnings. In 27% of these cases the inferred preconditions were also sufficient, meaning all warnings within the method body disappeared. For annotated code, the inference algorithms find necessary preconditions for over 68% of methods with warnings. In almost 50% of these cases the preconditions were also sufficient. Overall, the precision improvement obtained by precondition inference (counted as the additional number of methods with no warnings) ranged between 9% and 21%.
|Published in||in Proceedings of the 14th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13)|
Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Mike Barnett. An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts, ACM SIGPLAN, 23 October 2012.
Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett. A Semantic Integrated Development Environment, ACM SIGPLAN, October 2012.
Mike Barnett, Manuel Fahndrich, and Francesco Logozzo. Embedded Contract Languages, Association for Computing Machinery, Inc., March 2010.
Patrick Cousot, Radhia Cousot, and Francesco Logozzo. Contract Precondition Inference from Intermittent Assertions on Collections, Microsoft Research, September 2010.
Mehdi Bouaziz, Francesco Logozzo, and Manuel Fahndrich. Inference of Necessary Field Conditions with Abstract Interpretation , Springer, December 2012.
Francesco Logozzo and Tom Ball. Modular and Verified Automatic Program Repair, ACM SIGPLAN, 23 October 2012.