add with shift, beginning

7 files changed, 86 insertions, 13 deletions

diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index c1f21f8d..e1a7f916 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -1068,7 +1068,7 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pfmuld => Val.mulf v1 v2
   | Pfmulw => Val.mulfs v1 v2
 
-  | Paddxw shift => Val.add v2 (Val.shl v1 (Vint (int_of_shift1_4 shift)))
+  | 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)))
 
   | Prevsubxw shift => Val.sub v2 (Val.shl v1 (Vint (int_of_shift1_4 shift)))
@@ -1099,7 +1099,7 @@ 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 => Val.add (Vint i) (Val.shl v (Vint (int_of_shift1_4 shift)))
+  | Paddxiw shift => ExtValues.addx (int_of_shift1_4 shift) v (Vint i)
   | Prevsubxiw shift => Val.sub (Vint i) (Val.shl v (Vint (int_of_shift1_4 shift)))
   end.
 
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 735d5c3c..32d84b60 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -13,6 +13,28 @@ Definition z_of_shift1_4 (x : shift1_4) :=
   | SHIFT4 => 4
   end.
 
+Definition shift1_4_of_z (x : Z) :=
+  if Z.eq_dec x 1 then Some SHIFT1
+  else if Z.eq_dec x 2 then Some SHIFT2
+  else if Z.eq_dec x 3 then Some SHIFT3
+  else if Z.eq_dec x 4 then Some SHIFT4
+  else None.
+
+Lemma shift1_4_of_z_correct :
+  forall z,
+    match shift1_4_of_z z with
+    | Some x => z_of_shift1_4 x = z
+    | None => True
+    end.
+Proof.
+  intro. unfold shift1_4_of_z.
+  destruct (Z.eq_dec _ _); simpl; try congruence.
+  destruct (Z.eq_dec _ _); simpl; try congruence.
+  destruct (Z.eq_dec _ _); simpl; try congruence.
+  destruct (Z.eq_dec _ _); simpl; try congruence.
+  trivial.
+Qed.
+
 Definition int_of_shift1_4 (x : shift1_4) :=
   Int.repr (z_of_shift1_4 x).
 
@@ -178,3 +200,5 @@ Proof.
   apply Int64.neg_mul_distr_r.
 Qed.
 
+Definition addx sh v1 v2 :=
+  Val.add v2 (Val.shl v1 (Vint sh)).
\ No newline at end of file
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index ac40c293..69620934 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -403,8 +403,8 @@ Definition eval_operation
   | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
   | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2)
   | Oaddimm n, v1 :: nil => Some (Val.add v1 (Vint n))
-  | Oaddx shift, v1 :: v2 :: nil => Some (Val.add v2 (Val.shl v1 (Vint (int_of_shift1_4 shift))))
-  | Oaddximm shift n, v1 :: nil => Some (Val.add (Vint n) (Val.shl v1 (Vint (int_of_shift1_4 shift))))
+  | Oaddx s14, v1 :: v2 :: nil => Some (addx (int_of_shift1_4 s14) v1 v2)
+  | Oaddximm s14 n, v1 :: nil => Some (addx (int_of_shift1_4 s14) v1 (Vint n))
   | Oneg, v1 :: nil => Some (Val.neg v1)
   | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2)
   | Orevsubimm n, v1 :: nil => Some (Val.sub (Vint n) v1)
@@ -1446,7 +1446,8 @@ Proof.
   (* addx, addximm *)
   - apply Val.add_inject; trivial.
     inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto.
-  - inv H4; simpl; trivial. try destruct (Int.ltu _ _); simpl; auto.
+  - inv H4; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
   (* neg, sub *)
   - inv H4; simpl; auto.
   - apply Val.sub_inject; auto.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index f428fe49..3618969a 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -466,6 +466,7 @@ type real_instruction =
   | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd
   | Maddw | Maddd | Msbfw | Msbfd | Cmoved
   | Make | Nop | Extfz | Extfs | Insf
