1
1
mirror of https://github.com/github/semantic.git synced 2024-12-01 09:15:01 +03:00

Merge pull request #2188 from github/while-effect

Implement while as an effect
This commit is contained in:
Timothy Clem 2018-09-21 09:33:12 -07:00 committed by GitHub
commit d656988dd0
9 changed files with 143 additions and 68 deletions

View File

@ -1,4 +1,4 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, TypeOperators #-}
{-# LANGUAGE GeneralizedNewtypeDeriving, TypeOperators, ScopedTypeVariables #-}
module Control.Abstract.Evaluator
( Evaluator(..)
-- * Effects
@ -9,6 +9,7 @@ module Control.Abstract.Evaluator
, LoopControl(..)
, throwBreak
, throwContinue
, throwAbort
, catchLoopControl
, runLoopControl
, module X
@ -59,6 +60,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
@ -71,6 +73,10 @@ throwContinue :: Member (Exc (LoopControl address)) effects
-> Evaluator address value effects address
throwContinue = throwError . Continue
throwAbort :: forall address effects value a . Member (Exc (LoopControl address)) effects
=> Evaluator address value effects a
throwAbort = throwError (Abort @address)
catchLoopControl :: (Member (Exc (LoopControl address)) effects, Effectful (m address value)) => m address value effects a -> (LoopControl address -> m address value effects a) -> m address value effects a
catchLoopControl = catchError

View File

@ -16,6 +16,7 @@ module Control.Abstract.Value
, while
, doWhile
, forLoop
, While(..)
, makeNamespace
, evaluateInScopedEnv
, address
@ -36,7 +37,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
@ -102,6 +103,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 address value effects value -- ^ Condition
-> Evaluator address value effects value -- ^ Body
-> Evaluator 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 address value effects value -- ^ Body
-> Evaluator address value effects value -- ^ Condition
-> Evaluator 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 address value effects value -- ^ Initial statement
-> Evaluator address value effects value -- ^ Condition
-> Evaluator address value effects value -- ^ Increment/stepper
-> Evaluator address value effects value -- ^ Body
-> Evaluator 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.
@ -204,42 +235,6 @@ class AbstractIntro value => AbstractValue address value effects where
-- | Extract the environment from any scoped object (e.g. classes, namespaces, etc).
scopedEnvironment :: address -> Evaluator 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 address value effects value -> Evaluator address value effects value) -> Evaluator address value effects value
-- | C-style for loops.
forLoop :: ( AbstractValue address value effects
, Member (Boolean value) effects
, Member (Env address) effects
)
=> Evaluator address value effects value -- ^ Initial statement
-> Evaluator address value effects value -- ^ Condition
-> Evaluator address value effects value -- ^ Increment/stepper
-> Evaluator address value effects value -- ^ Body
-> Evaluator 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 address value effects, Member (Boolean value) effects)
=> Evaluator address value effects value
-> Evaluator address value effects value
-> Evaluator 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 address value effects, Member (Boolean value) effects)
=> Evaluator address value effects value
-> Evaluator address value effects value
-> Evaluator address value effects value
doWhile body cond = loop $ \ continue -> body *> do
this <- cond
ifthenelse this continue (pure unit)
makeNamespace :: ( AbstractValue address value effects
, Member (Deref value) effects

View File

@ -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
@ -53,6 +53,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
@ -93,6 +94,7 @@ type ModuleEffects address value rest
type ValueEffects address value rest
= Function address value
': While value
': Boolean value
': rest

View File

@ -3,6 +3,7 @@ module Data.Abstract.Value.Abstract
( Abstract (..)
, runFunction
, runBoolean
, runWhile
) where
import Control.Abstract as Abstract
@ -50,6 +51,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 address Abstract (While Abstract ': effects) a
-> Evaluator 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
@ -72,7 +94,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
)
@ -102,6 +123,4 @@ instance ( Member (Allocator address) effects
liftComparison _ _ _ = pure Abstract
loop f = f empty
castToInteger _ = pure Abstract

View File

@ -1,18 +1,20 @@
{-# LANGUAGE GADTs, RankNTypes, TypeOperators, UndecidableInstances, LambdaCase #-}
{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ScopedTypeVariables, UndecidableInstances, LambdaCase #-}
module Data.Abstract.Value.Concrete
( Value (..)
, ValueError (..)
, ClosureBody (..)
, 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.Name
@ -24,7 +26,7 @@ import Data.Scientific (Scientific, coefficient, normalize)
import Data.Scientific.Exts
import qualified Data.Set as Set
import Data.Word
import Prologue
import Prologue hiding (catchError)
data Value address body
= Closure PackageInfo ModuleInfo (Maybe Name) [Name] (ClosureBody address body) (Environment address)
@ -116,6 +118,44 @@ runBoolean = interpret $ \case
if a'' then pure a' else runBoolean (Evaluator b)
runWhile :: forall effects address body a .
( PureEffects effects
, Member (Deref (Value address body)) effects
, Member (Abstract.Boolean (Value address body)) effects
, Member (Exc (LoopControl address)) effects
, Member (Reader ModuleInfo) effects
, Member (Reader Span) effects
, Member (Resumable (BaseError (AddressError address (Value address body)))) effects
, Member (Resumable (BaseError (ValueError address body))) effects
, Member (Resumable (BaseError (UnspecializedError (Value address body)))) effects
, Member (State (Heap address (Value address body))) effects
, Ord address
, Show address
)
=> Evaluator address (Value address body) (Abstract.While (Value address body) ': effects) a
-> Evaluator address (Value address body) 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 address body))))
(\(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 address body) where
hole = Hole
@ -244,11 +284,7 @@ instance ( Coercible body (Eff effects)
tentative x i j = attemptUnsafeArithmetic (x i j)
-- Dispatch whatever's contained inside a 'Number.SomeNumber' to its appropriate 'MonadValue' ctor
specialize :: ( AbstractValue address (Value address body) effects
, Member (Reader ModuleInfo) effects
, Member (Reader Span) effects
, Member (Resumable (BaseError (ValueError address body))) effects
)
specialize :: ( AbstractValue address (Value address body) effects)
=> Either ArithException Number.SomeNumber
-> Evaluator address (Value address body) effects (Value address body)
specialize (Left exc) = throwValueError (ArithmeticError exc)
@ -269,7 +305,7 @@ instance ( Coercible body (Eff effects)
where
-- Explicit type signature is necessary here because we're passing all sorts of things
-- to these comparison functions.
go :: (AbstractValue address (Value address body) effects, Member (Abstract.Boolean (Value address body)) effects, Ord a) => a -> a -> Evaluator address (Value address body) effects (Value address body)
go :: (AbstractValue address (Value address body) effects, Ord a) => a -> a -> Evaluator address (Value address body) effects (Value address body)
go l r = case comparator of
Concrete f -> boolean (f l r)
Generalized -> pure $ integer (orderingToInt (compare l r))
@ -299,11 +335,6 @@ instance ( Coercible body (Eff 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)

View File

@ -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(..), raiseHandler)
import Control.Abstract hiding (Boolean(..), Function(..), While(..), raiseHandler)
import Control.Monad.Effect.Internal (raiseHandler)
import Data.Abstract.Environment as Env
import Data.Abstract.BaseError
@ -277,6 +278,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 address Type (Abstract.While Type ': effects) a
-> Evaluator 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
@ -297,7 +322,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
@ -354,6 +378,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

View File

@ -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.Coerce
@ -130,7 +130,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 (Abstract.runBoolean . Abstract.runFunction) modules))
extractGraph <$> runEvaluator (runGraphAnalysis (evaluate lang analyzeModule analyzeTerm runAddressEffects (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 (runImportGraphAnalysis (evaluate lang analyzeModule id runAddressEffects (Concrete.runBoolean . Concrete.runFunction coerce coerce) (ModuleTable.toPairs (packageModules package) >>= toList . snd)))
in extractGraph <$> runEvaluator (runImportGraphAnalysis (evaluate lang analyzeModule id runAddressEffects (Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction coerce coerce) (ModuleTable.toPairs (packageModules package) >>= toList . snd)))
type ConcreteEffects address rest
= Reader Span
@ -285,7 +285,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 (Concrete.runBoolean . Concrete.runFunction coerce coerce . runPythonPackaging) [ setupModule ])
fst <$> runAnalysis (evaluate (Proxy @'Language.Python) id id runAddressEffects (Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction coerce coerce . runPythonPackaging) [ setupModule ])
Nothing -> pure PythonPackage.Unknown
case strat of
PythonPackage.Unknown -> do

View File

@ -106,7 +106,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) (Concrete.runBoolean . Concrete.runFunction coerce coerce) modules
$ evaluate proxy id (withTermSpans . step (fmap (\ (x:|_) -> moduleBody x) <$> ModuleTable.toPairs (packageModules (fst <$> package)))) (Precise.runAllocator . Precise.runDeref) (Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction coerce coerce) modules
-- TODO: REPL for typechecking/abstract semantics
-- TODO: drive the flow from within the REPL instead of from without

View File

@ -108,7 +108,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) (Concrete.runBoolean . Concrete.runFunction coerce coerce) modules)))))))
(evaluate proxy id withTermSpans (Precise.runAllocator . Precise.runDeref) (Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction coerce coerce) modules)))))))
evaluatePythonProjects proxy parser lang path = runTaskWithOptions debugOptions $ do
project <- readProject Nothing path lang []
@ -121,7 +121,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) (Concrete.runBoolean . Concrete.runFunction coerce coerce) modules)))))))
(evaluate proxy id withTermSpans (Precise.runAllocator . Precise.runDeref) (Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction coerce coerce) modules)))))))
evaluateProjectWithCaching proxy parser path = runTaskWithOptions debugOptions $ do
@ -133,7 +133,7 @@ evaluateProjectWithCaching proxy parser path = runTaskWithOptions debugOptions $
(runReader (lowerBound @Span)
(runReader (lowerBound @(ModuleTable (NonEmpty (Module (ModuleResult Monovariant)))))
(raiseHandler (runModules (ModuleTable.modulePaths (packageModules package)))
(evaluate proxy id withTermSpans (Monovariant.runAllocator . Monovariant.runDeref) (Type.runBoolean . Type.runFunction) modules))))))
(evaluate proxy id withTermSpans (Monovariant.runAllocator . Monovariant.runDeref) (Type.runBoolean . Type.runWhile . Type.runFunction) modules))))))
parseFile :: Parser term -> FilePath -> IO term