[IR] LLVM cmpxchg Rework (hernanponcedeleon#976)

Author: xeren

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

@@ -38,7 +38,6 @@
 
 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.google.common.base.Preconditions.checkState;
 import static com.google.common.base.Verify.verify;
 
@@ -810,19 +809,11 @@ public Expression visitCmpXchgInst(CmpXchgInstContext ctx) {
         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 Register value = function.newRegister(comparator.getType());
-        final Register asExpected = function.newRegister(types.getBooleanType());
-        final boolean weak = ctx.weak != null;
+        final boolean strong = ctx.weak == null;
         final String mo = parseMemoryOrder(ctx.atomicOrdering(0));
-        block.events.add(newCompareExchange(value, asExpected, address, comparator, substitute, mo, weak));
         final Register register = currentRegisterName == null ? null :
                 getOrNewCurrentRegister(types.getAggregateType(List.of(comparator.getType(), getIntegerType(1))));
-        if (register != null) {
-            final Expression cast = expressions.makeIntegerCast(asExpected, getIntegerType(1), false);
-            final Type type = types.getAggregateType(List.of(value.getType(), cast.getType()));
-            final Expression result = expressions.makeConstruct(type, List.of(value, cast));
-            block.events.add(newLocal(register, result));
-        }
+        block.events.add(Llvm.newCompareExchange(register, address, comparator, substitute, mo, strong));
         return register;
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java

@@ -10,7 +10,6 @@
 import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.core.CondJump;
 import com.dat3m.dartagnan.program.event.core.Label;
-import com.dat3m.dartagnan.program.event.lang.llvm.LlvmCmpXchg;
 import com.dat3m.dartagnan.program.processing.Intrinsics;
 import com.dat3m.dartagnan.utils.UniqueIdGenerator;
 import com.google.common.base.Preconditions;
@@ -222,7 +221,7 @@ public void validate() {
                         });
             }
 
-            if (ev instanceof RegWriter writer && !(writer instanceof LlvmCmpXchg) && !registers.contains(writer.getResultRegister())) {
+            if (ev instanceof RegWriter writer && !registers.contains(writer.getResultRegister())) {
                 final String error = String.format("Event %s of function %s writes to external register %s of function %s",
                         writer, this, writer.getResultRegister(), writer.getResultRegister().getFunction()
                 );

dartagnan/src/main/java/com/dat3m/dartagnan/program/IRHelper.java

@@ -11,7 +11,6 @@
 import com.dat3m.dartagnan.program.event.core.Init;
 import com.dat3m.dartagnan.program.event.functions.AbortIf;
 import com.dat3m.dartagnan.program.event.functions.Return;
-import com.dat3m.dartagnan.program.event.lang.llvm.LlvmCmpXchg;
 import com.google.common.base.Preconditions;
 import com.google.common.base.Verify;
 
@@ -126,10 +125,7 @@ public Expression visitRegister(Register reg) {
             if (event instanceof RegReader reader) {
                 reader.transformExpressions(regSubstitutor);
             }
-            if (event instanceof LlvmCmpXchg xchg) {
-                xchg.setStructRegister(0, (Register)xchg.getStructRegister(0).accept(regSubstitutor));
-                xchg.setStructRegister(1, (Register)xchg.getStructRegister(1).accept(regSubstitutor));
-            } else if (event instanceof RegWriter regWriter) {
+            if (event instanceof RegWriter regWriter) {
                 regWriter.setResultRegister((Register) regWriter.getResultRegister().accept(regSubstitutor));
             }
         };

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

@@ -485,12 +485,9 @@ public static LlvmXchg newExchange(Register register, Expression address, Expres
             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) {
-            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) {
-            return newCompareExchange(oldValueRegister, cmpRegister, address, expectedAddr, desiredValue, mo, false);
+        public static LlvmCmpXchg newCompareExchange(Register oldValueAndSuccess, Expression address,
+                Expression expected, Expression newValue, String mo, boolean strong) {
+            return new LlvmCmpXchg(oldValueAndSuccess, address, expected, newValue, mo, strong);
         }
 
         public static LlvmRMW newRMW(Register register, Expression address, Expression value, IntBinaryOp op, String mo) {

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmCmpXchg.java

@@ -1,64 +1,32 @@
 package com.dat3m.dartagnan.program.event.lang.llvm;
 
 import com.dat3m.dartagnan.expression.Expression;
-import com.dat3m.dartagnan.expression.type.BooleanType;
+import com.dat3m.dartagnan.expression.type.AggregateType;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.EventVisitor;
 import com.dat3m.dartagnan.program.event.common.RMWCmpXchgBase;
 import com.google.common.base.Preconditions;
 
-// FIXME: This instruction writes to two registers, which we cannot express right now.
 public class LlvmCmpXchg extends RMWCmpXchgBase {
 
-    private Register cmpRegister;
-
-    public LlvmCmpXchg(Register oldValueRegister, Register cmpRegister, Expression address,
-                       Expression expectedValue, Expression value, String mo, boolean isStrong) {
-        super(oldValueRegister, address, expectedValue, value, isStrong, mo);
+    public LlvmCmpXchg(Register oldValueAndSuccessRegister, Expression address, Expression expectedValue,
+            Expression value, String mo, boolean isStrong) {
+        super(oldValueAndSuccessRegister, address, expectedValue, value, isStrong, mo);
         Preconditions.checkArgument(!mo.isEmpty(), "LLVM events cannot have empty memory order");
-        Preconditions.checkArgument(cmpRegister.getType() instanceof BooleanType,
-                "Non-boolean result register of LlvmCmpXchg.");
-        this.cmpRegister = cmpRegister;
+        Preconditions.checkArgument(oldValueAndSuccessRegister.getType() instanceof AggregateType t
+                        && t.getFields().size() == 2,
+                "Non-aggregate result register of LlvmCmpXchg.");
     }
 
     private LlvmCmpXchg(LlvmCmpXchg other) {
         super(other);
-        this.cmpRegister = other.cmpRegister;
-    }
-
-    // The llvm instructions actually returns a structure.
-    // In most cases the structure is not used as a whole, 
-    // but rather by accessing its members. Thus, there is
-    // no need to support this method.
-    // NOTE: we use the inherited "resultRegister" to store the old value
-    @Override
-    public Register getResultRegister() {
-        throw new UnsupportedOperationException("getResultRegister() not supported for " + this);
-    }
-
-    public Register getStructRegister(int idx) {
-        return switch (idx) {
-            case 0 -> resultRegister;
-            case 1 -> cmpRegister;
-            default ->
-                    throw new UnsupportedOperationException("Cannot access structure with id " + idx + " in " + getClass().getName());
-        };
-    }
-
-    public void setStructRegister(int idx, Register newRegister) {
-        switch (idx) {
-            case 0 -> resultRegister = newRegister;
-            case 1 -> cmpRegister = newRegister;
-            default ->
-                    throw new UnsupportedOperationException("Cannot access structure with id " + idx + " in " + getClass().getName());
-        }
     }
 
     @Override
     public String defaultString() {
         final String strongSuffix = isStrong ? "strong" : "weak";
-        return String.format("(%s, %s) = llvm_cmpxchg_%s(%s, %s, %s, %s)",
-                resultRegister, cmpRegister, strongSuffix, address, expectedValue, storeValue, mo);
+        return String.format("%s = llvm_cmpxchg_%s(%s, %s, %s, %s)",
+                resultRegister, strongSuffix, address, expectedValue, storeValue, mo);
     }
 
     @Override