add Coq typeclass index problem draft

[web.git] / personal / _posts / 2017-06-06-MIR-semantics.md

diff --git a/personal/_posts/2017-06-06-MIR-semantics.md b/personal/_posts/2017-06-06-MIR-semantics.md
index 13f51dbf52059be34db8b51eadecd09dde9d3cec..4221da5dac3cbe058c4b9043b98f7fa091b84912 100644 (file)
--- a/personal/_posts/2017-06-06-MIR-semantics.md
+++ b/personal/_posts/2017-06-06-MIR-semantics.md
@@ -7,7 +7,7 @@ reddit: /rust/comments/6fqzub/exploring_mir_semantics_through_miri/
 It's now been two weeks since my internship started (two weeks already, can you believe it?).
 In other words, if I want to post "weekly or bi-weekly" updates, I better write one today ;) .
 
 It's now been two weeks since my internship started (two weeks already, can you believe it?).
 In other words, if I want to post "weekly or bi-weekly" updates, I better write one today ;) .
 

-As [already mentioned]({{ site.baseurl }}{% post_url
+As [already mentioned]({% post_url

 2017-05-23-internship-starting %}), the goal for this internship is to
 experiment with
 [unsafe code guidelines](https://internals.rust-lang.org/t/next-steps-for-unsafe-code-guidelines/3864)
 2017-05-23-internship-starting %}), the goal for this internship is to
 experiment with
 [unsafe code guidelines](https://internals.rust-lang.org/t/next-steps-for-unsafe-code-guidelines/3864)


@@ -20,8 +20,8 @@ This post is about what I found, and it also serves as a nice demonstration of h
 
 ## Live and Let Die
 
 
 ## Live and Let Die
 

-The first miri task that I took on was for miri to do something sensible with MIR's [`StroageLive` and `StroageDead` statements](https://github.com/solson/miri/issues/49).
-If you haven't seen these before, that's because they do not come up in Rust code; instead, `StroageLive` and `StroageDead` are inserted by the compiler.
+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).
+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.

 For example, the following Rust code
 {% highlight rust %}
 fn main() {
 For example, the following Rust code
 {% highlight rust %}
 fn main() {


@@ -62,7 +62,7 @@ For example, the compiler marks `_4` as dead right after the multiplication.
 
 Liveness information is important because it is forwarded to LLVM, which then uses this information to allocate variables into stack slots.
 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.
 
 Liveness information is important because it is forwarded to LLVM, which then uses this information to allocate variables into stack slots.
 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.

-To this end, rustc will translate `StorageLive` to [`llvm.lifetime.start`](http://llvm.org/docs/LangRef.html#llvm-lifetime-start-intrinsic) and `StroageDead` to [`llvm.lifetime.end`](http://llvm.org/docs/LangRef.html#llvm-lifetime-end-intrinsic).
+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).

 These are intrinsics that LLVM understands and takes into account when computing the layout of the stack frame.
 
 ## Giving It Semantics
 These are intrinsics that LLVM understands and takes into account when computing the layout of the stack frame.
 
 ## Giving It Semantics


@@ -140,7 +140,7 @@ So, did we find a bug?
 
 Well, maybe.
 Or maybe the rules we picked were just too conservative.
 
 Well, maybe.
 Or maybe the rules we picked were just too conservative.

-At this point, I ended up in a lengthy discussion with @eddyb and @arielb1, who both know approximately infinitely more about LLVM and rustc than I do, and this is how the third option in the list arose:
+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:

 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.
 This is consistent with what we have caught LLVM doing.
 It is hard to get any more definite than this.
 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.
 This is consistent with what we have caught LLVM doing.
 It is hard to get any more definite than this.


@@ -151,7 +151,7 @@ This is not very satisfying, but lacking a more precise description of the LLVM
 The good news is that with this choice of MIR semantics, miri's test suite passes.
 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.
 
 The good news is that with this choice of MIR semantics, miri's test suite passes.
 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.
 

-## And the moral of this story
+## And the Moral of This Story

 
 So, what did we learn?
 
 
 So, what did we learn?