ACM通信

研究突出了

静态分析中的未知推理

伊丝·迪利格、托马斯·迪利格、亚历克斯·艾肯著
ACM通讯，2010年8月，Vol. 53 No. 8, 115-123页
10.1145/1787234.1787259
评论

静态程序分析技术在分析时无法知道某些值，例如用户输入的值或网络状态。虽然需要将这些未知值视为程序执行环境做出的不确定性选择，但仍然有可能收集到关于这些静态未知值可能或必须如何影响计算的非常有用的信息。我们给出了一种将这种不确定性选择与具有表达性的静态分析相结合的方法。有趣的是，我们不能直接解决由此产生的递归约束，但我们给出了一个精确的方法来回答所有可能和必须的查询。我们通过实验证明，得到的解决形式在实践中是简洁的，使我们能够将该技术应用于非常大的程序，包括整个操作系统。

回到顶部

1.简介

防止软件错误是软件工程的核心挑战。解决这个问题的许多基于工具的方法大致可以分为两类。动态分析技术通过监视程序执行来发现属性特定的输入;标准测试是动态分析最常用的形式。相比之下,一个静态分析发现保存的属性所有可能的输入;一个声音只有在程序确实没有错误的情况下，静态分析才能得出一个程序是没有错误的结论。

与动态分析不同，声音静态分析的优势是不会漏掉任何潜在的错误，但不幸的是，没有免费的午餐:可靠性通常以报告为代价假阳性(例如，关于无错误代码的虚假警告)因为静态分析必须近似程序行为的某些方面。这种近似是不可避免的，因为即使分析程序行为的非常简单的属性也是不可确定的。因此，静态分析技术的一个关键挑战是通过报告尽可能少的误报来实现精度、可靠性和可伸缩性的令人满意的组合，同时仍然是可靠的，并可扩展到真实的系统。

获得满意精度的目标由于某些值在静态中是未知的这一事实而进一步复杂化:例如，如果一个程序向用户查询一个输入，这个输入对静态分析来说就会显示为一个不确定的环境选择。类似地，从网络接收任意数据的结果或读取操作系统状态的结果都是未知的，需要被分析视为不确定的环境选择。

即使在所有程序输入都已知的特殊情况下，静态分析仍然需要处理由于近似程序行为而产生的未知。静态分析不能简单地进行精确的程序模拟;即使程序没有终止，我们通常也要保证分析终止。因此，静态分析总是有一些不精确的内置。例如，由于列表、集合和树可能具有无限数量的元素，许多静态技术不能精确地建模数据结构的内容。从数据结构中读取元素被建模为返回数据结构的任何元素的非确定性选择。类似地，如果所选的程序抽象不能表示非线性算术，则“复杂”表达式的值，例如系数* a * b +大小，也可能需要被静态分析视为未知。

从这些未知的价值中可以获得什么有用的信息，如果有的话，这个问题在文献中没有太多讨论。我们的印象是，如果这个问题得到了充分的考虑，它就会作为一个工程细节留在执行中;至少，这是我们过去采取的方法。但有两个观察结果改变了我们的想法:首先，在静态分析程序时，未知值惊人地普遍存在;总是会调用没有经过分析建模的外部函数，以及丢失信息的近似函数。其次，根据我们的经验，处理未知值时做得不好的分析最终要么无法扩展，要么太不精确。由于这些原因，我们现在相信处理未知值的系统方法是表达性静态分析设计的第一阶问题。

我们首先非正式地概述一个非常简单，但不精确的方法来处理静态分析中的未知值。考虑下面的代码片段:

假设我们想要证明对每一个调用打开外部文件，只有一个匹配的调用文件关闭．如果要违反匹配的属性，则必须是输入是“y”在第2行，但是的值输入不是“y”4号线。由于输入的值是未知的，一种简单的方法是使用特殊的抽象常数*表示未知值。现在，程序可能有多个未知值的来源，所有这些来源都用*表示。因此，*不是一个特定的未知数，而是程序中所有未知数的集合。因此，谓词* =“y”(应读作:“y”等于由*)和*表示的值的某个元素“y”(应读作:“y”不等于用*)表示的某些值元素同时可满足。因此，程序路径在哪里输入等于“y”在第(2)行，但不等于“y”在第(4)行(或者相反)不能被排除，分析将错误地报告一个错误。

