From a02e52919de565fc3fba82723b48200fbf034ff9 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 20 Sep 2017 15:38:14 +0100 Subject: add support for x86 lock prefix (also remove unused Read/Write_tag kind in etc/regfp.sail. --- etc/regfp.sail | 4 +- src/lem_interp/sail_impl_base.lem | 6 ++ x86/x64.sail | 210 ++++++++++++++++++++------------------ 3 files changed, 119 insertions(+), 101 deletions(-) diff --git a/etc/regfp.sail b/etc/regfp.sail index c0792df0..15d1a489 100644 --- a/etc/regfp.sail +++ b/etc/regfp.sail @@ -32,7 +32,6 @@ typedef diafp = const union { typedef read_kind = enumerate { Read_plain; - Read_tag; Read_reserve; Read_acquire; Read_exclusive; @@ -43,11 +42,11 @@ typedef read_kind = enumerate { Read_RISCV_reserved; Read_RISCV_reserved_acquire; Read_RISCV_reserved_strong_acquire; + Read_X86_locked; } typedef write_kind = enumerate { Write_plain; - Write_tag; Write_conditional; Write_release; Write_exclusive; @@ -57,6 +56,7 @@ typedef write_kind = enumerate { Write_RISCV_conditional; Write_RISCV_conditional_release; Write_RISCV_conditional_strong_release; + Write_X86_locked; } typedef barrier_kind = enumerate { diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index e6169762..e39c4421 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -441,6 +441,7 @@ type read_kind = | Read_RISCV_acquire | Read_RISCV_strong_acquire | Read_RISCV_reserved | Read_RISCV_reserved_acquire | Read_RISCV_reserved_strong_acquire + | Read_X86_locked instance (Show read_kind) let show = function @@ -455,6 +456,7 @@ instance (Show read_kind) | Read_RISCV_reserved -> "Read_RISCV_reserved" | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire" | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire" + | Read_X86_locked -> "Read_X86_locked" end end @@ -469,6 +471,7 @@ type write_kind = | Write_RISCV_release | Write_RISCV_strong_release | Write_RISCV_conditional | Write_RISCV_conditional_release | Write_RISCV_conditional_strong_release + | Write_X86_locked instance (Show write_kind) let show = function @@ -482,6 +485,7 @@ instance (Show write_kind) | Write_RISCV_conditional -> "Write_RISCV_conditional" | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release" | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release" + | Write_X86_locked -> "Write_X86_locked" end end @@ -580,6 +584,7 @@ instance (EnumerationType read_kind) | Read_RISCV_reserved -> 8 | Read_RISCV_reserved_acquire -> 9 | Read_RISCV_reserved_strong_acquire -> 10 + | Read_X86_locked -> 11 end end @@ -595,6 +600,7 @@ instance (EnumerationType write_kind) | Write_RISCV_conditional -> 7 | Write_RISCV_conditional_release -> 8 | Write_RISCV_conditional_strong_release -> 9 + | Write_X86_locked -> 10 end end diff --git a/x86/x64.sail b/x86/x64.sail index 7cce4262..0b0d2230 100644 --- a/x86/x64.sail +++ b/x86/x64.sail @@ -103,15 +103,17 @@ register bit[1] OF -------------------------------------------------------------------------- *) val extern forall Nat 'n. (qword, [|'n|]) -> (bit[8 * 'n]) effect { rmem } rMEM - - +val extern forall Nat 'n. (qword, [|'n|]) -> (bit[8 * 'n]) effect { rmem } rMEM_locked +function forall Nat 'n. (bit[8 * 'n]) effect { rmem } rMEMl ((bool) locked, (qword) addr, ([|'n|]) size) = + if locked then rMEM_locked(addr, size) else rMEM(addr, size) val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_locked val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval val extern unit -> unit effect { barr } X86_MFENCE -function forall Nat 'n. unit effect {eamem, wmv} wMEM ((qword) addr, ([|'n|]) len, (bit[8 * 'n]) data) = { - MEMea(addr, len); +function forall Nat 'n. unit effect {eamem, wmv} wMEM ((bool) locked, (qword) addr, ([|'n|]) len, (bit[8 * 'n]) data) = { + if locked then MEMea_locked(addr, len) else MEMea(addr, len); MEMval(addr, len, data); } @@ -265,7 +267,7 @@ function qword restrict_size ((wsize) sz, (qword) imm) = function regn sub4 ((regn) r) = negative_to_zero (r - 4) -function qword effect { rreg, rmem } EA ((ea) e) = +function qword effect { rreg, rmem } EA ((bool) locked, (ea) e) = switch e { case (Ea_i(sz,i)) -> restrict_size(sz,i) case (Ea_r((Sz8(have_rex)),r)) -> @@ -274,13 +276,13 @@ function qword effect { rreg, rmem } EA ((ea) e) = else (REG[sub4 (r)] >> 8) & 0x00000000000000FF case (Ea_r(sz,r)) -> restrict_size(sz, REG[r]) - case (Ea_m((Sz8(_)),a)) -> EXTZ (rMEM(a, 1)) - case (Ea_m(Sz16,a)) -> EXTZ (rMEM(a, 2)) - case (Ea_m(Sz32,a)) -> EXTZ (rMEM(a, 4)) - case (Ea_m(Sz64,a)) -> rMEM(a, 8) + case (Ea_m((Sz8(_)),a)) -> EXTZ (rMEMl(locked, a, 1)) + case (Ea_m(Sz16,a)) -> EXTZ (rMEMl(locked, a, 2)) + case (Ea_m(Sz32,a)) -> EXTZ (rMEMl(locked, a, 4)) + case (Ea_m(Sz64,a)) -> rMEMl(locked, a, 8) } -function unit effect { wmem, wreg, escape } wEA ((ea) e, (qword) w) = +function unit effect { wmem, wreg, escape } wEA ((bool) locked, (ea) e, (qword) w) = switch e { case (Ea_i(_,_)) -> exit () case (Ea_r((Sz8(have_rex)),r)) -> @@ -304,15 +306,15 @@ function unit effect { wmem, wreg, escape } wEA ((ea) e, (qword) w) = } case (Ea_r(Sz32,r)) -> REG[r] := (qword) (EXTZ (w[31 .. 0])) case (Ea_r(Sz64,r)) -> REG[r] := w - case (Ea_m((Sz8(_)),a)) -> wMEM(a, 1, w[7 .. 0]) - case (Ea_m(Sz16,a)) -> wMEM(a, 2, w[15 .. 0]) - case (Ea_m(Sz32,a)) -> wMEM(a, 4, w[31 .. 0]) - case (Ea_m(Sz64,a)) -> wMEM(a, 8, w) + case (Ea_m((Sz8(_)),a)) -> wMEM(locked, a, 1, w[7 .. 0]) + case (Ea_m(Sz16,a)) -> wMEM(locked, a, 2, w[15 .. 0]) + case (Ea_m(Sz32,a)) -> wMEM(locked, a, 4, w[31 .. 0]) + case (Ea_m(Sz64,a)) -> wMEM(locked, a, 8, w) } -function (ea, qword, qword) read_dest_src_ea ((wsize) sz, (dest_src) ds) = +function (ea, qword, qword) read_dest_src_ea ((bool) locked, (wsize) sz, (dest_src) ds) = let e = ea_dest (sz, ds) in - (e, EA(e), EA(ea_src(sz, ds))) + (e, EA(locked, e), EA(locked, ea_src(sz, ds))) function qword call_dest_from_ea ((ea) e) = switch e { @@ -419,28 +421,28 @@ function (qword, bit, bit) add_with_carry_out ((wsize) sz, (qword) a, (qword) b) function (qword, bit, bit) sub_with_borrow ((wsize) sz, (qword) a, (qword) b) = (a - b, (bit) (a < b), word_signed_overflow_sub (sz, a, b)) -function unit write_arith_result ((wsize) sz, (qword) w, (bit) c, (bit) x, (ea) e) = +function unit write_arith_result ((bool) locked, (wsize) sz, (qword) w, (bit) c, (bit) x, (ea) e) = { write_arith_eflags (sz, w, c, x); - wEA (e) := w; + wEA (locked, e) := w; } -function unit write_arith_result_no_CF_OF ((wsize) sz, (qword) w, (ea) e) = +function unit write_arith_result_no_CF_OF ((bool) locked, (wsize) sz, (qword) w, (ea) e) = { write_arith_eflags_except_CF_OF (sz, w); - wEA (e) := w; + wEA (locked, e) := w; } -function unit write_logical_result ((wsize) sz, (qword) w, (ea) e) = +function unit write_logical_result ((bool) locked, (wsize) sz, (qword) w, (ea) e) = { write_arith_eflags_except_CF_OF (sz, w); - wEA (e) := w; + wEA (locked, e) := w; } -function unit write_result_erase_eflags ((qword) w, (ea) e) = +function unit write_result_erase_eflags ((bool) locked, (qword) w, (ea) e) = { erase_eflags (); - wEA (e) := w; + wEA (locked, e) := w; } function qword effect { escape } sign_extension ((qword) w, (wsize) size1, (wsize) size2) = @@ -485,23 +487,23 @@ function qword sar ((wsize) sz, (qword) a, (qword) b) = case Sz64 -> ASR64 (a, b[5 .. 0]) } -function unit write_binop ((wsize) sz, (binop_name) bop, (qword) a, (qword) b, (ea) e) = +function unit write_binop ((bool) locked, (wsize) sz, (binop_name) bop, (qword) a, (qword) b, (ea) e) = switch bop { case Add -> let (w,c,x) = add_with_carry_out (sz, a, b) in - write_arith_result (sz, w, c, x, e) + write_arith_result (locked, sz, w, c, x, e) case Sub -> let (w,c,x) = sub_with_borrow (sz, a, b) in - write_arith_result (sz, w, c, x, e) + write_arith_result (locked, sz, w, c, x, e) case Cmp -> let (w,c,x) = sub_with_borrow (sz, a, b) in write_arith_eflags (sz, w, c, x) case Test -> write_logical_eflags (sz, a & b) - case And -> write_logical_result (sz, a & b, e) (* XXX rmn30 wrong flags? *) - case Xor -> write_logical_result (sz, a ^ b, e) - case Or -> write_logical_result (sz, a | b, e) - case Rol -> write_result_erase_eflags (rol (sz, a, b), e) - case Ror -> write_result_erase_eflags (ror (sz, a, b), e) - case Sar -> write_result_erase_eflags (sar (sz, a, b), e) - case Shl -> write_result_erase_eflags (a << mask_shift (sz, b), e) - case Shr -> write_result_erase_eflags (a >> mask_shift (sz, b), e) + case And -> write_logical_result (locked, sz, a & b, e) (* XXX rmn30 wrong flags? *) + case Xor -> write_logical_result (locked, sz, a ^ b, e) + case Or -> write_logical_result (locked, sz, a | b, e) + case Rol -> write_result_erase_eflags (locked, rol (sz, a, b), e) + case Ror -> write_result_erase_eflags (locked, ror (sz, a, b), e) + case Sar -> write_result_erase_eflags (locked, sar (sz, a, b), e) + case Shl -> write_result_erase_eflags (locked, a << mask_shift (sz, b), e) + case Shr -> write_result_erase_eflags (locked, a >> mask_shift (sz, b), e) case Adc -> { let carry = (bit) CF in @@ -509,7 +511,7 @@ function unit write_binop ((wsize) sz, (binop_name) bop, (qword) a, (qword) b, ( { CF := (bit) ((int) (value_width (sz)) <= unsigned(a) + unsigned(b)); OF := undefined; - write_arith_result_no_CF_OF (sz, result, e); + write_arith_result_no_CF_OF (locked, sz, result, e); } } case Sbb -> @@ -519,18 +521,18 @@ function unit write_binop ((wsize) sz, (binop_name) bop, (qword) a, (qword) b, ( { CF := (bit) (unsigned(a) < unsigned(b) + (int) carry); OF := undefined; - write_arith_result_no_CF_OF (sz, result, e); + write_arith_result_no_CF_OF (locked, sz, result, e); } } case _ -> exit () } -function unit write_monop ((wsize) sz, (monop_name) mop, (qword) a, (ea) e) = +function unit write_monop ((bool) locked, (wsize) sz, (monop_name) mop, (qword) a, (ea) e) = switch mop { - case Not -> wEA(e) := ~(a) - case Dec -> write_arith_result_no_CF_OF (sz, a - 1, e) - case Inc -> write_arith_result_no_CF_OF (sz, a + 1, e)(* XXX rmn30 should set OF *) - case Neg -> { write_arith_result_no_CF_OF (sz, 0 - a, e); + case Not -> wEA(locked, e) := ~(a) + case Dec -> write_arith_result_no_CF_OF (locked, sz, a - 1, e) + case Inc -> write_arith_result_no_CF_OF (locked, sz, a + 1, e)(* XXX rmn30 should set OF *) + case Neg -> { write_arith_result_no_CF_OF (locked, sz, 0 - a, e); CF := undefined; } } @@ -566,12 +568,12 @@ function qword pop_aux () = function unit push_aux ((qword) w) = { RSP := RSP - 8; - wMEM(RSP, 8) := w; + wMEM(false, RSP, 8) := w; } -function unit pop ((rm) r) = wEA (ea_rm (Sz64,r)) := pop_aux() +function unit pop ((rm) r) = wEA (false, ea_rm (Sz64,r)) := pop_aux() function unit pop_rip () = RIP := pop_aux() -function unit push ((imm_rm) i) = push_aux (EA (ea_imm_rm (i))) +function unit push ((imm_rm) i) = push_aux (EA (false, ea_imm_rm (i))) function unit push_rip () = push_aux (RIP) function unit drop ((qword) i) = if i[7 ..0] != 0 then () else RSP := RSP + i @@ -589,11 +591,11 @@ val ast -> unit effect {escape, rmem, rreg, undef, eamem, wmv, wreg, barr} execu Binop ========================================================================== *) -union ast member (binop_name,wsize,dest_src) Binop +union ast member (bool,binop_name,wsize,dest_src) Binop -function clause execute (Binop (bop,sz,ds)) = - let (e, val_dst, val_src) = read_dest_src_ea (sz, ds) in - write_binop (sz, bop, val_dst, val_src, e) +function clause execute (Binop (locked,bop,sz,ds)) = + let (e, val_dst, val_src) = read_dest_src_ea (locked, sz, ds) in + write_binop (locked, sz, bop, val_dst, val_src, e) (* ========================================================================== CALL @@ -627,20 +629,20 @@ function clause execute CMC = CF := ~(CF) CMPXCHG ========================================================================== *) -union ast member (wsize,rm,regn) CMPXCHG +union ast member (bool, wsize,rm,regn) CMPXCHG -function clause execute (CMPXCHG (sz,r,n)) = +function clause execute (CMPXCHG (locked, sz,r,n)) = let src = Ea_r(sz, n) in let acc = Ea_r(sz, 0) in (* RAX *) let dst = ea_rm(sz, r) in - let val_dst = EA(dst) in - let val_acc = EA(src) in + let val_dst = EA(locked, dst) in + let val_acc = EA(false, acc) in { - write_binop (sz, Cmp, val_acc, val_dst, src); + write_binop (locked, sz, Cmp, val_acc, val_dst, src); if val_acc == val_dst then - wEA(dst) := EA (src) + wEA(locked, dst) := EA (false, src) else - wEA(acc) := val_dst; + wEA(false, acc) := val_dst; } (* ========================================================================== @@ -653,15 +655,15 @@ function clause execute (DIV (sz,r)) = let w = (int) (value_width(sz)) in let eax = Ea_r(sz, 0) in (* RAX *) let edx = Ea_r(sz, 2) in (* RDX *) - let n = unsigned(EA(edx)) * w + unsigned(EA(eax)) in - let d = unsigned(EA(ea_rm(sz, r))) in + let n = unsigned(EA(false, edx)) * w + unsigned(EA(false, eax)) in + let d = unsigned(EA(false, ea_rm(sz, r))) in let q = n quot d in let m = n mod d in if d == 0 | w < q then exit () else { - wEA(eax) := (qword) q; - wEA(edx) := (qword) m; + wEA(false, eax) := (qword) q; + wEA(false, edx) := (qword) m; erase_eflags(); } @@ -689,7 +691,7 @@ function clause execute (Jcc (c,i)) = union ast member rm JMP -function clause execute (JMP (r)) = RIP := EA (ea_rm (Sz64, r)) +function clause execute (JMP (r)) = RIP := EA (false, ea_rm (Sz64, r)) (* ========================================================================== LEA @@ -700,7 +702,7 @@ union ast member (wsize,dest_src) LEA function clause execute (LEA (sz,ds)) = let src = ea_src (sz, ds) in let dst = ea_dest (sz, ds) in - wEA(dst) := get_ea_address (src) + wEA(false, dst) := get_ea_address (src) (* ========================================================================== LEAVE @@ -739,10 +741,10 @@ function clause execute (MFENCE) = Monop ========================================================================== *) -union ast member (monop_name,wsize,rm) Monop +union ast member (bool,monop_name,wsize,rm) Monop -function clause execute (Monop (mop,sz,r)) = - let e = ea_rm (sz, r) in write_monop (sz, mop, EA(e), e) +function clause execute (Monop (locked,mop,sz,r)) = + let e = ea_rm (sz, r) in write_monop (locked, sz, mop, EA(locked, e), e) (* ========================================================================== MOV @@ -754,7 +756,7 @@ function clause execute (MOV (c,sz,ds)) = if read_cond (c) then let src = ea_src (sz, ds) in let dst = ea_dest (sz, ds) in - wEA(dst) := EA(src) + wEA(false, dst) := EA(false, src) else () (* ========================================================================== @@ -766,7 +768,7 @@ union ast member (wsize,dest_src,wsize) MOVSX function clause execute (MOVSX (sz1,ds,sz2)) = let src = ea_src (sz1, ds) in let dst = ea_dest (sz2, ds) in - wEA(dst) := sign_extension (EA(src), sz1, sz2) + wEA(false, dst) := sign_extension (EA(false, src), sz1, sz2) (* ========================================================================== MOVZX @@ -777,7 +779,7 @@ union ast member (wsize,dest_src,wsize) MOVZX function clause execute (MOVZX (sz1,ds,sz2)) = let src = ea_src (sz1, ds) in let dst = ea_dest (sz2, ds) in - wEA(dst) := EA(src) + wEA(false, dst) := EA(false, src) (* ========================================================================== MUL @@ -787,16 +789,16 @@ union ast member (wsize,rm) MUL function clause execute (MUL (sz,r)) = let eax = Ea_r (sz, 0) in (* RAX *) - let val_eax = EA(eax) in - let val_src = EA(ea_rm (sz, r)) in + let val_eax = EA(false, eax) in + let val_src = EA(false, ea_rm (sz, r)) in switch sz { - case (Sz8(_)) -> wEA(Ea_r(Sz16,0)) := (val_eax * val_src)[63 .. 0] + case (Sz8(_)) -> wEA(false, Ea_r(Sz16,0)) := (val_eax * val_src)[63 .. 0] case _ -> let m = val_eax * val_src in let edx = Ea_r (sz, 2) in (* RDX *) { - wEA(eax) := m[63 .. 0]; - wEA(edx) := (m >> size_width(sz))[63 .. 0] + wEA(false, eax) := m[63 .. 0]; + wEA(false, edx) := (m >> size_width(sz))[63 .. 0] } } @@ -843,7 +845,7 @@ function clause execute (RET (i)) = union ast member (cond,bool,rm) SET function clause execute (SET (c,b,r)) = - wEA(ea_rm(Sz8(b),r)) := if read_cond (c) then 1 else 0 + wEA(false, ea_rm(Sz8(b),r)) := if read_cond (c) then 1 else 0 (* ========================================================================== STC @@ -857,32 +859,32 @@ function clause execute STC = CF := true XADD ========================================================================== *) -union ast member (wsize,rm,regn) XADD +union ast member (bool, wsize,rm,regn) XADD -function clause execute (XADD (sz,r,n)) = +function clause execute (XADD (locked,sz,r,n)) = let src = Ea_r (sz, n) in let dst = ea_rm (sz, r) in - let val_src = EA(src) in - let val_dst = EA(dst) in + let val_src = EA(false, src) in + let val_dst = EA(locked, dst) in { - wEA(src) := val_dst; - write_binop (sz, Add, val_src, val_dst, dst); + wEA(false, src) := val_dst; + write_binop (locked, sz, Add, val_src, val_dst, dst); } (* ========================================================================== XCHG ========================================================================== *) -union ast member (wsize,rm,regn) XCHG +union ast member (bool,wsize,rm,regn) XCHG -function clause execute (XCHG (sz,r,n)) = +function clause execute (XCHG (locked,sz,r,n)) = let src = Ea_r (sz, n) in let dst = ea_rm (sz, r) in - let val_src = EA(src) in - let val_dst = EA(dst) in + let val_src = EA(false, src) in + let val_dst = EA(locked, dst) in { - wEA(src) := val_dst; - wEA(dst) := val_src; + wEA(false, src) := val_dst; + wEA(locked, dst) := val_src; } end ast @@ -1302,14 +1304,16 @@ function (instruction_kind, regfps, regfps, regfps) regfp_dest_src ((dest_src) d } (* as above but where destination is also a source operand *) -function (instruction_kind, regfps, regfps, regfps) regfp_dest_src_rmw ((dest_src) ds) = +function (instruction_kind, regfps, regfps, regfps) regfp_dest_src_rmw (locked, (dest_src) ds) = + let rk = if locked then Read_X86_locked else Read_plain in + let wk = if locked then Write_X86_locked else Write_plain in switch ds { case (Rm_i (r_m, i)) -> let (m,rds, ars) = regfp_rm(r_m) in - (if m then IK_mem_rmw(Read_plain, Write_plain) else IK_simple, append(rds, ars), rds, ars) + (if m then IK_mem_rmw(rk, wk) else IK_simple, append(rds, ars), rds, ars) case (Rm_r (r_m, r)) -> let (m,rds, ars) = regfp_rm(r_m) in - (if m then IK_mem_rmw(Read_plain, Write_plain) else IK_simple, RFull(GPRstr[r]) :: append(rds, ars), rds, ars) + (if m then IK_mem_rmw(rk, wk) else IK_simple, RFull(GPRstr[r]) :: append(rds, ars), rds, ars) case (R_rm (r, r_m)) -> let rds = [|| RFull(GPRstr[r]) ||] in let (m,rs,ars) = regfp_rm(r_m) in @@ -1372,9 +1376,9 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( Dia := DIAFP_none; x := (qword) RIP; switch instr { - case(Binop (binop, sz, ds)) -> { + case(Binop (locked, binop, sz, ds)) -> { let flags = regfp_binop_flags (binop) in - let (ik', iRs, oRs, aRs) = regfp_dest_src_rmw(ds) in { + let (ik', iRs, oRs, aRs) = regfp_dest_src_rmw(locked, ds) in { ik := ik'; iR := append(iRs, iR); oR := append(flags, append(oRs, oR)); @@ -1398,9 +1402,11 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( iR := RFull("CF") :: iR; oR := RFull("CF") :: oR; } - case(CMPXCHG (sz, r_m, reg) ) -> + case(CMPXCHG (locked, sz, r_m, reg) ) -> + let rk = if locked then Read_X86_locked else Read_plain in + let wk = if locked then Write_X86_locked else Write_plain in let (m, rs, aRs) = regfp_rm (r_m) in { - iK := if m then IK_mem_rmw (Read_plain, Write_plain) else IK_simple; + iK := if m then IK_mem_rmw (rk, wk) else IK_simple; iR := RFull("RAX") :: RFull(GPRstr[reg]) :: append(rs, aRs); oR := RFull("RAX") :: append(regfp_binop_flags(Cmp), rs); aR := aRs; @@ -1447,9 +1453,11 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( Nias := NIAFP_concrete_address(RIP + imm64) :: Nias; } case(MFENCE ) -> iK := IK_barrier (Barrier_x86_MFENCE) - case(Monop (monop, sz, r_m) ) -> + case(Monop (locked, monop, sz, r_m) ) -> + let rk = if locked then Read_X86_locked else Read_plain in + let wk = if locked then Write_X86_locked else Write_plain in let (m, rds, ars) = regfp_rm(r_m) in { - iK := if m then IK_mem_rmw(Read_plain, Write_plain) else IK_simple; + iK := if m then IK_mem_rmw(rk, wk) else IK_simple; iR := append(rds, ars); oR := append(all_flags_but_cf_of, rds); (* XXX fix flags *) aR := ars; @@ -1516,16 +1524,20 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( aR := ars; } case(STC ) -> oR := [|| RFull("CF") ||] - case(XADD (sz, r_m, reg) ) -> + case(XADD (locked, sz, r_m, reg) ) -> + let rk = if locked then Read_X86_locked else Read_plain in + let wk = if locked then Write_X86_locked else Write_plain in let (m, rs, ars) = regfp_rm(r_m) in { - iK := if m then IK_mem_rmw(Read_plain, Write_plain) else IK_simple; + iK := if m then IK_mem_rmw(rk, wk) else IK_simple; iR := RFull(GPRstr[reg]) :: append(rs, ars); oR := RFull(GPRstr[reg]) :: append(rs, all_flags); aR := ars; } - case(XCHG (sz, r_m, reg) ) -> + case(XCHG (locked, sz, r_m, reg) ) -> + let rk = if locked then Read_X86_locked else Read_plain in + let wk = if locked then Write_X86_locked else Write_plain in let (m, rs, ars) = regfp_rm(r_m) in { - iK := if m then IK_mem_rmw(Read_plain, Write_plain) else IK_simple; + iK := if m then IK_mem_rmw(rk, wk) else IK_simple; iR := RFull(GPRstr[reg]) :: append(rs, ars); oR := RFull(GPRstr[reg]) :: rs; aR := ars; -- cgit v1.2.3