Implement goto using Goto effects embedding evaluators.

2024-12-24 23:42:31 +03:00 · 2018-05-08 10:19:50 -04:00 · 2018-05-08 10:19:50 -04:00 · eacb5b47d7
commit eacb5b47d7
parent 84a566197f
4 changed files with 50 additions and 47 deletions
--- a/src/Control/Abstract/Label.hs
+++ b/src/Control/Abstract/Label.hs
@ -16,43 +16,35 @@ import qualified Data.IntMap as IntMap
 import           Prelude hiding (fail)
 import           Prologue

-type JumpTable term = IntMap.IntMap (Instruction term)
-type Instruction term = (PackageInfo, ModuleInfo, term)
+type JumpTable effects value = IntMap.IntMap (Instruction effects value)
+type Instruction effects value = (PackageInfo, ModuleInfo, Eff effects value)

 -- | The type of labels.
 --   TODO: This should be rolled into 'Name' and tracked in the environment, both so that we can abstract over labels like any other location, and so that we can garbage collect unreachable labels.
 type Label = Int


-getJumpTable :: Member (State (JumpTable term)) effects => Evaluator location term vlaue effects (JumpTable term)
-getJumpTable = raise get
-
 -- | Allocate a 'Label' for the given @term@.
 --
 --   Labels must be allocated before being jumped to with 'goto', but are suitable for nonlocal jumps; thus, they can be used to implement coroutines, exception handling, call with current continuation, and other esoteric control mechanisms.
-label :: Members '[Reader ModuleInfo, Reader PackageInfo, State (JumpTable term)] effects => term -> Evaluator location term value effects Label
-label term = do
-  m <- getJumpTable
+label :: Members '[Reader ModuleInfo, Reader PackageInfo] effects => Evaluator location term value (Goto effects value ': effects) value -> Evaluator location term value (Goto effects value ': effects) Label
+label action = do
  moduleInfo <- currentModule
  packageInfo <- currentPackage
-  let i = IntMap.size m
-  raise (put (IntMap.insert i (packageInfo, moduleInfo, term) m))
-  pure i
+  send (Label packageInfo moduleInfo (lower action))

 -- | “Jump” to a previously-allocated 'Label' (retrieving the @term@ at which it points, which can then be evaluated in e.g. a 'MonadAnalysis' instance).
-goto :: Members '[Fail, Reader ModuleInfo, Reader PackageInfo, State (JumpTable term)] effects => Label -> (term -> Evaluator location term value effects a) -> Evaluator location term value effects a
+goto :: Members '[Reader ModuleInfo, Reader PackageInfo] effects => Label -> (Evaluator location term value (Goto effects value ': effects) value -> Evaluator location term value (Goto effects value ': effects) a) -> Evaluator location term value (Goto effects value ': effects) a
 goto label comp = do
