Optimization refactoring: VarsInfo and BuiltinsInfo, pure conapps #5551

michaelpj · 2023-09-20T10:18:22Z

This is some preparatory refactoring for doing case-of-case:

Add a generic VarsInfo pass that collects information about PIR variables, such as strictness, arity, and whether they are constructors/matchers.
- This sets us up to use this information to do case-of-case generically.
Adds a BuiltinsInfo type that (for now) just contains the semantics variant, to hold user-provided information about builtins.
- We'll want to add more information about builtins in order to know that e.g. ifThenElse is a matcher-like function that should participate in case-of-case.
Use these throughout
- This includes using them in some places that previously weren't handling variable strictness.
Demonstrate the utility by using the new info to consider constructor applications to be pure

The actual optimization changes come from making more passes use variable info (which they should!) and making conapps pure (which they are!). It's a bit of a wash: some things are a little better, some things are a little worse, but the PIR looks better to me, and I think it's better to have accurate information.

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

michaelpj · 2023-09-20T10:19:27Z

plutus-benchmark/nofib/test/formulaBudget.pir-readable.golden

@@ -39,7 +39,7 @@
    !equalsInteger : integer -> integer -> Bool
      = \(x : integer) (y : integer) ->
          ifThenElse {Bool} (equalsInteger x y) True False
-    ~`$fOrdInteger` : Ord integer
+    !`$fOrdInteger` : Ord integer


Now we know that the dictionary constructor is pure, so it's safe to strictify this!

michaelpj · 2023-09-20T10:20:01Z

plutus-benchmark/nofib/test/formulaBudget.pir-readable.golden

@@ -312,62 +312,63 @@
  in
  let
    ~`$dOrd` : Ord (List integer)
-      = let
-        !v : Ord integer = `$fOrdInteger`


this got inlined thanks to the above strictification

michaelpj · 2023-09-20T10:21:21Z

plutus-benchmark/nofib/test/formulaBudget.pir-readable.golden

-                              in
-                              Eqv (Sym 1) dt)
-                              dt)
+                              (Eqv (Sym 1) (Sym 1))


All these conapps were pure and singly used, so we inline lots here

michaelpj · 2023-09-20T10:21:52Z

plutus-benchmark/script-contexts/test/checkScriptContext1.pir-readable.golden

-                        !arg : data
-                          = headList {data} (sndPair {integer} {list data} tup)
-                      in
-                      Finite {a} (`$dUnsafeFromData` arg))


Now we know that Finite is strict, so arg is the first possibly-effectful thing evaluated here, so we can inline it!

michaelpj · 2023-09-20T10:22:21Z

plutus-tx-plugin/test/Budget/9.2/allEmptyList.pir-readable.golden

-let
-  !eta : List integer = Nil {integer}
-in
-go eta


first-effectful-term firing again

michaelpj · 2023-09-20T10:22:45Z

plutus-tx-plugin/test/Budget/9.2/applicative.pir-readable.golden

-     /\dead ->
-       Maybe_match
-         {integer}
-         y


y is singly used and now known to be pure, so we inline and COKC fires!

plutus-core/plutus-core/src/PlutusCore/Core/Type.hs

zliu41 · 2023-09-21T18:10:49Z

plutus-core/plutus-ir/src/PlutusIR/Analysis/VarInfo.hs

+  | DatatypeTyVar { dtNumTyVars :: Int, dtConstructors :: [name] }
+
+data VarInfo tyname name =
+  NormalVar { varStrictness :: Strictness, varArity :: Maybe Arity }


Can we do without these partial field accessors?

The pattern matching is much nicer with them... Wish we could drop 8.10 so I can use NoFieldSelectors... but sure

plutus-core/plutus-ir/src/PlutusIR/Purity.hs

zliu41 · 2023-09-21T18:23:07Z

plutus-core/plutus-ir/src/PlutusIR/Purity.hs

+        -- in this case!
+        (splitApplication -> (h@(Var _ n), args))
+          | Just (DatatypeConstructor{}) <- lookupVarInfo n vinfo ->
+            evalThis (EvalTerm Pure MaybeWork h)


Why MaybeWork? Does a constructor application do any non-trivial work?

Unclear - I'm generally unclear on what "work free" should actually mean. At the moment the only things that are "work free" are immediately returning a value, which a constructor application certainly does not do.

Oh, I thought h is the whole constructor application. If it is the head - the constructor itself, then shouldn't it always be WorkFree?

Also, shouldn't there be an evalThis (EvalTerm Pure MaybeWork t) after goAppCtx args? Because t is the constructor application, and t may not be workfree like you said.

Btw, Unknown seems redundant - can we use EvalTerm Impure MaybeWork in place of Unknown?

Also, shouldn't there be an evalThis (EvalTerm Pure MaybeWork t) after goAppCtx args?

Nvm about this, I see you just added it!

