Trace Typing: An Approach for Evaluating Retrofitted Type Systems
Trace Typing: An Approach for Evaluating Retrofitted Type Systems
复制标题
跟踪类型：一种评估改装类型系统的方法
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Koushik Sen
中科院分区：
文献类型：
--
作者：
Esben Andreasen;Colin S. Gordon;S. Chandra;Manu Sridharan;F. Tip;Koushik Sen
近年来，人们对将类型系统改造到动态类型的编程语言上的兴趣越来越大，以提高类型安全性，程序员生产率或性能。在这种情况下，类型系统开发人员必须在不承担某些编码模式以使类型系统保持简单或以额外的复杂性和精力为代价之间取得微妙的平衡。到目前为止，设计翻新类型系统的过程在很大程度上是临时的，因为评估现有代码的大物体上类型系统的多种变化是一项重要的工作。
我们提出跟踪键入：用于自动和定量评估大型代码库中翻新类型系统的变化的框架。跟踪键入方法涉及收集程序执行的痕迹，以痕迹中发生的变量和表达式的实例来推断类型，并根据反映源级类型系统设计空间中特定（组合）选择的合并策略合并类型。
我们通过多个实验评估了迹线键入。我们比较了在JavaScript上翻新的几种类型系统变体，在每种情况下，在每种情况下都在五万行JavaScript代码的套件上测量了类型错误的程序位置数量。我们还使用跟踪键入来验证和指导新的翻新类型系统的设计，该系统为JavaScript对象执行固定的对象布局。最后，我们利用了通过跟踪键入计算的类型来自动识别标签测试---精炼类型的动态检查 - 并检查了所识别的测试的多样性。
Recent years have seen growing interest in the retrofitting of type systems onto dynamically-typed programming languages, in order to improve type safety, programmer productivity, or performance. In such cases, type system developers must strike a delicate balance between disallowing certain coding patterns to keep the type system simple, or including them at the expense of additional complexity and effort. Thus far, the process for designing retrofitted type systems has been largely ad hoc, because evaluating multiple variations of a type system on large bodies of existing code is a significant undertaking.
We present trace typing: a framework for automatically and quantitatively evaluating variations of a retrofitted type system on large code bases. The trace typing approach involves gathering traces of program executions, inferring types for instances of variables and expressions occurring in a trace, and merging types according to merge strategies that reflect specific (combinations of) choices in the source-level type system design space.
We evaluated trace typing through several experiments. We compared several variations of type systems retrofitted onto JavaScript, measuring the number of program locations with type errors in each case on a suite of over fifty thousand lines of JavaScript code. We also used trace typing to validate and guide the design of a new retrofitted type system that enforces fixed object layout for JavaScript objects. Finally, we leveraged the types computed by trace typing to automatically identify tag tests --- dynamic checks that refine a type --- and examined the variety of tests identified.