tweak wording

[web.git] / personal / _posts / 2020-12-14-provenance.md

diff --git a/personal/_posts/2020-12-14-provenance.md b/personal/_posts/2020-12-14-provenance.md
index 2f8c23c83d850273e727e05eb0656ea168f1f13b..ee3f5b6e3192b1e8ca75cc430691bc8a8665cf83 100644 (file)
--- a/personal/_posts/2020-12-14-provenance.md
+++ b/personal/_posts/2020-12-14-provenance.md
@@ -1,7 +1,9 @@
 ---
 title: "Pointers Are Complicated II, or: We need better language specs"
 ---
 title: "Pointers Are Complicated II, or: We need better language specs"

-categories: rust
+categories: rust research

 forum: https://internals.rust-lang.org/t/pointers-are-complicated-ii-or-we-need-better-language-specs/13562
 forum: https://internals.rust-lang.org/t/pointers-are-complicated-ii-or-we-need-better-language-specs/13562

+license: CC BY-SA 4.0
+license-url: https://creativecommons.org/licenses/by-sa/4.0/

 ---
 
 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 %}).
 ---
 
 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 %}).


@@ -86,7 +88,7 @@ All involved optimizations need to exactly agree on what is and is not UB, to en
 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.[^ub-difference]
 Sure, no human is going to write many programs in LLVM IR, so their syntax barely matters, but clang and rustc produce LLVM IR programs all the time, and as we have seen understanding the exact rules governing the behavior of programs is crucial to ensuring that the optimizations LLVM performs do not change program behavior.
 
 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.[^ub-difference]
 Sure, no human is going to write many programs in LLVM IR, so their syntax barely matters, but clang and rustc produce LLVM IR programs all the time, and as we have seen understanding the exact rules governing the behavior of programs is crucial to ensuring that the optimizations LLVM performs do not change program behavior.
 

