search

hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
179 stars 19 forks source link

Incorrect order for Deps.sort #379

Open cmester0 opened 10 months ago

cmester0 commented 10 months ago

The following piece of code

pub trait Foo {
    const c : u32;
}

pub struct foo {}
impl Foo for foo {
    const c : u32 = 17;
}

type F = foo;

pub fn bar(random: u32) -> u32 {
    random % F::c
}

gets sorted incorrectly, as the bar function is moved before the impl block. If possible we should probably keep the order of the original program instead of moving functions earlier, if there are no conflicts in the dependency graph.

cmester0 commented 10 months ago

This issue is related to #375 as the graph is not getting an edge, since the concrete idents are not equal.

W95Psp commented 10 months ago

Hi Lasse, thanks for the bug report! That's indeed related to #375, and also to #372, which I have to debug. Gonna try to look at that soon.

W95Psp commented 6 months ago

Hey, this should be fixed now, impl expressions are taken into account for the dependency analysis. Can you check if that works for you on main and close if it's the case? Thanks!

github-actions[bot] commented 2 days ago

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.