对未知值进行推理的更精确的替代方法是使用变量(称为选择变量)，代表一种单一但未知的价值。注意，这种引入选择变量的策略是对前一种方法的改进，因为两个不同的环境选择是由两个不同的选择变量建模的。因此，虽然一个选择变量可以表示任何值，但它不能同时表示两个不同的值。例如，如果我们为调用的结果的未知值引入choice变量get_user_input在第1行，描述失效条件的约束为= yY，这是无法满足的，建立了对打开外部文件调用文件关闭．其中的深刻见解是，选择变量的使用允许分析确定两个值何时产生于相同的环境选择，而不需要对它们的值施加任何限制。

虽然后一种策略允许更精确的推理，但它导致了两个困难，一个是理论上的，另一个是

更简单，但不那么精确的策略不会受到实际影响。考虑以下函数:^一个

假设我们想知道什么时候query_user返回真正的．的返回值get_user_input是静态未知;因此，它是由选择变量确定的。的变量feature_enabled，但是，绝对不是一个不确定的选择，因为它的值是由函数调用者决定的。我们代表feature_enabled由一个可观察到的变量，由该函数的调用者提供。在…的条件下query_user返回真正的(缩写T)在任何调用上下文中，则由约束给出:

公式如下:这个词=T捕获函数返回的数据真正的只有在feature_enabled是真正的此外，用户输入必须是“y”(词=“y”和C)行，否则它一定不是“n”(术语(=“n”)和行D)，行G上的递归调用必须返回真正的(项T/))。注意，因为函数是递归的，所以公式也是递归的。在任期内[T/]，替换[T/]表示在递归调用中，形式参数被实际参数取代真正的．最后，绑定。提醒我们这是一个选择变量。当方程展开进行代入时[T/]我们也必须对环境做出选择。我们可以做的最普遍的选择是用一个新的变量替换'，这表明我们不知道做出了什么选择，但它可能不同于后续递归调用的任何其他选择。因此,(T/)展开:

式(*)表示的是query_user返回真正的，递归定义意味着它不会立即有用。此外，由于[的重复展开，很容易看出不存在有限的非递归公式作为递归方程(*)的解。T/]引入了一个无限序列的新鲜选择变量'，"，'"，....因此，不总是可能给出一个有限的封闭形式的公式来描述程序属性保持的确切条件。

在实践方面，真正的程序有许多未知的来源;例如，假设我们不推断内存管理系统的内部状态，每次调用都要malloc在C程序中显示为返回的非确定性选择零或者新分配的内存。在实践中，选择变量的数量会随着程序的大小而迅速增长，这会压倒约束求解器，导致分析的可伸缩性很差。因此，当选择变量对证明属性没有必要时，避免跟踪它们是很重要的。

我们对理论和实际问题的解决方案只能在更大的背景下理解，即我们为什么要首先执行静态分析。选择变量允许我们创建程序与环境交互的精确模型，这很好，因为我们永远不知道程序的哪些部分是需要精确分析的，所以在模型中任何地方引入不必要的不精确都可能是灾难性的。但这个模型拥有的信息比回答我们关心的大多数个人问题所需要的更多;事实上，我们通常只对两种1比特的决策问题感兴趣，五月而且必须查询。如果一个人有兴趣证明一个程序没有做一些“坏”的事情(所谓的安全属性)，那么分析需要问一些可能的问题，比如“这个程序可能解引用NULL吗?”或者“这个程序可能引发异常吗?”另一方面，如果一个人有兴趣证明一个程序最终能做一些好的事情(所谓的活性属性)，那么分析就需要问一些必须的问题，比如“这个内存最终必须被释放吗?”

