Update aarch64.cat to newer version & add NoRet support

[ThomasHaas]

I think I got every feature we need. We should add a few more litmus tests though.

TODO:

• Add the two new MSA litmus tests from herd7 for the updated MSA support
• Add litmus tests for NoRet support
  -- The tests are added, but we are missing support for LDADD, STADD, and CAS instructions in the grammar/parser.
• The grammar needs some cleanup.

There are still missing variants of STADD, but at least we have enough support for the litmus tests that show correct NoRet behavior.

[ThomasHaas]

We can add the litmus tests from herd7. I just tested one of them, and got the expected outcome with the changes in this PR.

[ThomasHaas]

The RelationAnalysisTest just ignores the skip list and the expected values list and so also tries to parse the unsupported litmus tests...

[ThomasHaas]

Herd7 has some more tests for NoRet loads.

[ThomasHaas]

We should have all variants of STXXX and LDXXX now, including the min/max variants.
I think the only thing that is missing are more litmus tests

[ThomasHaas]

Btw. this case can be simplified if we perform the load always into a fresh register r_fresh and only at the end assign resultReg=r_fresh.
However, this solution has one disadvantage: SCCP will propagate the resultReg=r_fresh assignment, thereby only leaving the r_fresh register. Therefore, this transformation effectively eliminates the original register name.
If we don't care about this, then we can use the easier solution. If we want to preserve the original register name, we have to do this complex capturing process.
Some middleground would be to use a fresh register and just give it a name related to the original one, e.g., by adding a unique suffix.

EDIT: In general, I'm pretty sure that we have several compilation schemes that would fail if the result register was used as part of any operand. This is certainly something we should fix in a streamlined way.

[hernanponcedeleon]

However, this solution has one disadvantage: SCCP will propagate the resultReg=r_fresh assignment, thereby only leaving the r_fresh register. Therefore, this transformation effectively eliminates the original register name.

Can't we prevent this by using NOOPT?

EDIT: In general, I'm pretty sure that we have several compilation schemes that would fail if the result register was used as part of any operand. This is certainly something we should fix in a streamlined way.

What do you mean by "fail"? Can you give a concrete example where some compilation would fail?

[ThomasHaas]

However, this solution has one disadvantage: SCCP will propagate the resultReg=r_fresh assignment, thereby only leaving the r_fresh register. Therefore, this transformation effectively eliminates the original register name.

Can't we prevent this by using NOOPT?

We have NOOPT tags for litmus code (do they survive compilation though?). SCCP will still propagate the assignment, but just not delete the (dead) register assignment. Semantically, the code is correct either way. The question is if we even care about the original registers all too much. For LLVM code, they have random names anyways. For Litmus code, the register assignment will remain for the purpose of exists/forall clauses I think. The witness might look a bit different though.

EDIT: The NOOPT tag does not survive compilation. We could propagate it, or instead use Metadata to signify it (Metadata is propagated through compilation).

EDIT: In general, I'm pretty sure that we have several compilation schemes that would fail if the result register was used as part of any operand. This is certainly something we should fix in a streamlined way.

What do you mean by "fail"? Can you give a concrete example where some compilation would fail?

The compilation won't fail per say, but the semantics becomes wrong.
For example, consider this code from the ARM8 compilation visitor:

    @Override
    public List<Event> visitXchg(Xchg xchg) {
        Register resultRegister = xchg.getResultRegister();
        Expression address = xchg.getAddress();
        String loadMo = xchg.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : "";
        String storeMo = xchg.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";

        return eventSequence(
                newRMWLoadExclusiveWithMo(resultRegister, address, loadMo),
                newRMWStoreExclusiveWithMo(address, xchg.getValue(), true, storeMo)
        );
    }

Now suppose the Xchg was of shape r = Xchg(&x, r), i.e. the exchange value was the same as the result register.
Then the generated load will overwrite r and the generated store will write the just-observed value.

// Wrong:
  r = load(x);
  store(x, r);

// Correct (A)
   r_old = r;
   r = load(x);
   store(x, r_old);

// Correct (B)
  r_fresh = load(x);
  store(x, r);
  r = r_fresh;

[hernanponcedeleon]

am I right that we were never hit by this because of LLVM's SSA form?

Is the only disadvantage of the "perform the load always into a fresh register r_fresh" option that we lose register name? That is a no issue a think: witnesses do not show register names anyway, so this is only visible by the printer (and only after compilation!) which anyway has many similar things (e.g., all the __side_effect registers).

[ThomasHaas]

am I right that we were never hit by this because of LLVM's SSA form?

SSA certainly prevents this issue. But I'm 99% sure that we already considered this problem when writing several compiler mappings, for example, in LKMMXchg

...
Register dummy = e.getFunction().newRegister(resultRegister.getType());
Load load = newRMWLoadExclusiveWithMo(dummy, address, ARMv8.extractLoadMoFromLKMo(mo));
Store store = newRMWStoreExclusiveWithMo(address, e.getValue(), true, ARMv8.extractStoreMoFromLKMo(mo));
...
return eventSequence(
           load,
           store,
           newLocal(resultRegister, dummy),
...

Is the only disadvantage of the "perform the load always into a fresh register r_fresh" option that we lose register name? That is a no issue a think: witnesses do not show register names anyway, so this is only visible by the printer (and only after compilation!) which anyway has many similar things (e.g., all the __side_effect registers).

Yes, we only lose register names. However, for llvm code, it doesn't matter too much because the register names are meaningless anyways (most of the time at least).
My concern was more about litmus code where we try to stay more truthful to the actul source code. I mean, we even put NOOPT everywhere for no other reason than making the code look like the original (though I think the NOOPT gets lost during compilation anyways...)
I know that there was a time where some optimizations were wrong on litmus code, possibly due to the lack of SSA form, and so we disabled them. But nowadays, everything we do should be sound.

Also witnesses do contain register names: they contain all local events. And even if they didn't they would still contain at least the load events which also assign to a register.

[hernanponcedeleon]

Also witnesses do contain register names: they contain all local events. And even if they didn't they would still contain at least the load events which also assign to a register.

Witnesses (to be clear, I refer to png file) contain local and load events, but we do not display the register name but the value it got in the execution.

[ThomasHaas]

I just generated a png witness and it has nodes like

  bv32 _mem2Reg#2(1800) <- _mem2Reg#3 + bv(1500)

I mean, how would you even display the value of a local event without the register it assigns to? It would just be a single number connected to nothing?

[hernanponcedeleon]

Ok, you are right we show the register name for Local; it is for Load that we just show the value.

As we discussed, for LLVM register name is not that relevant. I just checked witnesses in litmus code and we have things like bool DUMMY_REG#4(true) <- bv64 DUMMY_REG#6 == bv64 DUMMY_REG#5 in the event.

I do not think things get worse by using r_fresh or r_old.

[ThomasHaas]

Then I will change the compilation scheme accordingly.

[ThomasHaas]

I changed the compilation and also fixed the one for Xchg.