diff --git a/dartagnan/src/main/antlr4/LitmusAssertions.g4 b/dartagnan/src/main/antlr4/LitmusAssertions.g4 index 8b3df0ccff..8086c2d3b5 100644 --- a/dartagnan/src/main/antlr4/LitmusAssertions.g4 +++ b/dartagnan/src/main/antlr4/LitmusAssertions.g4 @@ -28,6 +28,7 @@ assertion assertionValue : varName LBracket DigitSequence RBracket | varName + | LBracket varName RBracket | threadId Colon varName | constant ; diff --git a/dartagnan/src/main/antlr4/LitmusPPC.g4 b/dartagnan/src/main/antlr4/LitmusPPC.g4 index 385f2a818c..804264da81 100644 --- a/dartagnan/src/main/antlr4/LitmusPPC.g4 +++ b/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,6 +198,9 @@ Bge Li : 'li' ; +Lwarx: 'lwarx' + ; + Lwzx: 'lwzx' ; @@ -194,6 +208,10 @@ Lwz : 'lwz' ; +Stwcx + : 'stwcx.' + ; + Stwx : 'stwx' ; @@ -223,7 +241,7 @@ Register ; Label - : 'LC' DigitSequence + : 'L' Identifier ; LitmusLanguage diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java index a26bda4444..11a8921282 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java +++ b/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); + } + } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java index 7203312258..7f680aa8c9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java +++ b/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 visitStoreExclusive(StoreExclusive e) { + RMWStoreExclusive store = newRMWStoreExclusiveWithMo(e.getAddress(), e.getMemValue(), true, e.getMo()); + + return eventSequence( + store, + newExecutionStatus(e.getResultRegister(), store) + ); + } + // ============================================================================================= // ========================================= PTHREAD =========================================== // ============================================================================================= diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/WrongTargetTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/WrongTargetTest.java index fa35c086e0..958f5216c9 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/WrongTargetTest.java +++ b/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); - } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusOpenClTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusOpenClTest.java index ef686b6bb2..9ff8546ca0 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusOpenClTest.java +++ b/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 { diff --git a/dartagnan/src/test/resources/PPC-expected.csv b/dartagnan/src/test/resources/PPC-expected.csv index 3f07bf8e36..cd5cc0b213 100644 --- a/dartagnan/src/test/resources/PPC-expected.csv +++ b/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 diff --git a/litmus/PPC/R+lwsync+sync+excl+sync.litmus b/litmus/PPC/R+lwsync+sync+excl+sync.litmus new file mode 100644 index 0000000000..8dcba21d3c --- /dev/null +++ b/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) \ No newline at end of file