函数程序的自动高效可变性提升
Automatic and Efficient Variability-Aware Lifting of Functional Programs
摘要：
软件分析是一种计算机程序，它将软件产品的某些表示作为输入，并产生有关该产品的某些有用信息作为输出。软件产品线包含\emph{many}软件产品变体，因此现有分析可单独应用于每个产品变体，但不能应用于整个产品线。枚举所有的产品变体，并分析他们一个接一个通常是棘手的，由于组合爆炸的产品变体的数量相对于产品线功能。一些软件分析（例如，类型检查器、模型检查器、数据流分析）已经被重新设计/重新实现以支持可变性。这通常需要大量的时间和精力，并且可变性感知版本的分析可能会有新的错误/bug，这些错误/bug在原始版本中不存在。给出了一个基于PCF的函数式语言编写的分析程序，在本文中，我们提出了两种方法将其转换（提升）为语义等效的变量感知分析。轻量级方法（称为\emph{shallow lifting}）将分析程序包装成可变性感知版本，探索其输入参数的所有组合。另一方面，深度提升是一种程序重写机制，其中输入程序的语法结构被重写为它们的可变性感知对应物。在组成上，这导致了一个有效的程序语义等价于输入程序，模可变性。我们提出的正确性标准的功能程序提升，连同正确性证明我们的程序转换草图。我们评估我们的方法上的一组程序分析适用于BusyBox C语言产品线。
英文摘要：
A software analysis is a computer program that takes some representation of a software product as input and produces some useful information about that product as output. A software product line encompasses \emph{many} software product variants, and thus existing analyses can be applied to each of the product variations individually, but not to the entire product line as a whole. Enumerating all product variants and analyzing them one by one is usually intractable due to the combinatorial explosion of the number of product variants with respect to product line features. Several software analyses (e.g., type checkers, model checkers, data flow analyses) have been redesigned/re-implemented to support variability. This usually requires a lot of time and effort, and the variability-aware version of the analysis might have new errors/bugs that do not exist in the original one. Given an analysis program written in a functional language based on PCF, in this paper we present two approaches to transforming (lifting) it into a semantically equivalent variability-aware analysis. A light-weight approach (referred to as \emph{shallow lifting}) wraps the analysis program into a variability-aware version, exploring all combinations of its input arguments. Deep lifting, on the other hand, is a program rewriting mechanism where the syntactic constructs of the input program are rewritten into their variability-aware counterparts. Compositionally this results in an efficient program semantically equivalent to the input program, modulo variability. We present the correctness criteria for functional program lifting, together with correctness proof sketches of our program transformations. We evaluate our approach on a set of program analyses applied to the BusyBox C-language product line.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
