Stream: t-lang/wg-unsafe-code-guidelines

Topic: playground miri redeploy


RalfJ (Nov 16 2018 at 09:49, on Zulip):

@Jake Goulding Could I get you to trigger a redeploy of miri on the playground? That would make it fetch an update that I'd like to be deployed when publishing a certain blog post. ;)

Jake Goulding (Nov 16 2018 at 14:27, on Zulip):

done

Jake Goulding (Nov 16 2018 at 14:27, on Zulip):

well, check the version yourself; I pushed the buttons

RalfJ (Nov 16 2018 at 15:22, on Zulip):

commit number looks identical to master, thanks <3

Jake Goulding (Nov 17 2018 at 20:42, on Zulip):

Where's the blog post @RalfJ ?

RalfJ (Nov 17 2018 at 20:43, on Zulip):

@Jake Goulding https://www.ralfj.de/blog/2018/11/16/stacked-borrows-implementation.html

RalfJ (Nov 17 2018 at 20:43, on Zulip):

been on IRLO and reddit since yesterday :)

Jake Goulding (Nov 17 2018 at 21:01, on Zulip):

I try to mostly stay away from r/rust and I'm not doing enough internals development to hang out on IRLO.

Jake Goulding (Nov 17 2018 at 21:02, on Zulip):

I just knew you had mentioned the blog post in regards to the update so I figured I'd see what's what.

Jake Goulding (Nov 17 2018 at 21:06, on Zulip):

The amazing @shepmaster has integrated miri into the playground

Aww :heart:

blitzerr (Nov 17 2018 at 23:46, on Zulip):

@RalfJ Excellent post that one. :wait_one_second:️ I will have to go over it again to fully wrap my head around it. Do you have a list of PRs that made the model possible ?

blitzerr (Nov 17 2018 at 23:57, on Zulip):

Also, rustc does not incorporate miri at this point right ? What's the plan on integrating it ?

RalfJ (Nov 18 2018 at 08:14, on Zulip):

@RalfJ Excellent post that one. :wait_one_second:️ I will have to go over it again to fully wrap my head around it. Do you have a list of PRs that made the model possible ?

I guess on the rustc side that would be
https://github.com/rust-lang/rust/pull/54461
https://github.com/rust-lang/rust/pull/54762
https://github.com/rust-lang/rust/pull/54955
https://github.com/rust-lang/rust/pull/55125
https://github.com/rust-lang/rust/pull/55270
https://github.com/rust-lang/rust/pull/55316
https://github.com/rust-lang/rust/pull/55549
https://github.com/rust-lang/rust/pull/55716
and https://github.com/rust-lang/rust/pull/55916 still waits to land

and on the miri side
https://github.com/solson/miri/pull/468
https://github.com/solson/miri/pull/473
https://github.com/solson/miri/pull/474
https://github.com/solson/miri/pull/477
https://github.com/solson/miri/pull/487
https://github.com/solson/miri/pull/492
https://github.com/solson/miri/pull/506
https://github.com/solson/miri/pull/513
https://github.com/solson/miri/pull/524
and https://github.com/solson/miri/pull/526 still waits to land

RalfJ (Nov 18 2018 at 08:14, on Zulip):

Also, rustc does not incorporate miri at this point right ? What's the plan on integrating it ?

rustc uses the miri engine for CTFE. but CTFE does not implement stacked borrows. I am not sure if there are any plans to change that -- this stuff comes with a significant performance cost.

blitzerr (Nov 18 2018 at 16:19, on Zulip):

Thanks a lot for all the info and the PR list
Even if not in rustc directly, but stacked borrow gives people a way to verify unsafe rust. And that's a great step forward. So thank you for that. @RalfJ

Gankro (Nov 19 2018 at 18:15, on Zulip):

@RalfJ so i just finished a chat with niko about NLL which touched on your stacked model. It came up that creating a raw ptr from an &mut makes all raw ptrs allowed to access the &mut's memory -- is that true even if it's dead code?

Gankro (Nov 19 2018 at 18:16, on Zulip):

e.g.

Gankro (Nov 19 2018 at 18:16, on Zulip):
mut_ref as *mut _;
*other_aliasing_ptr += 1;
Gankro (Nov 19 2018 at 18:39, on Zulip):

examples: https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=e2a61d03963423a824292b287f842fb6

RalfJ (Nov 19 2018 at 18:42, on Zulip):

is that true even if it's dead code?

No. This is completely a dynamic model, think of an instrumented execution, if a statement is not executed it has no effect.

But you seem to have a different definition of dead code, if I look at your example... it does not matter whether the result of the cast is used. It does matter whether the cast is executed.

RalfJ (Nov 19 2018 at 18:43, on Zulip):

