Merge branch 'mppa-madd' into mppa_postpass

9 files changed, 86 insertions, 25 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 312d2386..5b00a64f 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -639,7 +639,6 @@ Definition transl_op
           Psrlil RTMP RTMP (Int.sub Int64.iwordsize' n) ::i
           Paddl RTMP rs RTMP ::i
           Psrail rd RTMP n ::i k)
-         (* FIXME
   | Omaddl, a1 :: a2 :: a3 :: nil =>
     assertion (mreg_eq a1 res);
       do r1 <- ireg_of a1;
@@ -651,7 +650,6 @@ Definition transl_op
       do r1 <- ireg_of a1;
       do r2 <- ireg_of a2;
         OK (Pmaddil r1 r2 n ::i k)
-*)
   | Oabsf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
       OK (Pfabsd rd rs ::i k)
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index ef0f97a9..4de37af4 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -210,7 +210,7 @@ Global Opaque
 
 Definition two_address_op (op: operation) : bool :=
   match op with
-  | Ocast32unsigned | Omadd | Omaddimm _ => true
+  | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ => true
   | _ => false
   end.
 
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 68f43894..2577370c 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -105,6 +105,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oshrlimm n => op1 (default nv)
   | Oshrluimm n => op1 (default nv)
   | Oshrxlimm n => op1 (default nv)
+  | Omaddl => op3 (default nv)
+  | Omaddlimm n => op2 (default nv)
   | Onegf | Oabsf => op1 (default nv)
   | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
   | Onegfs | Oabsfs => op1 (default nv)
@@ -156,6 +158,39 @@ Proof.
   eapply default_needs_of_condition_sound; eauto.
 Qed.
 
+Lemma addl_sound:
+  forall v1 w1 v2 w2 x,
+  vagree v1 w1 (default x) -> vagree v2 w2 (default x) ->
+  vagree (Val.addl v1 v2) (Val.addl w1 w2) x.
+Proof.
+  unfold default; intros.
+  destruct x; simpl in *; trivial.
+  - unfold Val.addl.
+    destruct v1; destruct v2; trivial; destruct Archi.ptr64; trivial.
+  - apply Val.addl_lessdef; trivial.
+Qed.
+
+
+Lemma mull_sound:
+  forall v1 w1 v2 w2 x,
+  vagree v1 w1 (default x) -> vagree v2 w2 (default x) ->
+  vagree (Val.mull v1 v2) (Val.mull w1 w2) x.
+Proof.
+  unfold default; intros.
+  destruct x; simpl in *; trivial.
+  - unfold Val.mull.
+    destruct v1; destruct v2; trivial.
+  - unfold Val.mull.
+    destruct v1; destruct v2; trivial.
+    inv H. inv H0.
+    trivial.
+Qed.
+
+Remark default_idem: forall nv, default (default nv) = default nv.
+Proof.
+  destruct nv; simpl; trivial.
+Qed.
+
 Lemma needs_of_operation_sound:
   forall op args v nv args',
   eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v ->
@@ -198,6 +233,11 @@ Proof.
   (* madd *)
 - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption.
 - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption.
+  (* maddl *)
+- apply addl_sound; trivial.
+  apply mull_sound; trivial.
+  rewrite default_idem; trivial.
+  rewrite default_idem; trivial.
 Qed.
 
 Lemma operation_is_redundant_sound:
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 0e9a7af9..c4338857 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -146,10 +146,8 @@ Inductive operation : Type :=
   | Oshrlu                   (**r [rd = r1 >> r2] (unsigned) *)
   | Oshrluimm (n: int)       (**r [rd = r1 >> n] (unsigned) *)
   | Oshrxlimm (n: int)       (**r [rd = r1 / 2^n] (signed) *)
-              (* FIXME
   | Omaddl                   (**r [rd = rd + r1 * r2] *)
   | Omaddlimm (n: int64)     (**r [rd = rd + r1 * imm] *)
-*)
 (*c Floating-point arithmetic: *)
   | Onegf                    (**r [rd = - r1] *)
   | Oabsf                    (**r [rd = abs(r1)] *)
@@ -346,11 +344,8 @@ Definition eval_operation
   | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2)
   | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n))
   | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n)
-
-                                      (*
   | Omaddl, v1::v2::v3::nil => Some (Val.addl v1 (Val.mull v2 v3))
   | (Omaddlimm n), v1::v2::nil => Some (Val.addl v1 (Val.mull v2 (Vlong n)))
-                                       *)
                                       
   | Onegf, v1::nil => Some (Val.negf v1)
   | Oabsf, v1::nil => Some (Val.absf v1)
@@ -536,10 +531,9 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oshrlu => (Tlong :: Tint :: nil, Tlong)
   | Oshrluimm _ => (Tlong :: nil, Tlong)
   | Oshrxlimm _ => (Tlong :: nil, Tlong)
-                     (* FIXME
   | Omaddl => (Tlong :: Tlong :: Tlong :: nil, Tlong)
   | Omaddlimm _ => (Tlong :: Tlong :: nil, Tlong)
-*)
+
   | Onegf => (Tfloat :: nil, Tfloat)
   | Oabsf => (Tfloat :: nil, Tfloat)
   | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat)
@@ -753,10 +747,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
   (* shrxl *)
   - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0...
