diff options
Diffstat (limited to 'powerpc/SelectOp.v')
-rw-r--r-- | powerpc/SelectOp.v | 179 |
1 files changed, 33 insertions, 146 deletions
diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v index e6a281b2..c421cdc5 100644 --- a/powerpc/SelectOp.v +++ b/powerpc/SelectOp.v @@ -50,6 +50,14 @@ Require Import CminorSel. Open Local Scope cminorsel_scope. +(** ** Constants **) + +Definition addrsymbol (id: ident) (ofs: int) := + Eop (Oaddrsymbol id ofs) Enil. + +Definition addrstack (ofs: int) := + Eop (Oaddrstack ofs) Enil. + (** ** Integer logical negation *) (** The natural way to write smart constructors is by pattern-matching @@ -846,148 +854,6 @@ Definition subf (e1: expr) (e2: expr) := end else Eop Osubf (e1:::e2:::Enil). -(** ** Truncations and sign extensions *) - -Inductive cast8signed_cases: forall (e1: expr), Type := - | cast8signed_case1: - forall (e2: expr), - cast8signed_cases (Eop Ocast8signed (e2 ::: Enil)) - | cast8signed_case2: - forall mode args, - cast8signed_cases (Eload Mint8signed mode args) - | cast8signed_default: - forall (e1: expr), - cast8signed_cases e1. - -Definition cast8signed_match (e1: expr) := - match e1 as z1 return cast8signed_cases z1 with - | Eop Ocast8signed (e2 ::: Enil) => - cast8signed_case1 e2 - | Eload Mint8signed mode args => - cast8signed_case2 mode args - | e1 => - cast8signed_default e1 - end. - -Definition cast8signed (e: expr) := - match cast8signed_match e with - | cast8signed_case1 e1 => e - | cast8signed_case2 mode args => e - | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil) - end. - -Inductive cast8unsigned_cases: forall (e1: expr), Type := - | cast8unsigned_case1: - forall (e2: expr), - cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil)) - | cast8unsigned_case2: - forall mode args, - cast8unsigned_cases (Eload Mint8unsigned mode args) - | cast8unsigned_default: - forall (e1: expr), - cast8unsigned_cases e1. - -Definition cast8unsigned_match (e1: expr) := - match e1 as z1 return cast8unsigned_cases z1 with - | Eop Ocast8unsigned (e2 ::: Enil) => - cast8unsigned_case1 e2 - | Eload Mint8unsigned mode args => - cast8unsigned_case2 mode args - | e1 => - cast8unsigned_default e1 - end. - -Definition cast8unsigned (e: expr) := - match cast8unsigned_match e with - | cast8unsigned_case1 e1 => e - | cast8unsigned_case2 mode args => e - | cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil) - end. - -Inductive cast16signed_cases: forall (e1: expr), Type := - | cast16signed_case1: - forall (e2: expr), - cast16signed_cases (Eop Ocast16signed (e2 ::: Enil)) - | cast16signed_case2: - forall mode args, - cast16signed_cases (Eload Mint16signed mode args) - | cast16signed_default: - forall (e1: expr), - cast16signed_cases e1. - -Definition cast16signed_match (e1: expr) := - match e1 as z1 return cast16signed_cases z1 with - | Eop Ocast16signed (e2 ::: Enil) => - cast16signed_case1 e2 - | Eload Mint16signed mode args => - cast16signed_case2 mode args - | e1 => - cast16signed_default e1 - end. - -Definition cast16signed (e: expr) := - match cast16signed_match e with - | cast16signed_case1 e1 => e - | cast16signed_case2 mode args => e - | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil) - end. - -Inductive cast16unsigned_cases: forall (e1: expr), Type := - | cast16unsigned_case1: - forall (e2: expr), - cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil)) - | cast16unsigned_case2: - forall mode args, - cast16unsigned_cases (Eload Mint16unsigned mode args) - | cast16unsigned_default: - forall (e1: expr), - cast16unsigned_cases e1. - -Definition cast16unsigned_match (e1: expr) := - match e1 as z1 return cast16unsigned_cases z1 with - | Eop Ocast16unsigned (e2 ::: Enil) => - cast16unsigned_case1 e2 - | Eload Mint16unsigned mode args => - cast16unsigned_case2 mode args - | e1 => - cast16unsigned_default e1 - end. - -Definition cast16unsigned (e: expr) := - match cast16unsigned_match e with - | cast16unsigned_case1 e1 => e - | cast16unsigned_case2 mode args => e - | cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil) - end. - -Inductive singleoffloat_cases: forall (e1: expr), Type := - | singleoffloat_case1: - forall (e2: expr), - singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil)) - | singleoffloat_case2: - forall mode args, - singleoffloat_cases (Eload Mfloat32 mode args) - | singleoffloat_default: - forall (e1: expr), - singleoffloat_cases e1. - -Definition singleoffloat_match (e1: expr) := - match e1 as z1 return singleoffloat_cases z1 with - | Eop Osingleoffloat (e2 ::: Enil) => - singleoffloat_case1 e2 - | Eload Mfloat32 mode args => - singleoffloat_case2 mode args - | e1 => - singleoffloat_default e1 - end. - -Definition singleoffloat (e: expr) := - match singleoffloat_match e with - | singleoffloat_case1 e1 => e - | singleoffloat_case2 mode args => e - | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil) - end. - (** ** Comparisons *) Inductive comp_cases: forall (e1: expr) (e2: expr), Type := @@ -1034,15 +900,36 @@ Definition compu (c: comparison) (e1: expr) (e2: expr) := Definition compf (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). +(** ** Floating-point conversions *) + +Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). + +Definition intuoffloat (e: expr) := + let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in + Elet e + (Econdition (CEcond (Ccompf Clt) (Eletvar O ::: f ::: Enil)) + (intoffloat (Eletvar O)) + (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar O) f)))). + +Definition floatofintu (e: expr) := + subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) + (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil). + +Definition floatofint (e: expr) := + subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil + ::: addimm Float.ox8000_0000 e ::: Enil)) + (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil). + (** ** Other operators, not optimized. *) +Definition cast8unsigned (e: expr) := Eop Ocast8unsigned (e ::: Enil). +Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil). +Definition cast16unsigned (e: expr) := Eop Ocast16unsigned (e ::: Enil). +Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil). +Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). Definition negint (e: expr) := Eop (Osubimm Int.zero) (e ::: Enil). Definition negf (e: expr) := Eop Onegf (e ::: Enil). Definition absf (e: expr) := Eop Oabsf (e ::: Enil). -Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). -Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). -Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). -Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil). Definition xor (e1 e2: expr) := Eop Oxor (e1 ::: e2 ::: Enil). Definition shr (e1 e2: expr) := Eop Oshr (e1 ::: e2 ::: Enil). Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). |