summaryrefslogtreecommitdiff
path: root/risc-v/gen
diff options
context:
space:
mode:
Diffstat (limited to 'risc-v/gen')
-rw-r--r--risc-v/gen/ast.hgen17
-rw-r--r--risc-v/gen/fold.hgen16
-rw-r--r--risc-v/gen/herdtools_ast_to_shallow_ast.hgen86
-rw-r--r--risc-v/gen/herdtools_types_to_shallow_types.hgen90
-rw-r--r--risc-v/gen/lexer.hgen190
-rw-r--r--risc-v/gen/map.hgen15
-rw-r--r--risc-v/gen/parser.hgen74
-rw-r--r--risc-v/gen/pretty.hgen30
-rw-r--r--risc-v/gen/pretty_xml.hgen137
-rw-r--r--risc-v/gen/sail_trans_out.hgen23
-rw-r--r--risc-v/gen/shallow_ast_to_herdtools_ast.hgen23
-rw-r--r--risc-v/gen/shallow_types_to_herdtools_types.hgen84
-rw-r--r--risc-v/gen/token_types.hgen23
-rw-r--r--risc-v/gen/tokens.hgen19
-rw-r--r--risc-v/gen/trans_sail.hgen153
-rw-r--r--risc-v/gen/types.hgen172
-rw-r--r--risc-v/gen/types_sail_trans_out.hgen98
-rw-r--r--risc-v/gen/types_trans_sail.hgen57
18 files changed, 0 insertions, 1307 deletions
diff --git a/risc-v/gen/ast.hgen b/risc-v/gen/ast.hgen
deleted file mode 100644
index b1968173..00000000
--- a/risc-v/gen/ast.hgen
+++ /dev/null
@@ -1,17 +0,0 @@
-| `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 * bool * bool
-| `RISCVStore of bit12 * reg * reg * wordWidth * bool * bool
-| `RISCVADDIW of bit12 * reg * reg
-| `RISCVSHIFTW of bit5 * reg * reg * riscvSop
-| `RISCVRTYPEW of reg * reg * reg * riscvRopw
-| `RISCVFENCE of bit4 * bit4
-| `RISCVFENCEI
-| `RISCVLoadRes of bool * bool * reg * wordWidth * reg
-| `RISCVStoreCon of bool * bool * reg * reg * wordWidth * reg
-| `RISCVAMO of riscvAmoop * bool * bool * reg * reg * wordWidth * reg
diff --git a/risc-v/gen/fold.hgen b/risc-v/gen/fold.hgen
deleted file mode 100644
index 4c51e114..00000000
--- a/risc-v/gen/fold.hgen
+++ /dev/null
@@ -1,16 +0,0 @@
-| `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)))
-| `RISCVLoadRes (_, _, rs1, _, rd) -> fold_reg rs1 (fold_reg rd (y_reg, y_sreg))
-| `RISCVStoreCon (_, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg)))
-| `RISCVAMO (_, _, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg)))
diff --git a/risc-v/gen/herdtools_ast_to_shallow_ast.hgen b/risc-v/gen/herdtools_ast_to_shallow_ast.hgen
deleted file mode 100644
index 07c1d082..00000000
--- a/risc-v/gen/herdtools_ast_to_shallow_ast.hgen
+++ /dev/null
@@ -1,86 +0,0 @@
-| `RISCVStopFetching -> EBREAK
-| `RISCVUTYPE(imm, rd, op) -> UTYPE(
- translate_imm20 "imm" imm,
- translate_reg "rd" rd,
- translate_uop op)
-| `RISCVJAL(imm, rd) -> RISCV_JAL(
- translate_imm21 "imm" imm,
- translate_reg "rd" rd)
-| `RISCVJALR(imm, rs, rd) -> RISCV_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)
-| `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, aq, rl) -> LOAD(
- translate_imm12 "imm" imm,
- translate_reg "rs" rs,
- translate_reg "rd" rd,
- translate_bool "unsigned" unsigned,
- translate_wordWidth width,
- translate_bool "aq" aq,
- translate_bool "rl" rl)
-| `RISCVStore(imm, rs, rd, width, aq, rl) -> STORE (
- translate_imm12 "imm" imm,
- translate_reg "rs" rs,
- translate_reg "rd" rd,
- translate_wordWidth width,
- translate_bool "aq" aq,
- translate_bool "rl" rl)
-| `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)
-| `RISCVFENCEI -> FENCEI
-| `RISCVLoadRes(aq, rl, rs1, width, rd) -> LOADRES(
- translate_bool "aq" aq,
- translate_bool "rl" rl,
- translate_reg "rs1" rs1,
- translate_wordWidth width,
- translate_reg "rd" rd)
-| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> STORECON(
- translate_bool "aq" aq,
- translate_bool "rl" rl,
- translate_reg "rs2" rs2,
- translate_reg "rs1" rs1,
- translate_wordWidth width,
- translate_reg "rd" rd)
-| `RISCVAMO (op, aq, rl, rs2, rs1, width, rd) -> AMO(
- translate_amoop op,
- translate_bool "aq" aq,
- translate_bool "rl" rl,
- translate_reg "rs2" rs2,
- translate_reg "rs1" rs1,
- translate_wordWidth width,
- translate_reg "rd" rd)
diff --git a/risc-v/gen/herdtools_types_to_shallow_types.hgen b/risc-v/gen/herdtools_types_to_shallow_types.hgen
deleted file mode 100644
index e6edd24d..00000000
--- a/risc-v/gen/herdtools_types_to_shallow_types.hgen
+++ /dev/null
@@ -1,90 +0,0 @@
-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 -> RISCV_LUI
- | RISCVAUIPC -> RISCV_AUIPC
-
-let translate_bop op = match op with
- | RISCVBEQ -> RISCV_BEQ
- | RISCVBNE -> RISCV_BNE
- | RISCVBLT -> RISCV_BLT
- | RISCVBGE -> RISCV_BGE
- | RISCVBLTU -> RISCV_BLTU
- | RISCVBGEU -> RISCV_BGEU
-
-let translate_iop op = match op with
- | RISCVADDI -> RISCV_ADDI
- | RISCVSLTI -> RISCV_SLTI
- | RISCVSLTIU -> RISCV_SLTIU
- | RISCVXORI -> RISCV_XORI
- | RISCVORI -> RISCV_ORI
- | RISCVANDI -> RISCV_ANDI
-
-let translate_sop op = match op with
- | RISCVSLLI -> RISCV_SLLI
- | RISCVSRLI -> RISCV_SRLI
- | RISCVSRAI -> RISCV_SRAI
-
-let translate_rop op = match op with
- | RISCVADD -> RISCV_ADD
- | RISCVSUB -> RISCV_SUB
- | RISCVSLL -> RISCV_SLL
- | RISCVSLT -> RISCV_SLT
- | RISCVSLTU -> RISCV_SLTU
- | RISCVXOR -> RISCV_XOR
- | RISCVSRL -> RISCV_SRL
- | RISCVSRA -> RISCV_SRA
- | RISCVOR -> RISCV_OR
- | RISCVAND -> RISCV_AND
-
-let translate_ropw op = match op with
- | RISCVADDW -> RISCV_ADDW
- | RISCVSUBW -> RISCV_SUBW
- | RISCVSLLW -> RISCV_SLLW
- | RISCVSRLW -> RISCV_SRLW
- | RISCVSRAW -> RISCV_SRAW
-
-let translate_amoop op = match op with
- | RISCVAMOSWAP -> AMOSWAP
- | RISCVAMOADD -> AMOADD
- | RISCVAMOXOR -> AMOXOR
- | RISCVAMOAND -> AMOAND
- | RISCVAMOOR -> AMOOR
- | RISCVAMOMIN -> AMOMIN
- | RISCVAMOMAX -> AMOMAX
- | RISCVAMOMINU -> AMOMINU
- | RISCVAMOMAXU -> AMOMAXU
-
-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/gen/lexer.hgen b/risc-v/gen/lexer.hgen
deleted file mode 100644
index e42b8a62..00000000
--- a/risc-v/gen/lexer.hgen
+++ /dev/null
@@ -1,190 +0,0 @@
-"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; aq=false; rl=false};
-"lbu", LOAD{unsigned=true; width=RISCVBYTE; aq=false; rl=false};
-"lh", LOAD{unsigned=false; width=RISCVHALF; aq=false; rl=false};
-"lhu", LOAD{unsigned=true; width=RISCVHALF; aq=false; rl=false};
-"lw", LOAD{unsigned=false; width=RISCVWORD; aq=false; rl=false};
-"lwu", LOAD{unsigned=true; width=RISCVWORD; aq=false; rl=false};
-"ld", LOAD{unsigned=false; width=RISCVDOUBLE; aq=false; rl=false};
-
-"lb.aq", LOAD{unsigned=false; width=RISCVBYTE; aq=true; rl=false};
-"lbu.aq", LOAD{unsigned=true; width=RISCVBYTE; aq=true; rl=false};
-"lh.aq", LOAD{unsigned=false; width=RISCVHALF; aq=true; rl=false};
-"lhu.aq", LOAD{unsigned=true; width=RISCVHALF; aq=true; rl=false};
-"lw.aq", LOAD{unsigned=false; width=RISCVWORD; aq=true; rl=false};
-"lwu.aq", LOAD{unsigned=true; width=RISCVWORD; aq=true; rl=false};
-"ld.aq", LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=false};
-
-"lb.aq.rl", LOAD{unsigned=false; width=RISCVBYTE; aq=true; rl=true};
-"lbu.aq.rl", LOAD{unsigned=true; width=RISCVBYTE; aq=true; rl=true};
-"lh.aq.rl", LOAD{unsigned=false; width=RISCVHALF; aq=true; rl=true};
-"lhu.aq.rl", LOAD{unsigned=true; width=RISCVHALF; aq=true; rl=true};
-"lw.aq.rl", LOAD{unsigned=false; width=RISCVWORD; aq=true; rl=true};
-"lwu.aq.rl", LOAD{unsigned=true; width=RISCVWORD; aq=true; rl=true};
-"ld.aq.rl", LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=true};
-
-"sb", STORE{width=RISCVBYTE; aq=false; rl=false};
-"sh", STORE{width=RISCVHALF; aq=false; rl=false};
-"sw", STORE{width=RISCVWORD; aq=false; rl=false};
-"sd", STORE{width=RISCVDOUBLE; aq=false; rl=false};
-
-"sb.rl", STORE{width=RISCVBYTE; aq=false; rl=true};
-"sh.rl", STORE{width=RISCVHALF; aq=false; rl=true};
-"sw.rl", STORE{width=RISCVWORD; aq=false; rl=true};
-"sd.rl", STORE{width=RISCVDOUBLE; aq=false; rl=true};
-
-"sb.aq.rl", STORE{width=RISCVBYTE; aq=true; rl=true};
-"sh.aq.rl", STORE{width=RISCVHALF; aq=true; rl=true};
-"sw.aq.rl", STORE{width=RISCVWORD; aq=true; rl=true};
-"sd.aq.rl", STORE{width=RISCVDOUBLE; aq=true; rl=true};
-
-"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;
-
-"fence.i", FENCEI ();
-
-"lr.w", LOADRES {width=RISCVWORD; aq=false; rl=false};
-"lr.w.aq", LOADRES {width=RISCVWORD; aq=true; rl=false};
-"lr.w.aq.rl", LOADRES {width=RISCVWORD; aq=true; rl=true};
-"lr.d", LOADRES {width=RISCVDOUBLE; aq=false; rl=false};
-"lr.d.aq", LOADRES {width=RISCVDOUBLE; aq=true; rl=false};
-"lr.d.aq.rl", LOADRES {width=RISCVDOUBLE; aq=true; rl=true};
-
-"sc.w", STORECON {width=RISCVWORD; aq=false; rl=false};
-"sc.w.rl", STORECON {width=RISCVWORD; aq=false; rl=true};
-"sc.w.aq.rl", STORECON {width=RISCVWORD; aq=true; rl=true};
-"sc.d", STORECON {width=RISCVDOUBLE; aq=false; rl=false};
-"sc.d.rl", STORECON {width=RISCVDOUBLE; aq=false; rl=true};
-"sc.d.aq.rl", STORECON {width=RISCVDOUBLE; aq=true; rl=true};
-
-"amoswap.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOSWAP};
-"amoadd.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOADD};
-"amoand.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOAND};
-"amoor.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOOR};
-"amoxor.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOXOR};
-"amomax.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMAX};
-"amomin.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMIN};
-"amomaxu.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMAXU};
-"amominu.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMINU};
-
-"amoswap.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOSWAP};
-"amoadd.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOADD};
-"amoand.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOAND};
-"amoor.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOOR};
-"amoxor.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOXOR};
-"amomax.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMAX};
-"amomin.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMIN};
-"amomaxu.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMAXU};
-"amominu.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMINU};
-
-"amoswap.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOSWAP};
-"amoadd.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOADD};
-"amoand.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOAND};
-"amoor.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOOR};
-"amoxor.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOXOR};
-"amomax.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMAX};
-"amomin.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMIN};
-"amomaxu.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMAXU};
-"amominu.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMINU};
-
-"amoswap.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOSWAP};
-"amoadd.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOADD};
-"amoand.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOAND};
-"amoor.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOOR};
-"amoxor.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOXOR};
-"amomax.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMAX};
-"amomin.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMIN};
-"amomaxu.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMAXU};
-"amominu.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMINU};
-
-"amoswap.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOSWAP};
-"amoadd.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOADD};
-"amoand.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOAND};
-"amoor.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOOR};
-"amoxor.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOXOR};
-"amomax.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMAX};
-"amomin.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMIN};
-"amomaxu.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMAXU};
-"amominu.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMINU};
-
-"amoswap.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOSWAP};
-"amoadd.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOADD};
-"amoand.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOAND};
-"amoor.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOOR};
-"amoxor.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOXOR};
-"amomax.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMAX};
-"amomin.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMIN};
-"amomaxu.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMAXU};
-"amominu.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMINU};
-
-"amoswap.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOSWAP};
-"amoadd.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOADD};
-"amoand.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOAND};
-"amoor.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOOR};
-"amoxor.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOXOR};
-"amomax.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMAX};
-"amomin.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMIN};
-"amomaxu.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMAXU};
-"amominu.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMINU};
-
-"amoswap.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOSWAP};
-"amoadd.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOADD};
-"amoand.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOAND};
-"amoor.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOOR};
-"amoxor.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOXOR};
-"amomax.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMAX};
-"amomin.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMIN};
-"amomaxu.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMAXU};
-"amominu.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMINU};
-
-(** pseudo instructions *********************************************)
-
-"li", LI ()
diff --git a/risc-v/gen/map.hgen b/risc-v/gen/map.hgen
deleted file mode 100644
index bab5ced8..00000000
--- a/risc-v/gen/map.hgen
+++ /dev/null
@@ -1,15 +0,0 @@
-| `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, a, b) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a, b)
-| `RISCVStore (x, r0, r1, y, z, a) -> `RISCVStore (x, map_reg r0, map_reg r1, y, z, a)
-| `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)
-| `RISCVLoadRes (aq, rl, rs1, w, rd) -> `RISCVLoadRes (aq, rl, map_reg rs1, w, map_reg rd)
-| `RISCVStoreCon (aq, rl, rs2, rs1, w, rd) -> `RISCVStoreCon (aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd)
-| `RISCVAMO (op, aq, rl, rs2, rs1, w, rd) -> `RISCVAMO (op, aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd)
diff --git a/risc-v/gen/parser.hgen b/risc-v/gen/parser.hgen
deleted file mode 100644
index 210e38fb..00000000
--- a/risc-v/gen/parser.hgen
+++ /dev/null
@@ -1,74 +0,0 @@
-| UTYPE reg COMMA NUM
- { (* it's not clear if NUM here should be before or after filling the
- lowest 12 bits with zeros, or if it should be signed or unsigned;
- currently assuming: NUM does not include the 12 zeros, and is unsigned *)
- if not (iskbituimm 20 $4) then failwith "immediate is not 20bit"
- else `RISCVUTYPE ($4, $2, $1.op) }
-| JAL reg COMMA NUM
- { if not ($4 mod 2 = 0) then failwith "odd offset"
- else if not (iskbitsimm 21 $4) then failwith "offset is not 21bit"
- else `RISCVJAL ($4, $2) }
-| JALR reg COMMA reg COMMA NUM
- { if not (iskbitsimm 12 $6) then failwith "offset is not 12bit"
- else `RISCVJALR ($6, $4, $2) }
-| BTYPE reg COMMA reg COMMA NUM
- { if not ($6 mod 2 = 0) then failwith "odd offset"
- else if not (iskbitsimm 13 $6) then failwith "offset is not 13bit"
- else `RISCVBType ($6, $4, $2, $1.op) }
-| ITYPE reg COMMA reg COMMA NUM
- { if $1.op <> RISCVSLTIU && not (iskbitsimm 12 $6) then failwith "immediate is not 12bit"
- else if $1.op = RISCVSLTIU && not (iskbituimm 12 $6) then failwith "unsigned immediate is not 12bit"
- else `RISCVIType ($6, $4, $2, $1.op) }
-| ADDIW reg COMMA reg COMMA NUM
- { if not (iskbitsimm 12 $6) then failwith "immediate is not 12bit"
- else `RISCVADDIW ($6, $4, $2) }
-| SHIFTIOP reg COMMA reg COMMA NUM
- { if not (iskbituimm 6 $6) then failwith "unsigned immediate is not 6bit"
- else `RISCVShiftIop ($6, $4, $2, $1.op) }
-| SHIFTW reg COMMA reg COMMA NUM
- { if not (iskbituimm 5 $6) then failwith "unsigned immediate is not 5bit"
- else `RISCVSHIFTW ($6, $4, $2, $1.op) }
-| RTYPE reg COMMA reg COMMA reg
- { `RISCVRType ($6, $4, $2, $1.op) }
-| LOAD reg COMMA NUM LPAR reg RPAR
- { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit"
- else `RISCVLoad ($4, $6, $2, $1.unsigned, $1.width, $1.aq, $1.rl) }
-| STORE reg COMMA NUM LPAR reg RPAR
- { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit"
- else `RISCVStore ($4, $2, $6, $1.width, $1.aq, $1.rl) }
-| 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_R, Fence_R) -> `RISCVFENCE (0b0010, 0b0010)
- | (Fence_RW, Fence_W) -> `RISCVFENCE (0b0011, 0b0001)
- | (Fence_W, Fence_W) -> `RISCVFENCE (0b0001, 0b0001)
- | (Fence_RW, Fence_R) -> failwith "'fence rw,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"
- }
-| FENCEI
- { `RISCVFENCEI }
-| LOADRES reg COMMA LPAR reg RPAR
- { `RISCVLoadRes ($1.aq, $1.rl, $5, $1.width, $2) }
-| LOADRES reg COMMA NUM LPAR reg RPAR
- { if $4 <> 0 then failwith "'lr' offset must be 0" else
- `RISCVLoadRes ($1.aq, $1.rl, $6, $1.width, $2) }
-| STORECON reg COMMA reg COMMA LPAR reg RPAR
- { `RISCVStoreCon ($1.aq, $1.rl, $4, $7, $1.width, $2) }
-| STORECON reg COMMA reg COMMA NUM LPAR reg RPAR
- { if $6 <> 0 then failwith "'sc' offset must be 0" else
- `RISCVStoreCon ($1.aq, $1.rl, $4, $8, $1.width, $2) }
-| AMO reg COMMA reg COMMA LPAR reg RPAR
- { `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $7, $1.width, $2) }
-| AMO reg COMMA reg COMMA NUM LPAR reg RPAR
- { if $6 <> 0 then failwith "'amo<op>' offset must be 0" else
- `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $8, $1.width, $2) }
-
-/* pseudo-ops */
-| LI reg COMMA NUM
- { if not (iskbitsimm 12 $4) then failwith "immediate is not 12bit (li is currently implemented only with small immediate)"
- else `RISCVIType ($4, IReg R0, $2, RISCVORI) }
diff --git a/risc-v/gen/pretty.hgen b/risc-v/gen/pretty.hgen
deleted file mode 100644
index fc1c0000..00000000
--- a/risc-v/gen/pretty.hgen
+++ /dev/null
@@ -1,30 +0,0 @@
-| `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, aq, rl) ->
- sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq, rl)) (pp_reg rd) imm (pp_reg rs)
-
-| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
- sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, aq, rl)) (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)
-| `RISCVFENCEI -> sprintf "fence.i"
-
-| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
- sprintf "%s %s, (%s)" (pp_riscv_load_reserved_op (aq, rl, width)) (pp_reg rd) (pp_reg rs1)
-
-| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
- sprintf "%s %s, %s, (%s)" (pp_riscv_store_conditional_op (aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1)
-
-| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
- sprintf "%s %s, %s, (%s)" (pp_riscv_amo_op (op, aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1)
diff --git a/risc-v/gen/pretty_xml.hgen b/risc-v/gen/pretty_xml.hgen
deleted file mode 100644
index b0306161..00000000
--- a/risc-v/gen/pretty_xml.hgen
+++ /dev/null
@@ -1,137 +0,0 @@
-| `RISCVThreadStart -> ("op_thread_start", [])
-
-| `RISCVStopFetching -> ("op_stop_fetching", [])
-
-| `RISCVUTYPE(imm, rd, op) ->
- ("op_U_type",
- [ ("op", pp_riscv_uop op);
- ("uimm", sprintf "%d" imm);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVJAL(imm, rd) ->
- ("op_jal",
- [ ("offset", sprintf "%d" imm);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVJALR(imm, rs1, rd) ->
- ("op_jalr",
- [ ("offset", sprintf "%d" imm);
- ("base", pp_reg rs1);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVBType(imm, rs2, rs1, op) ->
- ("op_branch",
- [ ("op", pp_riscv_bop op);
- ("offset", sprintf "%d" imm);
- ("src2", pp_reg rs2);
- ("src1", pp_reg rs1);
- ])
-
-| `RISCVIType(imm, rs1, rd, op) ->
- ("op_I_type",
- [ ("op", pp_riscv_iop op);
- ("iimm", sprintf "%d" imm);
- ("src", pp_reg rs1);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVShiftIop(imm, rs1, rd, op) ->
- ("op_IS_type",
- [ ("op", pp_riscv_sop op);
- ("shamt", sprintf "%d" imm);
- ("src", pp_reg rs1);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVSHIFTW(imm, rs1, rd, op) ->
- ("op_ISW_type",
- [ ("op", pp_riscv_sop op);
- ("shamt", sprintf "%d" imm);
- ("src", pp_reg rs1);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVRType (rs2, rs1, rd, op) ->
- ("op_R_type",
- [ ("op", pp_riscv_rop op);
- ("src2", pp_reg rs2);
- ("src1", pp_reg rs1);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVLoad(imm, rs1, rd, unsigned, width, aq, rl) ->
- ("op_load",
- [ ("aq", if aq then "true" else "false");
- ("rl", if rl then "true" else "false");
- ("width", pp_word_width width);
- ("unsigned", if unsigned then "true" else "false");
- ("base", pp_reg rs1);
- ("offset", sprintf "%d" imm);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
- ("op_store",
- [ ("aq", if aq then "true" else "false");
- ("rl", if rl then "true" else "false");
- ("width", pp_word_width width);
- ("src", pp_reg rs2);
- ("base", pp_reg rs1);
- ("offset", sprintf "%d" imm);
- ])
-
-| `RISCVADDIW(imm, rs1, rd) ->
- ("op_addiw",
- [ ("iimm", sprintf "%d" imm);
- ("src", pp_reg rs1);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVRTYPEW(rs2, rs1, rd, op) ->
- ("op_RW_type",
- [ ("op", pp_riscv_ropw op);
- ("src2", pp_reg rs2);
- ("src1", pp_reg rs1);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVFENCE(pred, succ) ->
- ("op_fence",
- [ ("pred", pp_riscv_fence_option pred);
- ("succ", pp_riscv_fence_option succ);
- ])
-
-| `RISCVFENCEI -> ("op_fence_i", [])
-
-| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
- ("op_lr",
- [ ("aq", if aq then "true" else "false");
- ("rl", if rl then "true" else "false");
- ("width", pp_word_width width);
- ("addr", pp_reg rs1);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
- ("op_sc",
- [ ("aq", if aq then "true" else "false");
- ("rl", if rl then "true" else "false");
- ("width", pp_word_width width);
- ("addr", pp_reg rs1);
- ("src", pp_reg rs2);
- ("dest", pp_reg rd);
- ])
-
-| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
- ("op_amo",
- [ ("op", pp_riscv_amo_op_part op);
- ("aq", if aq then "true" else "false");
- ("rl", if rl then "true" else "false");
- ("width", pp_word_width width);
- ("src", pp_reg rs2);
- ("addr", pp_reg rs1);
- ("dest", pp_reg rd);
- ])
diff --git a/risc-v/gen/sail_trans_out.hgen b/risc-v/gen/sail_trans_out.hgen
deleted file mode 100644
index 2f9a80f1..00000000
--- a/risc-v/gen/sail_trans_out.hgen
+++ /dev/null
@@ -1,23 +0,0 @@
-| ("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; aq; rl])
- -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
-| ("STORE", [imm; rs; rd; width; aq; rl])
- -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
-| ("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)
-| ("FENCEI", []) -> `RISCVFENCEI
-| ("LOADRES", [aq; rl; rs1; width; rd])
- -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
-| ("STORECON", [aq; rl; rs2; rs1; width; rd])
- -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
-| ("AMO", [op; aq; rl; rs2; rs1; width; rd])
- -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
diff --git a/risc-v/gen/shallow_ast_to_herdtools_ast.hgen b/risc-v/gen/shallow_ast_to_herdtools_ast.hgen
deleted file mode 100644
index 3025992e..00000000
--- a/risc-v/gen/shallow_ast_to_herdtools_ast.hgen
+++ /dev/null
@@ -1,23 +0,0 @@
-| EBREAK -> `RISCVStopFetching
-| UTYPE( imm, rd, op) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
-| RISCV_JAL( imm, rd) -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg rd)
-| RISCV_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, aq, rl)
- -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
-| STORE( imm, rs, rd, width, aq, rl)
- -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
-| 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)
-| FENCEI -> `RISCVFENCEI
-| LOADRES( aq, rl, rs1, width, rd)
- -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
-| STORECON( aq, rl, rs2, rs1, width, rd)
- -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
-| AMO( op, aq, rl, rs2, rs1, width, rd)
- -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
diff --git a/risc-v/gen/shallow_types_to_herdtools_types.hgen b/risc-v/gen/shallow_types_to_herdtools_types.hgen
deleted file mode 100644
index 6b3b7f51..00000000
--- a/risc-v/gen/shallow_types_to_herdtools_types.hgen
+++ /dev/null
@@ -1,84 +0,0 @@
-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
- | RISCV_LUI -> RISCVLUI
- | RISCV_AUIPC -> RISCVAUIPC
-
-let translate_out_bop op = match op with
- | RISCV_BEQ -> RISCVBEQ
- | RISCV_BNE -> RISCVBNE
- | RISCV_BLT -> RISCVBLT
- | RISCV_BGE -> RISCVBGE
- | RISCV_BLTU -> RISCVBLTU
- | RISCV_BGEU -> RISCVBGEU
-
-let translate_out_iop op = match op with
- | RISCV_ADDI -> RISCVADDI
- | RISCV_SLTI -> RISCVSLTI
- | RISCV_SLTIU -> RISCVSLTIU
- | RISCV_XORI -> RISCVXORI
- | RISCV_ORI -> RISCVORI
- | RISCV_ANDI -> RISCVANDI
-
-let translate_out_sop op = match op with
- | RISCV_SLLI -> RISCVSLLI
- | RISCV_SRLI -> RISCVSRLI
- | RISCV_SRAI -> RISCVSRAI
-
-let translate_out_rop op = match op with
- | RISCV_ADD -> RISCVADD
- | RISCV_SUB -> RISCVSUB
- | RISCV_SLL -> RISCVSLL
- | RISCV_SLT -> RISCVSLT
- | RISCV_SLTU -> RISCVSLTU
- | RISCV_XOR -> RISCVXOR
- | RISCV_SRL -> RISCVSRL
- | RISCV_SRA -> RISCVSRA
- | RISCV_OR -> RISCVOR
- | RISCV_AND -> RISCVAND
-
-let translate_out_ropw op = match op with
- | RISCV_ADDW -> RISCVADDW
- | RISCV_SUBW -> RISCVSUBW
- | RISCV_SLLW -> RISCVSLLW
- | RISCV_SRLW -> RISCVSRLW
- | RISCV_SRAW -> RISCVSRAW
-
-let translate_out_amoop op = match op with
- | AMOSWAP -> RISCVAMOSWAP
- | AMOADD -> RISCVAMOADD
- | AMOXOR -> RISCVAMOXOR
- | AMOAND -> RISCVAMOAND
- | AMOOR -> RISCVAMOOR
- | AMOMIN -> RISCVAMOMIN
- | AMOMAX -> RISCVAMOMAX
- | AMOMINU -> RISCVAMOMINU
- | AMOMAXU -> RISCVAMOMAXU
-
-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/gen/token_types.hgen b/risc-v/gen/token_types.hgen
deleted file mode 100644
index f29e318d..00000000
--- a/risc-v/gen/token_types.hgen
+++ /dev/null
@@ -1,23 +0,0 @@
-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; aq: bool; rl: bool }
-type token_Store = {width : wordWidth; aq: bool; rl: bool }
-type token_ADDIW = unit
-type token_SHIFTW = {op : riscvSop }
-type token_RTYPEW = {op : riscvRopw }
-type token_FENCE = unit
-type token_FENCEI = unit
-type token_LoadRes = {width : wordWidth; aq: bool; rl: bool }
-type token_StoreCon = {width : wordWidth; aq: bool; rl: bool }
-type token_AMO = {width : wordWidth; aq: bool; rl: bool; op: riscvAmoop }
-
-type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW
-
-(* pseudo-ops *)
-
-type token_LI = unit
diff --git a/risc-v/gen/tokens.hgen b/risc-v/gen/tokens.hgen
deleted file mode 100644
index f812adbd..00000000
--- a/risc-v/gen/tokens.hgen
+++ /dev/null
@@ -1,19 +0,0 @@
-%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
-%token <RISCVHGenBase.token_FENCEI> FENCEI
-%token <RISCVHGenBase.token_LoadRes> LOADRES
-%token <RISCVHGenBase.token_StoreCon> STORECON
-%token <RISCVHGenBase.token_AMO> AMO
-%token <RISCVHGenBase.token_LI> LI
diff --git a/risc-v/gen/trans_sail.hgen b/risc-v/gen/trans_sail.hgen
deleted file mode 100644
index 8b7cbe11..00000000
--- a/risc-v/gen/trans_sail.hgen
+++ /dev/null
@@ -1,153 +0,0 @@
-| `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, aq, rl) ->
- ("LOAD",
- [
- translate_imm12 "imm" imm;
- translate_reg "rs" rs;
- translate_reg "rd" rd;
- translate_bool "unsigned" unsigned;
- translate_width "width" width;
- translate_bool "aq" aq;
- translate_bool "rl" rl;
- ],
- [])
-| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
- ("STORE",
- [
- translate_imm12 "imm" imm;
- translate_reg "rs2" rs2;
- translate_reg "rs1" rs1;
- translate_width "width" width;
- translate_bool "aq" aq;
- translate_bool "rl" rl;
- ],
- [])
-| `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;
- ],
- [])
-| `RISCVFENCEI ->
- ("FENCEI",
- [],
- [])
-| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
- ("LOADRES",
- [
- translate_bool "aq" aq;
- translate_bool "rl" rl;
- translate_reg "rs1" rs1;
- translate_width "width" width;
- translate_reg "rd" rd;
- ],
- [])
-| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
- ("STORECON",
- [
- translate_bool "aq" aq;
- translate_bool "rl" rl;
- translate_reg "rs2" rs2;
- translate_reg "rs1" rs1;
- translate_width "width" width;
- translate_reg "rd" rd;
- ],
- [])
-| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
- ("AMO",
- [
- translate_amoop "op" op;
- translate_bool "aq" aq;
- translate_bool "rl" rl;
- translate_reg "rs2" rs2;
- translate_reg "rs1" rs1;
- translate_width "width" width;
- translate_reg "rd" rd;
- ],
- [])
diff --git a/risc-v/gen/types.hgen b/risc-v/gen/types.hgen
deleted file mode 100644
index a0b75606..00000000
--- a/risc-v/gen/types.hgen
+++ /dev/null
@@ -1,172 +0,0 @@
-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_word_width width : string =
- begin match width with
- | RISCVBYTE -> "b"
- | RISCVHALF -> "h"
- | RISCVWORD -> "w"
- | RISCVDOUBLE -> "d"
- end
-
-let pp_riscv_load_op (unsigned, width, aq, rl) =
- "l" ^
- (pp_word_width width) ^
- (if unsigned then "u" else "") ^
- (if aq then ".aq" else "") ^
- (if rl then ".rl" else "")
-
-let pp_riscv_store_op (width, aq, rl) =
- "s" ^
- (pp_word_width width) ^
- (if aq then ".aq" else "") ^
- (if rl then ".rl" else "")
-
-let pp_riscv_load_reserved_op (aq, rl, width) =
- "lr." ^
- (pp_word_width width) ^
- (if aq then ".aq" else "") ^
- (if rl then ".rl" else "")
-
-let pp_riscv_store_conditional_op (aq, rl, width) =
- "sc." ^
- (pp_word_width width) ^
- (if aq then ".aq" else "") ^
- (if rl then ".rl" else "")
-
-type riscvAmoop =
- | RISCVAMOSWAP
- | RISCVAMOADD
- | RISCVAMOXOR
- | RISCVAMOAND
- | RISCVAMOOR
- | RISCVAMOMIN
- | RISCVAMOMAX
- | RISCVAMOMINU
- | RISCVAMOMAXU
-
-let pp_riscv_amo_op_part = function
- | RISCVAMOSWAP -> "swap"
- | RISCVAMOADD -> "add"
- | RISCVAMOXOR -> "xor"
- | RISCVAMOAND -> "and"
- | RISCVAMOOR -> "or"
- | RISCVAMOMIN -> "min"
- | RISCVAMOMAX -> "max"
- | RISCVAMOMINU -> "minu"
- | RISCVAMOMAXU -> "maxu"
-
-let pp_riscv_amo_op (op, aq, rl, width) =
- "amo" ^
- pp_riscv_amo_op_part op ^
- begin match width with
- | RISCVWORD -> ".w"
- | RISCVDOUBLE -> ".d"
- | _ -> assert false
- end ^
- (if aq then ".aq" else "") ^
- (if rl then ".rl" else "")
-
-let pp_riscv_fence_option = function
- | 0b0011 -> "rw"
- | 0b0010 -> "r"
- | 0b0001 -> "w"
- | _ -> failwith "unexpected fence option"
diff --git a/risc-v/gen/types_sail_trans_out.hgen b/risc-v/gen/types_sail_trans_out.hgen
deleted file mode 100644
index 66a2020c..00000000
--- a/risc-v/gen/types_sail_trans_out.hgen
+++ /dev/null
@@ -1,98 +0,0 @@
-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"
-
-let translate_out_amoop op = match translate_out_enum op with
-| 0 -> RISCVAMOSWAP
-| 1 -> RISCVAMOADD
-| 2 -> RISCVAMOXOR
-| 3 -> RISCVAMOAND
-| 4 -> RISCVAMOOR
-| 5 -> RISCVAMOMIN
-| 6 -> RISCVAMOMAX
-| 7 -> RISCVAMOMINU
-| 8 -> RISCVAMOMAXU
-| _ -> failwith "Unknown amoop in sail translate out"
diff --git a/risc-v/gen/types_trans_sail.hgen b/risc-v/gen/types_trans_sail.hgen
deleted file mode 100644
index 238c7e5b..00000000
--- a/risc-v/gen/types_trans_sail.hgen
+++ /dev/null
@@ -1,57 +0,0 @@
-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_amoop = translate_enum [RISCVAMOSWAP; RISCVAMOADD; RISCVAMOXOR; RISCVAMOAND; RISCVAMOOR; RISCVAMOMIN; RISCVAMOMAX; RISCVAMOMINU; RISCVAMOMAXU]
-
-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-09 18:50:33 +0000