Use newExclusiveStore for stwcx instruction

Signed-off-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Oct 26, 2024 · 4d72f2e · 4d72f2e
1 parent 2525f05
commit 4d72f2e
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 1 deletion.
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
@@ -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
@@ -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 ===========================================
     // =============================================================================================