SHErrLoc: Static Holistic Error Locator

SHErrLoc is a new, general approach to locate programmer mistakes that are detected by static program analyses, such as ML type inference, information flow analysis and dataflow analysis.

The SHErrLoc tool analyzes a system of constraints in a constraint language that is expressive enough for a large class of static program analyses, including the highly expressive type system implemented by the Glasgow Haskell Compiler (GHC) (with type classes, GADTs, and type families). Both satisfiable and unsatisfiable constraints are analyzed to identify the most likely cause of errors. Based on Bayesian grounds, the likelihood of different error explanations is evaluated via two general heuristics:

For example, the EasyOCaml++ tool generates constraints in the constraint language format from OCaml programs. The SHErrLoc tool then analyzes these application-agnostic constraints to locate the most likely programmer mistakes, as illustrate in the overview graph. Please try our demo for OCaml.

Less compiler modifications are required for diagnosing Haskell type errors, since existing compilers, such as GHC, already generate type-checking constraints. A light-weight constraint translator then feeds these constraints to the general SHErrLoc tool, in order to better localize programmer mistakes. Please try our demo for Haskell.

Evaluation on very different program analyses, type inference in OCaml and Haskell, as well as information flow analysis in Jif, suggests that this general approach identifies error locations significantly more accurately than existing tools.

Downloads

The SHErrLoc tool takes a constraint file describing program analysis, and diagnoses the most likely cause of errors detected by the static program analysis. The latest version of SHErrLoc, as described in our PLDI'15 paper, is available at the SHErrLoc GitHub repository.

SHErrLoc GitHub repository

The version used in our POPL'14 paper is packaged here:

EasyOCaml++, an extension to EasyOCaml, generates constraints describing OCaml type inference.

Related publications

Project members

Support

The development of SHErrLoc has been supported by 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.