Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary

12 files changed, 259 insertions, 82 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 245804f3..a3634c7a 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -66,6 +66,7 @@ Inductive instruction : Type :=
   | Pj_l    (l: label)                              (**r jump to label *)

   | Pcb     (bt: btest) (r: ireg) (l: label)        (**r branch based on btest *)

   | Pcbu    (bt: btest) (r: ireg) (l: label)        (**r branch based on btest with unsigned semantics *)

+  | Pjumptable (r: ireg) (labels: list label)

   | Ploopdo (count: ireg) (loopend: label)

 

   (** Loads **)

@@ -224,6 +225,7 @@ Definition control_to_instruction (c: control) :=
   | PCtlFlow (Asmblock.Pj_l l)              => Pj_l l

   | PCtlFlow (Asmblock.Pcb bt r l)          => Pcb bt r l

   | PCtlFlow (Asmblock.Pcbu bt r l)         => Pcbu bt r l

+  | PCtlFlow (Asmblock.Pjumptable r label)  => Pjumptable r label

   end.

 

 Definition basic_to_instruction (b: basic) :=

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 2fe27143..392a4f80 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -231,6 +231,7 @@ Inductive cf_instruction : Type :=
   | Pret                                            (**r return *)
   | Pcall   (l: label)                              (**r function call *)
   | Picall  (r: ireg)                               (**r function call on register value *)
+  | Pjumptable (r: ireg) (labels: list label) (**r N-way branch through a jump table (pseudo) *)
 
   (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *)
   | Pgoto   (l: label)                              (**r goto *)
