ACM通信

研究突出了

未定义行为检测的差分方法

作者:王曦，Nickolai Zeldovich, M. Frans Kaashoek, Armando Solar-Lezama
ACM通讯，2016年3月，第59卷第3期，99-106页
10.1145 / 2885256
评论

本文研究了C/ c++等系统编程语言中产生的未定义行为。未定义的行为错误会导致不可预测和微妙的系统行为，它们的影响可以通过编译器优化进一步放大。许多系统中都存在未定义的行为错误，包括Linux内核和Postgres数据库。其后果包括从不正确的功能到缺少安全检查。

本文提出了一种正式而实用的方法，该方法通过在利用未定义行为的优化方面找到“不稳定代码”来发现未定义的行为bug。使用这种方法，我们引入了一个新的静态检查器STACK，它可以精确地识别未定义的行为错误。将STACK应用到广泛使用的系统中发现了161个新的bug，这些bug已经被开发人员确认并修复了。

回到顶部

1.简介

许多编程语言的规范将某些代码片段指定为具有未定义的行为(参考文献2.3节。¹⁸)．例如，在C语言中“使用不可移植的或错误的程序构造或错误的数据”会导致未定义的行为(参考文献3.4.3节)。²³）;在C语言规范中有一个未定义行为的全面列表(参考文献中的J.2节)。²³)．

一类未定义的行为是简单的编程错误，例如缓冲区溢出和空指针解引用。另一类是不可移植操作，其硬件实现通常有细微的差别。例如，当有符号整数溢出或被零除法发生时，一个除法指令会在x86上触发(参考文献3.2节)。²²)，而它会在PowerPC上静默地生成一个未定义的结果(参考文献3.3.8节)。^30.)．另一个例子是移位指令:将一个32位左移1 × 32位在ARM和PowerPC上产生0，但在x86上产生1;然而，将一个32位左移一个64位在ARM上产生0，但在x86和PowerPC上产生1。

通过将某些编程错误和不可移植的操作指定为具有未定义的行为，规范允许编译器自由地生成在这些情况下以任意方式行为的指令，允许编译器生成高效和可移植的代码，而无需额外的检查。例如，许多高级编程语言(如Java)对缓冲区溢出有良好定义的处理(如运行时异常)，编译器将需要为内存访问操作插入额外的边界检查。然而，C/ c++编译器可以不需要插入边界检查，因为越界情况是未定义的。避免未定义的行为是程序员的责任。

根据C/ c++规范，调用未定义行为的程序可能会出现任意问题。正如有人总结的那样，“可以允许的未定义的行为包括完全忽略结果不可预测的情况，以及让恶魔从你的鼻子里飞出来。”⁴⁵但在实践中会发生什么呢?本文的其余部分将展示现代编译器越来越多地利用未定义行为来执行主动优化;通过这些优化，许多程序可以产生出乎程序员意料的结果。

回到顶部

2.未定义行为的风险

未定义行为的一个风险是，程序将观察到不同硬件架构、操作系统或编译器上的不同行为。例如，一个执行超大左移的程序在ARM和x86处理器上会观察到不同的结果。作为另一个例子，考虑一个简单的SQL查询:

这个查询会导致Postgres数据库服务器中有符号整数溢出，在32位Windows系统上不会导致任何问题，但在64位Windows系统上会导致服务器崩溃，原因是两个系统上除法指令的行为不同。⁴⁴

此外，编译器优化可以放大未定义行为的影响。例如，考虑指针溢出检查Buf + len < Buf所示图1,在那里缓冲区是一个指针len是一个正整数。程序员的目的是抓住这种情况len太大了buf +兰包围并绕过第一次检入图1．我们在许多系统中都发现了类似的检查，包括Chromium浏览器、Linux内核和Python解释器。⁴⁴

虽然这个检查似乎对平面地址空间有效，但它在分段结构上失败(参考文献6.3.2.3节)。³²)．因此，C标准规定溢出的指针是未定义的(参考文献6.5.6节。^23(p8))，这样GCC就可以简单地假定上面没有发生指针溢出任何体系结构。在这种假设下,buf +兰必须大于缓冲区，因此“溢出”检查的计算结果总是为假的。因此，gcc删除了检查，为系统的攻击铺平了道路。¹⁷

