github/semantic
1
1
Fork 0
mirror of https://github.com/github/semantic.git synced 2024-12-24 23:42:31 +03:00
Code Issues Projects Releases Wiki Activity

Merge remote-tracking branch 'origin/master' into eval-__FILE__

Browse Source
This commit is contained in:
Timothy Clem 2018-04-26 13:23:42 -07:00
commit 08600b4155
30 changed files with 355 additions and 389 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
semantic.cabal
View File

@ -16,15 +16,16 @@ library
exposed-modules:
-- Analyses & term annotations
Analysis.Abstract.BadAddresses
Analysis.Abstract.BadVariables
Analysis.Abstract.BadValues
Analysis.Abstract.BadModuleResolutions
, Analysis.Abstract.BadSyntax
, Analysis.Abstract.BadModuleResolutions
, Analysis.Abstract.BadVariables
, Analysis.Abstract.BadValues
, Analysis.Abstract.Caching
, Analysis.Abstract.Collecting
, Analysis.Abstract.Dead
, Analysis.Abstract.Erroring
, Analysis.Abstract.Evaluating
, Analysis.Abstract.ImportGraph
, Analysis.Abstract.Quiet
, Analysis.Abstract.Tracing
, Analysis.Abstract.TypeChecking
, Analysis.CallGraph
@ -45,17 +46,15 @@ library
, Control.Abstract.Value
-- Control flow
, Control.Effect
-- Effects used for program analysis
, Control.Effect.Fresh
-- Datatypes for abstract interpretation
, Data.Abstract.Address
, Data.Abstract.Cache
, Data.Abstract.Configuration
, Data.Abstract.Declarations
, Data.Abstract.Environment
, Data.Abstract.Evaluatable
, Data.Abstract.Exports
, Data.Abstract.FreeVariables
, Data.Abstract.Declarations
, Data.Abstract.Heap
, Data.Abstract.Live
, Data.Abstract.Located

31
src/Analysis/Abstract/BadAddresses.hs
View File

