From 9adb576998f3b2017db5c062b459449e1721579a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 19 Mar 2019 21:31:20 +0100 Subject: mul immediate --- mppa_k1c/Asmblockgen.v | 8 ++++++++ mppa_k1c/NeedOp.v | 1 + mppa_k1c/Op.v | 5 +++++ mppa_k1c/SelectOp.vp | 2 +- mppa_k1c/SelectOpproof.v | 4 ++-- mppa_k1c/ValueAOp.v | 1 + 6 files changed, 18 insertions(+), 3 deletions(-) diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 1646ff94..ba01883d 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -85,6 +85,7 @@ Definition opimm32 (op: arith_name_rrr) end. Definition addimm32 := opimm32 Paddw Paddiw. +Definition mulimm32 := opimm32 Pmulw Pmuliw. Definition andimm32 := opimm32 Pandw Pandiw. Definition nandimm32 := opimm32 Pnandw Pnandiw. Definition orimm32 := opimm32 Porw Poriw. @@ -109,6 +110,7 @@ Definition opimm64 (op: arith_name_rrr) end. Definition addimm64 := opimm64 Paddl Paddil. +Definition mulimm64 := opimm64 Pmull Pmulil. Definition orimm64 := opimm64 Porl Poril. Definition andimm64 := opimm64 Pandl Pandil. Definition xorimm64 := opimm64 Pxorl Pxoril. @@ -420,6 +422,9 @@ Definition transl_op | Omul, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmulw rd rs1 rs2 ::i k) + | Omulimm n, a1 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; + OK (mulimm32 rd rs1 n ::i k) | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") (* Normalement pas émis *) | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") (* Normalement pas émis *) | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.") @@ -546,6 +551,9 @@ Definition transl_op | Omull, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmull rd rs1 rs2 ::i k) + | Omullimm n, a1 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; + OK (mulimm64 rd rs1 n ::i k) | Omullhs, _ => Error (msg "Asmblockgen.transl_op: Omullhs") (* Normalement pas émis *) | Omullhu, _ => Error (msg "Asmblockgen.transl_op: Omullhu") (* Normalement pas émis *) | Odivl, _ => Error (msg "Asmblockgen.transl_op: Odivl") (* Géré par fonction externe *) diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index c7b59a34..68f43894 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -81,6 +81,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Onegl => op1 (default nv) | Osubl => op2 (default nv) | Omull => op2 (default nv) + | Omullimm _ => op1 (default nv) | Omullhs | Omullhu | Odivl | Odivlu | Omodl | Omodlu => op2 (default nv) | Oandl => op2 (default nv) | Oandlimm n => op1 (default nv) diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 04081158..0e9a7af9 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -115,6 +115,7 @@ Inductive operation : Type := | Onegl (**r [rd = - r1] *) | Osubl (**r [rd = r1 - r2] *) | Omull (**r [rd = r1 * r2] *) + | Omullimm (n: int64) (**r [rd = r1 * n] *) | Omullhs (**r [rd = high part of r1 * r2, signed] *) | Omullhu (**r [rd = high part of r1 * r2, unsigned] *) | Odivl (**r [rd = r1 / r2] (signed) *) @@ -314,6 +315,7 @@ Definition eval_operation | Onegl, v1::nil => Some (Val.negl v1) | Osubl, v1::v2::nil => Some (Val.subl v1 v2) | Omull, v1::v2::nil => Some (Val.mull v1 v2) + | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n)) | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2) | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2) | Odivl, v1::v2::nil => Val.divls v1 v2 @@ -503,6 +505,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Onegl => (Tlong :: nil, Tlong) | Osubl => (Tlong :: Tlong :: nil, Tlong) | Omull => (Tlong :: Tlong :: nil, Tlong) + | Omullimm _ => (Tlong :: nil, Tlong) | Omullhs => (Tlong :: Tlong :: nil, Tlong) | Omullhu => (Tlong :: Tlong :: nil, Tlong) | Odivl => (Tlong :: Tlong :: nil, Tlong) @@ -700,6 +703,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). destruct (eq_block b b0)... (* mull, mullhs, mullhu *) - destruct v0; destruct v1... + - destruct v0... - destruct v0; destruct v1... - destruct v0; destruct v1... (* divl, divlu *) @@ -1205,6 +1209,7 @@ Proof. - apply Val.subl_inject; auto. (* mull, mullhs, mullhu *) - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. - inv H4; inv H2; simpl; auto. - inv H4; inv H2; simpl; auto. (* divl, divlu *) diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 22211167..d87c837e 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -173,7 +173,7 @@ Definition mulimm_base (n1: int) (e2: expr) := | i :: j :: nil => Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) | _ => - Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil) + Eop (Omulimm n1) (e2 ::: Enil) end. Nondetfunction mulimm (n1: int) (e2: expr) := diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index fe678383..a8889430 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -301,7 +301,7 @@ Proof. generalize (Int.one_bits_decomp n). generalize (Int.one_bits_range n). destruct (Int.one_bits n). - - intros. auto. + - intros. TrivialExists. - destruct l. + intros. rewrite H1. simpl. rewrite Int.add_zero. @@ -319,7 +319,7 @@ Proof. rewrite Val.mul_add_distr_r. repeat rewrite Val.shl_mul. eapply Val.lessdef_trans. 2: eauto. apply Val.add_lessdef; auto. simpl. repeat rewrite H0; auto with coqlib. - intros. auto. + intros. TrivialExists. Qed. Theorem eval_mulimm: diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 3bb25807..b43c4d78 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -101,6 +101,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Onegl, v1::nil => negl v1 | Osubl, v1::v2::nil => subl v1 v2 | Omull, v1::v2::nil => mull v1 v2 + | Omullimm n, v1::nil => mull v1 (L n) | Omullhs, v1::v2::nil => mullhs v1 v2 | Omullhu, v1::v2::nil => mullhu v1 v2 | Odivl, v1::v2::nil => divls v1 v2 -- cgit