Cil2Csyntax: added goto and labels; added assignment between structs

Kildall: simplified the interface
Constprop, CSE, Allocation, Linearize: updated for the new Kildall
RTL, LTL: removed the well-formedness condition on the CFG, 
  it is no longer necessary with the new Kildall and it is problematic
  for validated optimizations.
Maps: more efficient implementation of PTree.fold.


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

24 files changed, 608 insertions, 523 deletions

diff --git a/arm/Constprop.v b/arm/Constprop.v
index 5bd84b6..154a5fc 100644
--- a/arm/Constprop.v
+++ b/arm/Constprop.v
@@ -702,7 +702,7 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
 Module DS := Dataflow_Solver(D)(NodeSetForward).
 
 Definition analyze (f: RTL.function): PMap.t D.t :=
-  match DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) 
+  match DS.fixpoint (successors f) (transfer f) 
                     ((f.(fn_entrypoint), D.top) :: nil) with
   | None => PMap.init D.top
   | Some res => res
@@ -1219,19 +1219,6 @@ Definition transf_instr (approx: D.t) (instr: instruction) :=
 Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code :=
   PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
 
-Lemma transf_code_wf:
-  forall f approxs,
-  (forall pc, Plt pc f.(fn_nextpc) \/ f.(fn_code)!pc = None) ->
-  (forall pc, Plt pc f.(fn_nextpc)
-      \/ (transf_code approxs f.(fn_code))!pc = None).
-Proof.
-  intros. 
-  elim (H pc); intro.
-  left; auto.
-  right. unfold transf_code. rewrite PTree.gmap. 
-  unfold option_map; rewrite H0. reflexivity.
-Qed.
-
 Definition transf_function (f: function) : function :=
   let approxs := analyze f in
   mkfunction
@@ -1239,9 +1226,7 @@ Definition transf_function (f: function) : function :=
     f.(fn_params)
     f.(fn_stacksize)
     (transf_code approxs f.(fn_code))
-    f.(fn_entrypoint)
-    f.(fn_nextpc)
-    (transf_code_wf f approxs f.(fn_code_wf)).
+    f.(fn_entrypoint).
 
 Definition transf_fundef (fd: fundef) : fundef :=
   AST.transf_fundef transf_function fd.
diff --git a/arm/Constpropproof.v b/arm/Constpropproof.v
index 08c5baf..a3e2b82 100644
--- a/arm/Constpropproof.v
+++ b/arm/Constpropproof.v
@@ -213,19 +213,19 @@ Qed.
   a solution of the forward dataflow inequations. *)
 
 Lemma analyze_correct_1:
-  forall f pc rs pc',
-  In pc' (successors f pc) ->
+  forall f pc rs pc' i,
+  f.(fn_code)!pc = Some i ->
+  In pc' (successors_instr i) ->
   regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
   regs_match_approx (analyze f)!!pc' rs.
 Proof.
-  intros until pc'. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (fn_nextpc f) (transfer f)
+  intros until i. unfold analyze. 
+  caseEq (DS.fixpoint (successors f) (transfer f)
                       ((fn_entrypoint f, D.top) :: nil)).
   intros approxs; intros.
   apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
   eapply DS.fixpoint_solution; eauto.
-  elim (fn_code_wf f pc); intro. auto. 
-  unfold successors in H0; rewrite H2 in H0; simpl; contradiction.
+  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
   auto.
   intros. rewrite PMap.gi. apply regs_match_approx_top. 
 Qed.
@@ -235,7 +235,7 @@ Lemma analyze_correct_3:
   regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
 Proof.
   intros. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (fn_nextpc f) (transfer f)
+  caseEq (DS.fixpoint (successors f) (transfer f)
                       ((fn_entrypoint f, D.top) :: nil)).
   intros approxs; intros.
   apply regs_match_approx_increasing with D.top.
@@ -772,7 +772,7 @@ Proof.
   TransfInstr; intro. eapply exec_Inop; eauto.
   econstructor; eauto.
   eapply analyze_correct_1 with (pc := pc); eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  simpl; auto.
   unfold transfer; rewrite H. auto.
 
   (* Iop *)
@@ -796,7 +796,7 @@ Proof.
   rewrite A; rewrite B; auto.
   econstructor; eauto. 
   eapply analyze_correct_1 with (pc := pc); eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  simpl; auto.
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. 
   eapply eval_static_operation_correct; eauto.
@@ -814,8 +814,7 @@ Proof.
   exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split.
   eapply exec_Iload; eauto.
   econstructor; eauto. 
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. simpl; auto.
 
@@ -831,8 +830,7 @@ Proof.
   exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split.
   eapply exec_Istore; eauto.
   econstructor; eauto. 
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. auto. 
 
   (* Icall *)
@@ -842,8 +840,7 @@ Proof.
   eapply exec_Icall; eauto. apply sig_function_translated; auto.
   constructor; auto. constructor; auto.
   econstructor; eauto. 
-  intros. apply analyze_correct_1 with pc; auto.
-  unfold successors; rewrite H; auto with coqlib.
+  intros. eapply analyze_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H.
   apply regs_match_approx_update; auto. simpl. auto.
 
@@ -852,7 +849,7 @@ Proof.
   TransfInstr; intro.
   econstructor; split.
   eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
-  constructor; auto.
+  constructor; auto. 
 
   (* Icond, true *)
   exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. 
@@ -870,8 +867,8 @@ Proof.
   replace b with true. intro; eapply exec_Inop; eauto. congruence.
   intros. eapply exec_Icond_true; eauto.
   econstructor; eauto.
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto.
+  simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Icond, false *)
@@ -890,8 +887,8 @@ Proof.
   replace b with false. intro; eapply exec_Inop; eauto. congruence.
   intros. eapply exec_Icond_false; eauto.
   econstructor; eauto.
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto.
+  simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Ireturn *)
diff --git a/backend/Allocation.v b/backend/Allocation.v
index 2389a33..7d843e5 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -116,7 +116,7 @@ Module RegsetLat := LFSet(Regset).
 Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward).
 
 Definition analyze (f: RTL.function): option (PMap.t Regset.t) :=
-  DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) nil.
+  DS.fixpoint (successors f)  (transfer f) nil.
 
 (** * Translation from RTL to LTL *)
 
@@ -171,16 +171,6 @@ Definition transf_instr
       Lreturn (option_map assign optarg)
   end.
 
-Lemma transf_body_wf:
-  forall (f: RTL.function) (live: PMap.t Regset.t) (assign: reg -> loc),
-  let tc := PTree.map (transf_instr f live assign) (RTL.fn_code f) in
-  forall (pc: node), Plt pc (RTL.fn_nextpc f) \/ tc!pc = None.
-Proof.
-  intros. elim (RTL.fn_code_wf f pc); intro.
-  left. auto. right. unfold tc. rewrite PTree.gmap.
-  unfold option_map. rewrite H. auto.
-Qed.
-
 Definition transf_fun (f: RTL.function) (live: PMap.t Regset.t)
                       (assign: reg -> loc) : LTL.function :=
   LTL.mkfunction
@@ -188,9 +178,7 @@ Definition transf_fun (f: RTL.function) (live: PMap.t Regset.t)
      (List.map assign (RTL.fn_params f))
      (RTL.fn_stacksize f)
      (PTree.map (transf_instr f live assign) (RTL.fn_code f))
-     (RTL.fn_entrypoint f)
-     (RTL.fn_nextpc f)
-     (transf_body_wf f live assign).
+     (RTL.fn_entrypoint f).
 
 (** The translation of a function performs liveness analysis,
   construction and coloring of the inference graph, and per-instruction
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 7e9334a..fc0a0f3 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -154,21 +154,19 @@ Proof.
 Qed.
 
 Lemma agree_succ:
-  forall n s rs ls live,
+  forall n s rs ls live i,
   analyze f = Some live ->
-  In s (RTL.successors f n) ->
+  f.(RTL.fn_code)!n = Some i ->
+  In s (RTL.successors_instr i) ->
   agree live!!n rs ls ->
   agree (transfer f s live!!s) rs ls.
 Proof.
   intros.
-  elim (RTL.fn_code_wf f n); intro.
-  elim (RTL.fn_code_wf f s); intro.
   apply agree_increasing with (live!!n).
   eapply DS.fixpoint_solution. unfold analyze in H; eauto.
-  auto. auto. auto. auto.
-  unfold transfer. rewrite H3.
-  red; intros. elim (Regset.empty_1 H4).
-  unfold RTL.successors in H0; rewrite H2 in H0; elim H0.
+  unfold RTL.successors, Kildall.successors_list. 
+  rewrite PTree.gmap. rewrite H0. simpl. auto.
+  auto.
 Qed.
 
 (** Some useful special cases of [agree_increasing]. *)
@@ -543,12 +541,11 @@ Ltac MatchStates :=
       eapply match_states_intro; eauto; MatchStates
   | H: (PTree.get ?pc _ = Some _) |- agree _ _ _ _ =>
       eapply agree_succ with (n := pc); eauto; MatchStates
-  | H: (PTree.get _ _ = Some _) |- In _ (RTL.successors _ _) =>
-      unfold RTL.successors; rewrite H; auto with coqlib
+  | |- In _ (RTL.successors_instr _) =>
+      unfold RTL.successors_instr; auto with coqlib
   | _ => idtac
   end.
 
-
 Lemma transl_find_function:
   forall ros f args lv rs ls alloc,
   RTL.find_function ge ros rs = Some f ->
@@ -659,7 +656,7 @@ Proof.
   econstructor; eauto.
   econstructor; eauto.
   intros. eapply agree_succ with (n := pc); eauto.
-  unfold RTL.successors; rewrite H; auto with coqlib.
+  simpl. auto.
   eapply agree_postcall; eauto.
 
   (* Itailcall *)
diff --git a/backend/CSE.v b/backend/CSE.v
index cad3503..ff8d41a 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -364,8 +364,7 @@ Definition transfer (f: function) (pc: node) (before: numbering) :=
   and effectively deactivates the CSE optimization. *)
 
 Definition analyze (f: RTL.function): PMap.t numbering :=
-  match Solver.fixpoint (successors f) f.(fn_nextpc) 
-                        (transfer f) f.(fn_entrypoint) with
+  match Solver.fixpoint (successors f) (transfer f) f.(fn_entrypoint) with
   | None => PMap.init empty_numbering
   | Some res => res
   end.
@@ -410,19 +409,6 @@ Definition transf_instr (n: numbering) (instr: instruction) :=
 Definition transf_code (approxs: PMap.t numbering) (instrs: code) : code :=
   PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
 
-Lemma transf_code_wf:
-  forall f approxs,
-  (forall pc, Plt pc f.(fn_nextpc) \/ f.(fn_code)!pc = None) ->
-  (forall pc, Plt pc f.(fn_nextpc)
-      \/ (transf_code approxs f.(fn_code))!pc = None).
-Proof.
-  intros. 
-  elim (H pc); intro.
-  left; auto.
-  right. unfold transf_code. rewrite PTree.gmap. 
-  unfold option_map; rewrite H0. reflexivity.
-Qed.
-
 Definition transf_function (f: function) : function :=
   let approxs := analyze f in
   mkfunction
