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

5 files changed, 24 insertions, 36 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 002119e..4fc38ba 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 4c1167b..478cdf5 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 5b98d27..e8c6757 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 27bc901..c00332e 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 1766a79..e1f0911 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)