summaryrefslogtreecommitdiff
path: root/risc-v/hgen
diff options
context:
space:
mode:
Diffstat (limited to 'risc-v/hgen')
-rw-r--r--risc-v/hgen/ast.hgen13
-rw-r--r--risc-v/hgen/fold.hgen13
-rw-r--r--risc-v/hgen/herdtools_ast_to_shallow_ast.hgen60
-rw-r--r--risc-v/hgen/herdtools_types_to_shallow_types.hgen79
-rw-r--r--risc-v/hgen/lexer.hgen64
-rw-r--r--risc-v/hgen/map.hgen12
-rw-r--r--risc-v/hgen/parser.hgen36
-rw-r--r--risc-v/hgen/pretty.hgen15
-rw-r--r--risc-v/hgen/sail_trans_out.hgen14
-rw-r--r--risc-v/hgen/shallow_ast_to_herdtools_ast.hgen14
-rw-r--r--risc-v/hgen/shallow_types_to_herdtools_types.hgen73
-rw-r--r--risc-v/hgen/token_types.hgen15
-rw-r--r--risc-v/hgen/tokens.hgen14
-rw-r--r--risc-v/hgen/trans_sail.hgen112
-rw-r--r--risc-v/hgen/types.hgen123
-rw-r--r--risc-v/hgen/types_sail_trans_out.hgen86
-rw-r--r--risc-v/hgen/types_trans_sail.hgen39
17 files changed, 782 insertions, 0 deletions
diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
new file mode 100644
index 00000000..8983b5ae
--- /dev/null
+++ b/risc-v/hgen/ast.hgen
@@ -0,0 +1,13 @@
+| `RISCVUTYPE of bit20 * reg * riscvUop
+| `RISCVJAL of bit20 * reg
+| `RISCVJALR of bit12 * reg * reg
+| `RISCVBType of bit12 * reg * reg * riscvBop
+| `RISCVIType of bit12 * reg * reg * riscvIop
+| `RISCVShiftIop of bit6 * reg * reg * riscvSop
+| `RISCVRType of reg * reg * reg * riscvRop
+| `RISCVLoad of bit12 * reg * reg * bool * wordWidth
+| `RISCVStore of bit12 * reg * reg * wordWidth
+| `RISCVADDIW of bit12 * reg * reg
+| `RISCVSHIFTW of bit5 * reg * reg * riscvSop
+| `RISCVRTYPEW of reg * reg * reg * riscvRopw
+| `RISCVFENCE of bit4 * bit4
diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen
new file mode 100644
index 00000000..03318805
--- /dev/null
+++ b/risc-v/hgen/fold.hgen
@@ -0,0 +1,13 @@
+| `RISCVThreadStart -> (y_reg, y_sreg)
+| `RISCVUTYPE (_, r0, _) -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJAL (_, r0) -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJALR (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVBType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVIType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVShiftIop (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVRType (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
+| `RISCVLoad (_, r0, r1, _, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVStore (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVADDIW (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVSHIFTW (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVRTYPEW (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
new file mode 100644
index 00000000..50026612
--- /dev/null
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -0,0 +1,60 @@
+| `RISCVStopFetching -> EBREAK
+| `RISCVUTYPE(imm, rd, op) -> UTYPE(
+ translate_imm20 "imm" imm,
+ translate_reg "rd" rd,
+ translate_uop op)
+| `RISCVJAL(imm, rd) -> JAL0(
+ 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_imm13 "imm" imm,
+ translate_reg "rs2" rs2,
+ translate_reg "rs1" rs1,
+ translate_bop op)
+| `RISCVIType(imm, rs1, rd, op) -> ITYPE(
+ translate_imm12 "imm" imm,
+ translate_reg "rs1" rs1,
+ translate_reg "rd" rd,
+ translate_iop op)
+| `RISCVShiftIop(imm, rs, rd, op) -> SHIFTIOP(
+ translate_imm6 "imm" imm,
+ translate_reg "rs" rs,
+ translate_reg "rd" rd,
+ translate_sop op)
+| `RISCVRType (rs2, rs1, rd, op) -> RTYPE (
+ translate_reg "rs2" rs2,
+ translate_reg "rs1" rs1,
+ translate_reg "rd" rd,
+ translate_rop op)
+| `RISCVLoad(imm, rs, rd, unsigned, width) -> LOAD(
+ translate_imm12 "imm" imm,
+ translate_reg "rs" rs,
+ translate_reg "rd" rd,
+ translate_bool "unsigned" unsigned,
+ translate_wordWidth width)
+| `RISCVStore(imm, rs, rd, width) -> STORE (
+ translate_imm12 "imm" imm,
+ translate_reg "rs" rs,
+ translate_reg "rd" rd,
+ translate_wordWidth width)
+| `RISCVADDIW(imm, rs, rd) -> ADDIW(
+ translate_imm12 "imm" imm,
+ translate_reg "rs" rs,
+ translate_reg "rd" rd)
+| `RISCVSHIFTW(imm, rs, rd, op) -> SHIFTW(
+ translate_imm5 "imm" imm,
+ translate_reg "rs" rs,
+ translate_reg "rd" rd,
+ translate_sop op)
+| `RISCVRTYPEW(rs2, rs1, rd, op) -> RTYPEW(
+ translate_reg "rs2" rs2,
+ translate_reg "rs1" rs1,
+ translate_reg "rd" rd,
+ translate_ropw op)
+| `RISCVFENCE(pred, succ) -> FENCE(
+ translate_imm4 "pred" pred,
+ translate_imm4 "succ" succ)
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
new file mode 100644
index 00000000..4d8bd87a
--- /dev/null
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -0,0 +1,79 @@
+let is_inc = false
+
+let translate_reg name value =
+ Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int (reg_to_int value))
+
+let translate_uop op = match op with
+ | RISCVLUI -> LUI0
+ | RISCVAUIPC -> AUIPC
+
+let translate_bop op = match op with
+ | RISCVBEQ -> BEQ0
+ | RISCVBNE -> BNE
+ | RISCVBLT -> BLT
+ | RISCVBGE -> BGE
+ | RISCVBLTU -> BLTU
+ | RISCVBGEU -> BGEU
+
+let translate_iop op = match op with
+ | RISCVADDI -> ADDI0
+ | RISCVSLTI -> SLTI0
+ | RISCVSLTIU -> SLTIU0
+ | RISCVXORI -> XORI0
+ | RISCVORI -> ORI0
+ | RISCVANDI -> ANDI0
+
+let translate_sop op = match op with
+ | RISCVSLLI -> SLLI
+ | RISCVSRLI -> SRLI
+ | RISCVSRAI -> SRAI
+
+let translate_rop op = match op with
+ | RISCVADD -> ADD0
+ | RISCVSUB -> SUB0
+ | RISCVSLL -> SLL0
+ | RISCVSLT -> SLT0
+ | RISCVSLTU -> SLTU0
+ | RISCVXOR -> XOR0
+ | RISCVSRL -> SRL0
+ | RISCVSRA -> SRA0
+ | RISCVOR -> OR0
+ | RISCVAND -> AND0
+
+let translate_ropw op = match op with
+ | RISCVADDW -> ADDW
+ | RISCVSUBW -> SUBW
+ | RISCVSLLW -> SLLW
+ | RISCVSRLW -> SRLW
+ | RISCVSRAW -> SRAW
+
+let translate_wordWidth op = match op with
+ | RISCVBYTE -> BYTE
+ | RISCVHALF -> HALF
+ | RISCVWORD -> WORD
+ | RISCVDOUBLE -> DOUBLE
+
+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)
+
+let translate_imm6 name value =
+ Sail_values.to_vec0 is_inc (Nat_big_num.of_int 6,Nat_big_num.of_int value)
+
+let translate_imm5 name value =
+ Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value)
+
+let translate_imm4 name value =
+ Sail_values.to_vec0 is_inc (Nat_big_num.of_int 4,Nat_big_num.of_int value)
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
new file mode 100644
index 00000000..5f2c8326
--- /dev/null
+++ b/risc-v/hgen/lexer.hgen
@@ -0,0 +1,64 @@
+"lui" , UTYPE { op=RISCVLUI };
+"auipc" , UTYPE { op=RISCVAUIPC };
+
+"jal", JAL ();
+"jalr", JALR ();
+
+"beq", BTYPE {op=RISCVBEQ};
+"bne", BTYPE {op=RISCVBNE};
+"blt", BTYPE {op=RISCVBLT};
+"bge", BTYPE {op=RISCVBGE};
+"bltu", BTYPE {op=RISCVBLTU};
+"bgeu", BTYPE {op=RISCVBGEU};
+
+"addi", ITYPE {op=RISCVADDI};
+"stli", ITYPE {op=RISCVSLTI};
+"sltiu", ITYPE {op=RISCVSLTIU};
+"xori", ITYPE {op=RISCVXORI};
+"ori", ITYPE {op=RISCVORI};
+"andi", ITYPE {op=RISCVANDI};
+
+"slli", SHIFTIOP{op=RISCVSLLI};
+"srli", SHIFTIOP{op=RISCVSRLI};
+"srai", SHIFTIOP{op=RISCVSRAI};
+
+"add", RTYPE{op=RISCVADD};
+"sub", RTYPE{op=RISCVSUB};
+"sll", RTYPE{op=RISCVSLL};
+"slt", RTYPE{op=RISCVSLT};
+"sltu", RTYPE{op=RISCVSLT};
+"xor", RTYPE{op=RISCVXOR};
+"srl", RTYPE{op=RISCVSRL};
+"sra", RTYPE{op=RISCVSRA};
+"or", RTYPE{op=RISCVOR};
+"and", RTYPE{op=RISCVAND};
+
+"lb", LOAD{unsigned=false; width=RISCVBYTE};
+"lbu", LOAD{unsigned=true; width=RISCVBYTE};
+"lh", LOAD{unsigned=false; width=RISCVHALF};
+"lhu", LOAD{unsigned=true; width=RISCVHALF};
+"lw", LOAD{unsigned=false; width=RISCVWORD};
+"lwu", LOAD{unsigned=true; width=RISCVWORD};
+"ld", LOAD{unsigned=false; width=RISCVDOUBLE};
+
+"sb", STORE{width=RISCVBYTE};
+"sh", STORE{width=RISCVHALF};
+"sw", STORE{width=RISCVWORD};
+"sd", STORE{width=RISCVDOUBLE};
+
+"addiw", ADDIW ();
+
+"slliw", SHIFTW{op=RISCVSLLI};
+"srliw", SHIFTW{op=RISCVSRLI};
+"sraiw", SHIFTW{op=RISCVSRAI};
+
+"addw", RTYPEW{op=RISCVADDW};
+"subw", RTYPEW{op=RISCVSUBW};
+"sslw", RTYPEW{op=RISCVSLLW};
+"srlw", RTYPEW{op=RISCVSRLW};
+"sraw", RTYPEW{op=RISCVSRAW};
+
+"fence", FENCE ();
+"r", FENCEOPTION Fence_R;
+"w", FENCEOPTION Fence_W;
+"rw", FENCEOPTION Fence_RW;
diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen
new file mode 100644
index 00000000..ff14c428
--- /dev/null
+++ b/risc-v/hgen/map.hgen
@@ -0,0 +1,12 @@
+| `RISCVUTYPE (x, r0, y) -> `RISCVUTYPE (x, map_reg r0, y)
+| `RISCVJAL (x, r0) -> `RISCVJAL (x, map_reg r0)
+| `RISCVJALR (x, r0, r1) -> `RISCVJALR (x, map_reg r0, map_reg r1)
+| `RISCVBType (x, r0, r1, y) -> `RISCVBType (x, map_reg r0, map_reg r1, y)
+| `RISCVIType (x, r0, r1, y) -> `RISCVIType (x, map_reg r0, map_reg r1, y)
+| `RISCVShiftIop (x, r0, r1, y) -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y)
+| `RISCVRType (r0, r1, r2, y) -> `RISCVRType (r0, map_reg r1, map_reg r2, y)
+| `RISCVLoad (x, r0, r1, y, z) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z)
+| `RISCVStore (x, r0, r1, y) -> `RISCVStore (x, map_reg r0, map_reg r1, y)
+| `RISCVADDIW (x, r0, r1) -> `RISCVADDIW (x, map_reg r0, map_reg r1)
+| `RISCVSHIFTW (x, r0, r1, y) -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y)
+| `RISCVRTYPEW (r0, r1, r2, x) -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x)
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
new file mode 100644
index 00000000..37fd8d8d
--- /dev/null
+++ b/risc-v/hgen/parser.hgen
@@ -0,0 +1,36 @@
+| UTYPE reg COMMA NUM
+ { `RISCVUTYPE($4, $2, $1.op) }
+| JAL reg COMMA NUM
+ { `RISCVJAL($4, $2) }
+| JALR reg COMMA reg COMMA NUM
+ { `RISCVJALR($6, $4, $2) }
+| BTYPE reg COMMA reg COMMA NUM
+ { `RISCVBType($6, $4, $2, $1.op) }
+| ITYPE reg COMMA reg COMMA NUM
+ { `RISCVIType($6, $4, $2, $1.op) }
+| SHIFTIOP reg COMMA reg COMMA NUM
+ { `RISCVShiftIop($6, $4, $2, $1.op) }
+| RTYPE reg COMMA reg COMMA reg
+ { `RISCVRType ($6, $4, $2, $1.op) }
+| LOAD reg COMMA NUM LPAR reg RPAR
+ { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width) }
+| STORE reg COMMA NUM LPAR reg RPAR
+ { `RISCVStore($4, $2, $6, $1.width) }
+| ADDIW reg COMMA reg COMMA NUM
+ { `RISCVADDIW ($6, $4, $2) }
+| SHIFTW reg COMMA reg COMMA NUM
+ { `RISCVSHIFTW ($6, $4, $2, $1.op) }
+| RTYPEW reg COMMA reg COMMA reg
+ { `RISCVRTYPEW ($6, $4, $2, $1.op) }
+| FENCE FENCEOPTION COMMA FENCEOPTION
+ { match ($2, $4) with
+ | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011)
+ | (Fence_R, Fence_RW) -> `RISCVFENCE (0b0010, 0b0011)
+ | (Fence_RW, Fence_W) -> `RISCVFENCE (0b0011, 0b0001)
+ | (Fence_RW, Fence_R) -> failwith "'fence rw,r' is not supported"
+ | (Fence_R, Fence_R) -> failwith "'fence r,r' is not supported"
+ | (Fence_R, Fence_W) -> failwith "'fence r,w' is not supported"
+ | (Fence_W, Fence_RW) -> failwith "'fence w,rw' is not supported"
+ | (Fence_W, Fence_R) -> failwith "'fence w,r' is not supported"
+ | (Fence_W, Fence_W) -> failwith "'fence w,w' is not supported"
+ }
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
new file mode 100644
index 00000000..1da3ef11
--- /dev/null
+++ b/risc-v/hgen/pretty.hgen
@@ -0,0 +1,15 @@
+| `RISCVThreadStart -> "start"
+| `RISCVStopFetching -> "stop"
+| `RISCVUTYPE(imm, rd, op) -> sprintf "%s %s, %d" (pp_riscv_uop op) (pp_reg rd) imm
+| `RISCVJAL(imm, rd) -> sprintf "jal %s, %d" (pp_reg rd) imm
+| `RISCVJALR(imm, rs, rd) -> sprintf "jalr %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
+| `RISCVBType(imm, rs2, rs1, op) -> sprintf "%s %s, %s, %d" (pp_riscv_bop op) (pp_reg rs1) (pp_reg rs2) imm
+| `RISCVIType(imm, rs2, rs1, op) -> sprintf "%s %s, %s, %d" (pp_riscv_iop op) (pp_reg rs1) (pp_reg rs2) imm
+| `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
+| `RISCVRType (rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
+| `RISCVLoad(imm, rs, rd, unsigned, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width)) (pp_reg rd) imm (pp_reg rs)
+| `RISCVStore(imm, rs2, rs1, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rs2) imm (pp_reg rs1)
+| `RISCVADDIW(imm, rs, rd) -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
+| `RISCVSHIFTW(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
+| `RISCVRTYPEW(rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
+| `RISCVFENCE(pred, succ) -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ)
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
new file mode 100644
index 00000000..dca5bea1
--- /dev/null
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -0,0 +1,14 @@
+| ("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_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_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)
+| ("LOAD", [imm; rs; rd; unsigned; width]) -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width)
+| ("STORE", [imm; rs; rd; width]) -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width)
+| ("ADDIW", [imm; rs; rd]) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| ("SHIFTW", [imm; rs; rd; op]) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| ("RTYPEW", [rs2; rs1; rd; op]) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
+| ("FENCE", [pred; succ]) -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
new file mode 100644
index 00000000..6158ebd7
--- /dev/null
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -0,0 +1,14 @@
+| 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_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_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)
+| LOAD( imm, rs, rd, unsigned, width) -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width)
+| STORE( imm, rs, rd, width) -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width)
+| ADDIW( imm, rs, rd) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| SHIFTW( imm, rs, rd, op) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| RTYPEW( rs2, rs1, rd, op) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
+| FENCE( pred, succ) -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
new file mode 100644
index 00000000..a891d7d0
--- /dev/null
+++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
@@ -0,0 +1,73 @@
+let translate_out_big_bit = Sail_values.unsigned
+
+let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
+let translate_out_signed_int inst bits =
+ let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
+ if (i >= (1 lsl (bits - 1))) then
+ (i - (1 lsl bits)) else
+ i
+
+let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_uop op = match op with
+ | LUI0 -> RISCVLUI
+ | AUIPC -> RISCVAUIPC
+
+let translate_out_bop op = match op with
+ | BEQ0 -> RISCVBEQ
+ | BNE -> RISCVBNE
+ | BLT -> RISCVBLT
+ | BGE -> RISCVBGE
+ | BLTU -> RISCVBLTU
+ | BGEU -> RISCVBGEU
+
+let translate_out_iop op = match op with
+ | ADDI0 -> RISCVADDI
+ | SLTI0 -> RISCVSLTI
+ | SLTIU0 -> RISCVSLTIU
+ | XORI0 -> RISCVXORI
+ | ORI0 -> RISCVORI
+ | ANDI0 -> RISCVANDI
+
+let translate_out_sop op = match op with
+ | SLLI -> RISCVSLLI
+ | SRLI -> RISCVSRLI
+ | SRAI -> RISCVSRAI
+
+let translate_out_rop op = match op with
+ | ADD0 -> RISCVADD
+ | SUB0 -> RISCVSUB
+ | SLL0 -> RISCVSLL
+ | SLT0 -> RISCVSLT
+ | SLTU0 -> RISCVSLTU
+ | XOR0 -> RISCVXOR
+ | SRL0 -> RISCVSRL
+ | SRA0 -> RISCVSRA
+ | OR0 -> RISCVOR
+ | AND0 -> RISCVAND
+
+let translate_out_ropw op = match op with
+ | ADDW -> RISCVADDW
+ | SUBW -> RISCVSUBW
+ | SLLW -> RISCVSLLW
+ | SRLW -> RISCVSRLW
+ | SRAW -> RISCVSRAW
+
+let translate_out_wordWidth op = match op with
+ | BYTE -> RISCVBYTE
+ | HALF -> RISCVHALF
+ | WORD -> RISCVWORD
+ | DOUBLE -> RISCVDOUBLE
+
+let translate_out_bool = function
+ | Sail_values.B1 -> true
+ | 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
+let translate_out_imm4 imm = translate_out_int imm
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
new file mode 100644
index 00000000..2980b985
--- /dev/null
+++ b/risc-v/hgen/token_types.hgen
@@ -0,0 +1,15 @@
+type token_UTYPE = {op : riscvUop }
+type token_JAL = unit
+type token_JALR = unit
+type token_BType = {op : riscvBop }
+type token_IType = {op : riscvIop }
+type token_ShiftIop = {op : riscvSop }
+type token_RTYPE = {op : riscvRop }
+type token_Load = {unsigned: bool; width : wordWidth }
+type token_Store = {width : wordWidth }
+type token_ADDIW = unit
+type token_SHIFTW = {op : riscvSop }
+type token_RTYPEW = {op : riscvRopw }
+type token_FENCE = unit
+
+type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen
new file mode 100644
index 00000000..f952cf77
--- /dev/null
+++ b/risc-v/hgen/tokens.hgen
@@ -0,0 +1,14 @@
+%token <RISCVHGenBase.token_UTYPE> UTYPE
+%token <RISCVHGenBase.token_JAL> JAL
+%token <RISCVHGenBase.token_JALR> JALR
+%token <RISCVHGenBase.token_BType> BTYPE
+%token <RISCVHGenBase.token_IType> ITYPE
+%token <RISCVHGenBase.token_ShiftIop> SHIFTIOP
+%token <RISCVHGenBase.token_RTYPE> RTYPE
+%token <RISCVHGenBase.token_Load> LOAD
+%token <RISCVHGenBase.token_Store> STORE
+%token <RISCVHGenBase.token_ADDIW> ADDIW
+%token <RISCVHGenBase.token_SHIFTW> SHIFTW
+%token <RISCVHGenBase.token_RTYPEW> RTYPEW
+%token <RISCVHGenBase.token_FENCE> FENCE
+%token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
new file mode 100644
index 00000000..df22d9dc
--- /dev/null
+++ b/risc-v/hgen/trans_sail.hgen
@@ -0,0 +1,112 @@
+| `RISCVStopFetching -> ("EBREAK", [], [])
+| `RISCVUTYPE(imm, rd, op) ->
+ ("UTYPE",
+ [
+ translate_imm20 "imm" imm;
+ translate_reg "rd" rd;
+ translate_uop "op" op;
+ ],
+ [])
+| `RISCVJAL(imm, rd) ->
+ ("JAL",
+ [
+ translate_imm21 "imm" imm;
+ translate_reg "rd" rd;
+ ],
+ [])
+| `RISCVJALR(imm, rs, rd) ->
+ ("JALR",
+ [
+ translate_imm12 "imm" imm;
+ translate_reg "rs" rd;
+ translate_reg "rd" rd;
+ ],
+ [])
+| `RISCVBType(imm, rs2, rs1, op) ->
+ ("BTYPE",
+ [
+ translate_imm13 "imm" imm;
+ translate_reg "rs2" rs2;
+ translate_reg "rs1" rs1;
+ translate_bop "op" op;
+ ],
+ [])
+| `RISCVIType(imm, rs1, rd, op) ->
+ ("ITYPE",
+ [
+ translate_imm12 "imm" imm;
+ translate_reg "rs1" rs1;
+ translate_reg "rd" rd;
+ translate_iop "op" op;
+ ],
+ [])
+| `RISCVShiftIop(imm, rs, rd, op) ->
+ ("SHIFTIOP",
+ [
+ translate_imm6 "imm" imm;
+ translate_reg "rs" rs;
+ translate_reg "rd" rd;
+ translate_sop "op" op;
+ ],
+ [])
+| `RISCVRType (rs2, rs1, rd, op) ->
+ ("RTYPE",
+ [
+ translate_reg "rs2" rs2;
+ translate_reg "rs1" rs1;
+ translate_reg "rd" rd;
+ translate_rop "op" op;
+ ],
+ [])
+| `RISCVLoad(imm, rs, rd, unsigned, width) ->
+ ("LOAD",
+ [
+ translate_imm12 "imm" imm;
+ translate_reg "rs" rs;
+ translate_reg "rd" rd;
+ translate_bool "unsigned" unsigned;
+ translate_width "width" width;
+ ],
+ [])
+| `RISCVStore(imm, rs2, rs1, width) ->
+ ("STORE",
+ [
+ translate_imm12 "imm" imm;
+ translate_reg "rs2" rs2;
+ translate_reg "rs1" rs1;
+ translate_width "width" width;
+ ],
+ [])
+| `RISCVADDIW(imm, rs, rd) ->
+ ("ADDIW",
+ [
+ translate_imm12 "imm" imm;
+ translate_reg "rs" rs;
+ translate_reg "rd" rd;
+ ],
+ [])
+| `RISCVSHIFTW(imm, rs, rd, op) ->
+ ("SHIFTW",
+ [
+ translate_imm5 "imm" imm;
+ translate_reg "rs" rs;
+ translate_reg "rd" rd;
+ translate_sop "op" op;
+ ],
+ [])
+| `RISCVRTYPEW(rs2, rs1, rd, op) ->
+ ("RTYPEW",
+ [
+ translate_reg "rs2" rs2;
+ translate_reg "rs1" rs1;
+ translate_reg "rd" rd;
+ translate_ropw "op" op;
+ ],
+ [])
+| `RISCVFENCE(pred, succ) ->
+ ("FENCE",
+ [
+ translate_imm4 "pred" pred;
+ translate_imm4 "succ" succ;
+ ],
+ [])
diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen
new file mode 100644
index 00000000..87fc9b95
--- /dev/null
+++ b/risc-v/hgen/types.hgen
@@ -0,0 +1,123 @@
+type bit20 = int
+type bit12 = int
+type bit6 = int
+type bit5 = int
+type bit4 = int
+
+type riscvUop = (* upper immediate ops *)
+| RISCVLUI
+| RISCVAUIPC
+
+let pp_riscv_uop = function
+| RISCVLUI -> "lui"
+| RISCVAUIPC -> "auipc"
+
+
+type riscvBop = (* branch ops *)
+| RISCVBEQ
+| RISCVBNE
+| RISCVBLT
+| RISCVBGE
+| RISCVBLTU
+| RISCVBGEU
+
+let pp_riscv_bop = function
+| RISCVBEQ -> "beq"
+| RISCVBNE -> "bne"
+| RISCVBLT -> "blt"
+| RISCVBGE -> "bge"
+| RISCVBLTU -> "bltu"
+| RISCVBGEU -> "bgeu"
+
+type riscvIop = (* immediate ops *)
+| RISCVADDI
+| RISCVSLTI
+| RISCVSLTIU
+| RISCVXORI
+| RISCVORI
+| RISCVANDI
+
+let pp_riscv_iop = function
+| RISCVADDI -> "addi"
+| RISCVSLTI -> "slti"
+| RISCVSLTIU -> "sltiu"
+| RISCVXORI -> "xori"
+| RISCVORI -> "ori"
+| RISCVANDI -> "andi"
+
+type riscvSop = (* shift ops *)
+| RISCVSLLI
+| RISCVSRLI
+| RISCVSRAI
+
+let pp_riscv_sop = function
+| RISCVSLLI -> "slli"
+| RISCVSRLI -> "srli"
+| RISCVSRAI -> "srai"
+
+type riscvRop = (* reg-reg ops *)
+| RISCVADD
+| RISCVSUB
+| RISCVSLL
+| RISCVSLT
+| RISCVSLTU
+| RISCVXOR
+| RISCVSRL
+| RISCVSRA
+| RISCVOR
+| RISCVAND
+
+let pp_riscv_rop = function
+| RISCVADD -> "add"
+| RISCVSUB -> "sub"
+| RISCVSLL -> "sll"
+| RISCVSLT -> "slt"
+| RISCVSLTU -> "sltu"
+| RISCVXOR -> "xor"
+| RISCVSRL -> "srl"
+| RISCVSRA -> "sra"
+| RISCVOR -> "or"
+| RISCVAND -> "and"
+
+type riscvRopw = (* reg-reg 32-bit ops *)
+| RISCVADDW
+| RISCVSUBW
+| RISCVSLLW
+| RISCVSRLW
+| RISCVSRAW
+
+let pp_riscv_ropw = function
+| RISCVADDW -> "addw"
+| RISCVSUBW -> "subw"
+| RISCVSLLW -> "sllw"
+| RISCVSRLW -> "srlw"
+| RISCVSRAW -> "sraw"
+
+type wordWidth =
+ | RISCVBYTE
+ | RISCVHALF
+ | RISCVWORD
+ | RISCVDOUBLE
+
+let pp_riscv_load_op (unsigned, width) = match (unsigned, width) with
+ | (false, RISCVBYTE) -> "lb"
+ | (true, RISCVBYTE) -> "lbu"
+ | (false, RISCVHALF) -> "lh"
+ | (true, RISCVHALF) -> "lhu"
+ | (false, RISCVWORD) -> "lw"
+ | (true, RISCVWORD) -> "lwu"
+ | (_, RISCVDOUBLE) -> "ld"
+ | _ -> failwith "unexpected load op"
+
+let pp_riscv_store_op width = match width with
+| RISCVBYTE -> "sb"
+| RISCVHALF -> "sh"
+| RISCVWORD -> "sw"
+| RISCVDOUBLE -> "sd"
+| _ -> failwith "unexpected store op"
+
+let pp_riscv_fence_option = function
+ | 0b0011 -> "rw"
+ | 0b0010 -> "r"
+ | 0b0001 -> "w"
+ | _ -> failwith "unexpected fence option"
diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen
new file mode 100644
index 00000000..e22110d0
--- /dev/null
+++ b/risc-v/hgen/types_sail_trans_out.hgen
@@ -0,0 +1,86 @@
+let translate_out_big_bit = function
+ | (name, Bvector _, bits) -> IInt.integer_of_bit_list bits
+ | _ -> assert false
+
+let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
+let translate_out_signed_int inst bits =
+ let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
+ if (i >= (1 lsl (bits - 1))) then
+ (i - (1 lsl bits)) else
+ i
+
+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
+let translate_out_imm4 imm = translate_out_int imm
+
+let translate_out_bool = function
+ | (name, Bit, [Bitc_one]) -> true
+ | (name, Bit, [Bitc_zero]) -> false
+ | _ -> assert false
+
+let translate_out_enum (name,_,bits) =
+ Nat_big_num.to_int (IInt.integer_of_bit_list bits)
+
+let translate_out_wordWidth w =
+ match translate_out_enum w with
+ | 0 -> RISCVBYTE
+ | 1 -> RISCVHALF
+ | 2 -> RISCVWORD
+ | 3 -> RISCVDOUBLE
+ | _ -> failwith "Unknown wordWidth in sail translate out"
+
+let translate_out_uop op = match translate_out_enum op with
+ | 0 -> RISCVLUI
+ | 1 -> RISCVAUIPC
+ | _ -> failwith "Unknown uop in sail translate out"
+
+let translate_out_bop op = match translate_out_enum op with
+| 0 -> RISCVBEQ
+| 1 -> RISCVBNE
+| 2 -> RISCVBLT
+| 3 -> RISCVBGE
+| 4 -> RISCVBLTU
+| 5 -> RISCVBGEU
+| _ -> failwith "Unknown bop in sail translate out"
+
+let translate_out_iop op = match translate_out_enum op with
+| 0 -> RISCVADDI
+| 1 -> RISCVSLTI
+| 2 -> RISCVSLTIU
+| 3 -> RISCVXORI
+| 4 -> RISCVORI
+| 5 -> RISCVANDI
+| _ -> failwith "Unknown iop in sail translate out"
+
+let translate_out_sop op = match translate_out_enum op with
+| 0 -> RISCVSLLI
+| 1 -> RISCVSRLI
+| 2 -> RISCVSRAI
+| _ -> failwith "Unknown sop in sail translate out"
+
+let translate_out_rop op = match translate_out_enum op with
+| 0 -> RISCVADD
+| 1 -> RISCVSUB
+| 2 -> RISCVSLL
+| 3 -> RISCVSLT
+| 4 -> RISCVSLTU
+| 5 -> RISCVXOR
+| 6 -> RISCVSRL
+| 7 -> RISCVSRA
+| 8 -> RISCVOR
+| 9 -> RISCVAND
+| _ -> failwith "Unknown rop in sail translate out"
+
+let translate_out_ropw op = match translate_out_enum op with
+| 0 -> RISCVADDW
+| 1 -> RISCVSUBW
+| 2 -> RISCVSLLW
+| 3 -> RISCVSRLW
+| 4 -> RISCVSRAW
+| _ -> failwith "Unknown ropw in sail translate out"
diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen
new file mode 100644
index 00000000..1bf174fa
--- /dev/null
+++ b/risc-v/hgen/types_trans_sail.hgen
@@ -0,0 +1,39 @@
+let translate_enum enum_values name value =
+ let rec bit_count n =
+ if n = 0 then 0
+ else 1 + (bit_count (n lsr 1)) in
+ let rec find_index element = function
+ | h::tail -> if h = element then 0 else 1 + (find_index element tail)
+ | _ -> failwith "translate_enum could not find value"
+ in
+ let size = bit_count (List.length enum_values) in
+ let index = find_index value enum_values in
+ (name, Range0 (Some size), IInt.bit_list_of_integer size (Nat_big_num.of_int index))
+
+let translate_uop = translate_enum [RISCVLUI; RISCVAUIPC]
+let translate_bop = translate_enum [RISCVBEQ; RISCVBNE; RISCVBLT; RISCVBGE; RISCVBLTU; RISCVBGEU] (* branch ops *)
+let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI; RISCVORI; RISCVANDI] (* immediate ops *)
+let translate_sop = translate_enum [RISCVSLLI; RISCVSRLI; RISCVSRAI] (* shift ops *)
+let translate_rop = translate_enum [RISCVADD; RISCVSUB; RISCVSLL; RISCVSLT; RISCVSLTU; RISCVXOR; RISCVSRL; RISCVSRA; RISCVOR; RISCVAND] (* reg-reg ops *)
+let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; RISCVSRAW] (* reg-reg 32-bit ops *)
+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 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 =
+ (name, Bvector (Some 6), bit_list_of_integer 6 (Nat_big_num.of_int value))
+let translate_imm5 name value =
+ (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value))
+let translate_imm4 name value =
+ (name, Bvector (Some 4), bit_list_of_integer 4 (Nat_big_num.of_int value))
+let translate_bool name value =
+ (name, Bit, [if value then Bitc_one else Bitc_zero])
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:25:01 +0000