diff options
| author | Alasdair | 2020-07-31 13:30:53 +0100 |
|---|---|---|
| committer | Alasdair | 2020-07-31 13:30:53 +0100 |
| commit | dd76fdfd819bb1a5423cea369df0e7f2ae449b62 (patch) | |
| tree | 88d8d69e39b724902b280beaa8ce874e444f5dbc /old/x86 | |
| parent | 71db59830383b7db5316b5c99ccebe776fc837dc (diff) | |
Remove old specs that have more up to date version
Move outdated things into old subdirectory
Diffstat (limited to 'old/x86')
24 files changed, 4147 insertions, 0 deletions
diff --git a/old/x86/Makefile b/old/x86/Makefile new file mode 100644 index 00000000..0c6e830e --- /dev/null +++ b/old/x86/Makefile @@ -0,0 +1,20 @@ +SAIL=../src/sail.native +LEM:=../../lem/lem + +SOURCES=../lib/regfp.sail x64.sail + +all: x86.lem x86.ml x86_embed.lem + +x86.lem: + $(SAIL) -lem_ast -o x86 $(SOURCES) + +x86.ml: x86.lem ../src/lem_interp/interp_ast.lem + $(LEM) -ocaml -lib ../src/lem_interp/ $< + +x86_embed.lem: $(SOURCES) +# also generates x86_embed_sequential.lem, x86_embed_types.lem, x86_toFromInterp.lem + $(SAIL) -lem -lem_lib X86_extras_embed -o x86 $(SOURCES) + +clean: + rm -f x86.lem x86.ml + rm -f x86_embed*.lem x86_toFromInterp.lem diff --git a/old/x86/gen/ast.hgen b/old/x86/gen/ast.hgen new file mode 100644 index 00000000..83488eda --- /dev/null +++ b/old/x86/gen/ast.hgen @@ -0,0 +1,26 @@ +| `X86BINOP of bool * x86Binop * x86Size * x86Dest_src +| `X86BITOP of bool * x86Bitop * x86Size * x86Bit_offset +| `X86CALL of x86Imm_rm +| `X86CLC +| `X86CMC +| `X86CMPXCHG of bool * x86Size * x86Rm * reg +| `X86DIV of x86Size * x86Rm +| `X86JCC of x86Cond * bit64 +| `X86JMP of x86Rm +| `X86LEA of x86Size * x86Dest_src +| `X86LEAVE +| `X86LOOP of x86Cond * bit64 +| `X86MFENCE +| `X86MONOP of bool * x86Monop * x86Size * x86Rm +| `X86MOV of x86Cond * x86Size * x86Dest_src +| `X86MOVSX of x86Size * x86Dest_src * x86Size +| `X86MOVZX of x86Size * x86Dest_src * x86Size +| `X86MUL of x86Size * x86Rm +| `X86NOP +| `X86POP of x86Rm +| `X86PUSH of x86Imm_rm +| `X86RET of bit64 +| `X86SET of x86Cond * bool * x86Rm +| `X86STC +| `X86XADD of bool * x86Size * x86Rm * reg +| `X86XCHG of bool * x86Size * x86Rm * reg diff --git a/old/x86/gen/fold.hgen b/old/x86/gen/fold.hgen new file mode 100644 index 00000000..df546a13 --- /dev/null +++ b/old/x86/gen/fold.hgen @@ -0,0 +1,26 @@ +| `X86BINOP (_, _, _, ds) -> fold_dest_src ds c +| `X86BITOP (_, _, _, bo) -> fold_bit_offset bo c +| `X86CALL irm -> fold_imm_rm irm c +| `X86CLC -> c +| `X86CMC -> c +| `X86CMPXCHG (_, _, rm, r) -> fold_rm rm (fold_reg r c) +| `X86DIV (_, rm) -> fold_rm rm c +| `X86JCC _ -> c +| `X86JMP rm -> fold_rm rm c +| `X86LEA (_, ds) -> fold_dest_src ds c +| `X86LEAVE -> c +| `X86LOOP _ -> c +| `X86MFENCE -> c +| `X86MONOP (_, _, _, rm) -> fold_rm rm c +| `X86MOV (_, _, ds) -> fold_dest_src ds c +| `X86MOVSX (_, ds, _) -> fold_dest_src ds c +| `X86MOVZX (_, ds, _) -> fold_dest_src ds c +| `X86MUL (_, rm) -> fold_rm rm c +| `X86NOP -> c +| `X86POP rm -> fold_rm rm c +| `X86PUSH irm -> fold_imm_rm irm c +| `X86RET _ -> c +| `X86SET (_, _, rm) -> fold_rm rm c +| `X86STC -> c +| `X86XADD (_, _, rm, r) -> fold_rm rm (fold_reg r c) +| `X86XCHG (_, _, rm, r) -> fold_rm rm (fold_reg r c) diff --git a/old/x86/gen/herdtools_ast_to_shallow_ast.hgen b/old/x86/gen/herdtools_ast_to_shallow_ast.hgen new file mode 100644 index 00000000..c709ee6c --- /dev/null +++ b/old/x86/gen/herdtools_ast_to_shallow_ast.hgen @@ -0,0 +1,28 @@ +| `X86BINOP(locked, binop, sz, dest_src) -> Binop (translate_bool locked, translate_binop binop, translate_size sz, translate_dest_src dest_src) +| `X86BITOP(locked, op, sz, bo) -> Bitop (translate_bool locked, translate_bitop op, translate_size sz, translate_bitoffset bo) +| `X86CALL (imm_rm) -> CALL (translate_imm_rm imm_rm) +| `X86CLC -> CLC +| `X86CMC -> CMC +| `X86CMPXCHG (locked, sz, rm , reg) -> CMPXCHG (translate_bool locked, translate_size sz, translate_rm rm, translate_reg reg) +| `X86DIV (sz, rm) -> X86_DIV (translate_size sz, translate_rm rm) +| `X86StopFetching -> HLT +| `X86JCC (cond, imm64) -> Jcc (translate_cond cond, translate_imm64 imm64) +| `X86JMP (rm) -> JMP (translate_rm rm) +| `X86LEA (sz, dest_src) -> LEA (translate_size sz, translate_dest_src dest_src) +| `X86LEAVE -> LEAVE +| `X86LOOP (cond, imm64) -> LOOP (translate_cond cond, translate_imm64 imm64) +| `X86MFENCE -> MFENCE +| `X86MONOP (locked, monop, sz, rm) -> Monop (translate_bool locked, translate_monop monop, translate_size sz, translate_rm rm) +| `X86MOV (cond, sz, dest_src) -> MOV (translate_cond cond, translate_size sz, translate_dest_src dest_src) +| `X86MOVSX (sz1, dest_src, sz2) -> MOVSX (translate_size sz1, translate_dest_src dest_src, translate_size sz2) +| `X86MOVZX (sz1, dest_src, sz2) -> MOVZX (translate_size sz1, translate_dest_src dest_src, translate_size sz2) +| `X86MUL (sz, rm) -> X86_MUL (translate_size sz, translate_rm rm) +| `X86NOP -> NOP (Nat_big_num.of_int 0) +| `X86POP (rm) -> POP (translate_rm rm) +| `X86PUSH (imm_rm) -> PUSH (translate_imm_rm imm_rm) +| `X86RET (imm64) -> RET (translate_imm64 imm64) +| `X86SET (cond, b, rm) -> SET (translate_cond cond, translate_bool b, translate_rm rm) +| `X86STC -> STC +| `X86XADD (locked, sz, rm, reg) -> XADD (translate_bool locked, translate_size sz, translate_rm rm, translate_reg reg) +| `X86XCHG (locked, sz, rm, reg) -> XCHG (translate_bool locked, translate_size sz, translate_rm rm, translate_reg reg) + diff --git a/old/x86/gen/herdtools_types_to_shallow_types.hgen b/old/x86/gen/herdtools_types_to_shallow_types.hgen new file mode 100644 index 00000000..44e16991 --- /dev/null +++ b/old/x86/gen/herdtools_types_to_shallow_types.hgen @@ -0,0 +1,93 @@ +let is_inc = false + +let translate_bool = function + | true -> Sail_values.B1 + | false -> Sail_values.B0 + +let translate_binop = function + | X86ADD -> X86_Add + | X86OR -> X86_Or + | X86ADC -> X86_Adc + | X86SBB -> X86_Sbb + | X86AND -> X86_And + | X86SUB -> X86_Sub + | X86XOR -> X86_Xor + | X86CMP -> X86_Cmp + | X86ROL -> X86_Rol + | X86ROR -> X86_Ror + | X86RCL -> X86_Rcl + | X86RCR -> X86_Rcr + | X86SHL -> X86_Shl + | X86SHR -> X86_Shr + | X86TEST -> X86_Test + | X86SAR -> X86_Sar + +let translate_bitop = function + | X86Btc -> Btc + | X86Bts -> Bts + | X86Btr -> Btr + +let translate_size = function + | X86S8(high) -> Sz8 (translate_bool high) + | X86S16 -> Sz16 + | X86S32 -> Sz32 + | X86S64 -> Sz64 + +let translate_reg r = Nat_big_num.of_int (reg_to_int r) + +let translate_scale s = + Sail_values.to_vec0 is_inc (Nat_big_num.of_int 2, Nat_big_num.of_int s) + +let translate_imm64 i = Sail_values.to_vec0 is_inc (Nat_big_num.of_int 64, i) + +let translate_msi = function + | Some (scale, reg) -> Some (translate_scale scale, translate_reg reg) + | None -> None + +let translate_base = function + | X86HGenBase.NoBase -> X86_embed_types.NoBase + | X86HGenBase.RegBase(r) -> X86_embed_types.RegBase (translate_reg r) + | X86HGenBase.RipBase -> X86_embed_types.RipBase + +let translate_rm = function + | X86HGenBase.Reg (r) -> X86_embed_types.X86_Reg (translate_reg r) + | X86HGenBase.Mem (m_si, base, imm) -> X86_embed_types.Mem (translate_msi m_si, translate_base base, translate_imm64 imm) + | X86HGenBase.Sym (s) -> X86_embed_types.Mem (None, X86_embed_types.NoBase, translate_imm64 Nat_big_num.zero) + +let translate_dest_src = function + | X86HGenBase.R_rm (reg, rm) -> X86_embed_types.R_rm (translate_reg reg, translate_rm rm) + | X86HGenBase.Rm_i (rm, imm64) -> X86_embed_types.Rm_i (translate_rm rm, translate_imm64 imm64) + | X86HGenBase.Rm_r (rm, reg) -> X86_embed_types.Rm_r (translate_rm rm, translate_reg reg) + +let translate_imm_rm = function + | X86HGenBase.Imm (imm) -> X86_embed_types.Imm (translate_imm64 imm) + | X86HGenBase.Rm (rm) -> X86_embed_types.Rm (translate_rm rm) + +let translate_bitoffset = function + | X86HGenBase.Bit_rm_imm (rm, imm) -> Bit_rm_imm (translate_rm rm, translate_imm64 (Nat_big_num.of_int imm)) + | X86HGenBase.Bit_rm_r (rm, r) -> Bit_rm_r (translate_rm rm, translate_reg r) + +let translate_cond = function + | X86O -> X86_O + | X86NO -> X86_NO + | X86B -> X86_B + | X86NB -> X86_NB + | X86E -> X86_E + | X86NE -> X86_NE + | X86NA -> X86_NA + | X86A -> X86_A + | X86S -> X86_S + | X86NS -> X86_NS + | X86P -> X86_P + | X86NP -> X86_NP + | X86L -> X86_L + | X86NL -> X86_NL + | X86NG -> X86_NG + | X86G -> X86_G + | X86ALWAYS -> X86_ALWAYS + +let translate_monop = function + | X86DEC -> X86_Dec + | X86INC -> X86_Inc + | X86NOT -> X86_Not + | X86NEG -> X86_Neg diff --git a/old/x86/gen/lexer.hgen b/old/x86/gen/lexer.hgen new file mode 100644 index 00000000..56944e6d --- /dev/null +++ b/old/x86/gen/lexer.hgen @@ -0,0 +1,399 @@ +"addb" , BINOP { txt = "ADDB"; op = X86ADD; sz = X86BYTE }; +"orb" , BINOP { txt = "ORB"; op = X86OR; sz = X86BYTE }; +"adcb" , BINOP { txt = "ADCB"; op = X86ADC; sz = X86BYTE }; +"sbbb" , BINOP { txt = "SBBB"; op = X86SBB; sz = X86BYTE }; +"andb" , BINOP { txt = "ANDB"; op = X86AND; sz = X86BYTE }; +"subb" , BINOP { txt = "SUBB"; op = X86SUB; sz = X86BYTE }; +"xorb" , BINOP { txt = "XORB"; op = X86XOR; sz = X86BYTE }; +"cmpb" , BINOP { txt = "CMPB"; op = X86CMP; sz = X86BYTE }; +"rolb" , BINOP { txt = "ROLB"; op = X86ROL; sz = X86BYTE }; +"rorb" , BINOP { txt = "RORB"; op = X86ROR; sz = X86BYTE }; +"shlb" , BINOP { txt = "SHLB"; op = X86SHL; sz = X86BYTE }; +"shrb" , BINOP { txt = "SHRB"; op = X86SHR; sz = X86BYTE }; +"testb" , BINOP { txt = "TESTB"; op = X86TEST; sz = X86BYTE }; +"sarb" , BINOP { txt = "SARB"; op = X86SAR; sz = X86BYTE }; +"addw" , BINOP { txt = "ADDW"; op = X86ADD; sz = X86WORD }; +"orw" , BINOP { txt = "ORW"; op = X86OR; sz = X86WORD }; +"adcw" , BINOP { txt = "ADCW"; op = X86ADC; sz = X86WORD }; +"sbbw" , BINOP { txt = "SBBW"; op = X86SBB; sz = X86WORD }; +"andw" , BINOP { txt = "ANDW"; op = X86AND; sz = X86WORD }; +"subw" , BINOP { txt = "SUBW"; op = X86SUB; sz = X86WORD }; +"xorw" , BINOP { txt = "XORW"; op = X86XOR; sz = X86WORD }; +"cmpw" , BINOP { txt = "CMPW"; op = X86CMP; sz = X86WORD }; +"rolw" , BINOP { txt = "ROLW"; op = X86ROL; sz = X86WORD }; +"rorw" , BINOP { txt = "RORW"; op = X86ROR; sz = X86WORD }; +"shlw" , BINOP { txt = "SHLW"; op = X86SHL; sz = X86WORD }; +"shrw" , BINOP { txt = "SHRW"; op = X86SHR; sz = X86WORD }; +"testw" , BINOP { txt = "TESTW"; op = X86TEST; sz = X86WORD }; +"sarw" , BINOP { txt = "SARW"; op = X86SAR; sz = X86WORD }; +"addl" , BINOP { txt = "ADDL"; op = X86ADD; sz = X86LONG }; +"orl" , BINOP { txt = "ORL"; op = X86OR; sz = X86LONG }; +"adcl" , BINOP { txt = "ADCL"; op = X86ADC; sz = X86LONG }; +"sbbl" , BINOP { txt = "SBBL"; op = X86SBB; sz = X86LONG }; +"andl" , BINOP { txt = "ANDL"; op = X86AND; sz = X86LONG }; +"subl" , BINOP { txt = "SUBL"; op = X86SUB; sz = X86LONG }; +"xorl" , BINOP { txt = "XORL"; op = X86XOR; sz = X86LONG }; +"cmpl" , BINOP { txt = "CMPL"; op = X86CMP; sz = X86LONG }; +"roll" , BINOP { txt = "ROLL"; op = X86ROL; sz = X86LONG }; +"rorl" , BINOP { txt = "RORL"; op = X86ROR; sz = X86LONG }; +"shll" , BINOP { txt = "SHLL"; op = X86SHL; sz = X86LONG }; +"shrl" , BINOP { txt = "SHRL"; op = X86SHR; sz = X86LONG }; +"testl" , BINOP { txt = "TESTL"; op = X86TEST; sz = X86LONG }; +"sarl" , BINOP { txt = "SARL"; op = X86SAR; sz = X86LONG }; +"addq" , BINOP { txt = "ADDQ"; op = X86ADD; sz = X86QUAD }; +"orq" , BINOP { txt = "ORQ"; op = X86OR; sz = X86QUAD }; +"adcq" , BINOP { txt = "ADCQ"; op = X86ADC; sz = X86QUAD }; +"sbbq" , BINOP { txt = "SBBQ"; op = X86SBB; sz = X86QUAD }; +"andq" , BINOP { txt = "ANDQ"; op = X86AND; sz = X86QUAD }; +"subq" , BINOP { txt = "SUBQ"; op = X86SUB; sz = X86QUAD }; +"xorq" , BINOP { txt = "XORQ"; op = X86XOR; sz = X86QUAD }; +"cmpq" , BINOP { txt = "CMPQ"; op = X86CMP; sz = X86QUAD }; +"rolq" , BINOP { txt = "ROLQ"; op = X86ROL; sz = X86QUAD }; +"rorq" , BINOP { txt = "RORQ"; op = X86ROR; sz = X86QUAD }; +"shlq" , BINOP { txt = "SHLQ"; op = X86SHL; sz = X86QUAD }; +"shrq" , BINOP { txt = "SHRQ"; op = X86SHR; sz = X86QUAD }; +"testq" , BINOP { txt = "TESTQ"; op = X86TEST; sz = X86QUAD }; +"sarq" , BINOP { txt = "SARQ"; op = X86SAR; sz = X86QUAD }; +"add" , BINOP { txt = "ADDQ"; op = X86ADD; sz = X86NONE }; +"or" , BINOP { txt = "OR"; op = X86OR; sz = X86NONE }; +"adc" , BINOP { txt = "ADC"; op = X86ADC; sz = X86NONE }; +"sbb" , BINOP { txt = "SBB"; op = X86SBB; sz = X86NONE }; +"and" , BINOP { txt = "AND"; op = X86AND; sz = X86NONE }; +"sub" , BINOP { txt = "SUB"; op = X86SUB; sz = X86NONE }; +"xor" , BINOP { txt = "XOR"; op = X86XOR; sz = X86NONE }; +"cmp" , BINOP { txt = "CMP"; op = X86CMP; sz = X86NONE }; +"rol" , BINOP { txt = "ROL"; op = X86ROL; sz = X86NONE }; +"ror" , BINOP { txt = "ROR"; op = X86ROR; sz = X86NONE }; +"shl" , BINOP { txt = "SHL"; op = X86SHL; sz = X86NONE }; +"shr" , BINOP { txt = "SHR"; op = X86SHR; sz = X86NONE }; +"test" , BINOP { txt = "TEST"; op = X86TEST; sz = X86NONE }; +"sar" , BINOP { txt = "SAR"; op = X86SAR; sz = X86NONE }; +"btcw" , BITOP { txt = "BTSW"; op = X86Btc; sz = X86WORD }; +"btsw" , BITOP { txt = "BTCW"; op = X86Bts; sz = X86WORD }; +"btrw" , BITOP { txt = "BTRW"; op = X86Btr; sz = X86WORD }; +"btcl" , BITOP { txt = "BTSL"; op = X86Btc; sz = X86LONG }; +"btsl" , BITOP { txt = "BTCL"; op = X86Bts; sz = X86LONG }; +"btrl" , BITOP { txt = "BTRL"; op = X86Btr; sz = X86LONG }; +"btcq" , BITOP { txt = "BTSQ"; op = X86Btc; sz = X86QUAD }; +"btsq" , BITOP { txt = "BTCQ"; op = X86Bts; sz = X86QUAD }; +"btrq" , BITOP { txt = "BTRQ"; op = X86Btr; sz = X86QUAD }; +"btc" , BITOP { txt = "BTS"; op = X86Btc; sz = X86NONE }; +"bts" , BITOP { txt = "BTC"; op = X86Bts; sz = X86NONE }; +"btr" , BITOP { txt = "BTR"; op = X86Btr; sz = X86NONE }; +"call" , CALL { txt = "CALL" }; +"clc" , CLC { txt = "CLC" }; +"cmc" , CMC { txt = "CMC" }; +"cmpxchgb" , CMPXCHG { txt = "CMPXCHGB"; sz = X86BYTE }; +"cmpxchgw" , CMPXCHG { txt = "CMPXCHGW"; sz = X86WORD }; +"cmpxchgl" , CMPXCHG { txt = "CMPXCHGL"; sz = X86LONG }; +"cmpxchgq" , CMPXCHG { txt = "CMPXCHGQ"; sz = X86QUAD }; +"cmpxchg" , CMPXCHG { txt = "CMPXCHG"; sz = X86NONE }; +"divb" , DIV { txt = "DIVB"; sz = X86BYTE }; +"divw" , DIV { txt = "DIVW"; sz = X86WORD }; +"divl" , DIV { txt = "DIVL"; sz = X86LONG }; +"divq" , DIV { txt = "DIVQ"; sz = X86QUAD }; +"div" , DIV { txt = "DIV"; sz = X86NONE }; +"jo" , JCC { txt = "JO"; cond = X86O }; +"jb" , JCC { txt = "JB"; cond = X86B }; +"jc" , JCC { txt = "JC"; cond = X86B }; +"jnae" , JCC { txt = "JNAE"; cond = X86B }; +"je" , JCC { txt = "JE"; cond = X86E }; +"jz" , JCC { txt = "JZ"; cond = X86E }; +"ja" , JCC { txt = "JA"; cond = X86A }; +"jnbe" , JCC { txt = "JNBE"; cond = X86A }; +"js" , JCC { txt = "JS"; cond = X86S }; +"jp" , JCC { txt = "JP"; cond = X86P }; +"jpe" , JCC { txt = "JPE"; cond = X86P }; +"jl" , JCC { txt = "JL"; cond = X86L }; +"jnge" , JCC { txt = "JNGE"; cond = X86L }; +"jg" , JCC { txt = "JG"; cond = X86G }; +"jnle" , JCC { txt = "JNLE"; cond = X86G }; +"jno" , JCC { txt = "JNO"; cond = X86NO }; +"jnb" , JCC { txt = "JNB"; cond = X86NB }; +"jnc" , JCC { txt = "JNC"; cond = X86NB }; +"jae" , JCC { txt = "JAE"; cond = X86NB }; +"jne" , JCC { txt = "JNE"; cond = X86NE }; +"jnz" , JCC { txt = "JNZ"; cond = X86NE }; +"jna" , JCC { txt = "JNA"; cond = X86NA }; +"jbe" , JCC { txt = "JBE"; cond = X86NA }; +"jns" , JCC { txt = "JNS"; cond = X86NS }; +"jnp" , JCC { txt = "JNP"; cond = X86NP }; +"jpo" , JCC { txt = "JPO"; cond = X86NP }; +"jnl" , JCC { txt = "JNL"; cond = X86NL }; +"jge" , JCC { txt = "JGE"; cond = X86NL }; +"jng" , JCC { txt = "JNG"; cond = X86NG }; +"jle" , JCC { txt = "JLE"; cond = X86NG }; +"jmp" , JMP { txt = "JMP" }; +"leaw" , LEA { txt = "LEAW"; sz = X86BYTE }; +"leal" , LEA { txt = "LEAL"; sz = X86LONG }; +"leaq" , LEA { txt = "LEAQ"; sz = X86QUAD }; +"lea" , LEA { txt = "LEA"; sz = X86NONE }; +"leave" , LEAVE { txt = "LEAVE" }; +"loopo" , LOOP { txt = "LOOPO"; cond = X86O }; +"loopb" , LOOP { txt = "LOOPB"; cond = X86B }; +"loopc" , LOOP { txt = "LOOPC"; cond = X86B }; +"loopnae" , LOOP { txt = "LOOPNAE"; cond = X86B }; +"loope" , LOOP { txt = "LOOPE"; cond = X86E }; +"loopz" , LOOP { txt = "LOOPZ"; cond = X86E }; +"loopa" , LOOP { txt = "LOOPA"; cond = X86A }; +"loopnbe" , LOOP { txt = "LOOPNBE"; cond = X86A }; +"loops" , LOOP { txt = "LOOPS"; cond = X86S }; +"loopp" , LOOP { txt = "LOOPP"; cond = X86P }; +"looppe" , LOOP { txt = "LOOPPE"; cond = X86P }; +"loopl" , LOOP { txt = "LOOPL"; cond = X86L }; +"loopnge" , LOOP { txt = "LOOPNGE"; cond = X86L }; +"loopg" , LOOP { txt = "LOOPG"; cond = X86G }; +"loopnle" , LOOP { txt = "LOOPNLE"; cond = X86G }; +"loopno" , LOOP { txt = "LOOPNO"; cond = X86NO }; +"loopnb" , LOOP { txt = "LOOPNB"; cond = X86NB }; +"loopnc" , LOOP { txt = "LOOPNC"; cond = X86NB }; +"loopae" , LOOP { txt = "LOOPAE"; cond = X86NB }; +"loopne" , LOOP { txt = "LOOPNE"; cond = X86NE }; +"loopnz" , LOOP { txt = "LOOPNZ"; cond = X86NE }; +"loopna" , LOOP { txt = "LOOPNA"; cond = X86NA }; +"loopbe" , LOOP { txt = "LOOPBE"; cond = X86NA }; +"loopns" , LOOP { txt = "LOOPNS"; cond = X86NS }; +"loopnp" , LOOP { txt = "LOOPNP"; cond = X86NP }; +"looppo" , LOOP { txt = "LOOPPO"; cond = X86NP }; +"loopnl" , LOOP { txt = "LOOPNL"; cond = X86NL }; +"loopge" , LOOP { txt = "LOOPGE"; cond = X86NL }; +"loopng" , LOOP { txt = "LOOPNG"; cond = X86NG }; +"loople" , LOOP { txt = "LOOPLE"; cond = X86NG }; +"mfence" , MFENCE { txt = "MFENCE" }; +"decb" , MONOP { txt = "DECB"; op = X86DEC; sz = X86BYTE }; +"incb" , MONOP { txt = "INCB"; op = X86INC; sz = X86BYTE }; +"notb" , MONOP { txt = "NOTB"; op = X86NOT; sz = X86BYTE }; +"negb" , MONOP { txt = "NEGB"; op = X86NEG; sz = X86BYTE }; +"decw" , MONOP { txt = "DECW"; op = X86DEC; sz = X86WORD }; +"incw" , MONOP { txt = "INCW"; op = X86INC; sz = X86WORD }; +"notw" , MONOP { txt = "NOTW"; op = X86NOT; sz = X86WORD }; +"negw" , MONOP { txt = "NEGW"; op = X86NEG; sz = X86WORD }; +"decl" , MONOP { txt = "DECL"; op = X86DEC; sz = X86LONG }; +"incl" , MONOP { txt = "INCL"; op = X86INC; sz = X86LONG }; +"notl" , MONOP { txt = "NOTL"; op = X86NOT; sz = X86LONG }; +"negl" , MONOP { txt = "NEGL"; op = X86NEG; sz = X86LONG }; +"decq" , MONOP { txt = "DECQ"; op = X86DEC; sz = X86QUAD }; +"incq" , MONOP { txt = "INCQ"; op = X86INC; sz = X86QUAD }; +"notq" , MONOP { txt = "NOTQ"; op = X86NOT; sz = X86QUAD }; +"negq" , MONOP { txt = "NEGQ"; op = X86NEG; sz = X86QUAD }; +"dec" , MONOP { txt = "DEC"; op = X86DEC; sz = X86NONE }; +"inc" , MONOP { txt = "INC"; op = X86INC; sz = X86NONE }; +"not" , MONOP { txt = "NOT"; op = X86NOT; sz = X86NONE }; +"neg" , MONOP { txt = "NEG"; op = X86NEG; sz = X86NONE }; +"cmovow" , CMOV { txt = "CMOVOW"; cond = X86O; sz = X86WORD }; +"cmovbw" , CMOV { txt = "CMOVBW"; cond = X86B; sz = X86WORD }; +"cmovcw" , CMOV { txt = "CMOVCW"; cond = X86B; sz = X86WORD }; +"cmovnaew" , CMOV { txt = "CMOVNAEW"; cond = X86B; sz = X86WORD }; +"cmovew" , CMOV { txt = "CMOVEW"; cond = X86E; sz = X86WORD }; +"cmovzw" , CMOV { txt = "CMOVZW"; cond = X86E; sz = X86WORD }; +"cmovaw" , CMOV { txt = "CMOVAW"; cond = X86A; sz = X86WORD }; +"cmovnbew" , CMOV { txt = "CMOVNBEW"; cond = X86A; sz = X86WORD }; +"cmovsw" , CMOV { txt = "CMOVSW"; cond = X86S; sz = X86WORD }; +"cmovpw" , CMOV { txt = "CMOVPW"; cond = X86P; sz = X86WORD }; +"cmovpew" , CMOV { txt = "CMOVPEW"; cond = X86P; sz = X86WORD }; +"cmovlw" , CMOV { txt = "CMOVLW"; cond = X86L; sz = X86WORD }; +"cmovngew" , CMOV { txt = "CMOVNGEW"; cond = X86L; sz = X86WORD }; +"cmovgw" , CMOV { txt = "CMOVGW"; cond = X86G; sz = X86WORD }; +"cmovnlew" , CMOV { txt = "CMOVNLEW"; cond = X86G; sz = X86WORD }; +"cmovnow" , CMOV { txt = "CMOVNOW"; cond = X86NO; sz = X86WORD }; +"cmovnbw" , CMOV { txt = "CMOVNBW"; cond = X86NB; sz = X86WORD }; +"cmovncw" , CMOV { txt = "CMOVNCW"; cond = X86NB; sz = X86WORD }; +"cmovaew" , CMOV { txt = "CMOVAEW"; cond = X86NB; sz = X86WORD }; +"cmovnew" , CMOV { txt = "CMOVNEW"; cond = X86NE; sz = X86WORD }; +"cmovnzw" , CMOV { txt = "CMOVNZW"; cond = X86NE; sz = X86WORD }; +"cmovnaw" , CMOV { txt = "CMOVNAW"; cond = X86NA; sz = X86WORD }; +"cmovbew" , CMOV { txt = "CMOVBEW"; cond = X86NA; sz = X86WORD }; +"cmovnsw" , CMOV { txt = "CMOVNSW"; cond = X86NS; sz = X86WORD }; +"cmovnpw" , CMOV { txt = "CMOVNPW"; cond = X86NP; sz = X86WORD }; +"cmovpow" , CMOV { txt = "CMOVPOW"; cond = X86NP; sz = X86WORD }; +"cmovnlw" , CMOV { txt = "CMOVNLW"; cond = X86NL; sz = X86WORD }; +"cmovgew" , CMOV { txt = "CMOVGEW"; cond = X86NL; sz = X86WORD }; +"cmovngw" , CMOV { txt = "CMOVNGW"; cond = X86NG; sz = X86WORD }; +"cmovlew" , CMOV { txt = "CMOVLEW"; cond = X86NG; sz = X86WORD }; +"cmovol" , CMOV { txt = "CMOVOL"; cond = X86O; sz = X86LONG }; +"cmovbl" , CMOV { txt = "CMOVBL"; cond = X86B; sz = X86LONG }; +"cmovcl" , CMOV { txt = "CMOVCL"; cond = X86B; sz = X86LONG }; +"cmovnael" , CMOV { txt = "CMOVNAEL"; cond = X86B; sz = X86LONG }; +"cmovel" , CMOV { txt = "CMOVEL"; cond = X86E; sz = X86LONG }; +"cmovzl" , CMOV { txt = "CMOVZL"; cond = X86E; sz = X86LONG }; +"cmoval" , CMOV { txt = "CMOVAL"; cond = X86A; sz = X86LONG }; +"cmovnbel" , CMOV { txt = "CMOVNBEL"; cond = X86A; sz = X86LONG }; +"cmovsl" , CMOV { txt = "CMOVSL"; cond = X86S; sz = X86LONG }; +"cmovpl" , CMOV { txt = "CMOVPL"; cond = X86P; sz = X86LONG }; +"cmovpel" , CMOV { txt = "CMOVPEL"; cond = X86P; sz = X86LONG }; +"cmovll" , CMOV { txt = "CMOVLL"; cond = X86L; sz = X86LONG }; +"cmovngel" , CMOV { txt = "CMOVNGEL"; cond = X86L; sz = X86LONG }; +"cmovgl" , CMOV { txt = "CMOVGL"; cond = X86G; sz = X86LONG }; +"cmovnlel" , CMOV { txt = "CMOVNLEL"; cond = X86G; sz = X86LONG }; +"cmovnol" , CMOV { txt = "CMOVNOL"; cond = X86NO; sz = X86LONG }; +"cmovnbl" , CMOV { txt = "CMOVNBL"; cond = X86NB; sz = X86LONG }; +"cmovncl" , CMOV { txt = "CMOVNCL"; cond = X86NB; sz = X86LONG }; +"cmovael" , CMOV { txt = "CMOVAEL"; cond = X86NB; sz = X86LONG }; +"cmovnel" , CMOV { txt = "CMOVNEL"; cond = X86NE; sz = X86LONG }; +"cmovnzl" , CMOV { txt = "CMOVNZL"; cond = X86NE; sz = X86LONG }; +"cmovnal" , CMOV { txt = "CMOVNAL"; cond = X86NA; sz = X86LONG }; +"cmovbel" , CMOV { txt = "CMOVBEL"; cond = X86NA; sz = X86LONG }; +"cmovnsl" , CMOV { txt = "CMOVNSL"; cond = X86NS; sz = X86LONG }; +"cmovnpl" , CMOV { txt = "CMOVNPL"; cond = X86NP; sz = X86LONG }; +"cmovpol" , CMOV { txt = "CMOVPOL"; cond = X86NP; sz = X86LONG }; +"cmovnll" , CMOV { txt = "CMOVNLL"; cond = X86NL; sz = X86LONG }; +"cmovgel" , CMOV { txt = "CMOVGEL"; cond = X86NL; sz = X86LONG }; +"cmovngl" , CMOV { txt = "CMOVNGL"; cond = X86NG; sz = X86LONG }; +"cmovlel" , CMOV { txt = "CMOVLEL"; cond = X86NG; sz = X86LONG }; +"cmovoq" , CMOV { txt = "CMOVOQ"; cond = X86O; sz = X86QUAD }; +"cmovbq" , CMOV { txt = "CMOVBQ"; cond = X86B; sz = X86QUAD }; +"cmovcq" , CMOV { txt = "CMOVCQ"; cond = X86B; sz = X86QUAD }; +"cmovnaeq" , CMOV { txt = "CMOVNAEQ"; cond = X86B; sz = X86QUAD }; +"cmoveq" , CMOV { txt = "CMOVEQ"; cond = X86E; sz = X86QUAD }; +"cmovzq" , CMOV { txt = "CMOVZQ"; cond = X86E; sz = X86QUAD }; +"cmovaq" , CMOV { txt = "CMOVAQ"; cond = X86A; sz = X86QUAD }; +"cmovnbeq" , CMOV { txt = "CMOVNBEQ"; cond = X86A; sz = X86QUAD }; +"cmovsq" , CMOV { txt = "CMOVSQ"; cond = X86S; sz = X86QUAD }; +"cmovpq" , CMOV { txt = "CMOVPQ"; cond = X86P; sz = X86QUAD }; +"cmovpeq" , CMOV { txt = "CMOVPEQ"; cond = X86P; sz = X86QUAD }; +"cmovlq" , CMOV { txt = "CMOVLQ"; cond = X86L; sz = X86QUAD }; +"cmovngeq" , CMOV { txt = "CMOVNGEQ"; cond = X86L; sz = X86QUAD }; +"cmovgq" , CMOV { txt = "CMOVGQ"; cond = X86G; sz = X86QUAD }; +"cmovnleq" , CMOV { txt = "CMOVNLEQ"; cond = X86G; sz = X86QUAD }; +"cmovnoq" , CMOV { txt = "CMOVNOQ"; cond = X86NO; sz = X86QUAD }; +"cmovnbq" , CMOV { txt = "CMOVNBQ"; cond = X86NB; sz = X86QUAD }; +"cmovncq" , CMOV { txt = "CMOVNCQ"; cond = X86NB; sz = X86QUAD }; +"cmovaeq" , CMOV { txt = "CMOVAEQ"; cond = X86NB; sz = X86QUAD }; +"cmovneq" , CMOV { txt = "CMOVNEQ"; cond = X86NE; sz = X86QUAD }; +"cmovnzq" , CMOV { txt = "CMOVNZQ"; cond = X86NE; sz = X86QUAD }; +"cmovnaq" , CMOV { txt = "CMOVNAQ"; cond = X86NA; sz = X86QUAD }; +"cmovbeq" , CMOV { txt = "CMOVBEQ"; cond = X86NA; sz = X86QUAD }; +"cmovnsq" , CMOV { txt = "CMOVNSQ"; cond = X86NS; sz = X86QUAD }; +"cmovnpq" , CMOV { txt = "CMOVNPQ"; cond = X86NP; sz = X86QUAD }; +"cmovpoq" , CMOV { txt = "CMOVPOQ"; cond = X86NP; sz = X86QUAD }; +"cmovnlq" , CMOV { txt = "CMOVNLQ"; cond = X86NL; sz = X86QUAD }; +"cmovgeq" , CMOV { txt = "CMOVGEQ"; cond = X86NL; sz = X86QUAD }; +"cmovngq" , CMOV { txt = "CMOVNGQ"; cond = X86NG; sz = X86QUAD }; +"cmovleq" , CMOV { txt = "CMOVLEQ"; cond = X86NG; sz = X86QUAD }; +"cmovo" , CMOV { txt = "CMOVO"; cond = X86O; sz = X86NONE }; +"cmovb" , CMOV { txt = "CMOVB"; cond = X86B; sz = X86NONE }; +"cmovc" , CMOV { txt = "CMOVC"; cond = X86B; sz = X86NONE }; +"cmovnae" , CMOV { txt = "CMOVNAE"; cond = X86B; sz = X86NONE }; +"cmove" , CMOV { txt = "CMOVE"; cond = X86E; sz = X86NONE }; +"cmovz" , CMOV { txt = "CMOVZ"; cond = X86E; sz = X86NONE }; +"cmova" , CMOV { txt = "CMOVA"; cond = X86A; sz = X86NONE }; +"cmovnbe" , CMOV { txt = "CMOVNBE"; cond = X86A; sz = X86NONE }; +"cmovs" , CMOV { txt = "CMOVS"; cond = X86S; sz = X86NONE }; +"cmovp" , CMOV { txt = "CMOVP"; cond = X86P; sz = X86NONE }; +"cmovpe" , CMOV { txt = "CMOVPE"; cond = X86P; sz = X86NONE }; +"cmovl" , CMOV { txt = "CMOVL"; cond = X86L; sz = X86NONE }; +"cmovnge" , CMOV { txt = "CMOVNGE"; cond = X86L; sz = X86NONE }; +"cmovg" , CMOV { txt = "CMOVG"; cond = X86G; sz = X86NONE }; +"cmovnle" , CMOV { txt = "CMOVNLE"; cond = X86G; sz = X86NONE }; +"cmovno" , CMOV { txt = "CMOVNO"; cond = X86NO; sz = X86NONE }; +"cmovnb" , CMOV { txt = "CMOVNB"; cond = X86NB; sz = X86NONE }; +"cmovnc" , CMOV { txt = "CMOVNC"; cond = X86NB; sz = X86NONE }; +"cmovae" , CMOV { txt = "CMOVAE"; cond = X86NB; sz = X86NONE }; +"cmovne" , CMOV { txt = "CMOVNE"; cond = X86NE; sz = X86NONE }; +"cmovnz" , CMOV { txt = "CMOVNZ"; cond = X86NE; sz = X86NONE }; +"cmovna" , CMOV { txt = "CMOVNA"; cond = X86NA; sz = X86NONE }; +"cmovbe" , CMOV { txt = "CMOVBE"; cond = X86NA; sz = X86NONE }; +"cmovns" , CMOV { txt = "CMOVNS"; cond = X86NS; sz = X86NONE }; +"cmovnp" , CMOV { txt = "CMOVNP"; cond = X86NP; sz = X86NONE }; +"cmovpo" , CMOV { txt = "CMOVPO"; cond = X86NP; sz = X86NONE }; +"cmovnl" , CMOV { txt = "CMOVNL"; cond = X86NL; sz = X86NONE }; +"cmovge" , CMOV { txt = "CMOVGE"; cond = X86NL; sz = X86NONE }; +"cmovng" , CMOV { txt = "CMOVNG"; cond = X86NG; sz = X86NONE }; +"cmovle" , CMOV { txt = "CMOVLE"; cond = X86NG; sz = X86NONE }; +"movb" , MOV { txt = "MOVB"; sz = X86BYTE }; +"movw" , MOV { txt = "MOVW"; sz = X86WORD }; +"movl" , MOV { txt = "MOVL"; sz = X86LONG }; +"movq" , MOV { txt = "MOVQ"; sz = X86QUAD }; +"mov" , MOV { txt = "MOV"; sz = X86NONE }; +"movabs" , MOV { txt = "MOVABS"; sz = X86QUAD }; +"movsbw" , MOVSX { txt = "MOVSBW"; sz1 = X86BYTE; sz2 = X86WORD }; +"movsbl" , MOVSX { txt = "MOVSBL"; sz1 = X86BYTE; sz2 = X86LONG }; +"movsbq" , MOVSX { txt = "MOVSBQ"; sz1 = X86BYTE; sz2 = X86QUAD }; +"movswl" , MOVSX { txt = "MOVSWL"; sz1 = X86WORD; sz2 = X86LONG }; +"movswq" , MOVSX { txt = "MOVSWQ"; sz1 = X86WORD; sz2 = X86QUAD }; +"movslq" , MOVSX { txt = "MOVSWQ"; sz1 = X86LONG; sz2 = X86QUAD }; +"movzbw" , MOVZX { txt = "MOVZBW"; sz1 = X86BYTE; sz2 = X86WORD }; +"movzbl" , MOVZX { txt = "MOVZBL"; sz1 = X86BYTE; sz2 = X86LONG }; +"movzbq" , MOVZX { txt = "MOVZBQ"; sz1 = X86BYTE; sz2 = X86QUAD }; +"movzwl" , MOVZX { txt = "MOVZWL"; sz1 = X86WORD; sz2 = X86LONG }; +"movzwq" , MOVZX { txt = "MOVZWQ"; sz1 = X86WORD; sz2 = X86QUAD }; +"mulb" , MUL { txt = "MULB"; sz = X86BYTE }; +"mulw" , MUL { txt = "MULW"; sz = X86WORD }; +"mull" , MUL { txt = "MULL"; sz = X86LONG }; +"mulq" , MUL { txt = "MULQ"; sz = X86QUAD }; +"mul" , MUL { txt = "MUL"; sz = X86NONE }; +"nop" , NOP { txt = "NOP" }; +"pop" , POP { txt = "POP" }; +"push" , PUSH { txt = "PUSH" }; +"ret" , PUSH { txt = "RET" }; +"setob" , SET { txt = "SETOB"; cond = X86O }; +"setbb" , SET { txt = "SETBB"; cond = X86B }; +"setcb" , SET { txt = "SETCB"; cond = X86B }; +"setnaeb" , SET { txt = "SETNAEB"; cond = X86B }; +"seteb" , SET { txt = "SETEB"; cond = X86E }; +"setzb" , SET { txt = "SETZB"; cond = X86E }; +"setab" , SET { txt = "SETAB"; cond = X86A }; +"setnbeb" , SET { txt = "SETNBEB"; cond = X86A }; +"setsb" , SET { txt = "SETSB"; cond = X86S }; +"setpb" , SET { txt = "SETPB"; cond = X86P }; +"setpeb" , SET { txt = "SETPEB"; cond = X86P }; +"setlb" , SET { txt = "SETLB"; cond = X86L }; +"setngeb" , SET { txt = "SETNGEB"; cond = X86L }; +"setgb" , SET { txt = "SETGB"; cond = X86G }; +"setnleb" , SET { txt = "SETNLEB"; cond = X86G }; +"setnob" , SET { txt = "SETNOB"; cond = X86NO }; +"setnbb" , SET { txt = "SETNBB"; cond = X86NB }; +"setncb" , SET { txt = "SETNCB"; cond = X86NB }; +"setaeb" , SET { txt = "SETAEB"; cond = X86NB }; +"setneb" , SET { txt = "SETNEB"; cond = X86NE }; +"setnzb" , SET { txt = "SETNZB"; cond = X86NE }; +"setnab" , SET { txt = "SETNAB"; cond = X86NA }; +"setbeb" , SET { txt = "SETBEB"; cond = X86NA }; +"setnsb" , SET { txt = "SETNSB"; cond = X86NS }; +"setnpb" , SET { txt = "SETNPB"; cond = X86NP }; +"setpob" , SET { txt = "SETPOB"; cond = X86NP }; +"setnlb" , SET { txt = "SETNLB"; cond = X86NL }; +"setgeb" , SET { txt = "SETGEB"; cond = X86NL }; +"setngb" , SET { txt = "SETNGB"; cond = X86NG }; +"setleb" , SET { txt = "SETLEB"; cond = X86NG }; +"seto" , SET { txt = "SETO"; cond = X86O }; +"setb" , SET { txt = "SETB"; cond = X86B }; +"setc" , SET { txt = "SETC"; cond = X86B }; +"setnae" , SET { txt = "SETNAE"; cond = X86B }; +"sete" , SET { txt = "SETE"; cond = X86E }; +"setz" , SET { txt = "SETZ"; cond = X86E }; +"seta" , SET { txt = "SETA"; cond = X86A }; +"setnbe" , SET { txt = "SETNBE"; cond = X86A }; +"sets" , SET { txt = "SETS"; cond = X86S }; +"setp" , SET { txt = "SETP"; cond = X86P }; +"setpe" , SET { txt = "SETPE"; cond = X86P }; +"setl" , SET { txt = "SETL"; cond = X86L }; +"setnge" , SET { txt = "SETNGE"; cond = X86L }; +"setg" , SET { txt = "SETG"; cond = X86G }; +"setnle" , SET { txt = "SETNLE"; cond = X86G }; +"setno" , SET { txt = "SETNO"; cond = X86NO }; +"setnb" , SET { txt = "SETNB"; cond = X86NB }; +"setnc" , SET { txt = "SETNC"; cond = X86NB }; +"setae" , SET { txt = "SETAE"; cond = X86NB }; +"setne" , SET { txt = "SETNE"; cond = X86NE }; +"setnz" , SET { txt = "SETNZ"; cond = X86NE }; +"setna" , SET { txt = "SETNA"; cond = X86NA }; +"setbe" , SET { txt = "SETBE"; cond = X86NA }; +"setns" , SET { txt = "SETNS"; cond = X86NS }; +"setnp" , SET { txt = "SETNP"; cond = X86NP }; +"setpo" , SET { txt = "SETPO"; cond = X86NP }; +"setnl" , SET { txt = "SETNL"; cond = X86NL }; +"setge" , SET { txt = "SETGE"; cond = X86NL }; +"setng" , SET { txt = "SETNG"; cond = X86NG }; +"setle" , SET { txt = "SETLE"; cond = X86NG }; +"stc" , STC { txt = "STC" }; +"xaddb" , XADD { txt = "XADDB"; sz = X86BYTE }; +"xaddw" , XADD { txt = "XADDW"; sz = X86WORD }; +"xaddl" , XADD { txt = "XADDL"; sz = X86LONG }; +"xaddq" , XADD { txt = "XADDQ"; sz = X86QUAD }; +"xadd" , XADD { txt = "XADD"; sz = X86NONE }; +"xchgb" , XCHG { txt = "XCHGB"; sz = X86BYTE }; +"xchgw" , XCHG { txt = "XCHGW"; sz = X86WORD }; +"xchgl" , XCHG { txt = "XCHGL"; sz = X86LONG }; +"xchgq" , XCHG { txt = "XCHGQ"; sz = X86QUAD }; +"xchg" , XCHG { txt = "XCHG"; sz = X86NONE }; diff --git a/old/x86/gen/lexer_intel.hgen b/old/x86/gen/lexer_intel.hgen new file mode 100644 index 00000000..e1854a14 --- /dev/null +++ b/old/x86/gen/lexer_intel.hgen @@ -0,0 +1,161 @@ +"add" , BINOP { txt = "ADDQ"; op = X86ADD; sz = X86NONE }; +"or" , BINOP { txt = "OR"; op = X86OR; sz = X86NONE }; +"adc" , BINOP { txt = "ADC"; op = X86ADC; sz = X86NONE }; +"sbb" , BINOP { txt = "SBB"; op = X86SBB; sz = X86NONE }; +"and" , BINOP { txt = "AND"; op = X86AND; sz = X86NONE }; +"sub" , BINOP { txt = "SUB"; op = X86SUB; sz = X86NONE }; +"xor" , BINOP { txt = "XOR"; op = X86XOR; sz = X86NONE }; +"cmp" , BINOP { txt = "CMP"; op = X86CMP; sz = X86NONE }; +"rol" , BINOP { txt = "ROL"; op = X86ROL; sz = X86NONE }; +"ror" , BINOP { txt = "ROR"; op = X86ROR; sz = X86NONE }; +"shl" , BINOP { txt = "SHL"; op = X86SHL; sz = X86NONE }; +"shr" , BINOP { txt = "SHR"; op = X86SHR; sz = X86NONE }; +"test" , BINOP { txt = "TEST"; op = X86TEST; sz = X86NONE }; +"sar" , BINOP { txt = "SAR"; op = X86SAR; sz = X86NONE }; +"btc" , BITOP { txt = "BTS"; op = X86Btc; sz = X86NONE }; +"bts" , BITOP { txt = "BTC"; op = X86Bts; sz = X86NONE }; +"btr" , BITOP { txt = "BTR"; op = X86Btr; sz = X86NONE }; +"call" , CALL { txt = "CALL" }; +"clc" , CLC { txt = "CLC" }; +"cmc" , CMC { txt = "CMC" }; +"cmpxchg" , CMPXCHG { txt = "CMPXCHG"; sz = X86NONE }; +"div" , DIV { txt = "DIV"; sz = X86NONE }; +"jo" , JCC { txt = "JO"; cond = X86O }; +"jb" , JCC { txt = "JB"; cond = X86B }; +"jc" , JCC { txt = "JC"; cond = X86B }; +"jnae" , JCC { txt = "JNAE"; cond = X86B }; +"je" , JCC { txt = "JE"; cond = X86E }; +"jz" , JCC { txt = "JZ"; cond = X86E }; +"ja" , JCC { txt = "JA"; cond = X86A }; +"jnbe" , JCC { txt = "JNBE"; cond = X86A }; +"js" , JCC { txt = "JS"; cond = X86S }; +"jp" , JCC { txt = "JP"; cond = X86P }; +"jpe" , JCC { txt = "JPE"; cond = X86P }; +"jl" , JCC { txt = "JL"; cond = X86L }; +"jnge" , JCC { txt = "JNGE"; cond = X86L }; +"jg" , JCC { txt = "JG"; cond = X86G }; +"jnle" , JCC { txt = "JNLE"; cond = X86G }; +"jno" , JCC { txt = "JNO"; cond = X86NO }; +"jnb" , JCC { txt = "JNB"; cond = X86NB }; +"jnc" , JCC { txt = "JNC"; cond = X86NB }; +"jae" , JCC { txt = "JAE"; cond = X86NB }; +"jne" , JCC { txt = "JNE"; cond = X86NE }; +"jnz" , JCC { txt = "JNZ"; cond = X86NE }; +"jna" , JCC { txt = "JNA"; cond = X86NA }; +"jbe" , JCC { txt = "JBE"; cond = X86NA }; +"jns" , JCC { txt = "JNS"; cond = X86NS }; +"jnp" , JCC { txt = "JNP"; cond = X86NP }; +"jpo" , JCC { txt = "JPO"; cond = X86NP }; +"jnl" , JCC { txt = "JNL"; cond = X86NL }; +"jge" , JCC { txt = "JGE"; cond = X86NL }; +"jng" , JCC { txt = "JNG"; cond = X86NG }; +"jle" , JCC { txt = "JLE"; cond = X86NG }; +"jmp" , JMP { txt = "JMP" }; +"lea" , LEA { txt = "LEA"; sz = X86NONE }; +"leave" , LEAVE { txt = "LEAVE" }; +"loopo" , LOOP { txt = "LOOPO"; cond = X86O }; +"loopb" , LOOP { txt = "LOOPB"; cond = X86B }; +"loopc" , LOOP { txt = "LOOPC"; cond = X86B }; +"loopnae" , LOOP { txt = "LOOPNAE"; cond = X86B }; +"loope" , LOOP { txt = "LOOPE"; cond = X86E }; +"loopz" , LOOP { txt = "LOOPZ"; cond = X86E }; +"loopa" , LOOP { txt = "LOOPA"; cond = X86A }; +"loopnbe" , LOOP { txt = "LOOPNBE"; cond = X86A }; +"loops" , LOOP { txt = "LOOPS"; cond = X86S }; +"loopp" , LOOP { txt = "LOOPP"; cond = X86P }; +"looppe" , LOOP { txt = "LOOPPE"; cond = X86P }; +"loopl" , LOOP { txt = "LOOPL"; cond = X86L }; +"loopnge" , LOOP { txt = "LOOPNGE"; cond = X86L }; +"loopg" , LOOP { txt = "LOOPG"; cond = X86G }; +"loopnle" , LOOP { txt = "LOOPNLE"; cond = X86G }; +"loopno" , LOOP { txt = "LOOPNO"; cond = X86NO }; +"loopnb" , LOOP { txt = "LOOPNB"; cond = X86NB }; +"loopnc" , LOOP { txt = "LOOPNC"; cond = X86NB }; +"loopae" , LOOP { txt = "LOOPAE"; cond = X86NB }; +"loopne" , LOOP { txt = "LOOPNE"; cond = X86NE }; +"loopnz" , LOOP { txt = "LOOPNZ"; cond = X86NE }; +"loopna" , LOOP { txt = "LOOPNA"; cond = X86NA }; +"loopbe" , LOOP { txt = "LOOPBE"; cond = X86NA }; +"loopns" , LOOP { txt = "LOOPNS"; cond = X86NS }; +"loopnp" , LOOP { txt = "LOOPNP"; cond = X86NP }; +"looppo" , LOOP { txt = "LOOPPO"; cond = X86NP }; +"loopnl" , LOOP { txt = "LOOPNL"; cond = X86NL }; +"loopge" , LOOP { txt = "LOOPGE"; cond = X86NL }; +"loopng" , LOOP { txt = "LOOPNG"; cond = X86NG }; +"loople" , LOOP { txt = "LOOPLE"; cond = X86NG }; +"mfence" , MFENCE { txt = "MFENCE" }; +"dec" , MONOP { txt = "DEC"; op = X86DEC; sz = X86NONE }; +"inc" , MONOP { txt = "INC"; op = X86INC; sz = X86NONE }; +"not" , MONOP { txt = "NOT"; op = X86NOT; sz = X86NONE }; +"neg" , MONOP { txt = "NEG"; op = X86NEG; sz = X86NONE }; +"cmovo" , CMOV { txt = "CMOVO"; cond = X86O; sz = X86NONE }; +"cmovb" , CMOV { txt = "CMOVB"; cond = X86B; sz = X86NONE }; +"cmovc" , CMOV { txt = "CMOVC"; cond = X86B; sz = X86NONE }; +"cmovnae" , CMOV { txt = "CMOVNAE"; cond = X86B; sz = X86NONE }; +"cmove" , CMOV { txt = "CMOVE"; cond = X86E; sz = X86NONE }; +"cmovz" , CMOV { txt = "CMOVZ"; cond = X86E; sz = X86NONE }; +"cmova" , CMOV { txt = "CMOVA"; cond = X86A; sz = X86NONE }; +"cmovnbe" , CMOV { txt = "CMOVNBE"; cond = X86A; sz = X86NONE }; +"cmovs" , CMOV { txt = "CMOVS"; cond = X86S; sz = X86NONE }; +"cmovp" , CMOV { txt = "CMOVP"; cond = X86P; sz = X86NONE }; +"cmovpe" , CMOV { txt = "CMOVPE"; cond = X86P; sz = X86NONE }; +"cmovl" , CMOV { txt = "CMOVL"; cond = X86L; sz = X86NONE }; +"cmovnge" , CMOV { txt = "CMOVNGE"; cond = X86L; sz = X86NONE }; +"cmovg" , CMOV { txt = "CMOVG"; cond = X86G; sz = X86NONE }; +"cmovnle" , CMOV { txt = "CMOVNLE"; cond = X86G; sz = X86NONE }; +"cmovno" , CMOV { txt = "CMOVNO"; cond = X86NO; sz = X86NONE }; +"cmovnb" , CMOV { txt = "CMOVNB"; cond = X86NB; sz = X86NONE }; +"cmovnc" , CMOV { txt = "CMOVNC"; cond = X86NB; sz = X86NONE }; +"cmovae" , CMOV { txt = "CMOVAE"; cond = X86NB; sz = X86NONE }; +"cmovne" , CMOV { txt = "CMOVNE"; cond = X86NE; sz = X86NONE }; +"cmovnz" , CMOV { txt = "CMOVNZ"; cond = X86NE; sz = X86NONE }; +"cmovna" , CMOV { txt = "CMOVNA"; cond = X86NA; sz = X86NONE }; +"cmovbe" , CMOV { txt = "CMOVBE"; cond = X86NA; sz = X86NONE }; +"cmovns" , CMOV { txt = "CMOVNS"; cond = X86NS; sz = X86NONE }; +"cmovnp" , CMOV { txt = "CMOVNP"; cond = X86NP; sz = X86NONE }; +"cmovpo" , CMOV { txt = "CMOVPO"; cond = X86NP; sz = X86NONE }; +"cmovnl" , CMOV { txt = "CMOVNL"; cond = X86NL; sz = X86NONE }; +"cmovge" , CMOV { txt = "CMOVGE"; cond = X86NL; sz = X86NONE }; +"cmovng" , CMOV { txt = "CMOVNG"; cond = X86NG; sz = X86NONE }; +"cmovle" , CMOV { txt = "CMOVLE"; cond = X86NG; sz = X86NONE }; +"mov" , MOV { txt = "MOV"; sz = X86NONE }; +"movsx" , MOVSX { txt = "MOVSBW"; sz1 = X86NONE; sz2 = X86NONE }; +"movzx" , MOVZX { txt = "MOVZBW"; sz1 = X86NONE; sz2 = X86NONE }; +"mul" , MUL { txt = "MUL"; sz = X86NONE }; +"nop" , NOP { txt = "NOP" }; +"pop" , POP { txt = "POP" }; +"push" , PUSH { txt = "PUSH" }; +"ret" , PUSH { txt = "RET" }; +"seto" , SET { txt = "SETO"; cond = X86O }; +"setb" , SET { txt = "SETB"; cond = X86B }; +"setc" , SET { txt = "SETC"; cond = X86B }; +"setnae" , SET { txt = "SETNAE"; cond = X86B }; +"sete" , SET { txt = "SETE"; cond = X86E }; +"setz" , SET { txt = "SETZ"; cond = X86E }; +"seta" , SET { txt = "SETA"; cond = X86A }; +"setnbe" , SET { txt = "SETNBE"; cond = X86A }; +"sets" , SET { txt = "SETS"; cond = X86S }; +"setp" , SET { txt = "SETP"; cond = X86P }; +"setpe" , SET { txt = "SETPE"; cond = X86P }; +"setl" , SET { txt = "SETL"; cond = X86L }; +"setnge" , SET { txt = "SETNGE"; cond = X86L }; +"setg" , SET { txt = "SETG"; cond = X86G }; +"setnle" , SET { txt = "SETNLE"; cond = X86G }; +"setno" , SET { txt = "SETNO"; cond = X86NO }; +"setnb" , SET { txt = "SETNB"; cond = X86NB }; +"setnc" , SET { txt = "SETNC"; cond = X86NB }; +"setae" , SET { txt = "SETAE"; cond = X86NB }; +"setne" , SET { txt = "SETNE"; cond = X86NE }; +"setnz" , SET { txt = "SETNZ"; cond = X86NE }; +"setna" , SET { txt = "SETNA"; cond = X86NA }; +"setbe" , SET { txt = "SETBE"; cond = X86NA }; +"setns" , SET { txt = "SETNS"; cond = X86NS }; +"setnp" , SET { txt = "SETNP"; cond = X86NP }; +"setpo" , SET { txt = "SETPO"; cond = X86NP }; +"setnl" , SET { txt = "SETNL"; cond = X86NL }; +"setge" , SET { txt = "SETGE"; cond = X86NL }; +"setng" , SET { txt = "SETNG"; cond = X86NG }; +"setle" , SET { txt = "SETLE"; cond = X86NG }; +"stc" , STC { txt = "STC" }; +"xadd" , XADD { txt = "XADD"; sz = X86NONE }; +"xchg" , XCHG { txt = "XCHG"; sz = X86NONE }; diff --git a/old/x86/gen/map.hgen b/old/x86/gen/map.hgen new file mode 100644 index 00000000..843e8832 --- /dev/null +++ b/old/x86/gen/map.hgen @@ -0,0 +1,26 @@ +| `X86BINOP (locked, bop, sz, ds) -> `X86BINOP (locked, bop, sz, map_dest_src ds) +| `X86BITOP (locked, bop, sz, bo) -> `X86BITOP (locked, bop, sz, map_bit_offset bo) +| `X86CALL irm -> `X86CALL (map_imm_rm irm) +| `X86CLC -> `X86CLC +| `X86CMC -> `X86CMC +| `X86CMPXCHG (locked, sz, rm, r) -> `X86CMPXCHG (locked, sz, map_rm rm, map_reg r) +| `X86DIV (sz, rm) -> `X86DIV (sz, map_rm rm) +| `X86JCC x -> `X86JCC x +| `X86JMP rm -> `X86JMP (map_rm rm) +| `X86LEA (sz, ds) -> `X86LEA (sz, map_dest_src ds) +| `X86LEAVE -> `X86LEAVE +| `X86LOOP x -> `X86LOOP x +| `X86MFENCE -> `X86MFENCE +| `X86MONOP (locked, mop, sz, rm) -> `X86MONOP (locked, mop, sz, map_rm rm) +| `X86MOV (cnd, sz, ds) -> `X86MOV (cnd, sz, map_dest_src ds) +| `X86MOVSX (sz1, ds, sz2) -> `X86MOVSX (sz1, map_dest_src ds, sz2) +| `X86MOVZX (sz1, ds, sz2) -> `X86MOVZX (sz1, map_dest_src ds, sz2) +| `X86MUL (sz, rm) -> `X86MUL (sz, map_rm rm) +| `X86NOP -> `X86NOP +| `X86POP rm -> `X86POP (map_rm rm) +| `X86PUSH irm -> `X86PUSH (map_imm_rm irm) +| `X86RET i -> `X86RET i +| `X86SET (cnd, b, rm) -> `X86SET (cnd, b, map_rm rm) +| `X86STC -> `X86STC +| `X86XADD (locked, sz, rm, r) -> `X86XADD (locked, sz, map_rm rm, map_reg r) +| `X86XCHG (locked, sz, rm, r) -> `X86XCHG (locked, sz, map_rm rm, map_reg r) diff --git a/old/x86/gen/parser.hgen b/old/x86/gen/parser.hgen new file mode 100644 index 00000000..b3c9dc72 --- /dev/null +++ b/old/x86/gen/parser.hgen @@ -0,0 +1,600 @@ +| BINOP imm COMMA addr + { `X86BINOP (false, $1.op, suffix_size $1.sz, Rm_i ($4, bit64_of_int $2)) } +| LOCK BINOP imm COMMA addr + { check_binop_lockable $2.op + ; `X86BINOP (true, $2.op, suffix_size $2.sz, Rm_i ($5, bit64_of_int $3)) } +| BINOP imm COMMA breg + { check_size ($1.sz, X86BYTE) + ; `X86BINOP (false, $1.op, X86S8 ($4.high), Rm_i (Reg (IReg ($4.reg)), bit64_of_int $2)) + } +| BINOP breg COMMA breg + { check_size ($1.sz, X86BYTE) + ; check_byte_regs ($2, $4) + ; `X86BINOP (false, $1.op, X86S8 ($4.high), Rm_r (Reg (IReg ($4.reg)), IReg ($2.reg))) + } +| BINOP addr COMMA breg + { check_size ($1.sz, X86BYTE) + ; `X86BINOP (false, $1.op, X86S8 ($4.high), R_rm (IReg ($4.reg), $2)) + } +| BINOP breg COMMA addr + { check_size ($1.sz, X86BYTE) + ; `X86BINOP (false, $1.op, X86S8 ($2.high), Rm_r ($4, IReg ($2.reg))) + } +| LOCK BINOP breg COMMA addr + { check_binop_lockable $2.op + ; check_size ($2.sz, X86BYTE) + ; `X86BINOP (true, $2.op, X86S8 ($3.high), Rm_r ($5, IReg ($3.reg))) + } +| BINOP imm COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86BINOP (false, $1.op, X86S16, Rm_i (Reg $4, bit64_of_int $2)) + } +| BINOP wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86BINOP (false, $1.op, X86S16, Rm_r (Reg $4, $2)) + } +| BINOP addr COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86BINOP (false, $1.op, X86S16, R_rm ($4, $2)) + } +| BINOP wreg COMMA addr + { check_size ($1.sz, X86WORD) + ; `X86BINOP (false, $1.op, X86S16, Rm_r ($4, $2)) + } +| LOCK BINOP wreg COMMA addr + { check_binop_lockable $2.op + ; check_size ($2.sz, X86WORD) + ; `X86BINOP (true, $2.op, X86S16, Rm_r ($5, $3)) + } +| BINOP imm COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86BINOP (false, $1.op, X86S32, Rm_i (Reg $4, bit64_of_int $2)) + } +| BINOP lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86BINOP (false, $1.op, X86S32, Rm_r (Reg $4, $2)) + } +| BINOP addr COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86BINOP (false, $1.op, X86S32, R_rm ($4, $2)) + } +| BINOP lreg COMMA addr + { check_size ($1.sz, X86LONG) + ; `X86BINOP (false, $1.op, X86S32, Rm_r ($4, $2)) + } +| LOCK BINOP lreg COMMA addr + { check_binop_lockable $2.op + ; check_size ($2.sz, X86LONG) + ; `X86BINOP (true, $2.op, X86S32, Rm_r ($5, $3)) + } +| BINOP imm COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86BINOP (false, $1.op, X86S64, Rm_i (Reg $4, bit64_of_int $2)) + } +| BINOP qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86BINOP (false, $1.op, X86S64, Rm_r (Reg $4, $2)) + } +| BINOP addr COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86BINOP (false, $1.op, X86S64, R_rm ($4, $2)) + } +| BINOP qreg COMMA addr + { check_size ($1.sz, X86QUAD) + ; `X86BINOP (false, $1.op, X86S64, Rm_r ($4, $2)) + } +| LOCK BINOP qreg COMMA addr + { check_binop_lockable $2.op + ; check_size ($2.sz, X86QUAD) + ; `X86BINOP (true, $2.op, X86S64, Rm_r ($5, $3)) + } +| BITOP imm COMMA addr + { `X86BITOP (false, $1.op, suffix_size $1.sz, Bit_rm_imm ($4, $2)) + } +| LOCK BITOP imm COMMA addr + { `X86BITOP (true, $2.op, suffix_size $2.sz, Bit_rm_imm ($5, $3)) + } +| BITOP imm COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86BITOP (false, $1.op, X86S16, Bit_rm_imm (Reg $4, $2)) + } +| LOCK BITOP imm COMMA wreg + { check_size ($2.sz, X86WORD) + ; `X86BITOP (true, $2.op, X86S16, Bit_rm_imm (Reg $5, $3)) + } +| BITOP wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86BITOP (true, $1.op, X86S16, Bit_rm_r (Reg $4, $2)) + } +| LOCK BITOP wreg COMMA wreg + { check_size ($2.sz, X86WORD) + ; `X86BITOP (false, $2.op, X86S16, Bit_rm_r (Reg $5, $3)) + } +| BITOP wreg COMMA addr + { check_size ($1.sz, X86WORD) + ; `X86BITOP (false, $1.op, X86S16, Bit_rm_r ($4, $2)) + } +| LOCK BITOP wreg COMMA addr + { check_size ($2.sz, X86WORD) + ; `X86BITOP (true, $2.op, X86S16, Bit_rm_r ($5, $3)) + } +| BITOP imm COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86BITOP (false, $1.op, X86S32, Bit_rm_imm (Reg $4, $2)) + } +| LOCK BITOP imm COMMA lreg + { check_size ($2.sz, X86LONG) + ; `X86BITOP (true, $2.op, X86S32, Bit_rm_imm (Reg $5, $3)) + } +| BITOP lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86BITOP (false, $1.op, X86S32, Bit_rm_r (Reg $4, $2)) + } +| LOCK BITOP lreg COMMA lreg + { check_size ($2.sz, X86LONG) + ; `X86BITOP (true, $2.op, X86S32, Bit_rm_r (Reg $5, $3)) + } +| BITOP lreg COMMA addr + { check_size ($1.sz, X86LONG) + ; `X86BITOP (false, $1.op, X86S32, Bit_rm_r ($4, $2)) + } +| LOCK BITOP lreg COMMA addr + { check_size ($2.sz, X86LONG) + ; `X86BITOP (true, $2.op, X86S32, Bit_rm_r ($5, $3)) + } +| BITOP imm COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86BITOP (false, $1.op, X86S64, Bit_rm_imm (Reg $4, $2)) + } +| LOCK BITOP imm COMMA qreg + { check_size ($2.sz, X86QUAD) + ; `X86BITOP (true, $2.op, X86S64, Bit_rm_imm (Reg $5, $3)) + } +| BITOP qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86BITOP (false, $1.op, X86S64, Bit_rm_r (Reg $4, $2)) + } +| LOCK BITOP qreg COMMA qreg + { check_size ($2.sz, X86QUAD) + ; `X86BITOP (true, $2.op, X86S64, Bit_rm_r (Reg $5, $3)) + } +| BITOP qreg COMMA addr + { check_size ($1.sz, X86QUAD) + ; `X86BITOP (false, $1.op, X86S64, Bit_rm_r ($4, $2)) + } +| LOCK BITOP qreg COMMA addr + { check_size ($2.sz, X86QUAD) + ; `X86BITOP (true, $2.op, X86S64, Bit_rm_r ($5, $3)) + } +| CALL big_imm + { `X86CALL (Imm $2) } +| CALL addr + { `X86CALL (Rm $2) } +| CALL qreg + { `X86CALL (Rm (Reg $2)) } +| CLC + { `X86CLC } +| CMC + { `X86CMC } +| CMOV addr COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86MOV ($1.cond, X86S16, R_rm ($4, $2)) + } +| CMOV addr COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86MOV ($1.cond, X86S32, R_rm ($4, $2)) + } +| CMOV addr COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86MOV ($1.cond, X86S64, R_rm ($4, $2)) + } +| CMOV wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86MOV ($1.cond, X86S16, R_rm ($4, Reg $2)) + } +| CMOV lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86MOV ($1.cond, X86S32, R_rm ($4, Reg $2)) + } +| CMOV qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86MOV ($1.cond, X86S64, R_rm ($4, Reg $2)) + } +| CMPXCHG breg COMMA breg + { check_size ($1.sz, X86BYTE) + ; check_byte_regs ($2, $4) + ; `X86CMPXCHG (false, X86S8 ($2.high), Reg (IReg ($4.reg)), IReg ($2.reg)) + } +| CMPXCHG breg COMMA addr + { check_size ($1.sz, X86BYTE) + ; `X86CMPXCHG (false, X86S8 ($2.high), $4, IReg ($2.reg)) + } +| LOCK CMPXCHG breg COMMA addr + { check_size ($2.sz, X86BYTE) + ; `X86CMPXCHG (true, X86S8 ($3.high), $5, IReg ($3.reg)) + } +| CMPXCHG wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86CMPXCHG (false, X86S16, Reg $4, $2) + } +| CMPXCHG wreg COMMA addr + { check_size ($1.sz, X86WORD) + ; `X86CMPXCHG (false, X86S16, $4, $2) + } +| LOCK CMPXCHG wreg COMMA addr + { check_size ($2.sz, X86WORD) + ; `X86CMPXCHG (true, X86S16, $5, $3) + } +| CMPXCHG lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86CMPXCHG (false, X86S32, Reg $4, $2) + } +| CMPXCHG lreg COMMA addr + { check_size ($1.sz, X86LONG) + ; `X86CMPXCHG (false, X86S32, $4, $2) + } +| LOCK CMPXCHG lreg COMMA addr + { check_size ($2.sz, X86LONG) + ; `X86CMPXCHG (true, X86S32, $5, $3) + } +| CMPXCHG qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86CMPXCHG (false, X86S64, Reg $4, $2) + } +| CMPXCHG qreg COMMA addr + { check_size ($1.sz, X86QUAD) + ; `X86CMPXCHG (false, X86S64, $4, $2) + } +| LOCK CMPXCHG qreg COMMA addr + { check_size ($2.sz, X86QUAD) + ; `X86CMPXCHG (true, X86S64, $5, $3) + } +| DIV addr + { `X86DIV (suffix_size $1.sz, $2) } +| DIV breg + { check_size ($1.sz, X86BYTE) + ; `X86DIV (X86S8 ($2.high), Reg (IReg ($2.reg))) + } +| DIV wreg + { check_size ($1.sz, X86WORD) + ; `X86DIV (X86S16, Reg $2) + } +| DIV lreg + { check_size ($1.sz, X86LONG) + ; `X86DIV (X86S32, Reg $2) + } +| DIV qreg + { check_size ($1.sz, X86QUAD) + ; `X86DIV (X86S64, Reg $2) + } +| JCC big_num + { `X86JCC ($1.cond, $2) } +| JMP big_num + { `X86JCC (X86ALWAYS, $2) } +| JMP addr + { `X86JMP $2 } +| JMP qreg + { `X86JMP (Reg $2) } +| LEA addr COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86LEA (X86S16, R_rm ($4, $2)) + } +| LEA addr COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86LEA (X86S32, R_rm ($4, $2)) + } +| LEA addr COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86LEA (X86S64, R_rm ($4, $2)) + } +| LEAVE + { `X86LEAVE } +| LOOP big_num + { `X86LOOP ($1.cond, $2) } +| MFENCE + { `X86MFENCE } +| MONOP addr + { `X86MONOP (false, $1.op, suffix_size $1.sz, $2) } +| LOCK MONOP addr + { `X86MONOP (true, $2.op, suffix_size $2.sz, $3) } +| MONOP breg + { check_size ($1.sz, X86BYTE) + ; `X86MONOP (false, $1.op, X86S8 ($2.high), Reg (IReg $2.reg)) + } +| MONOP wreg + { check_size ($1.sz, X86WORD) + ; `X86MONOP (false, $1.op, X86S16, Reg $2) + } +| MONOP lreg + { check_size ($1.sz, X86LONG) + ; `X86MONOP (false, $1.op, X86S32, Reg $2) + } +| MONOP qreg + { check_size ($1.sz, X86QUAD) + ; `X86MONOP (false, $1.op, X86S64, Reg $2) + } +| MOV big_imm COMMA addr + { `X86MOV (X86ALWAYS, suffix_size $1.sz, Rm_i ($4, $2)) } +| MOV imm COMMA breg + { check_size ($1.sz, X86BYTE) + ; `X86MOV (X86ALWAYS, X86S8 ($4.high), Rm_i (Reg (IReg $4.reg), bit64_of_int $2)) + } +| MOV breg COMMA breg + { check_size ($1.sz, X86BYTE) + ; check_byte_regs ($2, $4) + ; `X86MOV (X86ALWAYS, X86S8 ($4.high), Rm_r (Reg (IReg $4.reg), (IReg $2.reg))) + } +| MOV addr COMMA breg + { check_size ($1.sz, X86BYTE) + ; `X86MOV (X86ALWAYS, X86S8 ($4.high), R_rm (IReg $4.reg, $2)) + } +| MOV breg COMMA addr + { check_size ($1.sz, X86BYTE) + ; `X86MOV (X86ALWAYS, X86S8 ($2.high), Rm_r ($4, IReg $2.reg)) + } +| MOV imm COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86MOV (X86ALWAYS, X86S16, Rm_i (Reg $4, bit64_of_int $2)) + } +| MOV wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86MOV (X86ALWAYS, X86S16, Rm_r (Reg $4, $2)) + } +| MOV addr COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86MOV (X86ALWAYS, X86S16, R_rm ($4, $2)) + } +| MOV wreg COMMA addr + { check_size ($1.sz, X86WORD) + ; `X86MOV (X86ALWAYS, X86S16, Rm_r ($4, $2)) + } +| MOV imm COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86MOV (X86ALWAYS, X86S32, Rm_i (Reg $4, bit64_of_int $2)) + } +| MOV lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86MOV (X86ALWAYS, X86S32, Rm_r (Reg $4, $2)) + } +| MOV addr COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86MOV (X86ALWAYS, X86S32, R_rm ($4, $2)) + } +| MOV lreg COMMA addr + { check_size ($1.sz, X86LONG) + ; `X86MOV (X86ALWAYS, X86S32, Rm_r ($4, $2)) + } +| MOV big_imm COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86MOV (X86ALWAYS, X86S64, Rm_i (Reg $4, $2)) + } +| MOV qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; if $1.txt = "MOVABS" then failwith "movabs expects and immediate" else () + ; `X86MOV (X86ALWAYS, X86S64, Rm_r (Reg $4, $2)) + } +| MOV addr COMMA qreg + { check_size ($1.sz, X86QUAD) + ; if $1.txt = "MOVABS" then failwith "movabs expects and immediate" else () + ; `X86MOV (X86ALWAYS, X86S64, R_rm ($4, $2)) + } +| MOV qreg COMMA addr + { check_size ($1.sz, X86QUAD) + ; if $1.txt = "MOVABS" then failwith "movabs expects and immediate" else () + ; `X86MOV (X86ALWAYS, X86S64, Rm_r ($4, $2)) + } +| MOVSX breg COMMA wreg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86WORD) + ; `X86MOVSX (X86S16, R_rm ($4, Reg (IReg $2.reg)), X86S8 $2.high) + } +| MOVSX breg COMMA lreg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86LONG) + ; `X86MOVSX (X86S32, R_rm ($4, Reg (IReg $2.reg)), X86S8 $2.high) + } +| MOVSX breg COMMA qreg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86QUAD) + ; `X86MOVSX (X86S64, R_rm ($4, Reg (IReg $2.reg)), X86S8 $2.high) + } +| MOVSX wreg COMMA lreg + { check_size ($1.sz1, X86WORD) + ; check_size ($1.sz2, X86LONG) + ; `X86MOVSX (X86S32, R_rm ($4, Reg $2), X86S16) + } +| MOVSX wreg COMMA qreg + { check_size ($1.sz1, X86WORD) + ; check_size ($1.sz2, X86QUAD) + ; `X86MOVSX (X86S64, R_rm ($4, Reg $2), X86S16) + } +| MOVSX lreg COMMA qreg + { check_size ($1.sz1, X86LONG) + ; check_size ($1.sz2, X86QUAD) + ; `X86MOVSX (X86S64, R_rm ($4, Reg $2), X86S32) + } +| MOVSX addr COMMA wreg + { check_size ($1.sz2, X86WORD) + ; `X86MOVSX (X86S16, R_rm ($4, $2), suffix_size $1.sz1) + } +| MOVSX addr COMMA lreg + { check_size ($1.sz2, X86LONG) + ; `X86MOVSX (X86S32, R_rm ($4, $2), suffix_size $1.sz1) + } +| MOVSX addr COMMA qreg + { check_size ($1.sz2, X86QUAD) + ; `X86MOVSX (X86S64, R_rm ($4, $2), suffix_size $1.sz1) + } +| MOVZX breg COMMA wreg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86WORD) + ; `X86MOVZX (X86S16, R_rm ($4, Reg (IReg $2.reg)), X86S8 $2.high) + } +| MOVZX breg COMMA lreg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86LONG) + ; `X86MOVZX (X86S32, R_rm ($4, Reg (IReg $2.reg)), X86S8 $2.high) + } +| MOVZX breg COMMA qreg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86QUAD) + ; `X86MOVZX (X86S64, R_rm ($4, Reg (IReg $2.reg)), X86S8 $2.high) + } +| MOVZX wreg COMMA lreg + { check_size ($1.sz1, X86WORD) + ; check_size ($1.sz2, X86LONG) + ; `X86MOVZX (X86S32, R_rm ($4, Reg $2), X86S16) + } +| MOVZX wreg COMMA qreg + { check_size ($1.sz1, X86WORD) + ; check_size ($1.sz2, X86QUAD) + ; `X86MOVZX (X86S64, R_rm ($4, Reg $2), X86S16) + } +| MOVZX addr COMMA wreg + { check_size ($1.sz2, X86WORD) + ; `X86MOVZX (X86S16, R_rm ($4, $2), suffix_size $1.sz1) + } +| MOVZX addr COMMA lreg + { check_size ($1.sz2, X86LONG) + ; `X86MOVZX (X86S32, R_rm ($4, $2), suffix_size $1.sz1) + } +| MOVZX addr COMMA qreg + { check_size ($1.sz2, X86QUAD) + ; `X86MOVZX (X86S64, R_rm ($4, $2), suffix_size $1.sz1) + } +| MUL addr + { `X86MUL (suffix_size $1.sz, $2) } +| MUL breg + { check_size ($1.sz, X86BYTE) + ; `X86MUL (X86S8 ($2.high), Reg (IReg $2.reg)) + } +| MUL wreg + { check_size ($1.sz, X86WORD) + ; `X86MUL (X86S16, Reg $2) + } +| MUL lreg + { check_size ($1.sz, X86LONG) + ; `X86MUL (X86S32, Reg $2) + } +| MUL qreg + { check_size ($1.sz, X86QUAD) + ; `X86MUL (X86S64, Reg $2) + } +| NOP + { `X86NOP } +| POP qreg + { `X86POP (Reg $2) } +| POP addr + { `X86POP $2 } +| PUSH big_imm + { `X86PUSH (Imm $2) } +| PUSH addr + { `X86PUSH (Rm $2) } +| PUSH qreg + { `X86PUSH (Rm (Reg $2)) } +| RET big_imm + { `X86RET $2 } +| SET breg + { `X86SET ($1.cond, $2.high, Reg (IReg $2.reg)) } +| SET addr + { `X86SET ($1.cond, false, $2) } +| STC + { `X86STC } +| XADD breg COMMA breg + { check_size ($1.sz, X86BYTE) + ; check_byte_regs ($2, $4) + ; `X86XADD (false, X86S8 ($2.high), Reg (IReg $4.reg), (IReg $2.reg)) + } +| XADD breg COMMA addr + { check_size ($1.sz, X86BYTE) + ; `X86XADD (false, X86S8 ($2.high), $4, (IReg $2.reg)) + } +| LOCK XADD breg COMMA addr + { check_size ($2.sz, X86BYTE) + ; `X86XADD (true, X86S8 ($3.high), $5, (IReg $3.reg)) + } +| XADD wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86XADD (false, X86S16, Reg $4, $2) + } +| XADD wreg COMMA addr + { check_size ($1.sz, X86WORD) + ; `X86XADD (false, X86S16, $4, $2) + } +| LOCK XADD wreg COMMA addr + { check_size ($2.sz, X86WORD) + ; `X86XADD (true, X86S16, $5, $3) + } +| XADD lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86XADD (false, X86S32, Reg $4, $2) + } +| XADD lreg COMMA addr + { check_size ($1.sz, X86LONG) + ; `X86XADD (false, X86S32, $4, $2) + } +| LOCK XADD lreg COMMA addr + { check_size ($2.sz, X86LONG) + ; `X86XADD (true, X86S32, $5, $3) + } +| XADD qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86XADD (false, X86S64, Reg $4, $2) + } +| XADD qreg COMMA addr + { check_size ($1.sz, X86QUAD) + ; `X86XADD (false, X86S64, $4, $2) + } +| LOCK XADD qreg COMMA addr + { check_size ($2.sz, X86QUAD) + ; `X86XADD (true, X86S64, $5, $3) + } +| XCHG breg COMMA breg + { check_size ($1.sz, X86BYTE) + ; check_byte_regs ($2, $4) + ; `X86XCHG (false, X86S8 ($2.high), Reg (IReg $4.reg), IReg $2.reg) + } +| XCHG breg COMMA addr + { check_size ($1.sz, X86BYTE) + ; `X86XCHG (false, X86S8 ($2.high), $4, (IReg $2.reg)) + } +| LOCK XCHG breg COMMA addr + { check_size ($2.sz, X86BYTE) + ; `X86XCHG (true, X86S8 ($3.high), $5, (IReg $3.reg)) + } +| XCHG wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86XCHG (false, X86S16, Reg $4, $2) + } +| XCHG wreg COMMA addr + { check_size ($1.sz, X86WORD) + ; `X86XCHG (false, X86S16, $4, $2) + } +| LOCK XCHG wreg COMMA addr + { check_size ($2.sz, X86WORD) + ; `X86XCHG (true, X86S16, $5, $3) + } +| XCHG lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86XCHG (false, X86S32, Reg $4, $2) + } +| XCHG lreg COMMA addr + { check_size ($1.sz, X86LONG) + ; `X86XCHG (false, X86S32, $4, $2) + } +| LOCK XCHG lreg COMMA addr + { check_size ($2.sz, X86LONG) + ; `X86XCHG (true, X86S32, $5, $3) + } +| XCHG qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86XCHG (false, X86S64, Reg $4, $2) + } +| XCHG qreg COMMA addr + { check_size ($1.sz, X86QUAD) + ; `X86XCHG (false, X86S64, $4, $2) + } +| LOCK XCHG qreg COMMA addr + { check_size ($2.sz, X86QUAD) + ; `X86XCHG (true, X86S64, $5, $3) + } diff --git a/old/x86/gen/parser_intel.hgen b/old/x86/gen/parser_intel.hgen new file mode 100644 index 00000000..72fa0ede --- /dev/null +++ b/old/x86/gen/parser_intel.hgen @@ -0,0 +1,601 @@ +| BINOP addr COMMA imm + { `X86BINOP (false, $1.op, suffix_size $1.sz, Rm_i ($2, bit64_of_int $4)) + (* XXX size is ambigious -- should require anotation *) } +| LOCK BINOP addr COMMA imm + { check_binop_lockable $2.op + ; `X86BINOP (true, $2.op, suffix_size $2.sz, Rm_i ($3, bit64_of_int $5)) } +| BINOP breg COMMA imm + { check_size ($1.sz, X86BYTE) + ; `X86BINOP (false, $1.op, X86S8 ($2.high), Rm_i (Reg (IReg ($2.reg)), bit64_of_int $4)) + } +| BINOP breg COMMA breg + { check_size ($1.sz, X86BYTE) + ; check_byte_regs ($2, $4) + ; `X86BINOP (false, $1.op, X86S8 ($2.high), Rm_r (Reg (IReg ($2.reg)), IReg ($4.reg))) + } +| BINOP addr COMMA breg + { check_size ($1.sz, X86BYTE) + ; `X86BINOP (false, $1.op, X86S8 ($4.high), Rm_r ($2, IReg ($4.reg))) + } +| LOCK BINOP addr COMMA breg + { check_binop_lockable $2.op; + check_size ($2.sz, X86BYTE) + ; `X86BINOP (true, $2.op, X86S8 ($5.high), Rm_r ($3, IReg ($5.reg))) + } +| BINOP breg COMMA addr + { check_size ($1.sz, X86BYTE) + ; `X86BINOP (false, $1.op, X86S8 ($2.high), R_rm (IReg ($2.reg), $4)) + } +| BINOP wreg COMMA imm + { check_size ($1.sz, X86WORD) + ; `X86BINOP (false, $1.op, X86S16, Rm_i (Reg $2, bit64_of_int $4)) + } +| BINOP wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86BINOP (false, $1.op, X86S16, Rm_r (Reg $2, $4)) + } +| BINOP addr COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86BINOP (false, $1.op, X86S16, Rm_r ($2, $4)) + } +| LOCK BINOP addr COMMA wreg + { check_binop_lockable $2.op; + check_size ($2.sz, X86WORD) + ; `X86BINOP (true, $2.op, X86S16, Rm_r ($3, $5)) + } +| BINOP wreg COMMA addr + { check_size ($1.sz, X86WORD) + ; `X86BINOP (false, $1.op, X86S16, R_rm ($2, $4)) + } +| BINOP lreg COMMA imm + { check_size ($1.sz, X86LONG) + ; `X86BINOP (false, $1.op, X86S32, Rm_i (Reg $2, bit64_of_int $4)) + } +| BINOP lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86BINOP (false, $1.op, X86S32, Rm_r (Reg $2, $4)) + } +| BINOP addr COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86BINOP (false, $1.op, X86S32, Rm_r ($2, $4)) + } +| LOCK BINOP addr COMMA lreg + { check_binop_lockable $2.op; + check_size ($2.sz, X86LONG) + ; `X86BINOP (true, $2.op, X86S32, Rm_r ($3, $5)) + } +| BINOP lreg COMMA addr + { check_size ($1.sz, X86LONG) + ; `X86BINOP (false, $1.op, X86S32, R_rm ($2, $4)) + } +| BINOP qreg COMMA imm + { check_size ($1.sz, X86QUAD) + ; `X86BINOP (false, $1.op, X86S64, Rm_i (Reg $2, bit64_of_int $4)) + } +| BINOP qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86BINOP (false, $1.op, X86S64, Rm_r (Reg $2, $4)) + } +| BINOP addr COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86BINOP (false, $1.op, X86S64, Rm_r ($2, $4)) + } +| LOCK BINOP addr COMMA qreg + { check_binop_lockable $2.op; + check_size ($2.sz, X86QUAD) + ; `X86BINOP (true, $2.op, X86S64, Rm_r ($3, $5)) + } +| BINOP qreg COMMA addr + { check_size ($1.sz, X86QUAD) + ; `X86BINOP (false, $1.op, X86S64, R_rm ($2, $4)) + } +| BITOP addr COMMA imm + { `X86BITOP (false, $1.op, suffix_size $1.sz, Bit_rm_imm ($2, $4)) + } +| LOCK BITOP addr COMMA imm + { `X86BITOP (true, $2.op, suffix_size $2.sz, Bit_rm_imm ($3, $5)) + } +| BITOP wreg COMMA imm + { check_size ($1.sz, X86WORD) + ; `X86BITOP (false, $1.op, X86S16, Bit_rm_imm (Reg $2, $4)) + } +| LOCK BITOP wreg COMMA imm + { check_size ($2.sz, X86WORD) + ; `X86BITOP (true, $2.op, X86S16, Bit_rm_imm (Reg $3, $5)) + } +| BITOP wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86BITOP (true, $1.op, X86S16, Bit_rm_r (Reg $2, $4)) + } +| LOCK BITOP wreg COMMA wreg + { check_size ($2.sz, X86WORD) + ; `X86BITOP (false, $2.op, X86S16, Bit_rm_r (Reg $3, $5)) + } +| BITOP addr COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86BITOP (false, $1.op, X86S16, Bit_rm_r ($2, $4)) + } +| LOCK BITOP addr COMMA wreg + { check_size ($2.sz, X86WORD) + ; `X86BITOP (true, $2.op, X86S16, Bit_rm_r ($3, $5)) + } +| BITOP lreg COMMA imm + { check_size ($1.sz, X86LONG) + ; `X86BITOP (false, $1.op, X86S32, Bit_rm_imm (Reg $2, $4)) + } +| LOCK BITOP lreg COMMA imm + { check_size ($2.sz, X86LONG) + ; `X86BITOP (true, $2.op, X86S32, Bit_rm_imm (Reg $3, $5)) + } +| BITOP lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86BITOP (false, $1.op, X86S32, Bit_rm_r (Reg $2, $4)) + } +| LOCK BITOP lreg COMMA lreg + { check_size ($2.sz, X86LONG) + ; `X86BITOP (true, $2.op, X86S32, Bit_rm_r (Reg $3, $5)) + } +| BITOP addr COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86BITOP (false, $1.op, X86S32, Bit_rm_r ($2, $4)) + } +| LOCK BITOP addr COMMA lreg + { check_size ($2.sz, X86LONG) + ; `X86BITOP (true, $2.op, X86S32, Bit_rm_r ($3, $5)) + } +| BITOP qreg COMMA imm + { check_size ($1.sz, X86QUAD) + ; `X86BITOP (false, $1.op, X86S64, Bit_rm_imm (Reg $2, $4)) + } +| LOCK BITOP qreg COMMA imm + { check_size ($2.sz, X86QUAD) + ; `X86BITOP (true, $2.op, X86S64, Bit_rm_imm (Reg $3, $5)) + } +| BITOP qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86BITOP (false, $1.op, X86S64, Bit_rm_r (Reg $2, $4)) + } +| LOCK BITOP qreg COMMA qreg + { check_size ($2.sz, X86QUAD) + ; `X86BITOP (true, $2.op, X86S64, Bit_rm_r (Reg $3, $5)) + } +| BITOP addr COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86BITOP (false, $1.op, X86S64, Bit_rm_r ($2, $4)) + } +| LOCK BITOP addr COMMA qreg + { check_size ($2.sz, X86QUAD) + ; `X86BITOP (true, $2.op, X86S64, Bit_rm_r ($3, $5)) + } +| CALL big_imm + { `X86CALL (Imm $2) } +| CALL addr + { `X86CALL (Rm $2) } +| CALL qreg + { `X86CALL (Rm (Reg $2)) } +| CLC + { `X86CLC } +| CMC + { `X86CMC } +| CMOV wreg COMMA addr + { check_size ($1.sz, X86WORD) + ; `X86MOV ($1.cond, X86S16, R_rm ($2, $4)) + } +| CMOV lreg COMMA addr + { check_size ($1.sz, X86LONG) + ; `X86MOV ($1.cond, X86S32, R_rm ($2, $4)) + } +| CMOV qreg COMMA addr + { check_size ($1.sz, X86QUAD) + ; `X86MOV ($1.cond, X86S64, R_rm ($2, $4)) + } +| CMOV wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86MOV ($1.cond, X86S16, R_rm ($2, Reg $4)) + } +| CMOV lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86MOV ($1.cond, X86S32, R_rm ($2, Reg $4)) + } +| CMOV qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86MOV ($1.cond, X86S64, R_rm ($2, Reg $4)) + } +| CMPXCHG breg COMMA breg + { check_size ($1.sz, X86BYTE) + ; check_byte_regs ($2, $4) + ; `X86CMPXCHG (false, X86S8 ($2.high), Reg (IReg ($2.reg)), IReg ($4.reg)) + } +| CMPXCHG addr COMMA breg + { check_size ($1.sz, X86BYTE) + ; `X86CMPXCHG (false, X86S8 ($4.high), $2, IReg ($4.reg)) + } +| LOCK CMPXCHG addr COMMA breg + { check_size ($2.sz, X86BYTE) + ; `X86CMPXCHG (true, X86S8 ($5.high), $3, IReg ($5.reg)) + } +| CMPXCHG wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86CMPXCHG (false, X86S16, Reg $2, $4) + } +| CMPXCHG addr COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86CMPXCHG (false, X86S16, $2, $4) + } +| LOCK CMPXCHG addr COMMA wreg + { check_size ($2.sz, X86WORD) + ; `X86CMPXCHG (true, X86S16, $3, $5) + } +| CMPXCHG lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86CMPXCHG (false, X86S32, Reg $2, $4) + } +| CMPXCHG addr COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86CMPXCHG (false, X86S32, $2, $4) + } +| LOCK CMPXCHG addr COMMA lreg + { check_size ($2.sz, X86LONG) + ; `X86CMPXCHG (true, X86S32, $3, $5) + } +| CMPXCHG qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86CMPXCHG (false, X86S64, Reg $2, $4) + } +| CMPXCHG addr COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86CMPXCHG (false, X86S64, $2, $4) + } +| LOCK CMPXCHG addr COMMA qreg + { check_size ($2.sz, X86QUAD) + ; `X86CMPXCHG (true, X86S64, $3, $5) + } +| DIV addr + { `X86DIV (suffix_size $1.sz, $2) } +| DIV breg + { check_size ($1.sz, X86BYTE) + ; `X86DIV (X86S8 ($2.high), Reg (IReg ($2.reg))) + } +| DIV wreg + { check_size ($1.sz, X86WORD) + ; `X86DIV (X86S16, Reg $2) + } +| DIV lreg + { check_size ($1.sz, X86LONG) + ; `X86DIV (X86S32, Reg $2) + } +| DIV qreg + { check_size ($1.sz, X86QUAD) + ; `X86DIV (X86S64, Reg $2) + } +| JCC big_num + { `X86JCC ($1.cond, $2) } +| JMP big_num + { `X86JCC (X86ALWAYS, $2) } +| JMP addr + { `X86JMP $2 } +| JMP qreg + { `X86JMP (Reg $2) } +| LEA wreg COMMA addr + { check_size ($1.sz, X86WORD) + ; `X86LEA (X86S16, R_rm ($2, $4)) + } +| LEA lreg COMMA addr + { check_size ($1.sz, X86LONG) + ; `X86LEA (X86S32, R_rm ($2, $4)) + } +| LEA qreg COMMA addr + { check_size ($1.sz, X86QUAD) + ; `X86LEA (X86S64, R_rm ($2, $4)) + } +| LEAVE + { `X86LEAVE } +| LOOP big_num + { `X86LOOP ($1.cond, $2) } +| MFENCE + { `X86MFENCE } +| MONOP addr + { `X86MONOP (false, $1.op, suffix_size $1.sz, $2) } +| LOCK MONOP addr + { `X86MONOP (true, $2.op, suffix_size $2.sz, $3) } +| MONOP breg + { check_size ($1.sz, X86BYTE) + ; `X86MONOP (false, $1.op, X86S8 ($2.high), Reg (IReg $2.reg)) + } +| MONOP wreg + { check_size ($1.sz, X86WORD) + ; `X86MONOP (false, $1.op, X86S16, Reg $2) + } +| MONOP lreg + { check_size ($1.sz, X86LONG) + ; `X86MONOP (false, $1.op, X86S32, Reg $2) + } +| MONOP qreg + { check_size ($1.sz, X86QUAD) + ; `X86MONOP (false, $1.op, X86S64, Reg $2) + } +| MOV addr COMMA big_imm + { `X86MOV (X86ALWAYS, suffix_size $1.sz, Rm_i ($2, $4)) } +| MOV breg COMMA imm + { check_size ($1.sz, X86BYTE) + ; `X86MOV (X86ALWAYS, X86S8 ($2.high), Rm_i (Reg (IReg $2.reg), bit64_of_int $4)) + } +| MOV breg COMMA breg + { check_size ($1.sz, X86BYTE) + ; check_byte_regs ($2, $4) + ; `X86MOV (X86ALWAYS, X86S8 ($2.high), Rm_r (Reg (IReg $2.reg), (IReg $4.reg))) + } +| MOV addr COMMA breg + { check_size ($1.sz, X86BYTE) + ; `X86MOV (X86ALWAYS, X86S8 ($4.high), Rm_r ($2, IReg $4.reg)) + } +| MOV breg COMMA addr + { check_size ($1.sz, X86BYTE) + ; `X86MOV (X86ALWAYS, X86S8 ($2.high), R_rm (IReg $2.reg, $4)) + } +| MOV wreg COMMA imm + { check_size ($1.sz, X86WORD) + ; `X86MOV (X86ALWAYS, X86S16, Rm_i (Reg $2, bit64_of_int $4)) + } +| MOV wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86MOV (X86ALWAYS, X86S16, Rm_r (Reg $2, $4)) + } +| MOV addr COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86MOV (X86ALWAYS, X86S16, Rm_r ($2, $4)) + } +| MOV wreg COMMA addr + { check_size ($1.sz, X86WORD) + ; `X86MOV (X86ALWAYS, X86S16, R_rm ($2, $4)) + } +| MOV lreg COMMA imm + { check_size ($1.sz, X86LONG) + ; `X86MOV (X86ALWAYS, X86S32, Rm_i (Reg $2, bit64_of_int $4)) + } +| MOV lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86MOV (X86ALWAYS, X86S32, Rm_r (Reg $2, $4)) + } +| MOV addr COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86MOV (X86ALWAYS, X86S32, Rm_r ($2, $4)) + } +| MOV lreg COMMA addr + { check_size ($1.sz, X86LONG) + ; `X86MOV (X86ALWAYS, X86S32, R_rm ($2, $4)) + } +| MOV qreg COMMA big_imm + { check_size ($1.sz, X86QUAD) + ; `X86MOV (X86ALWAYS, X86S64, Rm_i (Reg $2, $4)) + } +| MOV qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; if $1.txt = "MOVABS" then failwith "movabs expects an immediate" else () + ; `X86MOV (X86ALWAYS, X86S64, Rm_r (Reg $2, $4)) + } +| MOV addr COMMA qreg + { check_size ($1.sz, X86QUAD) + ; if $1.txt = "MOVABS" then failwith "movabs expects an immediate" else () + ; `X86MOV (X86ALWAYS, X86S64, Rm_r ($2, $4)) + } +| MOV qreg COMMA addr + { check_size ($1.sz, X86QUAD) + ; if $1.txt = "MOVABS" then failwith "movabs expects an immediate" else () + ; `X86MOV (X86ALWAYS, X86S64, R_rm ($2, $4)) + } +| MOVSX wreg COMMA breg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86WORD) + ; `X86MOVSX (X86S16, R_rm ($2, Reg (IReg $4.reg)), X86S8 $4.high) + } +| MOVSX lreg COMMA breg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86LONG) + ; `X86MOVSX (X86S32, R_rm ($2, Reg (IReg $4.reg)), X86S8 $4.high) + } +| MOVSX qreg COMMA breg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86QUAD) + ; `X86MOVSX (X86S64, R_rm ($2, Reg (IReg $4.reg)), X86S8 $4.high) + } +| MOVSX lreg COMMA wreg + { check_size ($1.sz1, X86WORD) + ; check_size ($1.sz2, X86LONG) + ; `X86MOVSX (X86S32, R_rm ($2, Reg $4), X86S16) + } +| MOVSX qreg COMMA wreg + { check_size ($1.sz1, X86WORD) + ; check_size ($1.sz2, X86QUAD) + ; `X86MOVSX (X86S64, R_rm ($2, Reg $4), X86S16) + } +| MOVSX qreg COMMA lreg + { check_size ($1.sz1, X86LONG) + ; check_size ($1.sz2, X86QUAD) + ; `X86MOVSX (X86S64, R_rm ($2, Reg $4), X86S32) + } +| MOVSX wreg COMMA addr + { check_size ($1.sz2, X86WORD) + ; `X86MOVSX (X86S16, R_rm ($2, $4), suffix_size $1.sz1) (* XXX size *) + } +| MOVSX lreg COMMA addr + { check_size ($1.sz2, X86LONG) + ; `X86MOVSX (X86S32, R_rm ($2, $4), suffix_size $1.sz1) + } +| MOVSX qreg COMMA addr + { check_size ($1.sz2, X86QUAD) + ; `X86MOVSX (X86S64, R_rm ($2, $4), suffix_size $1.sz1) + } +| MOVZX wreg COMMA breg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86WORD) + ; `X86MOVZX (X86S16, R_rm ($2, Reg (IReg $4.reg)), X86S8 $4.high) + } +| MOVZX lreg COMMA breg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86LONG) + ; `X86MOVZX (X86S32, R_rm ($2, Reg (IReg $4.reg)), X86S8 $4.high) + } +| MOVZX qreg COMMA breg + { check_size ($1.sz1, X86BYTE) + ; check_size ($1.sz2, X86QUAD) + ; `X86MOVZX (X86S64, R_rm ($2, Reg (IReg $4.reg)), X86S8 $4.high) + } +| MOVZX lreg COMMA wreg + { check_size ($1.sz1, X86WORD) + ; check_size ($1.sz2, X86LONG) + ; `X86MOVZX (X86S32, R_rm ($2, Reg $4), X86S16) + } +| MOVZX qreg COMMA wreg + { check_size ($1.sz1, X86WORD) + ; check_size ($1.sz2, X86QUAD) + ; `X86MOVZX (X86S64, R_rm ($2, Reg $4), X86S16) + } +| MOVZX wreg COMMA addr + { check_size ($1.sz2, X86WORD) + ; `X86MOVZX (X86S16, R_rm ($2, $4), suffix_size $1.sz1) (* XXX size *) + } +| MOVZX lreg COMMA addr + { check_size ($1.sz2, X86LONG) + ; `X86MOVZX (X86S32, R_rm ($2, $4), suffix_size $1.sz1) + } +| MOVZX qreg COMMA addr + { check_size ($1.sz2, X86QUAD) + ; `X86MOVZX (X86S64, R_rm ($2, $4), suffix_size $1.sz1) + } +| MUL addr + { `X86MUL (suffix_size $1.sz, $2) } +| MUL breg + { check_size ($1.sz, X86BYTE) + ; `X86MUL (X86S8 ($2.high), Reg (IReg $2.reg)) + } +| MUL wreg + { check_size ($1.sz, X86WORD) + ; `X86MUL (X86S16, Reg $2) + } +| MUL lreg + { check_size ($1.sz, X86LONG) + ; `X86MUL (X86S32, Reg $2) + } +| MUL qreg + { check_size ($1.sz, X86QUAD) + ; `X86MUL (X86S64, Reg $2) + } +| NOP + { `X86NOP } +| POP qreg + { `X86POP (Reg $2) } +| POP addr + { `X86POP $2 } +| PUSH big_imm + { `X86PUSH (Imm $2) } +| PUSH addr + { `X86PUSH (Rm $2) } +| PUSH qreg + { `X86PUSH (Rm (Reg $2)) } +| RET big_imm + { `X86RET $2 } +| SET breg + { `X86SET ($1.cond, $2.high, Reg (IReg $2.reg)) } +| SET addr + { `X86SET ($1.cond, false, $2) } +| STC + { `X86STC } +| XADD breg COMMA breg + { check_size ($1.sz, X86BYTE) + ; check_byte_regs ($2, $4) + ; `X86XADD (false, X86S8 ($2.high), Reg (IReg $2.reg), (IReg $4.reg)) + } +| XADD addr COMMA breg + { check_size ($1.sz, X86BYTE) + ; `X86XADD (false, X86S8 ($4.high), $2, (IReg $4.reg)) + } +| LOCK XADD addr COMMA breg + { check_size ($2.sz, X86BYTE) + ; `X86XADD (true, X86S8 ($5.high), $3, (IReg $5.reg)) + } +| XADD wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86XADD (false, X86S16, Reg $2, $4) + } +| XADD addr COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86XADD (false, X86S16, $2, $4) + } +| LOCK XADD addr COMMA wreg + { check_size ($2.sz, X86WORD) + ; `X86XADD (true, X86S16, $3, $5) + } +| XADD lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86XADD (false, X86S32, Reg $2, $4) + } +| XADD addr COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86XADD (false, X86S32, $2, $4) + } +| LOCK XADD addr COMMA lreg + { check_size ($2.sz, X86LONG) + ; `X86XADD (true, X86S32, $3, $5) + } +| XADD qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86XADD (false, X86S64, Reg $2, $4) + } +| XADD addr COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86XADD (false, X86S64, $2, $4) + } +| LOCK XADD addr COMMA qreg + { check_size ($2.sz, X86QUAD) + ; `X86XADD (true, X86S64, $3, $5) + } +| XCHG breg COMMA breg + { check_size ($1.sz, X86BYTE) + ; check_byte_regs ($2, $4) + ; `X86XCHG (false, X86S8 ($2.high), Reg (IReg $2.reg), IReg $4.reg) + } +| XCHG addr COMMA breg + { check_size ($1.sz, X86BYTE) + ; `X86XCHG (false, X86S8 ($4.high), $2, (IReg $4.reg)) + } +| LOCK XCHG addr COMMA breg + { check_size ($2.sz, X86BYTE) + ; `X86XCHG (true, X86S8 ($5.high), $3, (IReg $5.reg)) + } +| XCHG wreg COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86XCHG (false, X86S16, Reg $2, $4) + } +| XCHG addr COMMA wreg + { check_size ($1.sz, X86WORD) + ; `X86XCHG (false, X86S16, $2, $4) + } +| LOCK XCHG addr COMMA wreg + { check_size ($2.sz, X86WORD) + ; `X86XCHG (true, X86S16, $3, $5) + } +| XCHG lreg COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86XCHG (false, X86S32, Reg $2, $4) + } +| XCHG addr COMMA lreg + { check_size ($1.sz, X86LONG) + ; `X86XCHG (false, X86S32, $2, $4) + } +| LOCK XCHG addr COMMA lreg + { check_size ($2.sz, X86LONG) + ; `X86XCHG (true, X86S32, $3, $5) + } +| XCHG qreg COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86XCHG (false, X86S64, Reg $2, $4) + } +| XCHG addr COMMA qreg + { check_size ($1.sz, X86QUAD) + ; `X86XCHG (false, X86S64, $2, $4) + } +| LOCK XCHG addr COMMA qreg + { check_size ($2.sz, X86QUAD) + ; `X86XCHG (true, X86S64, $3, $5) + } diff --git a/old/x86/gen/pretty.hgen b/old/x86/gen/pretty.hgen new file mode 100644 index 00000000..fc0c59d4 --- /dev/null +++ b/old/x86/gen/pretty.hgen @@ -0,0 +1,50 @@ +| `X86BINOP (locked, bop, sz, dst_src) -> + pp_locked locked ^ pp_x86Binop bop ^ pp_x86Size sz ^ " " ^ pp_x86Dest_src (sz, dst_src) +| `X86BITOP (locked, bop, sz, bo) -> + pp_locked locked ^ pp_x86Bitop bop ^ pp_x86Size sz ^ " " ^ pp_x86Bit_offset (sz, bo) +| `X86CALL (Imm i) -> "call " ^ " $" ^ bit64_to_string i +| `X86CALL (Rm rm) -> "call " ^ pp_x86Rm (X86S64, rm) +| `X86CLC -> "clc" +| `X86CMC -> "cmc" +| `X86CMPXCHG (locked, sz, rm, r) -> + sprintf "%scmpxchg%s %s, %s" + (pp_locked locked) (pp_x86Size sz) (pp_size_reg sz r) (pp_x86Rm (sz, rm)) +| `X86DIV (sz, rm) -> "div" ^ pp_x86Size sz ^ " " ^ pp_x86Rm (sz, rm) +| `X86JCC (X86ALWAYS, i) -> "jmp " ^ bit64_to_string i +| `X86JCC (cnd, i) -> "j" ^ pp_x86Cond cnd ^ " " ^ bit64_to_string i +| `X86JMP (rm) -> "jmp " ^ pp_x86Rm(X86S64, rm) +| `X86LEA (sz, dst_src) -> + "lea" ^ (pp_x86Size sz) ^ " " ^ pp_x86Dest_src (sz, dst_src) +| `X86LEAVE -> "leave" +| `X86LOOP (cnd, i) -> "loop" ^ pp_x86Cond cnd ^ " " ^ bit64_to_string i +| `X86MFENCE -> "mfence" +| `X86MONOP (locked, mop, sz, rm) -> + pp_x86Monop mop ^ pp_x86Size sz ^ " " ^ pp_x86Rm (sz, rm) +| `X86MOV (X86ALWAYS, sz, dst_src) -> + "mov" ^ pp_x86Size sz ^ " " ^ pp_x86Dest_src (sz, dst_src) +| `X86MOV (cnd, sz, dst_src) -> + "cmov" ^ pp_x86Cond cnd ^ pp_x86Size sz ^ " " ^ pp_x86Dest_src (sz, dst_src) +| `X86MOVSX (sz1, R_rm (r, rm), sz2) -> + "movs" ^ pp_x86Size sz1 ^ pp_x86Size sz2 ^ " " ^ pp_x86Rm (sz1, rm) ^ + ", " ^ pp_size_reg sz2 r +| `X86MOVSX (sz1, _, sz2) -> failwith "bad movsx instruction" +| `X86MOVZX (sz1, R_rm (r, rm), sz2) -> + "movz" ^ pp_x86Size sz1 ^ pp_x86Size sz2 ^ " " ^ pp_x86Rm (sz1, rm) ^ + ", " ^ pp_size_reg sz2 r +| `X86MOVZX (sz1, _, sz2) -> failwith "bad movzx instruction" +| `X86MUL (sz, rm) -> "mul" ^ pp_x86Size sz ^ " " ^ pp_x86Rm (sz, rm) +| `X86NOP -> "nop" +| `X86POP rm -> "pop " ^ (pp_x86Rm (X86S64, rm)) +| `X86PUSH (Imm i) -> "push $" ^ bit64_to_string i +| `X86PUSH (Rm rm) -> "push " ^ pp_x86Rm (X86S64, rm) +| `X86RET i -> "ret " ^ bit64_to_string i +| `X86SET (cnd, b, rm) -> "set" ^ pp_x86Cond cnd ^ " " ^ pp_x86Rm (X86S8 b, rm) +| `X86STC -> "stc" +| `X86XADD (locked, sz, rm, r) -> + sprintf "%s xadd%s %s, %s" + (pp_locked locked) (pp_x86Size sz) (pp_size_reg sz r) (pp_x86Rm (sz, rm)) +| `X86XCHG (locked, sz, rm, r) -> + sprintf "%sxchg%s %s, %s" + (pp_locked locked) (pp_x86Size sz) (pp_size_reg sz r) (pp_x86Rm (sz, rm)) +| `X86ThreadStart -> "start" +| `X86StopFetching -> "hlt" diff --git a/old/x86/gen/sail_trans_out.hgen b/old/x86/gen/sail_trans_out.hgen new file mode 100644 index 00000000..948db8fa --- /dev/null +++ b/old/x86/gen/sail_trans_out.hgen @@ -0,0 +1 @@ +(* *) diff --git a/old/x86/gen/shallow_ast_to_herdtools_ast.hgen b/old/x86/gen/shallow_ast_to_herdtools_ast.hgen new file mode 100644 index 00000000..ed5d6680 --- /dev/null +++ b/old/x86/gen/shallow_ast_to_herdtools_ast.hgen @@ -0,0 +1,27 @@ +| Binop (locked, binop, sz, dest_src) -> `X86BINOP (translate_out_bool locked, translate_out_binop binop, translate_out_size sz, translate_out_dest_src dest_src) +| Bitop (locked, bitop, sz, bo) -> `X86BITOP (translate_out_bool locked, translate_out_bitop bitop, translate_out_size sz, translate_out_bitoffset bo) +| CALL (imm_rm) -> `X86CALL (translate_out_imm_rm imm_rm) +| CLC -> `X86CLC +| CMC -> `X86CMC +| CMPXCHG (locked, sz, rm , reg) -> `X86CMPXCHG (translate_out_bool locked, translate_out_size sz, translate_out_rm rm, translate_out_reg reg) +| X86_DIV (sz, rm) -> `X86DIV (translate_out_size sz, translate_out_rm rm) +| HLT -> `X86StopFetching +| Jcc (cond, imm64) -> `X86JCC (translate_out_cond cond, translate_out_imm64 imm64) +| JMP (rm) -> `X86JMP (translate_out_rm rm) +| LEA (sz, dest_src) -> `X86LEA (translate_out_size sz, translate_out_dest_src dest_src) +| LEAVE -> `X86LEAVE +| LOOP (cond, imm64) -> `X86LOOP (translate_out_cond cond, translate_out_imm64 imm64) +| MFENCE -> `X86MFENCE +| Monop (locked, monop, sz, rm) -> `X86MONOP (translate_out_bool locked, translate_out_monop monop, translate_out_size sz, translate_out_rm rm) +| MOV (cond, sz, dest_src) -> `X86MOV (translate_out_cond cond, translate_out_size sz, translate_out_dest_src dest_src) +| MOVSX (sz1, dest_src, sz2) -> `X86MOVSX (translate_out_size sz1, translate_out_dest_src dest_src, translate_out_size sz2) +| MOVZX (sz1, dest_src, sz2) -> `X86MOVZX (translate_out_size sz1, translate_out_dest_src dest_src, translate_out_size sz2) +| X86_MUL (sz, rm) -> `X86MUL (translate_out_size sz, translate_out_rm rm) +| NOP (_) -> `X86NOP +| POP (rm) -> `X86POP (translate_out_rm rm) +| PUSH (imm_rm) -> `X86PUSH (translate_out_imm_rm imm_rm) +| RET (imm64) -> `X86RET (translate_out_imm64 imm64) +| SET (cond, b, rm) -> `X86SET (translate_out_cond cond, translate_out_bool b, translate_out_rm rm) +| STC -> `X86STC +| XADD (locked, sz, rm, reg) -> `X86XADD (translate_out_bool locked, translate_out_size sz, translate_out_rm rm, translate_out_reg reg) +| XCHG (locked, sz, rm, reg) -> `X86XCHG (translate_out_bool locked, translate_out_size sz, translate_out_rm rm, translate_out_reg reg) diff --git a/old/x86/gen/shallow_types_to_herdtools_types.hgen b/old/x86/gen/shallow_types_to_herdtools_types.hgen new file mode 100644 index 00000000..ba4eccaa --- /dev/null +++ b/old/x86/gen/shallow_types_to_herdtools_types.hgen @@ -0,0 +1,97 @@ +let is_inc = false + +let translate_out_bool = function + | Sail_values.B1 -> true + | Sail_values.B0 -> false + | _ -> failwith "translate_out_bool Undef" + +let translate_out_binop = function + | X86_Add -> X86ADD + | X86_Or -> X86OR + | X86_Adc -> X86ADC + | X86_Sbb -> X86SBB + | X86_And -> X86AND + | X86_Sub -> X86SUB + | X86_Xor -> X86XOR + | X86_Cmp -> X86CMP + | X86_Rol -> X86ROL + | X86_Ror -> X86ROR + | X86_Rcl -> X86RCL + | X86_Rcr -> X86RCR + | X86_Shl -> X86SHL + | X86_Shr -> X86SHR + | X86_Test -> X86TEST + | X86_Sar -> X86SAR + +let translate_out_bitop = function + | Btc -> X86Btc + | Bts -> X86Bts + | Btr -> X86Btr + +let translate_out_size = function + | Sz8 (high) -> X86S8 (translate_out_bool high) + | Sz16 -> X86S16 + | Sz32 -> X86S32 + | Sz64 -> X86S64 + +let translate_out_big_bit = Sail_values.unsigned + +let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst)) + +let translate_out_reg r = IReg (int_to_ireg (Nat_big_num.to_int r)) + +let translate_out_scale = translate_out_int + +let translate_out_imm64 i = translate_out_big_bit i + +let translate_out_msi = function + | Some (scale, reg) -> Some (translate_out_scale scale, translate_out_reg reg) + | None -> None + +let translate_out_base = function + | X86_embed_types.NoBase -> X86HGenBase.NoBase + | X86_embed_types.RegBase(r) -> X86HGenBase.RegBase (translate_out_reg r) + | X86_embed_types.RipBase -> X86HGenBase.RipBase + +let translate_out_rm = function + | X86_embed_types.X86_Reg (r) -> X86HGenBase.Reg (translate_out_reg r) + | X86_embed_types.Mem (m_si, base, imm) -> X86HGenBase.Mem (translate_out_msi m_si, translate_out_base base, translate_out_imm64 imm) + +let translate_out_dest_src = function + | X86_embed_types.R_rm (reg, rm) -> X86HGenBase.R_rm (translate_out_reg reg, translate_out_rm rm) + | X86_embed_types.Rm_i (rm, imm64) -> X86HGenBase.Rm_i (translate_out_rm rm, translate_out_imm64 imm64) + | X86_embed_types.Rm_r (rm, reg) -> X86HGenBase.Rm_r (translate_out_rm rm, translate_out_reg reg) + +let translate_out_imm_rm = function + | X86_embed_types.Imm (imm) -> X86HGenBase.Imm (translate_out_imm64 imm) + | X86_embed_types.Rm (rm) -> X86HGenBase.Rm (translate_out_rm rm) + +let translate_out_bitoffset = function + | Bit_rm_imm (rm, imm) -> X86HGenBase.Bit_rm_imm (translate_out_rm rm, Nat_big_num.to_int (translate_out_imm64 imm)) + | Bit_rm_r (rm, r) -> X86HGenBase.Bit_rm_r (translate_out_rm rm, translate_out_reg r) + +let translate_out_cond = function + | X86_O -> X86O + | X86_NO -> X86NO + | X86_B -> X86B + | X86_NB -> X86NB + | X86_E -> X86E + | X86_NE -> X86NE + | X86_NA -> X86NA + | X86_A -> X86A + | X86_S -> X86S + | X86_NS -> X86NS + | X86_P -> X86P + | X86_NP -> X86NP + | X86_L -> X86L + | X86_NL -> X86NL + | X86_NG -> X86NG + | X86_G -> X86G + | X86_ALWAYS -> X86ALWAYS + +let translate_out_monop = function + | X86_Dec -> X86DEC + | X86_Inc -> X86INC + | X86_Not -> X86NOT + | X86_Neg -> X86NEG + diff --git a/old/x86/gen/token_types.hgen b/old/x86/gen/token_types.hgen new file mode 100644 index 00000000..9485e544 --- /dev/null +++ b/old/x86/gen/token_types.hgen @@ -0,0 +1,29 @@ +type token_BINOP = { txt : string; op : x86Binop; sz : x86Suffix } +type token_BITOP = { txt : string; op : x86Bitop; sz : x86Suffix } +type token_CALL = { txt : string } +type token_CLC = { txt : string } +type token_CMC = { txt : string } +type token_CMOV = { txt : string; cond : x86Cond; sz : x86Suffix } +type token_CMPXCHG = { txt : string; sz : x86Suffix } +type token_DIV = { txt : string; sz : x86Suffix } +type token_JCC = { txt : string; cond : x86Cond } +type token_JMP = { txt : string } +type token_LEA = { txt : string; sz : x86Suffix } +type token_LEAVE = { txt : string } +type token_LOOP = { txt : string; cond : x86Cond } +type token_MFENCE = { txt : string; } +type token_MONOP = { txt : string; op : x86Monop; sz : x86Suffix } +type token_MOV = { txt : string; sz : x86Suffix } +type token_MOVABS = { txt : string } +type token_MOVSX = { txt : string; sz1 : x86Suffix; sz2 : x86Suffix } +type token_MOVZX = { txt : string; sz1 : x86Suffix; sz2 : x86Suffix } +type token_MUL = { txt : string; sz : x86Suffix } +type token_NOP = { txt : string } +type token_POP = { txt : string } +type token_PUSH = { txt : string } +type token_RET = { txt : string } +type token_SET = { txt : string; cond : x86Cond } +type token_STC = { txt : string } +type token_XADD = { txt : string; sz : x86Suffix } +type token_XCHG = { txt : string; sz : x86Suffix } + diff --git a/old/x86/gen/tokens.hgen b/old/x86/gen/tokens.hgen new file mode 100644 index 00000000..7aa5256f --- /dev/null +++ b/old/x86/gen/tokens.hgen @@ -0,0 +1,28 @@ +%token <X86HGenBase.token_BINOP> BINOP +%token <X86HGenBase.token_BITOP> BITOP +%token <X86HGenBase.token_CALL> CALL +%token <X86HGenBase.token_CLC> CLC +%token <X86HGenBase.token_CMC> CMC +%token <X86HGenBase.token_CMPXCHG> CMPXCHG +%token <X86HGenBase.token_DIV> DIV +%token <X86HGenBase.token_JCC> JCC +%token <X86HGenBase.token_JMP> JMP +%token <X86HGenBase.token_LEA> LEA +%token <X86HGenBase.token_LEAVE> LEAVE +%token <X86HGenBase.token_LOOP> LOOP +%token <X86HGenBase.token_MFENCE> MFENCE +%token <X86HGenBase.token_MONOP> MONOP +%token <X86HGenBase.token_CMOV> CMOV +%token <X86HGenBase.token_MOV> MOV +%token <X86HGenBase.token_MOVABS> MOVABS +%token <X86HGenBase.token_MOVSX> MOVSX +%token <X86HGenBase.token_MOVZX> MOVZX +%token <X86HGenBase.token_MUL> MUL +%token <X86HGenBase.token_NOP> NOP +%token <X86HGenBase.token_POP> POP +%token <X86HGenBase.token_PUSH> PUSH +%token <X86HGenBase.token_RET> RET +%token <X86HGenBase.token_SET> SET +%token <X86HGenBase.token_STC> STC +%token <X86HGenBase.token_XADD> XADD +%token <X86HGenBase.token_XCHG> XCHG diff --git a/old/x86/gen/trans_sail.hgen b/old/x86/gen/trans_sail.hgen new file mode 100644 index 00000000..0fdfc803 --- /dev/null +++ b/old/x86/gen/trans_sail.hgen @@ -0,0 +1,28 @@ +(*| `X86BINOP(binop, sz, dest_src) -> ("Binop", [translate_binop binop; translate_size sz; translate_dest_src dest_src], []) +| `X86CALL (imm_rm) -> ("CALL", [translate_imm_rm imm_rm], []) +| `X86CLC -> ("CLC", [], []) +| `X86CMC -> ("CMC", [], []) +| `X86CMPXCHG (sz, rm , reg) -> ("CMPXCHG", [translate_size sz; translate_rm rm; translate_reg reg], []) +| `X86DIV (sz, rm) -> ("DIV", [translate_size sz; translate_rm rm], []) +| `X86StopFetching -> ("HLT", [], []) +| `X86JCC (cond, imm64) -> ("Jcc", [translate_cond cond; translate_imm64 imm64], []) +| `X86JMP (rm) -> ("JMP", [translate_rm rm], []) +| `X86LEA (sz, dest_src) -> ("LEA", [translate_size sz; translate_dest_src dest_src], []) +| `X86LEAVE -> ("LEAVE", [], []) +| `X86LOOP (cond, imm64) -> ("LOOP", [translate_cond cond; translate_imm64 imm64], []) +| `X86MFENCE -> ("MFENCE", [], []) +| `X86MONOP (monop, sz, rm) -> ("Monop", [translate_monop monop; translate_size sz; translate_rm rm], []) +| `X86MOV (cond, sz, dest_src) -> ("MOV", [translate_cond cond; translate_size sz; translate_dest_src dest_src], []) +| `X86MOVSX (sz1, dest_src, sz2) -> ("MOVSX", [translate_size sz1; translate_dest_src dest_src; translate_size sz2], []) +| `X86MOVZX (sz1, dest_src, sz2) -> ("MOVZX", [translate_size sz1; translate_dest_src dest_src; translate_size sz2], []) +| `X86MUL (sz, rm) -> ("MUL", [translate_size sz; translate_rm rm], []) +| `X86NOP -> ("NOP", [Nat_big_num.of_int 0], []) +| `X86POP (rm) -> ("POP", [translate_rm rm], []) +| `X86PUSH (imm_rm) -> ("PUSH", [translate_imm_rm imm_rm], []) +| `X86RET (imm64) -> ("RET", [translate_imm64 imm64], []) +| `X86SET (cond, b, rm) -> ("SET", [translate_cond cond; translate_bool b; translate_rm rm], []) +| `X86STC -> ("STC", [], []) +| `X86XADD (sz, rm, reg) -> ("XADD", [translate_size sz; translate_rm rm; translate_reg reg], []) +| `X86XCHG (sz, rm, reg) -> ("XCHG", [translate_size sz; translate_rm rm; translate_reg reg], []) + +*)
\ No newline at end of file diff --git a/old/x86/gen/types.hgen b/old/x86/gen/types.hgen new file mode 100644 index 00000000..117f0f4d --- /dev/null +++ b/old/x86/gen/types.hgen @@ -0,0 +1,134 @@ +type bit2 = int +type bit64 = Nat_big_num.num +let bit64_of_int = Nat_big_num.of_int +let bit64_to_int = Nat_big_num.to_int +let bit64_to_string = Nat_big_num.to_string +let eq_bit64 = Nat_big_num.equal + +type x86Binop = +| X86ADD +| X86OR +| X86ADC +| X86SBB +| X86AND +| X86SUB +| X86XOR +| X86CMP +| X86ROL +| X86ROR +| X86RCL +| X86RCR +| X86SHL +| X86SHR +| X86TEST +| X86SAR + +let pp_x86Binop = function +| X86ADD -> "add" +| X86OR -> "or" +| X86ADC -> "adc" +| X86SBB -> "sbb" +| X86AND -> "and" +| X86SUB -> "sub" +| X86XOR -> "xor" +| X86CMP -> "cmp" +| X86ROL -> "rol" +| X86ROR -> "ror" +| X86RCL -> "rcl" +| X86RCR -> "rcr" +| X86SHL -> "shl" +| X86SHR -> "shr" +| X86TEST -> "test" +| X86SAR -> "sar" + +type x86Bitop = X86Bts | X86Btc | X86Btr + +let pp_x86Bitop = function +| X86Bts -> "bts" +| X86Btc -> "btc" +| X86Btr -> "btr" + +type x86Monop = +| X86DEC +| X86INC +| X86NOT +| X86NEG + +let pp_x86Monop = function +| X86DEC -> "dec" +| X86INC -> "inc" +| X86NOT -> "not" +| X86NEG -> "neg" + +type x86Cond = +| X86O +| X86NO +| X86B +| X86NB +| X86E +| X86NE +| X86NA +| X86A +| X86S +| X86NS +| X86P +| X86NP +| X86L +| X86NL +| X86NG +| X86G +| X86ALWAYS + +let pp_x86Cond = function +| X86O -> "o" +| X86NO -> "no" +| X86B -> "b" +| X86NB -> "nb" +| X86E -> "e" +| X86NE -> "ne" +| X86NA -> "na" +| X86A -> "a" +| X86S -> "s" +| X86NS -> "ns" +| X86P -> "p" +| X86NP -> "np" +| X86L -> "l" +| X86NL -> "nl" +| X86NG -> "ng" +| X86G -> "g" +| X86ALWAYS -> "" + +type x86Suffix = +| X86BYTE +| X86WORD +| X86LONG +| X86QUAD +| X86NONE + +let pp_x86Suffix = function +| X86BYTE -> "byte" +| X86WORD -> "word" +| X86LONG -> "long" +| X86QUAD -> "quad" +| X86NONE -> "" + +type x86Size = +| X86S8 of bool +| X86S16 +| X86S32 +| X86S64 + +let pp_x86Size = function +| X86S8(_) -> "b" +| X86S16 -> "w" +| X86S32 -> "l" +| X86S64 -> "q" + +let pp_locked l = if l then "lock " else "" + +let suffix_size = function +| X86BYTE -> X86S8 false +| X86WORD -> X86S16 +| X86LONG -> X86S32 +| X86QUAD -> X86S64 +| X86NONE -> X86S64 diff --git a/old/x86/gen/types_sail_trans_out.hgen b/old/x86/gen/types_sail_trans_out.hgen new file mode 100644 index 00000000..948db8fa --- /dev/null +++ b/old/x86/gen/types_sail_trans_out.hgen @@ -0,0 +1 @@ +(* *) diff --git a/old/x86/gen/types_trans_sail.hgen b/old/x86/gen/types_trans_sail.hgen new file mode 100644 index 00000000..f088db39 --- /dev/null +++ b/old/x86/gen/types_trans_sail.hgen @@ -0,0 +1,61 @@ +(*let translate_enum enum_values name value = + let rec bit_count n = + if n = 0 then 0 + else 1 + (bit_count (n lsr 1)) in + let rec find_index element = function + | h::tail -> if h = element then 0 else 1 + (find_index element tail) + | _ -> failwith "translate_enum could not find value" + in + let size = bit_count (List.length enum_values) in + let index = find_index value enum_values in + (name, Range0 (Some size), IInt.bit_list_of_integer size (Nat_big_num.of_int index)) + +let translate_binop = translate_enum [X86ADD ; X86OR ; X86ADC ; X86SBB ; X86AND ; X86SUB ; X86XOR ; X86CMP ; X86ROL ; X86ROR ; X86RCL ; X86RCR ; X86SHL ; X86SHR ; X86TEST; X86SAR] + +let translate_cond = translate_enum [X86O ; X86NO ; X86B ; X86NB ; X86E ; X86NE ; X86NA ; X86A ; X86S ; X86NS ; X86P ; X86NP ; X86L ; X86NL ; X86NG ; X86G ; X86ALWAYS ] + +let translate_monop = translate_enum [X86DEC; X86INC; X86NOT; X86NEG] + +let translate_bool value = + ("bool", Bit, [if value then Bitc_one else Bitc_zero]) + +let translate_size = function + | X86S8(high) -> ("Sz8", [translate_bool high], []) + | X86S16 -> ("Sz16", [], []) + | X86S32 -> ("Sz32", [], []) + | X86S64 -> ("Sz64", [], []) + +let translate_bits bits value = + ("bits", Bvector (Some bits), IInt.bit_list_of_integer bits (Nat_big_num.of_int value)) + +let translate_bits_big bits value = + ("bits", Bvector (Some bits), IInt.bit_list_of_integer bits value) + +let translate_reg r = translate_bits 4 (reg_to_int r) + +let translate_scale s = translate_bits 2 s + +let translate_imm64 i = translate_bits_big 64 i + +let translate_msi = function + | Some (scale, reg) -> ("Some", [translate_scale scale; translate_reg reg], []) + | None -> ("None", [], []) + +let translate_base = function + | X86HGenBase.NoBase -> ("NoBase", [], []) + | X86HGenBase.RegBase(r) -> ("RegBase", [translate_reg r], []) + | X86HGenBase.RipBase -> ("RipBase", [], []) + +let translate_rm = function + | X86HGenBase.Reg (r) -> ("Reg", [translate_reg r], []) + | X86HGenBase.Mem (m_si, base, imm) -> ("Mem", [translate_msi m_si; translate_base base; translate_imm64 imm], []) + +let translate_dest_src = function + | X86HGenBase.R_rm (reg, rm) -> ("R_rm", [translate_reg reg; translate_rm rm], []) + | X86HGenBase.Rm_i (rm, imm64) -> ("Rm_i", [translate_rm rm; translate_imm64 imm64], []) + | X86HGenBase.Rm_r (rm, reg) -> ("Rm_r", [translate_rm rm; translate_reg reg], []) + +let translate_imm_rm = function + | X86HGenBase.Imm (imm) -> ("Imm", [translate_imm64 imm], []) + | X86HGenBase.Rm (rm) -> ("Rm", [translate_rm rm], []) + *) diff --git a/old/x86/x64.sail b/old/x86/x64.sail new file mode 100644 index 00000000..3549b123 --- /dev/null +++ b/old/x86/x64.sail @@ -0,0 +1,1610 @@ +(*========================================================================*) +(* *) +(* 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 Type 'a. ('a, list<'a>) -> bool effect pure ismember +val extern forall Type 'a. list<'a> -> nat effect pure listlength + +function (bit[8 ]) ASR8 ((bit[8 ]) v, ([|8 |]) shift) = let v2 = ((bit[16 ]) (EXTS(v))) in (bit[8 ]) (mask(v2 >> shift)) +function (bit[16]) ASR16 ((bit[16]) v, ([|16|]) shift) = let v2 = ((bit[32 ]) (EXTS(v))) in (bit[16]) (mask(v2 >> shift)) +function (bit[32]) ASR32 ((bit[32]) v, ([|32|]) shift) = let v2 = ((bit[64 ]) (EXTS(v))) in (bit[32]) (mask(v2 >> shift)) +function (bit[64]) ASR64 ((bit[64]) v, ([|64|]) shift) = let v2 = ((bit[128]) (EXTS(v))) in (bit[64]) (mask(v2 >> shift)) + +function (bit[8 ]) ROR8 ((bit[8 ]) v, ([|8 |]) shift) = let v2 = ((bit[16 ]) (v:v)) in (bit[8 ]) (mask(v2 >> shift)) +function (bit[16]) ROR16 ((bit[16]) v, ([|16|]) shift) = let v2 = ((bit[32 ]) (v:v)) in (bit[16]) (mask(v2 >> shift)) +function (bit[32]) ROR32 ((bit[32]) v, ([|32|]) shift) = let v2 = ((bit[64 ]) (v:v)) in (bit[32]) (mask(v2 >> shift)) +function (bit[64]) ROR64 ((bit[64]) v, ([|64|]) shift) = let v2 = ((bit[128]) (v:v)) in (bit[64]) (mask(v2 >> shift)) + +function (bit[8 ]) ROL8 ((bit[8 ]) v, ([|8 |]) shift) = let v2 = ((bit[16 ]) (v:v)) in (bit[8 ]) (mask(v2 << shift)) +function (bit[16]) ROL16 ((bit[16]) v, ([|16|]) shift) = let v2 = ((bit[32 ]) (v:v)) in (bit[16]) (mask(v2 << shift)) +function (bit[32]) ROL32 ((bit[32]) v, ([|32|]) shift) = let v2 = ((bit[64 ]) (v:v)) in (bit[32]) (mask(v2 << shift)) +function (bit[64]) ROL64 ((bit[64]) v, ([|64|]) shift) = let v2 = ((bit[128]) (v:v)) in (bit[64]) (mask(v2 << shift)) + +(*val cast bool -> bit effect pure cast_bool_bit +val cast bit -> int effect pure cast_bit_int *) +function forall Nat 'n, Nat 'm, Nat 'o, 'n <= 0, 'm <= 'o. ([|0:'o|]) negative_to_zero (([|'n:'m|]) x) = + if x < 0 then 0 else x + +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[1] CF +register bit[1] PF +register bit[1] AF +register bit[1] ZF +register bit[1] SF +register bit[1] OF + +(* -------------------------------------------------------------------------- + Memory + -------------------------------------------------------------------------- *) + +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 ((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); +} + +(* -------------------------------------------------------------------------- + Helper functions + -------------------------------------------------------------------------- *) + +(* Instruction addressing modes *) + +typedef wsize = const union { + bool Sz8; + unit Sz16; + unit Sz32; + unit Sz64; +} + +function ([|8:64|]) size_to_int((wsize) s) = + switch(s) { + case (Sz8(_)) -> 8 + case Sz16 -> 16 + case Sz32 -> 32 + case Sz64 -> 64 + } + +typedef base = const union { + unit NoBase; + unit RipBase; + regn RegBase; +} + +typedef scale_index = (bit[2],regn) + +typedef rm = const union { + regn X86_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 bit_offset = const union { + (rm, qword) Bit_rm_imm; + (rm, regn) Bit_rm_r; +} + +typedef monop_name = enumerate { X86_Dec; X86_Inc; X86_Not; X86_Neg } + +typedef binop_name = enumerate { + X86_Add; X86_Or; X86_Adc; X86_Sbb; X86_And; X86_Sub; X86_Xor; X86_Cmp; + X86_Rol; X86_Ror; X86_Rcl; X86_Rcr; X86_Shl; X86_Shr; X86_Test; X86_Sar; +} + +typedef bitop_name = enumerate { Bts; Btc; Btr } + +function binop_name opc_to_binop_name ((bit[4]) opc) = + switch opc + { + case 0x0 -> X86_Add + case 0x1 -> X86_Or + case 0x2 -> X86_Adc + case 0x3 -> X86_Sbb + case 0x4 -> X86_And + case 0x5 -> X86_Sub + case 0x6 -> X86_Xor + case 0x7 -> X86_Cmp + case 0x8 -> X86_Rol + case 0x9 -> X86_Ror + case 0xa -> X86_Rcl + case 0xb -> X86_Rcr + case 0xc -> X86_Shl + case 0xd -> X86_Shr + case 0xe -> X86_Test + case 0xf -> X86_Sar + } + +typedef cond = enumerate { + X86_O; X86_NO; X86_B; X86_NB; X86_E; X86_NE; X86_NA; X86_A; X86_S; + X86_NS; X86_P; X86_NP; X86_L; X86_NL; X86_NG; X86_G; X86_ALWAYS; +} + +function cond bv_to_cond ((bit[4]) v) = + switch v + { + case 0x0 -> X86_O + case 0x1 -> X86_NO + case 0x2 -> X86_B + case 0x3 -> X86_NB + case 0x4 -> X86_E + case 0x5 -> X86_NE + case 0x6 -> X86_NA + case 0x7 -> X86_A + case 0x8 -> X86_S + case 0x9 -> X86_NS + case 0xa -> X86_P + case 0xb -> X86_NP + case 0xc -> X86_L + case 0xd -> X86_NL + case 0xe -> X86_NG + case 0xf -> X86_G + } + +(* Effective addresses *) + +typedef ea = const union { + (wsize,qword) Ea_i; + (wsize,regn) Ea_r; + (wsize,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 ((wsize) sz, (rm) r) = + switch r { + case (X86_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 ((wsize) 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 ((wsize) 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 ((imm_rm) i_rm) = + switch i_rm { + case (Rm (v)) -> ea_rm (Sz64, v) + case (Imm (v)) -> Ea_i (Sz64, v) + } + +function qword restrict_size ((wsize) 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 ((bool) locked, (ea) e) = + switch e { + case (Ea_i(sz,i)) -> restrict_size(sz,i) + case (Ea_r((Sz8(have_rex)),r)) -> + if have_rex | r < 4 (* RSP *) | r > 7 (* RDI *) then + REG[r] + else + (REG[sub4 (r)] >> 8) & 0x00000000000000FF + case (Ea_r(sz,r)) -> restrict_size(sz, REG[r]) + 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 ((bool) locked, (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 + (REG[r])[7 .. 0] := w[7 .. 0] + else + (REG[sub4(r)])[15 .. 8] := (vector<15,8,dec,bit>) (w[7 .. 0]) + case (Ea_r(Sz16,r)) ->(REG[r])[15 .. 0] := w[15 .. 0] + 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(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 ((bool) locked, (wsize) sz, (dest_src) ds) = + let e = ea_dest (sz, ds) in + (e, EA(locked, e), EA(locked, 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)) -> rMEM(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)) -> a + } + +function unit jump_to_ea ((ea) e) = RIP := call_dest_from_ea(e) + +function (ea, nat) bit_offset_ea ((wsize) sz, (bit_offset) bo) = + let s = size_to_int (sz) in + switch bo { + case (Bit_rm_imm (r_m, imm)) -> + let base_ea = ea_rm (sz, r_m) in + switch (base_ea) { + case (Ea_r(_, r)) -> (Ea_r(sz, r), imm mod s) + case (Ea_m(_, a)) -> (Ea_m(sz, a), imm mod s) + } + case (Bit_rm_r (r_m, r)) -> + let base_ea = ea_rm (sz, r_m) in + let offset = REG[r] in + switch (base_ea) { + case (Ea_r(_, r)) -> (Ea_r(sz, r), offset mod s) + case (Ea_m(_, a)) -> (Ea_m(Sz64, a + (offset div 8)), offset mod 64) + } + } + +(* 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 ((wsize) sz) = + switch sz { + case (Sz8(_)) -> 8 + case Sz16 -> 16 + case Sz32 -> 32 + case Sz64 -> 64 + } + +function [|63|] size_width_sub1 ((wsize) sz) = + switch sz { + case (Sz8(_)) -> 7 + case Sz16 -> 15 + case Sz32 -> 31 + case Sz64 -> 63 + } + +(* XXXXX +function bit word_size_msb ((wsize) sz, (qword) w) = w[size_width(sz) - 1] +*) + +function bit word_size_msb ((wsize) sz, (qword) w) = w[size_width_sub1(sz)] + +function unit write_PF ((qword) w) = PF := byte_parity (w[7 .. 0]) + +function unit write_SF ((wsize) sz, (qword) w) = SF := word_size_msb (sz, w) + +function unit write_ZF ((wsize) 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 ((wsize) sz, (qword) w) = +{ + AF := undefined; + write_PF(w); + write_SF(sz, w); + write_ZF(sz, w); +} + +function unit write_arith_eflags ((wsize) sz, (qword) w, (bit) c, (bit) x) = +{ + CF := c; + OF := x; + write_arith_eflags_except_CF_OF (sz, w) +} + +function unit write_logical_eflags ((wsize) 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; +} + +function nat value_width ((wsize) sz) = 2 ** size_width(sz) + +function bit word_signed_overflow_add ((wsize) 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 ((wsize) 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 ((wsize) 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 ((wsize) sz, (qword) a, (qword) b) = + (a - b, (bit) (a < b), word_signed_overflow_sub (sz, a, b)) + +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 (locked, e) := w; +} + +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 (locked, e) := w; +} + +function unit write_logical_result ((bool) locked, (wsize) sz, (qword) w, (ea) e) = +{ + write_arith_eflags_except_CF_OF (sz, w); + wEA (locked, e) := w; +} + +function unit write_result_erase_eflags ((bool) locked, (qword) w, (ea) e) = +{ + erase_eflags (); + wEA (locked, e) := w; +} + +function qword effect { escape } sign_extension ((qword) w, (wsize) size1, (wsize) 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 ((wsize) sz, (qword) w) = + if sz == Sz64 then w[5 .. 0] else w[4 .. 0] + +function qword rol ((wsize) sz, (qword) a, (qword) b) = + switch sz { + case (Sz8(_)) -> EXTZ (ROL8 (a[7 .. 0], b[2 .. 0])) + case Sz16 -> EXTZ (ROL16 (a[15 .. 0], b[3 .. 0])) + case Sz32 -> EXTZ (ROL32 (a[31 .. 0], b[4 .. 0])) + case Sz64 -> ROL64 (a, b[5 .. 0]) + } + +function qword ror ((wsize) sz, (qword) a, (qword) b) = + switch sz { + case (Sz8(_)) -> EXTZ (ROR8 (a[7 .. 0], b[2 .. 0])) + case Sz16 -> EXTZ (ROR16 (a[15 .. 0], b[3 .. 0])) + case Sz32 -> EXTZ (ROR32 (a[31 .. 0], b[4 .. 0])) + case Sz64 -> ROR64 (a, b[5 .. 0]) + } + +function qword sar ((wsize) sz, (qword) a, (qword) b) = + switch sz { + case (Sz8(_)) -> EXTZ (ASR8 (a[7 .. 0], b[2 .. 0])) + case Sz16 -> EXTZ (ASR16 (a[15 .. 0], b[3 .. 0])) + case Sz32 -> EXTZ (ASR32 (a[31 .. 0], b[4 .. 0])) + case Sz64 -> ASR64 (a, b[5 .. 0]) + } + +function unit write_binop ((bool) locked, (wsize) sz, (binop_name) bop, (qword) a, (qword) b, (ea) e) = + switch bop { + case X86_Add -> let (w,c,x) = add_with_carry_out (sz, a, b) in + write_arith_result (locked, sz, w, c, x, e) + case X86_Sub -> let (w,c,x) = sub_with_borrow (sz, a, b) in + write_arith_result (locked, sz, w, c, x, e) + case X86_Cmp -> let (w,c,x) = sub_with_borrow (sz, a, b) in + write_arith_eflags (sz, w, c, x) + case X86_Test -> write_logical_eflags (sz, a & b) + case X86_And -> write_logical_result (locked, sz, a & b, e) (* XXX rmn30 wrong flags? *) + case X86_Xor -> write_logical_result (locked, sz, a ^ b, e) + case X86_Or -> write_logical_result (locked, sz, a | b, e) + case X86_Rol -> write_result_erase_eflags (locked, rol (sz, a, b), e) + case X86_Ror -> write_result_erase_eflags (locked, ror (sz, a, b), e) + case X86_Sar -> write_result_erase_eflags (locked, sar (sz, a, b), e) + case X86_Shl -> write_result_erase_eflags (locked, a << mask_shift (sz, b), e) + case X86_Shr -> write_result_erase_eflags (locked, a >> mask_shift (sz, b), e) + case X86_Adc -> + { + let carry = (bit) 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 (locked, sz, result, e); + } + } + case X86_Sbb -> + { + let carry = (bit) 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 (locked, sz, result, e); + } + } + case _ -> exit () + } + +function unit write_monop ((bool) locked, (wsize) sz, (monop_name) mop, (qword) a, (ea) e) = + switch mop { + case X86_Not -> wEA(locked, e) := ~(a) + case X86_Dec -> write_arith_result_no_CF_OF (locked, sz, a - 1, e) + case X86_Inc -> write_arith_result_no_CF_OF (locked, sz, a + 1, e)(* XXX rmn30 should set OF *) + case X86_Neg -> { write_arith_result_no_CF_OF (locked, sz, 0 - a, e); + CF := undefined; + } + } + +function bool read_cond ((cond) c) = + switch c { + case X86_A -> ~(CF) & ~(ZF) + case X86_NB -> ~(CF) + case X86_B -> CF + case X86_NA -> CF | (bit) ZF + case X86_E -> ZF + case X86_G -> ~(ZF) & (SF == OF) + case X86_NL -> SF == OF + case X86_L -> SF != OF + case X86_NG -> ZF | SF != OF + case X86_NE -> ~(ZF) + case X86_NO -> ~(OF) + case X86_NP -> ~(PF) + case X86_NS -> ~(SF) + case X86_O -> OF + case X86_P -> PF + case X86_S -> SF + case X86_ALWAYS -> true + } + +function qword pop_aux () = + let top = rMEM(RSP, 8) in + { + RSP := RSP + 8; + top; + } + +function unit push_aux ((qword) w) = +{ + RSP := RSP - 8; + wMEM(false, RSP, 8) := w; +} + +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 (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 + +(* -------------------------------------------------------------------------- + Instructions + -------------------------------------------------------------------------- *) + +scattered function unit execute +scattered typedef ast = const union + +val ast -> unit effect {escape, rmem, rreg, undef, eamem, wmv, wreg, barr} execute + +(* ========================================================================== + Binop + ========================================================================== *) + +union ast member (bool,binop_name,wsize,dest_src) Binop + +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) + +(* ========================================================================== + Bitop + ========================================================================== *) + +union ast member (bool,bitop_name,wsize,bit_offset) Bitop + +function clause execute (Bitop (locked,bop,sz,boffset)) = + let (base_ea, offset) = bit_offset_ea (sz, boffset) in { + word := EA(locked, base_ea); + bitval := word[offset]; + word[offset] := switch(bop) { + case Bts -> bitone + case Btc -> (~ (bitval)) + case Btr -> bitzero + }; + CF := bitval; + wEA(locked, base_ea) := word; + } + +(* ========================================================================== + CALL + ========================================================================== *) + +union ast member imm_rm CALL + +function clause execute (CALL (i)) = +{ + push_rip(); + jump_to_ea (ea_imm_rm (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 (bool, wsize,rm,regn) CMPXCHG + +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(locked, dst) in + let val_acc = EA(false, acc) in + { + write_binop (locked, sz, X86_Cmp, val_acc, val_dst, src); + if val_acc == val_dst then + wEA(locked, dst) := EA (false, src) + else { + wEA(false, acc) := val_dst; + (* write back the original value in dst so that we always + perform locked write after locked read *) + wEA(locked, dst) := val_dst; + } + } + +(* ========================================================================== + DIV + ========================================================================== *) + +union ast member (wsize,rm) X86_DIV + +function clause execute (X86_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(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(false, eax) := (qword) q; + wEA(false, edx) := (qword) m; + erase_eflags(); + } + +(* ========================================================================== + HLT -- halt instruction used to end test in RMEM + ========================================================================== *) + +union ast member unit HLT + +function clause execute (HLT) = () + + +(* ========================================================================== + 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 (false, ea_rm (Sz64, r)) + +(* ========================================================================== + LEA + ========================================================================== *) + +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(false, dst) := get_ea_address (src) + +(* ========================================================================== + LEAVE + ========================================================================== *) + +union ast member unit LEAVE + +function clause execute LEAVE = +{ + RSP := RBP; + pop (X86_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 (); +} + +(* ========================================================================== + MFENCE + ========================================================================== *) + +union ast member unit MFENCE + +function clause execute (MFENCE) = + X86_MFENCE () + +(* ========================================================================== + Monop + ========================================================================== *) + +union ast member (bool,monop_name,wsize,rm) Monop + +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 + ========================================================================== *) + +union ast member (cond,wsize,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(false, dst) := EA(false, src) + else () + +(* ========================================================================== + MOVSX + ========================================================================== *) + +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(false, dst) := sign_extension (EA(false, src), sz1, sz2) + +(* ========================================================================== + MOVZX + ========================================================================== *) + +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(false, dst) := EA(false, src) + +(* ========================================================================== + MUL + ========================================================================== *) + +union ast member (wsize,rm) X86_MUL + +function clause execute (X86_MUL (sz,r)) = + let eax = Ea_r (sz, 0) in (* RAX *) + let val_eax = EA(false, eax) in + let val_src = EA(false, ea_rm (sz, r)) in + switch sz { + 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(false, eax) := m[63 .. 0]; + wEA(false, edx) := (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(false, 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 (bool, wsize,rm,regn) XADD + +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(false, src) in + let val_dst = EA(locked, dst) in + { + wEA(false, src) := val_dst; + write_binop (locked, sz, X86_Add, val_src, val_dst, dst); + } + +(* ========================================================================== + XCHG + ========================================================================== *) + +union ast member (bool,wsize,rm,regn) XCHG + +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(false, src) in + let val_dst = EA(locked, dst) in + { + wEA(false, src) := val_dst; + wEA(locked, dst) := val_src; + } + +end ast +end execute + +(* -------------------------------------------------------------------------- + Decoding + -------------------------------------------------------------------------- *) +(* +function (qword,ostream) oimmediate8 ((ostream) strm) = + switch strm { + case (Some (b :: t)) -> ((qword) (EXTS(b)), Some (t)) + case _ -> ((qword) undefined, (ostream) None) + } + +function (qword,ostream) immediate8 ((byte_stream) strm) = + oimmediate8 (Some (strm)) + +function (qword,ostream) immediate16 ((byte_stream) strm) = + switch strm { + case b1 :: b2 :: t -> ((qword) (EXTS(b2 : b1)), Some (t)) + case _ -> ((qword) undefined, (ostream) None) + } + +function (qword,ostream) immediate32 ((byte_stream) strm) = + switch strm { + case b1 :: b2 :: b3 :: b4 :: t -> + ((qword) (EXTS(b4 : b3 : b2 : b1)), Some (t)) + case _ -> ((qword) undefined, (ostream) None) + } + +function (qword,ostream) immediate64 ((byte_stream) strm) = + switch strm { + case b1 :: b2 :: b3 :: b4 :: b5 :: b6 :: b7 :: b8 :: t -> + ((qword) (EXTS(b8 : b7 : b6 : b5 : b4 : b3 : b2 : b1)), Some (t)) + case _ -> ((qword) undefined, (ostream) None) + } + +function (qword, ostream) immediate ((wsize) sz, (byte_stream) strm) = + switch sz { + case (Sz8 (_)) -> immediate8 (strm) + case Sz16 -> immediate16 (strm) + case _ -> immediate32 (strm) + } + +function (qword, ostream) oimmediate ((wsize) sz, (ostream) strm) = + switch strm { + case (Some (s)) -> immediate (sz, s) + case None -> ((qword) undefined, (ostream) None) + } + +function (qword, ostream) full_immediate ((wsize) sz, (byte_stream) strm) = + if sz == Sz64 then immediate64 (strm) else immediate (sz, strm) + +(* - Parse ModR/M and SIB bytes --------------------------------------------- *) + +typedef REX = register bits [3 : 0] { + 3 : W; + 2 : R; + 1 : X; + 0 : B +} + +function regn rex_reg ((bit[1]) b, (bit[3]) r) = unsigned(b : r) + +function (qword, ostream) read_displacement ((bit[2]) Mod, (byte_stream) strm) = + if Mod == 0b01 + then immediate8 (strm) + else if Mod == 0b10 + then immediate32 (strm) + else (0x0000000000000000, (Some (strm))) + +function (qword, ostream) + read_sib_displacement ((bit[2]) Mod, (byte_stream) strm) = + if Mod == 0b01 then immediate8 (strm) else immediate32 (strm) + +function (rm, ostream) + read_SIB ((REX) rex, (bit[2]) Mod, (byte_stream) strm) = + switch strm { + case ((bit[2]) SS : (bit[3]) Index : (bit[3]) Base) :: strm1 -> + (let bbase = rex_reg (rex.B, Base) in + let index = rex_reg (rex.X, Index) in + let scaled_index = if index == 4 (* RSP *) then + (option<scale_index>) None + else let x = (scale_index) (SS, index) in + Some (x) in + (if bbase == 5 (* RBP *) + then let (displacement, strm2) = + read_sib_displacement (Mod, strm1) in + let bbase = if Mod == 0b00 then NoBase else RegBase (bbase) + in + (Mem (scaled_index, bbase, displacement), strm2) + else let (displacement, strm2) = read_displacement (Mod, strm1) in + (Mem (scaled_index, RegBase (bbase), displacement), strm2))) + case _ -> ((rm) undefined, (ostream) None) + } + +function (regn, rm, ostream) read_ModRM ((REX) rex, (byte_stream) strm) = + switch strm { + case (0b00 : (bit[3]) RegOpc : 0b101) :: strm1 -> + let (displacement, strm2) = immediate32 (strm1) in + (rex_reg (rex.R, RegOpc), Mem (None, RipBase, displacement), strm2) + case (0b11 : (bit[3]) REG : (bit[3]) RM) :: strm1 -> + (rex_reg (rex.R, REG), Reg (rex_reg (rex.B, RM)), Some (strm1)) + case ((bit[2]) Mod : (bit[3]) RegOpc : 0b100) :: strm1 -> + let (sib, strm2) = read_SIB (rex, Mod, strm1) in + (rex_reg (rex.R, RegOpc), sib, strm2) + case ((bit[2]) Mod : (bit[3]) RegOpc : (bit[3]) RM) :: strm1 -> + let (displacement, strm2) = read_displacement (Mod, strm1) in + (rex_reg (rex.R, RegOpc), + Mem (None, RegBase (rex_reg (rex.B, RM)), displacement), + strm2) + case _ -> ((regn) undefined, (rm) undefined, (ostream) None) + } + +function (bit[3], rm, ostream) + read_opcode_ModRM ((REX) rex, (byte_stream) strm) = + let (opcode, r, strm1) = read_ModRM (rex, strm) in + ((bit[3]) (cast_int_vec((int) opcode mod 8)), r, strm1) + +(* - Prefixes --------------------------------------------------------------- *) + +typedef prefix = [|5|] + +function prefix prefix_group ((byte) b) = + switch b { + case 0xf0 -> 1 + case 0xf2 -> 1 + case 0xf3 -> 1 + case 0x26 -> 2 + case 0x2e -> 2 + case 0x36 -> 2 + case 0x3e -> 2 + case 0x64 -> 2 + case 0x65 -> 2 + case 0x66 -> 3 + case 0x67 -> 4 + case _ -> if b[7 .. 4] == 0b0100 then 5 else 0 + } + +typedef atuple = (byte_stream, bool, REX, byte_stream) + +val (list<prefix>, byte_stream, byte_stream) -> option<atuple> effect {undef} read_prefix + +function rec option<atuple> read_prefix + ((list<prefix>) s, (byte_stream) p, (byte_stream) strm) = + switch strm { + case h :: strm1 -> + let group = prefix_group (h) in + if group == 0 then + let x = (p, false, (REX) 0b0000, strm) in Some (x) + else if group == 5 then + let x = (p, true, (REX) (h[3 .. 0]), strm1) in Some (x) + else if ismember (group, s) then + None + else + read_prefix (group :: s, h :: p, strm1) + case _ -> let x = (p, false, (REX) undefined, strm) in Some (x) + } + +function option<atuple> read_prefixes ((byte_stream) strm) = + read_prefix ([||||], [||||], strm) + +function wsize op_size ((bool) have_rex, (bit[1]) w, (bit[1]) v, (bool) override) = + if v == 1 then + Sz8 (have_rex) + else if w == 1 then + Sz64 + else if override then + Sz16 + else + Sz32 + +function bool is_mem ((rm) r) = + switch r {case (Mem (_, _, _)) -> true case _ -> false} + +(* - Decoder ---------------------------------------------------------------- *) + +function (ast, ostream) decode_aux + ((byte_stream) strm, (bool) have_rex, (REX) rex, (bool) op_size_override) = + switch strm + { + case (0b00 : (bit[3]) opc : 0b0 : (bit[1]) x : (bit[1]) v) :: strm2 -> + let (reg, r, strm3) = read_ModRM (rex, strm2) in + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let binop = opc_to_binop_name (EXTZ (opc)) in + let src_dst = if x == 0 then Rm_r (r, reg) else R_rm (reg, r) in + (Binop (binop, sz, src_dst), strm3) + case (0b00 : (bit[3]) opc : 0b10 : (bit[1]) v) :: strm2 -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let binop = opc_to_binop_name (EXTZ (opc)) in + let (imm, strm3) = immediate (sz, strm2) in + (Binop (binop, sz, Rm_i (Reg (0), imm)), strm3) + case (0x5 : (bit[1]) b : (bit[3]) r) :: strm2 -> + let reg = Reg (([|15|]) (rex.B : r)) in + (if b == 0b0 then PUSH (Rm (reg)) else POP (reg), Some (strm2)) + case 0x63 :: strm2 -> + let (reg, r, strm3) = read_ModRM (rex, strm2) in + (MOVSX (Sz32, R_rm (reg, r), Sz64), strm3) + case (0x6 : 0b10 : (bit[1]) b : 0b0) :: strm2 -> + let (imm, strm3) = if b == 1 then immediate8 (strm2) + else immediate32 (strm2) in + (PUSH (Imm (imm)), strm3) + case (0x7 : (bit[4]) c) :: strm2 -> + let (imm, strm3) = immediate8 (strm2) in + (Jcc (bv_to_cond (c), imm), strm3) + case (0x8 : 0b000 : (bit[1]) v) :: strm2 -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let (opc, r, strm3) = read_opcode_ModRM (rex, strm2) in + let (imm, strm4) = oimmediate (sz, strm3) in + let binop = opc_to_binop_name (EXTZ (opc)) in + (Binop (binop, sz, Rm_i (r, imm)), strm4) + case 0x83 :: strm2 -> + let sz = op_size (have_rex, rex.W, 1, op_size_override) in + let (opc, r, strm3) = read_opcode_ModRM (rex, strm2) in + let (imm, strm4) = oimmediate (sz, strm3) in + let binop = opc_to_binop_name (EXTZ (opc)) in + (Binop (binop, sz, Rm_i (r, imm)), strm4) + case (0x8 : 0b010 : (bit[1]) v) :: strm2 -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let (reg, r, strm3) = read_ModRM (rex, strm2) in + (Binop (Test, sz, Rm_r (r, reg)), strm3) + case (0x8 : 0b011 : (bit[1]) v) :: strm2 -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let (reg, r, strm3) = read_ModRM (rex, strm2) in + (XCHG (sz, r, reg), strm3) + case (0x8 : 0b10 : (bit[1]) x : (bit[1]) v) :: strm2 -> + let (reg, r, strm3) = read_ModRM (rex, strm2) in + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let src_dst = if x == 0 then Rm_r (r, reg) else R_rm (reg, r) in + (MOV (ALWAYS, sz, src_dst), strm3) + case 0x8d :: strm2 -> + let sz = op_size (true, rex.W, 1, op_size_override) in + let (reg, r, strm3) = read_ModRM (rex, strm2) in + if is_mem (r) then (LEA (sz, R_rm (reg, r)), strm3) else exit () + case 0x8f :: strm2 -> + let (opc, r, strm3) = read_opcode_ModRM (rex, strm2) in + if opc == 0 then (POP (r), strm3) else exit () + case (0x9 : 0b0 : (bit[3]) r) :: strm2 -> + let sz = op_size (true, rex.W, 1, op_size_override) in + let reg = rex_reg (rex.B, r) in + if reg == 0 then + (NOP (listlength (strm)), Some (strm2)) + else + (XCHG (sz, Reg (0), reg), Some (strm2)) + case (0xa : 0b100 : (bit[1]) v) :: strm2 -> + let sz = op_size (true, rex.W, v, op_size_override) in + let (imm, strm3) = immediate (sz, strm2) in + (Binop (Test, sz, Rm_i (Reg (0), imm)), strm3) + case (0xb : (bit[1]) v : (bit[3]) r) :: strm2 -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let (imm, strm3) = full_immediate (sz, strm2) in + let reg = rex_reg (rex.B, r) in + (MOV (ALWAYS, sz, Rm_i (Reg (reg), imm)), strm3) + case (0xc : 0b000 : (bit[1]) v) :: strm2 -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let (opc, r, strm3) = read_opcode_ModRM (rex, strm2) in + let (imm, strm4) = oimmediate8 (strm3) in + let binop = opc_to_binop_name (0b1 : opc) in + if opc == 0b110 then exit () + else (Binop (binop, sz, Rm_i (r, imm)), strm4) + case (0xc : 0b001 : (bit[1]) v) :: strm2 -> + if v == 0 then + let (imm, strm3) = immediate16 (strm2) in (RET (imm), strm3) + else + (RET (0), Some (strm2)) + case (0xc : 0b011 : (bit[1]) v) :: strm2 -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let (opc, r, strm3) = read_opcode_ModRM (rex, strm2) in + let (imm, strm4) = oimmediate (sz, strm3) in + if opc == 0 then (MOV (ALWAYS, sz, Rm_i (r, imm)), strm4) + else exit () + case 0xc9 :: strm2 -> + (LEAVE, Some (strm2)) + case (0xd : 0b00 : (bit[1]) b : (bit[1]) v) :: strm2 -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let (opc, r, strm3) = read_opcode_ModRM (rex, strm2) in + let shift = if b == 0 then Rm_i (r, 1) else Rm_r (r, 1) in + let binop = opc_to_binop_name (0b1 : opc) in + if opc == 0b110 then exit () + else (Binop (binop, sz, shift), strm3) + case (0xe : 0b000 : (bit[1]) b) :: strm2 -> + let (imm, strm3) = immediate8 (strm2) in + let cnd = if b == 0 then NE else E in + (LOOP (cnd, imm), strm3) + case 0xe2 :: strm2 -> + let (imm, strm3) = immediate8 (strm2) in + (LOOP (ALWAYS, imm), strm3) + case 0xe8 :: strm2 -> + let (imm, strm3) = immediate32 (strm2) in + (CALL (Imm (imm)), strm3) + case (0xe : 0b10 : (bit[1]) b : 0b1) :: strm2 -> + let (imm, strm3) = if b == 0 then immediate32 (strm2) + else immediate8 (strm2) in + (Jcc (ALWAYS, imm), strm3) + case 0xf5 :: strm2 -> (CMC, Some (strm2)) + case 0xf8 :: strm2 -> (CLC, Some (strm2)) + case 0xf9 :: strm2 -> (STC, Some (strm2)) + case (0xf : 0b011 : (bit[1]) v) :: strm2 -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let (opc, r, strm3) = read_opcode_ModRM (rex, strm2) in + switch opc { + case 0b000 -> let (imm, strm4) = oimmediate (sz, strm3) in + (Binop (Test, sz, Rm_i (r, imm)), strm4) + case 0b010 -> (Monop (Not, sz, r), strm3) + case 0b011 -> (Monop (Neg, sz, r), strm3) + case 0b100 -> (MUL (sz, r), strm3) + case 0b110 -> (DIV (sz, r), strm3) + case _ -> exit () + } + case 0xfe :: strm2 -> + let (opc, r, strm3) = read_opcode_ModRM (rex, strm2) in + switch opc { + case 0b000 -> (Monop (Inc, Sz8 (have_rex), r), strm3) + case 0b001 -> (Monop (Dec, Sz8 (have_rex), r), strm3) + case _ -> exit () + } + case 0xff :: strm2 -> + let sz = op_size (have_rex, rex.W, 1, op_size_override) in + let (opc, r, strm3) = read_opcode_ModRM (rex, strm2) in + switch opc { + case 0b000 -> (Monop (Inc, sz, r), strm3) + case 0b001 -> (Monop (Dec, sz, r), strm3) + case 0b010 -> (CALL (Rm (r)), strm3) + case 0b100 -> (JMP (r), strm3) + case 0b110 -> (PUSH (Rm (r)), strm3) + case _ -> exit () + } + case 0x0f :: opc :: strm2 -> + switch opc { + case 0x1f -> + let (opc, r, strm3) = read_opcode_ModRM (rex, strm2) in + (NOP (listlength (strm)), strm3) + case (0x4 : (bit[4]) c) -> + let sz = op_size (true, rex.W, 1, op_size_override) in + let (reg, r, strm3) = read_ModRM (rex, strm2) in + (MOV (bv_to_cond (c), sz, R_rm (reg, r)), strm3) + case (0x8 : (bit[4]) c) -> + let (imm, strm3) = immediate32 (strm2) in + (Jcc (bv_to_cond (c), imm), strm3) + case (0x9 : (bit[4]) c) -> + let (reg, r, strm3) = read_ModRM (rex, strm2) in + (SET (bv_to_cond (c), have_rex, r), strm3) + case (0xb : 0b000 : (bit[1]) v) -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let (reg, r, strm3) = read_ModRM (rex, strm2) in + (CMPXCHG (sz, r, reg), strm3) + case (0xc : 0b000 : (bit[1]) v) -> + let sz = op_size (have_rex, rex.W, v, op_size_override) in + let (reg, r, strm3) = read_ModRM (rex, strm2) in + (XADD (sz, r, reg), strm3) + case (0xb : (bit[1]) s : 0b11 : (bit[1]) v) -> + let sz2 = op_size (have_rex, rex.W, 1, op_size_override) in + let sz = if v == 1 then Sz16 else Sz8 (have_rex) in + let (reg, r, strm3) = read_ModRM (rex, strm2) in + if s == 1 then + (MOVSX (sz, R_rm (reg, r), sz2), strm3) + else + (MOVZX (sz, R_rm (reg, r), sz2), strm3) + case _ -> exit () + } + case _ -> exit () + } + +function (byte_stream, ast, nat) decode ((byte_stream) strm) = + switch read_prefixes (strm) + { + case None -> exit () + case (Some (prefixes, have_rex, rex, strm1)) -> + let op_size_override = ismember (0x66, prefixes) in + if rex.W == 1 & op_size_override | ismember (0x67, prefixes) then + exit () + else + switch decode_aux (strm1, have_rex, rex, op_size_override) { + case (instr, (Some (strm2))) -> (prefixes, instr, listlength (strm2)) + case _ -> exit () + } + } + *) + +let (vector <0, 16, inc, string >) GPRstr = + ["RAX","RCX","RDX","RBX","RSP","RBP","RSI","RDI","R8","R9","R10","R11","R12","R13","R14","R15"] + +function (regfps) regfp_base ((base) b) = + switch b { + case NoBase -> [|| ||] + case RipBase -> [|| RFull("RIP") ||] + case (RegBase(b)) -> [|| RFull(GPRstr[b]) ||] + } + +function (regfps) regfp_idx ((option<scale_index>) idx) = + switch idx { + case (None) -> [|| ||] + case (Some(scale, idx)) -> [|| RFull(GPRstr[idx]) ||] + } + +function (bool, regfps, regfps) regfp_rm ((rm) r) = + switch r { + case (X86_Reg(n)) -> + (false, [|| RFull(GPRstr[n]) ||], [|| ||]) + case (Mem(idx, b, d)) -> { + (true, [|| ||], append(regfp_idx(idx), regfp_base(b))) + } + } + +function (instruction_kind, regfps, regfps, regfps) regfp_dest_src ((dest_src) ds) = + switch ds { + case (Rm_i (r_m, i)) -> + let (m,rd,ars) = regfp_rm(r_m) in + (if m then IK_mem_write(Write_plain) else IK_simple, ars, rd, ars) + case (Rm_r (r_m, r)) -> + let (m,rd,ars) = regfp_rm(r_m) in + (if m then IK_mem_write(Write_plain) else IK_simple, RFull(GPRstr[r]) :: ars, rd, ars) + case (R_rm (r, r_m)) -> + let (m,rs,ars) = regfp_rm(r_m) in + (if m then IK_mem_read(Read_plain) else IK_simple, append(rs, ars), [|| RFull(GPRstr[r]) ||], ars) + } + +(* as above but where destination is also a source operand *) +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(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(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 + (if m then IK_mem_read(Read_plain) else IK_simple, append(rds, ars), rds, ars) + } + +function (bool, regfps, regfps) regfp_imm_rm ((imm_rm) i_rm) = + switch i_rm { + case (Rm (v)) -> regfp_rm (v) + case (Imm (v)) -> (false, [|| ||], [|| ||]) + } + +let all_flags_but_cf_of = [|| RFull("AF"), RFull("PF"), RFull("SF"), RFull("ZF") ||] +let all_flags = append([|| RFull("CF"), RFull("OF") ||], all_flags_but_cf_of) + +function (regfps) regfp_binop_flags ((binop_name) op) = + switch (op) { + case X86_Add -> all_flags + case X86_Sub -> all_flags + case X86_Cmp -> all_flags + case X86_Test -> all_flags_but_cf_of + case X86_And -> all_flags_but_cf_of + case X86_Xor -> all_flags_but_cf_of + case X86_Or -> all_flags_but_cf_of + case X86_Rol -> all_flags + case X86_Ror -> all_flags + case X86_Sar -> all_flags + case X86_Shl -> all_flags + case X86_Shr -> all_flags + case X86_Adc -> all_flags + case X86_Sbb -> all_flags + } +function (regfps) regfp_cond ((cond) c) = + switch c { + case X86_A -> [|| RFull("CF"), RFull("ZF") ||] + case X86_NB -> [|| RFull("CF") ||] + case X86_B -> [|| RFull("CF") ||] + case X86_NA -> [|| RFull("CF"), RFull("ZF") ||] + case X86_E -> [|| RFull("ZF") ||] + case X86_G -> [|| RFull("ZF"), RFull("SF"), RFull("OF") ||] + case X86_NL -> [|| RFull("SF"), RFull("OF") ||] + case X86_L -> [|| RFull("SF"), RFull("OF") ||] + case X86_NG -> [|| RFull("ZF"), RFull("SF"), RFull("OF") ||] + case X86_NE -> [|| RFull("ZF") ||] + case X86_NO -> [|| RFull("OF") ||] + case X86_NP -> [|| RFull("PF") ||] + case X86_NS -> [|| RFull("SF") ||] + case X86_O -> [|| RFull("OF") ||] + case X86_P -> [|| RFull("PF") ||] + case X86_S -> [|| RFull("SF") ||] + case X86_ALWAYS -> [|| ||] + } + +function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (instr) = { + iR := [|| ||]; + oR := [|| ||]; + aR := [|| ||]; + ik := IK_simple; + Nias := [|| NIAFP_successor ||]; + Dia := DIAFP_none; + switch instr { + case(Binop (locked, binop, sz, ds)) -> { + let flags = regfp_binop_flags (binop) 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)); + aR := append(aRs, aR); + } + } + case(Bitop (locked, bitop, sz, bitoff)) -> { + 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 (ik', iRs, oRs, aRs) = switch(bitoff) { + case (Bit_rm_imm (r_m, imm)) -> + let (m, rs, ars) = regfp_rm(r_m) in + (if m then IK_mem_rmw(rk, wk) else IK_simple, + append(rs, ars), rs, ars) + case (Bit_rm_r (r_m, r)) -> + let rfp = RFull(GPRstr[r]) in + let (m, rs, ars) = regfp_rm(r_m) in + (if m then IK_mem_rmw(rk, wk) else IK_simple, + rfp::append(rs, ars), rs, + if m then (rfp::ars) else ars) (* in memory case r is a third input to address! *) + } in { + ik := ik'; + iR := append(iRs, iR); + oR := RFull("CF")::append(oRs, oR); + aR := append(aRs, aR); + } + } + case(CALL (irm) ) -> + let (m, rs, ars) = regfp_imm_rm (irm) in { + ik := if m then IK_mem_rmw(Read_plain, Write_plain) else IK_mem_write(Write_plain); + iR := RFull("RIP") :: RFull("RSP") :: rs; + oR := RFull("RSP") :: oR; + aR := ars; + Nias := switch irm { + case (Rm (v)) -> NIAFP_indirect_address + case (Imm (v)) -> NIAFP_concrete_address(RIP + v) + } :: Nias; + } + case(CLC ) -> oR := RFull("CF") :: oR + case(CMC ) -> { + iR := RFull("CF") :: iR; + oR := RFull("CF") :: oR; + } + 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 (rk, wk) else IK_simple; + iR := RFull("RAX") :: RFull(GPRstr[reg]) :: append(rs, aRs); + oR := RFull("RAX") :: append(regfp_binop_flags(X86_Cmp), rs); + aR := aRs; + } + case(X86_DIV (sz, r_m) ) -> + let (m, rs, ars) = regfp_rm (r_m) in { + ik := if m then IK_mem_read (Read_plain) else IK_simple; + iR := RFull("RAX") :: RFull("RDX") :: append(rs, ars); + oR := RFull("RAX") :: RFull("RDX") :: append(oR, all_flags); + aR := ars; + } + case(HLT ) -> () + case(Jcc (c, imm64) ) -> + let flags = regfp_cond(c) in { + ik := IK_branch; + iR := RFull("RIP") :: flags; + Nias := NIAFP_concrete_address(RIP + imm64) :: Nias; + } + case(JMP (r_m) ) -> + let (m, rs, ars) = regfp_rm (r_m) in { + ik := if m then IK_mem_read(Read_plain) else IK_simple; + iR := RFull("RIP")::append(rs, ars); + aR := ars; + Nias := NIAFP_indirect_address :: Nias; + } + case(LEA (sz, ds) ) -> + let (_, irs, ors, ars) = regfp_dest_src (ds) in { + iR := irs; + oR := ors; + aR := ars; + } + case(LEAVE ) -> { + ik := IK_mem_read(Read_plain); + iR := RFull("RBP") :: iR; + oR := RFull("RBP") :: RFull("RSP") :: oR; + aR := RFull("RBP") :: aR; + } + case(LOOP (c, imm64) ) -> + let flags = regfp_cond(c) in { + ik := IK_branch; + iR := RFull("RCX") :: flags; + oR := RFull("RCX") :: oR; + Nias := NIAFP_concrete_address(RIP + imm64) :: Nias; + } + case(MFENCE ) -> + ik := IK_barrier (Barrier_x86_MFENCE) + 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(rk, wk) else IK_simple; + iR := append(rds, ars); + oR := append(all_flags_but_cf_of, rds); (* XXX fix flags *) + aR := ars; + } + case(MOV (c, sz, ds) ) -> + let (ik', irs, ors, ars) = regfp_dest_src (ds) in + let flags = regfp_cond(c) in + { + ik := ik'; + iR := append(irs, flags); + oR := ors; + aR := ars; + } + case(MOVSX (sz1, ds, sz2) ) -> + let (ik', irs, ors, ars) = regfp_dest_src (ds) in { + ik := ik'; + iR := irs; + oR := ors; + aR := ars; + } + case(MOVZX (sz1, ds, sz2) ) -> + let (ik', irs, ors, ars) = regfp_dest_src (ds) in { + ik := ik'; + iR := irs; + oR := ors; + aR := ars; + } + case(X86_MUL (sz, r_m) ) -> + let (m, rs, ars) = regfp_rm (r_m) in { + ik := if m then IK_mem_read (Read_plain) else IK_simple; + iR := RFull("RAX") :: append(rs, ars); + oR := RFull("RAX") :: RFull("RDX") :: append(oR, all_flags); + aR := ars; + } + case(NOP (_) ) -> () + case(POP (r_m) ) -> + let (m, rd, ars) = regfp_rm (r_m) in { + ik := if m then IK_mem_rmw(Read_plain, Write_plain) else IK_mem_write(Write_plain); + iR := RFull("RSP") :: ars; + oR := RFull("RSP") :: rd; + aR := RFull("RSP") :: ars; + } + case(PUSH (irm) ) -> + let (m, rs, ars) = regfp_imm_rm (irm) in { + ik := if m then IK_mem_rmw(Read_plain, Write_plain) else IK_mem_write(Write_plain); + iR := RFull("RSP") :: append(rs, ars); + oR := RFull("RSP") :: oR; + aR := RFull("RSP") :: ars; + } + case(RET (imm64) ) -> { + ik := IK_mem_read(Read_plain); + iR := RFull("RSP") :: iR; + oR := RFull("RSP") :: oR; + aR := RFull("RSP") :: aR; + Nias := NIAFP_indirect_address :: Nias; + } + case(SET (c, b, r_m) ) -> + let flags = regfp_cond(c) in + let (m, rs, ars) = regfp_rm(r_m) in { + ik := if m then IK_mem_write(Write_plain) else IK_simple; + iR := append(flags, ars); + oR := rs; + aR := ars; + } + case(STC ) -> oR := [|| RFull("CF") ||] + 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(rk, wk) else IK_simple; + iR := RFull(GPRstr[reg]) :: append(rs, ars); + oR := RFull(GPRstr[reg]) :: append(rs, all_flags); + aR := ars; + } + 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(rk, wk) else IK_simple; + iR := RFull(GPRstr[reg]) :: append(rs, ars); + oR := RFull(GPRstr[reg]) :: rs; + aR := ars; + } + }; + (iR,oR,aR,Nias,Dia,ik) +} diff --git a/old/x86/x86_extras.lem b/old/x86/x86_extras.lem new file mode 100644 index 00000000..d6498d87 --- /dev/null +++ b/old/x86/x86_extras.lem @@ -0,0 +1,53 @@ +open import Pervasives +open import Interp_ast +open import Interp_interface +open import Sail_impl_base +open import Interp_inter_imp +import Set_extra + +let memory_parameter_transformer mode v = + match v with + | Interp_ast.V_tuple [location;length] -> + let (v,loc_regs) = extern_with_track mode extern_vector_value location in + + match length with + | Interp_ast.V_lit (L_aux (L_num len) _) -> + (v,(natFromInteger len),loc_regs) + | Interp_ast.V_track (Interp_ast.V_lit (L_aux (L_num len) _)) size_regs -> + match loc_regs with + | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))) + | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))) + end + | _ -> Assert_extra.failwith "expected 'V_lit (L_aux (L_num _) _)' or 'V_track (V_lit (L_aux (L_num len) _)) _'" + end + | _ -> Assert_extra.failwith ("memory_parameter_transformer: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) + end + +let memory_parameter_transformer_option_address _mode v = + match v with + | Interp_ast.V_tuple [location;_] -> + Just (extern_vector_value location) + | _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) + end + +let x86_read_memory_functions : memory_reads = + [ ("rMEM", (MR Read_plain memory_parameter_transformer)); + ("rMEM_locked", (MR Read_X86_locked memory_parameter_transformer)); + ] + +let x86_memory_writes : memory_writes = + [] + +let x86_memory_eas : memory_write_eas = + [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); + ("MEMea_locked", (MEA Write_X86_locked memory_parameter_transformer)); + ] + +let x86_memory_vals : memory_write_vals = + [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); + ] + +let x86_barrier_functions = + [ + ("X86_MFENCE", Barrier_x86_MFENCE); + ] diff --git a/old/x86/x86_extras_embed.lem b/old/x86/x86_extras_embed.lem new file mode 100644 index 00000000..f5130995 --- /dev/null +++ b/old/x86/x86_extras_embed.lem @@ -0,0 +1,24 @@ +open import Pervasives +open import Pervasives_extra +open import Sail_impl_base +open import Sail_values +open import Prompt + +val rMEM : (vector bitU * integer) -> M (vector bitU) +val rMEM_locked : (vector bitU * integer) -> M (vector bitU) + +let rMEM (addr,size) = read_mem false Read_plain addr size +let rMEM_locked (addr,size) = read_mem false Read_X86_locked addr size + +val MEMea : (vector bitU * integer) -> M unit +val MEMea_locked : (vector bitU * integer) -> M unit + +let MEMea (addr,size) = write_mem_ea Write_plain addr size +let MEMea_locked (addr,size) = write_mem_ea Write_X86_locked addr size + +val MEMval : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU + +let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () + +let X86_MFENCE () = barrier Barrier_x86_MFENCE diff --git a/old/x86/x86_extras_embed_sequential.lem b/old/x86/x86_extras_embed_sequential.lem new file mode 100644 index 00000000..2703b6c4 --- /dev/null +++ b/old/x86/x86_extras_embed_sequential.lem @@ -0,0 +1,24 @@ +open import Pervasives +open import Pervasives_extra +open import Sail_impl_base +open import Sail_values +open import State + +val rMEM : (vector bitU * integer) -> M (vector bitU) +val rMEM_locked : (vector bitU * integer) -> M (vector bitU) + +let rMEM (addr,size) = read_mem false Read_plain addr size +let rMEM_locked (addr,size) = read_mem false Read_X86_locked addr size + +val MEMea : (vector bitU * integer) -> M unit +val MEMea_locked : (vector bitU * integer) -> M unit + +let MEMea (addr,size) = write_mem_ea Write_plain addr size +let MEMea_locked (addr,size) = write_mem_ea Write_X86_locked addr size + +val MEMval : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU + +let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () + +let X86_MFENCE () = barrier Barrier_x86_MFENCE |