另外一个例子,图2显示了Linux内核中的一个轻微缺陷，程序员错误地放置了解引用桶——> sk之前检查空指针!桶．通常，内核禁止对页0的访问;一个空桶指向页0会导致内核在桶——> sk并终止当前进程。即使页面0是可访问的(例如，通过mmap或者其他一些利用^24，38),检查!桶会捕获一个null桶并防止任何进一步的利用。无论哪种情况，对手都应该这样做不能够超越空指针检查。

不幸的是，当gcc第一次看到解引用时桶——> sk，它的结论是指针桶必须是非空的，因为C标准规定对空指针解引用是未定义的(Ref。²³)．自桶为非空时，GCC进一步确定空指针检查是不必要的，并消除了检查，使特权升级利用成为可能。¹³

为了进一步理解编译器优化是如何利用未定义的行为的，我们使用六个真实世界的示例进行了研究，以健全检查的形式，如最上面一行所示图3．所有这些检查都可以评估为假并在优化后变成死代码，因为它们调用了未定义的行为。接下来我们将使用它们来测试现有的编译器。

• 检查p+ 100 <p就像图1．
• 空指针检查!p与之前的取消引用类似图2．
• 检查x+ 100 <x有符号整数x在gcc的bugzilla中引起了激烈的争论。⁵
• 检查x⁺+ 100 < 0测试优化是否执行更精细的推理;x⁺众所周知是积极的。
• shift check !(1 <<x)的目的是捕捉大量移动的数量x，从一个补丁到ext4文件系统。⁶
• 检查腹肌（x) < 0，目的是捕捉最负值(即-2ⁿ¹)，测试优化是否理解库函数。⁷

我们选择了12个知名的C/ c++编译器来看看它们对上面的代码示例做了什么:2个开源编译器(gcc和clang)和10个最近的商业编译器(惠普的aCC、ARM的armcc、英特尔的icc、微软的msvc、AMD的open64、PathScale的pathcc、Oracle的suncc、TI的TMS320C6000、风河的Diab编译器和IBM的XL C编译器)。对于每个代码示例，我们都测试编译器是否优化了入检假，则得到最低优化级别-0n它发生的时候。结果显示在图3．

我们进一步使用gcc和clang来研究优化的演变，因为历史很容易访问。对于gcc，我们选择了以下具有代表性的版本，它们跨越了十多年的时间:

• GCC 2.95.3，最后2个。x，发行于2001年;
• GCC 3.4.6，最后3个。x， 2006年发行;
• gcc 4.2.1, GPLv2的最后一个版本，发布于2007年，至今仍广泛用于BSD系统;
• GCC 4.9.1, 2014年发布。

为了进行比较，我们选择了两个版本的clang，分别是2009年发布的1.0和2014年发布的3.4。

我们可以看到，利用未定义的行为来消除代码在编译器中很常见，而不仅仅是像一些程序员声称的那样，在最近的gcc版本中。²⁶甚至gcc 2.95.3也消除了这一点x+ 100 <x。有些编译器会删除gcc不能删除的代码(例如，clang on 1 <<)。x)．

即使对于资深的C程序员来说，这些优化也会导致令人困惑的结果，因为与未定义行为无关的代码会被优化掉或以意想不到的方式转换。这样的错误导致编译器开发人员和使用C语言但不遵守官方C规范的从业者之间激烈的争论。实践者将这些优化描述为“毫无意义”⁴⁰而仅仅是编译器“对基本C语义的创造性重新解释”。²⁶另一方面，编译器作者认为优化在规范下是合法的;这就是“坏掉的代码”⁵程序员应该解决这个问题。更糟糕的是，随着编译器的发展，引入了新的优化，可能会破坏以前工作的代码;正如我们所展示的图3，在过去的20年里，许多编译器在这种优化方面变得更加积极。

回到顶部

3.未定义行为检测的挑战

