add padding Index to ArrayType

tonghaining · tonghaining · commit 5f09ecb5b317 · 2025-04-29T15:59:29.000+02:00
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/ArrayType.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/ArrayType.java
@@ -6,10 +6,20 @@ public class ArrayType implements Type {
 
     private final Type elementType;
     private final int numElements;
+    private final int paddingStart;
 
     ArrayType(Type elementType, int numElements) {
+        this(elementType, numElements, numElements + 1);
+    }
+
+    ArrayType(Type elementType, int numElements, int paddingStart) {
         this.elementType = elementType;
         this.numElements = numElements;
+        this.paddingStart = paddingStart;
+    }
+
+    public int getPaddingStart() {
+        return paddingStart;
     }
 
     // NOTE: We use empty arrays to represent unknown size.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/TypeFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/TypeFactory.java
@@ -123,6 +123,13 @@ public ArrayType getArrayType(Type element, int size) {
         return typeNormalizer.normalize(new ArrayType(element, size));
     }
 
+    public ArrayType getArrayType(Type element, int size, int paddingStart) {
+        checkArgument(0 <= size, "Negative element count in array.");
+        checkArgument(0 <= paddingStart, "Negative padding start index in array.");
+        checkArgument(paddingStart <= size, "Padding start index %s is greater than array size %s", paddingStart, size);
+        return typeNormalizer.normalize(new ArrayType(element, size, paddingStart));
+    }
+
     public IntegerType getArchType() {
         return pointerDifferenceType;
     }
@@ -268,7 +275,7 @@ public static boolean isStaticTypeOf(Type staticType, Type runtimeType) {
         }
         if (staticType instanceof ArrayType aStaticType && runtimeType instanceof ArrayType aRuntimeType) {
             int countStatic = aStaticType.getNumElements();
-            int countRuntime = aRuntimeType.getNumElements();
+            int countRuntime = Math.min(aRuntimeType.getPaddingStart(), aRuntimeType.getNumElements());
             if (countStatic != countRuntime && (countRuntime != -1 || countStatic <= 0)) {
                 return false;
             }
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
@@ -169,7 +169,7 @@ private Expression getOpVariableInitialValue(SpirvParser.OpVariableContext ctx,
         }
         Expression initExpr = builder.getExpression(ctx.initializer().getText());
         if (alignment.getValue(id) != null) {
-            initExpr = HelperTypes.getAlignedValue(id, initExpr, type);
+            initExpr = builder.getAlignedValue(id, initExpr, type);
         }
         return initExpr;
     }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ProgramBuilder.java
@@ -5,9 +5,8 @@
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
 import com.dat3m.dartagnan.expression.Type;
-import com.dat3m.dartagnan.expression.type.FunctionType;
-import com.dat3m.dartagnan.expression.type.ScopedPointerType;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
+import com.dat3m.dartagnan.expression.aggregates.ConstructExpr;
+import com.dat3m.dartagnan.expression.type.*;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.decorations.BuiltIn;
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Program;
@@ -23,9 +22,11 @@
 import com.dat3m.dartagnan.program.processing.transformers.MemoryTransformer;
 
 import java.util.HashMap;
+import java.util.List;
 import java.util.Map;
 import java.util.Set;
 import java.util.stream.Collectors;
+import java.util.stream.IntStream;
 
 import static com.dat3m.dartagnan.parsers.program.visitors.spirv.decorations.DecorationType.BUILT_IN;
 
@@ -51,6 +52,34 @@ public ProgramBuilder(ThreadGrid grid) {
         this.decorationsBuilder = new DecorationsBuilder(grid);
     }
 
+    public Expression getAlignedValue(String id, Expression base, Type type) {
+        if (type instanceof AggregateType aggregateType && base instanceof ConstructExpr constructExpr) {
+            List<Expression> elements = aggregateType.getFields().stream()
+                    .map(field -> {
+                        int index = aggregateType.getFields().indexOf(field);
+                        return getAlignedValue(id, constructExpr.getOperands().get(index), field.type());
+                    })
+                    .collect(Collectors.toList());
+            return ExpressionFactory.getInstance().makeConstruct(type, elements);
+        }
+        if (type instanceof ArrayType arrayType && base instanceof ConstructExpr constructExpr) {
+            int numOperands = constructExpr.getOperands().size();
+            if (arrayType.getNumElements() < numOperands) {
+                throw new ParsingException("Array initializer has too many elements for variable '%s'", id);
+            }
+            List<Expression> elements = IntStream.range(0, arrayType.getNumElements())
+                    .mapToObj(i -> i < numOperands
+                            ? getAlignedValue(id, constructExpr.getOperands().get(i), arrayType.getElementType())
+                            : makeUndefinedValue(arrayType.getElementType()))
+                    .collect(Collectors.toList());
+            return ExpressionFactory.getInstance().makeArray(arrayType.getElementType(), elements, true);
+        }
+        if (base.getType().equals(type)) {
+            return base;
+        }
+        throw new ParsingException("Cannot align initializer for variable '" + id + "' of type " + type);
+    }
+
     public Program build() {
         validateBeforeBuild();
         controlFlowBuilder.build();
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/helpers/HelperTypes.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/helpers/HelperTypes.java
@@ -10,9 +10,7 @@
 import com.dat3m.dartagnan.expression.type.*;
 
 import java.util.ArrayList;
-import java.util.Collections;
 import java.util.List;
-import java.util.stream.Collectors;
 import java.util.stream.IntStream;
 
 import static com.dat3m.dartagnan.expression.integers.IntBinaryOp.ADD;
@@ -69,23 +67,6 @@ public static Expression getMemberAddress(String id, Expression base, Type type,
         return base;
     }
 
-    public static Expression getAlignedValue(String id, Expression base, Type type) {
-        if (type instanceof AggregateType aggregateType && base instanceof ConstructExpr constructExpr) {
-            List<Expression> elements = IntStream.range(0, aggregateType.getFields().size())
-                    .mapToObj(i -> {
-                        Type elType = aggregateType.getFields().get(i).type();
-                        Expression elBase = constructExpr.getOperands().get(i);
-                        return getAlignedValue(id, elBase, elType);
-                    })
-                    .collect(Collectors.toList());
-            return expressions.makeConstruct(type, elements);
-        }
-        if (base.getType().equals(type)) {
-            return base;
-        }
-        throw new ParsingException("Cannot align initializer for variable '" + id + "' of type " + type);
-    }
-
     public static Expression createResultExpression(String id, Type type, Expression op1, Expression op2, IntBinaryOp op) {
         if (type instanceof BooleanType || type instanceof IntegerType || type instanceof FloatType) {
             return expressions.makeBinary(op1, op, op2);
@@ -211,18 +192,13 @@ public static Type getAlignedType(Type type, int alignmentNum) {
         }
         if (type instanceof ArrayType arrayType) {
             Type elementType = arrayType.getElementType();
-            int elementAlignmentNum;
-            if (types.getMemorySizeInBytes(elementType) > alignmentNum) {
-                elementType = getAlignedType(elementType, alignmentNum);
-                elementAlignmentNum = types.getMemorySizeInBytes(elementType);
-            } else {
-                elementAlignmentNum = alignmentNum;
+            int arraySizeInBytes = types.getMemorySizeInBytes(arrayType);
+            if (arraySizeInBytes > alignmentNum) {
+                return types.getArrayType(getAlignedType(elementType, alignmentNum), arrayType.getNumElements());
             }
-            List<Type> elementTypes = Collections.nCopies(arrayType.getNumElements(), elementType);
-            List<Integer> alignmentList = IntStream.range(0, arrayType.getNumElements())
-                    .mapToObj(i -> i * elementAlignmentNum)
-                    .collect(Collectors.toList());
-            return types.getAggregateType(elementTypes, alignmentList);
+            int paddedSize = alignmentNum / types.getMemorySizeInBytes(elementType);
+            int paddingStart = arrayType.getNumElements();
+            return types.getArrayType(elementType, paddedSize, paddingStart);
         }
         throw new ParsingException("Invalid type '%s' for alignment '%d'", type, alignmentNum);
     }
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
@@ -247,7 +247,9 @@ public void testAlignedVariable() {
         assertEquals(256, ((IntegerType) v1.getInnerType()).getBitWidth());
         ScopedPointerVariable v2 = (ScopedPointerVariable) builder.getExpression("%v2");
         assertNotNull(v2);
-        assertEquals(64, ((AggregateType) v2.getInnerType()).getFields().get(1).offset());
+        assertEquals(64, TypeFactory.getInstance().getMemorySizeInBytes(v2.getInnerType()));
+        assertEquals(4, ((ArrayType) v2.getInnerType()).getNumElements());
+        assertEquals(3, ((ArrayType) v2.getInnerType()).getPaddingStart());
     }
 
     @Test

Original file line number	Diff line number	Diff line change
`@@ -123,6 +123,13 @@ public ArrayType getArrayType(Type element, int size) {`
`123`	`123`	`return typeNormalizer.normalize(new ArrayType(element, size));`
`124`	`124`	`}`
`125`	`125`
	`126`	`+ public ArrayType getArrayType(Type element, int size, int paddingStart) {`
	`127`	`+ checkArgument(0 <= size, "Negative element count in array.");`
	`128`	`+ checkArgument(0 <= paddingStart, "Negative padding start index in array.");`
	`129`	`+ checkArgument(paddingStart <= size, "Padding start index %s is greater than array size %s", paddingStart, size);`
	`130`	`+ return typeNormalizer.normalize(new ArrayType(element, size, paddingStart));`
	`131`	`+ }`
	`132`	`+`
`126`	`133`	`public IntegerType getArchType() {`
`127`	`134`	`return pointerDifferenceType;`
`128`	`135`	`}`
`@@ -268,7 +275,7 @@ public static boolean isStaticTypeOf(Type staticType, Type runtimeType) {`
`268`	`275`	`}`
`269`	`276`	`if (staticType instanceof ArrayType aStaticType && runtimeType instanceof ArrayType aRuntimeType) {`
`270`	`277`	`int countStatic = aStaticType.getNumElements();`
`271`		`- int countRuntime = aRuntimeType.getNumElements();`
	`278`	`+ int countRuntime = Math.min(aRuntimeType.getPaddingStart(), aRuntimeType.getNumElements());`
`272`	`279`	`if (countStatic != countRuntime && (countRuntime != -1 \|\| countStatic <= 0)) {`
`273`	`280`	`return false;`
`274`	`281`	`}`
Original file line number	Diff line number	Diff line change
`@@ -169,7 +169,7 @@ private Expression getOpVariableInitialValue(SpirvParser.OpVariableContext ctx,`
`169`	`169`	`}`
`170`	`170`	`Expression initExpr = builder.getExpression(ctx.initializer().getText());`
`171`	`171`	`if (alignment.getValue(id) != null) {`
`172`		`- initExpr = HelperTypes.getAlignedValue(id, initExpr, type);`
	`172`	`+ initExpr = builder.getAlignedValue(id, initExpr, type);`
`173`	`173`	`}`
`174`	`174`	`return initExpr;`
`175`	`175`	`}`