@ -1,30 +1,27 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, KindSignatures, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the Interpreter instance’s MonadEvaluator constraint
module Analysis.Abstract.BadAddresses where
import Control.Abstract.Analysis
import Data.Abstract.Address
import Prologue
newtype BadAddresses m (effects :: [* -> *]) a = BadAddresses (m effects a)
newtype BadAddresses m (effects :: [* -> *]) a = BadAddresses { runBadAddresses :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadAddresses m)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (BadAddresses m)
instance ( Effectful m
, Member (Resumable (AddressError location value)) effects
, MonadAnalysis location term value effects m
, MonadValue location value effects (BadAddresses m)
instance ( Interpreter effects result rest m
, MonadEvaluator location term value effects m
, AbstractHole value
, Monoid (Cell location value)
, Show location
)
=> MonadAnalysis location term value effects (BadAddresses m) where
type Effects location term value (BadAddresses m) = Effects location term value m
analyzeTerm eval term = resume @(AddressError location value) (liftAnalyze analyzeTerm eval term) (
\yield error -> do
traceM ("AddressError:" <> show error)
case error of
UnallocatedAddress _ -> yield mempty
UninitializedAddress _ -> hole >>= yield)
analyzeModule = liftAnalyze analyzeModule
=> Interpreter (Resumable (AddressError location value) ': effects) result rest (BadAddresses m) where
interpret
= interpret
. runBadAddresses
. raiseHandler (relay pure (\ (Resumable err) yield -> traceM ("AddressError:" <> show err) *> case err of
UnallocatedAddress _ -> yield mempty
UninitializedAddress _ -> yield hole))

31
src/Analysis/Abstract/BadModuleResolutions.hs
View File

@ -1,29 +1,24 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, KindSignatures, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the Interpreter instance’s MonadEvaluator constraint
module Analysis.Abstract.BadModuleResolutions where
import Control.Abstract.Analysis
import Data.Abstract.Evaluatable
import Prologue
newtype BadModuleResolutions m (effects :: [* -> *]) a = BadModuleResolutions (m effects a)
newtype BadModuleResolutions m (effects :: [* -> *]) a = BadModuleResolutions { runBadModuleResolutions :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadModuleResolutions m)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (BadModuleResolutions m)
instance ( Effectful m
, Member (Resumable (ResolutionError value)) effects
, Member (State [Name]) effects
, MonadAnalysis location term value effects m
, MonadValue location value effects (BadModuleResolutions m)
instance ( Interpreter effects result rest m
, MonadEvaluator location term value effects m
)
=> MonadAnalysis location term value effects (BadModuleResolutions m) where
type Effects location term value (BadModuleResolutions m) = State [Name] ': Effects location term value m
analyzeTerm eval term = resume @(ResolutionError value) (liftAnalyze analyzeTerm eval term) (
\yield error -> do
traceM ("ResolutionError:" <> show error)
case error of
(NotFoundError nameToResolve _ _) -> yield nameToResolve
(GoImportError pathToResolve) -> yield [pathToResolve])
analyzeModule = liftAnalyze analyzeModule
=> Interpreter (Resumable (ResolutionError value) ': effects) result rest (BadModuleResolutions m) where
interpret
= interpret
. runBadModuleResolutions
. raiseHandler (relay pure (\ (Resumable err) yield -> traceM ("ResolutionError:" <> show err) *> case err of
NotFoundError nameToResolve _ _ -> yield nameToResolve
GoImportError pathToResolve -> yield [pathToResolve]))

32
src/Analysis/Abstract/BadSyntax.hs Normal file
View File

@ -0,0 +1,32 @@
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, KindSignatures, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the Interpreter instance’s MonadEvaluator constraint
module Analysis.Abstract.BadSyntax
( BadSyntax
) where
import Control.Abstract.Analysis
import Data.Abstract.Evaluatable
import Prologue
-- | An analysis which resumes exceptions instead of failing.
--
-- Use it by composing it onto an analysis:
--
-- > runAnalysis @(BadSyntax (Evaluating term value)) (…)
--
-- Note that exceptions thrown by other analyses may not be caught if 'BadSyntax' doesn’t know about them, i.e. if they’re not part of the generic 'MonadValue', 'MonadAddressable', etc. machinery.
newtype BadSyntax m (effects :: [* -> *]) a = BadSyntax { runBadSyntax :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadSyntax m)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (BadSyntax m)
instance ( Interpreter effects result rest m
, MonadEvaluator location term value effects m
, AbstractHole value
)
=> Interpreter (Resumable (Unspecialized value) ': effects) result rest (BadSyntax m) where
interpret
= interpret
. runBadSyntax
. raiseHandler (relay pure (\ (Resumable err@(Unspecialized _)) yield -> traceM ("Unspecialized:" <> show err) *> yield hole))

62
src/Analysis/Abstract/BadValues.hs
View File

@ -1,44 +1,38 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, KindSignatures, ScopedTypeVariables, TypeOperators, UndecidableInstances #-}
module Analysis.Abstract.BadValues where
import Control.Abstract.Analysis
import Data.Abstract.Evaluatable
import Data.Abstract.Environment as Env
import Prologue
import Data.ByteString.Char8 (pack)
import Prologue
newtype BadValues m (effects :: [* -> *]) a = BadValues (m effects a)
newtype BadValues m (effects :: [* -> *]) a = BadValues { runBadValues :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadValues m)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadValues m)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (BadValues m)
instance ( Effectful m
, Member (Resumable (ValueError location value)) effects
, Member (State [Name]) effects
, MonadAnalysis location term value effects m
, MonadValue location value effects (BadValues m)
instance ( Interpreter effects result rest m
, MonadEvaluator location term value effects m
, AbstractHole value
, Show value
)
=> MonadAnalysis location term value effects (BadValues m) where
type Effects location term value (BadValues m) = State [Name] ': Effects location term value m
analyzeTerm eval term = resume @(ValueError location value) (liftAnalyze analyzeTerm eval term) (
\yield error -> do
traceM ("ValueError" <> show error)
case error of
ScopedEnvironmentError{} -> do
env <- getEnv
yield (Env.push env)
CallError val -> yield val
StringError val -> yield (pack $ show val)
BoolError{} -> yield True
NumericError{} -> hole >>= yield
Numeric2Error{} -> hole >>= yield
ComparisonError{} -> hole >>= yield
NamespaceError{} -> getEnv >>= yield
BitwiseError{} -> hole >>= yield
Bitwise2Error{} -> hole >>= yield
KeyValueError{} -> hole >>= \x -> yield (x, x)
ArithmeticError{} -> hole >>= yield
)
analyzeModule = liftAnalyze analyzeModule
=> Interpreter (Resumable (ValueError location value) ': effects) result rest (BadValues m) where
interpret
= interpret
. runBadValues
. raiseHandler (relay pure (\ (Resumable err) yield -> traceM ("ValueError" <> show err) *> case err of
ScopedEnvironmentError{} -> do
env <- lower @m getEnv
yield (Env.push env)
CallError val -> yield val
StringError val -> yield (pack (show val))
BoolError{} -> yield True
NumericError{} -> yield hole
Numeric2Error{} -> yield hole
ComparisonError{} -> yield hole
NamespaceError{} -> lower @m getEnv >>= yield
BitwiseError{} -> yield hole
Bitwise2Error{} -> yield hole
KeyValueError{} -> yield (hole, hole)
ArithmeticError{} -> yield hole))

44
src/Analysis/Abstract/BadVariables.hs
View File

@ -1,4 +1,5 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, KindSignatures, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the Interpreter instance’s MonadEvaluator constraint
module Analysis.Abstract.BadVariables
( BadVariables
) where
@ -8,30 +9,27 @@ import Data.Abstract.Evaluatable
import Prologue
-- An analysis that resumes from evaluation errors and records the list of unresolved free variables.
newtype BadVariables m (effects :: [* -> *]) a = BadVariables (m effects a)
newtype BadVariables m (effects :: [* -> *]) a = BadVariables { runBadVariables :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadVariables m)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (BadVariables m)
instance ( Effectful m
, Member (Resumable (EvalError value)) effects
, Member (State [Name]) effects
, MonadAnalysis location term value effects m
, MonadValue location value effects (BadVariables m)
instance ( Interpreter effects (result, [Name]) rest m
, MonadEvaluator location term value effects m
, AbstractHole value
)
=> MonadAnalysis location term value effects (BadVariables m) where
type Effects location term value (BadVariables m) = State [Name] ': Effects location term value m
analyzeTerm eval term = resume @(EvalError value) (liftAnalyze analyzeTerm eval term) (
\yield err -> do
traceM ("EvalError" <> show err)
case err of
DefaultExportError{} -> yield ()
ExportError{} -> yield ()
IntegerFormatError{} -> yield 0
FloatFormatError{} -> yield 0
RationalFormatError{} -> yield 0
FreeVariableError name -> raise (modify' (name :)) >> hole >>= yield
FreeVariablesError names -> raise (modify' (names <>)) >> yield (fromMaybeLast "unknown" names))
analyzeModule = liftAnalyze analyzeModule
=> Interpreter (Resumable (EvalError value) ': State [Name] ': effects) result rest (BadVariables m) where
interpret
= interpret
. runBadVariables
. raiseHandler
( flip runState []
. relay pure (\ (Resumable err) yield -> traceM ("EvalError" <> show err) *> case err of
DefaultExportError{} -> yield ()
ExportError{} -> yield ()
IntegerFormatError{} -> yield 0
FloatFormatError{} -> yield 0
RationalFormatError{} -> yield 0
FreeVariableError name -> modify' (name :) *> yield hole
FreeVariablesError names -> modify' (names <>) *> yield (fromMaybeLast "unknown" names)))

33
src/Analysis/Abstract/Caching.hs
View File

@ -1,9 +1,11 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, KindSignatures, ScopedTypeVariables, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the Interpreter instance’s MonadEvaluator constraint
module Analysis.Abstract.Caching
( Caching
) where
import Control.Abstract.Analysis
import Control.Monad.Effect hiding (interpret)
import Data.Abstract.Address
import Data.Abstract.Cache
import Data.Abstract.Configuration
@ -19,7 +21,7 @@ type CachingEffects location term value effects
': effects
-- | A (coinductively-)cached analysis suitable for guaranteeing termination of (suitably finitized) analyses over recursive programs.
newtype Caching m (effects :: [* -> *]) a = Caching (m effects a)
newtype Caching m (effects :: [* -> *]) a = Caching { runCaching :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (Caching m)
@ -73,9 +75,6 @@ instance ( Alternative (m effects)
, Ord value
)
=> MonadAnalysis location term value effects (Caching m) where
-- We require the 'CachingEffects' in addition to the underlying analysis’ 'Effects'.
type Effects location term value (Caching m) = CachingEffects location term value (Effects location term value m)
-- Analyze a term using the in-cache as an oracle & storing the results of the analysis in the out-cache.
analyzeTerm recur e = do
c <- getConfiguration (embedSubterm e)
@ -92,15 +91,18 @@ instance ( Alternative (m effects)
cache <- converge (\ prevCache -> isolateCache $ do
putHeap (configurationHeap c)
-- We need to reset fresh generation so that this invocation converges.
reset 0
reset 0 $
-- This is subtle: though the calling context supports nondeterminism, we want
-- to corral all the nondeterminism that happens in this @eval@ invocation, so
-- that it doesn't "leak" to the calling context and diverge (otherwise this
-- would never complete). We don’t need to use the values, so we 'gather' the
-- nondeterministic values into @()@.
withOracle prevCache (raise (gather (const ()) (lower (liftAnalyze analyzeModule recur m))))) mempty
withOracle prevCache (raise (gather (const ()) (lower (liftAnalyze analyzeModule recur m))))) mempty
maybe empty scatter (cacheLookup c cache)
reset :: (Effectful m, Member Fresh effects) => Int -> m effects a -> m effects a
reset start = raiseHandler (interposeState start (const pure) (\ counter Fresh yield -> (yield $! succ counter) counter))
-- | Iterate a monadic action starting from some initial seed until the results converge.
--
-- This applies the Kleene fixed-point theorem to finitize a monotone action. cf https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem
@ -119,3 +121,20 @@ converge f = loop
-- | Nondeterministically write each of a collection of stores & return their associated results.
scatter :: (Alternative (m effects), Foldable t, MonadEvaluator location term value effects m) => t (a, Heap location value) -> m effects a
scatter = foldMapA (\ (value, heap') -> putHeap heap' $> value)
instance ( Interpreter effects ([result], Cache location term value) rest m
, MonadEvaluator location term value effects m
, Ord (Cell location value)
, Ord location
, Ord term
, Ord value
)
=> Interpreter (NonDet ': Reader (Cache location term value) ': State (Cache location term value) ': effects) result rest (Caching m) where
interpret
= interpret
. runCaching
. raiseHandler
( flip runState mempty
. flip runReader mempty
. makeChoiceA @[])

17
src/Analysis/Abstract/Collecting.hs
View File

@ -1,4 +1,5 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the Interpreter instance’s MonadEvaluator constraint
module Analysis.Abstract.Collecting
( Collecting
) where
@ -10,7 +11,7 @@ import Data.Abstract.Heap
import Data.Abstract.Live
import Prologue
newtype Collecting m (effects :: [* -> *]) a = Collecting (m effects a)
newtype Collecting m (effects :: [* -> *]) a = Collecting { runCollecting :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
instance ( Effectful m
@ -29,10 +30,6 @@ instance ( Effectful m
, ValueRoots location value
)
=> MonadAnalysis location term value effects (Collecting m) where
type Effects location term value (Collecting m)
= Reader (Live location value)
': Effects location term value m
-- Small-step evaluation which garbage-collects any non-rooted addresses after evaluating each term.
analyzeTerm recur term = do
roots <- askRoots
@ -76,3 +73,11 @@ reachable roots heap = go mempty roots
Just (a, as) -> go (liveInsert a seen) (case heapLookupAll a heap of
Just values -> liveDifference (foldr ((<>) . valueRoots) mempty values <> as) seen
_ -> seen)
instance ( Interpreter effects result rest m
, MonadEvaluator location term value effects m
, Ord location
)
=> Interpreter (Reader (Live location value) ': effects) result rest (Collecting m) where
interpret = interpret . runCollecting . raiseHandler (`runReader` mempty)

14
src/Analysis/Abstract/Dead.hs
View File

@ -1,4 +1,5 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the Interpreter instance’s MonadEvaluator constraint
module Analysis.Abstract.Dead
( DeadCode
) where
@ -10,7 +11,7 @@ import Data.Set (delete)
import Prologue
-- | An analysis tracking dead (unreachable) code.
newtype DeadCode m (effects :: [* -> *]) a = DeadCode (m effects a)
newtype DeadCode m (effects :: [* -> *]) a = DeadCode { runDeadCode :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (DeadCode m)
@ -43,8 +44,6 @@ instance ( Corecursive term
, Recursive term
)
=> MonadAnalysis location term value effects (DeadCode m) where
type Effects location term value (DeadCode m) = State (Dead term) ': Effects location term value m
analyzeTerm recur term = do
revive (embedSubterm term)
liftAnalyze analyzeTerm recur term
@ -52,3 +51,10 @@ instance ( Corecursive term
analyzeModule recur m = do
killAll (subterms (subterm (moduleBody m)))
liftAnalyze analyzeModule recur m
instance ( Interpreter effects (result, Dead term) rest m
, MonadEvaluator location term value effects m
, Ord term
)
=> Interpreter (State (Dead term) ': effects) result rest (DeadCode m) where
interpret = interpret . runDeadCode . raiseHandler (`runState` mempty)

18
src/Analysis/Abstract/Erroring.hs Normal file
View File

@ -0,0 +1,18 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures, TypeOperators, UndecidableInstances #-}
module Analysis.Abstract.Erroring
( Erroring
) where
import Control.Abstract.Analysis
import Prologue
-- | An analysis that fails on errors.
newtype Erroring (exc :: * -> *) m (effects :: [* -> *]) a = Erroring { runErroring :: m effects a }
deriving (Alternative, Applicative, Effectful, Functor, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (Erroring exc m)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (Erroring exc m)
instance Interpreter effects (Either (SomeExc exc) result) rest m
=> Interpreter (Resumable exc ': effects) result rest (Erroring exc m) where
interpret = interpret . runErroring . raiseHandler runError

47
src/Analysis/Abstract/Evaluating.hs
View File

@ -1,20 +1,23 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Analysis.Abstract.Evaluating
( Evaluating
) where
import Control.Abstract.Analysis
import Control.Monad.Effect
import Control.Monad.Effect.Exception as Exc
import Control.Monad.Effect.Resumable as Res
import Data.Abstract.Address
import Data.Abstract.Configuration
import Data.Abstract.Environment as Env
import Data.Abstract.Environment
import Data.Abstract.Evaluatable
import Data.Abstract.Module
import Data.Abstract.ModuleTable
import Data.Abstract.Origin
import Prologue
import Data.Empty
import Prologue hiding (empty)
-- | An analysis evaluating @term@s to @value@s with a list of @effects@ using 'Evaluatable', and producing incremental results of type @a@.
newtype Evaluating location term value effects a = Evaluating (Eff effects a)
newtype Evaluating location term value effects a = Evaluating { runEvaluating :: Eff effects a }
deriving (Applicative, Functor, Effectful, Monad)
deriving instance Member NonDet effects => Alternative (Evaluating location term value effects)
@ -23,12 +26,7 @@ deriving instance Member NonDet effects => Alternative (Evaluating location term
type EvaluatingEffects location term value
= '[ Exc (ReturnThrow value)
, Exc (LoopThrow value)
, Resumable (EvalError value)
, Resumable (ResolutionError value)
, Resumable (LoadError term value)
, Resumable (ValueError location value)
, Resumable (Unspecialized value)
, Resumable (AddressError location value)
, Fail -- Failure with an error message
, Fresh -- For allocating new addresses and/or type variables.
, Reader (SomeOrigin term) -- The current term’s origin.
@ -55,8 +53,33 @@ instance ( Corecursive term
, Recursive term
)
=> MonadAnalysis location term value effects (Evaluating location term value) where
type Effects location term value (Evaluating location term value) = EvaluatingEffects location term value
analyzeTerm eval term = pushOrigin (termOrigin (embedSubterm term)) (eval term)
analyzeModule eval m = pushOrigin (moduleOrigin (subterm <$> m)) (eval m)
instance ( Ord location
, Semigroup (Cell location value)
)
=> Interpreter
(EvaluatingEffects location term value) result
( Either String
(Either (SomeExc (LoadError term value))
(Either (LoopThrow value)
(Either (ReturnThrow value)
result)))
, EvaluatorState location term value)
(Evaluating location term value) where
interpret
= interpret
. runEvaluating
. raiseHandler
( flip runState empty -- State (EvaluatorState location term value)
. flip runReader empty -- Reader (Environment location value)
. flip runReader empty -- Reader (ModuleTable [Module term])
. flip runReader empty -- Reader (SomeOrigin term)
. flip runFresh' 0
. runFail
. Res.runError
. Exc.runError
. Exc.runError)

14
src/Analysis/Abstract/ImportGraph.hs
View File

@ -1,5 +1,4 @@
{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving,
TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, KindSignatures, ScopedTypeVariables, TypeOperators, UndecidableInstances #-}
module Analysis.Abstract.ImportGraph
( ImportGraph(..)
, renderImportGraph
@ -54,7 +53,7 @@ style = (defaultStyle vertexName)
edgeAttributes Variable{} Module{} = [ "color" := "blue" ]
edgeAttributes _ _ = []
newtype ImportGraphing m (effects :: [* -> *]) a = ImportGraphing (m effects a)
newtype ImportGraphing m (effects :: [* -> *]) a = ImportGraphing { runImportGraphing :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (ImportGraphing m)
@ -66,12 +65,10 @@ instance ( Effectful m
, Member (State ImportGraph) effects
, Member Syntax.Identifier syntax
, MonadAnalysis (Located location term) term value effects m
, term ~ Term (Union syntax) ann
, Show ann
, term ~ Term (Union syntax) ann
)
=> MonadAnalysis (Located location term) term value effects (ImportGraphing m) where
type Effects (Located location term) term value (ImportGraphing m) = State ImportGraph ': Effects (Located location term) term value m
analyzeTerm eval term@(In _ syntax) = do
case prj syntax of
Just (Syntax.Identifier name) -> do
@ -169,3 +166,8 @@ vertexToType :: Vertex -> Text
vertexToType Package{} = "package"
vertexToType Module{} = "module"
vertexToType Variable{} = "variable"
instance Interpreter effects (result, ImportGraph) rest m
=> Interpreter (State ImportGraph ': effects) result rest (ImportGraphing m) where
interpret = interpret . runImportGraphing . raiseHandler (`runState` mempty)

33
src/Analysis/Abstract/Quiet.hs
View File

@ -1,33 +0,0 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, TypeApplications, TypeFamilies, UndecidableInstances #-}
module Analysis.Abstract.Quiet
( Quietly
) where
import Control.Abstract.Analysis
import Data.Abstract.Evaluatable
import Prologue
-- | An analysis which resumes exceptions instead of failing.
--
-- Use it by composing it onto an analysis:
--
-- > runAnalysis @(Quietly (Evaluating term value)) (…)
--
-- Note that exceptions thrown by other analyses may not be caught if 'Quietly' doesn’t know about them, i.e. if they’re not part of the generic 'MonadValue', 'MonadAddressable', etc. machinery.
newtype Quietly m (effects :: [* -> *]) a = Quietly (m effects a)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (Quietly m)
instance ( Effectful m
, Member (Resumable (Unspecialized value)) effects
, MonadAnalysis location term value effects m
, MonadValue location value effects (Quietly m)
)
=> MonadAnalysis location term value effects (Quietly m) where
type Effects location term value (Quietly m) = Effects location term value m
analyzeTerm eval term = resume @(Unspecialized value) (liftAnalyze analyzeTerm eval term) (\yield err@(Unspecialized _) ->
traceM ("Unspecialized:" <> show err) >> hole >>= yield)
analyzeModule = liftAnalyze analyzeModule

14
src/Analysis/Abstract/Tracing.hs
View File

@ -1,4 +1,5 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures, ScopedTypeVariables, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the Interpreter instance’s MonadEvaluator constraint
module Analysis.Abstract.Tracing
( Tracing
) where
@ -13,7 +14,7 @@ import Prologue
-- | Trace analysis.
--
-- Instantiating @trace@ to @[]@ yields a linear trace analysis, while @Set@ yields a reachable state analysis.
newtype Tracing (trace :: * -> *) m (effects :: [* -> *]) a = Tracing (m effects a)
newtype Tracing (trace :: * -> *) m (effects :: [* -> *]) a = Tracing { runTracing :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (Tracing trace m)
@ -26,11 +27,16 @@ instance ( Corecursive term
, Reducer (Configuration location term value) (trace (Configuration location term value))
)
=> MonadAnalysis location term value effects (Tracing trace m) where
type Effects location term value (Tracing trace m) = Writer (trace (Configuration location term value)) ': Effects location term value m
analyzeTerm recur term = do
config <- getConfiguration (embedSubterm term)
raise (tell @(trace (Configuration location term value)) (Reducer.unit config))
liftAnalyze analyzeTerm recur term
analyzeModule = liftAnalyze analyzeModule
instance ( Interpreter effects (result, trace (Configuration location term value)) rest m
, MonadEvaluator location term value effects m
, Monoid (trace (Configuration location term value))
)
=> Interpreter (Writer (trace (Configuration location term value)) ': effects) result rest (Tracing trace m) where
interpret = interpret . runTracing . raiseHandler runWriter

45
src/Analysis/Abstract/TypeChecking.hs
View File

@ -1,4 +1,4 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures, ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, KindSignatures, TypeOperators, UndecidableInstances #-}
module Analysis.Abstract.TypeChecking
( TypeChecking
@ -8,35 +8,22 @@ import Control.Abstract.Analysis
import Data.Abstract.Type
import Prologue hiding (TypeError)
newtype TypeChecking m (effects :: [* -> *]) a = TypeChecking (m effects a)
newtype TypeChecking m (effects :: [* -> *]) a = TypeChecking { runTypeChecking :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (TypeChecking m)
deriving instance MonadEvaluator location term Type effects m => MonadEvaluator location term Type effects (TypeChecking m)
deriving instance MonadAnalysis location term Type effects m => MonadAnalysis location term Type effects (TypeChecking m)
instance ( Effectful m
, Alternative (m effects)
, MonadAnalysis location term value effects m
, Member (Resumable TypeError) effects
, Member NonDet effects
, MonadValue location value effects (TypeChecking m)
, value ~ Type
instance ( Interpreter effects (Either (SomeExc TypeError) result) rest m
, MonadEvaluator location term Type effects m
)
=> MonadAnalysis location term value effects (TypeChecking m) where
type Effects location term value (TypeChecking m) = Resumable TypeError ': Effects location term value m
analyzeTerm eval term =
resume @TypeError (liftAnalyze analyzeTerm eval term) (
\yield err -> case err of
NoValueError _ a -> yield a
-- TODO: These should all yield both sides of the exception,
-- but something is mysteriously busted in the innards of typechecking,
-- so doing that just yields an empty list in the result type, which isn't
-- extraordinarily helpful. Better for now to just die with an error and
-- tackle this issue in a separate PR.
BitOpError{} -> throwResumable err
NumOpError{} -> throwResumable err
UnificationError{} -> throwResumable err
)
analyzeModule = liftAnalyze analyzeModule
=> Interpreter (Resumable TypeError ': effects) result rest (TypeChecking m) where
interpret
= interpret
. runTypeChecking
-- TODO: We should handle TypeError by yielding both sides of the exception,
-- but something is mysteriously busted in the innards of typechecking,
-- so doing that just yields an empty list in the result type, which isn't
-- extraordinarily helpful. Better for now to just die with an error and
-- tackle this issue in a separate PR.
. raiseHandler runError

6
src/Control/Abstract/Addressable.hs
View File

@ -1,10 +1,10 @@
{-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE GADTs, UndecidableInstances #-}
module Control.Abstract.Addressable where
import Control.Abstract.Evaluator
import Control.Applicative
import Control.Effect
import Control.Effect.Fresh
import Control.Monad.Effect.Fresh
import Control.Monad.Effect.Resumable as Eff
import Data.Abstract.Address
import Data.Abstract.Environment (insert)
@ -57,7 +57,7 @@ letrec' name body = do
-- | 'Precise' locations are always 'alloc'ated a fresh 'Address', and 'deref'erence to the 'Latest' value written.
instance (Effectful m, Member Fresh effects, Monad (m effects)) => MonadAddressable Precise effects m where
derefCell _ = pure . unLatest
allocLoc _ = Precise <$> fresh
allocLoc _ = Precise <$> raise fresh
-- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically.
instance (Alternative (m effects), Effectful m, Member Fresh effects, Monad (m effects)) => MonadAddressable Monovariant effects m where

35
src/Control/Abstract/Analysis.hs
View File

@ -1,22 +1,19 @@
{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For runAnalysis
module Control.Abstract.Analysis
( MonadAnalysis(..)
, liftAnalyze
, runAnalysis
, SomeAnalysis(..)
, runSomeAnalysis
, module X
, Subterm(..)
, SubtermAlgebra
) where
import Control.Abstract.Addressable as X
import Control.Abstract.Evaluator as X
import Control.Abstract.Value as X
import Control.Effect as X
import Control.Effect.Fresh as X
import Control.Monad.Effect.Fail as X
import Control.Monad.Effect.Fresh as X
import Control.Monad.Effect.Internal as X (Eff, relay)
import Control.Monad.Effect.NonDet as X
import Control.Monad.Effect.Reader as X
import Control.Monad.Effect.State as X
@ -30,9 +27,6 @@ import Prologue
--
-- This typeclass is left intentionally unconstrained to avoid circular dependencies between it and other typeclasses.
class MonadEvaluator location term value effects m => MonadAnalysis location term value effects m where
-- | The effects necessary to run the analysis. Analyses which are composed on top of (wrap) other analyses should include the inner analyses 'Effects' in their own list.
type family Effects location term value m :: [* -> *]
-- | Analyze a term using the semantics of the current analysis.
analyzeTerm :: (Base term (Subterm term (outer effects value)) -> m effects value)
-> (Base term (Subterm term (outer effects value)) -> m effects value)
@ -57,25 +51,8 @@ liftAnalyze analyze recur term = coerce (analyze (coerceWith (sym Coercion) . r
--
-- This enables us to refer to the analysis type as e.g. @Analysis1 (Analysis2 Evaluating) Term Value@ without explicitly mentioning its effects (which are inferred to be simply its 'Effects').
runAnalysis :: ( Effectful m
, Effects location term value m ~ effects
, MonadAnalysis location term value effects m
, RunEffects effects a
, Interpreter effects a function m
)
=> m effects a
-> Final effects a
runAnalysis = X.run
-- | An abstraction over analyses.
data SomeAnalysis m result where
SomeAnalysis :: ( Effectful m
, effects ~ Effects location term value m
, MonadAnalysis location term value effects m
, RunEffects effects a
)
=> m effects a
-> SomeAnalysis m (Final effects a)
-- | Run an abstracted analysis.
runSomeAnalysis :: SomeAnalysis m result -> result
runSomeAnalysis (SomeAnalysis a) = X.run a
-> function
runAnalysis = interpret

7
src/Control/Abstract/Value.hs
View File

@ -1,6 +1,7 @@
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, Rank2Types #-}
module Control.Abstract.Value
( MonadValue(..)
, AbstractHole(..)
, Comparator(..)
, while
, doWhile
@ -31,6 +32,9 @@ data Comparator
= Concrete (forall a . Ord a => a -> a -> Bool)
| Generalized
class AbstractHole value where
hole :: value
-- | A 'Monad' abstracting the evaluation of (and under) binding constructs (functions, methods, etc).
--
-- This allows us to abstract the choice of whether to evaluate under binders for different value types.
@ -39,9 +43,6 @@ class (Monad (m effects), Show value) => MonadValue location value (effects :: [
-- TODO: This might be the same as the empty tuple for some value types
unit :: m effects value
-- | Construct an abstract hole.
hole :: m effects value
-- | Construct an abstract integral value.
integer :: Prelude.Integer -> m effects value

106
src/Control/Effect.hs
View File

@ -1,99 +1,22 @@
{-# LANGUAGE RankNTypes, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies, RankNTypes, TypeOperators #-}
module Control.Effect
( Control.Effect.run
, RunEffects(..)
, RunEffect(..)
, Effectful(..)
( Effectful(..)
, raiseHandler
, Interpreter(..)
, resume
, mergeEither
) where
import Control.Monad.Effect as Effect
import Control.Monad.Effect.Exception as Exception
import Control.Monad.Effect.Fail
import Control.Monad.Effect.NonDet
import Control.Monad.Effect.Reader
import Control.Monad.Effect.Resumable as Resumable
import Control.Monad.Effect.State
import Control.Monad.Effect.Writer
import Data.Empty as E
import Data.Semigroup.Reducer
import Prologue
import Control.Monad.Effect as Effect
import Control.Monad.Effect.Resumable as Resumable
-- | Run an 'Effectful' computation to completion, interpreting each effect with some sensible defaults, and return the 'Final' result.
run :: (Effectful m, RunEffects effects a) => m effects a -> Final effects a
run = runEffects . lower
-- | A typeclass to run a computation to completion, interpreting each effect with some sensible defaults.
class RunEffects fs a where
-- | The final result type of the computation, factoring in the results of any effects, e.g. pairing 'State' results with the final state, wrapping 'Fail' results in 'Either', etc.
type Final fs a
runEffects :: Eff fs a -> Final fs a
instance (RunEffect f a, RunEffects fs (Result f a)) => RunEffects (f ': fs) a where
type Final (f ': fs) a = Final fs (Result f a)
runEffects = runEffects . runEffect
instance RunEffects '[] a where
type Final '[] a = a
runEffects = Effect.run
-- | A typeclass to interpret a single effect with some sensible defaults (defined per-effect).
class RunEffect f a where
-- | The incremental result of an effect w.r.t. the parameter value, factoring in the interpretation of the effect.
type Result f a
type instance Result f a = a
-- | Interpret the topmost effect in a computation with some sensible defaults (defined per-effect), and return the incremental 'Result'.
runEffect :: Eff (f ': fs) a -> Eff fs (Result f a)
-- | 'State' effects with 'Monoid'al states are interpreted starting from the 'mempty' state value into a pair of result value and final state.
instance E.Empty b => RunEffect (State b) a where
type Result (State b) a = (a, b)
runEffect = flip runState E.empty
-- | 'Reader' effects with 'Monoid'al environments are interpreted starting from the 'mempty' environment value.
instance Monoid b => RunEffect (Reader b) a where
runEffect = flip runReader mempty
-- | 'Fail' effects are interpreted into 'Either' s.t. failures are in 'Left' and successful results are in 'Right'.
instance RunEffect Fail a where
type Result Fail a = Either String a
runEffect = runFail
-- | 'Writer' effects are interpreted into a pair of result value and final log.
instance Monoid w => RunEffect (Writer w) a where
type Result (Writer w) a = (a, w)
runEffect = runWriter
-- | 'NonDet' effects are interpreted into a nondeterministic set of result values.
instance Ord a => RunEffect NonDet a where
type Result NonDet a = Set a
runEffect = runNonDet unit
-- | 'Resumable' effects are interpreted into 'Either' s.t. failures are in 'Left' and successful results are in 'Right'.
instance RunEffect (Resumable exc) a where
type Result (Resumable exc) a = Either (SomeExc exc) a
runEffect = Resumable.runError
-- | Standard (non-resumable) exceptions, as above, are rendered into 'Left's and 'Right's.
instance RunEffect (Exc exc) a where
type Result (Exc exc) a = Either exc a
runEffect = Exception.runError
resume :: (Resumable exc :< e, Effectful m) => m e a -> (forall v . (v -> m e a) -> exc v -> m e a) -> m e a
resume :: (Member (Resumable exc) e, Effectful m) => m e a -> (forall v . (v -> m e a) -> exc v -> m e a) -> m e a
resume m handle = raise (resumeError (lower m) (\yield -> lower . handle (raise . yield)))
-- | Reassociate 'Either's, combining errors into 'Left' values and successes in a single level of 'Right'.
mergeEither :: Either a (Either b c) -> Either (Either a b) c
mergeEither = either (Left . Left) (either (Left . Right) Right)
-- | Types wrapping 'Eff' actions.
--
-- Most instances of 'Effectful' will be derived using @-XGeneralizedNewtypeDeriving@, with these ultimately bottoming out on the instance for 'Eff' (for which 'raise' and 'lower' are simply the identity). Because of this, types can be nested arbitrarily deeply and still call 'raise'/'lower' just once to get at the (ultimately) underlying 'Eff'.
class Effectful (m :: [* -> *] -> * -> *) where
class Effectful m where
-- | Raise an action in 'Eff' into an action in @m@.
raise :: Eff effects a -> m effects a
-- | Lower an action in @m@ into an action in 'Eff'.
@ -102,3 +25,16 @@ class Effectful (m :: [* -> *] -> * -> *) where
instance Effectful Eff where
raise = id
lower = id
raiseHandler :: Effectful m => (Eff effectsA a -> Eff effectsB b) -> m effectsA a -> m effectsB b
raiseHandler handler = raise . handler . lower
-- | Interpreters determine and interpret a list of effects, optionally taking extra arguments.
--
-- Instances will generally be defined recursively in terms of underlying interpreters, bottoming out with the instance for 'Eff' which uses 'Effect.run' to produce a final value.
class Effectful m => Interpreter effects result function m | m -> effects, m result -> function where
interpret :: m effects result -> function
instance Interpreter '[] result result Eff where
interpret = Effect.run

27
src/Control/Effect/Fresh.hs
View File

@ -1,27 +0,0 @@
{-# LANGUAGE GADTs, MultiParamTypeClasses, TypeOperators, UndecidableInstances #-}
module Control.Effect.Fresh where
import Control.Effect
import Control.Monad.Effect.Internal
-- | An effect offering a (resettable) sequence of always-incrementing, and therefore “fresh,” type variables.
data Fresh a where
-- | Request a reset of the sequence of variable names.
Reset :: Int -> Fresh ()
-- | Request a fresh variable name.
Fresh :: Fresh Int
-- | Get a fresh variable name, guaranteed unused (since the last 'reset').
fresh :: (Effectful m, Member Fresh effects) => m effects Int
fresh = raise (send Fresh)
-- | Reset the sequence of variable names. Useful to avoid complicated alpha-equivalence comparisons when iteratively recomputing the results of an analysis til convergence.
reset :: (Effectful m, Member Fresh effects) => Int -> m effects ()
reset = raise . send . Reset
-- | 'Fresh' effects are interpreted starting from 0, incrementing the current name with each request for a fresh name, and overwriting the counter on reset.
instance RunEffect Fresh a where
runEffect = relayState (0 :: Int) (const pure) (\ s action k -> case action of
Fresh -> k (succ s) s
Reset s' -> k s' ())

9
src/Data/Abstract/Evaluatable.hs
View File

@ -55,7 +55,6 @@ type MonadEvaluatable location term value effects m =
, Member (Exc.Exc (LoopThrow value)) effects
, Member Fail effects
, Member (Resumable (Unspecialized value)) effects
, Member (Resumable (ValueError location value)) effects
, Member (Resumable (LoadError term value)) effects
, Member (Resumable (EvalError value)) effects
, Member (Resumable (ResolutionError value)) effects
@ -119,7 +118,7 @@ data EvalError value resume where
-- | Look up and dereference the given 'Name', throwing an exception for free variables.
variable :: MonadEvaluatable location term value effects m => Name -> m effects value
variable :: (Member (Resumable (AddressError location value)) effects, Member (Resumable (EvalError value)) effects, MonadAddressable location effects m, MonadEvaluator location term value effects m) => Name -> m effects value
variable name = lookupWith deref name >>= maybeM (throwResumable (FreeVariableError name))
deriving instance Eq (EvalError a b)
@ -137,13 +136,13 @@ instance Eq1 (EvalError term) where
liftEq _ _ _ = False
throwValueError :: MonadEvaluatable location term value effects m => ValueError location value resume -> m effects resume
throwValueError :: (Member (Resumable (ValueError location value)) effects, MonadEvaluator location term value effects m) => ValueError location value resume -> m effects resume
throwValueError = throwResumable
throwLoadError :: MonadEvaluatable location term value effects m => LoadError term value resume -> m effects resume
throwLoadError :: (Member (Resumable (LoadError term value)) effects, MonadEvaluator location term value effects m) => LoadError term value resume -> m effects resume
throwLoadError = throwResumable
throwEvalError :: MonadEvaluatable location term value effects m => EvalError value resume -> m effects resume
throwEvalError :: (Member (Resumable (EvalError value)) effects, MonadEvaluator location term value effects m) => EvalError value resume -> m effects resume
throwEvalError = throwResumable
throwLoop :: MonadEvaluatable location term value effects m => LoopThrow value -> m effects a

23
src/Data/Abstract/Type.hs
View File

@ -38,21 +38,18 @@ data Type
-- TODO: À la carte representation of types.
data TypeError resume where
NoValueError :: Type -> a -> TypeError a
NumOpError :: Type -> Type -> TypeError Type
BitOpError :: Type -> Type -> TypeError Type
UnificationError :: Type -> Type -> TypeError Type
deriving instance Show resume => Show (TypeError resume)
deriving instance Show (TypeError resume)
instance Show1 TypeError where
liftShowsPrec _ _ _ (NoValueError v _) = showString "NoValueError " . shows v
liftShowsPrec _ _ _ (NumOpError l r) = showString "NumOpError " . shows [l, r]
liftShowsPrec _ _ _ (BitOpError l r) = showString "BitOpError " . shows [l, r]
liftShowsPrec _ _ _ (UnificationError l r) = showString "UnificationError " . shows [l, r]
instance Eq1 TypeError where
liftEq _ (NoValueError a _) (NoValueError b _) = a == b
liftEq _ (BitOpError a b) (BitOpError c d) = a == c && b == d
liftEq _ (NumOpError a b) (NumOpError c d) = a == c && b == d
liftEq _ (UnificationError a b) (UnificationError c d) = a == c && b == d
@ -74,6 +71,10 @@ unify t1 t2
instance Ord location => ValueRoots location Type where
valueRoots _ = mempty
instance AbstractHole Type where
hole = Hole
-- | Discard the value arguments (if any), constructing a 'Type' instead.
instance ( Alternative (m effects)
, Member Fresh effects
@ -86,14 +87,13 @@ instance ( Alternative (m effects)
lambda names (Subterm _ body) = do
(env, tvars) <- foldr (\ name rest -> do
a <- alloc name
tvar <- Var <$> fresh
tvar <- Var <$> raise fresh
assign a tvar
(env, tvars) <- rest
pure (Env.insert name a env, tvar : tvars)) (pure mempty) names
ret <- localEnv (mappend env) body
pure (Product tvars :-> ret)
hole = pure Hole
unit = pure Unit
integer _ = pure Int
boolean _ = pure Bool
@ -113,9 +113,12 @@ instance ( Alternative (m effects)
scopedEnvironment _ = pure mempty
asString _ = throwResumable (NoValueError String "")
asPair _ = throwResumable (NoValueError (Product []) (Hole, Hole))
asBool _ = throwResumable (NoValueError Bool True)
asString t = unify t String $> ""
asPair t = do
t1 <- raise fresh
t2 <- raise fresh
unify t (Product [Var t1, Var t2]) $> (Var t1, Var t2)
asBool t = unify t Bool *> (pure True <|> pure False)
isHole ty = pure (ty == Hole)
@ -146,7 +149,7 @@ instance ( Alternative (m effects)
_ -> unify left right $> Bool
call op params = do
tvar <- fresh
tvar <- raise fresh
paramTypes <- sequenceA params
let needed = Product paramTypes :-> Var tvar
unified <- op `unify` needed

14
src/Data/Abstract/Value.hs
View File

@ -198,9 +198,15 @@ instance Ord location => ValueRoots location (Value location) where
| otherwise = mempty
instance AbstractHole (Value location) where
hole = injValue Hole
-- | Construct a 'Value' wrapping the value arguments (if any).
instance (Monad (m effects), MonadEvaluatable location term (Value location) effects m) => MonadValue location (Value location) effects m where
hole = pure . injValue $ Hole
instance ( Monad (m effects)
, Member (Resumable (ValueError location (Value location))) effects
, MonadEvaluatable location term (Value location) effects m
)
=> MonadValue location (Value location) effects m where
unit = pure . injValue $ Unit
integer = pure . injValue . Integer . Number.Integer
boolean = pure . injValue . Boolean
@ -247,7 +253,7 @@ instance (Monad (m effects), MonadEvaluatable location term (Value location) eff
ifthenelse cond if' else' = do
isHole <- isHole cond
if isHole then
hole
pure hole
else do
bool <- asBool cond
if bool then if' else else'
@ -280,7 +286,7 @@ instance (Monad (m effects), MonadEvaluatable location term (Value location) eff
tentative x i j = attemptUnsafeArithmetic (x i j)
-- Dispatch whatever's contained inside a 'Number.SomeNumber' to its appropriate 'MonadValue' ctor
specialize :: MonadEvaluatable location term value effects m => Either ArithException Number.SomeNumber -> m effects value
specialize :: (Member (Resumable (ValueError location value)) effects, MonadEvaluatable location term value effects m) => Either ArithException Number.SomeNumber -> m effects value
specialize (Left exc) = throwValueError (ArithmeticError exc)
specialize (Right (Number.SomeNumber (Number.Integer i))) = integer i
specialize (Right (Number.SomeNumber (Number.Ratio r))) = rational r

16
src/Semantic/Graph.hs
View File

@ -1,4 +1,4 @@
{-# LANGUAGE GADTs, ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
module Semantic.Graph where
import qualified Analysis.Abstract.ImportGraph as Abstract
@ -15,10 +15,10 @@ import Data.Abstract.Located
import Data.Abstract.Address
import Analysis.Abstract.BadAddresses
import Analysis.Abstract.BadModuleResolutions
import Analysis.Abstract.BadSyntax
import Analysis.Abstract.BadValues
import Analysis.Abstract.BadVariables
import Analysis.Abstract.Evaluating
import Analysis.Abstract.Quiet
import Data.Output
import Parsing.Parser
import Prologue hiding (MonadError (..))
@ -63,13 +63,12 @@ parseModule parser rootDir file = do
type ImportGraphAnalysis term effects value =
Abstract.ImportGraphing
(BadAddresses (BadModuleResolutions (BadVariables (BadValues (Quietly (Evaluating (Located Precise term) term (Value (Located Precise term))))))))
(BadAddresses (BadModuleResolutions (BadVariables (BadValues (BadSyntax (Evaluating (Located Precise term) term (Value (Located Precise term))))))))
effects
value
-- | Render the import graph for a given 'Package'.
graphImports :: (
Show ann
graphImports :: ( Show ann
, Ord ann
, Apply Analysis.Declarations1 syntax
, Apply Analysis.Evaluatable syntax
@ -80,10 +79,9 @@ graphImports :: (
, Apply Show1 syntax
, Member Syntax.Identifier syntax
, Members '[Exc SomeException, Task] effs
, term ~ Term (Union syntax) ann
)
=> Package term -> Eff effs Abstract.ImportGraph
graphImports package = analyze (Analysis.SomeAnalysis (Analysis.evaluatePackage package `asAnalysisForTypeOfPackage` package)) >>= extractGraph
=> Package (Term (Union syntax) ann) -> Eff effs Abstract.ImportGraph
graphImports package = analyze (Analysis.evaluatePackage package `asAnalysisForTypeOfPackage` package) >>= extractGraph
where
asAnalysisForTypeOfPackage :: ImportGraphAnalysis term effs value
-> Package term
@ -91,5 +89,5 @@ graphImports package = analyze (Analysis.SomeAnalysis (Analysis.evaluatePackage
asAnalysisForTypeOfPackage = const
extractGraph result = case result of
(Right (Right (Right (Right (Right (Right (Right (Right (Right ((((_, graph), _), _), _))))))))), _) -> pure $! graph
(Right (Right (Right (Right ((_, graph), _)))), _) -> pure graph
_ -> throwError (toException (Exc.ErrorCall ("graphImports: import graph rendering failed " <> show result)))

6
src/Semantic/Task.hs
View File

@ -88,7 +88,7 @@ parse :: Member Task effs => Parser term -> Blob -> Eff effs term
parse parser = send . Parse parser
-- | A task running some 'Analysis.MonadAnalysis' to completion.
analyze :: Member Task effs => Analysis.SomeAnalysis m result -> Eff effs result
analyze :: (Analysis.Interpreter analysisEffects result function m, Member Task effs) => m analysisEffects result -> Eff effs function
analyze = send . Analyze
-- | A task which decorates a 'Term' with values computed using the supplied 'RAlgebra' function.
@ -131,7 +131,7 @@ runTaskWithOptions options task = do
-- | An effect describing high-level tasks to be performed.
data Task output where
Parse :: Parser term -> Blob -> Task term
Analyze :: Analysis.SomeAnalysis m result -> Task result
Analyze :: Analysis.Interpreter effects result function m => m effects result -> Task function
Decorate :: Functor f => RAlgebra (TermF f (Record fields)) (Term f (Record fields)) field -> Term f (Record fields) -> Task (Term f (Record (field ': fields)))
Diff :: Differ syntax ann1 ann2 -> Term syntax ann1 -> Term syntax ann2 -> Task (Diff syntax ann1 ann2)
Render :: Renderer input output -> input -> Task output
@ -140,7 +140,7 @@ data Task output where
runTaskF :: Members '[Reader Options, Telemetry, Exc SomeException, IO] effs => Eff (Task ': effs) a -> Eff effs a
runTaskF = interpret $ \ task -> case task of
Parse parser blob -> runParser blob parser
Analyze analysis -> pure (Analysis.runSomeAnalysis analysis)
Analyze analysis -> pure (Analysis.runAnalysis analysis)
Decorate algebra term -> pure (decoratorWithAlgebra algebra term)
Semantic.Task.Diff differ term1 term2 -> pure (differ term1 term2)
Render renderer input -> pure (renderer input)

27
src/Semantic/Util.hs
View File

@ -1,15 +1,17 @@
-- MonoLocalBinds is to silence a warning about a simplifiable constraint.
{-# LANGUAGE MonoLocalBinds, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
{-# LANGUAGE MonoLocalBinds, TypeOperators #-}
{-# OPTIONS_GHC -Wno-missing-signatures #-}
module Semantic.Util where
import Analysis.Abstract.BadAddresses
import Analysis.Abstract.BadModuleResolutions
import Analysis.Abstract.BadSyntax
import Analysis.Abstract.BadValues
import Analysis.Abstract.BadVariables
import Analysis.Abstract.Caching
import Analysis.Abstract.Erroring
import Analysis.Abstract.Evaluating as X
import Analysis.Abstract.ImportGraph
import Analysis.Abstract.Quiet
import Analysis.Abstract.TypeChecking
import Analysis.Declaration
import Control.Abstract.Analysis
@ -43,13 +45,26 @@ import qualified Language.Python.Assignment as Python
import qualified Language.Ruby.Assignment as Ruby
import qualified Language.TypeScript.Assignment as TypeScript
type JustEvaluating term = Evaluating (Located Precise term) term (Value (Located Precise term))
type EvaluatingWithHoles term = BadModuleResolutions (BadVariables (BadValues (Quietly (Evaluating (Located Precise term) term (Value (Located Precise term))))))
-- type TestEvaluating term = Evaluating Precise term (Value Precise)
type JustEvaluating term
= Erroring (AddressError (Located Precise term) (Value (Located Precise term)))
( Erroring (EvalError (Value (Located Precise term)))
( Erroring (ResolutionError (Value (Located Precise term)))
( Erroring (Unspecialized (Value (Located Precise term)))
( Erroring (ValueError (Located Precise term) (Value (Located Precise term)))
( Evaluating (Located Precise term) term (Value (Located Precise term)))))))
type EvaluatingWithHoles term = BadAddresses (BadModuleResolutions (BadVariables (BadValues (BadSyntax (Evaluating (Located Precise term) term (Value (Located Precise term)))))))
type ImportGraphingWithHoles term = ImportGraphing (EvaluatingWithHoles term)
-- The order is significant here: Caching has to come on the outside, or the RunEffect instance for NonDet
-- will expect the TypeError exception type to have an Ord instance, which is wrong.
type Checking term = Caching (TypeChecking (Evaluating Monovariant term Type))
type Checking term
= Caching
( TypeChecking
( Erroring (AddressError Monovariant Type)
( Erroring (EvalError Type)
( Erroring (ResolutionError Type)
( Erroring (Unspecialized Type)
( Evaluating Monovariant term Type))))))
evalGoProject path = runAnalysis @(JustEvaluating Go.Term) <$> evaluateProject goParser Language.Go Nothing path
evalRubyProject path = runAnalysis @(JustEvaluating Ruby.Term) <$> evaluateProject rubyParser Language.Ruby rubyPrelude path

2
test/Analysis/Ruby/Spec.hs
View File

@ -30,7 +30,7 @@ spec = parallel $ do
it "evaluates load with wrapper" $ do
res <- evaluate "load-wrap.rb"
fst res `shouldBe` Right (Right (Right (Right (Right (Right (Left (SomeExc (FreeVariableError "foo"))))))))
fst res `shouldBe` Right (Right (Right (Right (Right (Right (Right (Left (SomeExc (FreeVariableError "foo")))))))))
environment (snd res) `shouldBe` [ ("Object", addr 0) ]
it "evaluates subclass" $ do

2
test/Analysis/TypeScript/Spec.hs
View File

@ -34,7 +34,7 @@ spec = parallel $ do
it "fails exporting symbols not defined in the module" $ do
v <- fst <$> evaluate "bad-export.ts"
v `shouldBe` Right (Right (Right (Right (Right (Right (Left (SomeExc $ ExportError "foo.ts" (Name "pip"))))))))
v `shouldBe` Right (Right (Right (Right (Right (Right (Right (Left (SomeExc (ExportError "foo.ts" (Name "pip"))))))))))
it "evaluates early return statements" $ do
res <- evaluate "early-return.ts"

14
test/SpecHelpers.hs
View File

@ -12,8 +12,13 @@ module SpecHelpers (
, TestEvaluating
, ) where
import Analysis.Abstract.Erroring
import Analysis.Abstract.Evaluating
import Control.Abstract.Addressable
import Control.Abstract.Evaluator as X (EvaluatorState(..))
import Control.Abstract.Value
import Data.Abstract.Address as X
import Data.Abstract.Evaluatable
import Data.Abstract.FreeVariables as X hiding (dropExtension)
import Data.Abstract.Heap as X
import Data.Abstract.ModuleTable as X hiding (lookup)
@ -50,7 +55,6 @@ import Test.LeanCheck as X
import qualified Data.ByteString as B
import qualified Semantic.IO as IO
import Data.Abstract.Value
import Analysis.Abstract.Evaluating
-- | Returns an s-expression formatted diff for the specified FilePath pair.
diffFilePaths :: Both FilePath -> IO ByteString
@ -68,7 +72,13 @@ readFilePair paths = let paths' = fmap file paths in
readFileVerbatim :: FilePath -> IO Verbatim
readFileVerbatim = fmap verbatim . B.readFile
type TestEvaluating term = Evaluating Precise term (Value Precise)
type TestEvaluating term
= Erroring (AddressError Precise (Value Precise))
( Erroring (EvalError (Value Precise))
( Erroring (ResolutionError (Value Precise))
( Erroring (Unspecialized (Value Precise))
( Erroring (ValueError Precise (Value Precise))
( Evaluating Precise term (Value Precise))))))
ns n = Just . Latest . Just . injValue . Namespace n
addr = Address . Precise

2
vendor/effects vendored

@ -1 +1 @@
Subproject commit 06b08cd6354b109581388d40181e96de856b698a
Subproject commit 635733602419b0a0da86bf06a1de3d5bc67ab3d4