Structured control flow

hernanponcedeleon · Nov 25, 2024 · 8753bab · 8753bab
1 parent e8622b7
commit 8753bab
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 67 deletions.
diff --git a/...c/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlow.java b/...c/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlow.java
@@ -161,13 +161,13 @@ private Event visitIfBranch(Expression guard, String trueLabelId, String falseLa
                 throw new ParsingException("Illegal backward jump to '%s' from a structured branch", labelId);
             }
         }
-        mergeLabelId = null;
         nextLabelId = trueLabelId;
         builder.setNextOps(Set.of("OpLabel"));
         Label falseLabel = cfBuilder.getOrCreateLabel(falseLabelId);
-        Label mergeLabel = cfBuilder.createMergeLabel(falseLabelId);
+        Label mergeLabel = cfBuilder.getOrCreateLabel(mergeLabelId);
         Event event = EventFactory.newIfJumpUnless(guard, falseLabel, mergeLabel);
         builder.addEvent(event);
+        mergeLabelId = null;
         return cfBuilder.endBlock(event);
     }
 

diff --git a/.../java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ControlFlowBuilder.java b/.../java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ControlFlowBuilder.java
@@ -15,7 +15,6 @@ public class ControlFlowBuilder {
 
     protected final Map<String, Label> blockLabels = new HashMap<>();
     protected final Map<String, Event> lastBlockEvents = new HashMap<>();
-    protected final Map<String, String> mergeLabelIds = new HashMap<>();
     protected final Deque<String> blockStack = new ArrayDeque<>();
     protected final Map<String, Map<Register, String>> phiDefinitions = new HashMap<>();
     protected final Map<String, SourceLocation> phiDefinitionLocations = new HashMap<>();
@@ -44,8 +43,6 @@ public void build() {
                     if (loc != null) { event.setMetadata(loc); }
                     lastBlockEvents.get(blockId).getPredecessor().insertAfter(event);
                 }));
