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 --- arm/ConstpropOpproof.v | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) (limited to 'arm/ConstpropOpproof.v') diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index bf3b216c..242f29b0 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -124,7 +124,7 @@ Proof. unfold eval_static_operation. case (eval_static_operation_match op al); intros; InvVLMA; simpl in *; FuncInv; try (subst v); try (rewrite eval_static_shift_correct); auto. - + destruct (propagate_float_constants tt); simpl; auto. rewrite shift_symbol_address; auto. rewrite shift_symbol_address; auto. rewrite Val.add_assoc; auto. @@ -145,7 +145,8 @@ Proof. destruct (Int.ltu n2 Int.iwordsize); simpl; auto. unfold eval_static_intoffloat. destruct (Float.intoffloat n1); simpl in H0; inv H0; simpl; auto. unfold eval_static_intuoffloat. destruct (Float.intuoffloat n1); simpl in H0; inv H0; simpl; auto. - + destruct (propagate_float_constants tt); 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). @@ -153,6 +154,27 @@ 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); try (rewrite eval_static_shift_correct); 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. + rewrite Val.add_assoc. auto. +Qed. + (** * Correctness of strength reduction *) (** We now show that strength reduction over operators and addressing -- cgit