@@ -1485,6 +1486,16 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem)
       Next (rs#PC <- (rs#r)) m
   | Pj_l l =>
       goto_label f l rs m
+  | Pjumptable r tbl =>
+      match rs#r with
+      | Vint n =>
+          match list_nth_z tbl (Int.unsigned n) with
+          | None => Stuck
+          | Some lbl => goto_label f lbl (rs #GPR62 <- Vundef #GPR63 <- Vundef) m
+          end
+      | _ => Stuck
+      end
+      
   | Pcb bt r l =>
       match cmp_for_btest bt with
       | (Some c, Int)  => eval_branch f l rs m (Val.cmp_bool c rs#r (Vint (Int.repr 0)))
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 6d124556..af2cd46d 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -42,6 +42,7 @@ Inductive control_op :=
   | Odivu
   | OError
   | OIncremPC (sz: Z)
+  | Ojumptable (l: list label)
 .
 
 Inductive arith_op :=
@@ -180,6 +181,15 @@ Definition eval_branch_deps (f: function) (l: label) (vpc: val) (res: option boo
 Definition control_eval (o: control_op) (l: list value) :=
   let (ge, fn) := Ge in
   match o, l with
+  | (Ojumptable tbl), [Val index; Val vpc] =>
+    match index with
+    | Vint n => 
+      match list_nth_z tbl (Int.unsigned n) with
+      | None => None
+      | Some lbl => goto_label_deps fn lbl vpc
+      end
+    | _ => None
+    end
   | Oj_l l, [Val vpc] => goto_label_deps fn l vpc
   | Ocb bt l, [Val v; Val vpc] =>
     match cmp_for_btest bt with
@@ -356,6 +366,7 @@ Definition control_op_eq (c1 c2: control_op): ?? bool :=
   | Oj_l l1, Oj_l l2 => phys_eq l1 l2
   | Ocb bt1 l1, Ocb bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2)
   | Ocbu bt1 l1, Ocbu bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2)
+  | Ojumptable tbl1, Ojumptable tbl2 => phys_eq tbl1 tbl2
   | Odiv, Odiv => RET true
   | Odivu, Odivu => RET true
   | OIncremPC sz1, OIncremPC sz2 => RET (Z.eqb sz1 sz2)
@@ -371,6 +382,7 @@ Proof.
   - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence.
   - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence.
   - rewrite Z.eqb_eq in * |-. congruence.
+  - congruence.
 Qed.
 
 
@@ -540,6 +552,9 @@ Definition trans_control (ctl: control) : macro :=
   | Pj_l l => [(#PC, Op (Control (Oj_l l)) (Name (#PC) @ Enil))]
   | Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (Name (#r) @ Name (#PC) @ Enil))]
   | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (Name (#r) @ Name (#PC) @ Enil))]
+  | Pjumptable r labels => [(#PC, Op (Control (Ojumptable labels)) (Name (#r) @ Name (#PC) @ Enil));
+                            (#GPR62, Op (Constant Vundef) Enil);
+                            (#GPR63, Op (Constant Vundef) Enil) ]
   | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)]
   end.
 
@@ -861,8 +876,27 @@ Proof.
   intros. destruct ex.
   - simpl in *. inv H1. destruct c; destruct i; try discriminate.
     all: try (inv H0; eexists; split; try split; [ simpl control_eval; pose (H3 PC); simpl in e; rewrite e; reflexivity | Simpl | intros rr; destruct rr; Simpl]).
+    (* Pjumptable *)
+    + unfold goto_label in *.
+      repeat (rewrite Pregmap.gso in H0; try discriminate).
+      destruct (nextblock _ _ _) eqn:NB; try discriminate.
+      destruct (list_nth_z _ _) eqn:LI; try discriminate.
+      destruct (label_pos _ _ _) eqn:LPOS; try discriminate.
+      destruct (nextblock b rs PC) eqn:MB2; try discriminate. inv H0.
+      eexists; split; try split.
+      * simpl control_eval. rewrite (H3 PC). simpl. Simpl.
+        rewrite H3. unfold nextblock in NB. rewrite Pregmap.gso in NB; try discriminate. rewrite NB.
+        rewrite LI. unfold goto_label_deps. rewrite LPOS.
+        unfold nextblock in MB2. rewrite Pregmap.gss in MB2. rewrite MB2.
+        reflexivity.
+      * Simpl.
+      * intros rr; destruct rr; Simpl.
+        destruct (preg_eq GPR62 g); Simpl. rewrite e. Simpl.
+        destruct (preg_eq GPR63 g); Simpl. rewrite e. Simpl.
     (* Pj_l *)
-    + unfold goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (nextblock _ _ _) eqn:NB; try discriminate. inv H0.
+    + unfold goto_label in H0.
+      destruct (label_pos _ _ _) eqn:LPOS; try discriminate.
+      destruct (nextblock _ _ _) eqn:NB; try discriminate. inv H0.
       eexists; split; try split.
       * simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl. unfold goto_label_deps. rewrite LPOS. rewrite nextblock_pc in NB.
         rewrite NB. reflexivity.
@@ -1052,6 +1086,11 @@ Lemma exec_exit_none:
 Proof.
   intros. inv H0. destruct ex as [ctl|]; try discriminate.
   destruct ctl; destruct i; try reflexivity; try discriminate.
+(* Pjumptable *)
+  - simpl in *. repeat (rewrite H3 in H1).
+    destruct (rs r); try discriminate; auto. destruct (list_nth_z _ _); try discriminate; auto.
+    unfold goto_label_deps in H1. unfold goto_label. Simpl.
+    destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
 (* Pj_l *)
   - simpl in *. pose (H3 PC); simpl in e; rewrite e in H1. clear e.
     unfold goto_label_deps in H1. unfold goto_label.
@@ -1163,6 +1202,10 @@ Lemma forward_simu_exit_stuck:
 Proof.
   intros. inv H1. destruct ex as [ctl|]; try discriminate.
   destruct ctl; destruct i; try discriminate; try (simpl; reflexivity).
+  (* Pjumptable *)
+  - simpl in *. repeat (rewrite H3). destruct (rs r); try discriminate; auto. destruct (list_nth_z _ _); try discriminate; auto.
+    unfold goto_label_deps. unfold goto_label in H0.
+    destruct (label_pos _ _ _); auto. repeat (rewrite Pregmap.gso in H0; try discriminate). destruct (rs PC); auto. discriminate.
 (* Pj_l *)
   - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold goto_label in H0.
     destruct (label_pos _ _ _); auto. clear e. destruct (rs PC); auto. discriminate.
@@ -1505,6 +1548,7 @@ Definition string_of_control (op: control_op) : pstring :=
   | Ocbu _ _ => "Ocbu"
   | Odiv => "Odiv"
   | Odivu => "Odivu"
+  | Ojumptable _ => "Ojumptable"
   | OError => "OError"
   | OIncremPC _ => "OIncremPC"
   end.
@@ -1732,6 +1776,37 @@ Proof.
   - simpl in H. inv H. inv MSR. inv MSW. eexists. split; try split. assumption. assumption.
 Qed.
 
+Theorem forward_simu_par_wio_basic_Stuck ge fn rsr rsw mr mw sr sw bi:
+  Ge = Genv ge fn ->
+  match_states (State rsr mr) sr ->
+  match_states (State rsw mw) sw ->
+  parexec_basic_instr ge bi rsr rsw mr mw = Stuck ->
+  macro_prun Ge (trans_basic bi) sw sr sr = None.
+Proof.
+  intros GENV MSR MSW H0. inv MSR; inv MSW.
+  unfold parexec_basic_instr in H0. destruct bi; try discriminate.
+(* PLoad *)
+  - destruct i; destruct i.
+    all: simpl; rewrite H; rewrite (H1 ra); unfold parexec_load in H0;
+    destruct (eval_offset _ _); auto; destruct (Mem.loadv _ _ _); auto; discriminate.
+(* PStore *)
+  - destruct i; destruct i;
+    simpl; rewrite H; rewrite (H1 ra); rewrite (H1 rs);
+    unfold parexec_store in H0; destruct (eval_offset _ _); auto; destruct (Mem.storev _ _ _); auto; discriminate.
+(* Pallocframe *)
+  - simpl. Simpl. rewrite (H1 SP). rewrite H. destruct (Mem.alloc _ _ _). simpl in H0.
+    destruct (Mem.store _ _ _ _); try discriminate. reflexivity.
+(* Pfreeframe *)
+  - simpl. Simpl. rewrite (H1 SP). rewrite H.
+    destruct (Mem.loadv _ _ _); auto. destruct (rsr GPR12); auto. destruct (Mem.free _ _ _ _); auto.
+    discriminate.
+(* Pget *)
+  - simpl. destruct rs; subst; try discriminate.
+    all: simpl; auto.
+  - simpl. destruct rd; subst; try discriminate.
+    all: simpl; auto.
+Qed.
+
 Theorem forward_simu_par_body:
   forall bdy ge fn rsr mr sr rsw mw sw rs' m',
   Ge = Genv ge fn ->
@@ -1771,6 +1846,17 @@ Proof.
   - destruct c; destruct i; try discriminate.
     all: try (inv H0; inv MSR; inv MSW; eexists; split; [| split]; [simpl; rewrite (H0 PC); reflexivity | Simpl | intros rr; destruct rr; unfold par_nextblock; Simpl]).
 
+    (* Pjumptable *)
+    + simpl in H0. destruct (par_nextblock _ _ _) eqn:PNEXT; try discriminate.
+      destruct (list_nth_z _ _) eqn:LISTS; try discriminate. unfold par_goto_label in H0.
+      destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ rsr PC) eqn:NB; try discriminate. inv H0.
+      inv MSR; inv MSW. eexists; split; try split.
+      * simpl. rewrite (H0 PC). Simpl. rewrite (H0 r). unfold par_nextblock in PNEXT. rewrite Pregmap.gso in PNEXT; try discriminate. rewrite PNEXT.
+        rewrite LISTS. unfold goto_label_deps. rewrite LPOS. unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity.
+      * Simpl.
+      * intros rr; destruct rr; unfold par_nextblock; Simpl.
+        destruct (preg_eq g GPR62). rewrite e. Simpl.
+        destruct (preg_eq g GPR63). rewrite e. Simpl. Simpl.
     (* Pj_l *)
     + simpl in H0. unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ _) eqn:NB; try discriminate. inv H0.
       inv MSR; inv MSW.
@@ -1857,20 +1943,56 @@ Proof.
     intros rr. destruct rr; unfold par_nextblock; Simpl.
 Qed.
 
-Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil).
-
-(* Lemma put in Parallelizability. 
-Lemma prun_iw_app_some:
-  forall c c' sr sw s' s'',
-  prun_iw Ge c sw sr = Some s' ->
-  prun_iw Ge c' s' sr = Some s'' ->
-  prun_iw Ge (c ++ c') sw sr = Some s''.
+Lemma forward_simu_par_control_Stuck ge fn rsr rsw mr mw sr sw sz ex:
+  Ge = Genv ge fn ->
+  match_states (State rsr mr) sr ->
+  match_states (State rsw mw) sw ->
+  parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) (par_nextblock (Ptrofs.repr sz) rsw) mw = Stuck ->
+  macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None.
 Proof.
-  induction c.
-  - simpl. intros. congruence.
-  - intros. simpl in *. destruct (macro_prun _ _ _ _); auto. eapply IHc; eauto. discriminate.
+  intros GENV MSR MSW H0. inv MSR; inv MSW. destruct ex as [ctl|]; try discriminate.
+  destruct ctl; destruct i; try discriminate; try (simpl; reflexivity).
+(* Pbuiltin *)
+  - simpl in *. rewrite (H1 PC). reflexivity.
+(* Pjumptable *)
+  - simpl in *. rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate.
+    destruct (rsr r); auto. destruct (list_nth_z _ _); auto. unfold par_goto_label in H0. unfold goto_label_deps.
+    destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); try discriminate; auto.
+(* Pj_l *)
+  - simpl in *. rewrite (H1 PC). unfold goto_label_deps. unfold par_goto_label in H0.
+    destruct (label_pos _ _ _); auto. simpl in *. unfold par_nextblock in H0. rewrite Pregmap.gss in H0. 
+    destruct (Val.offset_ptr _ _); try discriminate; auto.
+(* Pcb *)
+  - simpl in *. destruct (cmp_for_btest bt). destruct i.
+    -- destruct o.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
+        rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate.
+        destruct (Val.cmp_bool _ _ _); auto. destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0.
+        destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); auto. discriminate.
+      + rewrite (H1 PC). Simpl. rewrite (H1 r). reflexivity.
+    -- destruct o.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
+        rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate.
+        destruct (Val.cmpl_bool _ _ _); auto. destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0.
+        destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); auto. discriminate.
+      + rewrite (H1 PC). Simpl. rewrite (H1 r). reflexivity.
+(* Pcbu *)
+  - simpl in *. destruct (cmpu_for_btest bt). destruct i.
+    -- destruct o.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
+        rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate.
+        destruct (Val_cmpu_bool _ _ _); auto. destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0.
+        destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); auto. discriminate.
+      + rewrite (H1 PC). Simpl. rewrite (H1 r). reflexivity.
+    -- destruct o.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
+        rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate.
+        destruct (Val_cmplu_bool _ _ _); auto. destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0.
+        destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); auto. discriminate.
+      + rewrite (H1 PC). Simpl. rewrite (H1 r). reflexivity.
 Qed.
-*)
+
+Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil).
 
 Theorem forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy ex sz rs' m':
   Ge = Genv ge fn ->
@@ -1909,41 +2031,6 @@ Proof.
   erewrite prun_iw_app_Some; eauto. eassumption.
 Qed.
 
-Lemma trans_body_perserves_permutation bdy1 bdy2:
-  Permutation bdy1 bdy2 ->
-  Permutation (trans_body bdy1) (trans_body bdy2).
-Proof.
-  induction 1; simpl; econstructor; eauto.
-Qed.
-
-Lemma trans_body_app bdy1: forall bdy2,
-   trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2).
-Proof.
-  induction bdy1; simpl; congruence.
-Qed.
-
-Theorem trans_block_perserves_permutation bdy1 bdy2 b:
-  Permutation (bdy1 ++ bdy2) (body b) ->
-  Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)).
-Proof.
-  intro H; unfold trans_block, trans_block_aux.
-  eapply perm_trans.
-  - eapply Permutation_app_tail. 
-    apply trans_body_perserves_permutation.
-    apply Permutation_sym; eapply H.
-  - rewrite trans_body_app. rewrite <-! app_assoc.
-    apply Permutation_app_head.
-    apply Permutation_app_comm.
-Qed.
-
-Lemma forward_simu_par_wio_basic_Stuck ge fn rsr rsw mr mw sr sw bi:
-  Ge = Genv ge fn ->
-  match_states (State rsr mr) sr ->
-  match_states (State rsw mw) sw ->
-  parexec_basic_instr ge bi rsr rsw mr mw = Stuck ->
-  macro_prun Ge (trans_basic bi) sw sr sr = None.
-Admitted.
-
 Lemma forward_simu_par_body_Stuck bdy: forall ge fn rsr mr sr rsw mw sw,
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
@@ -1963,14 +2050,6 @@ Proof.
       intros X; simpl; rewrite X; auto.
 Qed.
 
