Skip to content

Commit 22d7cc9

Browse files
pennyannnpennyannn
committed
Add additional instructions required by AES-XTS on x86
1 parent a47f1ba commit 22d7cc9

File tree

5 files changed

+266
-32
lines changed

5 files changed

+266
-32
lines changed

‎x86/allowed_asm

Lines changed: 33 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,3 @@
1-
: aesdec$
2-
: aesdeclast$
3-
: aesenc$
4-
: aesenclast$
5-
: aeskeygenassist$
61
: adc$
72
: adcl$
83
: adcq$
@@ -12,6 +7,11 @@
127
: addq$
138
: adox$
149
: adoxq$
10+
: aesdec$
11+
: aesdeclast$
12+
: aesenc$
13+
: aesenclast$
14+
: aeskeygenassist$
1515
: and$
1616
: andl$
1717
: andq$
@@ -21,8 +21,15 @@
2121
: bswapq$
2222
: bt$
2323
: btq$
24+
: btc$
25+
: btcq$
26+
: btr$
27+
: btrq$
28+
: bts$
29+
: btsq$
2430
: call$
2531
: callq$
32+
: clc$
2633
: cmc$
2734
: cmova$
2835
: cmovaq$
@@ -38,6 +45,7 @@
3845
: cmpq$
3946
: dec$
4047
: decq$
48+
: div$
4149
: endbr64$
4250
: imul$
4351
: imulq$
@@ -46,37 +54,50 @@
4654
: jmp$
4755
: lea$
4856
: leaq$
57+
: lzcnt$
58+
: lzcntq$
4959
: mov$
60+
: movl$
61+
: movq$
62+
: movw$
5063
: movabs$
5164
: movabsq$
5265
: movaps$
5366
: movdqa$
5467
: movdqu$
5568
: movups$
56-
: movl$
57-
: movq$
58-
: movw$
5969
: mul$
6070
: mulq$
6171
: mulx$
6272
: mulxq$
6373
: neg$
6474
: negq$
75+
: nop$
6576
: not$
6677
: notq$
6778
: or$
6879
: orq$
80+
: paddd$
81+
: paddq$
82+
: pand$
6983
: pop$
7084
: popq$
85+
: pshufd$
86+
: psrad$
7187
: push$
7288
: pushq$
89+
: pxor$
90+
: rcl$
7391
: rcr$
7492
: ret$
7593
: retq$
94+
: rol$
95+
: ror$
7696
: sar$
7797
: sbb$
7898
: sbbl$
7999
: sbbq$
100+
: set$
80101
: shl$
81102
: shld$
82103
: shldq$
@@ -90,8 +111,12 @@
90111
: subq$
91112
: test$
92113
: testq$
114+
: tzcnt$
115+
: tzcntq$
116+
: vpxor$
93117
: xchg$
94118
: xor$
95119
: xorl$
96120
: xorq$
121+
: xorps$
97122
: $

‎x86/proofs/decode.ml

Lines changed: 55 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -293,6 +293,18 @@ 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)
304+
| [0x1f:8] -> if has_unhandled_pfxs pfxs then NONE else
305+
let sz = op_size_W rex T pfxs in
306+
read_ModRM_operand rex sz l >>= \((_,rm),l).
307+
SOME (NOP_N rm,l)
296308
| [0b0010100:7; d] -> if has_pfxs pfxs then NONE else
297309
let sz = Lower_128 in
298310
read_ModRM rex l >>= \((reg,rm),l).
@@ -334,14 +346,18 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
334346
read_imm Byte l >>= \(imm8,l).
335347
SOME (AESKEYGENASSIST (mmreg reg sz) (simd_of_RM sz rm) imm8, l)
336348
| _ -> 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)
341349
| [0x4:4; c:4] -> if has_pfxs pfxs then NONE else
342350
let sz = op_size T (rex_W rex) T pfxs in
343351
read_ModRM_operand rex sz l >>= \((reg,rm),l).
344352
SOME (CMOV (decode_condition c) reg rm,l)
353+
| [0x57:8] -> if has_pfxs pfxs then NONE else
354+
let sz = Lower_128 in
355+
read_ModRM rex l >>= \((reg,rm),l).
356+
SOME (XORPS (mmreg reg sz) (simd_of_RM sz rm), l)
357+
| [0x66:8] -> if has_unhandled_pfxs pfxs then NONE else
358+
let sz = Lower_128 in
359+
read_ModRM rex l >>= \((reg,rm),l).
360+
SOME (PCMPGTD (mmreg reg sz) (simd_of_RM sz rm), l)
345361
| [0b011:3; d; 0b1111:4] ->
346362
let sz = Lower_128 in
347363
read_ModRM rex l >>= \((reg,rm),l).
@@ -352,6 +368,20 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
352368
| (T, Rep0) -> SOME (MOVDQA dest src, l)
353369
| (F, RepZ) -> SOME (MOVDQU dest src, l)
354370
| _ -> NONE)
371+
| [0x70:8] -> if has_unhandled_pfxs pfxs then NONE else
372+
let sz = Lower_128 in
373+
read_ModRM rex l >>= \((reg,rm),l).
374+
read_imm Byte l >>= \(imm8,l).
375+
SOME (PSHUFD (mmreg reg sz) (simd_of_RM sz rm) imm8, l)
376+
| [0x72:8] -> if has_unhandled_pfxs pfxs then NONE else
377+
let sz = Lower_128 in
378+
(read_ModRM rex l >>= \((reg,rm),l).
379+
match rm with
380+
| RM_reg _ -> if (word_zx reg):(3 word) = word 0b100 then
381+
(read_imm Byte l >>= \(imm8,l).
382+
SOME (PSRAD (simd_of_RM sz rm) imm8, l))
383+
else NONE
384+
| _ -> NONE)
355385
| [0x8:4; c:4] -> if has_pfxs pfxs then NONE else
356386
read_int32 l >>= \(imm,l).
357387
SOME (JUMP (decode_condition c) (Imm32 imm),l)
@@ -404,14 +434,26 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
404434
read_ModRM rex l >>= \((reg,rm),l).
405435
let op = if s then MOVSX else MOVZX in
406436
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)
437+
| [0b11001:5; r:3] -> if has_pfxs pfxs then NONE else
438+
let sz = op_size_W rex T pfxs in
439+
let reg = rex_reg (rex_B rex) r in
440+
SOME (BSWAP (%(gpr_adjust reg sz)),l)
441+
| [0xd4: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 (PADDQ (mmreg reg sz) (simd_of_RM sz rm), l)
445+
| [0xdb: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 (PAND (mmreg reg sz) (simd_of_RM sz rm), l)
449+
| [0xef:8] -> if has_unhandled_pfxs pfxs then NONE else
450+
let sz = Lower_128 in
451+
read_ModRM rex l >>= \((reg,rm),l).
452+
SOME (PXOR (mmreg reg sz) (simd_of_RM sz rm), l)
453+
| [0xfe:8] -> if has_unhandled_pfxs pfxs then NONE else
454+
let sz = Lower_128 in
455+
read_ModRM rex l >>= \((reg,rm),l).
456+
SOME (PADDD (mmreg reg sz) (simd_of_RM sz rm), l)
415457
| _ -> NONE)
416458
| [0b01010:5; r:3] -> if has_pfxs pfxs then NONE else
417459
SOME (PUSH (%(Gpr (rex_reg (rex_B rex) r) Full_64)),l)
@@ -467,7 +509,7 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
467509
if opc = word 0 then
468510
SOME (POP rm,l)
469511
else NONE
470-
| [0x90:8] -> if has_pfxs pfxs then NONE else
512+
| [0x90:8] -> if has_unhandled_pfxs pfxs then NONE else
471513
SOME (NOP,l)
472514
| [0b1010100:7; v] -> if has_pfxs pfxs then NONE else
473515
let sz = op_size T (rex_W rex) v pfxs in

‎x86/proofs/instruction.ml

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -237,10 +237,10 @@ let instruction_INDUCTION,instruction_RECURSION = define_type
237237
| ADCX operand operand
238238
| ADD operand operand
239239
| ADOX operand operand
240-
| AESENC operand operand
241-
| AESENCLAST operand operand
242240
| AESDEC operand operand
243241
| AESDECLAST operand operand
242+
| AESENC operand operand
243+
| AESENCLAST operand operand
244244
| AESKEYGENASSIST operand operand operand
245245
| AND operand operand
246246
| BSF operand operand
@@ -276,10 +276,18 @@ let instruction_INDUCTION,instruction_RECURSION = define_type
276276
| MULX4 (operand#operand) (operand#operand)
277277
| NEG operand
278278
| NOP
279+
| NOP_N operand
279280
| NOT operand
280281
| OR operand operand
282+
| PADDD operand operand
283+
| PADDQ operand operand
284+
| PAND operand operand
285+
| PCMPGTD operand operand
281286
| POP operand
287+
| PSHUFD operand operand operand
288+
| PSRAD operand operand
282289
| PUSH operand
290+
| PXOR operand operand
283291
| RCL operand operand
284292
| RCR operand operand
285293
| RET
@@ -298,7 +306,8 @@ let instruction_INDUCTION,instruction_RECURSION = define_type
298306
| TZCNT operand operand
299307
| VPXOR operand operand operand
300308
| XCHG operand operand
301-
| XOR operand operand";;
309+
| XOR operand operand
310+
| XORPS operand operand";;
302311

303312
(* ------------------------------------------------------------------------- *)
304313
(* Some shorthands for addressing modes etc. *)

‎x86/proofs/simulator.ml

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -273,6 +273,25 @@ 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)) *)
290+
[0x66; 0x45; 0x0f; 0x66; 0xfe]; (*PCMPGTD (%_% xmm15) (%_% xmm14) *)
291+
[0x66; 0x0f; 0x66; 0xcb]; (*PCMPGTD (%_% xmm1) (%_% xmm3) *)
292+
[0x66; 0x90]; (* NOP *)
293+
[0x0f; 0x1f; 0x4f; 0x00]; (* NOP_N (Memop Doubleword (%% (rdi,0))) *)
294+
[0x66; 0x0f; 0x1f; 0x84; 0x00; 0x00; 0x01; 0x02; 0x03]; (* NOP_N (Memop Word (%%%% (rax,0,rax,&50462976))) *)
276295
];;
277296

278297
(* ------------------------------------------------------------------------- *)

0 commit comments

Comments
 (0)