From 360c094189bd8f6334b23be6ea66f8b7677d9563 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Sat, 9 Nov 2024 19:49:47 +0100 Subject: [PATCH 1/4] Disable RegisterDecomposition (hopefully subsumed by SCCP). --- .../com/dat3m/dartagnan/expression/type/TypeFactory.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 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 index a63fbfdb20..c7307d93fb 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; @@ -170,7 +173,7 @@ public int getAlignment(Type type) { return getMemorySizeInBytes(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); } From c385a454dd86ac9b50247a2bc6585afe70280b00 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Sun, 10 Nov 2024 22:40:39 +0100 Subject: [PATCH 2/4] Allow 0-sized members in TypeFactory.getAggregateType Fixed alignment computation of arrays. Added TypeFactory.hasKnownSize helper function. --- .../expression/type/TypeFactory.java | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 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 index c7307d93fb..099b0f5688 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 @@ -73,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) { @@ -85,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)); } @@ -149,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(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) { @@ -170,7 +168,7 @@ 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).orElse(1); @@ -186,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; } From ea0478ab4542b9c566cdfbb05da838ec812e0ca2 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 11 Nov 2024 00:03:05 +0100 Subject: [PATCH 3/4] Fixed wrong parameter causing endless recursion. --- .../java/com/dat3m/dartagnan/expression/type/TypeFactory.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 099b0f5688..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 @@ -147,7 +147,7 @@ public int getMemorySizeInBytes(Type type, boolean padded) { } if (type instanceof AggregateType aType) { List typeOffsets = aType.getTypeOffsets(); - if (aType.getTypeOffsets().stream().anyMatch(o -> !hasKnownSize(type))) { + if (aType.getTypeOffsets().stream().anyMatch(o -> !hasKnownSize(o.type()))) { return -1; } if (typeOffsets.isEmpty()) { From ba9aea0b3fdb156c10fcdf12dc597dac0f8f2a28 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 11 Nov 2024 10:51:09 +0100 Subject: [PATCH 4/4] Add unit tests for empty struct type --- .../expression/type/AggregateTypeTest.java | 14 ++++++++++++++ 1 file changed, 14 insertions(+) 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);