Added new nondet_loop.c code + unit test.

Moved IntrinsicsInlining to after Unrolling
Minor cleanup

benchmarks/c/miscellaneous/nondet_loop.c

@@ -0,0 +1,17 @@
+#include <stdint.h>
+#include <assert.h>
+
+int main()
+{
+    int x = 0;
+    while (x != 5) {
+        if (__VERIFIER_nondet_int() == 0) {
+            x += 2;
+        } else {
+            x += 3;
+        }
+    }
+    assert (0);
+
+    return 0;
+}

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

@@ -43,10 +43,7 @@ public void run(Program program) {
     }
 
     private void run(Thread thread) {
-        for (Event event : List.copyOf(thread.getEvents())) {
-            if (!(event instanceof DirectFunctionCall call)) {
-                continue;
-            }
+        for (DirectFunctionCall call : thread.getEvents(DirectFunctionCall.class)) {
             assert !call.getCallTarget().hasBody();
 
             List<Event> replacement = switch (call.getCallTarget().getName()) {
@@ -59,8 +56,8 @@ private void run(Thread thread) {
                         String.format("Undefined function %s", call.getCallTarget().getName()));
             };
 
-            call.insertAfter(replacement);
-            call.forceDelete();
+            replacement.forEach(e -> e.copyAllMetadataFrom(call));
+            call.replaceBy(replacement);
         }
     }
 
@@ -70,9 +67,10 @@ private List<Event> inlineNonDet(DirectFunctionCall call) {
         assert call instanceof DirectValueFunctionCall;
         Register register = ((DirectValueFunctionCall) call).getResultRegister();
         String name = call.getCallTarget().getName();
-        String prefix = name.startsWith("__V") ? "__VERIFIER_nondet_" : "__SMACK_nondet_";
-        assert name.startsWith(prefix);
-        String suffix = call.getCallTarget().getName().substring(prefix.length());
+        final String separator = "nondet_";
+        int index = name.indexOf(separator);
+        assert index > -1;
+        String suffix = name.substring(index + separator.length());
 
         // Nondeterministic booleans
         if (suffix.equals("bool")) {
@@ -109,9 +107,9 @@ private List<Event> inlineNonDet(DirectFunctionCall call) {
             throw new ParsingException(String.format("Non-integer result register %s.", register));
         }
         var expression = new INonDet(constantId++, type, signed);
-        call.getFunction().getProgram().addConstant(expression);
         expression.setMin(min);
         expression.setMax(max);
+        call.getFunction().getProgram().addConstant(expression);
         return List.of(EventFactory.newLocal(register, expression));
     }
 }

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

@@ -79,7 +79,6 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
                 StaticMemoryInitializer.newInstance(),
                 Inlining.fromConfig(config),
                 ThreadCreation.fromConfig(config),
-                IntrinsicsInlining.fromConfig(config),
                 UnreachableCodeElimination.fromConfig(config),
                 ComplexBlockSplitting.newInstance(),
                 BranchReordering.fromConfig(config),
@@ -91,6 +90,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
                 SimpleSpinLoopDetection.fromConfig(config),
                 LoopUnrolling.fromConfig(config),
                 printAfterUnrolling ? DebugPrint.withHeader("After loop unrolling") : null,
+                IntrinsicsInlining.fromConfig(config),
                 dynamicPureLoopCutting ? DynamicPureLoopCutting.fromConfig(config) : null,
                 constantPropagation ? SparseConditionalConstantPropagation.fromConfig(config) : null,
                 dce ? DeadAssignmentElimination.fromConfig(config) : null,

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

@@ -21,7 +21,7 @@
 import java.util.stream.Collectors;
 
 /*
-    This pass finds and marks simple loops that are totally side effect free (simple spin loops).
+    This pass finds and marks simple loops that are totally side-effect-free (simple spin loops).
     It will also mark side-effect-full loops if they are annotated by a SpinStart event
     (we assume the user guarantees the correctness of the annotation)
 
@@ -30,6 +30,9 @@ The pass is unable to detect complex types of loops that may spin endlessly (i.e
 
     TODO: Instead of tagging labels as spinning and checking for that tag during loop unrolling
           we could let this pass produce LoopBound-Annotations to guide the unrolling implicitly.
+
+    TODO 2: Intrinsic calls need to get special treatment as they might be side-effect-full
+     (for now, all our intrinsics are side-effect-free, so it works fine).
  */
 public class SimpleSpinLoopDetection implements ProgramProcessor {
 

dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java

@@ -56,7 +56,8 @@ public static Iterable<Object[]> data() throws IOException {
                 {"thread_inlining", IMM, PASS, 1},
                 {"thread_inlining_complex", IMM, PASS, 1},
                 {"thread_inlining_complex_2", IMM, PASS, 1},
-                {"thread_local", IMM, PASS, 1}
+                {"thread_local", IMM, PASS, 1},
+                {"nondet_loop", IMM, FAIL, 3}
         });
     }