Subtraction of virtual addresses bug

[RemyCiterin]

Currently the sub of two virtual addresses x, y just return the value of
Constant.compare x y, so it return a value in 0, 1, -1, and is used in
practice to set the correct flag for the equality test of virtual addresses in
code sequences like cmp x,y; b.eq label; because the cmp instruction will
use the same implementation as sub in herd/symbValue.ml.
This semantic is unsound because

AArch64 Sub bug
{ 0:x0=x; 0:x1=y; int x = 0; int y = 0; }
P0             ;
  sub x0,x0,x1 ;
exists ( 0:x0=1 )

will return

States 1
0:X0=-1;
No
Witnesses
Positive: 0 Negative: 1
Condition exists (0:X0=1)
Observation L001 Never 0 1

even if this value is not possible: the subtraction of two addresses must be a
multiple of their alignment (4 in this case). Also only one possible value is
returned by herd7, but this is not coherent with litmus because it may return
more than one value (PAGE_SIZE, 2PAGE_SIZE, 3PAGE_SIZE...). So we may
expect an user error to be raise in this situation instead of one incorrect
value.

[RemyCiterin]

One way to solve this issue may be to have two different implementations for sub, one if the destination register is ZR to set the correct flags for the cmp instruction, and another with more restriction in case of a general sub. But cmp will still be unsound if we test for ordering properties instead of equalities of virtual addresses. We may want to raise an user error in the first case but the cmp instruction that write the NZCV flag and the branch (that read the NZCV flag) are not executed in the same times...