Some improvements to aarch64 pseudo-assembly

Signed-off-by: Hernan Ponce de Leon <[email protected]>

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;}
@@ -244,15 +254,15 @@ register64 returns[String id]
     ;
 
 register32 returns[String id]
-    :   r = Register32 {$id = $r.text.replace("W","X");}
+    :   r = Register32 {$id = $r.text.replace("W","X").replace("w","x");}
     ;
 
 location
     :   Identifier
     ;
 
 immediate
-    :   Num constant
+    :   Num Hexa? constant
     ;
 
 label
@@ -265,6 +275,18 @@ assertionValue
     |   constant
     ;
 
+Hexa
+    :   '0x'
+    ;
+
+Ret
+    :   'ret'
+    ;
+
+Nop
+    :   'nop'
+    ;
+
 Locations
     :   'locations'
     ;
@@ -371,10 +393,16 @@ BitfieldOperator
 
 Register64
     :   'X' DigitSequence
+    |   'x' DigitSequence
+    |   'XZR' // zero register
+    |   'xzr' // zero register
     ;
 
 Register32
     :   'W' DigitSequence
+    |   'w' DigitSequence
+    |   'WZR' // zero register
+    |   'wzr' // zero register
     ;
 
 LitmusLanguage

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

@@ -4,7 +4,9 @@
 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.LitmusAArch64BaseVisitor;
@@ -13,10 +15,12 @@
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.EventFactory;
+import com.dat3m.dartagnan.program.event.RegReader;
 import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.core.Load;
 
+import java.math.BigInteger;
 import java.util.HashMap;
 import java.util.Map;
 
@@ -53,9 +57,32 @@ 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();
+        replaceXZRRegister(prog);
+
+        return prog;
+
     }
 
+    /*
+    The "xzr" register plays a special role in AArhc64:
+      1. Reading accesses always return the value 0.
+      2. Discards data when written.
+     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 xzr,
+      the value of xzr 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 replaceXZRRegister(Program program) {
+        final ExpressionVisitor<Expression> xzrReplacer = new ExprTransformer() {
+            @Override
+            public Expression visitRegister(Register reg) {
+                return reg.getName().equals("xzr") ? expressions.makeGeneralZero(reg.getType()) : reg;
+            }
+        };
+        program.getThreadEvents(RegReader.class)
+                .forEach(e -> e.transformExpressions(xzrReplacer));
+    }
 
     // ----------------------------------------------------------------------------------------------------------------
     // Variable declarator list, e.g., { 0:EAX=0; 1:EAX=1; x=2; }
@@ -211,6 +238,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 +288,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/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(),