diff options
| -rw-r--r-- | backend/SelectDiv.vp | 6 | ||||
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 4 |
2 files changed, 7 insertions, 3 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 6ddcd6ac..662162e8 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -309,20 +309,20 @@ Definition modls (e1 e2: expr) := end | _, _ => modls_base e1 e2 end. - + (** Floating-point division by a constant can also be turned into a FP multiplication by the inverse constant, but only for powers of 2. *) Definition divfimm (e: expr) (n: float) := match Float.exact_inverse n with | Some n' => Eop Omulf (e ::: Eop (Ofloatconst n') Enil ::: Enil) - | None => Eop Odivf (e ::: Eop (Ofloatconst n) Enil ::: Enil) + | None => divfbase e (Eop (Ofloatconst n) Enil) end. Nondetfunction divf (e1: expr) (e2: expr) := match e2 with | Eop (Ofloatconst n2) Enil => divfimm e1 n2 - | _ => Eop Odivf (e1 ::: e2 ::: Enil) + | _ => divfbase e1 e2 end. Definition divfsimm (e: expr) (n: float32) := diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index b2ce1fef..80eb641c 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -535,4 +535,8 @@ Nondetfunction builtin_arg (e: expr) := | _ => BA e end. +(* float division *) + +Definition divfbase (e1: expr) (e2: expr) := + Eop Odivf (e1 ::: e2 ::: Enil). End SELECT. |