Some improvements to aarch64 pseudo-assembly

[hernanponcedeleon]

This PR adds support for

• return instructions
• nop instructions
• hexa constant
• registers name using underscored names
• special handling for zero registers (similar to RISCV)

It also enables some more passes for litmus code.

TODO

• Fix special treatment of zero registers in LazyRelationAnalysis and NativeRelationAnalysis Relation analysis with immutable and lazy data structures #743

[ThomasHaas]

LGTM

[hernanponcedeleon]

I clarified with Luc about the zero registers (see herd/herdtools7#988). Memory orderings are preserved (thus we need to keep loads targeting zero registers, but use a dummy register), but there are no data/addr/ctrl dependencies. Thus, we need to replace regWriters of the form zr <- e with dummy <- e ; zr <- 0. Also, since zero registers are not necessarily initialized explicitly in litmus code, the pass adds zr <- 0 before any RegReader using zr.

[hernanponcedeleon]

Tested by @db7 on tests generated from real assembly. @ThomasHaas unless you have further comments I will merge

[hernanponcedeleon]

@ThomasHaas as we discussed, I ended up fully moving the transformation to the parsing rather than trying to add zero registers to the core language to avoid problems with all the other passes.

AFAIK the current behavior should be equivalent to herd7, e.g. this program

RISCV xzr
{
0:x6=x; 0:x8=y;
x=1; y=0;
}
 P0          ;
 lw x0,0(x6) ;
 sw x0,0(x8) ;
exists (y=0)

generates a witness where the read value is one, but the value is discarded

[ThomasHaas]

Sounds good. I will approve once the CI is done.

EDIT: You have this TODO about the relation analysis. You should fix that before merging.

[ThomasHaas]

LGTM

[hernanponcedeleon]

I am waiting for @db7 to finish some testing and if there are no problems, I will merge

[db7]

I am waiting for @db7 to finish some testing and if there are no problems, I will merge

The test is still running. The generation of test cases is still quite inefficient.