Further "-variant self" changes

[artkhyzha]

This is a PR aiming to make a few adjustments to the tools in relation to the ifetch functionality:

1. The set of ifetch accesses that need to be subject to CMODX rules is exported into cat.
2. Previously, ISB instructions were prevented from overwriting instructions -- this limitation is removed.
3. The support for DIC/IDC features is being changed. There has been feedback suggesting that the ifetch model will want to support those as globally enabled flags. To this end, these features are being implemented as variants, but the previously suggested syntax of using "CacheType" field is being preserved. Hence, the logic for this support is somewhat special.
4. The "self" semantics of AArch64 instructions drops the check for whether the instruction "is_overwriteable". It has been introduced for optimisation purposes, but presently the gains are minimal -- on the one hand. On the other, for running tests taking advantage of CMODX, this checks needs to be removed. Therefore, this PR suggests removing it (and, perhaps, reintroduce it via a flag once optimisation becomes necessary).

[relokin]

@artkhyzha can you rebase and clean this up, so we can have a look?

IIUC, the change that adds CMODX seems ready for review. Then we have the options to either extend the set of instructions that can be ovewriten/can overwrite as per the two patches in this PR, or make them equal to the CMODX set, or get rid of the restriction altogether as we've discussed. What do you think would be best and not too challenging?

[artkhyzha]

@relokin, yes, will do this next. I wanted to finish trying out the (already initiated) idea for different treatment of DIC/IDC, which now seems to work, so back to cleaning up the changes before making next steps.

I'll be revisiting the logic in AArch64Sem to see what the tradeoff is as per your question.

[artkhyzha]

Hi @relokin, @maranget -- if you have time, may I ask you to review the changes of this PR? I have just moved it out of draft. The PR description gives a brief motivation for each of the separate commits, but please let me know if any extra information (or changes) would help. Many thanks in advance!

[relokin]

Two minor comments otherwise LGTM!

[relokin]

Thanks for all the changes Artem, LGTM! Let's see if @maranget has any comments and then we can merge.

[HadrienRenaud]

Hi! I don't think I understand totally the magic that is happening here with the variants, and I don't know what cmodx is, but I have a few comments on ocaml

Note that this PR has a conflict with #599, but probably very minor.

[artkhyzha]

Thank you for your feedback, @HadrienRenaud, it is very much appreciated!

Looking at #599: yes, I agree it looks like a minor conflict, so shouldn't be too hard to rebase. (Happy to rebase or help out either way.)

[HadrienRenaud]

Looks great, thank you!

For #599, we'll see what gets merged first and rebase the other :)

[artkhyzha]

Had this rebased w.r.t. master (and to clean up a few intermediate steps).

[artkhyzha]

In recent commits I simplified the support for DIC/IDC. These are parsed as global flags only. This allowed for a bit of refactoring, so the occurrences of cache_type configuration are removed from various places in herd.

[artkhyzha]

Separately, I've realised that the rebasing against the master uncovered what might be a regression. Right now herd complains at tests like the following one:

AArch64 MP.RF+dmb.st+ctrlisb
{ 0:X0=NOP;       0:X1=P1:m0; 1:X1=P1:m0;
  0:X2=1; 1:X2=0; 0:X3=z; 1:X3=z; 1:X9=0; }
P0           | P1            ;
STR W0,[X1]  |     LDR W2,[X3] ;
DMB ST       |     CBNZ W2,l1  ;
STR W2,[X3]  | l1: ISB         ;
             | m0: B l0        ;
             |     MOV W9,#1   ;
             | l0:             ;
exists 1:X2=1 /\ 1:X9=0

# herd7 -variant self tests/ifetch/DIC0-IDC0/MP.RF+dmb.st+ctrlisb.litmus
Warning: File "tests/ifetch/DIC0-IDC0/MP.RF+dmb.st+ctrlisb.litmus": Segmentation fault (kidding, address 0x4e38 does not point to code) (User error)

However, writing l0: NOP; instead of the last line of the test fixes complaints. I will investigate ASAP. This likely boils down to revising the most recent changes to loader.ml.

UPD. Also, adding a line break into l1: ISB ; affects whether the test breaks.

