Translate instance methods via static-call-with-self encoding - #452
Open
fabiomadge wants to merge 14 commits into
Open
Translate instance methods via static-call-with-self encoding#452fabiomadge wants to merge 14 commits into
fabiomadge wants to merge 14 commits into
Conversation
fabiomadge
changed the title
fabiomadge
changed the title
fabiomadge
changed the title
fabiomadge
force-pushed
the
pr/step3-instance-methods
branch
from
June 17, 2026 22:50
98f9177 to
c2053c1
Compare
Strata rejects a function declaration that carries postconditions (LaurelToCoreTranslator.lean). The procedure/function selector keyed off isPure, so a @pure method with a postcondition was emitted as a function with a non-empty OpaqueSpec and failed translation. Key the selector off canStayTransparent (isPure && ensures.isEmpty()) instead: a pure method stays a transparent function only with no postconditions, otherwise it is emitted as an opaque procedure. Add a regression test (pureWithPostcondition) covering the previously untested @Pure-with-postcondition case.
qualifiedMethodName used outermostClass(), so a nested class's method Outer.Inner.foo mangled to Outer_foo and collided with Outer.foo. Use the immediately enclosing class instead (Outer.Inner_foo), keeping the package-qualified, dot-preserving scheme that already prevents cross-package collisions. The flat Class_method mangling also collapses every overload of a name onto one Laurel procedure name. Add refuseIfOverloaded, which counts the source-declared (non-synthetic) methods of a name in the enclosing class and throws JavaViolationException when there is more than one, at both the declaration and call sites. The per-method catch turns this into a graceful skip. Add StaticOverloadRefusal covering the refusal.
Drop the Flags.STATIC gate so instance methods are translated, using the
static-call-with-self encoding (PLAN.md §1): instance methods take an
explicit 'self' first parameter, 'this' becomes identifier("self"), and
instance calls prepend the receiver as the first argument — all lowering
to Laurel .StaticCall, never .InstanceCall/.This.
Scope and refusals (graceful skip via JavaViolationException; silent for
instance methods, reported for static ones):
- Constructors, synthetic/Lower-generated members, anonymous/local-class
methods, and @verify(false) methods are skipped (not emitted).
- Instance field access (read or write) is refused — composites carry no
fields yet (Step 8a).
- Polymorphic dispatch through a supertype reference is refused (Strata
#1174), except where the callee/class is final/private (no real dispatch).
- Object allocation (including lambdas) inside a contract is refused: a
'new' in a pre/postcondition reaches Core as an un-lowered block, which
Strata only lifts out of bodies, not contracts.
- @pure methods with a postcondition or a constrained (int/char) return are
emitted as opaque procedures, not functions (Strata rejects those on
functions).
Consistency: a two-pass transitive-emittability fixpoint drops any
procedure that calls a user method which itself was not emitted, so no
emitted Laurel references an unresolved name (avoids Strata 'Resolution
failed'). Guard the line-map lookup against synthetic '<unknown>' sources
so an unmappable Strata diagnostic no longer crashes the run.
Flips VerifyBooleanOperators green. Re-baselines test annotations for
methods that were previously counted as vacuously verified (never
translated under the gate) and are now honestly Skipped or refused;
VerifyStatements is skipped pending the Strata-side loop-invariant fix.
…ts, new-receiver calls
Self-review follow-ups (all conservative robustness fixes; soundness was
confirmed intact):
- Refuse object allocation / lambdas inside a LOOP invariant, not just
method pre/postconditions: extractLoopParts now sets inContractContext
around invariant conversion, so a 'new'/lambda there skips gracefully
instead of leaking an un-lowered block to Strata (crash/spurious-fail).
- Refuse a method call on a freshly-allocated receiver ('new T().m()'):
the opaque new_(T) value has no shape to pass as 'self', which made
Strata fail to unify; refuse for a graceful skip until constructor-
allocated values can be captured (Step 8a).
- Add regression tests for both (NewInLoopInvariantRefusal, NewReceiverRefusal).
Cleanup: extract an isStatic(JCMethodDecl) helper (was inlined at 3 sites),
import JVerifyIndex instead of using its FQN, drop refuseFieldAccess's
unused SourceRange parameter.
…sions Follow-ups from the Step-3b self-review: - S6: the transitive-emittability fixpoint keyed on the mangled NAME, so two distinct methods that mangle to the same Laurel name (e.g. instance methods Foo_bar.baz and Foo.bar_baz, both -> ...Foo_bar_baz) aliased each other and could falsely drop an unrelated caller. Key the fixpoint on MethodSymbol identity instead. Separately, add a pre-fixpoint guard that detects two surviving methods with the same mangled name and skips the whole colliding group (rather than emitting a duplicate Laurel symbol that Strata rejects abnormally); done before the fixpoint so callers of a dropped method cascade. Static methods are unaffected (namespaced by the ?static separator). - S3: add TransitiveSkip — regresses the fixpoint's transitive static-drop diagnostic (a static caller of a refused callee is dropped and reported). - Add MangleCollisionRefusal — regresses the collision guard (two instance methods colliding both skip; 3 ctors verified, 2 methods skipped).
Self-review cleanups (no behavior change, suite green): - Delete the orphaned 'Transitive-emittability fixpoint' comment left above the collision-guard code after the collision/fixpoint reorder; the actual fixpoint already carries its own accurate comment. - Move the isStatic helper below isNonConstantInstanceField so the latter's Javadoc again directly precedes the method it documents.
Per PLAN.md §12, mark each workaround for a current Strata gap so migration is a grep when Strata catches up: - strata-gap-1 (Strata#1172): the static-call-with-self encoding — the synthesized parameter and the receiver-prepended .StaticCall at the call site; migrate to native obj#method/.InstanceCall. - strata-gap-2 (Strata#1173): @pure methods with postconditions / constrained returns emitted as opaque procedures; let them stay functions once Strata supports it (or functions are removed per #1352). - strata-gap-3 (Strata#1174): refuseIfPolymorphicDispatch; remove once runtime dispatch lands. The Step-8a-deferred refusals (instance-field access, new-receiver, super call) and the contract-allocation refusal already carry explanatory comments naming their follow-up; they are J-side/Strata-lift gaps without a numbered Strata issue, so they get no strata-gap-N marker.
Tighten the comments added across this work and remove pointers a reader of
this repo can't resolve: 'See PLAN.md \xc2\xa7N' (PLAN.md isn't in this repo) and
internal plan-step labels ('Step 8a/8d', 'Step 6', 'Step 3b', '\xc2\xa71'). Keep
the load-bearing rationale and the TODO(strata-gap-N) markers, now anchored
to the Strata issue numbers (#1172/#1173/#1174) which are resolvable. No
behavior change; suite green.
Address the review's request-changes on #392: - SOUNDNESS (false-verify): refuseIfPolymorphicDispatch keyed on whether the callee OVERRIDES a parent (getBase != null), which missed the unsound direction — a non-overriding method that IS overridden by a subclass, called through a base-typed reference, verified against the base contract while the runtime target differs. Refuse unless provably monomorphic (callee final/private or enclosing class final). Regression: PolyDispatchSoundness (bisection-proven — fails on the old logic). - Split VerifyStatements: the verifiable methods stay in a non-skipped class (the @pure P/P2/P3 chain made static so static->static calls aren't subject to the now-broader dispatch refusal); the loop-invariant methods that hit the Strata LoopElim limitation move to a skipped VerifyStatementsLoops. Restores coverage the whole-file skip had dropped. - Diagnostic attribution: set reporter.compilationUnit before reportError in the collision and fixpoint passes, so a dropped method's diagnostic attributes to its own file. Regression: CrossFileTransitiveSkip (multi-file, bisection-proven). - Narrow the line-map fallback to the synthetic <unknown> URI only; restore fail-fast for any other unmapped URI. - Lock intent with methodsSkipped assertions on the re-baselined silent-skip tests; reorder receiverSelf before the dispatch refusal so a fresh-receiver call keeps its specific diagnostic. The broadened dispatch refusal correctly skips more non-monomorphic instance calls; re-baselined methodsVerified/methodsSkipped on the affected fixtures (PolymorphicLambdas, PolymorphicAnonymousClasses, MethodContractsVerification, SameLineAndColumnLambdaA, PureLambda) to honest counts. Suite green.
- Trim the over-written <unknown> line-map fallback comment (13 lines -> 4) and the EmittedProcedure javadoc (it re-explained the fixpoint's symbol-keying that the fixpoint comment already covers). - Fix a stale comment: currentReferencedCallees was described as 'callee mangled names' but holds MethodSymbols since the identity-keying fix. - Lightly tighten the refuseIfPolymorphicDispatch javadoc while keeping the load-bearing 'must NOT be keyed on whether the callee overrides' note that documents the soundness bug not to reintroduce. Comments only; suite green.
CI runs ./gradlew test (all modules); the instance-method re-baseline had only covered :verifier. SourceContract (in :examples) calls foo.foo(2) through the @impure interface Foo — a virtual call now correctly refused as non-monomorphic, so User.test skips. Update the count to 2 verified / 1 skipped (errorCount unchanged). Verified :examples/:test-engine/ :javac-plugin-test/:contracts2jqwik all green locally.
The rebase merged #435's 0-argument-lambda contract handling with this PR's contract-context logic; lambdaInPostcondition now verifies (orthogonal to the dispatch refusal, which targets instance calls — not postcondition lambdas). Update 7->9 verified, 4->3 skipped. Diagnostics still []; suite green.
fabiomadge
force-pushed
the
pr/step3-instance-methods
branch
from
July 2, 2026 19:53
c2053c1 to
27a6697
Compare
Soundness: a skipped user constructor or anonymous/local-class method carrying a real contract was counted Verified but never checked (its Laurel was never emitted, so Strata never saw its obligations). Demote any skipped member to Skipped, except generated implicit constructors (which have no user body and are vacuously verified by convention). Regression: SkippedConstructorContractNotVerified (a false constructor postcondition must Skip, not Verify). Simplify: mangle the enclosing-class/method join with '?' (illegal in a Java identifier) instead of '_', making method-name mangling injective. This removes the whole mangle-collision detection/refusal pass and the EmittedProcedure.mangledName field. MangleCollisionRefusal (which documented the now-impossible collision) becomes MangledNameSeparation, proving Foo_bar.baz and Foo.bar_baz stay distinct and both verify. Also: collapse qualifiedMethodName's unreachable no-enclosing-class fallback into the shared enclosingClassOrRefuse guard; drop the parallel unitsInOrder list (LinkedHashMap keeps unit order); remove a dead reporter.compilationUnit write and an always-true callee-enclClass check; guard the callee enclClass() derefs added during the rebase; and let a plain @unbounded int return stay a transparent (inlinable) function rather than an opaque procedure. Tests: add InstanceMethodVerifies / InstanceMethodContractViolated (the positive happy path and its caught-violation twin) and PureCallResultUsedDirectly / PureCallResultViaUnboundedLocal (a pure-call result is usable directly, or via a local when the local is @unbounded). Re-baseline fixtures whose counts previously baked in the constructor false-Verified.
Comments only, no behavior change: tighten the wordiest blocks (the <unknown> line-map fallback, the skipped-member soundness rationale, the two-pass/clause-threading notes, and two test javadocs) and drop duplicated restatement. ~45 fewer comment lines.
fabiomadge
marked this pull request as ready for review
July 2, 2026 23:52
Contributor
|
Nice Work. Soundness reasoning holds: the polymorphic-dispatch refusal is keyed correctly, Scope: this covers only stateless, monomorphically-reached instance methods. Field access, dispatch through overridable types, constructors, Nit: - |
kadirayk
approved these changes
Jul 16, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Translate instance methods via static-call-with-self: drop the
Flags.STATICgate, add an explicitselffirst parameter, mapthis→self, prepend the receiver at call sites — all lowering to Laurel.StaticCall(never.InstanceCall/.This).Soundness.
selfis an unconstrained, never-dereferenced opaque composite (instance-state access is refused), so it only strengthens obligations, never discharges a false postcondition. Calls are refused unless provably monomorphic (callee/classfinalorprivate): static mangling binds the static type, so an overridable call would verify the wrong contract.PolyDispatchSoundnessguards this (bisection-proven);InstanceMethodVerifies/InstanceMethodContractViolatedshow real contracts verify and violations are caught.No false Verified. A skipped member emits no Laurel but keeps its default
Verifiedentry — so a skipped user constructor or anon/local method with a real contract would readVerifiedunchecked. These are now demoted toSkipped(implicit constructors excepted: no body, vacuously verified). Guarded bySkippedConstructorContractNotVerified.Refused (graceful skip): constructors, anon/local classes, instance fields, polymorphic dispatch, allocation in a contract, overloads. A transitive-emittability fixpoint drops callers of un-emitted methods (across files) so no emitted call is unresolved.
Mangling. Names join class and method with
?(illegal in Java identifiers), so mangling is injective — collisions are impossible and the old collision pass is gone (MangledNameSeparation).@pure. Emitted as an inlinable
function, or an opaqueprocedurewhen it has a postcondition or constrained return (Strata rejects both on afunction). A plain@Unboundedreturn stays a function; its result is usable directly (PureCallResultUsedDirectly) or via an@Unboundedlocal (PureCallResultViaUnboundedLocal).Tests. Affected fixtures re-baselined to honest
methodsVerified/methodsSkippedcounts.VerifyStatementssplit (loop-invariant methods → skippedVerifyStatementsLoops, pending a Strata loop-elim fix). PlusStaticOverloadRefusal,NewReceiverRefusal,NewInLoopInvariantRefusal,TransitiveSkip,CrossFileTransitiveSkip.Workarounds to undo:
grep -rn "TODO(strata-gap-" verifier/src/main/→ gap-1 (#1172 instance methods), gap-2 (#1173 function postconditions), gap-3 (#1174 dispatch). Constructor/anon translation and instance fields skip cleanly meanwhile.Rebased onto
main(#451 crash-guard superseded by #433, already on main). Clean build green, all modules.Closes #420 — translator-skipped members count
Skipped, not silentlyVerified. The broader Verified-by-default design stays tracked in #455.