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/Inlining.v | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) (limited to 'backend/Inlining.v') diff --git a/backend/Inlining.v b/backend/Inlining.v index a9b1e7e..7b19f80 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -180,11 +180,17 @@ Next Obligation. intros; constructor; simpl; xomega. Qed. -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. +Program Definition ptree_mfold {A: Type} (f: positive -> A -> mon unit) (t: PTree.t A): mon unit := + fun s => + R tt + (PTree.fold (fun s1 k v => match f k v s1 return _ with R _ s2 _ => s2 end) t s) + _. +Next Obligation. + apply PTree_Properties.fold_rec. + auto. + apply sincr_refl. + intros. destruct (f k v a). eapply sincr_trans; eauto. +Qed. (** ** Inlining contexts *) @@ -422,7 +428,7 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit := Definition expand_cfg_rec (ctx: context) (f: function): mon unit := do x <- request_stack (ctx.(dstk) + ctx.(mstk)); - mlist_iter2 (expand_instr ctx) (PTree.elements f.(fn_code)). + ptree_mfold (expand_instr ctx) f.(fn_code). End EXPAND_CFG. -- cgit v1.2.3