-Lemma forward_simu_par_control_Stuck ge fn rsr rsw mr mw sr sw sz ex:
-  Ge = Genv ge fn ->
-  match_states (State rsr mr) sr ->
-  match_states (State rsw mw) sw ->
-  parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) (par_nextblock (Ptrofs.repr sz) rsw) mw = Stuck ->
-  macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None.
-Admitted.
-
 Lemma forward_simu_par_wio_stuck_bdy1 ge fn rs m s1' bdy1 sz ex:
   Ge = Genv ge fn ->
   match_states (State rs m) s1' ->
@@ -2000,6 +2079,33 @@ Proof.
   eapply forward_simu_par_body_Stuck. 4: eauto. all: eauto.
 Qed.
 
+Lemma trans_body_perserves_permutation bdy1 bdy2:
+  Permutation bdy1 bdy2 ->
+  Permutation (trans_body bdy1) (trans_body bdy2).
+Proof.
+  induction 1; simpl; econstructor; eauto.
+Qed.
+
+Lemma trans_body_app bdy1: forall bdy2,
+   trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2).
+Proof.
+  induction bdy1; simpl; congruence.
+Qed.
+
+Theorem trans_block_perserves_permutation bdy1 bdy2 b:
+  Permutation (bdy1 ++ bdy2) (body b) ->
+  Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)).
+Proof.
+  intro H; unfold trans_block, trans_block_aux.
+  eapply perm_trans.
+  - eapply Permutation_app_tail. 
+    apply trans_body_perserves_permutation.
+    apply Permutation_sym; eapply H.
+  - rewrite trans_body_app. rewrite <-! app_assoc.
+    apply Permutation_app_head.
+    apply Permutation_app_comm.
+Qed.
+
 Theorem forward_simu_par:
   forall rs1 m1 s1' b ge fn rs2 m2,
   Ge = Genv ge fn ->
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index cf0b2a0a..91d64a3f 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -913,8 +913,9 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co
     | MBreturn =>
         OK (make_epilogue f (Pret ::g nil))
       (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*) 