可以将问题表述为可满足性查询;如果一个表示坏事件发生的条件的公式是可满足的，那么程序不保证是无错误的。相反，必须问题自然地被表述为有效性查询:如果一个表示好事发生的条件的公式是无效的，那么程序可能会违反期望的属性。因此，要精确地回答关于程序的“可能”和“必须”问题，我们不一定需要解出描述属性的精确公式，而只需要解出保持可满足性(对于“可能”查询)或有效性(对于“必须”查询)的公式。

我们技术的关键思想是，虽然选择变量在产生它们的函数调用中增加了有用的精度，但函数的聚合行为可以精确地总结为仅用于回答可能和必须查询的可观察变量。给定程序的有限抽象，我们的技术首先生成递归方程组，相对于初始抽象是精确的，但包含选择变量。然后，我们从这个递归系统中剔除选择变量，得到仅对可观察变量的可满足和等价系统。在保证了句法替换下的可满足性和有效性之后，我们再通过标准不动点计算来求解这两个递归系统。最后的结果是括弧约束_数控，_SC对于每个初始方程，对应于封闭形式的最强必要条件和最弱充分条件。

我们通过实验证明，在实践中产生的括号约束很小，而且最令人惊讶的是，它不会随着程序的大小而增长，这使得我们的技术可以扩展到分析像整个Linux内核那样大的程序。我们还将这种技术用于在大型开源C应用程序中查找空解引用错误，并表明这种技术对于将误报的数量减少一个数量级是有用的。

回到顶部

2.从程序到约束

正如在第1节中提到的，静态分析操作程序的模型或抽象，而不是程序本身。在本文中，我们考虑了一个有限抽象族，其中每个变量都有一个抽象值C₁、……C_k．这些抽象值可以是任何固定的谓词集、类型状态、数据流值或任何选定的有限域。我们考虑一种具有抽象值的语言C₁、……C_k；虽然简单，但这种语言足以说明我们技术的主要思想:

表达式是真的,假的，抽象的价值观C_我，变量x，函数调用，条件表达式，let绑定和比较两个表达式。布尔值表达式可以使用标准的布尔连接词来组合，，,¬。在这种语言中，我们通过引用未绑定变量来建模未知值，按照惯例，未绑定变量在函数调用时选择一个不确定的值。因此，在函数体中出现的任何自由变量都是选择变量。注意，这种语言在条件语句中使用了一组具有表达性的谓词，因此某些程序属性所处的条件可能是非平凡的。

具体地说，在本文的其余部分中，我们将考虑程序属性五月给定函数返回常数(即抽象值)C_我?”和“必须给定函数返回常数C_我?”。因此，我们的目标是计算每个函数返回常数的约束条件C_我．这些限制的形式如下:

定义1(约束)。

符号年代在约束语言中是抽象值C_我，选择对应抽象值未知的变量，以及代表调用方提供的函数输入的可观察变量。因为每个函数的输入值f是由变量表示的，由分析产生的约束是多态的，即，可以在任何调用上下文中使用f．约束符号之间的等式(年代₁＝年代₂)，用替换约束变量[C_我/或约束的布尔组合。替换(C_我/约束变量是用来用实数代替形式的，回想一下选择变量的向量命名用的变量被替换为vector的新鲜选择变量在方程的每一次展开中。更正式一点，if。＝,那么:

这种重命名是必要的，既可以避免命名冲突，也可以在不同的递归调用上建模不同的环境选择。约束表示函数所处的条件f输入返回一个特定的抽象值C_我；我们通常对相应的约束变量进行索引_f、c为清晰。例如，如果只有两个抽象值C₁而且C₂方程

描述了函数f总是返回C₁,

描述了函数f返回C₁如果它的输入有抽象的值C₂反之亦然。最后一个例子，函数

未绑定变量在哪里y非确定性选择的模型描述如下:

注意，这两个约束是共享的;特别是，在任何解决方案中都必须是其中之一C₁或C₂，捕捉一个函数调用只返回一个值。

我们的目标是生成约束来表征给定函数返回抽象值的条件C_我．图1给出了上述语言的大多数约束推理规则;由于篇幅不足，将省略其余的规则，但它们都是所示规则的简单类比。在这些推理规则中，环境一个用约束语言将程序变量映射到变量。规则15证明判决在哪里b｛真的,假的}，描述约束条件在这个表达式下e计算结果为真正的或假在环境一个．规则6dash;11证明判断这就给出了表达式的约束条件e计算结果为C_我．最后，规则12构造方程组，给出(可能)相互递归的条件，在这些条件下，函数返回每个抽象值。^b

我们将简要地更详细地解释规则的一个子集。在规则3中，两个表达式e₁而且e₂当两者具有相同的抽象值时相等。规则8说如果在环境中一个，变量的抽象值x由约束变量表示，那么x具有抽象的价值C_我只有=C_我．规则11给出了函数调用的规则:如果是函数的输入f具有抽象的价值C_k约束条件下_k的约束条件f返回C_我是,然后f（e)评估C_我约束条件下．

