Skip to content
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

Fix callsite inliner #5395

Closed
wants to merge 11 commits into from
Closed

Conversation

thealmarty
Copy link
Contributor

@thealmarty thealmarty commented Jun 21, 2023

This aims to fix the problem I mentioned in this comment, which will unblock #5385, which currently has a bunch of free uniques errors.

A couple of the UPLC tests failed - I think because they are ill-typed. I would appreciate clarifications on those.

Pre-submit checklist:

  • Branch
    • Tests are provided (if possible)
    • Commit sequence broadly makes sense
    • Key commits have useful messages
    • Changelog fragments have been written (if appropriate)
    • Relevant tickets are mentioned in commit messages
    • Formatting, PNG optimization, etc. are updated
  • PR
    • (For external contributions) Corresponding issue exists and is linked in the description
    • Targeting master unless this is a cherry-pick backport
    • Self-reviewed the diff
    • Useful pull request description
    • Reviewer requested

@@ -129,30 +130,39 @@ fullyApplyAndBetaReduce ::
AppContext tyname name uni fun ann ->
InlineM tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
fullyApplyAndBetaReduce info args0 = do
rhsBody <- liftDupable (let Done rhsBody = varRhsBody info in rhsBody)
let go ::
-- cannot use `liftDupable` here because then the variables will get renamed and we won't be
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The only reason the inliner worked before (even though rhsBody was renamed) is that the body only has free variables, and they are untouched! See Rename.

@@ -1 +1 @@
(lam b_5 [ (lam x_8 (lam y_9 [ (con integer 1) x_8 ])) (con integer 1) ])
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Frankly I don't think these original golden files look right?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's just a weird example that cannot have a sensible type. But we're testing the behavior of the UPLC inliner, so types are irrelevant and we can afford doing weird things. But that's just my guess.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I still don't know what to do/think about these 2 UPLC tests. What do you think I should do @effectfully

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I still don't know what to do/think about these 2 UPLC tests. What do you think I should do @effectfully

They look to me like they expose a bug in your code. So inlinePure3 is

[(\x -> \y -> [x x]) (con integer 1)]

which if spelled in a way readable not only for cylons (and with replacing the immediately applied lambda with a semantically equivalent let) is:

let x = 1
in \y -> x x

What do we expect it to simplify to? Well, there exist options, e.g. this:

\y -> 1 1

or this

let x = 1
in \y -> x 1

or this

let x = 1
in \y -> 1 x

or to stay the same.

In the previous golden test it was

(lam b_5 [ (lam x_8 (lam y_9 [ (con integer 1) x_8 ])) (con integer 1) ])

which if I'm parsing it correctly is

\b ->
  let x = 1
  in \y -> 1 x

where b is garbage added by the testing machinery (precisely, mkInlinePurityTest), i.e. it's one of the reasonable options.

Now in your PR it's

(lam b_5 [ (lam x_8 (lam y_9 (con integer 1))) (con integer 1) ])

which if I'm parsing it correctly is

\b_5 ->
  let x_8 = 1
  in \y_9 -> 1

which doesn't make any sense to me.

I still don't know what to do/think about these 2 UPLC tests. What do you think I should do @effectfully

I think you should communicate clearly what you find weird about these tests and why, because I'm failing to grasp what's going on in this PR in general and I may easily be wrong on what I was able to decipher.

@thealmarty thealmarty marked this pull request as ready for review June 23, 2023 16:22
@thealmarty thealmarty force-pushed the thealmarty/plt-6326-fix-callsite-inliner branch from 4db23c9 to 6f297da Compare June 23, 2023 16:29
@@ -0,0 +1,3 @@
### Fixed

- The callsite inliners used to wrap the function body of a function variable in `Dupable`, making it possible to independently rename the function body, creating free variables. This is now fixed.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand this. Renaming cannot create free variables and it doesn't touch existing ones. Renaming must always produce an alpha-equal thing, so if that is not happening somewhere, it's a major bug.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did you see this comment?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, but I didn't understand it either! :)
I think it's because it's been a long time since I last looked into the inliners and I don't understand them. I'm going to take a look and come back to you.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh actually, you are right, as I found/explained elsewhere, it doesn't touch free variables. The renaming itself doesn't create the free variables. I'll re-phrase.

@@ -498,10 +507,10 @@ inlineSaturatedApp t
fullyApplyAndBetaReduce varInfo args >>= \case
Nothing -> pure t
Just fullyApplied -> do
rhs <- liftDupable (let Done rhs = _varRhs varInfo in rhs)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The renaming of the RHS wasn't done before, because it wasn't an InlineTerm, but I think it should be done.

@effectfully
Copy link
Contributor

I've read up about the callsite inliners and I agree that we need to rename the whole binding, not just the body.

I'll conduct a proper review some time later. Are you blocked, do you need me to review the PR ASAP?

@effectfully effectfully self-requested a review June 26, 2023 22:35
@thealmarty
Copy link
Contributor Author

I've read up about the callsite inliners and I agree that we need to rename the whole binding, not just the body.

I'll conduct a proper review some time later. Are you blocked, do you need me to review the PR ASAP?

Thanks. Not blocked. I can work on other things.

@thealmarty thealmarty force-pushed the thealmarty/plt-6326-fix-callsite-inliner branch from 394b8e8 to a4fd332 Compare July 3, 2023 15:41
@effectfully
Copy link
Contributor

I'd probably refactor the code like this, but do feel free to ignore.

@thealmarty
Copy link
Contributor Author

I'd probably refactor the code like this, but do feel free to ignore.

What's the advantage of this? I'm a little hesitant because we return Maybe in a few other places too so I feel if we do refactor here we'll have to refactor those as well, which is fine, but it's work, so I'd like to know what we're getting.

