Added support for jump tables in back end.

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

40 files changed, 380 insertions, 88 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 7d843e5..b802f4a 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -103,6 +103,8 @@ Definition transfer
 	  reg_list_live args (reg_sum_live ros Regset.empty)
       | Icond cond args ifso ifnot =>
           reg_list_live args after
+      | Ijumptable arg tbl =>
+          reg_live arg after
       | Ireturn optarg =>
           reg_option_live optarg Regset.empty
       end
@@ -167,6 +169,8 @@ Definition transf_instr
       Ltailcall sig (sum_left_map assign ros) (List.map assign args)
   | Icond cond args ifso ifnot =>
       Lcond cond (List.map assign args) ifso ifnot
+  | Ijumptable arg tbl =>
+      Ljumptable (assign arg) tbl
   | Ireturn optarg =>
       Lreturn (option_map assign optarg)
   end.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index fc0a0f3..10eaa5b 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -683,6 +683,12 @@ Proof.
   eapply exec_Lcond_false; eauto. TranslInstr.
   MatchStates. eapply agree_reg_list_live. eauto.
 
+  (* Ijumptable *)
+  assert (rs#arg = ls (assign arg)). apply AG. apply Regset.add_1. auto. 
+  econstructor; split.
+  eapply exec_Ljumptable; eauto. TranslInstr. congruence. 
+  MatchStates. eapply list_nth_z_in; eauto. eapply agree_reg_live; eauto. 
+
   (* Ireturn *)
   econstructor; split.
   eapply exec_Lreturn; eauto. TranslInstr; eauto.
diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v
index aba9660..260297f 100644
--- a/backend/Alloctyping.v
+++ b/backend/Alloctyping.v
@@ -141,6 +141,8 @@ Proof.
   rewrite transf_unroll; auto.
   (* cond *)
   WT.
+  (* jumptable *)
+  WT. 
   (* return *)
   WT.
   rewrite transf_unroll; simpl. 
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 8c5f536..15468c5 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -106,6 +106,7 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Llabel lbl => nil
   | Lgoto lbl => nil
   | Lcond cond args lbl => nil
+  | Ljumptable arg tbl => nil
   | Lreturn => nil
   end.
 
diff --git a/backend/CSE.v b/backend/CSE.v
index ff8d41a..98b7bbf 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -350,6 +350,8 @@ Definition transfer (f: function) (pc: node) (before: numbering) :=
           empty_numbering
       | Icond cond args ifso ifnot =>
           before
+      | Ijumptable arg tbl =>
+          before
       | Ireturn optarg =>
           before
       end
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 14027bf..7f94246 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -916,6 +916,13 @@ Proof.
   eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H; auto.
 
+  (* Icond false *)
+  econstructor; split.
+  eapply exec_Ijumptable; eauto. 
+  econstructor; eauto.
+  eapply analysis_correct_1; eauto. simpl. eapply list_nth_z_in; eauto.
+  unfold transfer; rewrite H; auto.
+
   (* Ireturn *)
   econstructor; split.
   eapply exec_Ireturn; eauto.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index cccce9a..e1ab2e9 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -121,26 +121,14 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
   | None => before
   | Some i =>
       match i with
-      | Inop s =>
-          before
       | Iop op args res s =>
           let a := eval_static_operation op (approx_regs before args) in
           D.set res a before
       | Iload chunk addr args dst s =>
           D.set dst Unknown before
-      | Istore chunk addr args src s =>
-          before
       | Icall sig ros args res s =>
           D.set res Unknown before
-      | Itailcall sig ros args =>
-          before
-(*
-      | Ialloc arg res s =>
-          D.set res Unknown before
-*)
-      | Icond cond args ifso ifnot =>
-          before
-      | Ireturn optarg =>
+      | _ =>
           before
       end
   end.
@@ -212,6 +200,15 @@ Definition transf_instr (app: D.t) (instr: instruction) :=
           let (cond', args') := cond_strength_reduction (approx_reg app) cond args in
           Icond cond' args' s1 s2
       end
+  | Ijumptable arg tbl =>
+      match intval (approx_reg app) arg with
+      | Some n =>
+          match list_nth_z tbl (Int.signed n) with
+          | Some s => Inop s
+          | None => instr
+          end
+      | None => instr
+      end
   | _ =>
       instr
   end.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index dadb192..fff9a60 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -390,6 +390,18 @@ Proof.
   simpl; auto.
   unfold transfer; rewrite H; auto.
 
+  (* Ijumptable *)
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split.
+  caseEq (intval (approx_reg (analyze f)!!pc) arg); intros.
+  exploit intval_correct; eauto. eexact MATCH. intro VRS.
+  eapply exec_Inop; eauto. TransfInstr. rewrite H2. 
+  replace i with n by congruence. rewrite H1. auto.
+  eapply exec_Ijumptable; eauto. TransfInstr. rewrite H2. auto.
+  constructor; auto.
+  eapply analyze_correct_1; eauto.
+  simpl. eapply list_nth_z_in; eauto.
+  unfold transfer; rewrite  H; auto.
+
   (* Ireturn *)
   exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split.
   eapply exec_Ireturn; eauto. TransfInstr; auto.
diff --git a/backend/LTL.v b/backend/LTL.v
index 2505566..6a69336 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -42,6 +42,7 @@ Inductive instruction: Type :=
   | Lcall: signature -> loc + ident -> list loc -> loc -> node -> instruction
   | Ltailcall: signature -> loc + ident -> list loc -> instruction
   | Lcond: condition -> list loc -> node -> node -> instruction
+  | Ljumptable: loc -> list node -> instruction
   | Lreturn: option loc -> instruction.
 
 Definition code: Type := PTree.t instruction.
@@ -206,6 +207,13 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_condition cond (map rs args) = Some false ->
       step (State s f sp pc rs m)
         E0 (State s f sp ifnot rs m)
+  | exec_Ljumptable:
+      forall s f sp pc rs m arg tbl n pc',
+      (fn_code f)!pc = Some(Ljumptable arg tbl) ->
+      rs arg = Vint n ->
+      list_nth_z tbl (Int.signed n) = Some pc' ->
+      step (State s f sp pc rs m)
+        E0 (State s f sp pc' rs m)
   | exec_Lreturn:
       forall s f stk pc rs m or,
       (fn_code f)!pc = Some(Lreturn or) ->
@@ -263,6 +271,7 @@ Definition successors_instr (i: instruction) : list node :=
   | Lcall sig ros args res s => s :: nil
   | Ltailcall sig ros args => nil
   | Lcond cond args ifso ifnot => ifso :: ifnot :: nil
+  | Ljumptable arg tbl => tbl
   | Lreturn optarg => nil
   end.
 
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 10b7d83..e353338 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -50,6 +50,7 @@ Inductive instruction: Type :=
   | Llabel: label -> instruction
   | Lgoto: label -> instruction
   | Lcond: condition -> list loc -> label -> instruction
+  | Ljumptable: loc -> list label -> instruction
   | Lreturn: option loc -> instruction.
 
 Definition code: Type := list instruction.
@@ -204,6 +205,13 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_condition cond (map rs args) = Some false ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b rs m)
+  | exec_Ljumptable:
+      forall s f sp arg tbl b rs m n lbl b',
+      rs arg = Vint n ->
+      list_nth_z tbl (Int.signed n) = Some lbl ->
+      find_label lbl f.(fn_code) = Some b' ->
+      step (State s f sp (Ljumptable arg tbl :: b) rs m)
+        E0 (State s f sp b' rs m)
   | exec_Lreturn:
       forall s f stk rs m or b,
       step (State s f (Vptr stk Int.zero) (Lreturn or :: b) rs m)
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 9f3f589..6013a17 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -76,6 +76,11 @@ Inductive wt_instr : instruction -> Prop :=
       List.map Loc.type args = type_of_condition cond ->
       locs_acceptable args ->
       wt_instr (Lcond cond args lbl)
+  | wt_Ljumptable:
+      forall arg tbl,
+      Loc.type arg = Tint ->
+      loc_acceptable arg ->
+      wt_instr (Ljumptable arg tbl)
   | wt_Lreturn: 
       forall optres,
       option_map Loc.type optres = funsig.(sig_res) ->
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 0461c9a..e62f928 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -94,6 +94,12 @@ Inductive wt_instr : instruction -> Prop :=
       locs_acceptable args ->
       valid_successor s1 -> valid_successor s2 ->
       wt_instr (Lcond cond args s1 s2)
+  | wt_Ljumptable:
+      forall arg tbl,
+      Loc.type arg = Tint ->
+      loc_acceptable arg ->
+      (forall lbl, In lbl tbl -> valid_successor lbl) ->
+      wt_instr (Ljumptable arg tbl)
   | wt_Lreturn: 
       forall optres,
       option_map Loc.type optres = funct.(fn_sig).(sig_res) ->
diff --git a/backend/Linear.v b/backend/Linear.v
index e025407..bf21cb7 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -46,6 +46,7 @@ Inductive instruction: Type :=
   | Llabel: label -> instruction
   | Lgoto: label -> instruction
   | Lcond: condition -> list mreg -> label -> instruction
+  | Ljumptable: mreg -> list label -> instruction
   | Lreturn: instruction.
 
 Definition code: Type := list instruction.
@@ -293,6 +294,13 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_condition cond (reglist rs args) = Some false ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b rs m)
+  | exec_Ljumptable:
+      forall s f sp arg tbl b rs m n lbl b',
+      rs (R arg) = Vint n ->
+      list_nth_z tbl (Int.signed n) = Some lbl ->
+      find_label lbl f.(fn_code) = Some b' ->
+      step (State s f sp (Ljumptable arg tbl :: b) rs m)
+        E0 (State s f sp b' rs m)
   | exec_Lreturn:
       forall s f stk b rs m,
       step (State s f (Vptr stk Int.zero) (Lreturn :: b) rs m)
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 431fe17..31d0318 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -190,6 +190,8 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code :=
         Lcond (negate_condition cond) args s2 :: add_branch s1 k
       else
         Lcond cond args s1 :: add_branch s2 k
+  | LTL.Ljumptable arg tbl =>
+      Ljumptable arg tbl :: k
   | LTL.Lreturn or =>
       Lreturn or :: k
   end.
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index b273860..1f4e5fa 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -96,6 +96,8 @@ let basic_blocks f joins =
          | Ltailcall (sig0, ros, args) -> end_block blk minpc
          | Lcond (cond, args, ifso, ifnot) ->
              end_block blk minpc; start_block ifso; start_block ifnot
+         | Ljumptable(arg, tbl) ->
+             end_block blk minpc; List.iter start_block tbl
          | Lreturn optarg -> end_block blk minpc
   (* next_in_block: check if join point and either extend block
      or start block *)
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index e35fb11..c79908d 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -639,6 +639,18 @@ Proof.
   traceEq.
   econstructor; eauto.
 
+  (* Ljumptable *)
+  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. simpl. eapply list_nth_z_in; eauto.
+  exploit find_label_lin_succ; eauto.
+  inv WTI. apply H6. eapply list_nth_z_in; eauto. 
+  intros [c'' AT'].
+  econstructor; split.
+  apply plus_one. eapply exec_Ljumptable; eauto. 
+  econstructor; eauto.
+
   (* Lreturn *)
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v
index 627c878..716b66f 100644
--- a/backend/Linearizetyping.v
+++ b/backend/Linearizetyping.v
@@ -60,6 +60,7 @@ Proof.
   apply wt_add_branch; auto.
   constructor; auto. apply wt_add_branch; auto.
   apply wt_add_instr. constructor; auto. auto.
+  apply wt_add_instr. constructor; auto. auto.
 Qed.
 
 Lemma wt_linearize_body:
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 33b570b..ba4952b 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -95,6 +95,10 @@ Inductive wt_instr : instruction -> Prop :=
       forall cond args lbl,
       List.map mreg_type args = type_of_condition cond ->
       wt_instr (Lcond cond args lbl)
+  | wt_Ljumptable:
+      forall arg tbl,
+      mreg_type arg = Tint ->
+      wt_instr (Ljumptable arg tbl)
   | wt_Lreturn: 
       wt_instr (Lreturn).
 
diff --git a/backend/Mach.v b/backend/Mach.v
index 0bb2442..f7e85c3 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -61,6 +61,7 @@ Inductive instruction: Type :=
   | Mlabel: label -> instruction
   | Mgoto: label -> instruction
   | Mcond: condition -> list mreg -> label -> instruction
+  | Mjumptable: mreg -> list label -> instruction
   | Mreturn: instruction.
 
 Definition code := list instruction.
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index aa17cd4..a2630a2 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -282,6 +282,13 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_condition cond rs##args = Some false ->
       step (State s f sp (Mcond cond args lbl :: c) rs fr m)
         E0 (State s f sp c rs fr m)
+  | exec_Mjumptable:
+      forall s f sp arg tbl c rs fr m n lbl c',
+      rs arg = Vint n ->
+      list_nth_z tbl (Int.signed n) = Some lbl ->
+      find_label lbl f.(fn_code) = Some c' ->
+      step (State s f sp (Mjumptable arg tbl :: c) rs fr m)
+        E0 (State s f sp c' rs fr m)
   | exec_Mreturn:
       forall s f stk soff c rs fr m,
       step (State s f (Vptr stk soff) (Mreturn :: c) rs fr m)
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
index 139eac7..89529fd 100644
--- a/backend/Machabstr2concr.v
+++ b/backend/Machabstr2concr.v
@@ -842,6 +842,11 @@ Proof.
   eapply exec_Mcond_false; eauto.
   econstructor; eauto.
 
+  (* Mjumptable *)
+  econstructor; split.
+  eapply exec_Mjumptable; eauto. 
+  econstructor; eauto.
+
   (* Mreturn *)
   assert (WTF: wt_function f) by (inv WTS; auto).
   econstructor; split.
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index 876f558..84ae0a4 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -204,6 +204,14 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_condition cond rs##args = Some false ->
       step (State s f sp (Mcond cond args lbl :: c) rs m)
         E0 (State s f sp c rs m)
+  | exec_Mjumptable:
+      forall s fb f sp arg tbl c rs m n lbl c',
+      rs arg = Vint n ->
+      list_nth_z tbl (Int.signed n) = Some lbl ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      find_label lbl f.(fn_code) = Some c' ->
+      step (State s fb sp (Mjumptable arg tbl :: c) rs m)
+        E0 (State s fb sp c' rs m)
   | exec_Mreturn:
       forall s fb stk soff c rs m f,
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index ef59e6f..fe086cb 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -79,6 +79,10 @@ Inductive wt_instr : instruction -> Prop :=
       forall cond args lbl,
       List.map mreg_type args = type_of_condition cond ->
       wt_instr (Mcond cond args lbl)
+  | wt_Mjumptable:
+      forall arg tbl,
+      mreg_type arg = Tint ->
+      wt_instr (Mjumptable arg tbl)
   | wt_Mreturn: 
       wt_instr Mreturn.
 
@@ -280,6 +284,7 @@ Proof.
 
   apply is_tail_find_label with lbl; congruence.
   apply is_tail_find_label with lbl; congruence. 
+  apply is_tail_find_label with lbl; congruence. 
 
   econstructor; eauto.
 
diff --git a/backend/RTL.v b/backend/RTL.v
index 5de073e..b2ee80f 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -75,6 +75,10 @@ Inductive instruction: Type :=
           [cond] over the values of registers [args].  If the condition
           is true, it transitions to [ifso].  If the condition is false,
           it transitions to [ifnot]. *)
+  | Ijumptable: reg -> list node -> instruction
+      (** [Ijumptable arg tbl] transitions to the node that is the [n]-th
+          element of the list [tbl], where [n] is the signed integer
+          value of register [arg]. *)
   | Ireturn: option reg -> instruction.
       (** [Ireturn] terminates the execution of the current function
           (it has no successor).  It returns the value of the given
@@ -252,6 +256,13 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_condition cond rs##args = Some false ->
       step (State s c sp pc rs m)
         E0 (State s c sp ifnot rs m)
+  | exec_Ijumptable:
+      forall s c sp pc rs m arg tbl n pc',
+      c!pc = Some(Ijumptable arg tbl) ->
+      rs#arg = Vint n ->
+      list_nth_z tbl (Int.signed n) = Some pc' ->
+      step (State s c sp pc rs m)
+        E0 (State s c sp pc' rs m)
   | exec_Ireturn:
       forall s c stk pc rs m or,
       c!pc = Some(Ireturn or) ->
@@ -339,30 +350,13 @@ Definition successors_instr (i: instruction) : list node :=
   | Icall sig ros args res s => s :: nil
   | Itailcall sig ros args => nil
   | Icond cond args ifso ifnot => ifso :: ifnot :: nil
+  | Ijumptable arg tbl => tbl
   | 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
-  | Some i =>
-      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
-  end.
-*)
-
 (** Transformation of a RTL function instruction by instruction.
   This applies a given transformation function to all instructions
   of a function and constructs a transformed function from that. *)
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 39add98..942dc50 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -474,6 +474,15 @@ Definition transl_exit (nexits: list node) (n: nat) : mon node :=
   | Some ne => ret ne
   end.
 
+Fixpoint transl_jumptable (nexits: list node) (tbl: list nat) : mon (list node) :=
+  match tbl with
+  | nil => ret nil
+  | t1 :: tl =>
+      do n1 <- transl_exit nexits t1;
+      do nl <- transl_jumptable nexits tl;
+      ret (n1 :: nl)
+  end.
+
 Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
                        {struct t} : mon node :=
   match t with
@@ -487,6 +496,14 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
       do n2 <- transl_switch r nexits t2;
       do n1 <- transl_switch r nexits t1;
       add_instr (Icond (Ccompuimm Clt key) (r :: nil) n1 n2)
+  | CTjumptable ofs sz tbl t' =>
+      do rt <- new_reg;
+      do ttbl <- transl_jumptable nexits tbl;
+      do n1 <- add_instr (Ijumptable rt ttbl);
+      do n2 <- transl_switch r nexits t';
+      do n3 <- add_instr (Icond (Ccompuimm Clt sz) (rt :: nil) n1 n2);
+      let op := if Int.eq ofs Int.zero then Omove else Oaddimm (Int.neg ofs) in
+      add_instr (Iop op (r :: nil) rt n3)
   end.
 
 (** Translation of statements.  [transl_stmt map s nd nexits nret rret]
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index 4c1fc05..7e42c80 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -27,16 +27,16 @@ module IntOrd =
 module IntSet = Set.Make(IntOrd)
 
 let normalize_table tbl =
-  let rec norm seen = function
-  | [] -> []
+  let rec norm keys accu = function
+  | [] -> (accu, keys)
   | Datatypes.Coq_pair(key, act) :: rem ->
-      if IntSet.mem key seen
-      then norm seen rem
-      else (key, act) :: norm (IntSet.add key seen) rem
-  in norm IntSet.empty tbl
+      if IntSet.mem key keys
+      then norm keys accu rem
+      else norm (IntSet.add key keys) ((key, act) :: accu) rem
+  in norm IntSet.empty [] tbl
 
-let compile_switch default table =
-  let sw = Array.of_list (normalize_table table) in
+let compile_switch_as_tree default tbl =
+  let sw = Array.of_list tbl in
   Array.stable_sort (fun (n1, _) (n2, _) -> IntOrd.compare n1 n2) sw;
   let rec build lo hi minval maxval =
     match hi - lo with
@@ -70,3 +70,37 @@ let compile_switch default table =
               build lo mid minval (Integers.Int.sub pivot Integers.Int.one),
               build mid hi pivot maxval)
   in build 0 (Array.length sw) Integers.Int.zero Integers.Int.max_unsigned
+
+let uint64_of_coqint n = (* force unsigned interpretation *)
+  Int64.logand (Int64.of_int32 (camlint_of_coqint n)) 0xFFFF_FFFFL
+
+let compile_switch_as_jumptable default cases minkey maxkey =
+  let tblsize = 1 + Int64.to_int (Int64.sub maxkey minkey) in
+  assert (tblsize >= 0 && tblsize <= Sys.max_array_length);
+  let tbl = Array.make tblsize default in
+  List.iter
+    (fun (key, act) ->
+       let pos = Int64.to_int (Int64.sub (uint64_of_coqint key) minkey) in
+       tbl.(pos) <- act)
+    cases;
+  CTjumptable(coqint_of_camlint (Int64.to_int32 minkey), 
+              coqint_of_camlint (Int32.of_int tblsize),
+              Array.to_list tbl,
+              CTaction default)
+
+let dense_enough (numcases: int) (minkey: int64) (maxkey: int64) =
+  let span = Int64.sub maxkey minkey in
+  assert (span >= 0L);
+  let tree_size = Int64.mul 4L (Int64.of_int numcases)
+  and table_size = Int64.add 8L span in
+  numcases >= 7           (* really small jump tables are less efficient *)
+  && span < Int64.of_int Sys.max_array_length
+  && table_size <= tree_size
+
+let compile_switch default table =
+  let (tbl, keys) = normalize_table table in
+  let minkey = uint64_of_coqint (IntSet.min_elt keys)
+  and maxkey = uint64_of_coqint (IntSet.max_elt keys) in
+  if dense_enough (List.length tbl) minkey maxkey
+  then compile_switch_as_jumptable default tbl minkey maxkey
+  else compile_switch_as_tree default tbl
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index df1ade9..d07bd08 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -419,37 +419,65 @@ Qed.
 (** Correctness of the translation of [switch] statements *)
 
 Lemma transl_switch_correct:
-  forall cs sp rs m i code r nexits t ns,
-  tr_switch code r nexits t ns ->
+  forall cs sp e m code map r nexits t ns,
+  tr_switch code map r nexits t ns ->
+  forall rs i act,
   rs#r = Vint i ->
-  exists nd,
-  star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs m) /\
-  nth_error nexits (comptree_match i t) = Some nd.
+  map_wf map ->
+  match_env map e nil rs ->
+  comptree_match i t = Some act ->
+  exists nd, exists rs',
+  star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\
+  nth_error nexits act = Some nd /\
+  match_env map e nil rs'.
 Proof.
-  induction 1; intros; simpl.
-  exists n. split. apply star_refl. auto. 
-
-  caseEq (Int.eq i key); intros.
-  exists nfound; split. 
+  induction 1; simpl; intros.
+(* action *)
+  inv H3. exists n; exists rs; intuition.
+  apply star_refl.
+(* ifeq *)
+  caseEq (Int.eq i key); intro EQ; rewrite EQ in H5.
+  inv H5. exists nfound; exists rs; intuition.
   apply star_one. eapply exec_Icond_true; eauto. 
-  simpl. rewrite H2. congruence. auto.
-  exploit IHtr_switch; eauto. intros [nd [EX MATCH]].
-  exists nd; split.
+  simpl. rewrite H2. congruence.
+  exploit IHtr_switch; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
+  exists nd1; exists rs1; intuition.
   eapply star_step. eapply exec_Icond_false; eauto. 
   simpl. rewrite H2. congruence. eexact EX. traceEq.
-  auto.
-
-  caseEq (Int.ltu i key); intros.
-  exploit IHtr_switch1; eauto. intros [nd [EX MATCH]].
-  exists nd; split. 
+(* iflt *)
+  caseEq (Int.ltu i key); intro EQ; rewrite EQ in H5.
+  exploit IHtr_switch1; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
+  exists nd1; exists rs1; intuition.
   eapply star_step. eapply exec_Icond_true; eauto. 
   simpl. rewrite H2. congruence. eexact EX. traceEq.
-  auto.
-  exploit IHtr_switch2; eauto. intros [nd [EX MATCH]].
-  exists nd; split. 
+  exploit IHtr_switch2; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
+  exists nd1; exists rs1; intuition.
   eapply star_step. eapply exec_Icond_false; eauto. 
   simpl. rewrite H2. congruence. eexact EX. traceEq.
-  auto.
+(* jumptable *)
+  set (rs1 := rs#rt <- (Vint(Int.sub i ofs))).
+  assert (ME1: match_env map e nil rs1).
+    unfold rs1. eauto with rtlg.
+  assert (EX1: step tge (State cs code sp n rs m) E0 (State cs code sp n1 rs1 m)).
+    eapply exec_Iop; eauto. 
+    predSpec Int.eq Int.eq_spec ofs Int.zero; simpl.
+    rewrite H10. rewrite Int.sub_zero_l. congruence.
+    rewrite H6. rewrite <- Int.sub_add_opp. auto. 
+  caseEq (Int.ltu (Int.sub i ofs) sz); intro EQ; rewrite EQ in H9.
+  exploit H5; eauto. intros [nd [A B]].
+  exists nd; exists rs1; intuition. 
+  eapply star_step. eexact EX1.
+  eapply star_step. eapply exec_Icond_true; eauto. 
+  simpl. unfold rs1. rewrite Regmap.gss. congruence. 
+  apply star_one. eapply exec_Ijumptable; eauto. unfold rs1. apply Regmap.gss. 
+  reflexivity. traceEq.
+  exploit (IHtr_switch rs1); eauto. unfold rs1. rewrite Regmap.gso; auto.
+  intros [nd [rs' [EX [NTH ME]]]].
+  exists nd; exists rs'; intuition.
+  eapply star_step. eexact EX1.
+  eapply star_step. eapply exec_Icond_false; eauto. 
+  simpl. unfold rs1. rewrite Regmap.gss. congruence.
+  eexact EX. reflexivity. traceEq.
 Qed.
 
 (** ** Semantic preservation for the translation of expressions *)
@@ -530,8 +558,6 @@ Definition transl_condition_prop
   /\ match_env map e le rs'
   /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
 
-
-
 (** The correctness of the translation is a huge induction over
   the Cminor evaluation derivation for the source program.  To keep
   the proof manageable, we put each case of the proof in a separate
@@ -1194,15 +1220,16 @@ Proof.
   econstructor; eauto. econstructor; eauto.
 
   (* switch *)
-  inv TS. 
+  inv TS.
+  exploit validate_switch_correct; eauto. intro CTM.
   exploit transl_expr_correct; eauto. 
   intros [rs' [A [B [C D]]]].
   exploit transl_switch_correct; eauto. 
-  intros [nd [E F]].
+  intros [nd [rs'' [E [F G]]]].
   econstructor; split.
   right; split. eapply star_trans. eexact A. eexact E.  traceEq. Lt_state. 
-  econstructor; eauto. 
-  rewrite (validate_switch_correct _ _ _ H3 n). constructor. auto.
+  econstructor; eauto.
+  constructor. auto.
 
   (* return none *)
   inv TS.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index caf93c8..037eb3f 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -713,22 +713,36 @@ Definition tr_store_optvar (c: code) (map: mapping)
 
 (** Auxiliary for the compilation of [switch] statements. *)
 
+Definition tr_jumptable (nexits: list node) (tbl: list nat) (ttbl: list node) : Prop :=
+  forall v act,
+  list_nth_z tbl v = Some act ->
+  exists n, list_nth_z ttbl v = Some n /\ nth_error nexits act = Some n.
+
 Inductive tr_switch
-     (c: code) (r: reg) (nexits: list node):
+     (c: code) (map: mapping) (r: reg) (nexits: list node):
      comptree -> node -> Prop :=
   | tr_switch_action: forall act n,
       nth_error nexits act = Some n ->
-      tr_switch c r nexits (CTaction act) n
+      tr_switch c map r nexits (CTaction act) n
   | tr_switch_ifeq: forall key act t' n ncont nfound,
-      tr_switch c r nexits t' ncont ->
+      tr_switch c map r nexits t' ncont ->
       nth_error nexits act = Some nfound ->
       c!n = Some(Icond (Ccompimm Ceq key) (r :: nil) nfound ncont) ->
-      tr_switch c r nexits (CTifeq key act t') n
+      tr_switch c map r nexits (CTifeq key act t') n
   | tr_switch_iflt: forall key t1 t2 n n1 n2,
-      tr_switch c r nexits t1 n1 ->
-      tr_switch c r nexits t2 n2 ->
+      tr_switch c map r nexits t1 n1 ->
+      tr_switch c map r nexits t2 n2 ->
       c!n = Some(Icond (Ccompuimm Clt key) (r :: nil) n1 n2) ->
-      tr_switch c r nexits (CTiflt key t1 t2) n.
+      tr_switch c map r nexits (CTiflt key t1 t2) n
+  | tr_switch_jumptable: forall ofs sz tbl t n n1 n2 n3 rt ttbl,
+      ~reg_in_map map rt -> rt <> r ->
+      c!n = Some(Iop (if Int.eq ofs Int.zero then Omove else Oaddimm (Int.neg ofs))
+                     (r ::nil) rt n1) ->
+      c!n1 = Some(Icond (Ccompuimm Clt sz) (rt :: nil) n2 n3) ->
+      c!n2 = Some(Ijumptable rt ttbl) ->
+      tr_switch c map r nexits t n3 ->
+      tr_jumptable nexits tbl ttbl ->
+      tr_switch c map r nexits (CTjumptable ofs sz tbl t) n.
 
 (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c],
   starting at node [ns], contains instructions that perform the Cminor
@@ -786,7 +800,7 @@ Inductive tr_stmt (c: code) (map: mapping):
   | tr_Sswitch: forall a cases default ns nd nexits ngoto nret rret n r t,
      validate_switch default cases t = true ->
      tr_expr c map nil a ns n r ->
-     tr_switch c r nexits t n ->
+     tr_switch c map r nexits t n ->
      tr_stmt c map (Sswitch a cases default) ns nd nexits ngoto nret rret
   | tr_Sreturn_none: forall nret nd nexits ngoto,
      tr_stmt c map (Sreturn None) nret nd nexits ngoto nret None
@@ -1000,9 +1014,9 @@ Qed.
 
 Lemma tr_switch_incr:
   forall s1 s2, state_incr s1 s2 ->
-  forall r nexits t ns,
-  tr_switch s1.(st_code) r nexits t ns ->
-  tr_switch s2.(st_code) r nexits t ns.
+  forall map r nexits t ns,
+  tr_switch s1.(st_code) map r nexits t ns ->
+  tr_switch s2.(st_code) map r nexits t ns.
 Proof.
   induction 2; econstructor; eauto with rtlg.
 Qed.
@@ -1051,24 +1065,47 @@ Proof.
   destruct (nth_error nexits n); intro; monadInv H. auto.
 Qed.
 
+Lemma transl_jumptable_charact:
+  forall nexits tbl s nl s' incr,
+  transl_jumptable nexits tbl s = OK nl s' incr ->
+  tr_jumptable nexits tbl nl /\ s' = s.
+Proof.
+  induction tbl; intros.
+  monadInv H. split. red. simpl. intros. discriminate. auto.
+  monadInv H. exploit transl_exit_charact; eauto. intros [A B]. 
+  exploit IHtbl; eauto. intros [C D].
+  split. red. simpl. intros. destruct (zeq v 0). inv H. exists x; auto. auto.
+  congruence.
+Qed.
+
 Lemma transl_switch_charact:
-  forall r nexits t s ns s' incr,
+  forall map r nexits t s ns s' incr,
+  map_valid map s -> reg_valid r s ->
   transl_switch r nexits t s = OK ns s' incr ->
-  tr_switch s'.(st_code) r nexits t ns.
+  tr_switch s'.(st_code) map r nexits t ns.
 Proof.
   induction t; simpl; intros.
   exploit transl_exit_charact; eauto. intros [A B].
   econstructor; eauto.
 
-  monadInv H.
+  monadInv H1.
   exploit transl_exit_charact; eauto. intros [A B]. subst s1.
   econstructor; eauto with rtlg. 
   apply tr_switch_incr with s0; eauto with rtlg.
 
-  monadInv H.
+  monadInv H1.
   econstructor; eauto with rtlg. 
   apply tr_switch_incr with s1; eauto with rtlg.
   apply tr_switch_incr with s0; eauto with rtlg.
+
+  monadInv H1.
+  exploit transl_jumptable_charact; eauto. intros [A B]. subst s1.
+  econstructor. eauto with rtlg.
+  apply sym_not_equal. apply valid_fresh_different with s; eauto with rtlg.
+  eauto with rtlg. eauto with rtlg. eauto with rtlg. 
+  apply tr_switch_incr with s3. eauto with rtlg.
+  eapply IHt with (s := s2); eauto with rtlg.
+  auto.
 Qed.
  
 Lemma transl_stmt_charact:
@@ -1091,8 +1128,9 @@ Proof.
   apply tr_expr_incr with s3; eauto with rtlg.
   eapply transl_expr_charact; eauto with rtlg. 
   (* Scall *)
-  assert (state_incr s0 s3) by eauto with rtlg.
-  assert (state_incr s3 s6) by eauto with rtlg.
+  assert (state_incr s0 s2) by eauto with rtlg.
+  assert (state_incr s2 s4) by eauto with rtlg.
+  assert (state_incr s4 s6) by eauto with rtlg.
   econstructor; eauto with rtlg.
   eapply transl_expr_charact; eauto with rtlg.
   apply tr_exprlist_incr with s6. auto. 
@@ -1101,7 +1139,6 @@ Proof.
   apply regs_valid_cons; eauto with rtlg.
   apply regs_valid_incr with s1; eauto with rtlg.
   apply regs_valid_cons; eauto with rtlg.
-  apply regs_valid_incr with s2; eauto with rtlg.
   apply tr_store_optvar_incr with s4; eauto with rtlg.
   eapply store_optvar_charact; eauto with rtlg.
   (* Stailcall *)
@@ -1149,7 +1186,7 @@ Proof.
   econstructor; eauto with rtlg.
   eapply transl_expr_charact; eauto with rtlg.
   apply tr_switch_incr with s1; auto with rtlg.
-  eapply transl_switch_charact; eauto with rtlg.
+  eapply transl_switch_charact with (s := s0); eauto with rtlg.
   monadInv TR. 
   (* Sreturn *)
   destruct o; destruct rret; inv TR.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 2df9d5d..86f0eaf 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -112,6 +112,11 @@ Inductive wt_instr : instruction -> Prop :=
       valid_successor s1 ->
       valid_successor s2 ->
       wt_instr (Icond cond args s1 s2)
+  | wt_Ijumptable:
+      forall arg tbl,
+      env arg = Tint ->
+      (forall s, In s tbl -> valid_successor s) ->
+      wt_instr (Ijumptable arg tbl)
   | wt_Ireturn: 
       forall optres,
       option_map env optres = funct.(fn_sig).(sig_res) ->
@@ -224,6 +229,9 @@ Definition check_instr (i: instruction) : bool :=
       check_regs args (type_of_condition cond)
       && check_successor s1
       && check_successor s2
+  | Ijumptable arg tbl =>
+      check_reg arg Tint
+      && List.forallb check_successor tbl
   | Ireturn optres =>
       match optres, funct.(fn_sig).(sig_res) with
       | None, None => true
@@ -326,6 +334,10 @@ Proof.
   constructor. apply check_regs_correct; auto.
   apply check_successor_correct; auto.
   apply check_successor_correct; auto.
+  (* jumptable *)
+  constructor. apply check_reg_correct; auto.
+  rewrite List.forallb_forall in H0. intros. apply check_successor_correct; auto.
+  intros. 
   (* return *)
   constructor. 
   destruct o; simpl; destruct funct.(fn_sig).(sig_res); try discriminate.
@@ -538,6 +550,8 @@ Proof.
   (* Icond *)
   econstructor; eauto.
   econstructor; eauto.
+  (* Ijumptable *)
+  econstructor; eauto.
   (* Ireturn *)
   econstructor; eauto. 
   destruct or; simpl in *.
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index cc7edf4..406ca07 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -87,6 +87,8 @@ let type_instr retty (Coq_pair(pc, i)) =
       end
   | Icond(cond, args, _, _) ->
       set_types args (type_of_condition cond)
+  | Ijumptable(arg, _) ->
+      set_type arg Tint
   | Ireturn(optres) ->
       begin match optres, retty with
       | None, None -> ()
diff --git a/backend/Reload.v b/backend/Reload.v
index 621e75b..5728a62 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -242,6 +242,9 @@ Definition transf_instr
   | LTLin.Lcond cond args lbl =>
       let rargs := regs_for args in
       add_reloads args rargs (Lcond cond rargs lbl :: k)
+  | LTLin.Ljumptable arg tbl =>
+      let rarg := reg_for arg in
+      add_reload arg rarg (Ljumptable rarg tbl :: k)
   | LTLin.Lreturn None =>
       Lreturn :: k
   | LTLin.Lreturn (Some loc) =>
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index a7becc3..21d5f38 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -1257,6 +1257,20 @@ Proof.
   econstructor; eauto with coqlib.
   apply agree_exten with ls; auto.
 
+  (* Ljumptable *)
+  ExploitWT; inv WTI.
+  exploit add_reload_correct_2.
+  intros [ls2 [A [B [C D]]]].
+  left; econstructor; split.
+  eapply plus_right. eauto. eapply exec_Ljumptable; eauto. 
+  assert (Val.lessdef (rs arg) (ls arg)). apply AG. auto.
+  rewrite H in H2. inv H2. congruence.
+  apply find_label_transf_function; eauto.
+  traceEq.
+  econstructor; eauto with coqlib.
+  apply agree_exten with ls; auto.
+  eapply LTLin.find_label_is_tail; eauto.
+
   (* Lreturn *)
   ExploitWT; inv WTI. 
   destruct or; simpl.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index 375bbfd..df0715e 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -35,7 +35,7 @@ Require Import Reloadproof.
 
 Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove
              wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall
-             wt_Llabel wt_Lgoto wt_Lcond wt_Lreturn: reloadty.
+             wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty.
 
 Remark wt_code_cons:
   forall f i c, wt_instr f i -> wt_code f c -> wt_code f (i :: c).
@@ -295,6 +295,10 @@ Proof.
     eauto with reloadty.
   auto with reloadty.
 
+  assert (mreg_type (reg_for arg) = Loc.type arg).
+    eauto with reloadty.
+  auto with reloadty.
+
   destruct optres; simpl in *; auto with reloadty.
   apply wt_add_reload; auto with reloadty. 
   unfold loc_result. rewrite <- H1.
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 182c322..5d9cf37 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -185,6 +185,8 @@ Definition transl_instr
       Mgoto lbl :: k
   | Lcond cond args lbl =>
       Mcond cond args lbl :: k
+  | Ljumptable arg tbl =>
+      Mjumptable arg tbl :: k
   | Lreturn =>
       restore_callee_save fe
         (Mreturn :: k)
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 5b6f2dc..ba42958 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1510,6 +1510,15 @@ Proof.
   rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; auto.
   econstructor; eauto with coqlib.
 
+  (* Ljumptable *)
+  econstructor; split.
+  apply plus_one; eapply exec_Mjumptable.
+  rewrite <- (agree_eval_reg _ _ _ _ _ _ _ arg AG) in H; eauto.
+  eauto. 
+  apply transl_find_label; eauto.
+  econstructor; eauto.
+  eapply find_label_incl; eauto.
+
   (* Lreturn *)
   exploit restore_callee_save_correct; eauto.
   intros [ls' [A [B C]]].
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index 1bafc35..8ba5cae 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -185,6 +185,9 @@ Proof.
   (* cond *)
   apply wt_instrs_cons; auto.
   constructor; auto.
+  (* jumptable *)
+  apply wt_instrs_cons; auto.
+  constructor; auto.
   (* return *)
   apply wt_restore_callee_save. apply wt_instrs_cons. constructor. auto.
 Qed.
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 1423e1e..8681d84 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -630,6 +630,13 @@ Proof.
   apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto.
   constructor; auto. 
 
+(* jumptable *)
+  TransfInstr. 
+  left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'); split.
+  eapply exec_Ijumptable; eauto.
+  generalize (RLD arg). rewrite H0. intro. inv H2. auto.
+  constructor; auto. 
+
 (* return *)
   TransfInstr.
   left. exists (Returnstate s' (regmap_optget or Vundef rs') (free m' stk)); split.
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index ef55a15..3ad8c4d 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -106,6 +106,8 @@ Definition tunnel_instr (uf: U.t) (b: instruction) : instruction :=
       Ltailcall sig ros args
   | Lcond cond args s1 s2 =>
       Lcond cond args (U.repr uf s1) (U.repr uf s2)
+  | Ljumptable arg tbl =>
+      Ljumptable arg (List.map (U.repr uf) tbl)
   | Lreturn or =>
       Lreturn or
   end.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index eccb62d..92ec68c 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -315,6 +315,13 @@ Proof.
   eapply exec_Lcond_false; eauto.
   rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
   econstructor; eauto.
+  (* jumptable *)
+  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
+  left; econstructor; split.
+  eapply exec_Ljumptable. 
+  rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
+  eauto. rewrite list_nth_z_map. change U.elt with node. rewrite H1. reflexivity. 
+  econstructor; eauto. 
   (* return *)
   generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
   left; econstructor; split.
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v
index 91745df..8990cb4 100644
--- a/backend/Tunnelingtyping.v
+++ b/backend/Tunnelingtyping.v
@@ -74,7 +74,9 @@ Lemma wt_tunnel_instr:
   wt_instr f i -> wt_instr (tunnel_function f) (tunnel_instr (record_gotos f) i).
 Proof.
   intros; inv H0; simpl; econstructor; eauto;
-  eapply branch_target_valid; eauto.
+  try (eapply branch_target_valid; eauto).
+  intros. exploit list_in_map_inv; eauto. intros [x [A B]]. subst lbl.
+  eapply branch_target_valid; eauto. 
 Qed.
 
 Lemma wt_tunnel_function: