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

4 files changed, 111 insertions, 41 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 0e6032fe..18dc93ab 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -115,6 +115,7 @@ Inductive instruction : Type :=
   | Pbs: ident -> instruction                                 (**r branch to symbol *)
   | Pblr: instruction                                         (**r branch to contents of register LR *)
   | Pbt: crbit -> label -> instruction                        (**r branch if true *)
+  | Pbtbl: ireg -> list label -> instruction                  (**r N-way branch through a jump table *)
   | Pcmplw: ireg -> ireg -> instruction                       (**r unsigned integer comparison *)
   | Pcmplwi: ireg -> constant -> instruction                  (**r same, with immediate argument *)
   | Pcmpw: ireg -> ireg -> instruction                        (**r signed integer comparison *)
@@ -196,8 +197,8 @@ Inductive instruction : Type :=
   Expands to a float load [lfd] from an address in the constant data section
   initialized with the floating-point constant:
 <<
-        addis   r2, 0, ha16(lbl)
-        lfd     rdst, lo16(lbl)(r2)
+        addis   r12, 0, ha16(lbl)
+        lfd     rdst, lo16(lbl)(r12)
         .const_data
 lbl:    .double floatcst
         .text
@@ -218,8 +219,8 @@ lbl:    .double floatcst
   constant [2^31], subtract [2^31] if bigger, then convert to a signed
   integer as above, then add back [2^31] if needed.  Expands to:
 <<
-        addis   r2, 0, ha16(lbl1)
-        lfd     f13, lo16(lbl1)(r2)
+        addis   r12, 0, ha16(lbl1)
+        lfd     f13, lo16(lbl1)(r12)
         fcmpu   cr7, rsrc, f13
         cror    30, 29, 30
         beq     cr7, lbl2
@@ -242,12 +243,12 @@ lbl1:   .long   0x41e00000, 0x00000000    # 2^31 in double precision
   arithmetic over a memory word, which our memory model and axiomatization
   of floats cannot express.  Expands to:
 <<
-        addis   r2, 0, 0x4330
-        stwu    r2, -8(r1)
-        addis   r2, rsrc, 0x8000
-        stw     r2, 4(r1)
-        addis   r2, 0, ha16(lbl)
-        lfd     f13, lo16(lbl)(r2)
+        addis   r12, 0, 0x4330
+        stwu    r12, -8(r1)
+        addis   r12, rsrc, 0x8000
+        stw     r12, 4(r1)
+        addis   r12, 0, ha16(lbl)
+        lfd     f13, lo16(lbl)(r12)
         lfd     rdst, 0(r1)
         addi    r1, r1, 8
         fsub    rdst, rdst, f13
@@ -260,11 +261,11 @@ lbl:    .long   0x43300000, 0x80000000
 - [Piuctf]: convert an unsigned integer to a float.  The expansion is close
   to that [Pictf], and equally obscure.
 <<
-        addis   r2, 0, 0x4330
-        stwu    r2, -8(r1)
+        addis   r12, 0, 0x4330
+        stwu    r12, -8(r1)
         stw     rsrc, 4(r1)
-        addis   r2, 0, ha16(lbl)
-        lfd     f13, lo16(lbl)(r2)
+        addis   r12, 0, ha16(lbl)
+        lfd     f13, lo16(lbl)(r12)
         lfd     rdst, 0(r1)
         addi    r1, r1, 8
         fsub    rdst, rdst, f13
@@ -294,6 +295,18 @@ lbl:    .long   0x43300000, 0x00000000
 >>
   Again, our memory model cannot comprehend that this operation
   frees (logically) the current stack frame.
+- [Pbtbl reg table]: this is a N-way branch, implemented via a jump table
+  as follows:
+<<
+        rlwinm  r12, reg, 2, 0, 29
+        addis   r12, r12, ha16(lbl)
+        lwz     r12, lo16(lbl)(r12)
+        mtctr   r12
+        bctr    r12
+        .const_data
+lbl:    .long   table[0], table[1], ...
+        .text
+>>
 *)
 
 Definition code := list instruction.
@@ -608,6 +621,15 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       | Vint n => if Int.eq n Int.zero then OK (nextinstr rs) m else goto_label c lbl rs m
       | _ => Error
       end
