diff options
Diffstat (limited to 'mips/gen')
| -rw-r--r-- | mips/gen/ast.hgen | 18 | ||||
| -rw-r--r-- | mips/gen/fold.hgen | 19 | ||||
| -rw-r--r-- | mips/gen/herdtools_ast_to_shallow_ast.hgen | 121 | ||||
| -rw-r--r-- | mips/gen/herdtools_types_to_shallow_types.hgen | 120 | ||||
| -rw-r--r-- | mips/gen/lexer.hgen | 116 | ||||
| -rw-r--r-- | mips/gen/map.hgen | 19 | ||||
| -rw-r--r-- | mips/gen/parser.hgen | 34 | ||||
| -rw-r--r-- | mips/gen/pretty.hgen | 36 | ||||
| -rw-r--r-- | mips/gen/sail_trans_out.hgen | 98 | ||||
| -rw-r--r-- | mips/gen/shallow_ast_to_herdtools_ast.hgen | 98 | ||||
| -rw-r--r-- | mips/gen/shallow_types_to_herdtools_types.hgen | 39 | ||||
| -rw-r--r-- | mips/gen/token_types.hgen | 39 | ||||
| -rw-r--r-- | mips/gen/tokens.hgen | 17 | ||||
| -rw-r--r-- | mips/gen/trans_sail.hgen | 122 | ||||
| -rw-r--r-- | mips/gen/types.hgen | 209 | ||||
| -rw-r--r-- | mips/gen/types_sail_trans_out.hgen | 47 | ||||
| -rw-r--r-- | mips/gen/types_trans_sail.hgen | 44 |
17 files changed, 0 insertions, 1196 deletions
diff --git a/mips/gen/ast.hgen b/mips/gen/ast.hgen deleted file mode 100644 index a251adff..00000000 --- a/mips/gen/ast.hgen +++ /dev/null @@ -1,18 +0,0 @@ -| `MIPSThreadStart -| `MIPSRType of mipsRTypeOp * reg * reg * reg -| `MIPSIType of mipsITypeOp * reg * reg * bit16 -| `MIPSShiftI of mipsShiftIOp * reg * reg * bit5 -| `MIPSShiftV of mipsShiftVOp * reg * reg * reg -| `MIPSMulDiv of mipsMulDivOp * reg * reg -| `MIPSMFHiLo of mipsMFHiLoOp * reg -| `MIPSLUI of reg * bit16 -| `MIPSLoad of mipsWordWidth * bool * bool * reg * reg * bit16 (* width, signed, linked, base, rt, offset *) -| `MIPSStore of mipsWordWidth * bool * reg * reg * bit16 (* width, conditional, base, rt, offset *) -| `MIPSLSLR of bool * bool * bool * reg * reg * bit16 (* store, double, left, base, rt, offset *) -| `MIPSSYNC -| `MIPSBEQ of reg * reg * bit16 * bool * bool (* rs, rt, offset, not equal, likely *) -| `MIPSBCMPZ of reg * bit16 * mipsCmp * bool * bool (* rs, offset, cmp, link, likely *) -| `MIPSJ of bit26 -| `MIPSJAL of bit26 -| `MIPSJR of reg -| `MIPSJALR of reg * reg (* rs, rd *) diff --git a/mips/gen/fold.hgen b/mips/gen/fold.hgen deleted file mode 100644 index 05b9c808..00000000 --- a/mips/gen/fold.hgen +++ /dev/null @@ -1,19 +0,0 @@ -| `MIPSThreadStart -> (y_reg, y_sreg) -| `MIPSRType (op, rd, rs, rt) -> fold_reg rt (fold_reg rs (fold_reg rd (y_reg, y_sreg))) -| `MIPSIType (op, rs, rt, imm) -> fold_reg rs (fold_reg rt (y_reg, y_sreg)) -| `MIPSShiftI (op, rd, rt, imm) -> fold_reg rt (fold_reg rd (y_reg, y_sreg)) -| `MIPSShiftV (op, rd, rt, rs) -> fold_reg rs (fold_reg rt (fold_reg rd (y_reg, y_sreg))) -| `MIPSMulDiv (op, rs, rt) -> fold_reg rs (fold_reg rt (y_reg, y_sreg)) -| `MIPSMFHiLo (op, rs) -> fold_reg rs (y_reg, y_sreg) -| `MIPSLUI (rt, imm) -> fold_reg rt (y_reg, y_sreg) -| `MIPSLoad (width, signed, linked, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg)) -| `MIPSStore (width, conditional, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg)) -| `MIPSLSLR (store, double, left, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg)) -| `MIPSSYNC -> (y_reg, y_sreg) -| `MIPSBEQ (rs, rt, offset, ne, likely) -> fold_reg rs (fold_reg rt (y_reg, y_sreg)) -| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> fold_reg rs (y_reg, y_sreg) -| `MIPSJ (offset) -> (y_reg, y_sreg) -| `MIPSJAL (offset) -> fold_reg (IReg(R31)) (y_reg, y_sreg) -| `MIPSJR (rd) -> fold_reg rd (y_reg, y_sreg) -| `MIPSJALR (rd, rs) -> fold_reg rd (fold_reg rs (y_reg, y_sreg)) - diff --git a/mips/gen/herdtools_ast_to_shallow_ast.hgen b/mips/gen/herdtools_ast_to_shallow_ast.hgen deleted file mode 100644 index 7b1a58d9..00000000 --- a/mips/gen/herdtools_ast_to_shallow_ast.hgen +++ /dev/null @@ -1,121 +0,0 @@ -| `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/gen/herdtools_types_to_shallow_types.hgen b/mips/gen/herdtools_types_to_shallow_types.hgen deleted file mode 100644 index 5a0e3bfc..00000000 --- a/mips/gen/herdtools_types_to_shallow_types.hgen +++ /dev/null @@ -1,120 +0,0 @@ -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.B1 - | false -> Sail_values.B0 - -let translate_wordsize _ = function - | MIPSByte -> Mips_embed_types.B2 - | 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/gen/lexer.hgen b/mips/gen/lexer.hgen deleted file mode 100644 index c01b14cc..00000000 --- a/mips/gen/lexer.hgen +++ /dev/null @@ -1,116 +0,0 @@ -"add" , RTYPE {txt="ADD" ; op=MIPSROpADD }; -"addu" , RTYPE {txt="ADDU" ; op=MIPSROpADDU }; -"and" , RTYPE {txt="AND" ; op=MIPSROpAND }; -"dadd" , RTYPE {txt="DADD" ; op=MIPSROpDADD }; -"daddu" , RTYPE {txt="DADDU" ; op=MIPSROpDADDU }; -"dsub" , RTYPE {txt="DSUB" ; op=MIPSROpDSUB }; -"dsubu" , RTYPE {txt="DSUBU" ; op=MIPSROpDSUBU }; -"movn" , RTYPE {txt="MOVN" ; op=MIPSROpMOVN }; -"movz" , RTYPE {txt="MOVZ" ; op=MIPSROpMOVZ }; -"mul" , RTYPE {txt="MUL" ; op=MIPSROpMUL }; -"nor" , RTYPE {txt="NOR" ; op=MIPSROpNOR }; -"or" , RTYPE {txt="OR" ; op=MIPSROpOR }; -"slt" , RTYPE {txt="SLT" ; op=MIPSROpSLT }; -"sltu" , RTYPE {txt="SLTU" ; op=MIPSROpSLTU }; -"sub" , RTYPE {txt="SUB" ; op=MIPSROpSUB }; -"subu" , RTYPE {txt="SUBU" ; op=MIPSROpSUBU }; -"xor" , RTYPE {txt="XOR" ; op=MIPSROpXOR }; - -"addi" , ITYPE {txt="ADDI" ; op=MIPSIOpADDI }; -"addiu" , ITYPE {txt="ADDIU" ; op=MIPSIOpADDIU }; -"andi" , ITYPE {txt="ANDI" ; op=MIPSIOpANDI }; -"daddi" , ITYPE {txt="DADDI" ; op=MIPSIOpDADDI }; -"daddiu", ITYPE {txt="DADDIU"; op=MIPSIOpDADDIU }; -"ori" , ITYPE {txt="ORI" ; op=MIPSIOpORI }; -"slti" , ITYPE {txt="SLTI" ; op=MIPSIOpSLTI }; -"sltiu" , ITYPE {txt="SLTIU" ; op=MIPSIOpSLTIU }; -"xori" , ITYPE {txt="XORI" ; op=MIPSIOpXORI }; - -"dsll" , SHIFTI {txt="DSLL" ; op=MIPSDSLL }; -"dsll32" , SHIFTI {txt="DSLL32" ; op=MIPSDSLL32 }; -"dsra" , SHIFTI {txt="DSRA" ; op=MIPSDSRA }; -"dsra32" , SHIFTI {txt="DSRA32" ; op=MIPSDSRA32 }; -"dsrl" , SHIFTI {txt="DSRL" ; op=MIPSDSRL }; -"dsrl32" , SHIFTI {txt="DSRL32" ; op=MIPSDSRL32 }; -"sll" , SHIFTI {txt="SLL" ; op=MIPSSLL }; -"sra" , SHIFTI {txt="SRA" ; op=MIPSSRA }; -"srl" , SHIFTI {txt="SRL" ; op=MIPSSRL }; - -"dsllv", SHIFTV {txt="DSLLV" ; op=MIPSDSLLV }; -"dsrav", SHIFTV {txt="DSRAV" ; op=MIPSDSRAV }; -"dsrlv", SHIFTV {txt="DSRLV" ; op=MIPSDSRLV }; -"sllv" , SHIFTV {txt="SLLV" ; op=MIPSSLLV }; -"srav" , SHIFTV {txt="SRAV" ; op=MIPSSRAV }; -"srlv" , SHIFTV {txt="SRLV" ; op=MIPSSRLV }; - -"ddiv" , MULDIV {txt="DDIV" ; op=MIPSDDIV }; -"ddivu" , MULDIV {txt="DDIVU" ; op=MIPSDDIVU }; -"div" , MULDIV {txt="DIV" ; op=MIPSDIV }; -"divu" , MULDIV {txt="DIVU" ; op=MIPSDIVU }; -"dmult" , MULDIV {txt="DMULT" ; op=MIPSDMULT }; -"dmultu", MULDIV {txt="DMULTU"; op=MIPSDMULTU }; -"madd" , MULDIV {txt="MADD" ; op=MIPSMADD }; -"maddu" , MULDIV {txt="MADDU" ; op=MIPSMADDU }; -"msub" , MULDIV {txt="MSUB" ; op=MIPSMSUB }; -"msubu" , MULDIV {txt="MSUBU" ; op=MIPSMSUBU }; -"mult" , MULDIV {txt="MULT" ; op=MIPSMULT }; -"multu" , MULDIV {txt="MULTU" ; op=MIPSMULTU }; - -"mfhi" , MFHILO {txt="MFHI" ; op=MIPSMFHI }; -"mflo" , MFHILO {txt="MFLO" ; op=MIPSMFLO }; -"mthi" , MFHILO {txt="MTHI" ; op=MIPSMTHI }; -"mtlo" , MFHILO {txt="MTLO" ; op=MIPSMTLO }; - -"lui" , LUI {txt="LUI" }; - -"lb" , LOAD {txt="LB" ; width=MIPSByte ; signed=true; linked=false }; -"lbu" , LOAD {txt="LBU" ; width=MIPSByte ; signed=false; linked=false }; -"lh" , LOAD {txt="LH" ; width=MIPSHalf ; signed=true; linked=false }; -"lhu" , LOAD {txt="LHU" ; width=MIPSHalf ; signed=false; linked=false }; -"lw" , LOAD {txt="LW" ; width=MIPSWord ; signed=true; linked=false }; -"lwu" , LOAD {txt="LWU" ; width=MIPSWord ; signed=false; linked=false }; -"ld" , LOAD {txt="LD" ; width=MIPSDouble ; signed=false; linked=false }; -"ll" , LOAD {txt="LL" ; width=MIPSWord ; signed=true; linked=true }; -"lld" , LOAD {txt="LLD" ; width=MIPSDouble ; signed=false; linked=true }; - -"sb" , STORE {txt="SB" ; width=MIPSByte ; conditional=false }; -"sh" , STORE {txt="SH" ; width=MIPSHalf ; conditional=false }; -"sw" , STORE {txt="SW" ; width=MIPSWord ; conditional=false }; -"sd" , STORE {txt="SD" ; width=MIPSDouble ; conditional=false }; -"sc" , STORE {txt="SC" ; width=MIPSWord ; conditional=true }; -"scd" , STORE {txt="SCD" ; width=MIPSDouble ; conditional=true }; - -"lwl" , LSLR {txt="LWL" ; store=false; double=false; left=true }; -"lwr" , LSLR {txt="LWR" ; store=false; double=false; left=false}; -"ldl" , LSLR {txt="LDL" ; store=false; double=true ; left=true }; -"ldr" , LSLR {txt="LDR" ; store=false; double=true ; left=false}; -"swl" , LSLR {txt="SWL" ; store=true ; double=false; left=true }; -"swr" , LSLR {txt="SWR" ; store=true ; double=false; left=false}; -"sdl" , LSLR {txt="SDL" ; store=true ; double=true ; left=true }; -"sdr" , LSLR {txt="SDR" ; store=true ; double=true ; left=false}; -"sync", SYNC {txt="SYNC"}; - -"beq", BEQ {txt="BEQ"; ne=false; likely=false }; -"beql", BEQ {txt="BEQ"; ne=false; likely=true }; -"bne", BEQ {txt="BEQ"; ne=true ; likely=false }; -"bnel", BEQ {txt="BEQ"; ne=true ; likely=true }; - -"bltz", BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=false; link=false }; -"bltzal", BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=false; link=true }; -"bltzl", BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=true; link=false }; -"bltzall",BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=true; link=true }; - -"bgez", BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=false; link=false }; -"bgezal", BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=false; link=true }; -"bgezl", BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=true; link=false }; -"bgezall",BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=true; link=true }; - -"bgtz", BCMPZ {txt="BCMPZ"; cmp=MIPS_GT; likely=false; link=false }; -"bgtzl", BCMPZ {txt="BCMPZ"; cmp=MIPS_GT; likely=true; link=false }; - -"blez", BCMPZ {txt="BCMPZ"; cmp=MIPS_LE; likely=false; link=false }; -"blezl", BCMPZ {txt="BCMPZ"; cmp=MIPS_LE; likely=true; link=false }; -"j", J {txt="J"}; -"jal", JAL {txt="JAL"}; -"jr", JR {txt="JR"}; -"jalr", JALR {txt="JALR"}; diff --git a/mips/gen/map.hgen b/mips/gen/map.hgen deleted file mode 100644 index f5116bae..00000000 --- a/mips/gen/map.hgen +++ /dev/null @@ -1,19 +0,0 @@ -| `MIPSThreadStart -> `MIPSThreadStart -| `MIPSRType (op, rd, rs, rt) -> `MIPSRType (op, map_reg rd, map_reg rs, map_reg rt) -| `MIPSIType (op, rs, rt, imm) -> `MIPSIType (op, map_reg rs, map_reg rt, imm) -| `MIPSShiftI (op, rd, rt, imm) -> `MIPSShiftI (op, map_reg rd, map_reg rt, imm) -| `MIPSShiftV (op, rd, rt, rs) -> `MIPSShiftV (op, map_reg rd, map_reg rt, map_reg rs) -| `MIPSMulDiv (op, rs, rt) -> `MIPSMulDiv (op, map_reg rs, map_reg rt) -| `MIPSMFHiLo (op, rs) -> `MIPSMFHiLo (op, map_reg rs) -| `MIPSLUI (rt, imm) -> `MIPSLUI (map_reg rt, imm) -| `MIPSLoad (width, signed, linked, base, rt, offset) -> `MIPSLoad (width, signed, linked, map_reg base, map_reg rt, offset) -| `MIPSStore (width, conditional, base, rt, offset) -> `MIPSStore (width, conditional, map_reg base, map_reg rt, offset) -| `MIPSLSLR (store, double, left, base, rt, offset) -> `MIPSLSLR (store, double, left, map_reg base, map_reg rt, offset) -| `MIPSSYNC -> `MIPSSYNC -| `MIPSBEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ (map_reg rs, map_reg rt, offset, ne, likely) -| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ (map_reg rs, offset, cmp, link, likely) -| `MIPSJ (offset) -> `MIPSJ (offset) -| `MIPSJAL (offset) -> `MIPSJAL (offset) (* implicit R31? *) -| `MIPSJR (rd) -> `MIPSJR (map_reg rd) -| `MIPSJALR (rd, rs) -> `MIPSJALR(map_reg rd, map_reg rs) - diff --git a/mips/gen/parser.hgen b/mips/gen/parser.hgen deleted file mode 100644 index 8f573aa5..00000000 --- a/mips/gen/parser.hgen +++ /dev/null @@ -1,34 +0,0 @@ -| RTYPE reg COMMA reg COMMA reg - { `MIPSRType ($1.op, $2, $4, $6) } -| ITYPE reg COMMA reg COMMA NUM - { `MIPSIType ($1.op, $2, $4, $6) } -| SHIFTI reg COMMA reg COMMA NUM - { `MIPSShiftI ($1.op, $2, $4, $6) } -| SHIFTV reg COMMA reg COMMA reg - { `MIPSShiftV ($1.op, $2, $4, $6) } -| MULDIV reg COMMA reg - { `MIPSMulDiv ($1.op, $2, $4) } -| MFHILO reg - { `MIPSMFHiLo ($1.op, $2) } -| LUI reg COMMA NUM - { `MIPSLUI ($2, $4) } -| LOAD reg COMMA NUM LPAR reg RPAR - { `MIPSLoad ($1.width, $1.signed, $1.linked, $6, $2, $4) } -| STORE reg COMMA NUM LPAR reg RPAR - { `MIPSStore ($1.width, $1.conditional, $6, $2, $4) } -| LSLR reg COMMA NUM LPAR reg RPAR - { `MIPSLSLR ($1.store, $1.double, $1.left, $6, $2, $4) } -| SYNC - { `MIPSSYNC } -| BEQ reg COMMA reg COMMA NUM - { `MIPSBEQ ( $2, $4, $6, $1.ne, $1.likely) } -| BCMPZ reg COMMA NUM - { `MIPSBCMPZ ( $2, $4, $1.cmp, $1.link, $1.likely) } -| J NUM - { `MIPSJ ($2) } -| JAL NUM - { `MIPSJAL ($2) } -| JR reg - { `MIPSJR ($2) } -| JALR reg COMMA reg - { `MIPSJALR ($2, $4) } diff --git a/mips/gen/pretty.hgen b/mips/gen/pretty.hgen deleted file mode 100644 index 98f56f2e..00000000 --- a/mips/gen/pretty.hgen +++ /dev/null @@ -1,36 +0,0 @@ -| `MIPSThreadStart -> "syscall 0xfffff" (* thread start *) -| `MIPSStopFetching -> "STOP" (* TODO *) -| `MIPSRType (op, rd,rs,rt) -> - sprintf "%s %s,%s,%s" (pp_rtype_op op) (pp_reg rd) (pp_reg rs) (pp_reg rt) -| `MIPSIType (op,rd,rs,imm) -> - sprintf "%s %s,%s,%d" (pp_itype_op op) (pp_reg rd) (pp_reg rs) imm -| `MIPSShiftI (op, rs, rt, imm) -> - sprintf "%s %s,%s,%d" (pp_shifti_op op) (pp_reg rs) (pp_reg rt) imm -| `MIPSShiftV (op, rd,rs,rt) -> - sprintf "%s %s,%s,%s" (pp_shiftv_op op) (pp_reg rd) (pp_reg rs) (pp_reg rt) -| `MIPSMulDiv (op, rs, rt) -> - sprintf "%s %s,%s" (pp_muldiv_op op) (pp_reg rs) (pp_reg rt) -| `MIPSMFHiLo (op, rs) -> - sprintf "%s %s" (pp_mfhilo_op op) (pp_reg rs) -| `MIPSLUI (rt, imm) -> - sprintf "lui %s,%d" (pp_reg rt) imm -| `MIPSLoad (width, signed, linked, base, rt, offset) -> - sprintf "%s %s,%d(%s)" (pp_load_op width signed linked) (pp_reg rt) offset (pp_reg base) -| `MIPSStore (width, conditional, base, rt, offset) -> - sprintf "%s %s,%d(%s)" (pp_store_op width conditional) (pp_reg rt) offset (pp_reg base) -| `MIPSLSLR (store, double, left, base, rt, offset) -> - sprintf "%s %s,%d(%s)" (pp_lslr_op store double left) (pp_reg rt) offset (pp_reg base) -| `MIPSSYNC -> "sync" -| `MIPSBEQ (rs, rt, offset, ne, likely) -> - sprintf "%s %s,%s,.%+d" (pp_beq_op ne likely) (pp_reg rs) (pp_reg rt) offset -| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> - sprintf "%s,%s,.%+d" (pp_bcmpz_op cmp link likely) (pp_reg rs) offset -| `MIPSJ (offset) -> - sprintf "j %d" offset -| `MIPSJAL (offset) -> - sprintf "jal %d" offset -| `MIPSJR(rd) -> - sprintf "jr %s" (pp_reg rd) -| `MIPSJALR(rd, rs) -> - sprintf "jalr %s,%s" (pp_reg rd) (pp_reg rs) - diff --git a/mips/gen/sail_trans_out.hgen b/mips/gen/sail_trans_out.hgen deleted file mode 100644 index f2d006e8..00000000 --- a/mips/gen/sail_trans_out.hgen +++ /dev/null @@ -1,98 +0,0 @@ -| ("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/gen/shallow_ast_to_herdtools_ast.hgen b/mips/gen/shallow_ast_to_herdtools_ast.hgen deleted file mode 100644 index efe2c77e..00000000 --- a/mips/gen/shallow_ast_to_herdtools_ast.hgen +++ /dev/null @@ -1,98 +0,0 @@ -| 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/gen/shallow_types_to_herdtools_types.hgen b/mips/gen/shallow_types_to_herdtools_types.hgen deleted file mode 100644 index a02d83b7..00000000 --- a/mips/gen/shallow_types_to_herdtools_types.hgen +++ /dev/null @@ -1,39 +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_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.B1 -> true - | Sail_values.B0 -> false - | _ -> failwith "translate_out_bool Undef" - - -let translate_out_wordWidth = function - | Mips_embed_types.B2 -> 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 *) diff --git a/mips/gen/token_types.hgen b/mips/gen/token_types.hgen deleted file mode 100644 index 170b42d3..00000000 --- a/mips/gen/token_types.hgen +++ /dev/null @@ -1,39 +0,0 @@ -type token_RTYPE = {txt : string; op : mipsRTypeOp } -type token_ITYPE = {txt : string; op : mipsITypeOp } -type token_ShiftI = {txt : string; op : mipsShiftIOp } -type token_ShiftV = {txt : string; op : mipsShiftVOp } -type token_MulDiv = {txt : string; op : mipsMulDivOp } -type token_MFHiLo = {txt : string; op : mipsMFHiLoOp } -type token_LUI = {txt : string } -type token_Load = {txt : string; width: mipsWordWidth; signed : bool; linked : bool} -type token_Store = {txt : string; width: mipsWordWidth; conditional : bool} -type token_LSLR = {txt : string; store : bool; double : bool; left: bool } (* Load/Store Left/Right *) -type token_SYNC = {txt : string} -type token_BEQ = {txt : string; ne : bool; likely : bool } -type token_BCMPZ = {txt : string; cmp : mipsCmp; likely : bool; link : bool } -type token_J = {txt : string} -type token_JAL = {txt : string} -type token_JR = {txt : string} -type token_JALR = {txt : string} -(* -(regno, imm16, Comparison) TRAPIMM - -(regno, regno) RDHWR -(regno, regno, Comparison) TRAPREG -(regno, regno, bit[3], bool) MFC0 -(regno, regno, bit[3], bool) MTC0 -(regno, regno, imm16, bool, bool) BEQ -TLBP -TLBR -TLBWI -TLBWR - -regregimm16 CACHE -regregimm16 PREF - -unit BREAK -unit ERET -unit HCF -unit SYSCALL -unit WAIT -*)
\ No newline at end of file diff --git a/mips/gen/tokens.hgen b/mips/gen/tokens.hgen deleted file mode 100644 index 937c6354..00000000 --- a/mips/gen/tokens.hgen +++ /dev/null @@ -1,17 +0,0 @@ -%token <MIPSHGenBase.token_RTYPE> RTYPE -%token <MIPSHGenBase.token_ITYPE> ITYPE -%token <MIPSHGenBase.token_ShiftI> SHIFTI -%token <MIPSHGenBase.token_ShiftV> SHIFTV -%token <MIPSHGenBase.token_MulDiv> MULDIV -%token <MIPSHGenBase.token_MFHiLo> MFHILO -%token <MIPSHGenBase.token_LUI> LUI -%token <MIPSHGenBase.token_Load> LOAD -%token <MIPSHGenBase.token_Store> STORE -%token <MIPSHGenBase.token_LSLR> LSLR -%token <MIPSHGenBase.token_SYNC> SYNC -%token <MIPSHGenBase.token_BEQ> BEQ -%token <MIPSHGenBase.token_BCMPZ> BCMPZ -%token <MIPSHGenBase.token_J> J -%token <MIPSHGenBase.token_JAL> JAL -%token <MIPSHGenBase.token_JR> JR -%token <MIPSHGenBase.token_JALR> JALR diff --git a/mips/gen/trans_sail.hgen b/mips/gen/trans_sail.hgen deleted file mode 100644 index e42d1b19..00000000 --- a/mips/gen/trans_sail.hgen +++ /dev/null @@ -1,122 +0,0 @@ -| `MIPSThreadStart -> - ("SYSCALL_THREAD_START", [], []) -| `MIPSStopFetching -> - ("ImplementationDefinedStopFetching", - [], - []) - -(* 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/gen/types.hgen b/mips/gen/types.hgen deleted file mode 100644 index a1c61f4b..00000000 --- a/mips/gen/types.hgen +++ /dev/null @@ -1,209 +0,0 @@ -type mipsRTypeOp = -| MIPSROpADD -| MIPSROpADDU -| MIPSROpAND -| MIPSROpDADD -| MIPSROpDADDU -| MIPSROpDSUB -| MIPSROpDSUBU -| MIPSROpMOVN -| MIPSROpMOVZ -| MIPSROpMUL -| MIPSROpNOR -| MIPSROpOR -| MIPSROpSLT -| MIPSROpSLTU -| MIPSROpSUB -| MIPSROpSUBU -| MIPSROpXOR - -let pp_rtype_op = function -| MIPSROpADD -> "add" -| MIPSROpADDU -> "addu" -| MIPSROpAND -> "and" -| MIPSROpDADD -> "dadd" -| MIPSROpDADDU -> "daddu" -| MIPSROpDSUB -> "dsub" -| MIPSROpDSUBU -> "dsubu" -| MIPSROpMOVN -> "movn" -| MIPSROpMOVZ -> "movz" -| MIPSROpMUL -> "mul" -| MIPSROpNOR -> "nor" -| MIPSROpOR -> "or" -| MIPSROpSLT -> "slt" -| MIPSROpSLTU -> "sltu" -| MIPSROpSUB -> "sub" -| MIPSROpSUBU -> "subu" -| MIPSROpXOR -> "xor" - -type bit26 = int -type bit16 = int -type bit5 = int - -type mipsITypeOp = -| MIPSIOpADDI -| MIPSIOpADDIU -| MIPSIOpANDI -| MIPSIOpDADDI -| MIPSIOpDADDIU -| MIPSIOpORI -| MIPSIOpSLTI -| MIPSIOpSLTIU -| MIPSIOpXORI - -let pp_itype_op = function -| MIPSIOpADDI -> "addi" -| MIPSIOpADDIU -> "addiu" -| MIPSIOpANDI -> "andi" -| MIPSIOpDADDI -> "daddi" -| MIPSIOpDADDIU -> "daddiu" -| MIPSIOpORI -> "ori" -| MIPSIOpSLTI -> "slti" -| MIPSIOpSLTIU -> "sltiu" -| MIPSIOpXORI -> "xori" - -type mipsShiftIOp = -| MIPSDSLL -| MIPSDSLL32 -| MIPSDSRA -| MIPSDSRA32 -| MIPSDSRL -| MIPSDSRL32 -| MIPSSLL -| MIPSSRA -| MIPSSRL - -let pp_shifti_op = function -| MIPSDSLL -> "dsll" -| MIPSDSLL32 -> "dsll32" -| MIPSDSRA -> "dsra" -| MIPSDSRA32 -> "dsra32" -| MIPSDSRL -> "dsrl" -| MIPSDSRL32 -> "dsrl32" -| MIPSSLL -> "sll" -| MIPSSRA -> "sra" -| MIPSSRL -> "srl" - -type mipsShiftVOp = -| MIPSDSLLV -| MIPSDSRAV -| MIPSDSRLV -| MIPSSLLV -| MIPSSRAV -| MIPSSRLV - -let pp_shiftv_op = function -| MIPSDSLLV -> "dsllv" -| MIPSDSRAV -> "dsrav" -| MIPSDSRLV -> "dsrlv" -| MIPSSLLV -> "sllv" -| MIPSSRAV -> "srav" -| MIPSSRLV -> "srlv" - -type mipsMulDivOp = -| MIPSDDIV -| MIPSDDIVU -| MIPSDIV -| MIPSDIVU -| MIPSDMULT -| MIPSDMULTU -| MIPSMADD -| MIPSMADDU -| MIPSMSUB -| MIPSMSUBU -| MIPSMULT -| MIPSMULTU - -let pp_muldiv_op = function -| MIPSDDIV -> "ddiv" -| MIPSDDIVU -> "ddivu" -| MIPSDIV -> "div" -| MIPSDIVU -> "divu" -| MIPSDMULT -> "dmult" -| MIPSDMULTU -> "dmultu" -| MIPSMADD -> "madd" -| MIPSMADDU -> "maddu" -| MIPSMSUB -> "msub" -| MIPSMSUBU -> "msubu" -| MIPSMULT -> "mult" -| MIPSMULTU -> "multu" - -type mipsMFHiLoOp = -| MIPSMFHI -| MIPSMFLO -| MIPSMTHI -| MIPSMTLO - -let pp_mfhilo_op = function -| MIPSMFHI -> "mfhi" -| MIPSMFLO -> "mflo" -| MIPSMTHI -> "mthi" -| MIPSMTLO -> "mtlo" - -type mipsWordWidth = -| MIPSByte -| MIPSHalf -| MIPSWord -| MIPSDouble - -type mipsCmp = -| MIPS_EQ (* equal *) -| MIPS_NE (* not equal *) -| MIPS_GE (* signed greater than or equal *) -| MIPS_GEU (* unsigned greater than or equal *) -| MIPS_GT (* signed strictly greater than *) -| MIPS_LE (* signed less than or equal *) -| MIPS_LT (* signed strictly less than *) -| MIPS_LTU (* unsigned less than or qual *) - -let pp_load_op width signed linked = match (width, signed, linked) with - | (MIPSByte, true, false) -> "lb" - | (MIPSByte, false, false) -> "lbu" - | (MIPSHalf, true, false) -> "lh" - | (MIPSHalf, false, false) -> "lhu" - | (MIPSWord, true, false) -> "lw" - | (MIPSWord, false, false) -> "lwu" - | (MIPSDouble, false, false) -> "ld" - | (MIPSWord, true, true) -> "ll" - | (MIPSDouble, false, true) -> "lld" - | _ -> failwith "unexpected load op" - -let pp_store_op width conditional = match (width, conditional) with - | (MIPSByte, false) -> "sb" - | (MIPSHalf, false) -> "sh" - | (MIPSWord, false) -> "sw" - | (MIPSDouble, false) -> "sd" - | (MIPSWord, true) -> "sc" - | (MIPSDouble, true) -> "scd" - | _ -> failwith "unexpected store op" - -let pp_lslr_op store double left = match (store, double, left) with - | (false, false, true ) -> "lwl" - | (false, false, false) -> "lwr" - | (false, true , true ) -> "ldl" - | (false, true , false) -> "ldr" - | (true , false, true ) -> "swl" - | (true , false, false) -> "swr" - | (true , true , true ) -> "sdl" - | (true , true , false) -> "sdr" - -let pp_beq_op ne likely = match (ne, likely) with - | (false, false) -> "beq" - | (false, true) -> "beql" - | (true , false) -> "bne" - | (true , true) -> "bnel" - -let pp_bcmpz_op cmp link likely = match (cmp, likely, link) with -| (MIPS_LT, false , false ) -> "bltz" -| (MIPS_LT, false , true ) -> "bltzal" -| (MIPS_LT, true , false ) -> "bltzl" -| (MIPS_LT, true , true ) -> "bltzall" -| (MIPS_GE, false , false ) -> "bgez" -| (MIPS_GE, false , true ) -> "bgezal" -| (MIPS_GE, true , false ) -> "bgezl" -| (MIPS_GE, true , true ) -> "bgezall" -| (MIPS_GT, false , false ) -> "bgtz" -| (MIPS_GT, true , false ) -> "bgtzl" -| (MIPS_LE, false , false ) -> "blez" -| (MIPS_LE, true , false ) -> "blezl" -| _ -> failwith "unknown bcmpz instruction" diff --git a/mips/gen/types_sail_trans_out.hgen b/mips/gen/types_sail_trans_out.hgen deleted file mode 100644 index ebd31fcb..00000000 --- a/mips/gen/types_sail_trans_out.hgen +++ /dev/null @@ -1,47 +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_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 - | (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 inst = - match translate_out_enum inst with - | 0 -> MIPSByte - | 1 -> MIPSHalf - | 2 -> MIPSWord - | 3 -> MIPSDouble - | _ -> failwith "Unknown wordWidth in sail translate out" - -let translate_out_cmp inst = - match translate_out_enum inst with - | 0 -> MIPS_EQ (* equal *) - | 1 -> MIPS_NE (* not equal *) - | 2 -> MIPS_GE (* signed greater than or equal *) - | 3 -> MIPS_GEU (* unsigned greater than or equal *) - | 4 -> MIPS_GT (* signed strictly greater than *) - | 5 -> MIPS_LE (* signed less than or equal *) - | 6 -> MIPS_LT (* signed strictly less than *) - | 7 -> MIPS_LTU (* unsigned less than or qual *) - | _ -> failwith "Unknown mipsCmp in sail translate out" diff --git a/mips/gen/types_trans_sail.hgen b/mips/gen/types_trans_sail.hgen deleted file mode 100644 index 63880ae9..00000000 --- a/mips/gen/types_trans_sail.hgen +++ /dev/null @@ -1,44 +0,0 @@ -let translate_rtype_op op = uppercase (pp_rtype_op op) -let translate_itype_op op = uppercase (pp_itype_op op) -let translate_shifti_op op = uppercase (pp_shifti_op op) -let translate_shiftv_op op = uppercase (pp_shiftv_op op) -let translate_muldiv_op op = uppercase (pp_muldiv_op op) -let translate_mfhilo_op op = uppercase (pp_mfhilo_op op) -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 = uppercase (pp_lslr_op store double left) -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 = - (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value))) -let translate_imm26 name value = - (name, Bvector (Some 26), bit_list_of_integer 26 (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_imm5 name value = - (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value)) -let translate_bool name value = - (name, Bit, [if value then Bitc_one else Bitc_zero]) -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_wordsize = translate_enum [MIPSByte; MIPSHalf; MIPSWord; MIPSDouble] -let translate_cmp = translate_enum [ -MIPS_EQ ;(* equal *) -MIPS_NE ;(* not equal *) -MIPS_GE ;(* signed greater than or equal *) -MIPS_GEU ;(* unsigned greater than or equal *) -MIPS_GT ;(* signed strictly greater than *) -MIPS_LE ;(* signed less than or equal *) -MIPS_LT ;(* signed strictly less than *) -MIPS_LTU ;(* unsigned less than or qual *) -]
\ No newline at end of file |