Classifying Bugs with Interpolants
We present an approach to the classification of error messages in the context of static checking in the style of ESC/Java. The idea is to compute a semantics-based signature for each error message and then group together error messages with the same signa
- PDF / 902,192 Bytes
- 18 Pages / 439.37 x 666.142 pts Page_size
- 77 Downloads / 221 Views
University of Freiburg, Freiburg im Breisgau, Germany 2 SRI International, Menlo Park, USA [email protected] 3 New York University, New York, USA
Abstract. We present an approach to the classification of error messages in the context of static checking in the style of ESC/Java. The idea is to compute a semantics-based signature for each error message and then group together error messages with the same signature. The approach aims at exploiting modern verification techniques based on, e.g., Craig interpolation in order to generate small but significant signatures. We have implemented the approach and applied it to three benchmark sets (from Apache Ant, Apache Cassandra, and our own tool). Our experiments indicate an interesting practical potential. More than half of the considered error messages (for procedures with more than just one error message) can be grouped together with another error message.
1
Introduction
The classification of error messages, bug reports, exception warnings, etc. is an active research topic [1,3,5,13,16,25,30]. The underlying motivation is that grouping related error messages together will help with their analysis. The problem of classification is to infer what error messages are related (and, in what sense). In this paper, we address the problem of classification in the context of static checking of sequential procedural programs in the style of ESC/Java, as in [4,15,21]. Although in this context error messages may refer to an error in the specification rather than the code, the same motivation applies. The error messages may come in batches of, say, thousands, and they have to be analyzed, if only to debug the specification. In the context of static checking, it seems natural to explore whether concepts and techniques from semantics and verification can be put to use for the classification of error messages. In this paper, we present an approach to semantics-based classification of error messages which come in the form of a sequence of statements along with a witness; a witness here is an initial state from which the execution of the sequence of statements leads to the violation of a specified assertion. As in verification, semantics here is used to abstract away from syntactical details. For example, we can abstract a statement (or a sequence of statements) by its summary in the form of a pre-and postcondition pair. c Springer International Publishing Switzerland 2016 B.K. Aichernig and C.A. Furia (Eds.): TAP 2016, LNCS 9762, pp. 151–168, 2016. DOI: 10.1007/978-3-319-41135-4 9
152
A. Podelski et al.
The idea behind the approach is to compute a semantics-based signature for each of the error messages and then group together error messages with the same signature. More concretely, we associate each error message with a new verification problem. We apply a verification engine to infer a proof in the form of Hoare triples. We remove the invariant-type Hoare triples (of the form {F } st {F }, expressing that an assertion F is invariant under a statement st). We take the remaining change-type
Data Loading...
