From a34adc8e005447e7fa44ca3b71db35ceb7facb4c Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 24 Jun 2022 18:55:21 +0200
Subject: Expand "j_s symb" to "jump symb, x31" assembly pseudo-instruction
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

As suggested by Léo Gourdin in #437.

The previous expansion as a plain "j" instruction fails when the jump
offset is too large to be represented (issue #436).

Fixes: #436
Closes: #437
---
 riscV/Asm.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'riscV/Asm.v')

diff --git a/riscV/Asm.v b/riscV/Asm.v
index a47573a2..cbe3476a 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -751,7 +751,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pj_l l =>
       goto_label f l rs m
   | Pj_s s sg =>
-      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
+      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero) #X31 <- Vundef) m
   | Pj_r r sg =>
       Next (rs#PC <- (rs#r)) m
   | Pjal_s s sg =>
-- 
cgit