diff options
| -rw-r--r-- | mips/hgen/ast.hgen | 13 | ||||
| -rw-r--r-- | mips/hgen/fold.hgen | 13 | ||||
| -rw-r--r-- | mips/hgen/lexer.hgen | 112 | ||||
| -rw-r--r-- | mips/hgen/map.hgen | 14 | ||||
| -rw-r--r-- | mips/hgen/parser.hgen | 26 | ||||
| -rw-r--r-- | mips/hgen/pretty.hgen | 27 | ||||
| -rw-r--r-- | mips/hgen/regs_out_in.hgen | 5 | ||||
| -rw-r--r-- | mips/hgen/sail_trans_out.hgen | 93 | ||||
| -rw-r--r-- | mips/hgen/token_types.hgen | 42 | ||||
| -rw-r--r-- | mips/hgen/tokens.hgen | 13 | ||||
| -rw-r--r-- | mips/hgen/trans_sail.hgen | 112 | ||||
| -rw-r--r-- | mips/hgen/types.hgen | 208 | ||||
| -rw-r--r-- | mips/hgen/types_sail_trans_out.hgen | 39 | ||||
| -rw-r--r-- | mips/hgen/types_trans_sail.hgen | 30 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 94 | ||||
| -rw-r--r-- | mips/mips_tlb.sail | 94 | ||||
| -rw-r--r-- | mips/mips_tlb_stub.sail | 4 | ||||
| -rw-r--r-- | src/Makefile | 13 |
18 files changed, 856 insertions, 96 deletions
diff --git a/mips/hgen/ast.hgen b/mips/hgen/ast.hgen new file mode 100644 index 00000000..c9a39bbf --- /dev/null +++ b/mips/hgen/ast.hgen @@ -0,0 +1,13 @@ +| `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 *) diff --git a/mips/hgen/fold.hgen b/mips/hgen/fold.hgen new file mode 100644 index 00000000..08b6cc16 --- /dev/null +++ b/mips/hgen/fold.hgen @@ -0,0 +1,13 @@ +| `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) diff --git a/mips/hgen/lexer.hgen b/mips/hgen/lexer.hgen new file mode 100644 index 00000000..17e72450 --- /dev/null +++ b/mips/hgen/lexer.hgen @@ -0,0 +1,112 @@ +"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 }; diff --git a/mips/hgen/map.hgen b/mips/hgen/map.hgen new file mode 100644 index 00000000..68c9e46a --- /dev/null +++ b/mips/hgen/map.hgen @@ -0,0 +1,14 @@ +| `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) + diff --git a/mips/hgen/parser.hgen b/mips/hgen/parser.hgen new file mode 100644 index 00000000..bf15ab1e --- /dev/null +++ b/mips/hgen/parser.hgen @@ -0,0 +1,26 @@ +| RTYPE ARCH_REG COMMA ARCH_REG COMMA ARCH_REG + { `MIPSRType ($1.op, $2, $4, $6) } +| ITYPE ARCH_REG COMMA ARCH_REG COMMA NUM + { `MIPSIType ($1.op, $2, $4, $6) } +| SHIFTI ARCH_REG COMMA ARCH_REG COMMA NUM + { `MIPSShiftI ($1.op, $2, $4, $6) } +| SHIFTV ARCH_REG COMMA ARCH_REG COMMA ARCH_REG + { `MIPSShiftV ($1.op, $2, $4, $6) } +| MULDIV ARCH_REG COMMA ARCH_REG + { `MIPSMulDiv ($1.op, $2, $4) } +| MFHILO ARCH_REG + { `MIPSMFHiLo ($1.op, $2) } +| LUI ARCH_REG COMMA NUM + { `MIPSLUI ($2, $4) } +| LOAD ARCH_REG COMMA NUM LPAR ARCH_REG RPAR + { `MIPSLoad ($1.width, $1.signed, $1.linked, $6, $2, $4) } +| STORE ARCH_REG COMMA NUM LPAR ARCH_REG RPAR + { `MIPSStore ($1.width, $1.conditional, $6, $2, $4) } +| LSLR ARCH_REG COMMA NUM LPAR ARCH_REG RPAR + { `MIPSLSLR ($1.store, $1.double, $1.left, $6, $2, $4) } +| SYNC + { `MIPSSYNC } +| BEQ ARCH_REG COMMA ARCH_REG COMMA NUM + { `MIPSBEQ ( $2, $4, $6, $1.ne, $1.likely) } +| BCMPZ ARCH_REG COMMA NUM + { `MIPSBCMPZ ( $2, $4, $1.cmp, $1.link, $1.likely) } diff --git a/mips/hgen/pretty.hgen b/mips/hgen/pretty.hgen new file mode 100644 index 00000000..43c41bb8 --- /dev/null +++ b/mips/hgen/pretty.hgen @@ -0,0 +1,27 @@ +| `MIPSThreadStart -> "START" (* TODO *) +| `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 diff --git a/mips/hgen/regs_out_in.hgen b/mips/hgen/regs_out_in.hgen new file mode 100644 index 00000000..8e1fd093 --- /dev/null +++ b/mips/hgen/regs_out_in.hgen @@ -0,0 +1,5 @@ +(* for each instruction instance, identify the role of the registers + and possible branching: (outputs, inputs, voidstars, branch) *) + +| `MIPSAdd -> + ([], [], [], [Next]) diff --git a/mips/hgen/sail_trans_out.hgen b/mips/hgen/sail_trans_out.hgen new file mode 100644 index 00000000..5ecad705 --- /dev/null +++ b/mips/hgen/sail_trans_out.hgen @@ -0,0 +1,93 @@ +| ("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_imm16 imm)) +| ("ADDIU" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpADDIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 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_imm16 imm)) +| ("DADDIU", [rs; rt; imm]) -> `MIPSIType (MIPSIOpDADDIU,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 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_imm16 imm)) +| ("SLTIU" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpSLTIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 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_imm16 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_imm16 offset) + ) +| "LWL", [base; rt; offset] -> `MIPSLSLR (false, false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset)) +| "LWR", [base; rt; offset] -> `MIPSLSLR (false, false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset)) +| "LDL", [base; rt; offset] -> `MIPSLSLR (false, true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset)) +| "LDR", [base; rt; offset] -> `MIPSLSLR (false, true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset)) +| "SWL", [base; rt; offset] -> `MIPSLSLR (true , false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset)) +| "SWR", [base; rt; offset] -> `MIPSLSLR (true , false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset)) +| "SDL", [base; rt; offset] -> `MIPSLSLR (true , true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset)) +| "SDR", [base; rt; offset] -> `MIPSLSLR (true , true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset)) +| "SYNC", [] -> `MIPSSYNC +| "BEQ", [rs; rt; offset; ne; likely] -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_imm16 offset), (translate_out_bool ne), (translate_out_bool likely)) +| "BCMPZ", [rs; offset; cmp; link; likely] -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_imm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely)) + diff --git a/mips/hgen/token_types.hgen b/mips/hgen/token_types.hgen new file mode 100644 index 00000000..2c2df1a6 --- /dev/null +++ b/mips/hgen/token_types.hgen @@ -0,0 +1,42 @@ +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 } + +(* +(bit[26]) J +(bit[26]) JAL +(regno, imm16, Comparison) TRAPIMM +(regno, imm16, Comparison, bool, bool) BCMPZ + +(regno, regno) JALR + +(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 +regno JR + +regregimm16 CACHE +regregimm16 PREF + +unit BREAK +unit ERET +unit HCF +unit SYSCALL +unit WAIT +*)
\ No newline at end of file diff --git a/mips/hgen/tokens.hgen b/mips/hgen/tokens.hgen new file mode 100644 index 00000000..00b99e8e --- /dev/null +++ b/mips/hgen/tokens.hgen @@ -0,0 +1,13 @@ +%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 diff --git a/mips/hgen/trans_sail.hgen b/mips/hgen/trans_sail.hgen new file mode 100644 index 00000000..5dcecfd2 --- /dev/null +++ b/mips/hgen/trans_sail.hgen @@ -0,0 +1,112 @@ +| `MIPSStopFetching -> + ("ImplementationDefinedStopFetching", + [], + []) + +(* Note different argument order, which reflects difference + between instruction encoding and asm format *) +| `MIPSRType (op, rd, rs, rt) -> + (pp_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) -> + (pp_itype_op op, + [ + translate_reg "rs" rs; + translate_reg "rt" rt; + translate_imm16 "imm" imm; + ], + []) + +| `MIPSShiftI (op, rd, rt, sa) -> + (pp_shifti_op op, + [ + translate_reg "rt" rt; + translate_reg "rd" rd; + translate_imm5 "sa" sa; + ], + []) + +| `MIPSShiftV (op, rd, rt, rs) -> + (pp_shiftv_op op, + [ + translate_reg "rs" rs; + translate_reg "rt" rt; + translate_reg "rd" rd; + ], + []) + +| `MIPSMulDiv (op, rs, rt) -> + (pp_muldiv_op op, + [ + translate_reg "rs" rs; + translate_reg "rt" rt; + ], + []) + +| `MIPSMFHiLo (op, rs) -> + (pp_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) -> + (pp_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; + ], []) diff --git a/mips/hgen/types.hgen b/mips/hgen/types.hgen new file mode 100644 index 00000000..ba576e06 --- /dev/null +++ b/mips/hgen/types.hgen @@ -0,0 +1,208 @@ +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 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/hgen/types_sail_trans_out.hgen b/mips/hgen/types_sail_trans_out.hgen new file mode 100644 index 00000000..c48c4b6f --- /dev/null +++ b/mips/hgen/types_sail_trans_out.hgen @@ -0,0 +1,39 @@ +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_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) + +let translate_out_imm16 imm = translate_out_int imm + +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/hgen/types_trans_sail.hgen b/mips/hgen/types_trans_sail.hgen new file mode 100644 index 00000000..111cc3fd --- /dev/null +++ b/mips/hgen/types_trans_sail.hgen @@ -0,0 +1,30 @@ +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_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 diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index b282764d..80350af1 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -499,100 +499,6 @@ function unit incrementCP0Count() = { SignalException(Int); } -function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) = - let entryValid = entry.valid in - let entryR = entry.r in - let entryMask = entry.pagemask in - let entryVPN = entry.vpn2 in - let entryASID = entry.asid in - let entryG = entry.g in - (entryValid & - (r == entryR) & - ((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) & - ((asid == (entryASID)) | (entryG))) - -function option<TLBIndexT> tlbSearch((bit[64]) VAddr) = - let r = (VAddr[63..62]) in - let vpn2 = (VAddr[39..13]) in - let asid = TLBEntryHi.ASID in { - foreach (idx from 0 to 63) { - if(tlbEntryMatch(r, vpn2, asid, (TLBEntries[idx]))) then - return (Some ((TLBIndexT) idx)) - }; - None - } - -function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = { - let idx = tlbSearch(vAddr) in - switch(idx) { - case (Some(idx)) -> - let entry = (TLBEntries[idx]) in - let entryMask = entry.pagemask in - - let evenOddBit = switch(entryMask) { - case 0x0000 -> 12 - case 0x0003 -> 14 - case 0x000f -> 16 - case 0x003f -> 18 - case 0x00ff -> 20 - case 0x03ff -> 22 - case 0x0fff -> 24 - case 0x3fff -> 26 - case 0xffff -> 28 - case _ -> undefined - } in - let isOdd = (vAddr[evenOddBit]) in - let (caps, capl, (bit[24])pfn, d, v) = if (isOdd) then - (entry.caps1, entry.capl1, entry.pfn1, entry.d1, entry.v1) - else - (entry.caps0, entry.capl0, entry.pfn0, entry.d0, entry.v0) in - if (~(v)) then - (SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr)) - else if ((accessType == StoreData) & ~(d)) then - (SignalExceptionTLB(TLBMod, vAddr)) - else - (EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]), - if (accessType == StoreData) then caps else capl) - case None -> (SignalExceptionTLB( - if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr)) - } -} - -function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) = - { - let currentAccessLevel = getAccessLevel() in - let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in - let (requiredLevel, addr) = switch(vAddr[63..62]) { - case 0b11 -> switch(compat32, vAddr[30..29]) { (* xkseg *) - case (true, 0b11) -> (Kernel, None) (* kseg3 mapped 32-bit compat *) - case (true, 0b10) -> (Supervisor, None) (* sseg mapped 32-bit compat *) - case (true, 0b01) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *) - case (true, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *) - case (_, _) -> (Kernel, None) (* xkseg mapped *) - } - case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0]))) (* xkphys bits 61-59 are cache mode (ignored) *) - case 0b01 -> (Supervisor, None) (* xsseg - supervisor mapped *) - case 0b00 -> (User, None) (* xuseg - user mapped *) - } in - if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then - (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)) - else - let (pa, c) = switch(addr) { - case (Some(a)) -> (a, false) - case None -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then - (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)) - else - TLBTranslate2(vAddr, accessType) - } - in if (unsigned(pa) > MAX_PA) then - (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)) - else - (pa, c) - } - -function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = - let (addr, c) = TLBTranslateC(vAddr, accessType) in addr - typedef regno = bit[5] (* a register number *) typedef imm16 = bit[16] (* 16-bit immediate *) (* a commonly used instruction format with three register operands *) diff --git a/mips/mips_tlb.sail b/mips/mips_tlb.sail new file mode 100644 index 00000000..e2549dd6 --- /dev/null +++ b/mips/mips_tlb.sail @@ -0,0 +1,94 @@ + +function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) = + let entryValid = entry.valid in + let entryR = entry.r in + let entryMask = entry.pagemask in + let entryVPN = entry.vpn2 in + let entryASID = entry.asid in + let entryG = entry.g in + (entryValid & + (r == entryR) & + ((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) & + ((asid == (entryASID)) | (entryG))) + +function option<TLBIndexT> tlbSearch((bit[64]) VAddr) = + let r = (VAddr[63..62]) in + let vpn2 = (VAddr[39..13]) in + let asid = TLBEntryHi.ASID in { + foreach (idx from 0 to 63) { + if(tlbEntryMatch(r, vpn2, asid, (TLBEntries[idx]))) then + return (Some ((TLBIndexT) idx)) + }; + None + } + +function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = { + let idx = tlbSearch(vAddr) in + switch(idx) { + case (Some(idx)) -> + let entry = (TLBEntries[idx]) in + let entryMask = entry.pagemask in + + let evenOddBit = switch(entryMask) { + case 0x0000 -> 12 + case 0x0003 -> 14 + case 0x000f -> 16 + case 0x003f -> 18 + case 0x00ff -> 20 + case 0x03ff -> 22 + case 0x0fff -> 24 + case 0x3fff -> 26 + case 0xffff -> 28 + case _ -> undefined + } in + let isOdd = (vAddr[evenOddBit]) in + let (caps, capl, (bit[24])pfn, d, v) = if (isOdd) then + (entry.caps1, entry.capl1, entry.pfn1, entry.d1, entry.v1) + else + (entry.caps0, entry.capl0, entry.pfn0, entry.d0, entry.v0) in + if (~(v)) then + (SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr)) + else if ((accessType == StoreData) & ~(d)) then + (SignalExceptionTLB(TLBMod, vAddr)) + else + (EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]), + if (accessType == StoreData) then caps else capl) + case None -> (SignalExceptionTLB( + if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr)) + } +} + +function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) = + { + let currentAccessLevel = getAccessLevel() in + let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in + let (requiredLevel, addr) = switch(vAddr[63..62]) { + case 0b11 -> switch(compat32, vAddr[30..29]) { (* xkseg *) + case (true, 0b11) -> (Kernel, None) (* kseg3 mapped 32-bit compat *) + case (true, 0b10) -> (Supervisor, None) (* sseg mapped 32-bit compat *) + case (true, 0b01) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *) + case (true, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *) + case (_, _) -> (Kernel, None) (* xkseg mapped *) + } + case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0]))) (* xkphys bits 61-59 are cache mode (ignored) *) + case 0b01 -> (Supervisor, None) (* xsseg - supervisor mapped *) + case 0b00 -> (User, None) (* xuseg - user mapped *) + } in + if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then + (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)) + else + let (pa, c) = switch(addr) { + case (Some(a)) -> (a, false) + case None -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then + (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)) + else + TLBTranslate2(vAddr, accessType) + } + in if (unsigned(pa) > MAX_PA) then + (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)) + else + (pa, c) + } + +function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = + let (addr, c) = TLBTranslateC(vAddr, accessType) in addr diff --git a/mips/mips_tlb_stub.sail b/mips/mips_tlb_stub.sail new file mode 100644 index 00000000..b2ddfca8 --- /dev/null +++ b/mips/mips_tlb_stub.sail @@ -0,0 +1,4 @@ +function option<TLBIndexT> tlbSearch((bit[64]) VAddr) = None + +function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = + vAddr diff --git a/src/Makefile b/src/Makefile index 937c76c9..7849e666 100644 --- a/src/Makefile +++ b/src/Makefile @@ -25,9 +25,10 @@ LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib ELFDIR= $(BITBUCKET_ROOT)/linksem MIPS_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/mips -MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail +MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail +MIPS_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri -CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail elf: make -C $(ELFDIR) @@ -48,6 +49,11 @@ _build/mips.lem: $(MIPS_SAILS) ./sail.native cd _build ;\ ../sail.native -lem_ast -o mips $(MIPS_SAILS) +_build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native + mkdir -p _build + cd _build ; \ + ../sail.native -lem_ast -o mips_notlb $(MIPS_NOTLB_SAILS) + _build/cheri.lem: $(CHERI_SAILS) ./sail.native mkdir -p _build cd _build ;\ @@ -74,6 +80,9 @@ run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml int run_cheri.native: _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml -o run_cheri.native +mips_notlb: _build/mips_notlb.ml _build/mips_extras.ml + true + mips: elf run_mips.native cheri: elf run_cheri.native |