@@ -430,9 +416,7 @@ Definition transf_function (f: function) : function :=
         f.(fn_params)
         f.(fn_stacksize)
         (transf_code approxs f.(fn_code))
-        f.(fn_entrypoint)
-        f.(fn_nextpc)
-        (transf_code_wf f approxs f.(fn_code_wf)).
+        f.(fn_entrypoint).
 
 Definition transf_fundef (f: fundef) : fundef :=
   AST.transf_fundef transf_function f.
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 3751cec..14027bf 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -242,8 +242,7 @@ Theorem wf_analyze:
   forall f pc, wf_numbering (analyze f)!!pc.
 Proof.
   unfold analyze; intros.
-  caseEq (Solver.fixpoint (successors f) (fn_nextpc f) 
-                          (transfer f) (fn_entrypoint f)).
+  caseEq (Solver.fixpoint (successors f) (transfer f) (fn_entrypoint f)).
   intros approx EQ.
   eapply Solver.fixpoint_invariant with (P := wf_numbering); eauto.
   exact wf_empty_numbering.   
@@ -689,22 +688,21 @@ End SATISFIABILITY.
   satisfiability at [pc']. *)
 
 Theorem analysis_correct_1:
-  forall ge sp rs m f pc pc',
-  In pc' (successors f pc) ->
+  forall ge sp rs m f pc pc' i,
+  f.(fn_code)!pc = Some i -> In pc' (successors_instr i) ->
   numbering_satisfiable ge sp rs m (transfer f pc (analyze f)!!pc) ->
   numbering_satisfiable ge sp rs m (analyze f)!!pc'.
 Proof.
-  intros until pc'.
+  intros until i.
   generalize (wf_analyze f pc).
   unfold analyze.
-  caseEq (Solver.fixpoint (successors f) (fn_nextpc f) 
-                          (transfer f) (fn_entrypoint f)).
-  intros res FIXPOINT WF SUCC NS.
+  caseEq (Solver.fixpoint (successors f) (transfer f) (fn_entrypoint f)).
+  intros res FIXPOINT WF AT SUCC.
   assert (Numbering.ge res!!pc' (transfer f pc res!!pc)).
     eapply Solver.fixpoint_solution; eauto.
-    elim (fn_code_wf f pc); intro. auto.
-    unfold successors in SUCC; rewrite H in SUCC; contradiction.
-  apply H. auto.
+    unfold successors_list, successors. rewrite PTree.gmap.
+    rewrite AT. auto.
+  apply H.
   intros. rewrite PMap.gi. apply empty_numbering_satisfiable.
 Qed.
 
@@ -717,8 +715,7 @@ Proof.
           with empty_numbering.
   apply empty_numbering_satisfiable.
   unfold analyze.
-  caseEq (Solver.fixpoint (successors f) (fn_nextpc f) 
-                          (transfer f) (fn_entrypoint f)).
+  caseEq (Solver.fixpoint (successors f) (transfer f) (fn_entrypoint f)).
   intros res FIXPOINT. 
   symmetry. change empty_numbering with Solver.L.top.
   eapply Solver.fixpoint_entry; eauto.
@@ -835,8 +832,7 @@ Proof.
   exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split.
   apply exec_Inop; auto.
   econstructor; eauto. 
-  apply analysis_correct_1 with pc. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H; auto.
 
   (* Iop *)
@@ -854,8 +850,7 @@ Proof.
   congruence.
   intros. eapply exec_Iop'; eauto.
   econstructor; eauto.
-  apply analysis_correct_1 with pc.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H. 
   eapply add_op_satisfiable; eauto. apply wf_analyze.
 
@@ -874,8 +869,7 @@ Proof.
   congruence.
   intros. eapply exec_Iload'; eauto.
   econstructor; eauto.
-  apply analysis_correct_1 with pc.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   eapply add_load_satisfiable; eauto. apply wf_analyze.
 
@@ -885,8 +879,7 @@ Proof.
     rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Istore; eauto.
   econstructor; eauto.
-  apply analysis_correct_1 with pc. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H.
   eapply kill_load_satisfiable; eauto. 
 
@@ -898,8 +891,7 @@ Proof.
   econstructor; eauto. 
   constructor; auto. 
   econstructor; eauto. 
-  intros. apply analysis_correct_1 with pc.
-  unfold successors; rewrite H; auto with coqlib.
+  intros. eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   apply empty_numbering_satisfiable.
 
@@ -914,16 +906,14 @@ Proof.
   econstructor; split.
   eapply exec_Icond_true; eauto. 
   econstructor; eauto.
-  apply analysis_correct_1 with pc. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Icond false *)
   econstructor; split.
   eapply exec_Icond_false; eauto. 
   econstructor; eauto.
-  apply analysis_correct_1 with pc. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Ireturn *)
diff --git a/backend/Kildall.v b/backend/Kildall.v
index 188a23f..83206f7 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -55,6 +55,11 @@ approximations do not exist or are too expensive to compute. *)
 
 (** * Solving forward dataflow problems using Kildall's algorithm *)
 
+Definition successors_list (successors: PTree.t (list positive)) (pc: positive) : list positive :=
+  match successors!pc with None => nil | Some l => l end.
+
+Notation "a !!! b" := (successors_list a b) (at level 1).
+
 (** A forward dataflow solver has the following generic interface.
   Unknowns range over the type [L.t], which is equipped with
   semi-lattice operations (see file [Lattice]).  *)
@@ -64,32 +69,30 @@ Module Type DATAFLOW_SOLVER.
   Declare Module L: SEMILATTICE.
 
   Variable fixpoint:
-    (positive -> list positive) ->
-    positive ->
-    (positive -> L.t -> L.t) ->
-    list (positive * L.t) ->
+    forall (successors: PTree.t (list positive))
+           (transf: positive -> L.t -> L.t)
+           (entrypoints: list (positive * L.t)),
     option (PMap.t L.t).
 
-  (** [fixpoint successors topnode transf entrypoints] is the solver.
+  (** [fixpoint successors transf entrypoints] is the solver.
     It returns either an error or a mapping from program points to
     values of type [L.t] representing the solution.  [successors]
-    is a function returning the list of successors of the given program
-    point.  [topnode] is the maximal number of nodes considered.
-    [transf] is the transfer function, and [entrypoints] the additional
+    is a finite map returning the list of successors of the given program
+    point. [transf] is the transfer function, and [entrypoints] the additional
     constraints imposed on the solution. *)
 
   Hypothesis fixpoint_solution:
-    forall successors topnode transf entrypoints res n s,
-    fixpoint successors topnode transf entrypoints = Some res ->
-    Plt n topnode -> In s (successors n) ->
+    forall successors transf entrypoints res n s,
+    fixpoint successors transf entrypoints = Some res ->
+    In s successors!!!n ->
     L.ge res!!s (transf n res!!n).
 
   (** The [fixpoint_solution] theorem shows that the returned solution,
     if any, satisfies the dataflow inequations. *)
 
   Hypothesis fixpoint_entry:
-    forall successors topnode transf entrypoints res n v,
-    fixpoint successors topnode transf entrypoints = Some res ->
+    forall successors transf entrypoints res n v,
+    fixpoint successors transf entrypoints = Some res ->
     In (n, v) entrypoints ->
     L.ge res!!n v.
 
@@ -97,6 +100,21 @@ Module Type DATAFLOW_SOLVER.
     if any, satisfies the additional constraints expressed 
     by [entrypoints]. *)
 
+  Hypothesis fixpoint_invariant:
+    forall successors transf entrypoints 
+           (P: L.t -> Prop),
+    P L.bot ->
+    (forall x y, P x -> P y -> P (L.lub x y)) ->
+    (forall pc x, P x -> P (transf pc x)) ->
+    (forall n v, In (n, v) entrypoints -> P v) ->
+    forall res pc,
+    fixpoint successors transf entrypoints = Some res ->
+    P res!!pc.
+
+  (** Finally, any property that is preserved by [L.lub] and [transf]
+      and that holds for [L.bot] also holds for the results of
+      the analysis. *)
+
 End DATAFLOW_SOLVER.
 
 (** Kildall's algorithm manipulates worklists, which are sets of CFG nodes
@@ -111,7 +129,7 @@ Module Type NODE_SET.
   Variable t: Type.
   Variable add: positive -> t -> t.
   Variable pick: t -> option (positive * t).
-  Variable initial: positive -> t.
+  Variable initial: PTree.t (list positive) -> t.
 
   Variable In: positive -> t -> Prop.
   Hypothesis add_spec:
@@ -122,7 +140,8 @@ Module Type NODE_SET.
     forall s n s', pick s = Some(n, s') ->
     forall n', In n' s <-> n = n' \/ In n' s'.
   Hypothesis initial_spec:
-    forall numnodes n, Plt n numnodes -> In n (initial numnodes).
+    forall successors n s,
+    successors!n = Some s -> In n (initial successors).
 
 End NODE_SET.
 
@@ -136,8 +155,7 @@ Module L := LAT.
 
 Section Kildall.
 
-Variable successors: positive -> list positive.
-Variable topnode: positive.
+Variable successors: PTree.t (list positive).
 Variable transf: positive -> L.t -> L.t.
 Variable entrypoints: list (positive * L.t).
 
@@ -172,7 +190,7 @@ The initial state is built as follows:
   the associated approximation as initial value.  Since a program
   point can be mentioned several times in [entrypoints], with different
   approximations, we actually take the l.u.b. of these approximations.
-- The initial worklist contains all the program points up to [topnode]. *)
+- The initial worklist contains all the program points. *)
 
 Fixpoint start_state_in (ep: list (positive * L.t)) : PMap.t L.t :=
   match ep with
@@ -183,7 +201,7 @@ Fixpoint start_state_in (ep: list (positive * L.t)) : PMap.t L.t :=
   end.
 
 Definition start_state :=
-  mkstate (start_state_in entrypoints) (NS.initial topnode).
+  mkstate (start_state_in entrypoints) (NS.initial successors).
 
 (** [propagate_succ] corresponds, in the pseudocode,
   to the body of the [for] loop iterating over all successors. *)
