diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-14 15:41:26 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-14 15:41:26 +0000 |
commit | 5aea6849eed83009e300b04ef17786643ead9cbc (patch) | |
tree | eb9a329ce46a7ddc568a2fba7692b8eaea1e618f /ia32/Asm.v | |
parent | fd0f28867db2f183216b27d7030265ae9e887586 (diff) | |
download | compcert-5aea6849eed83009e300b04ef17786643ead9cbc.tar.gz compcert-5aea6849eed83009e300b04ef17786643ead9cbc.zip |
Locations.v: add Loc.diff_dec.
ia32: lift restriction that 1st arg of ops cannot be ECX
(could be useful for a future, better reloading strategy)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1711 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asm.v')
-rw-r--r-- | ia32/Asm.v | 15 |
1 files changed, 3 insertions, 12 deletions
@@ -120,6 +120,7 @@ Inductive instruction: Type := | Pfld_m (a: addrmode) (**r [fld] from memory *) | Pfstp_f (rd: freg) (**r [fstp] to XMM register (pseudo) *) | Pfstp_m (a: addrmode) (**r [fstp] to memory *) + | Pxchg_rr (r1: ireg) (r2: ireg) (**r register-register exchange *) (** Moves with conversion *) | Pmovb_mr (a: addrmode) (rs: ireg) (**r [mov] (8-bit int) *) | Pmovw_mr (a: addrmode) (rs: ireg) (**r [mov] (16-bit int) *) @@ -380,18 +381,6 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool := | Vint n => Some (Int.eq n Int.zero) | _ => None end -(* - | Cond_nep => - match rs PF, rs ZF with - | Vint p, Vint z => Some (Int.eq p Int.one || Int.eq z Int.zero) - | _, _ => None - end - | Cond_enp => - match rs PF, rs ZF with - | Vint p, Vint z => Some (Int.eq p Int.zero && Int.eq z Int.one) - | _, _ => None - end -*) end. (** The semantics is purely small-step and defined as a function @@ -491,6 +480,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome Next (nextinstr (rs#rd <- (rs ST0) #ST0 <- Vundef)) m | Pfstp_m a => exec_store Mfloat64 m a rs ST0 + | Pxchg_rr r1 r2 => + Next (nextinstr (rs#r1 <- (rs r2) #r2 <- (rs r1))) m (** Moves with conversion *) | Pmovb_mr a r1 => exec_store Mint8unsigned m a rs r1 |