例1。假设我们分析如下函数:

在哪里y模型环境选择和唯一抽象的值是C1而且C2．然后

是由推理规则计算出的方程。注意这个替换［C₁/］在公式中表示递归调用的参数f是C₁．

我们简要概述约束的语义。约束在标准四点点阵上用真的,假的，而且真的,假的,在那里是见面,加入,,¬真=假,¬假= true。给定一个赋值的选择变量，一个方程组的意义E是一系列近似的标准极限(E⁰), (E¹),…通过反复展开产生E。我们对最小不动点(所有变量的第一个近似值为)都感兴趣)和最大不动点(这里是第一个近似值)语义。的值在最小不动点语义(resp。在最大不动点)表示被分析程序的不终止。

2.1.简化为布尔约束

我们的主要技术结果是一个完整的方法，用于回答定义1的约束的可满足性(可能)和有效性(必须)查询。如第1节所述，该算法有四个主要步骤:

• 通过提取最强的必要条件和最弱的充分条件来消除选择变量
• 重写方程式以保持代入条件下的可满足性/有效性
• 通过定点计算消除递归
• 最后，对闭式方程进行了决策

因为我们的抽象是有限的，定义1中的约束可以使用布尔逻辑进行编码，因此我们最后一步的目标决策过程是布尔SAT。我们必须在某个点上转换约束图1转化为等效布尔约束;在执行上面的任何步骤之前，我们首先执行这个转换。

对于每个变量({，})，我们引入布尔变量_我1、……_在这样_ij是真正的当且仅当_我＝C_j．我们映射方程变量到相同名称的布尔变量。一个变量的条件f返回C_我，故称为的年代返回变量。我们也会翻译年代₁＝年代₂在约束条件中出现如下:

注意表单的子表达式_我＝_j永远不会出现由系统产生的约束图1．我们替换每一个替换[C_j/_我通过布尔值替换[真正的/_ij]和[假/_本土知识]jk．

例2。示例1的第一行产生以下布尔约束(这里是布尔变量₁代表了方程＝C₁而且₂代表＝C₂)：

在一般情况下，约束来自图1会产生如下形式的布尔约束递归系统:

方程组1。

在哪里而且b_我｛真的,假的}和s是没有量词的公式，,．

观察根据规则生成的约束的任何解决方案图1必须为每个变量指定一个抽象值。更具体地说，在原始语义中，=C_我＝C_j是谁都无法满足的我,我这样我j,是有效的;但是，在布尔编码中_我j而且都是可以满足的。因此，为了对原始约束的这些隐式唯一性和存在性公理进行编码，我们将可满足性和有效性定义为:

在哪里_存在而且_独特的被定义为:

回到顶部

3.最强必要条件和最弱充分条件

正如前面所讨论的，我们算法中的一个关键步骤是从一个约束系统中提取必要/充分条件E．必要的职责。充分的)条件应该是可满足的(对应。有效)当且仅当E是可以满足的(分别地。有效)。这一节精确地给出了我们需要的充分必要条件;具体来说，有两个技术要求:

• 必要的职责。充分的)条件应该是强大的(职责。弱)。
• 必要/充分条件应该只在可观察变量上。

