Merge branch 'master' of github.com:input-output-hk/plutus into zliu4…

…1/app-inline-uplc
IntersectMBO · May 26, 2023 · 0a20e6f · 0a20e6f
2 parents b3b258a + e2f664e
commit 0a20e6f
Show file tree

Hide file tree

Showing 29 changed files with 389 additions and 339 deletions.
diff --git a/.github/workflows/check-changelog.yml b/.github/workflows/check-changelog.yml
@@ -11,7 +11,7 @@ jobs:
 
       - name: Find Changed Files in changelog.d
         id: changed-files
-        uses: tj-actions/changed-files@v35
+        uses: tj-actions/changed-files@v36
         with:
           files: '**/changelog.d/**'
 

diff --git a/.github/workflows/script-evaluation-test.yml b/.github/workflows/script-evaluation-test.yml
@@ -19,11 +19,9 @@ jobs:
         uses: actions/checkout@v3.3.0
 
       - name: Quick Install Nix
-        uses: nixbuild/nix-quick-install-action@v22
+        uses: cachix/install-nix-action@v21
         with:
-          # 2.14.1 seems to have issues, see https://github.com/nixbuild/nix-quick-install-action/issues/29
-          nix_version: '2.13.3'
-          nix_conf: |
+          extra_nix_config: |
             experimental-features = nix-command flakes
             accept-flake-config = true
 

diff --git a/plutus-benchmark/nofib/test/Spec.hs b/plutus-benchmark/nofib/test/Spec.hs
@@ -95,7 +95,7 @@ testQueens = testGroup "queens"
                , runTestNested    $ Tx.goldenBudget "queens5budget" $
                   Queens.mkQueensCode 5 Queens.Bt
                ]
-             , Tx.fitsInto "Bt (size)" (Queens.mkQueensCode 5 Queens.Bt) 1943
+             , Tx.fitsInto "Bt (size)" (Queens.mkQueensCode 5 Queens.Bt) 1939
              ]
 
 ---------------- Primes ----------------

diff --git a/plutus-benchmark/script-contexts/test/Spec.hs b/plutus-benchmark/script-contexts/test/Spec.hs
@@ -20,7 +20,7 @@ testCheckSc1 = testGroup "checkScriptContext1"
         runTermCek $ compiledCodeToTerm $ mkCheckScriptContext1Code (mkScriptContext 4)
     , testCase "fails on 5" $ assertBool "evaluation succeeded" $ isEvaluationFailure $
         runTermCek $ compiledCodeToTerm $ mkCheckScriptContext1Code (mkScriptContext 5)
-    , Tx.fitsInto "checkScriptContext1 (size)" (mkCheckScriptContext1Code (mkScriptContext 1)) 2032
+    , Tx.fitsInto "checkScriptContext1 (size)" (mkCheckScriptContext1Code (mkScriptContext 1)) 1963
     , runTestNested $ Tx.goldenBudget "checkScriptContext1-4" $
         mkCheckScriptContext1Code (mkScriptContext 4)
     , runTestNested $ Tx.goldenBudget "checkScriptContext1-20" $
@@ -33,7 +33,7 @@ testCheckSc2 = testGroup "checkScriptContext2"
           runTermCek $ compiledCodeToTerm $ mkCheckScriptContext2Code (mkScriptContext 4)
     , testCase "succeed on 5" $ assertBool "evaluation failed" $ isEvaluationSuccess $
           runTermCek $ compiledCodeToTerm $ mkCheckScriptContext2Code (mkScriptContext 5)
-    , Tx.fitsInto "checkScriptContext2 (size)" (mkCheckScriptContext2Code (mkScriptContext 1)) 1963
+    , Tx.fitsInto "checkScriptContext2 (size)" (mkCheckScriptContext2Code (mkScriptContext 1)) 1897
     , runTestNested $ Tx.goldenBudget "checkScriptContext2-4" $
           mkCheckScriptContext2Code (mkScriptContext 4)
     , runTestNested $ Tx.goldenBudget "checkScriptContext2-20" $

