-
Notifications
You must be signed in to change notification settings - Fork 3.7k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[compiler-v2] Lambda lifting + first steps towards a pipeline for ast trafo #12318
Conversation
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #12318 +/- ##
========================================
Coverage 63.9% 63.9%
========================================
Files 801 803 +2
Lines 177744 178075 +331
========================================
+ Hits 113629 113945 +316
- Misses 64115 64130 +15 ☔ View full report in Codecov by Sentry. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Any chance we can split the AST pipeline from the lambda lifting?
AST pipeline looks reasonable. Lambda lifting will take more time to review.
@@ -11,3 +11,122 @@ error: Break outside of a loop not supported in function-typed arguments (lambda | |||
│ | |||
40 │ brk2(| | break); | |||
│ ^^^^^ | |||
|
|||
// -- Model dump before bytecode pipeline |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this being dumped after an error? Doing so is dangerous, as model may be not consistent.
} else { | ||
self.env_pipeline.run(&mut env); | ||
ok = Self::check_diags(&mut test_output.borrow_mut(), &env); | ||
if self.dump_ast == AstDumpLevel::EndStage { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Only dump if ok.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You forgot about Assign
statements. See comments below for recognizing free modified variables. Rewriting the lambda body to turn modified variables into &mut ref
parameters may be tricky (but perhaps also kind of fun). I note that an Assign
may set multiple variables, some of them also appearing in the RHS of the Assign
. It's probably wisest to treat free_modified_vars the same as free_vars in the body of the closure and copy them in and out from &mut
params at start and end of the function. (Good thing we don't currently allow return in lambdas.)
I really, really suggest splitting the AST pipeline from the Lambda lifting.
third_party/move/move-compiler-v2/src/env_pipeline/lambda_lifter.rs
Outdated
Show resolved
Hide resolved
third_party/move/move-compiler-v2/src/env_pipeline/lambda_lifter.rs
Outdated
Show resolved
Hide resolved
let mut curr_free_params = mem::take(&mut self.free_params); | ||
let mut curr_free_locals = mem::take(&mut self.free_locals); | ||
let result = self.rewrite_exp_descent(exp); | ||
self.free_params.append(&mut curr_free_params); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Probably better to keep the earlier use, since that way any error about the free var will reference the first use in the code. Easiest just to swap before the append:
mem::swap(&mut self.free_params, &mut curr_free_params);
mem::swap(&mut self.free_locals, &mut curr_free_locals);
though we could use a new var and mem::replace
instead, I think this code is small enough to not allow confusion.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not getting your swap comment. Those vars need to be cleared before descent, then when we return joined back into the result. Its written in the comment above. The swap wont do this.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, yeah. I forgot that BTreeMap::append
overwrites the original.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ack
self.free_locals.retain(|name, _| !exiting.contains(name)); | ||
} | ||
|
||
fn rewrite_local_var(&mut self, id: NodeId, sym: Symbol) -> Option<Exp> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You also need to implement rewrite_pattern
and catch the case matches!(pat, Pattern::Var(id, sym))
and entering_scope=false
and record it in self.free_modified_syms
. You will have to subtract exiting syms from it in rewrite_exit_scope
above, and then do a second rewrite pass to turn all free modified syms into &mut
params and modify all uses to read/write through the references. Note that both Temporary
and Parameter
can show up as a Pattern::Var
, but that's a tiny part of the problem.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good catch, but I'm not going for this complexity, at least for now. When a variable is assigned to our mutably borrowed, I produce now an error.
This is similar as in Java and C# lambdas, and I think C++ has this too. We may go back and make this more powerful, but lets start simple here. Indeed, for inlined lambdas this restriction doesn't exist, but they also have other stuff which can be done which can't be in a regular lambda.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok, then you need an error in this case. Ok, see it.
I forgot to note that occurrences of free vars (of both types: Index and Symbol) in a mutable But this is sounding even harder to implement, even if we could have refs in tuples and could represent a pointer to a |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you, PTAL
let mut curr_free_params = mem::take(&mut self.free_params); | ||
let mut curr_free_locals = mem::take(&mut self.free_locals); | ||
let result = self.rewrite_exp_descent(exp); | ||
self.free_params.append(&mut curr_free_params); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not getting your swap comment. Those vars need to be cleared before descent, then when we return joined back into the result. Its written in the comment above. The swap wont do this.
self.free_locals.retain(|name, _| !exiting.contains(name)); | ||
} | ||
|
||
fn rewrite_local_var(&mut self, id: NodeId, sym: Symbol) -> Option<Exp> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good catch, but I'm not going for this complexity, at least for now. When a variable is assigned to our mutably borrowed, I produce now an error.
This is similar as in Java and C# lambdas, and I think C++ has this too. We may go back and make this more powerful, but lets start simple here. Indeed, for inlined lambdas this restriction doesn't exist, but they also have other stuff which can be done which can't be in a regular lambda.
third_party/move/move-compiler-v2/src/env_pipeline/lambda_lifter.rs
Outdated
Show resolved
Hide resolved
third_party/move/move-compiler-v2/src/env_pipeline/lambda_lifter.rs
Outdated
Show resolved
Hide resolved
let mut curr_free_params = mem::take(&mut self.free_params); | ||
let mut curr_free_locals = mem::take(&mut self.free_locals); | ||
let result = self.rewrite_exp_descent(exp); | ||
self.free_params.append(&mut curr_free_params); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, yeah. I forgot that BTreeMap::append
overwrites the original.
self.free_locals.retain(|name, _| !exiting.contains(name)); | ||
} | ||
|
||
fn rewrite_local_var(&mut self, id: NodeId, sym: Symbol) -> Option<Exp> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok, then you need an error in this case. Ok, see it.
env.error( | ||
&loc, | ||
&format!( | ||
"captured parameter `{}` cannot be modified inside of a lambda", |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You should probably also call this a "captured variable" here, since parameters can appear in an Assign
expression as a symbol and will be treated as a local. Determining whether the Assign
symbol is a parameter or not requires tracking var scoping outside of the lambda, so probably isn't worth it. Easier to just change the error message to be consistent.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
c0cd2dc
to
472a1e1
Compare
Addressed for now by error message. PTAL |
7815551
to
d9847a1
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Mostly minor comments.
/// Represents a pipeline of processors working on the global environment. | ||
#[derive(Default)] | ||
pub struct EnvProcessorPipeline<'a> { | ||
/// A sequence of transformations to run on the model. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
/// A sequence of transformations to run on the model. | |
/// A sequence of transformations to run on the model. | |
/// For each processor, we store its name and the transformation function. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
|
||
impl<'a> EnvProcessorPipeline<'a> { | ||
/// Adds a processor to the pipeline. | ||
pub fn add<P>(&mut self, name: &str, processor: P) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice, I think we can do this style of generics for stackless bytecode add_processor
as well, and reduce quite a bunch of code!
Not an action item for this PR, I can do it as a follow up refactoring once this lands.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The stackless processors are significantly more expressive via their trait, I was just to lazy to introduce a trait here.
But we can build an adapter for a processor which wraps a function and makes it easier to create.
} | ||
|
||
/// Runs the pipeline. Running will be ended if any of the steps produces an error. | ||
/// The function returns true of all steps succeeded without errors. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
/// The function returns true of all steps succeeded without errors. | |
/// The function returns true if all steps succeeded without errors. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
@@ -1314,6 +1314,7 @@ impl<'a> ExpRewriterFunctions for ExpRewriter<'a> { | |||
pub enum Operation { | |||
MoveFunction(ModuleId, FunId), | |||
SpecFunction(ModuleId, SpecFunId, Option<Vec<MemoryLabel>>), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
move SpecFunction
to below the comment // Specification specific
(while not related to the change in the PR, it is an easy fix, hence suggested).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Closure
should also be in the "Spec only" section.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
enum AstDumpLevel { | ||
#[default] | ||
None, | ||
EndStage, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
EndStage, | |
EndStage, // only dump model AST after running all stages of env processor pipeline. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is the AST operation which does not have this section, its also not that easy because there is 75% overlap.
function_checker::check_access_and_use(&mut env, false); | ||
ok = Self::check_diags(&mut test_output.borrow_mut(), &env); | ||
// Run env processor pipeline. | ||
if self.dump_ast == AstDumpLevel::AllStages { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We may eventually want to selectively dump stages, but I am ok implementing that when we have a concrete usecase.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
SG
result_type: Type, | ||
def: Exp, | ||
) { | ||
let called_funs = def.called_funs(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would we want to extend called_funs()
to include closures that can be called as well (it is currently limited to move functions called)? Or maybe we expect this to be implemented when full support for lambda is added?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually a good catch, I added this now to called_funs()
so it is not forgotten.
} | ||
} | ||
// Now that we have processed all functions and released | ||
// al references to the env, mutate it. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
// al references to the env, mutate it. | |
// all references to the env, mutate it. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
/// Any unbound locals used so far. | ||
free_locals: BTreeMap<Symbol, VarInfo>, | ||
/// NodeId's of lambdas which are parameters to inline functions | ||
/// if those should be exempted. Pushed down during descend. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
exempted from what? (document)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
exempted from lambda lifting. Clarified.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It would be good if we could have single-purpose PRs.
The lambda change still needs more scrutiny and tests (e.g., nested lambdas, proper errors with mutation constructs), but as it's disabled by default it's probably ok to commit as is.
//! | ||
//! - Inside of specification expressions; | ||
//! - For a lambda argument of a regular (not inline) function | ||
//! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
//! - For a lambda without side-effects to free variables
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
@@ -1314,6 +1314,7 @@ impl<'a> ExpRewriterFunctions for ExpRewriter<'a> { | |||
pub enum Operation { | |||
MoveFunction(ModuleId, FunId), | |||
SpecFunction(ModuleId, SpecFunId, Option<Vec<MemoryLabel>>), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Closure
should also be in the "Spec only" section.
@@ -1,4 +1,4 @@ | |||
// ---- Model Dump | |||
// -- Model dump before bytecode pipeline |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure it was useful to change this message, as it's clearly the final Model.
… trafo This implements lambda lifting as rewrite on `GlobalEnv`. Lambda lifting appeared necessary for prover connection, because this is how the v1 integration works. Its not that clear any longer whether lambda lifting is really needed, but now the work is done, and we shoukd preseve it for future general support of HOFs. As this is now the 5th or so so transformation on the environment before the bytecode pipeline starts. to support this adequate in the test suite, there is also a first step towards an `EnvProcessorPipeline`, and a new submodule `env-pipeline` which should contain those processors. For now it is just lambda lifting.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the reviews.
It would be good if we could have single-purpose PRs.
Actually I think we are more productive if we refactor this code on the fly while we develop new features. But it also depends on the particular use case. Here the new pipeline is a triviality compared to the rest of the PR, larger refactorings would be a different story.
The lambda change still needs more scrutiny and tests (e.g., nested lambdas, proper errors with mutation constructs), but as it's disabled by default it's probably ok to commit as is.
Added a test for nesting.
//! | ||
//! - Inside of specification expressions; | ||
//! - For a lambda argument of a regular (not inline) function | ||
//! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
let mut curr_free_params = mem::take(&mut self.free_params); | ||
let mut curr_free_locals = mem::take(&mut self.free_locals); | ||
let result = self.rewrite_exp_descent(exp); | ||
self.free_params.append(&mut curr_free_params); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ack
@@ -1314,6 +1314,7 @@ impl<'a> ExpRewriterFunctions for ExpRewriter<'a> { | |||
pub enum Operation { | |||
MoveFunction(ModuleId, FunId), | |||
SpecFunction(ModuleId, SpecFunId, Option<Vec<MemoryLabel>>), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
✅ Forge suite
|
✅ Forge suite
|
This implements lambda lifting as rewrite on
GlobalEnv
. Lambda lifting appeared necessary for prover connection, because this is how the v1 integration works. It's not that clear any longer whether lambda lifting is really needed, but now the work is done, and we should preserve it for future general support of HOFs.As this is now the 5th or so so transformation on the environment before the bytecode pipeline starts. to support this adequate in the test suite, there is also a first step towards an
EnvProcessorPipeline
, and a new submoduleenv-pipeline
which should eventually contain those processors. For now it is just lambda lifting.