Danfeng Zhang and Andrew C. Myers
Department of Computer Science, Cornell University
We introduce a general way to locate program errors that are detected by type systems and other program analyses. The program analysis is expressed in a constraint language in which program errors manifest as unsatisfiable constraints. Given an unsatisfiable system of constraints, both satisfiable and unsatisfiable constraints are analyzed, to identify the program expressions most likely to be the cause of unsatisfiability. The likelihood of different error explanations is evaluated under the assumption that the programmer's code is mostly correct, so the simplest error explanations are chosen, following Bayesian principles. For analyses that rely on programmer-stated assumptions, the diagnosis also identifies assumptions likely to have been omitted. The new error diagnosis approach has been implemented for two very different program analyses: type inference in OCaml and information flow checking in Jif. The effectiveness of the approach is evaluated using previously collected programs containing errors. The results show that the general technique identifies the location of program errors significantly more accurately than do existing compilers and other tools.
[ Full paper | TR ]