diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-18 15:28:46 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-18 15:28:46 +0000 |
| commit | 5b73a4f223a0cadb7df3f1320fed86cde0d67d6e (patch) | |
| tree | fd315fb086acb9e81882a2bc1b255b9562d8940d /ia32/Asm.v | |
| parent | 50ee6bdf639ffba989968abb9c24a57126ab35a4 (diff) | |
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
Diffstat (limited to 'ia32/Asm.v')
| -rw-r--r-- | ia32/Asm.v | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -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 |