diff options
Diffstat (limited to 'mips/hgen')
| -rw-r--r-- | mips/hgen/herdtools_ast_to_shallow_ast.hgen | 121 | ||||
| -rw-r--r-- | mips/hgen/herdtools_types_to_shallow_types.hgen | 120 | ||||
| -rw-r--r-- | mips/hgen/shallow_ast_to_herdtools_ast.hgen | 98 | ||||
| -rw-r--r-- | mips/hgen/shallow_types_to_herdtools_types.hgen | 39 |
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 *) |
