Renamed Location to FinalMemoryValue.

Minor refactoring of related code.
hernanponcedeleon · Sep 2, 2024 · a5ac481 · a5ac481
1 parent 9a23ab0
commit a5ac481
Show file tree

Hide file tree

Showing 8 changed files with 41 additions and 49 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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<TRet> {
     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/...n/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java b/...n/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/.../src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java b/.../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<Expression> {
 
     private static final TypeFactory types = TypeFactory.getInstance();
     private static final ExpressionFactory expressions = ExpressionFactory.getInstance();
-    private final Map<Location, Type> 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<Integer> 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,16 +174,14 @@ private IntCmpOp parseOperand(SpirvParser.AssertionCompareContext ctx) {
         throw new ParsingException("Unrecognised comparison operator");
     }
 
-    private Location createLocation(ScopedPointerVariable base, List<Integer> indexes) {
+    private FinalMemoryValue createFinalMemoryValue(ScopedPointerVariable base, List<Integer> 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);
         if (elType instanceof ArrayType || elType instanceof AggregateType) {
             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);
     }
 }
diff --git a/...3m/dartagnan/program/memory/Location.java → ...gnan/program/memory/FinalMemoryValue.java b/...3m/dartagnan/program/memory/Location.java → ...gnan/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<Type> {
+// 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<Type> {
 
     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> T accept(ExpressionVisitor<T> 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;
     }
 }
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
@@ -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;
         }
     }
 }