Some improvements to aarch64 pseudo-assembly

dartagnan/src/main/antlr4/LitmusAArch64.g4

@@ -76,6 +76,8 @@ instruction
     |   branchRegister
     |   branchLabel
     |   fence
+    |   return
+    |   nop
     ;
 
 mov locals [String rD, int size]
@@ -131,6 +133,14 @@ branchLabel
     :   label Colon
     ;
 
+return
+    :   Ret
+    ;
+
+nop
+    :   Nop
+    ;
+
 loadInstruction locals [String mo]
     :   LDR     {$mo = MO_RX;}
     |   LDAR    {$mo = MO_ACQ;}
@@ -252,7 +262,7 @@ location
     ;
 
 immediate
-    :   Num constant
+    :   Num Hexa? constant
     ;
 
 label
@@ -265,6 +275,18 @@ assertionValue
     |   constant
     ;
 
+Hexa
+    :   '0x'
+    ;
+
+Ret
+    :   'ret'
+    ;
+
+Nop
+    :   'nop'
+    ;
+
 Locations
     :   'locations'
     ;
@@ -371,10 +393,12 @@ BitfieldOperator
 
 Register64
     :   'X' DigitSequence
+    |   'XZR' // zero register
     ;
 
 Register32
     :   'W' DigitSequence
+    |   'WZR' // zero register
     ;
 
 LitmusLanguage

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java

@@ -7,12 +7,14 @@
 import com.dat3m.dartagnan.expression.Type;
 import com.dat3m.dartagnan.expression.integers.IntLiteral;
 import com.dat3m.dartagnan.expression.type.FunctionType;
+import com.dat3m.dartagnan.expression.type.IntegerType;
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.*;
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.Program.SourceLanguage;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventFactory;
+import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
 import com.dat3m.dartagnan.program.event.metadata.OriginalId;
@@ -89,6 +91,27 @@ public static void processAfterParsing(Program program) {
         }
     }
 
+    public static void replaceZeroRegisters(Program program, List<String> zeroRegNames) {
+        for (Function func : Iterables.concat(program.getThreads(), program.getFunctions())) {
+            if (func.hasBody()) {
+                for (String zeroRegName : zeroRegNames) {
+                    Register zr = func.getRegister(zeroRegName);
+                    if (zr != null) {
+                        for (RegWriter rw : func.getEvents(RegWriter.class)) {
+                            if (rw.getResultRegister().equals(zr)) {
+                                Register dummy = rw.getThread().getOrNewRegister("__zeroRegDummy_" + zr.getName(), zr.getType());
+                                rw.setResultRegister(dummy);
+                            }
+                        }
+                        // This comes after the loop to avoid the renaming in the initialization event
+                        Event initToZero = EventFactory.newLocal(zr, expressions.makeGeneralZero(zr.getType()));
+                        func.getEntry().insertAfter(initToZero);
+                    }
+                }
+            }
+        }
+    }
+
     // ----------------------------------------------------------------------------------------------------------------
     // Misc
 

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java

@@ -17,9 +17,13 @@
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.core.Load;
 
+import java.math.BigInteger;
+import java.util.Arrays;
 import java.util.HashMap;
 import java.util.Map;
 