+  | Addxw | Addxd
   (* LSU *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo
   | Sb | Sh | Sw | Sd | Sq | So
@@ -479,6 +480,8 @@ type real_instruction =
 
 let ab_inst_to_real = function
   | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw
+  | "Paddxw" | "Paddxiw" -> Addxw
+  | "Paddxl" | "Paddxil" -> Addxd
   | "Paddl" | "Paddil" | "Pmv" | "Pmvw2l" -> Addd
   | "Pandw" | "Pandiw" -> Andw
   | "Pnandw" | "Pnandiw" -> Nandw
@@ -585,12 +588,12 @@ 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  -> 
+  | Nxorw | Andnw | Ornw | Addxw  -> 
       (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 -> 
+  | Nxord | Andnd | Ornd | Cmoved | Addxd -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | Some E27U27L10 -> alu_tiny_y)
@@ -643,7 +646,7 @@ let real_inst_to_latency = function
   | Rorw | Nandw | Norw | Nxorw | Ornw | Andnw
   | Nandd | Nord | Nxord | Ornd | Andnd
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srsd | Srld | Slld | Xord | Make
-  | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved
+  | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved | Addxw | Addxd
         -> 1
   | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
   | Mulw | Muld | Maddw | Maddd | Msbfw | Msbfd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 81e288cb..ae9d64b9 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -114,6 +114,12 @@ Nondetfunction addimm (n: int) (e: expr) :=
   | _ => Eop (Oaddimm n) (e ::: Enil)
   end.
 
+Definition add_shlimm n e1 e2 :=
+  match shift1_4_of_z (Int.unsigned n) with
+  | Some s14 => Eop (Oaddx s14) (e1:::e2:::Enil)
+  | None => Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil)
+  end.
+
 Nondetfunction add (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 => addimm n1 t2
@@ -135,7 +141,9 @@ Nondetfunction add (e1: expr) (e2: expr) :=
   | t1, (Eop (Omulimm n) (t2:::Enil)) =>
       Eop (Omaddimm n) (t1:::t2:::Enil)
   | (Eop (Omulimm n) (t2:::Enil)), t1 =>
-      Eop (Omaddimm n) (t1:::t2:::Enil)
+    Eop (Omaddimm n) (t1:::t2:::Enil)
+  | (Eop (Oshlimm n) (t1:::Enil)), t2 =>
+    add_shlimm n t1 t2
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 17024826..7b026bf5 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -201,6 +201,37 @@ Proof.
     + TrivialExists.
 Qed.
 
+Lemma eval_addx: forall n, binary_constructor_sound (add_shlimm n) (ExtValues.addx n).
+Proof.
+  red.
+  intros.
+  unfold add_shlimm.
+  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.
+  - TrivialExists;
+    repeat econstructor; eassumption.
+Qed.
+  
 Theorem eval_add: binary_constructor_sound add Val.add.
 Proof.
   red; intros until y.
@@ -238,6 +269,11 @@ Proof.
     subst. TrivialExists.
   - (* Omaddimm rev *)
     subst. rewrite Val.add_commut. TrivialExists.
+    (* Oaddx *)
+  - subst. pose proof eval_addx as ADDX.
+    unfold binary_constructor_sound in ADDX.
+    rewrite Val.add_commut.
+    apply ADDX; assumption.
   - TrivialExists.
 Qed.
 
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index adc27010..1f47fd8f 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -371,19 +371,20 @@ Theorem eval_static_operation_sound:
   list_forall2 (vmatch bc) vargs aargs ->
   vmatch bc vres (eval_static_operation op aargs).
 Proof.
-  unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs; intros;
-  destruct op; try (InvHyps; eauto with va).
+  unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs; intros.
+  destruct op; InvHyps; eauto with va.
   - destruct (propagate_float_constants tt); constructor.
   - destruct (propagate_float_constants tt); constructor.
   - rewrite Ptrofs.add_zero_l; eauto with va.
-  - replace (match Val.shl a1 (Vint (int_of_shift1_4 shift)) with
+  - unfold addx. eauto with va.
+  - replace(match Val.shl a1 (Vint (int_of_shift1_4 shift)) with
     | Vint n2 => Vint (Int.add n n2)
     | Vptr b2 ofs2 =>
         if Archi.ptr64
         then Vundef
         else Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int n))
     | _ => Vundef
-             end) with (Val.add (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))).
+    end)  with (Val.add (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))).
     + eauto with va.
     + destruct a1; destruct shift; reflexivity.
   - (*revsubimm*) inv H1; constructor.