@@ -216,7 +234,7 @@ Definition step (s: state) : PMap.t L.t + state :=
       inr _ (propagate_succ_list
               (mkstate s.(st_in) rem)
               (transf n s.(st_in)!!n)
-              (successors n))
+              (successors!!!n))
   end.
 
 (** The whole fixpoint computation is the iteration of [step] from
@@ -259,10 +277,10 @@ Proof.
 Qed.
 
 Lemma propagate_succ_list_incr:
-  forall out succs st,
-  in_incr st.(st_in) (propagate_succ_list st out succs).(st_in).
+  forall out scs st,
+  in_incr st.(st_in) (propagate_succ_list st out scs).(st_in).
 Proof.
-  induction succs; simpl; intros.
+  induction scs; simpl; intros.
   apply in_incr_refl.
   apply in_incr_trans with (propagate_succ st out a).(st_in). 
   apply propagate_succ_incr. auto.
@@ -291,7 +309,7 @@ Qed.
 (** ** Correctness invariant *)
 
 (** The following invariant is preserved at each iteration of Kildall's
-  algorithm: for all program points [n] below [topnode], either
+  algorithm: for all program points [n], either
   [n] is in the worklist, or the inequations associated with [n]
   ([st_in[s] >= transf n st_in[n]] for all successors [s] of [n])
   hold.  In other terms, the worklist contains all nodes that do not
@@ -299,10 +317,9 @@ Qed.
 
 Definition good_state (st: state) : Prop :=
   forall n,
-  Plt n topnode ->
   NS.In n st.(st_wrk) \/
-  (forall s, In s (successors n) -> 
-                L.ge st.(st_in)!!s (transf n st.(st_in)!!n)).
+  (forall s, In s (successors!!!n) ->
+             L.ge st.(st_in)!!s (transf n st.(st_in)!!n)).
 
 (** We show that the start state satisfies the invariant, and that
   the [step] function preserves it. *)
@@ -311,7 +328,9 @@ Lemma start_state_good:
   good_state start_state.
 Proof.
   unfold good_state, start_state; intros.
-  left; simpl. apply NS.initial_spec. auto.
+  case_eq (successors!n); intros.
+  left; simpl. eapply NS.initial_spec. eauto.
+  unfold successors_list. rewrite H. right; intros. contradiction.
 Qed.
 
 Lemma propagate_succ_charact:
@@ -337,15 +356,15 @@ Proof.
 Qed.
 
 Lemma propagate_succ_list_charact:
-  forall out succs st,
-  let st' := propagate_succ_list st out succs in
+  forall out scs st,
+  let st' := propagate_succ_list st out scs in
   forall s,
-  (In s succs -> L.ge st'.(st_in)!!s out) /\
-  (~(In s succs) -> st'.(st_in)!!s = st.(st_in)!!s).
+  (In s scs -> L.ge st'.(st_in)!!s out) /\
+  (~(In s scs) -> st'.(st_in)!!s = st.(st_in)!!s).
 Proof.
-  induction succs; simpl; intros.
+  induction scs; simpl; intros.
   tauto.
-  generalize (IHsuccs (propagate_succ st out a) s). intros [A B].
+  generalize (IHscs (propagate_succ st out a) s). intros [A B].
   generalize (propagate_succ_charact st out a). intros [C D].
   split; intros.
   elim H; intro.
@@ -369,12 +388,12 @@ Proof.
 Qed.
 
 Lemma propagate_succ_list_incr_worklist:
-  forall out succs st x,
-  NS.In x st.(st_wrk) -> NS.In x (propagate_succ_list st out succs).(st_wrk).
+  forall out scs st x,
+  NS.In x st.(st_wrk) -> NS.In x (propagate_succ_list st out scs).(st_wrk).
 Proof.
-  induction succs; simpl; intros.
+  induction scs; simpl; intros.
   auto.
-  apply IHsuccs. apply propagate_succ_incr_worklist. auto.
+  apply IHscs. apply propagate_succ_incr_worklist. auto.
 Qed.
 
 Lemma propagate_succ_records_changes:
@@ -391,11 +410,11 @@ Proof.
 Qed.
 
 Lemma propagate_succ_list_records_changes:
-  forall out succs st s,
-  let st' := propagate_succ_list st out succs in
+  forall out scs st s,
+  let st' := propagate_succ_list st out scs in
   NS.In s st'.(st_wrk) \/ st'.(st_in)!!s = st.(st_in)!!s.
 Proof.
-  induction succs; simpl; intros.
+  induction scs; simpl; intros.
   right; auto.
   elim (propagate_succ_records_changes st out a s); intro.
   left. apply propagate_succ_list_incr_worklist. auto.
@@ -408,37 +427,37 @@ Lemma step_state_good:
   good_state st ->
   good_state (propagate_succ_list (mkstate st.(st_in) rem)
                                   (transf n st.(st_in)!!n)
-                                  (successors n)).
+                                  (successors!!!n)).
 Proof.
-  unfold good_state. intros st n rem WKL GOOD x LTx.
+  unfold good_state. intros st n rem WKL GOOD x.
   generalize (NS.pick_some _ _ _ WKL); intro PICK.
   set (out := transf n st.(st_in)!!n).
   elim (propagate_succ_list_records_changes 
-          out (successors n) (mkstate st.(st_in) rem) x).
+          out (successors!!!n) (mkstate st.(st_in) rem) x).
   intro; left; auto.
-  simpl; intro EQ. rewrite EQ.
+  simpl; intros EQ. rewrite EQ.
   (* Case 1: x = n *)
   case (peq x n); intro.
-  subst x. fold out.
+  subst x.
   right; intros.