+  | Pbtbl r tbl =>
+      match rs#r with
+      | Vint n => 
+          match list_nth_z tbl (Int.signed n) with
+          | None => Error
+          | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
+          end
+      | _ => Error
+      end
   | Pcmplw r1 r2 =>
       OK (nextinstr (compare_uint rs rs#r1 rs#r2)) m
   | Pcmplwi r1 cst =>
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index aebb4834..4beabb1c 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -502,6 +502,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       let p := crbit_for_cond cond in
       transl_cond cond args
         (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k)
+  | Mjumptable arg tbl =>
+      Pbtbl (ireg_of arg) tbl :: k
   | Mreturn =>
       Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
       Pmtlr GPR12 ::
@@ -523,17 +525,11 @@ Definition transl_function (f: Mach.function) :=
   Pstw GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
   transl_code f f.(fn_code).
 
-Fixpoint code_size (c: code) : Z :=
-  match c with
-  | nil => 0
-  | instr :: c' => code_size c' + 1
-  end.
-
 Open Local Scope string_scope.
 
 Definition transf_function (f: Mach.function) : res Asm.code :=
   let c := transl_function f in
-  if zlt Int.max_unsigned (code_size c)
+  if zlt Int.max_unsigned (list_length_z c)
   then Errors.Error (msg "code size exceeded")
   else Errors.OK c.
 
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 2710eddd..4e45c8ea 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -65,19 +65,19 @@ Proof.
   intros. 
   destruct (functions_translated _ _ H) as [tf [A B]].
   rewrite A. generalize B. unfold transf_fundef, transf_partial_fundef, transf_function.
-  case (zlt Int.max_unsigned (code_size (transl_function f))); simpl; intro.
+  case (zlt Int.max_unsigned (list_length_z (transl_function f))); simpl; intro.
   congruence. intro. inv B0. auto.
 Qed.
 
 Lemma functions_transl_no_overflow:
   forall b f,
   Genv.find_funct_ptr ge b = Some (Internal f) ->
-  code_size (transl_function f) <= Int.max_unsigned.
+  list_length_z (transl_function f) <= Int.max_unsigned.
 Proof.
   intros. 
   destruct (functions_translated _ _ H) as [tf [A B]].
   generalize B. unfold transf_fundef, transf_partial_fundef, transf_function.
-  case (zlt Int.max_unsigned (code_size (transl_function f))); simpl; intro.
+  case (zlt Int.max_unsigned (list_length_z (transl_function f))); simpl; intro.
   congruence. intro; omega.
 Qed.
 
@@ -105,21 +105,23 @@ Proof.
   eauto.
 Qed.
 
+(*
 Remark code_size_pos:
   forall fn, code_size fn >= 0.
 Proof.
   induction fn; simpl; omega.
 Qed.
+*)
 
 Remark code_tail_bounds:
   forall fn ofs i c,
-  code_tail ofs fn (i :: c) -> 0 <= ofs < code_size fn.
+  code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn.
 Proof.
   assert (forall ofs fn c, code_tail ofs fn c ->
-          forall i c', c = i :: c' -> 0 <= ofs < code_size fn).
+          forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn).
   induction 1; intros; simpl. 
-  rewrite H. simpl. generalize (code_size_pos c'). omega.
-  generalize (IHcode_tail _ _ H0). omega.
+  rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega.
+  rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega.
   eauto.
 Qed.
 
@@ -138,7 +140,7 @@ Qed.
 
 Lemma code_tail_next_int:
   forall fn ofs i c,
-  code_size fn <= Int.max_unsigned ->
+  list_length_z fn <= Int.max_unsigned ->
   code_tail (Int.unsigned ofs) fn (i :: c) ->
   code_tail (Int.unsigned (Int.add ofs Int.one)) fn c.
 Proof.
@@ -167,7 +169,7 @@ Inductive transl_code_at_pc: val -> block -> Mach.function -> Mach.code -> Prop
 Lemma exec_straight_steps_1:
   forall fn c rs m c' rs' m',
   exec_straight tge fn c rs m c' rs' m' ->
-  code_size fn <= Int.max_unsigned ->
+  list_length_z fn <= Int.max_unsigned ->
   forall b ofs,
   rs#PC = Vptr b ofs ->
   Genv.find_funct_ptr tge b = Some (Internal fn) ->
@@ -191,7 +193,7 @@ Qed.
 Lemma exec_straight_steps_2:
   forall fn c rs m c' rs' m',
   exec_straight tge fn c rs m c' rs' m' ->
-  code_size fn <= Int.max_unsigned ->
+  list_length_z fn <= Int.max_unsigned ->
   forall b ofs,
   rs#PC = Vptr b ofs ->
   Genv.find_funct_ptr tge b = Some (Internal fn) ->
@@ -284,7 +286,7 @@ Lemma label_pos_code_tail:
   exists pos',
   label_pos lbl pos c = Some pos' 
   /\ code_tail (pos' - pos) c c'
-  /\ pos < pos' <= pos + code_size c.
+  /\ pos < pos' <= pos + list_length_z c.
 Proof.
   induction c. 
   simpl; intros. discriminate.
@@ -293,12 +295,12 @@ Proof.
   intro EQ; injection EQ; intro; subst c'.
   exists (pos + 1). split. auto. split.
   replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. 
-  generalize (code_size_pos c). omega. 
+  rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. 
   intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]].
   exists pos'. split. auto. split.
   replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega.
   constructor. auto. 
-  omega.
+  rewrite list_length_z_cons. omega.
 Qed.
 
 (** The following lemmas show that the translation from Mach to PPC
@@ -863,7 +865,7 @@ Proof.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inversion WTI.
   inv AT. 
-  assert (NOOV: code_size (transl_function f) <= Int.max_unsigned).
+  assert (NOOV: list_length_z (transl_function f) <= Int.max_unsigned).
     eapply functions_transl_no_overflow; eauto.
   destruct ros; simpl in H; simpl transl_code in H7.
   (* Indirect call *)
@@ -940,7 +942,7 @@ Proof.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inversion WTI.
   inversion AT. subst b f0 c0.
-  assert (NOOV: code_size (transl_function f) <= Int.max_unsigned).
+  assert (NOOV: list_length_z (transl_function f) <= Int.max_unsigned).
     eapply functions_transl_no_overflow; eauto.
   destruct ros; simpl in H; simpl in H9.
   (* Indirect call *)
@@ -1127,6 +1129,40 @@ Proof.
   auto with ppcgen.
 Qed.
 
+Lemma exec_Mjumptable_prop:
+  forall (s : list stackframe) (fb : block) (f : function) (sp : val)
+         (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction)
+         (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label)
+         (c' : Mach.code),
+  rs arg = Vint n ->
+  list_nth_z tbl (Int.signed n) = Some lbl ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  Mach.find_label lbl (fn_code f) = Some c' ->
+  exec_instr_prop
+    (Machconcr.State s fb sp (Mjumptable arg tbl :: c) rs m) E0
+    (Machconcr.State s fb sp c' rs m).
+Proof.
+  intros; red; intros; inv MS.
+  assert (f0 = f) by congruence. subst f0.
+  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
+  intro WTI. inv WTI.
+  pose (rs1 := rs0 # GPR12 <- Vundef # CTR <- Vundef).
+  inv AT. simpl in H6.
+  assert (rs1 PC = Vptr fb ofs). rewrite H3. reflexivity.
+  generalize (functions_transl _ _ H1); intro FN.
+  generalize (functions_transl_no_overflow _ _ H1); intro NOOV.
+  exploit find_label_goto_label; eauto. intros [rs2 [A [B C]]].
+  left; exists (State rs2 m); split.
+  apply plus_one. econstructor. symmetry; eauto. eauto.
+  eapply find_instr_tail. eauto. 
+  simpl. rewrite (ireg_val _ _ _ _ AG H4) in H. rewrite H. 
+  change label with Mach.label; rewrite H0. eexact A. 
+  econstructor; eauto. 
+  eapply Mach.find_label_incl; eauto.
+  apply agree_exten_2 with rs1; auto.
+  unfold rs1. repeat apply agree_set_other; auto with ppcgen.
+Qed.
+
 Lemma exec_Mreturn_prop:
   forall (s : list stackframe) (fb stk : block) (soff : int)
          (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function),
@@ -1292,6 +1328,7 @@ Proof
            exec_Mgoto_prop
            exec_Mcond_true_prop
            exec_Mcond_false_prop
+           exec_Mjumptable_prop
            exec_Mreturn_prop
            exec_function_internal_prop
            exec_function_external_prop
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 539d9894..df1b0629 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -261,6 +261,17 @@ let print_instruction oc labels = function
       fprintf oc "	blr\n"
   | Pbt(bit, lbl) ->
       fprintf oc "	bt	%a, %a\n" crbit bit label (transl_label lbl)
+  | Pbtbl(r, tbl) ->
+      let lbl = new_label() in
+      fprintf oc "	rlwinm	%a, %a, 2, 0, 29\n" ireg GPR12 ireg r;
+      fprintf oc "	addis	%a, %a, %a\n" ireg GPR12 ireg GPR12 label_high lbl;
+      fprintf oc "	lwz	%a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12;
+      fprintf oc "	mtctr	%a\n" ireg GPR12;
+      fprintf oc "	bctr\n";
+      fprintf oc "%a:" label lbl;
+      List.iter
+        (fun l -> fprintf oc "	.long	%a\n" label (transl_label l))
+        tbl
   | Pcmplw(r1, r2) ->
       fprintf oc "	cmplw	%a, %a, %a\n" creg 0 ireg r1 ireg r2
   | Pcmplwi(r1, c) ->
@@ -472,11 +483,15 @@ let print_instruction oc labels = function
       if Labelset.mem lbl labels then
         fprintf oc "%a:\n" label (transl_label lbl)
 
-let rec labels_of_code = function
-  | [] -> Labelset.empty
+let rec labels_of_code accu = function
+  | [] ->
+      accu
   | (Pb lbl | Pbf(_, lbl) | Pbt(_, lbl)) :: c ->
-      Labelset.add lbl (labels_of_code c)
-  | _ :: c -> labels_of_code c
+      labels_of_code (Labelset.add lbl accu) c
+  | Pbtbl(_, tbl) :: c ->
+      labels_of_code (List.fold_right Labelset.add tbl accu) c
+  | _ :: c ->
+      labels_of_code accu c
 
 let print_function oc name code =
   Hashtbl.clear current_function_labels;
@@ -488,7 +503,7 @@ let print_function oc name code =
   if not (Cil2Csyntax.atom_is_static name) then
     fprintf oc "	.globl %a\n" symbol name;
   fprintf oc "%a:\n" symbol name;
-  List.iter (print_instruction oc (labels_of_code code)) code
+  List.iter (print_instruction oc (labels_of_code Labelset.empty code)) code
 
 (* Generation of stub functions *)