[litmus-kvm] final condition check

[RemyCiterin]

if I write a program that expect a given address in a register, and this address doesn't match because of an offset then herd will return a fail without error, but litmus will return that the test pass:

AArch64 offset_cex
{ 0:x0=x; int64_t 0:x1=4; }
P0;
  add x0,x0,x1;
forall
  ( 0:x0=x )

herd will return:

States 1
0:X0=x+4;
No
Witnesses
Positive: 0 Negative: 1

but litmus will return:

Histogram (1 states)
4000000:>0:X0=x;
Ok

Witnesses
Positive: 4000000, Negative: 0
Condition forall (0:X0=x) is validated

btw if the offset is greater than 4096, litmus will fail with this error:

Failure: Cannot find symbol for address
Failure: Cannot find symbol for address
Failure: Cannot find symbol for address

EXIT: STATUS=3

I suppose this is because the final_cond function take as argument the result of the idx_addr function:

static int idx_addr(intmax_t *v_addr,vars_t *p) {
  intmax_t *p_addr =
    (intmax_t *)((uintptr_t)v_addr & PAGE_MASK);
  if (p_addr == p->x) return DATA_SYMB_ID_X;
  if ((pteval_t *)v_addr == p->pte_x) return DATA_SYMB_ID_PTE_X;
  fatal("Cannot find symbol for address"); return -1;
}

but this function only return the ID of the variable it detect and doesn't search to find any information about the offset. So litmus fail to perform the final check and pretty print the wrong value (x instead of x+4 here).
Idealy we may also expect a warning in herd if the offset is greater than 4095 or negative during a memop or in the final state to inform the user that the result may not be coherent with litmus? (I don't know if this is also correct without kvm)