From 8d9b63f10d2822d97b9085353b429468396270a7 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Tue, 1 Mar 2022 00:24:41 -0500
Subject: [PATCH] use same getReg/setReg in MinimalCSRs

---
 src/riscv/Platform/MinimalCSRs.v | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/riscv/Platform/MinimalCSRs.v b/src/riscv/Platform/MinimalCSRs.v
index 3e0ebaf..ad25851 100644
--- a/src/riscv/Platform/MinimalCSRs.v
+++ b/src/riscv/Platform/MinimalCSRs.v
@@ -53,14 +53,15 @@ Section Riscv.
     { mach with pc := mach.(nextPc); nextPc ::= word.add (word.of_Z 4) }.
 
   Definition getReg(regs: Registers)(reg: Z): word :=
-    if Z.eq_dec reg 0 then word.of_Z 0
-    else match map.get regs reg with
-         | Some x => x
-         | None => word.of_Z 0
-         end.
+    if ((0 <? reg) && (reg <? 32))%bool then
+      match map.get regs reg with
+      | Some x => x
+      | None => word.of_Z 0
+      end
+    else word.of_Z 0.
 
   Definition setReg(reg: Z)(v: word)(regs: Registers): Registers :=
-    if Z.eq_dec reg Register0 then regs else map.put regs reg v.
+    if ((0 <? reg) && (reg <? 32))%bool then map.put regs reg v else regs.
 
   Definition run_primitive(a: riscv_primitive)(mach: State):
              (primitive_result a -> State -> Prop) -> (State -> Prop) -> Prop :=