diff --git a/plutus-benchmark/script-contexts/test/checkScriptContext1-20.budget.golden b/plutus-benchmark/script-contexts/test/checkScriptContext1-20.budget.golden
@@ -1,2 +1,2 @@
-({cpu: 424297997
-| mem: 1316969})
+({cpu: 419053997
+| mem: 1294169})
diff --git a/plutus-benchmark/script-contexts/test/checkScriptContext1-4.budget.golden b/plutus-benchmark/script-contexts/test/checkScriptContext1-4.budget.golden
@@ -1,2 +1,2 @@
-({cpu: 124093245
-| mem: 389193})
+({cpu: 122161245
+| mem: 380793})
diff --git a/plutus-benchmark/script-contexts/test/checkScriptContext2-20.budget.golden b/plutus-benchmark/script-contexts/test/checkScriptContext2-20.budget.golden
@@ -1,2 +1,2 @@
-({cpu: 405027508
-| mem: 1254326})
+({cpu: 399852508
+| mem: 1231826})
diff --git a/plutus-benchmark/script-contexts/test/checkScriptContext2-4.budget.golden b/plutus-benchmark/script-contexts/test/checkScriptContext2-4.budget.golden
@@ -1,2 +1,2 @@
-({cpu: 118430388
-| mem: 371382})
+({cpu: 116567388
+| mem: 363282})
diff --git a/plutus-core/changelog.d/20230525_144849_unsafeFixIO_firstEffectfulTerm.md b/plutus-core/changelog.d/20230525_144849_unsafeFixIO_firstEffectfulTerm.md
@@ -0,0 +1,4 @@
+### Fixed
+
+- Fixed `PlutusIR.Purity.firstEffectfulTerm` and `UntypedPlutusCore.Transform.Inline.firstEffectfulTerm`,
+  which were sometimes too conservative and sometimes incorrect.
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
@@ -382,21 +382,21 @@ toBuiltinsRuntime
     => BuiltinVersion fun -> cost -> BuiltinsRuntime fun val
 toBuiltinsRuntime ver cost =
     let runtime = BuiltinsRuntime $ toBuiltinRuntime cost . inline toBuiltinMeaning ver
