Pointers Are Complicated II, or: We need better language specs
1–10 of 135 posts
Re: Pointers Are Complicated II, or: We need better language specs
#2This is a standalone sequel to "Pointers Are Complicated, or: What's in a Byte?" (https://www.ralfj.de/blog/2018/07/24/pointers-and-bytes.html).
Which has been discussed on HN
Re: Pointers Are Complicated II, or: We need better language specs
#3Does this have implications about the safety guarantees even safe Rust can make? It seems like incorrect optimization passes could result in bugs/security issues that are a byproduct of the compiler rather than the language itself. I wonder how big of an issue this is for Rust (relatively probably a bigger issue than for C/C++ where basic resource ownership bugs are more common).
Re: Pointers Are Complicated II, or: We need better language specs
#4Does this have implications about the safety guarantees even safe Rust can make? It seems like incorrect optimization passes could result in bugs/security issues that are a byproduct of the compiler rather than the language itself. I wonder how big of an issue this is for Rust (relatively probably a bigger issue than for C/C++ where basic resource ownership bugs are more common).
Yes, the pointer issues Ralf raises has implications about what operations Rust can make safe. An example Ralf posed to the safe transmute working group: a transmutation from a reference (i.e., a pointer with provenance) to one without (e.g., a "raw" pointer) or to a `usize` number cannot be safe. (Rust can safely provide these conversions via the `as` keyword, just not via the more general framework of transmutations).
More broadly: Rust is very sensitive to LLVM bugs that inadvertently generate UB. The longstanding issues with `noalias` optimizations is the prime example of this: https://stackoverflow.com/a/57259339/7501301
Re: Pointers Are Complicated II, or: We need better language specs
#5> 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 documented.
This is a great point as to why formal semantics of programming languages matters. Even if an optimization seems "obviously" correct, finicky things like introducing the possibility of UB can, as the post outlines, cascade into compiler passes that change the program more and more drastically. The post mentions that one need not go overly formal with the semantics, but I'll demonstrate what could happen when one does.
One possible formulation of semantics is denotational semantics, which describes how to map a program source syntax into values, i.e. eval : Expr -> Val. So when we have an optimization opt : Expr -> Expr, the desired correctness property for that optimization is that
Definition opt_correct (opt : Expr -> Expr) := forall (e : Expr), eval e = eval (opt e).
Theorem e_plus_0_to_e_correct : opt_correct e_plus_0_to_e.
Theorem opt_correct_compose (opt1, opt2 : Expr -> Expr) :
opt_correct opt1 -> opt_correct op2 -> opt_correct (opt1 ∘ opt2).
eval (opt1 (opt2 e))
= { since opt1 is correct }
eval (opt2 e)
= { since opt2 is correct }
eval eRe: Pointers Are Complicated II, or: We need better language specs
#6Does this have implications about the safety guarantees even safe Rust can make? It seems like incorrect optimization passes could result in bugs/security issues that are a byproduct of the compiler rather than the language itself. I wonder how big of an issue this is for Rust (relatively probably a bigger issue than for C/C++ where basic resource ownership bugs are more common).
Yes, absolutely. https://github.com/rust-lang/rust/issues/28728 is probably the most famous bug here, but many I-unsound bugs are similar.
This would be the case even without this. Compilers are programs. Programs have bugs.
Re: Pointers Are Complicated II, or: We need better language specs
#7This is a standalone sequel to "Pointers Are Complicated, or: What's in a Byte?" ( https://www.ralfj.de/blog/2018/07/24/pointers-and-bytes.html ). Which has been discussed on HN 2020: https://news.ycombinator.com/item?id=24376797 2018: https://news.ycombinator.com/item?id=17604402
Oh, there was a repost in 2020, that explains the sudden spike in page hits that I saw earlier this year and couldn't trace back. ;)
Re: Pointers Are Complicated II, or: We need better language specs
#8First of all: fantastic article. In-depth, insightful, and the examples are absolutely top-notch. On the razor's edge between accessible and profound. Hats off to the author.
I will say that the problems seem to lie in a few interesting interlanguage quirks, and not so much on language specs. For example, LLVM and C have different definitions of "undefined behavior"[1] -- this is pointed out when looking at the `poison` identifier. In LLVM this might just be a weird side-effect we don't care about, but actually having an integer overflow is a big deal in C that introduces UB. Given the introduction, LLVM (incorrectly) introduces (C) UB at times.
The second section, on pointer provenance, is much trickier, as there's no "obvious" UB introduced there. Further, I would argue that pointer provenance is a meta-language (or meta-computational) concept (which the Rust docs hint at), and logically speaking, might be intractable in the general case (I'd have to think about this more). Pointer arithmetic can fiddle with meta-state, whereas IRs like LLVM tend to focus purely on symbol manipulation.
As a side note, I'd be curious what happens when LLVM sees something like: `void *p = &p` which is a self-referential pointer. What does it deduce about it? Does it optimize it away?
Cool thought-provoking article.
Re: Pointers Are Complicated II, or: We need better language specs
#9Does this have implications about the safety guarantees even safe Rust can make? It seems like incorrect optimization passes could result in bugs/security issues that are a byproduct of the compiler rather than the language itself. I wonder how big of an issue this is for Rust (relatively probably a bigger issue than for C/C++ where basic resource ownership bugs are more common).
It’s enough of an issue for C at least that a fully formally verified compiler exists: https://en.m.wikipedia.org/wiki/CompCert . That is, there’s proof that its (limited) optimisation passes are correct.
There’s other approaches to assurance of compiled code too, such as seL4 which has proofs that the binary itself is correct, I believe.
Re: Pointers Are Complicated II, or: We need better language specs
#10Excellent article.
It seems to me (and this is somewhat off-the-cuff) that compilers have another option: integers which are cast from pointers have provenance.
That is, provenance is a taint: you can't clean it off through casting. So casting from pointer means the user can do integer-things like addition, but it means the compiler can't do integer-things like constant folding.