diff options
-rw-r--r-- | mppa_k1c/Machregs.v | 2 | ||||
-rw-r--r-- | mppa_k1c/SelectLong.vp | 8 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 4 | ||||
-rw-r--r-- | test/monniaux/madd/madd.c | 20 | ||||
-rw-r--r-- | test/monniaux/madd/madd_run.c | 6 |
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; } |