diff --git a/dartagnan/src/main/antlr4/C11Lexer.g4 b/dartagnan/src/main/antlr4/C11Lexer.g4 index ed74f0632e..b825e063ef 100644 --- 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 index 17d56d3760..644c7abcca 100644 --- 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 index bbdd3df887..7f73d7e15f 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 @@ -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);