From b306be5ee6f6b3a2551f1728e66e57ad7e415cdd Mon Sep 17 00:00:00 2001
From: Natalia Gavrilenko <natgavrilenko@gmail.com>
Date: Tue, 9 Jul 2024 20:46:31 +0200
Subject: [PATCH] wip

---
 .../visitors/spirv/ProgramBuilderSpv.java     | 185 +++++-------------
 .../visitors/spirv/VisitorOpsAtomic.java      |   8 +-
 .../visitors/spirv/VisitorOpsMemory.java      | 142 +++++---------
 .../visitors/spirv/VisitorSpirvOutput.java    |  19 +-
 .../processing/compilation/Compilation.java   |   4 +-
 .../visitors/spirv/VisitorOpsMemoryTest.java  |   4 +-
 .../spirv/gpuverify/SpirvRacesTest.java       |   4 +-
 .../global_reduce_strength.spv.dis            |   4 +-
 8 files changed, 127 insertions(+), 243 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/ProgramBuilderSpv.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/ProgramBuilderSpv.java
index a9a5778a6c..01e97320b7 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/ProgramBuilderSpv.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/ProgramBuilderSpv.java
@@ -6,14 +6,16 @@
 import com.dat3m.dartagnan.expression.integers.IntLiteral;
 import com.dat3m.dartagnan.expression.processing.ExprTransformer;
 import com.dat3m.dartagnan.expression.type.FunctionType;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.decorations.BuiltIn;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.decorations.Decoration;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.decorations.DecorationType;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperDecorations;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperTags;
+import com.dat3m.dartagnan.program.memory.ScopedPointer;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.transformers.MemoryTransformer;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.transformers.RegisterTransformer;
+import com.dat3m.dartagnan.program.memory.ScopedPointerVariable;
+import com.dat3m.dartagnan.expression.type.ScopedPointerType;
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.*;
 import com.dat3m.dartagnan.program.event.*;
