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

1 files changed, 44 insertions, 0 deletions

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
+