add draft on Tree Borrows

[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 4e95665df3daa7bc67ad5806493469143e2c6ee2..94040c417cecb1e86a83942f6530cd8fb0b22a2c 100644 (file)
--- a/personal/_posts/2020-12-14-provenance.md
+++ b/personal/_posts/2020-12-14-provenance.md
@@ -1,6 +1,6 @@
 ---
 title: "Pointers Are Complicated II, or: We need better language specs"
 ---
 title: "Pointers Are Complicated II, or: We need better language specs"

-categories: rust research
+categories: rust research programming

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


@@ -55,10 +55,12 @@ int sum_up(int i, int j, unsigned int n) { // optimized version
 {% endhighlight %}
 However, that transformation is actually incorrect.
 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.
 {% endhighlight %}
 However, that transformation is actually incorrect.
 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.

-However, after the desired optimization, the program now causes a signed integer overflow, which is UB (Undefined Behavior) and thus May Never Happen!
+However, after the desired optimization, the program now causes a signed integer overflow, which is UB (Undefined Behavior) and thus May Never Happen![^signed-int-overflow]

 
 [^loop]: If you are a regular reader of my blog, you will recognize this as the same optimization that already played a crucial role in [a previous post of mine]({% post_url 2020-07-15-unused-data %}). Loop-invariant code motion is a great optimization to look at when considering corner cases of IR semantics.
 
 
 [^loop]: If you are a regular reader of my blog, you will recognize this as the same optimization that already played a crucial role in [a previous post of mine]({% post_url 2020-07-15-unused-data %}). Loop-invariant code motion is a great optimization to look at when considering corner cases of IR semantics.
 

+[^signed-int-overflow]: If you are coming here with a Rust mindset, imagine `i + j` was written as `i.unchecked_add(j)`.
+

 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.
 However, there might be other compiler passes running after the optimization we are considering.
 One such pass might inline `sum_up`, and another pass might notice the `INT_MAX+1` and replace it by `unreachable` since UB code is "by definition" unreachable, and another pass might then just remove all our code since it is unreachable.
 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.
 However, there might be other compiler passes running after the optimization we are considering.
 One such pass might inline `sum_up`, and another pass might notice the `INT_MAX+1` and replace it by `unreachable` since UB code is "by definition" unreachable, and another pass might then just remove all our code since it is unreachable.


@@ -88,7 +90,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.