指针很复杂II,或者:我们需要更好的语言规范

2020-12-15 02:10:37

前段时间,我写了一篇博客文章,内容是关于指针的更多内容。

仅仅因为两个指针指向同一个地址,并不意味着它们在可以互换使用的意义上是相等的。

这种区别于同一地址的不同指针的“额外信息”通常称为“出处”。这是另一种尝试,通过讲述一个警告性故事,即当未充分考虑出处时会出问题的原因,从而使您确信该出处是“真实的”该帖子是独立的;我并不是以为您已经阅读了第一篇。这里还有一个更大的信息,关于如何通过在编译器IR的规范上花费更多的精力来防止将来出现此类问题。

下面,我将展示一系列三个编译器转换,每个转换看起来都“直观上是合理的”,但是将它们组合在一起会导致明显不正确的结果。我将在这些示例中使用LLVM,但目标不是选择LLVM,而是其他编译器也遇到类似的问题。我们的目标是说服您,为允许进行不安全指针操作的语言(例如C,C ++或Rust)构建正确的编译器,我们需要更加认真地对待IR语义(尤其是出处)。我使用LLVM以这些示例为例,因为使用它的单一且详细记录的IR可以轻松地研究许多基础设施的发展,因此让我们开始吧!

作为热身,我将举一个简单的示例,说明诸如LLVM IR之类的编译器IR需要精确的(并有精确记录的)语义。如果您已经熟悉将编译器IR视为本身就是正确的编程语言的想法, ,或者如果您只是在这里查看指针及其来源,则可以跳到下一部分。

考虑以下简单(为方便起见,人为设计)的C代码计算n *(i + j):

