search

GaloisInc / grift

Galois RISC-V ISA Formal Tools
GNU Affero General Public License v3.0
56 stars 8 forks source link

investigate bugs found by imperas #2

Open benjaminselfridge opened 3 years ago

benjaminselfridge commented 3 years ago

bugs

benjaminselfridge commented 3 years ago

"GRIFT updates the RA register on an invalid jump (target address not 32 bit aligned on RV32I) before triggering an illegal instruction exception (which is incorrect, since illegal instruction should have no side effects). Furthermore, the RV32IMC compliance testing target has been incorrectly configured to RV32GC, thus floating point and atomic instructions are erroneously accepted as well. In addition, similar to VP, reserved non-hint compressed instructions are also erroneously accepted as legal instructions. Finally, we also found the bug that SC.W instruction performs memory access even without pending LR.W reservation (which was the only bug found by the official compliance test-suite)."