[herd7] Comparing labels with integers

[artkhyzha]

The objective of this PR is to resolve issue #646. In that issue we are looking at the following litmus test:

AArch64 CMP-int-vs-label
{
ins_t *y;
0:X0=y;
}
 P0           ;
 ADR X4,L0   ;
 STR X4,[X0] ;
 DMB LD      ;
 LDR X1,[X0] ;
 CMP X1,X4   ;
 CSET W5,NE  ;
L0:          ; 
 NOP         ;
locations [0:X1;0:X4]
forall (0:X5=0)

What happens is that there is a candidate execution, where the LDR reads from the initial state. In that candidate execution, CMP ends up comparing 0 (the initial value) and P0:L0, at which point herd7 crashes with a user error. This is not a correct behaviour, because the model will filter out such an execution as violating the internal visibility axioms, and only well-behaving executions (comparing P0:L0 read from memory to the constant P0:L0) will remain.

To resolve the issue, this PR simply extends the functionality of the comparisons to enable comparing 0 and P0:L0.

[artkhyzha]

Hi @maranget, marking this as a non-draft in relation to #646. This PR basically lets the result of subtraction of labels from integers be a result of comparison of two corresponding constants.

This is very ad-hoc! I find it very unsatisfactory that this fix makes it legal to apply SUB to a label and an integer. That is, I'd say that this following test would be best to let raise a user error:

AArch64 SUB-int-vs-label-error
{
0:X1=42;
}
 P0            ;
 ADR X2,L0     ;
 SUB X1,X1,X2  ;
L0:            ; 
 NOP           ;
locations [0:X1;0:X2]

Instead, the result right now becomes:

Test SUB-int-vs-label-error Required
States 1
0:X1=-1; 0:X2=0:L0;
Ok
Witnesses
Positive: 1 Negative: 0
Condition forall (true)
Observation SUB-int-vs-label-error Always 1 0
Time SUB-int-vs-label-error 0.01
Hash=424a79e2759efa5e89f49816a4e183b4

Alas, I am not sure what can be done about it -- without decoupling subtractions and comparisons, that is.

[maranget]

PR #686 implements delaying errors until after model application and gives what I believed are the expected results on your two tests. Would you please have a try. Even better, if you can think of other challenging examples.

Before merging PR #686, I'd like to find out why we did not have adopted this solution earlier. That is why error were delayed until the last phase of equation solving and not later. If anybody has ideas or memories?

[artkhyzha]

Thank you, @maranget -- I agree that PR #686 resolves the issue I originally had. I prefer its more general solution over this PR's ad-hoc approach.

You raise an interesting question. Can't think of disadvantages from deferring most errors until the last moment possible; would be curious if there are such disadvantages.

[artkhyzha]

Closing this PR as the alternative solution (PR #686) seems to be nicer. Thanks for the discussion!