fix: prevent infinite loop when modifies clause references non-composite type (#490)#731
Merged
MikaelMayer merged 16 commits intomainfrom Apr 3, 2026
Merged
Conversation
…490) When a procedure has a modifies clause referencing a non-composite type (e.g., a global variable of type int), the heap parameterization pass incorrectly treated the procedure as heap-modifying, and the modifies clause transformation generated invalid frame conditions comparing Composite objects to primitive types. Fix by filtering out non-composite modifies entries in two places: - HeapParameterization: filter before heap analysis so non-composite modifies entries don't trigger heap parameterization - ModifiesClauses: filter in extractModifiesEntries so only Composite and Set types generate frame conditions
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
keyboardDrummer
requested changes
Apr 1, 2026
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
This comment was marked as resolved.
This comment was marked as resolved.
…lication, add regression test - HeapParameterization now emits diagnostic errors for non-composite modifies entries instead of silently filtering them - Introduced classifyModifiesType in ModifiesClauses to eliminate duplication between isHeapRelevantType and extractModifiesEntries - Added T8_NonCompositeModifies regression test for issue #490
tautschnig
reviewed
Apr 2, 2026
…yModifiesHighType
This comment was marked as resolved.
This comment was marked as resolved.
keyboardDrummer
previously requested changes
Apr 2, 2026
…difiesClauses Address review feedback: keep HeapParameterization agnostic to modifies clauses by moving the non-composite modifies filtering and diagnostics into a new filterNonCompositeModifies function in ModifiesClauses.lean. This function runs before heap parameterization in the pipeline.
tautschnig
approved these changes
Apr 3, 2026
joscoh
approved these changes
Apr 3, 2026
MikaelMayer
deleted the
issue-490-laurelanalyze-infinite-loop-when-procedu
branch
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
4 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.
Problem
strata laurelAnalyzeenters an infinite loop (emitting PANIC messages and consuming unbounded memory) when a Laurel program contains a procedure with amodifiesclause referencing a non-composite type, such as a parameter of typeint.The root cause is that the heap parameterization pass treats any procedure with a non-empty
modifieslist as heap-modifying, regardless of the types in the list. When the modifies list contains a non-composite type, the modifies clause transformation generates invalid frame conditions, leading to downstream failures.Fix
Single source of truth:
ModifiesTypeKindenum andclassifyModifiesHighTypeinLaurelTypes.leanserve as the canonical type classification for modifies clauses. BothisHeapRelevantTypeandclassifyModifiesTypedelegate to it.Separation of concerns: Non-composite modifies filtering and diagnostics live in
ModifiesClauses.lean(filterNonCompositeModifies), keeping the heap parameterization phase agnostic to modifies clauses. The filtering runs as a pre-pass before heap parameterization in the pipeline.Error reporting: Non-composite modifies entries produce a diagnostic error (e.g.
modifies clause entry has non-composite type 'int' and will be ignored) instead of being silently filtered.Testing
All existing tests pass. Added a regression test (
T8_NonCompositeModifies) that verifies procedures with non-composite modifies entries terminate and produce the expected diagnostic errors.Fixes #490