decode-test-usra.ml

decode-test-usra.ml

(* usra v1.2d, v3.2d, #30 *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x6f621461)`;;
(*   output: - : thm = |- decode (word 1868698721) = SOME (arm_USRA_VEC Q1 Q3 30 64 128) *)
(* 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)`;;
(*   output: - : thm = |- decode (word 1864045995) = SOME (arm_USRA_VEC Q11 Q13 5 16 128) *)
(* 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)`;;
(*   output: - : thm = |- decode (word 792073973) = SOME (arm_USRA_VEC Q21 Q23 10 32 64) *)
(* 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]);;