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, 81 insertions, 0 deletions

diff --git a/backend/Renumber.v b/backend/Renumber.v
new file mode 100644
index 0000000..b933bba
--- /dev/null
+++ b/backend/Renumber.v
@@ -0,0 +1,81 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Postorder renumbering of RTL control-flow graphs. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import Postorder.
+Require Import AST.
+Require Import RTL.
+
+(** CompCert's dataflow analyses (module [Kildall]) are more precise
+  and run faster when the sequence [1, 2, 3, ...]  is a postorder
+  enumeration of the nodes of the control-flow graph.  This property
+  can be guaranteed when generating the CFG (module [RTLgen]), but
+  is, however, invalidated by further RTL optimization passes such as
+  [Inlining].  
+
+  In this module, we renumber the nodes of RTL control-flow graphs
+  to restore the postorder property given above.  In passing,
+  we also eliminate CFG nodes that are not reachable from the entry point:
+  these nodes are dead code. *)
+
+Section RENUMBER.
+
+Variable pnum: PTree.t positive.   (**r a postorder numbering *)
+
+Definition renum_pc (pc: node) : node :=
+  match pnum!pc with
+  | Some pc' => pc'
+  | None => 1%positive          (**r impossible case, never exercised *)
+  end.
+
+Definition renum_instr (i: instruction) : instruction :=
+  match i with
+  | Inop s => Inop (renum_pc s)
+  | Iop op args res s => Iop op args res (renum_pc s)
+  | Iload chunk addr args res s => Iload chunk addr args res (renum_pc s)
+  | Istore chunk addr args src s => Istore chunk addr args src (renum_pc s)
+  | Icall sg ros args res s => Icall sg ros args res (renum_pc s)
+  | Itailcall sg ros args => i
+  | Ibuiltin ef args res s => Ibuiltin ef args res (renum_pc s)
+  | Icond cond args s1 s2 => Icond cond args (renum_pc s1) (renum_pc s2)
+  | Ijumptable arg tbl => Ijumptable arg (List.map renum_pc tbl)
+  | Ireturn or => i
+  end.
+
+Definition renum_node (c': code) (pc: node) (i: instruction) : code :=
+  match pnum!pc with
+  | None => c'
+  | Some pc' => PTree.set pc' (renum_instr i) c'
+  end.
+
+Definition renum_cfg (c: code) : code :=
+  PTree.fold renum_node c (PTree.empty instruction).
+
+End RENUMBER.
+
+Definition transf_function (f: function) : function :=
+  let pnum := postorder (successors f) f.(fn_entrypoint) in
+  mkfunction
+    f.(fn_sig)
+    f.(fn_params)
+    f.(fn_stacksize)
+    (renum_cfg pnum f.(fn_code))
+    (renum_pc pnum f.(fn_entrypoint)).
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  AST.transform_program transf_fundef p.