personal/_posts/2017-06-06-MIR-semantics.md

   1 ---
   2 title: Exploring MIR Semantics through miri
   3 categories: internship rust
   4 reddit: /rust/comments/6fqzub/exploring_mir_semantics_through_miri/
   5 ---
   6
   7 It's now been two weeks since my internship started (two weeks already, can you believe it?).
   8 In other words, if I want to post "weekly or bi-weekly" updates, I better write one today ;) .
   9
  10 As [already mentioned]({% post_url
  11 2017-05-23-internship-starting %}), the goal for this internship is to
  12 experiment with
  13 [unsafe code guidelines](https://internals.rust-lang.org/t/next-steps-for-unsafe-code-guidelines/3864)
  14 by implementing them in [miri](https://github.com/solson/miri).  Before I tackle that, however,
  15 it seemed sensible for me to grab some low-hanging fruit in miri just to make
  16 myself familiar with the codebase.  It turns out I entered "unsafe code
  17 guidelines" territory much quicker than expected.
  18 This post is about what I found, and it also serves as a nice demonstration of how we envision my unsafe code guidelines workflow to look like.
  19 <!-- MORE -->
  20
  21 ## Live and Let Die
  22
  23 The first miri task that I took on was for miri to do something sensible with MIR's [`StorageLive` and `StorageDead` statements](https://github.com/solson/miri/issues/49).
  24 If you haven't seen these before, that's because they do not come up in Rust code; instead, `StorageLive` and `StorageDead` are inserted by the compiler.
  25 For example, the following Rust code
  26 {% highlight rust %}
  27 fn main() {
  28     let x = 13;
  29     let y = 3*x + 3;
  30 }
  31 {% endhighlight %}
  32 compiles to the following MIR (in release mode)[^1]:
  33
  34 [^1]: You can run `rustc -O --emit=mir` to reproduce this. `-O` turns on release mode, which turns off overflow checking, which makes the MIR code significantly shorter. Alternatively, you can compile Rust code to MIR on the [playground](https://play.rust-lang.org/).
  35
  36 ```
  37     bb0: {
  38         StorageLive(_1);
  39         _1 = const 13i32;               // let x = 13;
  40         StorageLive(_2);
  41         StorageLive(_3);
  42         StorageLive(_4);
  43         _4 = _1;                        // let tmp_4 = x;
  44         _3 = Mul(const 3i32, _4);       // let tmp_3 = 3 * tmp_4;
  45         StorageDead(_4);
  46         _2 = Add(_3, const 3i32);       // let y = tmp_3 + x;
  47         StorageDead(_3);
  48         _0 = ();
  49         StorageDead(_2);
  50         StorageDead(_1);
  51         return;
  52     }
  53 ```
  54 That's quite verbose, but you can still see our little test program in there: There's a `const 13i32`, there's a `Mul` by `3i32`, and there's an `Add` with `3i32`.
  55 The surrounding `bb0` hints at the fact that MIR is a language built around [basic blocks](https://en.wikipedia.org/wiki/Basic_block).
  56 That's not really relevant right now, so we'll gloss over this.
  57
  58 What *is* relevant is that the MIR code contains all these extra statements we did not write, all these `StorageLive(...)` and `StorageDead(...)`.
  59 They indicate when a variable is *live*, i.e., when the value of a variable is relevant for the program execution.
  60 For example, the compiler marks `_4` as dead right after the multiplication.
  61 `_4` is not used again by the program, so there is no point in keeping its value around.
  62
  63 Liveness information is important because it is forwarded to LLVM, which then uses this information to allocate variables into stack slots.
  64 If two variables are never live at the same time, the compiler can assign both of them the *same* slot, which is great because it makes the stack frame smaller.
  65 To this end, rustc will translate `StorageLive` to [`llvm.lifetime.start`](http://llvm.org/docs/LangRef.html#llvm-lifetime-start-intrinsic) and `StorageDead` to [`llvm.lifetime.end`](http://llvm.org/docs/LangRef.html#llvm-lifetime-end-intrinsic).
  66 These are intrinsics that LLVM understands and takes into account when computing the layout of the stack frame.
  67
  68 ## Giving It Semantics
  69
  70 Now, the trouble is:  How do we know if rustc made a mistake when it added the liveness information?
  71 That would be bad, because it could lead to miscompilation.
  72 However, to figure out whether the information is "wrong", we first have to find a definition of what it means for the information to be "right".
  73 You may think that's obvious: Just make sure that every access to a variable is after the `StorageLive`, and before the `StorageDead`, done -- right?
  74 Unfortunately, it's not always so easy.  What if we say `StorageLive` twice on the same variable, is that allowed?  What if there is a `StorageLive` in a loop?
  75
  76 One way to give a definite answer to all such questions is to give these annotations an actual *behavior*, i.e., to give them *semantics*.
  77 When the program above runs, we actually imagine that every local variable comes with an additional bit storing whether the variable is currently live, and `StorageLive` and `StorageDead` modify said bit.
  78 When a variable is accessed, we can check that bit to make sure the variable is currently live.
  79 And we can actually *implement* this behavior, so that questions like the ones I raised above can be answered by just executing programs that do these things, and see what happens.
  80 So that's exactly what I did:  I [extended miri](https://github.com/solson/miri/pull/176) to no longer just ignore `StorageLive` and `StorageDead`, but instead keep track of liveness of all local variables.
  81
  82 It is in the implementation of `StorageLive` that the aforementioned questions come up:  When we see `StorageLive` on a variable that *already is live*, what do we do?
  83 We have three options (well, I am sure we have more, but these are the three I considered):
  84 1. Do nothing.  The variable is already live, it is marked live again, so we are good.
  85 2. Bail out.  Marking something as live *twice* is bogus, MIR programs should not do that.
  86 3. Forget the value that is currently in the local variable, but otherwise keep it live.
  87
  88 ## LLVM Chiming In
  89
  90 I started out with the first option.
  91 However, it turns out that's a bad choice.
  92 The trouble is, we are not entirely unconstrained in what we allow and forbid.
  93 After all, `StorageLive` and `StorageDead` are compiled into LLVM intrinsics, and LLVM has some rules for what these intrinsics mean and when they are allowed to be used -- and when not.
  94 Here's what the [LLVM specification of `llvm.lifetime.start`](http://llvm.org/docs/LangRef.html#llvm-lifetime-start-intrinsic) has to say:
  95
  96 > This intrinsic indicates that before this point in the code, the value of the memory pointed to by `ptr` is dead. This means that it is known to never be used and has an undefined value. A load from the pointer that precedes this intrinsic can be replaced with `undef`.
  97
  98 Unfortunately, this is rather short and does not cover lots of interesting questions.
  99 For example: Is it allowed to mark a variable as live, and then dead, and then live again?
 100 The text somewhat reads like it is not, but that would make it illegal to use these intrinsics in a loop, which is probably not the intended meaning.
 101 Such imprecision in natural language specifications is the entire reason why we also want to have an *executable* specification of Rust.
 102 (This is not to say that natural language specifications are useless. Ideally, you have them both.)
 103
 104 Anyway, what does seem clear from this specification is that adding a redundant `StorageLive` at the wrong place can have bad side-effects, like make preceding loads yield `undef`.
 105 We'd rather not have that happen in code produced by rustc.
 106 To guarantee this doesn't happen, we should define the semantics of these MIR statements such that they forbid redundant `StorageLive`.
 107 As a consequence of this, we can be sure that if we start with a "valid" MIR program -- a program that does not execute forbidden instructions, like a redundant `StorageLive` -- then the resulting LLVM will also be "valid".
 108
 109 Executing such bad instructions is often referred to as the program having "undefined behavior".
 110 The reason for this is that we just don't want to talk about the possible behaviors of such programs, we just give the compiler the license to do whatever.
 111 For this reason, it is crucially important that the programs we care about do *not* have undefined behavior (or, for short: UB).
 112
 113 How is making `StorageLive` UB helpful, you may wonder?  Didn't we just shift the problem from rustc producing invalid LLVM to rustc producing invalid MIR?
 114 In a sense, that's true, but I would still argue this is helpful.
 115 First of all, it is now clear where the bug (if there is one) has to be fixed:
 116 The pass that lowers HIR to MIR should make sure that it emits liveness annotations that match MIR's rules.
 117 All the passes that transform MIR (e.g. to optimize it) have a clear idea of what they are working against.
 118 They can all *rely* on the MIR program they get to not to have UB, and they have to *guarantee* that they do not change the program in a way that it now does have UB.
 119 Code generation from MIR to LLVM is right when it emits the aforementioned intrinsics, because all it relies on is the MIR program not having UB.
 120
 121 And, secondly, we actually now have a way to test *if* the compiler emits incorrect liveness annotations for a give piece of code:
 122 We implement the MIR rules in miri, and then we run miri on a body of representative MIR code produced by the latest compiler to see whether UB arises or not.
 123 miri's test suite is tiny compared to the body of Rust code out there, but it exercises pretty much all syntactic features of core Rust and some standard library code (mostly around `Vec` as well as all the code needed to even get a program running and to tear it down again -- there's quite a few things going on before and after your `fn main()`, but that would be a topic for another blog post).
 124 It's a good enough start.
 125
 126 So, I implemented the second of the three behaviors of `StorageLive` that I outlined above:
 127 Marking something as live *twice* is bogus, MIR programs should not do that.
 128 The reasoning here is to play safe; this is as conservative as it gets.
 129 If a program is fine under these rules, we can be fairly certain that LLVM also considers this program to be fine.
 130
 131 Of course, the inevitable happened and...
 132
 133 ## rustc Disagrees, A Compromise Arises
 134
 135 That's right, there was a test failure.
 136 It turns out rustc *does* produce code that violates the rules we picked.[^2]
 137 So, did we find a bug?
 138
 139 [^2]: In case you are curious, it was [this test](https://github.com/solson/miri/blob/ec7f1d5248fe1cee904a6d8af094167ded779781/tests/run-pass/loops.rs) that failed. Somewhat unsurprisingly, loops are involved.
 140
 141 Well, maybe.
 142 Or maybe the rules we picked were just too conservative.
 143 At this point, I ended up in a lengthy discussion with @eddyb and @arielb1 and some folks in #rustc, who know approximately infinitely more about LLVM and rustc than I do, and this is how the third option in the list arose:
 144 When performing `StorageLive` on a variable that already is live, forget the value that is currently in the local variable, but otherwise keep it live.
 145 This is consistent with what we have caught LLVM doing.
 146 It is hard to get any more definite than this.
 147 The "real" semantics of the relevant LLVM intrinsics is implicitly hidden between the lines of the LLVM code that uses these intrinsics to perform analyses.
 148 Often, not even the LLVM developers will be sure what is allowed and what is not.  (In fact, this is exactly what happened here.)
 149 This is not very satisfying, but lacking a more precise description of the LLVM semantics, this is all we can do.
 150
 151 The good news is that with this choice of MIR semantics, miri's test suite passes.
 152 We can thus be sure (well, insofar as the test suite is representative -- this will hopefully get better over time) that rustc produces code that follows our new rules.
 153
 154 ## And the Moral of This Story
 155
 156 So, what did we learn?
 157
 158 First of all, we learned that it is frustrating not to know whether a certain concrete program, with given concrete input, is actually triggering undefined behavior or not.
 159 This kind of uncertainty is even more worrying if we consider that tons and tons of code out there is compiled by LLVM -- most of it is probably fine, but still, I think we should be able to be somewhat more certain about whether the programs we write and run are actually doing what we think they do.
 160 (Because, remember -- if a program has UB, the compiler has license to do literally anything to your code, and most modern compilers are making use of this possibility without a second thought.  To be fair, they kind of have to, because all the other compilers do, and this is how they make programs go fast and win benchmarks, and this is what everybody cares about when it comes to compilers.  Sad world.)
 161 In Rust, we want to do better than this, and that's in fact the entire point of the [unsafe code guidelines](https://internals.rust-lang.org/t/next-steps-for-unsafe-code-guidelines/3864) project.
 162 If we can realize the Rust specification in miri's code (besides having a natural language description), that should get us a long way towards reducing ambiguity and gaps in our specification.
 163 For the near future, LLVM and its issues (and speed!) will still remain the pipeline, but [who knows what happens long-term](https://github.com/stoklund/cretonne)?
 164
 165 Secondly, you have seen an example of how an "instrumented machine" looks like.
 166 I didn't actually call it that way, but notice how miri now keeps track of the liveness of a local variable.
 167 That's not something that the final program does.
 168 And that's fine, because entirely ignoring all liveness information just means that programs that used to be UB, are now fully defined -- which is always a legal thing to do. (You may however lose some optimization potential on the way.)
 169 However, miri has the goal of detecting *all* liveness-related UB, and to this end, it "instruments" the program (or the execution, or the machine -- however you look at it) with additional information, additional state.
 170 This is a very common approach.
 171 It is used, for example, by valgrind to tell you when your program's memory accesses are invalid, but it is also used in formal verification of programs (in this domain, we often refer to the additional state of the instrumented machine as "logical state" or "ghost state").
 172
 173 And finally, the workflow above is actually somewhat representative of how my contribution to the unsafe code guidelines within the next few months will hopefully look like:
 174 The plan is to add additional instructions to MIR that express certain facts the compiler believes to be true (just like the liveness annotations do), and to give these instructions a semantics in miri (this will involve adding state that the actual program does not have, i.e., adding more instrumentation).
 175 There will be a tension between the semantics being "conservative enough" such that LLVM's assumptions are satisfied (for example, some of this will relate to the [`noalias`](http://llvm.org/docs/LangRef.html#noalias-and-alias-scope-metadata) flag that rustc emits), and such that rustc can perform some clever optimizations we really want it to perform, while at the same time the semantics should be "permissive enough" such that the code all the Rust developers out there write, and the MIR that rustc generates from that code, is actually permitted.
 176 There will be back and forth between various alternatives, and in the end, hopefully there will be a compromise that everybody can accept.
 177
 178 Happy safe hacking!