From c5468bfae887cba70c0a76fdc4a6dcf715a037e0 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Wed, 20 Nov 2024 09:44:08 +0100 Subject: [PATCH] Add support for encoding tuples (Tuple theory) (#775) * Add support for AggregateTypes in encoding. Also add new Aggregate operations EQ and NEQ * Remove RegisterDecomposition.java --- .../dartagnan/encoding/EncodingContext.java | 23 ++++++ .../dartagnan/encoding/ExpressionEncoder.java | 33 ++++++++ .../encoding/formulas/TupleFormula.java | 45 +++++++++++ .../formulas/TupleFormulaManager.java | 45 +++++++++++ .../expression/ExpressionFactory.java | 16 +++- .../expression/ExpressionPrinter.java | 4 +- .../expression/ExpressionVisitor.java | 6 +- .../aggregates/AggregateCmpExpr.java | 21 +++++ .../expression/aggregates/AggregateCmpOp.java | 20 +++++ .../{misc => aggregates}/ConstructExpr.java | 2 +- .../{misc => aggregates}/ExtractExpr.java | 2 +- .../expression/processing/ExprSimplifier.java | 28 ++++++- .../processing/ExprTransformer.java | 17 +++- .../visitors/spirv/decorations/BuiltIn.java | 2 +- .../visitors/spirv/helpers/HelperInputs.java | 2 +- .../program/memory/MemoryObject.java | 2 +- .../program/processing/ProcessingManager.java | 1 - .../processing/RegisterDecomposition.java | 79 ------------------- .../visitors/spirv/VisitorOpsMemoryTest.java | 2 +- 19 files changed, 251 insertions(+), 99 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/encoding/formulas/TupleFormula.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/encoding/formulas/TupleFormulaManager.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/AggregateCmpExpr.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/AggregateCmpOp.java rename dartagnan/src/main/java/com/dat3m/dartagnan/expression/{misc => aggregates}/ConstructExpr.java (97%) rename dartagnan/src/main/java/com/dat3m/dartagnan/expression/{misc => aggregates}/ExtractExpr.java (97%) delete mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RegisterDecomposition.java diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java index 491a864500..1682726021 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java @@ -1,11 +1,15 @@ package com.dat3m.dartagnan.encoding; import com.dat3m.dartagnan.configuration.ProgressModel; +import com.dat3m.dartagnan.encoding.formulas.TupleFormula; +import com.dat3m.dartagnan.encoding.formulas.TupleFormulaManager; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.integers.IntCmpOp; +import com.dat3m.dartagnan.expression.type.AggregateType; import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.expression.type.IntegerType; +import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.analysis.BranchEquivalence; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; @@ -33,7 +37,9 @@ import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import java.math.BigInteger; +import java.util.ArrayList; import java.util.HashMap; +import java.util.List; import java.util.Map; import static com.dat3m.dartagnan.configuration.OptionNames.*; @@ -54,6 +60,7 @@ public final class EncodingContext { private final RelationAnalysis relationAnalysis; private final FormulaManager formulaManager; private final BooleanFormulaManager booleanFormulaManager; + private final TupleFormulaManager tupleFormulaManager; @Option( name=IDL_TO_SAT, @@ -88,6 +95,7 @@ private EncodingContext(VerificationTask t, Context a, FormulaManager m) { relationAnalysis = a.requires(RelationAnalysis.class); formulaManager = m; booleanFormulaManager = m.getBooleanFormulaManager(); + tupleFormulaManager = new TupleFormulaManager(this); } public static EncodingContext of(VerificationTask task, Context analysisContext, FormulaManager formulaManager) throws InvalidConfigurationException { @@ -126,6 +134,10 @@ public BooleanFormulaManager getBooleanFormulaManager() { return booleanFormulaManager; } + public TupleFormulaManager getTupleFormulaManager() { + return tupleFormulaManager; + } + public Formula encodeFinalExpression(Expression expression) { return new ExpressionEncoder(this, null).encode(expression); } @@ -249,6 +261,9 @@ public BooleanFormula equal(Formula left, Formula right) { if (left instanceof BooleanFormula l && right instanceof BooleanFormula r) { return booleanFormulaManager.equivalence(l, r); } + if (left instanceof TupleFormula l && right instanceof TupleFormula r) { + return tupleFormulaManager.equal(l, r); + } throw new UnsupportedOperationException(String.format("Unknown types for equal(%s,%s)", left, right)); } @@ -439,6 +454,14 @@ Formula makeVariable(String name, Type type) { return formulaManager.getBitvectorFormulaManager().makeVariable(integerType.getBitWidth(), name); } } + if (type instanceof AggregateType) { + final Map primitives = TypeFactory.getInstance().decomposeIntoPrimitives(type); + final List elements = new ArrayList<>(); + for (Type eleType : primitives.values()) { + elements.add(makeVariable(name + "@" + elements.size(), eleType)); + } + return tupleFormulaManager.makeTuple(elements); + } throw new UnsupportedOperationException(String.format("Cannot encode variable of type %s.", type)); } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java index dcf629961a..798b7d8fb4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java @@ -1,8 +1,12 @@ package com.dat3m.dartagnan.encoding; +import com.dat3m.dartagnan.encoding.formulas.TupleFormula; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionVisitor; import com.dat3m.dartagnan.expression.Type; +import com.dat3m.dartagnan.expression.aggregates.AggregateCmpExpr; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; +import com.dat3m.dartagnan.expression.aggregates.ExtractExpr; import com.dat3m.dartagnan.expression.booleans.BoolBinaryExpr; import com.dat3m.dartagnan.expression.booleans.BoolLiteral; import com.dat3m.dartagnan.expression.booleans.BoolUnaryExpr; @@ -18,6 +22,8 @@ import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import java.math.BigInteger; +import java.util.ArrayList; +import java.util.List; import static com.google.common.base.Preconditions.checkState; import static java.util.Arrays.asList; @@ -282,6 +288,33 @@ public Formula visitITEExpression(ITEExpr iteExpr) { return booleanFormulaManager.ifThenElse(guard, tBranch, fBranch); } + @Override + public Formula visitConstructExpression(ConstructExpr construct) { + final List elements = new ArrayList<>(); + for (Expression inner : construct.getOperands()) { + elements.add(encode(inner)); + } + return context.getTupleFormulaManager().makeTuple(elements); + } + + @Override + public Formula visitAggregateCmpExpression(AggregateCmpExpr expr) { + final Formula left = encode(expr.getLeft()); + final Formula right = encode(expr.getRight()); + final BooleanFormula eq = context.equal(left, right); + return switch (expr.getKind()) + { + case EQ -> eq; + case NEQ -> context.getBooleanFormulaManager().not(eq); + }; + } + + @Override + public Formula visitExtractExpression(ExtractExpr extract) { + final TupleFormula inner = (TupleFormula) encode(extract.getOperand()); + return context.getTupleFormulaManager().extract(inner, extract.getFieldIndex()); + } + @Override public Formula visitRegister(Register reg) { String name = event == null ? diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/formulas/TupleFormula.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/formulas/TupleFormula.java new file mode 100644 index 0000000000..9a97a4fa20 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/formulas/TupleFormula.java @@ -0,0 +1,45 @@ +package com.dat3m.dartagnan.encoding.formulas; + +import org.sosy_lab.java_smt.api.Formula; + +import java.util.List; +import java.util.stream.Collectors; + +/* + Implementation Note: + We implement JavaSMT's Formula interface so this appears like a normal formula, + however, it won't support many of JavaSMT's features like formula traversal. + */ +public class TupleFormula implements Formula { + + final List elements; + + TupleFormula(List elements) { + this.elements = elements; + } + + @Override + public String toString() { + return elements.stream() + .map(Object::toString) + .collect(Collectors.joining(",", "{ ", " }")); + } + + @Override + public int hashCode() { + return elements.hashCode(); + } + + @Override + public boolean equals(Object obj) { + if (obj == this) { + return true; + } else if (obj == null || obj.getClass() != this.getClass()) { + return false; + } else { + final TupleFormula other = (TupleFormula) obj; + return this.elements.equals(other.elements); + } + } + +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/formulas/TupleFormulaManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/formulas/TupleFormulaManager.java new file mode 100644 index 0000000000..901b83df20 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/formulas/TupleFormulaManager.java @@ -0,0 +1,45 @@ +package com.dat3m.dartagnan.encoding.formulas; + +import com.dat3m.dartagnan.encoding.EncodingContext; +import com.google.common.base.Preconditions; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Formula; + +import java.util.ArrayList; +import java.util.List; + + +/* + Note: This class cannot actually create variables of tuple type and merely gives the illusion of + a proper tuple theory. + To simulate tuple variables, the user instead has to construct tuples of variables. + */ +public final class TupleFormulaManager { + + private final EncodingContext context; + + public TupleFormulaManager(EncodingContext context) { + this.context = context; + + } + + public BooleanFormula equal(TupleFormula x, TupleFormula y) { + Preconditions.checkArgument(x.elements.size() == y.elements.size()); + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + final List enc = new ArrayList<>(); + for (int i = 0; i < x.elements.size(); i++) { + enc.add(context.equal(x.elements.get(i), y.elements.get(i)));; + } + return bmgr.and(enc); + } + + public Formula extract(TupleFormula f, int index) { + Preconditions.checkArgument(0 <= index && index < f.elements.size()); + return f.elements.get(index); + } + + public TupleFormula makeTuple(List elements) { + return new TupleFormula(elements); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java index 79cc12a5bb..ffe20ffc1d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java @@ -1,10 +1,12 @@ package com.dat3m.dartagnan.expression; +import com.dat3m.dartagnan.expression.aggregates.AggregateCmpExpr; +import com.dat3m.dartagnan.expression.aggregates.AggregateCmpOp; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; +import com.dat3m.dartagnan.expression.aggregates.ExtractExpr; import com.dat3m.dartagnan.expression.booleans.*; import com.dat3m.dartagnan.expression.floats.*; import com.dat3m.dartagnan.expression.integers.*; -import com.dat3m.dartagnan.expression.misc.ConstructExpr; -import com.dat3m.dartagnan.expression.misc.ExtractExpr; import com.dat3m.dartagnan.expression.misc.GEPExpr; import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.expression.type.*; @@ -271,6 +273,10 @@ public Expression makeExtract(int fieldIndex, Expression object) { return new ExtractExpr(fieldIndex, object); } + public Expression makeAggregateCmp(Expression x, AggregateCmpOp op, Expression y) { + return new AggregateCmpExpr(booleanType, x, op, y); + } + // ----------------------------------------------------------------------------------------------------------------- // Pointers @@ -345,6 +351,8 @@ public Expression makeEQ(Expression leftOperand, Expression rightOperand) { } else if (type instanceof FloatType) { // TODO: Decide on a default semantics for float equality? return makeFloatCmp(leftOperand, FloatCmpOp.OEQ, rightOperand); + } else if (type instanceof AggregateType) { + return makeAggregateCmp(leftOperand, AggregateCmpOp.EQ, rightOperand); } throw new UnsupportedOperationException("Equality not supported on type: " + type); } @@ -358,6 +366,8 @@ public Expression makeNEQ(Expression leftOperand, Expression rightOperand) { } else if (type instanceof FloatType) { // TODO: Decide on a default semantics for float equality? return makeFloatCmp(leftOperand, FloatCmpOp.ONEQ, rightOperand); + } else if (type instanceof AggregateType) { + return makeAggregateCmp(leftOperand, AggregateCmpOp.NEQ, rightOperand); } throw new UnsupportedOperationException("Disequality not supported on type: " + type); } @@ -391,6 +401,8 @@ public Expression makeCompare(Expression x, ExpressionKind cmpOp, Expression y) return makeIntCmp(x, intCmpOp, y); } else if (cmpOp instanceof FloatCmpOp floatOp) { return makeFloatCmp(x, floatOp, y); + } else if (cmpOp instanceof AggregateCmpOp aggrCmpOp) { + return makeAggregateCmp(x, aggrCmpOp, y); } throw new UnsupportedOperationException(String.format("Expression kind %s is no comparison operator.", cmpOp)); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionPrinter.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionPrinter.java index 2d393c8553..f20d48ffb5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionPrinter.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionPrinter.java @@ -1,5 +1,7 @@ package com.dat3m.dartagnan.expression; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; +import com.dat3m.dartagnan.expression.aggregates.ExtractExpr; import com.dat3m.dartagnan.expression.booleans.BoolBinaryOp; import com.dat3m.dartagnan.expression.booleans.BoolUnaryOp; import com.dat3m.dartagnan.expression.floats.FloatSizeCast; @@ -8,8 +10,6 @@ import com.dat3m.dartagnan.expression.integers.IntBinaryOp; import com.dat3m.dartagnan.expression.integers.IntSizeCast; import com.dat3m.dartagnan.expression.integers.IntUnaryOp; -import com.dat3m.dartagnan.expression.misc.ConstructExpr; -import com.dat3m.dartagnan.expression.misc.ExtractExpr; import com.dat3m.dartagnan.expression.misc.GEPExpr; import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.program.Register; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java index 1e4640b963..ec5064976b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java @@ -1,12 +1,13 @@ package com.dat3m.dartagnan.expression; +import com.dat3m.dartagnan.expression.aggregates.AggregateCmpExpr; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; +import com.dat3m.dartagnan.expression.aggregates.ExtractExpr; import com.dat3m.dartagnan.expression.booleans.BoolBinaryExpr; import com.dat3m.dartagnan.expression.booleans.BoolLiteral; 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.ConstructExpr; -import com.dat3m.dartagnan.expression.misc.ExtractExpr; import com.dat3m.dartagnan.expression.misc.GEPExpr; import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.program.Function; @@ -46,6 +47,7 @@ public interface ExpressionVisitor { default TRet visitFloatLiteral(FloatLiteral lit) { return visitLeafExpression(lit); } // =================================== Aggregates =================================== + default TRet visitAggregateCmpExpression(AggregateCmpExpr expr) { return visitBinaryExpression(expr); } default TRet visitExtractExpression(ExtractExpr extract) { return visitUnaryExpression(extract); } default TRet visitConstructExpression(ConstructExpr construct) { return visitExpression(construct); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/AggregateCmpExpr.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/AggregateCmpExpr.java new file mode 100644 index 0000000000..1f95517b5f --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/AggregateCmpExpr.java @@ -0,0 +1,21 @@ +package com.dat3m.dartagnan.expression.aggregates; + +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.ExpressionVisitor; +import com.dat3m.dartagnan.expression.base.BinaryExpressionBase; +import com.dat3m.dartagnan.expression.type.AggregateType; +import com.dat3m.dartagnan.expression.type.BooleanType; +import com.dat3m.dartagnan.expression.utils.ExpressionHelper; + +public final class AggregateCmpExpr extends BinaryExpressionBase { + + public AggregateCmpExpr(BooleanType type, Expression left, AggregateCmpOp kind, Expression right) { + super(type, kind, left, right); + ExpressionHelper.checkSameExpectedType(left, right, AggregateType.class); + } + + @Override + public T accept(ExpressionVisitor visitor) { + return visitor.visitAggregateCmpExpression(this); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/AggregateCmpOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/AggregateCmpOp.java new file mode 100644 index 0000000000..e3d1bdf86f --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/AggregateCmpOp.java @@ -0,0 +1,20 @@ +package com.dat3m.dartagnan.expression.aggregates; + +import com.dat3m.dartagnan.expression.ExpressionKind; + +public enum AggregateCmpOp implements ExpressionKind { + EQ, NEQ; + + @Override + public String toString() { + return getSymbol(); + } + + @Override + public String getSymbol() { + return switch (this) { + case EQ -> "=="; + case NEQ -> "!="; + }; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/misc/ConstructExpr.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/ConstructExpr.java similarity index 97% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/misc/ConstructExpr.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/ConstructExpr.java index 05eee31598..cfd75acb90 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/misc/ConstructExpr.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/ConstructExpr.java @@ -1,4 +1,4 @@ -package com.dat3m.dartagnan.expression.misc; +package com.dat3m.dartagnan.expression.aggregates; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionKind; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/misc/ExtractExpr.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/ExtractExpr.java similarity index 97% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/misc/ExtractExpr.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/ExtractExpr.java index 663502d8f9..21e57d5b9c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/misc/ExtractExpr.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/ExtractExpr.java @@ -1,4 +1,4 @@ -package com.dat3m.dartagnan.expression.misc; +package com.dat3m.dartagnan.expression.aggregates; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionKind; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java index d2ad08b8ac..05ca6d9627 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java @@ -4,10 +4,12 @@ import com.dat3m.dartagnan.expression.BinaryExpression; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionKind; +import com.dat3m.dartagnan.expression.aggregates.AggregateCmpExpr; +import com.dat3m.dartagnan.expression.aggregates.AggregateCmpOp; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; +import com.dat3m.dartagnan.expression.aggregates.ExtractExpr; import com.dat3m.dartagnan.expression.booleans.*; import com.dat3m.dartagnan.expression.integers.*; -import com.dat3m.dartagnan.expression.misc.ConstructExpr; -import com.dat3m.dartagnan.expression.misc.ExtractExpr; import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.expression.utils.IntegerHelper; import com.google.common.base.VerifyException; @@ -310,10 +312,30 @@ public Expression visitExtractExpression(ExtractExpr expr) { if (inner instanceof ConstructExpr construct) { return construct.getOperands().get(expr.getFieldIndex()); } - return expressions.makeExtract(expr.getFieldIndex(), inner); } + @Override + public Expression visitAggregateCmpExpression(AggregateCmpExpr expr) { + final Expression left = expr.getLeft().accept(this); + final Expression right = expr.getRight().accept(this); + assert expr.getKind() == AggregateCmpOp.EQ || expr.getKind() == AggregateCmpOp.NEQ; + final boolean isEq = expr.getKind() == AggregateCmpOp.EQ; + if (left instanceof ConstructExpr l && right instanceof ConstructExpr r) { + if (l.getOperands().size() == r.getOperands().size()) { + if (l.getOperands().isEmpty()) { + return expressions.makeValue(isEq); + } else if (l.getOperands().size() == 1) { + final Expression lOp = l.getOperands().get(0); + final Expression rOp = r.getOperands().get(0); + return (isEq ? expressions.makeEQ(lOp, rOp) : expressions.makeNEQ(lOp, rOp)).accept(this); + } + } + } + + return expressions.makeAggregateCmp(left, expr.getKind(), right); + } + // =================================== Helper methods =================================== // An expression is potentially eliminable if it either carries no dependencies diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java index 385f4df364..578909e4fd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java @@ -4,6 +4,9 @@ import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.ExpressionVisitor; import com.dat3m.dartagnan.expression.LeafExpression; +import com.dat3m.dartagnan.expression.aggregates.AggregateCmpExpr; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; +import com.dat3m.dartagnan.expression.aggregates.ExtractExpr; import com.dat3m.dartagnan.expression.booleans.BoolBinaryExpr; import com.dat3m.dartagnan.expression.booleans.BoolUnaryExpr; import com.dat3m.dartagnan.expression.floats.FloatBinaryExpr; @@ -13,8 +16,6 @@ import com.dat3m.dartagnan.expression.integers.IntCmpExpr; import com.dat3m.dartagnan.expression.integers.IntSizeCast; import com.dat3m.dartagnan.expression.integers.IntUnaryExpr; -import com.dat3m.dartagnan.expression.misc.ConstructExpr; -import com.dat3m.dartagnan.expression.misc.ExtractExpr; import com.dat3m.dartagnan.expression.misc.GEPExpr; import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.expression.type.TypeFactory; @@ -90,8 +91,16 @@ public Expression visitConstructExpression(ConstructExpr construct) { @Override public Expression visitExtractExpression(ExtractExpr expr) { - Expression object = expr.getOperand().accept(this); - return expressions.makeExtract(expr.getFieldIndex(), object); + return expressions.makeExtract(expr.getFieldIndex(), expr.getOperand().accept(this)); + } + + @Override + public Expression visitAggregateCmpExpression(AggregateCmpExpr expr) { + return expressions.makeAggregateCmp( + expr.getLeft().accept(this), + expr.getKind(), + expr.getRight().accept(this) + ); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/decorations/BuiltIn.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/decorations/BuiltIn.java index 23341ae7ef..0db9aea5b6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/decorations/BuiltIn.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/decorations/BuiltIn.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.Type; -import com.dat3m.dartagnan.expression.misc.ConstructExpr; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; import com.dat3m.dartagnan.expression.type.ArrayType; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/helpers/HelperInputs.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/helpers/HelperInputs.java index 92a874ae44..4e7c4933fc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/helpers/HelperInputs.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/helpers/HelperInputs.java @@ -4,8 +4,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.Type; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; import com.dat3m.dartagnan.expression.integers.IntLiteral; -import com.dat3m.dartagnan.expression.misc.ConstructExpr; import com.dat3m.dartagnan.expression.type.*; import java.util.ArrayList; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java index 6b606ba576..b849b2337b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java @@ -4,9 +4,9 @@ import com.dat3m.dartagnan.expression.ExpressionKind; import com.dat3m.dartagnan.expression.ExpressionVisitor; import com.dat3m.dartagnan.expression.Type; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; import com.dat3m.dartagnan.expression.base.LeafExpressionBase; import com.dat3m.dartagnan.expression.integers.IntLiteral; -import com.dat3m.dartagnan.expression.misc.ConstructExpr; import com.dat3m.dartagnan.expression.type.*; import com.dat3m.dartagnan.program.event.core.Alloc; import com.google.common.base.Preconditions; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java index 451fc3678c..dd7d547c0a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java @@ -99,7 +99,6 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep ), Target.ALL, true ), ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.ALL, true), - RegisterDecomposition.newInstance(), RemoveDeadFunctions.newInstance(), printAfterSimplification ? DebugPrint.withHeader("After simplification", Printer.Mode.ALL) : null, Compilation.fromConfig(config), // We keep compilation global for now diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RegisterDecomposition.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RegisterDecomposition.java deleted file mode 100644 index 4072947aa6..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RegisterDecomposition.java +++ /dev/null @@ -1,79 +0,0 @@ -package com.dat3m.dartagnan.program.processing; - -import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.misc.ConstructExpr; -import com.dat3m.dartagnan.expression.misc.ExtractExpr; -import com.dat3m.dartagnan.expression.processing.ExprTransformer; -import com.dat3m.dartagnan.expression.type.AggregateType; -import com.dat3m.dartagnan.program.Function; -import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.Event; -import com.dat3m.dartagnan.program.event.RegReader; -import com.dat3m.dartagnan.program.event.RegWriter; -import com.dat3m.dartagnan.program.event.core.Local; -import com.dat3m.dartagnan.program.event.lang.llvm.LlvmCmpXchg; - -import java.util.ArrayList; -import java.util.HashMap; -import java.util.List; -import java.util.Map; - -import static com.dat3m.dartagnan.program.event.EventFactory.newLocal; -import static com.google.common.base.Preconditions.checkNotNull; - -public class RegisterDecomposition implements ProgramProcessor { - - private RegisterDecomposition() {} - - public static RegisterDecomposition newInstance() { - return new RegisterDecomposition(); - } - - @Override - public void run(Program program) { - final var transformer = new ExtractSubstitutor(); - for (Function function : program.getFunctions()) { - //TODO assume that no constructor occurs anywhere other than as the root operation of a local - for (RegWriter writer : function.getEvents(RegWriter.class)) { - if (!(writer instanceof LlvmCmpXchg) && - writer.getResultRegister().getType() instanceof AggregateType) { - if (!(writer instanceof Local local) || - !(local.getExpr() instanceof ConstructExpr construct)) { - throw new UnsupportedOperationException("No support for indirect aggregate construct"); - } - final List arguments = construct.getOperands(); - final var componentAssignments = new ArrayList(); - for (int i = 0; i < arguments.size(); i++) { - final Expression argument = arguments.get(i); - final Register register = function.newRegister(argument.getType()); - final var index = new RegisterIndex(local.getResultRegister(), i); - transformer.map.put(index, register); - componentAssignments.add(newLocal(register, argument)); - //TODO recur if no leaf type - } - local.replaceBy(componentAssignments); - } - } - for (RegReader reader : function.getEvents(RegReader.class)) { - reader.transformExpressions(transformer); - } - } - } - - private record RegisterIndex(Register origin, int index) {} - - private static final class ExtractSubstitutor extends ExprTransformer { - - private final Map map = new HashMap<>(); - - @Override - public Expression visitExtractExpression(ExtractExpr expr) { - if (!(expr.getOperand() instanceof Register reg)) { - throw new UnsupportedOperationException("No support for indirect expr"); - } - final var index = new RegisterIndex(reg, expr.getFieldIndex()); - return checkNotNull(map.get(index)); - } - } -} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemoryTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemoryTest.java index 14ef9f4fb5..0863b0baf0 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemoryTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemoryTest.java @@ -4,8 +4,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.Type; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; import com.dat3m.dartagnan.expression.integers.IntBinaryExpr; -import com.dat3m.dartagnan.expression.misc.ConstructExpr; import com.dat3m.dartagnan.expression.type.*; import com.dat3m.dartagnan.parsers.SpirvParser; import com.dat3m.dartagnan.parsers.program.visitors.spirv.mocks.MockProgramBuilder;