I think this is a property (flaw?) inherent in all models that make casts have side-effects: You cannot remove them even if the result is unused.

RalfJ (Nov 19 2018 at 18:43, on Zulip):

And I doubt it is possible to get an access-based model for rust references where casts are side-effect-free.

RalfJ (Nov 19 2018 at 18:44, on Zulip):

@Gankro also see https://internals.rust-lang.org/t/types-as-contracts/5562/113?u=ralfjung

Gankro (Nov 19 2018 at 18:46, on Zulip):

yeah by "dead" I mean "otherwise pure code that could be compiled out of the final binary"

RalfJ (Nov 19 2018 at 18:46, on Zulip):

though the funny thing is that is_ub_1012A is actually not UB in my model... @nikomatsakis should it be? It is no more UB since I made [T]::iter_mut work

RalfJ (Nov 19 2018 at 18:46, on Zulip):

yeah by "dead" I mean "otherwise pure code that could be compiled out of the final binary"

escape-to-raw is not pure code :D

Gankro (Nov 19 2018 at 18:46, on Zulip):

@RalfJ also you still haven't posted that blog post yet, eh?

RalfJ (Nov 19 2018 at 18:46, on Zulip):

in the MIR this is explicit. the cast has no side-effect, it is pure, but the escape-to-raw statement that got emitted next to it is not pure

RalfJ (Nov 19 2018 at 18:47, on Zulip):

I have, even posted the here in the very topic we are talking in^^

RalfJ (Nov 19 2018 at 18:47, on Zulip):

@Gankro https://www.ralfj.de/blog/2018/11/16/stacked-borrows-implementation.html

Gankro (Nov 19 2018 at 18:47, on Zulip):

@RalfJ ah, I checked your blog's index, which lacks it :)

Gankro (Nov 19 2018 at 18:47, on Zulip):

or, wait

RalfJ (Nov 19 2018 at 18:48, on Zulip):

uh, no? https://www.ralfj.de/blog/

RalfJ (Nov 19 2018 at 18:48, on Zulip):

it's on https://www.ralfj.de/blog/feed.xml as well

Gankro (Nov 19 2018 at 18:48, on Zulip):

@RalfJ oh I followed links and ended up on https://www.ralfj.de/blog/categories/research.html

Gankro (Nov 19 2018 at 18:48, on Zulip):

shrug

RalfJ (Nov 19 2018 at 18:48, on Zulip):

ah^^

Gankro (Nov 19 2018 at 18:49, on Zulip):

@RalfJ so is the playground I linked correct?

RalfJ (Nov 19 2018 at 18:49, on Zulip):

yeah it's in the Rust category but not in Research... dunno, Research is MPI stuff^^

RalfJ (Nov 19 2018 at 18:50, on Zulip):

hm seems like the edition switch isnt propagated to miri, example1 dosn't compile

RalfJ (Nov 19 2018 at 18:52, on Zulip):

@Gankro yes that looks all right, and if you run it in miri it agrees^^

Gankro (Nov 19 2018 at 18:52, on Zulip):

sweet

RalfJ (Nov 19 2018 at 18:52, on Zulip):

it points out exactly the two lines you marked UB

RalfJ (Nov 19 2018 at 18:52, on Zulip):

and I'll need to ask @Jake Goulding about the edition

RalfJ (Nov 19 2018 at 18:53, on Zulip):

where only the top of the stack is the valid path

@Gankro that's not correct or at least not how I'd put it. Every item on the stack is valid to use. But using one invalidates everything further up the stack.

Gankro (Nov 19 2018 at 18:54, on Zulip):

Sure

Gankro (Nov 19 2018 at 18:54, on Zulip):

I handled that by suggesting accessing A "pops" everything above it implicitly

Jake Goulding (Nov 19 2018 at 18:54, on Zulip):

@RalfJ If I'm reading correctly, You are saying that setting the edition to 2018 doesn't affect running Miri? Mind filing an issue if so?

Jake Goulding (Nov 19 2018 at 18:55, on Zulip):

I wonder how rustfmt and clippy handle the edition...

RalfJ (Nov 19 2018 at 18:55, on Zulip):

@Jake Goulding I was literally filing the issue while you posted :) https://github.com/integer32llc/rust-playground/issues/429

RalfJ (Nov 19 2018 at 18:56, on Zulip):

I wonder how rustfmt and clippy handle the edition...

clippy on playground has the same problem

RalfJ (Nov 19 2018 at 18:57, on Zulip):

when using miri directly I think you just have to pass --edition

RalfJ (Nov 19 2018 at 18:57, on Zulip):

I guess cargo miri should do that based on what it says in the Cargo.toml?

RalfJ (Nov 19 2018 at 18:57, on Zulip):

I wonder if cargo provides a nice API for that

Last update: Nov 20 2019 at 13:15UTC