SHErrLoc
SHErrLoc
复制标题
谢尔洛克
DOI：
--
复制
发表时间：
2017
影响因子：
1.3
通讯作者：
S. Jones
中科院分区：
文献类型：
--
作者：
Danfeng Zhang;A. Myers;Dimitrios Vytiniotis;S. Jones
我们介绍了一种通用的方法来定位程序员的错误，检测到的静态分析。程序分析是用一种通用的约束语言来表示的，这种语言的功能足以对类型检查、信息流分析、流分析和指向分析进行建模。程序分析中的错误会导致不可满足的约束。给定一个不可满足的约束系统，分析可满足和不可满足的约束，以确定最有可能导致不可满足性的程序表达式。不同的错误解释的可能性是在假设程序员的代码大多数是正确的情况下评估的，因此选择最简单的解释，遵循贝叶斯原理。对于依赖于程序员声明的假设的分析，诊断还识别可能被忽略的假设。新的错误诊断方法已被实现为一个工具，称为SHErrLoc，这是适用于三个非常不同的程序分析，如类型推理的一个高度表达的类型系统实现的格拉斯哥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.