diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorSpirv.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorSpirv.java index 86c5d52704..f0e88ad0ba 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorSpirv.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorSpirv.java @@ -66,6 +66,7 @@ public Program visitOp(SpirvParser.OpContext ctx) { private ProgramBuilder createBuilder(SpirvParser.SpvContext ctx) { ThreadGrid grid = new ThreadGrid(1, 1, 1, 1, 1); + SpirvVersion version = SpirvVersion.parse(ctx.getStart().getInputStream().toString()); boolean hasConfig = false; for (SpirvParser.SpvHeaderContext header : ctx.spvHeaders().spvHeader()) { SpirvParser.ConfigHeaderContext cfgCtx = header.configHeader(); @@ -85,7 +86,7 @@ private ProgramBuilder createBuilder(SpirvParser.SpvContext ctx) { logger.warn("Unknown header {}", unknownCtx.ModeHeader_UnknownType()); } } - return new ProgramBuilder(grid); + return new ProgramBuilder(grid, version); } private void initializeVisitors() { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/SpirvVersion.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/SpirvVersion.java new file mode 100644 index 0000000000..265fcea7e4 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/SpirvVersion.java @@ -0,0 +1,33 @@ +package com.dat3m.dartagnan.parsers.program.visitors.spirv; + +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +public record SpirvVersion(int major, int minor) implements Comparable { + + public static final SpirvVersion UNKNOWN = new SpirvVersion(0, 0); + private static final Pattern VERSION_PATTERN = Pattern.compile( + "(?m)^\\s*;\\s*Version:\\s*(\\d+)\\.(\\d+)\\s*$"); + + public static SpirvVersion parse(String input) { + Matcher matcher = VERSION_PATTERN.matcher(input); + return matcher.find() + ? new SpirvVersion(Integer.parseInt(matcher.group(1)), Integer.parseInt(matcher.group(2))) + : UNKNOWN; + } + + public boolean isAtLeast(SpirvVersion other) { + return compareTo(other) >= 0; + } + + @Override + public int compareTo(SpirvVersion other) { + int majorComparison = Integer.compare(major, other.major); + return majorComparison != 0 ? majorComparison : Integer.compare(minor, other.minor); + } + + @Override + public String toString() { + return major + "." + minor; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlow.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlow.java index ceac27f947..5285f3dea9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlow.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlow.java @@ -21,6 +21,7 @@ public class VisitorOpsControlFlow extends SpirvBaseVisitor { + private static final SpirvVersion VERSION_1_6 = new SpirvVersion(1, 6); private static final TypeFactory types = TypeFactory.getInstance(); private final ProgramBuilder builder; private final ControlFlowBuilder cfBuilder; @@ -104,8 +105,8 @@ public Event visitOpBranchConditional(SpirvParser.OpBranchConditionalContext ctx Expression guard = builder.getExpression(ctx.condition().getText()); String trueLabelId = ctx.trueLabel().getText(); String falseLabelId = ctx.falseLabel().getText(); - if (trueLabelId.equals(falseLabelId)) { - throw new ParsingException("Labels of conditional branch cannot be the same"); + if (trueLabelId.equals(falseLabelId) && builder.getSpirvVersion().isAtLeast(VERSION_1_6)) { + throw new ParsingException("Labels of conditional branch must be different in SPIR-V 1.6 and later"); } if (mergeLabelId != null) { if (continueLabelId != null) { 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 index 10f4db6083..8aa11f34bd 100644 --- 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 @@ -8,6 +8,7 @@ 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.parsers.program.visitors.spirv.SpirvVersion; import com.dat3m.dartagnan.parsers.program.visitors.spirv.decorations.BuiltIn; import com.dat3m.dartagnan.program.*; import com.dat3m.dartagnan.program.event.Event; @@ -33,6 +34,7 @@ public class ProgramBuilder { protected final Map inputs = new HashMap<>(); protected final Map debugInfos = new HashMap<>(); protected final ThreadGrid grid; + private final SpirvVersion spirvVersion; protected final Program program; protected ControlFlowBuilder controlFlowBuilder; protected DecorationsBuilder decorationsBuilder; @@ -43,7 +45,12 @@ public class ProgramBuilder { protected Set nextOps; public ProgramBuilder(ThreadGrid grid) { + this(grid, SpirvVersion.UNKNOWN); + } + + public ProgramBuilder(ThreadGrid grid, SpirvVersion spirvVersion) { this.grid = grid; + this.spirvVersion = spirvVersion; this.program = new Program(new Memory(), Program.SourceLanguage.SPV); this.controlFlowBuilder = new ControlFlowBuilder(expressions); this.decorationsBuilder = new DecorationsBuilder(grid); @@ -63,6 +70,10 @@ public ThreadGrid getThreadGrid() { return grid; } + public SpirvVersion getSpirvVersion() { + return spirvVersion; + } + public ControlFlowBuilder getControlFlowBuilder() { return controlFlowBuilder; } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/ParserSpirvTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/ParserSpirvTest.java index e050a66a25..fe0f1d4cae 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/ParserSpirvTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/ParserSpirvTest.java @@ -45,6 +45,23 @@ public void testInvalidMemoryOperands() throws IOException { doTestParsingInvalidProgram("memory-operands/unnecessary-scope-2.spvasm", null); } + @Test + public void testSameConditionalLabelsSpirv15() { + Program program = new ParserSpirv().parse(CharStreams.fromString(sameConditionalLabelsProgram("1.5"))); + assertNotNull(program); + } + + @Test + public void testSameConditionalLabelsSpirv16() { + try { + new ParserSpirv().parse(CharStreams.fromString(sameConditionalLabelsProgram("1.6"))); + fail("Should throw exception"); + } catch (ParsingException e) { + assertEquals("Labels of conditional branch must be different in SPIR-V 1.6 and later", + e.getMessage()); + } + } + private void doTestParsingValidProgram(String file) throws IOException { Path path = getTestResourcePath("parsers/program/spirv/valid/" + file); try (var stream = Files.newInputStream(path)) { @@ -70,4 +87,25 @@ private void doTestParsingInvalidProgram(String file, String error) throws IOExc } } } + + private String sameConditionalLabelsProgram(String version) { + return """ + ; SPIR-V + ; Version: %s + OpCapability Shader + OpCapability VulkanMemoryModel + OpMemoryModel Logical Vulkan + OpEntryPoint GLCompute %%main "main" + %%void = OpTypeVoid + %%bool = OpTypeBool + %%true = OpConstantTrue %%bool + %%function = OpTypeFunction %%void + %%main = OpFunction %%void None %%function + %%entry = OpLabel + OpBranchConditional %%true %%exit %%exit + %%exit = OpLabel + OpReturn + OpFunctionEnd + """.formatted(version); + } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlowTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlowTest.java index ba0417c59f..8471140483 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlowTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlowTest.java @@ -571,24 +571,52 @@ public void testOpBranchConditionalUnstructured() { } @Test - public void testOpBranchConditionalSameLabels() { + public void testOpBranchConditionalSameLabelsSpirv15() { // given String input = """ %label0 = OpLabel OpBranchConditional %value %label1 %label1 """; + MockProgramBuilder builder = new MockProgramBuilder(new SpirvVersion(1, 5)); + builder.mockFunctionStart(false); + builder.mockBoolType("%bool"); + builder.mockUndefinedValue("%value", "%bool"); + + // when + new MockSpirvParser(input).spv().accept(new VisitorOpsControlFlow(builder)); + + // then + List events = builder.getCurrentFunction().getEvents(); + CondJump trueJump = (CondJump) events.get(1); + CondJump falseJump = (CondJump) events.get(2); + assertFalse(trueJump.isGoto()); + assertTrue(falseJump.isGoto()); + assertEquals("%label1", trueJump.getLabel().getName()); + assertEquals("%label1", falseJump.getLabel().getName()); + } + + @Test + public void testOpBranchConditionalSameLabelsSpirv16() { + // given + String input = """ + %label0 = OpLabel + OpBranchConditional %value %label1 %label1 + """; + + MockProgramBuilder builder = new MockProgramBuilder(new SpirvVersion(1, 6)); builder.mockFunctionStart(false); builder.mockBoolType("%bool"); builder.mockUndefinedValue("%value", "%bool"); try { // when - visit(input); + new MockSpirvParser(input).spv().accept(new VisitorOpsControlFlow(builder)); fail("Should throw exception"); } catch (ParsingException e) { // then - assertEquals("Labels of conditional branch cannot be the same", e.getMessage()); + assertEquals("Labels of conditional branch must be different in SPIR-V 1.6 and later", + e.getMessage()); } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/mocks/MockProgramBuilder.java b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/mocks/MockProgramBuilder.java index 5261757872..f3d7ce2ebd 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/mocks/MockProgramBuilder.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/mocks/MockProgramBuilder.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.expression.integers.IntLiteral; import com.dat3m.dartagnan.expression.type.*; import com.dat3m.dartagnan.parsers.program.visitors.spirv.builders.ProgramBuilder; +import com.dat3m.dartagnan.parsers.program.visitors.spirv.SpirvVersion; 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.decorations.Offset; @@ -34,6 +35,11 @@ public MockProgramBuilder(ThreadGrid grid) { controlFlowBuilder = new MockControlFlowBuilder(expressions); } + public MockProgramBuilder(SpirvVersion spirvVersion) { + super(new ThreadGrid(1, 1, 1, 1, 1), spirvVersion); + controlFlowBuilder = new MockControlFlowBuilder(expressions); + } + @Override public void setNextOps(Set nextOps) { // Do nothing in the mock