Fix: pure function body lost in modular verification#74
Open
Fix: pure function body lost in modular verification#74
Conversation
…dular verification of a method
jesyspa
requested changes
Mar 18, 2026
...er.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/ProgramConverter.kt
Outdated
Show resolved
Hide resolved
...er.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/ProgramConverter.kt
Outdated
Show resolved
Hide resolved
…aligned branches for pure and non-pure functions
jesyspa
requested changes
Mar 21, 2026
| } | ||
| embedPureUserFunction(declaration.symbol, signature) | ||
| } else { | ||
| val returnTarget = returnTargetProducer.getFresh(signature.callableType.returnType) |
Collaborator
There was a problem hiding this comment.
This code fragment looks duplicated, am I missing something?
Collaborator
Author
There was a problem hiding this comment.
I've merged your PR and resolved it.
...er.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/ProgramConverter.kt
Outdated
Show resolved
Hide resolved
## Summary - Extracts `createBodyConversionContext` helper to eliminate duplicated creation of `ReturnTarget`, `RootParameterResolver`, and `StmtConversionContext` between `registerForVerification` (non-pure branch) and `embedPureUserFunction`. - Net reduction of ~10 lines; both call sites now delegate to the shared helper. ## Test plan - [x] `./gradlew :formver.compiler-plugin:compileKotlin` passes - [x] `./gradlew :formver.compiler-plugin:test --tests "*Pure*"` passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
jesyspa
requested changes
Apr 9, 2026
| symbol: FirFunctionSymbol<*>, | ||
| signature: FullNamedFunctionSignature | ||
| ): PureUserFunctionEmbedding { | ||
| // Return if already registered |
Collaborator
There was a problem hiding this comment.
This comment is not helpful, please remove it.
| val new = PureUserFunctionEmbedding(processCallable(symbol, signature)) | ||
| // Insert into the map before processing the body, so recursive calls can find the embedding. | ||
| functions[signature.name] = new | ||
| val declaration = symbol.fir as? FirSimpleFunction |
Collaborator
There was a problem hiding this comment.
What is the desired behaviour if this cast fails?
Collaborator
Author
There was a problem hiding this comment.
The cast would fail when symbol is not a FirSimpleFunction, but we allow the @Pure annotation only on normal functions. So if I understand correctly, this should never occur, but it could fail silently. Should I throw an error here for safety?
Collaborator
There was a problem hiding this comment.
Yes, if the case cannot happen please throw an exception.
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.
Description:
When a @pure function B is called from within another function A that is being verified, its Viper function body was missing from the generated program. The verifier could only reason about B via its pre- and postconditions, which limited the usage of pure functions.
Suspected Cause:
The
PureUserFunctionEmbeddingcan be generated in two different ways, either by callingregisterForVerification(triggered when the function itself was verified; generated the body) or by callingembedPureFunction(triggered when the function was called in the specifications or body of another function/method; did not generate the body).Without the body, Viper's function inlining did not work, leading to the verification limitations.
Fix:
Changes in
ProgramConverter.kt:convertAndSetPureBodyhelper: converts and registers the body of a pure functionembedPureFunction: triggers the new helper functionregisterForVerification: also triggers the new helper functionNote: I am not entirely sure if the implementation of the helper function satisfies our code requirements, please verify this.