From 5b73a4f223a0cadb7df3f1320fed86cde0d67d6e Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 18 Aug 2011 15:28:46 +0000 Subject: More careful treatment of 'load immediate 0' as 'xor self' git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1718 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asm.v | 6 ++++++ ia32/Asmgen.v | 6 ++++-- ia32/Asmgenproof.v | 2 ++ ia32/Asmgenproof1.v | 26 ++++---------------------- ia32/PrintAsm.ml | 20 ++++++++------------ 5 files changed, 24 insertions(+), 36 deletions(-) (limited to 'ia32') diff --git a/ia32/Asm.v b/ia32/Asm.v index 002119e4..4fc38baf 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -149,6 +149,7 @@ Inductive instruction: Type := | Pand_ri (rd: ireg) (n: int) | Por_rr (rd: ireg) (r1: ireg) | Por_ri (rd: ireg) (n: int) + | Pxor_r (rd: ireg) (**r [xor] with self = set to zero *) | Pxor_rr (rd: ireg) (r1: ireg) | Pxor_ri (rd: ireg) (n: int) | Psal_rcl (rd: ireg) @@ -172,6 +173,7 @@ Inductive instruction: Type := | Pnegd (rd: freg) | Pabsd (rd: freg) | Pcomisd_ff (r1 r2: freg) + | Pxorpd_f (rd: freg) (**r [xor] with self = set to zero *) (** Branches and calls *) | Pjmp_l (l: label) | Pjmp_s (symb: ident) @@ -538,6 +540,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome Next (nextinstr_nf (rs#rd <- (Val.or rs#rd rs#r1))) m | Por_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.or rs#rd (Vint n)))) m + | Pxor_r rd => + Next (nextinstr_nf (rs#rd <- Vzero)) m | Pxor_rr rd r1 => Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd rs#r1))) m | Pxor_ri rd n => @@ -590,6 +594,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome Next (nextinstr (rs#rd <- (Val.absf rs#rd))) m | Pcomisd_ff r1 r2 => Next (nextinstr (compare_floats (rs r1) (rs r2) rs)) m + | Pxorpd_f rd => + Next (nextinstr_nf (rs#rd <- (Vfloat Float.zero))) m (** Branches and calls *) | Pjmp_l lbl => goto_label c lbl rs m diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 4c1167b5..478cdf5d 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -317,9 +317,11 @@ Definition transl_op | Omove, a1 :: nil => mk_mov (preg_of res) (preg_of a1) k | Ointconst n, nil => - do r <- ireg_of res; OK (Pmov_ri r n :: k) + do r <- ireg_of res; + OK ((if Int.eq_dec n Int.zero then Pxor_r r else Pmov_ri r n) :: k) | Ofloatconst f, nil => - do r <- freg_of res; OK (Pmovsd_fi r f :: k) + do r <- freg_of res; + OK ((if Float.eq_dec f Float.zero then Pxorpd_f r else Pmovsd_fi r f) :: k) | Ocast8signed, a1 :: nil => do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsb_rr r r1 k | Ocast8unsigned, a1 :: nil => diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 5b98d277..e8c6757f 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -455,6 +455,8 @@ Remark transl_op_label: Proof. unfold transl_op; intros. destruct op; ArgsInv; auto. eapply mk_mov_label; eauto. + destruct (Int.eq_dec i Int.zero); auto. + destruct (Float.eq_dec f Float.zero); auto. eapply mk_intconv_label; eauto. eapply mk_intconv_label; eauto. eapply mk_intconv_label; eauto. diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 27bc9013..c00332ed 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -1429,28 +1429,6 @@ Qed. (** Translation of arithmetic operations. *) -(* -Ltac TranslOpSimpl := - match goal with - | |- exists rs' : regset, - exec_straight ?c ?rs ?m ?k rs' ?m /\ - agree (Regmap.set ?res ?v ?ms) ?sp rs' => - (exists (nextinstr (rs#(ireg_of res) <- v)); - split; - [ apply exec_straight_one; - [ repeat (rewrite (ireg_val ms sp rs); auto); reflexivity - | reflexivity ] - | auto with ppcgen ]) - || - (exists (nextinstr (rs#(freg_of res) <- v)); - split; - [ apply exec_straight_one; - [ repeat (rewrite (freg_val ms sp rs); auto); reflexivity - | reflexivity ] - | auto with ppcgen ]) - end. -*) - Ltac ArgsInv := match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -1484,6 +1462,10 @@ Proof. (* move *) exploit mk_mov_correct; eauto. intros [rs2 [A [B C]]]. exists rs2. split. eauto. split. simpl. auto. intros. destruct H; auto. +(* intconst *) + inv EV. destruct (Int.eq_dec i Int.zero). subst i. TranslOp. TranslOp. +(* floatconst *) + inv EV. destruct (Float.eq_dec f Float.zero). subst f. TranslOp. TranslOp. (* cast8signed *) eapply mk_intconv_correct; eauto. (* cast8unsigned *) diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 1766a796..e1f0911d 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -475,11 +475,7 @@ let print_instruction oc = function | Pmov_rr(rd, r1) -> fprintf oc " movl %a, %a\n" ireg r1 ireg rd | Pmov_ri(rd, n) -> - let n = camlint_of_coqint n in - if n = 0l then - fprintf oc " xorl %a, %a\n" ireg rd ireg rd - else - fprintf oc " movl $%ld, %a\n" n ireg rd + fprintf oc " movl $%ld, %a\n" (camlint_of_coqint n) ireg rd | Pmov_rm(rd, a) -> fprintf oc " movl %a, %a\n" addressing a ireg rd | Pmov_mr(a, r1) -> @@ -492,13 +488,9 @@ let print_instruction oc = function fprintf oc " movapd %a, %a\n" freg r1 freg rd | Pmovsd_fi(rd, n) -> let b = Int64.bits_of_float n in - if b = 0L then (* +0.0 *) - fprintf oc " xorpd %a, %a %s +0.0\n" freg rd freg rd comment - else begin - let lbl = new_label() in - fprintf oc " movsd %a, %a %s %.18g\n" label lbl freg rd comment n; - float_literals := (lbl, b) :: !float_literals - end + let lbl = new_label() in + fprintf oc " movsd %a, %a %s %.18g\n" label lbl freg rd comment n; + float_literals := (lbl, b) :: !float_literals | Pmovsd_fm(rd, a) -> fprintf oc " movsd %a, %a\n" addressing a freg rd | Pmovsd_mf(a, r1) -> @@ -577,6 +569,8 @@ let print_instruction oc = function fprintf oc " orl %a, %a\n" ireg r1 ireg rd | Por_ri(rd, n) -> fprintf oc " orl $%a, %a\n" coqint n ireg rd + | Pxor_r(rd) -> + fprintf oc " xorl %a, %a\n" ireg rd ireg rd | Pxor_rr(rd, r1) -> fprintf oc " xorl %a, %a\n" ireg r1 ireg rd | Pxor_ri(rd, n) -> @@ -625,6 +619,8 @@ let print_instruction oc = function fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg rd | Pcomisd_ff(r1, r2) -> fprintf oc " comisd %a, %a\n" freg r2 freg r1 + | Pxorpd_f (rd) -> + fprintf oc " xorpd %a, %a\n" freg rd freg rd (** Branches and calls *) | Pjmp_l(l) -> fprintf oc " jmp %a\n" label (transl_label l) -- cgit