Skip to content
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

[NLL] extend MIR type checker to check aggregate rvalues #45889

Closed
nikomatsakis opened this issue Nov 9, 2017 · 3 comments
Closed

[NLL] extend MIR type checker to check aggregate rvalues #45889

nikomatsakis opened this issue Nov 9, 2017 · 3 comments
Labels
E-mentor Call for participation: This issue has a mentor. Use #t-compiler/help on Zulip for discussion. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.

Comments

@nikomatsakis
Copy link
Contributor

nikomatsakis commented Nov 9, 2017

Once #45825 lands, we will be using the MIR type checker to drive the NLL region checker. This means we'll have to fix a few omissions. One of them is that MIR type checker does not check MIR rvalues (expressions that construct a value) for internal validity.

Here is an example NLL program affected by this:

#![allow(unused_assignments)]

struct Wrap<'a> { w: &'a mut u32 }

fn foo() {
    let mut x = 22;
    let wrapper = Wrap { w: &mut x };
    x += 1;
    *wrapper.w += 1;
}

fn main() { }

If you run this with -Znll -Zborrowck-mir, you'll see that it emits just one error, tagged with (Ast):

error[E0506]: cannot assign to `x` because it is borrowed (Ast)
 --> /home/nmatsakis/tmp/mir-rvalue.rs:8:5
  |
7 |     let wrapper = Wrap { w: &mut x };
  |                                  - borrow of `x` occurs here
8 |     x += 1;
  |     ^^^^^^ assignment to borrowed `x` occurs here

This error indicates that the old borrow checker is reporting an error, but we would expect both the old and new borrow check to report an error.

What's going wrong here is as follows:

  • The Wrap { w: &mut x } expression introduces a region variable '?0 representing the region parameter of Wrap. You can think of it like Wrap::<'?0> { w: &mut x }.
  • For the struct expression to be well-typed, then, we ought to check that the expected type E of each field (as taken from the struct declaration) is a supertype of the type V of the value assigned to it (in other words, that V <: E).
    • Here, the expected type would be &'?0 mut u32, and the type V would be the type &'?1 mut u32, where '?1 that is the lifetime of the borrow. Hence you would have &'?1 u32 <: &'?0 u32, which in turn means '?1: '?0.
    • However, the current MIR type-checker does not generate such a constraint, so we wind up with no relation between '?0 and '?1.

The reason why is not hard to see. The MIR type checker's "main loop" is right here:

for block in mir.basic_blocks() {
for stmt in &block.statements {
if stmt.source_info.span != DUMMY_SP {
self.last_span = stmt.source_info.span;
}
self.check_stmt(mir, stmt);
}
self.check_terminator(mir, block.terminator());
self.check_iscleanup(mir, block);
}

It basically invokes check_stmt on every MIR statement. In this case, the statement in question will be an assignment statement. You can see that yourself if you run with -Zverbose -Zmir-dump='foo&nll' (in addition to the other options) and open the resulting NLL file (it will generate a lot of files; the you want is rustc.node12.-------.nll.0.mir). The interesting statement is this one, the 7th statement in bb0 (written bb0[7]):

        _2 = Wrap<'_#2r> { w: _3 };

Here we have an assignment statement, with the lvalue (left-hand side) being the variable _2 and the rvalue (right-hand side) being Wrap<'_#2r> { w: _3 }. This is a struct aggregate rvalue. If we look then at the types of the variables _2 and _3, we see:

let _2: Wrap<'_#5r>;
let mut _3: &'_#6r mut u32;

Right now, what check_stmt does for an assignment statement is to compute the type of the rvalue and check that it is a subtype of the lvalue:

StatementKind::Assign(ref lv, ref rv) => {
let lv_ty = lv.ty(mir, tcx).to_ty(tcx);
let rv_ty = rv.ty(mir, tcx);
if let Err(terr) = self.sub_types(rv_ty, lv_ty) {
span_mirbug!(self, stmt, "bad assignment ({:?} = {:?}): {:?}",
lv_ty, rv_ty, terr);
}
}

The type of the rvalue here will be Wrap<'_#2r>, so we will get a relationship '_#2r: '_#5r (this '_# is the compiler's way of printing a region variable; equivalent to the '? I was using). But we get no relation to the type of _3.

So we need to add some kind of function check_rvalue, and call it here. It would visit the inside of an rvalue and make sure its types are internally consistent. I think that for the purposes of this bug, it would only handle aggregate rvalues, we can add other cases later.

The first step we need to do for this case is to compute the expected types of all the fields, based on the field declaration. There is actually code to do this already. The sanitize_projection method has the job of checking that a path like a.b has a valid type. To do that, it must lookup the type of b and check it. This is done by invoking the field_ty method, defined on TypeVerifier. (The type verifier is kind of like a little pre-pass; it checks that some basic assumptions are met before the type-checker proper runs.)

There is no reason for this method to be confined to TypeVerified; it should be easy enough to promote to the TypeChecker (the verifier can then invoke it via self.cx.field_ty instead).

Once that method has been moved, our check_rvalue method can invoke it to find the types of each field in the aggregate, and then can invoke sub_types on the actual type of the operand.

So, the complete set of steps:

  • Promote field_ty onto the TypeChecker
  • Introduce check_rvalue method, leaving cases largely unhandled
  • For aggregate, use field_ty to check the relationship between the operand provided and the field's expected type
  • Done.

Once we've finished this, there is more to do. For example, we need to check that the various where clauses declared on the type are met, and handle other kinds of rvalues. But I'm going to defer those to other issues. (Predicates, for example, are #45827)

@nikomatsakis nikomatsakis added E-mentor Call for participation: This issue has a mentor. Use #t-compiler/help on Zulip for discussion. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. WG-compiler-nll labels Nov 9, 2017
@nikomatsakis
Copy link
Contributor Author

This should probably be done based off my branch from #45889, as the MIR type checker has changed somewhat.

@Nashenas88
Copy link
Contributor

I volunteer to take this one :-)

@nikomatsakis
Copy link
Contributor Author

Fixed in nikomatsakis#13.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
E-mentor Call for participation: This issue has a mentor. Use #t-compiler/help on Zulip for discussion. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.
Projects
None yet
Development

No branches or pull requests

2 participants