Toward General Diagnosis of Static Errors: Technical Report

Content replaced at author's request on 2013-12-17.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.This work was supported by two grants from the Office of Naval Research, N00014-09-1-0652 and N00014-13-1-0089, by MURI grant FA9550-12-1-0400, by a grant from the National Science Foundation (CCF-09644909), and by a grant administered by the Air Force Research Laboratory