diff options
-rw-r--r-- | mppa_k1c/Asm.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 2 | ||||
-rw-r--r-- | mppa_k1c/NeedOp.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Op.v | 9 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 6 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 | ||||
-rw-r--r-- | mppa_k1c/ValueAOp.v | 1 | ||||
-rw-r--r-- | test/monniaux/madd/madd.c | 4 |
9 files changed, 32 insertions, 4 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 1a57e554..0ca554ab 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -177,6 +177,7 @@ Inductive instruction : Type := | Pcompiw (it: itest) (rd rs: ireg) (imm: int) (**r comparison imm word *)
| Paddiw (rd rs: ireg) (imm: int) (**r add imm word *)
+ | Pmuliw (rd rs: ireg) (imm: int) (**r mul imm word *)
| Pandiw (rd rs: ireg) (imm: int) (**r and imm word *)
| Pnandiw (rd rs: ireg) (imm: int) (**r nand imm word *)
| Poriw (rd rs: ireg) (imm: int) (**r or imm word *)
@@ -197,6 +198,7 @@ Inductive instruction : Type := (** Arith RRI64 *)
| Pcompil (it: itest) (rd rs: ireg) (imm: int64) (**r comparison imm long *)
| Paddil (rd rs: ireg) (imm: int64) (**r add immediate long *)
+ | Pmulil (rd rs: ireg) (imm: int64) (**r add immediate long *)
| Pandil (rd rs: ireg) (imm: int64) (**r and immediate long *)
| Pnandil (rd rs: ireg) (imm: int64) (**r and immediate long *)
| Poril (rd rs: ireg) (imm: int64) (**r or immediate long *)
@@ -319,6 +321,7 @@ Definition basic_to_instruction (b: basic) := (* RRI32 *)
| PArithRRI32 (Asmblock.Pcompiw it) rd rs imm => Pcompiw it rd rs imm
| PArithRRI32 Asmblock.Paddiw rd rs imm => Paddiw rd rs imm
+ | PArithRRI32 Asmblock.Pmuliw rd rs imm => Pmuliw rd rs imm
| PArithRRI32 Asmblock.Pandiw rd rs imm => Pandiw rd rs imm
| PArithRRI32 Asmblock.Pnandiw rd rs imm => Pnandiw rd rs imm
| PArithRRI32 Asmblock.Poriw rd rs imm => Poriw rd rs imm
@@ -338,6 +341,7 @@ Definition basic_to_instruction (b: basic) := (* RRI64 *)
| PArithRRI64 (Asmblock.Pcompil it) rd rs imm => Pcompil it rd rs imm
| PArithRRI64 Asmblock.Paddil rd rs imm => Paddil rd rs imm
+ | PArithRRI64 Asmblock.Pmulil rd rs imm => Pmulil rd rs imm
| PArithRRI64 Asmblock.Pandil rd rs imm => Pandil rd rs imm
| PArithRRI64 Asmblock.Pnandil rd rs imm => Pnandil rd rs imm
| PArithRRI64 Asmblock.Poril rd rs imm => Poril rd rs imm
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index b3e1532d..386106d6 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -376,6 +376,7 @@ Inductive arith_name_rri32 : Type := | Pcompiw (it: itest) (**r comparison imm word *) | Paddiw (**r add imm word *) + | Pmuliw (**r add imm word *) | Pandiw (**r and imm word *) | Pnandiw (**r nand imm word *) | Poriw (**r or imm word *) @@ -396,6 +397,7 @@ Inductive arith_name_rri32 : Type := Inductive arith_name_rri64 : Type := | Pcompil (it: itest) (**r comparison imm long *) | Paddil (**r add immediate long *) + | Pmulil (**r mul immediate long *) | Pandil (**r and immediate long *) | Pnandil (**r nand immediate long *) | Poril (**r or immediate long *) @@ -1168,6 +1170,7 @@ Definition arith_eval_rri32 n v i := match n with | Pcompiw c => compare_int c v (Vint i) | Paddiw => Val.add v (Vint i) + | Pmuliw => Val.mul v (Vint i) | Pandiw => Val.and v (Vint i) | Pnandiw => Val.notint (Val.and v (Vint i)) | Poriw => Val.or v (Vint i) @@ -1189,6 +1192,7 @@ Definition arith_eval_rri64 n v i := match n with | Pcompil c => compare_long c v (Vlong i) | Paddil => Val.addl v (Vlong i) + | Pmulil => Val.mull v (Vlong i) | Pandil => Val.andl v (Vlong i) | Pnandil => Val.notl (Val.andl v (Vlong i)) | Poril => Val.orl v (Vlong i) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index e05f92a7..f50b7d4a 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1382,6 +1382,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := match n with Pcompiw _ => "Pcompiw" | Paddiw => "Paddiw" + | Pmuliw => "Pmuliw" | Pandiw => "Pandiw" | Pnandiw => "Pnandiw" | Poriw => "Poriw" @@ -1403,6 +1404,7 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := match n with Pcompil _ => "Pcompil" | Paddil => "Paddil" + | Pmulil => "Pmulil" | Pandil => "Pandil" | Pnandil => "Pnandil" | Poril => "Poril" diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 801a520e..c7b59a34 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -45,6 +45,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oneg => op1 (modarith nv) | Osub => op2 (default nv) | Omul => op2 (modarith nv) + | Omulimm _ => op1 (modarith nv) | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv) | Oand => op2 (bitwise nv) | Oandimm n => op1 (andimm nv n) @@ -171,6 +172,7 @@ Proof. - apply add_sound; auto with na. - apply neg_sound; auto. - apply mul_sound; auto. +- apply mul_sound; auto with na. - apply and_sound; auto. - apply andimm_sound; auto. - apply notint_sound; apply and_sound; auto. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index c56a9649..04081158 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -70,6 +70,7 @@ Inductive operation : Type := | Oneg (**r [rd = - r1] *) | Osub (**r [rd = r1 - r2] *) | Omul (**r [rd = r1 * r2] *) + | Omulimm (n: int) (**r [rd = r1 * n] *) | Omulhs (**r [rd = high part of r1 * r2, signed] *) | Omulhu (**r [rd = high part of r1 * r2, unsigned] *) | Odiv (**r [rd = r1 / r2] (signed) *) @@ -268,6 +269,7 @@ Definition eval_operation | Oneg, v1 :: nil => Some (Val.neg v1) | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2) | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2) + | Omulimm n, v1 :: nil => Some (Val.mul v1 (Vint n)) | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2) | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2) | Odiv, v1 :: v2 :: nil => Val.divs v1 v2 @@ -456,6 +458,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oneg => (Tint :: nil, Tint) | Osub => (Tint :: Tint :: nil, Tint) | Omul => (Tint :: Tint :: nil, Tint) + | Omulimm _ => (Tint :: nil, Tint) | Omulhs => (Tint :: Tint :: nil, Tint) | Omulhu => (Tint :: Tint :: nil, Tint) | Odiv => (Tint :: Tint :: nil, Tint) @@ -623,8 +626,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* neg, sub *) - destruct v0... - unfold Val.sub. destruct v0; destruct v1... - (* mul, mulhs, mulhu *) + (* mul, mulimm, mulhs, mulhu *) - destruct v0; destruct v1... + - destruct v0... - destruct v0; destruct v1... - destruct v0; destruct v1... (* div, divu *) @@ -1124,8 +1128,9 @@ Proof. (* neg, sub *) - inv H4; simpl; auto. - apply Val.sub_inject; auto. - (* mul, mulhs, mulhu *) + (* mul, mulimm, mulhs, mulhu *) - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. - inv H4; inv H2; simpl; auto. - inv H4; inv H2; simpl; auto. (* div, divu *) diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index f7702a9d..e1948a03 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -95,6 +95,7 @@ let arith_rrr_str = function let arith_rri32_str = function | Pcompiw it -> "Pcompiw" | Paddiw -> "Paddiw" + | Pmuliw -> "Pmuliw" | Pandiw -> "Pandiw" | Pnandiw -> "Pnandiw" | Poriw -> "Poriw" @@ -114,6 +115,7 @@ let arith_rri32_str = function let arith_rri64_str = function | Pcompil it -> "Pcompil" | Paddil -> "Paddil" + | Pmulil -> "Pmulil" | Pandil -> "Pandil" | Pnandil -> "Pnandil" | Poril -> "Poril" @@ -437,8 +439,8 @@ let ab_inst_to_real = function | "Pcompl" | "Pcompil" -> Compd | "Pfcompw" -> Fcompw | "Pfcompl" -> Fcompd - | "Pmulw" -> Mulw - | "Pmull" -> Muld + | "Pmulw" | "Pmuliw" -> Mulw + | "Pmull" | "Pmulil" -> Muld | "Porw" | "Poriw" -> Orw | "Pnorw" | "Pnoriw" -> Norw | "Porl" | "Poril" -> Ord diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 5c5d6c79..69824852 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -442,6 +442,8 @@ module Target (*: TARGET*) = fprintf oc " compw.%a %a = %a, %a\n" icond it ireg rd ireg rs coqint imm | Paddiw (rd, rs, imm) -> fprintf oc " addw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Pmuliw (rd, rs, imm) -> + fprintf oc " mulw %a = %a, %a\n" ireg rd ireg rs coqint imm | Pandiw (rd, rs, imm) -> fprintf oc " andw %a = %a, %a\n" ireg rd ireg rs coqint imm | Pnandiw (rd, rs, imm) -> @@ -481,6 +483,8 @@ module Target (*: TARGET*) = fprintf oc " compd.%a %a = %a, %a\n" icond it ireg rd ireg rs coqint64 imm | Paddil (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pmulil (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " muld %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pandil (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " andd %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pnandil (rd, rs, imm) -> assert Archi.ptr64; diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index a92358ca..3bb25807 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -57,6 +57,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oneg, v1::nil => neg v1 | Osub, v1::v2::nil => sub v1 v2 | Omul, v1::v2::nil => mul v1 v2 + | Omulimm n, v1::nil => mul v1 (I n) | Omulhs, v1::v2::nil => mulhs v1 v2 | Omulhu, v1::v2::nil => mulhu v1 v2 | Odiv, v1::v2::nil => divs v1 v2 diff --git a/test/monniaux/madd/madd.c b/test/monniaux/madd/madd.c index e1e5eeb7..f847edf3 100644 --- a/test/monniaux/madd/madd.c +++ b/test/monniaux/madd/madd.c @@ -2,6 +2,10 @@ unsigned madd(unsigned a, unsigned b, unsigned c) { return a + b*c; } +unsigned maddimm(unsigned a, unsigned b) { + return a + b*17113; +} + unsigned madd2(unsigned a, unsigned b, unsigned c) { return c + b*a; } |