Add support for atomic_exchange_explicit in litmus code (#740)

Signed-off-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Sep 20, 2024 · 90c3a7b · 90c3a7b
1 parent 690a283
commit 90c3a7b
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 0 deletions.
diff --git a/dartagnan/src/main/antlr4/C11Lexer.g4 b/dartagnan/src/main/antlr4/C11Lexer.g4
@@ -2,6 +2,7 @@ lexer grammar C11Lexer;
 
 C11AtomicLoad                 :   'atomic_load_explicit';
 C11AtomicStore                :   'atomic_store_explicit';
+C11AtomicXchg                 :   'atomic_exchange_explicit';
 C11AtomicSCAS                 :   'atomic_compare_exchange_strong_explicit';
 C11AtomicWCAS                 :   'atomic_compare_exchange_weak_explicit';
 C11AtomicFence                :   'atomic_thread_fence';

diff --git a/dartagnan/src/main/antlr4/LitmusC.g4 b/dartagnan/src/main/antlr4/LitmusC.g4
@@ -108,6 +108,8 @@ re locals [IntBinaryOp op, String mo]
         | XchgAcquire LPar address = re Comma value = re RPar {$mo = Linux.MO_ACQUIRE;}
         | XchgRelease LPar address = re Comma value = re RPar {$mo = Linux.MO_RELEASE;})                                # reXchg
 
+    |   C11AtomicXchg   LPar address = re Comma value = re Comma c11Mo RPar                                             # reC11AtomicXchg
+
     |   ( AtomicCmpXchg        LPar address = re Comma cmp = re Comma value = re RPar {$mo = Linux.MO_MB;}
         | AtomicCmpXchgRelaxed LPar address = re Comma cmp = re Comma value = re RPar {$mo = Linux.MO_RELAXED;}
         | AtomicCmpXchgAcquire LPar address = re Comma cmp = re Comma value = re RPar {$mo = Linux.MO_ACQUIRE;}

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java
@@ -277,6 +277,15 @@ public Expression visitReAtomicAddUnless(LitmusCParser.ReAtomicAddUnlessContext
         return register;
     }
 
+    @Override
+    public Expression visitReC11AtomicXchg(LitmusCParser.ReC11AtomicXchgContext ctx) {
+        Register register = getReturnRegister(true);
+        Expression value = (Expression) ctx.value.accept(this);
+        Event event = EventFactory.Atomic.newExchange(register, getAddress(ctx.address), value, ctx.c11Mo().mo);
+        programBuilder.addChild(currentThread, event);
+        return register;
+    }
+
     @Override
     public Expression visitReXchg(LitmusCParser.ReXchgContext ctx){
         Register register = getReturnRegister(true);