Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

9 files changed, 363 insertions, 197 deletions

diff --git a/backend/Linearize.v b/backend/Linearize.v
index 305473ba..57919b87 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -3,9 +3,13 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Ordered.
+Require Import FSets.
+Require FSetAVL.
 Require Import AST.
 Require Import Values.
 Require Import Globalenvs.
+Require Import Errors.
 Require Import Op.
 Require Import Locations.
 Require Import LTL.
@@ -13,10 +17,12 @@ Require Import LTLin.
 Require Import Kildall.
 Require Import Lattice.
 
-(** To translate from LTL to LTLin, we must lay out the basic blocks
+Open Scope error_monad_scope.
+
+(** To translate from LTL to LTLin, we must lay out the nodes
   of the LTL control-flow graph in some linear order, and insert
   explicit branches and conditional branches to make sure that
-  each basic block jumps to its successors as prescribed by the
+  each node jumps to its successors as prescribed by the
   LTL control-flow graph.  However, branches are not necessary
   if the fall-through behaviour of LTLin instructions already
   implements the desired flow of control.  For instance,
@@ -39,29 +45,28 @@ Require Import Lattice.
     L2: ...
 >>
   The main challenge in code linearization is therefore to pick a
-  ``good'' order for the basic blocks that exploits well the
+  ``good'' order for the nodes that exploits well the
   fall-through behavior.  Many clever trace picking heuristics
   have been developed for this purpose.  
 
   In this file, we present linearization in a way that clearly
   separates the heuristic part (choosing an order for the basic blocks)
   from the actual code transformation parts.  We proceed in three passes:
-- Choosing an order for the basic blocks.  This returns an enumeration
-  of CFG nodes stating that the basic blocks must be laid out in
-  the order shown in the list.
-- Generate LTLin code where each basic block branches explicitly
-  to its successors, except if one of these successors is the
-  immediately following instruction.
+- Choosing an order for the nodes.  This returns an enumeration of CFG
+  nodes stating that they must be laid out in the order shown in the
+  list.
+- Generate LTLin code where each node branches explicitly to its
+  successors, except if one of these successors is the immediately
+  following instruction.
 
   The beauty of this approach is that correct code is generated
   under surprisingly weak hypotheses on the enumeration of
   CFG nodes: it suffices that every reachable instruction occurs
-  exactly once in the enumeration.  While the enumeration heuristic we use
-  is quite trivial, it is easy to implement more sophisticated
-  trace picking heuristics: as long as they satisfy the property above,
-  we do not need to re-do the proof of semantic preservation.
-  The enumeration could even be performed by external, untrusted
-  Caml code, then verified (for the property above) by certified Coq code.
+  exactly once in the enumeration.  We therefore follow an approach
+  based on validation a posteriori: a piece of untrusted Caml code
+  implements the node enumeration heuristics, and the resulting
+  enumeration is checked for correctness by Coq functions that are
+  proved to be sound.
 *)
 
 (** * Determination of the order of basic blocks *)
@@ -88,21 +93,44 @@ Definition reachable (f: LTL.function) : PMap.t bool :=
   | Some rs => rs
   end.
 
-(** We then enumerate the nodes of reachable basic blocks.  The heuristic
-  we take is trivial: nodes are enumerated in decreasing numerical
-  order.  Remember that CFG nodes are positive integers, and that
-  the [RTLgen] pass allocated fresh nodes 1, 2, 3, ..., but generated
-  instructions in roughly reverse control-flow order: often,
-  a basic block at label [n] has [n-1] as its only successor.
-  Therefore, by enumerating reachable nodes in decreasing order,
-  we recover a reasonable layout of basic blocks that globally respects
-  the structure of the original Cminor code. *)
-
-Definition enumerate (f: LTL.function) : list node :=
+(** We then enumerate the nodes of reachable instructions.
+  This task is performed by external, untrusted Caml code. *)
+
+Parameter enumerate_aux: LTL.function -> PMap.t bool -> list node.
+
+(** Now comes the validation of an enumeration a posteriori. *)
+
+Module Nodeset := FSetAVL.Make(OrderedPositive).
+
+(** Build a Nodeset.t from a list of nodes, checking that the list
+  contains no duplicates. *)
+
+Fixpoint nodeset_of_list (l: list node) (s: Nodeset.t)
+                         {struct l}: res Nodeset.t :=
+  match l with
+  | nil => OK s
+  | hd :: tl =>
+      if Nodeset.mem hd s 
+      then Error (msg "Linearize: duplicates in enumeration")
+      else nodeset_of_list tl (Nodeset.add hd s)
+  end.
+
+Definition check_reachable_aux
+     (reach: PMap.t bool) (s: Nodeset.t)
+     (ok: bool) (pc: node) (i: LTL.instruction) : bool :=
+  if reach!!pc then ok && Nodeset.mem pc s else ok.
+
+Definition check_reachable
+     (f: LTL.function) (reach: PMap.t bool) (s: Nodeset.t) : bool :=
+  PTree.fold (check_reachable_aux reach s) f.(LTL.fn_code) true.
+
+Definition enumerate (f: LTL.function) : res (list node) :=
   let reach := reachable f in
-  positive_rec (list node) nil
-    (fun pc nodes => if reach!!pc then pc :: nodes else nodes)
-    f.(fn_nextpc).
+  let enum := enumerate_aux f reach in
+  do s <- nodeset_of_list enum Nodeset.empty;
+  if check_reachable f reach s
+  then OK enum
+  else Error (msg "Linearize: wrong enumeration").
 
 (** * Translation from LTL to LTLin *)
 
@@ -172,15 +200,16 @@ Fixpoint linearize_body (f: LTL.function) (enum: list node)
 
 (** * Entry points for code linearization *)
 
-Definition transf_function (f: LTL.function) : LTLin.function :=
-  mkfunction
-    (LTL.fn_sig f)
-    (LTL.fn_params f)
-    (LTL.fn_stacksize f)
-    (add_branch (LTL.fn_entrypoint f) (linearize_body f (enumerate f))).
+Definition transf_function (f: LTL.function) : res LTLin.function :=
+  do enum <- enumerate f;
+  OK (mkfunction
+       (LTL.fn_sig f)
+       (LTL.fn_params f)
+       (LTL.fn_stacksize f)
+       (add_branch (LTL.fn_entrypoint f) (linearize_body f enum))).
 
-Definition transf_fundef (f: LTL.fundef) : LTLin.fundef :=
-  AST.transf_fundef transf_function f.
+Definition transf_fundef (f: LTL.fundef) : res LTLin.fundef :=
+  AST.transf_partial_fundef transf_function f.
 
-Definition transf_program (p: LTL.program) : LTLin.program :=
-  transform_program transf_fundef p.
+Definition transf_program (p: LTL.program) : res LTLin.program :=
+  transform_partial_program transf_fundef p.
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index c7299085..a625ba75 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -2,12 +2,15 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Ordered.
+Require Import FSets.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
 Require Import Mem.
 Require Import Events.
 Require Import Globalenvs.
+Require Import Errors.
 Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
@@ -17,10 +20,14 @@ Require Import LTLin.
 Require Import Linearize.
 Require Import Lattice.
 
+Module NodesetFacts := FSetFacts.Facts(Nodeset).
+
 Section LINEARIZATION.
 
 Variable prog: LTL.program.
-Let tprog := transf_program prog.
+Variable tprog: LTLin.program.
+
+Hypothesis TRANSF: transf_program prog = OK tprog.
 
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
@@ -28,33 +35,40 @@ Let tge := Genv.globalenv tprog.
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (transf_fundef f).
-Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog).
+  exists tf,
+  Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_transf_partial transf_fundef TRANSF).
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
-  Genv.find_funct_ptr tge v = Some (transf_fundef f).
-Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog).
+  exists tf,
+  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF).
 
 Lemma symbols_preserved:
   forall id,
   Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (@Genv.find_symbol_transf _ _ _ transf_fundef prog).
