分析数值特征程序族的决策树提升域（扩展版）
A Decision Tree Lifted Domain for Analyzing Program Families with Numerical Features (Extended Version)
摘要：
通过抽象解释的提升（基于族的）静态分析能够在一次运行中同时分析程序族的所有变体，而不显式地生成任何变体。底层提升分析域的元素是元组，每个变体维护一个属性。尽管如此，元组中的显式属性枚举（针对所有变体逐个）会立即产生组合爆炸。这是特别明显的情况下，程序的家庭，除了布尔功能，还包含数值功能与大域，从而承认天文配置空间。有效的提升分析的关键是正确处理语言的可变性特定结构（例如，基于功能的运行时测试和#if指令）。在这项工作中，我们引入了一个新的符号表示的提升抽象域，可以有效地分析程序族的数值特征。这使得与不同变体相对应的属性元素之间的共享显式地成为可能。新的提升域的元素是基于约束的决策树，其中决策节点被标记有在数值特征上定义的线性约束，并且叶节点属于现有的单个程序分析域。为了说明这种表示的潜力，我们实现了一个实验性的提升静态分析器，称为SPLNUM^2Analyzer，用于推断C程序的不变量。它使用现有的数值域（例如，间隔、八边形、多面体）作为参数。基于SV-COMP和BusyBox的基准测试结果表明，本文提出的基于决策树的方法是有效的，并且优于基于元组的方法，后者是基于抽象解释的基线提升分析。
英文摘要：
Lifted (family-based) static analysis by abstract interpretation is capable of analyzing all variants of a program family simultaneously, in a single run without generating any of the variants explicitly. The elements of the underlying lifted analysis domain are tuples, which maintain one property per variant. Still, explicit property enumeration in tuples, one by one for all variants, immediately yields combinatorial explosion. This is particularly apparent in the case of program families that, apart from Boolean features, contain also numerical features with big domains, thus admitting astronomic configuration spaces. The key for an efficient lifted analysis is proper handling of variability-specific constructs of the language (e.g., feature-based runtime tests and #if directives). In this work, we introduce a new symbolic representation of the lifted abstract domain that can efficiently analyze program families with numerical features. This makes sharing between property elements corresponding to different variants explicitly possible. The elements of the new lifted domain are constraint-based decision trees, where decision nodes are labeled with linear constraints defined over numerical features and the leaf nodes belong to an existing single-program analysis domain. To illustrate the potential of this representation, we have implemented an experimental lifted static analyzer, called SPLNUM^2Analyzer, for inferring invariants of C programs. It uses existing numerical domains (e.g., intervals, octagons, polyhedra) from the APRON library as parameters. An empirical evaluation on benchmarks from SV-COMP and BusyBox yields promising preliminary results indicating that our decision trees-based approach is effective and outperforms the tuple-based approach, which is used as a baseline lifted analysis based on abstract interpretation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
