apply .xs onto addx4 etc

10 files changed, 180 insertions, 27 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 7be83962..71af4798 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -449,6 +449,12 @@ Definition transl_op
   | Oaddximm shift n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (Paddxiw shift rd rs n ::i k)
+  | Oaddxl shift, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Paddxl shift rd rs1 rs2 ::i k)
+  | Oaddxlimm shift n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Paddxil shift rd rs n ::i k)
   | Oneg, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (Pnegw rd rs ::i k)
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index e1a7f916..9a933741 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -1069,7 +1069,7 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pfmulw => Val.mulfs v1 v2
 
   | Paddxw shift => ExtValues.addx (int_of_shift1_4 shift) v1 v2
-  | Paddxl shift => Val.addl v1 (Val.shll v1 (Vint (int_of_shift1_4 shift)))
+  | Paddxl shift => ExtValues.addxl (int_of_shift1_4 shift) v1 v2
 
   | Prevsubxw shift => Val.sub v2 (Val.shl v1 (Vint (int_of_shift1_4 shift)))
 
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 32d84b60..284d55f3 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -201,4 +201,7 @@ Proof.
 Qed.
 
 Definition addx sh v1 v2 :=
-  Val.add v2 (Val.shl v1 (Vint sh)).
\ No newline at end of file
+  Val.add v2 (Val.shl v1 (Vint sh)).
+
+Definition addxl sh v1 v2 :=
+  Val.addl v2 (Val.shll v1 (Vint sh)).
\ No newline at end of file
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 69620934..98635677 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -454,8 +454,8 @@ Definition eval_operation
   | Ocast32unsigned, v1 :: nil => Some (Val.longofintu v1)
   | Oaddl, v1 :: v2 :: nil => Some (Val.addl v1 v2)
   | Oaddlimm n, v1::nil => Some (Val.addl v1 (Vlong n))
-  | Oaddxl shift, v1 :: v2 :: nil => Some (Val.addl v2 (Val.shll v1 (Vint (int_of_shift1_4 shift))))
-  | Oaddxlimm shift n, v1 :: nil => Some (Val.addl (Vlong n) (Val.shll v1 (Vint (int_of_shift1_4 shift))))
+  | Oaddxl s14, v1 :: v2 :: nil => Some (addxl (int_of_shift1_4 s14) v1 v2)
+  | Oaddxlimm s14 n, v1 :: nil => Some (addxl (int_of_shift1_4 s14) v1 (Vlong n))
   | Onegl, v1::nil => Some (Val.negl v1)
   | Osubl, v1::v2::nil => Some (Val.subl v1 v2)
   | Orevsublimm n, v1 :: nil => Some (Val.subl (Vlong n) v1)
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 3618969a..24087caf 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -405,6 +405,10 @@ let alu_lite_x : int array = let resmap = fun r -> match r with
   | "ISSUE" -> 2 | "TINY" -> 1 | "LITE" -> 1 |  _ -> 0 
   in Array.of_list (List.map resmap resource_names)
 
+let alu_lite_y : int array = let resmap = fun r -> match r with 
+  | "ISSUE" -> 3 | "TINY" -> 1 | "LITE" -> 1 |  _ -> 0 
+  in Array.of_list (List.map resmap resource_names)
+
 let alu_full : int array = let resmap = fun r -> match r with
   | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 | "ALU" -> 1 | _ -> 0
   in Array.of_list (List.map resmap resource_names)
@@ -588,15 +592,23 @@ let rec_to_usage r =
   and real_inst = ab_inst_to_real r.inst
   in match real_inst with
   | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw
-  | Nxorw | Andnw | Ornw | Addxw  -> 
+  | Nxorw | Andnw | Ornw -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | _ -> raise InvalidEncoding)
   | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord
-  | Nxord | Andnd | Ornd | Cmoved | Addxd -> 
+  | Nxord | Andnd | Ornd | Cmoved -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | Some E27U27L10 -> alu_tiny_y)
+  | Addxw -> 
+      (match encoding with None | Some U6 | Some S10 -> alu_lite 
+                          | Some U27L5 | Some U27L10 -> alu_lite_x
+                          | _ -> raise InvalidEncoding)
+  | Addxd -> 
+      (match encoding with None | Some U6 | Some S10 -> alu_lite 
+                          | Some U27L5 | Some U27L10 -> alu_lite_x
+                          | Some E27U27L10 -> alu_lite_y)
   | Compw -> (match encoding with None -> alu_tiny
                                 | Some U6 | Some S10 | Some U27L5 -> alu_tiny_x
                                 | _ -> raise InvalidEncoding)
