diff options
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index ec3985c5..0974f872 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -168,13 +168,21 @@ Nondetfunction add (e1: expr) (e2: expr) := | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) | t1, (Eop Omul (t2:::t3:::Enil)) => - Eop Omadd (t1:::t2:::t3:::Enil) + if Compopts.optim_madd tt + then Eop Omadd (t1:::t2:::t3:::Enil) + else Eop Oadd (e1:::e2:::Enil) | (Eop Omul (t2:::t3:::Enil)), t1 => - Eop Omadd (t1:::t2:::t3:::Enil) + if Compopts.optim_madd tt + then Eop Omadd (t1:::t2:::t3:::Enil) + else Eop Oadd (e1:::e2:::Enil) | t1, (Eop (Omulimm n) (t2:::Enil)) => - Eop (Omaddimm n) (t1:::t2:::Enil) + if Compopts.optim_madd tt + then Eop (Omaddimm n) (t1:::t2:::Enil) + else Eop Oadd (e1:::e2:::Enil) | (Eop (Omulimm n) (t2:::Enil)), t1 => - Eop (Omaddimm n) (t1:::t2:::Enil) + if Compopts.optim_madd tt + then Eop (Omaddimm n) (t1:::t2:::Enil) + else Eop Oadd (e1:::e2:::Enil) | (Eop (Oshlimm n) (t1:::Enil)), t2 => add_shlimm n t1 t2 | t2, (Eop (Oshlimm n) (t1:::Enil)) => @@ -197,7 +205,9 @@ Nondetfunction sub (e1: expr) (e2: expr) := | t1, (Eop Omul (t2:::t3:::Enil)) => Eop Omsub (t1:::t2:::t3:::Enil) | t1, (Eop (Omulimm n) (t2:::Enil)) => - Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil) + if Compopts.optim_madd tt + then Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil) + else Eop Osub (e1:::e2:::Enil) | _, _ => Eop Osub (e1:::e2:::Enil) end. @@ -712,4 +722,4 @@ End SELECT. (* Local Variables: *) (* mode: coq *) -(* End: *)
\ No newline at end of file +(* End: *) |