The RISC-V spec justifies the semantics of auipc+jalr by that it enables code to jump anywhere in a 32-bit offset relative to the PC.
However, I was doing some experimenting and it seem to me that there are some 32-bit offsets just below S32_MAX (2^31 - 1) that
cannot be encoded in this scheme on RV64.
One such example would be an offset of 0x7ffffffe. The normal strategy would be to construct the upper 20 and lower 12 bits
of the offset for auipc+jalr, and add 1 to the auipc immediate to compensate for the sign-extension from jalr. In this edge case however,
adding that additional 1 causes the sign of the auipc constant to flip, messing up the sign extension performed by auipc. This isn't
a problem on RV32 because there are no upper bits to sign extend into.
In fact, it seems to me that there is no pair of auipc+jalr instructions that can encode 0x7ffffffe because of the double sign-extension.
For loading an immediate, you can get around this by using an addiw instruction instead of addi, but there's no such equivalent for jalr.
I tried to do some digging and see if anyone else has brought this up but didn't see any prior discussion.
Thanks for the help,
P.S. To anybody curious, I tried modeling this problem in the Rosette
programming language to ask an SMT solver to come up
with immediates that encode the offset. The SMT returns unsat, indiciating there are no such immediates given my model of
the instructions. This means either that there really is no way to encode this offset using an auipc+jalr pair, or my model is wrong :)
; Initial program counter
(define-symbolic pc (bitvector 64))
; 32-bit offset
(define offset (bv #x7ffffffe 32))
; Immediate for auipc
(define-symbolic upper (bitvector 20))
; Immediate for jalr
(define-symbolic lower (bitvector 12))
; Construct new program counter by simulating the effects of auipc+jalr
(define newpc (bvadd pc
(sign-extend (concat upper (bv 0 12)) (bitvector 64)) ; auipc
(sign-extend lower (bitvector 64)))) ; jalr
; Ask the SMT solver for an assignment to the immediates that produces
; the desired offset.
(solve (assert (equal? newpc (bvadd pc (sign-extend offset (bitvector 64))))))