diff --git a/src/Control/Abstract/Evaluator.hs b/src/Control/Abstract/Evaluator.hs index 62528a324..0533799a8 100644 --- a/src/Control/Abstract/Evaluator.hs +++ b/src/Control/Abstract/Evaluator.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE GeneralizedNewtypeDeriving, TypeOperators #-} +{-# LANGUAGE GeneralizedNewtypeDeriving, TypeOperators, ScopedTypeVariables #-} module Control.Abstract.Evaluator ( Evaluator(..) , Open @@ -10,6 +10,7 @@ module Control.Abstract.Evaluator , LoopControl(..) , throwBreak , throwContinue + , throwAbort , catchLoopControl , runLoopControl , module X @@ -65,6 +66,7 @@ runReturn = Eff.raiseHandler (fmap (either unReturn id) . runError) data LoopControl address = Break { unLoopControl :: address } | Continue { unLoopControl :: address } + | Abort deriving (Eq, Ord, Show) throwBreak :: Member (Exc (LoopControl address)) effects @@ -77,6 +79,10 @@ throwContinue :: Member (Exc (LoopControl address)) effects -> Evaluator term address value effects address throwContinue = throwError . Continue +throwAbort :: forall term address effects value a . Member (Exc (LoopControl address)) effects + => Evaluator term address value effects a +throwAbort = throwError (Abort @address) + catchLoopControl :: Member (Exc (LoopControl address)) effects => Evaluator term address value effects a -> (LoopControl address -> Evaluator term address value effects a) -> Evaluator term address value effects a catchLoopControl = catchError diff --git a/src/Control/Abstract/Value.hs b/src/Control/Abstract/Value.hs index caa4799f2..62db19d54 100644 --- a/src/Control/Abstract/Value.hs +++ b/src/Control/Abstract/Value.hs @@ -18,6 +18,7 @@ module Control.Abstract.Value , while , doWhile , forLoop +, While(..) , makeNamespace , evaluateInScopedEnv , address @@ -38,7 +39,7 @@ import Data.Abstract.Number as Number import Data.Abstract.Ref import Data.Scientific (Scientific) import Data.Span -import Prologue hiding (TypeError) +import Prologue hiding (TypeError, catchError) -- | This datum is passed into liftComparison to handle the fact that Ruby and PHP -- have built-in generalized-comparison ("spaceship") operators. If you want to @@ -118,6 +119,36 @@ instance PureEffect (Boolean value) where handle handler (Request (AsBool v) k) = Request (AsBool v) (handler . k) handle handler (Request (Disjunction a b) k) = Request (Disjunction (handler a) (handler b)) (handler . k) +-- | The fundamental looping primitive, built on top of 'ifthenelse'. +while :: Member (While value) effects + => Evaluator term address value effects value -- ^ Condition + -> Evaluator term address value effects value -- ^ Body + -> Evaluator term address value effects value +while (Evaluator cond) (Evaluator body) = send (While cond body) + +-- | Do-while loop, built on top of while. +doWhile :: Member (While value) effects + => Evaluator term address value effects value -- ^ Body + -> Evaluator term address value effects value -- ^ Condition + -> Evaluator term address value effects value +doWhile body cond = body *> while cond body + +-- | C-style for loops. +forLoop :: (Member (While value) effects, Member (Env address) effects) + => Evaluator term address value effects value -- ^ Initial statement + -> Evaluator term address value effects value -- ^ Condition + -> Evaluator term address value effects value -- ^ Increment/stepper + -> Evaluator term address value effects value -- ^ Body + -> Evaluator term address value effects value +forLoop initial cond step body = + locally (initial *> while cond (body *> step)) + +data While value m result where + While :: m value -> m value -> While value m value + +instance PureEffect (While value) where + handle handler (Request (While cond body) k) = Request (While (handler cond) (handler body)) (handler . k) + class Show value => AbstractIntro value where -- | Construct an abstract unit value. @@ -220,42 +251,6 @@ class AbstractIntro value => AbstractValue term address value effects where -- | Extract the environment from any scoped object (e.g. classes, namespaces, etc). scopedEnvironment :: address -> Evaluator term address value effects (Maybe (Environment address)) - -- | Primitive looping combinator, approximately equivalent to 'fix'. This should be used in place of direct recursion, as it allows abstraction over recursion. - -- - -- The function argument takes an action which recurs through the loop. - loop :: (Evaluator term address value effects value -> Evaluator term address value effects value) -> Evaluator term address value effects value - - --- | C-style for loops. -forLoop :: ( AbstractValue term address value effects - , Member (Boolean value) effects - , Member (Env address) effects - ) - => Evaluator term address value effects value -- ^ Initial statement - -> Evaluator term address value effects value -- ^ Condition - -> Evaluator term address value effects value -- ^ Increment/stepper - -> Evaluator term address value effects value -- ^ Body - -> Evaluator term address value effects value -forLoop initial cond step body = - locally (initial *> while cond (body *> step)) - --- | The fundamental looping primitive, built on top of 'ifthenelse'. -while :: (AbstractValue term address value effects, Member (Boolean value) effects) - => Evaluator term address value effects value - -> Evaluator term address value effects value - -> Evaluator term address value effects value -while cond body = loop $ \ continue -> do - this <- cond - ifthenelse this (body *> continue) (pure unit) - --- | Do-while loop, built on top of while. -doWhile :: (AbstractValue term address value effects, Member (Boolean value) effects) - => Evaluator term address value effects value - -> Evaluator term address value effects value - -> Evaluator term address value effects value -doWhile body cond = loop $ \ continue -> body *> do - this <- cond - ifthenelse this continue (pure unit) makeNamespace :: ( AbstractValue term address value effects , Member (Deref value) effects diff --git a/src/Data/Abstract/Evaluatable.hs b/src/Data/Abstract/Evaluatable.hs index f2f076d2c..0c5e7ed9e 100644 --- a/src/Data/Abstract/Evaluatable.hs +++ b/src/Data/Abstract/Evaluatable.hs @@ -27,7 +27,7 @@ import Control.Abstract.Environment as X hiding (runEnvironmentError, runEnviron import Control.Abstract.Evaluator as X hiding (LoopControl(..), Return(..), catchLoopControl, runLoopControl, catchReturn, runReturn) import Control.Abstract.Heap as X hiding (runAddressError, runAddressErrorWith) import Control.Abstract.Modules as X (Modules, ModuleResult, ResolutionError(..), load, lookupModule, listModulesInDir, require, resolve, throwResolutionError) -import Control.Abstract.Value as X hiding (Boolean(..), Function(..)) +import Control.Abstract.Value as X hiding (Boolean(..), Function(..), While(..)) import Control.Abstract.ScopeGraph import Data.Abstract.Declarations as X import Data.Abstract.Environment as X @@ -54,6 +54,7 @@ class (Show1 constr, Foldable constr) => Evaluatable constr where , FreeVariables term , Member (Allocator address) effects , Member (Boolean value) effects + , Member (While value) effects , Member (Deref value) effects , Member (ScopeEnv address) effects , Member (Env address) effects @@ -95,6 +96,7 @@ type ModuleEffects address value rest type ValueEffects term address value rest = Function term address value + ': While value ': Boolean value ': rest diff --git a/src/Data/Abstract/Value/Abstract.hs b/src/Data/Abstract/Value/Abstract.hs index 4a3bc0960..f7b53f67c 100644 --- a/src/Data/Abstract/Value/Abstract.hs +++ b/src/Data/Abstract/Value/Abstract.hs @@ -3,6 +3,7 @@ module Data.Abstract.Value.Abstract ( Abstract (..) , runFunction , runBoolean +, runWhile ) where import Control.Abstract as Abstract @@ -52,6 +53,27 @@ runBoolean = interpret $ \case AsBool _ -> pure True <|> pure False Disjunction a b -> runBoolean (Evaluator (a <|> b)) +runWhile :: + ( Member (Allocator address) effects + , Member (Deref Abstract) effects + , Member (Abstract.Boolean Abstract) effects + , Member NonDet effects + , Member (Env address) effects + , Member (Exc (Return address)) effects + , Member Fresh effects + , Member (Reader ModuleInfo) effects + , Member (Reader Span) effects + , Member (Resumable (BaseError (AddressError address Abstract))) effects + , Member (State (Heap address Abstract)) effects + , Ord address + , PureEffects effects + ) + => Evaluator term address Abstract (While Abstract ': effects) a + -> Evaluator term address Abstract effects a +runWhile = interpret $ \case + Abstract.While cond body -> do + cond' <- runWhile (raiseEff cond) + ifthenelse cond' (runWhile (raiseEff body) *> empty) (pure unit) instance Ord address => ValueRoots address Abstract where valueRoots = mempty @@ -74,7 +96,6 @@ instance AbstractIntro Abstract where instance ( Member (Allocator address) effects , Member (Deref Abstract) effects , Member Fresh effects - , Member NonDet effects , Member (State (Heap address Abstract)) effects , Ord address ) @@ -104,6 +125,4 @@ instance ( Member (Allocator address) effects liftComparison _ _ _ = pure Abstract - loop f = f empty - castToInteger _ = pure Abstract diff --git a/src/Data/Abstract/Value/Concrete.hs b/src/Data/Abstract/Value/Concrete.hs index 90ff89baf..eb3ead19f 100644 --- a/src/Data/Abstract/Value/Concrete.hs +++ b/src/Data/Abstract/Value/Concrete.hs @@ -1,17 +1,19 @@ -{-# LANGUAGE GADTs, RankNTypes, TypeOperators, UndecidableInstances, LambdaCase #-} +{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ScopedTypeVariables, UndecidableInstances, LambdaCase #-} module Data.Abstract.Value.Concrete ( Value (..) , ValueError (..) , runFunction , runBoolean + , runWhile , materializeEnvironment , runValueError , runValueErrorWith ) where import qualified Control.Abstract as Abstract -import Control.Abstract hiding (Boolean(..), Function(..)) +import Control.Abstract hiding (Boolean(..), Function(..), While(..)) import Data.Abstract.BaseError +import Data.Abstract.Evaluatable (UnspecializedError(..)) import Data.Abstract.Environment (Environment, Bindings, EvalContext(..)) import qualified Data.Abstract.Environment as Env import Data.Abstract.FreeVariables @@ -24,7 +26,7 @@ import Data.Scientific.Exts import qualified Data.Set as Set import Data.Text (pack) import Data.Word -import Prologue +import Prologue hiding (catchError) data Value term address = Closure PackageInfo ModuleInfo (Maybe Name) [Name] (Either BuiltIn term) (Environment address) @@ -113,6 +115,45 @@ runBoolean = interpret $ \case if a'' then pure a' else runBoolean (Evaluator b) +runWhile :: forall effects term address a . + ( PureEffects effects + , Member (Deref (Value term address)) effects + , Member (Abstract.Boolean (Value term address)) effects + , Member (Exc (LoopControl address)) effects + , Member (Reader ModuleInfo) effects + , Member (Reader Span) effects + , Member (Resumable (BaseError (AddressError address (Value term address)))) effects + , Member (Resumable (BaseError (ValueError term address))) effects + , Member (Resumable (BaseError (UnspecializedError (Value term address)))) effects + , Member (State (Heap address (Value term address))) effects + , Ord address + , Show address + , Show term + ) + => Evaluator term address (Value term address) (Abstract.While (Value term address) ': effects) a + -> Evaluator term address (Value term address) effects a +runWhile = interpret $ \case + Abstract.While cond body -> loop $ \continue -> do + cond' <- runWhile (raiseEff cond) + + -- `interpose` is used to handle 'UnspecializedError's and abort out of the + -- loop, otherwise under concrete semantics we run the risk of the + -- conditional always being true and getting stuck in an infinite loop. + let body' = interpose @(Resumable (BaseError (UnspecializedError (Value term address)))) + (\(Resumable (BaseError _ _ (UnspecializedError _))) -> throwAbort) $ + runWhile (raiseEff body) *> continue + + ifthenelse cond' body' (pure unit) + where + loop x = catchLoopControl (fix x) (\ control -> case control of + Break value -> deref value + Abort -> pure unit + -- FIXME: Figure out how to deal with this. Ruby treats this as the result + -- of the current block iteration, while PHP specifies a breakout level + -- and TypeScript appears to take a label. + Continue _ -> loop x) + + instance AbstractHole (Value term address) where hole = Hole @@ -242,9 +283,6 @@ instance ( Member (Allocator address) effects -- Dispatch whatever's contained inside a 'Number.SomeNumber' to its appropriate 'MonadValue' ctor specialize :: ( AbstractValue term address (Value term address) effects - , Member (Reader ModuleInfo) effects - , Member (Reader Span) effects - , Member (Resumable (BaseError (ValueError term address))) effects ) => Either ArithException Number.SomeNumber -> Evaluator term address (Value term address) effects (Value term address) @@ -266,7 +304,7 @@ instance ( Member (Allocator address) effects where -- Explicit type signature is necessary here because we're passing all sorts of things -- to these comparison functions. - go :: (AbstractValue term address (Value term address) effects, Member (Abstract.Boolean (Value term address)) effects, Ord a) => a -> a -> Evaluator term address (Value term address) effects (Value term address) + go :: (AbstractValue term address (Value term address) effects, Ord a) => a -> a -> Evaluator term address (Value term address) effects (Value term address) go l r = case comparator of Concrete f -> boolean (f l r) Generalized -> pure $ integer (orderingToInt (compare l r)) @@ -296,11 +334,6 @@ instance ( Member (Allocator address) effects ourShift :: Word64 -> Int -> Integer ourShift a b = toInteger (shiftR a b) - loop x = catchLoopControl (fix x) (\ control -> case control of - Break value -> deref value - -- FIXME: Figure out how to deal with this. Ruby treats this as the result of the current block iteration, while PHP specifies a breakout level and TypeScript appears to take a label. - Continue _ -> loop x) - castToInteger (Integer (Number.Integer i)) = pure (Integer (Number.Integer i)) castToInteger (Float (Number.Decimal i)) = pure (Integer (Number.Integer (coefficient (normalize i)))) castToInteger i = throwValueError (NumericError i) diff --git a/src/Data/Abstract/Value/Type.hs b/src/Data/Abstract/Value/Type.hs index 76c1d09cd..e65598f32 100644 --- a/src/Data/Abstract/Value/Type.hs +++ b/src/Data/Abstract/Value/Type.hs @@ -8,10 +8,11 @@ module Data.Abstract.Value.Type , unify , runFunction , runBoolean + , runWhile ) where import qualified Control.Abstract as Abstract -import Control.Abstract hiding (Boolean(..), Function(..)) +import Control.Abstract hiding (Boolean(..), Function(..), While(..)) import Control.Monad.Effect.Internal (raiseHandler) import Data.Abstract.Environment as Env import Data.Abstract.BaseError @@ -280,6 +281,30 @@ runBoolean = interpret $ \case Abstract.Disjunction t1 t2 -> (runBoolean (Evaluator t1) >>= unify Bool) <|> (runBoolean (Evaluator t2) >>= unify Bool) +runWhile :: + ( Member (Allocator address) effects + , Member (Deref Type) effects + , Member (Abstract.Boolean Type) effects + , Member NonDet effects + , Member (Env address) effects + , Member (Exc (Return address)) effects + , Member Fresh effects + , Member (Reader ModuleInfo) effects + , Member (Reader Span) effects + , Member (Resumable (BaseError TypeError)) effects + , Member (Resumable (BaseError (AddressError address Type))) effects + , Member (State (Heap address Type)) effects + , Member (State TypeMap) effects + , Ord address + , PureEffects effects + ) + => Evaluator term address Type (Abstract.While Type ': effects) a + -> Evaluator term address Type effects a +runWhile = interpret $ \case + Abstract.While cond body -> do + cond' <- runWhile (raiseEff cond) + ifthenelse cond' (runWhile (raiseEff body) *> empty) (pure unit) + instance AbstractHole Type where hole = Hole @@ -300,7 +325,6 @@ instance AbstractIntro Type where instance ( Member (Allocator address) effects , Member (Deref Type) effects , Member Fresh effects - , Member NonDet effects , Member (Reader ModuleInfo) effects , Member (Reader Span) effects , Member (Resumable (BaseError (AddressError address Type))) effects @@ -357,6 +381,4 @@ instance ( Member (Allocator address) effects (Int, Float) -> pure Int _ -> unify left right $> Bool - loop f = f empty - castToInteger t = unify t (Int :+ Float :+ Rational) $> Int diff --git a/src/Semantic/Graph.hs b/src/Semantic/Graph.hs index 7a495d65b..151a1dd7b 100644 --- a/src/Semantic/Graph.hs +++ b/src/Semantic/Graph.hs @@ -42,7 +42,7 @@ import qualified Data.Abstract.ModuleTable as ModuleTable import Data.Abstract.Package as Package import Data.Abstract.Value.Abstract as Abstract import Data.Abstract.Value.Concrete as Concrete - (Value, ValueError (..), runBoolean, runFunction, runValueErrorWith) + (Value, ValueError (..), runWhile, runBoolean, runFunction, runValueErrorWith) import Data.Abstract.Value.Type as Type import Data.Blob import Data.Graph @@ -128,7 +128,7 @@ runCallGraph lang includePackages modules package = do runAddressEffects = Hole.runAllocator (Located.handleAllocator Monovariant.handleAllocator) . Hole.runDeref (Located.handleDeref Monovariant.handleDeref) - extractGraph <$> runEvaluator (runGraphAnalysis (evaluate lang analyzeModule analyzeTerm runAddressEffects (fmap Abstract.runBoolean . Abstract.runFunction) modules)) + extractGraph <$> runEvaluator (runGraphAnalysis (evaluate lang analyzeModule analyzeTerm runAddressEffects (fmap (Abstract.runBoolean . Abstract.runWhile) . Abstract.runFunction) modules)) runImportGraphToModuleInfos :: ( Declarations term , Evaluatable (Base term) @@ -198,7 +198,7 @@ runImportGraph lang (package :: Package term) f = runAddressEffects = Hole.runAllocator Precise.handleAllocator . Hole.runDeref Precise.handleDeref - in extractGraph <$> runEvaluator @_ @_ @(Value _ (Hole (Maybe Name) Precise)) (runImportGraphAnalysis (evaluate lang analyzeModule id runAddressEffects (fmap Concrete.runBoolean . Concrete.runFunction) (ModuleTable.toPairs (packageModules package) >>= toList . snd))) + in extractGraph <$> runEvaluator @_ @_ @(Value _ (Hole (Maybe Name) Precise)) (runImportGraphAnalysis (evaluate lang analyzeModule id runAddressEffects (fmap (Concrete.runBoolean . Concrete.runWhile) . Concrete.runFunction) (ModuleTable.toPairs (packageModules package) >>= toList . snd))) runHeap :: Effects effects => Evaluator term address value (State (Heap address value) ': effects) a -> Evaluator term address value effects (Heap address value, a) @@ -264,7 +264,7 @@ parsePythonPackage parser project = do strat <- case find ((== (projectRootDir project "setup.py")) . filePath) (projectFiles project) of Just setupFile -> do setupModule <- fmap snd <$> parseModule project parser setupFile - fst <$> runAnalysis (evaluate (Proxy @'Language.Python) id id runAddressEffects (\ eval -> Concrete.runBoolean . Concrete.runFunction eval . runPythonPackaging) [ setupModule ]) + fst <$> runAnalysis (evaluate (Proxy @'Language.Python) id id runAddressEffects (\ eval -> Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction eval . runPythonPackaging) [ setupModule ]) Nothing -> pure PythonPackage.Unknown case strat of PythonPackage.Unknown -> do diff --git a/src/Semantic/REPL.hs b/src/Semantic/REPL.hs index ac84a7d9e..370140ca4 100644 --- a/src/Semantic/REPL.hs +++ b/src/Semantic/REPL.hs @@ -105,7 +105,7 @@ repl proxy parser paths = defaultConfig debugOptions >>= \ config -> runM . runD . runReader (packageInfo package) . runState (lowerBound @Span) . runReader (lowerBound @Span) - $ evaluate proxy id (withTermSpans . step (fmap (\ (x:|_) -> moduleBody x) <$> ModuleTable.toPairs (packageModules (fst <$> package)))) (Precise.runAllocator . Precise.runDeref) (fmap Concrete.runBoolean . Concrete.runFunction) modules + $ evaluate proxy id (withTermSpans . step (fmap (\ (x:|_) -> moduleBody x) <$> ModuleTable.toPairs (packageModules (fst <$> package)))) (Precise.runAllocator . Precise.runDeref) (fmap (Concrete.runBoolean . Concrete.runWhile) . Concrete.runFunction) modules -- TODO: REPL for typechecking/abstract semantics -- TODO: drive the flow from within the REPL instead of from without diff --git a/src/Semantic/Util.hs b/src/Semantic/Util.hs index b1531083d..9095013fe 100644 --- a/src/Semantic/Util.hs +++ b/src/Semantic/Util.hs @@ -105,7 +105,7 @@ evaluateProject' (TaskConfig config logger statter) proxy parser paths = either (runReader (packageInfo package) (runState (lowerBound @Span) (runReader (lowerBound @Span) - (evaluate proxy id withTermSpans (Precise.runAllocator . Precise.runDeref) (fmap Concrete.runBoolean . Concrete.runFunction) modules))))))) + (evaluate proxy id withTermSpans (Precise.runAllocator . Precise.runDeref) (fmap (Concrete.runBoolean . Concrete.runWhile) . Concrete.runFunction) modules))))))) evaluatePythonProjects proxy parser lang path = runTaskWithOptions debugOptions $ do project <- readProject Nothing path lang [] @@ -118,7 +118,7 @@ evaluatePythonProjects proxy parser lang path = runTaskWithOptions debugOptions (runReader (packageInfo package) (runState (lowerBound @Span) (runReader (lowerBound @Span) - (evaluate proxy id withTermSpans (Precise.runAllocator . Precise.runDeref) (fmap Concrete.runBoolean . Concrete.runFunction) modules))))))) + (evaluate proxy id withTermSpans (Precise.runAllocator . Precise.runDeref) (fmap (Concrete.runBoolean . Concrete.runWhile) . Concrete.runFunction) modules))))))) evaluateProjectWithCaching proxy parser path = runTaskWithOptions debugOptions $ do @@ -130,7 +130,7 @@ evaluateProjectWithCaching proxy parser path = runTaskWithOptions debugOptions $ (runReader (lowerBound @Span) (runReader (lowerBound @(ModuleTable (NonEmpty (Module (ModuleResult Monovariant))))) (runModules (ModuleTable.modulePaths (packageModules package)) - (evaluate proxy id withTermSpans (Monovariant.runAllocator . Monovariant.runDeref) (fmap Type.runBoolean . Type.runFunction) modules)))))) + (evaluate proxy id withTermSpans (Monovariant.runAllocator . Monovariant.runDeref) (fmap (Type.runBoolean . Type.runWhile) . Type.runFunction) modules)))))) parseFile :: Parser term -> FilePath -> IO term