From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 21 May 2012 16:26:30 +0000
Subject: Merge of the newmem branch: - Revised memory model with Max and Cur
 permissions, but without bounds - Constant propagation of 'const' globals -
 Function inlining at RTL level - (Unprovable) elimination of unreferenced
 static definitions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/ConstpropOp.vp | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

(limited to 'powerpc/ConstpropOp.vp')

diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 32986713..60b5c63c 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -70,11 +70,13 @@ Definition eval_static_condition_val (cond: condition) (vl: list approx) :=
 Definition eval_static_intoffloat (f: float) :=
   match Float.intoffloat f with Some x => I x | None => Unknown end.
 
+Parameter propagate_float_constants: unit -> bool.
+
 Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   match op, vl with
   | Omove, v1::nil => v1
   | Ointconst n, nil => I n
-  | Ofloatconst n, nil => F n
+  | Ofloatconst n, nil => if propagate_float_constants tt then F n else Unknown
   | Oaddrsymbol s n, nil => G s n
   | Oaddrstack n, nil => S n
   | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n1)
@@ -119,11 +121,27 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2)
   | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
   | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1
-  | Ofloatofwords, I n1 :: I n2 :: nil => F(Float.from_words n1 n2)
+  | Ofloatofwords, I n1 :: I n2 :: nil => if propagate_float_constants tt then F(Float.from_words n1 n2) else Unknown
   | Ocmp c, vl => eval_static_condition_val c vl
   | _, _ => Unknown
   end.
 
+Nondetfunction eval_static_addressing (addr: addressing) (vl: list approx) :=
+  match addr, vl with
+  | Aindexed n, I n1::nil => I (Int.add n1 n)
+  | Aindexed n, G id ofs::nil => G id (Int.add ofs n)
+  | Aindexed n, S ofs::nil => S (Int.add ofs n)
+  | Aindexed2, I n1::I n2::nil => I (Int.add n1 n2)
+  | Aindexed2, G id ofs::I n2::nil => G id (Int.add ofs n2)
+  | Aindexed2, I n1::G id ofs::nil => G id (Int.add ofs n1)
+  | Aindexed2, S ofs::I n2::nil => S (Int.add ofs n2)
+  | Aindexed2, I n1::S ofs::nil => S (Int.add ofs n1)
+  | Aglobal id ofs, nil => G id ofs
+  | Abased id ofs, I n1::nil => G id (Int.add ofs n1)
+  | Ainstack ofs, nil => S ofs
+  | _, _ => Unknown
+  end.
+
 (** * Operator strength reduction *)
 
 (** We now define auxiliary functions for strength reduction of
-- 
cgit