From 947a61ee5d1f972054157b66a094d6a356a91654 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 20 Mar 2019 09:29:52 +0100 Subject: maddl declared --- mppa_k1c/NeedOp.v | 40 ++++++++++++++++++++++++++++++++++++++++ mppa_k1c/Op.v | 27 ++++++++++----------------- mppa_k1c/ValueAOp.v | 2 ++ 3 files changed, 52 insertions(+), 17 deletions(-) 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/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 -- cgit From 5487cf64164eeea716e3ad140977aa73ccbe00ce Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 20 Mar 2019 09:35:06 +0100 Subject: maddl gets to assembly --- mppa_k1c/Asmblockgen.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 80b712e3..b4532dc4 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -641,7 +641,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; @@ -653,7 +652,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) -- cgit From a0c25ff1259a8373fb71e780f70d28916c321612 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 20 Mar 2019 09:49:45 +0100 Subject: maddl / maddlim are synthesized (but not for pointers it seems) --- mppa_k1c/Machregs.v | 2 +- mppa_k1c/SelectLong.vp | 8 ++++++++ mppa_k1c/SelectLongproof.v | 4 ++++ test/monniaux/madd/madd.c | 20 +++++++++++++++++--- 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 + +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 +#include -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; } -- cgit