Skip to content

Fix incoherent CallGraph build in ProcedureInlining#931

Merged
shigoel merged 10 commits intomainfrom
jlee/cachetest
Apr 17, 2026
Merged

Fix incoherent CallGraph build in ProcedureInlining#931
shigoel merged 10 commits intomainfrom
jlee/cachetest

Conversation

@aqjune-aws
Copy link
Copy Markdown
Contributor

CallGraph is stored in CachedAnalyses of the Core transformation monad state (CoreTransformState), and it is supposed to be correctly incrementarily updated during transformations (e.g., when call is eliminated, etc). However, ProcedureInlining was incorrectly updating this.

The reason was as follows: the CachedAnalyses is (correctly) eagerly updated after every call is inlined, whereas the program that ProcedureInlining was actually using was not being updated. ProcedureInlining is supposed to look at the intermediate program after inlinings are happened, because that is exactly the program that CachedAnalyses stores for.

In theory, this can make ProcedureInlining more aggressive: if f1 is calling f2 and f2 is calling f3 and f3 is calling f4,

  • After this patch: during one round of ProcedureInlining, if f2 -> f3 in f2 happened to be inlined first, inlining f1->f2 will see the latest update and introduce f1->f4
  • Before this patch: one round of ProcedureInlining of f1->f2 would have always introduced f1->f3 because ProcedureInlining always saw the "old" program.

However, in practice, this doesn't matter because we are using the 'roots' mode during bugFinding (and ProcedureInlining is only called from bugFinding mode) and calls whose callers are the roots are only of concerns.

Issue #, if available:

Description of changes:

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

CallGraph is stored in CachedAnalyses of the Core transformation monad state (CoreTransformState), and it is supposed to be correctly incrementarily updated during transformations (e.g., when call is eliminated, etc).
However, ProcedureInlining was incorrectly updating this.

The reason was as follows: the CachedAnalyses is (correctly) eagerly updated after every call is inlined, whereas the program that ProcedureInlining was actually using was not being updated.
ProcedureInlining is supposed to look at the intermediate program after inlinings are happened, because that is exactly the program that CachedAnalyses stores for.

In theory, this can make ProcedureInlining more aggressive: if f1 is calling f2 and f2 is calling f3 and f3 is calling f4,
* After this patch: during one round of ProcedureInlining, if f2 -> f3 in f2 happened to be inlined first, inlining f1->f2 will see the latest update and introduce f1->f4
* Before this patch: one round of ProcedureInlining of f1->f2 would have always introduced f1->f3 because ProcedureInlining always saw the "old" program.

However, in practice, this doesn't matter because we are using the 'roots' mode during bugFinding (and ProcedureInlining is only called from bugFinding mode) and calls whose callers are the roots are only of concerns.
@aqjune-aws aqjune-aws requested a review from a team April 15, 2026 19:39
Comment thread Strata/Languages/Core/CallGraph.lean Outdated
Comment thread Strata/Transform/CoreTransform.lean
Comment thread Strata/Transform/CoreTransform.lean
Comment thread Strata/Transform/CoreTransform.lean
Comment thread StrataTest/Transform/ProcedureInlining.lean Outdated
Comment thread Strata/Languages/Core/CallGraph.lean
Comment thread Strata/Transform/CoreTransform.lean
Comment thread Strata/Transform/CoreTransform.lean
@shigoel shigoel enabled auto-merge April 17, 2026 02:04
@shigoel shigoel added this pull request to the merge queue Apr 17, 2026
Merged via the queue into main with commit 42a954f Apr 17, 2026
17 checks passed
@shigoel shigoel deleted the jlee/cachetest branch April 17, 2026 02:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants