-
Notifications
You must be signed in to change notification settings - Fork 13.7k
Add MIR Validate statement #43403
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Add MIR Validate statement #43403
Changes from 16 commits
Commits
Show all changes
30 commits
Select commit
Hold shift + click to select a range
5264103
add new instructions for asserting when values are valid, and to desc…
RalfJung 735ace9
add a pass for validation commands; for now just emit the initial Acq…
RalfJung 33585f4
CleanEndRegions: do not clean regions that occur in types in validati…
RalfJung 82786b2
emit validation for function calls and Ref
RalfJung 24a2ac9
add_validation: handle drop
RalfJung 511b88c
only emit Suspend validation for mutable paths
RalfJung a233afa
respect lifetime rendering when rendering Suspend validation op
RalfJung 60096b9
when suspending, we need to specify for which lifetime to recover
RalfJung e869cf2
make ValidationOperand generic so that we can reuse it in miri with a…
RalfJung 23cd90e
add -Z flag for AddValidation pass
RalfJung b6816b2
please the tidy
RalfJung 04f962a
after a Ref, only acquire the Deref'd destination
RalfJung b934506
Reorder passes so that AddValidation can run after ElaborateDrops
RalfJung 7ec50df
also release/validate around non-Misc casts
RalfJung 57958d1
Add tests for emitting validation statements
RalfJung 29ed317
silence tidy
RalfJung 6641415
do not use doc comments inside functions
RalfJung 6ff7c8f
more documentation
RalfJung 6135461
CleanEndRegions: use default impl where possible
RalfJung 5e426e1
optionally only emit basic validation for functions containing unsafe…
RalfJung 09cbe58
more readable printing of validation operands
RalfJung 26ca0d1
tidy
RalfJung e73d314
fix AddValidation on methods
RalfJung 584d823
Handle closures. Add some more tests.
RalfJung 4310edb
handle tuple struct ctors
RalfJung 8f910bc
handle trait items as well
RalfJung c5154d0
use FnLike to recognize functions for us
RalfJung a8129d1
add a closure inside an unsafe fn to the tests
RalfJung 321a72c
closure unsafety check: stop moving up when we hit an item
RalfJung 7d8dc7a
also release-validate return value before a call
RalfJung File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -25,7 +25,7 @@ use ty::{self, AdtDef, ClosureSubsts, Region, Ty}; | |
use ty::fold::{TypeFoldable, TypeFolder, TypeVisitor}; | ||
use util::ppaux; | ||
use rustc_back::slice; | ||
use hir::InlineAsm; | ||
use hir::{self, InlineAsm}; | ||
use std::ascii; | ||
use std::borrow::{Cow}; | ||
use std::cell::Ref; | ||
|
@@ -818,12 +818,16 @@ pub enum StatementKind<'tcx> { | |
/// End the current live range for the storage of the local. | ||
StorageDead(Lvalue<'tcx>), | ||
|
||
/// Execute a piece of inline Assembly. | ||
InlineAsm { | ||
asm: Box<InlineAsm>, | ||
outputs: Vec<Lvalue<'tcx>>, | ||
inputs: Vec<Operand<'tcx>> | ||
}, | ||
|
||
/// Assert the given lvalues to be valid inhabitants of their type. | ||
Validate(ValidationOp, Vec<ValidationOperand<'tcx, Lvalue<'tcx>>>), | ||
|
||
/// Mark one terminating point of an extent (i.e. static region). | ||
/// (The starting point(s) arise implicitly from borrows.) | ||
EndRegion(CodeExtent), | ||
|
@@ -832,13 +836,56 @@ pub enum StatementKind<'tcx> { | |
Nop, | ||
} | ||
|
||
#[derive(Copy, Clone, RustcEncodable, RustcDecodable, PartialEq, Eq)] | ||
pub enum ValidationOp { | ||
Acquire, | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Can we document at least a bit the semantics of each of these operations in doc comment form? |
||
Release, | ||
Suspend(CodeExtent), | ||
} | ||
|
||
impl Debug for ValidationOp { | ||
fn fmt(&self, fmt: &mut Formatter) -> fmt::Result { | ||
use self::ValidationOp::*; | ||
match *self { | ||
Acquire => write!(fmt, "Acquire"), | ||
Release => write!(fmt, "Release"), | ||
// (reuse lifetime rendering policy from ppaux.) | ||
Suspend(ref ce) => write!(fmt, "Suspend({})", ty::ReScope(*ce)), | ||
} | ||
} | ||
} | ||
|
||
// This is generic so that it can be reused by miri | ||
#[derive(Clone, RustcEncodable, RustcDecodable)] | ||
pub struct ValidationOperand<'tcx, T> { | ||
pub lval: T, | ||
pub ty: Ty<'tcx>, | ||
pub re: Option<CodeExtent>, | ||
pub mutbl: hir::Mutability, | ||
} | ||
|
||
impl<'tcx, T: Debug> Debug for ValidationOperand<'tcx, T> { | ||
fn fmt(&self, fmt: &mut Formatter) -> fmt::Result { | ||
write!(fmt, "{:?}@{:?}", self.lval, self.ty)?; | ||
if let Some(ce) = self.re { | ||
// (reuse lifetime rendering policy from ppaux.) | ||
write!(fmt, "/{}", ty::ReScope(ce))?; | ||
} | ||
if let hir::MutImmutable = self.mutbl { | ||
write!(fmt, " (imm)")?; | ||
} | ||
Ok(()) | ||
} | ||
} | ||
|
||
impl<'tcx> Debug for Statement<'tcx> { | ||
fn fmt(&self, fmt: &mut Formatter) -> fmt::Result { | ||
use self::StatementKind::*; | ||
match self.kind { | ||
Assign(ref lv, ref rv) => write!(fmt, "{:?} = {:?}", lv, rv), | ||
// (reuse lifetime rendering policy from ppaux.) | ||
EndRegion(ref ce) => write!(fmt, "EndRegion({})", ty::ReScope(*ce)), | ||
Validate(ref op, ref lvalues) => write!(fmt, "Validate({:?}, {:?})", op, lvalues), | ||
StorageLive(ref lv) => write!(fmt, "StorageLive({:?})", lv), | ||
StorageDead(ref lv) => write!(fmt, "StorageDead({:?})", lv), | ||
SetDiscriminant{lvalue: ref lv, variant_index: index} => { | ||
|
@@ -1481,6 +1528,21 @@ impl<'tcx> TypeFoldable<'tcx> for BasicBlockData<'tcx> { | |
} | ||
} | ||
|
||
impl<'tcx> TypeFoldable<'tcx> for ValidationOperand<'tcx, Lvalue<'tcx>> { | ||
fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self { | ||
ValidationOperand { | ||
lval: self.lval.fold_with(folder), | ||
ty: self.ty.fold_with(folder), | ||
re: self.re, | ||
mutbl: self.mutbl, | ||
} | ||
} | ||
|
||
fn super_visit_with<V: TypeVisitor<'tcx>>(&self, visitor: &mut V) -> bool { | ||
self.lval.visit_with(visitor) || self.ty.visit_with(visitor) | ||
} | ||
} | ||
|
||
impl<'tcx> TypeFoldable<'tcx> for Statement<'tcx> { | ||
fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self { | ||
use mir::StatementKind::*; | ||
|
@@ -1505,6 +1567,10 @@ impl<'tcx> TypeFoldable<'tcx> for Statement<'tcx> { | |
// trait with a `fn fold_extent`. | ||
EndRegion(ref extent) => EndRegion(extent.clone()), | ||
|
||
Validate(ref op, ref lvals) => | ||
Validate(op.clone(), | ||
lvals.iter().map(|operand| operand.fold_with(folder)).collect()), | ||
|
||
Nop => Nop, | ||
}; | ||
Statement { | ||
|
@@ -1530,6 +1596,9 @@ impl<'tcx> TypeFoldable<'tcx> for Statement<'tcx> { | |
// trait with a `fn visit_extent`. | ||
EndRegion(ref _extent) => false, | ||
|
||
Validate(ref _op, ref lvalues) => | ||
lvalues.iter().any(|ty_and_lvalue| ty_and_lvalue.visit_with(visitor)), | ||
|
||
Nop => false, | ||
} | ||
} | ||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we could extend this comment. For example, it's worth saying that this is part of an experimental attempt at giving semantics to unsafe code, and these statements are not generated during normal MIR execution. Maybe include a link to your blog post. =)