Transform.runProgram return an extra updated bool result, add analysis cache, and updates to ProcedureInlining#377
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#377Conversation
…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
left a comment
shigoel
left a comment
There was a problem hiding this comment.
Looks great, in general! Thank you.
| match program.filterProcedures procs (transform := CallElim.callElim') with | ||
| let passes := fun prog => do | ||
| let prog ← FilterProcedures.run prog procs | ||
| let (_changed,prog) ← CallElim.callElim' prog |
There was a problem hiding this comment.
Looks very nice!
We can pass in the procedure inlining transform too here, right? Perhaps it makes sense to have the transform to apply be an argument to this function.
There was a problem hiding this comment.
Yes, indeed. :) We can get an option that turns on CallElim or ProcedureInlining depending on which checks to run (assert vs. cover).
| /-- Define the state of transformation in Strata Core. | ||
| It is the duty of the transformation to keep the analysis cache keep the | ||
| correct information after code transformation, or one can simply drop the | ||
| cached result. |
There was a problem hiding this comment.
Said another way, this kinda guarantees that what we have here is an optimization. Right?
There was a problem hiding this comment.
Yes, this is to optimize the implementations of transformations.
…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. | |||
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 |
There was a problem hiding this comment.
| 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. | ||
| -/ |
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. -/ |
There was a problem hiding this comment.
Is this correct for a recursive function (or do we prevent constructing CGs for/inlining recursive functions)?
3 participants
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