Improve PPC grammar and visitor (#762)

dartagnan/src/main/antlr4/LitmusAssertions.g4

@@ -28,6 +28,7 @@ assertion
 assertionValue
     :   varName LBracket DigitSequence RBracket
     |   varName
+    |   LBracket varName RBracket
     |   threadId Colon varName
     |   constant
     ;

dartagnan/src/main/antlr4/LitmusPPC.g4

@@ -63,8 +63,10 @@ instruction
     |   li
     |   lwz
     |   lwzx
+    |   lwarx
     |   stw
     |   stwx
+    |   stwcx
     |   mr
     |   addi
     |   xor
@@ -86,6 +88,10 @@ lwzx
     :   Lwzx register Comma register Comma register
     ;
 
+lwarx
+    :   Lwarx register Comma register Comma register
+    ;
+
 stw
     :   Stw register Comma offset LPar register RPar
     ;
@@ -94,6 +100,10 @@ stwx
     :   Stwx register Comma register Comma register
     ;
 
+stwcx
+    :   Stwcx register Comma register Comma register
+    ;
+
 mr
     :   Mr register Comma register
     ;
@@ -124,6 +134,7 @@ fence
 
 location
     :   Identifier
+    |   LBracket Identifier RBracket
     ;
 
 register
@@ -187,13 +198,20 @@ Bge
 Li  :   'li'
     ;
 
+Lwarx:   'lwarx'
+    ;
+
 Lwzx:   'lwzx'
     ;
 
 Lwz
     :   'lwz'
     ;
 
+Stwcx
+    :   'stwcx.'
+    ;
+
 Stwx
     :   'stwx'
     ;
@@ -223,7 +241,7 @@ Register
     ;
 
 Label
-    :   'LC' DigitSequence
+    :   'L' Identifier
     ;
 
 LitmusLanguage

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

@@ -116,15 +116,15 @@ public Object visitInstructionRow(LitmusPPCParser.InstructionRowContext ctx) {
 
     @Override
     public Object visitLi(LitmusPPCParser.LiContext ctx) {
-        Register register = programBuilder.getOrNewRegister(mainThread, ctx.register().getText(), archType);
+        Register register = (Register) ctx.register().accept(this);
         IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType);
         return programBuilder.addChild(mainThread, EventFactory.newLocal(register, constant));
     }
 
     @Override
     public Object visitLwz(LitmusPPCParser.LwzContext ctx) {
-        Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
-        Register ra = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+        Register r1 = (Register) ctx.register(0).accept(this);
+        Register ra = (Register) ctx.register(1).accept(this);
         return programBuilder.addChild(mainThread, EventFactory.newLoad(r1, ra));
     }
 
@@ -134,10 +134,18 @@ public Object visitLwzx(LitmusPPCParser.LwzxContext ctx) {
         throw new ParsingException("lwzx is not implemented");
     }
 
+    @Override
+    public Object visitLwarx(LitmusPPCParser.LwarxContext ctx) {
+        Register r1 = (Register) ctx.register(0).accept(this);
+        Register ra = (Register) ctx.register(1).accept(this);
+        Register rb = (Register) ctx.register(2).accept(this);
+        return programBuilder.addChild(mainThread, EventFactory.newRMWLoadExclusive(r1, expressions.makeAdd(ra, rb)));
+    }
+
     @Override
     public Object visitStw(LitmusPPCParser.StwContext ctx) {
-        Register r1 = programBuilder.getOrErrorRegister(mainThread, ctx.register(0).getText());
-        Register ra = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+        Register r1 = (Register) ctx.register(0).accept(this);
+        Register ra = (Register) ctx.register(1).accept(this);
         return programBuilder.addChild(mainThread, EventFactory.newStore(ra, r1));
     }
 
@@ -147,33 +155,45 @@ public Object visitStwx(LitmusPPCParser.StwxContext ctx) {
         throw new ParsingException("stwx is not implemented");
     }
 
+    @Override
+    public Object visitStwcx(LitmusPPCParser.StwcxContext ctx) {
+        // This instruction is usually followed by a branch instruction.
+        // Thus, the execution status of the store is saved in r0
+        // (the default register for branch conditions).
+        Register rs = programBuilder.getOrNewRegister(mainThread, "r0", types.getBooleanType());
+        Register r1 = (Register) ctx.register(0).accept(this);
+        Register ra = (Register) ctx.register(1).accept(this);
+        Register rb = (Register) ctx.register(2).accept(this);
+        return programBuilder.addChild(mainThread, EventFactory.Common.newExclusiveStore(rs, expressions.makeAdd(ra, rb), r1, ""));
+    }
+
     @Override
     public Object visitMr(LitmusPPCParser.MrContext ctx) {
-        Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
-        Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+        Register r1 = (Register) ctx.register(0).accept(this);
+        Register r2 = (Register) ctx.register(1).accept(this);
         return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, r2));
     }
 
     @Override
     public Object visitAddi(LitmusPPCParser.AddiContext ctx) {
-        Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
-        Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+        Register r1 = (Register) ctx.register(0).accept(this);
+        Register r2 = (Register) ctx.register(1).accept(this);
         IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType);
         return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, expressions.makeAdd(r2, constant)));
     }
 
     @Override
     public Object visitXor(LitmusPPCParser.XorContext ctx) {
-        Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType);
-        Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
-        Register r3 = programBuilder.getOrErrorRegister(mainThread, ctx.register(2).getText());
+        Register r1 = (Register) ctx.register(0).accept(this);
+        Register r2 = (Register) ctx.register(1).accept(this);
+        Register r3 = (Register) ctx.register(2).accept(this);
         return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, expressions.makeIntXor(r2, r3)));
     }
 
     @Override
     public Object visitCmpw(LitmusPPCParser.CmpwContext ctx) {
-        Register r1 = programBuilder.getOrErrorRegister(mainThread, ctx.register(0).getText());
-        Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText());
+        Register r1 = (Register) ctx.register(0).accept(this);
+        Register r2 = (Register) ctx.register(1).accept(this);
         lastCmpInstructionPerThread.put(mainThread, new CmpInstruction(r1, r2));
         return null;
     }
