Fix parsing of atomic_exchange for litmus C (#791)

Co-authored-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Dec 18, 2024 · e39d090 · e39d090
1 parent 69abc4c
commit e39d090
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/dartagnan/src/main/antlr4/C11Lexer.g4 b/dartagnan/src/main/antlr4/C11Lexer.g4
@@ -4,8 +4,8 @@ C11AtomicLoadExplicit         :   'atomic_load_explicit';
 C11AtomicLoad                 :   'atomic_load';
 C11AtomicStoreExplicit        :   'atomic_store_explicit';
 C11AtomicStore                :   'atomic_store';
-C11AtomicXchgExplicit         :   'atomic_exchange_explicit_explicit';
-C11AtomicXchg                 :   'atomic_exchange_explicit';
+C11AtomicXchgExplicit         :   'atomic_exchange_explicit';
+C11AtomicXchg                 :   'atomic_exchange';
 C11AtomicSCASExplicit         :   'atomic_compare_exchange_strong_explicit';
 C11AtomicSCAS                 :   'atomic_compare_exchange_strong';
 C11AtomicWCASExplicit         :   'atomic_compare_exchange_weak_explicit';

diff --git a/dartagnan/src/main/antlr4/LitmusC.g4 b/dartagnan/src/main/antlr4/LitmusC.g4
@@ -121,7 +121,7 @@ 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
+    |   C11AtomicXchg           LPar address = re Comma value = re RPar                                                                     # reC11AtomicXchg
     |   C11AtomicXchgExplicit   LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar                                    # reC11AtomicXchgExplicit
 
     |   ( AtomicCmpXchg        LPar address = re Comma cmp = re Comma value = re RPar {$mo = Linux.MO_MB;}

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
@@ -312,7 +312,7 @@ public Expression visitReC11AtomicXchg(LitmusCParser.ReC11AtomicXchgContext ctx)
         Register register = getReturnRegister(true);
         Expression value = (Expression) ctx.value.accept(this);
         Expression address = getAddress(ctx.address);
-        Event event = EventFactory.Atomic.newExchange(register, address, value, ctx.c11Mo().mo);
+        Event event = EventFactory.Atomic.newExchange(register, address, value, Tag.C11.MO_SC);
         addScopeTag(event, null);
         programBuilder.addChild(currentThread, event);
         return register;