Extend loop normalization (#705)

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com> Co-authored-by: Hernan Ponce de Leon <hernanl.leon@huawei.com> Co-authored-by: Thomas Haas <tomy.haas@t-online.de>
hernanponcedeleon · hernanponcedeleon · Sep 3, 2024 · May 27, 2024 · May 31, 2024 · Jun 3, 2024
commit 6582d4aaa1279a9fe42173505b1fdfc162a05828
diff --git 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/benchmarks/c/miscellaneous/MP_atomic_bool.c → benchmarks/miscellaneous/MP_atomic_bool.c b/benchmarks/c/miscellaneous/MP_atomic_bool.c → benchmarks/miscellaneous/MP_atomic_bool.c
diff --git a/benchmarks/c/miscellaneous/SB-RMW.c → benchmarks/miscellaneous/SB-RMW.c b/benchmarks/c/miscellaneous/SB-RMW.c → benchmarks/miscellaneous/SB-RMW.c
diff --git a/...arks/c/miscellaneous/SB-asm-lwsync+sync.c → ...hmarks/miscellaneous/SB-asm-lwsync+sync.c b/...arks/c/miscellaneous/SB-asm-lwsync+sync.c → ...hmarks/miscellaneous/SB-asm-lwsync+sync.c
diff --git a/benchmarks/c/miscellaneous/SB-asm-mfences.c → benchmarks/miscellaneous/SB-asm-mfences.c b/benchmarks/c/miscellaneous/SB-asm-mfences.c → benchmarks/miscellaneous/SB-asm-mfences.c
diff --git a/benchmarks/c/miscellaneous/SB-asm-syncs.c → benchmarks/miscellaneous/SB-asm-syncs.c b/benchmarks/c/miscellaneous/SB-asm-syncs.c → benchmarks/miscellaneous/SB-asm-syncs.c
diff --git a/benchmarks/c/miscellaneous/ctlz.c → benchmarks/miscellaneous/ctlz.c b/benchmarks/c/miscellaneous/ctlz.c → benchmarks/miscellaneous/ctlz.c
diff --git a/benchmarks/c/miscellaneous/cttz.c → benchmarks/miscellaneous/cttz.c b/benchmarks/c/miscellaneous/cttz.c → benchmarks/miscellaneous/cttz.c
diff --git a/...s/c/miscellaneous/funcPtrInStaticMemory.c → ...rks/miscellaneous/funcPtrInStaticMemory.c b/...s/c/miscellaneous/funcPtrInStaticMemory.c → ...rks/miscellaneous/funcPtrInStaticMemory.c
diff --git a/benchmarks/c/miscellaneous/idd_dynamic.c → benchmarks/miscellaneous/idd_dynamic.c b/benchmarks/c/miscellaneous/idd_dynamic.c → benchmarks/miscellaneous/idd_dynamic.c
diff --git a/benchmarks/miscellaneous/jumpIntoLoop.c b/benchmarks/miscellaneous/jumpIntoLoop.c
@@ -0,0 +1,21 @@
+#include <stdint.h>
+#include <assert.h>
+#include <dat3m.h>
+
+volatile int32_t x = 0;
+
+int main()
+{
+    int i = 0;
+    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));
+    return 0;
+}
diff --git a/benchmarks/c/miscellaneous/memcpy_s.c → benchmarks/miscellaneous/memcpy_s.c b/benchmarks/c/miscellaneous/memcpy_s.c → benchmarks/miscellaneous/memcpy_s.c
diff --git a/...marks/c/miscellaneous/multipleBackJumps.c → benchmarks/miscellaneous/multipleBackJumps.c b/...marks/c/miscellaneous/multipleBackJumps.c → benchmarks/miscellaneous/multipleBackJumps.c
diff --git a/benchmarks/c/miscellaneous/nondet_loop.c → benchmarks/miscellaneous/nondet_loop.c b/benchmarks/c/miscellaneous/nondet_loop.c → benchmarks/miscellaneous/nondet_loop.c
diff --git a/benchmarks/c/miscellaneous/offsetof.c → benchmarks/miscellaneous/offsetof.c b/benchmarks/c/miscellaneous/offsetof.c → benchmarks/miscellaneous/offsetof.c
diff --git a/...c/miscellaneous/propagatableSideEffects.c → ...s/miscellaneous/propagatableSideEffects.c b/...c/miscellaneous/propagatableSideEffects.c → ...s/miscellaneous/propagatableSideEffects.c
diff --git a/benchmarks/c/miscellaneous/pthread.c → benchmarks/miscellaneous/pthread.c b/benchmarks/c/miscellaneous/pthread.c → benchmarks/miscellaneous/pthread.c
diff --git a/benchmarks/c/miscellaneous/recursion.c → benchmarks/miscellaneous/recursion.c b/benchmarks/c/miscellaneous/recursion.c → benchmarks/miscellaneous/recursion.c
diff --git a/benchmarks/c/miscellaneous/staticLoops.c → benchmarks/miscellaneous/staticLoops.c b/benchmarks/c/miscellaneous/staticLoops.c → benchmarks/miscellaneous/staticLoops.c
diff --git a/benchmarks/c/miscellaneous/thread_chaining.c → benchmarks/miscellaneous/thread_chaining.c b/benchmarks/c/miscellaneous/thread_chaining.c → benchmarks/miscellaneous/thread_chaining.c
diff --git a/benchmarks/c/miscellaneous/thread_id.c → benchmarks/miscellaneous/thread_id.c b/benchmarks/c/miscellaneous/thread_id.c → benchmarks/miscellaneous/thread_id.c
diff --git a/benchmarks/c/miscellaneous/thread_inlining.c → benchmarks/miscellaneous/thread_inlining.c b/benchmarks/c/miscellaneous/thread_inlining.c → benchmarks/miscellaneous/thread_inlining.c
diff --git a/...c/miscellaneous/thread_inlining_complex.c → ...s/miscellaneous/thread_inlining_complex.c b/...c/miscellaneous/thread_inlining_complex.c → ...s/miscellaneous/thread_inlining_complex.c
diff --git a/...miscellaneous/thread_inlining_complex_2.c → ...miscellaneous/thread_inlining_complex_2.c b/...miscellaneous/thread_inlining_complex_2.c → ...miscellaneous/thread_inlining_complex_2.c
diff --git a/benchmarks/c/miscellaneous/thread_local.c → benchmarks/miscellaneous/thread_local.c b/benchmarks/c/miscellaneous/thread_local.c → benchmarks/miscellaneous/thread_local.c
diff --git a/benchmarks/c/miscellaneous/thread_loop.c → benchmarks/miscellaneous/thread_loop.c b/benchmarks/c/miscellaneous/thread_loop.c → benchmarks/miscellaneous/thread_loop.c
diff --git a/benchmarks/c/miscellaneous/uninitRead.c → benchmarks/miscellaneous/uninitRead.c b/benchmarks/c/miscellaneous/uninitRead.c → benchmarks/miscellaneous/uninitRead.c
diff --git a/benchmarks/miscellaneous/unsupported-loop-normalization.c 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);
+}
diff --git a/benchmarks/c/miscellaneous/verifierAssert.c → benchmarks/miscellaneous/verifierAssert.c b/benchmarks/c/miscellaneous/verifierAssert.c → benchmarks/miscellaneous/verifierAssert.c
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
@@ -1,46 +1,97 @@
 package com.dat3m.dartagnan.program.processing;
 