考虑到未定义行为可能导致的广泛问题，程序员应该如何处理它?naïve方法要求程序员仔细阅读和理解C语言规范，这样他们就可以编写谨慎的代码，避免调用未定义的行为。不幸的是，正如我们在第2节中演示的那样，即使是有经验的C程序员也不能完全理解C语言的复杂性，而且在实践中避免调用未定义的行为是极其困难的。

由于优化常常会放大未定义行为造成的问题，一些程序员(比如Postgres开发人员)已经尝试降低编译器的优化级别，这样激进的优化就不会利用代码中未定义的行为错误。正如我们在图3，编译器在利用未定义行为的优化级别上是不一致的，一些编译器甚至在优化级别为零(原则上应该禁用所有优化)时也会进行未定义的行为优化。

运行时检查可用于在运行时检测某些未定义的行为;例如，GCC提供了一个-ftrapv选项来捕获有符号整数溢出，并且clang提供了一个-fsanitize =未定义选择陷阱更多未定义的行为。也有人尝试提供对C语言更“程序员友好”的改进，^14，29它具有较少的未定义行为，尽管通常不清楚如何在不引起显著性能开销的情况下从规范中取缔未定义行为。^14，42

某些静态分析和模型检查器可以识别由于未定义行为而导致的bug。例如，编译器可以捕获一些明显的情况(例如，使用gcc的- wall)，但总的来说，这是具有挑战性的(参考文献的第三部分。²⁷）;用于查找缓冲区溢出bug的工具¹¹可以被视为寻找未定义的行为错误，因为引用缓冲区范围之外的位置是未定义的行为。有关相关工作的更详细讨论请参见第6节。

回到顶部

4.方法:发现不同的行为

理想情况下，当应用程序调用未定义的行为时，编译器会为开发人员生成警告，本文采用静态分析方法来发现未定义的行为错误。这可以归结为，对于程序中的每个操作，是否可以使用导致未定义行为的参数来调用它。由于C中的许多操作会调用未定义的行为(例如，有符号整数操作，指针算术)，为每个操作产生警告会让开发人员难以承受，所以精确分析是很重要的。全局推理可以精确地确定每个操作的参数的值，但它不能扩展到大型程序。

我们的目标不是执行全局推理，而是在给定操作的参数上找到局部不变量(或可能的不变量)。我们愿意不完整:如果没有足够的局部不变量，我们愿意不报告潜在的问题。另一方面，我们希望确保每一份报告都可能是一个真正的问题。¹

我们在本文中利用的局部可能性不变量与程序员编写的不必要的源代码有关。所谓“不必要的源代码”，我们指的是死代码、可以转换成更简单形式的不必要的复杂表达式，等等。我们期望程序员编写的所有源代码要么是必要的代码，要么是明显不必要的代码;也就是说，在不依赖C语言微妙语义的情况下，从本地上下文来看，代码是不必要的。例如，程序员可能会写如果(0){…},这显然是不必要的代码。然而，我们的可能性不变式告诉我们，程序员永远不会编写这样的代码A = b << c;如果(c >= 32){…}，在哪里b为32位整数。的如果语句是不必要的代码，因为c不能为32或更大，因为在前面的左移中未定义的行为。我们的不变量的核心是程序员不太可能编写这种微妙的不必要的代码。

为了形式化这个不变量，我们需要区分“活代码”(总是必要的代码)、“死代码”(总是不必要的代码)和“不稳定代码”(略微不必要的代码)。我们通过考虑程序员可能对C语言规范有不同的解释来做到这一点。特别地，我们认为C语言是该语言的官方规范，C '是程序员认为C语言拥有的规范。在本文中，C '不同于C，在C中，操作会导致未定义的行为。例如，程序员可能希望对所有可能的参数定义良好的转换;这是一个可能的C '换句话说，C '是官方C语言的一个宽松版本，它对C语言中未定义行为的操作进行了特定的解释。

使用不同语言规范的概念，我们说一段代码是生活如果对于每一个可能的C '，代码都是必要的。相反，一段代码是死如果对于所有可能的C '，代码都是不必要的;这捕获的代码如下如果(0){…}。最后，一段代码是不稳定如果，对于一些C '变体，它是不必要的，但在其他C '变体中，它是必要的。这意味着两个不完全理解C规范细节的程序员可能会对代码所做的事情产生分歧。正如我们在本文的其余部分所演示的，这种启发式方法通常表明存在bug。

基于此不变量，我们现在可以检测程序何时可能调用未定义的行为。特别是给定一个操作o在一个函数中f，我们计算不必要的代码集f在不同的解释下，在o。如果不必要的代码集合对于所有可能的解释都是相同的，我们就不能说是否如此o可能会调用未定义的行为。然而，如果不必要的代码集随未定义行为的变化而变化o触发器，这意味着程序员写的代码不稳定。然而，根据我们的假设，这种情况永远不会发生，我们得出的结论是，程序员可能认为他们在编写实时代码，只是没有意识到这一点o会触发未定义的行为相同代码运行所需的一组输入。

回到顶部

5.堆栈的工具

为了使用上述方法找到未定义的行为错误，我们构建了一个静态分析工具STACK。在实践中，很难列举和考虑所有可能的C '变量。因此，为了构建一个实用的工具，我们选择了一个称为C*的单一变体。C*定义了一个映射到地址0的空指针，以及指针和整数算术的包围语义。³¹我们认为这抓住了程序员(错误地)认为C提供的通用语义。虽然我们的C*只处理C规范中未定义行为的子集，但不同的C*可以捕获程序员可能隐式假定的其他语义，或者为C*没有处理的其他操作处理未定义行为。

STACK依赖于一个优化器O隐式标记不必要的代码。堆栈的O消除死代码，并分别在C和C*的语义下执行表达式简化。的代码片段e,如果O是不可以重写e在这两种语义下，STACK都考虑e“实时代码”;如果O能够重写e在这两个语义,e是“死代码”;如果O能够重写e在C而不是C*下，STACK将其报告为“不稳定代码”。

由于STACK只使用了语言规范的两种解释(即C和C*)，它可能会错过在不同解释下可能出现的bug。例如，任何代码消除O在C*下永远不会触发来自STACK的警告，即使可能存在另一个C '，不允许消除该代码。STACK的方法可以扩展为支持多种解释，以解决这一潜在缺陷。

5.1.不稳定代码的定义

现在我们给出不稳定代码的正式定义。一个代码片段e语句或表达式是否位于程序中特定的源位置P。如果编译器可以转换片段e在某种程度上，这将会改变P＇年代行为在C*下，而不是在C下，那么e不稳定的代码。

让P［e / e是一个由替换而形成的程序e一些片段e'在同一地点。什么时候编译器进行转换是合法的P成P［e / e'],表示PP［e / e']吗?在没有未定义行为的语言规范中，答案很简单:对于每个输入，两者都是合法的P而且P［e / e产生相同的结果。在语言规范中与未定义的行为，答案更复杂;也就是说，如果对于每一个输入，以下条件之一为真，则它是合法的:

