From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy 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 --- powerpc/ConstpropOpproof.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'powerpc/ConstpropOpproof.v') 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 -- cgit