From 43097dfc13f5d5668769b4003a7c41a5525274bf Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 13 Nov 2018 08:51:57 +0100 Subject: [PATCH] Show first example in annotated form early --- .../_drafts/stacked-borrows-implementation.md | 35 ++++++++++++++++--- 1 file changed, 31 insertions(+), 4 deletions(-) diff --git a/personal/_drafts/stacked-borrows-implementation.md b/personal/_drafts/stacked-borrows-implementation.md index 029b0be..17c8d27 100644 --- a/personal/_drafts/stacked-borrows-implementation.md +++ b/personal/_drafts/stacked-borrows-implementation.md @@ -112,8 +112,35 @@ it is not at the top yet, we pop the stack until it is, which is easy. Now the stack is just `[Uniq(0)]`. Now we use `y` again and... blast! Its tag is not on the stack. We have undefined behavior. -Well, actually that is good news, since that's what we wanted from the start! -And since there is an implementation of the model in +In case you got lost, here is the source code with comments indicating the tags +and the stack of the one location that interests us: + +{% highlight rust %} +fn demo0() { + let x = &mut 1u8; // tag: `Uniq(0)` + // stack: [Uniq(0)] + + let y = &mut *x; // tag: `Uniq(1)` + // stack: [Uniq(0), Uniq(1)] + + // Pop until `Uniq(1)`, the tag of `y`, is on top of the stack: + // Nothing changes. + *y = 5; + // stack: [Uniq(0), Uniq(1)] + + // Pop until `Uniq(0)`, the tag of `x`, is on top of the stack: + // We pop `Uniq(1)`. + *x = 3; + // stack: [Uniq(0)] + + // Pop until `Uniq(1)`, the tag of `y`, is on top of the stack: + // That is not possible, hence we have undefined behavior. + let _val = *y; +} +{% endhighlight %} + +Well, actually having undefined behavior here is good news, since that's what we +wanted from the start! And since there is an implementation of the model in [miri](https://github.com/solson/miri/), you can try this yourself: The amazing @shepmaster has integrated miri into the playground, so you can [put the example there](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=d15868687f79072688a0d0dd1e053721) @@ -225,8 +252,8 @@ pub struct Stack { Let us now look at what happens when we execute our two example programs. To this end, I will embed comments in the source code. There is only one location -of interest here, so whenever I talk about a "stack", it's the stack of that -location. +of interest here, so whenever I talk about a "stack", I am referring to the +stack of that location. {% highlight rust %} fn demo1() { -- 2.30.2