Type-guided worst-case input generation
Type-guided worst-case input generation
复制标题
DOI：
10.1145/3290326
复制
发表时间：
2019-01
影响因子：
--
通讯作者：
Di Wang;Jan Hoffmann
中科院分区：
文献类型：
--
作者：
Di Wang;Jan Hoffmann
本文介绍了一种针对功能程序的类型引导最差输入生成的新技术。该技术基于自动摊销资源分析（AARA），这是一种基于类型的技术，用于在功能的资源使用情况下得出符号界限。最差的输入生成是通过一种算法来执行的，该算法以输入功能，其资源注销的类型导数以及描述要生成的输入的形状和大小的骨架。如果成功，该算法填充整数，布尔值和数据结构，以产生骨架给出的形状值。稳健定理指出，生成的值在具有骨架形状的功能的所有参数中表现出最高的成本。此成本完全对应于类型推导建立的最坏情况结合。这样，算法的成功完成就证明了给定形状的输入的界限很紧。相应地，事实证明，相对完整的定理表明，只有当派生的最坏情况界限紧密时，算法才能成功。该定理是相对的，因为它取决于解决约束解决的决策过程。为具有线性资源界限的简单一阶语言提供了技术开发。但是，该技术缩放到并已针对资源意识ML实施，这是针对具有高阶函数，用户定义的数据类型和多项式界限的OCAML片段的AARA实现的。实验表明，该技术有效地工作，并可以通过数百个整数来得出最坏情况的输入，以分类算法，对搜索树的操作以及插入哈希表。
This paper presents a novel technique for type-guided worst-case input generation for functional programs. The technique builds on automatic amortized resource analysis (AARA), a type-based technique for deriving symbolic bounds on the resource usage of functions. Worst-case input generation is performed by an algorithm that takes as input a function, its resource-annotated type derivation in AARA, and a skeleton that describes the shape and size of the input that is to be generated. If successful, the algorithm fills in integers, booleans, and data structures to produce a value of the shape given by the skeleton. The soundness theorem states that the generated value exhibits the highest cost among all arguments of the functions that have the shape of the skeleton. This cost corresponds exactly to the worst-case bound that is established by the type derivation. In this way, a successful completion of the algorithm proves that the bound is tight for inputs of the given shape. Correspondingly, a relative completeness theorem is proved to show that the algorithm succeeds if and only if the derived worst-case bound is tight. The theorem is relative because it depends on a decision procedure for constraint solving. The technical development is presented for a simple first-order language with linear resource bounds. However, the technique scales to and has been implemented for Resource Aware ML, an implementation of AARA for a fragment of OCaml with higher-order functions, user-defined data types, and types for polynomial bounds. Experiments demonstrate that the technique works effectively and can derive worst-case inputs with hundreds of integers for sorting algorithms, operations on search trees, and insertions into hash tables.