From f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 6 Oct 2012 15:46:47 +0000
Subject: Merge of branch seq-and-or.  See Changelog for details.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/SelectOp.vp | 80 ++++++++++++++++++++++++++---------------------------
 1 file changed, 39 insertions(+), 41 deletions(-)

(limited to 'powerpc/SelectOp.vp')

diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index d913958..fbd2d7b 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -75,34 +75,6 @@ Nondetfunction notint (e: expr) :=
   | _ => Eop Onot (e:::Enil)
   end.
 
-(** ** Boolean value and boolean negation *)
-
-Fixpoint boolval (e: expr) {struct e} : expr :=
-  let default := Eop (Ocmp (Ccompuimm Cne Int.zero)) (e ::: Enil) in
-  match e with 
-  | Eop (Ointconst n) Enil =>
-      Eop (Ointconst (if Int.eq n Int.zero then Int.zero else Int.one)) Enil
-  | Eop (Ocmp cond) args =>
-      Eop (Ocmp cond) args
-  | Econdition e1 e2 e3 =>
-      Econdition e1 (boolval e2) (boolval e3)
-  | _ =>
-      default
-  end.
-
-Fixpoint notbool (e: expr) {struct e} : expr :=
-  let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in
-  match e with
-  | Eop (Ointconst n) Enil =>
-      Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil
-  | Eop (Ocmp cond) args =>
-      Eop (Ocmp (negate_condition cond)) args
-  | Econdition e1 e2 e3 =>
-      Econdition e1 (notbool e2) (notbool e3)
-  | _ =>
-      default
-  end.
-
 (** ** Integer addition and pointer addition *)
 
 Nondetfunction addimm (n: int) (e: expr) :=
@@ -386,12 +358,46 @@ Definition divf (e1 e2: expr) :=  Eop Odivf (e1 ::: e2 ::: Enil).
 
 (** ** Comparisons *)
 
+Nondetfunction compimm (default: comparison -> int -> condition)
+                       (sem: comparison -> int -> int -> bool)
+                       (c: comparison) (e1: expr) (n2: int) :=
+  match c, e1 with
+  | c, Eop (Ointconst n1) Enil =>
+      Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil
+  | Ceq, Eop (Ocmp c) el =>
+      if Int.eq_dec n2 Int.zero then
+        Eop (Ocmp (negate_condition c)) el
+      else if Int.eq_dec n2 Int.one then
+        Eop (Ocmp c) el
+      else 
+        Eop (Ointconst Int.zero) Enil
+  | Cne, Eop (Ocmp c) el =>
+      if Int.eq_dec n2 Int.zero then
+        Eop (Ocmp c) el
+      else if Int.eq_dec n2 Int.one then
+        Eop (Ocmp (negate_condition c)) el
+      else 
+        Eop (Ointconst Int.one) Enil
+  | Ceq, Eop (Oandimm n1) (t1 ::: Enil) =>
+      if Int.eq_dec n2 Int.zero then
+        Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil)
+      else
+        Eop (Ocmp (default c n2)) (e1 ::: Enil)
+  | Cne, Eop (Oandimm n1) (t1 ::: Enil) =>
+      if Int.eq_dec n2 Int.zero then
+        Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil)
+      else
+        Eop (Ocmp (default c n2)) (e1 ::: Enil)
+  | _, _ =>
+       Eop (Ocmp (default c n2)) (e1 ::: Enil)
+  end.
+
 Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 =>
-      Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2 ::: Enil)
+      compimm Ccompimm Int.cmp (swap_comparison c) t2 n1
   | t1, Eop (Ointconst n2) Enil =>
-      Eop (Ocmp (Ccompimm c n2)) (t1 ::: Enil)
+      compimm Ccompimm Int.cmp c t1 n2
   | _, _ =>
       Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil)
   end.
@@ -399,9 +405,9 @@ Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
 Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 =>
-      Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2 ::: Enil)
+      compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1
   | t1, Eop (Ointconst n2) Enil =>
-      Eop (Ocmp (Ccompuimm c n2)) (t1 ::: Enil)
+      compimm Ccompuimm Int.cmpu c t1 n2
   | _, _ =>
       Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil)
   end.
@@ -426,7 +432,7 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
 Definition intuoffloat (e: expr) :=
   Elet e
   (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil)
-    (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
+    (Econdition (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)
       (intoffloat (Eletvar 1))
       (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
 
@@ -452,11 +458,3 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | Eop Oadd (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil)
   | _ => (Aindexed Int.zero, e:::Enil)
   end.
-  
-(** ** Turning an expression into a condition *)
-
-Nondetfunction cond_of_expr (e: expr) :=
-  match e with
-  | Eop (Oandimm n) (t1:::Enil) => (Cmasknotzero n, t1:::Enil)
-  | _ => (Ccompuimm Cne Int.zero, e:::Enil)
-  end.
-- 
cgit v1.2.3