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.

Sign up for GitHub

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

Jump to bottom

ICE with pretty printing macro expanded auto_serialized tuples #3250

Closed
erickt opened this issue Aug 22, 2012 · 3 comments
Closed

ICE with pretty printing macro expanded auto_serialized tuples #3250

erickt opened this issue Aug 22, 2012 · 3 comments
Labels
A-pretty Area: Pretty printing (including `-Z unpretty`) A-syntaxext Area: Syntax extensions I-ICE Issue: The compiler panicked, giving an Internal Compilation Error (ICE) ❄️
Milestone
0.6

Comments

@erickt
Copy link
Contributor

erickt commented Aug 22, 2012

I've put an example and stack trace in this gist: https://gist.github.com/3426928.
@dbp
Copy link
Contributor

dbp commented Aug 22, 2012

I'm going to take a look at it. The error is in this assertion:
assert arm.body.node.stmts.is_empty();

erickt has a workaround: https://gist.github.com/3428070

But possibly it will be better to get the AST structure to actually be the same. I don't know how macros work, so I'm not sure if they are doing their own AST generation (in which case, maybe auto_serialize needs to be changed), or if something more subtle is going on.

@catamorphism
Copy link
Contributor

Can't reproduce with b865b4b -- I assume it got accidentally fixed since the auto-serializer has changed a bit over the past 4 months :-)

This does sound like #3121 (which is still open), though.

@catamorphism
Copy link
Contributor

Added the test case ( test/run-pass/issue-3250.rs )

tedhorst pushed a commit to tedhorst/rust that referenced this issue Dec 22, 2012
@catamorphism
tests: Add test case. Closes rust-lang#3250
5c6e928
catamorphism added a commit that referenced this issue Dec 25, 2012
@catamorphism
tests: Add test case. Closes #3250
d722217
bors pushed a commit to rust-lang-ci/rust that referenced this issue May 15, 2021
@topecongiro
Merge pull request rust-lang#3250 from scampi/issue3229
d1c7afe 
version-gate the trailing semicolon change of return statements inside a match arm
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Jul 29, 2024
@adpaco-aws
Add a #[derive(Invariant)] macro (rust-lang#3250)
5c7cd63 
This PR adds a `#[derive(Invariant)]` macro for structs which allows
users to automatically derive the `Invariant` implementations for any
struct. The derived implementation determines the invariant for the
struct as the conjunction of invariants of its fields. In other words,
the invariant is derived as `true && self.field1.is_safe() &&
self.field2.is_safe() && ..`.

For example, for the struct

```rs
#[derive(kani::Invariant)]
struct Point<X, Y> {
    x: X,
    y: Y,
}
```

we derive the `Invariant` implementation as

```rs
impl<X: kani::Invariant, Y: kani::Invariant> kani::Invariant for Point<X, Y> {
    fn is_safe(&self) -> bool {
        true && self.x.is_safe() && self.y.is_safe()
    }
}
```

Related rust-lang#3095
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Jul 29, 2024
@adpaco-aws
Enable an #[safety_constraint(...)] attribute helper for the `Arbit…
7ad4d1c 
…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
Assignees
No one assigned
Labels
A-pretty Area: Pretty printing (including `-Z unpretty`) A-syntaxext Area: Syntax extensions I-ICE Issue: The compiler panicked, giving an Internal Compilation Error (ICE) ❄️
Projects
None yet
Milestone
0.6
Development

No branches or pull requests
3 participants
@erickt @catamorphism @dbp