• 这两个P而且P［e / e生成相同的结果，而不调用未定义的行为，或
• P调用未定义的行为，在这种情况下，它无关紧要P［e / e']。

使用这种表示法，我们在下面定义了不稳定代码。

定义1(不稳定代码)。程序P中的代码片段e是不稳定的。如果存在一个片段e '，使得P P[e/e ']在C下合法，但在C*下不合法。

例如，对于中列出的完整性检查图3， C编译器有权将它们替换为假，因为根据C规范，这是合法的，而假设的C*编译器不能做同样的事情。因此，这些检查是不稳定的代码。

5.2.用于识别不稳定代码的算法

上面的定义捕获了什么是不稳定代码，但没有提供一种寻找不稳定代码的方法，因为很难推断整个程序的行为。作为更改程序行为的代理，STACK寻找可以被某些优化器转换的代码O在C下，而不是在C*下。特别地，STACK使用了一个两阶段方案:

1. 运行O没有利用未定义的行为，在C*下捕获优化;而且
2. 运行O同样，这一次利用了未定义的行为，它捕获了C下(更积极的)优化。

如果O在第二阶段优化额外的代码，我们假设原因O在第一阶段没有这样做是因为这会改变程序在C*下的语义，所以STACK认为代码是不稳定的。

STACK的基于优化器的寻找不稳定代码的方法将会错过特定的优化器无法在第二阶段消除的不稳定代码，即使存在一些优化器可以消除这些不稳定代码。如果优化器在第一阶段没有足够积极地消除代码，那么这种方法也会生成错误的报告。因此，STACK设计中的一个挑战是提出一个足够积极的优化器来最小化这些问题。

