SHErrLoc: A Static Holistic Error Locator
SHErrLoc: A Static Holistic Error Locator
复制标题
SHErrLoc：静态整体错误定位器
DOI：
10.1145/3121137
复制
发表时间：
2017
影响因子：
1.3
通讯作者：
Peyton-Jones, Simon
中科院分区：
文献类型：
--
作者：
Zhang, Danfeng;Myers, Andrew C.;Vytiniotis, Dimitrios;Peyton-Jones, Simon
我们介绍了一种通用的方法来定位通过静态分析检测到的程序员错误。程序分析用通用约束语言表示，该语言足够强大，可以对类型检查、信息流分析、数据流分析和指向分析进行建模。程序分析中的错误会导致不可满足的约束。给定一个不可满足的约束系统，分析可满足和不可满足的约束，以确定最有可能是不可满足的原因的程序表达式。不同错误解释的可能性是在程序员的代码大部分是正确的假设下进行评估的，因此遵循贝叶斯原则选择最简单的解释。对于依赖于程序员陈述的假设的分析，诊断还确定了可能已被省略的假设。新的错误诊断方法已经被实现为一个名为SHErrLoc的工具，它被应用于三个非常不同的程序分析，例如由Glasgow Haskell编译器实现的高度表达类型系统的类型推理-包括类型类、通用代数数据类型(GADT)和类型族。使用先前收集的包含错误的程序来评估该方法的有效性。结果表明，与现有的编译器和其他工具相比，SHErrLoc一致地更准确地识别程序员错误的位置，而不需要任何特定语言的启发式方法。
We introduce a general way to locate programmer mistakes that are detected by static analyses. The program analysis is expressed in a general constraint language that is powerful enough to model type checking, information flow analysis, dataflow analysis, and points-to analysis. Mistakes in program analysis result in 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 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 as a tool called SHErrLoc, which is applied to three very different program analyses, such as type inference for a highly expressive type system implemented by the Glasgow Haskell Compiler—including type classes, Generalized Algebraic Data Types (GADTs), and type families. The effectiveness of the approach is evaluated using previously collected programs containing errors. The results show that when compared to existing compilers and other tools, SHErrLoc consistently identifies the location of programmer errors significantly more accurately, without any language-specific heuristics.