论文标题
自动有效的可变性 - 功能程序的解除
Automatic and Efficient Variability-Aware Lifting of Functional Programs
论文作者
论文摘要
软件分析是一种计算机程序，该程序将软件产品的某种表示形式表示为输入，并生成有关该产品作为输出的一些有用信息。软件产品线包含\ emph {许多}软件产品变体，因此可以单独应用现有的分析，而不是整个产品线。列举所有产品变体并一一分析它们通常是由于产品线特征的产品变体数量的组合爆炸而棘手。对几种软件分析（例如类型的检查器，模型检查器，数据流分析）进行了重新设计/重新实施以支持可变性。这通常需要大量的时间和精力，并且分析的可变性版本可能具有原始错误中不存在的新错误/错误。 给定一个基于PCF的功能语言编写的分析程序，在本文中，我们提出了将其转换为语义上等效的可变性分析的两种方法。一种轻量级的方法（称为\ emph {shallow lifting}）将分析程序包裹在变异性的版本中，探索其输入参数的所有组合。另一方面，深度提升是一种程序重写机制，其中输入程序的句法结构被重写为其可变性 - 意识到的对应物。在构图上，这会导致一个有效的程序在语义上等同于输入程序Modulo的可变性。我们介绍了功能程序提升的正确性标准，以及我们程序转换的正确性证明草图。我们在应用于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.
