Merge loop normalization passes into one

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleEntry.java → dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java

@@ -14,8 +14,10 @@
 import java.util.Map;
 
 /*
-    This pass transforms loops to have a single point.
-    Given a loop of the form
+    This pass normalizes loops to have a single unconditional backjump and a single entry point.
+    It achieves this via two transformations.
+
+    (1) Given a loop of the form
 
         entry:
         ...
@@ -52,14 +54,37 @@
         ...
         __jumpedTo_L_From <- 2
         goto L
+
+    (2) Given a loop of the form
+
+        L:
+        ...
+        if X goto L
+        ...
+        if Y goto L
+        More Code
+
+    it transforms it to
+
+        L:
+        ...
+        if X goto __repeatLoop_L
+        ...
+        if Y goto __repeatLoop_L
+        goto __breakLoop_L
+        __repeatLoop_L:
+        goto L
+        __breakLoop_L
+        More Code
+        ...
 */
-public class NormalizeLoopsSingleEntry implements FunctionProcessor {
+public class NormalizeLoops implements FunctionProcessor {
 
     private final TypeFactory types = TypeFactory.getInstance();
     private final ExpressionFactory expressions = ExpressionFactory.getInstance();
 
-    public static NormalizeLoopsSingleEntry newInstance() {
-        return new NormalizeLoopsSingleEntry();
+    public static NormalizeLoops newInstance() {
+        return new NormalizeLoops();
     }
 
     @Override
@@ -116,5 +141,38 @@ public void run(Function function) {
                 }
             }
         }
+
+        IdReassignment.newInstance().run(function);
+
+        // Guarantees having a single unconditional backjump
+        int counter = 0;
+        for (Label label : function.getEvents(Label.class)) {
+            final List<CondJump> backJumps = label.getJumpSet().stream()
+                    .filter(j -> j.getLocalId() > label.getLocalId())
+                    .sorted()
+                    .toList();
+
+            // LoopFormVerification requires a unique and unconditional backjump
+            if (backJumps.isEmpty() || (backJumps.size() == 1 && backJumps.get(0).isGoto())) {
+                continue;
+            }
+
+            final CondJump last = backJumps.get(backJumps.size() - 1);
+
+            final Label forwardLabel = EventFactory.newLabel("__repeatLoop_#" + counter);
+            final CondJump gotoRepeat = EventFactory.newGoto(label);
+
+            final Label breakLabel = EventFactory.newLabel("__breakLoop_#" + counter);
+            final CondJump gotoBreak = EventFactory.newGoto(breakLabel);
+
+            last.insertAfter(List.of(gotoBreak, forwardLabel, gotoRepeat, breakLabel));
+
+            for(CondJump j : backJumps) {
+                j.updateReferences(Map.of(j.getLabel(), forwardLabel));
+            }
+
+            counter++;
+        }
+
     }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java

@@ -85,10 +85,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
         final FunctionProcessor removeDeadJumps = RemoveDeadCondJumps.fromConfig(config);
         programProcessors.addAll(Arrays.asList(
                 printBeforeProcessing ? DebugPrint.withHeader("Before processing", Printer.Mode.ALL) : null,
-                // We need to update events id between the next two passes,
-                // thus they cannot be merged as a FunctionProcessor chain.
-                ProgramProcessor.fromFunctionProcessor(NormalizeLoopsSingleEntry.newInstance(), Target.FUNCTIONS, true),
-                ProgramProcessor.fromFunctionProcessor(NormalizeLoopsSingleBackJump.newInstance(), Target.FUNCTIONS, true),
+                ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.FUNCTIONS, true),
                 intrinsics.markIntrinsicsPass(),
                 GEPToAddition.newInstance(),
                 NaiveDevirtualisation.newInstance(),