@@ -182,10 +202,11 @@ public Object visitCmpw(LitmusPPCParser.CmpwContext ctx) {
     public Object visitBranchCond(LitmusPPCParser.BranchCondContext ctx) {
         Label label = programBuilder.getOrCreateLabel(mainThread, ctx.Label().getText());
         CmpInstruction cmp = lastCmpInstructionPerThread.put(mainThread, null);
-        if(cmp == null){
-            throw new ParsingException("Invalid syntax near " + ctx.getText());
-        }
-        Expression expr = expressions.makeIntCmp(cmp.left, ctx.cond().op, cmp.right);
+        Expression expr = cmp == null ?
+            // In PPC, when there is no previous comparison instruction,
+            // the value of r0 is used as the branching condition
+            expressions.makeBooleanCast(programBuilder.getOrNewRegister(mainThread, "r0")) :
+            expressions.makeIntCmp(cmp.left, ctx.cond().op, cmp.right);
         return programBuilder.addChild(mainThread, EventFactory.newJump(expr, label));
     }
 
@@ -202,4 +223,10 @@ public Object visitFence(LitmusPPCParser.FenceContext ctx) {
         }
         throw new ParsingException("Unrecognised fence " + name);
     }
+
+    @Override
+    public Register visitRegister(LitmusPPCParser.RegisterContext ctx) {
+        return programBuilder.getOrNewRegister(mainThread, ctx.getText(), archType);
+    }
+
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java

@@ -8,6 +8,7 @@
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.Tag.C11;
+import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
 import com.dat3m.dartagnan.program.event.core.*;
 import com.dat3m.dartagnan.program.event.lang.catomic.*;
 import com.dat3m.dartagnan.program.event.lang.linux.*;
@@ -40,6 +41,20 @@ protected VisitorPower(boolean useRC11Scheme, PowerScheme cToPowerScheme) {
         this.cToPowerScheme = cToPowerScheme;
     }
 
+    // =============================================================================================
+    // ========================================= Common ============================================
+    // =============================================================================================
+
+    @Override
+    public List<Event> visitStoreExclusive(StoreExclusive e) {
+        RMWStoreExclusive store = newRMWStoreExclusiveWithMo(e.getAddress(), e.getMemValue(), true, e.getMo());
+
+        return eventSequence(
+                store,
+                newExecutionStatus(e.getResultRegister(), store)
+        );
+    }
+
     // =============================================================================================
     // ========================================= PTHREAD ===========================================
     // =============================================================================================

dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/WrongTargetTest.java

@@ -57,13 +57,4 @@ public void ARMCompiledToTSO() throws Exception {
         comp.setTarget(Arch.TSO);
         comp.run(p);
     }
-
-    @Test(expected = IllegalArgumentException.class)
-    public void ARMCompiledToPower() throws Exception {
-        Program p = new ProgramParser().parse(new File(getRootPath("litmus/AARCH64/ATOM/2+2W+poxxs.litmus")));
-        LoopUnrolling.newInstance().run(p);
-        Compilation comp = Compilation.newInstance();
-        comp.setTarget(Arch.POWER);
-        comp.run(p);
-    }
 }

dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusOpenClTest.java

@@ -1,7 +1,6 @@
 package com.dat3m.dartagnan.litmus;
 
 import com.dat3m.dartagnan.configuration.Arch;
-import com.dat3m.dartagnan.configuration.Property;
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.utils.rules.Provider;
 import com.dat3m.dartagnan.utils.rules.Providers;
@@ -10,7 +9,6 @@
 import org.junit.runners.Parameterized;
 
 import java.io.IOException;
-import java.util.EnumSet;
 
 @RunWith(Parameterized.class)
 public class LitmusOpenClTest extends AbstractLitmusTest {

dartagnan/src/test/resources/PPC-expected.csv

@@ -1334,6 +1334,7 @@ litmus/PPC/R+isyncs.litmus,1
 litmus/PPC/R+lwsync+isync.litmus,1
 litmus/PPC/R+lwsync+po.litmus,1
 litmus/PPC/R+lwsync+sync.litmus,1
+litmus/PPC/R+lwsync+sync+excl+sync.litmus,1
 litmus/PPC/R+lwsyncs.litmus,1
 litmus/PPC/R+po+isync.litmus,1
 litmus/PPC/R+po+lwsync.litmus,1

litmus/PPC/R+lwsync+sync+excl+sync.litmus

@@ -0,0 +1,21 @@
+PPC A
+"LwSyncdWW Coe SyncdWRNaA SyncdRRANa Fre"
+Generator=diyone7 (version 7.57+1)
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
+Com=Co Fr
+Orig=LwSyncdWW Coe SyncdWRNaA SyncdRRANa Fre
+{
+0:r2=x; 0:r4=y;
+1:r2=y; 1:r3=z; 1:r6=x;
+}
+ P0           | P1              ;
+ li r1,1      | li r1,2         ;
+ stw r1,0(r2) | stw r1,0(r2)    ;
+ lwsync       | sync            ;
+ li r3,1      | Loop00:         ;
+ stw r3,0(r4) | lwarx r4,r0,r3  ;
+              | stwcx. r4,r0,r3 ;
+              | bne  Loop00     ;
+              | sync            ;
+              | lwz r5,0(r6)    ;
+exists ([y]=2 /\ 1:r5=0)