-  elim (propagate_succ_list_charact out (successors n)
+  elim (propagate_succ_list_charact out (successors!!!n)
           (mkstate st.(st_in) rem) s); intros.
   auto.
   (* Case 2: x <> n *)
-  elim (GOOD x LTx); intro.
+  elim (GOOD x); intro.
   (* Case 2.1: x was already in worklist, still is *)
   left. apply propagate_succ_list_incr_worklist.
   simpl. rewrite PICK in H. elim H; intro. congruence. auto.
   (* Case 2.2: x was not in worklist *)
   right; intros.
-  case (In_dec peq s (successors n)); intro.
+  case (In_dec peq s (successors!!!n)); intro.
   (* Case 2.2.1: s is a successor of n, it may have increased *)
   apply L.ge_trans with st.(st_in)!!s.
   change st.(st_in)!!s with (mkstate st.(st_in) rem).(st_in)!!s.
   apply propagate_succ_list_incr. 
   auto.
   (* Case 2.2.2: s is not a successor of n, it did not change *)
-  elim (propagate_succ_list_charact out (successors n)
+  elim (propagate_succ_list_charact out (successors!!!n)
           (mkstate st.(st_in) rem) s); intros.
   rewrite H2. simpl. auto. auto.
 Qed.
@@ -452,23 +471,25 @@ Qed.
 Theorem fixpoint_solution:
   forall res n s,
   fixpoint = Some res ->
-  Plt n topnode -> In s (successors n) ->
+  In s (successors!!!n) ->
   L.ge res!!s (transf n res!!n).
 Proof.
   assert (forall res, fixpoint = Some res ->
-          forall n s, Plt n topnode -> In s (successors n) ->
-                      L.ge res!!s (transf n res!!n)).
+          forall n s,
+          In s successors!!!n ->
+          L.ge res!!s (transf n res!!n)).
   unfold fixpoint. intros res PI. pattern res. 
   eapply (PrimIter.iterate_prop _ _ step good_state).
 
   intros st GOOD. unfold step. 
   caseEq (NS.pick st.(st_wrk)). 
   intros [n rem] PICK. apply step_state_good; auto. 
-  intros. elim (GOOD n H0); intro. 
+  intros. 
+  elim (GOOD n); intro. 
   elim (NS.pick_none _ n H). auto.
   auto.
 
-  eauto. apply start_state_good. auto.
+  eauto. apply start_state_good. eauto.
 Qed.
 
 (** As a consequence of the monotonicity property, the result of
@@ -505,6 +526,49 @@ Proof.
   apply start_state_in_entry. auto.
 Qed.
 
+(** ** Preservation of a property over solutions *)
+
+Variable P: L.t -> Prop.
+Hypothesis P_bot: P L.bot.
+Hypothesis P_lub: forall x y, P x -> P y -> P (L.lub x y).
+Hypothesis P_transf: forall pc x, P x -> P (transf pc x).
+Hypothesis P_entrypoints: forall n v, In (n, v) entrypoints -> P v.
+
+Theorem fixpoint_invariant:
+  forall res pc,
+  fixpoint = Some res ->
+  P res!!pc.
+Proof.
+  assert (forall ep,
+          (forall n v, In (n, v) ep -> P v) ->
+          forall pc, P (start_state_in ep)!!pc).
+    induction ep; intros; simpl.
+    rewrite PMap.gi. auto.
+    simpl in H.
+    assert (P (start_state_in ep)!!pc). apply IHep. eauto.  
+    destruct a as [n v]. rewrite PMap.gsspec. destruct (peq pc n).
+    apply P_lub. subst. auto. eapply H. left; reflexivity. auto.
+  set (inv := fun st => forall pc, P (st.(st_in)!!pc)).
+  assert (forall st v n, inv st -> P v -> inv (propagate_succ st v n)).
+    unfold inv, propagate_succ. intros. 
+    destruct (LAT.beq (st_in st)!!n (LAT.lub (st_in st)!!n v)).
+    auto. simpl. rewrite PMap.gsspec. destruct (peq pc n). 
+    apply P_lub. subst n; auto. auto.
+    auto.
+  assert (forall l st v, inv st -> P v -> inv (propagate_succ_list st v l)).
+    induction l; intros; simpl. auto.
+    apply IHl; auto.
+  assert (forall res, fixpoint = Some res -> forall pc, P res!!pc).
+    unfold fixpoint. intros res0 RES0. pattern res0.
+    eapply (PrimIter.iterate_prop _ _ step inv).
+    intros. unfold step. destruct (NS.pick (st_wrk a)) as [[n rem] | ].
+    apply H1. auto. apply P_transf. apply H2.
+    assumption.
+    eauto. 
+    unfold inv, start_state; simpl. auto. 
+  intros. auto.
+Qed.
+
 End Kildall.
 
 End Dataflow_Solver.
@@ -520,51 +584,53 @@ End Dataflow_Solver.
 
 Section Predecessor.
 
-Variable successors: positive -> list positive.
-Variable topnode: positive.
+Variable successors: PTree.t (list positive).
 
-Fixpoint add_successors (pred: PMap.t (list positive))
+Fixpoint add_successors (pred: PTree.t (list positive))
                         (from: positive) (tolist: list positive)
-                        {struct tolist} : PMap.t (list positive) :=
+                        {struct tolist} : PTree.t (list positive) :=
   match tolist with
   | nil => pred
-  | to :: rem =>
-      add_successors (PMap.set to (from :: pred!!to) pred) from rem
+  | to :: rem => add_successors (PTree.set to (from :: pred!!!to) pred) from rem
   end.
 
 Lemma add_successors_correct:
   forall tolist from pred n s,
-  In n pred!!s \/ (n = from /\ In s tolist) -> 
-  In n (add_successors pred from tolist)!!s.
+  In n pred!!!s \/ (n = from /\ In s tolist) -> 
+  In n (add_successors pred from tolist)!!!s.
 Proof.
   induction tolist; simpl; intros.
   tauto.
   apply IHtolist.
-  rewrite PMap.gsspec. case (peq s a); intro.
-  subst a. elim H; intro. left; auto with coqlib.
-  elim H0; intros. subst n. left; auto with coqlib.
-  intuition. elim n0; auto.
+  unfold successors_list at 1. rewrite PTree.gsspec. destruct (peq s a).
+  subst a. destruct H. auto with coqlib. 
+  destruct H. subst n. auto with coqlib. 
+  fold (successors_list pred s). intuition congruence.
 Qed.
 
-Definition make_predecessors : PMap.t (list positive) :=
-  positive_rec (PMap.t (list positive)) (PMap.init nil)
-    (fun n pred => add_successors pred n (successors n))
-    topnode.
+Definition make_predecessors : PTree.t (list positive) :=
+  PTree.fold add_successors successors (PTree.empty (list positive)).
 
 Lemma make_predecessors_correct:
   forall n s,
-  Plt n topnode ->
-  In s (successors n) ->
-  In n make_predecessors!!s.
+  In s successors!!!n ->
+  In n make_predecessors!!!s.
 Proof.
-  unfold make_predecessors. pattern topnode. 
-  apply positive_Peano_ind; intros.
-  compute in H. destruct n; discriminate.
-  rewrite positive_rec_succ.
-  apply add_successors_correct.
-  elim (Plt_succ_inv _ _ H0); intro.
-  left; auto.
-  right. subst x. tauto.
+  set (P := fun succ pred =>
+          forall n s, In s succ!!!n -> In n pred!!!s).
+  unfold make_predecessors.
+  apply PTree_Properties.fold_rec with (P := P).
+(* extensionality *)
+  unfold P; unfold successors_list; intros.
+  rewrite <- H in H1. auto.
+(* base case *)
+  red; unfold successors_list. intros n s. repeat rewrite PTree.gempty. auto.
+(* inductive case *)
+  unfold P; intros. apply add_successors_correct.
+  unfold successors_list in H2. rewrite PTree.gsspec in H2. 
+  destruct (peq n k).
+  subst k. auto.
+  fold (successors_list m n) in H2. auto.
 Qed.
 
 End Predecessor.
@@ -578,24 +644,33 @@ Module Type BACKWARD_DATAFLOW_SOLVER.
   Declare Module L: SEMILATTICE.
 
   Variable fixpoint:
-    (positive -> list positive) ->
-    positive ->
+    PTree.t (list positive) ->
     (positive -> L.t -> L.t) ->
     list (positive * L.t) ->
     option (PMap.t L.t).
 
   Hypothesis fixpoint_solution:
-    forall successors topnode transf entrypoints res n s,
-    fixpoint successors topnode transf entrypoints = Some res ->
-    Plt n topnode -> Plt s topnode -> In s (successors n) ->
+    forall successors transf entrypoints res n s,
+    fixpoint successors transf entrypoints = Some res ->
+    In s (successors!!!n) ->
     L.ge res!!n (transf s res!!s).
 
   Hypothesis fixpoint_entry:
-    forall successors topnode transf entrypoints res n v,
-    fixpoint successors topnode transf entrypoints = Some res ->
+    forall successors transf entrypoints res n v,
+    fixpoint successors transf entrypoints = Some res ->
     In (n, v) entrypoints ->
     L.ge res!!n v.
 
+  Hypothesis fixpoint_invariant:
+    forall successors transf entrypoints (P: L.t -> Prop),
+    P L.bot ->
+    (forall x y, P x -> P y -> P (L.lub x y)) ->
+    (forall pc x, P x -> P (transf pc x)) ->
+    (forall n v, In (n, v) entrypoints -> P v) ->
+    forall res pc,
+    fixpoint successors transf entrypoints = Some res ->
+    P res!!pc.
+
 End BACKWARD_DATAFLOW_SOLVER.
 
 (** We construct a generic backward dataflow solver, working over any
@@ -611,26 +686,22 @@ Module DS := Dataflow_Solver L NS.
 
 Section Kildall.
 
-Variable successors: positive -> list positive.
-Variable topnode: positive.
+Variable successors: PTree.t (list positive).
 Variable transf: positive -> L.t -> L.t.
 Variable entrypoints: list (positive * L.t).
 
 Definition fixpoint :=
-  let pred := make_predecessors successors topnode in
-  DS.fixpoint (fun s => pred!!s) topnode transf entrypoints.
+  DS.fixpoint (make_predecessors successors) transf entrypoints.
 
 Theorem fixpoint_solution:
   forall res n s,
   fixpoint = Some res ->
-  Plt n topnode -> Plt s topnode ->
-  In s (successors n) ->
+  In s (successors!!!n) ->
   L.ge res!!n (transf s res!!s).
 Proof.
   intros. apply DS.fixpoint_solution with
-    (fun s => (make_predecessors successors topnode)!!s) topnode entrypoints.
+    (make_predecessors successors) entrypoints.
   exact H.
-  assumption.
   apply make_predecessors_correct; auto.
 Qed.
 
@@ -641,10 +712,24 @@ Theorem fixpoint_entry:
   L.ge res!!n v.
 Proof.
   intros. apply DS.fixpoint_entry with
-    (fun s => (make_predecessors successors topnode)!!s) topnode transf entrypoints.
+    (make_predecessors successors) transf entrypoints.
   exact H. auto.
 Qed.
 
+Theorem fixpoint_invariant:
+  forall (P: L.t -> Prop),
+  P L.bot ->
+  (forall x y, P x -> P y -> P (L.lub x y)) ->
+  (forall pc x, P x -> P (transf pc x)) ->
+  (forall n v, In (n, v) entrypoints -> P v) ->
+  forall res pc,
+  fixpoint = Some res ->
+  P res!!pc.
+Proof.
+  intros. apply DS.fixpoint_invariant with 
+    (make_predecessors successors) transf entrypoints; auto. 
+Qed.
+
 End Kildall.
 
 End Backward_Dataflow_Solver.
@@ -681,30 +766,29 @@ Module Type BBLOCK_SOLVER.
   Declare Module L: ORDERED_TYPE_WITH_TOP.
 
   Variable fixpoint:
-    (positive -> list positive) ->
-    positive ->
+    PTree.t (list positive) ->
     (positive -> L.t -> L.t) ->
     positive ->
     option (PMap.t L.t).
 
   Hypothesis fixpoint_solution:
-    forall successors topnode transf entrypoint res n s,
-    fixpoint successors topnode transf entrypoint = Some res ->
-    Plt n topnode -> In s (successors n) ->
+    forall successors transf entrypoint res n s,
+    fixpoint successors transf entrypoint = Some res ->
+    In s (successors!!!n) ->
     L.ge res!!s (transf n res!!n).
 
   Hypothesis fixpoint_entry:
-    forall successors topnode transf entrypoint res,
-    fixpoint successors topnode transf entrypoint = Some res ->
+    forall successors transf entrypoint res,
+    fixpoint successors transf entrypoint = Some res ->
     res!!entrypoint = L.top.
 
   Hypothesis fixpoint_invariant:
-    forall successors topnode transf entrypoint 
+    forall successors transf entrypoint 
            (P: L.t -> Prop),
     P L.top ->
     (forall pc x, P x -> P (transf pc x)) ->
     forall res pc,
-    fixpoint successors topnode transf entrypoint = Some res ->
+    fixpoint successors transf entrypoint = Some res ->
     P res!!pc.
 
 End BBLOCK_SOLVER.
@@ -719,8 +803,7 @@ Module L := LAT.
 
 Section Solver.
 
-Variable successors: positive -> list positive.
-Variable topnode: positive.
+Variable successors: PTree.t (list positive).
 Variable transf: positive -> L.t -> L.t.
 Variable entrypoint: positive.
 Variable P: L.t -> Prop.
@@ -748,9 +831,8 @@ Record state : Type := mkstate
         extract a node n from st_wrk
         compute out = transf n st_in[n]
         for each successor s of n:
-            compute in = lub st_in[s] out
             if s has only one predecessor (namely, n):
-                st_in[s] := in
+                st_in[s] := out
                 st_wrk := st_wrk union {s}
             end if
         end for
@@ -777,33 +859,29 @@ Definition step (bb: bbmap) (st: state) : result + state :=
   match st.(st_wrk) with
   | nil => inl _ st.(st_in)
   | pc :: rem =>
-      if plt pc topnode then
         inr _ (propagate_successors 
-                 bb (successors pc)
+                 bb (successors!!!pc)
                  (transf pc st.(st_in)!!pc)
                  (mkstate st.(st_in) rem))
-      else
-        inr _ (mkstate st.(st_in) rem)
   end.
 
 (** Recognition of program points that have more than one predecessor. *)
 
 Definition is_basic_block_head 
-    (preds: PMap.t (list positive)) (pc: positive) : bool :=
-  match preds!!pc with
-  | nil => true
-  | s :: nil => 
-      if peq s pc then true else
-      if peq pc entrypoint then true else false
-  | _ :: _ :: _ => true
-  end.
+    (preds: PTree.t (list positive)) (pc: positive) : bool :=
+  if peq pc entrypoint then true else
+    match preds!!!pc with
+    | nil => false
+    | s :: nil => peq s pc
+    | _ :: _ :: _ => true
+    end.
 
 Definition basic_block_map : bbmap :=
-  is_basic_block_head (make_predecessors successors topnode).
+  is_basic_block_head (make_predecessors successors).
 
 Definition basic_block_list (bb: bbmap) : list positive :=
-  positive_rec (list positive) nil
-    (fun pc l => if bb pc then pc :: l else  l) topnode.
+  PTree.fold (fun l pc scs => if bb pc then pc :: l else l)
+             successors nil.
 
 (** The computation of the approximate solution. *)
 
@@ -813,43 +891,45 @@ Definition fixpoint : option result :=
 
 (** ** Properties of predecessors and multiple-predecessors nodes *)
 
-Definition predecessors := make_predecessors successors topnode.
+Definition predecessors := make_predecessors successors.
 
 Lemma predecessors_correct:
   forall n s,
-  Plt n topnode -> In s (successors n) -> In n predecessors!!s.
+  In s successors!!!n -> In n predecessors!!!s.
 Proof.
   intros. unfold predecessors. eapply make_predecessors_correct; eauto.
 Qed.
 
 Lemma multiple_predecessors:
   forall s n1 n2,
-  Plt n1 topnode -> In s (successors n1) ->
-  Plt n2 topnode -> In s (successors n2) ->
+  In s (successors!!!n1) ->
+  In s (successors!!!n2) ->
   n1 <> n2 ->
   basic_block_map s = true.
 Proof.
   intros. 
-  assert (In n1 predecessors!!s). apply predecessors_correct; auto.
-  assert (In n2 predecessors!!s). apply predecessors_correct; auto.
+  assert (In n1 predecessors!!!s). apply predecessors_correct; auto.
+  assert (In n2 predecessors!!!s). apply predecessors_correct; auto.
   unfold basic_block_map, is_basic_block_head.
+  destruct (peq s entrypoint). auto. 
   fold predecessors.
-  destruct (predecessors!!s). 
+  destruct (predecessors!!!s). 
   auto.
   destruct l.
-  simpl in H4. simpl in H5. intuition congruence. 
+  simpl in H2. simpl in H3. intuition congruence. 
   auto.
 Qed.
 
 Lemma no_self_loop:
   forall n,
-  Plt n topnode -> In n (successors n) -> basic_block_map n = true.
+  In n (successors!!!n) -> basic_block_map n = true.
 Proof.
   intros. unfold basic_block_map, is_basic_block_head.
+  destruct (peq n entrypoint). auto. 
   fold predecessors. 
-  generalize (predecessors_correct n n H H0). intro.
-  destruct (predecessors!!n). auto.
-  destruct l. replace n with p. apply peq_true. simpl in H1. tauto. 
+  generalize (predecessors_correct n n H). intro.
+  destruct (predecessors!!!n). auto.
+  destruct l. replace n with p. apply peq_true. simpl in H0. tauto. 
   auto.
 Qed.
 
@@ -864,9 +944,9 @@ Qed.
 Definition state_invariant (st: state) : Prop :=
   (forall n, basic_block_map n = true -> st.(st_in)!!n = L.top)
 /\
-  (forall n, Plt n topnode ->
+  (forall n,
    In n st.(st_wrk) \/
-   (forall s, In s (successors n) -> 
+   (forall s, In s (successors!!!n) -> 
                L.ge st.(st_in)!!s (transf n st.(st_in)!!n))).
 
 Lemma propagate_successors_charact1:
@@ -917,22 +997,21 @@ Qed.
 
 Lemma propagate_successors_invariant:
   forall pc res rem,
-  Plt pc topnode ->
   state_invariant (mkstate res (pc :: rem)) ->
   state_invariant 
-    (propagate_successors basic_block_map (successors pc)
+    (propagate_successors basic_block_map (successors!!!pc)
                           (transf pc res!!pc)
                           (mkstate res rem)).
 Proof.
-  intros until rem. intros PC [INV1 INV2]. simpl in INV1. simpl in INV2.
+  intros until rem. intros [INV1 INV2]. simpl in INV1. simpl in INV2.
   set (l := transf pc res!!pc).
   generalize (propagate_successors_charact1 basic_block_map
-                (successors pc) l (mkstate res rem)).
+                (successors!!! pc) l (mkstate res rem)).
   generalize (propagate_successors_charact2 basic_block_map
-                (successors pc) l (mkstate res rem)).
+                (successors!!!pc) l (mkstate res rem)).
   set (st1 := propagate_successors basic_block_map
-                 (successors pc) l (mkstate res rem)).
-  intros A B.
+                 (successors!!!pc) l (mkstate res rem)).
+  intros A B. simpl in A. 
   (* First part: BB entries remain at top *)
   split; intros.
   elim (A n); intros C D. rewrite D. simpl. apply INV1. auto. tauto. 
@@ -944,55 +1023,40 @@ Proof.
   replace (st1.(st_in)!!pc) with res!!pc. fold l. 
   caseEq (basic_block_map s); intro.
   rewrite D. simpl. rewrite INV1. apply L.top_ge. auto. tauto. 
-  elim (C H0 H1); intros. rewrite H3. apply L.refl_ge. 
+  elim (C H H0); intros. rewrite H2. apply L.refl_ge. 
   elim (A pc); intros E F. rewrite F. reflexivity. 
-  case (In_dec peq pc (successors pc)); intro.
+  case (In_dec peq pc (successors!!!pc)); intro.
   right. apply no_self_loop; auto. 
   left; auto.
   (* Case 2: n <> pc *)
-  elim (INV2 n H); intro.
+  elim (INV2 n); intro.
   (* Case 2.1: n was already in worklist, still is *)
-  left. apply B. simpl.  simpl in H0. tauto.
+  left. apply B. simpl. tauto.
   (* Case 2.2: n was not in worklist *)
-  assert (INV3: forall s, In s (successors n) -> st1.(st_in)!!s = res!!s).
+  assert (INV3: forall s, In s (successors!!!n) -> st1.(st_in)!!s = res!!s).
     (* Amazingly, successors of n do not change.  The only way
        they could change is if they were successors of pc as well,
        but that gives them two different predecessors, so
        they are basic block heads, and thus do not change! *)
     intros. elim (A s); intros C D. rewrite D. reflexivity. 
-    case (In_dec peq s (successors pc)); intro.
+    case (In_dec peq s (successors!!!pc)); intro.
     right. apply multiple_predecessors with n pc; auto.
     left; auto.
-  case (In_dec peq n (successors pc)); intro.
+  case (In_dec peq n (successors!!!pc)); intro.
   (* Case 2.2.1: n is a successor of pc. Either it is in the
      worklist or it did not change *)
   caseEq (basic_block_map n); intro.
   right; intros. 
-  elim (A n); intros C D. rewrite D. simpl. 
-  rewrite INV3; auto.
+  elim (A n); intros C D. rewrite D. rewrite INV3; auto.
   tauto.
-  left. elim (A n); intros C D. elim (C i H1); intros. auto.
+  left. elim (A n); intros C D. elim (C i H0); intros. auto.
   (* Case 2.2.2: n is not a successor of pc. It did not change. *)
   right; intros.
-  elim (A n); intros C D. rewrite D. simpl. 
+  elim (A n); intros C D. rewrite D. 
   rewrite INV3; auto.
   tauto.
 Qed.
 
-Lemma discard_top_worklist_invariant:
-  forall pc res rem,
-  ~(Plt pc topnode) ->
-  state_invariant (mkstate res (pc :: rem)) ->
-  state_invariant (mkstate res rem).
-Proof.
-  intros; red; intros.
-  elim H0; simpl; intros A B.
-  split. assumption. 
-  intros. elim (B n H1); intros.
-  left. elim H2; intro. subst n. contradiction. auto.
-  right. assumption.
-Qed.
-
 Lemma initial_state_invariant:
   state_invariant (mkstate (PMap.init L.top) (basic_block_list basic_block_map)).
 Proof.
@@ -1014,27 +1078,25 @@ Proof.
   unfold step. simpl. caseEq stwrk.
   intro. congruence.
 
-  intros pc rem WRK. case (plt pc topnode); intro.
+  intros pc rem WRK. 
   apply propagate_successors_invariant; auto. congruence. 
-  eapply discard_top_worklist_invariant; eauto. congruence.
 
   eauto. apply initial_state_invariant.
 Qed.
 
-
 (** ** Correctness of the returned solution *)
 
 Theorem fixpoint_solution:
   forall res n s,
   fixpoint = Some res ->
-  Plt n topnode -> In s (successors n) ->
+  In s (successors!!!n) ->
   L.ge res!!s (transf n res!!n).
 Proof.
   intros. 
   assert (state_invariant (mkstate res nil)).
   eapply analyze_invariant; eauto. 
-  elim H2; simpl; intros. 
-  elim (H4 n H0); intros. 
+  elim H1; simpl; intros. 
+  elim (H3 n); intros. 
   contradiction.
   auto.
 Qed.
@@ -1049,10 +1111,7 @@ Proof.
   eapply analyze_invariant; eauto. 
   elim H0; simpl; intros. 
   apply H1. unfold basic_block_map, is_basic_block_head.
-  fold predecessors. 
-  destruct (predecessors!!entrypoint). auto.
-  destruct l. destruct (peq p entrypoint). auto. apply peq_true.
-  auto.
+  fold predecessors. apply peq_true. 
 Qed. 
 
 (** ** Preservation of a property over solutions *)
@@ -1085,11 +1144,9 @@ Proof.
   apply PS.
   assert (PS2: Pstate (mkstate st.(st_in) l)).
     red; intro; simpl. apply PS.
-  case (plt p topnode); intro.
-  apply propagate_successors_P. auto. auto. 
-  auto.
+  apply propagate_successors_P. auto. auto. eauto. 
 
-  eauto. red; intro; simpl. rewrite PMap.gi. apply Ptop.
+  red; intro; simpl. rewrite PMap.gi. apply Ptop.
 Qed.
 
 End Solver.
@@ -1107,8 +1164,8 @@ End BBlock_solver.
   the enumeration [n-1], [n-2], ..., 3, 2, 1 where [n] is the
   top CFG node is a reverse postorder traversal.
   Therefore, for forward analysis, we will use an implementation
-  of [NODE_SET] where the greatest node in the working list 
-  is selected by the [pick] operation.  For backward analysis,
+  of [NODE_SET] where the [pick] operation selects the 
+  greatest node in the working list.  For backward analysis,
   we will similarly pick the smallest node in the working list. *)
 
 Require Import FSets.
@@ -1126,9 +1183,8 @@ Module NodeSetForward <: NODE_SET.
     | Some n => Some(n, PositiveSet.remove n s)
     | None => None
     end.
-  Definition initial (top: positive) :=
-    positive_rec t PositiveSet.empty PositiveSet.add top.
-
+  Definition initial (successors: PTree.t (list positive)) :=
+    PTree.fold (fun s pc scs => PositiveSet.add pc s) successors PositiveSet.empty.
   Definition In := PositiveSet.In.
 
   Lemma add_spec:
@@ -1159,15 +1215,20 @@ Module NodeSetForward <: NODE_SET.
   Qed.
 
   Lemma initial_spec:
-    forall numnodes n, Plt n numnodes -> In n (initial numnodes).
+    forall successors n s, 
+    successors!n = Some s -> In n (initial successors).
   Proof.
-    intros numnodes; pattern numnodes. 
-    apply positive_Peano_ind; unfold initial; intros.
-    assert (Zpos n > 0). compute; auto. red in H. omegaContradiction.
-    rewrite positive_rec_succ. rewrite PositiveSetFacts.add_iff. 
-    elim (Plt_succ_inv _ _ H0); intro.
-    right. apply H. auto.
-    left. auto.
+    intros successors.
+    apply PTree_Properties.fold_rec with
+      (P := fun succ set =>
+              forall n s, succ!n = Some s -> In n set).
+    (* extensionality *)
+    intros. rewrite <- H in H1. eauto.
+    (* base case *)
+    intros. rewrite PTree.gempty in H. congruence.
+    (* inductive case *)
+    intros. rewrite PTree.gsspec in H2. rewrite add_spec.
+    destruct (peq n k). auto. eauto.
   Qed.
 End NodeSetForward.
 
@@ -1179,9 +1240,8 @@ Module NodeSetBackward <: NODE_SET.
     | Some n => Some(n, PositiveSet.remove n s)
     | None => None
     end.
-  Definition initial (top: positive) :=
-    positive_rec t PositiveSet.empty PositiveSet.add top.
-
+  Definition initial (successors: PTree.t (list positive)) :=
+    PTree.fold (fun s pc scs => PositiveSet.add pc s) successors PositiveSet.empty.
   Definition In := PositiveSet.In.
 
   Lemma add_spec:
@@ -1210,7 +1270,8 @@ Module NodeSetBackward <: NODE_SET.
   Qed.
 
   Lemma initial_spec:
-    forall numnodes n, Plt n numnodes -> In n (initial numnodes).
+    forall successors n s, 
+    successors!n = Some s -> In n (initial successors).
   Proof NodeSetForward.initial_spec.
 End NodeSetBackward.
 
diff --git a/backend/LTL.v b/backend/LTL.v
index 3a61e6d..2505566 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -51,9 +51,7 @@ Record function: Type := mkfunction {
   fn_params: list loc;
   fn_stacksize: Z;
   fn_code: code;
-  fn_entrypoint: node;
-  fn_nextpc: node;
-  fn_code_wf: forall (pc: node), Plt pc fn_nextpc \/ fn_code!pc = None
+  fn_entrypoint: node
 }.
 
 Definition fundef := AST.fundef function.
@@ -256,18 +254,17 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop :=
 (** Computation of the possible successors of an instruction.
   This is used in particular for dataflow analyses. *)
 
-Definition successors (f: function) (pc: node) : list node :=
-  match f.(fn_code)!pc with
-  | None => nil
-  | Some i =>
-      match i with
-      | Lnop s => s :: nil
-      | Lop op args res s => s :: nil
-      | Lload chunk addr args dst s => s :: nil
-      | Lstore chunk addr args src s => s :: nil
-      | Lcall sig ros args res s => s :: nil
-      | Ltailcall sig ros args => nil
-      | Lcond cond args ifso ifnot => ifso :: ifnot :: nil
-      | Lreturn optarg => nil
-      end
+Definition successors_instr (i: instruction) : list node :=
+  match i with
+  | Lnop s => s :: nil
+  | Lop op args res s => s :: nil
+  | Lload chunk addr args dst s => s :: nil
+  | Lstore chunk addr args src s => s :: nil
+  | Lcall sig ros args res s => s :: nil
+  | Ltailcall sig ros args => nil
+  | Lcond cond args ifso ifnot => ifso :: ifnot :: nil
+  | Lreturn optarg => nil
   end.
+
+Definition successors (f: function): PTree.t (list node) :=
+  PTree.map (fun pc i => successors_instr i) f.(fn_code).
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 866d05b..431fe17 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -95,7 +95,6 @@ Module DS := Dataflow_Solver(LBoolean)(NodeSetForward).
 Definition reachable_aux (f: LTL.function) : option (PMap.t bool) :=
   DS.fixpoint
     (successors f)
-    (f.(fn_nextpc))
     (fun pc r => r)
     ((f.(fn_entrypoint), true) :: nil).
 
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 239e2a6..b273860 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -50,6 +50,7 @@ module IntSet = Set.Make(struct type t = int let compare = compare end)
 (* Determine join points: reachable nodes that have > 1 predecessor *)
 
 let join_points f =
+  let succs = LTL.successors f in
   let reached = ref IntSet.empty in
   let reached_twice = ref IntSet.empty in
   let rec traverse pc =
@@ -59,7 +60,7 @@ let join_points f =
         reached_twice := IntSet.add npc !reached_twice
     end else begin
       reached := IntSet.add npc !reached;
-      List.iter traverse (LTL.successors f pc)
+      List.iter traverse (Kildall.successors_list succs pc)
     end
   in traverse f.fn_entrypoint; !reached_twice
 
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 1fb068d..e35fb11 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -105,20 +105,20 @@ Qed.
 (** The successors of a reachable instruction are reachable. *)
 
 Lemma reachable_successors:
-  forall f pc pc',
-  In pc' (successors f pc) ->
+  forall f pc pc' i,
+  f.(LTL.fn_code)!pc = Some i -> In pc' (successors_instr i) ->
   (reachable f)!!pc = true ->
   (reachable f)!!pc' = true.
 Proof.
   intro f. unfold reachable.
   caseEq (reachable_aux f).
   unfold reachable_aux. intro reach; intros.
-  elim (LTL.fn_code_wf f pc); intro.
   assert (LBoolean.ge reach!!pc' reach!!pc).
   change (reach!!pc) with ((fun pc r => r) pc (reach!!pc)).
-  eapply DS.fixpoint_solution. eexact H. auto. auto.
+  eapply DS.fixpoint_solution. eexact H.
+  unfold Kildall.successors_list, successors. rewrite PTree.gmap.
+  rewrite H0; auto.
   elim H3; intro. congruence. auto.
-  unfold successors in H0. rewrite H2 in H0. contradiction.
   intros. apply PMap.gi.
 Qed.
 
@@ -514,8 +514,7 @@ Proof.
   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.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   econstructor; split.
   eapply add_branch_correct; eauto.
@@ -525,8 +524,7 @@ Proof.
   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.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   econstructor; split.
   eapply plus_left'.
@@ -541,8 +539,7 @@ Proof.
   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.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   econstructor; split.
   eapply plus_left'.
@@ -558,8 +555,7 @@ Proof.
   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.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   econstructor; split.
   eapply plus_left'.
@@ -575,8 +571,7 @@ Proof.
   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.
+  eapply reachable_successors; eauto. simpl; auto.
   assert (VALID: valid_successor f pc'). inv WTI; auto.
   exploit find_function_translated; eauto. intros [tf' [A B]].
   econstructor; split.
@@ -608,8 +603,7 @@ Proof.
   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.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   destruct (starts_with ifso c').
   econstructor; split.
@@ -629,8 +623,7 @@ Proof.
   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.
-  unfold successors; rewrite H; auto with coqlib.
+  eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
   destruct (starts_with ifso c').
   econstructor; split.
diff --git a/backend/RTL.v b/backend/RTL.v
index 344d271..5de073e 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -87,9 +87,7 @@ Record function: Type := mkfunction {
   fn_params: list reg;
   fn_stacksize: Z;
   fn_code: code;
-  fn_entrypoint: node;
-  fn_nextpc: node;
-  fn_code_wf: forall (pc: node), Plt pc fn_nextpc \/ fn_code!pc = None
+  fn_entrypoint: node
 }.
 
 (** A function description comprises a control-flow graph (CFG) [fn_code]
@@ -332,6 +330,22 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop :=
 (** Computation of the possible successors of an instruction.
   This is used in particular for dataflow analyses. *)
 
+Definition successors_instr (i: instruction) : list node :=
+  match i with
+  | Inop s => s :: nil
+  | Iop op args res s => s :: nil
+  | Iload chunk addr args dst s => s :: nil
+  | Istore chunk addr args src s => s :: nil
+  | Icall sig ros args res s => s :: nil
+  | Itailcall sig ros args => nil
+  | Icond cond args ifso ifnot => ifso :: ifnot :: nil
+  | Ireturn optarg => nil
+  end.
+
+Definition successors (f: function) : PTree.t (list node) :=
+  PTree.map (fun pc i => successors_instr i) f.(fn_code).
+
+(*
 Definition successors (f: function) (pc: node) : list node :=
   match f.(fn_code)!pc with
   | None => nil
@@ -347,6 +361,7 @@ Definition successors (f: function) (pc: node) : list node :=
       | Ireturn optarg => nil
       end
   end.
+*)
 
 (** Transformation of a RTL function instruction by instruction.
   This applies a given transformation function to all instructions
@@ -356,24 +371,12 @@ Section TRANSF.
 
 Variable transf: node -> instruction -> instruction.
 
-Lemma transf_code_wf:
-  forall (c: code) (nextpc: node),
-  (forall (pc: node), Plt pc nextpc \/ c!pc = None) ->
-  (forall (pc: node), Plt pc nextpc \/ (PTree.map transf c)!pc = None).
-Proof.
-  intros. elim (H pc); intro.
-  left; assumption.
-  right. rewrite PTree.gmap. rewrite H0. reflexivity.
-Qed.
-
 Definition transf_function (f: function) : function :=
   mkfunction
     f.(fn_sig)
     f.(fn_params)
     f.(fn_stacksize)
     (PTree.map transf f.(fn_code))
-    f.(fn_entrypoint)
-    f.(fn_nextpc)
-    (transf_code_wf f.(fn_code) f.(fn_nextpc) f.(fn_code_wf)).
+    f.(fn_entrypoint).
 
 End TRANSF.
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 65e873e..39add98 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -630,9 +630,7 @@ Definition transl_function (f: CminorSel.function) : Errors.res RTL.function :=
                    rparams
                    f.(CminorSel.fn_stackspace)
                    s.(st_code)
-                   nentry
-                   s.(st_nextnode)
-                   s.(st_wf))
+                   nentry)
   end.
 
 Definition transl_fundef := transf_partial_fundef transl_function.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 8e61271..caf93c8 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -807,7 +807,7 @@ Inductive tr_stmt (c: code) (map: mapping):
 
 Inductive tr_function: CminorSel.function -> RTL.function -> Prop :=
   | tr_function_intro:
-      forall f code rparams map1 s0 s1 i1 rvars map2 s2 i2 nentry ngoto nret rret orret nextnode wfcode,
+      forall f code rparams map1 s0 s1 i1 rvars map2 s2 i2 nentry ngoto nret rret orret,
       add_vars init_mapping f.(CminorSel.fn_params) s0 = OK (rparams, map1) s1 i1 ->
       add_vars map1 f.(CminorSel.fn_vars) s1 = OK (rvars, map2) s2 i2 ->
       orret = ret_reg f.(CminorSel.fn_sig) rret ->
@@ -818,9 +818,7 @@ Inductive tr_function: CminorSel.function -> RTL.function -> Prop :=
                        rparams
                        f.(CminorSel.fn_stackspace)
                        code
-                       nentry
-                       nextnode
-                       wfcode).
+                       nentry).
 
 (** * Correctness proof of the translation functions *)
 
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 83e82e1..2df9d5d 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -393,7 +393,7 @@ Qed.
 
 (** The type system for RTL is not sound in that it does not guarantee
   progress: well-typed instructions such as [Icall] can fail because
-  of run-time type tests (such as the equality between calle and caller's
+  of run-time type tests (such as the equality between callee and caller's
   signatures).  However, the type system guarantees a type preservation
   property: if the execution does not fail because of a failed run-time
   test, the result values and register states match the static
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index 4b1417f..ef55a15 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -110,16 +110,6 @@ Definition tunnel_instr (uf: U.t) (b: instruction) : instruction :=
       Lreturn or
   end.
 
-Lemma wf_tunneled_code:
-  forall (f: LTL.function) (uf: U.t),
-  let tc := PTree.map (fun pc b => tunnel_instr uf b) (fn_code f) in
-  forall (pc: node), Plt pc (fn_nextpc f) \/ tc!pc = None.
-Proof.
-  intros. elim (fn_code_wf f pc); intro.
-  left; auto. right; unfold tc.
-  rewrite PTree.gmap; unfold option_map; rewrite H; auto.
-Qed.
-
 Definition tunnel_function (f: LTL.function) : LTL.function :=
   let uf := record_gotos f in
   mkfunction
@@ -127,9 +117,7 @@ Definition tunnel_function (f: LTL.function) : LTL.function :=
     (fn_params f)
     (fn_stacksize f)
     (PTree.map (fun pc b => tunnel_instr uf b) (fn_code f))
-    (U.repr uf (fn_entrypoint f))
-    (fn_nextpc f)
-    (wf_tunneled_code f uf).
+    (U.repr uf (fn_entrypoint f)).
 
 Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef :=
   transf_fundef tunnel_function f.
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index efaf42e..2df07fa 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -213,6 +213,23 @@ let make_temp typ =
       let v = Cil.makeTempVar f typ in 
       intern_string v.vname
 
+let rec constant_address e =
+  match e with
+  | Expr(Evar v, _) -> true
+  | Expr(Efield(e, id), _) -> constant_address e
+  | _ -> false
+
+let cache_address ty e (f: expr -> statement) =
+  if constant_address e then
+    f e
+  else begin
+    let t = make_temp (TPtr(ty, [])) in
+    let ty = typeof e in
+    let typ = Tpointer ty in
+    Ssequence(Sassign(Expr(Evar t, typ), Expr(Eaddrof e, typ)),
+              f (Expr(Ederef(Expr(Evar t, typ)), ty)))
+  end
+
 (** Detect and report GCC's __builtin_ functions *)
 
 let check_builtin s =
@@ -221,6 +238,74 @@ let check_builtin s =
   && String.sub s 0 (String.length b) = b
   then unsupported ("GCC `" ^ s ^ "' built-in function")
 
+(** ** Helpers for struct assignment *)
+
+let eintconst n =
+  Expr(Econst_int n, Tint(I32, Signed))
+let eindex e1 e2 ty =
+  Expr(Ederef(Expr (Ebinop(Oadd, e1, e2), typeof e1)), ty)
+let eaddrof e =
+  Expr(Eaddrof e, Tpointer(typeof e))
+
+let memcpy_ident = intern_string "memcpy"
+let memcpy_arg_type =
+  Tcons(Tpointer Tvoid, Tcons(Tpointer Tvoid, Tcons(Tint(I32, Unsigned), Tnil)))
+let memcpy_res_type = Tpointer Tvoid
+let memcpy_type = Tfunction(memcpy_arg_type, memcpy_res_type)
+let memcpy_used = ref false
+
+exception Use_memcpy
+
+let max_assignment_num = 8
+
+let compile_assignment ty lhs rhs =
+
+  let num_assign = ref 0 in
+
+  let rec comp_assign l r =
+    match typeof l with
+    | Tstruct(id, flds) -> 
+        let rec comp_field = function
+        | Fnil -> Sskip
+        | Fcons(id, ty, rem) ->
+            let ty = unrollType id (Tstruct(id, flds)) ty in
+            Ssequence(comp_assign (Expr (Efield(l, id), ty))
+                                  (Expr (Efield(r, id), ty)),
+                      comp_field rem)
+        in comp_field flds
+    | Tunion(id, flds) -> raise Use_memcpy
+    | Tarray(ty, sz) -> 
+        let sz = camlint_of_coqint sz in
+        let rec comp_element i =
+          if i >= sz then Sskip else begin
+            let idx = eintconst (coqint_of_camlint i) in
+            Ssequence(comp_assign (eindex l idx ty) (eindex r idx ty),
+                      comp_element (Int32.succ i))
+          end
+        in comp_element 0l
+    | _ ->
+        if !num_assign >= max_assignment_num then raise Use_memcpy;
+        incr num_assign;
+        Sassign(l, r)
+  in
+    try 
+      cache_address ty lhs (fun lhs' ->
+        cache_address ty rhs (fun rhs' ->
+          comp_assign lhs' rhs'))
+    with Use_memcpy ->
+      memcpy_used := true;
+      Scall(None, Expr(Evar memcpy_ident, memcpy_type),
+                  [eaddrof lhs; eaddrof rhs; eintconst (sizeof (typeof lhs))])
+
+let declare_memcpy fundecl =
+  if !memcpy_used
+  && not (List.exists (fun (Datatypes.Coq_pair(id, _)) -> id = memcpy_ident)
+                      fundecl)
+  then Datatypes.Coq_pair(memcpy_ident,
+                          External(memcpy_ident, memcpy_arg_type, memcpy_res_type))
+       :: fundecl
+  else fundecl
+
 (** ** Translation functions *)
 
 (** Convert a [Cil.ikind] into a pair [(intsize * signedness)] *)
@@ -576,37 +661,37 @@ let makeFuncall2 tyfun tylhs elhs efun eargs =
       Ssequence(makeFuncall1 tyfun elhs' efun eargs,
                 Sassign(elhs, elhs'))
                 
+(** Convert a [Cil.instr] into a [CabsCoq.statement] *)
+let processInstr = function
+  | Set (lv, rv, loc) ->
+      updateLoc(loc);
+      let lv' = convertLval lv in
+      let rv' = convertExp rv in
+      begin match typeof lv' with
+      | Tstruct _ | Tunion _ -> compile_assignment (typeOfLval lv) lv' rv'
+      | t -> Sassign (lv', rv')
+      end
+  | Call (None, e, eList, loc) ->
+      updateLoc(loc);
+      let (efun, params) = convertExpFuncall e eList in
+      Scall(None, efun, params)
+  | Call (Some lv, e, eList, loc) ->
+      updateLoc(loc);
+      let (efun, params) = convertExpFuncall e eList in
+      makeFuncall2 (Cil.typeOf e) (Cil.typeOfLval lv) (convertLval lv) efun params
+  | Asm (_, _, _, _, _, loc) ->
+      updateLoc(loc);
+      unsupported "inline assembly"
 
 (** Convert a [Cil.instr list] into a [CabsCoq.statement] *)
-let rec processInstrList l =
-  (* convert an instruction *)
-  let convertInstr = function
-    | Set (lv, e, loc) ->
-	updateLoc(loc);
-        begin match convertTyp (Cil.typeOf e) with
-        | Tstruct _ | Tunion _ -> unsupported "struct or union assignment"
-        | t -> Sassign (convertLval lv, convertExp e)
-        end
-    | Call (None, e, eList, loc) ->
-	updateLoc(loc);
-        let (efun, params) = convertExpFuncall e eList in
-        Scall(None, efun, params)
-    | Call (Some lv, e, eList, loc) ->
-	updateLoc(loc);
-        let (efun, params) = convertExpFuncall e eList in
-        makeFuncall2 (Cil.typeOf e) (Cil.typeOfLval lv) (convertLval lv) efun params
-    | Asm (_, _, _, _, _, loc) ->
-	updateLoc(loc);
-        unsupported "inline assembly"
-  in
-    (* convert a list of instructions *)
-    match l with
-      | [] -> Sskip
-      | [s] -> convertInstr s
-      | s :: l -> 
-          let cs = convertInstr s in
-          let cl = processInstrList l in
-          Ssequence (cs, cl)
+
+let rec processInstrList = function
+  | [] -> Sskip
+  | [s] -> processInstr s
+  | s :: l -> 
+      let cs = processInstr s in
+      let cl = processInstrList l in
+      Ssequence (cs, cl)
 
 
 (** Convert a [Cil.stmt list] into a [CabsCoq.statement] *)
@@ -672,54 +757,68 @@ and processLblStmtList switchBody = function
 	end
 
 
-(** Convert a [Cil.stmt] into a [CabsCoq.statement] *)
-and convertStmt s =
-  match s.skind with
-    | Instr iList -> processInstrList iList
+(** Convert a [Cil.stmtkind] into a [CabsCoq.statement] *)
+and convertStmtKind = function
+    | Instr iList ->
+        processInstrList iList
     | Return (eOpt, loc) ->
-	updateLoc(loc);
+        updateLoc(loc);
         let eOpt' = match eOpt with
-	  | None -> None
-	  | Some e -> Some (convertExp e)
-	in 
+          | None -> None
+          | Some e -> Some (convertExp e)
+        in 
           Sreturn eOpt'
-    | Goto (_, loc) ->
-	updateLoc(loc);
-        unsupported "`goto' statement"
+    | Goto (sref, loc) ->
+        updateLoc(loc);
+        let rec extract_label = function
+        | [] -> internal_error "convertStmtKind: goto without label"
+        | Label(lbl, _, _) :: _ -> lbl
+        | _ :: rem -> extract_label rem
+        in
+          Sgoto (intern_string (extract_label (!sref).labels))
     | Break loc ->
-	updateLoc(loc);
-	Sbreak
+        updateLoc(loc);
+        Sbreak
     | Continue loc ->
-	updateLoc(loc);
-	Scontinue
+        updateLoc(loc);
+        Scontinue
     | If (e, b1, b2, loc) ->
-	updateLoc(loc);
+        updateLoc(loc);
         let e1 = processStmtList b1.bstmts in
         let e2 = processStmtList b2.bstmts in
-	  Sifthenelse (convertExp e, e1, e2)
+          Sifthenelse (convertExp e, e1, e2)
     | Switch (e, b, l, loc) ->
-	updateLoc(loc);
+        updateLoc(loc);
         Sswitch (convertExp e, processLblStmtList b.bstmts l)
     | While (e, b, loc) ->
-	updateLoc(loc);
+        updateLoc(loc);
         Swhile (convertExp e, processStmtList b.bstmts)
     | DoWhile (e, b, loc) ->
-	updateLoc(loc);
+        updateLoc(loc);
         Sdowhile (convertExp e, processStmtList b.bstmts)
     | For (bInit, e, bIter, b, loc) ->
-	updateLoc(loc);
-	let sInit = processStmtList bInit.bstmts in
-	let e' = convertExp e in
-	let sIter = processStmtList bIter.bstmts in
-	  Sfor (sInit, e', sIter, processStmtList b.bstmts)
+        updateLoc(loc);
+        let sInit = processStmtList bInit.bstmts in
+        let e' = convertExp e in
+        let sIter = processStmtList bIter.bstmts in
+          Sfor (sInit, e', sIter, processStmtList b.bstmts)
     | Block b -> processStmtList b.bstmts
     | TryFinally (_, _, loc) ->
-	updateLoc(loc);
+        updateLoc(loc);
         unsupported "`try'...`finally' statement"
     | TryExcept (_, _, _, loc) ->
-	updateLoc(loc);
+        updateLoc(loc);
         unsupported "`try'...`except' statement"
 
+(** Convert a [Cil.stmtkind] into a [CabsCoq.statement] *)
+and convertStmt s =
+  let rec add_labels l s =
+    match l with
+    | [] -> s
+    | Label(lbl, _, _) :: rem -> Slabel(intern_string lbl, add_labels rem s)
+    | _ :: rem -> add_labels rem s (* error? *)
+  in add_labels s.labels (convertStmtKind s.skind)
+
 (** Convert a [Cil.GFun] into a pair [(ident * coq_fundecl)] *)
 let convertGFun fdec =
   current_function := Some fdec;
@@ -986,17 +1085,18 @@ let convertFile f =
   Hashtbl.clear varinfo_atom;
   Hashtbl.clear stringTable;
   Hashtbl.clear stub_function_table;
+  memcpy_used := false;
   let (funList, defList) = processGlobals (cleanupGlobals f.globals) in
-  let funList' = declare_stub_functions funList in
-  let funList'' = match f.globinit with
-    | Some fdec -> convertGFun fdec :: funList'
-    | None -> funList' in
-  let defList' = globals_for_strings defList in
-  { AST.prog_funct = funList'';
-    AST.prog_vars = defList';
+  let funList1 = declare_stub_functions funList in
+  let funList2 = match f.globinit with
+    | Some fdec -> convertGFun fdec :: funList1
+    | None -> funList1 in
+  let funList3 = declare_memcpy funList2 in
+  let defList1 = globals_for_strings defList in
+  { AST.prog_funct = funList3;
+    AST.prog_vars = defList1;
     AST.prog_main = intern_string "main" }
 
-
 (*-----------------------------------------------------------------------*)
 end
 
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 5513b41..88e24ee 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -262,6 +262,10 @@ let rec print_stmt p s =
       fprintf p "return;"
   | Sreturn (Some e) ->
       fprintf p "return %a;" print_expr e
+  | Slabel(lbl, s1) ->
+      fprintf p "%s:@ %a" (extern_atom lbl) print_stmt s1
+  | Sgoto lbl ->
+      fprintf p "goto %s;" (extern_atom lbl)
 
 and print_cases p cases =
   match cases with
@@ -451,6 +455,8 @@ let rec collect_stmt = function
   | Sswitch(e, cases) -> collect_expr e; collect_cases cases
   | Sreturn None -> ()
   | Sreturn (Some e) -> collect_expr e
+  | Slabel(lbl, s) -> collect_stmt s
+  | Sgoto lbl -> ()
 
 and collect_cases = function
   | LSdefault s -> collect_stmt s
diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch
index b7e5b0b..6c94854 100644
--- a/extraction/Kildall.ml.patch
+++ b/extraction/Kildall.ml.patch
@@ -1,40 +1,21 @@
-*** kildall.ml.orig	2009-06-03 11:32:52.297641897 +0200
---- kildall.ml	2009-06-03 11:34:48.481516509 +0200
+*** kildall.ml.orig	2009-08-16 15:45:21.000000000 +0200
+--- kildall.ml	2009-08-16 15:45:27.000000000 +0200
 ***************
-*** 151,158 ****
-        -> (positive, LAT.t) prod list -> LAT.t PMap.t option **)
+*** 252,259 ****
     
-    let fixpoint successors topnode transf entrypoints =
-!     DS.fixpoint (fun s -> PMap.get s (make_predecessors successors topnode))
-!       topnode transf entrypoints
-   end
-  
-  module type ORDERED_TYPE_WITH_TOP = 
---- 151,158 ----
-        -> (positive, LAT.t) prod list -> LAT.t PMap.t option **)
+    (** val basic_block_map : positive list PTree.t -> positive -> bbmap **)
     
-    let fixpoint successors topnode transf entrypoints =
-!     let pred = make_predecessors successors topnode in
-!     DS.fixpoint (fun s -> PMap.get s pred) topnode transf entrypoints
-   end
-  
-  module type ORDERED_TYPE_WITH_TOP = 
-***************
-*** 248,255 ****
-    (** val basic_block_map :
-        (positive -> positive list) -> positive -> positive -> bbmap **)
-    
-!   let basic_block_map successors topnode entrypoint x =
-!     is_basic_block_head entrypoint (make_predecessors successors topnode) x
-    
-    (** val basic_block_list : positive -> bbmap -> positive list **)
+!   let basic_block_map successors entrypoint x =
+!     is_basic_block_head entrypoint (make_predecessors successors) x
     
---- 248,255 ----
-    (** val basic_block_map :
-        (positive -> positive list) -> positive -> positive -> bbmap **)
+    (** val basic_block_list :
+        positive list PTree.t -> bbmap -> positive list **)
+--- 252,259 ----
     
-!   let basic_block_map successors topnode entrypoint =
-!     is_basic_block_head entrypoint (make_predecessors successors topnode)
+    (** val basic_block_map : positive list PTree.t -> positive -> bbmap **)
     
-    (** val basic_block_list : positive -> bbmap -> positive list **)
+!   let basic_block_map successors entrypoint =
+!     is_basic_block_head entrypoint (make_predecessors successors)
     
+    (** val basic_block_list :
+        positive list PTree.t -> bbmap -> positive list **)
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 1d58ee5..390f49d 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -456,6 +456,3 @@ Lemma ge_lub_left: forall x y, ge (lub x y) x.
 Proof. destruct x; destruct y; compute; tauto. Qed.
 
 End LBoolean.
-
-
-
diff --git a/lib/Maps.v b/lib/Maps.v
index 766168a..b607d24 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -887,15 +887,49 @@ Module PTree <: TREE.
     intros. change (list_norepet (xkeys m 1)). apply xelements_keys_norepet.
   Qed.
 
+(*
   Definition fold (A B : Type) (f: B -> positive -> A -> B) (tr: t A) (v: B) :=
      List.fold_left (fun a p => f a (fst p) (snd p)) (elements tr) v.
+*)
+
+  Fixpoint xfold (A B: Type) (f: B -> positive -> A -> B)
+                 (i: positive) (m: t A) (v: B) {struct m} : B :=
+    match m with
+    | Leaf => v
+    | Node l None r =>
+        let v1 := xfold f (append i (xO xH)) l v in
+        xfold f (append i (xI xH)) r v1
+    | Node l (Some x) r =>
+        let v1 := xfold f (append i (xO xH)) l v in
+        let v2 := f v1 i x in
+        xfold f (append i (xI xH)) r v2
+    end.
+
+  Definition fold (A B : Type) (f: B -> positive -> A -> B) (m: t A) (v: B) :=
+    xfold f xH m v.
+
+  Lemma xfold_xelements:
+    forall (A B: Type) (f: B -> positive -> A -> B) m i v,
+    xfold f i m v =
+    List.fold_left (fun a p => f a (fst p) (snd p))
+                   (xelements m i)
+                   v.
+  Proof.
+    induction m; intros.
+    simpl. auto.
+    simpl. destruct o.
+    rewrite fold_left_app. simpl. 
+    rewrite IHm1. apply IHm2. 
+    rewrite fold_left_app. simpl.
+    rewrite IHm1. apply IHm2.
+  Qed.
 
   Theorem fold_spec:
     forall (A B: Type) (f: B -> positive -> A -> B) (v: B) (m: t A),
     fold f m v =
     List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
   Proof.
-    intros; unfold fold; auto.
+    intros. unfold fold, elements. apply xfold_xelements. 
   Qed.
 
 End PTree.
diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v
index 76ea153..109125c 100644
--- a/powerpc/Constprop.v
+++ b/powerpc/Constprop.v
@@ -674,7 +674,7 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
 Module DS := Dataflow_Solver(D)(NodeSetForward).
 
 Definition analyze (f: RTL.function): PMap.t D.t :=
-  match DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) 
+  match DS.fixpoint (successors f) (transfer f) 
                     ((f.(fn_entrypoint), D.top) :: nil) with
   | None => PMap.init D.top
   | Some res => res
@@ -1062,19 +1062,6 @@ Definition transf_instr (approx: D.t) (instr: instruction) :=
 Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code :=
   PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
 
-Lemma transf_code_wf:
-  forall f approxs,
-  (forall pc, Plt pc f.(fn_nextpc) \/ f.(fn_code)!pc = None) ->
-  (forall pc, Plt pc f.(fn_nextpc)
-      \/ (transf_code approxs f.(fn_code))!pc = None).
-Proof.
-  intros. 
-  elim (H pc); intro.
-  left; auto.
-  right. unfold transf_code. rewrite PTree.gmap. 
-  unfold option_map; rewrite H0. reflexivity.
-Qed.
-
 Definition transf_function (f: function) : function :=
   let approxs := analyze f in
   mkfunction
@@ -1082,9 +1069,7 @@ Definition transf_function (f: function) : function :=
     f.(fn_params)
     f.(fn_stacksize)
     (transf_code approxs f.(fn_code))
-    f.(fn_entrypoint)
-    f.(fn_nextpc)
-    (transf_code_wf f approxs f.(fn_code_wf)).
+    f.(fn_entrypoint).
 
 Definition transf_fundef (fd: fundef) : fundef :=
   AST.transf_fundef transf_function fd.
diff --git a/powerpc/Constpropproof.v b/powerpc/Constpropproof.v
index fb01f75..6e17f30 100644
--- a/powerpc/Constpropproof.v
+++ b/powerpc/Constpropproof.v
@@ -219,19 +219,19 @@ Qed.
   a solution of the forward dataflow inequations. *)
 
 Lemma analyze_correct_1:
-  forall f pc rs pc',
-  In pc' (successors f pc) ->
+  forall f pc rs pc' i,
+  f.(fn_code)!pc = Some i ->
+  In pc' (successors_instr i) ->
   regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
   regs_match_approx (analyze f)!!pc' rs.
 Proof.
-  intros until pc'. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (fn_nextpc f) (transfer f)
+  intros until i. unfold analyze. 
+  caseEq (DS.fixpoint (successors f) (transfer f)
                       ((fn_entrypoint f, D.top) :: nil)).
   intros approxs; intros.
   apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
   eapply DS.fixpoint_solution; eauto.
-  elim (fn_code_wf f pc); intro. auto. 
-  unfold successors in H0; rewrite H2 in H0; simpl; contradiction.
+  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
   auto.
   intros. rewrite PMap.gi. apply regs_match_approx_top. 
 Qed.
@@ -241,7 +241,7 @@ Lemma analyze_correct_3:
   regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
 Proof.
   intros. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (fn_nextpc f) (transfer f)
+  caseEq (DS.fixpoint (successors f) (transfer f)
                       ((fn_entrypoint f, D.top) :: nil)).
   intros approxs; intros.
   apply regs_match_approx_increasing with D.top.
@@ -756,7 +756,7 @@ Proof.
   TransfInstr; intro. eapply exec_Inop; eauto.
   econstructor; eauto.
   eapply analyze_correct_1 with (pc := pc); eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  simpl; auto.
   unfold transfer; rewrite H. auto.
 
   (* Iop *)
@@ -780,7 +780,7 @@ Proof.
   rewrite A; rewrite B; auto.
   econstructor; eauto. 
   eapply analyze_correct_1 with (pc := pc); eauto.
-  unfold successors; rewrite H; auto with coqlib.
+  simpl; auto.
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. 
   eapply eval_static_operation_correct; eauto.
@@ -798,8 +798,7 @@ Proof.
   exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split.
   eapply exec_Iload; eauto.
   econstructor; eauto. 
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. simpl; auto.
 
@@ -815,8 +814,7 @@ Proof.
   exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split.
   eapply exec_Istore; eauto.
   econstructor; eauto. 
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. auto. 
 
   (* Icall *)
@@ -826,8 +824,7 @@ Proof.
   eapply exec_Icall; eauto. apply sig_function_translated; auto.
   constructor; auto. constructor; auto.
   econstructor; eauto. 
-  intros. apply analyze_correct_1 with pc; auto.
-  unfold successors; rewrite H; auto with coqlib.
+  intros. eapply analyze_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H.
   apply regs_match_approx_update; auto. simpl. auto.
 
@@ -854,8 +851,8 @@ Proof.
   replace b with true. intro; eapply exec_Inop; eauto. congruence.
   intros. eapply exec_Icond_true; eauto.
   econstructor; eauto.
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto.
+  simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Icond, false *)
@@ -874,8 +871,8 @@ Proof.
   replace b with false. intro; eapply exec_Inop; eauto. congruence.
   intros. eapply exec_Icond_false; eauto.
   econstructor; eauto.
-  apply analyze_correct_1 with pc; auto. 
-  unfold successors; rewrite H; auto with coqlib.
+  eapply analyze_correct_1; eauto.
+  simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Ireturn *)
diff --git a/test/raytracer/Makefile b/test/raytracer/Makefile
index cd442c5..2812909 100644
--- a/test/raytracer/Makefile
+++ b/test/raytracer/Makefile
@@ -1,6 +1,7 @@
 CC=../../ccomp 
 CFLAGS=-U__GNUC__ -stdlib ../../runtime -dclight -dasm
 LIBS=
+TIME=xtime -mintime 2.0
 
 OBJS=memory.o gmllexer.o gmlparser.o eval.o \
   arrays.o vector.o matrix.o object.o intersect.o surface.o light.o \
@@ -41,3 +42,8 @@ gcc3:
 	mv render render.gcc3
 	$(MAKE) clean
 
+test:
+	./render < kal.gml
+
+bench:
+	$(TIME) ./render < kal.gml