-
Notifications
You must be signed in to change notification settings - Fork 13.1k
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
Comments
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:
|
@pcwalton 's example no longer works since the
I don't know if that's right or not. |
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 |
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. |
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). |
Dup of issue #3696, I think. |
moving out sched_getaffinity interception from linux'shim, FreeBSD su… …pporting it too.
…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
Test case:
Errors:
If the functions become inline lambdas, the problem goes away.
@nikomatsakis, any ideas?
The text was updated successfully, but these errors were encountered: