Skip to content

Instantly share code, notes, and snippets.

@aqjune

aqjune/tests.ml

Created April 21, 2023 13:04
Show Gist options
  • Save aqjune/aee276c8e4646dacad73f6a5575fa322 to your computer and use it in GitHub Desktop.
Save aqjune/aee276c8e4646dacad73f6a5575fa322 to your computer and use it in GitHub Desktop.
Download ZIP
PR-NEON8
Raw
tests.ml
(* ============= *)
(* 1. dup: https://developer.arm.com/documentation/ddi0602/2022-06/SIMD-FP-Instructions/DUP--general---Duplicate-general-purpose-register-to-vector- *)
(* dup v2.2d, x4 (0x4e080c82, 0100 1110 0000 1000 0000 1100 1000 0010) *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x4e080c82)`;;
(* output: - : thm = |- decode (word 1309150338) = SOME (arm_DUP Q2 X4) *)
(* 2. Check that the symbolic output looks ok *)
let code_4e080c82 = define `code_4e080c82:byte list = [word 0x82; word 0x0c; word 0x08; word 0x4e]`;;
let execth = ARM_MK_EXEC_RULE code_4e080c82;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_4e080c82 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q2 s1 = word_join (read X4 s0) (read X4 s0)`] ... *)
(* ============= *)
(* 2. movi: https://developer.arm.com/documentation/ddi0602/2022-06/SIMD-FP-Instructions/MOVI--Move-Immediate--vector-- *)
(* movi v4.2d, #0x000000ffffffff (0x6f00e5e4, 0110 1111 0000 0000 1110 0101 1110 0100) *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x6f00e5e4)`;;
(* output: - : thm = |- decode (word 1862329828) = SOME (arm_MOVI Q4 (word 4294967295)) *)
(* 2. Check that the symbolic output looks ok *)
let code_6f00e5e4 = define `code_6f00e5e4:byte list = [word 0xe4; word 0xe5; word 0x00; word 0x6f]`;;
let execth = ARM_MK_EXEC_RULE code_6f00e5e4;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_6f00e5e4 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q4 s1 = word 79228162495817593524129366015`] ... *)
(* ============= *)
(* 3. ext: https://developer.arm.com/documentation/ddi0602/2022-06/SIMD-FP-Instructions/EXT--Extract-vector-from-pair-of-vectors- *)
(* ext v1.16b, v0.16b, v0.16b, #8 (0x6e004001, 0110 1110 0000 0000 0100 0000 0000 0001) *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x6e004001)`;;
(* output: - : thm = |- decode (word 1845510145) = SOME (arm_EXT Q1 Q0 Q0 64) *)
(* 2. Check that the symbolic output looks ok *)
let code_6e004001 = define `code_6e004001:byte list = [word 0x01; word 0x40; word 0x00; word 0x6e]`;;
let execth = ARM_MK_EXEC_RULE code_6e004001;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_6e004001 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q1 s1 =
word_subword (word_join (read Q0 s0) (read Q0 s0)) (64,128)`] ... *)
(* ============= *)
(* 4. shrn: https://developer.arm.com/documentation/ddi0596/2021-12/SIMD-FP-Instructions/SHRN--SHRN2--Shift-Right-Narrow--immediate--?lang=en *)
(* shrn v2.2s, v0.2d, #32 (0x0f208402, 0000 1111 0010 0000 1000 0100 0000 0010)
- immh = 0100, immb: 000
- esize = 8 << 2 = 32
- shift = (2 * 32) - 0100:000 = 64 - 32 = 32
*)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x0f208402)`;;
(* output: - : thm = |- decode (word 253789186) = SOME (arm_SHRN Q2 Q0 32 32) *)
(* 2. Check that the symbolic output looks ok *)
let code_0f208402 = define `code_0f208402:byte list = [word 0x02; word 0x84; word 0x20; word 0x0f]`;;
let execth = ARM_MK_EXEC_RULE code_0f208402;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_0f208402 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q2 s1 =
word_subword
(word_join
(word_subword (word_ushr (word_subword (read Q0 s0) (64,64)) 32)
(0,32))
(word_subword (word_ushr (word_subword (read Q0 s0) (0,64)) 32) (0,32)))
(0,128)`] ... *)
(* shrn v2.2s, v0.2d, #25 (0x0f278402) *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x0f278402)`;;
(* output: - : thm = |- decode (word 254247938) = SOME (arm_SHRN Q2 Q0 25 32) *)
(* 2. Check that the symbolic output looks ok *)
let code_0f278402 = define `code_0f278402:byte list = [word 0x02; word 0x84; word 0x27; word 0x0f]`;;
let execth = ARM_MK_EXEC_RULE code_0f278402;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_0f278402 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q2 s1 =
word_subword
(word_join
(word_subword (word_ushr (word_subword (read Q0 s0) (64,64)) 25)
(0,32))
(word_subword (word_ushr (word_subword (read Q0 s0) (0,64)) 25) (0,32)))
(0,128)`] ... *)
(* shrn v6.4h, v5.4s, #13 (0x0f1384a6) *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x0f1384a6)`;;
(* output: - : thm = |- decode (word 252937382) = SOME (arm_SHRN Q6 Q5 13 16) *)
(* 2. Check that the symbolic output looks ok *)
let code_0f1384a6 = define `code_0f1384a6:byte list = [word 0xa6; word 0x84; word 0x13; word 0x0f]`;;
let execth = ARM_MK_EXEC_RULE code_0f1384a6;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_0f1384a6 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q6 s1 =
word_subword
(word_join
(word_join
(word_subword
(word_ushr
(word_subword (word_subword (read Q5 s0) (64,64)) (32,32))
13)
(0,16))
(word_subword
(word_ushr (word_subword (word_subword (read Q5 s0) (64,64)) (0,32))
13)
(0,16)))
(word_join
(word_subword
(word_ushr (word_subword (word_subword (read Q5 s0) (0,64)) (32,32))
13)
(0,16))
(word_subword
(word_ushr (word_subword (word_subword (read Q5 s0) (0,64)) (0,32))
13)
(0,16))))
(0,128)`] ... *)
(* ============= *)
(* 5. zip1: https://developer.arm.com/documentation/ddi0596/2021-12/SIMD-FP-Instructions/ZIP1--Zip-vectors--primary--?lang=en *)
(* zip1 v2.2s, v0.2s, v1.2s *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x0e813802)`;;
(* output: - : thm = |- decode (word 243349506) = SOME (arm_ZIP1 Q2 Q0 Q1 32 64) *)
(* 2. Check that the symbolic output looks ok *)
let code_0e813802 = define `code_0e813802:byte list = [word 0x02; word 0x38; word 0x81; word 0x0e]`;;
let execth = ARM_MK_EXEC_RULE code_0e813802;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_0e813802 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q2 s1 =
word_zx
(word_join (word_subword (read Q1 s0) (0,32))
(word_subword (read Q0 s0) (0,32)))`] ... *)
(* zip1 v12.4h, v10.4h, v11.4h *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x0e4b394c)`;;
(* output: - : thm = |- decode (word 239810892) = SOME (arm_ZIP1 Q12 Q10 Q11 16 64) *)
(* 2. Check that the symbolic output looks ok *)
let code_0e4b394c = define `code_0e4b394c:byte list = [word 0x4c; word 0x39; word 0x4b; word 0x0e]`;;
let execth = ARM_MK_EXEC_RULE code_0e4b394c;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_0e4b394c /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q12 s1 =
word_zx
(word_join
(word_join (word_subword (word_subword (read Q11 s0) (0,32)) (16,16))
(word_subword (word_subword (read Q10 s0) (0,32)) (16,16)))
(word_join (word_subword (word_subword (read Q11 s0) (0,32)) (0,16))
(word_subword (word_subword (read Q10 s0) (0,32)) (0,16))))`] ... *)
(* zip1 v22.8b, v20.8b, v21.8b *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x0e153a96)`;;
(* output: - : thm = |- decode (word 236272278) = SOME (arm_ZIP1 Q22 Q20 Q21 8 64) *)
(* 2. Check that the symbolic output looks ok *)
let code_0e153a96 = define `code_0e153a96:byte list = [word 0x96; word 0x3a; word 0x15; word 0x0e]`;;
let execth = ARM_MK_EXEC_RULE code_0e153a96;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_0e153a96 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... (long) ... *)
(* zip1 v5.2d, v4.2d, v3.2d *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x4ec33885)`;;
(* output: - : thm = |- decode (word 1321416837) = SOME (arm_ZIP1 Q5 Q4 Q3 64 128) *)
(* 2. Check that the symbolic output looks ok *)
let code_4ec33885 = define `code_4ec33885:byte list = [word 0x85; word 0x38; word 0xc3; word 0x4e]`;;
let execth = ARM_MK_EXEC_RULE code_4ec33885;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_4ec33885 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q5 s1 =
word_join (word_subword (read Q3 s0) (0,64))
(word_subword (read Q4 s0) (0,64))`] ... *)
(* zip1 v15.4s, v14.4s, v13.4s *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x4e8d39cf)`;;
(* output: - : thm = |- decode (word 1317878223) = SOME (arm_ZIP1 Q15 Q14 Q13 32 128) *)
(* 2. Check that the symbolic output looks ok *)
let code_4e8d39cf = define `code_4e8d39cf:byte list = [word 0xcf; word 0x39; word 0x8d; word 0x4e]`;;
let execth = ARM_MK_EXEC_RULE code_4e8d39cf;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_4e8d39cf /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q15 s1 =
word_join
(word_join (word_subword (word_subword (read Q13 s0) (0,64)) (32,32))
(word_subword (word_subword (read Q14 s0) (0,64)) (32,32)))
(word_join (word_subword (word_subword (read Q13 s0) (0,64)) (0,32))
(word_subword (word_subword (read Q14 s0) (0,64)) (0,32)))`] ... *)
(* zip1 v25.16b, v24.16b, v23.16b *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x4e173b19)`;;
(* output: - : thm = |- decode (word 1310145305) = SOME (arm_ZIP1 Q25 Q24 Q23 8 128) *)
(* 2. Check that the symbolic output looks ok *)
let code_4e173b19 = define `code_4e173b19:byte list = [word 0x19; word 0x3b; word 0x17; word 0x4e]`;;
let execth = ARM_MK_EXEC_RULE code_4e173b19;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_4e173b19 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... (long) ... *)
(* ============= *)
(* 6. and: https://developer.arm.com/documentation/ddi0596/2021-12/SIMD-FP-Instructions/AND--vector---Bitwise-AND--vector--?lang=en *)
(* and v3.8b, v1.8b, v2.8b *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x0e221c23)`;;
(* output: - : thm = |- decode (word 237116451) = SOME (arm_AND_VEC Q3 Q1 Q2 64) *)
(* 2. Check that the symbolic output looks ok *)
let code_0e221c23 = define `code_0e221c23:byte list = [word 0x23; word 0x1c; word 0x22; word 0x0e]`;;
let execth = ARM_MK_EXEC_RULE code_0e221c23;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_0e221c23 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q3 s1 =
word_zx (word_subword (word_and (read Q2 s0) (read Q1 s0)) (0,64))`] ... *)
(* and v13.16b, v11.16b, v12.16b *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x4e2c1d6d)`;;
(* output: - : thm = |- decode (word 1311513965) = SOME (arm_AND_VEC Q13 Q11 Q12 128) *)
(* 2. Check that the symbolic output looks ok *)
let code_4e2c1d6d = define `code_4e2c1d6d:byte list = [word 0x6d; word 0x1d; word 0x2c; word 0x4e]`;;
let execth = ARM_MK_EXEC_RULE code_4e2c1d6d;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_4e2c1d6d /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: 3 [`read Q13 s1 = word_and (read Q12 s0) (read Q11 s0)`] *)
(* ============= *)
(* 7. add: https://developer.arm.com/documentation/ddi0596/2021-12/SIMD-FP-Instructions/ADD--vector---Add--vector--?lang=en *)
(* add v3.2d, v1.2d, v2.2d *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x4ee28423)`;;
(* output: - : thm = |- decode (word 1323467811) = SOME (arm_ADD_VEC Q3 Q1 Q2 64 128) *)
(* 2. Check that the symbolic output looks ok *)
let code_4ee28423 = define `code_4ee28423:byte list = [word 0x23; word 0x84; word 0xe2; word 0x4e]`;;
let execth = ARM_MK_EXEC_RULE code_4ee28423;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_4ee28423 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q3 s1 =
word_join
(word_add (word_subword (read Q1 s0) (64,64))
(word_subword (read Q2 s0) (64,64)))
(word_add (word_subword (read Q1 s0) (0,64))
(word_subword (read Q2 s0) (0,64)))`] ... *)
(* add v13.4s, v11.4s, v12.4s *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x4eac856d)`;;
(* output: - : thm = |- decode (word 1319929197) = SOME (arm_ADD_VEC Q13 Q11 Q12 32 128) *)
(* 2. Check that the symbolic output looks ok *)
let code_4eac856d = define `code_4eac856d:byte list = [word 0x6d; word 0x85; word 0xac; word 0x4e]`;;
let execth = ARM_MK_EXEC_RULE code_4eac856d;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_4eac856d /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q13 s1 =
word_join
(word_join
(word_add (word_subword (word_subword (read Q11 s0) (64,64)) (32,32))
(word_subword (word_subword (read Q12 s0) (64,64)) (32,32)))
(word_add (word_subword (word_subword (read Q11 s0) (64,64)) (0,32))
(word_subword (word_subword (read Q12 s0) (64,64)) (0,32))))
(word_join
(word_add (word_subword (word_subword (read Q11 s0) (0,64)) (32,32))
(word_subword (word_subword (read Q12 s0) (0,64)) (32,32)))
(word_add (word_subword (word_subword (read Q11 s0) (0,64)) (0,32))
(word_subword (word_subword (read Q12 s0) (0,64)) (0,32))))`] ... *)
(* add v23.2s, v11.2s, v12.2s *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x0eac8577)`;;
(* output: - : thm = |- decode (word 246187383) = SOME (arm_ADD_VEC Q23 Q11 Q12 32 64) *)
(* 2. Check that the symbolic output looks ok *)
let code_0eac8577 = define `code_0eac8577:byte list = [word 0x77; word 0x85; word 0xac; word 0x0e]`;;
let execth = ARM_MK_EXEC_RULE code_0eac8577;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_0eac8577 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q23 s1 =
word_zx
(word_join
(word_add (word_subword (word_subword (read Q11 s0) (0,64)) (32,32))
(word_subword (word_subword (read Q12 s0) (0,64)) (32,32)))
(word_add (word_subword (word_subword (read Q11 s0) (0,64)) (0,32))
(word_subword (word_subword (read Q12 s0) (0,64)) (0,32))))`] ... *)
(* ============= *)
(* 8. mov:
mov (VEC) is orr's alias.
https://developer.arm.com/documentation/ddi0596/2021-12/SIMD-FP-Instructions/ORR--vector--register---Bitwise-inclusive-OR--vector--register--?lang=en *)
(* mov v2.16b, v1.16b *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x4ea11c22)`;;
(* output: - : thm = |- decode (word 1319181346) = SOME (arm_MOV_VEC Q2 Q1 128) *)
(* 2. Check that the symbolic output looks ok *)
let code_4ea11c22 = define `code_4ea11c22:byte list = [word 0x22; word 0x1c; word 0xa1; word 0x4e]`;;
let execth = ARM_MK_EXEC_RULE code_4ea11c22;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_4ea11c22 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q2 s1 = read Q1 s0`] ... *)
(* mov v12.8b, v11.8b *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x0eab1d6c)`;;
(* output: - : thm = |- decode (word 246095212) = SOME (arm_MOV_VEC Q12 Q11 64) *)
(* 2. Check that the symbolic output looks ok *)
let code_0eab1d6c = define `code_0eab1d6c:byte list = [word 0x6c; word 0x1d; word 0xab; word 0x0e]`;;
let execth = ARM_MK_EXEC_RULE code_0eab1d6c;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_0eab1d6c /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* output: ... 3 [`read Q12 s1 = word_zx (word_subword (read Q11 s0) (0,64))`] ... *)
(* IMPLEMENTED BUT NOT ADDED: usra
usra: https://developer.arm.com/documentation/ddi0596/2021-12/SIMD-FP-Instructions/USRA--Unsigned-Shift-Right-and-Accumulate--immediate--?lang=en
usra couldn't be added because its DECODE_CONV could not deal with its bit pattern under the existence of movi.
It seems DECODE_CONV confuses the usra's bit pattern with movi's bit pattern.
| [0:1; q; 0b1011110:7; immh:4; immb:3; 0b000101:6; Rn:5; Rd:5] ->
// USRA (NEON)
if immh = (word 0b0000:(4)word) then NONE // "asimdimm"
else if bit 3 immh /\ ~q then NONE // "UNDEFINED"
else
let highest_set_bit =
if bit 3 immh then 3 else
if bit 2 immh then 2 else
if bit 1 immh then 1 else 0 in
let esize = 8 * (2 EXP highest_set_bit) in
let datasize = if q then 128 else 64 in
let elements = datasize DIV esize in
let shift = (esize * 2) - val(word_join immh immb:(7)word) in
// unsigned is true, round is false, accumulate is true
SOME (arm_USRA_VEC (QREG' Rd) (QREG' Rn) shift esize datasize)
let arm_USRA_VEC = define
`arm_USRA_VEC Rd Rn shift esize datasize =
\s. let n:(128)word = read Rn s in
let n:(128)word =
if esize = 64 then usimd2 (\x. word_ushr x shift) n
else if esize = 32 then usimd4 (\x. word_ushr x shift) n
else if esize = 16 then usimd8 (\x. word_ushr x shift) n
else usimd16 (\x. word_ushr x shift) n in
let d:(128)word = read Rd s in
if datasize = 128 then
let d:(128)word =
if esize = 64 then simd2 word_add d n
else if esize = 32 then simd4 word_add d n
else if esize = 16 then simd8 word_add d n
else simd16 word_add d n in
(Rd := d) s
else // datasize = 64
let n:(64)word = word_subword n (0,64):(64)word in
let d:(64)word = word_subword d (0,64):(64)word in
let d:(64)word =
if esize = 32 then simd2 word_add d n
else if esize = 16 then simd4 word_add d n
else simd8 word_add d n in
(Rd := word_zx d:(128)word) s`;;
let arm_USRA_VEC_ALT = REWRITE_RULE all_simd_rules arm_USRA_VEC;;
(* usra v1.2d, v3.2d, #30 *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x6f621461)`;;
(* 2. Check that the symbolic output looks ok *)
let code_6f621461 = define `code_6f621461:byte list = [word 0x61; word 0x14; word 0x62; word 0x6f]`;;
let execth = ARM_MK_EXEC_RULE code_6f621461;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_6f621461 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* usra v11.8h, v13.8h, #5 *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x6f1b15ab)`;;
(* 2. Check that the symbolic output looks ok *)
let code_6f1b15ab = define `code_6f1b15ab:byte list = [word 0xab; word 0x15; word 0x1b; word 0x6f]`;;
let execth = ARM_MK_EXEC_RULE code_6f1b15ab;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_6f1b15ab /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
(* usra v21.2s, v23.2s, #10 *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x2f3616f5)`;;
(* 2. Check that the symbolic output looks ok *)
let code_2f3616f5 = define `code_2f3616f5:byte list = [word 0xf5; word 0x16; word 0x36; word 0x2f]`;;
let execth = ARM_MK_EXEC_RULE code_2f3616f5;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_2f3616f5 /\
read PC s = word pc)
(\s. read PC s = word(pc + 4))
(MAYCHANGE something)`;;
e(ENSURES_INIT_TAC "s0" THEN ARM_VSTEPS_TAC execth [1]);;
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment