summaryrefslogtreecommitdiff
path: root/mips/hgen
diff options
context:
space:
mode:
Diffstat (limited to 'mips/hgen')
-rw-r--r--mips/hgen/herdtools_ast_to_shallow_ast.hgen121
-rw-r--r--mips/hgen/herdtools_types_to_shallow_types.hgen120
-rw-r--r--mips/hgen/shallow_ast_to_herdtools_ast.hgen98
-rw-r--r--mips/hgen/shallow_types_to_herdtools_types.hgen39
4 files changed, 378 insertions, 0 deletions
diff --git a/mips/hgen/herdtools_ast_to_shallow_ast.hgen b/mips/hgen/herdtools_ast_to_shallow_ast.hgen
new file mode 100644
index 00000000..7b1a58d9
--- /dev/null
+++ b/mips/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -0,0 +1,121 @@
+| `MIPSThreadStart ->
+ SYSCALL_THREAD_START
+
+| `MIPSStopFetching ->
+ ImplementationDefinedStopFetching0
+
+(* Note different argument order, which reflects difference
+ between instruction encoding and asm format *)
+| `MIPSRType (op, rd, rs, rt) ->
+ (translate_rtype_op op)
+ (
+ translate_reg "rs" rs,
+ translate_reg "rt" rt,
+ translate_reg "rd" rd
+ )
+
+
+(* Note different argument order similar to above *)
+| `MIPSIType (op, rt, rs, imm) ->
+ (translate_itype_op op)
+ (
+ translate_reg "rs" rs,
+ translate_reg "rt" rt,
+ translate_imm16 "imm" imm
+ )
+
+
+| `MIPSShiftI (op, rd, rt, sa) ->
+ (translate_shifti_op op)
+ (
+ translate_reg "rt" rt,
+ translate_reg "rd" rd,
+ translate_imm5 "sa" sa
+ )
+
+
+| `MIPSShiftV (op, rd, rt, rs) ->
+ (translate_shiftv_op op)
+ (
+ translate_reg "rs" rs,
+ translate_reg "rt" rt,
+ translate_reg "rd" rd
+ )
+
+
+| `MIPSMulDiv (op, rs, rt) ->
+ (translate_muldiv_op op)
+ (
+ translate_reg "rs" rs,
+ translate_reg "rt" rt
+ )
+
+
+| `MIPSMFHiLo (op, rs) ->
+ (translate_mfhilo_op op)
+ (
+ translate_reg "rs" rs
+ )
+
+| `MIPSLUI (rt, imm) ->
+ LUI
+ (
+ translate_reg "rt" rt,
+ translate_imm16 "imm" imm
+ )
+
+| `MIPSLoad (width, signed, linked, base, rt, offset) ->
+ Load
+ (
+ translate_wordsize "width" width,
+ translate_bool "signed" signed,
+ translate_bool "linked" linked,
+ translate_reg "base" base,
+ translate_reg "rt" rt,
+ translate_imm16 "offset" offset
+ )
+
+| `MIPSStore (width, conditional, base, rt, offset) ->
+ Store
+ (
+ translate_wordsize "width" width,
+ translate_bool "conditional" conditional,
+ translate_reg "base" base,
+ translate_reg "rt" rt,
+ translate_imm16 "offset" offset
+ )
+
+| `MIPSLSLR (store, double, left, base, rt, offset) ->
+ (translate_lslr_op store double left)
+ (
+ translate_reg "base" base,
+ translate_reg "rt" rt,
+ translate_imm16 "offset" offset
+ )
+
+| `MIPSSYNC -> SYNC
+| `MIPSBEQ (rs, rt, offset, ne, likely) ->
+ BEQ
+ (translate_reg "rs" rs,
+ translate_reg "rt" rt,
+ translate_imm16 "offset" offset,
+ translate_bool "ne" ne,
+ translate_bool "likely" likely
+ )
+
+| `MIPSBCMPZ (rs, offset, cmp, link, likely) ->
+ BCMPZ
+ (translate_reg "rs" rs,
+ translate_imm16 "offset" offset,
+ translate_cmp "cmp" cmp,
+ translate_bool "link" link,
+ translate_bool "likely" likely
+ )
+| `MIPSJ (offset) ->
+ J (translate_imm26 "offset" offset)
+| `MIPSJAL (offset) ->
+ JAL (translate_imm26 "offset" offset)
+| `MIPSJR(rd) ->
+ JR (translate_reg "rd" rd)
+| `MIPSJALR(rd, rs) ->
+ JALR (translate_reg "rd" rd, translate_reg "rs" rs)
diff --git a/mips/hgen/herdtools_types_to_shallow_types.hgen b/mips/hgen/herdtools_types_to_shallow_types.hgen
new file mode 100644
index 00000000..115de27c
--- /dev/null
+++ b/mips/hgen/herdtools_types_to_shallow_types.hgen
@@ -0,0 +1,120 @@
+let is_inc = false
+
+let translate_rtype_op op = uppercase (pp_rtype_op op)
+
+let translate_rtype_op op x = match op with
+ | MIPSROpADD -> ADD x
+ | MIPSROpADDU -> ADDU x
+ | MIPSROpAND -> AND x
+ | MIPSROpDADD -> DADD x
+ | MIPSROpDADDU -> DADDU x
+ | MIPSROpDSUB -> DSUB x
+ | MIPSROpDSUBU -> DSUBU x
+ | MIPSROpMOVN -> MOVN x
+ | MIPSROpMOVZ -> MOVZ x
+ | MIPSROpMUL -> MUL x
+ | MIPSROpNOR -> NOR x
+ | MIPSROpOR -> OR x
+ | MIPSROpSLT -> SLT x
+ | MIPSROpSLTU -> SLTU x
+ | MIPSROpSUB -> SUB x
+ | MIPSROpSUBU -> SUBU x
+ | MIPSROpXOR -> XOR x
+
+let translate_itype_op op x = match op with
+ | MIPSIOpADDI -> ADDI x
+ | MIPSIOpADDIU -> ADDIU x
+ | MIPSIOpANDI -> ANDI x
+ | MIPSIOpDADDI -> DADDI x
+ | MIPSIOpDADDIU -> DADDIU x
+ | MIPSIOpORI -> ORI x
+ | MIPSIOpSLTI -> SLTI x
+ | MIPSIOpSLTIU -> SLTIU x
+ | MIPSIOpXORI -> XORI x
+
+let translate_shifti_op op x = match op with
+ | MIPSDSLL -> DSLL x
+ | MIPSDSLL32 -> DSLL32 x
+ | MIPSDSRA -> DSRA x
+ | MIPSDSRA32 -> DSRA32 x
+ | MIPSDSRL -> DSRL x
+ | MIPSDSRL32 -> DSRL32 x
+ | MIPSSLL -> SLL x
+ | MIPSSRA -> SRA x
+ | MIPSSRL -> SRL x
+
+let translate_shiftv_op op x = match op with
+ | MIPSDSLLV -> DSLLV x
+ | MIPSDSRAV -> DSRAV x
+ | MIPSDSRLV -> DSRLV x
+ | MIPSSLLV -> SLLV x
+ | MIPSSRAV -> SRAV x
+ | MIPSSRLV -> SRLV x
+
+let translate_muldiv_op op x = match op with
+ | MIPSDDIV -> DDIV x
+ | MIPSDDIVU -> DDIVU x
+ | MIPSDIV -> DIV x
+ | MIPSDIVU -> DIVU x
+ | MIPSDMULT -> DMULT x
+ | MIPSDMULTU -> DMULTU x
+ | MIPSMADD -> MADD x
+ | MIPSMADDU -> MADDU x
+ | MIPSMSUB -> MSUB x
+ | MIPSMSUBU -> MSUBU x
+ | MIPSMULT -> MULT x
+ | MIPSMULTU -> MULTU x
+
+let translate_mfhilo_op op x = match op with
+ | MIPSMFHI -> MFHI x
+ | MIPSMFLO -> MFLO x
+ | MIPSMTHI -> MTHI x
+ | MIPSMTLO -> MTLO x
+
+let translate_load_op width signed linked = uppercase (pp_load_op width signed linked)
+
+let translate_store_op width conditional = uppercase (pp_store_op width conditional)
+
+let translate_lslr_op store double left x = match (store,double,left) with
+ | (false, false, true ) -> LWL x
+ | (false, false, false) -> LWR x
+ | (false, true , true ) -> LDL x
+ | (false, true , false) -> LDR x
+ | (true , false, true ) -> SWL x
+ | (true , false, false) -> SWR x
+ | (true , true , true ) -> SDL x
+ | (true , true , false) -> SDR x
+
+let translate_beq_op ne likely = uppercase (pp_beq_op ne likely)
+
+let translate_bcmpz_op cmp link likely = uppercase (pp_bcmpz_op cmp link likely)
+
+
+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_imm26 name value =
+ Sail_values.to_vec0 is_inc (Nat_big_num.of_int 26,Nat_big_num.of_int value)
+let translate_imm16 name value =
+ Sail_values.to_vec0 is_inc (Nat_big_num.of_int 16,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_bool name = function
+ | true -> Sail_values.I
+ | false -> Sail_values.O
+
+let translate_wordsize _ = function
+ | MIPSByte -> Mips_embed_types.B0
+ | MIPSHalf -> Mips_embed_types.H
+ | MIPSWord -> Mips_embed_types.W
+ | MIPSDouble -> Mips_embed_types.D
+
+let translate_cmp _ = function
+ | MIPS_EQ -> EQ_
+ | MIPS_NE -> NE
+ | MIPS_GE -> GE
+ | MIPS_GEU -> GEU
+ | MIPS_GT -> GT_
+ | MIPS_LE -> LE
+ | MIPS_LT -> LT_
+ | MIPS_LTU -> LTU
diff --git a/mips/hgen/shallow_ast_to_herdtools_ast.hgen b/mips/hgen/shallow_ast_to_herdtools_ast.hgen
new file mode 100644
index 00000000..efe2c77e
--- /dev/null
+++ b/mips/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -0,0 +1,98 @@
+| SYSCALL_THREAD_START -> `MIPSThreadStart
+| (ADD (rs, rt, rd)) -> `MIPSRType (MIPSROpADD , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (ADDU (rs, rt, rd)) -> `MIPSRType (MIPSROpADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (AND (rs, rt, rd)) -> `MIPSRType (MIPSROpAND , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DADD (rs, rt, rd)) -> `MIPSRType (MIPSROpDADD , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DADDU (rs, rt, rd)) -> `MIPSRType (MIPSROpDADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DSUB (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUB , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DSUBU (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (MOVN (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVN , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (MOVZ (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVZ , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (MUL (rs, rt, rd)) -> `MIPSRType (MIPSROpMUL , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (NOR (rs, rt, rd)) -> `MIPSRType (MIPSROpNOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (OR (rs, rt, rd)) -> `MIPSRType (MIPSROpOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SLT (rs, rt, rd)) -> `MIPSRType (MIPSROpSLT , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SLTU (rs, rt, rd)) -> `MIPSRType (MIPSROpSLTU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SUB (rs, rt, rd)) -> `MIPSRType (MIPSROpSUB , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SUBU (rs, rt, rd)) -> `MIPSRType (MIPSROpSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (XOR (rs, rt, rd)) -> `MIPSRType (MIPSROpXOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+
+| (ADDI (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (ADDIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (ANDI (rs, rt, imm)) -> `MIPSIType (MIPSIOpANDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+| (DADDI (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (DADDIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDIU,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (ORI (rs, rt, imm)) -> `MIPSIType (MIPSIOpORI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+| (SLTI (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (SLTIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (XORI (rs, rt, imm)) -> `MIPSIType (MIPSIOpXORI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+
+| (DSLL (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSLL32 (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRA (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRA32 (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRL (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRL32 (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (SLL (rt, rd, sa)) -> `MIPSShiftI (MIPSSLL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (SRA (rt, rd, sa)) -> `MIPSShiftI (MIPSSRA , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (SRL (rt, rd, sa)) -> `MIPSShiftI (MIPSSRL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+
+| DSLLV (rs, rt, rd) -> `MIPSShiftV (MIPSDSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| DSRAV (rs, rt, rd) -> `MIPSShiftV (MIPSDSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| DSRLV (rs, rt, rd) -> `MIPSShiftV (MIPSDSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| SLLV (rs, rt, rd) -> `MIPSShiftV (MIPSSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| SRAV (rs, rt, rd) -> `MIPSShiftV (MIPSSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| SRLV (rs, rt, rd) -> `MIPSShiftV (MIPSSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+
+| DDIV (rs, rt) -> `MIPSMulDiv (MIPSDDIV , (translate_out_ireg rs), (translate_out_ireg rt))
+| DDIVU (rs, rt) -> `MIPSMulDiv (MIPSDDIVU , (translate_out_ireg rs), (translate_out_ireg rt))
+| DIV (rs, rt) -> `MIPSMulDiv (MIPSDIV , (translate_out_ireg rs), (translate_out_ireg rt))
+| DIVU (rs, rt) -> `MIPSMulDiv (MIPSDIVU , (translate_out_ireg rs), (translate_out_ireg rt))
+| DMULT (rs, rt) -> `MIPSMulDiv (MIPSDMULT , (translate_out_ireg rs), (translate_out_ireg rt))
+| DMULTU (rs, rt) -> `MIPSMulDiv (MIPSDMULTU , (translate_out_ireg rs), (translate_out_ireg rt))
+| MADD (rs, rt) -> `MIPSMulDiv (MIPSMADD , (translate_out_ireg rs), (translate_out_ireg rt))
+| MADDU (rs, rt) -> `MIPSMulDiv (MIPSMADDU , (translate_out_ireg rs), (translate_out_ireg rt))
+| MSUB (rs, rt) -> `MIPSMulDiv (MIPSMSUB , (translate_out_ireg rs), (translate_out_ireg rt))
+| MSUBU (rs, rt) -> `MIPSMulDiv (MIPSMSUBU , (translate_out_ireg rs), (translate_out_ireg rt))
+| MULT (rs, rt) -> `MIPSMulDiv (MIPSMULT , (translate_out_ireg rs), (translate_out_ireg rt))
+| MULTU (rs, rt) -> `MIPSMulDiv (MIPSMULTU , (translate_out_ireg rs), (translate_out_ireg rt))
+
+| MFHI (rs) -> `MIPSMFHiLo (MIPSMFHI, (translate_out_ireg rs))
+| MFLO (rs) -> `MIPSMFHiLo (MIPSMFLO, (translate_out_ireg rs))
+| MTHI (rs) -> `MIPSMFHiLo (MIPSMTHI, (translate_out_ireg rs))
+| MTLO (rs) -> `MIPSMFHiLo (MIPSMTLO, (translate_out_ireg rs))
+
+| LUI (rt, imm) -> `MIPSLUI ((translate_out_ireg rt), (translate_out_imm16 imm))
+| Load (width, signed, linked, base, rt, offset) ->
+ `MIPSLoad (
+ (translate_out_wordWidth width),
+ (translate_out_bool signed),
+ (translate_out_bool linked),
+ (translate_out_ireg base),
+ (translate_out_ireg rt),
+ (translate_out_simm16 offset)
+ )
+| Store (width, conditional, base, rt, offset) ->
+ `MIPSStore (
+ (translate_out_wordWidth width),
+ (translate_out_bool conditional),
+ (translate_out_ireg base),
+ (translate_out_ireg rt),
+ (translate_out_simm16 offset)
+ )
+| LWL (base, rt, offset) -> `MIPSLSLR (false, false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| LWR (base, rt, offset) -> `MIPSLSLR (false, false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| LDL (base, rt, offset) -> `MIPSLSLR (false, true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| LDR (base, rt, offset) -> `MIPSLSLR (false, true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SWL (base, rt, offset) -> `MIPSLSLR (true , false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SWR (base, rt, offset) -> `MIPSLSLR (true , false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SDL (base, rt, offset) -> `MIPSLSLR (true , true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SDR (base, rt, offset) -> `MIPSLSLR (true , true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SYNC -> `MIPSSYNC
+| BEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_simm16 offset), (translate_out_bool ne), (translate_out_bool likely))
+| BCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_simm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely))
+| J (offset) -> `MIPSJ (translate_out_imm26 offset)
+| JAL (offset) -> `MIPSJAL (translate_out_imm26 offset)
+| JR (rd) -> `MIPSJR (translate_out_ireg rd)
+| JALR (rd, rs) -> `MIPSJALR (translate_out_ireg rd, translate_out_ireg rs)
+
diff --git a/mips/hgen/shallow_types_to_herdtools_types.hgen b/mips/hgen/shallow_types_to_herdtools_types.hgen
new file mode 100644
index 00000000..88743ac0
--- /dev/null
+++ b/mips/hgen/shallow_types_to_herdtools_types.hgen
@@ -0,0 +1,39 @@
+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_imm26 imm = translate_out_int imm
+
+let translate_out_imm16 imm = translate_out_int imm
+let translate_out_simm16 imm = translate_out_signed_int imm 16
+
+let translate_out_imm5 imm = translate_out_int imm
+
+let translate_out_bool = function
+ | Sail_values.I -> true
+ | Sail_values.O -> false
+ | _ -> failwith "translate_out_bool Undef"
+
+
+let translate_out_wordWidth = function
+ | Mips_embed_types.B0 -> MIPSByte
+ | Mips_embed_types.H -> MIPSHalf
+ | Mips_embed_types.W -> MIPSWord
+ | Mips_embed_types.D -> MIPSDouble
+
+let translate_out_cmp = function
+ | Mips_embed_types.EQ_ -> MIPS_EQ (* equal *)
+ | Mips_embed_types.NE -> MIPS_NE (* not equal *)
+ | Mips_embed_types.GE -> MIPS_GE (* signed greater than or equal *)
+ | Mips_embed_types.GEU -> MIPS_GEU (* unsigned greater than or equal *)
+ | Mips_embed_types.GT_ -> MIPS_GT (* signed strictly greater than *)
+ | Mips_embed_types.LE -> MIPS_LE (* signed less than or equal *)
+ | Mips_embed_types.LT_ -> MIPS_LT (* signed strictly less than *)
+ | Mips_embed_types.LTU -> MIPS_LTU (* unsigned less than or qual *)