-        {-# INLINE runtime #-}
-       -- Force each 'BuiltinRuntime' to WHNF. Inlining 'force' manually, since it doesn't have an
-       -- @INLINE@ pragma. This allows GHC to get to the 'NFData' instance for 'BuiltinsRuntime',
-       -- which forces all the freshly created 'BuiltinRuntime' thunks. Which is important, because
-       -- the thunks are behind a lambda binding the @cost@ variable and GHC would supply the @cost@
-       -- value (the one that is in the current scope) at runtime, if we didn't tell it that the
-       -- thunks need to be forced early. Which would be detrimental to performance, since it would
-       -- mean that the thunks would be created at runtime over and over again, each time we go
-       -- under the lambda binding the @cost@ variable, i.e. each time the 'BuiltinRuntime' is
-       -- retrieved from the environment. The 'deepseq' nagging causes GHC to supply the @cost@
-       -- value at compile time, thus allocating the thunks within this entire function allowing
-       -- them to be reused each time the 'BuiltinRuntime' is looked up (after the initial phase
-       -- forcing all of them at once).
-       --
-       -- Note that despite @runtime@ being used twice, we don't get all the multiple thousands of
-       -- Core duplicated, because the 'BuiltinRuntime' thunks are shared in the two @runtime@s.
-    in runtime `deepseq` runtime
+        -- This pragma is very important, removing it destroys the carefully set up optimizations of
+        -- of costing functions (see Note [Optimizations of runCostingFun*]). The reason for that is
+        -- that if @runtime@ doesn't have a pragma, then GHC sees that it's only referenced once and
+        -- inlines it below, together with this entire function (since we tell GHC to), at which
+        -- point everything's inlined and we're completely at GHC's mercy to optimize things
+        -- properly. Unfortunately, GHC doesn't want to cooperate and push 'toBuiltinRuntime' to
+        -- the inside of the inlined to 'toBuiltinMeaning' call, creating lots of 'BuiltinMeaning's
+        -- instead of 'BuiltinRuntime's with the former hiding the costing optimizations behind a
+        -- lambda binding the @cost@ variable, which renders all the optimizations useless. By
+        -- using a @NOINLINE@ pragma we tell GHC to create a separate thunk, which it can properly
+        -- optimize, because the other bazillion things don't get in the way.
+        {-# NOINLINE runtime #-}
+    in
+        -- Force each 'BuiltinRuntime' to WHNF, so that the thunk is allocated and forced at
+        -- initialization time rather than at runtime. Not that we'd lose much by not forcing all
+        -- 'BuiltinRuntime's here, but why pay even very little if there's an easy way not to pay.
+        force runtime
 {-# INLINE toBuiltinsRuntime #-}
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Purity.hs b/plutus-core/plutus-ir/src/PlutusIR/Purity.hs
@@ -5,17 +5,19 @@
 
 module PlutusIR.Purity
     ( isPure
+    , FirstEffectfulTerm (..)
     , firstEffectfulTerm
     , asBuiltinApp
     , isSaturated
     , BuiltinApp (..)
     , Arg (..)
     ) where
 
+import PlutusCore.Builtin
 import PlutusIR
 
+import Control.Applicative
 import Data.List.NonEmpty qualified as NE
-import PlutusCore.Builtin
 
 -- | An argument taken by a builtin: could be a term of a type.
 data Arg tyname name uni fun a = TypeArg (Type tyname uni a) | TermArg (Term tyname name uni fun a)
@@ -127,39 +129,49 @@ isPure ver varStrictness = go
             TermBind _ Strict _ rhs -> go rhs
             _                       -> True
 
+-- | Isomorphic to @Maybe (Term tyname name uni fun a)@. Used to represent the first
+-- subterm which will be evaluated in a term and which could have an effect.
+data FirstEffectfulTerm tyname name uni fun a
+  = EffectfulTerm (Term tyname name uni fun a)
+  -- | `Uncertain` indicates that we don't know for sure.
+  | Uncertain
+
 {- |
 Try to identify the first sub term which will be evaluated in the given term and
-which could have an effect. 'Nothing' indicates that we don't know, this function
-is conservative.
+which could have an effect. 'Nothing' indicates that there's no term to evaluate.
 -}
-firstEffectfulTerm :: Term tyname name uni fun a -> Maybe (Term tyname name uni fun a)
+firstEffectfulTerm ::
+  forall tyname name uni fun a.
+  Term tyname name uni fun a ->
+  Maybe (FirstEffectfulTerm tyname name uni fun a)
 firstEffectfulTerm = goTerm
     where
+      goTerm :: Term tyname name uni fun a -> Maybe (FirstEffectfulTerm tyname name uni fun a)
       goTerm = \case
-        Let _ NonRec bs b -> case goBindings (NE.toList bs) of
-            Just t' -> Just t'
-            Nothing -> goTerm b
-
-        Apply _ l _ -> goTerm l
-        TyInst _ t _ -> goTerm t
-        IWrap _ _ _ t -> goTerm t
-        Unwrap _ t -> goTerm t
-        Constr _ _ _ [] -> Nothing
-        Constr _ _ _ (t:_) -> goTerm t
-        Case _ _ t _ -> goTerm t
-
-        t@Var{} -> Just t
-        t@Error{} -> Just t
-        t@Builtin{} -> Just t
+        Let _ NonRec bs b -> goBindings (NE.toList bs) <|> goTerm b
 
-        -- Hard to know what gets evaluated first in a recursive let-binding,
-        -- just give up and say nothing
-        (Let _ Rec _ _) -> Nothing
-        TyAbs{} -> Nothing
-        LamAbs{} -> Nothing
-        Constant{} -> Nothing
+        Apply _ fun args  -> goTerm fun <|> goTerm args
+        TyInst _ t _      -> goTerm t
+        IWrap _ _ _ t     -> goTerm t
+        Unwrap _ t        -> goTerm t
+        Constr _ _ _ []   -> Nothing
+        Constr _ _ _ ts   -> asum $ goTerm <$> ts
+        Case _ _ t _      -> goTerm t
+
+        t@Var{}           -> Just (EffectfulTerm t)
+        t@Error{}         -> Just (EffectfulTerm t)
+        Builtin{}         -> Nothing
 
-      goBindings :: [Binding tyname name uni fun a] -> Maybe (Term tyname name uni fun a)
+        -- Hard to know what gets evaluated first in a recursive let-binding,
+        -- just give up and return `Uncertain`.
+        (Let _ Rec _ _)   -> Just Uncertain
+        TyAbs{}           -> Nothing
+        LamAbs{}          -> Nothing
+        Constant{}        -> Nothing
+
+      goBindings ::
+        [Binding tyname name uni fun a] ->
+        Maybe (FirstEffectfulTerm tyname name uni fun a)
       goBindings [] = Nothing
       goBindings (b:bs) = case b of
         -- Only strict term bindings can cause effects

diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/Inline/Utils.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/Inline/Utils.hs
@@ -18,7 +18,7 @@ import PlutusCore.Subst (typeSubstTyNamesM)
 import PlutusIR
 import PlutusIR.Analysis.Dependencies qualified as Deps
 import PlutusIR.Analysis.Usages qualified as Usages
-import PlutusIR.Purity (firstEffectfulTerm, isPure)
+import PlutusIR.Purity (FirstEffectfulTerm (..), firstEffectfulTerm, isPure)
 import PlutusIR.Transform.Rename ()
 import PlutusPrelude
 
@@ -301,8 +301,8 @@ effectSafe body s n purity = do
     -- doing ~quadratic work as we process the program. However in practice most term
     -- types will make it give up, so it's not too bad.
     let immediatelyEvaluated = case firstEffectfulTerm body of
-            Just (Var _ n') -> n == n'
-            _               -> False
+            Just (EffectfulTerm (Var _ n')) -> n == n'
+            _                               -> False
     pure $ case s of
         Strict    -> purity || immediatelyEvaluated
         NonStrict -> True

diff --git a/plutus-core/plutus-ir/test/TransformSpec.hs b/plutus-core/plutus-ir/test/TransformSpec.hs
@@ -238,6 +238,8 @@ inline =
             , "single"
             , "immediateVar"
             , "immediateApp"
+            , "firstEffectfulTerm1"
+            , "firstEffectfulTerm2"
             -- these tests are all let bindings of functions
             , "letFunConstInt" -- const fn fully applied (integer)
             , "letFunConstBool" -- const fn fully applied (bool)

diff --git a/plutus-core/plutus-ir/test/transform/inline/firstEffectfulTerm1 b/plutus-core/plutus-ir/test/transform/inline/firstEffectfulTerm1
@@ -0,0 +1,10 @@
+-- `a` should be inlined since it is the first effectful term in the body.
+(let
+  (nonrec)
+  (termbind
+    (strict)
+    (vardecl a (con integer))
+    { error (con integer) }
+  )
+  [ (lam x (con integer) x) a ]
+)
diff --git a/plutus-core/plutus-ir/test/transform/inline/firstEffectfulTerm1.golden b/plutus-core/plutus-ir/test/transform/inline/firstEffectfulTerm1.golden
@@ -0,0 +1 @@
+[ (lam x (con integer) x) { error (con integer) } ]
diff --git a/plutus-core/plutus-ir/test/transform/inline/firstEffectfulTerm2 b/plutus-core/plutus-ir/test/transform/inline/firstEffectfulTerm2
@@ -0,0 +1,18 @@
+-- `a` should not be inlined since it changes the semantics of the program.
+(let
+  (nonrec)
+  (termbind
+    (strict)
+    (vardecl a (fun (con integer) (con integer)))
+    { error (fun (con integer) (con integer)) }
+  )
+  (let
+    (nonrec)
+    (termbind
+      (strict)
+      (vardecl b (con integer))
+      [ (lam x (con integer) x) { error (con integer) } ]
+    )
+    [ a b ]
+  )
+)
diff --git a/plutus-core/plutus-ir/test/transform/inline/firstEffectfulTerm2.golden b/plutus-core/plutus-ir/test/transform/inline/firstEffectfulTerm2.golden
@@ -0,0 +1,17 @@
+(let
+  (nonrec)
+  (termbind
+    (strict)
+    (vardecl a (fun (con integer) (con integer)))
+    { error (fun (con integer) (con integer)) }
+  )
+  (let
+    (nonrec)
+    (termbind
+      (strict)
+      (vardecl b (con integer))
+      [ (lam x (con integer) x) { error (con integer) } ]
+    )
+    [ a b ]
+  )
+)
diff --git a/plutus-core/plutus-ir/test/transform/inline/letNonPureMulti.golden b/plutus-core/plutus-ir/test/transform/inline/letNonPureMulti.golden
@@ -7,7 +7,6 @@
       [ { (builtin trace) (con integer) } (con string "hello") ] (con integer 1)
     ]
   )
-  (termbind (strict) (vardecl z (con integer)) y)
   (termbind (strict) (vardecl x (con integer)) y)
-  [ [ (builtin addInteger) z ] [ [ (builtin addInteger) x ] x ] ]
+  [ [ (builtin addInteger) y ] [ [ (builtin addInteger) x ] x ] ]
 )
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Inline.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Inline.hs
@@ -39,6 +39,7 @@ import UntypedPlutusCore.Rename ()
 import UntypedPlutusCore.Size
 import UntypedPlutusCore.Subst
 
+import Control.Applicative
 import Control.Lens hiding (Strict)
 import Control.Monad.Extra
 import Control.Monad.Reader
@@ -325,23 +326,22 @@ acceptable t =
 
 {- |
 Try to identify the first sub term which will be evaluated in the given term and
-which could have an effect. 'Nothing' indicates that we don't know, this function
-is conservative.
+which could have an effect. 'Nothing' indicates that there's no term to evaluate.
 -}
 firstEffectfulTerm :: Term name uni fun a -> Maybe (Term name uni fun a)
 firstEffectfulTerm = goTerm
     where
       goTerm = \case
 
-        Apply _ l _      -> goTerm l
+        Apply _ fun args -> goTerm fun <|> goTerm args
         Force _ t        -> goTerm t
         Constr _ _ []    -> Nothing
-        Constr _ _ (t:_) -> goTerm t
+        Constr _ _ ts    -> asum $ goTerm <$> ts
         Case _ t _       -> goTerm t
 
         t@Var{}          -> Just t
         t@Error{}        -> Just t
-        t@Builtin{}      -> Just t
+        Builtin{}        -> Nothing
 
         LamAbs{}         -> Nothing
         Constant{}       -> Nothing

diff --git a/plutus-tx-plugin/test/Budget/applicative.pir-readable.golden b/plutus-tx-plugin/test/Budget/applicative.pir-readable.golden
@@ -2,7 +2,6 @@ let
   data (Maybe :: * -> *) a | Maybe_match where
     Just : a -> Maybe a
     Nothing : Maybe a
-  !x : Maybe integer = Just {integer} 1
   !y : Maybe integer = Just {integer} 2
   !ds : Maybe (integer -> integer)
     = (let
@@ -25,7 +24,7 @@ let
                (/\dead -> Nothing {b})
                {all dead. dead})
         (\(x : integer) (y : integer) -> addInteger x y)
-        x
+        (Just {integer} 1)
 in
 Maybe_match
   {integer -> integer}

diff --git a/plutus-tx-plugin/test/Budget/show.budget.golden b/plutus-tx-plugin/test/Budget/show.budget.golden
@@ -1,2 +1,2 @@
-({cpu: 4608602372
-| mem: 13854201})
+({cpu: 4608533372
+| mem: 13853901})