From ba75a7b12c8ae46a043951e0636a64b228f9227c Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 22 Aug 2017 19:11:07 +0200 Subject: [PATCH] UB post: clarify --- personal/_posts/2017-07-14-undefined-behavior.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/personal/_posts/2017-07-14-undefined-behavior.md b/personal/_posts/2017-07-14-undefined-behavior.md index 4635668..851f737 100644 --- a/personal/_posts/2017-07-14-undefined-behavior.md +++ b/personal/_posts/2017-07-14-undefined-behavior.md @@ -52,6 +52,11 @@ However, if they *do* alias, that would violate the effective type restriction, As we have seen, in both of the possible cases, the reordering is correct; the compiler is thus free to perform the transformation. Undefined behavior moves the burden of proving the correctness of this optimization from the compiler to the programmer. +In the example above, what the "effective type" rule really means is that every single memory read of a `float` comes with a *proof obligation*: +The programmer has to show that that the last write to this memory actually happened through a `float` pointer (baring some exceptions around union and character pointers). +Similarly, the (in)famous rule that [signed integer overflow is undefined behavior](https://stackoverflow.com/questions/16188263/is-signed-integer-overflow-still-undefined-behavior-in-c) means that every single arithmetic operation on signed integers comes with the proof obligation that this operation will never, ever, overflow. +The compiler performs its optimization under the assumption that the programmer actually went through the effort and convinced itself that this is the case. + Considering that the compiler can only be so smart, this is a great way to justify optimizations that would otherwise be difficult or impossible to perform. Unfortunately, it is often not easy to say whether a program has undefined behavior or not -- after all, such an analysis being difficult is the entire reason compilers have to rely on UB to perform their optimizations. Furthermore, while C compilers are happy to exploit the fact that a particular program *has* UB, they do not provide a way to test that executing a program *does not* trigger UB. @@ -89,4 +94,6 @@ It is with such considerations in my mind that I have previously written about [ Coming up next on this channel: During my [internship]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}), I am working on such a specification. My ideas are concrete enough now that I can write down a draft, which I will share with the world to see what the world thinks about it. -**Uodate:** [Writing down has happened]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}). +**Update:** [Writing down has happened]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}). + +**Update:** Clarified "Shifting Responsibility". -- 2.30.2