-    | MBjumptable _ _ =>
-        Error (msg "Asmblockgen.transl_instr_control MBjumptable")
+    | MBjumptable arg tbl =>
+      do r <- ireg_of arg;
+      OK (Pjumptable r tbl ::g nil)
     end
   end.
 
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index ea4d1918..63f4c136 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -883,11 +883,16 @@ Proof.
   intros until x2. intros Hbuiltin TIC.

   destruct ex.

   - destruct c.

+    (* MBcall *)

     + simpl in TIC. exploreInst; simpl; eauto.

+    (* MBtailcall *)

     + simpl in TIC. exploreInst; simpl; eauto.

+    (* MBbuiltin *)

     + assert (H: Some (MBbuiltin e l b) <>  Some (MBbuiltin e l b)).

         apply Hbuiltin. contradict H; auto.

+    (* MBgoto *)

     + simpl in TIC. exploreInst; simpl; eauto.

+    (* MBcond *)

     + simpl in TIC. unfold transl_cbranch in TIC. exploreInst; simpl; eauto.

       * unfold transl_opt_compuimm. exploreInst; simpl; eauto.

       * unfold transl_opt_compluimm. exploreInst; simpl; eauto.

@@ -895,7 +900,9 @@ Proof.
       * unfold transl_comp_notfloat64. exploreInst; simpl; eauto.

       * unfold transl_comp_float32. exploreInst; simpl; eauto.

       * unfold transl_comp_notfloat32. exploreInst; simpl; eauto.