-  maybeTerm <- IntMap.lookup label <$> getJumpTable
-  case maybeTerm of
-    Just (packageInfo, moduleInfo, term) -> raiseHandler (local (const packageInfo)) (raiseHandler (local (const moduleInfo)) (comp term))
-    Nothing -> raise (fail ("unknown label: " <> show label))
+  (packageInfo, moduleInfo, action) <- send (Goto label)
+  raiseHandler (local (const packageInfo)) (raiseHandler (local (const moduleInfo)) (comp (raise action)))


 data Goto effects value return where
  Label :: PackageInfo -> ModuleInfo -> Eff (Goto effects value ': effects) value -> Goto effects value Label
  Goto  :: Label -> Goto effects value (PackageInfo, ModuleInfo, Eff (Goto effects value ': effects) value)

-runGoto :: Member Fail effects => IntMap.IntMap (PackageInfo, ModuleInfo, Eff (Goto effects value ': effects) value) -> Evaluator location term value (Goto effects value ': effects) a -> Evaluator location term value effects a
+runGoto :: Member Fail effects => JumpTable (Goto effects value ': effects) value -> Evaluator location term value (Goto effects value ': effects) a -> Evaluator location term value effects a
 runGoto initial = raiseHandler (relayState (IntMap.size initial, initial) (\ _ -> pure) (\ (supremum, table) goto yield -> case goto of
  Label packageInfo moduleInfo action -> yield (succ supremum, IntMap.insert supremum (packageInfo, moduleInfo, action) table) supremum
  Goto label                          -> case IntMap.lookup label table of
--- a/src/Data/Abstract/Evaluatable.hs
+++ b/src/Data/Abstract/Evaluatable.hs
@ -1,4 +1,4 @@
-{-# LANGUAGE ConstraintKinds, DefaultSignatures, GADTs, RankNTypes, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE ConstraintKinds, DefaultSignatures, GADTs, RankNTypes, ScopedTypeVariables, TypeOperators, UndecidableInstances #-}
 module Data.Abstract.Evaluatable
 ( module X
 , Evaluatable(..)
@ -19,6 +19,7 @@ module Data.Abstract.Evaluatable

 import Control.Abstract as X hiding (LoopControl(..), Return(..), Goto(..))
 import Control.Abstract.Evaluator (LoopControl, Return(..))
+import Control.Abstract.Label (Goto(..))
 import Control.Monad.Effect as Eff
 import Data.Abstract.Address
 import Data.Abstract.Declarations as X
@ -168,43 +169,50 @@ traceResolve name path = trace ("resolved " <> show name <> " -> " <> show path)

 -- | Evaluate a given package.
 evaluatePackageWith :: ( Evaluatable (Base term)
-                       , EvaluatableConstraints location term value termEffects
+                       , EvaluatableConstraints location term value gotoEffects
                       , Members '[ Fail
                                  , Reader (Environment location value)
                                  , State (Environment location value)
+                                  , State (Exports location value)
+                                  , State (Heap location value)
+                                  , State (ModuleTable (Environment location value, value))
                                  ] effects
                       , Recursive term
-                       , termEffects ~ (LoopControl value ': Return value ': EvalClosure term value ': moduleEffects)
+                       , gotoEffects ~ (Goto termEffects value ': termEffects)
+                       , termEffects ~ (LoopControl value ': Return value ': moduleEffects)
                       , moduleEffects ~ (Reader ModuleInfo ': EvalModule term value ': packageBodyEffects)
-                       , packageBodyEffects ~ (Reader LoadStack ': State (JumpTable term) ': Reader (ModuleTable [Module term]) ': packageEffects)
+                       , packageBodyEffects ~ (Reader LoadStack ': Reader (ModuleTable [Module term]) ': packageEffects)
                       , packageEffects ~ (Reader PackageInfo ': effects)
                       )
                    => (SubtermAlgebra Module term (Evaluator location term value moduleEffects value) -> SubtermAlgebra Module term (Evaluator location term value moduleEffects value))
-                    -> (SubtermAlgebra (Base term) term (Evaluator location term value termEffects value) -> SubtermAlgebra (Base term) term (Evaluator location term value termEffects value))
+                    -> (SubtermAlgebra (Base term) term (Evaluator location term value gotoEffects value) -> SubtermAlgebra (Base term) term (Evaluator location term value gotoEffects value))
                    -> Package term
                    -> Evaluator location term value effects [value]
 evaluatePackageWith perModule perTerm = runReader . packageInfo <*> evaluatePackageBodyWith perModule perTerm . packageBody

 -- | Evaluate a given package body (module table and entry points).
-evaluatePackageBodyWith :: ( Evaluatable (Base term)
-                           , EvaluatableConstraints location term value termEffects
+evaluatePackageBodyWith :: forall location term value gotoEffects termEffects moduleEffects packageBodyEffects effects
+                        .  ( Evaluatable (Base term)
+                           , EvaluatableConstraints location term value gotoEffects
                           , Members '[ Fail
                                      , Reader (Environment location value)
                                      , State (Environment location value)
+                                      , State (Exports location value)
+                                      , State (Heap location value)
+                                      , State (ModuleTable (Environment location value, value))
                                      ] effects
                           , Recursive term
-                           , termEffects ~ (LoopControl value ': Return value ': EvalClosure term value ': moduleEffects)
+                           , gotoEffects ~ (Goto termEffects value ': termEffects)
+                           , termEffects ~ (LoopControl value ': Return value ': moduleEffects)
                           , moduleEffects ~ (Reader ModuleInfo ': EvalModule term value ': packageBodyEffects)
-                           , packageBodyEffects ~ (Reader LoadStack ': State (JumpTable term) ': Reader (ModuleTable [Module term]) ': effects)
+                           , packageBodyEffects ~ (Reader LoadStack ': Reader (ModuleTable [Module term]) ': effects)
                           )
                        => (SubtermAlgebra Module term (Evaluator location term value moduleEffects value) -> SubtermAlgebra Module term (Evaluator location term value moduleEffects value))
-                        -> (SubtermAlgebra (Base term) term (Evaluator location term value termEffects value) -> SubtermAlgebra (Base term) term (Evaluator location term value termEffects value))
+                        -> (SubtermAlgebra (Base term) term (Evaluator location term value gotoEffects value) -> SubtermAlgebra (Base term) term (Evaluator location term value gotoEffects value))
                        -> PackageBody term
                        -> Evaluator location term value effects [value]
 evaluatePackageBodyWith perModule perTerm body
  = runReader (packageModules body)
-  . fmap fst
-  . runState lowerBound
  . runReader lowerBound
  . runEvalModule evalModule
  . withPrelude (packagePrelude body)
@ -216,12 +224,13 @@ evaluatePackageBodyWith perModule perTerm body
          . fmap (Subterm <*> evalTerm)
          $ m
        evalTerm
-          = runEvalClosure evalTerm
-          . runReturn
+          = runReturn
          . runLoopControl
+          . runGoto lowerBound
          . foldSubterms (perTerm eval)

-        evaluateEntryPoint m sym = runReader (ModuleInfo m) . runEvalClosure evalTerm . runReturn . runLoopControl $ do
+        evaluateEntryPoint :: ModulePath -> Maybe Name -> Evaluator location term value (EvalModule term value ': packageBodyEffects) value
+        evaluateEntryPoint m sym = runReader (ModuleInfo m) . runReturn . runLoopControl . runGoto lowerBound $ do
          v <- maybe unit (pure . snd) <$> require m
          maybe v ((`call` []) <=< variable) sym

--- a/src/Data/Abstract/Value.hs
+++ b/src/Data/Abstract/Value.hs
@ -206,9 +206,8 @@ instance AbstractHole (Value location) where
  hole = injValue Hole

 -- | Construct a 'Value' wrapping the value arguments (if any).
-instance ( Addressable location effects
-         , Members '[ EvalClosure term (Value location)
-                    , Fail
+instance ( Addressable location (Goto effects (Value location) ': effects)
+         , Members '[ Fail
                    , LoopControl (Value location)
                    , Reader (Environment location (Value location))
                    , Reader ModuleInfo
@ -218,12 +217,11 @@ instance ( Addressable location effects
                    , Return (Value location)
                    , State (Environment location (Value location))
                    , State (Heap location (Value location))
-                    , State (JumpTable term)
                    ] effects
         , Reducer (Value location) (Cell location (Value location))
         , Show location
         )
-      => AbstractValue location term (Value location) effects where
+      => AbstractValue location term (Value location) (Goto effects (Value location) ': effects) where
  unit     = pure . injValue $ Unit
  integer  = pure . injValue . Integer . Number.Integer
  boolean  = pure . injValue . Boolean
@ -351,8 +349,8 @@ instance ( Addressable location effects
    | otherwise = throwValueError (Bitwise2Error left right)
      where pair = (left, right)

-  lambda names (Subterm body _) = do
-    l <- label body
+  lambda names (Subterm body bodyValue) = do
+    l <- label bodyValue
    injValue . Closure names l . Env.bind (foldr Set.delete (Set.fromList (freeVariables body)) names) <$> getEnv

  call op params = do
@ -366,10 +364,8 @@ instance ( Addressable location effects
            a <- alloc name
            assign a v
            Env.insert name a <$> rest) (pure env) (zip names params)
-          localEnv (mergeEnvs bindings) (evalClosure body)
+          localEnv (mergeEnvs bindings) (catchReturn body (\ (Return value) -> pure value))
      Nothing -> throwValueError (CallError op)
-    where
-      evalClosure term = catchReturn (evaluateClosureBody term) (\ (Return value) -> pure value)

  loop x = catchLoopControl (fix x) (\ control -> case control of
    Break value -> pure value
--- a/test/Control/Abstract/Evaluator/Spec.hs
+++ b/test/Control/Abstract/Evaluator/Spec.hs
@ -1,3 +1,4 @@
+{-# LANGUAGE TypeOperators #-}
 module Control.Abstract.Evaluator.Spec where

 import Analysis.Abstract.Evaluating (evaluating)
@ -10,6 +11,7 @@ import qualified Data.Abstract.Value as Value
 import Data.Algebra
 import Data.Bifunctor (first)
 import Data.Functor.Const
+import Data.Semilattice.Lower
 import Data.Sum
 import SpecHelpers hiding (Term, reassociate)

@ -35,8 +37,13 @@ evaluate
  . Value.runValueError
  . runEnvironmentError
  . runAddressError
-  . runValue
-runValue = runEvalClosure (runValue . runTerm) . runReturn . runLoopControl
+  . runReturn
+  . runLoopControl
+  . runGoto lowerBound
+  . constraining
+
+constraining :: TermEvaluator Value -> TermEvaluator Value
+constraining = id

 reassociate :: Either String (Either (SomeExc exc1) (Either (SomeExc exc2) (Either (SomeExc exc3) result))) -> Either (SomeExc (Sum '[Const String, exc1, exc2, exc3])) result
 reassociate (Left s) = Left (SomeExc (injectSum (Const s)))
@ -45,10 +52,10 @@ reassociate (Right (Right (Right (Right a)))) = Right a
 term :: TermEvaluator Value -> Subterm Term (TermEvaluator Value)
 term eval = Subterm (Term eval) eval

-type TermEffects
+type TermEffects = Goto GotoEffects Value ': GotoEffects
+type GotoEffects
  = '[ LoopControl Value
     , Return Value
-     , EvalClosure Term Value
     , Resumable (AddressError Precise Value)
     , Resumable (EnvironmentError Value)
     , Resumable (Value.ValueError Precise)
@ -61,7 +68,6 @@ type TermEffects
     , State (Heap Precise Value)
     , State (ModuleTable (Environment Precise Value, Value))
     , State (Exports Precise Value)
-     , State (JumpTable Term)
     , IO
     ]