为了使这种方法起作用，STACK需要一个优化器，它可以有选择地利用未定义的行为。为了构建这样的优化器，我们将在5.2.1节中通过引入明确的项目假设，它抓住了C语言的假设，即程序员永远不会编写调用未定义行为的程序。给定一个可以将显式假设作为输入的优化器，STACK可以通过向优化器提供(或不提供)定义良好的程序假设，打开(或关闭)基于未定义行为的优化。我们构建了两个遵循这种方法的积极优化器:一个用来消除不可到达的代码(第5.2.2节)，另一个用来简化不必要的计算(第5.2.3节)。

明确的项目假设。我们将优化器中利用未定义行为的含义形式化如下。考虑一个带有输入的程序x。给定一个代码片段e,让R_e（x)表示其可达性条件,这是真正的敌我识别e将在输入下执行x；,让U_e（x)表示其未定义的行为条件，或简称为UB条件，用于指示是否e对输入显示未定义的行为x，摘要载于图4．

这两个R_e（x),U_e（x)是布尔表达式。例如，给定一个指针解引用*p在表达e，一个UB条件U_e（x)是p＝零(即，导致空指针解引用)。

直观地说，在一个定义良好的程序中对指针解引用p, p必须是非空的。换句话说，否定UB条件，p≠零，必须在表达式执行时保持不变。我们将其归纳如下。

定义2(定义良好的程序假设)。代码片段e定义了输入xIff执行不会触发未定义的行为：

此外，如果程序的每个片段都在输入上定义良好，则该程序在输入上定义良好，记为Δ:

消除不可到达的代码。第一个算法确定可以消除的不稳定语句(即，P P (e /Ø)在哪里e是一份声明)。例如，如果到达一条语句需要触发未定义的行为，那么该语句一定是不可到达的。我们在下面将其形式化。

定理1(消除)。在定义良好的程序P中，如果没有输入，优化器可以消除代码片段ex两者都达到e并且满足定义良好的程序假设Δ(x)：

布尔表达式R_e（x)∧Δ(x）被称为取消查询。

证明。假设Δ(x)是真正的，如果消除查询R_e（x)∧Δ(x)总是计算为假,然后R_e（x)必须假,这意味着e必须是遥不可及的。然后就可以安全地消除了e。

考虑图2作为一个例子。只有一个输入桶在这个程序中。通过较早的如果检查，可达性条件返回语句是桶。有一个UB条件桶=零,从指针解引用桶——> sk,其可达条件为真实的。因此，消除查询R_e（x)∧Δ(x)返回声明:

显然，没有桶满足这个问题。因此，可以消除返回声明。

根据上面的定义，很容易构造一个算法来识别由于代码消除而导致的不稳定代码(参见图5)．该算法首先在没有定义良好的程序假设的情况下删除不可到达的片段，然后根据这种假设对不可到达的片段发出警告。后者是不稳定的代码。

简化不必要的计算。第二个算法确定可以优化为更简单形式的不稳定表达式(即P P (e / e”)在哪里e而且e表达式)。例如，如果对布尔表达式求值为真正的需要触发未定义的行为，则该表达式必须求值为假的。我们在下面将其形式化。

定理2(简化)。在定义良好的程序P中，如果没有输入，优化器可以用另一个e '来简化表达式ex评估e（x）和e '（x）到不同的值，同时都达到e并满足定义良好的程序假设Δ(x)：

布尔表达式e（x)≠e”(x∧)R_e（x)∧Δ(x）被称为简化查询。

证明。假设Δ(x)是真正的，如果简化查询e（x)≠e”(x∧)R_e（x)∧Δ(x)总是计算为假,然后e（x) =e”(x)，这意味着它们的值相同;或R_e（x)是假,这意味着e是遥不可及的。无论哪种情况，都可以放心更换e与e”。