@@ -41,28 +43,26 @@ public class ProgramBuilderSpv {
 
     private static final Logger logger = LogManager.getLogger(ProgramBuilderSpv.class);
 
+    protected final Map<String, Type> types = new HashMap<>();
+    protected final Map<String, Expression> expressions = new HashMap<>();
+    protected final Set<String> specConstants = new HashSet<>();
+    protected final Map<String, Function> forwardFunctions = new HashMap<>();
+    protected final Map<String, Label> labels = new HashMap<>();
+    protected final Deque<Label> blocks = new ArrayDeque<>();
+    protected final Map<Label, Event> blockEndEvents = new HashMap<>();
+    protected final Map<Label, Map<Register, String>> phiDefinitions = new HashMap<>();
+    protected final Map<Label, Label> cfDefinitions = new HashMap<>();
+    protected final List<Integer> threadGrid;
+    protected final Map<String, Expression> inputs;
+    protected final Program program;
+
+    protected Function currentFunction;
+    protected String entryPointId;
+    protected int nextFunctionId = 0;
+    protected Set<String> nextOps;
+
     private final HelperTags helperTags = new HelperTags();
     private final HelperDecorations helperDecorations;
-    private final Map<String, Type> types = new HashMap<>();
-    private final Map<String, String> pointedTypes = new HashMap<>();
-    private final Map<String, Type> variableTypes = new HashMap<>();
-    private final Map<String, String> pointerClasses = new HashMap<>();
-    private final Map<String, String> registerClasses = new HashMap<>();
-    private final Map<String, Expression> expressions = new HashMap<>();
-    private final Map<String, Function> forwardFunctions = new HashMap<>();
-    private final Map<String, Label> labels = new HashMap<>();
-    private final Deque<Label> blocks = new ArrayDeque<>();
-    private final Map<Label, Event> blockEndEvents = new HashMap<>();
-    private final Map<Label, Map<Register, String>> phiDefinitions = new HashMap<>();
-    private final Map<Label, Label> cfDefinitions = new HashMap<>();
-    private final Set<String> specConstants = new HashSet<>();
-    private final List<Integer> threadGrid;
-    private final Map<String, Expression> inputs;
-    private final Program program;
-    protected Function currentFunction;
-    private String entryPointId;
-    private int nextFunctionId = 0;
-    private Set<String> nextOps;
 
     public ProgramBuilderSpv(List<Integer> threadGrid, Map<String, Expression> inputs) {
         validateThreadGrid(threadGrid);
@@ -109,7 +109,16 @@ public Program build() {
 
         Function entry = getEntryPointFunction();
         BuiltIn builtIn = (BuiltIn) getDecoration(DecorationType.BUILT_IN);
-        MemoryTransformer transformer = new MemoryTransformer(program, builtIn, variableTypes, registerClasses);
+
+        Map<String, Type> vType = expressions.entrySet().stream()
+                .filter(e -> e.getValue() instanceof ScopedPointerVariable)
+                .collect(Collectors.toMap((Map.Entry::getKey), (e -> ((ScopedPointerVariable)e.getValue()).getInnerType())));
+
+        Map<String, String> stClsMap = expressions.entrySet().stream()
+                .filter(e -> e.getValue() instanceof ScopedPointerVariable)
+                .collect(Collectors.toMap((Map.Entry::getKey), (e -> ((ScopedPointerVariable)e.getValue()).getScopeId())));
+
+        MemoryTransformer transformer = new MemoryTransformer(program, builtIn, vType, stClsMap);
         for (int z = 0; z < threadGrid.get(2); z++) {
             for (int y = 0; y < threadGrid.get(1); y++) {
                 for (int x = 0; x < threadGrid.get(0); x++) {
@@ -237,12 +246,10 @@ public Event addEvent(Event event) {
         return event;
     }
 
-    public MemoryObject allocateMemory(int bytes) {
-        return program.getMemory().allocate(bytes);
-    }
-
-    public MemoryObject allocateMemoryVirtual(int bytes) {
-        return program.getMemory().allocateVirtual(bytes, true, null);
+    public ScopedPointerVariable allocateMemoryVirtual(String id, String typeId, Type type, int bytes) {
+        MemoryObject memoryObject = program.getMemory().allocateVirtual(bytes, true, null);
+        memoryObject.setName(id);
+        return new ScopedPointerVariable(id, ((ScopedPointerType) getType(typeId)).getScopeId(), type, memoryObject);
     }
 
     public Expression newUndefinedValue(Type type) {
@@ -261,73 +268,28 @@ public Type addType(String name, Type type) {
         if (types.containsKey(name) || expressions.containsKey(name)) {
             throw new ParsingException("Duplicated definition '%s'", name);
         }
-        //if (TypeFactory.getInstance().isPointerType(type)) {
-        //    throw new ParsingException("Unexpected pointer type '%s'", name);
-        //}
-        types.put(name, type);
-        return type;
-    }
-
-    public Type addPointerType(String name, String innerTypeId, String cls) {
-        if (types.containsKey(name) || expressions.containsKey(name)) {
-            throw new ParsingException("Duplicated definition '%s'", name);
-        }
-        if (pointedTypes.containsKey(name)) {
-            throw new ParsingException("Duplicated pointer type definition '%s'", name);
-        }
-        getType(innerTypeId);
-        pointedTypes.put(name, innerTypeId);
-        if (pointerClasses.containsKey(name)) {
-            throw new ParsingException("Duplicated variable storage class definition '%s'", name);
-        }
-        pointerClasses.put(name, getStorageClass(cls));
-        Type type = TypeFactory.getInstance().getPointerType();
         types.put(name, type);
         return type;
     }
 
-    public Type getPointedType(String name) {
-        String typeId = pointedTypes.get(name);
-        if (typeId == null) {
-            if (!types.containsKey(name)) {
-                throw new ParsingException("Reference to undefined pointer type '%s'", name);
-            }
-            throw new ParsingException("Type '%s' is not a pointer type", name);
-        }
-        return getType(typeId);
-    }
-
-    public Type getVariableType(String name) {
-        Type type = variableTypes.get(name);
-        if (type == null) {
-            throw new ParsingException("Reference to undefined variable '%s'", name);
-        }
-        return type;
-    }
-
-    public Type addVariableType(String name, Type type) {
-        if (variableTypes.containsKey(name)) {
-            throw new ParsingException("Duplicated variable type definition '%s'", name);
-        }
-        variableTypes.put(name, type);
-        return type;
-    }
-
-    public List<MemoryObject> getVariablesWithStorageClass(String storageClass) {
-        return registerClasses.entrySet().stream()
-                .filter(e -> e.getValue().equals(storageClass))
-                .map(e -> getExpression(e.getKey()))
-                .filter(MemoryObject.class::isInstance)
-                .map(e -> (MemoryObject) e)
+    public List<ScopedPointerVariable> getVariablesWithStorageClass(String storageClass) {
+        return expressions.values().stream()
+                .filter(ScopedPointerVariable.class::isInstance)
+                .map(e -> (ScopedPointerVariable)e)
+                .filter(e -> e.getScopeId().equals(storageClass))
                 .toList();
     }
 
     public String getExpressionStorageClass(String name) {
-        String storageClass = registerClasses.get(name);
-        if (storageClass == null) {
-            throw new ParsingException("Reference to undefined pointer '%s'", name);
+        Expression expression = getExpression(name);
+        if (expression instanceof ScopedPointer pExpr) {
+            return pExpr.getScopeId();
+        }
+        if (expression instanceof Register) {
+            // TODO: Hacky, ideally new pointer type for registers
+            return Tag.Spirv.SC_FUNCTION;
         }
-        return storageClass;
+        throw new ParsingException("Reference to undefined pointer '%s'", name);
     }
 
     public Label makeBranchBackJumpLabel(Label label) {
@@ -391,24 +353,10 @@ public Register getRegister(String id) {
     }
 
     public Register addRegister(String id, String typeId) {
-        addStorageClassForExpr(id, typeId);
-        return getCurrentFunctionOrThrowError().newRegister(id, getType(typeId));
-    }
-
-    public String addStorageClassForExpr(String id, String typeId) {
-        if (pointedTypes.containsKey(typeId)) {
-            String storageClass = pointerClasses.get(typeId);
-            if (storageClass == null) {
-                throw new ParsingException("Missing storage class for pointer '%s'", typeId);
-            }
-            if (registerClasses.containsKey(id)) {
-                throw new ParsingException("Duplicated storage class definition  for expression'%s'", id);
-            }
-            registerClasses.put(id, storageClass);
-            return storageClass;
+        if (getType(typeId) instanceof ScopedPointerType) {
+            throw new ParsingException("Register cannot be a pointer");
         }
-        // TODO:
-        return null;
+        return getCurrentFunctionOrThrowError().newRegister(id, getType(typeId));
     }
 
     public boolean hasBlock(String id) {
@@ -625,18 +573,6 @@ public String getCurrentFunctionName() {
         return getCurrentFunctionOrThrowError().getName();
     }
 
-    public Set<Function> getForwardFunctions() {
-        return Set.copyOf(forwardFunctions.values());
-    }
-
-    public Map<Label, Event> getBlockEndEvents() {
-        return Map.copyOf(blockEndEvents);
-    }
-
-    public Map<Label, Label> getCfDefinition() {
-        return Map.copyOf(cfDefinitions);
-    }
-
     public Label makeBranchEndLabel(Label label) {
         String id = label.getName() + "_end";
         if (labels.containsKey(id)) {
@@ -650,23 +586,4 @@ public Label makeBranchEndLabel(Label label) {
     public Map<Register, String> getPhiDefinitions(Label label) {
         return phiDefinitions.computeIfAbsent(label, k -> new HashMap<>());
     }
-
-    public Map<String, Type> getTypes() {
-        return Map.copyOf(types);
-    }
-
-    public Map<String, Expression> getExpressions() {
-        return Map.copyOf(expressions);
-    }
-
-    public List<Label> getBlocks() {
-        return blocks.stream().toList();
-    }
-
-    public MemoryObject getMemoryObject(String id) {
-        return program.getMemory().getObjects().stream()
-                .filter(o -> o.getName().equals(id))
-                .findFirst()
-                .orElseThrow(() -> new ParsingException("Undefined memory object '%s'", id));
-    }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsAtomic.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsAtomic.java
index 8bdfe3a8b8..239e7eed30 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsAtomic.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsAtomic.java
@@ -7,7 +7,6 @@
 import com.dat3m.dartagnan.expression.integers.IntBinaryOp;
 import com.dat3m.dartagnan.expression.integers.IntCmpOp;
 import com.dat3m.dartagnan.expression.type.IntegerType;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.parsers.SpirvBaseVisitor;
 import com.dat3m.dartagnan.parsers.SpirvParser;
 import com.dat3m.dartagnan.program.Register;
@@ -20,7 +19,6 @@
 
 public class VisitorOpsAtomic extends SpirvBaseVisitor<Event> {
 
-    private static final TypeFactory TYPE_FACTORY = TypeFactory.getInstance();
     private final ProgramBuilderSpv builder;
 
     public VisitorOpsAtomic(ProgramBuilderSpv builder) {
@@ -229,11 +227,13 @@ private IntegerType getIntegerType(String typeId) {
     }
 
     private Expression getPointer(String ptrId) {
+        return builder.getExpression(ptrId);
+        /*
         Expression result = builder.getExpression(ptrId);
-        if (builder.getVariableType(ptrId) != null) {
+        if (result instanceof MemoryObject) {
             return result;
         }
-        throw new ParsingException("Unexpected type at '%s', expected pointer but received '%s'", ptrId, result.getType());
+        throw new ParsingException("Unexpected type at '%s', expected pointer but received '%s'", ptrId, result.getType());*/
     }
 
     public Set<String> getSupportedOps() {
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemory.java
index f58c9e0a6f..b1839443df 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemory.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemory.java
@@ -11,11 +11,13 @@
 import com.dat3m.dartagnan.parsers.SpirvParser;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.decorations.BuiltIn;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.decorations.DecorationType;
+import com.dat3m.dartagnan.program.memory.ScopedPointer;
+import com.dat3m.dartagnan.program.memory.ScopedPointerVariable;
+import com.dat3m.dartagnan.expression.type.ScopedPointerType;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.Tag;
-import com.dat3m.dartagnan.program.memory.MemoryObject;
 import org.antlr.v4.runtime.tree.ParseTree;
 
 import java.util.ArrayList;
@@ -83,23 +85,28 @@ public Event visitOpLoad(SpirvParser.OpLoadContext ctx) {
     public Event visitOpVariable(SpirvParser.OpVariableContext ctx) {
         String id = ctx.idResult().getText();
         String typeId = ctx.idResultType().getText();
-        Type type = builder.getPointedType(typeId);
-        Expression value = getOpVariableInitialValue(ctx, type);
-        if (value != null) {
-            type = validateVariableType(id, value, type, value.getType());
-        } else if (!isFixedSize(type)) {
-            throw new ParsingException("Missing initial value for runtime variable '%s'", id);
-        } else {
-            value = builder.newUndefinedValue(type);
+        if (builder.getType(typeId) instanceof ScopedPointerType pType) {
+            Type type = pType.getPointedType();
+            Expression value = getOpVariableInitialValue(ctx, type);
+            if (value != null) {
+                if (!TYPE_FACTORY.isExactTypeOf(value.getType(), type)) {
+                    throw new ParsingException("Mismatching value type for variable '%s', " +
+                            "expected '%s' but received '%s'", id, type, value.getType());
+                }
+                type = value.getType();
+            } else if (!TypeFactory.isExactType(type)) {
+                throw new ParsingException("Missing initial value for runtime variable '%s'", id);
+            } else {
+                value = builder.newUndefinedValue(type);
+            }
+            int size = TYPE_FACTORY.getMemorySizeInBytes(type);
+            ScopedPointerVariable pointer = builder.allocateMemoryVirtual(id, typeId, type, size);
+            setInitialValue(pointer, 0, value);
+            builder.addExpression(id, pointer);
+            validateStorageClass(pointer, ctx.storageClass().getText());
+            return null;
         }
-        int size = TYPE_FACTORY.getMemorySizeInBytes(type);
-        MemoryObject memObj = builder.allocateMemoryVirtual(size);
-        memObj.setName(id);
-        setInitialValue(memObj, 0, value);
-        builder.addExpression(id, memObj);
-        builder.addVariableType(id, type);
-        addVariableStorageClass(id, typeId, ctx.storageClass().getText());
-        return null;
+        throw new ParsingException("Type '%s' is not a pointer type", typeId);
     }
 
     private Expression getOpVariableInitialValue(SpirvParser.OpVariableContext ctx, Type type) {
@@ -124,27 +131,6 @@ private Expression getOpVariableInitialValue(SpirvParser.OpVariableContext ctx,
         return null;
     }
 
-    // TODO: Unit test for a nested runtime type
-    private boolean isFixedSize(Type type) {
-        if (type instanceof BooleanType
-                || type instanceof IntegerType
-                || type instanceof FloatType) {
-            return true;
-        }
-        if (type instanceof ArrayType aType) {
-            return aType.hasKnownNumElements() && isFixedSize(aType.getElementType());
-        }
-        if (type instanceof AggregateType aType) {
-            for (Type elType : aType.getDirectFields()) {
-                if (!isFixedSize(elType)) {
-                    return false;
-                }
-            }
-            return true;
-        }
-        throw new ParsingException("Unexpected variable type '%s'", type);
-    }
-
     private Expression castInput(String id, Type type, Expression value) {
         if (type instanceof ArrayType aType) {
             return castInputArray(id, aType, value);
@@ -160,12 +146,14 @@ private Expression castInputArray(String id, ArrayType type, Expression value) {
             // TODO: Handle empty arrays
             int size = type.getNumElements();
             if (size != -1 && size != cValue.getOperands().size()) {
-                // TODO: Add a unit test for this
                 throw new ParsingException("Unexpected number of elements in variable '%s', " +
-                        "expected '%d' elements but received '%d' elements", id, size, cValue.getOperands().size());
+                        "expected %d but received %d", id, size, cValue.getOperands().size());
             }
             Type eType = type.getElementType();
-            List<Expression> elements = cValue.getOperands().stream().map(a -> castInput(id, eType, a)).toList();
+            List<Expression> elements = new ArrayList<>();
+            for (int i = 0; i < cValue.getOperands().size(); i++) {
+                elements.add(castInput(String.format("%s[%d]", id, i), eType, cValue.getOperands().get(i)));
+            }
             return EXPR_FACTORY.makeArray(elements.get(0).getType(), elements, true);
         }
         throw new ParsingException("Mismatching value type for variable '%s', " +
@@ -177,9 +165,8 @@ private Expression castInputAggregate(String id, AggregateType type, Expression
             // TODO: Test empty structures
             int size = type.getDirectFields().size();
             if (size != cValue.getOperands().size()) {
-                // TODO: Add a unit test for this
                 throw new ParsingException("Unexpected number of elements in variable '%s', " +
-                        "expected '%d' elements but received '%d' elements", id, size, cValue.getOperands().size());
+                        "expected %d but received %d", id, size, cValue.getOperands().size());
             }
             List<Expression> elements = new ArrayList<>();
             for (int i = 0; i < size; i++) {
@@ -214,66 +201,39 @@ private Expression castInputScalar(String id, Type type, Expression value) {
                 "the value is not constant", id);
     }
 
-    private Type validateVariableType(String id, Expression value, Type varType, Type valType) {
-        if (varType.equals(valType)) {
-            return valType;
-        }
-        if (varType instanceof AggregateType t1 && valType instanceof AggregateType t2) {
-            int size = t1.getDirectFields().size();
-            if (size == t2.getDirectFields().size()) {
-                for (int i = 0; i < size; i++) {
-                    validateVariableType(id, value, t1.getDirectFields().get(i), t2.getDirectFields().get(i));
-                }
-                return valType;
-            }
-        }
-        if (varType instanceof ArrayType t1 && valType instanceof ArrayType t2) {
-            if (t1.getNumElements() == -1) {
-                if (t2.getNumElements() > 0) {
-                    return valType;
-                }
-            } else if (t1.getNumElements() == t2.getNumElements()) {
-                validateVariableType(id, value, t1.getElementType(), t2.getElementType());
-                return valType;
-            }
-        }
-        throw new ParsingException("Mismatching value type for variable '%s', " +
-                "expected '%s' but received '%s'", id, varType, valType);
-    }
-
-    private void setInitialValue(MemoryObject memObj, int offset, Expression value) {
+    private void setInitialValue(ScopedPointerVariable pointer, int offset, Expression value) {
         if (value.getType() instanceof ArrayType aType) {
             ConstructExpr cValue = (ConstructExpr) value;
             List<Expression> elements = cValue.getOperands();
             int step = TYPE_FACTORY.getMemorySizeInBytes(aType.getElementType());
             for (int i = 0; i < elements.size(); i++) {
-                setInitialValue(memObj, offset + i * step, elements.get(i));
+                setInitialValue(pointer, offset + i * step, elements.get(i));
             }
         } else if (value.getType() instanceof AggregateType) {
             ConstructExpr cValue = (ConstructExpr) value;
             final List<Expression> elements = cValue.getOperands();
             int currentOffset = offset;
             for (Expression element : elements) {
-                setInitialValue(memObj, currentOffset, element);
+                setInitialValue(pointer, currentOffset, element);
                 currentOffset += TYPE_FACTORY.getMemorySizeInBytes(element.getType());
             }
         } else if (value.getType() instanceof IntegerType) {
-            memObj.setInitialValue(offset, value);
+            pointer.setInitialValue(offset, value);
         } else if (value.getType() instanceof BooleanType) {
-            memObj.setInitialValue(offset, value);
+            pointer.setInitialValue(offset, value);
         } else {
             throw new ParsingException("Illegal variable value type '%s'", value.getType());
         }
     }
 
     // TODO: Unit tests for this
-    private void addVariableStorageClass(String id, String typeId, String classToken) {
-        String ptrStorageClass = builder.addStorageClassForExpr(id, typeId);
+    private void validateStorageClass(ScopedPointerVariable pointer, String classToken) {
+        String ptrStorageClass = pointer.getScopeId();
         String varStorageClass = builder.getStorageClass(classToken);
         if (!varStorageClass.equals(ptrStorageClass)) {
             throw new ParsingException("Mismatching storage class for variable '%s', " +
                     "definition storage class is '%s' but pointer storage class is '%s'",
-                    id, varStorageClass, ptrStorageClass);
+                    pointer.getId(), varStorageClass, ptrStorageClass);
         }
         if (Tag.Spirv.SC_GENERIC.equals(ptrStorageClass)) {
             throw new ParsingException("Illegal variable storage class '%s'", ptrStorageClass);
@@ -296,16 +256,22 @@ public Event visitOpInBoundsAccessChain(SpirvParser.OpInBoundsAccessChainContext
 
     private void visitOpAccessChain(String id, String typeId, String baseId,
                                     List<SpirvParser.IndexesIdRefContext> idxContexts) {
-        Type resultType = builder.getPointedType(typeId);
-        Type baseType = builder.getVariableType(baseId);
-        Expression base = builder.getExpression(baseId);
-        List<Expression> indexes = idxContexts.stream()
-                .map(c -> builder.getExpression(c.getText()))
-                .toList();
-        // TODO: Merge with GEPExpression?
-        builder.addStorageClassForExpr(id, typeId);
-        Expression expression = EXPR_FACTORY.makeBinary(base, ADD, getMemberPtr(id, resultType, baseType, indexes));
-        builder.addExpression(id, expression);
+        if (builder.getType(typeId) instanceof ScopedPointerType pType) {
+            Type resultType = pType.getPointedType();
+            // TODO: Validate type
+            ScopedPointer base = (ScopedPointer) builder.getExpression(baseId);
+            Type baseType = base.getInnerType();
+            List<Expression> indexes = idxContexts.stream()
+                    .map(c -> builder.getExpression(c.getText()))
+                    .toList();
+            // TODO: Merge with GEPExpression?
+            Expression expression = EXPR_FACTORY.makeBinary(base, ADD, getMemberPtr(id, resultType, baseType, indexes));
+            // TODO: resultType is from a pointer, use a concrete type instead
+            ScopedPointer pointer = new ScopedPointer(id, pType.getScopeId(), resultType, expression);
+            builder.addExpression(id, pointer);
+            return;
+        }
+        throw new ParsingException("Type '%s' is not a pointer type", typeId);
     }
 
     private Expression getMemberPtr(String id, Type resultType, Type type, List<Expression> indexes) {
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 a6c8e69c56..fd64a6c9e3 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
@@ -9,8 +9,8 @@
 import com.dat3m.dartagnan.expression.type.*;
 import com.dat3m.dartagnan.parsers.SpirvBaseVisitor;
 import com.dat3m.dartagnan.parsers.SpirvParser;
+import com.dat3m.dartagnan.program.memory.ScopedPointerVariable;
 import com.dat3m.dartagnan.program.memory.Location;
-import com.dat3m.dartagnan.program.memory.MemoryObject;
 import com.dat3m.dartagnan.program.specification.*;
 
 import java.util.HashMap;
@@ -120,7 +120,7 @@ private Expression acceptAssertionValue(SpirvParser.AssertionValueContext ctx) {
             return EXPR_FACTORY.parseValue(ctx.initBaseValue().getText(), TYPE_FACTORY.getArchType());
         }
         String name = ctx.varName().getText();
-        MemoryObject base = builder.getMemoryObject(name);
+        ScopedPointerVariable base = (ScopedPointerVariable) builder.getExpression(name);
         if (base != null) {
             List<Integer> indexes = ctx.indexValue().stream().map(this::acceptIndexValue).toList();
             return createLocation(base, indexes);
@@ -128,12 +128,11 @@ private Expression acceptAssertionValue(SpirvParser.AssertionValueContext ctx) {
         throw new ParsingException("Uninitialized location %s", name);
     }
 
-    private Location createLocation(MemoryObject base, List<Integer> indexes) {
-        String name = base.getName();
-        Type type = builder.getVariableType(name);
+    private Location createLocation(ScopedPointerVariable base, List<Integer> indexes) {
+        Type type = base.getInnerType();
         int offset = 0;
         for (int index : indexes) {
-            validateIndex(name, type, index);
+            validateIndex(base.getId(), type, index);
             if (type instanceof ArrayType arrayType) {
                 Type elementType = arrayType.getElementType();
                 int byteWidth = TYPE_FACTORY.getMemorySizeInBytes(elementType);
@@ -147,11 +146,11 @@ private Location createLocation(MemoryObject base, List<Integer> indexes) {
             }
         }
         if (type instanceof ArrayType || type instanceof AggregateType) {
-            throw new ParsingException("Illegal assertion for variable '%s', index not deep enough", name);
+            throw new ParsingException("Illegal assertion for variable '%s', index not deep enough", base.getId());
         }
-        String offsetName = indexes.isEmpty() ? name :
-                name + "[" + String.join("][", indexes.stream().map(Object::toString).toArray(String[]::new)) + "]";
-        Location location =  new Location(offsetName, base, offset);
+        String offsetName = indexes.isEmpty() ? base.getId() :
+                base.getId() + "[" + String.join("][", indexes.stream().map(Object::toString).toArray(String[]::new)) + "]";
+        Location location =  new Location(offsetName, base.getAddress(), offset);
         locationTypes.put(location, type);
         return location;
     }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/Compilation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/Compilation.java
index e55e03854e..8bc0e9ac34 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/Compilation.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/Compilation.java
@@ -38,7 +38,7 @@ public class Compilation implements ProgramProcessor {
     public Arch getTarget() { return target; }
     public void setTarget(Arch target) {
         this.target = target;
-        compiler = getCompiler();
+        this.compiler = getCompiler();
     }
 
     @Option(name = USE_RC11_TO_ARCH_SCHEME,
@@ -81,6 +81,7 @@ public void run(Program program) {
             logger.warn("Skipped compilation: Program is already compiled to {}", program.getArch());
             return;
         }
+        // TODO:
         if (program.getFormat() == Program.SourceLanguage.SPV) {
             compiler = new VisitorSpirvVulkan();
         }
@@ -113,6 +114,7 @@ private void run(Function function) {
      */
     // TODO: Refactoring. This shouldn't be used from outside,
     //  and the compiler should be resolved when program is passed
+
     public List<Event> getCompilationResult(Event toBeCompiled) {
         compiler.funcToBeCompiled = toBeCompiled.getFunction();
         return toBeCompiled.accept(compiler);
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 a47b3e9e50..71ce287e8c 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
@@ -551,7 +551,7 @@ public void testMismatchingValueTypeInNestedArray() {
         } catch (ParsingException e) {
             // then
             assertEquals("Mismatching value type for variable '%v', " +
-                    "expected 'bv32' but received 'bool'", e.getMessage());
+                    "expected '[2 x [2 x bv32]]' but received '[2 x [2 x bool]]'", e.getMessage());
         }
     }
 
@@ -583,7 +583,7 @@ public void testMismatchingValueTypeInNestedStruct() {
         } catch (ParsingException e) {
             // then
             assertEquals("Mismatching value type for variable '%v', " +
-                    "expected 'bv16' but received 'bv32'", e.getMessage());
+                    "expected '{ bool, { bool, bv16 } }' but received '{ bool, { bool, bv32 } }'", e.getMessage());
         }
     }
 
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java
index 3a7733b8c8..37bde4b71b 100644
--- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java
@@ -98,8 +98,8 @@ public static Iterable<Object[]> data() throws IOException {
                 {"test_2d_local_index_inference_2.spv.dis", 1, PASS},
                 {"test_for_benign_read_write_bug.spv.dis", 1, FAIL},
                 {"test_local_id_inference.spv.dis", 1, PASS},
-                {"test_mod_invariants/global_reduce_strength.spv.dis", 2, UNKNOWN},
-                {"test_mod_invariants/local_direct.spv.dis", 2, UNKNOWN},
+                {"test_mod_invariants/global_reduce_strength.spv.dis", 1, UNKNOWN},
+                //{"test_mod_invariants/local_direct.spv.dis", 2, UNKNOWN},
                 {"test_part_load_store/store_int_and_short.spv.dis", 1, PASS},
                 {"test_structs/use_array_element.spv.dis", 1, PASS},
                 {"test_structs/use_element.spv.dis", 1, PASS},
diff --git a/dartagnan/src/test/resources/spirv/gpuverify/test_mod_invariants/global_reduce_strength.spv.dis b/dartagnan/src/test/resources/spirv/gpuverify/test_mod_invariants/global_reduce_strength.spv.dis
index 1f6dd33986..0b1f50b75a 100644
--- a/dartagnan/src/test/resources/spirv/gpuverify/test_mod_invariants/global_reduce_strength.spv.dis
+++ b/dartagnan/src/test/resources/spirv/gpuverify/test_mod_invariants/global_reduce_strength.spv.dis
@@ -1,6 +1,6 @@
 ; @Input: %18 = {{0, 0, 0, 0, 0, 0, 0, 0, 0}}
-; @Input: %19 = {{0, 0, 0, 0, 0, 0, 0, 0, 0}}
-; @Input: %20 = {{0, 0, 0, 0, 0, 0, 0, 0, 0}}
+; @Input: %19 = {{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}}
+; @Input: %20 = {{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}}
 ; @Config: 3, 1, 3
 ; SPIR-V
 ; Version: 1.6