Transform.runProgram return an extra updated bool result, add analysis cache, and updates to ProcedureInlining#377
Open
aqjune-aws wants to merge 21 commits intomainfrom
Open
Transform.runProgram return an extra updated bool result, add analysis cache, and updates to ProcedureInlining#377aqjune-aws wants to merge 21 commits intomainfrom
Transform.runProgram return an extra updated bool result, add analysis cache, and updates to ProcedureInlining#377aqjune-aws wants to merge 21 commits intomainfrom
Conversation
…Cmd's doInline fn
…porarily comment proofs in CallElim
… TransformState to track the current (input) program
aqjune-aws
force-pushed
the
jlee/inline-planner
branch
from
651899b to
93baba8
Compare
aqjune-aws
changed the title
Transform.runProgram return an extra updated bool result, add analysis cache, and updates to ProcedureInlining
shigoel
reviewed
Feb 5, 2026
Contributor
shigoel
left a comment
shigoel
left a comment
There was a problem hiding this comment.
Looks great, in general! Thank you.
…to jlee/inline-planner
| @@ -418,7 +420,13 @@ def verify (smtsolver : String) (program : Program) | |||
| -- Verify specific procedures. By default, we apply the call elimination | |||
| -- transform to the targeted procedures to inline the contracts of any | |||
| -- callees. | |||
Contributor
There was a problem hiding this comment.
Can we clarify "apply call elim"? Specifically, I could imagine it's applied once, vs until fixpoint vs until we reach a procedure not in this list vs max N.
| def CachedAnalyses.emp : CachedAnalyses := {} | ||
|
|
||
| /-- Define the state of transformation in Strata Core. | ||
| It is the duty of the transformation to keep the analysis cache keep the |
Contributor
There was a problem hiding this comment.
Suggested change
| It is the duty of the transformation to keep the analysis cache keep the | |
| It is the duty of the transformation to update the analysis cache to keep the |
| Visit all procedures and run f | ||
| NOTE: please use runProgram if possible since CoreTransformState might result | ||
| in an inconsistent state. This function is for partial implementation. | ||
| -/ |
Contributor
There was a problem hiding this comment.
Maybe document that the Bool in Bool \times List Decl corresponds to changed (or better make a struct for the return value)?
| return ({ c with body := new_body, header := new_header }, var_map) | ||
|
|
||
|
|
||
| /-- Update the call graph after inlining one f(caller) -> g(callee) invocation. -/ |
Contributor
There was a problem hiding this comment.
Is this correct for a recursive function (or do we prevent constructing CGs for/inlining recursive functions)?
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
3 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 of changes:
Transform.runProgramnow returns(updated, new program), and receives an extra optional argallowProcList : Option (List String)that makes the transformation only run on specific procedures.The goal of this change is to allow the user iteratively apply the transformation to the specific procedure (e.g., the "main" function) until there is no change anymore.
doInlinefn to Procedure Inlining, let CoreTransformState cache the result of expensive analysis like CallGraph construction.In this patch, ProcedureInlining.inlineCallCmd takes a more generic lambda function
doInlinethat receives the calling procedure name as well as the CallGraph data structure and decide whether to inline or not.Since building CallGraph every time is expensive, CallGraph is incrementally updated after each inlining.
To keep the latest status of CallGraph, we have a new
CoreTransformStatedatatype which tracks analyses cache, and it is the transformation's responsibility that must invalidate or correctly update the cache. This mimics what LLVM's passes do.From the CallGraph, you can check whether e.g., there is only one caller of some procedure or not.
Also, since we have
CoreTransformState, more cleaups to the signatures of transformation functions were possible. The transformation passes were originally taking an extra sourceProgramargument that was being transformed, but this was awkward because transformations are defined at the Statement level. This removes the extra argument, and makesCoreTransformStatetrack the currently modifying Program and Procedure.Program.filterProceduresfunction is extracted out as a new transformation calledFilterProcedure.The new
Program.filterProceduresintroduced in #375 was extracted out toFilterProcedurebecause I thought that the correctness of thisFilterProcedurecan be very nicely described. :) To address the comment that I left in the pull request, I madeFilterProcedurea standalone transform that is not parameteric to other transformations.Also, there is performance win - combined with the AnalysisCache, now CallGraph is calculated inside
FilterProcedureonce, reused inProcedureInlining, then reused in the secondFilterProcedure!Also, the proofs in CallElimCorrect is commentized even more.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
@thanhnguyen-aws