简化依赖于神谕e的表达式e。注意，这里对提议的表达式没有限制e”。在实践中，它应该比原来的更简单e因为编译器倾向于简化代码。STACK目前实现了两个oracle:

• oracle:布尔提出真正的而且假依次为布尔表达式，枚举可能的值。
• 代数oracle:如果比较的一方是另一方的子表达式，建议消除比较双方的公共术语。它对于简化非常量表达式很有用，例如提议y< 0的X + y < X,通过消除x两边。

举个例子，考虑简化p+ 100 <p使用布尔oracle，其中p是一个指针。为简单起见，假定其可达性条件为真实的。从图4的UB条件p+ 100是p_∞+ 100_∞∉[0,2n- 1)。布尔oracle首先提出真实的。对应的简化查询为:

显然，这是可以满足的。然后布尔oracle提议假的。这次简化查询是:

因为没有指针p满足这个条件，可以折叠p+ 100 <p成假的。

根据上面的定义，可以直接构造一个算法来识别由于简化而不稳定的代码(参见图6)．算法查询每一个可能的更简单的形式e的表达式e。与消去类似，它会在发现时发出警告e'就相当于e只有在定义良好的程序假设下。

5.3.实现

我们使用LLVM编译器框架实现了STACK²⁸和Boolector求解器。⁴STACK由大约4000行c++代码组成。为了使该工具能够扩展到大型代码库，STACK实现了第5.2节中描述的近似版本的算法。有兴趣的读者可以参考我们的SOSP文件了解详情。⁴⁴

STACK主要通过探索两种基本的优化来识别不稳定的代码，一种是由于不可达而进行的消除，另一种是由于不必要的计算而进行的简化。以其他形式利用定义良好的程序假设是可能的。例如，一些优化不是丢弃代码，而是重新排序指令，并由于内存混叠产生不必要的代码⁴¹或数据,^3.STACK没有实现的。

STACK实现了两个oracle，布尔和代数，用于提出新的表达式来简化。人们可以通过引入新的神谕来扩展它。

5.4.主要结果

从2012年7月到2013年3月，我们定期将STACK应用于用C/ c++编写的系统软件，包括操作系统内核、虚拟机、数据库、多媒体编码器/解码器、语言运行时、安全库等。根据STACK的bug报告，我们向相应的开发人员提交了补丁。开发人员确认并修复了161个新bug。

截至2013年3月24日，我们还将STACK应用于Debian Wheezy存档中的所有17,432个包。STACK检查了其中包含C/ c++代码的8575个。在Intel Xeon E7-8870 2.4 GHz处理器上构建和分析这些包大约需要150个cpu天。对于这8575个包中的3471个(40%)，STACK至少发出了一个警告。

结果表明，未定义行为是普遍存在的，而STACK对于识别未定义行为是有用的。请参阅我们的论文以获得更完整的细节。⁴⁴

回到顶部

6.相关工作

据我们所知，我们给出了第一个定义和静态检查器来查找不稳定的代码，但我们构建在几个相关工作的基础上。特别是早期的调查^25，35，42和博客文章^27，33，34收集不稳定代码的示例，这些代码促使我们解决这个问题。我们还受到可以帮助处理不稳定代码的相关技术的激励，我们将在接下来讨论这些技术。

6.1.测试策略

我们对不稳定代码的经验表明，在实践中，程序员很难注意到某些关键代码片段从运行的系统中消失了，因为它们被编译器无声地丢弃了。维护一个全面的测试套件可能有助于在这种情况下捕获“消失”的代码，尽管这样做通常需要大量的努力来通过手动测试用例实现高代码覆盖率。程序员可能还需要准备各种各样的测试环境，因为不稳定的代码可能依赖于硬件和编译器。

自动化工具，如KLEE⁹能够使用符号执行生成高覆盖率的测试用例。然而，这些工具常常不能正确地建模未定义的行为。因此，他们可能会以不同于语言标准的方式解释程序，从而遗漏bug。考虑一个检查x+ 100 <x,在那里x是有符号整数。克利认为x+ 100包裹给定一个大x；换句话说，支票抓住了一个大x在KLEE中执行时，即使gcc丢弃检查。因此，为了检测不稳定的代码，这些工具需要增加一个未定义行为的模型，比如我们在本文中提出的模型。