+Proof (Genv.find_symbol_transf_partial transf_fundef _ TRANSF).
 
 Lemma sig_preserved:
-  forall f, funsig (transf_fundef f) = LTL.funsig f.
+  forall f tf,
+  transf_fundef f = OK tf ->
+  LTLin.funsig tf = LTL.funsig f.
 Proof.
-  destruct f; reflexivity.
+  unfold transf_fundef, transf_partial_fundef; intros.
+  destruct f. monadInv H. monadInv EQ. reflexivity.
+  inv H. reflexivity.
 Qed.
 
 Lemma find_function_translated:
   forall ros ls f,
   LTL.find_function ge ros ls = Some f ->
-  find_function tge ros ls = Some (transf_fundef f).
+  exists tf,
+  find_function tge ros ls = Some tf /\ transf_fundef f = OK tf.
 Proof.
-  intros until f. destruct ros; simpl.
-  intro. apply functions_translated; auto.
+  unfold LTL.find_function; intros; destruct ros; simpl.
+  apply functions_translated; auto.
   rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
   apply function_ptr_translated; auto.
   congruence.
@@ -102,54 +116,84 @@ Qed.
 - All nodes for reachable basic blocks must be in the list.
 - The list is without repetition (so that no code duplication occurs).
 
-We prove that our [enumerate] function satisfies all three. *)
+We prove that our [enumerate] function satisfies both conditions. *)
+
+
+Lemma nodeset_of_list_correct:
+  forall l s s',
+  nodeset_of_list l s = OK s' ->
+  list_norepet l
+  /\ (forall pc, Nodeset.In pc s' <-> Nodeset.In pc s \/ In pc l)
+  /\ (forall pc, In pc l -> ~Nodeset.In pc s).
+Proof.
+  induction l; simpl; intros. 
+  inv H. split. constructor. split. intro; tauto. intros; tauto.
+  generalize H; clear H; caseEq (Nodeset.mem a s); intros.
+  inv H0.
+  exploit IHl; eauto. intros [A [B C]].
+  split. constructor; auto. red; intro. elim (C a H1). apply Nodeset.add_1. hnf. auto.
+  split. intros. rewrite B. rewrite NodesetFacts.add_iff. 
+  unfold Nodeset.E.eq. unfold OrderedPositive.eq. tauto.
+  intros. destruct H1. subst pc. rewrite NodesetFacts.not_mem_iff. auto.
+  generalize (C pc H1). rewrite NodesetFacts.add_iff. tauto.
+Qed.
+
+Lemma check_reachable_correct:
+  forall f reach s pc i,
+  check_reachable f reach s = true ->
+  f.(LTL.fn_code)!pc = Some i ->
+  reach!!pc = true ->
+  Nodeset.In pc s.
+Proof.
+  intros f reach s.
+  assert (forall l ok, 
+    List.fold_left (fun a p => check_reachable_aux reach s a (fst p) (snd p)) l ok = true ->
+    ok = true /\
+    (forall pc i,
+     In (pc, i) l ->
+     reach!!pc = true ->
+     Nodeset.In pc s)).
+  induction l; simpl; intros.
+  split. auto. intros. destruct H0.
+  destruct a as [pc1 i1]. simpl in H. 
+  exploit IHl; eauto. intros [A B].
+  unfold check_reachable_aux in A. 
+  split. destruct (reach!!pc1). elim (andb_prop _ _ A). auto. auto.
+  intros. destruct H0. inv H0. rewrite H1 in A. destruct (andb_prop _ _ A). 
+  apply Nodeset.mem_2; auto.
+  eauto.
+
+  intros pc i. unfold check_reachable. rewrite PTree.fold_spec. intros.
+  exploit H; eauto. intros [A B]. eapply B; eauto. 
+  apply PTree.elements_correct. eauto.
+Qed.
 
 Lemma enumerate_complete:
-  forall f pc i,
+  forall f enum pc i,
+  enumerate f = OK enum ->
   f.(LTL.fn_code)!pc = Some i ->
   (reachable f)!!pc = true ->
-  In pc (enumerate f).
+  In pc enum.
 Proof.
-  intros. 
-  assert (forall p, 
-    Plt p f.(fn_nextpc) ->
-    (reachable f)!!p = true ->
-    In p (enumerate f)).
-  unfold enumerate. pattern (fn_nextpc f).
-  apply positive_Peano_ind. 
-  intros. compute in H1. destruct p; discriminate. 
-  intros. rewrite positive_rec_succ. elim (Plt_succ_inv _ _ H2); intro.
-  case (reachable f)!!x. apply in_cons. auto. auto.
-  subst x. rewrite H3. apply in_eq. 
-  elim (LTL.fn_code_wf f pc); intro. auto. congruence.
-Qed. 
+  intros until i. unfold enumerate. 
+  set (reach := reachable f).
+  intros. monadInv H. 
+  generalize EQ0; clear EQ0. caseEq (check_reachable f reach x); intros; inv EQ0.
+  exploit check_reachable_correct; eauto. intro.
+  exploit nodeset_of_list_correct; eauto. intros [A [B C]].
+  rewrite B in H2. destruct H2. elim (Nodeset.empty_1 pc H2). auto.
+Qed.
 
 Lemma enumerate_norepet:
-  forall f, list_norepet (enumerate f).
-Proof.
-  intro. 
-  unfold enumerate. pattern (fn_nextpc f).
-  apply positive_Peano_ind.  
-  rewrite positive_rec_base. constructor.
-  intros. rewrite positive_rec_succ.
-  case (reachable f)!!x.
-  constructor. 
-  assert (forall y,
-    In y (positive_rec
-     (list node) nil
-     (fun (pc : positive) (nodes : list node) =>
-      if (reachable f) !! pc then pc :: nodes else nodes) x) ->
-    Plt y x).
-    pattern x. apply positive_Peano_ind. 
-    rewrite positive_rec_base. intros. elim H0.
-    intros until y. rewrite positive_rec_succ. 
-    case (reachable f)!!x0. 
-    simpl. intros [A|B].
-    subst x0. apply Plt_succ.
-    apply Plt_trans_succ. auto. 
-    intro. apply Plt_trans_succ. auto.
-  red; intro. generalize (H0 x H1). exact (Plt_strict x). auto.
-  auto.
+  forall f enum,
+  enumerate f = OK enum ->
+  list_norepet enum.
+Proof.
+  intros until enum. unfold enumerate. 
+  set (reach := reachable f).
+  intros. monadInv H. 
+  generalize EQ0; clear EQ0. caseEq (check_reachable f reach x); intros; inv EQ0.
+  exploit nodeset_of_list_correct; eauto. intros [A [B C]]. auto.
 Qed.
 
 (** * Properties related to labels *)
@@ -243,23 +287,34 @@ Proof.
   auto.
 Qed.
 
+(*
+Lemma transf_function_inv:
+  forall f tf, transf_function f = OK tf ->
+  exists enum, enumerate f = OK enum /\ fn_code tf = add_branch (LTL.fn_entrypoint f) (linearize_body f enum).
+Proof.
+  intros. monadInv H. exists x; auto.
+Qed.
+*)
+
 Lemma find_label_lin:
-  forall f pc b,
+  forall f tf pc b,
+  transf_function f = OK tf ->
   f.(LTL.fn_code)!pc = Some b ->
   (reachable f)!!pc = true ->
   exists k,
-  find_label pc (fn_code (transf_function f)) = Some (linearize_instr b k).
+  find_label pc (fn_code tf) = Some (linearize_instr b k).
 Proof.
-  intros. unfold transf_function; simpl.
+  intros. monadInv H. simpl. 
   rewrite find_label_add_branch. apply find_label_lin_rec.
   eapply enumerate_complete; eauto. auto.
 Qed.
 
 Lemma find_label_lin_inv:
-  forall f pc b k ,
+  forall f tf pc b k,
+  transf_function f = OK tf ->
   f.(LTL.fn_code)!pc = Some b ->
   (reachable f)!!pc = true ->
-  find_label pc (fn_code (transf_function f)) = Some k ->
+  find_label pc (fn_code tf) = Some k ->
   exists k', k = linearize_instr b k'.
 Proof.
   intros. exploit find_label_lin; eauto. intros [k' FIND].
@@ -267,13 +322,14 @@ Proof.
 Qed.
 
 Lemma find_label_lin_succ:
-  forall f s,
+  forall f tf s,
+  transf_function f = OK tf ->
   valid_successor f s ->
   (reachable f)!!s = true ->
   exists k,
-  find_label s (fn_code (transf_function f)) = Some k.
+  find_label s (fn_code tf) = Some k.
 Proof.
-  intros. destruct H as [i AT]. 
+  intros. destruct H0 as [i AT]. 
   exploit find_label_lin; eauto. intros [k FIND].
   exists (linearize_instr i k); auto.
 Qed.
@@ -344,12 +400,13 @@ Proof.
 Qed.
 
 Lemma unique_labels_transf_function:
-  forall f,
-  unique_labels (fn_code (transf_function f)).
+  forall f tf,
+  transf_function f = OK tf ->
+  unique_labels (fn_code tf).
 Proof.
-  intros. unfold transf_function; simpl.
+  intros. monadInv H. simpl.
   apply unique_labels_add_branch. 
-  apply unique_labels_lin_rec. apply enumerate_norepet. 
+  apply unique_labels_lin_rec. eapply enumerate_norepet; eauto.
 Qed.
 
 (** Correctness of [add_branch]. *)
@@ -373,16 +430,17 @@ Proof.
 Qed.
 
 Lemma add_branch_correct:
-  forall lbl c k s f sp ls m,
-  is_tail k (transf_function f).(fn_code) ->
-  find_label lbl (transf_function f).(fn_code) = Some c ->
-  plus step tge (State s (transf_function f) sp (add_branch lbl k) ls m)
-             E0 (State s (transf_function f) sp c ls m).
+  forall lbl c k s f tf sp ls m,
+  transf_function f = OK tf ->
+  is_tail k tf.(fn_code) ->
+  find_label lbl tf.(fn_code) = Some c ->
+  plus step tge (State s tf sp (add_branch lbl k) ls m)
+             E0 (State s tf sp c ls m).
 Proof.
   intros. unfold add_branch.
   caseEq (starts_with lbl k); intro SW.
   eapply starts_with_correct; eauto.
-  apply unique_labels_transf_function.
+  eapply unique_labels_transf_function; eauto.
   apply plus_one. apply exec_Lgoto. auto.
 Qed.
 
@@ -407,30 +465,33 @@ Qed.
 
 Inductive match_stackframes: LTL.stackframe -> LTLin.stackframe -> Prop :=
   | match_stackframe_intro:
-      forall res f sp pc ls c,
+      forall res f sp pc ls tf c,
+      transf_function f = OK tf ->
       (reachable f)!!pc = true ->
       valid_successor f pc ->
-      is_tail c (fn_code (transf_function f)) ->
+      is_tail c (fn_code tf) ->
       wt_function f ->
       match_stackframes
         (LTL.Stackframe res f sp ls pc)
-        (LTLin.Stackframe res (transf_function f) sp ls (add_branch pc c)).
+        (LTLin.Stackframe res tf sp ls (add_branch pc c)).
 
 Inductive match_states: LTL.state -> LTLin.state -> Prop :=
   | match_states_intro:
-      forall s f sp pc ls m ts c
+      forall s f sp pc ls m tf ts c
         (STACKS: list_forall2 match_stackframes s ts)
+        (TRF: transf_function f = OK tf)
         (REACH: (reachable f)!!pc = true)
-        (AT: find_label pc (fn_code (transf_function f)) = Some c)
+        (AT: find_label pc (fn_code tf) = Some c)
         (WTF: wt_function f),
       match_states (LTL.State s f sp pc ls m)
-                   (LTLin.State ts (transf_function f) sp c ls m)
+                   (LTLin.State ts tf sp c ls m)
   | match_states_call:
-      forall s f ls m ts,
+      forall s f ls m tf ts,
       list_forall2 match_stackframes s ts ->
+      transf_fundef f = OK tf ->
       wt_fundef f ->
       match_states (LTL.Callstate s f ls m)
-                   (LTLin.Callstate ts (transf_fundef f) ls m)
+                   (LTLin.Callstate ts tf ls m)
   | match_states_return:
       forall s sig ls m ts,
       list_forall2 match_stackframes s ts ->
@@ -455,7 +516,7 @@ Proof.
   induction 1; intros; try (inv MS);
   try (generalize (wt_instrs _ WTF _ _ H); intro WTI).
   (* Lnop *)
-  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
   eapply reachable_successors; eauto.
@@ -466,7 +527,7 @@ Proof.
   eapply is_tail_add_branch. eapply is_tail_find_label. eauto.
   econstructor; eauto. 
   (* Lop *)
-  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
   eapply reachable_successors; eauto.
@@ -482,7 +543,7 @@ Proof.
   traceEq.
   econstructor; eauto.
   (* Lload *)
-  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
   eapply reachable_successors; eauto.
@@ -498,7 +559,7 @@ Proof.
   traceEq.
   econstructor; eauto.
   (* Lstore *)
-  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
   eapply reachable_successors; eauto.
@@ -516,16 +577,16 @@ Proof.
   (* Lcall *)
   unfold rs1 in *. inv MS. fold rs1.
   generalize (wt_instrs _ WTF _ _ H); intro WTI.
-  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
   eapply reachable_successors; eauto.
   unfold successors; rewrite H; auto with coqlib.
   assert (VALID: valid_successor f pc'). inv WTI; auto.
+  exploit find_function_translated; eauto. intros [tf' [A B]].
   econstructor; split.
-  apply plus_one. eapply exec_Lcall with (f' := transf_fundef f'); eauto.
-  apply find_function_translated; auto.
-  symmetry; apply sig_preserved.
+  apply plus_one. eapply exec_Lcall with (f' := tf'); eauto.
+  symmetry; apply sig_preserved; auto.
   econstructor; eauto.
   constructor; auto. econstructor; eauto.
   eapply is_tail_add_branch. eapply is_tail_cons_left. 
@@ -537,12 +598,12 @@ Proof.
 
   (* Ltailcall *)
   unfold rs2, rs1 in *. inv MS. fold rs1; fold rs2.
-  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
+  exploit find_function_translated; eauto. intros [tf' [A B]].
   econstructor; split.
-  apply plus_one. eapply exec_Ltailcall with (f' := transf_fundef f'); eauto.
-  apply find_function_translated; auto.
-  symmetry; apply sig_preserved.
+  apply plus_one. eapply exec_Ltailcall with (f' := tf'); eauto.
+  symmetry; apply sig_preserved; auto.
   rewrite (parent_locset_match _ _ STACKS).
   econstructor; eauto.
   destruct ros; simpl in H0.
@@ -551,7 +612,7 @@ Proof.
   eapply Genv.find_funct_ptr_prop; eauto.
 
   (* Lalloc *)
-  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
   eapply reachable_successors; eauto.
@@ -565,8 +626,9 @@ Proof.
   eapply is_tail_find_label. eauto.
   traceEq.
   econstructor; eauto.
+
   (* Lcond true *)
-  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!ifso = true).
   eapply reachable_successors; eauto.
@@ -585,8 +647,9 @@ Proof.
   econstructor; split.
   apply plus_one. eapply exec_Lcond_true; eauto.
   econstructor; eauto.
+
   (* Lcond false *)
-  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!ifnot = true).
   eapply reachable_successors; eauto.
@@ -605,29 +668,33 @@ Proof.
   eapply is_tail_find_label. eauto.
   traceEq.
   econstructor; eauto.
+
   (* Lreturn *)
-  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   econstructor; split.
   apply plus_one. eapply exec_Lreturn; eauto.
   rewrite (parent_locset_match _ _ STACKS).
-  econstructor; eauto. 
+  monadInv TRF. simpl. econstructor; eauto.
+ 
   (* internal function *)
   assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true).
     apply reachable_entrypoint.
-  inv H6. 
+  inv H7. monadInv H6.   
   exploit find_label_lin_succ; eauto. inv H1; auto. intros [c'' AT'].
-  simpl. econstructor; split.
+  generalize EQ; intro. monadInv EQ0. econstructor; simpl; split.
   eapply plus_left'.  
   eapply exec_function_internal; eauto.
-  simpl. eapply add_branch_correct. 
+  simpl. eapply add_branch_correct. eauto.  
   simpl. eapply is_tail_add_branch. constructor. eauto.
   traceEq.
   econstructor; eauto.
+
   (* external function *)
-  simpl. econstructor; split.
+  monadInv H6. econstructor; split.
   apply plus_one. eapply exec_function_external; eauto.
   econstructor; eauto.
+
   (* return *)
   inv H4. inv H1.
   exploit find_label_lin_succ; eauto. intros [c' AT].
@@ -642,17 +709,18 @@ Lemma transf_initial_states:
   forall st1, LTL.initial_state prog st1 ->
   exists st2, LTLin.initial_state tprog st2 /\ match_states st1 st2.
 Proof.
-  intros. inversion H. 
-  exists (Callstate nil (transf_fundef f) (Locmap.init Vundef) (Genv.init_mem tprog)); split.
+  intros. inversion H.
+  exploit function_ptr_translated; eauto. intros [tf [A B]].  
+  exists (Callstate nil tf (Locmap.init Vundef) (Genv.init_mem tprog)); split.
   econstructor; eauto.
-  change (prog_main tprog) with (prog_main prog).
+  replace (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
-  apply function_ptr_translated; auto.
-  rewrite <- H2. apply sig_preserved.
+  symmetry. apply (transform_partial_program_main transf_fundef _ TRANSF). 
+  rewrite <- H2. apply sig_preserved. auto.
   replace (Genv.init_mem tprog) with (Genv.init_mem prog).
-  constructor. constructor.
+  constructor. constructor. auto.
   eapply Genv.find_funct_ptr_prop; eauto.
-  symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf.
+  symmetry. apply Genv.init_mem_transf_partial with transf_fundef. auto.
 Qed.
 
 Lemma transf_final_states:
diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v
index c930ca52..473b3421 100644
--- a/backend/Linearizetyping.v
+++ b/backend/Linearizetyping.v
@@ -2,6 +2,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Errors.
 Require Import AST.
 Require Import Op.
 Require Import Locations.
@@ -65,33 +66,34 @@ Proof.
 Qed.
 
 Lemma wt_transf_function:
-  forall f,
+  forall f tf,
   LTLtyping.wt_function f ->
-  wt_function (transf_function f). 
+  transf_function f = OK tf ->
+  wt_function tf. 
 Proof.
-  intros. inv H. constructor; auto.
+  intros. inv H. monadInv H0. constructor; auto.
   simpl. apply wt_add_branch. 
   apply wt_linearize_body. auto. 
 Qed.
 
 Lemma wt_transf_fundef:
-  forall f,
+  forall f tf,
   LTLtyping.wt_fundef f ->
-  wt_fundef (transf_fundef f). 
+  transf_fundef f = OK tf ->
+  wt_fundef tf. 
 Proof.
-  induction 1; simpl.
-  constructor; assumption.
-  constructor; apply wt_transf_function; assumption.
+  induction 1; intros. monadInv H. constructor. 
+  monadInv H0. constructor; eapply wt_transf_function; eauto.
 Qed.
 
 Lemma program_typing_preserved:
-  forall (p: LTL.program),
+  forall (p: LTL.program) (tp: LTLin.program),
   LTLtyping.wt_program p ->
-  LTLintyping.wt_program (transf_program p).
+  transf_program p = OK tp ->
+  LTLintyping.wt_program tp.
 Proof.
   intros; red; intros.
-  generalize (transform_program_function transf_fundef p i f H0).
+  generalize (transform_partial_program_function transf_fundef _ _ _ H0 H1).
   intros [f0 [IN TR]].
-  subst f. apply wt_transf_fundef; auto. 
-  apply (H i f0 IN).
+  eapply wt_transf_fundef; eauto. 
 Qed.
diff --git a/caml/Linearizeaux.ml b/caml/Linearizeaux.ml
new file mode 100644
index 00000000..8a4297f4
--- /dev/null
+++ b/caml/Linearizeaux.ml
@@ -0,0 +1,83 @@
+open BinPos
+open Coqlib
+open Datatypes
+open LTL
+open Lattice
+open CList
+open Maps
+open Camlcoq
+
+(* Trivial enumeration, in decreasing order of PC *)
+
+(***
+let enumerate_aux f reach =
+  positive_rec
+    Coq_nil
+    (fun pc nodes ->
+      if PMap.get pc reach
+      then Coq_cons (pc, nodes)
+      else nodes) 
+    f.fn_nextpc
+***)
+
+(* More clever enumeration that flattens basic blocks *)
+
+let rec int_of_pos = function
+  | Coq_xI p -> (int_of_pos p lsl 1) + 1
+  | Coq_xO p -> int_of_pos p lsl 1
+  | Coq_xH -> 1
+
+(* Count the reachable predecessors for each node *)
+
+let reachable_predecessors f reach =
+  let count = Array.make (int_of_pos f.fn_nextpc) 0 in
+  let increment pc =
+    let i = int_of_pos pc in
+    count.(i) <- count.(i) + 1 in
+  positive_rec
+    ()
+    (fun pc _ ->
+      if PMap.get pc reach then coqlist_iter increment (successors f pc))
+    f.fn_nextpc;
+  count
+
+(* Recognize instructions with only one successor *)
+
+let single_successor f pc =
+  match PTree.get pc f.fn_code with
+    | Some i ->
+        (match i with
+           | Lnop s -> Some s
+           | Lop (op, args, res, s) -> Some s
+           | Lload (chunk, addr, args, dst, s) -> Some s
+           | Lstore (chunk, addr, args, src, s) -> Some s
+           | Lcall (sig0, ros, args, res, s) -> Some s
+           | Ltailcall (sig0, ros, args) -> None
+           | Lalloc (arg, res, s) -> Some s
+           | Lcond (cond, args, ifso, ifnot) -> None
+           | Lreturn optarg -> None)
+    | None -> None
+
+(* Build the enumeration *)
+
+let enumerate_aux f reach =
+  let preds = reachable_predecessors f reach in
+  let enum = ref Coq_nil in
+  let emitted = Array.make (int_of_pos f.fn_nextpc) false in
+  let rec emit_basic_block pc =
+    enum := Coq_cons(pc, !enum);
+    emitted.(int_of_pos pc) <- true;
+    match single_successor f pc with
+    | None -> ()
+    | Some pc' ->
+        let npc' = int_of_pos pc' in
+        if preds.(npc') <= 1 && not emitted.(npc') then emit_basic_block pc' in
+  let rec emit_all pc =
+    if pc <> Coq_xH then begin
+      let pc = coq_Ppred pc in
+      if not emitted.(int_of_pos pc) && PMap.get pc reach
+      then emit_basic_block pc;
+      emit_all pc
+    end in
+  emit_all f.fn_nextpc;
+  CList.rev !enum
diff --git a/common/Main.v b/common/Main.v
index db159298..bfee3ff3 100644
--- a/common/Main.v
+++ b/common/Main.v
@@ -100,7 +100,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res PPC.fundef :=
    @@ CSE.transf_fundef
   @@@ Allocation.transf_fundef
    @@ Tunneling.tunnel_fundef
-   @@ Linearize.transf_fundef
+  @@@ Linearize.transf_fundef
    @@ Reload.transf_fundef
   @@@ Stacking.transf_fundef
   @@@ PPCgen.transf_fundef.
@@ -224,7 +224,7 @@ Proof.
   destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H6) as [p5 [H5 P5]].
   clear H6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5.
   destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H5) as [p4 [H4 P4]].
-  clear H5. generalize (transform_program_partial_program _ _ _ _ _ _ P4). clear P4. intro P4.
+  clear H5.
   destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H4) as [p3 [H3 P3]].
   clear H4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3.
   destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]].
