Fix handling of empty type (#776)

hernanponcedeleon · Nov 11, 2024 · 025e4a7 · 025e4a7
1 parent 749c055
commit 025e4a7
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 12 deletions.
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
@@ -5,7 +5,10 @@
 import com.google.common.math.IntMath;
 
 import java.math.RoundingMode;
-import java.util.*;
+import java.util.ArrayList;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
 import java.util.stream.IntStream;
 
 import static com.google.common.base.Preconditions.checkArgument;
@@ -70,9 +73,7 @@ public FunctionType getFunctionType(Type returnType, List<? extends Type> parame
     }
 
     public AggregateType getAggregateType(List<Type> fields) {
-        checkNotNull(fields);
-        checkArgument(fields.stream().noneMatch(t -> t == voidType), "Void fields are not allowed");
-        return typeNormalizer.normalize(new AggregateType(fields, computeDefaultOffsets(fields)));
+        return getAggregateType(fields, computeDefaultOffsets(fields));
     }
 
     public AggregateType getAggregateType(List<Type> fields, List<Integer> offsets) {
@@ -82,11 +83,11 @@ public AggregateType getAggregateType(List<Type> fields, List<Integer> offsets)
         checkArgument(fields.size() == offsets.size(), "Offsets number does not match the fields number");
         checkArgument(offsets.stream().noneMatch(o -> o < 0), "Offset cannot be negative");
         checkArgument(offsets.isEmpty() || offsets.get(0) == 0, "The first offset must be zero");
-        checkArgument(IntStream.range(1, offsets.size()).boxed().allMatch(
+        checkArgument(IntStream.range(1, offsets.size()).allMatch(
                 i -> offsets.get(i) >= offsets.get(i - 1) + Integer.max(0, getMemorySizeInBytes(fields.get(i - 1), false))),
                 "Offset is too small");
-        checkArgument(IntStream.range(0, offsets.size() - 1).boxed().allMatch(
-                i -> getMemorySizeInBytes(fields.get(i)) > 0),
+        checkArgument(IntStream.range(0, fields.size() - 1).allMatch(
+                i -> hasKnownSize(fields.get(i))),
                 "Non-last element with unknown size");
         return typeNormalizer.normalize(new AggregateType(fields, offsets));
     }
@@ -146,12 +147,12 @@ public int getMemorySizeInBytes(Type type, boolean padded) {
         }
         if (type instanceof AggregateType aType) {
             List<TypeOffset> typeOffsets = aType.getTypeOffsets();
+            if (aType.getTypeOffsets().stream().anyMatch(o -> !hasKnownSize(o.type()))) {
+                return -1;
+            }
             if (typeOffsets.isEmpty()) {
                 return 0;
             }
-            if (aType.getTypeOffsets().stream().anyMatch(o -> getMemorySizeInBytes(o.type()) < 0)) {
-                return -1;
-            }
             TypeOffset lastTypeOffset = typeOffsets.get(typeOffsets.size() - 1);
             int baseSize = lastTypeOffset.offset() + getMemorySizeInBytes(lastTypeOffset.type());
             if (padded) {
@@ -167,10 +168,10 @@ public int getAlignment(Type type) {
             return getMemorySizeInBytes(type);
         }
         if (type instanceof ArrayType arrayType) {
-            return getMemorySizeInBytes(arrayType.getElementType());
+            return getAlignment(arrayType.getElementType());
         }
         if (type instanceof AggregateType aType) {
-            return aType.getTypeOffsets().stream().map(o -> getAlignment(o.type())).max(Integer::compare).orElseThrow();
+            return aType.getTypeOffsets().stream().map(o -> getAlignment(o.type())).max(Integer::compare).orElse(1);
         }
         throw new UnsupportedOperationException("Cannot compute memory layout of type " + type);
     }
@@ -183,6 +184,8 @@ public static int paddedSize(int size, int alignment) {
         return size;
     }
 
+    public boolean hasKnownSize(Type type) { return getMemorySizeInBytes(type) >= 0; }
+
     public int getMemorySizeInBits(Type type) {
         return getMemorySizeInBytes(type) * 8;
     }

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/expression/type/AggregateTypeTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/expression/type/AggregateTypeTest.java
@@ -85,6 +85,20 @@ public void testIllegalOffsets() {
         testIllegalOffsets(List.of(arr, i32), List.of(0, 8), "Non-last element with unknown size");
     }
 
+    @Test
+    public void testEmptyType() {
+        Type empty = types.getAggregateType(List.of());
+        Type emptyAlt = types.getAggregateType(List.of(), List.of());
+
+        assertEquals(empty, emptyAlt);
+
+        Type i32 = types.getIntegerType(32);
+        List<Type> structMembers = List.of(empty, i32, empty, empty, i32, empty);
+
+        testDefaultOffsets(structMembers, List.of(0, 0, 4, 4, 4, 8), 8);
+        testExplicitOffsets(structMembers, List.of(0, 0, 4, 5, 8, 13), 16);
+    }
+
     private void testStandardOffsets(List<Type> fields, List<Integer> offsets, int size) {
         testDefaultOffsets(fields, offsets, size);
         testExplicitOffsets(fields, offsets, size);