int sum_up(int i,int j,unsigned int n){int result = 0;而(n> 0){结果+ = i + j; n-= 1;返回结果; }

编译器可能想要进行的一种转换是将加法运算i + j移出循环,以避免每次绕循环计算总和(这称为“循环不变代码运动” 1):

int sum_up(int i,int j,unsigned int n){//优化版本int result = 0;整数s = i + j;而(n> 0){结果+ = s; n-= 1;返回结果; }

但是,这种转换实际上是不正确的。如果我们想象一个调用者将此函数用作sum_up(INT_MAX,1,0),则这是调用sum_up的一种完全正确的方法:永远不会进入循环,因此溢出的加法INT_MAX + 1但是,经过所需的优化后,该程序现在会导致有符号整数溢出,即UB(未定义行为),因此可能永远不会发生!

人们可能很想忽略这个问题,因为整数溢出的UB是仅编译器的概念;编译器支持的每个目标都会做明显的事情,并且只会产生溢出结果,但是,在我们考虑优化之后可能还会运行其他编译器遍历,其中一个遍历可以内联sum_up,而另一个遍历可能会注意到INT_MAX + 1并将其替换为不可达,因为UB代码“按定义”不可达,然后另一遍可能会删除我们所有的代码,因为它不可达。这些遍历中的每一个都有一个充分的理由存在(它可以帮助真正的代码变得更快或帮助修剪死代码),但如果将它们与循环不变代码运动结合在一起,结果将是一场灾难。

避免此类问题的一种方法(也是我所知道的唯一系统的方法)是确保我们可以孤立地证明每个优化的正确性。每个优化对于任何可能的程序都必须是正确的,其中正确意味着被优化的程序必须仅原始程序也可以做的“做某事”。(这基本上是C标准中的“假设”规则,在学术文献中通常称为“优化”。)尤其是,永远不必进行优化。将UB引入无UB程序中。

现在看来,在此前提下,不可能执行我们正在考虑的循环不变代码运动,但事实并非如此!到目前为止,我们所看到的是,优化是在对处理器执行的时候是不正确的C程序。但是当LLVM执行这些优化时,它不认为程序是用C编写的,而是认为程序是用LLVM IR编写的,它的语义与C有所不同。具体地说,LLVM LangRef表示带符号整数LLVM IR中的溢出会产生毒物值。不是UB产生毒物,只是以某种方式使用毒物的UB(此处的详细内容无关紧要)。在调用优化的sum_up(INT_MAX,1, 0),循环不变代码运动引入的s变量未使用,因此其值是有毒的事实无关紧要!

由于有符号整数溢出的这种行为,如果我们将其视为对LLVM IR编写的程序的优化,则这种循环不变代码运动的情况是正确的。 2为此,我们付出的“代价”是在LLVM IR中用不可达替换INT_MAX + 1是不正确的,因为它不是UB。

正确优化的妙处在于,我们可以按任意顺序组合任意数量的优化(例如,内联,用不可达代码替换确定的UB,以及删除不可达代码),并且我们可以确保所有这些优化之后获得的结果是正确地编写原始程序。(在学术术语中,我们会说“改进是可传递的”。)

但是,为了证明优化是正确的,需要记录LLVM IR的确切语义(所有可能的程序的行为以及当它们具有UB时的行为)。而不是UB,以确保它们产生的任何代码在以后的优化中都不会被视为UB。这正是我们对C等编程语言规范的期望,这就是为什么我认为我们应该将编译器IR视为适当的原因自行编程语言,并以与指定“常规”语言相同的努力来指定它们。 3当然,没有人会用LLVM IR编写许多程序,因此它们的语法几乎没有关系,但是clang和rustc始终会生成LLVM IR程序,而且正如我们所看到的那样,了解控制程序行为的确切规则对于确保LLVM执行的优化不会更改程序行为。

要点:如果我们希望能够以模块化的方式证明编译器的正确性,一次只考虑一次优化,那么我们需要在IR中执行这些优化,该IR必须对程序行为的各个方面进行精确说明(包括UB)。然后,我们可以针对每个优化分别考虑以下问题:优化是否会改变程序行为,是否将UB引入无UB程序中?对于正确的优化,这些问题的答案是“否”。 ”。

完成预热后,我们现在准备考虑一些更棘手的优化,我们将使用它们来探索语言规范需要达到的精确度的问题,我们将研究LLVM可以执行的三种不同的优化,我将表明由于我们正在考虑的第一个程序和最后一个程序实际上具有不同的行为,所以它们不可能都是正确的(更确切地说:最后一个程序具有第一个程序不可能的可能的行为)只有在至少一个优化以不正确的方式更改了程序行为,但是实际上并不清楚是哪个优化的罪魁祸首。

例子序列取材自Chung-Kil Hur的演讲。它是在研究严格的LLVM规范时发现的。

字符p [1],q [1] = {0}; uintptr_t ip =(uintptr_t)(p + 1); uintptr_t iq =(uintptr_t)q;如果(iq == ip){*(char *)iq = 10;打印(q [0]); }

我在这里使用C语法只是在LLVM IR中编写程序的一种便捷方式。

该程序有两种可能的行为:ip(p的地址的前一末尾)和iq(q的地址)不同,并且什么都不打印,或者两者相等,在这种情况下,程序将打印“ 10”(iq是将q强制转换为整数的结果,因此将其强制返回将产生原始指针,或至少指向内存中相同对象/位置的指针)。

我们将执行的第一个“优化”是利用如果我们输入if主体,则拥有iq == ip,因此我们可以将所有iq替换为ip。随后,ip的定义被内联:

字符p [1],q [1] = {0}; uintptr_t ip =(uintptr_t)(p + 1); uintptr_t iq =(uintptr_t)q;如果(iq == ip){*(char *)(uintptr_t)(p + 1)= 10; //<-此行更改了打印(q [0]); }

第二次优化注意到我们正在获取一个指针p + 1,将其强制转换为整数,然后将其强制返回,因此我们可以删除强制转换:

字符p [1],q [1] = {0}; uintptr_t ip =(uintptr_t)(p + 1); uintptr_t iq =(uintptr_t)q;如果(iq == ip){*(p + 1)= 10; //<-此行更改了打印(q [0]); }

最终的优化注意到q从未被写入,因此我们可以将q [0]替换为其初始值0:

字符p [1],q [1] = {0}; uintptr_t ip =(uintptr_t)(p + 1); uintptr_t iq =(uintptr_t)q;如果(iq == ip){*(p + 1)= 10;打印(0); //<-此行已更改}

但是,该最终程序与第一个程序不同!具体地说,最终程序将不打印任何内容或打印“ 0”,而原始程序则永远不会打印“ 0”。这表明我们执行了三个优化的顺序,如下所示:整体而言,是不正确的。

显然,这三种优化中的一种是不正确的,因为它引入了程序行为的改变,但是到底是哪一种呢?

在理想的世界中,我们将为LLVM IR提供足够精确的语义,以至于只需阅读文档(或者更好的是运行一些类似于Miri的工具)即可找到答案,但是在此描述语言语义LLVM LangRef在这里不会给我们一个明确的答案,实际上要获得一个明确的答案需要做出一些尚未明确做出的决定。

继续进行,我们将使用上面作为提示考虑的三个优化:假设该优化对于LLVM IR是正确的,那么这对语义有何启示?

让我们从最后一个优化开始,将print参数从q [0]更改为0。此优化基于别名分析:q [0]在程序开始时初始化为0,并且在因为q和p指向不同的局部变量,所以从p派生的指针不能别名q [0],因此我们知道该写操作不会影响存储在q [ 0]。

然而,更仔细地观察发现,事情并不是那么简单! p + 1是一个唯一的指针,因此它实际上可以具有与q [0]相同的地址(并且实际上,在条件内,我们知道是这样)。但是,LLVM IR(就像C)不允许通过过去的指针进行内存访问,即使我们知道(在那个分支中)两个指针都指向if,在if中使用p + 1或q也会有所不同。相同的内存位置。这表明在LLVM IR中,指向指针的不仅仅是指针指向的地址,这也关系到该地址的计算方式。这额外的信息通常称为出处。无法为正确性辩解在没有确认出处是LLVM IR程序语义的真正组成部分的情况下,在第三次优化中,在指针只是整数(例如大多数汇编语言)的平面内存模型中,这种优化是完全错误的。

既然我们知道指针中存在出处,那么我们还必须考虑当指针被强制转换为整数然后返回时会发生什么情况。第二种优化为我们提供了LLVM IR语义这一方面的线索:将指针强制转换为整数和back被优化掉了,这意味着整数具有出处。要了解原因,请考虑两个表达式(char *)(uintptr_t)(p + 1)和(char *)(uintptr_t)q:如果移除指针的优化-integer-pointer往返是正确的,第一个操作将输出p + 1,第二个操作将输出q,我们刚刚建立的是两个不同的指针(它们的来源不同)。唯一的解释方法是说(char *)类型转换的输入是不同的,因为在两种情况下程序状态都是相同的。但是我们知道由(uintptr_t)(p + 1)和(uintptr_t)q(即位模式)计算的整数值就像存储在某些CPU寄存器中一样),因此只能产生差异如果这些整数不仅仅包含该位模式,则就像指针一样,整数具有出处。

最后,让我们考虑第一个优化。在这里,成功的相等性测试iq == ip会提示优化器将一个值替换为另一个值。此优化表明整数不具有出处:该优化仅在成功运行时才正确-时间相等性测试意味着这两个值在用于描述语言语义的“抽象机”中是等效的。但这意味着该值的抽象机版本不能包含运行时未表示的任何“有趣”多余部分时间。当然,出处就是这样一个“有趣的”额外部分。用不同的方式表达同一论点的方法是说,只有当iq == ip评估为true时,这种优化才是正确的,这意味着两个值具有相同的“ “抽象机器”表示形式,因此,如果该表示形式包含出处,则两个值必须具有相同的出处。这可能是LLVM IR中==的定义,但仅在原则上—实际上,这意味着LLVM ba ckends必须以考虑指针出处的方式编译==,这当然是不可能的。

总结:通过就LLVM IR的语义告诉我们这三个优化中的每一个,我们了解到指针具有出处,在记住指向指针的情况下,整数记住它们来自的指针的出处-integer强制转换,并且整数不具有出处。这是一个矛盾,这个矛盾解释了为什么在将所有三个优化应用于同一程序时我们看到不正确的编译结果。

为了解决这个问题,我们必须声明三个优化之一不正确并停止执行它。就LLVM IR语义而言,这相当于确定指针和/或整数是否具有出处:

我们可以说指针具有出处,而整数则没有,这会使第二个优化无效。

在我看来,第一个和最后一个选项是站不住脚的。除去起源,除了最简单的别名分析外,其他所有分析都被杀死了。 4另一方面,声明整数具有出处不仅会禁用上面显示的链中的第一个优化,而且还会禁用常见的算术优化,例如x-x等于0。一旦整数具有出处。

因此,我认为应该通过说指针具有起源而不是整数来解决该问题,这意味着第二个优化是错误的,这也与最近向C标准委员会提出的建议相对应。 LLVM错误#34548说优化指针整数指针往返是不正确的,在一般情况下LLVM应该停止这样做,在某些特殊情况下仍然可以这样做,但要弄清楚这的局限性还需要更多LLVM IR语义的精确描述,例如我们在本文中提出的内容。

但是最终,将由LLVM社区来决定。我可以肯定地说的是,他们必须做出选择,因为执行这三种优化的现状都会导致错误的编译结果。

我们学到了什么?首先,指针很复杂。要以与通用别名分析一致的方式精确描述其语义,就需要添加“源”的概念。在Java或ML之类的语言中,指针是不透明的类型,其指针无法观察到表示形式,这实际上是很容易做到的。但是在诸如Rust,C或C ++之类的语言中,该语言支持指针整数类型转换,出处的引入提出了一些非常棘手的问题,并且至少是一个经常执行的问题。这个空间的优化必须给予。

我们还了解到LLVM有一个错误,但这不是本文的重点.GCC开发人员犯了完全相同的错误,我得知MSVC和ICC存在相同的问题(尽管我不知道如何验证我不能责怪他们;我认为这样的错误是不可避免的:在IR中出现准确的UB时,通常只是松散地指定,在许多情况下是“忽略”(在规范中未包括的情况是UB隐含的),因此评估在上面定义的意义上某些优化是否正确可能非常棘手甚至是不可能的。指针出处只是一个特别好的(且微妙的)示例。有关另一个示例,请参见本文的第2.3节(图3包含代码),其中显示了两种优化的序列如何导致编译错误,其中第一种优化在LLVM并发模型下是正确的,第二种优化在C ++ 11并发模型下是正确的,但是没有并发模型可以同时进行这两种优化是正确的,因此每个编译器(或更确切地说,每个编译器IR)都需要选择一个。最后,有关undef和中毒的论文提供了一些优化示例,这些优化被L中存在undef破坏了LVM,并描述了定义有毒的语义时出现的一些折衷;再次出现错误编译是因为在规范的某个地方声明的结果(每次使用undef都会获取新的值)并未在其他地方考虑(测试)等于零的等值整数并不意味着它为零;也可能是undef)。

这使我得出本文的主要结论:为避免不兼容的优化问题,我认为我们需要更认真地考虑编译器IR作为编程语言本身的重要性,并为它们提供精确的规范-包括所有UB。 ,您可能会说LLVM具有广泛的LangRef来表示反对,但通过阅读LLVM规范,您仍然可以使自己相信上述三个优化中的每一个都是正确的,正如我们所看到的,这是矛盾的。我们是否需要一个正式的数学定义来避免此类歧义?我认为有一些简单的方法已经可以帮上大忙了。矛盾的根源是规范的某些部分隐含地认为指针具有出处,这在考虑其他操作时很容易忘记,这就是为什么我认为它非常重要为了使这些假设更加明确:规范应明确描述“构成”值的信息,其中包括诸如出处以及是否(完全或部分)初始化该值。 5此信息需要足够广泛,以使假设的解释器可以使用它来检测所有UB。

......