If it is the head - the constructor itself, then shouldn't it always be WorkFree?

Unsure: this is the same as we do for variables. Is accessing a variable work-free? You have to look it up... maybe that counts as work? IDK, I just stuck to what was there.

Btw, Unknown seems redundant - can we use EvalTerm Impure MaybeWork in place of Unknown?

Yes, that would be a slightly different way of looking at it. Unknown has two purposes: it tells us that the evaluation goes somewhere unknown, which lets us distinguish terms for which we can see the whole evaluation order with ones where we actually just don't know what happens. If we only care about purity/work, then we can approximate that with "something that is maybe impure and does work", but I think it's kind of nice to say that it's an unknown jump. Also, it's what we use to terminate the traversal: we don't do any more stuff after we hit an Unknown, which is what stops us traversing the whole term in that case.

Although even if we didn't stop the traversal, if we were lazy enough then EvalTerm Impure MaybeWork should stop isPure and isWorkFree, so those should not traverse the whole term. Not sure, maybe that would be better 🤔

zliu41 · 2023-09-21T18:26:14Z

plutus-core/plutus-ir/src/PlutusIR/Analysis/VarInfo.hs

+
+data VarInfo tyname name =
+  NormalVar { varStrictness :: Strictness, varArity :: Maybe Arity }
+  | DatatypeConstructor { dcArity :: Arity , dcParentTyname :: tyname }


Need some Haddock explaining what the "parent" of a constructor or a matcher means.

If I get rid of the field names it will be even more obscure :(

Added haddock anyway

zliu41

LGTM.

) * Add VarInfo pass, use it everywhere * Add BuiltinsInfo type, use it everywhere * Strictify bindings uses VarsInfo * LetFloatOut uses VarsInfo * ThunkRecursions uses VarsInfo * LetFloatIn uses VarsInfo * Conapps are pure * Changelog * Update 9.6 test output * Fix pir * More fixups?? * Comments

…tersectMBO#5551) * Add VarInfo pass, use it everywhere * Add BuiltinsInfo type, use it everywhere * Strictify bindings uses VarsInfo * LetFloatOut uses VarsInfo * ThunkRecursions uses VarsInfo * LetFloatIn uses VarsInfo * Conapps are pure * Changelog * Update 9.6 test output * Fix pir * More fixups?? * Comments

michaelpj requested review from bezirg and zliu41 September 20, 2023 10:18

michaelpj commented Sep 20, 2023

View reviewed changes

michaelpj force-pushed the mpj/varinfo branch from f5fcf25 to d937cb1 Compare September 20, 2023 16:16

michaelpj mentioned this pull request Sep 21, 2023

PLT-506: Case-of-case #5554

Merged

11 tasks

zliu41 reviewed Sep 21, 2023

View reviewed changes

michaelpj added 12 commits September 22, 2023 11:50

Add VarInfo pass, use it everywhere

b5cae39

Add BuiltinsInfo type, use it everywhere

c2f8e63

Strictify bindings uses VarsInfo

d5b9d55

LetFloatOut uses VarsInfo

cca9b34

ThunkRecursions uses VarsInfo

0719c76

LetFloatIn uses VarsInfo

752df5c

Conapps are pure

a26baea

Changelog

58c2774

Update 9.6 test output

c4894c1

Fix pir

1f9701c

More fixups??

00d1718

Comments

dded1b8

michaelpj force-pushed the mpj/varinfo branch from e77e1df to dded1b8 Compare September 22, 2023 11:29

zliu41 approved these changes Sep 22, 2023

View reviewed changes

michaelpj merged commit b8917a0 into master Sep 22, 2023

michaelpj deleted the mpj/varinfo branch September 22, 2023 16:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Optimization refactoring: VarsInfo and BuiltinsInfo, pure conapps #5551

Optimization refactoring: VarsInfo and BuiltinsInfo, pure conapps #5551

michaelpj commented Sep 20, 2023

michaelpj Sep 20, 2023

michaelpj Sep 20, 2023

michaelpj Sep 20, 2023

michaelpj Sep 20, 2023

michaelpj Sep 20, 2023

michaelpj Sep 20, 2023

zliu41 Sep 21, 2023

michaelpj Sep 22, 2023

zliu41 Sep 21, 2023

michaelpj Sep 22, 2023

zliu41 Sep 22, 2023

zliu41 Sep 22, 2023

michaelpj Sep 22, 2023

michaelpj Sep 22, 2023

zliu41 Sep 21, 2023

michaelpj Sep 22, 2023

michaelpj Sep 22, 2023

zliu41 left a comment

Optimization refactoring: VarsInfo and BuiltinsInfo, pure conapps #5551

Optimization refactoring: VarsInfo and BuiltinsInfo, pure conapps #5551

Conversation

michaelpj commented Sep 20, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zliu41 left a comment

Choose a reason for hiding this comment