diff options
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 19 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 2 | ||||
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 4 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 6 |
4 files changed, 28 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index ba01883d..80b712e3 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -524,6 +524,11 @@ Definition transl_op do r2 <- ireg_of a2; do r3 <- ireg_of a3; OK (Pmaddw r1 r2 r3 ::i k) + | Omaddimm n, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + OK (Pmaddiw r1 r2 n ::i k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -636,7 +641,19 @@ 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; + do r2 <- ireg_of a2; + do r3 <- ireg_of a3; + OK (Pmaddl r1 r2 r3 ::i k) + | Omaddlimm n, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + 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) diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index e1948a03..f4732ee4 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -453,7 +453,7 @@ let ab_inst_to_real = function | "Psrll" | "Psrlil" -> Srld | "Psllw" | "Pslliw" -> Sllw | "Proriw" -> Rorw - | "Pmaddw" -> Maddw + | "Pmaddw" | "Pmaddiw" -> Maddw | "Pslll" | "Psllil" -> Slld | "Pxorw" | "Pxoriw" -> Xorw | "Pnxorw" | "Pnxoriw" -> Nxorw diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index d87c837e..e4d65ced 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -90,6 +90,10 @@ Nondetfunction add (e1: expr) (e2: expr) := Eop Omadd (t1:::t2:::t3:::Enil) | (Eop Omul (t2:::t3:::Enil)), t1 => Eop Omadd (t1:::t2:::t3:::Enil) + | t1, (Eop (Omulimm n) (t2:::Enil)) => + Eop (Omaddimm n) (t1:::t2:::Enil) + | (Eop (Omulimm n) (t2:::Enil)), t1 => + Eop (Omaddimm n) (t1:::t2:::Enil) | _, _ => Eop Oadd (e1:::e2:::Enil) end. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index a8889430..94d162a2 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -184,7 +184,11 @@ Proof. repeat rewrite Val.add_assoc. reflexivity. - (* Omadd *) subst. TrivialExists. - - (* Omadd *) + - (* Omadd rev *) + subst. rewrite Val.add_commut. TrivialExists. + - (* Omaddimm *) + subst. TrivialExists. + - (* Omaddimm rev *) subst. rewrite Val.add_commut. TrivialExists. - TrivialExists. Qed. |