From f776d85bd5cbd3e3854fd69fbd33892335476366 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sat, 27 Jul 2024 02:09:37 +0800
Subject: [PATCH 01/14] Initial commit

---
 .../program/processing/NormalizeLoops.java    | 40 +++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
index 62e4b1ef18..f5cdfa8bba 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
@@ -1,10 +1,15 @@
 package com.dat3m.dartagnan.program.processing;
 
+import com.dat3m.dartagnan.expression.ExpressionFactory;
+import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.Function;
+import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.core.CondJump;
 import com.dat3m.dartagnan.program.event.core.Label;
+import com.dat3m.dartagnan.program.event.core.Local;
 
+import java.util.Arrays;
 import java.util.List;
 import java.util.Map;
 
@@ -35,6 +40,9 @@
 */
 public class NormalizeLoops implements FunctionProcessor {
 
+    private final TypeFactory types = TypeFactory.getInstance();
+    private final ExpressionFactory expressions = ExpressionFactory.getInstance();
+
     public static NormalizeLoops newInstance() {
         return new NormalizeLoops();
     }
@@ -68,6 +76,38 @@ public void run(Function function) {
             }
 
             counter++;
+
+            // Guarantee header is the only fromOutside point
+            final Label loopBegin = label;
+            final CondJump uniqueBackJump = backJumps.get(0);
+
+            final List<Label> loopBodyLabels = loopBegin.getSuccessor().getSuccessors().stream()
+                    .takeWhile(ev -> ev != uniqueBackJump)
+                    .filter(Label.class::isInstance).map(Label.class::cast)
+                    .toList();
+            for (Label l : loopBodyLabels) {
+                final List<CondJump> externalEntries = l.getJumpSet().stream()
+                        .filter(j -> j.getLocalId() < loopBegin.getLocalId() ||
+                                j.getLocalId() > uniqueBackJump.getLocalId())
+                        .toList();
+
+                for(CondJump fromOutside : externalEntries) {
+
+                    final Register jumpedFromOutside = function.newRegister("__jumpedFromOutside", types.getBooleanType());
+                    final Local setJumpedFromOutside = EventFactory.newLocal(jumpedFromOutside, expressions.makeTrue());
+                    final CondJump jumpToHeader = EventFactory.newGoto(loopBegin);
+                    final Label internalLabel = fromOutside.getLabel();
+
+                    fromOutside.replaceBy(setJumpedFromOutside);
+                    setJumpedFromOutside.insertAfter(jumpToHeader);
+
+                    final CondJump jumpToInternal = EventFactory.newJump(jumpedFromOutside, internalLabel);
+                    final Local unsetJumpFromOutside = EventFactory.newLocal(jumpedFromOutside, expressions.makeFalse());
+
+                    loopBegin.insertAfter(Arrays.asList(jumpToInternal, unsetJumpFromOutside));
+                }
+            }
+
         }
     }
 }

From 609fc1b9f059316ca772c039973e81fb794a8be1 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sat, 27 Jul 2024 03:50:32 +0800
Subject: [PATCH 02/14] More changes

---
 .../program/processing/NormalizeLoops.java    | 82 +++++++++++++------
 1 file changed, 57 insertions(+), 25 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
index f5cdfa8bba..785c93c750 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
@@ -14,29 +14,55 @@
 import java.util.Map;
 
 /*
-    This pass transforms loops to have a single backjump using forward jumping.
-    Given a loop of the form
-
-    L:
-    ...
-    if X goto L
-    ...
-    if Y goto L
-    More Code
+    This pass normalizes loops to have a single unconditional backjump and a single entry point.
+    It achives this via two transformations.
+
+    (1) 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
+        ...
+
+    (2) Given code the form
+
+        goto C
+        ...
+        L:
+        ...
+        C:
+        ...
+        goto L
 
     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
-    ...
+        __jumpedFromOutside <- true
+        goto L
+        ...
+        __jumpedFromOutside <- false
+        L:
+        if __jumpedFromOutside goto C
+        __jumpedFromOutside <- false
+        ...
+        C:
+        ...
+        goto L
 */
 public class NormalizeLoops implements FunctionProcessor {
 
@@ -49,6 +75,8 @@ public static NormalizeLoops newInstance() {
 
     @Override
     public void run(Function function) {
+
+        // Guarantees having a single unconditional backjump
         int counter = 0;
         for (Label label : function.getEvents(Label.class)) {
             final List<CondJump> backJumps = label.getJumpSet().stream()
@@ -56,7 +84,6 @@ public void run(Function function) {
                     .sorted()
                     .toList();
 
-            // LoopFormVerification requires a unique and unconditional backjump
             if (backJumps.isEmpty() || (backJumps.size() == 1 && backJumps.get(0).isGoto())) {
                 continue;
             }
@@ -76,8 +103,10 @@ public void run(Function function) {
             }
 
             counter++;
+        }
 
-            // Guarantee header is the only fromOutside point
+        // Guarantees header is the only entry point
+        for (Label label : function.getEvents(Label.class)) {
             final Label loopBegin = label;
             final CondJump uniqueBackJump = backJumps.get(0);
 
@@ -91,9 +120,10 @@ public void run(Function function) {
                                 j.getLocalId() > uniqueBackJump.getLocalId())
                         .toList();
 
-                for(CondJump fromOutside : externalEntries) {
+                for (CondJump fromOutside : externalEntries) {
 
-                    final Register jumpedFromOutside = function.newRegister("__jumpedFromOutside", types.getBooleanType());
+                    final Register jumpedFromOutside = function.newRegister("__jumpedFromOutside",
+                            types.getBooleanType());
                     final Local setJumpedFromOutside = EventFactory.newLocal(jumpedFromOutside, expressions.makeTrue());
                     final CondJump jumpToHeader = EventFactory.newGoto(loopBegin);
                     final Label internalLabel = fromOutside.getLabel();
@@ -102,9 +132,11 @@ public void run(Function function) {
                     setJumpedFromOutside.insertAfter(jumpToHeader);
 
                     final CondJump jumpToInternal = EventFactory.newJump(jumpedFromOutside, internalLabel);
+                    final Local initJumpFromOutside = EventFactory.newLocal(jumpedFromOutside, expressions.makeFalse());
                     final Local unsetJumpFromOutside = EventFactory.newLocal(jumpedFromOutside, expressions.makeFalse());
 
-                    loopBegin.insertAfter(Arrays.asList(jumpToInternal, unsetJumpFromOutside));
+                    loopBegin.getPredecessor()
+                            .insertAfter(Arrays.asList(initJumpFromOutside, jumpToInternal, unsetJumpFromOutside));
                 }
             }
 

From 0c08c7c691c0b5be975287c1adb9ff1488a342a5 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sat, 27 Jul 2024 04:01:18 +0800
Subject: [PATCH 03/14] Add unit test

---
 benchmarks/c/miscellaneous/jumpFromOutside.c  |  28 ++++
 .../program/processing/NormalizeLoops.java    |   4 +
 .../dat3m/dartagnan/c/MiscellaneousTest.java  |   3 +-
 .../miscellaneous/jumpFromOutside.ll          | 140 ++++++++++++++++++
 4 files changed, 174 insertions(+), 1 deletion(-)
 create mode 100644 benchmarks/c/miscellaneous/jumpFromOutside.c
 create mode 100644 dartagnan/src/test/resources/miscellaneous/jumpFromOutside.ll

diff --git a/benchmarks/c/miscellaneous/jumpFromOutside.c b/benchmarks/c/miscellaneous/jumpFromOutside.c
new file mode 100644
index 0000000000..dc1cde0ee3
--- /dev/null
+++ b/benchmarks/c/miscellaneous/jumpFromOutside.c
@@ -0,0 +1,28 @@
+#include <stdint.h>
+#include <assert.h>
+#include <dat3m.h>
+
+volatile int32_t x = 0;
+
+int main()
+{
+    int x = __VERIFIER_nondet_uint();
+
+    if (x <= 0) {
+        return 0;
+    }
+
+A:
+    if (x >= 10) {
+        x = 5;
+        goto C;
+    }
+B:
+    x = x + 1;
+C:
+    if (x < 10) {
+        goto B;
+    }
+
+	return 0;
+}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
index 785c93c750..31100b5616 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
@@ -107,6 +107,10 @@ public void run(Function function) {
 
         // Guarantees header is the only entry point
         for (Label label : function.getEvents(Label.class)) {
+            final List<CondJump> backJumps = label.getJumpSet().stream()
+                    .filter(j -> j.getLocalId() > label.getLocalId())
+                    .sorted()
+                    .toList();
             final Label loopBegin = label;
             final CondJump uniqueBackJump = backJumps.get(0);
 
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java
index 20dc4de093..774a30dc31 100644
--- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java
@@ -90,7 +90,8 @@ public static Iterable<Object[]> data() throws IOException {
                 {"staticLoops", IMM, PASS, 1},
                 {"offsetof", IMM, PASS, 1},
                 {"ctlz", IMM, PASS, 1},
-                {"cttz", IMM, PASS, 1}
+                {"cttz", IMM, PASS, 1},
+                {"jumpFromOutside", IMM, PASS, 11}
         });
     }
 
diff --git a/dartagnan/src/test/resources/miscellaneous/jumpFromOutside.ll b/dartagnan/src/test/resources/miscellaneous/jumpFromOutside.ll
new file mode 100644
index 0000000000..6faa1c4c16
--- /dev/null
+++ b/dartagnan/src/test/resources/miscellaneous/jumpFromOutside.ll
@@ -0,0 +1,140 @@
+; ModuleID = '/home/drc/git/Dat3M/output/jumpFromOutside.ll'
+source_filename = "/home/drc/git/Dat3M/benchmarks/c/miscellaneous/jumpFromOutside.c"
+target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-pc-linux-gnu"
+
+@x = dso_local global i32 0, align 4, !dbg !0
+
+; Function Attrs: noinline nounwind uwtable
+define dso_local i32 @main() #0 !dbg !20 {
+  %1 = alloca i32, align 4
+  %2 = alloca i32, align 4
+  store i32 0, i32* %1, align 4
+  call void @llvm.dbg.declare(metadata i32* %2, metadata !24, metadata !DIExpression()), !dbg !25
+  %3 = call i32 @__VERIFIER_nondet_uint(), !dbg !26
+  store i32 %3, i32* %2, align 4, !dbg !25
+  %4 = load i32, i32* %2, align 4, !dbg !27
+  %5 = icmp sle i32 %4, 0, !dbg !29
+  br i1 %5, label %6, label %7, !dbg !30
+
+6:                                                ; preds = %0
+  store i32 0, i32* %1, align 4, !dbg !31
+  br label %21, !dbg !31
+
+7:                                                ; preds = %0
+  br label %8, !dbg !33
+
+8:                                                ; preds = %7
+  call void @llvm.dbg.label(metadata !34), !dbg !35
+  %9 = load i32, i32* %2, align 4, !dbg !36
+  %10 = icmp sge i32 %9, 10, !dbg !38
+  br i1 %10, label %11, label %12, !dbg !39
+
+11:                                               ; preds = %8
+  store i32 5, i32* %2, align 4, !dbg !40
+  br label %16, !dbg !42
+
+12:                                               ; preds = %8
+  br label %13, !dbg !43
+
+13:                                               ; preds = %19, %12
+  call void @llvm.dbg.label(metadata !44), !dbg !45
+  %14 = load i32, i32* %2, align 4, !dbg !46
+  %15 = add nsw i32 %14, 1, !dbg !47
+  store i32 %15, i32* %2, align 4, !dbg !48
+  br label %16, !dbg !49
+
+16:                                               ; preds = %13, %11
+  call void @llvm.dbg.label(metadata !50), !dbg !51
+  %17 = load i32, i32* %2, align 4, !dbg !52
+  %18 = icmp slt i32 %17, 10, !dbg !54
+  br i1 %18, label %19, label %20, !dbg !55
+
+19:                                               ; preds = %16
+  br label %13, !dbg !56
+
+20:                                               ; preds = %16
+  store i32 0, i32* %1, align 4, !dbg !58
+  br label %21, !dbg !58
+
+21:                                               ; preds = %20, %6
+  %22 = load i32, i32* %1, align 4, !dbg !59
+  ret i32 %22, !dbg !59
+}
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
+
+declare i32 @__VERIFIER_nondet_uint() #2
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.label(metadata) #1
+
+attributes #0 = { noinline nounwind uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
+attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
+attributes #2 = { "frame-pointer"="all" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
+
+!llvm.dbg.cu = !{!2}
+!llvm.module.flags = !{!12, !13, !14, !15, !16, !17, !18}
+!llvm.ident = !{!19}
+
+!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !5, line: 5, type: !6, isLocal: false, isDefinition: true)
+!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Ubuntu clang version 14.0.0-1ubuntu1.1", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, globals: !4, splitDebugInlining: false, nameTableKind: None)
+!3 = !DIFile(filename: "/home/drc/git/Dat3M/benchmarks/c/miscellaneous/jumpFromOutside.c", directory: "/home/drc/git/Dat3M", checksumkind: CSK_MD5, checksum: "93cac12dbf00c291fa6fe587b400c1e8")
+!4 = !{!0}
+!5 = !DIFile(filename: "benchmarks/c/miscellaneous/jumpFromOutside.c", directory: "/home/drc/git/Dat3M", checksumkind: CSK_MD5, checksum: "93cac12dbf00c291fa6fe587b400c1e8")
+!6 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !7)
+!7 = !DIDerivedType(tag: DW_TAG_typedef, name: "int32_t", file: !8, line: 26, baseType: !9)
+!8 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/stdint-intn.h", directory: "", checksumkind: CSK_MD5, checksum: "55bcbdc3159515ebd91d351a70d505f4")
+!9 = !DIDerivedType(tag: DW_TAG_typedef, name: "__int32_t", file: !10, line: 41, baseType: !11)
+!10 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/types.h", directory: "", checksumkind: CSK_MD5, checksum: "d108b5f93a74c50510d7d9bc0ab36df9")
+!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!12 = !{i32 7, !"Dwarf Version", i32 5}
+!13 = !{i32 2, !"Debug Info Version", i32 3}
+!14 = !{i32 1, !"wchar_size", i32 4}
+!15 = !{i32 7, !"PIC Level", i32 2}
+!16 = !{i32 7, !"PIE Level", i32 2}
+!17 = !{i32 7, !"uwtable", i32 1}
+!18 = !{i32 7, !"frame-pointer", i32 2}
+!19 = !{!"Ubuntu clang version 14.0.0-1ubuntu1.1"}
+!20 = distinct !DISubprogram(name: "main", scope: !5, file: !5, line: 7, type: !21, scopeLine: 8, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !23)
+!21 = !DISubroutineType(types: !22)
+!22 = !{!11}
+!23 = !{}
+!24 = !DILocalVariable(name: "x", scope: !20, file: !5, line: 9, type: !11)
+!25 = !DILocation(line: 9, column: 9, scope: !20)
+!26 = !DILocation(line: 9, column: 13, scope: !20)
+!27 = !DILocation(line: 11, column: 9, scope: !28)
+!28 = distinct !DILexicalBlock(scope: !20, file: !5, line: 11, column: 9)
+!29 = !DILocation(line: 11, column: 11, scope: !28)
+!30 = !DILocation(line: 11, column: 9, scope: !20)
+!31 = !DILocation(line: 12, column: 9, scope: !32)
+!32 = distinct !DILexicalBlock(scope: !28, file: !5, line: 11, column: 17)
+!33 = !DILocation(line: 11, column: 14, scope: !28)
+!34 = !DILabel(scope: !20, name: "A", file: !5, line: 15)
+!35 = !DILocation(line: 15, column: 1, scope: !20)
+!36 = !DILocation(line: 16, column: 9, scope: !37)
+!37 = distinct !DILexicalBlock(scope: !20, file: !5, line: 16, column: 9)
+!38 = !DILocation(line: 16, column: 11, scope: !37)
+!39 = !DILocation(line: 16, column: 9, scope: !20)
+!40 = !DILocation(line: 17, column: 11, scope: !41)
+!41 = distinct !DILexicalBlock(scope: !37, file: !5, line: 16, column: 18)
+!42 = !DILocation(line: 18, column: 9, scope: !41)
+!43 = !DILocation(line: 16, column: 14, scope: !37)
+!44 = !DILabel(scope: !20, name: "B", file: !5, line: 20)
+!45 = !DILocation(line: 20, column: 1, scope: !20)
+!46 = !DILocation(line: 21, column: 9, scope: !20)
+!47 = !DILocation(line: 21, column: 11, scope: !20)
+!48 = !DILocation(line: 21, column: 7, scope: !20)
+!49 = !DILocation(line: 21, column: 5, scope: !20)
+!50 = !DILabel(scope: !20, name: "C", file: !5, line: 22)
+!51 = !DILocation(line: 22, column: 1, scope: !20)
+!52 = !DILocation(line: 23, column: 9, scope: !53)
+!53 = distinct !DILexicalBlock(scope: !20, file: !5, line: 23, column: 9)
+!54 = !DILocation(line: 23, column: 11, scope: !53)
+!55 = !DILocation(line: 23, column: 9, scope: !20)
+!56 = !DILocation(line: 24, column: 9, scope: !57)
+!57 = distinct !DILexicalBlock(scope: !53, file: !5, line: 23, column: 17)
+!58 = !DILocation(line: 27, column: 2, scope: !20)
+!59 = !DILocation(line: 28, column: 1, scope: !20)

From a6f65e85cc39d5e2e2f33ce9ac6f563d0fafb6d7 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Date: Mon, 29 Jul 2024 14:46:07 +0200
Subject: [PATCH 04/14] Several fixes

---
 README.md                                     |   1 -
 .../program/processing/NormalizeLoops.java    | 149 ------------------
 .../NormalizeLoopsSingleBackJump.java         |  74 +++++++++
 .../processing/NormalizeLoopsSingleEntry.java | 120 ++++++++++++++
 .../program/processing/ProcessingManager.java |   5 +-
 5 files changed, 198 insertions(+), 151 deletions(-)
 delete mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
 create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleBackJump.java
 create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleEntry.java

diff --git a/README.md b/README.md
index 1b79dc8236..131b1ff33e 100644
--- a/README.md
+++ b/README.md
@@ -42,7 +42,6 @@ export DAT3M_OUTPUT=$DAT3M_HOME/output
 At least the following compiler flag needs to be set, further can be added (only to verify C programs)
 ```
 export CFLAGS="-I$DAT3M_HOME/include"
-export OPTFLAGS="-mem2reg -sroa -early-cse -indvars -loop-unroll -fix-irreducible -loop-simplify -simplifycfg -gvn"
 ```
 
 If you are verifying C code, be sure `clang` is in your `PATH`.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
deleted file mode 100644
index 31100b5616..0000000000
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
+++ /dev/null
@@ -1,149 +0,0 @@
-package com.dat3m.dartagnan.program.processing;
-
-import com.dat3m.dartagnan.expression.ExpressionFactory;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
-import com.dat3m.dartagnan.program.Function;
-import com.dat3m.dartagnan.program.Register;
-import com.dat3m.dartagnan.program.event.EventFactory;
-import com.dat3m.dartagnan.program.event.core.CondJump;
-import com.dat3m.dartagnan.program.event.core.Label;
-import com.dat3m.dartagnan.program.event.core.Local;
-
-import java.util.Arrays;
-import java.util.List;
-import java.util.Map;
-
-/*
-    This pass normalizes loops to have a single unconditional backjump and a single entry point.
-    It achives this via two transformations.
-
-    (1) 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
-        ...
-
-    (2) Given code the form
-
-        goto C
-        ...
-        L:
-        ...
-        C:
-        ...
-        goto L
-
-    it transforms it to
-
-        __jumpedFromOutside <- true
-        goto L
-        ...
-        __jumpedFromOutside <- false
-        L:
-        if __jumpedFromOutside goto C
-        __jumpedFromOutside <- false
-        ...
-        C:
-        ...
-        goto L
-*/
-public class NormalizeLoops implements FunctionProcessor {
-
-    private final TypeFactory types = TypeFactory.getInstance();
-    private final ExpressionFactory expressions = ExpressionFactory.getInstance();
-
-    public static NormalizeLoops newInstance() {
-        return new NormalizeLoops();
-    }
-
-    @Override
-    public void run(Function 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();
-
-            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++;
-        }
-
-        // Guarantees header is the only entry point
-        for (Label label : function.getEvents(Label.class)) {
-            final List<CondJump> backJumps = label.getJumpSet().stream()
-                    .filter(j -> j.getLocalId() > label.getLocalId())
-                    .sorted()
-                    .toList();
-            final Label loopBegin = label;
-            final CondJump uniqueBackJump = backJumps.get(0);
-
-            final List<Label> loopBodyLabels = loopBegin.getSuccessor().getSuccessors().stream()
-                    .takeWhile(ev -> ev != uniqueBackJump)
-                    .filter(Label.class::isInstance).map(Label.class::cast)
-                    .toList();
-            for (Label l : loopBodyLabels) {
-                final List<CondJump> externalEntries = l.getJumpSet().stream()
-                        .filter(j -> j.getLocalId() < loopBegin.getLocalId() ||
-                                j.getLocalId() > uniqueBackJump.getLocalId())
-                        .toList();
-
-                for (CondJump fromOutside : externalEntries) {
-
-                    final Register jumpedFromOutside = function.newRegister("__jumpedFromOutside",
-                            types.getBooleanType());
-                    final Local setJumpedFromOutside = EventFactory.newLocal(jumpedFromOutside, expressions.makeTrue());
-                    final CondJump jumpToHeader = EventFactory.newGoto(loopBegin);
-                    final Label internalLabel = fromOutside.getLabel();
-
-                    fromOutside.replaceBy(setJumpedFromOutside);
-                    setJumpedFromOutside.insertAfter(jumpToHeader);
-
-                    final CondJump jumpToInternal = EventFactory.newJump(jumpedFromOutside, internalLabel);
-                    final Local initJumpFromOutside = EventFactory.newLocal(jumpedFromOutside, expressions.makeFalse());
-                    final Local unsetJumpFromOutside = EventFactory.newLocal(jumpedFromOutside, expressions.makeFalse());
-
-                    loopBegin.getPredecessor()
-                            .insertAfter(Arrays.asList(initJumpFromOutside, jumpToInternal, unsetJumpFromOutside));
-                }
-            }
-
-        }
-    }
-}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleBackJump.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleBackJump.java
new file mode 100644
index 0000000000..5ebd8ae7c0
--- /dev/null
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleBackJump.java
@@ -0,0 +1,74 @@
+package com.dat3m.dartagnan.program.processing;
+
+import com.dat3m.dartagnan.program.Function;
+import com.dat3m.dartagnan.program.event.EventFactory;
+import com.dat3m.dartagnan.program.event.core.CondJump;
+import com.dat3m.dartagnan.program.event.core.Label;
+import java.util.List;
+import java.util.Map;
+
+/*
+    This pass transforms loops to have a single backjump using forward jumping.
+    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 NormalizeLoopsSingleBackJump implements FunctionProcessor {
+
+    public static NormalizeLoopsSingleBackJump newInstance() {
+        return new NormalizeLoopsSingleBackJump();
+    }
+
+    @Override
+    public void run(Function 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++;
+        }
+    }
+}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleEntry.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleEntry.java
new file mode 100644
index 0000000000..a60cf0e00d
--- /dev/null
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleEntry.java
@@ -0,0 +1,120 @@
+package com.dat3m.dartagnan.program.processing;
+
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.ExpressionFactory;
+import com.dat3m.dartagnan.expression.type.TypeFactory;
+import com.dat3m.dartagnan.program.Function;
+import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.event.EventFactory;
+import com.dat3m.dartagnan.program.event.core.CondJump;
+import com.dat3m.dartagnan.program.event.core.Label;
+import com.dat3m.dartagnan.program.event.core.Local;
+import java.math.BigInteger;
+import java.util.List;
+import java.util.Map;
+
+/*
+    This pass transforms loops to have a single point.
+    Given a loop of the form
+
+        entry:
+        ...
+        goto C
+        ...
+        L:
+        ...
+        C:
+        ...
+        D:
+        ...
+        goto L
+        ...
+        goto D
+
+    it transforms it to
+
+        entry:
+        __jumpedTo_L_From <- 0
+        ...
+        __jumpedTo_L_From <- 1
+        goto L
+        ...
+        L:
+        if __jumpedTo_L_From == 1 goto C
+        if __jumpedTo_L_From == 2 goto D
+        ...
+        C:
+        ...
+        D:
+        ...
+        __jumpedTo_L_From <- 0
+        goto L
+        ...
+        __jumpedTo_L_From <- 2
+        goto L
+*/
+public class NormalizeLoopsSingleEntry implements FunctionProcessor {
+
+    private final TypeFactory types = TypeFactory.getInstance();
+    private final ExpressionFactory expressions = ExpressionFactory.getInstance();
+
+    public static NormalizeLoopsSingleEntry newInstance() {
+        return new NormalizeLoopsSingleEntry();
+    }
+
+    @Override
+    public void run(Function function) {
+
+        // Guarantees header is the only entry point
+        for (Label label : function.getEvents(Label.class)) {
+
+            final List<CondJump> backJumps = label.getJumpSet().stream()
+                    .filter(j -> j.getLocalId() > label.getLocalId())
+                    .sorted()
+                    .toList();
+            if (backJumps.isEmpty()) {
+                continue;
+            }
+
+            int counter = 0;
+
+            final Label loopBegin = label;
+            final CondJump uniqueBackJump = backJumps.get(0);
+
+            final Register sourceReg = function.newRegister(String.format("__jumpedTo_%s_From", label), types.getArchType());
+            final Local initJumpedFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(types.getArchType()));
+            function.getEntry().insertAfter(initJumpedFromOutside);
+
+            final List<Label> loopBodyLabels = loopBegin.getSuccessor().getSuccessors().stream()
+                    .takeWhile(ev -> ev != uniqueBackJump)
+                    .filter(Label.class::isInstance).map(Label.class::cast)
+                    .toList();
+
+            for (Label l : loopBodyLabels) {
+                final List<CondJump> externalEntries = l.getJumpSet().stream()
+                        .filter(j -> j.getLocalId() < loopBegin.getLocalId() ||
+                                j.getLocalId() > uniqueBackJump.getLocalId())
+                        .toList();
+
+                for (CondJump fromOutside : externalEntries) {
+                    counter++;
+
+                    final Expression source = expressions.makeValue(BigInteger.valueOf(counter), types.getArchType());
+                    final Local jumpingFrom = EventFactory.newLocal(sourceReg, source);
+                    final CondJump jumpToHeader = EventFactory.newGoto(loopBegin);
+
+                    fromOutside.replaceBy(jumpingFrom);
+                    jumpingFrom.insertAfter(jumpToHeader);
+                    jumpToHeader.updateReferences(Map.of(jumpToHeader.getLabel(), loopBegin));
+
+                    final Label internalLabel = fromOutside.getLabel();
+                    final CondJump jumpToInternal = EventFactory.newJump(expressions.makeEQ(sourceReg, source), internalLabel);
+                    final Local resetJumpFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(types.getArchType()));
+
+                    loopBegin.insertAfter(jumpToInternal);
+                    uniqueBackJump.getPredecessor().insertAfter(resetJumpFromOutside);
+                }
+            }
+        }
+    }
+}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
index 3ba67f144d..1eb0585406 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
@@ -85,7 +85,10 @@ 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,
-                ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.FUNCTIONS, true),
+                // 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),
                 intrinsics.markIntrinsicsPass(),
                 GEPToAddition.newInstance(),
                 NaiveDevirtualisation.newInstance(),