6.2.优化策略

我们相信程序员应该避免未定义的行为。然而，过于激进的编译器优化也是引发这些bug的原因。传统上，编译器专注于生成快速且小的代码，甚至以牺牲安全性为代价，如第2节所示。编译器作者应该重新考虑生成安全代码的优化策略。

考虑x+ 100 <x有符号整数x一次。语言标准允许编译器将检查考虑为假并丢弃它。然而，根据我们的经验，程序员不太可能有意删除代码。程序员友好的编译器可以生成有效的溢出检查代码，例如，通过在计算后利用许多处理器上可用的溢出标志x+ 100。这种策略也被语言标准所允许，它产生的代码比放弃检查更安全。或者，当编译器以一种可能令人惊讶的方式利用未定义的行为时，可能会产生警告。⁸

目前，gcc提供了几个选项来改变编译器对未定义行为的假设，例如

• -fwrapv，假设加、减、乘用有符号整数;
• -fno-strict-overflow，假定指针算术绕除-fwrapv；而且
• -fno-delete-null-pointer-checks，³⁷假设不安全的空指针解除引用。

这些选项可以帮助减少令人惊讶的优化，但代价是生成更慢的代码。然而，它们涵盖了可能导致不稳定代码的未定义行为的不完整集合(例如，没有移位或除法选项)。另一个缺点是这些选项是gcc特有的;其他编译器可能不支持它们或以不同的方式解释它们。⁴²

6.3.跳棋

中列出的许多现有工具都可以检测到未定义的行为图4．例如，gcc提供-ftrapv选项插入有符号整数溢出的运行时检查(参考文献中3.18节)。³⁶）;国际奥委会¹⁵(现在是clang的消毒剂的一部分¹²),号⁴³覆盖更完整的整型误差集;土星¹⁶查找空指针解引用;几个专门的C语言解释器，如kcc¹⁹和Frama-C¹⁰执行未定义行为检查。见陈等人的调查¹¹总结。

作为对这些直接针对未定义行为的检查器的补充，STACK发现了由于未定义行为而死亡的不稳定代码。在这个意义上，STACK可以被认为是Engler等人不一致交叉检查框架的推广。^16，20.然而，STACK支持更有表现力的假设，比如指针和整数操作。

正如现有的检查程序所探索的那样，^2，21，39死代码是可能的bug的有效指示器。STACK通过查找找到未定义的行为bug巧妙地语言规范的不同解释下的不必要代码。

6.4.语言设计

语言设计者可能会重新考虑是否有必要将某些结构声明为未定义的行为，因为在规范中减少未定义的行为可能会避免不稳定的代码。一个例子是将有符号的32位左移1到31位。这是C语言中未定义的行为。²³)，即使结果是一致的0 x80000000在大多数现代处理器上。c++语言标准委员会在最新规范中为该操作指定了定义良好的语义。²⁹

回到顶部

7.总结

这篇文章证明了未定义的行为错误比我们之前认为的要普遍得多，它们会导致广泛的重大问题，它们经常被系统程序员误解，许多流行的编译器已经执行了意想不到的优化，导致行为不当或脆弱的系统。我们引入了一种识别未定义行为的新方法，并开发了一个静态检查器STACK，以帮助系统程序员识别和修复错误。我们希望编译器的作者也会重新考虑针对未定义行为的优化策略。最后，我们希望本文能够鼓励语言设计者在语言规范中谨慎使用未定义的行为。几乎每一种语言都允许开发人员根据语言规范编写具有未定义含义的程序。这项研究表明，对未定义的东西放任自流可能会导致微妙的bug。STACK的所有源代码都可以在http://css.csail.mit.edu/stack/．

回到顶部

致谢

我们感谢Xavier Leroy帮助改进本文，以及许多其他人对早期论文的反馈。^42，44这项研究得到了DARPA全新设计的弹性，自适应，安全主机(CRASH)计划的支持，合同\# n661-10-2 4089，以及美国国家科学基金会授予的CNS-1053143。

回到顶部

回到顶部

回到顶部

回到顶部

回到顶部

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

---

没有发现记录