+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;
+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.util.ArrayList;
 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
+    This pass normalizes loops to have a single unconditional backjump and a single entry point.
+    It achieves this via two transformations.
 
-    L:
-    ...
-    if X goto L
-    ...
-    if Y goto L
-    More Code
+    (1) Given a loop of the form
+
+        entry:
+        ...
+        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
-    ...
+        entry:
+        __loopEntryPoint_L <- 0
+        ...
+        __loopEntryPoint_L <- 1
+        goto L
+        ...
+        L:
+        __forwardTo_L <- __loopEntryPoint_L
+        __loopEntryPoint_L <- 0
+        if __forwardTo_L == 1 goto C
+        ...
+        C:
+        ...
+        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 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) {
+
+        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()
@@ -70,4 +121,83 @@ public void run(Function function) {
             counter++;
         }
     }
+
+    private void guaranteeSingleEntry(Function function) {
+        int loopCounter = 0;
+        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;
+            }
+
+            final CondJump loopEnd = backJumps.get(backJumps.size() - 1);
+            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 (loopIrregularEntryPoints.isEmpty()) {
+                continue;
+            }
+
+            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);
+
+            final List<Event> forwardingInstrumentation = new ArrayList<>();
+            forwardingInstrumentation.add(assignForwarderReg);
+            forwardingInstrumentation.add(resetEntryPointReg);
+
+            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 CondJump forwardingJump = EventFactory.newJump(expressions.makeEQ(forwarderReg, entryPointValue), entryPoint);
+                forwardingInstrumentation.add(forwardingJump);
+            }
+
+            loopBegin.insertAfter(forwardingInstrumentation);
+            loopCounter++;
+        }
+    }
+
+    private boolean isEntryPoint(Event beginning, Event end, Label internal) {
+        return !getEnteringJumps(beginning, end, internal).isEmpty();
+    }
+
+    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
@@ -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(),
@@ -99,6 +98,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
                                 Simplifier.fromConfig(config)
                         ), Target.FUNCTIONS, true
                 ),
+                ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.FUNCTIONS, true),
                 RegisterDecomposition.newInstance(),
                 RemoveDeadFunctions.newInstance(),
                 printAfterSimplification ? DebugPrint.withHeader("After simplification", Printer.Mode.ALL) : null,

diff --git 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},
+                {"jumpIntoLoop", IMM, PASS, 11}
         });
     }
 

diff --git 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);
+    }
 }
diff --git a/dartagnan/src/test/resources/exceptions/unsupported-loop-normalization.ll 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)
diff --git a/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll b/dartagnan/src/test/resources/miscellaneous/jumpIntoLoop.ll
@@ -0,0 +1,180 @@
+; 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 !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 !33
+
+9:                                                ; preds = %0
+  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 !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 !42
+
+14:                                               ; preds = %13, %8
+  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 !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 !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 !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 !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 !53
+  %31 = icmp eq i32 %30, 4, !dbg !53
+  br label %32
+
+32:                                               ; preds = %29, %26
+  %33 = phi i1 [ false, %26 ], [ %31, %29 ], !dbg !54
+  br label %34, !dbg !53
+
+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
+
+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 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: cold noreturn
+declare void @__assert_rtn(i8* noundef, i8* noundef, i32 noundef, i8* noundef) #3
+
+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 = { "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 = !{!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: !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)