@@ -620,9 +632,9 @@ let rec_to_usage r =
                                 | Some U27L5 | Some U27L10 -> mau_x
                                 | Some E27U27L10 -> mau_y)
   | Nop -> alu_nop
-  | Sraw | Srlw | Srsw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding)
+  | Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding)
   (* TODO: check *)
-  | Srsd | Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding)
+  | Srsw | Srsd | Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding)
   | Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding)
   | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index b29b9712..fe739a01 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -66,6 +66,12 @@ Definition longofintu (e: expr) :=
 
 (** ** Integer addition and pointer addition *)
 
+Definition addlimm_shllimm sh k2 e1 :=
+  match shift1_4_of_z (Int.unsigned sh) with
+  | Some s14 => Eop (Oaddxlimm s14 k2) (e1:::Enil)
+  | None => Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil)
+  end.
+
 Nondetfunction addlimm (n: int64) (e: expr) :=
   if Int64.eq n Int64.zero then e else
   match e with
@@ -76,9 +82,16 @@ Nondetfunction addlimm (n: int64) (e: expr) :=
      else Eop (Oaddlimm n) (e ::: Enil))
   | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil
   | Eop (Oaddlimm m) (t ::: Enil) => Eop (Oaddlimm(Int64.add n m)) (t ::: Enil)
+  | Eop (Oshllimm sh) (t1:::Enil) => addlimm_shllimm sh n t1
   | _ => Eop (Oaddlimm n) (e ::: Enil)
   end.
 
+Definition addl_shllimm n e1 e2 :=
+  match shift1_4_of_z (Int.unsigned n) with
+  | Some s14 => Eop (Oaddxl s14) (e1:::e2:::Enil)
+  | None => Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil)
+  end.
+
 Nondetfunction addl (e1: expr) (e2: expr) :=
   if Archi.splitlong then SplitLong.addl e1 e2 else
   match e1, e2 with
@@ -102,6 +115,10 @@ Nondetfunction addl (e1: expr) (e2: expr) :=
       Eop (Omaddlimm n) (t1:::t2:::Enil)
   | (Eop (Omullimm n) (t2:::Enil)), t1 =>
       Eop (Omaddlimm n) (t1:::t2:::Enil)
+  | (Eop (Oshllimm n) (t1:::Enil)), t2 =>
+    addl_shllimm n t1 t2
+  | t2, (Eop (Oshllimm n) (t1:::Enil)) =>
+    addl_shllimm n t1 t2
   | _, _ => Eop Oaddl (e1:::e2:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 257c7fd9..3c9f64d5 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -119,6 +119,67 @@ Proof.
 - TrivialExists.
 Qed.
 
+
+Theorem eval_addlimm_shllimm:
+  forall sh k2, unary_constructor_sound (addlimm_shllimm sh k2) (fun x => ExtValues.addxl sh x (Vlong k2)).
+Proof.
+  red; unfold addlimm_shllimm; intros.
+  destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT.
+  - TrivialExists. simpl.
+    f_equal.
+    unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *.
+    destruct (Z.eq_dec _ _) as [e1|].
+    { replace s14 with SHIFT1 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e1.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e1.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e2|].
+    { replace s14 with SHIFT2 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e2.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e2.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e3|].
+    { replace s14 with SHIFT3 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e3.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e3.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e4|].
+    { replace s14 with SHIFT4 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e4.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e4.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    discriminate.
+  - unfold addxl. rewrite Val.addl_commut.
+    TrivialExists.
+    repeat (try eassumption; try econstructor).
+    simpl.
+    reflexivity.
+Qed.
+
 Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)).
 Proof.
   unfold addlimm; intros; red; intros.
@@ -136,9 +197,47 @@ Proof.
   destruct sp; simpl; auto. destruct Archi.ptr64; auto. 
   rewrite Ptrofs.add_assoc, (Ptrofs.add_commut m0). auto. 
 - subst x. rewrite Val.addl_assoc. rewrite Int64.add_commut. TrivialExists.
+-  pose proof eval_addlimm_shllimm as ADDXL.
+      unfold unary_constructor_sound in ADDXL.
+      unfold addxl in ADDXL.
+      rewrite Val.addl_commut.
+      subst x.
+      apply ADDXL; assumption.
 - TrivialExists.
 Qed.
 