From 2e069fc984b7c1fc65cad0bf81ec9bdbdb4b4d8c Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Tue, 30 Jul 2024 00:03:15 +0800
Subject: [PATCH 05/14] Merge loop normalization passes into one

---
 ...psSingleEntry.java => NormalizeLoops.java} | 68 +++++++++++++++--
 .../NormalizeLoopsSingleBackJump.java         | 74 -------------------
 .../program/processing/ProcessingManager.java |  5 +-
 3 files changed, 64 insertions(+), 83 deletions(-)
 rename dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/{NormalizeLoopsSingleEntry.java => NormalizeLoops.java} (66%)
 delete mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleBackJump.java

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleEntry.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
similarity index 66%
rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleEntry.java
rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
index a60cf0e00d..7335beaffb 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleEntry.java
+++ b/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++;
+        }
+
     }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleBackJump.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleBackJump.java
deleted file mode 100644
index 5ebd8ae7c0..0000000000
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoopsSingleBackJump.java
+++ /dev/null
@@ -1,74 +0,0 @@
-package com.dat3m.dartagnan.program.processing;
-
-import com.dat3m.dartagnan.program.Function;
-import com.dat3m.dartagnan.program.event.EventFactory;
-import com.dat3m.dartagnan.program.event.core.CondJump;
-import com.dat3m.dartagnan.program.event.core.Label;
-import java.util.List;
-import java.util.Map;
-
-/*
-    This pass transforms loops to have a single backjump using forward jumping.
-    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 NormalizeLoopsSingleBackJump implements FunctionProcessor {
-
-    public static NormalizeLoopsSingleBackJump newInstance() {
-        return new NormalizeLoopsSingleBackJump();
-    }
-
-    @Override
-    public void run(Function 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++;
-        }
-    }
-}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
index 1eb0585406..3ba67f144d 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
+++ b/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(),

From aad7cd43d36d9404e43a008584c0b26fe919020c Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Wed, 31 Jul 2024 20:23:38 +0800
Subject: [PATCH 06/14] Fixes

---
 .../dat3m/dartagnan/program/processing/NormalizeLoops.java   | 5 ++++-
 .../dartagnan/program/processing/ProcessingManager.java      | 2 +-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
index 7335beaffb..30ee7c6074 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
@@ -91,6 +91,7 @@ public static NormalizeLoops newInstance() {
     public void run(Function function) {
 
         // Guarantees header is the only entry point
+        int labelCounter = 0;
         for (Label label : function.getEvents(Label.class)) {
 
             final List<CondJump> backJumps = label.getJumpSet().stream()
@@ -106,7 +107,7 @@ public void run(Function function) {
             final Label loopBegin = label;
             final CondJump uniqueBackJump = backJumps.get(0);
 
-            final Register sourceReg = function.newRegister(String.format("__jumpedTo_%s_From", label), types.getArchType());
+            final Register sourceReg = function.newRegister(String.format("__jumpedTo_%s#%s_From", label, labelCounter), types.getArchType());
             final Local initJumpedFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(types.getArchType()));
             function.getEntry().insertAfter(initJumpedFromOutside);
 
@@ -140,6 +141,8 @@ public void run(Function function) {
                     uniqueBackJump.getPredecessor().insertAfter(resetJumpFromOutside);
                 }
             }
+
+            labelCounter++;
         }
 
         IdReassignment.newInstance().run(function);
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
index 3ba67f144d..a509702fad 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
@@ -85,7 +85,6 @@ 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,
-                ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.FUNCTIONS, true),
                 intrinsics.markIntrinsicsPass(),
                 GEPToAddition.newInstance(),
                 NaiveDevirtualisation.newInstance(),
@@ -101,6 +100,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
                 ),
                 RegisterDecomposition.newInstance(),
                 RemoveDeadFunctions.newInstance(),
+                ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.FUNCTIONS, true),
                 printAfterSimplification ? DebugPrint.withHeader("After simplification", Printer.Mode.ALL) : null,
                 Compilation.fromConfig(config), // We keep compilation global for now
                 LoopFormVerification.fromConfig(config),

From e32674a089981b225663655387711f3ff737d66f Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Thu, 1 Aug 2024 17:20:10 +0800
Subject: [PATCH 07/14] Feedback implemented

---
 .../program/processing/NormalizeLoops.java          | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
index 30ee7c6074..1e875812c0 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
@@ -27,11 +27,7 @@
         ...
         C:
         ...
-        D:
-        ...
         goto L
-        ...
-        goto D
 
     it transforms it to
 
@@ -43,17 +39,11 @@
         ...
         L:
         if __jumpedTo_L_From == 1 goto C
-        if __jumpedTo_L_From == 2 goto D
         ...
         C:
         ...
-        D:
-        ...
         __jumpedTo_L_From <- 0
         goto L
-        ...
-        __jumpedTo_L_From <- 2
-        goto L
 
     (2) Given a loop of the form
 
@@ -118,8 +108,7 @@ public void run(Function function) {
 
             for (Label l : loopBodyLabels) {
                 final List<CondJump> externalEntries = l.getJumpSet().stream()
-                        .filter(j -> j.getLocalId() < loopBegin.getLocalId() ||
-                                j.getLocalId() > uniqueBackJump.getLocalId())
+                        .filter(j -> j.getLocalId() < loopBegin.getLocalId())
                         .toList();
 
                 for (CondJump fromOutside : externalEntries) {

From 0caede3ef971f9a0888555f36384d11577c5c88b Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Thu, 1 Aug 2024 19:18:41 +0800
Subject: [PATCH 08/14] Feedback implemented

---
 benchmarks/c/miscellaneous/jumpFromOutside.c  |  28 ----
 benchmarks/c/miscellaneous/jumpIntoLoop.c     |  19 +++
 .../program/processing/NormalizeLoops.java    |  72 ++++-----
 .../dat3m/dartagnan/c/MiscellaneousTest.java  |   2 +-
 .../miscellaneous/jumpFromOutside.ll          | 140 -----------------
 .../resources/miscellaneous/jumpIntoLoop.ll   | 142 ++++++++++++++++++
 6 files changed, 200 insertions(+), 203 deletions(-)
 delete mode 100644 benchmarks/c/miscellaneous/jumpFromOutside.c
 create mode 100644 benchmarks/c/miscellaneous/jumpIntoLoop.c
 delete mode 100644 dartagnan/src/test/resources/miscellaneous/jumpFromOutside.ll
 create mode 100644 dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll

diff --git a/benchmarks/c/miscellaneous/jumpFromOutside.c b/benchmarks/c/miscellaneous/jumpFromOutside.c
deleted file mode 100644
index dc1cde0ee3..0000000000
--- a/benchmarks/c/miscellaneous/jumpFromOutside.c
+++ /dev/null
@@ -1,28 +0,0 @@
-#include <stdint.h>
-#include <assert.h>
-#include <dat3m.h>
-
-volatile int32_t x = 0;
-
-int main()
-{
-    int x = __VERIFIER_nondet_uint();
-
-    if (x <= 0) {
-        return 0;
-    }
-
-A:
-    if (x >= 10) {
-        x = 5;
-        goto C;
-    }
-B:
-    x = x + 1;
-C:
-    if (x < 10) {
-        goto B;
-    }
-
-	return 0;
-}
diff --git a/benchmarks/c/miscellaneous/jumpIntoLoop.c b/benchmarks/c/miscellaneous/jumpIntoLoop.c
new file mode 100644
index 0000000000..657dca65ae
--- /dev/null
+++ b/benchmarks/c/miscellaneous/jumpIntoLoop.c
@@ -0,0 +1,19 @@
+#include <stdint.h>
+#include <assert.h>
+#include <dat3m.h>
+
+volatile int32_t x = 0;
+
+int main()
+{
+    int i = __VERIFIER_nondet_int();
+    if (i == 42) goto L;
+
+    for (i = 0; i < 5; i++) {
+L:
+    x++;
+    }
+
+    assert(x <= 5);
+	return 0;
+}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
index 1e875812c0..c874a54464 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
@@ -80,7 +80,44 @@ public static NormalizeLoops newInstance() {
     @Override
     public void run(Function function) {
 
-        // Guarantees header is the only entry point
+        guaranteeSingleEntry(function);
+        IdReassignment.newInstance().run(function);
+        guaranteeSingleUnconditionalBackjump(function);
+
+    }
+
+    private void guaranteeSingleUnconditionalBackjump(Function function) {
+        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++;
+        }
+    }
+
+    private void guaranteeSingleEntry(Function function) {
         int labelCounter = 0;
         for (Label label : function.getEvents(Label.class)) {
 
@@ -133,38 +170,5 @@ public void run(Function function) {
 
             labelCounter++;
         }
-
-        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++;
-        }
-
     }
 }
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java
index 774a30dc31..7a2c27dc89 100644
--- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java
@@ -91,7 +91,7 @@ public static Iterable<Object[]> data() throws IOException {
                 {"offsetof", IMM, PASS, 1},
                 {"ctlz", IMM, PASS, 1},
                 {"cttz", IMM, PASS, 1},
-                {"jumpFromOutside", IMM, PASS, 11}
+                {"jumpIntoLoop", IMM, PASS, 11}
         });
     }
 
diff --git a/dartagnan/src/test/resources/miscellaneous/jumpFromOutside.ll b/dartagnan/src/test/resources/miscellaneous/jumpFromOutside.ll
deleted file mode 100644
index 6faa1c4c16..0000000000
--- a/dartagnan/src/test/resources/miscellaneous/jumpFromOutside.ll
+++ /dev/null
@@ -1,140 +0,0 @@
-; ModuleID = '/home/drc/git/Dat3M/output/jumpFromOutside.ll'
-source_filename = "/home/drc/git/Dat3M/benchmarks/c/miscellaneous/jumpFromOutside.c"
-target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
-target triple = "x86_64-pc-linux-gnu"
-
-@x = dso_local global i32 0, align 4, !dbg !0
-
-; Function Attrs: noinline nounwind uwtable
-define dso_local i32 @main() #0 !dbg !20 {
-  %1 = alloca i32, align 4
-  %2 = alloca i32, align 4
-  store i32 0, i32* %1, align 4
-  call void @llvm.dbg.declare(metadata i32* %2, metadata !24, metadata !DIExpression()), !dbg !25
-  %3 = call i32 @__VERIFIER_nondet_uint(), !dbg !26
-  store i32 %3, i32* %2, align 4, !dbg !25
-  %4 = load i32, i32* %2, align 4, !dbg !27
-  %5 = icmp sle i32 %4, 0, !dbg !29
-  br i1 %5, label %6, label %7, !dbg !30
-
-6:                                                ; preds = %0
-  store i32 0, i32* %1, align 4, !dbg !31
-  br label %21, !dbg !31
-
-7:                                                ; preds = %0
-  br label %8, !dbg !33
-
-8:                                                ; preds = %7
-  call void @llvm.dbg.label(metadata !34), !dbg !35
-  %9 = load i32, i32* %2, align 4, !dbg !36
-  %10 = icmp sge i32 %9, 10, !dbg !38
-  br i1 %10, label %11, label %12, !dbg !39
-
-11:                                               ; preds = %8
-  store i32 5, i32* %2, align 4, !dbg !40
-  br label %16, !dbg !42
-
-12:                                               ; preds = %8
-  br label %13, !dbg !43
-
-13:                                               ; preds = %19, %12
-  call void @llvm.dbg.label(metadata !44), !dbg !45
-  %14 = load i32, i32* %2, align 4, !dbg !46
-  %15 = add nsw i32 %14, 1, !dbg !47
-  store i32 %15, i32* %2, align 4, !dbg !48
-  br label %16, !dbg !49
-
-16:                                               ; preds = %13, %11
-  call void @llvm.dbg.label(metadata !50), !dbg !51
-  %17 = load i32, i32* %2, align 4, !dbg !52
-  %18 = icmp slt i32 %17, 10, !dbg !54
-  br i1 %18, label %19, label %20, !dbg !55
-
-19:                                               ; preds = %16
-  br label %13, !dbg !56
-
-20:                                               ; preds = %16
-  store i32 0, i32* %1, align 4, !dbg !58
-  br label %21, !dbg !58
-
-21:                                               ; preds = %20, %6
-  %22 = load i32, i32* %1, align 4, !dbg !59
-  ret i32 %22, !dbg !59
-}
-
-; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
-declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
-
-declare i32 @__VERIFIER_nondet_uint() #2
-
-; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
-declare void @llvm.dbg.label(metadata) #1
-
-attributes #0 = { noinline nounwind uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
-attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
-attributes #2 = { "frame-pointer"="all" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
-
-!llvm.dbg.cu = !{!2}
-!llvm.module.flags = !{!12, !13, !14, !15, !16, !17, !18}
-!llvm.ident = !{!19}
-
-!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
-!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !5, line: 5, type: !6, isLocal: false, isDefinition: true)
-!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Ubuntu clang version 14.0.0-1ubuntu1.1", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, globals: !4, splitDebugInlining: false, nameTableKind: None)
-!3 = !DIFile(filename: "/home/drc/git/Dat3M/benchmarks/c/miscellaneous/jumpFromOutside.c", directory: "/home/drc/git/Dat3M", checksumkind: CSK_MD5, checksum: "93cac12dbf00c291fa6fe587b400c1e8")
-!4 = !{!0}
-!5 = !DIFile(filename: "benchmarks/c/miscellaneous/jumpFromOutside.c", directory: "/home/drc/git/Dat3M", checksumkind: CSK_MD5, checksum: "93cac12dbf00c291fa6fe587b400c1e8")
-!6 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !7)
-!7 = !DIDerivedType(tag: DW_TAG_typedef, name: "int32_t", file: !8, line: 26, baseType: !9)
-!8 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/stdint-intn.h", directory: "", checksumkind: CSK_MD5, checksum: "55bcbdc3159515ebd91d351a70d505f4")
-!9 = !DIDerivedType(tag: DW_TAG_typedef, name: "__int32_t", file: !10, line: 41, baseType: !11)
-!10 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/types.h", directory: "", checksumkind: CSK_MD5, checksum: "d108b5f93a74c50510d7d9bc0ab36df9")
-!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
-!12 = !{i32 7, !"Dwarf Version", i32 5}
-!13 = !{i32 2, !"Debug Info Version", i32 3}
-!14 = !{i32 1, !"wchar_size", i32 4}
-!15 = !{i32 7, !"PIC Level", i32 2}
-!16 = !{i32 7, !"PIE Level", i32 2}
-!17 = !{i32 7, !"uwtable", i32 1}
-!18 = !{i32 7, !"frame-pointer", i32 2}
-!19 = !{!"Ubuntu clang version 14.0.0-1ubuntu1.1"}
-!20 = distinct !DISubprogram(name: "main", scope: !5, file: !5, line: 7, type: !21, scopeLine: 8, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !23)
-!21 = !DISubroutineType(types: !22)
-!22 = !{!11}
-!23 = !{}
-!24 = !DILocalVariable(name: "x", scope: !20, file: !5, line: 9, type: !11)
-!25 = !DILocation(line: 9, column: 9, scope: !20)
-!26 = !DILocation(line: 9, column: 13, scope: !20)
-!27 = !DILocation(line: 11, column: 9, scope: !28)
-!28 = distinct !DILexicalBlock(scope: !20, file: !5, line: 11, column: 9)
-!29 = !DILocation(line: 11, column: 11, scope: !28)
-!30 = !DILocation(line: 11, column: 9, scope: !20)
-!31 = !DILocation(line: 12, column: 9, scope: !32)
-!32 = distinct !DILexicalBlock(scope: !28, file: !5, line: 11, column: 17)
-!33 = !DILocation(line: 11, column: 14, scope: !28)
-!34 = !DILabel(scope: !20, name: "A", file: !5, line: 15)
-!35 = !DILocation(line: 15, column: 1, scope: !20)
-!36 = !DILocation(line: 16, column: 9, scope: !37)
-!37 = distinct !DILexicalBlock(scope: !20, file: !5, line: 16, column: 9)
-!38 = !DILocation(line: 16, column: 11, scope: !37)
-!39 = !DILocation(line: 16, column: 9, scope: !20)
-!40 = !DILocation(line: 17, column: 11, scope: !41)
-!41 = distinct !DILexicalBlock(scope: !37, file: !5, line: 16, column: 18)
-!42 = !DILocation(line: 18, column: 9, scope: !41)
-!43 = !DILocation(line: 16, column: 14, scope: !37)
-!44 = !DILabel(scope: !20, name: "B", file: !5, line: 20)
-!45 = !DILocation(line: 20, column: 1, scope: !20)
-!46 = !DILocation(line: 21, column: 9, scope: !20)
-!47 = !DILocation(line: 21, column: 11, scope: !20)
-!48 = !DILocation(line: 21, column: 7, scope: !20)
-!49 = !DILocation(line: 21, column: 5, scope: !20)
-!50 = !DILabel(scope: !20, name: "C", file: !5, line: 22)
-!51 = !DILocation(line: 22, column: 1, scope: !20)
-!52 = !DILocation(line: 23, column: 9, scope: !53)
-!53 = distinct !DILexicalBlock(scope: !20, file: !5, line: 23, column: 9)
-!54 = !DILocation(line: 23, column: 11, scope: !53)
-!55 = !DILocation(line: 23, column: 9, scope: !20)
-!56 = !DILocation(line: 24, column: 9, scope: !57)
-!57 = distinct !DILexicalBlock(scope: !53, file: !5, line: 23, column: 17)
-!58 = !DILocation(line: 27, column: 2, scope: !20)
-!59 = !DILocation(line: 28, column: 1, scope: !20)
diff --git a/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll b/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll
new file mode 100644
index 0000000000..bf07e37fe8
--- /dev/null
+++ b/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll
@@ -0,0 +1,142 @@
+; ModuleID = '/home/drc/git/Dat3M/output/jumpIntoLoop.ll'
+source_filename = "/home/drc/git/Dat3M/benchmarks/c/miscellaneous/jumpIntoLoop.c"
+target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-pc-linux-gnu"
+
+@x = dso_local global i32 0, align 4, !dbg !0
+@.str = private unnamed_addr constant [7 x i8] c"x <= 5\00", align 1
+@.str.1 = private unnamed_addr constant [62 x i8] c"/home/drc/git/Dat3M/benchmarks/c/miscellaneous/jumpIntoLoop.c\00", align 1
+@__PRETTY_FUNCTION__.main = private unnamed_addr constant [11 x i8] c"int main()\00", align 1
+
+; Function Attrs: noinline nounwind uwtable
+define dso_local i32 @main() #0 !dbg !20 {
+  %1 = alloca i32, align 4
+  %2 = alloca i32, align 4
+  store i32 0, i32* %1, align 4
+  call void @llvm.dbg.declare(metadata i32* %2, metadata !24, metadata !DIExpression()), !dbg !25
+  %3 = call i32 @__VERIFIER_nondet_int(), !dbg !26
+  store i32 %3, i32* %2, align 4, !dbg !25
+  %4 = load i32, i32* %2, align 4, !dbg !27
+  %5 = icmp eq i32 %4, 42, !dbg !29
+  br i1 %5, label %6, label %7, !dbg !30
+
+6:                                                ; preds = %0
+  br label %12, !dbg !31
+
+7:                                                ; preds = %0
+  store i32 0, i32* %2, align 4, !dbg !32
+  br label %8, !dbg !34
+
+8:                                                ; preds = %15, %7
+  %9 = load i32, i32* %2, align 4, !dbg !35
+  %10 = icmp slt i32 %9, 5, !dbg !37
+  br i1 %10, label %11, label %18, !dbg !38
+
+11:                                               ; preds = %8
+  br label %12, !dbg !39
+
+12:                                               ; preds = %11, %6
+  call void @llvm.dbg.label(metadata !40), !dbg !42
+  %13 = load volatile i32, i32* @x, align 4, !dbg !43
+  %14 = add nsw i32 %13, 1, !dbg !43
+  store volatile i32 %14, i32* @x, align 4, !dbg !43
+  br label %15, !dbg !44
+
+15:                                               ; preds = %12
+  %16 = load i32, i32* %2, align 4, !dbg !45
+  %17 = add nsw i32 %16, 1, !dbg !45
+  store i32 %17, i32* %2, align 4, !dbg !45
+  br label %8, !dbg !46, !llvm.loop !47
+
+18:                                               ; preds = %8
+  %19 = load volatile i32, i32* @x, align 4, !dbg !50
+  %20 = icmp sle i32 %19, 5, !dbg !50
+  br i1 %20, label %21, label %22, !dbg !53
+
+21:                                               ; preds = %18
+  br label %23, !dbg !53
+
+22:                                               ; preds = %18
+  call void @__assert_fail(i8* noundef getelementptr inbounds ([7 x i8], [7 x i8]* @.str, i64 0, i64 0), i8* noundef getelementptr inbounds ([62 x i8], [62 x i8]* @.str.1, i64 0, i64 0), i32 noundef 17, i8* noundef getelementptr inbounds ([11 x i8], [11 x i8]* @__PRETTY_FUNCTION__.main, i64 0, i64 0)) #4, !dbg !50
+  unreachable, !dbg !50
+
+23:                                               ; preds = %21
+  ret i32 0, !dbg !54
+}
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
+
+declare i32 @__VERIFIER_nondet_int() #2
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.label(metadata) #1
+
+; Function Attrs: noreturn nounwind
+declare void @__assert_fail(i8* noundef, i8* noundef, i32 noundef, i8* noundef) #3
+
+attributes #0 = { noinline nounwind uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
+attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
+attributes #2 = { "frame-pointer"="all" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
+attributes #3 = { noreturn nounwind "frame-pointer"="all" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
+attributes #4 = { noreturn nounwind }
+
+!llvm.dbg.cu = !{!2}
+!llvm.module.flags = !{!12, !13, !14, !15, !16, !17, !18}
+!llvm.ident = !{!19}
+
+!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !5, line: 5, type: !6, isLocal: false, isDefinition: true)
+!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Ubuntu clang version 14.0.0-1ubuntu1.1", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, globals: !4, splitDebugInlining: false, nameTableKind: None)
+!3 = !DIFile(filename: "/home/drc/git/Dat3M/benchmarks/c/miscellaneous/jumpIntoLoop.c", directory: "/home/drc/git/Dat3M", checksumkind: CSK_MD5, checksum: "f0dc8ee3df8cc5d1d11ba0339e7a8a1b")
+!4 = !{!0}
+!5 = !DIFile(filename: "benchmarks/c/miscellaneous/jumpIntoLoop.c", directory: "/home/drc/git/Dat3M", checksumkind: CSK_MD5, checksum: "f0dc8ee3df8cc5d1d11ba0339e7a8a1b")
+!6 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !7)
+!7 = !DIDerivedType(tag: DW_TAG_typedef, name: "int32_t", file: !8, line: 26, baseType: !9)
+!8 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/stdint-intn.h", directory: "", checksumkind: CSK_MD5, checksum: "55bcbdc3159515ebd91d351a70d505f4")
+!9 = !DIDerivedType(tag: DW_TAG_typedef, name: "__int32_t", file: !10, line: 41, baseType: !11)
+!10 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/types.h", directory: "", checksumkind: CSK_MD5, checksum: "d108b5f93a74c50510d7d9bc0ab36df9")
+!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!12 = !{i32 7, !"Dwarf Version", i32 5}
+!13 = !{i32 2, !"Debug Info Version", i32 3}
+!14 = !{i32 1, !"wchar_size", i32 4}
+!15 = !{i32 7, !"PIC Level", i32 2}
+!16 = !{i32 7, !"PIE Level", i32 2}
+!17 = !{i32 7, !"uwtable", i32 1}
+!18 = !{i32 7, !"frame-pointer", i32 2}
+!19 = !{!"Ubuntu clang version 14.0.0-1ubuntu1.1"}
+!20 = distinct !DISubprogram(name: "main", scope: !5, file: !5, line: 7, type: !21, scopeLine: 8, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !23)
+!21 = !DISubroutineType(types: !22)
+!22 = !{!11}
+!23 = !{}
+!24 = !DILocalVariable(name: "i", scope: !20, file: !5, line: 9, type: !11)
+!25 = !DILocation(line: 9, column: 9, scope: !20)
+!26 = !DILocation(line: 9, column: 13, scope: !20)
+!27 = !DILocation(line: 10, column: 9, scope: !28)
+!28 = distinct !DILexicalBlock(scope: !20, file: !5, line: 10, column: 9)
+!29 = !DILocation(line: 10, column: 11, scope: !28)
+!30 = !DILocation(line: 10, column: 9, scope: !20)
+!31 = !DILocation(line: 10, column: 18, scope: !28)
+!32 = !DILocation(line: 12, column: 12, scope: !33)
+!33 = distinct !DILexicalBlock(scope: !20, file: !5, line: 12, column: 5)
+!34 = !DILocation(line: 12, column: 10, scope: !33)
+!35 = !DILocation(line: 12, column: 17, scope: !36)
+!36 = distinct !DILexicalBlock(scope: !33, file: !5, line: 12, column: 5)
+!37 = !DILocation(line: 12, column: 19, scope: !36)
+!38 = !DILocation(line: 12, column: 5, scope: !33)
+!39 = !DILocation(line: 12, column: 29, scope: !36)
+!40 = !DILabel(scope: !41, name: "L", file: !5, line: 13)
+!41 = distinct !DILexicalBlock(scope: !36, file: !5, line: 12, column: 29)
+!42 = !DILocation(line: 13, column: 1, scope: !41)
+!43 = !DILocation(line: 14, column: 6, scope: !41)
+!44 = !DILocation(line: 15, column: 5, scope: !41)
+!45 = !DILocation(line: 12, column: 25, scope: !36)
+!46 = !DILocation(line: 12, column: 5, scope: !36)
+!47 = distinct !{!47, !38, !48, !49}
+!48 = !DILocation(line: 15, column: 5, scope: !33)
+!49 = !{!"llvm.loop.mustprogress"}
+!50 = !DILocation(line: 17, column: 5, scope: !51)
+!51 = distinct !DILexicalBlock(scope: !52, file: !5, line: 17, column: 5)
+!52 = distinct !DILexicalBlock(scope: !20, file: !5, line: 17, column: 5)
+!53 = !DILocation(line: 17, column: 5, scope: !52)
+!54 = !DILocation(line: 18, column: 2, scope: !20)

From cb49ff8e3131107650c5cbbb6e1eefdabd16aaef Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Thu, 1 Aug 2024 19:25:24 +0800
Subject: [PATCH 09/14] Move miscenalleous folder one level up

---
 benchmarks/{c => }/miscellaneous/MP_atomic_bool.c            | 0
 benchmarks/{c => }/miscellaneous/SB-RMW.c                    | 0
 benchmarks/{c => }/miscellaneous/SB-asm-lwsync+sync.c        | 0
 benchmarks/{c => }/miscellaneous/SB-asm-mfences.c            | 0
 benchmarks/{c => }/miscellaneous/SB-asm-syncs.c              | 0
 benchmarks/{c => }/miscellaneous/ctlz.c                      | 0
 benchmarks/{c => }/miscellaneous/cttz.c                      | 0
 benchmarks/{c => }/miscellaneous/funcPtrInStaticMemory.c     | 0
 benchmarks/{c => }/miscellaneous/idd_dynamic.c               | 0
 benchmarks/{c => }/miscellaneous/jumpIntoLoop.c              | 0
 benchmarks/{c => }/miscellaneous/memcpy_s.c                  | 0
 benchmarks/{c => }/miscellaneous/multipleBackJumps.c         | 0
 benchmarks/{c => }/miscellaneous/nondet_loop.c               | 0
 benchmarks/{c => }/miscellaneous/offsetof.c                  | 0
 benchmarks/{c => }/miscellaneous/propagatableSideEffects.c   | 0
 benchmarks/{c => }/miscellaneous/pthread.c                   | 0
 benchmarks/{c => }/miscellaneous/recursion.c                 | 0
 benchmarks/{c => }/miscellaneous/staticLoops.c               | 0
 benchmarks/{c => }/miscellaneous/thread_chaining.c           | 0
 benchmarks/{c => }/miscellaneous/thread_id.c                 | 0
 benchmarks/{c => }/miscellaneous/thread_inlining.c           | 0
 benchmarks/{c => }/miscellaneous/thread_inlining_complex.c   | 0
 benchmarks/{c => }/miscellaneous/thread_inlining_complex_2.c | 0
 benchmarks/{c => }/miscellaneous/thread_local.c              | 0
 benchmarks/{c => }/miscellaneous/thread_loop.c               | 0
 benchmarks/{c => }/miscellaneous/uninitRead.c                | 0
 benchmarks/{c => }/miscellaneous/verifierAssert.c            | 0
 27 files changed, 0 insertions(+), 0 deletions(-)
 rename benchmarks/{c => }/miscellaneous/MP_atomic_bool.c (100%)
 rename benchmarks/{c => }/miscellaneous/SB-RMW.c (100%)
 rename benchmarks/{c => }/miscellaneous/SB-asm-lwsync+sync.c (100%)
 rename benchmarks/{c => }/miscellaneous/SB-asm-mfences.c (100%)
 rename benchmarks/{c => }/miscellaneous/SB-asm-syncs.c (100%)
 rename benchmarks/{c => }/miscellaneous/ctlz.c (100%)
 rename benchmarks/{c => }/miscellaneous/cttz.c (100%)
 rename benchmarks/{c => }/miscellaneous/funcPtrInStaticMemory.c (100%)
 rename benchmarks/{c => }/miscellaneous/idd_dynamic.c (100%)
 rename benchmarks/{c => }/miscellaneous/jumpIntoLoop.c (100%)
 rename benchmarks/{c => }/miscellaneous/memcpy_s.c (100%)
 rename benchmarks/{c => }/miscellaneous/multipleBackJumps.c (100%)
 rename benchmarks/{c => }/miscellaneous/nondet_loop.c (100%)
 rename benchmarks/{c => }/miscellaneous/offsetof.c (100%)
 rename benchmarks/{c => }/miscellaneous/propagatableSideEffects.c (100%)
 rename benchmarks/{c => }/miscellaneous/pthread.c (100%)
 rename benchmarks/{c => }/miscellaneous/recursion.c (100%)
 rename benchmarks/{c => }/miscellaneous/staticLoops.c (100%)
 rename benchmarks/{c => }/miscellaneous/thread_chaining.c (100%)
 rename benchmarks/{c => }/miscellaneous/thread_id.c (100%)
 rename benchmarks/{c => }/miscellaneous/thread_inlining.c (100%)
 rename benchmarks/{c => }/miscellaneous/thread_inlining_complex.c (100%)
 rename benchmarks/{c => }/miscellaneous/thread_inlining_complex_2.c (100%)
 rename benchmarks/{c => }/miscellaneous/thread_local.c (100%)
 rename benchmarks/{c => }/miscellaneous/thread_loop.c (100%)
 rename benchmarks/{c => }/miscellaneous/uninitRead.c (100%)
 rename benchmarks/{c => }/miscellaneous/verifierAssert.c (100%)

diff --git a/benchmarks/c/miscellaneous/MP_atomic_bool.c b/benchmarks/miscellaneous/MP_atomic_bool.c
similarity index 100%
rename from benchmarks/c/miscellaneous/MP_atomic_bool.c
rename to benchmarks/miscellaneous/MP_atomic_bool.c
diff --git a/benchmarks/c/miscellaneous/SB-RMW.c b/benchmarks/miscellaneous/SB-RMW.c
similarity index 100%
rename from benchmarks/c/miscellaneous/SB-RMW.c
rename to benchmarks/miscellaneous/SB-RMW.c
diff --git a/benchmarks/c/miscellaneous/SB-asm-lwsync+sync.c b/benchmarks/miscellaneous/SB-asm-lwsync+sync.c
similarity index 100%
rename from benchmarks/c/miscellaneous/SB-asm-lwsync+sync.c
rename to benchmarks/miscellaneous/SB-asm-lwsync+sync.c
diff --git a/benchmarks/c/miscellaneous/SB-asm-mfences.c b/benchmarks/miscellaneous/SB-asm-mfences.c
similarity index 100%
rename from benchmarks/c/miscellaneous/SB-asm-mfences.c
rename to benchmarks/miscellaneous/SB-asm-mfences.c
diff --git a/benchmarks/c/miscellaneous/SB-asm-syncs.c b/benchmarks/miscellaneous/SB-asm-syncs.c
similarity index 100%
rename from benchmarks/c/miscellaneous/SB-asm-syncs.c
rename to benchmarks/miscellaneous/SB-asm-syncs.c
diff --git a/benchmarks/c/miscellaneous/ctlz.c b/benchmarks/miscellaneous/ctlz.c
similarity index 100%
rename from benchmarks/c/miscellaneous/ctlz.c
rename to benchmarks/miscellaneous/ctlz.c
diff --git a/benchmarks/c/miscellaneous/cttz.c b/benchmarks/miscellaneous/cttz.c
similarity index 100%
rename from benchmarks/c/miscellaneous/cttz.c
rename to benchmarks/miscellaneous/cttz.c
diff --git a/benchmarks/c/miscellaneous/funcPtrInStaticMemory.c b/benchmarks/miscellaneous/funcPtrInStaticMemory.c
similarity index 100%
rename from benchmarks/c/miscellaneous/funcPtrInStaticMemory.c
rename to benchmarks/miscellaneous/funcPtrInStaticMemory.c
diff --git a/benchmarks/c/miscellaneous/idd_dynamic.c b/benchmarks/miscellaneous/idd_dynamic.c
similarity index 100%
rename from benchmarks/c/miscellaneous/idd_dynamic.c
rename to benchmarks/miscellaneous/idd_dynamic.c
diff --git a/benchmarks/c/miscellaneous/jumpIntoLoop.c b/benchmarks/miscellaneous/jumpIntoLoop.c
similarity index 100%
rename from benchmarks/c/miscellaneous/jumpIntoLoop.c
rename to benchmarks/miscellaneous/jumpIntoLoop.c
diff --git a/benchmarks/c/miscellaneous/memcpy_s.c b/benchmarks/miscellaneous/memcpy_s.c
similarity index 100%
rename from benchmarks/c/miscellaneous/memcpy_s.c
rename to benchmarks/miscellaneous/memcpy_s.c
diff --git a/benchmarks/c/miscellaneous/multipleBackJumps.c b/benchmarks/miscellaneous/multipleBackJumps.c
similarity index 100%
rename from benchmarks/c/miscellaneous/multipleBackJumps.c
rename to benchmarks/miscellaneous/multipleBackJumps.c
diff --git a/benchmarks/c/miscellaneous/nondet_loop.c b/benchmarks/miscellaneous/nondet_loop.c
similarity index 100%
rename from benchmarks/c/miscellaneous/nondet_loop.c
rename to benchmarks/miscellaneous/nondet_loop.c
diff --git a/benchmarks/c/miscellaneous/offsetof.c b/benchmarks/miscellaneous/offsetof.c
similarity index 100%
rename from benchmarks/c/miscellaneous/offsetof.c
rename to benchmarks/miscellaneous/offsetof.c
diff --git a/benchmarks/c/miscellaneous/propagatableSideEffects.c b/benchmarks/miscellaneous/propagatableSideEffects.c
similarity index 100%
rename from benchmarks/c/miscellaneous/propagatableSideEffects.c
rename to benchmarks/miscellaneous/propagatableSideEffects.c
diff --git a/benchmarks/c/miscellaneous/pthread.c b/benchmarks/miscellaneous/pthread.c
similarity index 100%
rename from benchmarks/c/miscellaneous/pthread.c
rename to benchmarks/miscellaneous/pthread.c
diff --git a/benchmarks/c/miscellaneous/recursion.c b/benchmarks/miscellaneous/recursion.c
similarity index 100%
rename from benchmarks/c/miscellaneous/recursion.c
rename to benchmarks/miscellaneous/recursion.c
diff --git a/benchmarks/c/miscellaneous/staticLoops.c b/benchmarks/miscellaneous/staticLoops.c
similarity index 100%
rename from benchmarks/c/miscellaneous/staticLoops.c
rename to benchmarks/miscellaneous/staticLoops.c
diff --git a/benchmarks/c/miscellaneous/thread_chaining.c b/benchmarks/miscellaneous/thread_chaining.c
similarity index 100%
rename from benchmarks/c/miscellaneous/thread_chaining.c
rename to benchmarks/miscellaneous/thread_chaining.c
diff --git a/benchmarks/c/miscellaneous/thread_id.c b/benchmarks/miscellaneous/thread_id.c
similarity index 100%
rename from benchmarks/c/miscellaneous/thread_id.c
rename to benchmarks/miscellaneous/thread_id.c
diff --git a/benchmarks/c/miscellaneous/thread_inlining.c b/benchmarks/miscellaneous/thread_inlining.c
similarity index 100%
rename from benchmarks/c/miscellaneous/thread_inlining.c
rename to benchmarks/miscellaneous/thread_inlining.c
diff --git a/benchmarks/c/miscellaneous/thread_inlining_complex.c b/benchmarks/miscellaneous/thread_inlining_complex.c
similarity index 100%
rename from benchmarks/c/miscellaneous/thread_inlining_complex.c
rename to benchmarks/miscellaneous/thread_inlining_complex.c
diff --git a/benchmarks/c/miscellaneous/thread_inlining_complex_2.c b/benchmarks/miscellaneous/thread_inlining_complex_2.c
similarity index 100%
rename from benchmarks/c/miscellaneous/thread_inlining_complex_2.c
rename to benchmarks/miscellaneous/thread_inlining_complex_2.c
diff --git a/benchmarks/c/miscellaneous/thread_local.c b/benchmarks/miscellaneous/thread_local.c
similarity index 100%
rename from benchmarks/c/miscellaneous/thread_local.c
rename to benchmarks/miscellaneous/thread_local.c
diff --git a/benchmarks/c/miscellaneous/thread_loop.c b/benchmarks/miscellaneous/thread_loop.c
similarity index 100%
rename from benchmarks/c/miscellaneous/thread_loop.c
rename to benchmarks/miscellaneous/thread_loop.c
diff --git a/benchmarks/c/miscellaneous/uninitRead.c b/benchmarks/miscellaneous/uninitRead.c
similarity index 100%
rename from benchmarks/c/miscellaneous/uninitRead.c
rename to benchmarks/miscellaneous/uninitRead.c
diff --git a/benchmarks/c/miscellaneous/verifierAssert.c b/benchmarks/miscellaneous/verifierAssert.c
similarity index 100%
rename from benchmarks/c/miscellaneous/verifierAssert.c
rename to benchmarks/miscellaneous/verifierAssert.c

From 5aaaa8aea5925ee1b8613c6c4a0b99d4bf536776 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Date: Thu, 1 Aug 2024 14:48:33 +0200
Subject: [PATCH 10/14] Feedback implemented

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
---
 benchmarks/miscellaneous/jumpIntoLoop.c       |  13 +-
 .../resources/miscellaneous/jumpIntoLoop.ll   | 246 ++++++++++--------
 2 files changed, 138 insertions(+), 121 deletions(-)

diff --git a/benchmarks/miscellaneous/jumpIntoLoop.c b/benchmarks/miscellaneous/jumpIntoLoop.c
index 657dca65ae..7b42934bae 100644
--- a/benchmarks/miscellaneous/jumpIntoLoop.c
+++ b/benchmarks/miscellaneous/jumpIntoLoop.c
@@ -6,14 +6,15 @@ volatile int32_t x = 0;
 
 int main()
 {
-    int i = __VERIFIER_nondet_int();
-    if (i == 42) goto L;
+    int i = 0;
+    int jumpIntoLoop = __VERIFIER_nondet_bool();
+    if (jumpIntoLoop) goto L;
 
-    for (i = 0; i < 5; i++) {
+    for (i = 1; i < 5; i++) {
 L:
-    x++;
+        x++;
     }
 
-    assert(x <= 5);
-	return 0;
+    assert((!jumpIntoLoop || x == 5) && (jumpIntoLoop || x == 4));
+    return 0;
 }
diff --git a/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll b/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll
index bf07e37fe8..cff00c2895 100644
--- a/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll
+++ b/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll
@@ -1,142 +1,158 @@
-; ModuleID = '/home/drc/git/Dat3M/output/jumpIntoLoop.ll'
-source_filename = "/home/drc/git/Dat3M/benchmarks/c/miscellaneous/jumpIntoLoop.c"
+; ModuleID = '/home/ponce/git/Dat3M/output/jumpIntoLoop.ll'
+source_filename = "/home/ponce/git/Dat3M/benchmarks/miscellaneous/jumpIntoLoop.c"
 target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
 target triple = "x86_64-pc-linux-gnu"
 
 @x = dso_local global i32 0, align 4, !dbg !0
-@.str = private unnamed_addr constant [7 x i8] c"x <= 5\00", align 1
-@.str.1 = private unnamed_addr constant [62 x i8] c"/home/drc/git/Dat3M/benchmarks/c/miscellaneous/jumpIntoLoop.c\00", align 1
+@.str = private unnamed_addr constant [54 x i8] c"(!jumpIntoLoop || x == 5) && (jumpIntoLoop || x == 4)\00", align 1
+@.str.1 = private unnamed_addr constant [62 x i8] c"/home/ponce/git/Dat3M/benchmarks/miscellaneous/jumpIntoLoop.c\00", align 1
 @__PRETTY_FUNCTION__.main = private unnamed_addr constant [11 x i8] c"int main()\00", align 1
 
 ; Function Attrs: noinline nounwind uwtable
-define dso_local i32 @main() #0 !dbg !20 {
+define dso_local i32 @main() #0 !dbg !17 {
   %1 = alloca i32, align 4
   %2 = alloca i32, align 4
+  %3 = alloca i32, align 4
   store i32 0, i32* %1, align 4
-  call void @llvm.dbg.declare(metadata i32* %2, metadata !24, metadata !DIExpression()), !dbg !25
-  %3 = call i32 @__VERIFIER_nondet_int(), !dbg !26
-  store i32 %3, i32* %2, align 4, !dbg !25
-  %4 = load i32, i32* %2, align 4, !dbg !27
-  %5 = icmp eq i32 %4, 42, !dbg !29
-  br i1 %5, label %6, label %7, !dbg !30
-
-6:                                                ; preds = %0
-  br label %12, !dbg !31
-
-7:                                                ; preds = %0
-  store i32 0, i32* %2, align 4, !dbg !32
-  br label %8, !dbg !34
-
-8:                                                ; preds = %15, %7
-  %9 = load i32, i32* %2, align 4, !dbg !35
-  %10 = icmp slt i32 %9, 5, !dbg !37
-  br i1 %10, label %11, label %18, !dbg !38
-
-11:                                               ; preds = %8
-  br label %12, !dbg !39
-
-12:                                               ; preds = %11, %6
-  call void @llvm.dbg.label(metadata !40), !dbg !42
-  %13 = load volatile i32, i32* @x, align 4, !dbg !43
-  %14 = add nsw i32 %13, 1, !dbg !43
-  store volatile i32 %14, i32* @x, align 4, !dbg !43
-  br label %15, !dbg !44
-
-15:                                               ; preds = %12
-  %16 = load i32, i32* %2, align 4, !dbg !45
-  %17 = add nsw i32 %16, 1, !dbg !45
-  store i32 %17, i32* %2, align 4, !dbg !45
-  br label %8, !dbg !46, !llvm.loop !47
-
-18:                                               ; preds = %8
-  %19 = load volatile i32, i32* @x, align 4, !dbg !50
-  %20 = icmp sle i32 %19, 5, !dbg !50
-  br i1 %20, label %21, label %22, !dbg !53
-
-21:                                               ; preds = %18
-  br label %23, !dbg !53
-
-22:                                               ; preds = %18
-  call void @__assert_fail(i8* noundef getelementptr inbounds ([7 x i8], [7 x i8]* @.str, i64 0, i64 0), i8* noundef getelementptr inbounds ([62 x i8], [62 x i8]* @.str.1, i64 0, i64 0), i32 noundef 17, i8* noundef getelementptr inbounds ([11 x i8], [11 x i8]* @__PRETTY_FUNCTION__.main, i64 0, i64 0)) #4, !dbg !50
-  unreachable, !dbg !50
-
-23:                                               ; preds = %21
-  ret i32 0, !dbg !54
+  call void @llvm.dbg.declare(metadata i32* %2, metadata !20, metadata !DIExpression()), !dbg !21
+  store i32 0, i32* %2, align 4, !dbg !21
+  call void @llvm.dbg.declare(metadata i32* %3, metadata !22, metadata !DIExpression()), !dbg !23
+  %4 = call zeroext i1 @__VERIFIER_nondet_bool(), !dbg !24
+  %5 = zext i1 %4 to i32, !dbg !24
+  store i32 %5, i32* %3, align 4, !dbg !23
+  %6 = load i32, i32* %3, align 4, !dbg !25
+  %7 = icmp ne i32 %6, 0, !dbg !25
+  br i1 %7, label %8, label %9, !dbg !27
+
+8:                                                ; preds = %0
+  br label %14, !dbg !28
+
+9:                                                ; preds = %0
+  store i32 1, i32* %2, align 4, !dbg !29
+  br label %10, !dbg !31
+
+10:                                               ; preds = %17, %9
+  %11 = load i32, i32* %2, align 4, !dbg !32
+  %12 = icmp slt i32 %11, 5, !dbg !34
+  br i1 %12, label %13, label %20, !dbg !35
+
+13:                                               ; preds = %10
+  br label %14, !dbg !36
+
+14:                                               ; preds = %13, %8
+  call void @llvm.dbg.label(metadata !37), !dbg !39
+  %15 = load volatile i32, i32* @x, align 4, !dbg !40
+  %16 = add nsw i32 %15, 1, !dbg !40
+  store volatile i32 %16, i32* @x, align 4, !dbg !40
+  br label %17, !dbg !41
+
+17:                                               ; preds = %14
+  %18 = load i32, i32* %2, align 4, !dbg !42
+  %19 = add nsw i32 %18, 1, !dbg !42
+  store i32 %19, i32* %2, align 4, !dbg !42
+  br label %10, !dbg !43, !llvm.loop !44
+
+20:                                               ; preds = %10
+  %21 = load i32, i32* %3, align 4, !dbg !47
+  %22 = icmp ne i32 %21, 0, !dbg !47
+  br i1 %22, label %23, label %26, !dbg !47
+
+23:                                               ; preds = %20
+  %24 = load volatile i32, i32* @x, align 4, !dbg !47
+  %25 = icmp eq i32 %24, 5, !dbg !47
+  br i1 %25, label %26, label %33, !dbg !47
+
+26:                                               ; preds = %23, %20
+  %27 = load i32, i32* %3, align 4, !dbg !47
+  %28 = icmp ne i32 %27, 0, !dbg !47
+  br i1 %28, label %32, label %29, !dbg !47
+
+29:                                               ; preds = %26
+  %30 = load volatile i32, i32* @x, align 4, !dbg !47
+  %31 = icmp eq i32 %30, 4, !dbg !47
+  br i1 %31, label %32, label %33, !dbg !50
+
+32:                                               ; preds = %29, %26
+  br label %34, !dbg !50
+
+33:                                               ; preds = %29, %23
+  call void @__assert_fail(i8* getelementptr inbounds ([54 x i8], [54 x i8]* @.str, i64 0, i64 0), i8* getelementptr inbounds ([62 x i8], [62 x i8]* @.str.1, i64 0, i64 0), i32 18, i8* getelementptr inbounds ([11 x i8], [11 x i8]* @__PRETTY_FUNCTION__.main, i64 0, i64 0)) #4, !dbg !47
+  unreachable, !dbg !47
+
+34:                                               ; preds = %32
+  ret i32 0, !dbg !51
 }
 
 ; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
 declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
 
-declare i32 @__VERIFIER_nondet_int() #2
+declare dso_local zeroext i1 @__VERIFIER_nondet_bool() #2
 
 ; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
 declare void @llvm.dbg.label(metadata) #1
 
 ; Function Attrs: noreturn nounwind
-declare void @__assert_fail(i8* noundef, i8* noundef, i32 noundef, i8* noundef) #3
+declare dso_local void @__assert_fail(i8*, i8*, i32, i8*) #3
 
-attributes #0 = { noinline nounwind uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
+attributes #0 = { noinline nounwind uwtable "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" }
 attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
-attributes #2 = { "frame-pointer"="all" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
-attributes #3 = { noreturn nounwind "frame-pointer"="all" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
+attributes #2 = { "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" }
+attributes #3 = { noreturn nounwind "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" }
 attributes #4 = { noreturn nounwind }
 
 !llvm.dbg.cu = !{!2}
-!llvm.module.flags = !{!12, !13, !14, !15, !16, !17, !18}
-!llvm.ident = !{!19}
+!llvm.module.flags = !{!13, !14, !15}
+!llvm.ident = !{!16}
 
 !0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
-!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !5, line: 5, type: !6, isLocal: false, isDefinition: true)
-!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Ubuntu clang version 14.0.0-1ubuntu1.1", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, globals: !4, splitDebugInlining: false, nameTableKind: None)
-!3 = !DIFile(filename: "/home/drc/git/Dat3M/benchmarks/c/miscellaneous/jumpIntoLoop.c", directory: "/home/drc/git/Dat3M", checksumkind: CSK_MD5, checksum: "f0dc8ee3df8cc5d1d11ba0339e7a8a1b")
-!4 = !{!0}
-!5 = !DIFile(filename: "benchmarks/c/miscellaneous/jumpIntoLoop.c", directory: "/home/drc/git/Dat3M", checksumkind: CSK_MD5, checksum: "f0dc8ee3df8cc5d1d11ba0339e7a8a1b")
-!6 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !7)
-!7 = !DIDerivedType(tag: DW_TAG_typedef, name: "int32_t", file: !8, line: 26, baseType: !9)
-!8 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/stdint-intn.h", directory: "", checksumkind: CSK_MD5, checksum: "55bcbdc3159515ebd91d351a70d505f4")
-!9 = !DIDerivedType(tag: DW_TAG_typedef, name: "__int32_t", file: !10, line: 41, baseType: !11)
-!10 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/types.h", directory: "", checksumkind: CSK_MD5, checksum: "d108b5f93a74c50510d7d9bc0ab36df9")
-!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
-!12 = !{i32 7, !"Dwarf Version", i32 5}
-!13 = !{i32 2, !"Debug Info Version", i32 3}
-!14 = !{i32 1, !"wchar_size", i32 4}
-!15 = !{i32 7, !"PIC Level", i32 2}
-!16 = !{i32 7, !"PIE Level", i32 2}
-!17 = !{i32 7, !"uwtable", i32 1}
-!18 = !{i32 7, !"frame-pointer", i32 2}
-!19 = !{!"Ubuntu clang version 14.0.0-1ubuntu1.1"}
-!20 = distinct !DISubprogram(name: "main", scope: !5, file: !5, line: 7, type: !21, scopeLine: 8, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !23)
-!21 = !DISubroutineType(types: !22)
-!22 = !{!11}
-!23 = !{}
-!24 = !DILocalVariable(name: "i", scope: !20, file: !5, line: 9, type: !11)
-!25 = !DILocation(line: 9, column: 9, scope: !20)
-!26 = !DILocation(line: 9, column: 13, scope: !20)
-!27 = !DILocation(line: 10, column: 9, scope: !28)
-!28 = distinct !DILexicalBlock(scope: !20, file: !5, line: 10, column: 9)
-!29 = !DILocation(line: 10, column: 11, scope: !28)
-!30 = !DILocation(line: 10, column: 9, scope: !20)
-!31 = !DILocation(line: 10, column: 18, scope: !28)
-!32 = !DILocation(line: 12, column: 12, scope: !33)
-!33 = distinct !DILexicalBlock(scope: !20, file: !5, line: 12, column: 5)
-!34 = !DILocation(line: 12, column: 10, scope: !33)
-!35 = !DILocation(line: 12, column: 17, scope: !36)
-!36 = distinct !DILexicalBlock(scope: !33, file: !5, line: 12, column: 5)
-!37 = !DILocation(line: 12, column: 19, scope: !36)
-!38 = !DILocation(line: 12, column: 5, scope: !33)
-!39 = !DILocation(line: 12, column: 29, scope: !36)
-!40 = !DILabel(scope: !41, name: "L", file: !5, line: 13)
-!41 = distinct !DILexicalBlock(scope: !36, file: !5, line: 12, column: 29)
-!42 = !DILocation(line: 13, column: 1, scope: !41)
-!43 = !DILocation(line: 14, column: 6, scope: !41)
-!44 = !DILocation(line: 15, column: 5, scope: !41)
-!45 = !DILocation(line: 12, column: 25, scope: !36)
-!46 = !DILocation(line: 12, column: 5, scope: !36)
-!47 = distinct !{!47, !38, !48, !49}
-!48 = !DILocation(line: 15, column: 5, scope: !33)
-!49 = !{!"llvm.loop.mustprogress"}
-!50 = !DILocation(line: 17, column: 5, scope: !51)
-!51 = distinct !DILexicalBlock(scope: !52, file: !5, line: 17, column: 5)
-!52 = distinct !DILexicalBlock(scope: !20, file: !5, line: 17, column: 5)
-!53 = !DILocation(line: 17, column: 5, scope: !52)
-!54 = !DILocation(line: 18, column: 2, scope: !20)
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !6, line: 5, type: !7, isLocal: false, isDefinition: true)
+!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Ubuntu clang version 12.0.0-3ubuntu1~20.04.5", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, enums: !4, globals: !5, splitDebugInlining: false, nameTableKind: None)
+!3 = !DIFile(filename: "/home/ponce/git/Dat3M/benchmarks/miscellaneous/jumpIntoLoop.c", directory: "/home/ponce/git/Dat3M")
+!4 = !{}
+!5 = !{!0}
+!6 = !DIFile(filename: "benchmarks/miscellaneous/jumpIntoLoop.c", directory: "/home/ponce/git/Dat3M")
+!7 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !8)
+!8 = !DIDerivedType(tag: DW_TAG_typedef, name: "int32_t", file: !9, line: 26, baseType: !10)
+!9 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/stdint-intn.h", directory: "")
+!10 = !DIDerivedType(tag: DW_TAG_typedef, name: "__int32_t", file: !11, line: 41, baseType: !12)
+!11 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/types.h", directory: "")
+!12 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!13 = !{i32 7, !"Dwarf Version", i32 4}
+!14 = !{i32 2, !"Debug Info Version", i32 3}
+!15 = !{i32 1, !"wchar_size", i32 4}
+!16 = !{!"Ubuntu clang version 12.0.0-3ubuntu1~20.04.5"}
+!17 = distinct !DISubprogram(name: "main", scope: !6, file: !6, line: 7, type: !18, scopeLine: 8, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !4)
+!18 = !DISubroutineType(types: !19)
+!19 = !{!12}
+!20 = !DILocalVariable(name: "i", scope: !17, file: !6, line: 9, type: !12)
+!21 = !DILocation(line: 9, column: 9, scope: !17)
+!22 = !DILocalVariable(name: "jumpIntoLoop", scope: !17, file: !6, line: 10, type: !12)
+!23 = !DILocation(line: 10, column: 9, scope: !17)
+!24 = !DILocation(line: 10, column: 24, scope: !17)
+!25 = !DILocation(line: 11, column: 9, scope: !26)
+!26 = distinct !DILexicalBlock(scope: !17, file: !6, line: 11, column: 9)
+!27 = !DILocation(line: 11, column: 9, scope: !17)
+!28 = !DILocation(line: 11, column: 23, scope: !26)
+!29 = !DILocation(line: 13, column: 12, scope: !30)
+!30 = distinct !DILexicalBlock(scope: !17, file: !6, line: 13, column: 5)
+!31 = !DILocation(line: 13, column: 10, scope: !30)
+!32 = !DILocation(line: 13, column: 17, scope: !33)
+!33 = distinct !DILexicalBlock(scope: !30, file: !6, line: 13, column: 5)
+!34 = !DILocation(line: 13, column: 19, scope: !33)
+!35 = !DILocation(line: 13, column: 5, scope: !30)
+!36 = !DILocation(line: 13, column: 29, scope: !33)
+!37 = !DILabel(scope: !38, name: "L", file: !6, line: 14)
+!38 = distinct !DILexicalBlock(scope: !33, file: !6, line: 13, column: 29)
+!39 = !DILocation(line: 14, column: 1, scope: !38)
+!40 = !DILocation(line: 15, column: 10, scope: !38)
+!41 = !DILocation(line: 16, column: 5, scope: !38)
+!42 = !DILocation(line: 13, column: 25, scope: !33)
+!43 = !DILocation(line: 13, column: 5, scope: !33)
+!44 = distinct !{!44, !35, !45, !46}
+!45 = !DILocation(line: 16, column: 5, scope: !30)
+!46 = !{!"llvm.loop.mustprogress"}
+!47 = !DILocation(line: 18, column: 5, scope: !48)
+!48 = distinct !DILexicalBlock(scope: !49, file: !6, line: 18, column: 5)
+!49 = distinct !DILexicalBlock(scope: !17, file: !6, line: 18, column: 5)
+!50 = !DILocation(line: 18, column: 5, scope: !49)
+!51 = !DILocation(line: 19, column: 5, scope: !17)

From 76b18b3e1cf03fba3ae529243b1ac9f5aa3559d5 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Date: Thu, 1 Aug 2024 22:17:08 +0200
Subject: [PATCH 11/14] Feedback implemented

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
---
 .../dartagnan/program/processing/NormalizeLoops.java | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
index c874a54464..020466c7ad 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
@@ -132,14 +132,14 @@ private void guaranteeSingleEntry(Function function) {
             int counter = 0;
 
             final Label loopBegin = label;
-            final CondJump uniqueBackJump = backJumps.get(0);
+            final CondJump last = backJumps.get(backJumps.size() - 1);
 
             final Register sourceReg = function.newRegister(String.format("__jumpedTo_%s#%s_From", label, labelCounter), types.getArchType());
             final Local initJumpedFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(types.getArchType()));
             function.getEntry().insertAfter(initJumpedFromOutside);
 
             final List<Label> loopBodyLabels = loopBegin.getSuccessor().getSuccessors().stream()
-                    .takeWhile(ev -> ev != uniqueBackJump)
+                    .takeWhile(ev -> ev != last)
                     .filter(Label.class::isInstance).map(Label.class::cast)
                     .toList();
 
@@ -153,18 +153,16 @@ private void guaranteeSingleEntry(Function function) {
 
                     final Expression source = expressions.makeValue(BigInteger.valueOf(counter), types.getArchType());
                     final Local jumpingFrom = EventFactory.newLocal(sourceReg, source);
-                    final CondJump jumpToHeader = EventFactory.newGoto(loopBegin);
 
-                    fromOutside.replaceBy(jumpingFrom);
-                    jumpingFrom.insertAfter(jumpToHeader);
-                    jumpToHeader.updateReferences(Map.of(jumpToHeader.getLabel(), loopBegin));
+                    fromOutside.updateReferences(Map.of(fromOutside.getLabel(), loopBegin));
+                    fromOutside.getPredecessor().insertAfter(jumpingFrom);
 
                     final Label internalLabel = fromOutside.getLabel();
                     final CondJump jumpToInternal = EventFactory.newJump(expressions.makeEQ(sourceReg, source), internalLabel);
                     final Local resetJumpFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(types.getArchType()));
 
                     loopBegin.insertAfter(jumpToInternal);
-                    uniqueBackJump.getPredecessor().insertAfter(resetJumpFromOutside);
+                    last.getPredecessor().insertAfter(resetJumpFromOutside);
                 }
             }
 

From 81dbe60f0bfc0273f46351a5b337e857770c5623 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sat, 3 Aug 2024 13:19:08 +0800
Subject: [PATCH 12/14] Feedback implemented

---
 .../program/processing/NormalizeLoops.java    | 63 +++++++++++--------
 1 file changed, 36 insertions(+), 27 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
index 020466c7ad..6ceba979bf 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
@@ -2,6 +2,7 @@
 
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
+import com.dat3m.dartagnan.expression.type.IntegerType;
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Register;
@@ -118,55 +119,63 @@ private void guaranteeSingleUnconditionalBackjump(Function function) {
     }
 
     private void guaranteeSingleEntry(Function function) {
+        final IntegerType sourceRegType = types.getArchType();
         int labelCounter = 0;
-        for (Label label : function.getEvents(Label.class)) {
 
-            final List<CondJump> backJumps = label.getJumpSet().stream()
-                    .filter(j -> j.getLocalId() > label.getLocalId())
+        for (Label loopBegin : function.getEvents(Label.class)) {
+            final List<CondJump> backJumps = loopBegin.getJumpSet().stream()
+                    .filter(j -> j.getLocalId() > loopBegin.getLocalId())
                     .sorted()
                     .toList();
             if (backJumps.isEmpty()) {
                 continue;
             }
-
             int counter = 0;
 
-            final Label loopBegin = label;
-            final CondJump last = backJumps.get(backJumps.size() - 1);
-
-            final Register sourceReg = function.newRegister(String.format("__jumpedTo_%s#%s_From", label, labelCounter), types.getArchType());
-            final Local initJumpedFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(types.getArchType()));
-            function.getEntry().insertAfter(initJumpedFromOutside);
-
+            final CondJump loopEnd = backJumps.get(backJumps.size() - 1);
             final List<Label> loopBodyLabels = loopBegin.getSuccessor().getSuccessors().stream()
-                    .takeWhile(ev -> ev != last)
+                    .takeWhile(ev -> ev != loopEnd)
                     .filter(Label.class::isInstance).map(Label.class::cast)
                     .toList();
+                    
+            if(loopBodyLabels.stream().noneMatch(l -> hasExternalEntries(loopBegin, l))) {
+                continue;
+            }
 
-            for (Label l : loopBodyLabels) {
-                final List<CondJump> externalEntries = l.getJumpSet().stream()
-                        .filter(j -> j.getLocalId() < loopBegin.getLocalId())
-                        .toList();
+            final Register sourceReg = function.newRegister(String.format("__jumpedTo_%s#%s_From", loopBegin, labelCounter), sourceRegType);
+            final Local initJumpedFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(sourceRegType));
+            function.getEntry().insertAfter(initJumpedFromOutside);
 
-                for (CondJump fromOutside : externalEntries) {
-                    counter++;
+            for (Label target : loopBodyLabels) {
+                final List<CondJump> externalEntries = getExternalEntries(loopBegin, target);
+                if(externalEntries.isEmpty()) {
+                    continue;
+                }
+                counter++;
 
-                    final Expression source = expressions.makeValue(BigInteger.valueOf(counter), types.getArchType());
-                    final Local jumpingFrom = EventFactory.newLocal(sourceReg, source);
+                final Expression source = expressions.makeValue(BigInteger.valueOf(counter), sourceRegType);
+                final Local jumpingFrom = EventFactory.newLocal(sourceReg, source);
+                final CondJump jumpToInternal = EventFactory.newJump(expressions.makeEQ(sourceReg, source), target);
+                loopBegin.insertAfter(jumpToInternal);
 
+                for (CondJump fromOutside : externalEntries) {
                     fromOutside.updateReferences(Map.of(fromOutside.getLabel(), loopBegin));
                     fromOutside.getPredecessor().insertAfter(jumpingFrom);
-
-                    final Label internalLabel = fromOutside.getLabel();
-                    final CondJump jumpToInternal = EventFactory.newJump(expressions.makeEQ(sourceReg, source), internalLabel);
-                    final Local resetJumpFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(types.getArchType()));
-
-                    loopBegin.insertAfter(jumpToInternal);
-                    last.getPredecessor().insertAfter(resetJumpFromOutside);
                 }
+
+                final Local resetJumpFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(sourceRegType));
+                loopEnd.getPredecessor().insertAfter(resetJumpFromOutside);
             }
 
             labelCounter++;
         }
     }
+
+    private boolean hasExternalEntries(Label loopBegin, Label internal) {
+        return internal.getJumpSet().stream().anyMatch(j -> j.getLocalId() < loopBegin.getLocalId());
+    }
+
+    private List<CondJump> getExternalEntries(Label loopBegin, Label internal) {
+        return internal.getJumpSet().stream().filter(j -> j.getLocalId() < loopBegin.getLocalId()).toList();
+    }
 }

From ec9af071a8beff09dd16c6c60101a480940699b6 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Sat, 3 Aug 2024 10:23:46 +0200
Subject: [PATCH 13/14] Fixed issues with NormalizeLoops pass and added error
 reporting for still unsupported cases.

---
 benchmarks/miscellaneous/jumpIntoLoop.c       |   3 +-
 .../program/processing/NormalizeLoops.java    |  94 ++++---
 .../program/processing/ProcessingManager.java |   2 +-
 .../resources/miscellaneous/jumpIntoLoop.ll   | 252 ++++++++++--------
 4 files changed, 198 insertions(+), 153 deletions(-)

diff --git a/benchmarks/miscellaneous/jumpIntoLoop.c b/benchmarks/miscellaneous/jumpIntoLoop.c
index 7b42934bae..8434e68318 100644
--- a/benchmarks/miscellaneous/jumpIntoLoop.c
+++ b/benchmarks/miscellaneous/jumpIntoLoop.c
@@ -10,11 +10,12 @@ int main()
     int jumpIntoLoop = __VERIFIER_nondet_bool();
     if (jumpIntoLoop) goto L;
 
+    __VERIFIER_loop_bound(6);
     for (i = 1; i < 5; i++) {
 L:
         x++;
     }
 
-    assert((!jumpIntoLoop || x == 5) && (jumpIntoLoop || x == 4));
+    assert ((jumpIntoLoop && x == 5) || (!jumpIntoLoop && x == 4));
     return 0;
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
index 6ceba979bf..0922e5013b 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NormalizeLoops.java
@@ -6,11 +6,14 @@
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis;
+import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.core.CondJump;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.core.Local;
-import java.math.BigInteger;
+
+import java.util.ArrayList;
 import java.util.List;
 import java.util.Map;
 
@@ -33,17 +36,18 @@
     it transforms it to
 
         entry:
-        __jumpedTo_L_From <- 0
+        __loopEntryPoint_L <- 0
         ...
-        __jumpedTo_L_From <- 1
+        __loopEntryPoint_L <- 1
         goto L
         ...
         L:
-        if __jumpedTo_L_From == 1 goto C
+        __forwardTo_L <- __loopEntryPoint_L
+        __loopEntryPoint_L <- 0
+        if __forwardTo_L == 1 goto C
         ...
         C:
         ...
-        __jumpedTo_L_From <- 0
         goto L
 
     (2) Given a loop of the form
@@ -119,9 +123,7 @@ private void guaranteeSingleUnconditionalBackjump(Function function) {
     }
 
     private void guaranteeSingleEntry(Function function) {
-        final IntegerType sourceRegType = types.getArchType();
-        int labelCounter = 0;
-
+        int loopCounter = 0;
         for (Label loopBegin : function.getEvents(Label.class)) {
             final List<CondJump> backJumps = loopBegin.getJumpSet().stream()
                     .filter(j -> j.getLocalId() > loopBegin.getLocalId())
@@ -130,52 +132,72 @@ private void guaranteeSingleEntry(Function function) {
             if (backJumps.isEmpty()) {
                 continue;
             }
-            int counter = 0;
 
             final CondJump loopEnd = backJumps.get(backJumps.size() - 1);
-            final List<Label> loopBodyLabels = loopBegin.getSuccessor().getSuccessors().stream()
+            final List<Label> loopIrregularEntryPoints = loopBegin.getSuccessor().getSuccessors().stream()
                     .takeWhile(ev -> ev != loopEnd)
                     .filter(Label.class::isInstance).map(Label.class::cast)
+                    .filter(l -> isEntryPoint(loopBegin, loopEnd, l))
                     .toList();
-                    
-            if(loopBodyLabels.stream().noneMatch(l -> hasExternalEntries(loopBegin, l))) {
+
+            if (loopIrregularEntryPoints.isEmpty()) {
                 continue;
             }
 
-            final Register sourceReg = function.newRegister(String.format("__jumpedTo_%s#%s_From", loopBegin, labelCounter), sourceRegType);
-            final Local initJumpedFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(sourceRegType));
-            function.getEntry().insertAfter(initJumpedFromOutside);
+            final IntegerType entryPointType = types.getByteType();
+            final Register entryPointReg = function.newRegister(String.format("__loopEntryPoint_%s#%s", loopBegin, loopCounter), entryPointType);
+            final Register forwarderReg = function.newRegister(String.format("__forwardTo_%s#%s", loopBegin, loopCounter), entryPointType);
+            final Local initEntryPointReg = EventFactory.newLocal(entryPointReg, expressions.makeZero(entryPointType));
+            final Local assignForwarderReg = EventFactory.newLocal(forwarderReg, entryPointReg);
+            final Local resetEntryPointReg = EventFactory.newLocal(entryPointReg, expressions.makeZero(entryPointType));
+            function.getEntry().insertAfter(initEntryPointReg);
 
-            for (Label target : loopBodyLabels) {
-                final List<CondJump> externalEntries = getExternalEntries(loopBegin, target);
-                if(externalEntries.isEmpty()) {
-                    continue;
-                }
-                counter++;
-
-                final Expression source = expressions.makeValue(BigInteger.valueOf(counter), sourceRegType);
-                final Local jumpingFrom = EventFactory.newLocal(sourceReg, source);
-                final CondJump jumpToInternal = EventFactory.newJump(expressions.makeEQ(sourceReg, source), target);
-                loopBegin.insertAfter(jumpToInternal);
+            final List<Event> forwardingInstrumentation = new ArrayList<>();
+            forwardingInstrumentation.add(assignForwarderReg);
+            forwardingInstrumentation.add(resetEntryPointReg);
 
-                for (CondJump fromOutside : externalEntries) {
-                    fromOutside.updateReferences(Map.of(fromOutside.getLabel(), loopBegin));
-                    fromOutside.getPredecessor().insertAfter(jumpingFrom);
+            int counter = 0;
+            for (Label entryPoint : loopIrregularEntryPoints) {
+                final List<CondJump> enteringJumps = getEnteringJumps(loopBegin,loopEnd, entryPoint);
+                assert (!enteringJumps.isEmpty());
+
+                final Expression entryPointValue = expressions.makeValue(++counter, entryPointType);
+                for (CondJump enteringJump : enteringJumps) {
+                    if (enteringJump.getLocalId() > loopEnd.getLocalId()) {
+                        // TODO: This case is rare as it would imply we have two (or more) overlapping loops.
+                        //  In this case, we should first merge the overlapping loops into one large loop.
+                        final String error = String.format("Cannot normalize loop with loop-entering backjump (overlapping loops?): %d:%s \t %s",
+                                enteringJump.getLocalId(), enteringJump, SyntacticContextAnalysis.getSourceLocationString(enteringJump));
+                        throw new UnsupportedOperationException(error);
+                    }
+                    if (!enteringJump.isGoto()) {
+                        // TODO: We should support this case, but the current implementation is wrong
+                        //  because if an instrumented jump is not taken, it still updates the entry point reg
+                        //  which will never get reset: we would end up accidentally forwarding a regular loop entry.
+                        final String error = String.format("Cannot normalize loop with conditional loop-entering jump: %d:%s \t %s",
+                                enteringJump.getLocalId(), enteringJump, SyntacticContextAnalysis.getSourceLocationString(enteringJump));
+                        throw new UnsupportedOperationException(error);
+                    }
+                    enteringJump.getPredecessor().insertAfter(EventFactory.newLocal(entryPointReg, entryPointValue));
+                    enteringJump.updateReferences(Map.of(entryPoint, loopBegin));
                 }
 
-                final Local resetJumpFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(sourceRegType));
-                loopEnd.getPredecessor().insertAfter(resetJumpFromOutside);
+                final CondJump forwardingJump = EventFactory.newJump(expressions.makeEQ(forwarderReg, entryPointValue), entryPoint);
+                forwardingInstrumentation.add(forwardingJump);
             }
 
-            labelCounter++;
+            loopBegin.insertAfter(forwardingInstrumentation);
+            loopCounter++;
         }
     }
 
-    private boolean hasExternalEntries(Label loopBegin, Label internal) {
-        return internal.getJumpSet().stream().anyMatch(j -> j.getLocalId() < loopBegin.getLocalId());
+    private boolean isEntryPoint(Event beginning, Event end, Label internal) {
+        return !getEnteringJumps(beginning, end, internal).isEmpty();
     }
 
-    private List<CondJump> getExternalEntries(Label loopBegin, Label internal) {
-        return internal.getJumpSet().stream().filter(j -> j.getLocalId() < loopBegin.getLocalId()).toList();
+    private List<CondJump> getEnteringJumps(Event beginning, Event end, Label internal) {
+        return internal.getJumpSet().stream()
+                .filter(j -> j.getLocalId() < beginning.getLocalId() || end.getLocalId() < j.getLocalId())
+                .toList();
     }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
index a509702fad..c3d986514f 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
@@ -98,9 +98,9 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
                                 Simplifier.fromConfig(config)
                         ), Target.FUNCTIONS, true
                 ),
+                ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.FUNCTIONS, true),
                 RegisterDecomposition.newInstance(),
                 RemoveDeadFunctions.newInstance(),
-                ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.FUNCTIONS, true),
                 printAfterSimplification ? DebugPrint.withHeader("After simplification", Printer.Mode.ALL) : null,
                 Compilation.fromConfig(config), // We keep compilation global for now
                 LoopFormVerification.fromConfig(config),
diff --git a/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll b/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll
index cff00c2895..38377683ef 100644
--- a/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll
+++ b/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll
@@ -1,158 +1,180 @@
-; ModuleID = '/home/ponce/git/Dat3M/output/jumpIntoLoop.ll'
-source_filename = "/home/ponce/git/Dat3M/benchmarks/miscellaneous/jumpIntoLoop.c"
-target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
-target triple = "x86_64-pc-linux-gnu"
-
-@x = dso_local global i32 0, align 4, !dbg !0
-@.str = private unnamed_addr constant [54 x i8] c"(!jumpIntoLoop || x == 5) && (jumpIntoLoop || x == 4)\00", align 1
-@.str.1 = private unnamed_addr constant [62 x i8] c"/home/ponce/git/Dat3M/benchmarks/miscellaneous/jumpIntoLoop.c\00", align 1
-@__PRETTY_FUNCTION__.main = private unnamed_addr constant [11 x i8] c"int main()\00", align 1
-
-; Function Attrs: noinline nounwind uwtable
-define dso_local i32 @main() #0 !dbg !17 {
+; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/jumpIntoLoop.c'
+source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/jumpIntoLoop.c"
+target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
+target triple = "arm64-apple-macosx14.0.0"
+
+@x = global i32 0, align 4, !dbg !0
+@__func__.main = private unnamed_addr constant [5 x i8] c"main\00", align 1
+@.str = private unnamed_addr constant [15 x i8] c"jumpIntoLoop.c\00", align 1
+@.str.1 = private unnamed_addr constant [54 x i8] c"(jumpIntoLoop && x == 5) || (!jumpIntoLoop && x == 4)\00", align 1
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i32 @main() #0 !dbg !21 {
   %1 = alloca i32, align 4
   %2 = alloca i32, align 4
   %3 = alloca i32, align 4
   store i32 0, i32* %1, align 4
-  call void @llvm.dbg.declare(metadata i32* %2, metadata !20, metadata !DIExpression()), !dbg !21
-  store i32 0, i32* %2, align 4, !dbg !21
-  call void @llvm.dbg.declare(metadata i32* %3, metadata !22, metadata !DIExpression()), !dbg !23
-  %4 = call zeroext i1 @__VERIFIER_nondet_bool(), !dbg !24
-  %5 = zext i1 %4 to i32, !dbg !24
-  store i32 %5, i32* %3, align 4, !dbg !23
-  %6 = load i32, i32* %3, align 4, !dbg !25
-  %7 = icmp ne i32 %6, 0, !dbg !25
-  br i1 %7, label %8, label %9, !dbg !27
+  call void @llvm.dbg.declare(metadata i32* %2, metadata !25, metadata !DIExpression()), !dbg !26
+  store i32 0, i32* %2, align 4, !dbg !26
+  call void @llvm.dbg.declare(metadata i32* %3, metadata !27, metadata !DIExpression()), !dbg !28
+  %4 = call zeroext i1 @__VERIFIER_nondet_bool(), !dbg !29
+  %5 = zext i1 %4 to i32, !dbg !29
+  store i32 %5, i32* %3, align 4, !dbg !28
+  %6 = load i32, i32* %3, align 4, !dbg !30
+  %7 = icmp ne i32 %6, 0, !dbg !30
+  br i1 %7, label %8, label %9, !dbg !32
 
 8:                                                ; preds = %0
-  br label %14, !dbg !28
+  br label %14, !dbg !33
 
 9:                                                ; preds = %0
-  store i32 1, i32* %2, align 4, !dbg !29
-  br label %10, !dbg !31
+  call void @__VERIFIER_loop_bound(i32 noundef 6), !dbg !34
+  store i32 1, i32* %2, align 4, !dbg !35
+  br label %10, !dbg !37
 
 10:                                               ; preds = %17, %9
-  %11 = load i32, i32* %2, align 4, !dbg !32
-  %12 = icmp slt i32 %11, 5, !dbg !34
-  br i1 %12, label %13, label %20, !dbg !35
+  %11 = load i32, i32* %2, align 4, !dbg !38
+  %12 = icmp slt i32 %11, 5, !dbg !40
+  br i1 %12, label %13, label %20, !dbg !41
 
 13:                                               ; preds = %10
-  br label %14, !dbg !36
+  br label %14, !dbg !42
 
 14:                                               ; preds = %13, %8
-  call void @llvm.dbg.label(metadata !37), !dbg !39
-  %15 = load volatile i32, i32* @x, align 4, !dbg !40
-  %16 = add nsw i32 %15, 1, !dbg !40
-  store volatile i32 %16, i32* @x, align 4, !dbg !40
-  br label %17, !dbg !41
+  call void @llvm.dbg.label(metadata !43), !dbg !45
+  %15 = load volatile i32, i32* @x, align 4, !dbg !46
+  %16 = add nsw i32 %15, 1, !dbg !46
+  store volatile i32 %16, i32* @x, align 4, !dbg !46
+  br label %17, !dbg !47
 
 17:                                               ; preds = %14
-  %18 = load i32, i32* %2, align 4, !dbg !42
-  %19 = add nsw i32 %18, 1, !dbg !42
-  store i32 %19, i32* %2, align 4, !dbg !42
-  br label %10, !dbg !43, !llvm.loop !44
+  %18 = load i32, i32* %2, align 4, !dbg !48
+  %19 = add nsw i32 %18, 1, !dbg !48
+  store i32 %19, i32* %2, align 4, !dbg !48
+  br label %10, !dbg !49, !llvm.loop !50
 
 20:                                               ; preds = %10
-  %21 = load i32, i32* %3, align 4, !dbg !47
-  %22 = icmp ne i32 %21, 0, !dbg !47
-  br i1 %22, label %23, label %26, !dbg !47
+  %21 = load i32, i32* %3, align 4, !dbg !53
+  %22 = icmp ne i32 %21, 0, !dbg !53
+  br i1 %22, label %23, label %26, !dbg !53
 
 23:                                               ; preds = %20
-  %24 = load volatile i32, i32* @x, align 4, !dbg !47
-  %25 = icmp eq i32 %24, 5, !dbg !47
-  br i1 %25, label %26, label %33, !dbg !47
+  %24 = load volatile i32, i32* @x, align 4, !dbg !53
+  %25 = icmp eq i32 %24, 5, !dbg !53
+  br i1 %25, label %34, label %26, !dbg !53
 
 26:                                               ; preds = %23, %20
-  %27 = load i32, i32* %3, align 4, !dbg !47
-  %28 = icmp ne i32 %27, 0, !dbg !47
-  br i1 %28, label %32, label %29, !dbg !47
+  %27 = load i32, i32* %3, align 4, !dbg !53
+  %28 = icmp ne i32 %27, 0, !dbg !53
+  br i1 %28, label %32, label %29, !dbg !53
 
 29:                                               ; preds = %26
-  %30 = load volatile i32, i32* @x, align 4, !dbg !47
-  %31 = icmp eq i32 %30, 4, !dbg !47
-  br i1 %31, label %32, label %33, !dbg !50
+  %30 = load volatile i32, i32* @x, align 4, !dbg !53
+  %31 = icmp eq i32 %30, 4, !dbg !53
+  br label %32
 
 32:                                               ; preds = %29, %26
-  br label %34, !dbg !50
+  %33 = phi i1 [ false, %26 ], [ %31, %29 ], !dbg !54
+  br label %34, !dbg !53
 
-33:                                               ; preds = %29, %23
-  call void @__assert_fail(i8* getelementptr inbounds ([54 x i8], [54 x i8]* @.str, i64 0, i64 0), i8* getelementptr inbounds ([62 x i8], [62 x i8]* @.str.1, i64 0, i64 0), i32 18, i8* getelementptr inbounds ([11 x i8], [11 x i8]* @__PRETTY_FUNCTION__.main, i64 0, i64 0)) #4, !dbg !47
-  unreachable, !dbg !47
+34:                                               ; preds = %32, %23
+  %35 = phi i1 [ true, %23 ], [ %33, %32 ]
+  %36 = xor i1 %35, true, !dbg !53
+  %37 = zext i1 %36 to i32, !dbg !53
+  %38 = sext i32 %37 to i64, !dbg !53
+  %39 = icmp ne i64 %38, 0, !dbg !53
+  br i1 %39, label %40, label %42, !dbg !53
 
-34:                                               ; preds = %32
-  ret i32 0, !dbg !51
+40:                                               ; preds = %34
+  call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([15 x i8], [15 x i8]* @.str, i64 0, i64 0), i32 noundef 19, i8* noundef getelementptr inbounds ([54 x i8], [54 x i8]* @.str.1, i64 0, i64 0)) #4, !dbg !53
+  unreachable, !dbg !53
+
+41:                                               ; No predecessors!
+  br label %43, !dbg !53
+
+42:                                               ; preds = %34
+  br label %43, !dbg !53
+
+43:                                               ; preds = %42, %41
+  ret i32 0, !dbg !55
 }
 
 ; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
 declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
 
-declare dso_local zeroext i1 @__VERIFIER_nondet_bool() #2
+declare zeroext i1 @__VERIFIER_nondet_bool() #2
+
+declare void @__VERIFIER_loop_bound(i32 noundef) #2
 
 ; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
 declare void @llvm.dbg.label(metadata) #1
 
-; Function Attrs: noreturn nounwind
-declare dso_local void @__assert_fail(i8*, i8*, i32, i8*) #3
+; Function Attrs: cold noreturn
+declare void @__assert_rtn(i8* noundef, i8* noundef, i32 noundef, i8* noundef) #3
 
-attributes #0 = { noinline nounwind uwtable "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" }
+attributes #0 = { noinline nounwind ssp uwtable "frame-pointer"="non-leaf" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
 attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
-attributes #2 = { "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" }
-attributes #3 = { noreturn nounwind "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" }
-attributes #4 = { noreturn nounwind }
+attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+attributes #3 = { cold noreturn "disable-tail-calls"="true" "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+attributes #4 = { cold noreturn }
 
 !llvm.dbg.cu = !{!2}
-!llvm.module.flags = !{!13, !14, !15}
-!llvm.ident = !{!16}
+!llvm.module.flags = !{!10, !11, !12, !13, !14, !15, !16, !17, !18, !19}
+!llvm.ident = !{!20}
 
 !0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
-!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !6, line: 5, type: !7, isLocal: false, isDefinition: true)
-!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Ubuntu clang version 12.0.0-3ubuntu1~20.04.5", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, enums: !4, globals: !5, splitDebugInlining: false, nameTableKind: None)
-!3 = !DIFile(filename: "/home/ponce/git/Dat3M/benchmarks/miscellaneous/jumpIntoLoop.c", directory: "/home/ponce/git/Dat3M")
-!4 = !{}
-!5 = !{!0}
-!6 = !DIFile(filename: "benchmarks/miscellaneous/jumpIntoLoop.c", directory: "/home/ponce/git/Dat3M")
-!7 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !8)
-!8 = !DIDerivedType(tag: DW_TAG_typedef, name: "int32_t", file: !9, line: 26, baseType: !10)
-!9 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/stdint-intn.h", directory: "")
-!10 = !DIDerivedType(tag: DW_TAG_typedef, name: "__int32_t", file: !11, line: 41, baseType: !12)
-!11 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/types.h", directory: "")
-!12 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
-!13 = !{i32 7, !"Dwarf Version", i32 4}
-!14 = !{i32 2, !"Debug Info Version", i32 3}
-!15 = !{i32 1, !"wchar_size", i32 4}
-!16 = !{!"Ubuntu clang version 12.0.0-3ubuntu1~20.04.5"}
-!17 = distinct !DISubprogram(name: "main", scope: !6, file: !6, line: 7, type: !18, scopeLine: 8, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !4)
-!18 = !DISubroutineType(types: !19)
-!19 = !{!12}
-!20 = !DILocalVariable(name: "i", scope: !17, file: !6, line: 9, type: !12)
-!21 = !DILocation(line: 9, column: 9, scope: !17)
-!22 = !DILocalVariable(name: "jumpIntoLoop", scope: !17, file: !6, line: 10, type: !12)
-!23 = !DILocation(line: 10, column: 9, scope: !17)
-!24 = !DILocation(line: 10, column: 24, scope: !17)
-!25 = !DILocation(line: 11, column: 9, scope: !26)
-!26 = distinct !DILexicalBlock(scope: !17, file: !6, line: 11, column: 9)
-!27 = !DILocation(line: 11, column: 9, scope: !17)
-!28 = !DILocation(line: 11, column: 23, scope: !26)
-!29 = !DILocation(line: 13, column: 12, scope: !30)
-!30 = distinct !DILexicalBlock(scope: !17, file: !6, line: 13, column: 5)
-!31 = !DILocation(line: 13, column: 10, scope: !30)
-!32 = !DILocation(line: 13, column: 17, scope: !33)
-!33 = distinct !DILexicalBlock(scope: !30, file: !6, line: 13, column: 5)
-!34 = !DILocation(line: 13, column: 19, scope: !33)
-!35 = !DILocation(line: 13, column: 5, scope: !30)
-!36 = !DILocation(line: 13, column: 29, scope: !33)
-!37 = !DILabel(scope: !38, name: "L", file: !6, line: 14)
-!38 = distinct !DILexicalBlock(scope: !33, file: !6, line: 13, column: 29)
-!39 = !DILocation(line: 14, column: 1, scope: !38)
-!40 = !DILocation(line: 15, column: 10, scope: !38)
-!41 = !DILocation(line: 16, column: 5, scope: !38)
-!42 = !DILocation(line: 13, column: 25, scope: !33)
-!43 = !DILocation(line: 13, column: 5, scope: !33)
-!44 = distinct !{!44, !35, !45, !46}
-!45 = !DILocation(line: 16, column: 5, scope: !30)
-!46 = !{!"llvm.loop.mustprogress"}
-!47 = !DILocation(line: 18, column: 5, scope: !48)
-!48 = distinct !DILexicalBlock(scope: !49, file: !6, line: 18, column: 5)
-!49 = distinct !DILexicalBlock(scope: !17, file: !6, line: 18, column: 5)
-!50 = !DILocation(line: 18, column: 5, scope: !49)
-!51 = !DILocation(line: 19, column: 5, scope: !17)
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !5, line: 5, type: !6, isLocal: false, isDefinition: true)
+!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Homebrew clang version 14.0.6", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, globals: !4, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk")
+!3 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/jumpIntoLoop.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!4 = !{!0}
+!5 = !DIFile(filename: "benchmarks/miscellaneous/jumpIntoLoop.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!6 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !7)
+!7 = !DIDerivedType(tag: DW_TAG_typedef, name: "int32_t", file: !8, line: 30, baseType: !9)
+!8 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_types/_int32_t.h", directory: "")
+!9 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!10 = !{i32 7, !"Dwarf Version", i32 4}
+!11 = !{i32 2, !"Debug Info Version", i32 3}
+!12 = !{i32 1, !"wchar_size", i32 4}
+!13 = !{i32 1, !"branch-target-enforcement", i32 0}
+!14 = !{i32 1, !"sign-return-address", i32 0}
+!15 = !{i32 1, !"sign-return-address-all", i32 0}
+!16 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
+!17 = !{i32 7, !"PIC Level", i32 2}
+!18 = !{i32 7, !"uwtable", i32 1}
+!19 = !{i32 7, !"frame-pointer", i32 1}
+!20 = !{!"Homebrew clang version 14.0.6"}
+!21 = distinct !DISubprogram(name: "main", scope: !5, file: !5, line: 7, type: !22, scopeLine: 8, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !24)
+!22 = !DISubroutineType(types: !23)
+!23 = !{!9}
+!24 = !{}
+!25 = !DILocalVariable(name: "i", scope: !21, file: !5, line: 9, type: !9)
+!26 = !DILocation(line: 9, column: 9, scope: !21)
+!27 = !DILocalVariable(name: "jumpIntoLoop", scope: !21, file: !5, line: 10, type: !9)
+!28 = !DILocation(line: 10, column: 9, scope: !21)
+!29 = !DILocation(line: 10, column: 24, scope: !21)
+!30 = !DILocation(line: 11, column: 9, scope: !31)
+!31 = distinct !DILexicalBlock(scope: !21, file: !5, line: 11, column: 9)
+!32 = !DILocation(line: 11, column: 9, scope: !21)
+!33 = !DILocation(line: 11, column: 23, scope: !31)
+!34 = !DILocation(line: 13, column: 5, scope: !21)
+!35 = !DILocation(line: 14, column: 12, scope: !36)
+!36 = distinct !DILexicalBlock(scope: !21, file: !5, line: 14, column: 5)
+!37 = !DILocation(line: 14, column: 10, scope: !36)
+!38 = !DILocation(line: 14, column: 17, scope: !39)
+!39 = distinct !DILexicalBlock(scope: !36, file: !5, line: 14, column: 5)
+!40 = !DILocation(line: 14, column: 19, scope: !39)
+!41 = !DILocation(line: 14, column: 5, scope: !36)
+!42 = !DILocation(line: 14, column: 29, scope: !39)
+!43 = !DILabel(scope: !44, name: "L", file: !5, line: 15)
+!44 = distinct !DILexicalBlock(scope: !39, file: !5, line: 14, column: 29)
+!45 = !DILocation(line: 15, column: 1, scope: !44)
+!46 = !DILocation(line: 16, column: 10, scope: !44)
+!47 = !DILocation(line: 17, column: 5, scope: !44)
+!48 = !DILocation(line: 14, column: 25, scope: !39)
+!49 = !DILocation(line: 14, column: 5, scope: !39)
+!50 = distinct !{!50, !41, !51, !52}
+!51 = !DILocation(line: 17, column: 5, scope: !36)
+!52 = !{!"llvm.loop.mustprogress"}
+!53 = !DILocation(line: 19, column: 5, scope: !21)
+!54 = !DILocation(line: 0, scope: !21)
+!55 = !DILocation(line: 20, column: 5, scope: !21)

From c9a2b5f4b998c2d2df2ac66ba659502d5e9efa35 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sun, 4 Aug 2024 00:57:23 +0800
Subject: [PATCH 14/14] Add unit test for unsupported case

---
 .../unsupported-loop-normalization.c          |  58 +++++
 .../dartagnan/exceptions/ExceptionsTest.java  |  11 +
 .../unsupported-loop-normalization.ll         | 235 ++++++++++++++++++
 3 files changed, 304 insertions(+)
 create mode 100644 benchmarks/miscellaneous/unsupported-loop-normalization.c
 create mode 100644 dartagnan/src/test/resources/exceptions/unsupported-loop-normalization.ll

diff --git a/benchmarks/miscellaneous/unsupported-loop-normalization.c b/benchmarks/miscellaneous/unsupported-loop-normalization.c
new file mode 100644
index 0000000000..c512ba2283
--- /dev/null
+++ b/benchmarks/miscellaneous/unsupported-loop-normalization.c
@@ -0,0 +1,58 @@
+#include <assert.h>
+#include <dat3m.h>
+
+int main()
+{
+	unsigned int x = __VERIFIER_nondet_uint();
+A:
+	if (x >= 1) {
+		x = 4;
+		goto B;
+	} else {
+		goto C;
+	}
+B:
+	// 3, 4, 5, 6
+	if (x > 3) {
+		goto D;
+	} else {
+		goto E;
+	}
+D:
+	// 3, 4, 5, 6
+	x++;
+
+	if (x > 5) {
+		goto Halt;
+	} else {
+		goto E;
+	}
+E:
+	// 3, 4, 5
+	if (x < 4) {
+		goto D;
+	} else {
+		goto F;
+	}
+F:
+	// 4, 5
+	if (x < 3) {
+		goto C;
+	} else {
+		goto G;
+	}
+G:
+	// 0, 1, 2, 4, 5
+	x++;
+	goto C;
+C:
+	// 0, 1, 2, 3, 5, 6
+	if (x > 2) {
+		goto B;
+	} else {
+		goto G;
+	}
+Halt:
+	// 6, 7
+	assert(x == 6);
+}
\ No newline at end of file
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/ExceptionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/ExceptionsTest.java
index 93dfbcc97f..0df8ef6469 100644
--- a/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/ExceptionsTest.java
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/ExceptionsTest.java
@@ -1,17 +1,21 @@
 package com.dat3m.dartagnan.exceptions;
 
 import com.dat3m.dartagnan.exception.MalformedProgramException;
+import java.lang.UnsupportedOperationException;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.parsers.program.ProgramParser;
 import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder;
+import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Program.SourceLanguage;
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.analysis.BranchEquivalence;
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.core.Skip;
+import com.dat3m.dartagnan.program.processing.NormalizeLoops;
+
 import org.junit.Test;
 import org.sosy_lab.common.configuration.Configuration;
 
@@ -83,4 +87,11 @@ public void LocationNotInitialized() throws Exception {
     public void RegisterNotInitialized() throws Exception {
         new ProgramParser().parse(new File(getTestResourcePath("exceptions/RegisterNotInitialized.litmus")));
     }
+
+    @Test(expected = UnsupportedOperationException.class)
+    public void UnsupportedLoopNormalization() throws Exception {
+        Program p = new ProgramParser().parse(new File(getTestResourcePath("exceptions/unsupported-loop-normalization.ll")));
+        Function main = p.getFunctionByName("main").get();
+        NormalizeLoops.newInstance().run(main);
+    }
 }
\ No newline at end of file
diff --git a/dartagnan/src/test/resources/exceptions/unsupported-loop-normalization.ll b/dartagnan/src/test/resources/exceptions/unsupported-loop-normalization.ll
new file mode 100644
index 0000000000..880ea38966
--- /dev/null
+++ b/dartagnan/src/test/resources/exceptions/unsupported-loop-normalization.ll
@@ -0,0 +1,235 @@
+; ModuleID = '/home/drc/git/Dat3M/output/unsupported-loop-normalization.ll'
+source_filename = "/home/drc/git/Dat3M/benchmarks/miscellaneous/unsupported-loop-normalization.c"
+target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-pc-linux-gnu"
+
+@.str = private unnamed_addr constant [7 x i8] c"x == 6\00", align 1
+@.str.1 = private unnamed_addr constant [78 x i8] c"/home/drc/git/Dat3M/benchmarks/miscellaneous/unsupported-loop-normalization.c\00", align 1
+@__PRETTY_FUNCTION__.main = private unnamed_addr constant [11 x i8] c"int main()\00", align 1
+
+; Function Attrs: noinline nounwind uwtable
+define dso_local i32 @main() #0 !dbg !10 {
+  %1 = alloca i32, align 4
+  %2 = alloca i32, align 4
+  store i32 0, i32* %1, align 4
+  call void @llvm.dbg.declare(metadata i32* %2, metadata !16, metadata !DIExpression()), !dbg !18
+  %3 = call i32 @__VERIFIER_nondet_uint(), !dbg !19
+  store i32 %3, i32* %2, align 4, !dbg !18
+  br label %4, !dbg !20
+
+4:                                                ; preds = %0
+  call void @llvm.dbg.label(metadata !21), !dbg !22
+  %5 = load i32, i32* %2, align 4, !dbg !23
+  %6 = icmp uge i32 %5, 1, !dbg !25
+  br i1 %6, label %7, label %8, !dbg !26
+
+7:                                                ; preds = %4
+  store i32 4, i32* %2, align 4, !dbg !27
+  br label %9, !dbg !29
+
+8:                                                ; preds = %4
+  br label %34, !dbg !30
+
+9:                                                ; preds = %37, %7
+  call void @llvm.dbg.label(metadata !32), !dbg !33
+  %10 = load i32, i32* %2, align 4, !dbg !34
+  %11 = icmp ugt i32 %10, 3, !dbg !36
+  br i1 %11, label %12, label %13, !dbg !37
+
+12:                                               ; preds = %9
+  br label %14, !dbg !38
+
+13:                                               ; preds = %9
+  br label %21, !dbg !40
+
+14:                                               ; preds = %24, %12
+  call void @llvm.dbg.label(metadata !42), !dbg !43
+  %15 = load i32, i32* %2, align 4, !dbg !44
+  %16 = add i32 %15, 1, !dbg !44
+  store i32 %16, i32* %2, align 4, !dbg !44
+  %17 = load i32, i32* %2, align 4, !dbg !45
+  %18 = icmp ugt i32 %17, 5, !dbg !47
+  br i1 %18, label %19, label %20, !dbg !48
+
+19:                                               ; preds = %14
+  br label %39, !dbg !49
+
+20:                                               ; preds = %14
+  br label %21, !dbg !51
+
+21:                                               ; preds = %20, %13
+  call void @llvm.dbg.label(metadata !53), !dbg !54
+  %22 = load i32, i32* %2, align 4, !dbg !55
+  %23 = icmp ult i32 %22, 4, !dbg !57
+  br i1 %23, label %24, label %25, !dbg !58
+
+24:                                               ; preds = %21
+  br label %14, !dbg !59
+
+25:                                               ; preds = %21
+  br label %26, !dbg !61
+
+26:                                               ; preds = %25
+  call void @llvm.dbg.label(metadata !63), !dbg !64
+  %27 = load i32, i32* %2, align 4, !dbg !65
+  %28 = icmp ult i32 %27, 3, !dbg !67
+  br i1 %28, label %29, label %30, !dbg !68
+
+29:                                               ; preds = %26
+  br label %34, !dbg !69
+
+30:                                               ; preds = %26
+  br label %31, !dbg !71
+
+31:                                               ; preds = %38, %30
+  call void @llvm.dbg.label(metadata !73), !dbg !74
+  %32 = load i32, i32* %2, align 4, !dbg !75
+  %33 = add i32 %32, 1, !dbg !75
+  store i32 %33, i32* %2, align 4, !dbg !75
+  br label %34, !dbg !76
+
+34:                                               ; preds = %31, %29, %8
+  call void @llvm.dbg.label(metadata !77), !dbg !78
+  %35 = load i32, i32* %2, align 4, !dbg !79
+  %36 = icmp ugt i32 %35, 2, !dbg !81
+  br i1 %36, label %37, label %38, !dbg !82
+
+37:                                               ; preds = %34
+  br label %9, !dbg !83
+
+38:                                               ; preds = %34
+  br label %31, !dbg !85
+
+39:                                               ; preds = %19
+  call void @llvm.dbg.label(metadata !87), !dbg !88
+  %40 = load i32, i32* %2, align 4, !dbg !89
+  %41 = icmp eq i32 %40, 6, !dbg !89
+  br i1 %41, label %42, label %43, !dbg !92
+
+42:                                               ; preds = %39
+  br label %44, !dbg !92
+
+43:                                               ; preds = %39
+  call void @__assert_fail(i8* noundef getelementptr inbounds ([7 x i8], [7 x i8]* @.str, i64 0, i64 0), i8* noundef getelementptr inbounds ([78 x i8], [78 x i8]* @.str.1, i64 0, i64 0), i32 noundef 57, i8* noundef getelementptr inbounds ([11 x i8], [11 x i8]* @__PRETTY_FUNCTION__.main, i64 0, i64 0)) #4, !dbg !89
+  unreachable, !dbg !89
+
+44:                                               ; preds = %42
+  %45 = load i32, i32* %1, align 4, !dbg !93
+  ret i32 %45, !dbg !93
+}
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
+
+declare i32 @__VERIFIER_nondet_uint() #2
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.label(metadata) #1
+
+; Function Attrs: noreturn nounwind
+declare void @__assert_fail(i8* noundef, i8* noundef, i32 noundef, i8* noundef) #3
+
+attributes #0 = { noinline nounwind uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
+attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
+attributes #2 = { "frame-pointer"="all" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
+attributes #3 = { noreturn nounwind "frame-pointer"="all" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
+attributes #4 = { noreturn nounwind }
+
+!llvm.dbg.cu = !{!0}
+!llvm.module.flags = !{!2, !3, !4, !5, !6, !7, !8}
+!llvm.ident = !{!9}
+
+!0 = distinct !DICompileUnit(language: DW_LANG_C99, file: !1, producer: "Ubuntu clang version 14.0.0-1ubuntu1.1", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, splitDebugInlining: false, nameTableKind: None)
+!1 = !DIFile(filename: "/home/drc/git/Dat3M/benchmarks/miscellaneous/unsupported-loop-normalization.c", directory: "/home/drc/git/Dat3M", checksumkind: CSK_MD5, checksum: "9e7cb84fbc836969402dbe7a76c7dd09")
+!2 = !{i32 7, !"Dwarf Version", i32 5}
+!3 = !{i32 2, !"Debug Info Version", i32 3}
+!4 = !{i32 1, !"wchar_size", i32 4}
+!5 = !{i32 7, !"PIC Level", i32 2}
+!6 = !{i32 7, !"PIE Level", i32 2}
+!7 = !{i32 7, !"uwtable", i32 1}
+!8 = !{i32 7, !"frame-pointer", i32 2}
+!9 = !{!"Ubuntu clang version 14.0.0-1ubuntu1.1"}
+!10 = distinct !DISubprogram(name: "main", scope: !11, file: !11, line: 4, type: !12, scopeLine: 5, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !15)
+!11 = !DIFile(filename: "benchmarks/miscellaneous/unsupported-loop-normalization.c", directory: "/home/drc/git/Dat3M", checksumkind: CSK_MD5, checksum: "9e7cb84fbc836969402dbe7a76c7dd09")
+!12 = !DISubroutineType(types: !13)
+!13 = !{!14}
+!14 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!15 = !{}
+!16 = !DILocalVariable(name: "x", scope: !10, file: !11, line: 6, type: !17)
+!17 = !DIBasicType(name: "unsigned int", size: 32, encoding: DW_ATE_unsigned)
+!18 = !DILocation(line: 6, column: 15, scope: !10)
+!19 = !DILocation(line: 6, column: 19, scope: !10)
+!20 = !DILocation(line: 6, column: 2, scope: !10)
+!21 = !DILabel(scope: !10, name: "A", file: !11, line: 7)
+!22 = !DILocation(line: 7, column: 1, scope: !10)
+!23 = !DILocation(line: 8, column: 6, scope: !24)
+!24 = distinct !DILexicalBlock(scope: !10, file: !11, line: 8, column: 6)
+!25 = !DILocation(line: 8, column: 8, scope: !24)
+!26 = !DILocation(line: 8, column: 6, scope: !10)
+!27 = !DILocation(line: 9, column: 5, scope: !28)
+!28 = distinct !DILexicalBlock(scope: !24, file: !11, line: 8, column: 14)
+!29 = !DILocation(line: 10, column: 3, scope: !28)
+!30 = !DILocation(line: 12, column: 3, scope: !31)
+!31 = distinct !DILexicalBlock(scope: !24, file: !11, line: 11, column: 9)
+!32 = !DILabel(scope: !10, name: "B", file: !11, line: 14)
+!33 = !DILocation(line: 14, column: 1, scope: !10)
+!34 = !DILocation(line: 16, column: 6, scope: !35)
+!35 = distinct !DILexicalBlock(scope: !10, file: !11, line: 16, column: 6)
+!36 = !DILocation(line: 16, column: 8, scope: !35)
+!37 = !DILocation(line: 16, column: 6, scope: !10)
+!38 = !DILocation(line: 17, column: 3, scope: !39)
+!39 = distinct !DILexicalBlock(scope: !35, file: !11, line: 16, column: 13)
+!40 = !DILocation(line: 19, column: 3, scope: !41)
+!41 = distinct !DILexicalBlock(scope: !35, file: !11, line: 18, column: 9)
+!42 = !DILabel(scope: !10, name: "D", file: !11, line: 21)
+!43 = !DILocation(line: 21, column: 1, scope: !10)
+!44 = !DILocation(line: 23, column: 3, scope: !10)
+!45 = !DILocation(line: 25, column: 6, scope: !46)
+!46 = distinct !DILexicalBlock(scope: !10, file: !11, line: 25, column: 6)
+!47 = !DILocation(line: 25, column: 8, scope: !46)
+!48 = !DILocation(line: 25, column: 6, scope: !10)
+!49 = !DILocation(line: 26, column: 3, scope: !50)
+!50 = distinct !DILexicalBlock(scope: !46, file: !11, line: 25, column: 13)
+!51 = !DILocation(line: 28, column: 3, scope: !52)
+!52 = distinct !DILexicalBlock(scope: !46, file: !11, line: 27, column: 9)
+!53 = !DILabel(scope: !10, name: "E", file: !11, line: 30)
+!54 = !DILocation(line: 30, column: 1, scope: !10)
+!55 = !DILocation(line: 32, column: 6, scope: !56)
+!56 = distinct !DILexicalBlock(scope: !10, file: !11, line: 32, column: 6)
+!57 = !DILocation(line: 32, column: 8, scope: !56)
+!58 = !DILocation(line: 32, column: 6, scope: !10)
+!59 = !DILocation(line: 33, column: 3, scope: !60)
+!60 = distinct !DILexicalBlock(scope: !56, file: !11, line: 32, column: 13)
+!61 = !DILocation(line: 35, column: 3, scope: !62)
+!62 = distinct !DILexicalBlock(scope: !56, file: !11, line: 34, column: 9)
+!63 = !DILabel(scope: !10, name: "F", file: !11, line: 37)
+!64 = !DILocation(line: 37, column: 1, scope: !10)
+!65 = !DILocation(line: 39, column: 6, scope: !66)
+!66 = distinct !DILexicalBlock(scope: !10, file: !11, line: 39, column: 6)
+!67 = !DILocation(line: 39, column: 8, scope: !66)
+!68 = !DILocation(line: 39, column: 6, scope: !10)
+!69 = !DILocation(line: 40, column: 3, scope: !70)
+!70 = distinct !DILexicalBlock(scope: !66, file: !11, line: 39, column: 13)
+!71 = !DILocation(line: 42, column: 3, scope: !72)
+!72 = distinct !DILexicalBlock(scope: !66, file: !11, line: 41, column: 9)
+!73 = !DILabel(scope: !10, name: "G", file: !11, line: 44)
+!74 = !DILocation(line: 44, column: 1, scope: !10)
+!75 = !DILocation(line: 46, column: 3, scope: !10)
+!76 = !DILocation(line: 47, column: 2, scope: !10)
+!77 = !DILabel(scope: !10, name: "C", file: !11, line: 48)
+!78 = !DILocation(line: 48, column: 1, scope: !10)
+!79 = !DILocation(line: 50, column: 6, scope: !80)
+!80 = distinct !DILexicalBlock(scope: !10, file: !11, line: 50, column: 6)
+!81 = !DILocation(line: 50, column: 8, scope: !80)
+!82 = !DILocation(line: 50, column: 6, scope: !10)
+!83 = !DILocation(line: 51, column: 3, scope: !84)
+!84 = distinct !DILexicalBlock(scope: !80, file: !11, line: 50, column: 13)
+!85 = !DILocation(line: 53, column: 3, scope: !86)
+!86 = distinct !DILexicalBlock(scope: !80, file: !11, line: 52, column: 9)
+!87 = !DILabel(scope: !10, name: "Halt", file: !11, line: 55)
+!88 = !DILocation(line: 55, column: 1, scope: !10)
+!89 = !DILocation(line: 57, column: 2, scope: !90)
+!90 = distinct !DILexicalBlock(scope: !91, file: !11, line: 57, column: 2)
+!91 = distinct !DILexicalBlock(scope: !10, file: !11, line: 57, column: 2)
+!92 = !DILocation(line: 57, column: 2, scope: !91)
+!93 = !DILocation(line: 58, column: 1, scope: !10)