maddl / maddlim are synthesized (but not for pointers it seems)

5 files changed, 34 insertions, 6 deletions

diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index 9f0f6a4d..25048809 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/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/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;
 }