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
---
 ia32/ConstpropOp.vp     |  6 ++++--
 ia32/ConstpropOpproof.v |  3 ++-
 ia32/Unusedglob1.ml     | 44 ++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 50 insertions(+), 3 deletions(-)
 create mode 100644 ia32/Unusedglob1.ml

(limited to 'ia32')

diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index b861107..b95ad66 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -91,11 +91,13 @@ Nondetfunction eval_static_addressing (addr: addressing) (vl: list approx) :=
   | _, _ => 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
   | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n1)
   | Ocast8unsigned, I n1 :: nil => I(Int.zero_ext 8 n1)
   | Ocast16signed, I n1 :: nil => I(Int.sign_ext 16 n1)
@@ -132,7 +134,7 @@ 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
-  | Ofloatofint, I n1 :: nil => F(Float.floatofint n1)
+  | Ofloatofint, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofint n1) else Unknown
   | Ocmp c, vl => eval_static_condition_val c vl
   | _, _ => Unknown
   end.
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 04a1725..1612bf6 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -141,7 +141,7 @@ Proof.
   unfold eval_static_operation. 
   case (eval_static_operation_match op al); intros;
   InvVLMA; simpl in *; FuncInv; try subst v; auto.
-
+  destruct (propagate_float_constants tt); simpl; auto.
   rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto.
   destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
   destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
@@ -159,6 +159,7 @@ Proof.
   unfold eval_static_intoffloat.
   destruct (Float.intoffloat n1) as []_eqn; simpl in H0; inv H0.
   simpl; auto.
+  destruct (propagate_float_constants tt); simpl; auto.
   unfold eval_static_condition_val. destruct (eval_static_condition c vl0) as [b|]_eqn.
   rewrite (eval_static_condition_correct _ _ _ m _ H Heqo). 
   destruct b; simpl; auto.
diff --git a/ia32/Unusedglob1.ml b/ia32/Unusedglob1.ml
new file mode 100644
index 0000000..fe962e2
--- /dev/null
+++ b/ia32/Unusedglob1.ml
@@ -0,0 +1,44 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Identifiers referenced from an IA32 Asm instruction *)
+
+open Datatypes
+open AST
+open Asm
+
+let referenced_addr (Addrmode(base, ofs, const)) =
+  match const with
+  | Coq_inl n -> []
+  | Coq_inr(s, ofs) -> [s]
+
+let referenced_builtin ef =
+  match ef with
+  | EF_vload_global(chunk, id, ofs) -> [id]
+  | EF_vstore_global(chunk, id, ofs) -> [id]
+  | _ -> []
+
+let referenced_instr = function
+  | Pmov_rm (_, a) | Pmov_mr (a, _)
+  | Pmovsd_fm (_, a) | Pmovsd_mf(a, _)
+  | Pfld_m a | Pfstp_m a
+  | Pmovb_mr (a, _) | Pmovw_mr (a, _)
+  | Pmovzb_rm (_, a) | Pmovsb_rm (_, a)
+  | Pmovzw_rm (_, a) | Pmovsw_rm (_, a)
+  | Pcvtss2sd_fm (_, a) | Pcvtsd2ss_mf (a, _) | Plea (_, a) -> referenced_addr a
+  | Pjmp_s s -> [s]
+  | Pcall_s s -> [s]
+  | Pbuiltin(ef, args, res) -> referenced_builtin ef
+  | _ -> []
+
+let code_of_function f = f
+
-- 
cgit v1.2.3