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

Unconstrained region variables when making str-ptr-ptr hash and eq #3283

Closed
pcwalton opened this issue Aug 26, 2012 · 6 comments
Closed

Unconstrained region variables when making str-ptr-ptr hash and eq #3283

pcwalton opened this issue Aug 26, 2012 · 6 comments
Labels
A-lifetimes Area: Lifetimes / regions
Milestone

Comments

@pcwalton
Copy link
Contributor

Test case:

pure fn view_hash(s: & &str) -> uint {
    hash::hash_str(*s) as uint
}

pure fn view_eq(a: & &str, b: & &str) -> bool {
    str::eq_slice(*a, *b)
}

fn main() {
    let map = send_map::linear::linear_map(view_hash, view_eq);
    map.insert("foo", ());
}

Errors:

/home/pcwalton/Source/rust/build/test.rs:11:58: 11:65 error: Unconstrained region variable #3
/home/pcwalton/Source/rust/build/test.rs:11         let map = send_map::linear::linear_map(view_hash, view_eq);
                                                                                                      ^~~~~~~
/home/pcwalton/Source/rust/build/test.rs:11:58: 11:65 error: Unconstrained region variable #4
/home/pcwalton/Source/rust/build/test.rs:11         let map = send_map::linear::linear_map(view_hash, view_eq);

If the functions become inline lambdas, the problem goes away.

@nikomatsakis, any ideas?

@bblum
Copy link
Contributor

bblum commented Aug 26, 2012

I was fiddling around with regioned stack closures, trying to see if it'd ever mean something to return one, and ran into the same error for the first time:

fn foo(+blk: fn(+p: &a/fn() -> &a/fn())) {
    let mut state = 0;
    let statep = &mut state;
    do blk {
        || { *statep = 1; }
    }
}
fn main() {
    do foo |p| { p()() }
}


frames.rs:1:0: 1:0 error: Unconstrained region variable #8
frames.rs:1 fn foo(+blk: fn(+p: &a/fn() -> &a/fn())) {
            ^
frames.rs:1:0: 1:0 error: Unconstrained region variable #10
frames.rs:1 fn foo(+blk: fn(+p: &a/fn() -> &a/fn())) {
            ^

@catamorphism
Copy link
Contributor

@pcwalton 's example no longer works since the linear_map function being used is now trait-based, rather than taking functions explicitly. I get a different error with @bblum's example:

/Users/tchevalier/rust2/src/test/run-pass/issue-3283.rs:4:11: 6:5 error: mismatched types: expected `&fn()` but found `@fn()` (expected & closure, found @ closure)
/Users/tchevalier/rust2/src/test/run-pass/issue-3283.rs:4     do blk {
/Users/tchevalier/rust2/src/test/run-pass/issue-3283.rs:5         || { *statep = 1; }
/Users/tchevalier/rust2/src/test/run-pass/issue-3283.rs:6     }

I don't know if that's right or not.

@catamorphism
Copy link
Contributor

bblum's example compiles now (if you add a & before the fn type of blk), and pcwalton's example won't compile now for other reasons. So I'm considering this done. Reopen if you have a repro case

@catamorphism
Copy link
Contributor

bblum's example compiled and ran just fine on my Mac, but segfaulted on the Linux and Windows bots. I don't have time right now to figure out why, so I'm checking it in xfailed.

@nikomatsakis
Copy link
Contributor

I think this system should not type check. This is probably a bug in how we are handling region closures (I know there is work to be done there, not sure what bug #, let me fish it up).

@nikomatsakis
Copy link
Contributor

Dup of issue #3696, I think.

RalfJung pushed a commit to RalfJung/rust that referenced this issue Feb 17, 2024
moving out sched_getaffinity interception from linux'shim, FreeBSD su…

…pporting it too.
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Jul 29, 2024
…rary` and `Invariant` macros (rust-lang#3283)

This PR enables an `#[safety_constraint(...)]` attribute helper for the
`#[derive(Arbitrary)]` and `#[derive(Invariant)]` macro.

For the `Invariant` derive macro, this allows users to derive more
sophisticated invariants for their data types by annotating individual
named fields with the `#[safety_constraint(<cond>)]` attribute, where
`<cond>` represents the predicate to be evaluated for the corresponding
field. In addition, the implementation always checks `#field.is_safe()`
for each field.

For example, let's say we are working with the `Point` type from rust-lang#3250
```rs
#[derive(kani::Invariant)]
struct Point<X, Y> {
    x: X,
    y: Y,
}
```

and we need to extend it to only allow positive values for both `x` and
`y`.
With the `[safety_constraint(...)]` attribute, we can achieve this
without explicitly writing the `impl Invariant for ...` as follows:

```rs
#[derive(kani::Invariant)]
struct PositivePoint {
    #[safety_constraint(*x >= 0)]
    x: i32,
    #[safety_constraint(*y >= 0)]
    y: i32,
}
```

For the `Arbitrary` derive macro, this allows users to derive more
sophisticated `kani::any()` generators that respect the specified
invariants. In other words, the `kani::any()` will assume any invariants
specified through the `#[safety_constraint(...)]` attribute helper.
Going back to the `PositivePoint` example, we'd expect this harness to
be successful:

```rs
#[kani::proof]
fn check_invariant_helper_ok() {
    let pos_point: PositivePoint = kani::any();
    assert!(pos_point.x >= 0);
    assert!(pos_point.y >= 0);
}
```

The PR includes tests to ensure it's working as expected, in addition to
UI tests checking for cases where the arguments provided to the macro
are incorrect. Happy to add any other cases that you feel are missing.

Related rust-lang#3095
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-lifetimes Area: Lifetimes / regions
Projects
None yet
Development

No branches or pull requests

4 participants