attempt to preserve signs of immediate where appropriate when translating to sail->ppcmem (no need to worry about reverse direction).

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