diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-21 16:11:50 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-21 16:11:50 +0000 |
commit | d2b9858f3f5e013bbd9d2221c8d1a3d2960665be (patch) | |
tree | 82d17ae170e7595045604663b152a04afe3e9c4c | |
parent | 88e55a6729b58cfc2ce32ed526dfd3c9cdf4feef (diff) |
powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a certain customer's code
backend/Coloringaux: avoid spilling the dummy result registers for built-ins that have no result.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1799 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | backend/Coloringaux.ml | 39 | ||||
-rw-r--r-- | powerpc/SelectOp.vp | 7 | ||||
-rw-r--r-- | powerpc/SelectOpproof.v | 15 |
3 files changed, 50 insertions, 11 deletions
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml index ab7d141..1f4e20d 100644 --- a/backend/Coloringaux.ml +++ b/backend/Coloringaux.ml @@ -809,21 +809,38 @@ let spill_costs f = let process_instr () pc i = match i with | Inop _ -> () - | Iop(Op.Omove, arg::nil, res, _) -> charge 1 arg; charge 1 res - | Iop(op, args, res, _) -> charge_list 10 args; charge 10 res - | Iload(chunk, addr, args, dst, _) -> charge_list 10 args; charge 10 dst - | Istore(chunk, addr, args, src, _) -> charge_list 10 args; charge 10 src + | Iop(Op.Omove, arg::nil, res, _) -> + charge 1 arg; charge 1 res + | Iop(op, args, res, _) -> + charge_list 10 args; charge 10 res + | Iload(chunk, addr, args, dst, _) -> + charge_list 10 args; charge 10 dst + | Istore(chunk, addr, args, src, _) -> + charge_list 10 args; charge 10 src | Icall(sg, ros, args, res, _) -> charge_ros 10 ros; charge_list 1 args; charge 1 res | Itailcall(sg, ros, args) -> charge_ros 10 ros; charge_list 1 args - | Ibuiltin(EF_annot _, args, res, _) -> () (* not actually used *) - | Ibuiltin(EF_annot_val _, args, res, _) -> charge_list 1 args; charge 1 res - | Ibuiltin(ef, args, res, _) -> charge_list 10 args; charge 10 res - | Icond(cond, args, _, _) -> charge_list 10 args - | Ijumptable(arg, _) -> charge 10 arg - | Ireturn(Some r) -> charge 1 r - | Ireturn None -> () in + | Ibuiltin(EF_annot _, args, res, _) -> + (* arguments are not actually used, so charge 0 for them; + result is not used but should not be spilled, so charge a lot *) + charge 1_000_000 res + | Ibuiltin(EF_annot_val _, args, res, _) -> + (* like a move *) + charge_list 1 args; charge 1 res + | Ibuiltin((EF_vstore _|EF_vstore_global _|EF_memcpy _), args, res, _) -> + (* result is not used but should not be spilled, so charge a lot *) + charge_list 10 args; charge 1_000_000 res + | Ibuiltin(ef, args, res, _) -> + charge_list 10 args; charge 10 res + | Icond(cond, args, _, _) -> + charge_list 10 args + | Ijumptable(arg, _) -> + charge 10 arg + | Ireturn(Some r) -> + charge 1 r + | Ireturn None -> + () in charge_list 1 f.fn_params; PTree.fold process_instr f.fn_code (); (* Result is cost function reg -> (num accesses, integer cost *) diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 40c9011..3bb5544 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -210,6 +210,13 @@ Nondetfunction andimm (n1: int) (e2: expr) := match e2 with | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.and n1 n2)) Enil + | Eop (Oandimm n2) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil) => + let n := Int.and n1 n2 in + if Int.eq (Int.shru (Int.shl n amount) amount) n + && Int.ltu amount Int.iwordsize + then rolm t2 (Int.sub Int.iwordsize amount) + (Int.and (Int.shru Int.mone amount) n) + else Eop (Oandimm n) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil) | Eop (Oandimm n2) (t2:::Enil) => Eop (Oandimm (Int.and n1 n2)) (t2:::Enil) | Eop (Orolm amount2 mask2) (t2:::Enil) => diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 8ad9807..cc14d33 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -343,6 +343,21 @@ Theorem eval_andimm: Proof. intros; red; intros until x. unfold andimm. case (andimm_match a); intros. InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto. + set (n' := Int.and n n2). + destruct (Int.eq (Int.shru (Int.shl n' amount) amount) n' && + Int.ltu amount Int.iwordsize) as []_eqn. + InvEval. destruct (andb_prop _ _ Heqb). + generalize (Int.eq_spec (Int.shru (Int.shl n' amount) amount) n'). rewrite H1; intros. + replace (Val.and x (Vint n)) + with (Val.rolm v0 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n')). + apply eval_rolm; auto. + subst. destruct v0; simpl; auto. rewrite H3. simpl. decEq. rewrite Int.and_assoc. + rewrite (Int.and_commut n2 n). + transitivity (Int.and (Int.shru i amount) (Int.and n n2)). + rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto. + symmetry. apply Int.shr_and_shru_and. auto. + set (e2 := Eop (Oshrimm amount) (t2 ::: Enil)) in *. + InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. InvEval. subst. TrivialExists. simpl. destruct v1; auto. simpl. unfold Int.rolm. rewrite Int.and_assoc. |