在下面，我们使用⁺()来表示，和中的可观察变量集合^-()表示选择变量的集合。

定义2。让使用无量词公式。我们说是最强可观察必要条件为如果:

第一个条件是是必要的，第二个条件保证比任何其他关于可观察变量的必要条件都强吗⁺()。额外的限制^-（) =强制公式的最强必要条件不包含选择变量。

定义3。让使用无量词公式。我们说是最弱可观察充分条件为如果:

设为某个程序属性的条件P成立。然后，通过是一个最强的必要条件，查询的可满足性等价于查询原始约束的可满足性来决定是否属性P可能持有。自的满足意味着的满足是一个必要条件吗．更有趣的是,因为最强的是这样的必要条件，满足吗也意味着满足;否则，更强的必要条件是假的。类似地，查询的有效性等价于查询原始约束的有效性以确定if属性P必须持有。

我们可以把最强的必要条件和最弱的充分条件定义为一个紧密的可观察的约束。如果只有可观察变量，则的最强必要条件和最弱充分条件等价于。如果只有选择变量，不等于真正的或假，那么最佳可能边界是＝真正的而且＝假的。直观上，最强必要条件和最弱充分条件之间的“差异”定义了原始公式中存在的未知信息的数量。

现在我们继续用一个非正式的例子来说明静态分析程序的最强可观察必要条件和最弱充分条件的有用性。

例3。考虑以下实现f给出了图2，假设我们想要确定指针的条件p是与f．很容易看出。的确切条件p的解引用由约束给出:

的返回值malloc（即。，缓冲区）用户输入（即。, *缓冲区）是静态未知的，最强的可观察必要条件f间接引用p由更简单的条件给出:

另一方面，解引用的最弱可观察充分条件为假，这就说得通了，因为对论证没有限制f可以保证,p反向引用。观察这些最强的必要条件和最弱的充分条件，它们与决定是否成立的原始公式一样精确p反向引用的f的任何呼叫地点f，而且，这些公式比原来的公式简洁得多。

回到顶部

4.解决约束

在本节中，我们现在回到计算仅包含可观察变量的最强必要条件和最弱充分条件的问题从方程组1。我们的算法首先从每个公式中消除选择变量。然后，我们对系统进行操作，以在替换(第4.2节)下保持最强的必要条件(最弱的充分条件)。最后，我们通过求解方程来消除递归约束(第4.3节)，在可观察变量上得到一个(非递归)公式系统。每一步都保留了原始方程的可满足性/有效性，因此可以使用标准的SAT解算器对最终公式确定原始的可能/必须查询。

4.1.取消选择变量

从公式中剔除选择变量图1，我们使用以下众所周知的结果来计算布尔公式的最强必要条件和最弱充分条件⁴：

引理1。布尔公式的最强必要条件和最弱充分条件不包含变量是由:

由于我们对可满足性和有效性的定义还必须考虑隐含的存在唯一性条件，因此必须对布尔公式最强必要条件和最弱充分条件的标准计算方法稍加修改。特别地，让是一个要消去的选择变量，让_存在而且_独特的表示包含的存在唯一性条件。然后，我们计算出最强的必要条件和最弱的充分条件:

将这些消去方法应用于约束系统图1，我们得到两组不同的方程，其形式为:

方程组2。

E_SC类似于E_数控．

例4。考虑例1中给出的函数，其布尔约束在例2中给出。的最弱充分条件：

读者可以验证，最强的必要条件是真实的。存在性和唯一性约束被省略，因为它们是冗余的。

4.2.保存在替换

我们的目标是通过迭代不动点计算来求解方程组2中给出的递归方程组。然而，存在一个问题:按照目前的情况，方程组2在代入条件下可能无法保持最强的必要条件和最弱的充分条件，原因有二:

