[DRAFT] Expression templates and generic RMW events

dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java

@@ -4,6 +4,7 @@
 import com.dat3m.dartagnan.expression.booleans.*;
 import com.dat3m.dartagnan.expression.floats.*;
 import com.dat3m.dartagnan.expression.integers.*;
+import com.dat3m.dartagnan.expression.misc.ExprHole;
 import com.dat3m.dartagnan.expression.misc.GEPExpr;
 import com.dat3m.dartagnan.expression.misc.ITEExpr;
 import com.dat3m.dartagnan.expression.type.*;
@@ -404,6 +405,10 @@ public ScopedPointerVariable makeScopedPointerVariable(String id, ScopedPointerT
     // -----------------------------------------------------------------------------------------------------------------
     // Misc
 
+    public Expression makeHole(Type type) {
+        return new ExprHole(type);
+    }
+
     public Expression makeGeneralZero(Type type) {
         if (type instanceof ArrayType arrayType) {
             Expression zero = makeGeneralZero(arrayType.getElementType());

dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java

@@ -9,6 +9,7 @@
 import com.dat3m.dartagnan.expression.booleans.BoolUnaryExpr;
 import com.dat3m.dartagnan.expression.floats.*;
 import com.dat3m.dartagnan.expression.integers.*;
+import com.dat3m.dartagnan.expression.misc.ExprHole;
 import com.dat3m.dartagnan.expression.misc.GEPExpr;
 import com.dat3m.dartagnan.expression.misc.ITEExpr;
 import com.dat3m.dartagnan.program.Function;
@@ -59,6 +60,7 @@ public interface ExpressionVisitor<TRet> {
     default TRet visitGEPExpression(GEPExpr expr) { return visitExpression(expr); }
 
     // =================================== Generic ===================================
+    default TRet visitExprHole(ExprHole hole) { return visitLeafExpression(hole); }
     default TRet visitITEExpression(ITEExpr expr) { return visitExpression(expr); }
 
     // =================================== Program-specific ===================================

dartagnan/src/main/java/com/dat3m/dartagnan/expression/misc/ExprHole.java

@@ -0,0 +1,38 @@
+package com.dat3m.dartagnan.expression.misc;
+
+import com.dat3m.dartagnan.expression.ExpressionKind;
+import com.dat3m.dartagnan.expression.ExpressionVisitor;
+import com.dat3m.dartagnan.expression.Type;
+import com.dat3m.dartagnan.expression.base.LeafExpressionBase;
+
+/*
+    A typed hole expression: can be used to make expression templates
+    where the hole gets later replaced by some concrete expression of the correct type.
+    TODO: Possibly add identifiers to allow to distinguish between different holes.
+ */
+public class ExprHole extends LeafExpressionBase<Type> {
+
+    public ExprHole(Type type) {
+        super(type);
+    }
+
+    @Override
+    public ExpressionKind getKind() {
+        return () -> "HOLE";
+    }
+
+    @Override
+    public String toString() {
+        return String.format("%s {_}", type);
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        return obj instanceof ExprHole other && type.equals(other.type);
+    }
+
+    @Override
+    public <T> T accept(ExpressionVisitor<T> visitor) {
+        return visitor.visitExprHole(this);
+    }
+}

dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java

@@ -12,9 +12,11 @@
 import com.dat3m.dartagnan.expression.booleans.BoolUnaryExpr;
 import com.dat3m.dartagnan.expression.floats.*;
 import com.dat3m.dartagnan.expression.integers.*;
+import com.dat3m.dartagnan.expression.misc.ExprHole;
 import com.dat3m.dartagnan.expression.misc.GEPExpr;
 import com.dat3m.dartagnan.expression.misc.ITEExpr;
 import com.dat3m.dartagnan.expression.type.TypeFactory;
+import com.google.common.base.Preconditions;
 
 import java.util.ArrayList;
 
@@ -23,6 +25,16 @@ public abstract class ExprTransformer implements ExpressionVisitor<Expression> {
     protected final TypeFactory types = TypeFactory.getInstance();
     protected final ExpressionFactory expressions = ExpressionFactory.getInstance();
 
+    public static Expression replaceHole(Expression exprTemplate, Expression replacement) {
+        return exprTemplate.accept(new ExprTransformer() {
+            @Override
+            public Expression visitExprHole(ExprHole hole) {
+                Preconditions.checkArgument(hole.getType().equals(replacement.getType()));
+                return replacement;
+            }
+        });
+    }
+
     @Override
     public Expression visitBoolBinaryExpression(BoolBinaryExpr expr) {
         return expressions.makeBoolBinary(expr.getLeft().accept(this), expr.getKind(), expr.getRight().accept(this));

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java

@@ -38,7 +38,7 @@
 
 import static com.dat3m.dartagnan.expression.utils.ExpressionHelper.isAggregateLike;
 import static com.dat3m.dartagnan.program.event.EventFactory.*;
-import static com.dat3m.dartagnan.program.event.EventFactory.Llvm.newCompareExchange;
+import static com.dat3m.dartagnan.program.event.EventFactory.Llvm.newCompareExchangeAlt;
 import static com.google.common.base.Preconditions.checkState;
 import static com.google.common.base.Verify.verify;
 
@@ -806,7 +806,7 @@ public Expression visitSelectInst(SelectInstContext ctx) {
     public Expression visitCmpXchgInst(CmpXchgInstContext ctx) {
         // see https://llvm.org/docs/LangRef.html#cmpxchg-instruction
         // TODO LLVM has no distinguished boolean type.
-        final Expression address = visitTypeValue(ctx.typeValue(0));
+        /*final Expression address = visitTypeValue(ctx.typeValue(0));
         final Expression comparator = visitTypeValue(ctx.typeValue(1));
         final Expression substitute = visitTypeValue(ctx.typeValue(2));
         check(comparator.getType().equals(substitute.getType()), "Type mismatch for comparator and new in %s.", ctx);
@@ -823,6 +823,20 @@ public Expression visitCmpXchgInst(CmpXchgInstContext ctx) {
             final Expression result = expressions.makeConstruct(type, List.of(value, cast));
             block.events.add(newLocal(register, result));
         }
+        return register;*/
+
+        // TODO: THIS IS JUST TEST CODE
+        final Expression address = visitTypeValue(ctx.typeValue(0));
+        final Expression comparator = visitTypeValue(ctx.typeValue(1));
+        final Expression substitute = visitTypeValue(ctx.typeValue(2));
+        check(comparator.getType().equals(substitute.getType()), "Type mismatch for comparator and new in %s.", ctx);
+        final boolean weak = ctx.weak != null;
+        final String mo = parseMemoryOrder(ctx.atomicOrdering(0));
+
+        final Register register = currentRegisterName == null ? null :
+                getOrNewCurrentRegister(types.getAggregateType(List.of(comparator.getType(), getIntegerType(1))));
+
+        block.events.add(newCompareExchangeAlt(register, address, comparator, substitute, mo, weak));
         return register;
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java

@@ -28,17 +28,20 @@
 import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker;
 import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker;
 import com.dat3m.dartagnan.program.event.core.annotations.StringAnnotation;
-import com.dat3m.dartagnan.program.event.core.InstructionBoundary;
 import com.dat3m.dartagnan.program.event.core.special.StateSnapshot;
 import com.dat3m.dartagnan.program.event.core.threading.*;
 import com.dat3m.dartagnan.program.event.functions.AbortIf;
 import com.dat3m.dartagnan.program.event.functions.Return;
 import com.dat3m.dartagnan.program.event.functions.ValueFunctionCall;
 import com.dat3m.dartagnan.program.event.functions.VoidFunctionCall;
+import com.dat3m.dartagnan.program.event.lang.GenericRMWReturn;
 import com.dat3m.dartagnan.program.event.lang.catomic.*;
 import com.dat3m.dartagnan.program.event.lang.dat3m.*;
 import com.dat3m.dartagnan.program.event.lang.linux.*;
-import com.dat3m.dartagnan.program.event.lang.llvm.*;
+import com.dat3m.dartagnan.program.event.lang.llvm.LlvmCmpXchg;
+import com.dat3m.dartagnan.program.event.lang.llvm.LlvmFence;
+import com.dat3m.dartagnan.program.event.lang.llvm.LlvmLoad;
+import com.dat3m.dartagnan.program.event.lang.llvm.LlvmStore;
 import com.dat3m.dartagnan.program.event.lang.spirv.*;
 import com.dat3m.dartagnan.program.event.lang.svcomp.*;
 import com.dat3m.dartagnan.program.memory.MemoryObject;
@@ -476,22 +479,58 @@ public static LlvmStore newStore(Expression address, Expression value, String mo
             return new LlvmStore(address, value, mo);
         }
 
-        public static LlvmXchg newExchange(Register register, Expression address, Expression value, String mo) {
-            return new LlvmXchg(register, address, value, mo);
+        public static Event newExchange(Register register, Expression address, Expression value, String mo) {
+            return newExchangeAlt(register, address, value, mo);
+            //return new LlvmXchg(register, address, value, mo);
         }
 
-        public static LlvmCmpXchg newCompareExchange(Register oldValueRegister, Register cmpRegister, Expression address, Expression expectedAddr, Expression desiredValue, String mo, boolean isStrong) {
+        public static Event newExchangeAlt(Register register, Expression address, Expression value, String mo) {
+            final Expression hole = expressions.makeHole(value.getType());
+            final Expression cond = null;
+            final Expression storeVal = value;
+            final Expression retVal = hole;
+
+            return new GenericRMWReturn(register, address, storeVal, cond, retVal, mo);
+        }
+
+        public static Event newCompareExchange(Register oldValueRegister, Register cmpRegister, Expression address, Expression expectedAddr, Expression desiredValue, String mo, boolean isStrong) {
+            // TODO: We don't forward this because the return signature has changed, and the
+            //  Intrinsics rely on the old one. However, the LLVM parse calls the new version directly.
+            //return newCompareExchangeAlt(oldValueRegister, address, expectedAddr, desiredValue, mo, isStrong);
             return new LlvmCmpXchg(oldValueRegister, cmpRegister, address, expectedAddr, desiredValue, mo, isStrong);
         }
 
-        public static LlvmCmpXchg newCompareExchange(Register oldValueRegister, Register cmpRegister, Expression address, Expression expectedAddr, Expression desiredValue, String mo) {
+        public static Event newCompareExchangeAlt(Register resultRegister, Expression address, Expression expectedValue, Expression desiredValue, String mo, boolean isStrong) {
+            final Expression hole = expressions.makeHole(desiredValue.getType());
+            final Expression cond = expressions.makeEQ(hole, expectedValue);
+            final Expression storeVal = desiredValue;
+            final Expression retVal = expressions.makeConstruct(types.getAggregateType(
+                    List.of(expectedValue.getType(), types.getIntegerType(1))),
+                    List.of(hole, expressions.makeCast(cond, types.getIntegerType(1)))
+            );
+
+            return new GenericRMWReturn(resultRegister, address, storeVal, cond, retVal, mo);
+        }
+
+        public static Event newCompareExchange(Register oldValueRegister, Register cmpRegister, Expression address, Expression expectedAddr, Expression desiredValue, String mo) {
             return newCompareExchange(oldValueRegister, cmpRegister, address, expectedAddr, desiredValue, mo, false);
         }
 
-        public static LlvmRMW newRMW(Register register, Expression address, Expression value, IntBinaryOp op, String mo) {
-            return new LlvmRMW(register, address, op, value, mo);
+        public static Event newRMW(Register register, Expression address, Expression value, IntBinaryOp op, String mo) {
+            return newRMWAlt(register, address, value, op, mo);
+            //return new LlvmRMW(register, address, op, value, mo);
         }
 
+        public static Event newRMWAlt(Register register, Expression address, Expression value, IntBinaryOp op, String mo) {
+            final Expression hole = expressions.makeHole(value.getType());
+            final Expression cond = null;
+            final Expression storeVal = expressions.makeIntBinary(hole, op, value);
+            final Expression retVal = hole;
+
+            return new GenericRMWReturn(register, address, storeVal, cond, retVal, mo);
+        }
+
+
         public static LlvmFence newFence(String mo) {
             return new LlvmFence(mo);
         }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java

@@ -14,6 +14,8 @@
 import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMWOp;
 import com.dat3m.dartagnan.program.event.core.*;
 import com.dat3m.dartagnan.program.event.core.annotations.CodeAnnotation;
+import com.dat3m.dartagnan.program.event.lang.GenericRMWNoReturn;
+import com.dat3m.dartagnan.program.event.lang.GenericRMWReturn;
 import com.dat3m.dartagnan.program.event.lang.catomic.*;
 import com.dat3m.dartagnan.program.event.lang.linux.*;
 import com.dat3m.dartagnan.program.event.lang.llvm.*;
@@ -55,7 +57,9 @@ public interface EventVisitor<T> {
 
     // ------------------ Common Events ------------------
     default T visitStoreExclusive(StoreExclusive e) { return visitMemEvent(e); }
-    default T visitXchg(Xchg xchg) { return visitMemEvent(xchg); };
+    default T visitXchg(Xchg xchg) { return visitMemEvent(xchg); }
+    default T visitGenericRMWReturn(GenericRMWReturn e) { return visitMemEvent(e); }
+    default T visitGenericRMWNoReturn(GenericRMWNoReturn e) { return visitMemEvent(e); }
 
     // ------------------ Linux Events ------------------
     default T visitLKMMAddUnless(LKMMAddUnless e) { return visitMemEvent(e); }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/GenericRMWNoReturn.java

@@ -0,0 +1,68 @@
+package com.dat3m.dartagnan.program.event.lang;
+
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.ExpressionVisitor;
+import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.event.EventVisitor;
+import com.dat3m.dartagnan.program.event.MemoryAccess;
+import com.dat3m.dartagnan.program.event.common.SingleAccessMemoryEvent;
+
+import java.util.Set;
+
+import static com.dat3m.dartagnan.program.event.Tag.*;
+
+/*
+    This is for non-value-returning RMWs/AMOs, i.e., every operation of shape
+        __temp = load(addr);
+        store(addr, op(__temp));
+ */
+public class GenericRMWNoReturn extends SingleAccessMemoryEvent {
+
+    protected Expression storeTransformer;
+
+    protected GenericRMWNoReturn(Expression address, Expression storeTransformer, String mo) {
+        super(address, storeTransformer.getType(), mo);
+        this.storeTransformer = storeTransformer;
+        addTags(READ, WRITE, RMW);
+    }
+
+    protected GenericRMWNoReturn(GenericRMWNoReturn other) {
+        super(other);
+        this.storeTransformer = other.storeTransformer;
+    }
+
+    public Expression getStoreTransformer() { return storeTransformer; }
+    public void setStoreTransformer(Expression storeTransformer) { this.storeTransformer = storeTransformer; }
+
+    @Override
+    public void transformExpressions(ExpressionVisitor<? extends Expression> exprTransformer) {
+        super.transformExpressions(exprTransformer);
+        this.storeTransformer = storeTransformer.accept(exprTransformer);
+    }
+
+    @Override
+    public <T> T accept(EventVisitor<T> visitor) {
+        return visitor.visitGenericRMWNoReturn(this);
+    }
+
+    @Override
+    public GenericRMWNoReturn getCopy() {
+        return new GenericRMWNoReturn(this);
+    }
+
+    @Override
+    protected String defaultString() {
+        return String.format("rmw (%s, %s)", address, storeTransformer);
+    }
+
+    @Override
+    public Set<Register.Read> getRegisterReads() {
+        return Register.collectRegisterReads(storeTransformer, Register.UsageType.DATA, super.getRegisterReads());
+    }
+
+    @Override
+    public MemoryAccess getMemoryAccess() {
+        return new MemoryAccess(address, accessType, MemoryAccess.Mode.RMW);
+    }
+
+}