@@ -240,7 +240,7 @@ Proof.
   assert (WT4 : LTLtyping.wt_program p4).
     subst p4. apply Tunnelingtyping.program_typing_preserved. auto.
   assert (WT5 : LTLintyping.wt_program p5).
-    subst p5. apply Linearizetyping.program_typing_preserved. auto.
+    apply Linearizetyping.program_typing_preserved with p4. auto. auto.
   assert (WT6 : Lineartyping.wt_program p6).
     subst p6. apply Reloadtyping.program_typing_preserved. auto.
   assert (WT7: Machtyping.wt_program p7).
@@ -250,7 +250,7 @@ Proof.
   apply Machabstr2concr.exec_program_equiv; auto.
   apply Stackingproof.transf_program_correct with p6; auto.
   subst p6; apply Reloadproof.transf_program_correct; auto.
-  subst p5; apply Linearizeproof.transf_program_correct; auto.
+  apply Linearizeproof.transf_program_correct with p4; auto.
   subst p4; apply Tunnelingproof.transf_program_correct. 
   apply Allocproof.transf_program_correct with p2; auto.
   subst p2; apply CSEproof.transf_program_correct.
diff --git a/extraction/.depend b/extraction/.depend
index 6ed07d8b..60534fdd 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -42,10 +42,10 @@
     ../caml/CMlexer.cmx 
 ../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo 
 ../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx 
