riscv: store the decoded branch immediate in the ast type -- this simplifies translation to and from herdtools ast.

9 files changed, 33 insertions, 20 deletions

diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
index 46b11310..16d827e2 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -4,14 +4,14 @@
       translate_reg "rd" rd,
       translate_uop op)
 | `RISCVJAL(imm, rd) -> JAL0(
-      translate_imm20 "imm" imm,
+      translate_imm21 "imm" imm,
       translate_reg "rd" rd)
 | `RISCVJALR(imm, rs, rd) -> JALR0(
       translate_imm12 "imm" imm,
       translate_reg "rs" rd,
       translate_reg "rd" rd)
 | `RISCVBType(imm, rs2, rs1, op) -> BTYPE(
-      translate_imm12 "imm" imm,
+      translate_imm13 "imm" imm,
       translate_reg "rs2" rs2,
       translate_reg "rs1" rs1,
       translate_bop op)
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
index c15b3f94..361c0e61 100644
--- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -57,10 +57,15 @@ let translate_bool name = function
   | true -> Sail_values.B1
   | false -> Sail_values.B0
 
+let translate_imm21 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 21,Nat_big_num.of_int value)
 
 let translate_imm20 name value = 
     Sail_values.to_vec0 is_inc (Nat_big_num.of_int 20,Nat_big_num.of_int value)
 
+let translate_imm13 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 13,Nat_big_num.of_int value)
+
 let translate_imm12 name value = 
     Sail_values.to_vec0 is_inc (Nat_big_num.of_int 12,Nat_big_num.of_int value)
 
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index a9d3159c..6073242e 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -1,8 +1,8 @@
 | ("EBREAK", [])                  -> `RISCVStopFetching
 | ("UTYPE", [imm; rd; op])        -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
-| ("JAL", [imm; rd])              -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg  rd)
+| ("JAL", [imm; rd])              -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg  rd)
 | ("JALR", [imm; rs; rd])         -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
-| ("BTYPE", [imm; rs2; rs1; op])  -> `RISCVBType(translate_out_simm12 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op)
+| ("BTYPE", [imm; rs2; rs1; op])  -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op)
 | ("ITYPE", [imm; rs1; rd; op])   -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
 | ("SHIFTIOP", [imm; rs; rd; op]) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
 | ("RTYPE", [rs2; rs1; rd; op])   -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index 9278b92e..da9047a3 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -1,8 +1,8 @@
 | EBREAK                      -> `RISCVStopFetching
 | UTYPE( imm, rd, op)         -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
-| JAL0( imm, rd)              -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg  rd)
+| JAL0( imm, rd)              -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg  rd)
 | JALR0( imm, rs, rd)         -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
-| BTYPE( imm, rs2, rs1, op)   -> `RISCVBType(translate_out_simm12 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op)
+| BTYPE( imm, rs2, rs1, op)   -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op)
 | ITYPE( imm, rs1, rd, op)    -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
 | SHIFTIOP( imm, rs, rd, op)  -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
 | RTYPE( rs2, rs1, rd, op)    -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
index d635efde..8ef18f06 100644
--- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen
+++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
@@ -64,7 +64,9 @@ let translate_out_bool = function
   | Sail_values.B0 -> false
   | _ -> failwith "translate_out_bool Undef"
 
+let translate_out_simm21 imm = translate_out_signed_int imm 21
 let translate_out_simm20 imm = translate_out_signed_int imm 20
+let translate_out_simm13 imm = translate_out_signed_int imm 13
 let translate_out_simm12 imm = translate_out_signed_int imm 12
 let translate_out_imm6 imm = translate_out_int imm
 let translate_out_imm5 imm = translate_out_int imm
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index 28a4f4ba..c72e84d5 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -10,7 +10,7 @@
 | `RISCVJAL(imm, rd) -> 
    ("JAL",
     [
-      translate_imm20 "imm" imm;
+      translate_imm21 "imm" imm;
       translate_reg "rd" rd;
     ],
     [])
@@ -25,7 +25,7 @@
 | `RISCVBType(imm, rs2, rs1, op)  -> 
    ("BTYPE",
     [
-      translate_imm12 "imm" imm;
+      translate_imm13 "imm" imm;
       translate_reg "rs2" rs2;
       translate_reg "rs1" rs1;
       translate_bop "op" op;
diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen
index e034cf37..297d0cf3 100644
--- a/risc-v/hgen/types_sail_trans_out.hgen
+++ b/risc-v/hgen/types_sail_trans_out.hgen
@@ -11,7 +11,9 @@ let translate_out_signed_int inst bits =
 
 let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
 
+let translate_out_simm21 imm = translate_out_signed_int imm 21
 let translate_out_simm20 imm = translate_out_signed_int imm 20
+let translate_out_simm13 imm = translate_out_signed_int imm 13
 let translate_out_simm12 imm = translate_out_signed_int imm 12
 let translate_out_imm6 imm = translate_out_int imm
 let translate_out_imm5 imm = translate_out_int imm
diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen
index 4dc7707e..1bf174fa 100644
--- a/risc-v/hgen/types_trans_sail.hgen
+++ b/risc-v/hgen/types_trans_sail.hgen
@@ -19,10 +19,14 @@ let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW;
 let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] 
 let translate_reg name value = 
     (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value)))
+let translate_imm21 name value = 
+    (name, Bvector (Some 21), bit_list_of_integer 21 (Nat_big_num.of_int value))
 let translate_imm20 name value = 
-    (name, Bvector (Some 26), bit_list_of_integer 26 (Nat_big_num.of_int value))
+    (name, Bvector (Some 20), bit_list_of_integer 20 (Nat_big_num.of_int value))
 let translate_imm16 name value = 
     (name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value))
+let translate_imm13 name value = 
+    (name, Bvector (Some 13), bit_list_of_integer 13 (Nat_big_num.of_int value))
 let translate_imm12 name value = 
     (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value))
 let translate_imm6 name value = 
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index 1a5a3b33..962d8280 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -95,10 +95,10 @@ function clause execute (UTYPE(imm, rd, op)) =
     } in
     wGPR(rd, ret)
 
-union ast member ((bit[20]), regno) JAL
-function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm, rd))
+union ast member ((bit[21]), regno) JAL
+function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd))
 function clause execute (JAL(imm, rd)) =
-    let (bit[64]) offset = EXTS(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0) in {
+    let (bit[64]) offset = EXTS(imm) in {
       nextPC :=  PC + offset;
       wGPR(rd, PC + 4);
     }
@@ -112,13 +112,13 @@ function clause execute (JALR(imm, rs1, rd)) =
       wGPR(rd, PC + 4);
     }
 
-union ast member ((bit[12]), regno, regno, bop) BTYPE
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BEQ))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BNE))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLT))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGE))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLTU))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGEU))
+union ast member ((bit[13]), regno, regno, bop) BTYPE
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BEQ))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BNE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLT))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLTU))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGEU))
 
 function clause execute (BTYPE(imm, rs2, rs1, op)) =
   let rs1_val = rGPR(rs1) in
@@ -132,7 +132,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) =
     case BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *)
   } in
   if (taken) then
-      nextPC := PC + EXTS(imm : 0b0)
+      nextPC := PC + EXTS(imm)
 
 union ast member ((bit[12]), regno, regno, iop) ITYPE
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI))