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 index a63fbfdb20..d1fa5b7391 100644 --- 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 parame } public AggregateType getAggregateType(List 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 fields, List offsets) { @@ -82,11 +83,11 @@ public AggregateType getAggregateType(List fields, List 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 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 index 2a0c87faee..f9d46870bd 100644 --- 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 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 fields, List offsets, int size) { testDefaultOffsets(fields, offsets, size); testExplicitOffsets(fields, offsets, size);