Stack Overflow / Hanging Flux when using `cargo flux`

[vrindisbacher]

I'm adding some refinements to structs in a project (see here). This struct has a lot of fields (probably 200 or so).

When I run cargo flux on the project, rustc gets killed due to stack overflow:

thread 'rustc' has overflowed its stack
fatal runtime error: stack overflow
warning: `veri-asm` (lib) generated 310 warnings (run `cargo fix --lib -p veri-asm` to apply 19 suggestions)
error: could not compile `veri-asm` (lib); 310 warnings emitted

Interestingly, if I remove the refinement here cargo flux hangs (seemingly) forever but there is no stack overflow.

If it's helpful, the struct hierarchy looks like this:

ARMv7m -> Memory -> PPB

PPB has 4 fields, each of which are structs:

• SysControl - 2 sub structs
  • SysControlBlock - a bunch of fields
  • SysControlRegId - a bunch of fields
• NVIC - 150+ fields

• MPU - a bunch of fields

  • SysTick - a bunch of fields

  Is there a good way to diagnose where this is getting hung?

[vrindisbacher]

I tried removing some of the fields from Ppb. If I remove Nvic which has close to 200 fields, cargo flux no longer hangs.

[vrindisbacher]

After removing Nvic from Ppb, I added redefined Nvic with refinements. I removed all the function annotations, so it is just the struct itself. This also causes cargo flux to hang. Seems like this might just have to do with the number of annotations on this struct?

EDIT:

Isolating this more...

The culprit seems to be this function:

fn addr_into_reg_mut(&mut self, address: u32) -> &mut u32 {
        match address {
            // NVIC_ISER0 - NVIC_ISER15
            ISER0_ADDR => &mut self.iser0,
            ISER1_ADDR => &mut self.iser1,
            ISER2_ADDR => &mut self.iser2,
            ISER3_ADDR => &mut self.iser3,
            ISER4_ADDR => &mut self.iser4,
            ...
}

It also seems that adding refinements annotations on other functions related to Nvic cause flux to hang.