• 最强的必要条件和最弱的充分条件不保留在否定下(即:而且)，方程组2中的公式包含了反的return()变量。因此，用*代替和¬会分别产生不正确的必要条件和充分条件。
• 方程组2中的公式可能包含包含返回变量的矛盾和重言式，由于将返回变量替换为各自的必要条件和充分条件，导致公式(在必要条件下)被削弱，(在充分条件下)被加强。因此，获得的必要(对应)。充分)条件可能不那么强。尽可能弱)。

幸运的是，这两个问题都可以补救。对于第一个问题，观察而且，下面的等价是成立的:

换句话说，的最强必要条件是对的最弱充分条件的否定，同样的，的最弱充分条件是对的最强必要条件的否定。因此，通过同时计算最强必要条件和最弱充分条件，可以利用上述等价解第一个问题。

为了克服第二个问题，一个明显的解决办法是将公式转换为析取范式，并在最强必要条件下应用替换之前去掉矛盾。同样，对于最弱的充分条件，可以将公式转换为合取范式，消除重言式。这一重写明确地加强了在原始公式中存在的任何矛盾和重言式，以便用它们的必要变量替换它们。充分条件不能减弱。加强)解决方案。

4.3.消除递归

由于我们现在有了在代入条件下保持最强必要条件和最弱充分条件的方法，因此可以使用标准的不动点计算技术，得到只包含可观察变量的方程组2的封闭形式解。为了计算最小不动点，我们使用以下格:

晶格l是有限的(直到逻辑等价)，因为只有有限数量的变量_ij因此只有有限个逻辑上不同的公式。这就产生了以下形式的括号约束:

方程组3。

回顾第2节，原始约束有四种可能的含义，即，真的,假的,，而由此得到的封闭形式强必要条件和最弱充分条件分别为任意一个真正的或假．这意味着在某些涉及非终止程序路径的情况下，原始方程组可能有意义在最少定点语义(或在最大不动点语义中)，但本文提出的算法可能返回任意一种真正的或假，取决于计算的是最大还是最小不动点。因此，我们的结果是由程序终止的假设来限定的。

例5。回想一下，在例4中我们计算过函数的f在例1中定义为:

找到最弱的充分条件，我们首先替换真正的为．这就得到了公式₁¬₁，一个同义反复。因此，我们的算法在最弱的充分条件下，发现不动点解为真．自f总是保证返回C₁，用我们的算法计算出的最弱充分条件是最精确的可能解。

回到顶部

5.限制

而本文提出的技术给出了一个性质的最强必要条件和最弱充分条件P就有限抽象而言，单独跟踪两个不同属性的条件是不精确的P₁而且P₂然后把各个结果结合起来。特别是,如果₁而且₂的最强必要条件是什么P₁而且P₂分别,然后₁₂做不的最强必要条件P₁而且P₂因为最强的必要条件不分布在连接上，而最弱的充分条件不分布在分离上而聚集在一起。因此，如果一个人对两个不同性质的组合推理感兴趣，就有必要计算出组合性质的最强必要条件和最弱充分条件。

虽然在我们的技术中，可能值的集合可以被详尽地枚举是很重要的(以保证不动点计算的收敛性，并能够将约束转换为布尔逻辑)，但集合不一定是有限的，只需要是有限的，即对给定的程序是有限的。此外，虽然这项技术显然可以应用于有限状态属性或枚举类型，但它也可以扩展到任何属性，其中可以派生出有限数量的等价类来描述可能的结果。然而，对于任意的非有限域，所提出的方法并不完全。

回到顶部

6.实验结果

我们在Saturn上实现了我们的方法，这是一个静态分析框架，用于检查C程序的属性。¹正如在第1节中提到的，分析中不精确的来源表现为不确定性的选择;在Saturn中，不精确的来源包括但不限于:从无界数据结构中读取数据、算法、不精确的函数指针目标、不精确的循环不变量和在线组装;分析中所有这些不精确的来源都被视为选择变量。

我们进行了两组实验来评估我们在OpenSSH、Samba和Linux内核上的技术。在第一组实验中，我们计算了指针解引用的充要条件。指针解引用在C程序中普遍存在，计算每个语法指针解引用的必要条件和充分条件是对我们的方法的一个很好的压力测试。作为第二个实验，我们将我们的技术合并到一个空解引用分析中，并证明我们的技术在不求助于特别启发式或损害可靠性的情况下，将假阳性的数量减少了近一个数量级。

