flux-rs / flux

Refinement Types for Rust
MIT License
648 stars 21 forks source link

Rudimentary support for dynamic trait objects #664

Closed ranjitjhala closed 3 months ago

ranjitjhala commented 3 months ago

Fixes #655

Totally ignores all the bound-vars stuff for TraitObject because I haven't understood it at all, but wanted to start iterating.

enjhnsn2 commented 3 months ago

This pr already helps a ton, although there are still some dyn trait related crashes when I try to apply it to Tock. So far, I've seen one main crash that I've minimized it down to:

struct Cow {}

trait CowContainer<'a> {
    fn get_cow(&self) -> &'a Cow;
}

pub struct CowCell<'a> {
    inner: &'a dyn CowContainer<'a>,
}

When you run flux on this code, it errors with: error: internal compiler error: crates/flux-fhir-analysis/src/conv/mod.rs:444:13: unexpected! conv_poly_dyn_trait_ref

Which points to this code: https://github.com/flux-rs/flux/blob/23c745369bec99cf6bee49dd84c8547fbeac39bc/crates/flux-fhir-analysis/src/conv/mod.rs#L438-L450

Comparing this code to other code that passes, it appears that that the problem is that the the trait being parameterized by the dyn trait has a lifetime parameter. Let me know if you need any other info

nilehmann commented 3 months ago

I'll probably have some time to look at this tomorrow

enjhnsn2 commented 3 months ago

Found one more issue: dyn traits are not implemented as possible return values. If you attempt to verify the code

trait Animal {
    fn noise(&self);
}

#[flux::trusted]
fn get_animal() -> &dyn Animal {
    unimplemented!()
}

It will error with: thread 'rustc' panicked at crates/flux-middle/src/rty/mod.rs:1160:45: not yet implemented which points to the code: https://github.com/flux-rs/flux/blob/23c745369bec99cf6bee49dd84c8547fbeac39bc/crates/flux-middle/src/rty/mod.rs#L1160

ranjitjhala commented 3 months ago

@enjhnsn2 are you sure about the second one, it seems to work fine for me:

rjhala@pozole ~/r/flux (dyn)> more tests/tests/todo/dyn02.rs 
pub trait Animal {
    fn noise(&self);
}

#[flux::trusted]
pub fn get_animal() -> &'static dyn Animal {
    unimplemented!()
}
rjhala@pozole ~/r/flux (dyn)> cargo xtask run tests/tests/todo/dyn02.rs
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.02s
     Running `target/debug/xtask run tests/tests/todo/dyn02.rs`
$ export FLUX_BUILD_SYSROOT=1
$ cargo build -p flux-rs
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.02s
$ cargo build
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.06s
ranjitjhala commented 3 months ago

@enjhnsn2 - the above two things work now, see

enjhnsn2 commented 3 months ago

pub trait Animal { fn noise(&self); }

[flux::trusted]

pub fn get_animal() -> &'static dyn Animal { unimplemented!() }

Whoops, I think I may have messed up the minimization for that one. When I was minimizing I started with tock code that pulled in the tock kernel and I think the error was in the dependency, not the minimized code. Let me try to get a better example

enjhnsn2 commented 3 months ago

Alright, I found a minimized example that triggers the error. Unfortunately its a little more complicated:

pub trait Animal {
    fn noise(&self);
}

fn apply_closure_to_animal<F>(closure: F, animal: &'static dyn Animal)
where
    F: FnOnce(&dyn Animal),
{
    closure(animal);
}

This bug isn't too frequent and is possible to work around, so I don't think you should block this pr on it.

ranjitjhala commented 3 months ago

Thanks, on it!

On Wed, Jul 24, 2024 at 10:33 AM enjhnsn2 @.***> wrote:

Alright, I found a minimized example that triggers the error. Unfortunately its a little more complicated:

pub trait Animal { fn noise(&self);} fn apply_closure_to_animal(closure: F, animal: &'static dyn Animal)where F: FnOnce(&dyn Animal),{ closure(animal);}

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/flux-rs/flux/pull/664*issuecomment-2248555787__;Iw!!Mih3wA!HMp_f3DiAmkkZyGYTraImuODudwhdIKDCrIJrm2GsTIaWArQDMIXCnEPBLprCdOC47H0ZBEGXZ2Wk2KUKDXHXJnO$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OCINCS2FSTVUEW3ZTTZN7QPNAVCNFSM6AAAAABLK6BQ4GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENBYGU2TKNZYG4__;!!Mih3wA!HMp_f3DiAmkkZyGYTraImuODudwhdIKDCrIJrm2GsTIaWArQDMIXCnEPBLprCdOC47H0ZBEGXZ2Wk2KUKF0HazE_$ . You are receiving this because you authored the thread.Message ID: @.***>

nilehmann commented 3 months ago

Alright, I found a minimized example that triggers the error. Unfortunately its a little more complicated:

pub trait Animal {
    fn noise(&self);
}

fn apply_closure_to_animal<F>(closure: F, animal: &'static dyn Animal)
where
    F: FnOnce(&dyn Animal),
{
    closure(animal);
}

This bug isn't too frequent and is possible to work around, so I don't think you should block this pr on it.

This feels it'll fail for various reasons not just dynamic objects. I'd prefer if we don't fix it in this PR.

ranjitjhala commented 3 months ago

Ok I think I've fixed the TraitObject/Dynamic mismatch ...

ranjitjhala commented 3 months ago

This bug isn't too frequent and is possible to work around, so I don't think you should block this pr on it.

This feels it'll fail for various reasons not just dynamic objects. I'd prefer if we don't fix it in this PR.

@nilehmann -- it turns out that for @enjhnsn2 example with closure and dyn above (see issue #666) -- just filling out the todo! case for Dynamic in the to_rustc(...) fixes #666 i.e. gets this to not crash, so I just tacked it onto this PR since its very much related to the whole conversion to/from ExistentialPredicate/ExistentialTraitRef that is the bulk of this PR...

ranjitjhala commented 3 months ago

Ok I think I addressed all the issues above -- except the

We are putting Dynamic in BaseTy which means they can be indexed (by unit as returned by this function),

But I'm pretty certain that's (for now at least) the sensible choice - as in dyn you have to forget all about the underlying concrete type; I suggest we revisit this later if we have reason to (or if we think there's some use-case for indexing Dynamic values...)