begin jumptables (does not work)

5 files changed, 57 insertions, 8 deletions

diff --git a/common/Switchaux.ml b/common/Switchaux.ml
index 06337e7d..69300feb 100644
--- a/common/Switchaux.ml
+++ b/common/Switchaux.ml
@@ -80,10 +80,6 @@ let compile_switch_as_jumptable default cases minkey maxkey =
               CTaction default)
 
 let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
-  (* FIXME DMonniaux disable jump tables until we can prove them through *)
-  false
-
-(*
   let span = Z.sub maxkey minkey in
   assert (Z.ge span Z.zero);
   let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases)
@@ -91,7 +87,6 @@ let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
   numcases >= 7           (* small jump tables are always less efficient *)
   && Z.le table_size tree_size
   && Z.lt span (Z.of_uint Sys.max_array_length)
- *)
   
 let compile_switch modulus default table =
   let (tbl, keys) = normalize_table table in
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 493f4a05..8c918c2d 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -69,6 +69,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 **)

@@ -228,6 +229,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 d335801e..dfe46e04 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -233,6 +233,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 *)
@@ -1470,6 +1471,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 501ec212..8c799927 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
@@ -540,6 +550,7 @@ 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)) ]
   | Pdiv => [(#GPR0, Op (Control Odiv) (Name (#GPR0) @ Name (#GPR1) @ Enil)); (#RA, Name (#RA))]
   | Pdivu => [(#GPR0, Op (Control Odivu) (Name (#GPR0) @ Name (#GPR1) @ Enil)); (#RA, Name (#RA))]
   | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)]
@@ -879,8 +890,37 @@ Proof.
         Simpl.
       * Simpl.
       * intros rr; destruct rr; Simpl. destruct (preg_eq GPR0 g); Simpl. rewrite e. Simpl.
+    (* Pjumptable *)
+    + unfold goto_label in *.
+      destruct (nextblock b rs r) eqn:NB_r in *; try discriminate.
+      destruct (list_nth_z _ _) eqn:LI in *; try discriminate.
+      destruct (label_pos _ _ _) eqn:LPOS in *; try discriminate.
+      rewrite Pregmap.gso in H0; try discriminate.
+      rewrite Pregmap.gso in H0; try discriminate.
+      eexists; split; try split.
+      * simpl control_eval.
+        rewrite (H3 PC).
+        simpl.
+        unfold goto_label_deps.
+        Simpl.
+        rewrite H3.
+        destruct (rs r); try discriminate.
+      ++ 
+      destruct (nextblock b rs PC) eqn:NB_PC in *; try discriminate.
+      inv H0.
+      
+      destruct (s (# PC)) eqn:sPC in *; try discriminate.
+      rewrite Pregmap.gso; try discriminate.
+      destruct (nextblock b rs r) eqn:NB_r in *; try discriminate.
+      destruct (list_nth_z _ _) eqn:LI in *; try discriminate.
+      destruct (label_pos _ _ _) eqn:LPOS in *; try discriminate.
+      destruct (nextblock b rs PC) eqn:NB_PC in *; try discriminate.
+      inv H1; try discriminate.
+      assumption.
     (* 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.
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 5b00a64f..f3b4b921 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -911,8 +911,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.