sli_umull.ml

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`                                                                        
*)