1 files changed, 33 insertions, 146 deletions
diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v
index e6a281b..c421cdc 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).