Skip to content

Commit c51f8b3

Browse files
pennyannnpennyannn
committed
Add additional instructions required by AES-XTS on x86
1 parent 8324ae0 commit c51f8b3

File tree

4 files changed

+173
-15
lines changed

4 files changed

+173
-15
lines changed

‎x86/proofs/decode.ml

Lines changed: 46 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -293,6 +293,14 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
293293
let rm = simd_of_RM sz rm in
294294
let dest,src = if d then rm,reg else reg,rm in
295295
SOME (MOVUPS dest src, l)
296+
| [0x1e:8] ->
297+
read_byte l >>= \(b,l).
298+
(bitmatch b with
299+
| [0xfa:8] ->
300+
(match pfxs with
301+
| (F, RepZ) -> SOME (ENDBR64,l)
302+
| _ -> NONE)
303+
| _ -> NONE)
296304
| [0b0010100:7; d] ->
297305
let sz = Lower_128 in
298306
read_ModRM rex l >>= \((reg,rm),l).
@@ -334,14 +342,14 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
334342
read_imm Byte l >>= \(imm8,l).
335343
SOME (AESKEYGENASSIST (mmreg reg sz) (simd_of_RM sz rm) imm8, l)
336344
| _ -> NONE)
337-
| [0b11001:5; r:3] -> if has_pfxs pfxs then NONE else
338-
let sz = op_size_W rex T pfxs in
339-
let reg = rex_reg (rex_B rex) r in
340-
SOME (BSWAP (%(gpr_adjust reg sz)),l)
341345
| [0x4:4; c:4] -> if has_pfxs pfxs then NONE else
342346
let sz = op_size T (rex_W rex) T pfxs in
343347
read_ModRM_operand rex sz l >>= \((reg,rm),l).
344348
SOME (CMOV (decode_condition c) reg rm,l)
349+
| [0x57:8] -> if has_pfxs pfxs then NONE else
350+
let sz = Lower_128 in
351+
read_ModRM rex l >>= \((reg,rm),l).
352+
SOME (XORPS (mmreg reg sz) (simd_of_RM sz rm), l)
345353
| [0b011:3; d; 0b1111:4] ->
346354
let sz = Lower_128 in
347355
read_ModRM rex l >>= \((reg,rm),l).
@@ -352,6 +360,20 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
352360
| (T, Rep0) -> SOME (MOVDQA dest src, l)
353361
| (F, RepZ) -> SOME (MOVDQU dest src, l)
354362
| _ -> NONE)
363+
| [0x70:8] -> if has_unhandled_pfxs pfxs then NONE else
364+
let sz = Lower_128 in
365+
read_ModRM rex l >>= \((reg,rm),l).
366+
read_imm Byte l >>= \(imm8,l).
367+
SOME (PSHUFD (mmreg reg sz) (simd_of_RM sz rm) imm8, l)
368+
| [0x72:8] -> if has_unhandled_pfxs pfxs then NONE else
369+
let sz = Lower_128 in
370+
(read_ModRM rex l >>= \((reg,rm),l).
371+
match rm with
372+
| RM_reg _ -> if (word_zx reg):(3 word) = word 0b100 then
373+
(read_imm Byte l >>= \(imm8,l).
374+
SOME (PSRAD (simd_of_RM sz rm) imm8, l))
375+
else NONE
376+
| _ -> NONE)
355377
| [0x8:4; c:4] -> if has_pfxs pfxs then NONE else
356378
read_int32 l >>= \(imm,l).
357379
SOME (JUMP (decode_condition c) (Imm32 imm),l)
@@ -404,14 +426,26 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
404426
read_ModRM rex l >>= \((reg,rm),l).
405427
let op = if s then MOVSX else MOVZX in
406428
SOME (op (%(gpr_adjust reg sz2)) (operand_of_RM sz rm),l)
407-
| [0x1e:8] ->
408-
read_byte l >>= \(b,l).
409-
(bitmatch b with
410-
| [0xfa:8] ->
411-
(match pfxs with
412-
| (F, RepZ) -> SOME (ENDBR64,l)
413-
| _ -> NONE)
414-
| _ -> NONE)
429+
| [0b11001:5; r:3] -> if has_pfxs pfxs then NONE else
430+
let sz = op_size_W rex T pfxs in
431+
let reg = rex_reg (rex_B rex) r in
432+
SOME (BSWAP (%(gpr_adjust reg sz)),l)
433+
| [0xd4:8] -> if has_unhandled_pfxs pfxs then NONE else
434+
let sz = Lower_128 in
435+
read_ModRM rex l >>= \((reg,rm),l).
436+
SOME (PADDQ (mmreg reg sz) (simd_of_RM sz rm), l)
437+
| [0xdb:8] -> if has_unhandled_pfxs pfxs then NONE else
438+
let sz = Lower_128 in
439+
read_ModRM rex l >>= \((reg,rm),l).
440+
SOME (PAND (mmreg reg sz) (simd_of_RM sz rm), l)
441+
| [0xef:8] -> if has_unhandled_pfxs pfxs then NONE else
442+
let sz = Lower_128 in
443+
read_ModRM rex l >>= \((reg,rm),l).
444+
SOME (PXOR (mmreg reg sz) (simd_of_RM sz rm), l)
445+
| [0xfe:8] -> if has_unhandled_pfxs pfxs then NONE else
446+
let sz = Lower_128 in
447+
read_ModRM rex l >>= \((reg,rm),l).
448+
SOME (PADDD (mmreg reg sz) (simd_of_RM sz rm), l)
415449
| _ -> NONE)
416450
| [0b01010:5; r:3] -> if has_pfxs pfxs then NONE else
417451
SOME (PUSH (%(Gpr (rex_reg (rex_B rex) r) Full_64)),l)

