test.ml

test.ml

let test_mc =
  define_assert_from_elf "test_mc" "test.o"
[
  0x3dc00000;       (* arm_LDR Q0 X0 (Immediate_Offset (word 0)) *)
  0xa9000c22        (* arm_STP X2 X3 X1 (Immediate_Offset (iword (&0))) *)
];;

let TEST_EXEC = ARM_MK_EXEC_RULE test_mc;;

let STORE_DOES_NOT_TOUCH_LDR_Q = prove(
  `!(x:int128) (addr_ld:int64) (addr_st:int64)
    (x2val:int64) (x3val:int64) pc.
        (nonoverlapping (word pc,8) (addr_st,8 * 2) /\
        nonoverlapping (addr_ld,8 * 2) (addr_st,8 * 2))
        ==> ensures arm
    (\s. aligned_bytes_loaded s (word pc) test_mc /\
          read PC s = word pc /\
          read X0 s = addr_ld /\
          read X1 s = addr_st /\
          read X2 s = x2val /\
          read X3 s = x3val /\
          read (memory :> bytes128 addr_ld) s = x:(128)word)
    (\s. read PC s = word (pc + 8) /\
          read (memory :> bytes128 addr_ld) s = x:(128)word)
    (MAYCHANGE [PC; X2; X3] ,,
    MAYCHANGE [Q0] ,,
    MAYCHANGE [memory :> bytes(addr_st, 8 * 2)])`,
  MAP_EVERY X_GEN_TAC
   [`x:int128`; `addr_ld:int64`; `addr_st:int64`;
    `x2val:int64`; `x3val:int64`; `pc:num`] THEN
  REWRITE_TAC[NONOVERLAPPING_CLAUSES] THEN
  DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  ENSURES_INIT_TAC "s0" THEN
  ARM_ACCSTEPS_TAC TEST_EXEC [] (1--2) THEN
  ENSURES_FINAL_STATE_TAC THEN
  ASM_REWRITE_TAC[]);;

The input file (test.S) looks like this:

ldr q0, [x0]
stp x2, x3, [x1]