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 f82fdea03b..914fb9c383 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java @@ -11,7 +11,7 @@ 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.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; import org.sosy_lab.java_smt.api.*; @@ -298,9 +298,9 @@ public Formula visitMemoryObject(MemoryObject memObj) { } @Override - public Formula visitLocation(Location location) { - checkState(event == null, "Cannot evaluate %s at event %s.", location, event); - int size = types.getMemorySizeInBits(location.getType()); - return context.lastValue(location.getMemoryObject(), location.getOffset(), size); + public Formula visitFinalMemoryValue(FinalMemoryValue val) { + checkState(event == null, "Cannot evaluate final memory value of %s at event %s.", val, event); + int size = types.getMemorySizeInBits(val.getType()); + return context.lastValue(val.getMemoryObject(), val.getOffset(), size); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java index afc86451c1..a2891b877c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionInspector; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.ImmutableSet; @@ -40,9 +40,9 @@ public MemoryObject visitMemoryObject(MemoryObject memObj) { } @Override - public Expression visitLocation(Location location) { - objects.add(location.getMemoryObject()); - return location; + public Expression visitFinalMemoryValue(FinalMemoryValue val) { + objects.add(val.getMemoryObject()); + return val; } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java index 57e26ad293..9abbc42896 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java @@ -16,6 +16,7 @@ enum Other implements ExpressionKind { NONDET, FUNCTION_ADDR, MEMORY_ADDR, + FINAL_MEM_VAL, REGISTER, GEP, CONSTRUCT, 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 b72021dd0a..1e4640b963 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java @@ -11,7 +11,7 @@ import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; @@ -59,7 +59,7 @@ public interface ExpressionVisitor { default TRet visitRegister(Register reg) { return visitLeafExpression(reg); } default TRet visitFunction(Function function) { return visitLeafExpression(function); } default TRet visitMemoryObject(MemoryObject memObj) { return visitLeafExpression(memObj); } - default TRet visitLocation(Location loc) { return visitLeafExpression(loc); } + default TRet visitFinalMemoryValue(FinalMemoryValue val) { return visitLeafExpression(val); } default TRet visitNonDetValue(NonDetValue nonDet) { return visitLeafExpression(nonDet); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java index c8ce2ca1d4..5f720d48b9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java @@ -8,7 +8,7 @@ import com.dat3m.dartagnan.parsers.LitmusAssertionsLexer; import com.dat3m.dartagnan.parsers.LitmusAssertionsParser; import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStreams; @@ -115,6 +115,6 @@ private Expression acceptAssertionValue(LitmusAssertionsParser.AssertionValueCon checkState(base != null, "uninitialized location %s", name); TerminalNode offset = ctx.DigitSequence(); int o = offset == null ? 0 : Integer.parseInt(offset.getText()); - return right && offset == null ? base : new Location(name, archType, base, o); + return right && offset == null ? base : new FinalMemoryValue(name, archType, base, o); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java index 1fbf076f80..6185fc6933 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java @@ -4,7 +4,6 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.Type; -import com.dat3m.dartagnan.expression.base.LiteralExpressionBase; import com.dat3m.dartagnan.expression.integers.IntCmpOp; import com.dat3m.dartagnan.expression.integers.IntLiteral; import com.dat3m.dartagnan.expression.type.AggregateType; @@ -13,15 +12,13 @@ import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.SpirvBaseVisitor; import com.dat3m.dartagnan.parsers.SpirvParser; -import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperTypes; import com.dat3m.dartagnan.parsers.program.visitors.spirv.builders.ProgramBuilder; +import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperTypes; import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.ScopedPointerVariable; -import java.util.HashMap; import java.util.List; -import java.util.Map; import static com.dat3m.dartagnan.expression.integers.IntCmpOp.*; import static com.dat3m.dartagnan.program.Program.SpecificationType.*; @@ -30,7 +27,6 @@ public class VisitorSpirvOutput extends SpirvBaseVisitor { private static final TypeFactory types = TypeFactory.getInstance(); private static final ExpressionFactory expressions = ExpressionFactory.getInstance(); - private final Map locationTypes = new HashMap<>(); private final ProgramBuilder builder; private Program.SpecificationType type; private Expression condition; @@ -48,7 +44,7 @@ public Expression visitSpvHeaders(SpirvParser.SpvHeadersContext ctx) { } if (type == null) { type = FORALL; - condition = ExpressionFactory.getInstance().makeTrue(); + condition = expressions.makeTrue(); } builder.setSpecification(type, condition); return null; @@ -103,7 +99,7 @@ public Expression visitAssertionValue(SpirvParser.AssertionValueContext ctx) { List indexes = ctx.indexValue().stream() .map(c -> Integer.parseInt(c.ModeHeader_PositiveInteger().getText())) .toList(); - return createLocation(base, indexes); + return createFinalMemoryValue(base, indexes); } throw new ParsingException("Uninitialized location %s", name); } @@ -114,9 +110,9 @@ private void appendAssertion(Program.SpecificationType newType, Expression expre condition = expression; } else if (newType.equals(type)) { if (type.equals(FORALL)) { - condition = ExpressionFactory.getInstance().makeAnd(condition, expression); + condition = expressions.makeAnd(condition, expression); } else if (type.equals(NOT_EXISTS)) { - condition = ExpressionFactory.getInstance().makeOr(condition, expression); + condition = expressions.makeOr(condition, expression); } else { throw new ParsingException("Multiline assertion is not supported for type " + newType); } @@ -126,15 +122,15 @@ private void appendAssertion(Program.SpecificationType newType, Expression expre } private Expression normalize(Expression target, Expression other) { - Type targetType = target instanceof Location ? locationTypes.get(target) : target.getType(); - Type otherType = other instanceof Location ? locationTypes.get(other) : other.getType(); + Type targetType = target.getType(); + Type otherType = other.getType(); if (targetType.equals(otherType)) { return target; } - if (target instanceof Location && other instanceof LiteralExpressionBase) { + if (target instanceof FinalMemoryValue && other.getKind() == Other.LITERAL) { return target; } - if (target instanceof IntLiteral iValue && other instanceof Location) { + if (target instanceof IntLiteral iValue && other instanceof FinalMemoryValue) { int size = types.getMemorySizeInBits(otherType); IntegerType newType = types.getIntegerType(size); return new IntLiteral(newType, iValue.getValue()); @@ -178,7 +174,7 @@ private IntCmpOp parseOperand(SpirvParser.AssertionCompareContext ctx) { throw new ParsingException("Unrecognised comparison operator"); } - private Location createLocation(ScopedPointerVariable base, List indexes) { + private FinalMemoryValue createFinalMemoryValue(ScopedPointerVariable base, List indexes) { String name = indexes.isEmpty() ? base.getId() : base.getId() + "[" + String.join("][", indexes.stream().map(Object::toString).toArray(String[]::new)) + "]"; Type elType = HelperTypes.getMemberType(base.getId(), base.getInnerType(), indexes); @@ -186,8 +182,6 @@ private Location createLocation(ScopedPointerVariable base, List indexe throw new ParsingException("Index is not deep enough for variable '%s'", name); } int offset = HelperTypes.getMemberOffset(base.getId(), 0, base.getInnerType(), indexes); - Location location = new Location(name, elType, base.getAddress(), offset); - locationTypes.put(location, elType); - return location; + return new FinalMemoryValue(name, elType, base.getAddress(), offset); } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/FinalMemoryValue.java similarity index 59% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/FinalMemoryValue.java index 094ecf5592..051152c72f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/FinalMemoryValue.java @@ -5,15 +5,17 @@ import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.base.LeafExpressionBase; -// TODO: Should be replaced with a Pointer class -public class Location extends LeafExpressionBase { +// TODO: Should work with an arbitrary pointer rather than "base + offset" +// Represents the final (co-maximal) value at a memory address as if read by a load instruction +// that observed the final store. +public class FinalMemoryValue extends LeafExpressionBase { private final String name; private final MemoryObject base; private final int offset; - public Location(String name, Type type, MemoryObject base, int offset) { - super(type); + public FinalMemoryValue(String name, Type loadType, MemoryObject base, int offset) { + super(loadType); this.name = name; this.base = base; this.offset = offset; @@ -33,12 +35,12 @@ public int getOffset() { @Override public ExpressionKind getKind() { - return ExpressionKind.Other.MEMORY_ADDR; + return ExpressionKind.Other.FINAL_MEM_VAL; } @Override public T accept(ExpressionVisitor visitor) { - return visitor.visitLocation(this); + return visitor.visitFinalMemoryValue(this); } @Override @@ -48,17 +50,12 @@ public String toString() { @Override public int hashCode() { - return base.hashCode() + offset; + return base.hashCode() + 31 * offset; } @Override public boolean equals(Object obj) { - if (this == obj) { - return true; - } else if (obj == null || getClass() != obj.getClass()) { - return false; - } - Location o = (Location) obj; - return base.equals(o.base) && offset == o.offset; + return (obj instanceof FinalMemoryValue o) && + base.equals(o.base) && offset == o.offset; } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java index 6feca6db62..0aeea91d3d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionInspector; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.event.RegReader; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.Sets; @@ -52,9 +52,9 @@ public Expression visitMemoryObject(MemoryObject address) { } @Override - public Expression visitLocation(Location location) { - memoryObjects.add(location.getMemoryObject()); - return location; + public Expression visitFinalMemoryValue(FinalMemoryValue val) { + memoryObjects.add(val.getMemoryObject()); + return val; } } }