‎x86/proofs/instruction.ml

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -278,8 +278,14 @@ let instruction_INDUCTION,instruction_RECURSION = define_type
278278
| NOP
279279
| NOT operand
280280
| OR operand operand
281+
| PADDD operand operand
282+
| PADDQ operand operand
283+
| PAND operand operand
281284
| POP operand
285+
| PSHUFD operand operand operand
286+
| PSRAD operand operand
282287
| PUSH operand
288+
| PXOR operand operand
283289
| RCL operand operand
284290
| RCR operand operand
285291
| RET
@@ -298,7 +304,8 @@ let instruction_INDUCTION,instruction_RECURSION = define_type
298304
| TZCNT operand operand
299305
| VPXOR operand operand operand
300306
| XCHG operand operand
301-
| XOR operand operand";;
307+
| XOR operand operand
308+
| XORPS operand operand";;
302309

303310
(* ------------------------------------------------------------------------- *)
304311
(* Some shorthands for addressing modes etc. *)

‎x86/proofs/simulator.ml

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -273,6 +273,20 @@ let iclasses = iclasses @
273273
[0x66; 0x0f; 0x3a; 0xdf; 0xc8; 0x01]; (*AESKEYGENASSIST (%_% xmm1) (%_% xmm0) (Imm8 (word 1)) *)
274274
[0x66; 0x0f; 0x3a; 0xdf; 0xf8; 0xff]; (*AESKEYGENASSIST (%_% xmm15) (%_% xmm0) (Imm8 (word 255)) *)
275275
[0x66; 0x0f; 0x3a; 0xdf; 0xdc; 0x19]; (*AESKEYGENASSIST (%_% xmm3) (%_% xmm12) (Imm8 (word 25)) *)
276+
[0x66; 0x0f; 0x70; 0xc9; 0x55]; (*PSHUFD (%_% xmm1) (%_% xmm1) (Imm8 (word 85)) *)
277+
[0x66; 0x44; 0x0f; 0x70; 0xca; 0x5f]; (*PSHUFD (%_% xmm9) (%_% xmm2) (Imm8 (word 95)) *)
278+
[0x66; 0x0f; 0xef; 0xd3]; (*PXOR (%_% xmm2) (%_% xmm3) *)
279+
[0x66; 0x41; 0x0f; 0xef; 0xff]; (*PXOR (%_% xmm7) (%_% xmm15) *)
280+
[0x66; 0x0f; 0xdb; 0xd3]; (*PAND (%_% xmm2) (%_% xmm3) *)
281+
[0x66; 0x41; 0x0f; 0xdb; 0xff]; (*PAND (%_% xmm7) (%_% xmm15) *)
282+
[0x0f; 0x57; 0xd3]; (*XORPS (%_% xmm2) (%_% xmm3) *)
283+
[0x41; 0x0f; 0x57; 0xff]; (*XORPS (%_% xmm7) (%_% xmm15) *)
284+
[0x66; 0x0f; 0xfe; 0xd3]; (*PADDD (%_% xmm2) (%_% xmm3) *)
285+
[0x66; 0x41; 0x0f; 0xfe; 0xff]; (*PADDD (%_% xmm7) (%_% xmm15) *)
286+
[0x66; 0x0f; 0xd4; 0xd3]; (*PADDQ (%_% xmm2) (%_% xmm3) *)
287+
[0x66; 0x41; 0x0f; 0xd4; 0xff]; (*PADDQ (%_% xmm7) (%_% xmm15) *)
288+
[0x66; 0x0f; 0x72; 0xe1; 0x1f]; (*PSRAD (%_% xmm1) (Imm8 (word 31)) *)
289+
[0x66; 0x41; 0x0f; 0x72; 0xe4; 0x38]; (*PSRAD (%_% xmm12) (Imm8 (word 56)) *)
276290
];;
277291

