SailBugfix: Modifies only mie in write Sie when the interrupt is dele…

[francois141]

…gated

Before modifying each specific interrupt enable bit (e.g., SEIE, STIE, or SSIE), the code checks whether the corresponding bit in Mideleg is set. Mideleg determines whether a specific interrupt is delegated to the supervisor level, so this ensures that only interrupts managed by the supervisor are updated.

[CharlyCst]

I see what you want to do here, shouldn't it simply be:

// Only delegated interrupts can be enabled through `sie`
let mideleg = self.get(Csr::Mideleg);
self.csr.mie = (self.csr.mie & !mideleg) | (mideleg & value);

where all delegated interrupts can be modified?

[francois141]

The two formulations are not equivalent. In the case mideleg is set to 0 you don't want to change the value of the bit. Therefore we need three if statements ^^

You can't beat kani ^^

[CharlyCst]

Well yes indeed, and the proposed code snipped does not change any value when mideleg is 0 as it evaluates to (self.csr.mie & u64::MAX) | (0x0 & value) = self.csr.mie, isn't that what is expected?

The reason I am asking is because the version in the PR is missing the LCOFIE bit, which is not it the Sail model but is present on the hardware, so we would need at least a 4th if to support it.

[francois141]

The problem is that if only one of the interrupt is delegated, with the previous implementation we can clear the entire mask which is wrong. Regarding lcofie, let me fix that

[francois141]

@CharlyCst Ready for review! I did the change

[CharlyCst]

Yes, I agree the previous implementation was wrong, but is:

// Only delegated interrupts can be enabled through `sie`
let mideleg = self.get(Csr::Mideleg);
self.csr.mie = (self.csr.mie & !mideleg) | (mideleg & value);

Correct? That was my question ^^

[francois141]

This also looks correct, let me test with kani

[francois141]

Works, pushed