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

3 files changed, 105 insertions, 2 deletions

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
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 3b5021e2..1c050bdb 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -118,6 +118,8 @@ Proof.
   case (eval_static_operation_match op al); intros;
   InvVLMA; simpl in *; FuncInv; try subst v; auto.
 
+  destruct (propagate_float_constants tt); simpl; auto.
+
   rewrite shift_symbol_address; auto.
 
   rewrite Int.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut. auto.
@@ -149,6 +151,8 @@ Proof.
   unfold eval_static_intoffloat. destruct (Float.intoffloat n1); simpl in H0; inv H0.
   simpl; auto.
 
+  destruct (propagate_float_constants tt); simpl; auto.
+
   unfold eval_static_condition_val, Val.of_optbool.
   destruct (eval_static_condition c vl0) as []_eqn.
   rewrite (eval_static_condition_correct _ _ _ m _ H Heqo).
@@ -156,6 +160,26 @@ Proof.
   simpl; auto.
 Qed.
 
+Lemma eval_static_addressing_correct:
+  forall addr al vl v,
+  val_list_match_approx al vl ->
+  eval_addressing ge sp addr vl = Some v ->
+  val_match_approx (eval_static_addressing addr al) v.
+Proof.
+  intros until v. unfold eval_static_addressing.
+  case (eval_static_addressing_match addr al); intros;
+  InvVLMA; simpl in *; FuncInv; try subst v; auto.
+  rewrite shift_symbol_address; auto.
+  rewrite Val.add_assoc. auto. 
+  repeat rewrite shift_symbol_address. auto.
+  fold (Val.add (Vint n1) (symbol_address ge id ofs)).
+  repeat rewrite shift_symbol_address. apply Val.add_commut.
+  repeat rewrite Val.add_assoc. auto.
+  fold (Val.add (Vint n1) (Val.add sp (Vint ofs))).
+  rewrite Val.add_permut. decEq. rewrite Val.add_commut. auto.
+  rewrite shift_symbol_address. auto.
+Qed.
+
 (** * Correctness of strength reduction *)
 
 (** We now show that strength reduction over operators and addressing
diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml
new file mode 100644
index 00000000..c16cd2f1
--- /dev/null
+++ b/powerpc/Unusedglob1.ml
@@ -0,0 +1,61 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 a PowerPC Asm instruction *)
+
+open Datatypes
+open AST
+open Asm
+
+let referenced_constant = function
+  | Cint n -> []
+  | Csymbol_low(s, ofs) -> [s]
+  | Csymbol_high(s, ofs) -> [s]
+  | Csymbol_sda(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
+  | Pbl s -> [s]
+  | Pbs s -> [s]
+  | Paddi(_, _, c)
+  | Paddic(_, _, c)
+  | Paddis(_, _, c)
+  | Pandi_(_, _, c)
+  | Pandis_(_, _, c)
+  | Pcmplwi(_, c)
+  | Pcmpwi(_, c)
+  | Plbz(_, c, _)
+  | Plfd(_, c, _)
+  | Plfs(_, c, _)
+  | Plha(_, c, _)
+  | Plhz(_, c, _)
+  | Plwz(_, c, _)
+  | Pmulli(_, _, c)
+  | Pori(_, _, c)
+  | Poris(_, _, c)
+  | Pstb(_, c, _)
+  | Pstfd(_, c, _)
+  | Pstfs(_, c, _)
+  | Psth(_, c, _) 
+  | Pstw(_, c, _) 
+  | Psubfic(_, _, c)
+  | Pxori(_, _, c)
+  | Pxoris(_, _, c) -> referenced_constant c
+  | Pbuiltin(ef, _, _) -> referenced_builtin ef
+  | _ -> []
+
+let code_of_function f = f