278292
(* ------------------------------------------------------------------------- *)

‎x86/proofs/x86.ml

Lines changed: 105 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -979,6 +979,46 @@ let x86_OR = new_definition
979979
OF := F ,,
980980
UNDEFINED_VALUES[AF]) s`;;
981981

982+
let x86_PADDD = new_definition
983+
`x86_PADDD dest src s =
984+
let x = read dest s in
985+
let y = read src s in
986+
let r0 = word_add
987+
((word_subword:(128 word->num#num->32 word)) x (0,32))
988+
((word_subword:(128 word->num#num->32 word)) y (0,32)) in
989+
let r1 = word_add
990+
((word_subword:(128 word->num#num->32 word)) x (32,32))
991+
((word_subword:(128 word->num#num->32 word)) y (32,32)) in
992+
let r2 = word_add
993+
((word_subword:(128 word->num#num->32 word)) x (64,32))
994+
((word_subword:(128 word->num#num->32 word)) y (64,32)) in
995+
let r3 = word_add
996+
((word_subword:(128 word->num#num->32 word)) x (96,32))
997+
((word_subword:(128 word->num#num->32 word)) y (96,32)) in
998+
let res = (word_join:(32 word->96 word->128 word)) r3
999+
((word_join:(32 word->64 word->96 word)) r2
1000+
((word_join:(32 word->32 word->64 word)) r1 r0)) in
1001+
(dest := res) s`;;
1002+
1003+
let x86_PADDQ = new_definition
1004+
`x86_PADDQ dest src s =
1005+
let x = read dest s in
1006+
let y = read src s in
1007+
let r0 = word_add
1008+
((word_subword:(128 word->num#num->64 word)) x (0,64))
1009+
((word_subword:(128 word->num#num->64 word)) y (0,64)) in
1010+
let r1 = word_add
1011+
((word_subword:(128 word->num#num->64 word)) x (64,64))
1012+
((word_subword:(128 word->num#num->64 word)) y (64,64)) in
1013+
let res = (word_join:(64 word->64 word->128 word)) r1 r0 in
1014+
(dest := res) s`;;
1015+
1016+
let x86_PAND = new_definition
1017+
`x86_PAND dest src s =
1018+
let x = read dest s in
1019+
let y = read src s in
1020+
(dest := word_and x y) s`;;
1021+
9821022
(*** Push and pop are a bit odd in several ways. First of all, there is ***)
9831023
(*** an implicit memory operand so this doesn't have quite the same ***)
9841024
(*** "shallowness": we refer to the memory component explicitly. And we ***)
@@ -1009,6 +1049,47 @@ let x86_PUSH = new_definition
10091049
(RSP := p' ,,
10101050
memory :> bytes(p',n) := x) s`;;
10111051

1052+
let x86_PSHUFD = new_definition
1053+
`x86_PSHUFD dest src imm8 s =
1054+
let src = read src s in
1055+
let od = read imm8 s in
1056+
let d0 = (word_subword:(128 word->num#num->32 word)) src
1057+
((val ((word_subword:(byte->num#num->2 word)) od (0,2)))*32,32) in
1058+
let d1 = (word_subword:(128 word->num#num->32 word)) src
1059+
((val ((word_subword:(byte->num#num->2 word)) od (2,2)))*32,32) in
1060+
let d2 = (word_subword:(128 word->num#num->32 word)) src
1061+
((val ((word_subword:(byte->num#num->2 word)) od (4,2)))*32,32) in
1062+
let d3 = (word_subword:(128 word->num#num->32 word)) src
1063+
((val ((word_subword:(byte->num#num->2 word)) od (6,2)))*32,32) in
1064+
let res = (word_join:(32 word->96 word->128 word)) d3
1065+
((word_join:(32 word->64 word->96 word)) d2
1066+
((word_join:(32 word->32 word->64 word)) d1 d0)) in
1067+
(dest := res) s`;;
1068+
1069+
let x86_PSRAD = new_definition
1070+
`x86_PSRAD dest imm8 s =
1071+
let d = read dest s in
1072+
let count_src = val (read imm8 s) in
1073+
let count = if count_src > 31 then 32 else count_src in
1074+
let r0 = word_ishr
1075+
((word_subword:(128 word->num#num->32 word)) d (0,32)) count in
1076+
let r1 = word_ishr
1077+
((word_subword:(128 word->num#num->32 word)) d (32,32)) count in
1078+
let r2 = word_ishr
1079+
((word_subword:(128 word->num#num->32 word)) d (64,32)) count in
1080+
let r3 = word_ishr
1081+
((word_subword:(128 word->num#num->32 word)) d (96,32)) count in
1082+
let res = (word_join:(32 word->96 word->128 word)) r3
1083+
((word_join:(32 word->64 word->96 word)) r2
1084+
((word_join:(32 word->32 word->64 word)) r1 r0)) in
1085+
(dest := res) s`;;
1086+
1087+
let x86_PXOR = new_definition
1088+
`x86_PXOR dest src s =
1089+
let x = read dest s in
1090+
let y = read src s in
1091+
(dest := word_xor x y) s`;;
1092+
10121093
(*** Out of alphabetical order as PUSH is a subroutine ***)
10131094

10141095
let x86_CALL = new_definition
@@ -1289,6 +1370,12 @@ let x86_XOR = new_definition
12891370
OF := F ,,
12901371
UNDEFINED_VALUES[AF]) s`;;
12911372

1373+
let x86_XORPS = new_definition
1374+
`x86_XORPS dest src s =
1375+
let x = read src s in
1376+
let y = read dest s in
1377+
(dest := word_xor x y) s`;;
1378+
12921379
(* ------------------------------------------------------------------------- *)
12931380
(* State components of various sizes corresponding to GPRs. *)
12941381
(* We also have a generic one "GPR" mapping to a number in all cases. *)
@@ -1765,14 +1852,26 @@ let x86_execute = define
17651852
| 32 -> x86_OR (OPERAND32 dest s) (OPERAND32 src s)
17661853
| 16 -> x86_OR (OPERAND16 dest s) (OPERAND16 src s)
17671854
| 8 -> x86_OR (OPERAND8 dest s) (OPERAND8 src s)) s
1855+
| PADDD dest src ->
1856+
x86_PADDD (OPERAND128_SSE dest s) (OPERAND128_SSE src s) s
1857+
| PADDQ dest src ->
1858+
x86_PADDQ (OPERAND128_SSE dest s) (OPERAND128_SSE src s) s
1859+
| PAND dest src ->
1860+
x86_PAND (OPERAND128_SSE dest s) (OPERAND128_SSE src s) s
17681861
| POP dest ->
17691862
(match operand_size dest with
17701863
64 -> x86_POP (OPERAND64 dest s)
17711864
| 16 -> x86_POP (OPERAND16 dest s)) s
1865+
| PSHUFD dest src imm8 ->
1866+
x86_PSHUFD (OPERAND128_SSE dest s) (OPERAND128_SSE src s) (OPERAND8 imm8 s) s
1867+
| PSRAD dest imm8 ->
1868+
x86_PSRAD (OPERAND128_SSE dest s) (OPERAND8 imm8 s) s
17721869
| PUSH src ->
17731870
(match operand_size src with
17741871
64 -> x86_PUSH (OPERAND64 src s)
17751872
| 16 -> x86_PUSH (OPERAND16 src s)) s
1873+
| PXOR dest src ->
1874+
x86_PXOR (OPERAND128_SSE dest s) (OPERAND128_SSE src s) s
17761875
| RCL dest src ->
17771876
(match operand_size dest with
17781877
64 -> x86_RCL (OPERAND64 dest s)
@@ -1910,6 +2009,8 @@ let x86_execute = define
19102009
| 32 -> x86_XOR (OPERAND32 dest s) (OPERAND32 src s)
19112010
| 16 -> x86_XOR (OPERAND16 dest s) (OPERAND16 src s)
19122011
| 8 -> x86_XOR (OPERAND8 dest s) (OPERAND8 src s)) s
2012+
| XORPS dest src ->
2013+
x86_XORPS (OPERAND128_SSE dest s) (OPERAND128_SSE src s) s
19132014
| _ -> (\s'. F)`;;
19142015

19152016
(* ------------------------------------------------------------------------- *)
@@ -2610,9 +2711,11 @@ let X86_OPERATION_CLAUSES =
26102711
x86_DIV2; x86_ENDBR64; x86_IMUL; x86_IMUL2; x86_IMUL3; x86_INC; x86_LEA; x86_LZCNT;
26112712
x86_MOV; x86_MOVAPS; x86_MOVDQA; x86_MOVDQU; x86_MOVSX; x86_MOVUPS; x86_MOVZX;
26122713
x86_MUL2; x86_MULX4; x86_NEG; x86_NOP; x86_NOT; x86_OR;
2613-
x86_POP_ALT; x86_PUSH_ALT; x86_RCL; x86_RCR; x86_RET; x86_ROL; x86_ROR;
2714+
x86_PADDD; x86_PADDQ; x86_PAND; x86_POP_ALT; x86_PSHUFD; x86_PSRAD;
2715+
x86_PUSH_ALT; x86_PXOR;
2716+
x86_RCL; x86_RCR; x86_RET; x86_ROL; x86_ROR;
26142717
x86_SAR; x86_SBB_ALT; x86_SET; x86_SHL; x86_SHLD; x86_SHR; x86_SHRD;
2615-
x86_STC; x86_SUB_ALT; x86_TEST; x86_TZCNT; x86_XCHG; x86_XOR;
2718+
x86_STC; x86_SUB_ALT; x86_TEST; x86_TZCNT; x86_XCHG; x86_XOR; x86_XORPS;
26162719
(*** AVX2 instructions ***)
26172720
x86_VPXOR;
26182721
(*** 32-bit backups since the ALT forms are 64-bit only ***)

0 commit comments

Comments
 (0)