diff options
| -rw-r--r-- | mips/hgen/sail_trans_out.hgen | 36 | ||||
| -rw-r--r-- | mips/hgen/types_sail_trans_out.hgen | 6 |
2 files changed, 24 insertions, 18 deletions
diff --git a/mips/hgen/sail_trans_out.hgen b/mips/hgen/sail_trans_out.hgen index 6c956675..f2d006e8 100644 --- a/mips/hgen/sail_trans_out.hgen +++ b/mips/hgen/sail_trans_out.hgen @@ -17,14 +17,14 @@ | ("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)) +| ("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_imm16 imm)) -| ("DADDIU", [rs; rt; imm]) -> `MIPSIType (MIPSIOpDADDIU,(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_imm16 imm)) -| ("SLTIU" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpSLTIU ,(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)) @@ -70,7 +70,7 @@ (translate_out_bool linked), (translate_out_ireg base), (translate_out_ireg rt), - (translate_out_imm16 offset) + (translate_out_simm16 offset) ) | "Store", [width; conditional; base; rt; offset] -> `MIPSStore ( @@ -78,19 +78,19 @@ (translate_out_bool conditional), (translate_out_ireg base), (translate_out_ireg rt), - (translate_out_imm16 offset) + (translate_out_simm16 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)) +| "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_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)) +| "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) diff --git a/mips/hgen/types_sail_trans_out.hgen b/mips/hgen/types_sail_trans_out.hgen index 392c33f3..ebd31fcb 100644 --- a/mips/hgen/types_sail_trans_out.hgen +++ b/mips/hgen/types_sail_trans_out.hgen @@ -3,12 +3,18 @@ let translate_out_big_bit = function | _ -> 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 |