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

diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 3b5021e..1c050bd 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