Oaddx -> P

5 files changed, 48 insertions, 21 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 839d444d..ef980894 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -443,6 +443,12 @@ Definition transl_op
   | Oaddimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (addimm32 rd rs n ::i k)
+  | Oaddx shift, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Paddxw shift rd rs1 rs2 ::i k)
+  | Oaddximm shift n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Paddxiw 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/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 1569aedf..86a0ff88 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1693,7 +1693,7 @@ Opaque Int.eq.
   split; intros; Simpl.
   assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
   destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. 
-  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. 
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity.
 - (* Oshrximm *)
   econstructor; split.
   + apply exec_straight_one. simpl. eauto.
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 2bf9115e..c1f21f8d 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -1068,8 +1068,8 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pfmuld => Val.mulf v1 v2
   | Pfmulw => Val.mulfs v1 v2
 
-  | 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)))
+  | Paddxw shift => Val.add v2 (Val.shl v1 (Vint (int_of_shift1_4 shift)))
+  | 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)))
 
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 4abd104e..fb6c454c 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -405,8 +405,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 (Val.shl v1 (Vint (int_of_shift1_4 shift))) v2)
-  | Oaddximm shift n, v1 :: nil => Some (Val.add (Val.shl v1 (Vint (int_of_shift1_4 shift))) (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))))
   | 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)
@@ -457,8 +457,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 (Val.shll v1 (Vint (int_of_shift1_4 shift))) v2)
-  | Oaddxlimm shift n, v1 :: nil => Some (Val.addl (Val.shll v1 (Vint (int_of_shift1_4 shift))) (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))))
   | 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)
@@ -836,7 +836,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - apply type_add.
   (* addx, addximm *)
   - apply type_add.
-  - apply type_add.
+  - destruct v0; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
   (* neg, sub *)
   - destruct v0...
   - apply type_sub.
@@ -917,7 +918,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - apply type_addl.
   (* addxl addxlimm *)
   - apply type_addl.
-  - apply type_addl.
+  - destruct v0; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
   (* negl, subl *)
   - destruct v0...
   - apply type_subl.
@@ -1452,8 +1454,7 @@ Proof.
   (* addx, addximm *)
   - apply Val.add_inject; trivial.
     inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto.
-  - apply Val.add_inject; trivial.
-    inv H4; simpl; try destruct (Int.ltu _ _); simpl; auto.
+  - inv H4; simpl; trivial. try destruct (Int.ltu _ _); simpl; auto.
   (* neg, sub *)
   - inv H4; simpl; auto.
   - apply Val.sub_inject; auto.
@@ -1543,8 +1544,7 @@ Proof.
   - apply Val.addl_inject; auto.
     inv H4; simpl; trivial.
     destruct (Int.ltu _ _); simpl; trivial.
-  - apply Val.addl_inject; auto.
-    inv H4; simpl; trivial.
+  - inv H4; simpl; trivial.
     destruct (Int.ltu _ _); simpl; trivial.
   (* negl, subl *)
   - inv H4; simpl; auto.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 27faa33c..00e8a1d8 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -161,8 +161,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ocast16signed, v1 :: nil => sign_ext 16 v1
   | Oadd, v1::v2::nil => add v1 v2
   | Oaddimm n, v1::nil => add v1 (I n)
-  | Oaddx shift, v1::v2::nil => add (shl v1 (I (int_of_shift1_4 shift))) v2
-  | Oaddximm shift n, v1::nil => add (shl v1 (I (int_of_shift1_4 shift))) (I n)
+  | Oaddx shift, v1::v2::nil => add v2 (shl v1 (I (int_of_shift1_4 shift)))
+  | Oaddximm shift n, v1::nil => add (I n) (shl v1 (I (int_of_shift1_4 shift)))
   | Oneg, v1::nil => neg v1
   | Osub, v1::v2::nil => sub v1 v2
   | Orevsubx shift, v1::v2::nil => sub v2 (shl v1 (I (int_of_shift1_4 shift)))
@@ -212,8 +212,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ocast32unsigned, v1::nil => longofintu v1
   | Oaddl, v1::v2::nil => addl v1 v2
   | Oaddlimm n, v1::nil => addl v1 (L n)
-  | Oaddxl shift, v1::v2::nil => addl (shll v1 (I (int_of_shift1_4 shift))) v2
-  | Oaddxlimm shift n, v1::nil => addl (shll v1 (I (int_of_shift1_4 shift))) (L n)
+  | Oaddxl shift, v1::v2::nil => addl v2 (shll v1 (I (int_of_shift1_4 shift)))
+  | Oaddxlimm shift n, v1::nil => addl (L n) (shll v1 (I (int_of_shift1_4 shift))) 
   | Onegl, v1::nil => negl v1
   | Osubl, v1::v2::nil => subl v1 v2
   | Orevsubxl shift, v1::v2::nil => subl v2 (shll v1 (I (int_of_shift1_4 shift)))
@@ -378,20 +378,41 @@ Proof.
   - 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
+    | 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)))).
+    + eauto with va.
+    + destruct a1; destruct shift; reflexivity.
   - (*revsubimm*) inv H1; constructor.
   - replace (match Val.shl a1 (Vint (int_of_shift1_4 shift)) with
     | Vint n2 => Vint (Int.sub n n2)
     | _ => Vundef
              end) with (Val.sub (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))).
-    eauto with va.
-    destruct a1; destruct shift; reflexivity.
+    + eauto with va.
+    + destruct a1; destruct shift; reflexivity.
+  - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
+    | Vlong n2 => Vlong (Int64.add n n2)
+    | Vptr b2 ofs2 =>
+        if Archi.ptr64
+        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)))).
+    + eauto with va.
+    + destruct a1; destruct shift; reflexivity.
   - inv H1; constructor.
   - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
     | Vlong n2 => Vlong (Int64.sub n n2)
     | _ => Vundef
              end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
-    eauto with va.
-    destruct a1; destruct shift; reflexivity.
+    + eauto with va.
+    + destruct a1; destruct shift; reflexivity.
   - apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
   (* select *)
   - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption).