be consistent about using lower case when parsing/pretty printing MIPS assembly.

4 files changed, 108 insertions, 96 deletions

diff --git a/mips/hgen/pretty.hgen b/mips/hgen/pretty.hgen
index e4bc0b6d..98f56f2e 100644
--- a/mips/hgen/pretty.hgen
+++ b/mips/hgen/pretty.hgen
@@ -13,18 +13,18 @@
 | `MIPSMFHiLo (op, rs) ->
       sprintf "%s %s" (pp_mfhilo_op op) (pp_reg rs)
 | `MIPSLUI (rt, imm) ->
-      sprintf "LUI %s,%d" (pp_reg 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"
+| `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
+      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
+      sprintf "%s,%s,.%+d" (pp_bcmpz_op cmp link likely) (pp_reg rs) offset
 | `MIPSJ (offset) ->
   sprintf "j %d" offset
 | `MIPSJAL (offset) ->
@@ -32,5 +32,5 @@
 | `MIPSJR(rd) ->
   sprintf "jr %s" (pp_reg rd)
 | `MIPSJALR(rd, rs) ->
-  sprintf "jalr %s, %s" (pp_reg rd) (pp_reg rs)
+  sprintf "jalr %s,%s" (pp_reg rd) (pp_reg rs)
 
diff --git a/mips/hgen/trans_sail.hgen b/mips/hgen/trans_sail.hgen
index 9a34ff49..e42d1b19 100644
--- a/mips/hgen/trans_sail.hgen
+++ b/mips/hgen/trans_sail.hgen
@@ -8,7 +8,7 @@
 (* Note different argument order, which reflects difference
    between instruction encoding and asm format  *)
 | `MIPSRType (op, rd, rs, rt) ->
-    (pp_rtype_op op,
+    (translate_rtype_op op,
       [
       translate_reg "rs" rs;
       translate_reg "rt" rt;
@@ -18,7 +18,7 @@
 
 (* Note different argument order similar to above *)
 | `MIPSIType (op, rt, rs, imm) ->
-    (pp_itype_op op,
+    (translate_itype_op op,
       [
       translate_reg "rs" rs;
       translate_reg "rt" rt;
@@ -27,7 +27,7 @@
       [])
 
 | `MIPSShiftI (op, rd, rt, sa) ->
-    (pp_shifti_op op,
+    (translate_shifti_op op,
       [
       translate_reg "rt" rt;
       translate_reg "rd" rd;
@@ -36,7 +36,7 @@
       [])
 
 | `MIPSShiftV (op, rd, rt, rs) ->
-    (pp_shiftv_op op,
+    (translate_shiftv_op op,
       [
       translate_reg "rs" rs;
       translate_reg "rt" rt;
@@ -45,7 +45,7 @@
       [])
 
 | `MIPSMulDiv (op, rs, rt) ->
-    (pp_muldiv_op op,
+    (translate_muldiv_op op,
       [
       translate_reg "rs" rs;
       translate_reg "rt" rt;
@@ -53,7 +53,7 @@
       [])
 
 | `MIPSMFHiLo (op, rs) ->
-    (pp_mfhilo_op op,
+    (translate_mfhilo_op op,
       [
       translate_reg "rs" rs;
       ],
@@ -87,7 +87,7 @@
       ],
       [])
 | `MIPSLSLR (store, double, left, base, rt, offset) ->
-  (pp_lslr_op store double left,
+  (translate_lslr_op store double left,
       [
       translate_reg "base" base;
       translate_reg "rt" rt;
diff --git a/mips/hgen/types.hgen b/mips/hgen/types.hgen
index e544902e..a1c61f4b 100644
--- a/mips/hgen/types.hgen
+++ b/mips/hgen/types.hgen
@@ -18,23 +18,23 @@ type mipsRTypeOp =
 | 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"
+| 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
@@ -52,15 +52,15 @@ type mipsITypeOp =
 | MIPSIOpXORI
 
 let pp_itype_op = function
-| MIPSIOpADDI   -> "ADDI"
-| MIPSIOpADDIU  -> "ADDIU"
-| MIPSIOpANDI   -> "ANDI"
-| MIPSIOpDADDI  -> "DADDI"
-| MIPSIOpDADDIU -> "DADDIU"
-| MIPSIOpORI    -> "ORI"
-| MIPSIOpSLTI   -> "SLTI"
-| MIPSIOpSLTIU  -> "SLTIU"
-| MIPSIOpXORI   -> "XORI"
+| MIPSIOpADDI   -> "addi"
+| MIPSIOpADDIU  -> "addiu"
+| MIPSIOpANDI   -> "andi"
+| MIPSIOpDADDI  -> "daddi"
+| MIPSIOpDADDIU -> "daddiu"
+| MIPSIOpORI    -> "ori"
+| MIPSIOpSLTI   -> "slti"
+| MIPSIOpSLTIU  -> "sltiu"
+| MIPSIOpXORI   -> "xori"
 
 type mipsShiftIOp = 
 | MIPSDSLL
@@ -74,15 +74,15 @@ type mipsShiftIOp =
 | MIPSSRL
 
 let pp_shifti_op = function
-| MIPSDSLL   -> "DSLL" 
-| MIPSDSLL32 -> "DSLL32"
-| MIPSDSRA   -> "DSRA"  
-| MIPSDSRA32 -> "DSRA32"
-| MIPSDSRL   -> "DSRL"  
-| MIPSDSRL32 -> "DSRL32"
-| MIPSSLL    -> "SLL"   
-| MIPSSRA    -> "SRA"   
-| MIPSSRL    -> "SRL"   
+| MIPSDSLL   -> "dsll" 
+| MIPSDSLL32 -> "dsll32"
+| MIPSDSRA   -> "dsra"  
+| MIPSDSRA32 -> "dsra32"
+| MIPSDSRL   -> "dsrl"  
+| MIPSDSRL32 -> "dsrl32"
+| MIPSSLL    -> "sll"   
+| MIPSSRA    -> "sra"   
+| MIPSSRL    -> "srl"   
 
 type mipsShiftVOp = 
 | MIPSDSLLV
@@ -93,12 +93,12 @@ type mipsShiftVOp =
 | MIPSSRLV
 
 let pp_shiftv_op = function
-| MIPSDSLLV -> "DSLLV"
-| MIPSDSRAV -> "DSRAV"
-| MIPSDSRLV -> "DSRLV"
-| MIPSSLLV  -> "SLLV" 
-| MIPSSRAV  -> "SRAV" 
-| MIPSSRLV  -> "SRLV" 
+| MIPSDSLLV -> "dsllv"
+| MIPSDSRAV -> "dsrav"
+| MIPSDSRLV -> "dsrlv"
+| MIPSSLLV  -> "sllv" 
+| MIPSSRAV  -> "srav" 
+| MIPSSRLV  -> "srlv" 
 
 type mipsMulDivOp =
 | MIPSDDIV
@@ -115,18 +115,18 @@ type mipsMulDivOp =
 | 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" 
+| 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
@@ -135,10 +135,10 @@ type mipsMFHiLoOp =
 | MIPSMTLO
 
 let pp_mfhilo_op = function
-| MIPSMFHI -> "MFHI"
-| MIPSMFLO -> "MFLO"
-| MIPSMTHI -> "MTHI"
-| MIPSMTLO -> "MTLO"
+| MIPSMFHI -> "mfhi"
+| MIPSMFLO -> "mflo"
+| MIPSMTHI -> "mthi"
+| MIPSMTLO -> "mtlo"
 
 type mipsWordWidth = 
 | MIPSByte
@@ -157,41 +157,41 @@ type mipsCmp =
 | 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"
+  | (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"
+  | (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"
+  | (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"
+  | (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"
diff --git a/mips/hgen/types_trans_sail.hgen b/mips/hgen/types_trans_sail.hgen
index 303ef43c..63880ae9 100644
--- a/mips/hgen/types_trans_sail.hgen
+++ b/mips/hgen/types_trans_sail.hgen
@@ -1,3 +1,15 @@
+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 =