From 5aea6849eed83009e300b04ef17786643ead9cbc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 14 Aug 2011 15:41:26 +0000 Subject: 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 --- ia32/Asm.v | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) (limited to 'ia32/Asm.v') diff --git a/ia32/Asm.v b/ia32/Asm.v index 2eb6a8d..002119e 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -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 -- cgit v1.2.3