-        mergeLabelIds.forEach((jumpLabelId, endLabelId) ->
-                lastBlockEvents.get(jumpLabelId).getPredecessor().insertAfter(blockLabels.get(endLabelId)));
     }
 
     public void startBlock(String id) {
@@ -68,12 +65,6 @@ public Label getOrCreateLabel(String id) {
         return blockLabels.computeIfAbsent(id, EventFactory::newLabel);
     }
 
-    public Label createMergeLabel(String id) {
-        String mergeId = id + "_end";
-        mergeLabelIds.put(id, mergeId);
-        return createLabel(mergeId);
-    }
-
     public void addPhiDefinition(String blockId, Register register, String expressionId) {
         phiDefinitions.computeIfAbsent(blockId, k -> new HashMap<>()).put(register, expressionId);
     }
@@ -121,11 +112,6 @@ private void validateBeforeBuild() {
             throw new ParsingException("Phi operation(s) refer to undefined block(s) %s",
                     String.join(", ", missingPhiBlocks));
         }
-        Set<String> missingMergeBlocks = Sets.difference(mergeLabelIds.keySet(), blockLabels.keySet());
-        if (!missingMergeBlocks.isEmpty()) {
-            throw new ParsingException("Branch merge label(s) refer to undefined block(s) %s",
-                    String.join(", ", missingMergeBlocks));
-        }
         Map<Event, String> reverse = new HashMap<>();
         lastBlockEvents.forEach((k, v) -> {
             if (reverse.containsKey(v)) {
@@ -135,13 +121,6 @@ private void validateBeforeBuild() {
         });
     }
 
-    private Label createLabel(String id) {
-        if (blockLabels.containsKey(id)) {
-            throw new ParsingException("Attempt to redefine label '%s'", id);
-        }
-        return getOrCreateLabel(id);
-    }
-
     private SourceLocation getPhiLocation(String blockId, Register register) {
         String id = phiDefinitionIds.get(blockId).get(register);
         if (id != null) {

diff --git a/...st/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlowTest.java b/...st/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlowTest.java
@@ -161,13 +161,12 @@ public void testStructuredBranch() {
 
         assertEquals("%label0", label0.getName());
         assertEquals("%label2", ifJump.getLabel().getName());
-        assertEquals("%label2_end", ifJump.getEndIf().getName());
+        assertEquals("%label2", ifJump.getEndIf().getName());
         assertEquals("%label1", label1.getName());
         assertEquals("%label2", jump.getLabel().getName());
         assertEquals("%label2", label2.getName());
 
         assertTrue(jump.isGoto());
-        assertEquals(Map.of("%label2", "%label2_end"), cfBuilder.getMergeLabelIds());
         assertEquals(Map.of("%label0", ifJump, "%label1", jump, "%label2", ret),
                 cfBuilder.getLastBlockEvents());
     }
@@ -213,10 +212,10 @@ public void testStructuredBranchNestedTrue() {
 
         assertEquals("%label0", label0.getName());
         assertEquals("%label2", ifJump.getLabel().getName());
-        assertEquals("%label2_end", ifJump.getEndIf().getName());
+        assertEquals("%label2", ifJump.getEndIf().getName());
         assertEquals("%label1", label1.getName());
         assertEquals("%label2_inner", ifJumpInner.getLabel().getName());
-        assertEquals("%label2_inner_end", ifJumpInner.getEndIf().getName());
+        assertEquals("%label2_inner", ifJumpInner.getEndIf().getName());
         assertEquals("%label1_inner", label1Inner.getName());
         assertEquals("%label2_inner", jumpInner.getLabel().getName());
         assertEquals("%label2_inner", label2Inner.getName());
@@ -281,12 +280,12 @@ public void testStructuredBranchNestedFalse() {
 
         assertEquals("%label0", label0.getName());
         assertEquals("%label3", ifJump.getLabel().getName());
-        assertEquals("%label3_end", ifJump.getEndIf().getName());
+        assertEquals("%label2", ifJump.getEndIf().getName());
         assertEquals("%label2", jump1.getLabel().getName());
         assertEquals("%label1", label1.getName());
         assertEquals("%label2", label2.getName());
         assertEquals("%label2_inner", ifJumpInner.getLabel().getName());
-        assertEquals("%label2_inner_end", ifJumpInner.getEndIf().getName());
+        assertEquals("%label2_inner", ifJumpInner.getEndIf().getName());
         assertEquals("%label1_inner", label1Inner.getName());
         assertEquals("%label2_inner", jumpInner.getLabel().getName());
         assertEquals("%label2_inner", label2Inner.getName());
@@ -307,36 +306,6 @@ public void testStructuredBranchNestedFalse() {
         ), cfBuilder.getLastBlockEvents());
     }
 
-    @Test
-    public void testStructuredBranchNestedSameLabel() {
-        // given
-        String input = """
-                %label0 = OpLabel
-                OpSelectionMerge %label2 None
-                OpBranchConditional %value %label1 %label2
-                %label1 = OpLabel
-                OpSelectionMerge %label2 None
-                OpBranchConditional %value %label1_inner %label2
-                %label1_inner = OpLabel
-                OpBranch %label2
-                %label2 = OpLabel
-                OpReturn
-                """;
-
-        builder.mockFunctionStart(false);
-        builder.mockBoolType("%bool");
-        builder.mockUndefinedValue("%value", "%bool");
-
-        try {
-            // when
-            visit(input);
-            fail("Should throw exception");
-        } catch (ParsingException e) {
-            // then
-            assertEquals("Attempt to redefine label '%label2_end'", e.getMessage());
-        }
-    }
-
     @Test
     public void testLoopWithForwardLabels() {
         // given
@@ -379,8 +348,6 @@ public void testLoopWithForwardLabels() {
         assertTrue(jump2.isGoto());
         assertTrue(jump3.isGoto());
 
-        assertTrue(cfBuilder.getMergeLabelIds().isEmpty());
-
         assertEquals(Map.of("%label0", jump1, "%label1", jump3, "%label2", ret),
                 cfBuilder.getLastBlockEvents());
     }
@@ -420,8 +387,6 @@ public void testLoopWithBackwardLabel() {
         assertFalse(jump1.isGoto());
         assertTrue(jump2.isGoto());
 
-        assertTrue(cfBuilder.getMergeLabelIds().isEmpty());
-
         assertEquals(Map.of("%label0", jump1, "%label1", ret),
                 cfBuilder.getLastBlockEvents());
     }

diff --git a/...java/com/dat3m/dartagnan/parsers/program/visitors/spirv/mocks/MockControlFlowBuilder.java b/...java/com/dat3m/dartagnan/parsers/program/visitors/spirv/mocks/MockControlFlowBuilder.java
@@ -18,10 +18,6 @@ public List<String> getBlockStack() {
         return blockStack.stream().toList();
     }
 
-    public Map<String, String> getMergeLabelIds() {
-        return Map.copyOf(mergeLabelIds);
-    }
-
     public Map<String, Event> getLastBlockEvents() {
         return Map.copyOf(lastBlockEvents);
     }