在我们的第一组实验中，我们测量指针解引用的必要条件和充分条件的大小汇，在这里指针是解引用的，以及在来源,在那里

指针首先从堆中分配或读取。在图2，考虑第7行中的指针解引用(sink)。对于汇聚实验，我们将，例如，计算必要和充分条件p的废弃,p !=零旗帜!= 0而且假分别。为了说明源实验，考虑下面的函数调用位置f从图2：

线标记/ * * /是指针的源吗p；的必要条件p的来源p最终解除引用是x >马克斯x < = MAXp !=零旗帜!= 0)充分条件是x >马克斯．

文中给出了该接收器在Linux环境下的实验结果图3．的表图4介绍了OpenSSH、Samba和Linux的源和接收实验结果的摘要。的柱状图图3绘制必要的大小(对应于。充分)条件相对于有必要(对应的)的约束的数量。(充分)给定大小的条件。在此图中，红色条表示必要条件，绿色条表示充分条件，请注意y-轴按对数比例绘制。观察95%的必要和充分条件有少于5个子句，99%有少于10个子句，表明必要和充分条件在实践中很小。图4给出我们分析的所有三个应用程序在汇聚处(第2行和第3行)的平均必要条件和充分条件大小，确认在所有基准测试中，平均必要条件和充分条件大小一致较小。

我们的第二个实验将这些技术应用于寻找空解引用错误。我们选择空解引用作为应用程序，因为以足够的精度检查空解引用错误通常需要跟踪复杂的路径条件。在结果中图5，我们比较两种不同的设置程序间path-sensitive分析中，我们使用了文中描述的技术，计算解引用空指针的最强必要条件。在第二种设置中(即intraprocedurally path-sensitive对于每个函数，我们只计算在该函数中哪些指针可以解引用，但不跟踪在哪些函数之间解引用指针的条件。我们相信这种比较在量化本文中提出的技术的好处是有用的，因为，如果不消除选择变量，(i)过程间路径敏感分析甚至可能不会终止，(ii)选择变量的数量随着程序的大小线性增长，压倒了约束求解器。事实上，由于这个原因，之前在Saturn上写的所有分析要么是过程间路径不敏感的，要么是采用不完全启发式来决定跨函数边界跟踪哪些条件。¹

的前三列图5给出第一次设置的实验结果，同图的最后三列显示第二次设置的结果。一个重要的警告是，这里报告的数字不包括由数组元素和数据结构的递归字段引起的错误报告。土星没有复杂的形状分析;因此，报告的无界数据结构元素的绝大多数错误(>95%)都是误报。然而，形状分析是一个正交问题，我们既没有解决，也没有在这项工作中评价。

对过程内和过程间路径敏感分析结果的比较表明，我们的技术在不诉诸启发式或损害合理性的情况下减少了误报的数量，以消除过程间依赖产生的错误。请注意，假阳性的存在并不与我们之前声称的技术完备的说法相矛盾。首先，即使是有限域，我们的技术也只能提供相对完整性；假阳性仍然可能来自于分析中不精确的正交来源。第二，虽然我们的结果对于有限域是完全的，但我们不能保证对于任意域是完全的。

回到顶部

7.结论

我们提出了一种对静态分析系统中的未知值进行系统推理的方法。我们认为，虽然通过选择变量来表示未知值可以通过关联相同未知值的多次使用来增加有用的精度，但为了避免可伸缩性和终止问题，在函数边界消除这些选择变量是必要的。我们提出了一种技术来消除这些选择变量，而不损失信息，以回答可能和必须查询的程序属性。我们还通过实验证明，以这种方式分析未知值可以获得更好的精度和更好的可伸缩性。

回到顶部

回到顶部

回到顶部

回到顶部

回到顶部

数字图书馆是由计算机协会出版的。版权所有©2010 ACM有限公司