From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Inliningspec.v | 33 ++++++++++++++++++++++++++++++++- 1 file changed, 32 insertions(+), 1 deletion(-) (limited to 'backend/Inliningspec.v') diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 82ef9cf9..e8dba674 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -180,6 +180,35 @@ Ltac monadInv H := ((progress simpl in H) || unfold F in H); monadInv1 H end. +Fixpoint mlist_iter2 {A B: Type} (f: A -> B -> mon unit) (l: list (A*B)): mon unit := + match l with + | nil => ret tt + | (x,y) :: l' => do z <- f x y; mlist_iter2 f l' + end. + +Remark mlist_iter2_fold: + forall (A B: Type) (f: A -> B -> mon unit) l s, + exists i, + mlist_iter2 f l s = + R tt (fold_left (fun a p => match f (fst p) (snd p) a with R _ s2 _ => s2 end) l s) i. +Proof. + induction l; simpl; intros. + exists (sincr_refl s); auto. + destruct a as [x y]. unfold bind. simpl. destruct (f x y s) as [xx s1 i1]. + destruct (IHl s1) as [i2 EQ]. rewrite EQ. econstructor; eauto. +Qed. + +Lemma ptree_mfold_spec: + forall (A: Type) (f: positive -> A -> mon unit) t s x s' i, + ptree_mfold f t s = R x s' i -> + exists i', mlist_iter2 f (PTree.elements t) s = R tt s' i'. +Proof. + intros. + destruct (mlist_iter2_fold _ _ f (PTree.elements t) s) as [i' EQ]. + unfold ptree_mfold in H. inv H. rewrite PTree.fold_spec. + econstructor. eexact EQ. +Qed. + (** ** Relational specification of the translation of moves *) Inductive tr_moves (c: code) : node -> list reg -> list reg -> node -> Prop := @@ -416,6 +445,7 @@ Lemma expand_cfg_rec_unchanged: Proof. intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ. transitivity ((st_code s0)!pc). + exploit ptree_mfold_spec; eauto. intros [INCR' ITER]. eapply iter_expand_instr_unchanged; eauto. subst s0; auto. subst s0; simpl. xomega. @@ -596,7 +626,8 @@ Proof. intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ. constructor. intros. rewrite H1. eapply max_def_function_params; eauto. - intros. eapply iter_expand_instr_spec; eauto. + intros. exploit ptree_mfold_spec; eauto. intros [INCR' ITER]. + eapply iter_expand_instr_spec; eauto. apply PTree.elements_keys_norepet. intros. rewrite H1. eapply max_def_function_instr; eauto. eapply PTree.elements_complete; eauto. -- cgit