-../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \
-    ../caml/Camlcoq.cmo CList.cmi AST.cmi 
-../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \
-    ../caml/Camlcoq.cmx CList.cmx AST.cmx 
+../caml/Linearizeaux.cmo: Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \
+    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi 
+../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTLin.cmx LTL.cmx \
+    Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx 
 ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
     CList.cmi AST.cmi 
 ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
@@ -129,8 +129,9 @@ Kildall.cmi: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \
     BinPos.cmi BinInt.cmi 
 Lattice.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \
     BinPos.cmi 
-Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi 
+Linearize.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \
+    Lattice.cmi LTLin.cmi LTL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \
+    CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
 Linear.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
     Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi 
@@ -351,12 +352,14 @@ Lattice.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \
     BinPos.cmi Lattice.cmi 
 Lattice.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Bool.cmx \
     BinPos.cmx Lattice.cmi 
-Linearize.cmo: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \
-    Kildall.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi \
-    Linearize.cmi 
-Linearize.cmx: Specif.cmx Op.cmx Maps.cmx Lattice.cmx LTLin.cmx LTL.cmx \
-    Kildall.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx AST.cmx \
-    Linearize.cmi 
+Linearize.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \
+    ../caml/Linearizeaux.cmo Lattice.cmi LTLin.cmi LTL.cmi Kildall.cmi \
+    FSetAVL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi \
+    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi Linearize.cmi 
+Linearize.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Op.cmx Maps.cmx \
+    ../caml/Linearizeaux.cmx Lattice.cmx LTLin.cmx LTL.cmx Kildall.cmx \
+    FSetAVL.cmx Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx \
+    BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx Linearize.cmi 
 Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
     Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi Linear.cmi 
