diff options
| -rw-r--r-- | x86/x64.sail | 809 |
1 files changed, 809 insertions, 0 deletions
diff --git a/x86/x64.sail b/x86/x64.sail new file mode 100644 index 00000000..46f7e741 --- /dev/null +++ b/x86/x64.sail @@ -0,0 +1,809 @@ +(*========================================================================*) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + +default Order dec + +val extern forall Nat 'n. (bit['n],[|'n|]) -> bit['n] effect pure ASR +val extern forall Nat 'n. (bit['n],[|'n|]) -> bit['n] effect pure LSR +val extern forall Nat 'n. (bit['n],[|'n|]) -> bit['n] effect pure ROR +val extern forall Nat 'n. (bit['n],[|'n|]) -> bit['n] effect pure ROL +val cast bool -> bit effect pure cast_bool_bit +val cast bit -> int effect pure cast_bit_int +val extern forall Num 'n. int -> bit['n] effect pure cast_int_vec +val extern forall 'n, 'm, 'o, 'n <= 0, 'm <= 'o. [|'n:'m|] -> [|0:'o|] effect pure negative_to_zero + +typedef byte = bit[8] +typedef qword = bit[64] +typedef regn = [|15|] +typedef byte_stream = list<byte> +typedef ostream = option<byte_stream> + +(* -------------------------------------------------------------------------- + Registers + -------------------------------------------------------------------------- *) + +(* Program Counter *) + +register qword RIP + +(* General purpose registers *) + +register qword RAX (* 0 *) +register qword RCX (* 1 *) +register qword RDX (* 2 *) +register qword RBX (* 3 *) +register qword RSP (* 4 *) +register qword RBP (* 5 *) +register qword RSI (* 6 *) +register qword RDI (* 7 *) +register qword R8 +register qword R9 +register qword R10 +register qword R11 +register qword R12 +register qword R13 +register qword R14 +register qword R15 + +let (vector<0,16,inc,(register<qword>)>) REG = + [RAX,RCX,RDX,RBX,RSP,RBP,RSI,RDI,R8,R9,R10,R11,R12,R13,R14,R15] + +(* Flags *) + +register bit CF +register bit PF +register bit AF +register bit ZF +register bit SF +register bit OF + +(* -------------------------------------------------------------------------- + Memory + -------------------------------------------------------------------------- *) + +val extern forall Nat 'n. (qword, [|'n|]) -> (bit[8 * 'n]) effect { rmem } MEM + +val extern forall Nat 'n. (qword, [|'n|], bit[8 * 'n]) -> unit effect { wmem } wMEM + +(* -------------------------------------------------------------------------- + Helper functions + -------------------------------------------------------------------------- *) + +(* Instruction addressing modes *) + +typedef size = const union { + bool Sz8; + unit Sz16; + unit Sz32; + unit Sz64; +} + +typedef base = const union { + unit NoBase; + unit RipBase; + regn RegBase; +} + +typedef scale_index = (bit[2],regn) + +typedef rm = const union { + regn Reg; + (option<scale_index>,base,qword) Mem; +} + +typedef dest_src = const union { + (rm,qword) Rm_i; + (rm,regn) Rm_r; + (regn,rm) R_rm; +} + +typedef imm_rm = const union { + rm Rm; + qword Imm; +} + +typedef monop_name = enumerate { Dec; Inc; Not; Neg } + +typedef binop_name = enumerate { + Add; Or; Adc; Sbb; And; Sub; Xor; Cmp; Rol; Ror; Rcl; Rcr; Shl; Shr; Test; Sar +} + +typedef cond = enumerate { + O; NO; B; NB; E; NE; NA; A; S; NS; P; NP; L; NL; NG; G; ALWAYS +} + +(* Effective addresses *) + +typedef ea = const union { + (size,qword) Ea_i; + (size,regn) Ea_r; + (size,qword) Ea_m; +} + +function qword ea_index ((option<scale_index>) index) = + switch (index) { + case None -> 0x0000000000000000 + case (Some(scale, idx)) -> + let x = (qword) (0x0000000000000001 << scale) in + let y = (qword) (REG[idx]) in + let z = (bit[128]) (x * y) in + z[63 .. 0] + } + +function qword ea_base ((base) b) = + switch b { + case NoBase -> 0x0000000000000000 + case RipBase -> RIP + case (RegBase(b)) -> REG[b] + } + +function ea ea_rm ((size) sz, (rm) r) = + switch r { + case (Reg(n)) -> Ea_r (sz, n) + case (Mem(idx, b, d)) -> Ea_m (sz, ea_index(idx) + (qword) (ea_base(b) + d)) + } + +function ea ea_dest ((size) sz, (dest_src) ds) = + switch ds { + case (Rm_i (v, _)) -> ea_rm (sz, v) + case (Rm_r (v, _)) -> ea_rm (sz, v) + case (R_rm (v, _)) -> Ea_r (sz, v) + } + +function ea ea_src ((size) sz, (dest_src) ds) = + switch ds { + case (Rm_i (_, v)) -> Ea_i (sz, v) + case (Rm_r (_, v)) -> Ea_r (sz, v) + case (R_rm (_, v)) -> ea_rm (sz, v) + } + +function ea ea_imm_rm ((size) sz, (imm_rm) i_rm) = + switch i_rm { + case (Rm (v)) -> ea_rm (sz, v) + case (Imm (v)) -> Ea_i (sz, v) + } + +function qword restrictSize ((size) sz, (qword) imm) = + switch sz { + case (Sz8(_)) -> imm & 0x00000000000000FF + case Sz16 -> imm & 0x000000000000FFFF + case Sz32 -> imm & 0x00000000FFFFFFFF + case Sz64 -> imm + } + +function regn sub4 ((regn) r) = negative_to_zero (r - 4) + +function qword effect { rreg, rmem } EA ((ea) e) = + switch e { + case (Ea_i(sz,i)) -> restrictSize(sz,i) + case (Ea_r((Sz8(have_rex)),r)) -> + if have_rex | r < 4 (* RSP *) | r > 7 (* RDI *) then + REG[r] + else + LSR (REG[sub4 (r)], 8) & 0x00000000000000FF + case (Ea_r(sz,r)) -> restrictSize(sz, REG[r]) + case (Ea_m((Sz8(_)),a)) -> EXTZ (MEM(a, 1)) + case (Ea_m(Sz16,a)) -> EXTZ (MEM(a, 2)) + case (Ea_m(Sz32,a)) -> EXTZ (MEM(a, 4)) + case (Ea_m(Sz64,a)) -> MEM(a, 8) + } + +function unit effect { wmem, wreg, escape } wEA ((ea) e, (qword) w) = + switch e { + case (Ea_i(_,_)) -> exit () + case (Ea_r((Sz8(have_rex)),r)) -> + if have_rex | r < 4 (* RSP *) | r > 7 (* RDI *) then + { + (qword) regr := REG[r]; + regr[7 .. 0] := w[7 .. 0]; + REG[r] := regr + } + else + { + (qword) regr := REG[sub4(r)]; + regr[15 .. 8] := (vector<15,8,dec,bit>) (adjust_dec(w[7 .. 0])); + REG[sub4(r)] := regr + } + case (Ea_r(Sz16,r)) -> + { + (qword) regr := REG[r]; + regr[15 .. 8] := w[15 .. 8]; + REG[r] := regr + } + 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) + } + +function (ea, qword, qword) read_dest_src_ea ((size) sz, (dest_src) ds) = + let e = ea_dest (sz, ds) in + (e, EA(e), EA(ea_src(sz, ds))) + +function qword call_dest_from_ea ((ea) e) = + switch e { + case (Ea_i(_, i)) -> RIP + i + case (Ea_r(_, r)) -> REG[r] + case (Ea_m(_, a)) -> MEM(a, 8) + } + +function qword get_ea_address ((ea) e) = + switch e { + case (Ea_i(_, i)) -> 0x0000000000000000 + case (Ea_r(_, r)) -> 0x0000000000000000 + case (Ea_m(_, a)) -> 0x0000000000000000 + } + +function unit jump_to_ea ((ea) e) = RIP := call_dest_from_ea(e) + +(* EFLAG updates *) + +function bit byte_parity ((byte) b) = +{ + (int) acc := 0; + foreach (i from 0 to 7) acc := acc + (int) (b[i]); + (bit) (acc mod 2 == 0) +} + +function [|64|] size_width ((size) sz) = + switch sz { + case (Sz8(_)) -> 8 + case Sz16 -> 16 + case Sz32 -> 32 + case Sz64 -> 64 + } + +function [|63|] size_width_sub1 ((size) sz) = + switch sz { + case (Sz8(_)) -> 7 + case Sz16 -> 15 + case Sz32 -> 31 + case Sz64 -> 63 + } + +(* XXXXX +function bit word_size_msb ((size) sz, (qword) w) = w[size_width(sz) - 1] +*) + +function bit word_size_msb ((size) sz, (qword) w) = w[size_width_sub1(sz)] + +function unit write_PF ((qword) w) = PF := byte_parity (w[7 .. 0]) + +function unit write_SF ((size) sz, (qword) w) = SF := word_size_msb (sz, w) + +function unit write_ZF ((size) sz, (qword) w) = + ZF := (bit) + (switch sz { + case (Sz8(_)) -> w[7 .. 0] == 0x00 + case Sz16 -> w[15 .. 0] == 0x0000 + case Sz32 -> w[31 .. 0] == 0x00000000 + case Sz64 -> w == 0x0000000000000000 + }) + +function unit write_arith_eflags_except_CF_OF ((size) sz, (qword) w) = +{ + AF := undefined; + write_PF(w); + write_SF(sz, w); + write_ZF(sz, w); +} + +function unit write_arith_eflags ((size) sz, (qword) w, (bit) c, (bit) x) = +{ + CF := c; + OF := x; + write_arith_eflags_except_CF_OF (sz, w) +} + +function unit write_logical_eflags ((size) sz, (qword) w) = + write_arith_eflags (sz, w, bitzero, bitzero) + +function unit erase_eflags () = +{ + AF := undefined; + CF := undefined; + OF := undefined; + PF := undefined; + SF := undefined; + ZF := undefined; +} + +(* XXXXX *) +function nat power ((nat) x, ([|64|]) y) = undefined + +function nat value_width ((size) sz) = power (2, size_width(sz)) + +function bit word_signed_overflow_add ((size) sz, (qword) a, (qword) b) = + (bit) (word_size_msb (sz, a) == word_size_msb (sz, b) & + word_size_msb (sz, a + b) != word_size_msb (sz, a)) + +function bit word_signed_overflow_sub ((size) sz, (qword) a, (qword) b) = + (bit) (word_size_msb (sz, a) != word_size_msb (sz, b) & + word_size_msb (sz, a - b) != word_size_msb (sz, a)) + +function (qword, bit, bit) add_with_carry_out ((size) sz, (qword) a, (qword) b) = + (a + b, (bit) ((int) (value_width (sz)) <= unsigned(a) + unsigned(b)), + word_signed_overflow_add (sz, a, b)) + +function (qword, bit, bit) sub_with_borrow ((size) sz, (qword) a, (qword) b) = + (a - b, (bit) (a < b), word_signed_overflow_sub (sz, a, b)) + +function unit write_arith_result ((size) sz, (qword) w, (bit) c, (bit) x, (ea) e) = +{ + write_arith_eflags (sz, w, c, x); + wEA (e) := w; +} + +function unit write_arith_result_no_CF_OF ((size) sz, (qword) w, (ea) e) = +{ + write_arith_eflags_except_CF_OF (sz, w); + wEA (e) := w; +} + +function unit write_logical_result ((size) sz, (qword) w, (ea) e) = +{ + write_arith_eflags_except_CF_OF (sz, w); + wEA (e) := w; +} + +function unit write_result_erase_eflags ((qword) w, (ea) e) = +{ + erase_eflags (); + wEA (e) := w; +} + +function qword effect { escape } sign_extension ((qword) w, (size) size1, (size) size2) = +{ + (qword) x := w; + switch (size1, size2) { + case ((Sz8(_)), Sz16) -> x[15 .. 0] := (bit[16]) (EXTS (w[7 .. 0])) + case ((Sz8(_)), Sz32) -> x[31 .. 0] := (bit[32]) (EXTS (w[7 .. 0])) + case ((Sz8(_)), Sz64) -> x := (qword) (EXTS (w[7 .. 0])) + case (Sz16, Sz32) -> x[31 .. 0] := (bit[32]) (EXTS (w[15 .. 0])) + case (Sz16, Sz64) -> x := (qword) (EXTS (w[15 .. 0])) + case (Sz32, Sz64) -> x := (qword) (EXTS (w[31 .. 0])) + case _ -> undefined + }; + x; +} + +function [|64|] mask_shift ((size) sz, (qword) w) = + if sz == Sz64 then w[5 .. 0] else w[4 .. 0] + +function qword rol ((size) sz, (qword) a, (qword) b) = + switch sz { + case (Sz8(_)) -> EXTZ (ROL (a[7 .. 0], b[2 .. 0])) + case Sz16 -> EXTZ (ROL (a[15 .. 0], b[3 .. 0])) + case Sz32 -> EXTZ (ROL (a[31 .. 0], b[4 .. 0])) + case Sz64 -> ROL (a, b[5 .. 0]) + } + +function qword ror ((size) sz, (qword) a, (qword) b) = + switch sz { + case (Sz8(_)) -> EXTZ (ROR (a[7 .. 0], b[2 .. 0])) + case Sz16 -> EXTZ (ROR (a[15 .. 0], b[3 .. 0])) + case Sz32 -> EXTZ (ROR (a[31 .. 0], b[4 .. 0])) + case Sz64 -> ROR (a, b[5 .. 0]) + } + +function qword sar ((size) sz, (qword) a, (qword) b) = + switch sz { + case (Sz8(_)) -> EXTZ (ASR (a[7 .. 0], b[2 .. 0])) + case Sz16 -> EXTZ (ASR (a[15 .. 0], b[3 .. 0])) + case Sz32 -> EXTZ (ASR (a[31 .. 0], b[4 .. 0])) + case Sz64 -> ASR (a, b[5 .. 0]) + } + +function unit write_binop ((size) 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) + case Sub -> let (w,c,x) = sub_with_borrow (sz, a, b) in + write_arith_result (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) + 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 (LSR (a, mask_shift (sz,b)), e) + case Adc -> + { + let carry = CF in + let (qword) result = a + (qword) (b + carry) in + { + CF := (bit) ((int) (value_width (sz)) <= unsigned(a) + unsigned(b)); + OF := undefined; + write_arith_result_no_CF_OF (sz, result, e); + } + } + case Sbb -> + { + let carry = CF in + let (qword) result = a - (qword) (b + carry) in + { + CF := (bit) (unsigned(a) < unsigned(b) + (int) carry); + OF := undefined; + write_arith_result_no_CF_OF (sz, result, e); + } + } + case _ -> exit () + } + +function unit write_monop ((size) 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) + case Neg -> { write_arith_result_no_CF_OF (sz, 0 - a, e); + CF := undefined; + } + } + +function bool read_cond ((cond) c) = + switch c { + case A -> ~(CF) & ~(ZF) + case NB -> ~(CF) + case B -> CF + case NA -> CF | (bit) ZF + case E -> ZF + case G -> ~(ZF) & (SF == OF) + case NL -> SF == OF + case L -> SF != OF + case NG -> ZF | SF != OF + case NE -> ~(ZF) + case NO -> ~(OF) + case NP -> ~(PF) + case NS -> ~(SF) + case O -> OF + case P -> PF + case S -> SF + case ALWAYS -> true + } + +function qword pop_aux () = + let top = MEM(RSP, 8) in + { + RSP := RSP + 8; + top; + } + +function unit push_aux ((qword) w) = +{ + RSP := RSP - 8; + wMEM(RSP, 8) := w; +} + +function unit pop ((rm) r) = wEA (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 (Sz64, i))) +function unit push_rip () = push_aux (RIP) + +function unit drop ((qword) i) = if i[7 ..0] != 0 then () else RSP := RSP + i + +(* -------------------------------------------------------------------------- + Instructions + -------------------------------------------------------------------------- *) + +scattered function unit execute +scattered typedef ast = const union + +val ast -> unit effect {escape, rmem, rreg, undef, wmem, wreg} execute + +(* ========================================================================== + Binop + ========================================================================== *) + +union ast member (binop_name,size,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) + +(* ========================================================================== + CALL + ========================================================================== *) + +union ast member imm_rm CALL + +function clause execute (CALL (i)) = +{ + push_rip(); + jump_to_ea (ea_imm_rm (Sz64, i)) +} + +(* ========================================================================== + CLC + ========================================================================== *) + +union ast member unit CLC + +function clause execute CLC = CF := false + +(* ========================================================================== + CMC + ========================================================================== *) + +union ast member unit CMC + +function clause execute CMC = CF := ~(CF) + +(* ========================================================================== + CMPXCHG + ========================================================================== *) + +union ast member (size,rm,regn) CMPXCHG + +function clause execute (CMPXCHG (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 + { + write_binop (sz, Cmp, val_acc, val_dst, src); + if val_acc == val_dst then + wEA(dst) := EA (src) + else + wEA(acc) := val_dst; + } + +(* ========================================================================== + DIV + ========================================================================== *) + +union ast member (size,rm) DIV + +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 q = n quot d in + let m = n mod d in + if d == 0 | w < q then exit () + else + { + wEA(eax) := cast_int_vec(q); + wEA(edx) := cast_int_vec(m); + erase_eflags(); + } + +(* ========================================================================== + Jcc + ========================================================================== *) + +union ast member (cond,qword) Jcc + +function clause execute (Jcc (c,i)) = + if read_cond (c) then RIP := RIP + i else () + +(* ========================================================================== + JMP + ========================================================================== *) + +union ast member rm JMP + +function clause execute (JMP (r)) = RIP := EA (ea_rm (Sz64, r)) + +(* ========================================================================== + LEA + ========================================================================== *) + +union ast member (size,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) + +(* ========================================================================== + LEAVE + ========================================================================== *) + +union ast member unit LEAVE + +function clause execute LEAVE = +{ + RSP := RBP; + pop (Reg (5)); (* RBP *) +} + +(* ========================================================================== + LOOP + ========================================================================== *) + +union ast member (cond,qword) LOOP + +function clause execute (LOOP (c,i)) = +{ + RCX := RCX - 1; + if RCX != 0 & read_cond (c) then RIP := RIP + i else (); +} + +(* ========================================================================== + Monop + ========================================================================== *) + +union ast member (monop_name,size,rm) Monop + +function clause execute (Monop (mop,sz,r)) = + let e = ea_rm (sz, r) in write_monop (sz, mop, EA(e), e) + +(* ========================================================================== + MOV + ========================================================================== *) + +union ast member (cond,size,dest_src) MOV + +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) + else () + +(* ========================================================================== + MOVSX + ========================================================================== *) + +union ast member (size,dest_src,size) 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) + +(* ========================================================================== + MOVZX + ========================================================================== *) + +union ast member (size,dest_src,size) 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) + +(* ========================================================================== + MUL + ========================================================================== *) + +union ast member (size,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 + switch sz { + case (Sz8(_)) -> wEA(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) := (LSR (m, size_width(sz)))[63 .. 0] + } + } + +(* ========================================================================== + NOP + ========================================================================== *) + +union ast member nat NOP + +function clause execute (NOP (_)) = () + +(* ========================================================================== + POP + ========================================================================== *) + +union ast member rm POP + +function clause execute (POP (r)) = pop(r) + +(* ========================================================================== + PUSH + ========================================================================== *) + +union ast member imm_rm PUSH + +function clause execute (PUSH (i)) = push(i) + +(* ========================================================================== + RET + ========================================================================== *) + +union ast member qword RET + +function clause execute (RET (i)) = +{ + pop_rip(); + drop(i); +} + +(* ========================================================================== + SET + ========================================================================== *) + +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 + +(* ========================================================================== + STC + ========================================================================== *) + +union ast member unit STC + +function clause execute STC = CF := true + +(* ========================================================================== + XADD + ========================================================================== *) + +union ast member (size,rm,regn) XADD + +function clause execute (XADD (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 + { + wEA(src) := val_dst; + write_binop (sz, Add, val_src, val_dst, dst); + } + +(* ========================================================================== + XCHG + ========================================================================== *) + +union ast member (size,rm,regn) XCHG + +function clause execute (XCHG (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 + { + wEA(src) := val_dst; + wEA(dst) := val_src; + } + +end ast +end execute |