2 title: "Pointers Are Complicated II, or: Why Provenance Matters"
6 Some time ago, I wrote a blog post about how [there's more to a pointer than meets the eye]({% post_url 2018-07-24-pointers-and-bytes %}).
7 One key point I was trying to make is that
9 > *just because two pointers point to the same address, does not mean they are equal and can be used interchangeably.*
11 This "extra information" that comes with a pointer is typically called [*provenance*](https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#pointer-provenance).
12 This post is a cautionary tale of what can happen when provenance is not considered sufficiently carefully in an optimizing compiler.
16 As an example, I will show a series of three compiler transformation that each seem "intuitively justified" based on wording in the C standard and some common understanding of how pointers work.
17 We will use LLVM for these examples, but the goal is not to pick on LLVM---other compilers suffer from similar issues.
18 The goal is to convince you that we need to take provenance seriously if we want to build a correct compiler for languages permitting unsafe pointer manipulation such as C, C++, or Rust.
20 ## Warm-up: Why IRs need a precise semantics
22 As a warm-up, let me try to convince you that compiler IRs such as LLVM IR need a precise (and precisely documented) semantics.
23 If you are already familiar with the idea of treating compiler IRs as proper programming languages in their own right, you can skip to the next section.
25 Consider the following simple (and contrived, for the sake of this example) piece of C code:
27 int sum_up(int i, int j, int n) {
35 One transformation the compiler might want to do is to move the addition `i+j` out of the loop, to avoid computing the sum each time around the loop:
37 int sum_up(int i, int j, int n) { // optimized version
46 However, that transformation is actually incorrect.
47 If we imagine a caller using this function as `sum_up(INT_MAX, 1, 0)`, then this is a perfectly correct way to call `sum_up`: the loop is never entered, so the overflowing addition `INT_MAX+1` is never performed.
48 However, after the desired optimization, the program now causes a signed integer overflow, which is UB (Undefined Behavior) and thus May Never Happen!
50 One might be tempted to ignore this problem because the UB on integer overflow is a compiler-only concept; every target supported by the compiler will do the obvious thing and just produce an overflowing result.
51 However, there might be other compiler passes running after the optimization we are considering.
52 One such pass might inline `sum_up`, and another pass might notice the `INT_MAX+1` and replace it by `unreachable`, and another pass might then just remove all our code since it is unreachable.
53 Each of these passes has a good reason to exist (it can help real code become a lot faster or help prune dead code), but if we combine them all with our loop hoisting optimization, the result is a disaster.
55 I am convinced that the only way to avoid such problems is to find a way to justify the correctness of each optimization *in isolation*.
56 Each optimization must be *correct* for any possible program, where *correct* means that the optimized program must only "do things" that the original program could have done as well.
57 (This is basically the "as-if" rule in the C standard, and is typically called "refinement" in the academic literature.)
58 In particular, no optimization must ever introduce UB into a UB-free program.
60 It may seem now that under this premise, it is impossible to perform the loop hoisting optimization we are considering.
61 But that is not the case!
62 We can perform the optimization, *we just cannot perform it in C*.
63 Instead, we have to perform it in LLVM IR (or any other IR with a suitable semantics).
64 Specifically, signed integer overflow in LLVM yields a `poison` result.
65 It is not UB to produce `poison`, it is just UB to use `poison` in certain ways (the details do not matter here).
66 In a call to `sum_up(INT_MAX, 1, 0)`, the `s` variable introduced by loop hoisting is unused, so the fact that its value is `poison` does not matter!
68 Due to this behavior of signed integer overflow, the loop hoisting optimization is *correct* if we consider it as an optimization on programs that are written in LLVM IR.[^cheat]
69 In particular, this means we can freely combine this optimization with any other optimization that is *correct* in LLVM IR (such as inlining, replacing definite UB by `unreachable`, and removing unreachable code), and we can be sure that the result obtained after all these optimizations is a correct compilation of our original program.
71 However, to make the argument that an optimization is *correct*, the exact semantics of LLVM IR (what the behavior of all possible programs is and when they have UB) needs to be precisely and unambiguously documented.
72 All involved optimizations need to exactly agree on what is and is not UB, to ensure that whatever code they produce will not be considered UB by a later optimization.[^ub-difference]
73 This is exactly what we also expect from the specification of a programming language such as C, which is why I think we should consider compiler IRs as proper programming languages in their own right, and specify them with the same diligence as we would specify "normal" languages.
74 Sure, no human is going to write many programs in LLVM IR, but clang and rustc produce LLVM IR programs all the time, and as we have seen understanding the exact rules governing these programs is crucial to ensuring that the optimizations LLVM performs do not change program behavior.
76 [^cheat]: If now you feel like we somehow cheated, since we can always translate the program from C to LLVM IR, optimize there, and translate back, consider this: translating from LLVM IR to C is really hard! In particular, singed integer addition in LLVM IR can *not* be translated into signed integer addition in C, since the former is well-defined with `poison` result in case of overflow, but the latter says overflow is UB. C has, in a sense, strictly more UB than LLVM IR, which makes translation in one direction easy, while the other direction is hard.
78 [^ub-difference]: In fact, I would say that two different variants of the IR with different rules for UB are really *two different programming languages*. A program that is well-defined in one language may have UB in another, so great care needs to be taken when the program is moved from being governed by one set of rules to another.
80 *Take-away:* If we want to be able to justify the correctness of a compiler in a modular way, considering only one optimization at a time, we need to perform these optimizations in an IR that has a precise specification of all aspects of program behavior, including UB.
81 Then we can, for each optimization separately, consider the question: does the optimization ever change program behavior, and does it ever introduce UB into UB-free programs?
83 ## How 3 (seemingly) correct optimizations can be incorrect when used together
85 With the warm-up done, we are now ready to consider some more tricky optimizations.
86 We will look at three different optimizations LLVM can perform, and I will show that they *cannot all be correct* since the first and last program we are considering actually have *different behavior*.
87 (More precisely: the last program has a possible behavior that was not possible for the first program.)
88 This is only possible if at least one optimization changed program behavior in an incorrect way.
89 To determine which optimization is at fault, we will need a more precise specification of LLVM IR than what currently exists.
91 The sequence of examples you are going is taken from [this talk](https://sf.snu.ac.kr/llvmtwin/files/presentation.pdf#page=32) by Chung-Kil Hur.
92 For simplicity, we assume that `int` has the right size to hold a pointer value; just imagine we used `uintptr_t` if you want to be more general.
94 Here is the source program:
96 char p[1], q[1] = {0};
104 We are using C syntax here, but remember that we just use C syntax as a convenient way to write programs in LLVM IR.
105 This program has two possible behaviors: either `ip` (the address one-past-the-end of `p`) and `iq` (the address of `q`) are different, and nothing is printed.
106 Or the two are equal, in which case the program will print "10" (`iq` is the result of casting `q` to an integer, so casting it back will yield the original pointer, or at least a pointer pointing to the same object / location in memory).
108 The first "optimization" we will perform is to exploit that `iq == ip`, so we can replace all `iq` by `ip`, and subsequently inline the definition of `ip`:
110 char p[1], q[1] = {0};
114 *(char*)(int)(p+1) = 10; // <- This line changed
119 The second optimization notices that we are taking a pointer `p+1`, casting it to an integer, and casting it back, so we can remove the cast roundtrip:
121 char p[1], q[1] = {0};
125 *(p+1) = 10; // <- This line changed
130 The final optimization notices that `q` is never written to, so we can replace `q[0]` by its initial value `0`:
132 char p[1], q[1] = {0};
137 print(0); // <- This line changed
141 However, this final program is different from the first one!
142 Specifically, the final program will either print nothing or print "0", while the original program *could never print "0"*.
143 This shows that the sequence of three optimizations we performed, as a whole, is *not correct*.
145 #### What went wrong?
147 Clearly, one of the three optimizations is incorrect in the sense that it introduced a change in program behavior.
150 In an ideal world, we would have a sufficiently precise semantics for LLVM IR that we would just have to read the docs (or, even better, run some Miri-like tool) to figure out the answer.
151 However, describing language semantics at this level of precision is *hard*, and full of trade-offs.
152 That's why the LLVM LangRef will not give us a clear answer here, and indeed obtaining a clear answer requires some decisions that have not been explicitly made yet.
153 As a formal researcher, all I can do is to structure the design space and uncover the trade-offs; it will be up to the LLVM community to decide which option to pick.
154 But the key point is that *they will have to make a choice*, because the status quo of doing all three of these optimizations leads to incorrect compilation results.
156 To proceed, we will use the three optimizations that we considered above as cues: assuming that the optimization is correct for LLVM IR, what does that tell us about the semantics?
158 We start with the last optimization, where the `print` argument is changed from `q[0]` to `0`.
159 This optimization is based on alias analysis:
160 `q[0]` gets initialized to `0` at the beginning of the program, and the only write between that initialization and the `print` is to the pointer `p+1`.
161 Since `q` and `p` point to different local variables, a pointer derived from `p` cannot alias `q[0]`, and hence we know that this write cannot affect the value stored at `q[0]`.
163 Looking more closely, however, reveals that things are not quite so simple!
164 `p+1` is a one-past-the-end pointer, so it actually *can* have the same address as `q[0]`
165 (and, in fact, inside the conditional we know this to be the case).
166 However, LLVM IR (just like C) does not permit memory accesses through one-past-the-end pointers.
167 It makes a difference whether we use `p+1` or `q` inside the `if`, even though we know (in that branch) that both pointers point to the same memory location.
168 This demonstrates that in LLVM IR, there is more to a pointer than just the address it points to---it also matters how this address was computed.
169 This something extra is what we typically call *provenance*.
170 It is impossible to argue for the correctness of the third optimization without acknowledging that provenance is a real part of the semantics of an LLVM IR program.
171 This is what I mean when I say *provenance matters*.
173 Now that we know that provenance exists in pointers, we have to also consider what happens to provenance when a pointer gets cast to an integer and back.
174 The second optimization gives us a clue into this aspect of LLVM IR semantics: casting a pointer to an integer and back is optimized away, which means that *integers have provenance*.
175 To see why, consider the two expressions `(char*)(int)(p+1)` and `(char*)(int)q` (this optimization consists of replacing one by the other):
176 if the optimization of removing pointer-integer-pointer roundtrips is correct, the first operation will output `p+1` and the second will output `q`, which we just established are two different pointers (they differ in their provenance).
177 The only way to explain this is to say that the input to the `(char*)` cast is different, since the Abstract Machine state is identical in both cases.
178 But we know that the integer value (i.e., the bit pattern of length 32) that serves as input to the `(char*)` cast is the same, and hence a difference can only arise if integers consist of more than just this bit pattern---just like pointers, integers have provenance.
180 Finally, let us consider the first optimization.
181 Here, a successful equality test `iq == ip` prompts the optimizer to replace one value by the other.
182 This optimization demonstrates that *integers do not have provenance*:
183 the optimization is only correct if a successful run-time equality test implies that the two values are equivalent in the Abstract Machine.
184 But this means that the Abstract Machine version of this value cannot have any "funny" extra parts that are not represented at run-time.
185 Of course, provenance is exactly such a "funny" extra part.
186 A different way to phrase the same argument is to say that this optimization is correct only if `iq == ip` implies that both values have the same provenance.
187 This would be a possible definition of `==` in LLVM IR only in principle---in practice this means the LLVM backends have to compile `==` in a way that pointer provenance is taken into account, which of course is impossible.
190 By considering each of these three optimizations in terms of what they tell us about the semantics of LLVM IR, we learned that pointers have provenance, that integers remember the provenance of the pointer they come from in case of a pointer-to-integer cast, and that integers do not have provenance.
191 This is a contradiction, and this contradiction explains why we saw incorrect compilation results when applying all three optimizations to the same program.
193 #### How can we fix this?
projects / web.git / blob