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 fd2d3edb22..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 @@ -157,10 +157,14 @@ public Object visitStwx(LitmusPPCParser.StwxContext ctx) { @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.Power.newRMWStoreConditional(expressions.makeAdd(ra, rb), r1, true)); + return programBuilder.addChild(mainThread, EventFactory.Common.newExclusiveStore(rs, expressions.makeAdd(ra, rb), r1, "")); } @Override 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<Event> visitStoreExclusive(StoreExclusive e) { + RMWStoreExclusive store = newRMWStoreExclusiveWithMo(e.getAddress(), e.getMemValue(), true, e.getMo()); + + return eventSequence( + store, + newExecutionStatus(e.getResultRegister(), store) + ); + } + // ============================================================================================= // ========================================= PTHREAD =========================================== // =============================================================================================