diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 12:50:57 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 12:50:57 +0000 |
commit | 74487f079dd56663f97f9731cea328931857495c (patch) | |
tree | 9de10b895da39adffaf66bff983d6ed573898068 /powerpc | |
parent | 0486654fac91947fec93d18a0738dd7aa10bcf96 (diff) | |
download | compcert-74487f079dd56663f97f9731cea328931857495c.tar.gz compcert-74487f079dd56663f97f9731cea328931857495c.zip |
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
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Asm.v | 50 | ||||
-rw-r--r-- | powerpc/Asmgen.v | 10 | ||||
-rw-r--r-- | powerpc/Asmgenproof.v | 67 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 25 |
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 *) |