diff --git a/x86/allowed_asm b/x86/allowed_asm index 0367a8fa..fd6fafe6 100644 --- a/x86/allowed_asm +++ b/x86/allowed_asm @@ -1,8 +1,3 @@ -: aesdec$ -: aesdeclast$ -: aesenc$ -: aesenclast$ -: aeskeygenassist$ : adc$ : adcl$ : adcq$ @@ -12,6 +7,11 @@ : addq$ : adox$ : adoxq$ +: aesdec$ +: aesdeclast$ +: aesenc$ +: aesenclast$ +: aeskeygenassist$ : and$ : andl$ : andq$ @@ -21,6 +21,12 @@ : bswapq$ : bt$ : btq$ +: btc$ +: btcq$ +: btr$ +: btrq$ +: bts$ +: btsq$ : call$ : callq$ : cmc$ @@ -47,15 +53,15 @@ : lea$ : leaq$ : mov$ +: movl$ +: movq$ +: movw$ : movabs$ : movabsq$ : movaps$ : movdqa$ : movdqu$ : movups$ -: movl$ -: movq$ -: movw$ : mul$ : mulq$ : mulx$ @@ -66,10 +72,16 @@ : notq$ : or$ : orq$ +: paddd$ +: paddq$ +: pand$ : pop$ : popq$ +: pshufd$ +: psrad$ : push$ : pushq$ +: pxor$ : rcr$ : ret$ : retq$ @@ -77,6 +89,22 @@ : sbb$ : sbbl$ : sbbq$ +: setb$ +: setbe$ +: setl$ +: setle$ +: setnb$ +: setnbe$ +: setnl$ +: setnle$ +: setno$ +: setnp$ +: setns$ +: setnz$ +: seto$ +: setp$ +: sets$ +: setz$ : shl$ : shld$ : shldq$ @@ -90,6 +118,7 @@ : subq$ : test$ : testq$ +: vpxor$ : xchg$ : xor$ : xorl$ diff --git a/x86/proofs/decode.ml b/x86/proofs/decode.ml index 0c5f529f..f9f61aa8 100644 --- a/x86/proofs/decode.ml +++ b/x86/proofs/decode.ml @@ -293,6 +293,18 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l = let rm = simd_of_RM sz rm in let dest,src = if d then rm,reg else reg,rm in SOME (MOVUPS dest src, l) + | [0x1e:8] -> + read_byte l >>= \(b,l). + (bitmatch b with + | [0xfa:8] -> + (match pfxs with + | (F, RepZ) -> SOME (ENDBR64,l) + | _ -> NONE) + | _ -> NONE) + | [0x1f:8] -> if has_unhandled_pfxs pfxs then NONE else + let sz = op_size_W rex T pfxs in + read_ModRM_operand rex sz l >>= \((_,rm),l). + SOME (NOP_N rm,l) | [0b0010100:7; d] -> if has_pfxs pfxs then NONE else let sz = Lower_128 in read_ModRM rex l >>= \((reg,rm),l). @@ -334,14 +346,14 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l = read_imm Byte l >>= \(imm8,l). SOME (AESKEYGENASSIST (mmreg reg sz) (simd_of_RM sz rm) imm8, l) | _ -> NONE) - | [0b11001:5; r:3] -> if has_pfxs pfxs then NONE else - let sz = op_size_W rex T pfxs in - let reg = rex_reg (rex_B rex) r in - SOME (BSWAP (%(gpr_adjust reg sz)),l) | [0x4:4; c:4] -> if has_pfxs pfxs then NONE else let sz = op_size T (rex_W rex) T pfxs in read_ModRM_operand rex sz l >>= \((reg,rm),l). SOME (CMOV (decode_condition c) reg rm,l) + | [0x66:8] -> if has_unhandled_pfxs pfxs then NONE else + let sz = Lower_128 in + read_ModRM rex l >>= \((reg,rm),l). + SOME (PCMPGTD (mmreg reg sz) (simd_of_RM sz rm), l) | [0b011:3; d; 0b1111:4] -> let sz = Lower_128 in read_ModRM rex l >>= \((reg,rm),l). @@ -352,6 +364,20 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l = | (T, Rep0) -> SOME (MOVDQA dest src, l) | (F, RepZ) -> SOME (MOVDQU dest src, l) | _ -> NONE) + | [0x70:8] -> if has_unhandled_pfxs pfxs then NONE else + let sz = Lower_128 in + read_ModRM rex l >>= \((reg,rm),l). + read_imm Byte l >>= \(imm8,l). + SOME (PSHUFD (mmreg reg sz) (simd_of_RM sz rm) imm8, l) + | [0x72:8] -> if has_unhandled_pfxs pfxs then NONE else + let sz = Lower_128 in + (read_ModRM rex l >>= \((reg,rm),l). + match rm with + | RM_reg _ -> if (word_zx reg):(3 word) = word 0b100 then + (read_imm Byte l >>= \(imm8,l). + SOME (PSRAD (simd_of_RM sz rm) imm8, l)) + else NONE + | _ -> NONE) | [0x8:4; c:4] -> if has_pfxs pfxs then NONE else read_int32 l >>= \(imm,l). SOME (JUMP (decode_condition c) (Imm32 imm),l) @@ -404,14 +430,26 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l = read_ModRM rex l >>= \((reg,rm),l). let op = if s then MOVSX else MOVZX in SOME (op (%(gpr_adjust reg sz2)) (operand_of_RM sz rm),l) - | [0x1e:8] -> - read_byte l >>= \(b,l). - (bitmatch b with - | [0xfa:8] -> - (match pfxs with - | (F, RepZ) -> SOME (ENDBR64,l) - | _ -> NONE) - | _ -> NONE) + | [0b11001:5; r:3] -> if has_pfxs pfxs then NONE else + let sz = op_size_W rex T pfxs in + let reg = rex_reg (rex_B rex) r in + SOME (BSWAP (%(gpr_adjust reg sz)),l) + | [0xd4:8] -> if has_unhandled_pfxs pfxs then NONE else + let sz = Lower_128 in + read_ModRM rex l >>= \((reg,rm),l). + SOME (PADDQ (mmreg reg sz) (simd_of_RM sz rm), l) + | [0xdb:8] -> if has_unhandled_pfxs pfxs then NONE else + let sz = Lower_128 in + read_ModRM rex l >>= \((reg,rm),l). + SOME (PAND (mmreg reg sz) (simd_of_RM sz rm), l) + | [0xef:8] -> if has_unhandled_pfxs pfxs then NONE else + let sz = Lower_128 in + read_ModRM rex l >>= \((reg,rm),l). + SOME (PXOR (mmreg reg sz) (simd_of_RM sz rm), l) + | [0xfe:8] -> if has_unhandled_pfxs pfxs then NONE else + let sz = Lower_128 in + read_ModRM rex l >>= \((reg,rm),l). + SOME (PADDD (mmreg reg sz) (simd_of_RM sz rm), l) | _ -> NONE) | [0b01010:5; r:3] -> if has_pfxs pfxs then NONE else SOME (PUSH (%(Gpr (rex_reg (rex_B rex) r) Full_64)),l) @@ -467,7 +505,7 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l = if opc = word 0 then SOME (POP rm,l) else NONE - | [0x90:8] -> if has_pfxs pfxs then NONE else + | [0x90:8] -> if has_unhandled_pfxs pfxs then NONE else SOME (NOP,l) | [0b1010100:7; v] -> if has_pfxs pfxs then NONE else let sz = op_size T (rex_W rex) v pfxs in diff --git a/x86/proofs/instruction.ml b/x86/proofs/instruction.ml index e4a3df55..068f22c4 100644 --- a/x86/proofs/instruction.ml +++ b/x86/proofs/instruction.ml @@ -237,10 +237,10 @@ let instruction_INDUCTION,instruction_RECURSION = define_type | ADCX operand operand | ADD operand operand | ADOX operand operand - | AESENC operand operand - | AESENCLAST operand operand | AESDEC operand operand | AESDECLAST operand operand + | AESENC operand operand + | AESENCLAST operand operand | AESKEYGENASSIST operand operand operand | AND operand operand | BSF operand operand @@ -276,10 +276,18 @@ let instruction_INDUCTION,instruction_RECURSION = define_type | MULX4 (operand#operand) (operand#operand) | NEG operand | NOP + | NOP_N operand | NOT operand | OR operand operand + | PADDD operand operand + | PADDQ operand operand + | PAND operand operand + | PCMPGTD operand operand | POP operand + | PSHUFD operand operand operand + | PSRAD operand operand | PUSH operand + | PXOR operand operand | RCL operand operand | RCR operand operand | RET diff --git a/x86/proofs/simulator.ml b/x86/proofs/simulator.ml index 18526bc5..392ac083 100755 --- a/x86/proofs/simulator.ml +++ b/x86/proofs/simulator.ml @@ -273,6 +273,23 @@ let iclasses = iclasses @ [0x66; 0x0f; 0x3a; 0xdf; 0xc8; 0x01]; (*AESKEYGENASSIST (%_% xmm1) (%_% xmm0) (Imm8 (word 1)) *) [0x66; 0x0f; 0x3a; 0xdf; 0xf8; 0xff]; (*AESKEYGENASSIST (%_% xmm15) (%_% xmm0) (Imm8 (word 255)) *) [0x66; 0x0f; 0x3a; 0xdf; 0xdc; 0x19]; (*AESKEYGENASSIST (%_% xmm3) (%_% xmm12) (Imm8 (word 25)) *) + [0x66; 0x0f; 0x70; 0xc9; 0x55]; (*PSHUFD (%_% xmm1) (%_% xmm1) (Imm8 (word 85)) *) + [0x66; 0x44; 0x0f; 0x70; 0xca; 0x5f]; (*PSHUFD (%_% xmm9) (%_% xmm2) (Imm8 (word 95)) *) + [0x66; 0x0f; 0xef; 0xd3]; (*PXOR (%_% xmm2) (%_% xmm3) *) + [0x66; 0x41; 0x0f; 0xef; 0xff]; (*PXOR (%_% xmm7) (%_% xmm15) *) + [0x66; 0x0f; 0xdb; 0xd3]; (*PAND (%_% xmm2) (%_% xmm3) *) + [0x66; 0x41; 0x0f; 0xdb; 0xff]; (*PAND (%_% xmm7) (%_% xmm15) *) + [0x66; 0x0f; 0xfe; 0xd3]; (*PADDD (%_% xmm2) (%_% xmm3) *) + [0x66; 0x41; 0x0f; 0xfe; 0xff]; (*PADDD (%_% xmm7) (%_% xmm15) *) + [0x66; 0x0f; 0xd4; 0xd3]; (*PADDQ (%_% xmm2) (%_% xmm3) *) + [0x66; 0x41; 0x0f; 0xd4; 0xff]; (*PADDQ (%_% xmm7) (%_% xmm15) *) + [0x66; 0x0f; 0x72; 0xe1; 0x1f]; (*PSRAD (%_% xmm1) (Imm8 (word 31)) *) + [0x66; 0x41; 0x0f; 0x72; 0xe4; 0x38]; (*PSRAD (%_% xmm12) (Imm8 (word 56)) *) + [0x66; 0x45; 0x0f; 0x66; 0xfe]; (*PCMPGTD (%_% xmm15) (%_% xmm14) *) + [0x66; 0x0f; 0x66; 0xcb]; (*PCMPGTD (%_% xmm1) (%_% xmm3) *) + [0x66; 0x90]; (* NOP *) + [0x0f; 0x1f; 0x4f; 0x00]; (* NOP_N (Memop Doubleword (%% (rdi,0))) *) + [0x66; 0x0f; 0x1f; 0x84; 0x00; 0x00; 0x01; 0x02; 0x03]; (* NOP_N (Memop Word (%%%% (rax,0,rax,&50462976))) *) ];; (* ------------------------------------------------------------------------- *) diff --git a/x86/proofs/x86.ml b/x86/proofs/x86.ml index eda07a82..e4580c9c 100644 --- a/x86/proofs/x86.ml +++ b/x86/proofs/x86.ml @@ -959,6 +959,13 @@ let x86_NEG = new_definition let x86_NOP = new_definition `x86_NOP (s:x86state) = \s'. s = s'`;; +(* + The multi-byte form of NOP is available on processors with model encoding: + CPUID.01H.EAX[Bytes 11:8] = 0110B or 1111B +*) +let x86_NOP_N = new_definition + `x86_NOP_N dest (s:x86state) = \s'. s = s'`;; + (*** In contrast to most logical ops, NOT doesn't affect any flags ***) let x86_NOT = new_definition @@ -979,6 +986,35 @@ let x86_OR = new_definition OF := F ,, UNDEFINED_VALUES[AF]) s`;; +let x86_PADDD = new_definition + `x86_PADDD dest src s = + let x = read dest s in + let y = read src s in + let res:(128)word = simd4 word_add x y in + (dest := res) s`;; + +let x86_PADDQ = new_definition + `x86_PADDQ dest src s = + let x = read dest s in + let y = read src s in + let res:(128)word = simd2 word_add x y in + (dest := res) s`;; + +let x86_PAND = new_definition + `x86_PAND dest src s = + let x = read dest s in + let y = read src s in + (dest := word_and x y) s`;; + +let x86_PCMPGTD = new_definition + `x86_PCMPGTD dest src s = + let x = read dest s in + let y = read src s in + let res:(128)word = simd4 (\(x:32 word) (y:32 word). + if word_igt x y then (word 0xffffffff) else (word 0)) + x y in + (dest := res) s`;; + (*** Push and pop are a bit odd in several ways. First of all, there is ***) (*** an implicit memory operand so this doesn't have quite the same ***) (*** "shallowness": we refer to the memory component explicitly. And we ***) @@ -1009,6 +1045,28 @@ let x86_PUSH = new_definition (RSP := p' ,, memory :> bytes(p',n) := x) s`;; +let x86_PSHUFD = new_definition + `x86_PSHUFD dest src imm8 s = + let src = read src s in + let od = read imm8 s in + let res:(128)word = usimd4 (\(od:(2)word). + word_subword src ((val od)*32,32)) od in + (dest := res) s`;; + +let x86_PSRAD = new_definition + `x86_PSRAD dest imm8 s = + let d = read dest s in + let count_src = val (read imm8 s) in + let count = if count_src > 31 then 32 else count_src in + let res:(128)word = usimd4 (\x. word_ishr x count) d in + (dest := res) s`;; + +let x86_PXOR = new_definition + `x86_PXOR dest src s = + let x = read dest s in + let y = read src s in + (dest := word_xor x y) s`;; + (*** Out of alphabetical order as PUSH is a subroutine ***) let x86_CALL = new_definition @@ -1678,11 +1736,6 @@ let x86_execute = define | 32 -> x86_INC (OPERAND32 dest s) | 16 -> x86_INC (OPERAND16 dest s) | 8 -> x86_INC (OPERAND8 dest s)) s - | LZCNT dest src -> - (match operand_size dest with - 64 -> x86_LZCNT (OPERAND64 dest s) (OPERAND64 src s) - | 32 -> x86_LZCNT (OPERAND32 dest s) (OPERAND32 src s) - | 16 -> x86_LZCNT (OPERAND16 dest s) (OPERAND16 src s)) s | JUMP cc off -> (RIP := if condition_semantics cc s @@ -1695,6 +1748,11 @@ let x86_execute = define | 32 -> (OPERAND32 dest s) := word_sx(bsid_semantics bsid s) | 16 -> (OPERAND16 dest s) := word_sx(bsid_semantics bsid s) | 8 -> (OPERAND8 dest s) := word_sx(bsid_semantics bsid s)) s + | LZCNT dest src -> + (match operand_size dest with + 64 -> x86_LZCNT (OPERAND64 dest s) (OPERAND64 src s) + | 32 -> x86_LZCNT (OPERAND32 dest s) (OPERAND32 src s) + | 16 -> x86_LZCNT (OPERAND16 dest s) (OPERAND16 src s)) s | MOV dest src -> (match operand_size dest with 64 -> x86_MOV (OPERAND64 dest s) (OPERAND64 src s) @@ -1753,6 +1811,10 @@ let x86_execute = define | 8 -> x86_NEG (OPERAND8 dest s)) s | NOP -> x86_NOP s + | NOP_N dest -> + (match operand_size dest with + 32 -> x86_NOP_N (OPERAND32 dest s) + | 16 -> x86_NOP_N (OPERAND16 dest s)) s | NOT dest -> (match operand_size dest with 64 -> x86_NOT (OPERAND64 dest s) @@ -1765,14 +1827,28 @@ let x86_execute = define | 32 -> x86_OR (OPERAND32 dest s) (OPERAND32 src s) | 16 -> x86_OR (OPERAND16 dest s) (OPERAND16 src s) | 8 -> x86_OR (OPERAND8 dest s) (OPERAND8 src s)) s + | PADDD dest src -> + x86_PADDD (OPERAND128_SSE dest s) (OPERAND128_SSE src s) s + | PADDQ dest src -> + x86_PADDQ (OPERAND128_SSE dest s) (OPERAND128_SSE src s) s + | PAND dest src -> + x86_PAND (OPERAND128_SSE dest s) (OPERAND128_SSE src s) s + | PCMPGTD dest src -> + x86_PCMPGTD (OPERAND128_SSE dest s) (OPERAND128_SSE src s) s | POP dest -> (match operand_size dest with 64 -> x86_POP (OPERAND64 dest s) | 16 -> x86_POP (OPERAND16 dest s)) s + | PSHUFD dest src imm8 -> + x86_PSHUFD (OPERAND128_SSE dest s) (OPERAND128_SSE src s) (OPERAND8 imm8 s) s + | PSRAD dest imm8 -> + x86_PSRAD (OPERAND128_SSE dest s) (OPERAND8 imm8 s) s | PUSH src -> (match operand_size src with 64 -> x86_PUSH (OPERAND64 src s) | 16 -> x86_PUSH (OPERAND16 src s)) s + | PXOR dest src -> + x86_PXOR (OPERAND128_SSE dest s) (OPERAND128_SSE src s) s | RCL dest src -> (match operand_size dest with 64 -> x86_RCL (OPERAND64 dest s) @@ -2064,6 +2140,8 @@ let OPERAND_SIZE_CASES = prove (match 16 with 64 -> a | 32 -> b | 16 -> c) = c /\ (match 64 with 64 -> a | 32 -> b) = a /\ (match 32 with 64 -> a | 32 -> b) = b /\ + (match 32 with 32 -> a | 16 -> b) = a /\ + (match 16 with 32 -> a | 16 -> b) = b /\ (match (64,32) with (64,32) -> a | (64,16) -> b | (64,8) -> c | (32,32) -> d | (32,16) -> e | (32,8) -> f | (16,8) -> g) = a /\ @@ -2600,6 +2678,22 @@ let x86_RET_POP_RIP = prove CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REWRITE_TAC[]);; +(*** Simplify word operations in SIMD instructions ***) + +let all_simd_rules = + [usimd16;usimd8;usimd4;usimd2;simd16;simd8;simd4;simd2];; + +let EXPAND_SIMD_RULE = + CONV_RULE (TOP_DEPTH_CONV WORD_SIMPLE_SUBWORD_CONV) o + CONV_RULE (DEPTH_CONV DIMINDEX_CONV) o REWRITE_RULE all_simd_rules;; + +let x86_PADDD_ALT = EXPAND_SIMD_RULE x86_PADDD;; +let x86_PADDQ_ALT = EXPAND_SIMD_RULE x86_PADDQ;; +let x86_PCMPGTD_ALT = EXPAND_SIMD_RULE x86_PCMPGTD;; +let x86_PSHUFD_ALT = EXPAND_SIMD_RULE x86_PSHUFD;; +let x86_PSRAD_ALT = EXPAND_SIMD_RULE x86_PSRAD;; + + let X86_OPERATION_CLAUSES = map (CONV_RULE(TOP_DEPTH_CONV let_CONV) o SPEC_ALL) [x86_ADC_ALT; x86_ADCX_ALT; x86_ADOX_ALT; x86_ADD_ALT; @@ -2609,8 +2703,10 @@ let X86_OPERATION_CLAUSES = x86_CALL_ALT; x86_CLC; x86_CMC; x86_CMOV; x86_CMP_ALT; x86_DEC; x86_DIV2; x86_ENDBR64; x86_IMUL; x86_IMUL2; x86_IMUL3; x86_INC; x86_LEA; x86_LZCNT; x86_MOV; x86_MOVAPS; x86_MOVDQA; x86_MOVDQU; x86_MOVSX; x86_MOVUPS; x86_MOVZX; - x86_MUL2; x86_MULX4; x86_NEG; x86_NOP; x86_NOT; x86_OR; - x86_POP_ALT; x86_PUSH_ALT; x86_RCL; x86_RCR; x86_RET; x86_ROL; x86_ROR; + x86_MUL2; x86_MULX4; x86_NEG; x86_NOP; x86_NOP_N; x86_NOT; x86_OR; + x86_PADDD_ALT; x86_PADDQ_ALT; x86_PAND; x86_PCMPGTD_ALT; x86_POP_ALT; + x86_PSHUFD_ALT; x86_PSRAD_ALT; x86_PUSH_ALT; x86_PXOR; + x86_RCL; x86_RCR; x86_RET; x86_ROL; x86_ROR; x86_SAR; x86_SBB_ALT; x86_SET; x86_SHL; x86_SHLD; x86_SHR; x86_SHRD; x86_STC; x86_SUB_ALT; x86_TEST; x86_TZCNT; x86_XCHG; x86_XOR; (*** AVX2 instructions ***)