[herd] Warnings -- fatal or not?

[artkhyzha]

Seems unrelated to this PR, but is the following behaviour buggy?

The following test is a modification of something that came up in #612, but is probably unrelated to that PR; hence recording this as a separate issue.

AArch64 MP+noBR
{
ins_t *y;
0:X1=x; 0:X3=y; 0:X2=P1:L0;
1:X0=y; 1:X2=x;
}
 P0           | P1          ;
 MOV W0,#1    | ADR X4,L1   ;
 STR W0,[X1]  | STR X4,[X0] ;
 STLR X2,[X3] | DMB LD      ;
              | LDR X1,[X0] ;
              |L0:          ; 
              | ISB         ;
              | LDR W3,[X2] ;
              |L1:          ;
              | CMP X1,X4   ;
              | CSET W5,NE  ;
exists (1:X5=1 /\ 1:X3=0)

# herd7 -cat aarch64.cat MP+noBR.litmus
Warning: File "MP+noBR.litmus": Illegal operation - on constants 0 and 1:L1 (User error)

Presumably, the model does not allow executions where 1:X1=0; however, herd7 might be creating a fatal warning before this knowledge is available. I conjecture that at a point in herd7's flow before the application of the cat model, CMP X1,X4 triggers the fatal error.

Should this error be deferred until after the cat constraints are applied?

[artkhyzha]

By the way, happy to investigate further and attempt a fix if necessary -- I think a similar issue arose in #573 at some point with some other warning.

This is just to record the issue and to confirm if it is even a bug rather than a feature.

[maranget]

Hi @artkhyzha. On the long run, we'll probably need to have explicit (i.e. non-label or integer) code pointers as values. For now, if the model indeed rejects executions where 1:X1=0;, then there is another way: delay the error, as performed in PR #676. I am looking at this alternative solution.

Notice that PR #676 is not merged yet.

[artkhyzha]

Thanks, @maranget -- the approach of #676 does look interesting. I agree that having code pointers could be handy in such a case, and the overall strategy of delaying an error seems right. I'll have a closer look at #676.

Last week I tried my hand at a very simple workaround in #684. Basically, what triggers a user error in this test is the CMP comparing a label and an integer. One way to look at this is to say that this comparison only happens in executions rejected by the model, so delaying the error until we know if the execution is allowed might help. Alternatively, the comparison should not result in an error in the first place. Yes, we can't accurately compare an integer to a label until we support labels as numeric addresses, but we could agree on an assumption that labels and integers are never equal. That's how #684 tries to get around the issue.

[maranget]

Hi @artkhyzha. At the moment, errors are delayed until the second phase of equation solving, i.e. the final phase, once memory read-from relations is selected. As a result, as in the case of your example, an execution candidate that raises a fatal error and that would be discarded by the model does raise the error and interrupts the program.

There must be reasons to do so :) However, I am going to submit a PR that would delay errors until after model verification.

As for this issue and the associated PR #684. I think the solution to have comparisons of labels and integers always to be false is a decent and efficient patch. If your code does so, may I suggest removing the draft status and ask for a final review.