forum: https://internals.rust-lang.org/t/types-as-contracts/5562
---
-Over the last couple of weeks of my [internship]({{ site.baseurl }}{% post_url
+Over the last couple of weeks of my [internship]({% post_url
2017-05-23-internship-starting %}), I have been working on a proposal for the "Unsafe Code Guidelines".
I got some very encouraging feedback at the [Mozilla All-Hands](https://internals.rust-lang.org/t/recapping-this-weeks-mozilla-all-hands/5465),
and now I'd like to put this proposal out there and start having a discussion.
<!-- MORE -->
Warning: Long post is long. You have been warned.
-If you need more context on this topic, I suggest you read my post on [unsafe code guidelines and undefined behavior]({{ site.baseurl }}{% post_url 2017-07-14-undefined-behavior %}) first.
+If you need more context on this topic, I suggest you read my post on [unsafe code guidelines and undefined behavior]({% post_url 2017-07-14-undefined-behavior %}) first.
## 1 It's in the Types
## 2 Specification Framework
-I have [previously written about my thoughts on undefined behavior]({{ site.baseurl }}{% post_url 2017-07-14-undefined-behavior %}):
+I have [previously written about my thoughts on undefined behavior]({% post_url 2017-07-14-undefined-behavior %}):
> I also think that tooling to *detect* UB is of paramount importance [...].
In fact, specifying a dynamic UB checker is a very good way to specify UB!
Following this, I will in the following describe how we could check the contracts expressed by Rust's types for violations.
I am considering a MIR program; if a Rust program is supposed to be checked, it has to be translated to MIR first.
-(You can [read up on my explanation]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}) of why I think this is a good way to proceed.)
-The validation of reference types (in particular, their exclusive / read-only nature) will need some extra "instrumented" state -- also see [this previous post on the topic]({{ site.baseurl }}{% post_url 2017-06-06-MIR-semantics %}).[^1]
+(You can [read up on my explanation]({% post_url 2017-05-23-internship-starting %}) of why I think this is a good way to proceed.)
+The validation of reference types (in particular, their exclusive / read-only nature) will need some extra "instrumented" state -- also see [this previous post on the topic]({% post_url 2017-06-06-MIR-semantics %}).[^1]
The extra state in my proposal consists of something akin to a reader-writer lock for every memory location.
I am first going to describe these locks and how they affect program behavior, before explaining contract validation.
If a function takes an `x: &Cell<i32>`, following the rules above, it will acquire a read lock of `*x` for the duration of the function call, making `*x` immutable.
Clearly, we do not want to do that -- calling `x.set` *will* actually mutate `*x`, and mutating through a shared reference is exactly the point of using `Cell`!
-Lucky enough, the compiler *already* says that interior mutability is only allowed via [`UnsafeCell`](https://doc.rust-lang.org/beta/core/cell/struct.UnsafeCell.html).
+Lucky enough, the compiler *already* says that interior mutability is only allowed via [`UnsafeCell`](https://doc.rust-lang.org/stable/core/cell/struct.UnsafeCell.html).
We can use this for our purposes: To adjust validation for interior mutability, we *stop* our recursive descent and do not do anything when reaching an `UnsafeCell` *while `mutbl` indicates we are in immutable mode* -- `&mut UnsafeCell` is not affected.
In particular, no locks are acquired.
This justifies calling `set` on a shared reference and having the value changed.
projects / web.git / blobdiff