Relax diff labels rule for conditional jumps prior to SPIRV 1.6

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() {

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<SpirvVersion> {
+
+    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;
+    }
+}

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlow.java

@@ -21,6 +21,7 @@
 
 public class VisitorOpsControlFlow extends SpirvBaseVisitor<Event> {
 
+    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) {

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<String, Expression> inputs = new HashMap<>();
     protected final Map<String, String> 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<String> 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;
     }

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);
+    }
 }

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<Event> 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());
         }
     }
 

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<String> nextOps) {
         // Do nothing in the mock