-[^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 strictly more UB than LLVM IR (for integer arithmetic), which makes translation in one direction easy, while the other direction is hard.
+[^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, signed 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 strictly more UB than LLVM IR (for integer arithmetic), which makes translation in one direction easy, while the other direction is hard.

 
 [^ub-difference]: In particular, 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.
 
 
 [^ub-difference]: In particular, 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.
 


@@ -106,15 +108,14 @@ The sequence of examples is taken from [this talk](https://sf.snu.ac.kr/llvmtwin
 Here is the source program:
 {% highlight c %}
 char p[1], q[1] = {0};
 Here is the source program:
 {% highlight c %}
 char p[1], q[1] = {0};

-int ip = (int)(p+1);
-int iq = (int)q;
+uintptr_t ip = (uintptr_t)(p+1);
+uintptr_t iq = (uintptr_t)q;

 if (iq == ip) {
   *(char*)iq = 10;
   print(q[0]);
 }
 {% endhighlight %}
 I am using C syntax here just as a convenient way to write programs in LLVM IR.
 if (iq == ip) {
   *(char*)iq = 10;
   print(q[0]);
 }
 {% endhighlight %}
 I am using C syntax here just as a convenient way to write programs in LLVM IR.

-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.

 
 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.
 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).
 
 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.
 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).


@@ -123,10 +124,10 @@ The first "optimization" we will perform is to exploit that if we enter the `if`
 Subsequently the definition of `ip` is inlined:
 {% highlight c %}
 char p[1], q[1] = {0};
 Subsequently the definition of `ip` is inlined:
 {% highlight c %}
 char p[1], q[1] = {0};

-int ip = (int)(p+1);
-int iq = (int)q;
+uintptr_t ip = (uintptr_t)(p+1);
+uintptr_t iq = (uintptr_t)q;

 if (iq == ip) {
 if (iq == ip) {

-  *(char*)(int)(p+1) = 10; // <- This line changed
+  *(char*)(uintptr_t)(p+1) = 10; // <- This line changed

   print(q[0]);
 }
 {% endhighlight %}
   print(q[0]);
 }
 {% endhighlight %}


@@ -134,8 +135,8 @@ if (iq == ip) {
 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:
 {% highlight c %}
 char p[1], q[1] = {0};
 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:
 {% highlight c %}
 char p[1], q[1] = {0};

-int ip = (int)(p+1);
-int iq = (int)q;
+uintptr_t ip = (uintptr_t)(p+1);
+uintptr_t iq = (uintptr_t)q;

 if (iq == ip) {
   *(p+1) = 10; // <- This line changed
   print(q[0]);
 if (iq == ip) {
   *(p+1) = 10; // <- This line changed
   print(q[0]);


@@ -145,8 +146,8 @@ if (iq == ip) {
 The final optimization notices that `q` is never written to, so we can replace `q[0]` by its initial value `0`:
 {% highlight c %}
 char p[1], q[1] = {0};
 The final optimization notices that `q` is never written to, so we can replace `q[0]` by its initial value `0`:
 {% highlight c %}
 char p[1], q[1] = {0};

-int ip = (int)(p+1);
-int iq = (int)q;
+uintptr_t ip = (uintptr_t)(p+1);
+uintptr_t iq = (uintptr_t)q;

 if (iq == ip) {
   *(p+1) = 10;
   print(0); // <- This line changed
 if (iq == ip) {
   *(p+1) = 10;
   print(0); // <- This line changed


@@ -185,10 +186,10 @@ In a flat memory model where pointers are just integers (such as most assembly l
 
 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.
 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*.
 
 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.
 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*.

-To see why, consider the two expressions `(char*)(int)(p+1)` and `(char*)(int)q`:
+To see why, consider the two expressions `(char*)(uintptr_t)(p+1)` and `(char*)(uintptr_t)q`:

 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).
 The only way to explain this is to say that the input to the `(char*)` cast is different, since the program state is otherwise identical in both cases.
 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).
 The only way to explain this is to say that the input to the `(char*)` cast is different, since the program state is otherwise identical in both cases.

-But we know that the integer values computed by `(int)(p+1)` and `(int)q` (i.e., the bit pattern of length 32 that serve as input to the `(char*)` casts) are the same, and hence a difference can only arise if these integers consist of more than just this bit pattern---just like pointers, integers have provenance.
+But we know that the integer values computed by `(uintptr_t)(p+1)` and `(uintptr_t)q` (i.e., the bit pattern as stored in some CPU register) are the same, and hence a difference can only arise if these integers consist of more than just this bit pattern---just like pointers, integers have provenance.

 
 Finally, let us consider the first optimization.
 Here, a successful equality test `iq == ip` prompts the optimizer to replace one value by the other.
 
 Finally, let us consider the first optimization.
 Here, a successful equality test `iq == ip` prompts the optimizer to replace one value by the other.


@@ -263,7 +264,7 @@ Nowadays, its main purpose is to help unsafe code authors avoid UB, but for me p
 It also feeds back into the design of the UB rules by discovering patterns that people want or need to use but that are not currently accepted by Miri.
 
 On the LLVM side, the main development in this area is [Alive](https://blog.regehr.org/archives/1722), a tool that can automatically validate[^validate] optimizations performed by LLVM.
 It also feeds back into the design of the UB rules by discovering patterns that people want or need to use but that are not currently accepted by Miri.
 
 On the LLVM side, the main development in this area is [Alive](https://blog.regehr.org/archives/1722), a tool that can automatically validate[^validate] optimizations performed by LLVM.

-Alive has found [many bugs in LLVM optimizations](https://github.com/AliveToolkit/alive2/blob/master/BugList.md), and indeed much of the recent dialog with the LLVM community aimed at a more precise IR semantics is pushed by the people building Alive, lead by Nuno P. Lopes and John Regehr.
+Alive has found [many bugs in LLVM optimizations](https://github.com/AliveToolkit/alive2/blob/master/BugList.md), and indeed much of the recent dialog with the LLVM community aimed at a more precise IR semantics is pushed by the people building Alive, led by Nuno P. Lopes and John Regehr.

 
 [^validate]: A note on terminology: "validating" an optimization means that given the program text before and after the optimization, the tool will try to prove that this particular transformation is correct. This is in contrast to "verifying" an optimization where a once-and-forall proof is carried out showing that the optimization will always perform a correct transformation. Verification gives a much stronger result, but is also extremely difficult to carry out, so validation is a great middle-ground that is still able to find plenty of bugs.
 
 
 [^validate]: A note on terminology: "validating" an optimization means that given the program text before and after the optimization, the tool will try to prove that this particular transformation is correct. This is in contrast to "verifying" an optimization where a once-and-forall proof is carried out showing that the optimization will always perform a correct transformation. Verification gives a much stronger result, but is also extremely difficult to carry out, so validation is a great middle-ground that is still able to find plenty of bugs.
 


@@ -271,7 +272,7 @@ Progress on these specification efforts is slow, though, in particular when it t
 I hope this post can raise awareness for the subtle problems optimizing compilers are facing, and convince some people that figuring out the specification of compiler IRs is an important and interesting problem to work on. :)
 
 That's all I have for today, thanks for sticking with me!
 I hope this post can raise awareness for the subtle problems optimizing compilers are facing, and convince some people that figuring out the specification of compiler IRs is an important and interesting problem to work on. :)
 
 That's all I have for today, thanks for sticking with me!

-As usual, this post can be [discussed in the Rust forums](https://internals.rust-lang.org/t/pointers-are-complicated-ii-or-we-need-better-language-specs/13562).
+As usual, this post can be [discussed in the Rust forums](https://internals.rust-lang.org/t/pointers-are-complicated-ii-or-we-need-better-language-specs/13562) and [on Reddit](https://www.reddit.com/r/rust/comments/kd157i/pointers_are_complicated_ii_or_we_need_better/).

 I am curious what your thoughts are on how we can build compilers that do not suffer from the issues I have discussed here.
 
 #### Footnotes
 I am curious what your thoughts are on how we can build compilers that do not suffer from the issues I have discussed here.
 
 #### Footnotes