@effectfully
Copy link
Contributor

What's the advantage of this? I'm a little hesitant because we return Maybe in a few other places too so I feel if we do refactor here we'll have to refactor those as well, which is fine, but it's work, so I'd like to know what we're getting.

Reads better to me, because it reduces the amount of code and indentation. As I said, do feel free to ignore, I fully understand that it's a very subjective thing.

@effectfully
Copy link
Contributor

Is this one ready for another review?

@thealmarty
Copy link
Contributor Author

thealmarty commented Jul 5, 2023

I'm not sure why CI failed (aborted, with log I don't understand), and I'm not sure what to do with the 2 UPLC tests.

Other than these, I'm ready for another review. I've removed some fields from VarInfo as suggested.

I don't think I'll incorporate your refactoring. We can do another PR for the refactoring if desired.

Copy link
Contributor

@effectfully effectfully left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've spent another three hours reviewing this PR and I'm still completely lost. I don't understand what's going on, the description seems to contradict the code and the tests seem to reveal a bug, but then again I have no idea what I'm looking at.

@@ -166,7 +177,7 @@ fullyApplyAndBetaReduce info args0 = do
Term tyname name uni fun ann ->
InlineM tyname name uni fun ann Bool
safeToBetaReduce a = shouldUnconditionallyInline Strict a rhsBody
go rhsBody (varArity info) args0
go rhs varArity args0
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why are you recursing on rhs instead of recursing on rhsBody as before and not introducing the ugly getFnBody?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is how to fix the problem. We cannot separate out just the rhsBody. We take the whole rhs and drop each beta reduced lambda as we go. I'll add more explanation in the code.

rhsBody <- liftDupable (let Done rhsBody = varRhsBody info in rhsBody)
let go ::
-- cannot use `liftDupable` here because then the variables will get renamed and we won't be
-- able to find them to do the substitutions
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So previously we'd rename rhsBody without renaming variables at their binding site, which means they were getting out of sync. However now you rename the entire rhs meaning that those variables bound by LamAbs and TyAbs no longer get out of sync with how they are used. Do we still need to avoid renaming then?

Regardless of the answer please specify what exactly goes wrong if we perform renaming here, what variables at which site we would be no longer able to find etc.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

will do

@@ -0,0 +1,3 @@
### Fixed

- The callsite inliners used to wrap the function *body* of a function variable in `Dupable`, which didn't achieve the desired renaming effect, because it would never be changed. Now the whole RHS is wrapped, and is renamed before inlining.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Now the whole RHS is wrapped, and is renamed before inlining.

Is it like the opposite of what is actually happening in the code?

@@ -180,8 +191,8 @@ inlineSaturatedApp t
Just varInfo ->
fullyApplyAndBetaReduce varInfo args >>= \case
Just fullyApplied -> do
let rhs = varRhs varInfo
-- Inline only if the size is no bigger than not inlining.
rhs <- liftDupable (let Done rhs = varRhs varInfo in rhs)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is this for?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same for in the UPLC inliner. See this comment. I'll add comment to the code too.

@@ -1 +1 @@
(lam b_5 [ (lam x_8 (lam y_9 [ (con integer 1) x_8 ])) (con integer 1) ])
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I still don't know what to do/think about these 2 UPLC tests. What do you think I should do @effectfully

They look to me like they expose a bug in your code. So inlinePure3 is

[(\x -> \y -> [x x]) (con integer 1)]

which if spelled in a way readable not only for cylons (and with replacing the immediately applied lambda with a semantically equivalent let) is:

let x = 1
in \y -> x x

What do we expect it to simplify to? Well, there exist options, e.g. this:

\y -> 1 1

or this

let x = 1
in \y -> x 1

or this

let x = 1
in \y -> 1 x

or to stay the same.

In the previous golden test it was

(lam b_5 [ (lam x_8 (lam y_9 [ (con integer 1) x_8 ])) (con integer 1) ])

which if I'm parsing it correctly is

\b ->
  let x = 1
  in \y -> 1 x

where b is garbage added by the testing machinery (precisely, mkInlinePurityTest), i.e. it's one of the reasonable options.

Now in your PR it's

(lam b_5 [ (lam x_8 (lam y_9 (con integer 1))) (con integer 1) ])

which if I'm parsing it correctly is

\b_5 ->
  let x_8 = 1
  in \y_9 -> 1

which doesn't make any sense to me.

I still don't know what to do/think about these 2 UPLC tests. What do you think I should do @effectfully

I think you should communicate clearly what you find weird about these tests and why, because I'm failing to grasp what's going on in this PR in general and I may easily be wrong on what I was able to decipher.

@thealmarty thealmarty force-pushed the thealmarty/plt-6326-fix-callsite-inliner branch from 8e90f73 to a561da6 Compare July 10, 2023 16:25
@michaelpj
Copy link
Contributor

I'm sceptical that this is the right way to go. Have we looked at the actual buggy output of the inliner in the other PR? I think it's not actually possible for the renamer to make new free variables, so what seems more likely to me is that we're incorrectly dropping some of the binders when we inline the term. That could happen if e.g. we substitute in varBody blindly.

@thealmarty thealmarty force-pushed the thealmarty/plt-6326-fix-callsite-inliner branch from d30d83e to be8b771 Compare July 17, 2023 17:32
@thealmarty thealmarty force-pushed the thealmarty/plt-6326-fix-callsite-inliner branch from be8b771 to 42c968f Compare July 17, 2023 17:46
@thealmarty
Copy link
Contributor Author

Superseded by #5426

@thealmarty thealmarty closed this Jul 21, 2023
@kwxm kwxm deleted the thealmarty/plt-6326-fix-callsite-inliner branch November 10, 2023 09:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants