1
1
mirror of https://github.com/github/semantic.git synced 2024-12-24 07:25:44 +03:00

Merge branch 'master' into first-order-closures

This commit is contained in:
Rob Rix 2018-09-25 16:53:41 -05:00
commit 891f238179
9 changed files with 143 additions and 66 deletions

View File

@ -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

View File

@ -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

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
@ -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

View File

@ -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

View File

@ -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)

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(..))
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

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.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

View File

@ -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

View File

@ -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