diff --git a/benchmarks/c/miscellaneous/nondet_loop.c b/benchmarks/c/miscellaneous/nondet_loop.c new file mode 100644 index 0000000000..136b6d3d98 --- /dev/null +++ b/benchmarks/c/miscellaneous/nondet_loop.c @@ -0,0 +1,17 @@ +#include +#include + +int main() +{ + int x = 0; + while (x != 5) { + if (__VERIFIER_nondet_int() == 0) { + x += 2; + } else { + x += 3; + } + } + assert (0); + + return 0; +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IntrinsicsInlining.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IntrinsicsInlining.java index c7c88078ba..a4fe531fa7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IntrinsicsInlining.java +++ b/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 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 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 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)); } } 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 c7a6172d0f..fe83d99c2f 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 @@ -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, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SimpleSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SimpleSpinLoopDetection.java index 5320c6ac50..02adeb764f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SimpleSpinLoopDetection.java +++ b/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 { 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 bad172bf9f..e4bc01caca 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java @@ -56,7 +56,8 @@ public static Iterable 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} }); }