From f1ceca440c0322001abe6c5de79bd4bc309fc002 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 12 Feb 2013 15:17:33 +0000 Subject: Updated PowerPC port to new integers. Added options -falign-branch-targets and -falign-cond-branches (experimental). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2113 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgenproof.v | 1 + powerpc/Asmgenproof1.v | 15 +++++++++----- powerpc/Op.v | 3 +-- powerpc/PrintAsm.ml | 56 +++++++++++++++++++++++++++++++++----------------- 4 files changed, 49 insertions(+), 26 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index e99049c2..de9decbd 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -385,6 +385,7 @@ Remark rolm_label: Proof. intros; unfold rolm. case (is_rlw_mask mask). reflexivity. +Opaque Int.eq. simpl. autorewrite with labels. auto. Qed. Hint Rewrite rolm_label: labels. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index f1c206e8..56cb2240 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -75,9 +75,11 @@ Qed. Lemma low_high_s: forall n, Int.add (Int.shl (high_s n) (Int.repr 16)) (low_s n) = n. Proof. - intros. rewrite Int.shl_mul_two_p. + intros. + rewrite Int.shl_mul_two_p. unfold high_s. rewrite <- (Int.divu_pow2 (Int.sub n (low_s n)) (Int.repr 65536) (Int.repr 16)). + 2: reflexivity. change (two_p (Int.unsigned (Int.repr 16))) with 65536. set (x := Int.sub n (low_s n)). assert (x = Int.add (Int.mul (Int.divu x (Int.repr 65536)) (Int.repr 65536)) @@ -88,9 +90,10 @@ Proof. change 0 with (0 mod 65536). change (Int.unsigned (Int.repr 65536)) with 65536. apply Int.eqmod_mod_eq. omega. - unfold x, low_s. eapply Int.eqmod_trans. - eapply Int.eqm_eqmod_two_p with (n := 16). compute; auto. - unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. + unfold x, low_s. eapply Int.eqmod_trans. + apply Int.eqmod_divides with Int.modulus. + unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. + exists 65536. compute; auto. replace 0 with (Int.unsigned n - Int.unsigned n) by omega. apply Int.eqmod_sub. apply Int.eqmod_refl. apply Int.eqmod_sign_ext'. compute; auto. @@ -98,7 +101,6 @@ Proof. rewrite <- H. unfold x. rewrite Int.sub_add_opp. rewrite Int.add_assoc. rewrite (Int.add_commut (Int.neg (low_s n))). rewrite <- Int.sub_add_opp. rewrite Int.sub_idem. apply Int.add_zero. - reflexivity. Qed. (** * Correspondence between Mach registers and PPC registers *) @@ -998,6 +1000,7 @@ Lemma transl_cond_correct_1: /\ forall r, is_data_reg r = true -> rs'#r = rs#r. Proof. intros. +Opaque Int.eq. destruct cond; simpl in H; TypeInv; simpl; UseTypeInfo. (* Ccomp *) fold (Val.cmp c (rs (ireg_of m0)) (rs (ireg_of m1))). @@ -1171,6 +1174,7 @@ Proof. rewrite (Int.add_commut (Int.neg (Int.add i Int.mone))). rewrite <- Int.sub_add_opp. rewrite Int.sub_add_r. rewrite Int.sub_idem. rewrite Int.add_zero_l. rewrite Int.add_neg_zero. rewrite Int.add_zero_l. +Transparent Int.eq. unfold Int.add_carry, Int.eq. rewrite Int.unsigned_zero. rewrite Int.unsigned_mone. unfold negb, Val.of_bool, Vtrue, Vfalse. @@ -1269,6 +1273,7 @@ Proof. destruct (mreg_type r1); apply exec_straight_one; auto. split. repeat SIMP. intros; repeat SIMP. (* Other instructions *) +Opaque Int.eq. destruct op; simpl; simpl in H3; injection H3; clear H3; intros; TypeInv; simpl in *; UseTypeInfo; inv EV; try (TranslOpSimpl). (* Ointconst *) diff --git a/powerpc/Op.v b/powerpc/Op.v index 58bcb2ca..4a1fb622 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -1044,8 +1044,7 @@ Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool := | O => rlw_accepting s | S m => - let (b, y) := Int.Z_bin_decomp x in - is_rlw_mask_rec m (rlw_transition s b) y + is_rlw_mask_rec m (rlw_transition s (Z.odd x)) (Z.div2 x) end. Definition is_rlw_mask (x: int) : bool := diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 0d2d201e..2ba3cfeb 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -219,12 +219,6 @@ let rolm_mask n = assert (!count = 2 || (!count = 0 && !last)); (!mb, !me-1) -(* Base-2 log of a Caml integer *) - -let rec log2 n = - assert (n > 0); - if n = 1 then 0 else 1 + log2 (n lsr 1) - (* Built-ins. They come in three flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; @@ -489,7 +483,7 @@ let short_cond_branch tbl pc lbl_dest = let float_literals : (int * int64) list ref = ref [] let jumptables : (int * label list) list ref = ref [] -let print_instruction oc tbl pc = function +let print_instruction oc tbl pc fallthrough = function | Padd(r1, r2, r3) -> fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Padde(r1, r2, r3) -> @@ -529,6 +523,8 @@ let print_instruction oc tbl pc = function | Pbctrl -> fprintf oc " bctrl\n" | Pbf(bit, lbl) -> + if !Clflags.option_faligncondbranchs > 0 then + fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs; if short_cond_branch tbl pc lbl then fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl) else begin @@ -544,6 +540,8 @@ let print_instruction oc tbl pc = function | Pblr -> fprintf oc " blr\n" | Pbt(bit, lbl) -> + if !Clflags.option_faligncondbranchs > 0 then + fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs; if short_cond_branch tbl pc lbl then fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl) else begin @@ -729,6 +727,8 @@ let print_instruction oc tbl pc = function | Pxoris(r1, r2, c) -> fprintf oc " xoris %a, %a, %a\n" ireg r1 ireg r2 constant c | Plabel lbl -> + if (not fallthrough) && !Clflags.option_falignbranchtargets > 0 then + fprintf oc " .balign %d\n" !Clflags.option_falignbranchtargets; fprintf oc "%a:\n" label (transl_label lbl) | Pbuiltin(ef, args, res) -> begin match ef with @@ -762,6 +762,15 @@ let print_instruction oc tbl pc = function assert false end +(* Determine if an instruction falls through *) + +let instr_fall_through = function + | Pb _ -> false + | Pbctr -> false + | Pbs _ -> false + | Pblr -> false + | _ -> true + (* Estimate the size of an Asm instruction encoding, in number of actual PowerPC instructions. We can over-approximate. *) @@ -782,6 +791,7 @@ let instr_size = function | EF_builtin(name, sg) -> begin match extern_atom name with | "__builtin_bswap" -> 3 + | "__builtin_fcti" -> 4 | _ -> 1 end | EF_vload chunk -> @@ -813,11 +823,11 @@ let rec label_positions tbl pc = function (* Emit a sequence of instructions *) -let rec print_instructions oc tbl pc = function +let rec print_instructions oc tbl pc fallthrough = function | [] -> () | i :: c -> - print_instruction oc tbl pc i; - print_instructions oc tbl (pc + instr_size i) c + print_instruction oc tbl pc fallthrough i; + print_instructions oc tbl (pc + instr_size i) (instr_fall_through i) c (* Print the code for a function *) @@ -842,23 +852,23 @@ let print_function oc name code = | _ -> (Section_text, Section_literal, Section_jumptable) in section oc text; let alignment = - match !Clflags.option_falignfunctions with Some n -> log2 n | None -> 2 in - fprintf oc " .align %d\n" alignment; + match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in + fprintf oc " .balign %d\n" alignment; if not (C2C.atom_is_static name) then fprintf oc " .globl %a\n" symbol name; fprintf oc "%a:\n" symbol name; - print_instructions oc (label_positions PTree.empty 0 code) 0 code; + print_instructions oc (label_positions PTree.empty 0 code) 0 true code; fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name; if !float_literals <> [] then begin section oc lit; - fprintf oc " .align 3\n"; + fprintf oc " .balign 8\n"; List.iter (print_literal oc) !float_literals; float_literals := [] end; if !jumptables <> [] then begin section oc jmptbl; - fprintf oc " .align 2\n"; + fprintf oc " .balign 4\n"; List.iter (print_jumptable oc) !jumptables; jumptables := [] end @@ -871,7 +881,7 @@ let re_variadic_stub = Str.regexp "\\(.*\\)\\$[if]*$" let variadic_stub oc stub_name fun_name args = section oc Section_text; - fprintf oc " .align 2\n"; + fprintf oc " .balign 4\n"; fprintf oc ".L%s$stub:\n" stub_name; (* bit 6 must be set if at least one argument is a float; clear otherwise *) if List.mem Tfloat args @@ -948,13 +958,13 @@ let print_var oc name v = | _ -> Section_data true and align = match C2C.atom_alignof name with - | Some a -> log2 a - | None -> 3 in (* 8-alignment is a safe default *) + | Some a -> a + | None -> 8 in (* 8-alignment is a safe default *) let name_sec = name_of_section sec in if name_sec <> "COMM" then begin fprintf oc " %s\n" name_sec; - fprintf oc " .align %d\n" align; + fprintf oc " .balign %d\n" align; if not (C2C.atom_is_static name) then fprintf oc " .globl %a\n" symbol name; fprintf oc "%a:\n" symbol name; @@ -976,8 +986,16 @@ let print_globdef oc (name, gdef) = | Gfun f -> print_fundef oc name f | Gvar v -> print_var oc name v +let print_prologue oc = + match target with + | Linux -> + () + | Diab -> + fprintf oc " .xopt align-fill-text = 0x60000000\n" + let print_program oc p = stubbed_functions := IdentSet.empty; List.iter record_extfun p.prog_defs; + print_prologue oc; List.iter (print_globdef oc) p.prog_defs -- cgit