-    + simpl in TIC. inv TIC.

+    (* MBjumptable *)

+    + simpl in TIC. exploreInst; simpl; eauto.

+    (* MBreturn *)

     + simpl in TIC. monadInv TIC. simpl. eauto.

   - monadInv TIC. simpl; auto.

 Qed.

@@ -1358,7 +1365,29 @@ Proof.
         intros. discriminate.

     + (* MBjumptable *)

       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.

-      inv TBC. inv TIC.

+      inv TBC. inv TIC. inv H0.

+

+      assert (f0 = f) by congruence. subst f0.

+      monadInv H1.

+      generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV.

+      assert (f1 = f) by congruence. subst f1.

+      exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef).

+        unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.

+      exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn.

+

+      intros [tc' [rs' [A [B C]]]].

+      exploit ireg_val; eauto. rewrite H13. intros LD; inv LD.

+      

+      repeat eexists.

+        rewrite H6. simpl extract_basic. simpl. eauto.

+        rewrite H7. simpl extract_ctl. simpl. Simpl. rewrite <- H1. unfold Mach.label in H14. unfold label. rewrite H14. eapply A.

+      econstructor; eauto.

+        eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen.

+        { assert (destroyed_by_jumptable = R62 :: R63 :: nil) by auto. rewrite H2 in H0. simpl in H0. inv H0.

+          destruct (preg_eq r' GPR63). subst. contradiction.

+          destruct (preg_eq r' GPR62). subst. contradiction.

+          destruct r'; Simpl. }

+        discriminate.

     + (* MBreturn *)

       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.

       inv TBC. inv TIC. inv H0.

diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index a6e9f04b..d553c612 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -211,6 +211,15 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset)
       Next (rsw#RA <- (rsr#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw
   | Picall r =>
       Next (rsw#RA <- (rsr#PC) #PC <- (rsr#r)) mw
+  | Pjumptable r tbl =>
+      match rsr#r with
+      | Vint n =>
+          match list_nth_z tbl (Int.unsigned n) with
+          | None => Stuck
+          | Some lbl => par_goto_label f lbl rsr (rsw #GPR62 <- Vundef #GPR63 <- Vundef) mw
+          end
+      | _ => Stuck
+      end
   | Pgoto s =>
       Next (rsw#PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw
   | Pigoto r =>
@@ -230,7 +239,6 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset)
       | (None, _) => Stuck
       end
 
-
 (** Pseudo-instructions *)
   | Pbuiltin ef args res =>
       Stuck (**r treated specially below *)
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index 2b3fb1aa..f494c67d 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -152,8 +152,7 @@ Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mre
 
 Definition destroyed_by_cond (cond: condition): list mreg := nil.
 
-(* Definition destroyed_by_jumptable: list mreg := R5 :: nil. *)
-Definition destroyed_by_jumptable: list mreg := nil.
+Definition destroyed_by_jumptable: list mreg := R62 :: R63 :: nil.
 
 Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
   match cl with
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 9e6e819c..32ca5d63 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -234,6 +234,7 @@ let ctl_flow_rec = function
   | Pj_l lbl -> { inst = "Pj_l"; write_locs = []; read_locs = []; imm = None ; is_control = true}
   | Pcb (bt, rs, lbl) -> { inst = "Pcb"; write_locs = []; read_locs = [Reg (IR rs)]; imm = None ; is_control = true}
   | Pcbu (bt, rs, lbl) -> { inst = "Pcbu"; write_locs = []; read_locs = [Reg (IR rs)]; imm = None ; is_control = true}
+  | Pjumptable (r, _) -> { inst = "Pjumptable"; write_locs = [Reg (IR GPR62); Reg (IR GPR63)]; read_locs = [Reg (IR r)]; imm = None ; is_control = true}
 
 let control_rec i =
   match i with
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index dd485ea4..4e33fc90 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -550,6 +550,7 @@ Proof.
   - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
   - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
   - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
 Qed.
 
 Lemma eval_offset_preserved:
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 6c34de19..60b8f094 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -384,10 +384,9 @@ Definition floatoflongu (e: expr) :=
   if Archi.splitlong then SplitLong.floatoflongu e else 
   Eop Ofloatoflongu (e:::Enil).
 
-(* SplitLong.longofsingle splits the operation into (longoffloat (floatofsingle e)) *)
-Definition longofsingle (e: expr) := SplitLong.longofsingle e.
+Definition longofsingle (e: expr) := longoffloat (floatofsingle e).
 
-Definition longuofsingle (e: expr) := SplitLong.longuofsingle e.
+Definition longuofsingle (e: expr) := longuoffloat (floatofsingle e).
 
 Definition singleoflong (e: expr) := SplitLong.singleoflong e.
 
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index dd4cfa69..11804d2e 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -703,16 +703,22 @@ Qed.
 
 Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle.
 Proof.
-  unfold longofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *)
-  eapply SplitLongproof.eval_longofsingle; eauto.
-(*   TrivialExists. *)
+  unfold longofsingle; red; intros.
+  destruct x; simpl in H0; inv H0. destruct (Float32.to_long f) as [n|] eqn:EQ; simpl in H2; inv H2.
+  exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B.
+  apply Float32.to_long_double in EQ.
+  eapply eval_longoffloat; eauto. simpl.
+  change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto.
 Qed.
 
 Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle.
 Proof.
   unfold longuofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *)
-  eapply SplitLongproof.eval_longuofsingle; eauto.
-(*   TrivialExists. *)
+  destruct x; simpl in H0; inv H0. destruct (Float32.to_longu f) as [n|] eqn:EQ; simpl in H2; inv H2.
+  exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B.
+  apply Float32.to_longu_double in EQ.
+  eapply eval_longuoffloat; eauto. simpl.
+  change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto.
 Qed.
 
 Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 4be94390..d9f49a5d 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -99,6 +99,14 @@ module Target (*: TARGET*) =
 
 (* Associate labels to floating-point constants and to symbols. *)
 
+    let print_tbl oc (lbl, tbl) =
+      fprintf oc "	.balign 4\n";
+      fprintf oc "%a:\n" label lbl;
+      List.iter
+        (fun l -> fprintf oc "	.4byte	%a\n"
+                    print_label l)
+        tbl
+
     let emit_constants oc lit =
       if exists_constants () then begin
          section oc lit;
@@ -264,6 +272,19 @@ module Target (*: TARGET*) =
          fprintf oc "	cb.%a	%a? %a\n" bcond bt ireg r print_label lbl
       | Ploopdo (r, lbl) ->
          fprintf oc "	loopdo	%a, %a\n" ireg r print_label lbl        
+      | Pjumptable (idx_reg, tbl) ->
+         let lbl = new_label() in
+         (* jumptables := (lbl, tbl) :: !jumptables; *)
+         let base_reg = if idx_reg=Asmblock.GPR63 then Asmblock.GPR62 else Asmblock.GPR63 in
+         fprintf oc "%s jumptable [ " comment;
+         List.iter (fun l -> fprintf oc "%a " print_label l) tbl;
+         fprintf oc "]\n";
+         fprintf oc "    make    %a = %a\n    ;;\n" ireg base_reg label lbl; 
+         fprintf oc "    lwz.xs  %a = %a[%a]\n    ;;\n" ireg base_reg ireg idx_reg ireg base_reg;
+         fprintf oc "    igoto   %a\n    ;;\n" ireg base_reg;
+         section oc Section_jumptable;
+         print_tbl oc (lbl, tbl);
+         section oc Section_text
 
       (* Load/Store instructions *)
       | Plb(rd, ra, ofs) ->
@@ -517,21 +538,14 @@ module Target (*: TARGET*) =
 
     let print_align oc alignment =
       fprintf oc "	.balign %d\n" alignment
-
-    let print_jumptable oc jmptbl =
-      let print_tbl oc (lbl, tbl) =
-        fprintf oc "%a:\n" label lbl;
-        List.iter
-          (fun l -> fprintf oc "	.long	%a - %a\n"
-                               print_label l label lbl)
-          tbl in
-      if !jumptables <> [] then
+      
+    let print_jumptable oc jmptbl = () 
+      (* if !jumptables <> [] then
         begin
           section oc jmptbl;
-          fprintf oc "	.balign 4\n";
           List.iter (print_tbl oc) !jumptables;
           jumptables := []
-        end
+        end *)
 
     let print_fun_info = elf_print_fun_info