Skip to content

Instantly share code, notes, and snippets.

@aqjune

aqjune/sli_umull.ml

Created May 16, 2023 01:19
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save aqjune/ef4763da43fcc1be99178ec56647afdc to your computer and use it in GitHub Desktop.
Save aqjune/ef4763da43fcc1be99178ec56647afdc to your computer and use it in GitHub Desktop.
Download ZIP
sli_umull.ml
Raw
sli_umull.ml
(* sli v3.2d, v4.2d, #32 *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x6f605483)`;;
(* output: - : thm = |- decode (word 1868584067) = SOME (arm_SLI_VEC Q3 Q4 32 64) *)
(* 2. Check that the symbolic output looks ok *)
let code_6f605483 = define `code_6f605483:byte list = [word 0x83; word 0x54; word 0x60; word 0x6f]`;;
let execth = ARM_MK_EXEC_RULE code_6f605483;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_6f605483 /\
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:
- : goalstack = 1 subgoal (1 total)
0 [`read PC s0 = word pc`]
1 [`aligned_bytes_loaded s1 (word pc) code_6f605483`]
2 [`(MAYCHANGE [PC] ,, MAYCHANGE [Q3]) s0 s1`]
3 [`read Q3 s1 =
word_join
(word_or (word_shl (word_subword (read Q4 s0) (64,64)) 32)
(word_and (word_subword (read Q3 s0) (64,64)) (word 4294967295)))
(word_or (word_shl (word_subword (read Q4 s0) (0,64)) 32)
(word_and (word_subword (read Q3 s0) (0,64)) (word 4294967295)))`]
4 [`read PC s1 = word (pc + 4)`]
`eventually arm
(\s'. read PC s' = word (pc + 4) /\ MAYCHANGE something s0 s')
s1` *)
(* umull v6.2d, v2.2s, v0.2s *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x2ea0c046)`;;
(* output: - : thm = |- decode (word 782286918) = SOME (arm_UMULL_VEC Q6 Q2 Q0 32) *)
(* 2. Check that the symbolic output looks ok *)
let code_2ea0c046 = define `code_2ea0c046:byte list = [word 0x46; word 0xc0; word 0xa0; word 0x2e]`;;
let execth = ARM_MK_EXEC_RULE code_2ea0c046;;
g `ensures arm
(\s. aligned_bytes_loaded s (word pc) code_2ea0c046 /\
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:
- : goalstack = 1 subgoal (1 total)
0 [`read PC s0 = word pc`]
1 [`aligned_bytes_loaded s1 (word pc) code_2ea0c046`]
2 [`(MAYCHANGE [PC] ,, MAYCHANGE [Q6]) s0 s1`]
3 [`read Q6 s1 =
word_join
(word_mul
(word_subword
(word_join
(word_zx (word_subword (word_subword (read Q2 s0) (0,64)) (32,32)))
(word_zx (word_subword (word_subword (read Q2 s0) (0,64)) (0,32))))
(64,64))
(word_subword
(word_join
(word_zx (word_subword (word_subword (read Q0 s0) (0,64)) (32,32)))
(word_zx (word_subword (word_subword (read Q0 s0) (0,64)) (0,32))))
(64,64)))
(word_mul
(word_subword
(word_join
(word_zx (word_subword (word_subword (read Q2 s0) (0,64)) (32,32)))
(word_zx (word_subword (word_subword (read Q2 s0) (0,64)) (0,32))))
(0,64))
(word_subword
(word_join
(word_zx (word_subword (word_subword (read Q0 s0) (0,64)) (32,32)))
(word_zx (word_subword (word_subword (read Q0 s0) (0,64)) (0,32))))
(0,64)))`]
4 [`read PC s1 = word (pc + 4)`]
`eventually arm
(\s'. read PC s' = word (pc + 4) /\ MAYCHANGE something s0 s')
s1`
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment