Added support for jump tables.

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

4 files changed, 87 insertions, 1 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index a8151a85..e8503bbd 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -148,7 +148,8 @@ Inductive instruction : Type :=
   | Pallocframe: Z -> Z -> int -> instruction      (**r allocate new stack frame *)
   | Pfreeframe: int -> instruction                 (**r deallocate stack frame and restore previous frame *)
   | Plabel: label -> instruction                   (**r define a code label *)
-  | Ploadsymbol: ireg -> ident -> int -> instruction. (**r load the address of a symbol *)
+  | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *)
+  | Pbtbl: ireg -> list label -> instruction.      (**r N-way branch through a jump table *)
 
 (** The pseudo-instructions are the following:
 
@@ -187,6 +188,14 @@ lbl:    .word   symbol
 >>
   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:
+<<
+        ldr     pc, [pc, reg]
+        mov     r0, r0          (* no-op *)
+        .word   table[0], table[1], ...
+>>
+  Note that [reg] contains 4 times the index of the desired table entry.
 *)
 
 Definition code := list instruction.
@@ -507,6 +516,18 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr rs) m
   | Ploadsymbol r1 lbl ofs =>
       OK (nextinstr (rs#r1 <- (symbol_offset lbl ofs))) m
+  | Pbtbl r tbl =>
+      match rs#r with
+      | Vint n => 
+          let pos := Int.signed n in
+          if zeq (Zmod pos 4) 0 then
+            match list_nth_z tbl (pos / 4) with
+            | None => Error
+            | Some lbl => goto_label c lbl rs m
+            end
+          else Error
+      | _ => Error
+      end
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 7e40949a..8e0805fe 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -483,6 +483,9 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pb lbl :: k
   | Mcond cond args lbl =>
       transl_cond cond args (Pbc (crbit_for_cond cond) lbl :: k)
+  | Mjumptable arg tbl =>
+      Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) ::
+      Pbtbl IR14 tbl :: k
   | Mreturn =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
         (Pfreeframe f.(fn_link_ofs) :: Pbreg IR14 :: k)
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 7b1fd62c..db84d64b 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -981,6 +981,61 @@ 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.
+  exploit list_nth_z_range; eauto. intro RANGE.
+  assert (SHIFT: Int.signed (Int.shl n (Int.repr 2)) = Int.signed n * 4).
+    rewrite Int.shl_mul.
+    rewrite Int.mul_signed.
+    apply Int.signed_repr.
+    split. apply Zle_trans with 0. vm_compute; congruence. omega. 
+    omega.
+  inv AT. simpl in H7. 
+  set (k1 := Pbtbl IR14 tbl :: transl_code f c).
+  set (rs1 := nextinstr (rs0 # IR14 <- (Vint (Int.shl n (Int.repr 2))))).
+  generalize (functions_transl _ _ H4); intro FN.
+  generalize (functions_transl_no_overflow _ _ H4); intro NOOV.
+  assert (exec_straight tge (transl_function f)
+            (Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) :: k1) rs0 m
+            k1 rs1 m).
+   apply exec_straight_one. 
+   simpl. rewrite <- (ireg_val _ _ _ _ AG H5). rewrite H. reflexivity. reflexivity. 
+  exploit exec_straight_steps_2; eauto. 
+  intros [ofs' [PC1 CT1]].
+  generalize (find_label_goto_label f lbl rs1 m _ _ _ FIND PC1 H2).
+  intros [rs3 [GOTO [AT3 INV3]]].
+  left; exists (State rs3 m); split.
+  eapply plus_right'. 
+  eapply exec_straight_steps_1; eauto.
+  econstructor; eauto. 
+  eapply find_instr_tail. unfold k1 in CT1. eauto.
+  unfold exec_instr.
+  change (rs1 IR14) with (Vint (Int.shl n (Int.repr 2))).
+Opaque Zmod.  Opaque Zdiv.
+  simpl. rewrite SHIFT. rewrite Z_mod_mult. rewrite zeq_true. 
+  rewrite Z_div_mult. 
+  change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq.
+  econstructor; eauto. 
+  eapply Mach.find_label_incl; eauto.
+  apply agree_exten_2 with rs1; auto. 
+  unfold rs1. apply agree_nextinstr. 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: function),
@@ -1141,6 +1196,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/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 9297a694..22399112 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -356,6 +356,12 @@ let print_instruction oc labels = function
       let lbl = label_symbol id ofs in
       fprintf oc "	ldr	%a, .L%d @ %a\n" 
          ireg r1 lbl print_symb_ofs (id, ofs); 1
+  | Pbtbl(r, tbl) ->
+      fprintf oc "	ldr	pc, [pc, %a]\n" ireg r;
+      fprintf oc "	mov	r0, r0\n"; (* no-op *)
+      List.iter
+        (fun l -> fprintf oc "	.word	%a\n" label (transl_label l));
+      2 + List.length tbl
 
 let no_fallthrough = function
   | Pb _ -> true