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

check predicates, well-formedness in the MIR type-checker #45827

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

check predicates, well-formedness in the MIR type-checker #45827

nikomatsakis opened this issue Nov 7, 2017 · 3 comments
Labels
T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.
Milestone

Comments

@nikomatsakis
Copy link
Contributor

nikomatsakis commented Nov 7, 2017

The MIR type-checker does not currently check that the predicates associated with values are met. For example, when you have a MIR rvalue that references a fn item, we should be checked that the where-clauses on that function are satisfied; similarly, we should check that when a struct rvalue is instantiated, its predicates are satisfied.

(More generally, to cope with NLL, I think we may need to ensure that the type of each variable is WF also when it is used, so that we enforce constraints at the right locations? But let's start with the basics.)

Before addressing this, we should fix #45889, which will introduce the check_rvalue method and build up a bit more infrastructure. The instructions in #45889 check that each field has a suitable type, but they don't check that the where-clauses declared on the struct are met. I'll leave some instructions here shortly once #45889 proceeds a bit further.

(Hint: a good first step is that we have to write-up a test case or 3!)

@nikomatsakis nikomatsakis added T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. WG-compiler-nll labels Nov 7, 2017
@arielb1 arielb1 added this to the NLL prototype milestone Nov 15, 2017
@SimonSapin
Copy link
Contributor

SimonSapin commented Nov 17, 2017

Has this been implemented? In b3f3390 the test case wrote (and expected to fail) passes. Or is my test not testing the right thing?

// Copyright 2017 The Rust Project Developers. See the COPYRIGHT
// file at the top-level directory of this distribution and at
// http://rust-lang.org/COPYRIGHT.
//
// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
// option. This file may not be copied, modified, or distributed
// except according to those terms.

//revisions: ast mir
//[mir] compile-flags: -Z emit-end-regions -Z borrowck-mir -Z nll

use std::cell::Cell;

fn assert_sync<T>(x: T) -> T where T: Sync { x }
struct AssertSync<T>(T) where T: Sync;

fn foo() {
    let _x = assert_sync(Cell::new(()));
    //[ast]~^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
    //[mir]~^^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
    let _x = AssertSync(Cell::new(()));
    //[ast]~^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
    //[ast]~^^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
    //[mir]~^^^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
    //[mir]~^^^^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
}

fn main() {}

(I don’t know why the same error is reported twice in the struct case, but that’s even further from the expected zero.)

@nikomatsakis
Copy link
Contributor Author

nikomatsakis commented Nov 20, 2017

Some example tests that ought not to pass. Try running them with -Znll -Zborrowck-mir. I'll update with more as I go.


#![allow(dead_code)]

fn foo<'a, 'b>(x: &'a u32, y: &'b u32) -> (&'a u32, &'b u32)
    where 'a: 'b
{
    (x, y)
}

fn bar<'a, 'b>(x: &'a u32, y: &'b u32) -> (&'a u32, &'b u32)
{
    foo(x, y)
}

fn main() { }

The problem here is that the where-clauses on foo are not being enforced by the MIR type-checker.


Another example, with structs.

#![allow(dead_code)]

use std::cell::Cell;

struct Foo<'a, 'b> where 'a: 'b {
    x: Cell<&'a u32>,
    y: Cell<&'b u32>,
}

fn bar<'a, 'b>(x: Cell<&'a u32>, y: Cell<&'b u32>) {
    Foo { x, y };
}

fn main() { }

In check_rvalue, when checking aggregate values, we need to also enforce the predicates from the aggregate.

To get those, we will want to write a helper like aggregate_field_ty. This will use predicates_of to get the predicates for the various kinds of things and then apply the appropriate substitutes. Example for ADTs:

match **ak {
    AggregateKind::Adt(def, _, substs, _) =>
        tcx.predicates_of(def).instantiate(tcx, substs),
    ...
}

bors added a commit that referenced this issue Nov 23, 2017
…ielb1

typeck aggregate rvalues in MIR type checker

This branch is an attempt to land content by @spastorino and @Nashenas88 that was initially landed on nll-master while we waited for #45825 to land.

The biggest change it contains is that it extends the MIR type-checker to also type-check MIR aggregate rvalues (at least partially). Specifically, it checks that the operands provided for each field have the right type.

It does not yet check that their well-formedness predicates are met. That is #45827. It also does not check other kinds of rvalues (that is #45959). @spastorino is working on those issues now.

r? @arielb1
@nikomatsakis
Copy link
Contributor Author

Done (in nll-master)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
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

3 participants