[artkhyzha]

As a matter of a brief status update: the bug is localised in lib/pseudo.ml and a tentative fixed is pushed. It is not too obvious to me that the fix is compehensive. In fact, I might have several tests that still behave suspiciously. Hence, my next steps will be to spend a bit more time evaluating the fix and preparing a few unit tests for herd7.

[artkhyzha]

It turned out there was another bug. Or rather let's call it a subtlety. Consider the following litmus test:

AArch64 A013
{
 0:X0=instr:"NOP"; 0:X1=P0:Lself00;
 0:X3=P0:L0;
}
P0            ;
 LDR W2,[X3]  ;
L0:           ;
 B L1         ;
 NOP          ;
L1:           ;
              ;
 STR W0,[X1]  ;
Lself00:      ;
 B Lout       ;
Lout:         ;

The prefix of it serves no purpose other than introducing a value instr:"B .+8" into the executions. Under such circumstances, the current implementation of the ifetch logic (check_self in AArch64Sem.ml) will attempt creating a graph where this value gets written into the address of the label P0:Lself00. Note, however, that if such execution existed, it would be ill-formed because of jumping out of bounds of the litmus test. Normally, herd7 would trigger a user error for such graphs, but here we are dealing with a graph that is only ill-formed if the contraint of instruction fetch loading instr:"B .+8" from P0:Lself00 is satisfied. It is never satisfied in this test, so the user must not be blamed.

In contrast, the following litmus test does result in an out-of-bounds jump, so the user error is appropriate.

AArch64 A014
{
 0:X1=P0:Lself00;
 0:X3=P0:L0;
}
P0            ;
 LDR W2,[X3]  ;
L0:           ;
 B L1         ;
 NOP          ;
L1:           ;
              ;
 STR W2,[X1]  ;
Lself00:      ;
 B Lout       ;
Lout:         ;

The proposed fix is to defer the user error until the memory constraints are resolved.

[artkhyzha]

The first bug could be illustrated with this litmus test (rather than a more complex MP.RF+dmb.st+ctrlisb):

AArch64 A015
{
  0:X0=NOP;0:X1=P0:Lself00; 0:X9=0;
}
P0                 ;
L0:L1: STR W0,[X1];
Lself00:    ;
 B Lout     ;
 MOV W9,#1  ;
Lout:       ;
exists 0:X9=0

The logic in lib/pseudo.ml gets called by AArch64Sem.ml as a part of an effort to make the list of instructions that may plausibly overwrite other instructions. Specifically, one part of that logic looks at the litmus test, a pseudoinstruction by pseudoinstruction, and it is supposed to make a list of instructions that have a label from a given set. (In practice, this set will be the set of labels mentioned in the initial state.)

This bit of logic revisiting the test had a tiny issue with enumerating instructions: if there were a line like "L0:L1: STR W0,[X1];", it would not get counted as an instruction. However, if that counter is not accurate, it turns out that converting branches to labels into branches with offsets is done incorrectly as a part of this logic -- to devastating effects.

The commit bdc28b0 fixes the tiny issue in the logic processing litmus tests. The subsequent commit a364b22 does something more radical: it removes the need for that logic at all. To the best of my understanding, all the relevant instructions will be found as a part of the preparation of the initial state (in mem.ml), and trying to reload instructions from code seems redundant and error-prone. It would be super to confirm this with @maranget though: namely, that get_overwriting_instructions in AArch64Sem.ml can be simplified like commit a364b22 suggests.

[artkhyzha]

@maranget @relokin With the bugs/subtleties fixed and described, could I ask you to please have another look at this PR when you have time? Hopefully, it is can advance towards merging!

[relokin]

Suggested change

	STR W0,[X1]| L2: B Lout1;
	Lself00: | L1:L0:Lsrc: NOP;
	STR W0,[X1]| B Lout1;
	Lself00: | Lsrc: NOP;

[artkhyzha]

Nope, the redundant labels were put there intentionally. The behaviors the test was trying to focus on are sensitive to what sequence of "pseudoinstructions" the test gets parsed into.

[maranget]

Merged, thanks @artkhyzha, @relokin, @HadrienRenaud @jalglave.