From c6c73c8002d5546bc461653c9938eb7f5711c414 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 17 Jul 2025 21:45:25 +0800 Subject: [PATCH 1/7] Prototype support for atomic modify-write operations --- dartagnan/src/main/antlr4/C11Lexer.g4 | 10 +++++ dartagnan/src/main/antlr4/LitmusC.g4 | 11 ++++++ .../program/visitors/VisitorLitmusC.java | 7 ++++ .../dartagnan/program/event/EventFactory.java | 4 ++ .../dartagnan/program/event/EventVisitor.java | 1 + .../dat3m/dartagnan/program/event/Tag.java | 4 +- .../program/event/lang/catomic/AtomicOp.java | 37 +++++++++++++++++++ .../processing/compilation/VisitorC11.java | 18 +++++++++ 8 files changed, 91 insertions(+), 1 deletion(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicOp.java diff --git a/dartagnan/src/main/antlr4/C11Lexer.g4 b/dartagnan/src/main/antlr4/C11Lexer.g4 index 8807a9ca40..470d786895 100644 --- a/dartagnan/src/main/antlr4/C11Lexer.g4 +++ b/dartagnan/src/main/antlr4/C11Lexer.g4 @@ -21,3 +21,13 @@ C11AtomicXorExplicit : 'atomic_fetch_xor_explicit'; C11AtomicXor : 'atomic_fetch_xor'; C11AtomicAndExplicit : 'atomic_fetch_and_explicit'; C11AtomicAnd : 'atomic_fetch_and'; +C11StoreAddExplicit : 'atomic_store_add_explicit'; +C11StoreAdd : 'atomic_store_add'; +C11StoreSubExplicit : 'atomic_store_sub_explicit'; +C11StoreSub : 'atomic_store_sub'; +C11StoreOrExplicit : 'atomic_store_or_explicit'; +C11StoreOr : 'atomic_store_or'; +C11StoreXorExplicit : 'atomic_store_xor_explicit'; +C11StoreXor : 'atomic_store_xor'; +C11StoreAndExplicit : 'atomic_store_and_explicit'; +C11StoreAnd : 'atomic_store_and'; diff --git a/dartagnan/src/main/antlr4/LitmusC.g4 b/dartagnan/src/main/antlr4/LitmusC.g4 index 3e80a23e1b..c2d7408bdf 100644 --- a/dartagnan/src/main/antlr4/LitmusC.g4 +++ b/dartagnan/src/main/antlr4/LitmusC.g4 @@ -179,6 +179,17 @@ nre locals [IntBinaryOp op, String mo, String name] | AtomicInc LPar address = re RPar {$op = IntBinaryOp.ADD;} | AtomicDec LPar address = re RPar {$op = IntBinaryOp.SUB;}) # nreAtomicOp + | ( C11StoreAddExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.ADD;} + | C11StoreAdd LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.ADD;} + | C11StoreSubExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.SUB;} + | C11StoreSub LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.SUB;} + | C11StoreAndExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.AND;} + | C11StoreAnd LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.AND;} + | C11StoreOrExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.OR;} + | C11StoreOr LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.OR;} + | C11StoreXorExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.XOR;} + | C11StoreXor LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.XOR;}) # nreC11AtomicOp + | ( AtomicSet LPar address = re Comma value = re RPar {$mo = Linux.MO_ONCE;} | AtomicSetRelease LPar address = re Comma value = re RPar {$mo = Linux.MO_RELEASE;} | SmpStoreRelease LPar address = re Comma value = re RPar {$mo = Linux.MO_RELEASE;} 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 1b9df82763..45dacaf7e7 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 @@ -534,6 +534,13 @@ public Object visitNreAtomicOp(LitmusCParser.NreAtomicOpContext ctx){ return programBuilder.addChild(currentThread, event); } + @Override + public Object visitNreC11AtomicOp(LitmusCParser.NreC11AtomicOpContext ctx){ + Expression value = returnExpressionOrOne(ctx.value); + Event event = EventFactory.Atomic.newRMWOp(getAddress(ctx.address), value, ctx.op, ctx.c11Mo().mo); + return programBuilder.addChild(currentThread, event); + } + @Override public Object visitNreStore(LitmusCParser.NreStoreContext ctx){ Expression value = (Expression)ctx.value.accept(this); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java index 5db66bebb8..a0c4ea414f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java @@ -441,6 +441,10 @@ public static AtomicFetchOp newFADD(Register register, Expression address, Expre return newFetchOp(register, address, value, IntBinaryOp.ADD, mo); } + public static AtomicOp newRMWOp(Expression address, Expression value, IntBinaryOp op, String mo) { + return new AtomicOp(address, op, value, mo); + } + public static AtomicFetchOp newIncrement(Register register, Expression address, String mo) { if (!(register.getType() instanceof IntegerType integerType)) { throw new IllegalArgumentException( diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java index a811bb2730..a57cadf5aa 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java @@ -83,6 +83,7 @@ public interface EventVisitor { default T visitAtomicStore(AtomicStore e) { return visitMemEvent(e); } default T visitAtomicThreadFence(AtomicThreadFence e) { return visitEvent(e); } default T visitAtomicXchg(AtomicXchg e) { return visitMemEvent(e); } + default T visitAtomicOp(AtomicOp e) { return visitMemEvent(e); } // ------------------ LLVM Events ------------------ default T visitLlvmCmpXchg(LlvmCmpXchg e) { return visitMemEvent(e); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java index 825c8e4642..0982b7b969 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -130,7 +130,9 @@ private C11() { public static final String MO_ACQUIRE_RELEASE = "ACQ_REL"; public static final String MO_SC = "SC"; - public static final String DEFAULT_MO = MO_SC; + public static final String DEFAULT_MO = MO_SC; + + public static final String NORETURN = "Noreturn"; public static String intToMo(int i) { switch (i) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicOp.java new file mode 100644 index 0000000000..9556f26369 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicOp.java @@ -0,0 +1,37 @@ +package com.dat3m.dartagnan.program.event.lang.catomic; + +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.integers.IntBinaryOp; +import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; +import com.dat3m.dartagnan.program.event.common.RMWOpBase; +import com.dat3m.dartagnan.program.event.Tag; +import com.google.common.base.Preconditions; + +public class AtomicOp extends RMWOpBase { + + public AtomicOp(Expression address, IntBinaryOp operator, Expression operand, String mo) { + super(address, operator, operand, mo); + Preconditions.checkArgument(!mo.isEmpty(), "Atomic events cannot have empty memory order"); + addTags(Tag.C11.NORETURN); + } + + private AtomicOp(AtomicOp other) { + super(other); + } + + @Override + public String defaultString() { + return String.format("atomic_store_%s(*%s, %s, %s)\t### C11", operator.getName(), address, operand, mo); + } + + @Override + public AtomicOp getCopy() { + return new AtomicOp(this); + } + + @Override + public T accept(EventVisitor visitor) { + return visitor.visitAtomicOp(this); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java index 7fc14ea2f6..89a419c314 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java @@ -4,6 +4,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.type.BooleanType; +import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; @@ -91,6 +92,23 @@ public List visitAtomicFetchOp(AtomicFetchOp e) { )); } + @Override + public List visitAtomicOp(AtomicOp e) { + Expression address = e.getAddress(); + String mo = e.getMo(); + + Register dummyReg = e.getFunction().newRegister(TypeFactory.getInstance().getArchType()); + Load load = newRMWLoad(dummyReg, address); + Local localOp = newLocal(dummyReg, expressions.makeIntBinary(dummyReg, e.getOperator(), e.getOperand())); + RMWStore store = newRMWStoreWithMo(load, address, dummyReg, Tag.C11.storeMO(mo)); + + return tagList(e, eventSequence( + load, + localOp, + store + )); + } + @Override public List visitAtomicLoad(AtomicLoad e) { return tagList(e, eventSequence( From 413b210aa6a09580400d0c1fbe03272e439ed2c4 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 12 Feb 2026 15:42:15 +0100 Subject: [PATCH 2/7] Add c26 header for atomic (reduction) ops Implemented first support for atomic reduction ops (only for C-code yet). --- .../program/processing/Intrinsics.java | 40 ++++++++++++++++++- .../processing/compilation/VisitorC11.java | 6 ++- include/c26.h | 39 ++++++++++++++++++ 3 files changed, 81 insertions(+), 4 deletions(-) create mode 100644 include/c26.h diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index c2ea7eb480..ed3547dd8f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -208,6 +208,8 @@ public enum Info { LLVM_MEMCPY("llvm.memcpy", true, true, true, false, Intrinsics::inlineMemCpy), LLVM_MEMSET("llvm.memset", true, false, true, false, Intrinsics::inlineMemSet), LLVM_THREADLOCAL("llvm.threadlocal.address.p0", false, false, true, true, Intrinsics::inlineLLVMThreadLocal), + // --------------------------- C26 --------------------------- + C26_ATOMIC_OP("__C26_atomic_op", true, true, true, true, Intrinsics::handleC26AtomicOP), // --------------------------- LKMM --------------------------- LKMM_LOAD("__LKMM_load", false, true, true, true, Intrinsics::handleLKMMIntrinsic), LKMM_STORE("__LKMM_store", true, false, true, true, Intrinsics::handleLKMMIntrinsic), @@ -289,7 +291,7 @@ public boolean isEarly() { private boolean matches(String funcName) { boolean isPrefix = switch(this) { - case LLVM, LLVM_ASSUME, LLVM_META, LLVM_MEMCPY, LLVM_MEMSET, LLVM_EXPECT, LLVM_OBJECTSIZE -> true; + case LLVM, LLVM_ASSUME, LLVM_META, LLVM_MEMCPY, LLVM_MEMSET, LLVM_EXPECT, LLVM_OBJECTSIZE, C26_ATOMIC_OP -> true; default -> false; }; BiPredicate matchingFunction = isPrefix ? String::startsWith : String::equals; @@ -297,7 +299,6 @@ private boolean matches(String funcName) { } } - @FunctionalInterface private interface Replacer { List replace(Intrinsics self, FunctionCall call); @@ -1406,6 +1407,41 @@ private Expression checkIfValueInRangeOfType(Expression value, IntegerType integ ); } + // -------------------------------------------------------------------------------------------------------- + // C26 atomics + + private IntBinaryOp toCOp(Expression opCode) { + if (!(opCode instanceof IntLiteral literal)) { + throw new UnsupportedOperationException("Variable op code \"" + opCode + "\""); + } + return switch (literal.getValueAsInt()) { + case 0 -> IntBinaryOp.ADD; + case 1 -> IntBinaryOp.SUB; + case 2 -> IntBinaryOp.AND; + case 3 -> IntBinaryOp.OR; + case 4 -> IntBinaryOp.XOR; + default -> throw new UnsupportedOperationException("Operation \"" + literal.getValueAsInt() + "\" not yet supported"); + }; + } + + private String toCMemoryOrder(Expression moCode) { + if (!(moCode instanceof IntLiteral literal)) { + throw new UnsupportedOperationException("Variable memory order \"" + moCode + "\""); + } + return Tag.C11.intToMo(literal.getValueAsInt()); + } + + private List handleC26AtomicOP(FunctionCall call) { + final Expression address = call.getArguments().get(0); + final Expression value = call.getArguments().get(1); + final Expression opCode = call.getArguments().get(2); + final Expression moCode = call.getArguments().get(3); + + return List.of( + EventFactory.Atomic.newRMWOp(address, value, toCOp(opCode), toCMemoryOrder(moCode)) + ); + } + // -------------------------------------------------------------------------------------------------------- // LKMM intrinsics diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java index 89a419c314..4a4d363c8a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java @@ -4,7 +4,6 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.type.BooleanType; -import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; @@ -97,11 +96,14 @@ public List visitAtomicOp(AtomicOp e) { Expression address = e.getAddress(); String mo = e.getMo(); - Register dummyReg = e.getFunction().newRegister(TypeFactory.getInstance().getArchType()); + Register dummyReg = e.getFunction().newRegister(e.getAccessType()); Load load = newRMWLoad(dummyReg, address); Local localOp = newLocal(dummyReg, expressions.makeIntBinary(dummyReg, e.getOperator(), e.getOperand())); RMWStore store = newRMWStoreWithMo(load, address, dummyReg, Tag.C11.storeMO(mo)); + load.addTags(Tag.C11.NORETURN); + store.addTags(Tag.C11.NORETURN); + return tagList(e, eventSequence( load, localOp, diff --git a/include/c26.h b/include/c26.h new file mode 100644 index 0000000000..13c08422a6 --- /dev/null +++ b/include/c26.h @@ -0,0 +1,39 @@ + +typedef enum { + __C26_op_add, + __C26_op_sub, + __C26_op_and, + __C26_op_or, + __C26_op_xor, + __C26_op_min, + __C26_op_max, +} __C26_op; + +#define __C26__DECLARE_ATOMIC_OP(type) \ + extern void __C26_atomic_op_##type(_Atomic(type)* ptr, type value, __C26_op, memory_order); + +__C26__DECLARE_ATOMIC_OP(short) +__C26__DECLARE_ATOMIC_OP(int) +__C26__DECLARE_ATOMIC_OP(long) + +#define __SELECT(p) _Generic((p), \ + _Atomic(short)* : __C26_atomic_op_short, \ + _Atomic(int)* : __C26_atomic_op_int, \ + _Atomic(long)* : __C26_atomic_op_long \ +) + +#define atomic_add_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_add, mo) +#define atomic_sub_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_sub, mo) +#define atomic_and_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_and, mo) +#define atomic_or_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_or, mo) +#define atomic_xor_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_xor, mo) +#define atomic_min_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_min, mo) +#define atomic_max_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_max, mo) + +#define atomic_add(p, v) __SELECT(p)(p, v, __C26_op_add, memory_order_seq_cst) +#define atomic_sub(p, v) __SELECT(p)(p, v, __C26_op_sub, memory_order_seq_cst) +#define atomic_and(p, v) __SELECT(p)(p, v, __C26_op_and, memory_order_seq_cst) +#define atomic_or(p, v) __SELECT(p)(p, v, __C26_op_or, memory_order_seq_cst) +#define atomic_xor(p, v) __SELECT(p)(p, v, __C26_op_xor, memory_order_seq_cst) +#define atomic_min(p, v) __SELECT(p)(p, v, __C26_op_min, memory_order_seq_cst) +#define atomic_max(p, v) __SELECT(p)(p, v, __C26_op_max, memory_order_seq_cst) From ba69de3c6e74aeb608a39bce945365207683b514 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 16 Feb 2026 20:11:44 +0100 Subject: [PATCH 3/7] Rename C26 reduction operators --- include/c26.h | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/include/c26.h b/include/c26.h index 13c08422a6..48c1ee36f3 100644 --- a/include/c26.h +++ b/include/c26.h @@ -22,18 +22,20 @@ __C26__DECLARE_ATOMIC_OP(long) _Atomic(long)* : __C26_atomic_op_long \ ) -#define atomic_add_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_add, mo) -#define atomic_sub_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_sub, mo) -#define atomic_and_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_and, mo) -#define atomic_or_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_or, mo) -#define atomic_xor_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_xor, mo) -#define atomic_min_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_min, mo) -#define atomic_max_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_max, mo) +// NOTE: for min/max we only have the signed version for now. -#define atomic_add(p, v) __SELECT(p)(p, v, __C26_op_add, memory_order_seq_cst) -#define atomic_sub(p, v) __SELECT(p)(p, v, __C26_op_sub, memory_order_seq_cst) -#define atomic_and(p, v) __SELECT(p)(p, v, __C26_op_and, memory_order_seq_cst) -#define atomic_or(p, v) __SELECT(p)(p, v, __C26_op_or, memory_order_seq_cst) -#define atomic_xor(p, v) __SELECT(p)(p, v, __C26_op_xor, memory_order_seq_cst) -#define atomic_min(p, v) __SELECT(p)(p, v, __C26_op_min, memory_order_seq_cst) -#define atomic_max(p, v) __SELECT(p)(p, v, __C26_op_max, memory_order_seq_cst) +#define atomic_store_add_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_add, mo) +#define atomic_store_sub_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_sub, mo) +#define atomic_store_and_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_and, mo) +#define atomic_store_or_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_or, mo) +#define atomic_store_xor_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_xor, mo) +#define atomic_store_min_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_min, mo) +#define atomic_store_max_explicit(p, v, mo) __SELECT(p)(p, v, __C26_op_max, mo) + +#define atomic_store_add(p, v) __SELECT(p)(p, v, __C26_op_add, memory_order_seq_cst) +#define atomic_store_sub(p, v) __SELECT(p)(p, v, __C26_op_sub, memory_order_seq_cst) +#define atomic_store_and(p, v) __SELECT(p)(p, v, __C26_op_and, memory_order_seq_cst) +#define atomic_store_or(p, v) __SELECT(p)(p, v, __C26_op_or, memory_order_seq_cst) +#define atomic_store_xor(p, v) __SELECT(p)(p, v, __C26_op_xor, memory_order_seq_cst) +#define atomic_store_min(p, v) __SELECT(p)(p, v, __C26_op_min, memory_order_seq_cst) +#define atomic_store_max(p, v) __SELECT(p)(p, v, __C26_op_max, memory_order_seq_cst) From dfea4c636bc03eeb832ae5a34589ccc98aa9c80f Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 16 Feb 2026 20:28:06 +0100 Subject: [PATCH 4/7] Add min/max operators to C --- dartagnan/src/main/antlr4/C11Lexer.g4 | 4 +++ dartagnan/src/main/antlr4/LitmusC.g4 | 6 +++- .../program/processing/Intrinsics.java | 29 ++++++++++++++----- 3 files changed, 30 insertions(+), 9 deletions(-) diff --git a/dartagnan/src/main/antlr4/C11Lexer.g4 b/dartagnan/src/main/antlr4/C11Lexer.g4 index 470d786895..3457a56925 100644 --- a/dartagnan/src/main/antlr4/C11Lexer.g4 +++ b/dartagnan/src/main/antlr4/C11Lexer.g4 @@ -31,3 +31,7 @@ C11StoreXorExplicit : 'atomic_store_xor_explicit'; C11StoreXor : 'atomic_store_xor'; C11StoreAndExplicit : 'atomic_store_and_explicit'; C11StoreAnd : 'atomic_store_and'; +C11StoreMinExplicit : 'atomic_store_min_explicit'; +C11StoreMin : 'atomic_store_min'; +C11StoreMaxExplicit : 'atomic_store_max_explicit'; +C11StoreMax : 'atomic_store_max'; diff --git a/dartagnan/src/main/antlr4/LitmusC.g4 b/dartagnan/src/main/antlr4/LitmusC.g4 index c2d7408bdf..95793bff90 100644 --- a/dartagnan/src/main/antlr4/LitmusC.g4 +++ b/dartagnan/src/main/antlr4/LitmusC.g4 @@ -188,7 +188,11 @@ nre locals [IntBinaryOp op, String mo, String name] | C11StoreOrExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.OR;} | C11StoreOr LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.OR;} | C11StoreXorExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.XOR;} - | C11StoreXor LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.XOR;}) # nreC11AtomicOp + | C11StoreXor LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.XOR;} + | C11StoreMinExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.SMIN;} + | C11StoreMin LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.SMIN;} + | C11StoreMaxExplicit LPar address = re Comma value = re Comma c11Mo (Comma openCLScope)? RPar {$op = IntBinaryOp.SMAX;} + | C11StoreMax LPar address = re Comma value = re (Comma openCLScope)? RPar {$op = IntBinaryOp.SMAX;}) # nreC11AtomicOp | ( AtomicSet LPar address = re Comma value = re RPar {$mo = Linux.MO_ONCE;} | AtomicSetRelease LPar address = re Comma value = re RPar {$mo = Linux.MO_RELEASE;} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index ed3547dd8f..6e2fb3c20c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -21,6 +21,7 @@ import com.dat3m.dartagnan.program.event.functions.ValueFunctionCall; import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic; import com.dat3m.dartagnan.program.memory.MemoryObject; +import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableList; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -1410,18 +1411,30 @@ private Expression checkIfValueInRangeOfType(Expression value, IntegerType integ // -------------------------------------------------------------------------------------------------------- // C26 atomics + private enum COp { + // WARNING: The order here must match with the enum defined in c26.h + C_ADD(IntBinaryOp.ADD), + C_SUB(IntBinaryOp.SUB), + C_AND(IntBinaryOp.AND), + C_OR(IntBinaryOp.OR), + C_XOR(IntBinaryOp.XOR), + C_MIN(IntBinaryOp.SMIN), + C_MAX(IntBinaryOp.SMAX); + + private final IntBinaryOp op; + COp(IntBinaryOp op) { + this.op = op; + } + } + private IntBinaryOp toCOp(Expression opCode) { if (!(opCode instanceof IntLiteral literal)) { throw new UnsupportedOperationException("Variable op code \"" + opCode + "\""); } - return switch (literal.getValueAsInt()) { - case 0 -> IntBinaryOp.ADD; - case 1 -> IntBinaryOp.SUB; - case 2 -> IntBinaryOp.AND; - case 3 -> IntBinaryOp.OR; - case 4 -> IntBinaryOp.XOR; - default -> throw new UnsupportedOperationException("Operation \"" + literal.getValueAsInt() + "\" not yet supported"); - }; + final COp[] cOps = COp.values(); + final int index = literal.getValue().intValueExact(); + Preconditions.checkArgument(0 <= index && index < cOps.length, "Invalid op code %s", opCode); + return cOps[index].op; } private String toCMemoryOrder(Expression moCode) { From 38cdfdd57402fa300ee0d1d0f6c1e54dbe165933 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 17 Feb 2026 18:18:54 +0100 Subject: [PATCH 5/7] Make the loads of atomic_store_op compilation atomic, even though they are have no memory order (~plain). --- .../dartagnan/program/processing/compilation/VisitorC11.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java index 4a4d363c8a..9ec7f7c79c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java @@ -97,11 +97,11 @@ public List visitAtomicOp(AtomicOp e) { String mo = e.getMo(); Register dummyReg = e.getFunction().newRegister(e.getAccessType()); - Load load = newRMWLoad(dummyReg, address); + Load load = newRMWLoad(dummyReg, address);); Local localOp = newLocal(dummyReg, expressions.makeIntBinary(dummyReg, e.getOperator(), e.getOperand())); RMWStore store = newRMWStoreWithMo(load, address, dummyReg, Tag.C11.storeMO(mo)); - load.addTags(Tag.C11.NORETURN); + load.addTags(C11.ATOMIC, Tag.C11.NORETURN); // Note that the load has no mo, but is still atomic! store.addTags(Tag.C11.NORETURN); return tagList(e, eventSequence( From 497ae55aae204b761d578eda5bf3f20b8f8fe713 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 17 Feb 2026 18:21:05 +0100 Subject: [PATCH 6/7] Fix accidental compilation error --- .../dartagnan/program/processing/compilation/VisitorC11.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java index 9ec7f7c79c..b4cee05f19 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java @@ -97,7 +97,7 @@ public List visitAtomicOp(AtomicOp e) { String mo = e.getMo(); Register dummyReg = e.getFunction().newRegister(e.getAccessType()); - Load load = newRMWLoad(dummyReg, address);); + Load load = newRMWLoad(dummyReg, address); Local localOp = newLocal(dummyReg, expressions.makeIntBinary(dummyReg, e.getOperator(), e.getOperand())); RMWStore store = newRMWStoreWithMo(load, address, dummyReg, Tag.C11.storeMO(mo)); From 1ca78bc7875f1af4d41b74b15b433638ee73e5d9 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Wed, 25 Feb 2026 21:35:19 +0800 Subject: [PATCH 7/7] Noreturn -> NORETURN Signed-off-by: Hernan Ponce de Leon --- .../src/main/java/com/dat3m/dartagnan/program/event/Tag.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java index 0982b7b969..e0aa8b5fb6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -132,7 +132,7 @@ private C11() { public static final String DEFAULT_MO = MO_SC; - public static final String NORETURN = "Noreturn"; + public static final String NORETURN = "NORETURN"; public static String intToMo(int i) { switch (i) {