sail-riscv
sail-riscv copied to clipboard
riscv
Add >=0 constraints to quot_round_zero and rem_round_zero
The type declarations for those division operators are missing >0 and >=0 constraints.
See https://github.com/riscv/sail-riscv/pull/552/files#r1768223964
I had a go at doing this. It should be possible, but there are a few places where we will need to add explicit asserts for divisors, even if it looks somewhat obvious:
if EMUL_pow < 0 then nf / (2 ^ (0 - EMUL_pow)) <= 8
This is never division by zero, but it requires reasoning about non-linear arithmetic to prove it which the SMT solver can't do.
Hmm isn't the output of 2 ^ always greater than zero? That does feel obvious...
Yes, but in practice the SMT solver just gives up whenever it sees 2 ^ n and n isn't bounded. I have a fallback routine that replaces 2 ^ with an arbitrary function that is equivalent up to 2 ^ 64 so I can check any problem that is unsatisfiable for such a function must be unsatisfiable in general, and I could improve that fallback to handle this case but it doesn't work without an explicit assert right now.
That does mean the other solution is to really understand the vector spec and add tight bounds to every variable.