+import static com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder.replaceZeroRegisters;
+
 public class VisitorLitmusAArch64 extends LitmusAArch64BaseVisitor<Object> {
 
     private static class CmpInstruction {
@@ -53,10 +57,11 @@ public Object visitMain(LitmusAArch64Parser.MainContext ctx) {
         visitVariableDeclaratorList(ctx.variableDeclaratorList());
         visitInstructionList(ctx.program().instructionList());
         VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter());
-        return programBuilder.build();
+        Program prog = programBuilder.build();
+        replaceZeroRegisters(prog, Arrays.asList("XZR, WZR"));
+        return prog;
     }
 
-
     // ----------------------------------------------------------------------------------------------------------------
     // Variable declarator list, e.g., { 0:EAX=0; 1:EAX=1; x=2; }
 
@@ -211,6 +216,12 @@ public Object visitFence(LitmusAArch64Parser.FenceContext ctx) {
         return programBuilder.addChild(mainThread, EventFactory.newFenceOpt(ctx.Fence().getText(), ctx.opt));
     }
 
+    @Override
+    public Object visitReturn(LitmusAArch64Parser.ReturnContext ctx) {
+        Label end = programBuilder.getEndOfThreadLabel(mainThread);
+        return programBuilder.addChild(mainThread, EventFactory.newGoto(end));
+    }
+
     @Override
     public Expression visitExpressionRegister64(LitmusAArch64Parser.ExpressionRegister64Context ctx) {
         Expression expr = programBuilder.getOrNewRegister(mainThread, ctx.register64().id, archType);
@@ -255,4 +266,12 @@ private Register visitOffset(LitmusAArch64Parser.OffsetContext ctx, Register reg
         programBuilder.addChild(mainThread, EventFactory.newLocal(result, expressions.makeAdd(register, expr)));
         return result;
     }
+
+    @Override
+    public Expression visitImmediate(LitmusAArch64Parser.ImmediateContext ctx) {
+        final int radix = ctx.Hexa() != null ? 16 : 10;
+        BigInteger value = new BigInteger(ctx.constant().getText(), radix);
+        return expressions.makeValue(value, archType);
+    }
+
 }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java

@@ -1,12 +1,11 @@
 package com.dat3m.dartagnan.parsers.program.visitors;
 
+import java.util.Arrays;
 import com.dat3m.dartagnan.configuration.Arch;
 import com.dat3m.dartagnan.exception.ParsingException;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
-import com.dat3m.dartagnan.expression.ExpressionVisitor;
 import com.dat3m.dartagnan.expression.integers.IntLiteral;
-import com.dat3m.dartagnan.expression.processing.ExprTransformer;
 import com.dat3m.dartagnan.expression.type.IntegerType;
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.parsers.LitmusRISCVBaseVisitor;
@@ -16,10 +15,11 @@
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventFactory;
-import com.dat3m.dartagnan.program.event.RegReader;
 import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.core.Label;
 
+import static com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder.replaceZeroRegisters;
+
 public class VisitorLitmusRISCV extends LitmusRISCVBaseVisitor<Object> {
 
     private final ProgramBuilder programBuilder = ProgramBuilder.forArch(Program.SourceLanguage.LITMUS, Arch.RISCV);
@@ -42,32 +42,10 @@ public Object visitMain(LitmusRISCVParser.MainContext ctx) {
         visitInstructionList(ctx.program().instructionList());
         VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter());
         Program prog = programBuilder.build();
-        replaceX0Register(prog);
-
+        replaceZeroRegisters(prog, Arrays.asList("x0"));
         return prog;
     }
 
-    /*
-    The "x0" register plays a special role in RISCV:
-      1. Reading accesses always return the value 0.
-      2. Writing accesses are discarded.
-     TODO: The below code is a simple fix to guarantee point 1. above.
-      Point 2. might also be resolved: although we do not prevent writing to x0,
-      the value of x0 is never read after the transformation so its value is effectively 0.
-      However, the exists/forall clauses could still refer to that register and observe a non-zero value.
-     */
-    private void replaceX0Register(Program program) {
-        final ExpressionVisitor<Expression> x0Replacer = new ExprTransformer() {
-            @Override
-            public Expression visitRegister(Register reg) {
-                return reg.getName().equals("x0") ? expressions.makeGeneralZero(reg.getType()) : reg;
-            }
-        };
-        program.getThreadEvents(RegReader.class)
-                .forEach(e -> e.transformExpressions(x0Replacer));
-    }
-
-
     // ----------------------------------------------------------------------------------------------------------------
     // Variable declarator list
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java

@@ -96,7 +96,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
                                 ComplexBlockSplitting.newInstance(),
                                 BranchReordering.fromConfig(config),
                                 Simplifier.fromConfig(config)
-                        ), Target.FUNCTIONS, true
+                        ), Target.ALL, true
                 ),
                 ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.ALL, true),
                 RegisterDecomposition.newInstance(),

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java

@@ -238,16 +238,8 @@ private EventGraph computeInternalDependencies(Set<Register.UsageType> usageType
                 reader.getRegisterReads().forEach(read -> {
                     if (usageTypes.contains(read.usageType())) {
                         Register register = read.register();
-                        // TODO: Update after this is merged
-                        //  https://github.com/hernanponcedeleon/Dat3M/pull/741
-                        // Register x0 is hardwired to the constant 0 in RISCV
-                        // https://en.wikichip.org/wiki/risc-v/registers,
-                        // and thus it generates no dependency, see
-                        // https://github.com/herd/herdtools7/issues/408
-                        if (!program.getArch().equals(RISCV) || !register.getName().equals("x0")) {
-                            state.ofRegister(register).getMayWriters().forEach(writer ->
-                                    data.computeIfAbsent(writer, x -> new HashSet<>()).add(reader));
-                        }
+                        state.ofRegister(register).getMayWriters()
+                                .forEach(writer -> data.computeIfAbsent(writer, x -> new HashSet<>()).add(reader));
                     }
                 });
             });

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java

@@ -40,7 +40,6 @@
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
-import static com.dat3m.dartagnan.configuration.Arch.RISCV;
 import static com.dat3m.dartagnan.program.Register.UsageType.*;
 import static com.dat3m.dartagnan.program.event.Tag.*;
 import static com.google.common.base.Preconditions.checkArgument;
@@ -915,16 +914,6 @@ private MutableKnowledge computeInternalDependencies(Set<UsageType> usageTypes)
                         continue;
                     }
                     final Register register = regRead.register();
-                    // TODO: Update after this is merged
-                    //  https://github.com/hernanponcedeleon/Dat3M/pull/741
-                    // Register x0 is hardwired to the constant 0 in RISCV
-                    // https://en.wikichip.org/wiki/risc-v/registers,
-                    // and thus it generates no dependency, see
-                    // https://github.com/herd/herdtools7/issues/408
-                    // TODO: Can't we just replace all reads of "x0" by 0 in RISC-specific preprocessing?
-                    if (program.getArch().equals(RISCV) && register.getName().equals("x0")) {
-                        continue;
-                    }
                     final List<? extends Event> writers = state.ofRegister(register).getMayWriters();
                     for (Event regWriter : writers) {
                         may.add(regWriter, regReader);