diff --git a/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java b/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java index 4c7a9e51..3808338a 100644 --- a/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java +++ b/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java @@ -136,6 +136,71 @@ private static String qualifiedMethodName(Symbol.MethodSymbol sym) { private class StaticMethodCollector extends TreeScanner { final List procedures = new ArrayList<>(); + private int labelCounter = 0; + + /** Label stack entry for break/continue resolution. */ + private record LabelEntry(String javaLabel, String breakLabel, String continueLabel) {} + private final Deque labelStack = new ArrayDeque<>(); + private String pendingLabel = null; + + /** Check if a statement tree contains break or continue (at the current loop level). */ + private boolean containsBreakOrContinue(JCTree.JCStatement stmt) { + boolean[] found = {false}; + stmt.accept(new TreeScanner() { + @Override public void visitBreak(JCTree.JCBreak tree) { found[0] = true; } + @Override public void visitContinue(JCTree.JCContinue tree) { found[0] = true; } + // Don't descend into nested loops — their break/continue don't target us + @Override public void visitWhileLoop(JCTree.JCWhileLoop tree) {} + @Override public void visitForLoop(JCTree.JCForLoop tree) {} + @Override public void visitDoLoop(JCTree.JCDoWhileLoop tree) {} + }); + return found[0]; + } + + private String freshLabel(String prefix) { + return prefix + "_" + (labelCounter++); + } + + /** Set up loop labels, push to stack, execute body, pop stack. */ + private StmtExpr withLoopLabels(JCTree.JCStatement loopBody, java.util.function.BiFunction body) { + boolean needsLabels = containsBreakOrContinue(loopBody); + String breakLbl = needsLabels ? freshLabel("loop_break") : null; + String continueLbl = needsLabels ? freshLabel("loop_continue") : null; + String javaLabel = pendingLabel; + pendingLabel = null; + labelStack.push(new LabelEntry(javaLabel, breakLbl, continueLbl)); + try { + return body.apply(breakLbl, continueLbl); + } finally { + labelStack.pop(); + } + } + + private String resolveBreakLabel(JCTree.JCBreak brk) { + if (brk.label != null) { + String target = brk.label.toString(); + for (var entry : labelStack) { + if (target.equals(entry.javaLabel)) return entry.breakLabel; + } + } else if (!labelStack.isEmpty()) { + return labelStack.peek().breakLabel; + } + throw new JavaViolationException("break target not found"); + } + + private String resolveContinueLabel(JCTree.JCContinue cont) { + if (cont.label != null) { + String target = cont.label.toString(); + for (var entry : labelStack) { + if (target.equals(entry.javaLabel) && entry.continueLabel != null) return entry.continueLabel; + } + } else { + for (var entry : labelStack) { + if (entry.continueLabel != null) return entry.continueLabel; + } + } + throw new JavaViolationException("continue target not found"); + } @Override public void visitMethodDef(JCTree.JCMethodDecl method) { @@ -233,6 +298,64 @@ private StmtExpr convertBlock(JCTree.JCBlock blk) { return block(toSourceRange(blk), statements); } + /** + * Emit a while loop with optional break/continue label wrapping. + * + * When labels are present, produces (for a for-loop with break/continue): + * 
+         * labelledBlock(breakLbl, {
+         *   preamble...        // e.g. init for for-loops, sentinel decl for do-while
+         *   while (cond)
+         *     invariants: [...]
+         *   {
+         *     labelledBlock(continueLbl, { body });
+         *     step;            // null for while/do-while
+         *   }
+         * })
+         *
+ * break emits as exit(breakLbl), continue as exit(continueLbl). + * The step is outside the continue label so continue skips the body but still runs the step. + * @param sr source range + * @param cond loop condition + * @param invariants loop invariants + * @param loopBody the translated loop body + * @param step optional step expression (for-loops); null for while/do-while + * @param preamble statements to emit before the while (e.g. init, sentinel decl) + * @param needsLabels whether break/continue is present + * @param breakLbl break label (null if !needsLabels) + * @param continueLbl continue label (null if !needsLabels) + */ + private StmtExpr emitLoop(SourceRange sr, StmtExpr cond, List invariants, + StmtExpr loopBody, StmtExpr step, List preamble, + String breakLbl, String continueLbl) { + if (breakLbl != null) { + StmtExpr wrappedBody = labelledBlock(sr, List.of(loopBody), continueLbl); + StmtExpr whileBody; + if (step != null) { + whileBody = block(sr, List.of(wrappedBody, step)); + } else { + whileBody = wrappedBody; + } + StmtExpr whileNode = while_(sr, cond, invariants, whileBody); + List outerStmts = new ArrayList<>(preamble); + outerStmts.add(whileNode); + return labelledBlock(sr, outerStmts, breakLbl); + } else { + if (step != null) { + // Use forLoop IR node for simple for-loops without break/continue + StmtExpr init = preamble.isEmpty() ? block(sr, List.of()) : preamble.getFirst(); + return forLoop(sr, init, cond, step, invariants, loopBody); + } + StmtExpr whileNode = while_(sr, cond, invariants, loopBody); + if (preamble.isEmpty()) { + return whileNode; + } + List stmts = new ArrayList<>(preamble); + stmts.add(whileNode); + return block(sr, stmts); + } + } + private StmtExpr convertStatement(JCTree.JCStatement statement) { return switch (statement) { case JCTree.JCAssert assertStmt -> @@ -266,34 +389,77 @@ yield varDecl(toSourceRange(varDecl), varDecl.name.toString(), yield null; } case JCTree.JCWhileLoop whileStmt -> { - StmtExpr cond = convertExpression(whileStmt.cond); - if (whileStmt.body instanceof JCTree.JCBlock loopBlock) { - var parts = extractLoopParts(loopBlock); - yield while_(toSourceRange(whileStmt), cond, parts.invariants, parts.body); - } - yield while_(toSourceRange(whileStmt), cond, List.of(), convertStatement(whileStmt.body)); + var sr = toSourceRange(whileStmt); + yield withLoopLabels(whileStmt.body, (breakLbl, continueLbl) -> { + StmtExpr cond = convertExpression(whileStmt.cond); + var parts = extractLoopParts(whileStmt.body); + return emitLoop(sr, cond, parts.invariants, parts.body, null, List.of(), + breakLbl, continueLbl); + }); } case JCTree.JCForLoop forLoop -> { if (forLoop.init.size() > 1 || forLoop.step.size() > 1) throw new JavaViolationException("Multi-init or multi-step for loops are not supported"); - StmtExpr init = forLoop.init.isEmpty() ? block(toSourceRange(forLoop), List.of()) - : convertStatement(forLoop.init.getFirst()); - StmtExpr cond = forLoop.cond != null - ? convertExpression(forLoop.cond) - : literalBool(toSourceRange(forLoop), true); - StmtExpr step = forLoop.step.isEmpty() ? block(toSourceRange(forLoop), List.of()) - : convertStatement(forLoop.step.getFirst()); - List invariants = List.of(); - StmtExpr loopBody; - if (forLoop.body instanceof JCTree.JCBlock loopBlock) { - var parts = extractLoopParts(loopBlock); - invariants = parts.invariants; - loopBody = parts.body; + var sr = toSourceRange(forLoop); + yield withLoopLabels(forLoop.body, (breakLbl, continueLbl) -> { + StmtExpr init = forLoop.init.isEmpty() ? block(sr, List.of()) + : convertStatement(forLoop.init.getFirst()); + StmtExpr cond = forLoop.cond != null + ? convertExpression(forLoop.cond) + : literalBool(sr, true); + StmtExpr step = forLoop.step.isEmpty() ? block(sr, List.of()) + : convertStatement(forLoop.step.getFirst()); + var parts = extractLoopParts(forLoop.body); + return emitLoop(sr, cond, parts.invariants, parts.body, step, List.of(init), + breakLbl, continueLbl); + }); + } + case JCTree.JCDoWhileLoop doWhileStmt -> { + var sr = toSourceRange(doWhileStmt); + yield withLoopLabels(doWhileStmt.body, (breakLbl, continueLbl) -> { + // Desugar: var __first_N = true; while(__first_N || cond) { __first_N = false; body } + String sentinel = "__first_" + labelCounter; + StmtExpr sentinelDecl = varDecl(sr, sentinel, + Optional.of(typeAnnotation(boolType())), + Optional.of(initializer(literalBool(sr, true)))); + StmtExpr cond = orElse(sr, identifier(sr, sentinel), convertExpression(doWhileStmt.cond)); + StmtExpr sentinelReset = assign(sr, identifier(sr, sentinel), literalBool(sr, false)); + + var parts = extractLoopParts(doWhileStmt.body); + StmtExpr loopBody = block(sr, List.of(sentinelReset, parts.body)); + return emitLoop(sr, cond, parts.invariants, loopBody, null, List.of(sentinelDecl), + breakLbl, continueLbl); + }); + } + case JCTree.JCBreak breakStmt -> { + yield exit(toSourceRange(breakStmt), resolveBreakLabel(breakStmt)); + } + case JCTree.JCContinue contStmt -> { + yield exit(toSourceRange(contStmt), resolveContinueLabel(contStmt)); + } + case JCTree.JCLabeledStatement labeledStmt -> { + // Set the pending label so the next loop picks it up + pendingLabel = labeledStmt.label.toString(); + // If the body is a loop, it will consume pendingLabel + // If not, wrap in a labelledBlock for break-out-of-block + if (labeledStmt.body instanceof JCTree.JCWhileLoop + || labeledStmt.body instanceof JCTree.JCForLoop + || labeledStmt.body instanceof JCTree.JCDoWhileLoop) { + yield convertStatement(labeledStmt.body); } else { - loopBody = convertStatement(forLoop.body); + // Non-loop labeled statement: only break is valid (no continue) + String breakLbl = freshLabel("label_break"); + labelStack.push(new LabelEntry(pendingLabel, breakLbl, null)); + pendingLabel = null; + try { + StmtExpr body = convertStatement(labeledStmt.body); + yield labelledBlock(toSourceRange(labeledStmt), List.of(body), breakLbl); + } finally { + labelStack.pop(); + } } - yield forLoop(toSourceRange(forLoop), init, cond, step, invariants, loopBody); } + case JCTree.JCSkip ignored -> null; default -> throw new JavaViolationException("Unsupported statement: " + statement.getClass().getSimpleName()); }; } @@ -316,19 +482,23 @@ private StmtExpr convertLambdaBody(JCTree.JCLambda lambda, Map r private record LoopParts(List invariants, StmtExpr body) {} - private LoopParts extractLoopParts(JCTree.JCBlock loopBlock) { - MethodOrLoopContract loopContract = contractCompiler.getContract(loopBlock); - List invariants = new ArrayList<>(); - for (var inv : loopContract.loopInvariants()) { - invariants.add(invariantClause(convertExpression(inv.get()))); - } - var implStatements = MethodOrLoopContractCompiler.getImplementationStatements(loopBlock); - List stmts = new ArrayList<>(); - for (var s : implStatements) { - StmtExpr converted = convertStatement(s); - if (converted != null) stmts.add(converted); + private LoopParts extractLoopParts(JCTree.JCStatement body) { + if (body instanceof JCTree.JCBlock loopBlock) { + MethodOrLoopContract loopContract = contractCompiler.getContract(loopBlock); + List invariants = new ArrayList<>(); + for (var inv : loopContract.loopInvariants()) { + invariants.add(invariantClause(convertExpression(inv.get()))); + } + var implStatements = MethodOrLoopContractCompiler.getImplementationStatements(loopBlock); + List stmts = new ArrayList<>(); + for (var s : implStatements) { + StmtExpr converted = convertStatement(s); + if (converted != null) stmts.add(converted); + } + return new LoopParts(invariants, block(toSourceRange(loopBlock), stmts)); + } else { + return new LoopParts(List.of(), convertStatement(body)); } - return new LoopParts(invariants, block(toSourceRange(loopBlock), stmts)); } private StmtExpr convertExpression(JCTree.JCExpression expr, Map renames) { diff --git a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/statements/VerifyBreakContinue.java b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/statements/VerifyBreakContinue.java new file mode 100644 index 00000000..0fd28d34 --- /dev/null +++ b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/statements/VerifyBreakContinue.java @@ -0,0 +1,162 @@ +package org.strata.jverify.verifier.tests.javasupport.statements; + +import org.strata.jverify.testengine.JVerifyTest; + +import static org.strata.jverify.JVerify.*; + +@SuppressWarnings({"ConditionalBreakInInfiniteLoop", "ConstantValue"}) +@JVerifyTest(methodsVerified = 11, errorCount = 0) +class VerifyBreakContinue { + static void forLoopBreak() { + int i = 0; + for (i = 0; i < 10; i = i + 1) { + invariant(i >= 0 && i <= 5); + if (i == 5) { + break; + } + } + check(i == 5); + } + + static void whileWithBreak() { + var x = 0; + while (x < 10) { + invariant(x >= 0 && x <= 5); + if (x == 5) { + break; + } + x = x + 1; + } + check(x == 5); + } + + static void whileInfiniteBreak() { + var x = 0; + while (true) { + invariant(x >= 0 && x <= 3); + if (x == 3) { + break; + } + x = x + 1; + } + check(x == 3); + } + + static void nestedBreakInner() { + int total = 0; + for (int i = 0; i < 3; i = i + 1) { + invariant(i >= 0 && i <= 3); + invariant(total == i * 2); + int j = 0; + for (j = 0; j < 5; j = j + 1) { + invariant(j >= 0 && j <= 2); + if (j == 2) { + break; + } + } + check(j == 2); + total = total + j; + } + check(total == 6); + } + + static void forLoopContinue() { + int i = 0; + int x = 0; + for (i = 0; i < 5; i = i + 1) { + invariant(i >= 0 && i <= 5); + invariant(i <= 2 ? x == i : x == 2); + if (i >= 2) { + continue; + } + x = x + 1; + } + check(x == 2); + } + + static void forLoopContinueSingleSkip() { + int i = 0; + int x = 0; + for (i = 0; i < 5; i = i + 1) { + invariant(i >= 0 && i <= 5); + invariant(i <= 2 ? x == i * (i - 1) / 2 : x == i * (i - 1) / 2 - 2); + if (i == 2) { + continue; + } + x = x + i; + } + check(x == 8); + } + + static void whileWithContinue() { + var i = 0; + var x = 0; + while (i < 5) { + invariant(i >= 0 && i <= 5); + invariant(i <= 2 ? x == i : x == 2); + if (i >= 2) { + i = i + 1; + continue; + } + x = x + 1; + i = i + 1; + } + check(x == 2); + } + + static void whileWithContinueSingleSkip() { + var i = 0; + var x = 0; + while (i < 5) { + invariant(i >= 0 && i <= 5); + invariant(i <= 2 ? x == i * (i - 1) / 2 : x == i * (i - 1) / 2 - 2); + if (i == 2) { + i = i + 1; + continue; + } + x = x + i; + i = i + 1; + } + check(x == 8); + } + + static void multipleLoopsWithBreakAndContinue() { + int a = 0; + for (int i = 0; i < 5; i = i + 1) { + invariant(i >= 0 && i <= 5); + invariant(i <= 3 ? a == i : a == i - 1); + if (i == 3) { + continue; + } + a = a + 1; + } + check(a == 4); + + int b = 0; + for (int j = 0; j < 5; j = j + 1) { + invariant(j >= 0 && j <= 5); + invariant(j <= 2 ? b == j : b == j - 1); + if (j == 2) { + continue; + } + b = b + 1; + } + check(b == 4); + } + + static void breakAndContinueInSameLoop() { + int x = 0; + for (int i = 0; i < 10; i = i + 1) { + invariant(i >= 0 && i <= 7); + invariant(i <= 3 ? x == i * (i - 1) / 2 : x == i * (i - 1) / 2 - 3); + if (i == 3) { + continue; + } + if (i == 7) { + break; + } + x = x + i; + } + check(x == 18); + } +} diff --git a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/statements/VerifyStatements.java b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/statements/VerifyStatements.java index b4ec7e0c..1182fc04 100644 --- a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/statements/VerifyStatements.java +++ b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/statements/VerifyStatements.java @@ -6,30 +6,8 @@ import static org.strata.jverify.JVerify.*; @SuppressWarnings({"ConditionalBreakInInfiniteLoop", "StatementWithEmptyBody", "ConstantValue"}) -@JVerifyTest(methodsVerified = 19, errorCount = 0) +@JVerifyTest(methodsVerified = 13, errorCount = 0) class VerifyStatements { - void whileWithBreak() { - var x = 0; - while(true) { - decreases(10 - x); - if (P(x)) { - break; - } - x = x + 1; - } - } - - void whileWithContinue() { - var x = 0; - while(x < 10) { - if (P(x)) { - continue; - } - check(!P(x)); - x = x + 1; - } - } - void forLoop() { int i = 0; for(i = 0; i < 5; i = i + 1) { @@ -37,34 +15,6 @@ void forLoop() { check(i == 5); } - void forLoopBreak() { - int i = 0; - int x = 0; - for(i = 0; true; i = i + 1) { - decreases(5 - i); - invariant(i <= 5); - invariant(x == i); - if (i == 5) { - break; - } - x = x + 1; - } - check(i == 5); - } - - void forLoopContinue() { - int i = 0; - int x = 0; - for(i = 0; i < 5; i = i + 1) { - invariant(i <= 3 ? x == i : x == i - 1); - if (i == 3) { - continue; - } - x = x + 1; - } - check(i == 5); - } - void nestedForLoop() { int x = 0; for (int i = 0; i < 5; i = i + 1) { @@ -95,26 +45,6 @@ void nestedForLoopContinue() { } } - void nestedForLoopBreak() { - int x = 0; - outerLoop: - for (int i = 0; i < 5; i = i + 1) { - invariant(x == i * 5); - invariant(i <= 2); - - for (int j = 0; j < 5; j = j + 1) { - invariant(x == j + i * 5); - invariant(i == 2 ? j <= 2 : true); - if (i == 2 && j == 2) { - check(x == 12); - break outerLoop; - } - x = x + 1; - } - } - check(x == 12); - } - void doWhileLoop() { int x = 0; do { @@ -125,20 +55,6 @@ void doWhileLoop() { check(x == 5); } - void twoForLoops() { - int cnt = 0; - for (var i = 0; i < 10; i++) { - invariant(cnt==i); - cnt++; - } - check(cnt==10); - for (var i = 0; i < 10; i++) { - invariant(cnt-10==i); - cnt++; - } - check(cnt==20); - } - void skip() { ;;;; check(true);