From cdf83055d96e2af784a97c783c94b83ba2032ae1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 19 Nov 2009 13:31:08 +0000 Subject: Added support for jump tables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1181 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asm.v | 23 ++++++++++++++++++++++- arm/Asmgen.v | 3 +++ arm/Asmgenproof.v | 56 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ arm/PrintAsm.ml | 6 ++++++ 4 files changed, 87 insertions(+), 1 deletion(-) 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 -- cgit