search

riscv / sail-riscv

Sail RISC-V model
https://lists.riscv.org/g/tech-golden-model
Other
407 stars 148 forks source link

Remove unnecessary matches for loads/stores #477

Closed Timmmm closed 3 weeks ago

Timmmm commented 1 month ago

Simplify the load/store code by removing the unnecessary matches on the access size. I have not done it for float loads/stores because that requires a separate change to make the float code generic over size.

Note, the first commit is #468 - only review the second.

github-actions[bot] commented 1 month ago

Test Results

712 tests  ±0   712 :white_check_mark: ±0   0s :stopwatch: ±0s   6 suites ±0     0 :zzz: ±0    1 files   ±0     0 :x: ±0 

Results for commit a6b656da. ± Comparison against base commit b15c0d3b.

:recycle: This comment has been updated with latest results.

Timmmm commented 1 month ago

This is ready now - I rebased it and fixed a small bug (mixing up vaddr and addr - see #434 ).

Timmmm commented 3 weeks ago

@billmcspadden-riscv I resolved the threads but I think we should merge #468 first (which is just the first commit from this PR) and then I'll rebase this and we can merge it. Hope that makes sense!

Timmmm commented 3 weeks ago

Ok this is rebased and ready to merge.

rmn30 commented 3 weeks ago

IIRC those matches exist because previous Sail versions had trouble with monomorphisation of this code when generating theorem prover definitions. No idea if that is still the case.

Timmmm commented 3 weeks ago

Ah interesting. @Alasdair do you know if that is still true?

bacam commented 3 weeks ago

I don't think any of the output that's currently produced requires monomorphisation (because the Lem/Isabelle output is currently using bit lists). If I remember correctly, this part of the spec isn't a problem anyway at the moment, but the vector specifications need some tweaks.