JALR with LSB of address set is untested

[cliffordwolf]

The ISA manual states that JALR should clear the LSB of the address:

The indirect jump instruction JALR (jump and link register) uses the I-type encoding. The target
address is obtained by adding the 12-bit signed I-immediate to the register rs1, then setting the
least-significant bit of the result to zero.

Using riscv-formal I just found a bug in my PicoRV32 processor: It does not clear the LSB of the address and instead triggers an illegal instruction address trap when the calculated address has its LSB bit set.

The following assembler code triggers that bug:

        la x1, foo
        addi x1, x1, 1
        jalr zero, x1, 0
foo:

        la x1, bar
        jalr zero, x1, 1
bar:

PicoRV32 is extensively tested with riscv-torture. Therefore I can only assume that riscv-torture never calculates an address with its LSB bit set in its auto-generated test cases. I recommend extending the range of generated instruction sequences accordingly.

PS: I would have found this problem earlier, but I had essentially the same bug in my formal specs. But now I am formally verifying the riscv-formal spec against riscv-isa-sim, which exposed the bug in both my projects.

[aswaterman]

More generally, I don't think we're testing jalr immediates well. When we add that feature, we should randomly set the LSB.

[cliffordwolf]

I think it would be important to make sure all 4 cases with rs1 LSB set and cleared and immediate LSB set and cleared should be covered, to make sure an implementation masks the LSB after the addition, not in one or both operands before performing the addition.

[aswaterman]

Yep.