diff options
Diffstat (limited to 'backend/SelectDiv.vp')
| -rw-r--r-- | backend/SelectDiv.vp | 39 |
1 files changed, 18 insertions, 21 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index d91797c5..9f852616 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -15,10 +15,13 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. -Require Import Op CminorSel SelectOp SplitLong SelectLong. +Require Import Op CminorSel OpHelpers SelectOp SplitLong SelectLong. Local Open Scope cminorsel_scope. +Section SELECT. +Context {hf: helper_functions}. + Definition is_intconst (e: expr) : option int := match e with | Eop (Ointconst n) _ => Some n @@ -221,10 +224,6 @@ Definition mods (e1: expr) (e2: expr) := (** 64-bit integer divisions *) -Section SELECT. - -Context {hf: helper_functions}. - Definition modl_from_divl (equo: expr) (n: int64) := subl (Eletvar O) (mullimm n equo). @@ -241,8 +240,8 @@ Definition divlu (e1 e2: expr) := divlu_base e1 e2 else match divlu_mul_params (Int64.unsigned n2) with - | None => divlu_base e1 e2 - | Some(p, m) => Elet e1 (divlu_mull p m) + | _ => divlu_base e1 e2 + (* | Some(p, m) => Elet e1 (divlu_mull p m) *) (* FIXME - hack K1 *) end end | _, _ => divlu_base e1 e2 @@ -258,8 +257,8 @@ Definition modlu (e1 e2: expr) := modlu_base e1 e2 else match divlu_mul_params (Int64.unsigned n2) with - | None => modlu_base e1 e2 - | Some(p, m) => Elet e1 (modl_from_divl (divlu_mull p m) n2) + | _ => modlu_base e1 e2 + (* | Some(p, m) => Elet e1 (modl_from_divl (divlu_mull p m) n2) *) (* FIXME - hack K1 *) end end | _, _ => modlu_base e1 e2 @@ -285,8 +284,8 @@ Definition divls (e1 e2: expr) := divls_base e1 e2 else match divls_mul_params (Int64.signed n2) with - | None => divls_base e1 e2 - | Some(p, m) => Elet e1 (divls_mull p m) + | _ => divls_base e1 e2 + (* | Some(p, m) => Elet e1 (divls_mull p m) *) (* FIXME - hack K1 *) end end | _, _ => divls_base e1 e2 @@ -304,40 +303,38 @@ Definition modls (e1 e2: expr) := modls_base e1 e2 else match divls_mul_params (Int64.signed n2) with - | None => modls_base e1 e2 - | Some(p, m) => Elet e1 (modl_from_divl (divls_mull p m) n2) + | _ => modls_base e1 e2 + (* | Some(p, m) => Elet e1 (modl_from_divl (divls_mull p m) n2) *) (* FIXME - hack K1 *) end end | _, _ => modls_base e1 e2 end. - -End SELECT. - + (** 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 => divf_base 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) + | _ => divf_base e1 e2 end. Definition divfsimm (e: expr) (n: float32) := match Float32.exact_inverse n with | Some n' => Eop Omulfs (e ::: Eop (Osingleconst n') Enil ::: Enil) - | None => Eop Odivfs (e ::: Eop (Osingleconst n) Enil ::: Enil) + | None => divfs_base e (Eop (Osingleconst n) Enil) end. Nondetfunction divfs (e1: expr) (e2: expr) := match e2 with | Eop (Osingleconst n2) Enil => divfsimm e1 n2 - | _ => Eop Odivfs (e1 ::: e2 ::: Enil) + | _ => divfs_base e1 e2 end. - +End SELECT.
\ No newline at end of file |