diff --git a/extraction/Linearize.ml.patch b/extraction/Linearize.ml.patch
deleted file mode 100644
index 47b6cc9b..00000000
--- a/extraction/Linearize.ml.patch
+++ /dev/null
@@ -1,22 +0,0 @@
-*** Linearize.ml.orig	2006-02-09 11:47:55.000000000 +0100
---- Linearize.ml	2006-02-09 11:58:42.000000000 +0100
-***************
-*** 28,35 ****
-  (** val enumerate : LTL.coq_function -> node list **)
-  
-  let enumerate f =
-    positive_rec Coq_nil (fun pc nodes ->
-!     match Maps.PMap.get pc (reachable f) with
-        | true -> Coq_cons (pc, nodes)
-        | false -> nodes) (coq_Psucc f.fn_entrypoint)
-  
---- 28,36 ----
-  (** val enumerate : LTL.coq_function -> node list **)
-  
-  let enumerate f =
-+   let reach = reachable f in
-    positive_rec Coq_nil (fun pc nodes ->
-!     match Maps.PMap.get pc reach with
-        | true -> Coq_cons (pc, nodes)
-        | false -> nodes) (coq_Psucc f.fn_entrypoint)
-  
diff --git a/extraction/Makefile b/extraction/Makefile
index 4274e8e1..513577c0 100644
--- a/extraction/Makefile
+++ b/extraction/Makefile
@@ -23,7 +23,7 @@ FILES=\
   LTL.ml LTLin.ml \
   InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \
   Allocation.ml  \
-  Tunneling.ml Linear.ml Linearize.ml \
+  Tunneling.ml Linear.ml ../caml/Linearizeaux.ml Linearize.ml \
   Parallelmove.ml Reload.ml \
   Mach.ml Bounds.ml Stacking.ml \
   PPC.ml PPCgen.ml \
diff --git a/extraction/extraction.v b/extraction/extraction.v
index cc33c981..e0f965d7 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -47,6 +47,9 @@ Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_en
 (* Coloring *)
 Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring".
 
+(* Linearize *)
+Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
+
 (* PPC *)
 Extract Constant PPC.low_half_signed => "fun _ -> assert false".
 Extract Constant PPC.high_half_signed => "fun _ -> assert false".