From 6f91fa8d31f8b91f467c5c96aa3534b5e4172185 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 19 May 2026 18:39:42 +0200 Subject: [PATCH 1/9] Bump Strata submodule to latest main MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bump the Strata submodule from 8593f7cf to 53a3df53 (latest main) and regenerate Laurel Java classes. Schema-affecting Strata commits: - strata-org/Strata#1076 — disallow transparent procedures (require `opaque` for procedures with visible bodies) - strata-org/Strata#969 — add `opaque` keyword to Laurel grammar; ensures and modifies are now wrapped in an optional OpaqueSpec - strata-org/Strata#1031 — add `modifies *` wildcard (new ModifiesWildcard variant; unused here) - strata-org/Strata#1077 — generalized multi-target assign (new MultiAssign + AssignTarget AST nodes; unused here) - strata-org/Strata#1140 — Provenance type / metadata migration Hand-written changes: - JavaToLaurelCompiler: emit OpaqueSpec for impure procedures (always) and for pure functions with non-empty ensures. - LaurelDriver: pass `--solver z3` explicitly. The previous Strata hardcoded `solver := "z3"` for the Laurel pipeline; the bumped Strata removed that override and now defaults to cvc5 (which our CI doesn't install). Passing `--solver z3` preserves prior behavior. All other diffs in verifier/src/main/java/org/strata/jverify/laurel/ are generated by `make generate-laurel-ast`. Note: pure functions that declare @Ensures used to be emitted as Transparent and are now emitted as Opaque (forced by the schema). No existing test combines @Pure with @Ensures, so nothing in the suite regresses; callers of such functions in the future will reason via the postcondition rather than by definitional unfolding. --- Strata | 2 +- .../strata/jverify/laurel/AssignTarget.java | 50 +++++++++++++++++++ .../org/strata/jverify/laurel/Laurel.java | 30 ++++++++--- .../strata/jverify/laurel/ModifiesClause.java | 17 ++++++- .../java/org/strata/jverify/laurel/Node.java | 2 +- .../org/strata/jverify/laurel/OpaqueSpec.java | 19 +++++++ .../org/strata/jverify/laurel/Procedure.java | 10 ++-- .../org/strata/jverify/laurel/StmtExpr.java | 18 ++++++- .../laurel/JavaToLaurelCompiler.java | 14 +++++- .../jverify/verifier/laurel/LaurelDriver.java | 2 +- 10 files changed, 144 insertions(+), 20 deletions(-) create mode 100644 verifier/src/main/java/org/strata/jverify/laurel/AssignTarget.java create mode 100644 verifier/src/main/java/org/strata/jverify/laurel/OpaqueSpec.java diff --git a/Strata b/Strata index 8593f7cf..53a3df53 160000 --- a/Strata +++ b/Strata @@ -1 +1 @@ -Subproject commit 8593f7cf9dc8faf3ca75fece40e9a10638be0242 +Subproject commit 53a3df5345ba8c09e5c1443b609f09369a556335 diff --git a/verifier/src/main/java/org/strata/jverify/laurel/AssignTarget.java b/verifier/src/main/java/org/strata/jverify/laurel/AssignTarget.java new file mode 100644 index 00000000..44091f34 --- /dev/null +++ b/verifier/src/main/java/org/strata/jverify/laurel/AssignTarget.java @@ -0,0 +1,50 @@ +package org.strata.jverify.laurel; + +public sealed interface AssignTarget extends Node permits AssignTarget.AssignTargetDecl, AssignTarget.AssignTargetVar, AssignTarget.AssignTargetField { + public record AssignTargetDecl( + SourceRange sourceRange, + java.lang.String name, LaurelType targetType + ) implements AssignTarget { + @Override + public java.lang.String operationName() { return "Laurel.assignTargetDecl"; } + + @Override + public com.amazon.ion.IonSexp toIon(IonSerializer $s) { + var sexp = $s.newOp("Laurel.assignTargetDecl", sourceRange()); + sexp.add($s.serializeIdent(name())); + sexp.add($s.serialize(targetType())); + return sexp; + } + } + + public record AssignTargetVar( + SourceRange sourceRange, + java.lang.String name + ) implements AssignTarget { + @Override + public java.lang.String operationName() { return "Laurel.assignTargetVar"; } + + @Override + public com.amazon.ion.IonSexp toIon(IonSerializer $s) { + var sexp = $s.newOp("Laurel.assignTargetVar", sourceRange()); + sexp.add($s.serializeIdent(name())); + return sexp; + } + } + + public record AssignTargetField( + SourceRange sourceRange, + java.lang.String obj, java.lang.String field + ) implements AssignTarget { + @Override + public java.lang.String operationName() { return "Laurel.assignTargetField"; } + + @Override + public com.amazon.ion.IonSexp toIon(IonSerializer $s) { + var sexp = $s.newOp("Laurel.assignTargetField", sourceRange()); + sexp.add($s.serializeIdent(obj())); + sexp.add($s.serializeIdent(field())); + return sexp; + } + } +} diff --git a/verifier/src/main/java/org/strata/jverify/laurel/Laurel.java b/verifier/src/main/java/org/strata/jverify/laurel/Laurel.java index b629115a..bd222267 100644 --- a/verifier/src/main/java/org/strata/jverify/laurel/Laurel.java +++ b/verifier/src/main/java/org/strata/jverify/laurel/Laurel.java @@ -73,6 +73,18 @@ public class Laurel { public static StmtExpr assign(SourceRange sourceRange, StmtExpr target, StmtExpr value) { return new StmtExpr.Assign(sourceRange, target, value); } public static StmtExpr assign(StmtExpr target, StmtExpr value) { return new StmtExpr.Assign(SourceRange.NONE, target, value); } + public static AssignTarget assignTargetDecl(SourceRange sourceRange, java.lang.String name, LaurelType targetType) { return new AssignTarget.AssignTargetDecl(sourceRange, name, targetType); } + public static AssignTarget assignTargetDecl(java.lang.String name, LaurelType targetType) { return new AssignTarget.AssignTargetDecl(SourceRange.NONE, name, targetType); } + + public static AssignTarget assignTargetVar(SourceRange sourceRange, java.lang.String name) { return new AssignTarget.AssignTargetVar(sourceRange, name); } + public static AssignTarget assignTargetVar(java.lang.String name) { return new AssignTarget.AssignTargetVar(SourceRange.NONE, name); } + + public static AssignTarget assignTargetField(SourceRange sourceRange, java.lang.String obj, java.lang.String field) { return new AssignTarget.AssignTargetField(sourceRange, obj, field); } + public static AssignTarget assignTargetField(java.lang.String obj, java.lang.String field) { return new AssignTarget.AssignTargetField(SourceRange.NONE, obj, field); } + + public static StmtExpr multiAssign(SourceRange sourceRange, java.util.List targets, StmtExpr value) { return new StmtExpr.MultiAssign(sourceRange, targets, value); } + public static StmtExpr multiAssign(java.util.List targets, StmtExpr value) { return new StmtExpr.MultiAssign(SourceRange.NONE, targets, value); } + public static StmtExpr add(SourceRange sourceRange, StmtExpr lhs, StmtExpr rhs) { return new StmtExpr.Add(sourceRange, lhs, rhs); } public static StmtExpr add(StmtExpr lhs, StmtExpr rhs) { return new StmtExpr.Add(SourceRange.NONE, lhs, rhs); } @@ -226,23 +238,29 @@ public class Laurel { public static EnsuresClause ensuresClause(SourceRange sourceRange, StmtExpr cond, java.util.Optional errorMessage) { return new EnsuresClause.Of(sourceRange, cond, errorMessage); } public static EnsuresClause ensuresClause(StmtExpr cond, java.util.Optional errorMessage) { return new EnsuresClause.Of(SourceRange.NONE, cond, errorMessage); } - public static ModifiesClause modifiesClause(SourceRange sourceRange, java.util.List refs) { return new ModifiesClause.Of(sourceRange, refs); } - public static ModifiesClause modifiesClause(java.util.List refs) { return new ModifiesClause.Of(SourceRange.NONE, refs); } + public static ModifiesClause modifiesClause(SourceRange sourceRange, java.util.List refs) { return new ModifiesClause.ModifiesClause_(sourceRange, refs); } + public static ModifiesClause modifiesClause(java.util.List refs) { return new ModifiesClause.ModifiesClause_(SourceRange.NONE, refs); } + + public static ModifiesClause modifiesWildcard(SourceRange sourceRange) { return new ModifiesClause.ModifiesWildcard(sourceRange); } + public static ModifiesClause modifiesWildcard() { return new ModifiesClause.ModifiesWildcard(SourceRange.NONE); } public static ReturnParameters returnParameters(SourceRange sourceRange, java.util.List parameters) { return new ReturnParameters.Of(sourceRange, parameters); } public static ReturnParameters returnParameters(java.util.List parameters) { return new ReturnParameters.Of(SourceRange.NONE, parameters); } + public static OpaqueSpec opaqueSpec(SourceRange sourceRange, java.util.List ensures, java.util.List modifies) { return new OpaqueSpec.Of(sourceRange, ensures, modifies); } + public static OpaqueSpec opaqueSpec(java.util.List ensures, java.util.List modifies) { return new OpaqueSpec.Of(SourceRange.NONE, ensures, modifies); } + public static Body body(SourceRange sourceRange, StmtExpr body) { return new Body.Body_(sourceRange, body); } public static Body body(StmtExpr body) { return new Body.Body_(SourceRange.NONE, body); } public static Body externalBody(SourceRange sourceRange) { return new Body.ExternalBody(sourceRange); } public static Body externalBody() { return new Body.ExternalBody(SourceRange.NONE); } - public static Procedure procedure(SourceRange sourceRange, java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.List ensures, java.util.List modifies, java.util.Optional body) { return new Procedure.Procedure_(sourceRange, name, parameters, returnType, returnParameters, requires, invokeOn, ensures, modifies, body); } - public static Procedure procedure(java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.List ensures, java.util.List modifies, java.util.Optional body) { return new Procedure.Procedure_(SourceRange.NONE, name, parameters, returnType, returnParameters, requires, invokeOn, ensures, modifies, body); } + public static Procedure procedure(SourceRange sourceRange, java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.Optional opaqueSpec, java.util.Optional body) { return new Procedure.Procedure_(sourceRange, name, parameters, returnType, returnParameters, requires, invokeOn, opaqueSpec, body); } + public static Procedure procedure(java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.Optional opaqueSpec, java.util.Optional body) { return new Procedure.Procedure_(SourceRange.NONE, name, parameters, returnType, returnParameters, requires, invokeOn, opaqueSpec, body); } - public static Procedure function(SourceRange sourceRange, java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.List ensures, java.util.List modifies, java.util.Optional body) { return new Procedure.Function(sourceRange, name, parameters, returnType, returnParameters, requires, invokeOn, ensures, modifies, body); } - public static Procedure function(java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.List ensures, java.util.List modifies, java.util.Optional body) { return new Procedure.Function(SourceRange.NONE, name, parameters, returnType, returnParameters, requires, invokeOn, ensures, modifies, body); } + public static Procedure function(SourceRange sourceRange, java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.Optional opaqueSpec, java.util.Optional body) { return new Procedure.Function(sourceRange, name, parameters, returnType, returnParameters, requires, invokeOn, opaqueSpec, body); } + public static Procedure function(java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.Optional opaqueSpec, java.util.Optional body) { return new Procedure.Function(SourceRange.NONE, name, parameters, returnType, returnParameters, requires, invokeOn, opaqueSpec, body); } public static Composite composite(SourceRange sourceRange, java.lang.String name, java.util.Optional extending, java.util.List fields, java.util.List procedures) { return new Composite.Of(sourceRange, name, extending, fields, procedures); } public static Composite composite(java.lang.String name, java.util.Optional extending, java.util.List fields, java.util.List procedures) { return new Composite.Of(SourceRange.NONE, name, extending, fields, procedures); } diff --git a/verifier/src/main/java/org/strata/jverify/laurel/ModifiesClause.java b/verifier/src/main/java/org/strata/jverify/laurel/ModifiesClause.java index 3c29c096..55ab2c65 100644 --- a/verifier/src/main/java/org/strata/jverify/laurel/ModifiesClause.java +++ b/verifier/src/main/java/org/strata/jverify/laurel/ModifiesClause.java @@ -1,7 +1,7 @@ package org.strata.jverify.laurel; -public sealed interface ModifiesClause extends Node permits ModifiesClause.Of { - public record Of( +public sealed interface ModifiesClause extends Node permits ModifiesClause.ModifiesClause_, ModifiesClause.ModifiesWildcard { + public record ModifiesClause_( SourceRange sourceRange, java.util.List refs ) implements ModifiesClause { @@ -15,4 +15,17 @@ public com.amazon.ion.IonSexp toIon(IonSerializer $s) { return sexp; } } + + public record ModifiesWildcard( + SourceRange sourceRange + ) implements ModifiesClause { + @Override + public java.lang.String operationName() { return "Laurel.modifiesWildcard"; } + + @Override + public com.amazon.ion.IonSexp toIon(IonSerializer $s) { + var sexp = $s.newOp("Laurel.modifiesWildcard", sourceRange()); + return sexp; + } + } } diff --git a/verifier/src/main/java/org/strata/jverify/laurel/Node.java b/verifier/src/main/java/org/strata/jverify/laurel/Node.java index 575bf678..be0c6120 100644 --- a/verifier/src/main/java/org/strata/jverify/laurel/Node.java +++ b/verifier/src/main/java/org/strata/jverify/laurel/Node.java @@ -2,7 +2,7 @@ import com.amazon.ion.IonSexp; -public sealed interface Node permits Parameter, ReturnType, ConstrainedType, Procedure, Composite, Datatype, DatatypeConstructorList, DatatypeConstructorArg, ElseBranch, Body, Extends, InvariantClause, Trigger, Initializer, Field, StmtExpr, Command, LaurelType, ErrorSummary, DatatypeConstructor, InvokeOnClause, RequiresClause, ReturnParameters, TypeAnnotation, ModifiesClause, EnsuresClause { +public sealed interface Node permits Parameter, AssignTarget, ReturnType, ConstrainedType, Composite, Procedure, Datatype, DatatypeConstructorList, DatatypeConstructorArg, ElseBranch, OpaqueSpec, Body, Extends, InvariantClause, Trigger, Initializer, Field, StmtExpr, Command, LaurelType, ErrorSummary, DatatypeConstructor, InvokeOnClause, RequiresClause, ReturnParameters, TypeAnnotation, ModifiesClause, EnsuresClause { SourceRange sourceRange(); java.lang.String operationName(); IonSexp toIon(IonSerializer $s); diff --git a/verifier/src/main/java/org/strata/jverify/laurel/OpaqueSpec.java b/verifier/src/main/java/org/strata/jverify/laurel/OpaqueSpec.java new file mode 100644 index 00000000..0c888cff --- /dev/null +++ b/verifier/src/main/java/org/strata/jverify/laurel/OpaqueSpec.java @@ -0,0 +1,19 @@ +package org.strata.jverify.laurel; + +public sealed interface OpaqueSpec extends Node permits OpaqueSpec.Of { + public record Of( + SourceRange sourceRange, + java.util.List ensures, java.util.List modifies + ) implements OpaqueSpec { + @Override + public java.lang.String operationName() { return "Laurel.opaqueSpec"; } + + @Override + public com.amazon.ion.IonSexp toIon(IonSerializer $s) { + var sexp = $s.newOp("Laurel.opaqueSpec", sourceRange()); + sexp.add($s.serializeSeq(ensures(), "seq", $s::serialize)); + sexp.add($s.serializeSeq(modifies(), "seq", $s::serialize)); + return sexp; + } + } +} diff --git a/verifier/src/main/java/org/strata/jverify/laurel/Procedure.java b/verifier/src/main/java/org/strata/jverify/laurel/Procedure.java index 5c355069..dbdc3c62 100644 --- a/verifier/src/main/java/org/strata/jverify/laurel/Procedure.java +++ b/verifier/src/main/java/org/strata/jverify/laurel/Procedure.java @@ -3,7 +3,7 @@ public sealed interface Procedure extends Node permits Procedure.Procedure_, Procedure.Function { public record Procedure_( SourceRange sourceRange, - java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.List ensures, java.util.List modifies, java.util.Optional body + java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.Optional opaqueSpec, java.util.Optional body ) implements Procedure { @Override public java.lang.String operationName() { return "Laurel.procedure"; } @@ -17,8 +17,7 @@ public com.amazon.ion.IonSexp toIon(IonSerializer $s) { sexp.add($s.serializeOption(returnParameters(), $s::serialize)); sexp.add($s.serializeSeq(requires(), "seq", $s::serialize)); sexp.add($s.serializeOption(invokeOn(), $s::serialize)); - sexp.add($s.serializeSeq(ensures(), "seq", $s::serialize)); - sexp.add($s.serializeSeq(modifies(), "seq", $s::serialize)); + sexp.add($s.serializeOption(opaqueSpec(), $s::serialize)); sexp.add($s.serializeOption(body(), $s::serialize)); return sexp; } @@ -26,7 +25,7 @@ public com.amazon.ion.IonSexp toIon(IonSerializer $s) { public record Function( SourceRange sourceRange, - java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.List ensures, java.util.List modifies, java.util.Optional body + java.lang.String name, java.util.List parameters, java.util.Optional returnType, java.util.Optional returnParameters, java.util.List requires, java.util.Optional invokeOn, java.util.Optional opaqueSpec, java.util.Optional body ) implements Procedure { @Override public java.lang.String operationName() { return "Laurel.function"; } @@ -40,8 +39,7 @@ public com.amazon.ion.IonSexp toIon(IonSerializer $s) { sexp.add($s.serializeOption(returnParameters(), $s::serialize)); sexp.add($s.serializeSeq(requires(), "seq", $s::serialize)); sexp.add($s.serializeOption(invokeOn(), $s::serialize)); - sexp.add($s.serializeSeq(ensures(), "seq", $s::serialize)); - sexp.add($s.serializeSeq(modifies(), "seq", $s::serialize)); + sexp.add($s.serializeOption(opaqueSpec(), $s::serialize)); sexp.add($s.serializeOption(body(), $s::serialize)); return sexp; } diff --git a/verifier/src/main/java/org/strata/jverify/laurel/StmtExpr.java b/verifier/src/main/java/org/strata/jverify/laurel/StmtExpr.java index 717b4583..89ab66d4 100644 --- a/verifier/src/main/java/org/strata/jverify/laurel/StmtExpr.java +++ b/verifier/src/main/java/org/strata/jverify/laurel/StmtExpr.java @@ -1,6 +1,6 @@ package org.strata.jverify.laurel; -public sealed interface StmtExpr extends Node permits StmtExpr.LiteralBool, StmtExpr.Int, StmtExpr.Real, StmtExpr.String_, StmtExpr.Hole, StmtExpr.NondetHole, StmtExpr.VarDecl, StmtExpr.Call, StmtExpr.New, StmtExpr.FieldAccess, StmtExpr.Identifier, StmtExpr.Parenthesis, StmtExpr.Assign, StmtExpr.Add, StmtExpr.Sub, StmtExpr.Mul, StmtExpr.Div, StmtExpr.Mod, StmtExpr.DivT, StmtExpr.ModT, StmtExpr.Eq, StmtExpr.Neq, StmtExpr.Gt, StmtExpr.Lt, StmtExpr.Le, StmtExpr.Ge, StmtExpr.And, StmtExpr.Or, StmtExpr.AndThen, StmtExpr.OrElse, StmtExpr.Implies, StmtExpr.StrConcat, StmtExpr.Not, StmtExpr.Neg, StmtExpr.ForallExpr, StmtExpr.ExistsExpr, StmtExpr.IfThenElse, StmtExpr.Assert, StmtExpr.Assume, StmtExpr.Return, StmtExpr.Block, StmtExpr.LabelledBlock, StmtExpr.Exit, StmtExpr.While, StmtExpr.ForLoop, StmtExpr.IsType, StmtExpr.AsType { +public sealed interface StmtExpr extends Node permits StmtExpr.LiteralBool, StmtExpr.Int, StmtExpr.Real, StmtExpr.String_, StmtExpr.Hole, StmtExpr.NondetHole, StmtExpr.VarDecl, StmtExpr.Call, StmtExpr.New, StmtExpr.FieldAccess, StmtExpr.Identifier, StmtExpr.Parenthesis, StmtExpr.Assign, StmtExpr.MultiAssign, StmtExpr.Add, StmtExpr.Sub, StmtExpr.Mul, StmtExpr.Div, StmtExpr.Mod, StmtExpr.DivT, StmtExpr.ModT, StmtExpr.Eq, StmtExpr.Neq, StmtExpr.Gt, StmtExpr.Lt, StmtExpr.Le, StmtExpr.Ge, StmtExpr.And, StmtExpr.Or, StmtExpr.AndThen, StmtExpr.OrElse, StmtExpr.Implies, StmtExpr.StrConcat, StmtExpr.Not, StmtExpr.Neg, StmtExpr.ForallExpr, StmtExpr.ExistsExpr, StmtExpr.IfThenElse, StmtExpr.Assert, StmtExpr.Assume, StmtExpr.Return, StmtExpr.Block, StmtExpr.LabelledBlock, StmtExpr.Exit, StmtExpr.While, StmtExpr.ForLoop, StmtExpr.IsType, StmtExpr.AsType { public record LiteralBool( SourceRange sourceRange, boolean b @@ -197,6 +197,22 @@ public com.amazon.ion.IonSexp toIon(IonSerializer $s) { } } + public record MultiAssign( + SourceRange sourceRange, + java.util.List targets, StmtExpr value + ) implements StmtExpr { + @Override + public java.lang.String operationName() { return "Laurel.multiAssign"; } + + @Override + public com.amazon.ion.IonSexp toIon(IonSerializer $s) { + var sexp = $s.newOp("Laurel.multiAssign", sourceRange()); + sexp.add($s.serializeSeq(targets(), "commaSepList", $s::serialize)); + sexp.add($s.serialize(value())); + return sexp; + } + } + public record Add( SourceRange sourceRange, StmtExpr lhs, StmtExpr rhs 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 e8ee3a6c..2bf62f84 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 @@ -180,11 +180,21 @@ public void visitMethodDef(JCTree.JCMethodDecl method) { : Optional.empty(); boolean isPure = jverifyUtils.isPure(method.sym); + // Strata rejects transparent (visible-body) procedures unless they're functional; + // emit an OpaqueSpec to mark the body opaque otherwise. Pure functions stay + // transparent only when they have no ensures clauses (the schema can't carry + // ensures without an OpaqueSpec wrapper). + // modifies is always empty: jverify doesn't yet emit modifies clauses. + boolean canStayTransparent = isPure && ensures.isEmpty(); + Optional optSpec = canStayTransparent + ? Optional.empty() + : Optional.of(opaqueSpec(ensures, List.of())); + Procedure proc = isPure ? function(toSourceRange(method), methodName, params, - retType, Optional.empty(), requires, Optional.empty(), ensures, List.of(), optBody) + retType, Optional.empty(), requires, Optional.empty(), optSpec, optBody) : procedure(toSourceRange(method), methodName, params, - retType, Optional.empty(), requires, Optional.empty(), ensures, List.of(), optBody); + retType, Optional.empty(), requires, Optional.empty(), optSpec, optBody); procedures.add(proc); } super.visitMethodDef(method); diff --git a/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java b/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java index 2e386547..7c1cbd32 100644 --- a/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java +++ b/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java @@ -108,7 +108,7 @@ public JVerifyResults verifyJavaFiles( public JVerifyResults runVerifier(FilesMap filesMap, IonValue serializedProgram) { var processBuilder = new ProcessBuilder( - "lake", "exe", "-q", "strata", "laurelAnalyzeBinary" + "lake", "exe", "-q", "strata", "laurelAnalyzeBinary", "--solver", "z3" ); processBuilder.directory(verifierOptions.backendPath().toFile()); return verifierOptions.time("Running Strata", () -> { From 731858a1e4d497e473933a5a20839bc3e8fdab9e Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Tue, 19 May 2026 21:20:21 +0000 Subject: [PATCH 2/9] feat: add break/continue/labeled statements/do-while support Add convertStatement cases for JCBreak, JCContinue, JCLabeledStatement, JCDoWhileLoop, and JCSkip in JavaToLaurelCompiler, resolving issue #407 (excluding decreases clause which is deferred to Strata-side work). Design: - Label stack with (javaLabel, breakLabel, continueLabel) tuples pushed on each loop/labeled-statement entry, popped on exit - Only wrap loops in labelledBlock when break/continue is actually present in the loop body (detected via tree scan) - When break/continue is present, desugar for-loops to while manually (not using the forLoop IR node) to produce the correct structure: labelledBlock(breakLbl, { init; while(cond) { labelledBlock(continueLbl, body); step } }) This matches the PythonToLaurel pattern and allows Strata to verify invariants correctly across continue paths. - break/continue emit as exit(label) to the resolved target - do-while desugared via sentinel variable - Labeled statements pass their label to the next loop via pendingLabel Add VerifyBreakContinue test exercising for-break, while-break, infinite-while-break, nested-break, for-continue, and while-continue. Fixes #407 (break/continue/labeled/do-while portion). --- .../laurel/JavaToLaurelCompiler.java | 212 ++++++++++++++++-- .../statements/VerifyBreakContinue.java | 122 ++++++++++ 2 files changed, 314 insertions(+), 20 deletions(-) create mode 100644 verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/statements/VerifyBreakContinue.java 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 2bf62f84..c6974ca8 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 @@ -123,6 +123,56 @@ private LaurelType translateType(com.sun.tools.javac.code.Type type) { 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++); + } + + 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) { @@ -244,34 +294,156 @@ 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); + var sr = toSourceRange(whileStmt); + boolean needsLabels = containsBreakOrContinue(whileStmt.body); + 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 { + StmtExpr cond = convertExpression(whileStmt.cond); + List invariants = List.of(); + StmtExpr loopBody; + if (whileStmt.body instanceof JCTree.JCBlock loopBlock) { + var parts = extractLoopParts(loopBlock); + invariants = parts.invariants; + loopBody = parts.body; + } else { + loopBody = convertStatement(whileStmt.body); + } + if (needsLabels) { + StmtExpr wrappedBody = labelledBlock(sr, List.of(loopBody), continueLbl); + StmtExpr whileNode = while_(sr, cond, invariants, wrappedBody); + yield labelledBlock(sr, List.of(whileNode), breakLbl); + } else { + yield while_(sr, cond, invariants, loopBody); + } + } finally { + labelStack.pop(); } - yield while_(toSourceRange(whileStmt), cond, List.of(), convertStatement(whileStmt.body)); } 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); + boolean needsLabels = containsBreakOrContinue(forLoop.body); + 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 { + 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()); + List invariants = List.of(); + StmtExpr loopBody; + if (forLoop.body instanceof JCTree.JCBlock loopBlock) { + var parts = extractLoopParts(loopBlock); + invariants = parts.invariants; + loopBody = parts.body; + } else { + loopBody = convertStatement(forLoop.body); + } + if (needsLabels) { + // Desugar to while manually to match the expected structure: + // labelledBlock(breakLbl, { init; while(cond) { labelledBlock(continueLbl, body); step } }) + StmtExpr wrappedBody = labelledBlock(sr, List.of(loopBody), continueLbl); + List whileBodyStmts = new ArrayList<>(); + whileBodyStmts.add(wrappedBody); + whileBodyStmts.add(step); + StmtExpr whileBody = block(sr, whileBodyStmts); + StmtExpr whileNode = while_(sr, cond, invariants, whileBody); + List outerStmts = new ArrayList<>(); + outerStmts.add(init); + outerStmts.add(whileNode); + yield labelledBlock(sr, outerStmts, breakLbl); + } else { + yield forLoop(sr, init, cond, step, invariants, loopBody); + } + } finally { + labelStack.pop(); + } + } + case JCTree.JCDoWhileLoop doWhileStmt -> { + var sr = toSourceRange(doWhileStmt); + boolean needsLabels = containsBreakOrContinue(doWhileStmt.body); + 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 { + // 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 sentinelId = identifier(sr, sentinel); + StmtExpr cond = orElse(sr, sentinelId, convertExpression(doWhileStmt.cond)); + StmtExpr sentinelReset = assign(sr, identifier(sr, sentinel), literalBool(sr, false)); + + List invariants = List.of(); + StmtExpr loopBody; + if (doWhileStmt.body instanceof JCTree.JCBlock loopBlock) { + var parts = extractLoopParts(loopBlock); + invariants = parts.invariants; + List bodyStmts = new ArrayList<>(); + bodyStmts.add(sentinelReset); + bodyStmts.add(parts.body); + loopBody = block(sr, bodyStmts); + } else { + List bodyStmts = new ArrayList<>(); + bodyStmts.add(sentinelReset); + bodyStmts.add(convertStatement(doWhileStmt.body)); + loopBody = block(sr, bodyStmts); + } + if (needsLabels) { + StmtExpr wrappedBody = labelledBlock(sr, List.of(loopBody), continueLbl); + StmtExpr whileNode = while_(sr, cond, invariants, wrappedBody); + yield labelledBlock(sr, List.of(sentinelDecl, whileNode), breakLbl); + } else { + StmtExpr whileNode = while_(sr, cond, invariants, loopBody); + yield block(sr, List.of(sentinelDecl, whileNode)); + } + } finally { + labelStack.pop(); + } + } + 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()); }; } 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..5c96265e --- /dev/null +++ b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/statements/VerifyBreakContinue.java @@ -0,0 +1,122 @@ +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 = 9, 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); + } +} From 8a3f88a4ae4b63b40f9253a2629cadb8da214d7f Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 20 May 2026 14:19:03 +0000 Subject: [PATCH 3/9] refactor: extract emitLoop helper to deduplicate loop emission Extract the shared loop emission logic (labelled block wrapping, while node creation, preamble handling) into a single emitLoop() method used by while, for, and do-while cases. Parameters: - cond, invariants, loopBody: the core loop components - step: optional (non-null for for-loops, null for while/do-while) - preamble: statements before the while (init for for, sentinel for do-while) - needsLabels, breakLbl, continueLbl: label wrapping control No behavioral change. --- .../laurel/JavaToLaurelCompiler.java | 147 +++++++++--------- 1 file changed, 75 insertions(+), 72 deletions(-) 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 c6974ca8..e6712846 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 @@ -148,6 +148,21 @@ 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(); @@ -261,6 +276,49 @@ private StmtExpr convertBlock(JCTree.JCBlock blk) { return block(toSourceRange(blk), statements); } + /** + * Emit a while loop with optional break/continue label wrapping. + * @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 -> @@ -295,13 +353,7 @@ yield varDecl(toSourceRange(varDecl), varDecl.name.toString(), } case JCTree.JCWhileLoop whileStmt -> { var sr = toSourceRange(whileStmt); - boolean needsLabels = containsBreakOrContinue(whileStmt.body); - 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 { + yield withLoopLabels(whileStmt.body, (breakLbl, continueLbl) -> { StmtExpr cond = convertExpression(whileStmt.cond); List invariants = List.of(); StmtExpr loopBody; @@ -312,28 +364,15 @@ yield varDecl(toSourceRange(varDecl), varDecl.name.toString(), } else { loopBody = convertStatement(whileStmt.body); } - if (needsLabels) { - StmtExpr wrappedBody = labelledBlock(sr, List.of(loopBody), continueLbl); - StmtExpr whileNode = while_(sr, cond, invariants, wrappedBody); - yield labelledBlock(sr, List.of(whileNode), breakLbl); - } else { - yield while_(sr, cond, invariants, loopBody); - } - } finally { - labelStack.pop(); - } + return emitLoop(sr, cond, invariants, loopBody, 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"); var sr = toSourceRange(forLoop); - boolean needsLabels = containsBreakOrContinue(forLoop.body); - 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 { + yield withLoopLabels(forLoop.body, (breakLbl, continueLbl) -> { StmtExpr init = forLoop.init.isEmpty() ? block(sr, List.of()) : convertStatement(forLoop.init.getFirst()); StmtExpr cond = forLoop.cond != null @@ -350,70 +389,34 @@ yield varDecl(toSourceRange(varDecl), varDecl.name.toString(), } else { loopBody = convertStatement(forLoop.body); } - if (needsLabels) { - // Desugar to while manually to match the expected structure: - // labelledBlock(breakLbl, { init; while(cond) { labelledBlock(continueLbl, body); step } }) - StmtExpr wrappedBody = labelledBlock(sr, List.of(loopBody), continueLbl); - List whileBodyStmts = new ArrayList<>(); - whileBodyStmts.add(wrappedBody); - whileBodyStmts.add(step); - StmtExpr whileBody = block(sr, whileBodyStmts); - StmtExpr whileNode = while_(sr, cond, invariants, whileBody); - List outerStmts = new ArrayList<>(); - outerStmts.add(init); - outerStmts.add(whileNode); - yield labelledBlock(sr, outerStmts, breakLbl); - } else { - yield forLoop(sr, init, cond, step, invariants, loopBody); - } - } finally { - labelStack.pop(); - } + return emitLoop(sr, cond, invariants, loopBody, step, List.of(init), + breakLbl, continueLbl); + }); } case JCTree.JCDoWhileLoop doWhileStmt -> { var sr = toSourceRange(doWhileStmt); - boolean needsLabels = containsBreakOrContinue(doWhileStmt.body); - 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 { + 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 sentinelId = identifier(sr, sentinel); - StmtExpr cond = orElse(sr, sentinelId, convertExpression(doWhileStmt.cond)); + StmtExpr cond = orElse(sr, identifier(sr, sentinel), convertExpression(doWhileStmt.cond)); StmtExpr sentinelReset = assign(sr, identifier(sr, sentinel), literalBool(sr, false)); List invariants = List.of(); - StmtExpr loopBody; + StmtExpr innerBody; if (doWhileStmt.body instanceof JCTree.JCBlock loopBlock) { var parts = extractLoopParts(loopBlock); invariants = parts.invariants; - List bodyStmts = new ArrayList<>(); - bodyStmts.add(sentinelReset); - bodyStmts.add(parts.body); - loopBody = block(sr, bodyStmts); + innerBody = parts.body; } else { - List bodyStmts = new ArrayList<>(); - bodyStmts.add(sentinelReset); - bodyStmts.add(convertStatement(doWhileStmt.body)); - loopBody = block(sr, bodyStmts); + innerBody = convertStatement(doWhileStmt.body); } - if (needsLabels) { - StmtExpr wrappedBody = labelledBlock(sr, List.of(loopBody), continueLbl); - StmtExpr whileNode = while_(sr, cond, invariants, wrappedBody); - yield labelledBlock(sr, List.of(sentinelDecl, whileNode), breakLbl); - } else { - StmtExpr whileNode = while_(sr, cond, invariants, loopBody); - yield block(sr, List.of(sentinelDecl, whileNode)); - } - } finally { - labelStack.pop(); - } + StmtExpr loopBody = block(sr, List.of(sentinelReset, innerBody)); + return emitLoop(sr, cond, invariants, loopBody, null, List.of(sentinelDecl), + breakLbl, continueLbl); + }); } case JCTree.JCBreak breakStmt -> { yield exit(toSourceRange(breakStmt), resolveBreakLabel(breakStmt)); From 525b4934c56286edd004adc4fc7c7d11f155c71e Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 20 May 2026 14:51:35 +0000 Subject: [PATCH 4/9] refactor: make extractLoopParts handle block/non-block dispatch extractLoopParts now accepts JCStatement directly instead of requiring a JCBlock, internalizing the if-block-then-extract-else-just-convert pattern that was duplicated in all three loop cases. --- .../laurel/JavaToLaurelCompiler.java | 66 +++++++------------ 1 file changed, 23 insertions(+), 43 deletions(-) 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 e6712846..4c617b06 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 @@ -355,16 +355,8 @@ yield varDecl(toSourceRange(varDecl), varDecl.name.toString(), var sr = toSourceRange(whileStmt); yield withLoopLabels(whileStmt.body, (breakLbl, continueLbl) -> { StmtExpr cond = convertExpression(whileStmt.cond); - List invariants = List.of(); - StmtExpr loopBody; - if (whileStmt.body instanceof JCTree.JCBlock loopBlock) { - var parts = extractLoopParts(loopBlock); - invariants = parts.invariants; - loopBody = parts.body; - } else { - loopBody = convertStatement(whileStmt.body); - } - return emitLoop(sr, cond, invariants, loopBody, null, List.of(), + var parts = extractLoopParts(whileStmt.body); + return emitLoop(sr, cond, parts.invariants, parts.body, null, List.of(), breakLbl, continueLbl); }); } @@ -380,16 +372,8 @@ yield withLoopLabels(forLoop.body, (breakLbl, continueLbl) -> { : literalBool(sr, true); StmtExpr step = forLoop.step.isEmpty() ? block(sr, 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; - } else { - loopBody = convertStatement(forLoop.body); - } - return emitLoop(sr, cond, invariants, loopBody, step, List.of(init), + var parts = extractLoopParts(forLoop.body); + return emitLoop(sr, cond, parts.invariants, parts.body, step, List.of(init), breakLbl, continueLbl); }); } @@ -404,17 +388,9 @@ yield withLoopLabels(doWhileStmt.body, (breakLbl, continueLbl) -> { StmtExpr cond = orElse(sr, identifier(sr, sentinel), convertExpression(doWhileStmt.cond)); StmtExpr sentinelReset = assign(sr, identifier(sr, sentinel), literalBool(sr, false)); - List invariants = List.of(); - StmtExpr innerBody; - if (doWhileStmt.body instanceof JCTree.JCBlock loopBlock) { - var parts = extractLoopParts(loopBlock); - invariants = parts.invariants; - innerBody = parts.body; - } else { - innerBody = convertStatement(doWhileStmt.body); - } - StmtExpr loopBody = block(sr, List.of(sentinelReset, innerBody)); - return emitLoop(sr, cond, invariants, loopBody, null, List.of(sentinelDecl), + 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); }); } @@ -469,19 +445,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) { From 2e11b61eb746663e266d00556ce47abc5ffe0704 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 20 May 2026 16:21:35 +0000 Subject: [PATCH 5/9] docs: add translation example to emitLoop javadoc --- .../generator/laurel/JavaToLaurelCompiler.java | 15 +++++++++++++++ 1 file changed, 15 insertions(+) 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 ad737897..8e32b73c 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 @@ -282,6 +282,21 @@ private StmtExpr convertBlock(JCTree.JCBlock blk) { /** * 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 From a71bfba15b387b5321080414be01e07d946d8af0 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 20 May 2026 16:49:28 +0000 Subject: [PATCH 6/9] test: add multi-loop test to verify label uniqueness Two sequential for-loops with continue in the same method, each generating distinct labelled block labels (loop_break_N, loop_continue_N) to confirm no label conflicts. --- .../statements/VerifyBreakContinue.java | 24 ++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) 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 index 5c96265e..9796e847 100644 --- 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 @@ -5,7 +5,7 @@ import static org.strata.jverify.JVerify.*; @SuppressWarnings({"ConditionalBreakInInfiniteLoop", "ConstantValue"}) -@JVerifyTest(methodsVerified = 9, errorCount = 0) +@JVerifyTest(methodsVerified = 10, errorCount = 0) class VerifyBreakContinue { static void forLoopBreak() { int i = 0; @@ -119,4 +119,26 @@ static void whileWithContinueSingleSkip() { } 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; + } + + 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; + } + } } From 124589aabd1993b385c6019d924e3eec00d8c163 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 20 May 2026 16:56:06 +0000 Subject: [PATCH 7/9] test: add break and continue in same loop Exercises both exit targets (continue skips i==3, break exits at i==7) within a single for-loop, verifying x == 0+1+2+4+5+6 == 18. --- .../statements/VerifyBreakContinue.java | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) 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 index 9796e847..a9bc0449 100644 --- 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 @@ -5,7 +5,7 @@ import static org.strata.jverify.JVerify.*; @SuppressWarnings({"ConditionalBreakInInfiniteLoop", "ConstantValue"}) -@JVerifyTest(methodsVerified = 10, errorCount = 0) +@JVerifyTest(methodsVerified = 11, errorCount = 0) class VerifyBreakContinue { static void forLoopBreak() { int i = 0; @@ -141,4 +141,20 @@ static void multipleLoopsWithBreakAndContinue() { b = b + 1; } } + + 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); + } } From 9260f5bbed028bdcee4fa68d9646538e000a7e8b Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 20 May 2026 18:37:16 +0000 Subject: [PATCH 8/9] test: add check statements to multipleLoopsWithBreakAndContinue --- .../tests/javasupport/statements/VerifyBreakContinue.java | 2 ++ 1 file changed, 2 insertions(+) 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 index a9bc0449..0fd28d34 100644 --- 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 @@ -130,6 +130,7 @@ static void multipleLoopsWithBreakAndContinue() { } a = a + 1; } + check(a == 4); int b = 0; for (int j = 0; j < 5; j = j + 1) { @@ -140,6 +141,7 @@ static void multipleLoopsWithBreakAndContinue() { } b = b + 1; } + check(b == 4); } static void breakAndContinueInSameLoop() { From 6b69911f30ecfd8e94e9e07bec21d6c7bee9bbbe Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 20 May 2026 18:43:24 +0000 Subject: [PATCH 9/9] test: remove break/continue tests from VerifyStatements Remove whileWithBreak, whileWithContinue, forLoopBreak, forLoopContinue, nestedForLoopBreak, and twoForLoops from VerifyStatements. These are now covered by VerifyBreakContinue which uses static methods that actually exercise the Laurel compiler code paths. The removed tests were instance methods that never went through the compiler (due to the Flags.STATIC gate), making them effectively no-ops. Kept in VerifyStatements: - nestedForLoopContinue: uses labeled 'continue outerLoop' (unique) - doWhileLoop: uses 'decreases' clause (unique) - forLoop, nestedForLoop: test loops without break/continue - skip, nativeAssert, P/P2/P3, underscoreVariableName, methodWithResult, ignoreCallResult: unrelated to break/continue --- .../statements/VerifyStatements.java | 86 +------------------ 1 file changed, 1 insertion(+), 85 deletions(-) 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);