Fix BL/BLR semantics

[relokin]

Prior to this change, for BL and BLR, there was an intrinsic data dependency from the the Register Write effect of the LR to the Intrinsic Branching effect. This is incorrect as the Intrinsic Branching effect is not dependent on the data of the LR. This change, changes the semantics of BL and BLR such there is an intrinsic order dependency from Register Write effect of the LR to the Intrinsic Branching effect.

In addition, this PR adds support for labels as values of registers in the post-condition of tests, like the following:

AArch64 A258
{
}
 P0        ;
L0:        ;
 ADR X0,L0 ;
forall(0:X0=label:"0:L0")

[maranget]

Hi @relokin. The following test is rejected:

% cat A.litmus
AArch64 A258

{
}
 P0        ;
 L0:       ;
 ADR X0,L0 ;

forall (0:X0=P0:L0)
% herd7 A.litmus
Warning: File "A.litmus": L0 is not a register (User error)

Namely, the syntax P0:L0 for a label is not recognised in the final condition, while it is in the init section. That is, teh following test is accepted:

 AArch64 A258

{
0:X1=P0:L0;
}
 P0        ;
 L0:       ;
 ADR X0,L0 ;

locations [0:X1;]

Would it be possible to accept the syntax P<i>:<label> in final conditions?

(For completeness, there is another, similar, glitch, labels in the init section are accepted as P0:L0 and printed as 0:L0)

[maranget]

The A.litmus test above was generated with mprog7. It looks difficult to fix the parser so as to accept P<i>:<label> syntax for label values in final conditions. Hence, an easier solution is to fix the pretty-printing of final conditions, for mprog7 (and other pretty-printers) to output syntax that can be parsed. The fix is coming.

[maranget]

Here is the fix.

[maranget]

Here is the fix.

Hum this fix does not handle all cases of condition pretty-printing. Some other places should undergo similar changes (e.g. here). Some refactoring may simplify things.

[relokin]

@maranget thanks for the reviews! I've added your commits to the PR but as I was looking at them, it occurred to me that we can require that labels in post-conditions always use the full format `label:"P:". This should ease things for the parser as it always provides its type. What do you think?

[maranget]

Hi @relokin, it looks like a good idea. Please proceed.

[maranget]

This PR is going beyond its initial aim to fix BL semantics. There still are minor problems (see the last two commits of this branch).

Nevertheless I am in favor of limiting the ambition of this PR and to aim at merging it as is, once label parsing has been changed as you have suggested. Your opinion?

[relokin]

hey @maranget apologies for the delay on this.

I've now had another look and applied you 2/3 of your patches from your branch (https://github.com/herd/herdtools7/tree/blr-fixes-luc). I didn't apply https://github.com/herd/herdtools7/commit/a0746aabb8ea25d6b5cdb664295d617a987c05bc because litmus7 produced extra warnings. I've forced pushed and merged my label-related commits to one, but I left your commits intact.

I've tested with make litmus-test after applying https://github.com/herd/herdtools7/pull/845

I think this is ready from my perspective, please let me know if you would like to see any changes.

[maranget]

Hi @relokin. I still wish to perform a few more tests before merging. I'll keep you informed.

As regard commit https://github.com/herd/herdtools7/commit/a0746aabb8ea25d6b5cdb664295d617a987c05bc, here is an example of a test whose produced C code does not compile without this commit:

AArch64 Label01
{
ins_t *0:X0;
}
   P0       ;
 L0:        ;
  ADR X0,L0 ;
locations [0:X0;]

However the same example was already problematic before this PR, although in a different way. So let us not address this problem for now. I'll submit a specific PR later.

[maranget]

Ok, nice work. Let us merge this PR. Beforehand, would you please rebase on master and squash all my commits into one, keeping all comments. Then I'll gladly merge :)

[relokin]

Hi @relokin. I still wish to perform a few more tests before merging. I'll keep you informed.

As regard commit a0746aa, here is an example of a test whose produced C code does not compile without this commit:

AArch64 Label01
{
ins_t *0:X0;
}
   P0       ;
 L0:        ;
  ADR X0,L0 ;
locations [0:X0;]

However the same example was already problematic before this PR, although in a different way. So let us not address this problem for now. I'll submit a specific PR later.

I agree, if this was an issue before and since this fix needs to be refined a separate PR is needed.

Ok, nice work. Let us merge this PR. Beforehand, would you please rebase on master and squash all my commits into one, keeping all comments. Then I'll gladly merge :)

Done, thanks Luc!

[maranget]

Merged! Thanks @relokin.