use shift 1-4 in backend

5 files changed, 62 insertions, 97 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 6a4095da..04f6969b 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -182,9 +182,9 @@ Inductive instruction : Type :=
   | Pfcompl (ft: ftest) (rd rs1 rs2: ireg)          (**r comparison float64 *)

 

   | Paddw               (rd rs1 rs2: ireg)          (**r add word *)

-  | Paddxw (shift : Z)  (rd rs1 rs2: ireg)          (**r add word *)

+  | Paddxw (shift : shift1_4)  (rd rs1 rs2: ireg)          (**r add word *)

   | Psubw               (rd rs1 rs2: ireg)          (**r sub word *)

-  | Psubxw (shift : Z)  (rd rs1 rs2: ireg)          (**r add word *)

+  | Psubxw (shift : shift1_4)  (rd rs1 rs2: ireg)          (**r add word *)

   | Pmulw               (rd rs1 rs2: ireg)          (**r mul word *)

   | Pandw               (rd rs1 rs2: ireg)          (**r and word *)

   | Pnandw              (rd rs1 rs2: ireg)          (**r nand word *)

@@ -202,9 +202,9 @@ Inductive instruction : Type :=
   | Pmsubw              (rd rs1 rs2: ireg)          (**r multiply-add words *)

 

   | Paddl               (rd rs1 rs2: ireg)          (**r add long *)

-  | Paddxl (shift : Z)  (rd rs1 rs2: ireg)          (**r add long shift *)

+  | Paddxl (shift : shift1_4)  (rd rs1 rs2: ireg)          (**r add long shift *)

   | Psubl               (rd rs1 rs2: ireg)          (**r sub long *)

-  | Psubxl (shift : Z)  (rd rs1 rs2: ireg)          (**r sub long shift *)

+  | Psubxl (shift : shift1_4)  (rd rs1 rs2: ireg)          (**r sub long shift *)

   | Pandl               (rd rs1 rs2: ireg)          (**r and long *)

   | Pnandl              (rd rs1 rs2: ireg)          (**r nand long *)

   | Porl                (rd rs1 rs2: ireg)          (**r or long *)

@@ -232,9 +232,9 @@ Inductive instruction : Type :=
   | Pcompiw (it: itest) (rd rs: ireg) (imm: int)    (**r comparison imm word *)

 

   | Paddiw              (rd rs: ireg) (imm: int)    (**r add imm word *)

-  | Paddxiw (shift : Z) (rd rs: ireg) (imm: int)    (**r add imm word *)

+  | Paddxiw (shift : shift1_4) (rd rs: ireg) (imm: int)    (**r add imm word *)

   | Psubiw              (rd rs: ireg) (imm: int)    (**r subtract imm word *)

-  | Psubxiw (shift : Z) (rd rs: ireg) (imm: int)    (**r subtract imm word *)

+  | Psubxiw (shift : shift1_4) (rd rs: ireg) (imm: int)    (**r subtract imm word *)

   | Pmuliw              (rd rs: ireg) (imm: int)    (**r mul imm word *)

   | Pandiw              (rd rs: ireg) (imm: int)    (**r and imm word *)

   | Pnandiw             (rd rs: ireg) (imm: int)    (**r nand imm word *)