-    (* FIXME
   (* maddl, maddlim *)
-  - destruct v0; destruct v1; destruct v2...
-  - destruct v0; destruct v1... *)
+  - destruct v0; destruct v1; destruct v2; simpl; trivial.
+    destruct Archi.ptr64; simpl; trivial.
+  - destruct v0; destruct v1; simpl; trivial.
+    destruct Archi.ptr64; simpl; trivial.
   (* negf, absf *)
   - destruct v0...
   - destruct v0...
@@ -1265,13 +1260,11 @@ Proof.
   - inv H4; simpl in H1; try discriminate. simpl.
     destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists.
 
-  (*
-  (* maddl, maddlim *)
-  - inv H2; inv H3; inv H4; simpl; auto; simpl.
-    destruct Archi.ptr64; trivial.
-    s
-  - inv H2; inv H4; simpl; auto.
-   *)
+  (* maddl, maddlimm *)
+  - apply Val.addl_inject; auto.
+    inv H2; inv H3; inv H4; simpl; auto.
+  - apply Val.addl_inject; auto.
+    inv H4; inv H2; simpl; auto.
     
   (* negf, absf *)
   - inv H4; simpl; auto.
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 07ebf1a2..3a17ab17 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -88,6 +88,14 @@ Nondetfunction addl (e1: expr) (e2: expr) :=
       addlimm n1 (Eop Oaddl (t1:::t2:::Enil))
   | t1, Eop (Oaddlimm n2) (t2:::Enil) =>
       addlimm n2 (Eop Oaddl (t1:::t2:::Enil))
+  | t1, (Eop Omull (t2:::t3:::Enil)) =>
+      Eop Omaddl (t1:::t2:::t3:::Enil)
+  | (Eop Omull (t2:::t3:::Enil)), t1 =>
+      Eop Omaddl (t1:::t2:::t3:::Enil)
+  | t1, (Eop (Omullimm n) (t2:::Enil)) =>
+      Eop (Omaddlimm n) (t1:::t2:::Enil)
+  | (Eop (Omullimm n) (t2:::Enil)), t1 =>
+      Eop (Omaddlimm n) (t1:::t2:::Enil)
   | _, _ => Eop Oaddl (e1:::e2:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 27681875..4723278a 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -185,6 +185,10 @@ Proof.
        with (Val.addl (Val.addl x v1) (Vlong n2)).
     apply eval_addlimm. EvalOp.
     repeat rewrite Val.addl_assoc. reflexivity.
+  - subst. TrivialExists.
+  - subst. rewrite Val.addl_commut. TrivialExists.
+  - subst. TrivialExists.
+  - subst. rewrite Val.addl_commut. TrivialExists.
   - TrivialExists.
 Qed.
 
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index b43c4d78..fb1977ea 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -132,6 +132,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Oshrlu, v1::v2::nil => shrlu v1 v2
   | Oshrluimm n, v1::nil => shrlu v1 (I n)
   | Oshrxlimm n, v1::nil => shrxl v1 (I n)
+  | Omaddl, v1::v2::v3::nil => addl v1 (mull v2 v3)
+  | Omaddlimm n, v1::v2::nil => addl v1 (mull v2 (L n))
   | Onegf, v1::nil => negf v1
   | Oabsf, v1::nil => absf v1
   | Oaddf, v1::v2::nil => addf v1 v2
diff --git a/test/monniaux/madd/madd.c b/test/monniaux/madd/madd.c
index f847edf3..68f348ad 100644
--- a/test/monniaux/madd/madd.c
+++ b/test/monniaux/madd/madd.c
@@ -1,11 +1,25 @@
-unsigned madd(unsigned a, unsigned b, unsigned c) {
+#include <stdint.h>
+
+uint32_t madd(uint32_t a, uint32_t b, uint32_t c) {
+  return a + b*c;
+}
+
+uint32_t maddimm(uint32_t a, uint32_t b) {
+  return a + b*17113;
+}
+
+uint32_t madd2(uint32_t a, uint32_t b, uint32_t c) {
+  return c + b*a;
+}
+
+uint64_t maddl(uint64_t a, uint64_t b, uint64_t c) {
   return a + b*c;
 }
 
-unsigned maddimm(unsigned a, unsigned b) {
+uint64_t maddlimm(uint64_t a, uint64_t b) {
   return a + b*17113;
 }
 
-unsigned madd2(unsigned a, unsigned b, unsigned c) {
+uint64_t maddl2(uint64_t a, uint64_t b, uint64_t c) {
   return c + b*a;
 }
diff --git a/test/monniaux/madd/madd_run.c b/test/monniaux/madd/madd_run.c
index d4238c53..28cdf9b3 100644
--- a/test/monniaux/madd/madd_run.c
+++ b/test/monniaux/madd/madd_run.c
@@ -1,9 +1,11 @@
 #include <stdio.h>
+#include <stdint.h>
 
-extern unsigned madd(unsigned a, unsigned b, unsigned c);
+extern uint32_t madd(uint32_t a, uint32_t b, uint32_t c);
+extern uint64_t maddl(uint64_t a, uint64_t b, uint64_t c);
 
 int main() {
   unsigned a = 7, b = 3, c = 4;
-  printf("res = %u\n", madd(a, b, c));
+  printf("res = %u %lu\n", madd(a, b, c), maddl(a, b, c));
   return 0;
 }