Bug: A Couple of Mono Bugs Found in Eurydice

[ssyram]

Simplified bug lists

A couple of issues have been identified in the Eurydice mono migration procedure. Tried my best to simplify them here.

Bug: assoc functions missing in trait & impl

The example where_clauses_fncg of Eurydice shows clearly the problem also in issue_49 (which uses std) that the trait assoc item method_foo is not in both trait UseFoo and the impl.

Bug: *index == r_abi::VariantIdx::ZERO

Simplified issue_105:

enum Never {}

enum MyResult<T, E> {
    Ok(T),
    Err(E),
}

fn use_result(_r: MyResult<Never, u8>) {}

fn main() {
    use_result(MyResult::Err(1));
}

This causes:

thread 'rustc' panicked at src/bin/charon-driver/translate/translate_types.rs:565:17:
assertion failed: *index == r_abi::VariantIdx::ZERO
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Bug: index out of bounds

Simplified issue_123:

#[derive(PartialEq)]
enum E1 {
    A = 1,
    B = 2,
}

enum E2 {
    C = 3,
    D = 4,
}

fn fun(e: E2) -> i32 {
    e as i32
}

fn main() {
    let _ = E1::A as isize;
    let _ = fun(E2::C);
}

Causing problem:

thread 'main' panicked at /Users/ssyram/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/index_vec-0.1.4/src/indexing.rs:128:10:
index out of bounds: the len is 0 but the index is 0
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Bug: Loop Translation Error in step_by & symcrust

Simplified step_by:

trait MyIterator {
    type Item;
    fn next(&mut self) -> Option<Self::Item>;
    
    // Method with recursive bound: Self::Item: MyIntoIterator
    // This is similar to Iterator::flatten in std
    fn my_flatten(self) -> MyFlatten<Self>
    where
        Self: Sized,
        Self::Item: MyIntoIterator,
    {
        MyFlatten { iter: self }
    }
}

trait MyIntoIterator {
    type Item;
    type IntoIter: MyIterator<Item = Self::Item>;
    fn into_iter(self) -> Self::IntoIter;
}

struct MyRange {
    start: i32,
    end: i32,
}

struct MyFlatten<I> {
    iter: I,
}

impl MyIterator for MyRange {
    type Item = i32;
    fn next(&mut self) -> Option<i32> {
        if self.start < self.end {
            let val = self.start;
            self.start += 1;
            Some(val)
        } else {
            None
        }
    }
}

impl MyIntoIterator for MyRange {
    type Item = i32;
    type IntoIter = MyRange;
    fn into_iter(self) -> MyRange {
        self
    }
}

fn use_iterator() {
    let mut iter = MyRange { start: 0, end: 1 };
    while let Some(_) = iter.next() {
    }
}

fn main() {
    use_iterator();
}

The error generated:

warning[E9999]: Could not find a clause for `Binder { value: <i32 as MyIntoIterator>, bound_vars: [] }` in the current context: `Unimplemented`
  --> step_by.rs:13:5
   |
13 | /     fn my_flatten(self) -> MyFlatten<Self>
14 | |     where
15 | |         Self: Sized,
16 | |         Self::Item: MyIntoIterator,
   | |___________________________________^
   |

[Nadrieril]

Good to know thank you. If you have time, it would b every helpful if you or someong else could minimize each of these into a small example that doesn't use the standard library (or at least such that the bug is not in std code).

[ssyram]

So mainly the step_by example? We would have a try but there is a 8-day holiday coming here...

[Nadrieril]

I mean, all of them could be minimized. To start with, a good bug report should include directly and only the code that causes the error. That's not just for me, it's for other people who may encounter this bug. Then when I say "not depend on stdlib code", that includes a case like issue_49 where the issue is in some impl Ord for whatever that's in the stdlib. To reproduce it would be helpful to see the impls in the reproducer instead.

[ssyram]

OK, will have a try.

[ssyram]

OK, tried to reduce the use of std. But the last case for almost all loops is somehow difficult to reproduce.

[Nadrieril]

Fix for the step_by bug is here: #830.

[ssyram]

Soooooooo quick!!! Amaaazing!

[Nadrieril]

The small reproducer really helped! :D

[Nadrieril]

For the first issue (missing methods), that's more-or-less on purpose: we can't monomorphize methods that have their own generics at the moment. This should not affect eurydice at all since traits are simply unused in --monomorphize mode since all methods are called directly. This will change when we support mono+dyn, but that's for later.