@@ -258,9 +258,9 @@ Inductive instruction : Type :=
   (** Arith RRI64 *)

   | Pcompil (it: itest) (rd rs: ireg) (imm: int64)  (**r comparison imm long *)

   | Paddil              (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

-  | Paddxil (shift : Z) (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

+  | Paddxil (shift : shift1_4) (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

   | Psubil              (rd rs: ireg) (imm: int64)  (**r subtract imm long *)

-  | Psubxil (shift : Z) (rd rs: ireg) (imm: int64)  (**r subtract imm long *)

+  | Psubxil (shift : shift1_4) (rd rs: ireg) (imm: int64)  (**r subtract imm long *)

   | Pmulil              (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

   | Pandil              (rd rs: ireg) (imm: int64)  (**r and immediate long *) 

   | Pnandil             (rd rs: ireg) (imm: int64)  (**r and immediate long *) 

diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index e8ea4318..e332cedc 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -429,9 +429,9 @@ Inductive arith_name_rrr : Type :=
   | Pfcompl (ft: ftest)                             (**r comparison float64 *)
 
   | Paddw                                           (**r add word *)
-  | Paddxw (shift : Z)                              (**r add shift *)
+  | Paddxw (shift : shift1_4)                              (**r add shift *)
   | Psubw                                           (**r sub word word *)
-  | Psubxw (shift : Z)                              (**r sub shift word *)
+  | Psubxw (shift : shift1_4)                              (**r sub shift word *)
   | Pmulw                                           (**r mul word *)
   | Pandw                                           (**r and word *)
   | Pnandw                                          (**r nand word *)
@@ -447,9 +447,9 @@ Inductive arith_name_rrr : Type :=
   | Psllw                                           (**r shift left logical word *)
 
   | Paddl                                           (**r add long *)
-  | Paddxl (shift : Z)                              (**r add shift long *)
+  | Paddxl (shift : shift1_4)                              (**r add shift long *)
   | Psubl                                           (**r sub long *)
-  | Psubxl (shift : Z)                              (**r sub shift long *)
+  | Psubxl (shift : shift1_4)                              (**r sub shift long *)
   | Pandl                                           (**r and long *)
   | Pnandl                                          (**r nand long *)
   | Porl                                            (**r or long *)
@@ -476,9 +476,9 @@ Inductive arith_name_rri32 : Type :=
   | Pcompiw (it: itest)                             (**r comparison imm word *)
 
   | Paddiw                                          (**r add imm word *)
-  | Paddxiw (shift : Z)
+  | Paddxiw (shift : shift1_4)
   | Psubiw                                          (**r add imm word *)
-  | Psubxiw (shift : Z)
+  | Psubxiw (shift : shift1_4)
   | Pmuliw                                          (**r add imm word *)
   | Pandiw                                          (**r and imm word *)
   | Pnandiw                                         (**r nand imm word *)
@@ -502,9 +502,9 @@ Inductive arith_name_rri32 : Type :=
 Inductive arith_name_rri64 : Type :=
   | Pcompil (it: itest)                             (**r comparison imm long *)
   | Paddil                                          (**r add immediate long *) 
-  | Paddxil (shift : Z)
+  | Paddxil (shift : shift1_4)
   | Psubil
-  | Psubxil (shift : Z)
+  | Psubxil (shift : shift1_4)
   | Pmulil                                          (**r mul immediate long *) 
   | Pandil                                          (**r and immediate long *) 
   | Pnandil                                         (**r nand immediate long *) 
@@ -1068,25 +1068,12 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pfmuld => Val.mulf v1 v2
   | Pfmulw => Val.mulfs v1 v2
 
-  | Paddxw shift =>
-    if Z.leb shift 4 && Z.leb 1 shift
-    then Val.add v1 (Val.shl v2 (Vint (Int.repr shift)))
-    else Vundef
-
-  | Paddxl shift =>
-    if Z.leb shift 4 && Z.leb 1 shift
-    then Val.addl v1 (Val.shll v2 (Vint (Int.repr shift)))
-    else Vundef
-
-  | Psubxw shift =>
-    if Z.leb shift 4 && Z.leb 1 shift
-    then Val.sub v1 (Val.shl v2 (Vint (Int.repr shift)))
-    else Vundef
-
-  | Psubxl shift =>
-    if Z.leb shift 4 && Z.leb 1 shift
-    then Val.subl v1 (Val.shll v2 (Vint (Int.repr shift)))
-    else Vundef
+  | Paddxw shift => Val.add v1 (Val.shl v2 (Vint (int_of_shift1_4 shift)))
+  | Paddxl shift => Val.addl v1 (Val.shll v2 (Vint (int_of_shift1_4 shift)))
+
+  | Psubxw shift => Val.sub v1 (Val.shl v2 (Vint (int_of_shift1_4 shift)))
+
+  | Psubxl shift => Val.subl v1 (Val.shll v2 (Vint (int_of_shift1_4 shift)))
   end.
 
 Definition arith_eval_rri32 n v i :=
@@ -1112,14 +1099,8 @@ Definition arith_eval_rri32 n v i :=
   | Psrxil  => ExtValues.val_shrxl v (Vint i)
   | Psrlil  => Val.shrlu v (Vint i)
   | Psrail  => Val.shrl  v (Vint i)
-  | Paddxiw shift =>
-        if Z.leb shift 4 && Z.leb 1 shift
-        then Val.add (Vint i) (Val.shl v (Vint (Int.repr shift)))
-        else Vundef
-  | Psubxiw shift =>
-        if Z.leb shift 4 && Z.leb 1 shift
-        then Val.sub (Vint i) (Val.shl v (Vint (Int.repr shift)))
-        else Vundef
+  | Paddxiw shift => Val.add (Vint i) (Val.shl v (Vint (int_of_shift1_4 shift)))
+  | Psubxiw shift => Val.sub (Vint i) (Val.shl v (Vint (int_of_shift1_4 shift)))
   end.
 
 Definition arith_eval_rri64 n v i :=
@@ -1136,14 +1117,8 @@ Definition arith_eval_rri64 n v i :=
   | Pnxoril  => Val.notl (Val.xorl  v (Vlong i))
   | Pandnil => Val.andl (Val.notl v) (Vlong i)
   | Pornil  => Val.orl (Val.notl v) (Vlong i)
-  | Paddxil shift =>
-    if Z.leb shift 4 && Z.leb 1 shift
-    then Val.addl (Vlong i) (Val.shll v (Vint (Int.repr shift)))
-    else Vundef
-  | Psubxil shift =>
-    if Z.leb shift 4 && Z.leb 1 shift
-    then Val.subl (Vlong i) (Val.shll v (Vint (Int.repr shift)))
-    else Vundef
+  | Paddxil shift => Val.addl (Vlong i) (Val.shll v (Vint (int_of_shift1_4 shift)))
+  | Psubxil shift => Val.subl (Vlong i) (Val.shll v (Vint (int_of_shift1_4 shift)))
   end.
 
 Definition arith_eval_arrr n v1 v2 v3 :=
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 5d16b79c..1aa17458 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -2,6 +2,20 @@ Require Import Coqlib.
 Require Import Integers.
 Require Import Values.
 
+Inductive shift1_4 : Type :=
+| SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4.
+
+Definition z_of_shift1_4 (x : shift1_4) :=
+  match x with
+  | SHIFT1 => 1
+  | SHIFT2 => 2
+  | SHIFT3 => 3
+  | SHIFT4 => 4
+  end.
+
+Definition int_of_shift1_4 (x : shift1_4) :=
+  Int.repr (z_of_shift1_4 x).
+
 Definition is_bitfield stop start :=
   (Z.leb start stop)
     && (Z.geb start Z.zero)
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index b93a9fc3..4abd104e 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -66,20 +66,6 @@ Definition arg_type_of_condition0 (cond: condition0) :=
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
 
-Inductive shift1_4 : Type :=
-| SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4.
-
-Definition z_of_shift1_4 (x : shift1_4) :=
-  match x with
-  | SHIFT1 => 1
-  | SHIFT2 => 2
-  | SHIFT3 => 3
-  | SHIFT4 => 4
-  end.
-
-Definition int_of_shift1_4 (x : shift1_4) :=
-  Int.repr (z_of_shift1_4 x).
-
 Inductive operation : Type :=
   | Omove                    (**r [rd = r1] *)
   | Ointconst (n: int)       (**r [rd] is set to the given integer constant *)
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 83d12da7..6a21e63d 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -130,6 +130,12 @@ module Target (*: TARGET*) =
       | RA   -> "$ra"
       | _ -> assert false
 
+    let scale_of_shift1_4 = let open ExtValues in function
+      | SHIFT1 -> 2
+      | SHIFT2 -> 4
+      | SHIFT3 -> 8
+      | SHIFT4 -> 16;;
+    
 (* Names of sections *)
 
     let name_of_section = function
@@ -513,17 +519,13 @@ module Target (*: TARGET*) =
 
       | Paddw (rd, rs1, rs2) ->
          fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Paddxw (zshift, rd, rs1, rs2) ->
-         let shift = camlint_of_coqint zshift in
-         assert(shift >= 1l && shift <= 4l);
-         fprintf oc "	addx%dw	%a = %a, %a\n" (1 lsl (Int32.to_int shift))
+      | Paddxw (s14, rd, rs1, rs2) ->
+         fprintf oc "	addx%dw	%a = %a, %a\n" (scale_of_shift1_4 s14)
            ireg rd ireg rs1 ireg rs2
       | Psubw (rd, rs1, rs2) ->
          fprintf oc "	sbfw	%a = %a, %a\n" ireg rd ireg rs2 ireg rs1
-      | Psubxw (zshift, rd, rs1, rs2) ->
-         let shift = camlint_of_coqint zshift in
-         assert(shift >= 1l && shift <= 4l);
-         fprintf oc "	subx%dw	%a = %a, %a\n" (1 lsl (Int32.to_int shift))
+      | Psubxw (s14, rd, rs1, rs2) ->
+         fprintf oc "	subx%dw	%a = %a, %a\n" (scale_of_shift1_4 s14)
            ireg rd ireg rs1 ireg rs2
       | Pmulw (rd, rs1, rs2) ->
          fprintf oc "	mulw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
@@ -558,17 +560,13 @@ module Target (*: TARGET*) =
 
       | Paddl (rd, rs1, rs2) ->
          fprintf oc "	addd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Paddxl (zshift, rd, rs1, rs2) ->
-         let shift = camlint_of_coqint zshift in
-         assert(shift >= 1l && shift <= 4l);
-         fprintf oc "	addx%dd	%a = %a, %a\n" (1 lsl (Int32.to_int shift))
+      | Paddxl (s14, rd, rs1, rs2) ->
+         fprintf oc "	addx%dd	%a = %a, %a\n" (scale_of_shift1_4 s14)
            ireg rd ireg rs1 ireg rs2
       | Psubl (rd, rs1, rs2) ->
          fprintf oc "	sbfd	%a = %a, %a\n" ireg rd ireg rs2 ireg rs1
-      | Psubxl (zshift, rd, rs1, rs2) ->
-         let shift = camlint_of_coqint zshift in
-         assert(shift >= 1l && shift <= 4l);
-         fprintf oc "	sbfx%dd	%a = %a, %a\n" (1 lsl (Int32.to_int shift))
+      | Psubxl (s14, rd, rs1, rs2) ->
+         fprintf oc "	sbfx%dd	%a = %a, %a\n" (scale_of_shift1_4 s14)
            ireg rd ireg rs1 ireg rs2
       | Pandl (rd, rs1, rs2) ->
          fprintf oc "	andd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
@@ -619,17 +617,13 @@ module Target (*: TARGET*) =
          fprintf oc "	compw.%a	%a = %a, %a\n" icond it ireg rd ireg rs coqint imm
       | Paddiw (rd, rs, imm) ->
          fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs coqint imm
-      | Paddxiw (zshift, rd, rs, imm) ->
-         let shift = camlint_of_coqint zshift in
-         assert(shift >= 1l && shift <= 4l);
-         fprintf oc "	addx%dw	%a = %a, %a\n"  (1 lsl (Int32.to_int shift))
+      | Paddxiw (s14, rd, rs, imm) ->
+         fprintf oc "	addx%dw	%a = %a, %a\n"  (scale_of_shift1_4 s14)
            ireg rd ireg rs coqint imm
       | Psubiw (rd, rs, imm) ->
          fprintf oc "	sbfw	%a = %a, %a\n" ireg rd ireg rs coqint imm
-      | Psubxiw (zshift, rd, rs, imm) ->
-         let shift = camlint_of_coqint zshift in
-         assert(shift >= 1l && shift <= 4l);
-         fprintf oc "	sbfx%dw	%a = %a, %a\n"  (1 lsl (Int32.to_int shift))
+      | Psubxiw (s14, rd, rs, imm) ->
+         fprintf oc "	sbfx%dw	%a = %a, %a\n"  (scale_of_shift1_4 s14)
            ireg rd ireg rs coqint imm
       | Pmuliw (rd, rs, imm) ->
          fprintf oc "	mulw	%a = %a, %a\n" ireg rd ireg rs coqint imm
@@ -676,17 +670,13 @@ module Target (*: TARGET*) =
          fprintf oc "	compd.%a	%a = %a, %a\n" icond it ireg rd ireg rs coqint64 imm
       | Paddil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	addd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
-      | Paddxil (zshift, rd, rs, imm) ->
-         let shift = camlint_of_coqint zshift in
-         assert(shift >= 1l && shift <= 4l);
-         fprintf oc "	addx%dd	%a = %a, %a\n"  (1 lsl (Int32.to_int shift))
+      | Paddxil (s14, rd, rs, imm) ->
+         fprintf oc "	addx%dd	%a = %a, %a\n"  (scale_of_shift1_4 s14)
            ireg rd ireg rs coqint imm
       | Psubil (rd, rs, imm) ->
          fprintf oc "	sbfd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
-      | Psubxil (zshift, rd, rs, imm) ->
-         let shift = camlint_of_coqint zshift in
-         assert(shift >= 1l && shift <= 4l);
-         fprintf oc "	sbfx%dd	%a = %a, %a\n"  (1 lsl (Int32.to_int shift))
+      | Psubxil (s14, rd, rs, imm) ->
+         fprintf oc "	sbfx%dd	%a = %a, %a\n"  (scale_of_shift1_4 s14)
            ireg rd ireg rs coqint64 imm
       | Pmulil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	muld	%a = %a, %a\n" ireg rd ireg rs coqint64 imm