+Lemma eval_addxl: forall n, binary_constructor_sound (addl_shllimm n) (ExtValues.addxl n).
+Proof.
+  red.
+  intros.
+  unfold addl_shllimm.
+  destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT.
+  - TrivialExists.
+    simpl.
+    f_equal. f_equal.
+    unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *.
+    destruct (Z.eq_dec _ _) as [e1|].
+    { replace s14 with SHIFT1 by congruence.
+      rewrite <- e1.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e2|].
+    { replace s14 with SHIFT2 by congruence.
+      rewrite <- e2.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e3|].
+    { replace s14 with SHIFT3 by congruence.
+      rewrite <- e3.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e4|].
+    { replace s14 with SHIFT4 by congruence.
+      rewrite <- e4.
+      apply Int.repr_unsigned. }
+    discriminate.
+    (* Oaddxl *)
+  - TrivialExists;
+    repeat econstructor; eassumption.
+Qed.
+
 Theorem eval_addl: binary_constructor_sound addl Val.addl.
 Proof.
   unfold addl. destruct Archi.splitlong eqn:SL. 
@@ -193,6 +292,14 @@ Proof.
   - subst. rewrite Val.addl_commut. TrivialExists.
   - subst. TrivialExists.
   - subst. rewrite Val.addl_commut. TrivialExists.
+  - subst. pose proof eval_addxl as ADDXL.
+    unfold binary_constructor_sound in ADDXL.
+    rewrite Val.addl_commut.
+    apply ADDXL; assumption.
+    (* Oaddxl *)
+  - subst. pose proof eval_addxl as ADDXL.
+    unfold binary_constructor_sound in ADDXL.
+    apply ADDXL; assumption.
   - TrivialExists.
 Qed.
 
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 9b4cfeb0..3427dda3 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -611,13 +611,14 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
      else (Aglobal id ofs, Enil))
   | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil)
   | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
-  | Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) =>
+  | Eop (Oaddxl sh) (e1:::e2:::Enil) =>
+    let zscale := ExtValues.z_of_shift1_4 sh in
+    let scale := Int.repr zscale in
     (if Compopts.optim_fxsaddr tt
-     then let zscale := Int.unsigned scale in
-          if Z.eq_dec zscale (zscale_of_chunk chunk)
-          then (Aindexed2XS zscale, e1:::e2:::Enil) 
-          else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil)
-     else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil))
+     then if Z.eq_dec zscale (zscale_of_chunk chunk)
+          then (Aindexed2XS zscale, e2:::e1:::Enil) 
+          else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil)
+     else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil))
   | Eop Oaddl (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) 
   | _ => (Aindexed Ptrofs.zero, e:::Enil)
   end.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 25b34fb9..8e1812c6 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -1377,18 +1377,25 @@ Proof.
   - exists (v1 :: nil); split. eauto with evalexpr. simpl.
     destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 
     simpl. auto.
-  - destruct (Compopts.optim_fxsaddr tt).
-    + destruct (Z.eq_dec _ _).
-      * exists (v1 :: v2 :: nil); split.
-        repeat (constructor; auto). simpl. rewrite Int.repr_unsigned. destruct v2; simpl in *; congruence.
-      * exists (v1 :: v0 :: nil); split.
-        repeat (constructor; auto). econstructor.
-        repeat (constructor; auto). eassumption. simpl. congruence.
-        simpl. congruence.
-    + exists (v1 :: v0 :: nil); split.
-        repeat (constructor; auto). econstructor.
-        repeat (constructor; auto). eassumption. simpl. congruence.
+  - unfold addxl in *.
+    destruct (Compopts.optim_fxsaddr tt).
+    + unfold int_of_shift1_4 in *.
+      destruct (Z.eq_dec _ _).
+      * exists (v0 :: v1 :: nil); split.
+        repeat (constructor; auto). simpl.
+        congruence.
+      * eexists; split.
+        repeat (constructor; auto). eassumption.
+        econstructor.
+        repeat (constructor; auto). eassumption. simpl.
+        reflexivity.
         simpl. congruence.
+    + eexists; split.
+        repeat (constructor; auto). eassumption.
+        econstructor.
+        repeat (constructor; auto). eassumption. simpl.
+        reflexivity.
+        simpl. unfold int_of_shift1_4 in *. congruence.
   - exists (v1 :: v0 :: nil); split. repeat (constructor; auto). simpl. congruence.
   - exists (v :: nil);  split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto.
 Qed.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 1f47fd8f..10f25701 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -394,6 +394,7 @@ Proof.
              end) with (Val.sub (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))).
     + eauto with va.
     + destruct a1; destruct shift; reflexivity.
+  - unfold addxl. eauto with va.
   - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
     | Vlong n2 => Vlong (Int64.add n n2)
     | Vptr b2 ofs2 =>
@@ -401,8 +402,7 @@ Proof.
         then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n))
         else Vundef
     | _ => Vundef
-             end) with
-    (Val.addl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
+             end) with (Val.addl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
     + eauto with va.
     + destruct a1; destruct shift; reflexivity.
   - inv H1; constructor.