diff options
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
-rw-r--r-- | mppa_k1c/SelectOp.vp | 41 |
1 files changed, 39 insertions, 2 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 3df0c682..ec3985c5 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -51,9 +51,10 @@ Require Import Floats. Require Import Op. Require Import CminorSel. Require Import OpHelpers. -Require Import ExtValues. +Require Import ExtValues ExtFloats. Require Import DecBoolOps. Require Import Chunks. +Require Import Builtins. Require Compopts. Local Open Scope cminorsel_scope. @@ -668,9 +669,45 @@ Definition divf_base (e1: expr) (e2: expr) := (* Eop Odivf (e1 ::: e2 ::: Enil). *) Eexternal f64_div sig_ff_f (e1 ::: e2 ::: Enil). -Definition divfs_base (e1: expr) (e2: expr) := +Definition divfs_base1 (e2 : expr) := + Eop Oinvfs (e2 ::: Enil). +Definition divfs_baseX (e1 : expr) (e2 : expr) := (* Eop Odivf (e1 ::: e2 ::: Enil). *) Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil). + +Nondetfunction divfs_base (e1: expr) := + match e1 with + | Eop (Osingleconst f) Enil => + (if Float32.eq_dec f ExtFloat32.one + then divfs_base1 + else divfs_baseX e1) + | _ => divfs_baseX e1 + end. + +Nondetfunction gen_fma args := + match args with + | (Eop Onegf (e1:::Enil)):::e2:::e3:::Enil => Some (Eop Ofmsubf (e3:::e1:::e2:::Enil)) + | e1:::e2:::e3:::Enil => Some (Eop Ofmaddf (e3:::e1:::e2:::Enil)) + | _ => None + end. + +Nondetfunction gen_fmaf args := + match args with + | (Eop Onegfs (e1:::Enil)):::e2:::e3:::Enil => Some (Eop Ofmsubfs (e3:::e1:::e2:::Enil)) + | e1:::e2:::e3:::Enil => Some (Eop Ofmaddfs (e3:::e1:::e2:::Enil)) + | _ => None + end. + +Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := + match b with + | BI_fmin => Some (Eop Ominf args) + | BI_fmax => Some (Eop Omaxf args) + | BI_fminf => Some (Eop Ominfs args) + | BI_fmaxf => Some (Eop Omaxfs args) + | BI_fabsf => Some (Eop Oabsfs args) + | BI_fma => gen_fma args + | BI_fmaf => gen_fmaf args + end. End SELECT. (* Local Variables: *) |