From e39d0905fbc54b7024ff605077f3cc7aa5f319c1 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Wed, 18 Dec 2024 09:12:10 +0100 Subject: [PATCH] Fix parsing of atomic_exchange for litmus C (#791) Co-authored-by: Hernan Ponce de Leon --- dartagnan/src/main/antlr4/C11Lexer.g4 | 4 ++-- dartagnan/src/main/antlr4/LitmusC.g4 | 2 +- .../dartagnan/parsers/program/visitors/VisitorLitmusC.java | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/dartagnan/src/main/antlr4/C11Lexer.g4 b/dartagnan/src/main/antlr4/C11Lexer.g4 index 9286970606..9497948dd0 100644 --- 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 index 236ea27377..95b08d7a5e 100644 --- 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 index b83da951a8..ab82897202 100644 --- 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;