1
1
mirror of https://github.com/github/semantic.git synced 2024-12-21 13:51:44 +03:00

Merge remote-tracking branch 'origin/master' into resumable-type-errors

This commit is contained in:
Patrick Thomson 2018-04-24 15:50:20 -04:00
commit 4fd34d0412
29 changed files with 541 additions and 570 deletions

View File

@ -2,32 +2,29 @@
module Analysis.Abstract.BadAddresses where
import Control.Abstract.Analysis
import Analysis.Abstract.Evaluating
import Data.Abstract.Address
import Prologue
newtype BadAddresses m (effects :: [* -> *]) a = BadAddresses (m effects a)
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadControl term (m effects) => MonadControl term (BadAddresses m effects)
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (BadAddresses m effects)
deriving instance MonadHeap location value (m effects) => MonadHeap location value (BadAddresses m effects)
deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (BadAddresses m effects)
deriving instance MonadEvaluator location term value (m effects) => MonadEvaluator location term value (BadAddresses m effects)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadAddresses m)
instance ( Effectful m
, Member (Resumable (AddressError location value)) effects
, Member (State (EvaluatingState location term value)) effects
, MonadAnalysis location term value (m effects)
, MonadValue location value (BadAddresses m effects)
, MonadAnalysis location term value effects m
, MonadValue location value effects (BadAddresses m)
, Monoid (Cell location value)
, Show location
)
=> MonadAnalysis location term value (BadAddresses m effects) where
type Effects location term value (BadAddresses m effects) = Effects location term value (m effects)
=> 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
(UninitializedAddress _) -> hole >>= yield)
UnallocatedAddress _ -> yield mempty
UninitializedAddress _ -> hole >>= yield)
analyzeModule = liftAnalyze analyzeModule

View File

@ -3,27 +3,21 @@ module Analysis.Abstract.BadModuleResolutions where
import Control.Abstract.Analysis
import Data.Abstract.Evaluatable
import Analysis.Abstract.Evaluating
import Prologue
newtype BadModuleResolutions m (effects :: [* -> *]) a = BadModuleResolutions (m effects a)
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadControl term (m effects) => MonadControl term (BadModuleResolutions m effects)
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (BadModuleResolutions m effects)
deriving instance MonadHeap location value (m effects) => MonadHeap location value (BadModuleResolutions m effects)
deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (BadModuleResolutions m effects)
deriving instance MonadEvaluator location term value (m effects) => MonadEvaluator location term value (BadModuleResolutions m effects)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadModuleResolutions m)
instance ( Effectful m
, Member (Resumable (ResolutionError value)) effects
, Member (State (EvaluatingState location term value)) effects
, Member (State [Name]) effects
, MonadAnalysis location term value (m effects)
, MonadValue location value (BadModuleResolutions m effects)
, MonadAnalysis location term value effects m
, MonadValue location value effects (BadModuleResolutions m)
)
=> MonadAnalysis location term value (BadModuleResolutions m effects) where
type Effects location term value (BadModuleResolutions m effects) = State [Name] ': Effects location term value (m effects)
=> 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

View File

@ -3,29 +3,23 @@ module Analysis.Abstract.BadValues where
import Control.Abstract.Analysis
import Data.Abstract.Evaluatable
import Analysis.Abstract.Evaluating
import Data.Abstract.Environment as Env
import Prologue
import Data.ByteString.Char8 (pack)
newtype BadValues m (effects :: [* -> *]) a = BadValues (m effects a)
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadControl term (m effects) => MonadControl term (BadValues m effects)
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (BadValues m effects)
deriving instance MonadHeap location value (m effects) => MonadHeap location value (BadValues m effects)
deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (BadValues m effects)
deriving instance MonadEvaluator location term value (m effects) => MonadEvaluator location term value (BadValues m effects)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadValues m)
instance ( Effectful m
, Member (Resumable (ValueError location value)) effects
, Member (State (EvaluatingState location term value)) effects
, Member (State [Name]) effects
, MonadAnalysis location term value (m effects)
, MonadValue location value (BadValues m effects)
, MonadAnalysis location term value effects m
, MonadValue location value effects (BadValues m)
)
=> MonadAnalysis location term value (BadValues m effects) where
type Effects location term value (BadValues m effects) = State [Name] ': Effects location term value (m effects)
=> 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

View File

@ -9,22 +9,18 @@ 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)
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadControl term (m effects) => MonadControl term (BadVariables m effects)
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (BadVariables m effects)
deriving instance MonadHeap location value (m effects) => MonadHeap location value (BadVariables m effects)
deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (BadVariables m effects)
deriving instance MonadEvaluator location term value (m effects) => MonadEvaluator location term value (BadVariables m effects)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadVariables m)
instance ( Effectful m
, Member (Resumable (EvalError value)) effects
, Member (State [Name]) effects
, MonadAnalysis location term value (m effects)
, MonadValue location value (BadVariables m effects)
, MonadAnalysis location term value effects m
, MonadValue location value effects (BadVariables m)
)
=> MonadAnalysis location term value (BadVariables m effects) where
type Effects location term value (BadVariables m effects) = State [Name] ': Effects location term value (m effects)
=> 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

View File

@ -20,38 +20,34 @@ type CachingEffects location term value 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)
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadControl term (m effects) => MonadControl term (Caching m effects)
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (Caching m effects)
deriving instance MonadHeap location value (m effects) => MonadHeap location value (Caching m effects)
deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Caching m effects)
deriving instance MonadEvaluator location term value (m effects) => MonadEvaluator location term value (Caching m effects)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (Caching m)
-- | Functionality used to perform caching analysis. This is not exported, and exists primarily for organizational reasons.
class MonadEvaluator location term value m => MonadCaching location term value m where
class MonadEvaluator location term value effects m => MonadCaching location term value effects m where
-- | Look up the set of values for a given configuration in the in-cache.
consultOracle :: Configuration location term value -> m (Set (value, Heap location value))
consultOracle :: Configuration location term value -> m effects (Set (value, Heap location value))
-- | Run an action with the given in-cache.
withOracle :: Cache location term value -> m a -> m a
withOracle :: Cache location term value -> m effects a -> m effects a
-- | Look up the set of values for a given configuration in the out-cache.
lookupCache :: Configuration location term value -> m (Maybe (Set (value, Heap location value)))
lookupCache :: Configuration location term value -> m effects (Maybe (Set (value, Heap location value)))
-- | Run an action, caching its result and 'Heap' under the given configuration.
caching :: Configuration location term value -> Set (value, Heap location value) -> m value -> m value
caching :: Configuration location term value -> Set (value, Heap location value) -> m effects value -> m effects value
-- | Run an action starting from an empty out-cache, and return the out-cache afterwards.
isolateCache :: m a -> m (Cache location term value)
isolateCache :: m effects a -> m effects (Cache location term value)
instance ( Effectful m
, Members (CachingEffects location term value '[]) effects
, MonadEvaluator location term value (m effects)
, MonadEvaluator location term value effects m
, Ord (Cell location value)
, Ord location
, Ord term
, Ord value
)
=> MonadCaching location term value (Caching m effects) where
=> MonadCaching location term value effects (Caching m) where
consultOracle configuration = raise (fromMaybe mempty . cacheLookup configuration <$> ask)
withOracle cache = raise . local (const cache) . lower
@ -68,17 +64,17 @@ instance ( Effectful m
instance ( Alternative (m effects)
, Corecursive term
, Effectful m
, Member Fresh effects
, Members (CachingEffects location term value '[]) effects
, MonadAnalysis location term value (m effects)
, MonadFresh (m effects)
, MonadAnalysis location term value effects m
, Ord (Cell location value)
, Ord location
, Ord term
, Ord value
)
=> MonadAnalysis location term value (Caching m effects) where
=> 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 effects) = CachingEffects location term value (Effects location term value (m 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
@ -121,5 +117,5 @@ converge f = loop
loop x'
-- | Nondeterministically write each of a collection of stores & return their associated results.
scatter :: (Alternative m, Foldable t, MonadEvaluator location term value m) => t (a, Heap location value) -> m a
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)

View File

@ -11,32 +11,27 @@ import Data.Abstract.Live
import Prologue
newtype Collecting m (effects :: [* -> *]) a = Collecting (m effects a)
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
deriving instance MonadControl term (m effects) => MonadControl term (Collecting m effects)
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (Collecting m effects)
deriving instance MonadHeap location value (m effects) => MonadHeap location value (Collecting m effects)
deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Collecting m effects)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
instance ( Effectful m
, Member (Reader (Live location value)) effects
, MonadEvaluator location term value (m effects)
, MonadEvaluator location term value effects m
)
=> MonadEvaluator location term value (Collecting m effects) where
=> MonadEvaluator location term value effects (Collecting m) where
getConfiguration term = Configuration term <$> askRoots <*> getEnv <*> getHeap
instance ( Effectful m
, Foldable (Cell location)
, Member (Reader (Live location value)) effects
, MonadAnalysis location term value (m effects)
, MonadAnalysis location term value effects m
, Ord location
, ValueRoots location value
)
=> MonadAnalysis location term value (Collecting m effects) where
type Effects location term value (Collecting m effects)
=> MonadAnalysis location term value effects (Collecting m) where
type Effects location term value (Collecting m)
= Reader (Live location value)
': Effects location term value (m effects)
': Effects location term value m
-- Small-step evaluation which garbage-collects any non-rooted addresses after evaluating each term.
analyzeTerm recur term = do

View File

@ -11,13 +11,9 @@ import Prologue
-- | An analysis tracking dead (unreachable) code.
newtype DeadCode m (effects :: [* -> *]) a = DeadCode (m effects a)
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadControl term (m effects) => MonadControl term (DeadCode m effects)
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (DeadCode m effects)
deriving instance MonadHeap location value (m effects) => MonadHeap location value (DeadCode m effects)
deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (DeadCode m effects)
deriving instance MonadEvaluator location term value (m effects) => MonadEvaluator location term value (DeadCode m effects)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (DeadCode m)
-- | A set of “dead” (unreachable) terms.
newtype Dead term = Dead { unDead :: Set term }
@ -42,12 +38,12 @@ instance ( Corecursive term
, Effectful m
, Foldable (Base term)
, Member (State (Dead term)) effects
, MonadAnalysis location term value (m effects)
, MonadAnalysis location term value effects m
, Ord term
, Recursive term
)
=> MonadAnalysis location term value (DeadCode m effects) where
type Effects location term value (DeadCode m effects) = State (Dead term) ': Effects location term value (m effects)
=> 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)

View File

@ -1,33 +1,22 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, RankNTypes, TypeFamilies, UndecidableInstances, ScopedTypeVariables #-}
{-# LANGUAGE GeneralizedNewtypeDeriving, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
module Analysis.Abstract.Evaluating
( Evaluating
, EvaluatingState(..)
, State
) where
import Control.Abstract.Analysis
import Control.Monad.Effect
import Data.Abstract.Address
import Data.Abstract.Configuration
import Data.Abstract.Environment as Env
import Data.Abstract.Evaluatable
import Data.Abstract.Exports
import Data.Abstract.Heap
import Data.Abstract.Module
import Data.Abstract.ModuleTable
import Data.Abstract.Origin
import Data.Empty
import qualified Data.IntMap as IntMap
import Lens.Micro
import Prelude hiding (fail)
import Prologue
import Control.Abstract.Analysis
import Control.Monad.Effect
import Data.Abstract.Configuration
import Data.Abstract.Environment as Env
import Data.Abstract.Evaluatable
import Data.Abstract.Module
import Data.Abstract.ModuleTable
import Data.Abstract.Origin
import Prologue
-- | 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)
deriving (Applicative, Functor, Effectful, Monad)
deriving instance Member Fail effects => MonadFail (Evaluating location term value effects)
deriving instance Member Fresh effects => MonadFresh (Evaluating location term value effects)
deriving instance Member NonDet effects => Alternative (Evaluating location term value effects)
-- | Effects necessary for evaluating (whether concrete or abstract).
@ -40,133 +29,33 @@ type EvaluatingEffects location 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 terms origin.
, Reader (ModuleTable [Module term]) -- Cache of unevaluated modules
, Reader (Environment location value) -- Default environment used as a fallback in lookupEnv
, State (EvaluatingState location term value) -- Environment, heap, modules, exports, and jumps.
, Fail -- Failure with an error message
, Fresh -- For allocating new addresses and/or type variables.
, Reader (SomeOrigin term) -- The current terms origin.
, Reader (ModuleTable [Module term]) -- Cache of unevaluated modules
, Reader (Environment location value) -- Default environment used as a fallback in lookupEnv
, State (EvaluatorState location term value) -- Environment, heap, modules, exports, and jumps.
]
data EvaluatingState location term value = EvaluatingState
{ environment :: Environment location value
, heap :: Heap location value
, modules :: ModuleTable (Environment location value, value)
, loadStack :: LoadStack
, exports :: Exports location value
, jumps :: IntMap.IntMap term
, origin :: SomeOrigin term
}
deriving instance (Eq (Cell location value), Eq location, Eq term, Eq value, Eq (Base term ())) => Eq (EvaluatingState location term value)
deriving instance (Ord (Cell location value), Ord location, Ord term, Ord value, Ord (Base term ())) => Ord (EvaluatingState location term value)
deriving instance (Show (Cell location value), Show location, Show term, Show value, Show (Base term ())) => Show (EvaluatingState location term value)
instance (Ord location, Semigroup (Cell location value)) => Semigroup (EvaluatingState location term value) where
EvaluatingState e1 h1 m1 l1 x1 j1 o1 <> EvaluatingState e2 h2 m2 l2 x2 j2 o2 = EvaluatingState (e1 <> e2) (h1 <> h2) (m1 <> m2) (l1 <> l2) (x1 <> x2) (j1 <> j2) (o1 <> o2)
instance (Ord location, Semigroup (Cell location value)) => Empty (EvaluatingState location term value) where
empty = EvaluatingState mempty mempty mempty mempty mempty mempty mempty
_environment :: Lens' (EvaluatingState location term value) (Environment location value)
_environment = lens environment (\ s e -> s {environment = e})
_heap :: Lens' (EvaluatingState location term value) (Heap location value)
_heap = lens heap (\ s h -> s {heap = h})
_modules :: Lens' (EvaluatingState location term value) (ModuleTable (Environment location value, value))
_modules = lens modules (\ s m -> s {modules = m})
_loadStack :: Lens' (EvaluatingState location term value) LoadStack
_loadStack = lens loadStack (\ s l -> s {loadStack = l})
_exports :: Lens' (EvaluatingState location term value) (Exports location value)
_exports = lens exports (\ s e -> s {exports = e})
_jumps :: Lens' (EvaluatingState location term value) (IntMap.IntMap term)
_jumps = lens jumps (\ s j -> s {jumps = j})
_origin :: Lens' (EvaluatingState location term value) (SomeOrigin term)
_origin = lens origin (\ s o -> s {origin = o})
(.=) :: Member (State (EvaluatingState location term value)) effects => ASetter (EvaluatingState location term value) (EvaluatingState location term value) a b -> b -> Evaluating location term value effects ()
lens .= val = raise (modify' (lens .~ val))
view :: Member (State (EvaluatingState location term value)) effects => Getting a (EvaluatingState location term value) a -> Evaluating location term value effects a
view lens = raise (gets (^. lens))
localEvaluatingState :: Member (State (EvaluatingState location term value)) effects => Lens' (EvaluatingState location term value) prj -> (prj -> prj) -> Evaluating location term value effects a -> Evaluating location term value effects a
localEvaluatingState lens f action = do
original <- view lens
lens .= f original
v <- action
v <$ lens .= original
instance Members '[Fail, State (EvaluatingState location term value)] effects => MonadControl term (Evaluating location term value effects) where
label term = do
m <- view _jumps
let i = IntMap.size m
_jumps .= IntMap.insert i term m
pure i
goto label = IntMap.lookup label <$> view _jumps >>= maybe (fail ("unknown label: " <> show label)) pure
instance Members '[ State (EvaluatingState location term value)
, Reader (Environment location value)
] effects
=> MonadEnvironment location value (Evaluating location term value effects) where
getEnv = view _environment
putEnv = (_environment .=)
withEnv s = localEvaluatingState _environment (const s)
defaultEnvironment = raise ask
withDefaultEnvironment e = raise . local (const e) . lower
getExports = view _exports
putExports = (_exports .=)
withExports s = localEvaluatingState _exports (const s)
localEnv f a = do
modifyEnv (f . Env.push)
result <- a
result <$ modifyEnv Env.pop
instance Member (State (EvaluatingState location term value)) effects
=> MonadHeap location value (Evaluating location term value effects) where
getHeap = view _heap
putHeap = (_heap .=)
instance Members '[ Reader (ModuleTable [Module term])
, State (EvaluatingState location term value)
, Reader (SomeOrigin term)
, Fail
] effects
=> MonadModuleTable location term value (Evaluating location term value effects) where
getModuleTable = view _modules
putModuleTable = (_modules .=)
askModuleTable = raise ask
localModuleTable f a = raise (local f (lower a))
getLoadStack = view _loadStack
putLoadStack = (_loadStack .=)
currentModule = do
o <- raise ask
maybeFail "unable to get currentModule" $ withSomeOrigin (originModule @term) o
instance Members (EvaluatingEffects location term value) effects
=> MonadEvaluator location term value (Evaluating location term value effects) where
instance ( Member Fail effects
, Member (Reader (Environment location value)) effects
, Member (Reader (ModuleTable [Module term])) effects
, Member (Reader (SomeOrigin term)) effects
, Member (State (EvaluatorState location term value)) effects
)
=> MonadEvaluator location term value effects (Evaluating location term value) where
getConfiguration term = Configuration term mempty <$> getEnv <*> getHeap
instance ( Corecursive term
, Members (EvaluatingEffects location term value) effects
, Member Fail effects
, Member (Reader (Environment location value)) effects
, Member (Reader (ModuleTable [Module term])) effects
, Member (Reader (SomeOrigin term)) effects
, Member (State (EvaluatorState location term value)) effects
, Recursive term
)
=> MonadAnalysis location term value (Evaluating location term value effects) where
type Effects location term value (Evaluating location term value effects) = EvaluatingEffects location term value
=> 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)

View File

@ -9,7 +9,7 @@ module Analysis.Abstract.ImportGraph
import qualified Algebra.Graph as G
import Algebra.Graph.Class hiding (Vertex)
import Algebra.Graph.Export.Dot hiding (vertexName)
import Control.Abstract.Analysis
import Control.Abstract.Analysis hiding (origin)
import Data.Abstract.Address
import Data.Abstract.Evaluatable (LoadError (..))
import Data.Abstract.FreeVariables
@ -55,13 +55,9 @@ style = (defaultStyle vertexName)
edgeAttributes _ _ = []
newtype ImportGraphing m (effects :: [* -> *]) a = ImportGraphing (m effects a)
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadControl term (m effects) => MonadControl term (ImportGraphing m effects)
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (ImportGraphing m effects)
deriving instance MonadHeap location value (m effects) => MonadHeap location value (ImportGraphing m effects)
deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (ImportGraphing m effects)
deriving instance MonadEvaluator location term value (m effects) => MonadEvaluator location term value (ImportGraphing m effects)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (ImportGraphing m)
instance ( Effectful m
@ -69,12 +65,12 @@ instance ( Effectful m
, Member (Resumable (LoadError term value)) effects
, Member (State ImportGraph) effects
, Member Syntax.Identifier syntax
, MonadAnalysis (Located location term) term value (m effects)
, MonadAnalysis (Located location term) term value effects m
, term ~ Term (Union syntax) ann
, Show ann
)
=> MonadAnalysis (Located location term) term value (ImportGraphing m effects) where
type Effects (Located location term) term value (ImportGraphing m effects) = State ImportGraph ': Effects (Located location term) term value (m effects)
=> 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 ann syntax) = do
traceShowM ann
@ -102,10 +98,8 @@ moduleGraph = maybe empty (vertex . Module . BC.pack . modulePath) . withSomeOri
-- | Add an edge from the current package to the passed vertex.
packageInclusion :: forall m location term value effects
. ( Effectful m
, Member (Reader (SomeOrigin term)) effects
, Member (State ImportGraph) effects
, MonadEvaluator location term value (m effects)
. ( Member (State ImportGraph) effects
, MonadEvaluator location term value effects m
)
=> Vertex
-> ImportGraphing m effects ()
@ -115,10 +109,8 @@ packageInclusion v = do
-- | Add an edge from the current module to the passed vertex.
moduleInclusion :: forall m location term value effects
. ( Effectful m
, Member (Reader (SomeOrigin term)) effects
, Member (State ImportGraph) effects
, MonadEvaluator location term value (m effects)
. ( Member (State ImportGraph) effects
, MonadEvaluator location term value effects m
)
=> Vertex
-> ImportGraphing m effects ()
@ -127,10 +119,11 @@ moduleInclusion v = do
appendGraph (moduleGraph @term o `connect` vertex v)
-- | Add an edge from the passed variable name to the module it originated within.
variableDefinition :: ( Effectful m
, Member (State ImportGraph) effects
, MonadEvaluator (Located location term) term value (m effects)
) => Name -> ImportGraphing m effects ()
variableDefinition :: ( Member (State ImportGraph) effects
, MonadEvaluator (Located location term) term value effects m
)
=> Name
-> ImportGraphing m effects ()
variableDefinition name = do
graph <- maybe empty (moduleGraph . origin . unAddress) <$> lookupEnv name
appendGraph (vertex (Variable (unName name)) `connect` graph)

View File

@ -15,21 +15,17 @@ import Prologue
--
-- Note that exceptions thrown by other analyses may not be caught if 'Quietly' doesnt know about them, i.e. if theyre not part of the generic 'MonadValue', 'MonadAddressable', etc. machinery.
newtype Quietly m (effects :: [* -> *]) a = Quietly (m effects a)
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadControl term (m effects) => MonadControl term (Quietly m effects)
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (Quietly m effects)
deriving instance MonadHeap location value (m effects) => MonadHeap location value (Quietly m effects)
deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Quietly m effects)
deriving instance MonadEvaluator location term value (m effects) => MonadEvaluator location term value (Quietly m effects)
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 (m effects)
, MonadValue location value (Quietly m effects)
, MonadAnalysis location term value effects m
, MonadValue location value effects (Quietly m)
)
=> MonadAnalysis location term value (Quietly m effects) where
type Effects location term value (Quietly m effects) = Effects location term value (m effects)
=> 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)

View File

@ -14,23 +14,19 @@ import Prologue
--
-- 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)
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadControl term (m effects) => MonadControl term (Tracing trace m effects)
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (Tracing trace m effects)
deriving instance MonadHeap location value (m effects) => MonadHeap location value (Tracing trace m effects)
deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Tracing trace m effects)
deriving instance MonadEvaluator location term value (m effects) => MonadEvaluator location term value (Tracing trace m effects)
deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (Tracing trace m)
instance ( Corecursive term
, Effectful m
, Member (Writer (trace (Configuration location term value))) effects
, MonadAnalysis location term value (m effects)
, MonadAnalysis location term value effects m
, Ord location
, Reducer (Configuration location term value) (trace (Configuration location term value))
)
=> MonadAnalysis location term value (Tracing trace m effects) where
type Effects location term value (Tracing trace m effects) = Writer (trace (Configuration location term value)) ': Effects location term value (m effects)
=> 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)

View File

@ -1,39 +1,39 @@
{-# LANGUAGE TypeFamilies, UndecidableInstances, GADTs #-}
{-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances #-}
module Control.Abstract.Addressable where
import Control.Abstract.Evaluator
import Control.Applicative
import Control.Effect
import Control.Effect.Fresh
import Control.Monad.Effect.Resumable as Eff
import Data.Abstract.Address
import Data.Abstract.Environment (insert)
import Data.Abstract.FreeVariables
import Data.Semigroup.Reducer
import Prelude hiding (fail)
import Prologue
-- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Heap.
class (MonadFresh m, Ord location) => MonadAddressable location m where
derefCell :: Address location value -> Cell location value -> m value
class (Effectful m, Member Fresh effects, Monad (m effects), Ord location) => MonadAddressable location effects m where
derefCell :: Address location value -> Cell location value -> m effects (Maybe value)
allocLoc :: Name -> m location
allocLoc :: Name -> m effects location
-- | Look up or allocate an address for a 'Name'.
lookupOrAlloc :: ( MonadAddressable location m
, MonadEnvironment location value m
lookupOrAlloc :: ( MonadAddressable location effects m
, MonadEvaluator location term value effects m
)
=> Name
-> m (Address location value)
-> m effects (Address location value)
lookupOrAlloc name = lookupEnv name >>= maybe (alloc name) pure
letrec :: ( MonadAddressable location m
, MonadEnvironment location value m
, MonadHeap location value m
letrec :: ( MonadAddressable location effects m
, MonadEvaluator location term value effects m
, Reducer value (Cell location value)
)
=> Name
-> m value
-> m (value, Address location value)
-> m effects value
-> m effects (value, Address location value)
letrec name body = do
addr <- lookupOrAlloc name
v <- localEnv (insert name addr) body
@ -41,12 +41,12 @@ letrec name body = do
pure (v, addr)
-- Lookup/alloc a name passing the address to a body evaluated in a new local environment.
letrec' :: ( MonadAddressable location m
, MonadEnvironment location value m
letrec' :: ( MonadAddressable location effects m
, MonadEvaluator location term value effects m
)
=> Name
-> (Address location value -> m value)
-> m value
-> (Address location value -> m effects value)
-> m effects value
letrec' name body = do
addr <- lookupOrAlloc name
v <- localEnv id (body addr)
@ -55,27 +55,28 @@ letrec' name body = do
-- Instances
-- | 'Precise' locations are always 'alloc'ated a fresh 'Address', and 'deref'erence to the 'Latest' value written.
instance (MonadFail m, MonadFresh m) => MonadAddressable Precise m where
derefCell addr = maybeM (uninitializedAddress addr) . unLatest
instance (Effectful m, Member Fresh effects, Monad (m effects)) => MonadAddressable Precise effects m where
derefCell _ = pure . unLatest
allocLoc _ = Precise <$> fresh
-- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically.
instance (Alternative m, MonadFresh m) => MonadAddressable Monovariant m where
derefCell _ = foldMapA pure
instance (Alternative (m effects), Effectful m, Member Fresh effects, Monad (m effects)) => MonadAddressable Monovariant effects m where
derefCell _ cell | null cell = pure Nothing
| otherwise = Just <$> foldMapA pure cell
allocLoc = pure . Monovariant
-- | Dereference the given 'Address'in the heap, or fail if the address is uninitialized.
deref :: (MonadResume (AddressError location value) m, MonadAddressable location m, MonadHeap location value m) => Address location value -> m value
deref addr = lookupHeap addr >>= maybe (throwAddressError $ UninitializedAddress addr) (derefCell addr)
deref :: (Member (Resumable (AddressError location value)) effects, MonadAddressable location effects m, MonadEvaluator location term value effects m) => Address location value -> m effects value
deref addr = do
cell <- lookupHeap addr >>= maybeM (throwAddressError (UnallocatedAddress addr))
derefed <- derefCell addr cell
maybeM (throwAddressError (UninitializedAddress addr)) derefed
alloc :: MonadAddressable location m => Name -> m (Address location value)
alloc :: MonadAddressable location effects m => Name -> m effects (Address location value)
alloc = fmap Address . allocLoc
-- | Fail with a message denoting an uninitialized address (i.e. one which was 'alloc'ated, but never 'assign'ed a value before being 'deref'erenced).
uninitializedAddress :: (MonadFail m, Show location) => Address location value -> m a
uninitializedAddress addr = fail $ "uninitialized address: " <> show addr
data AddressError location value resume where
UnallocatedAddress :: Address location value -> AddressError location value (Cell location value)
UninitializedAddress :: Address location value -> AddressError location value value
deriving instance Eq location => Eq (AddressError location value resume)
@ -83,9 +84,10 @@ deriving instance Show location => Show (AddressError location value resume)
instance Show location => Show1 (AddressError location value) where
liftShowsPrec _ _ = showsPrec
instance Eq location => Eq1 (AddressError location value) where
liftEq _ (UninitializedAddress a) (UninitializedAddress b) = a == b
liftEq _ (UninitializedAddress a) (UninitializedAddress b) = a == b
liftEq _ (UnallocatedAddress a) (UnallocatedAddress b) = a == b
liftEq _ _ _ = False
throwAddressError :: (MonadResume (AddressError location value) m) => AddressError location value resume -> m resume
throwAddressError = throwResumable
throwAddressError :: (Effectful m, Member (Resumable (AddressError location value)) effects) => AddressError location value resume -> m effects resume
throwAddressError = raise . Eff.throwError

View File

@ -29,20 +29,20 @@ import Prologue
-- | A 'Monad' in which one can evaluate some specific term type to some specific value type.
--
-- This typeclass is left intentionally unconstrained to avoid circular dependencies between it and other typeclasses.
class MonadEvaluator location term value m => MonadAnalysis location term value m where
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 value)) -> m value)
-> (Base term (Subterm term (outer value)) -> m value)
analyzeTerm :: (Base term (Subterm term (outer effects value)) -> m effects value)
-> (Base term (Subterm term (outer effects value)) -> m effects value)
-- | Analyze a module using the semantics of the current analysis. This should generally only be called by 'evaluateModule' and by definitions of 'analyzeModule' in instances for composite analyses.
analyzeModule :: (Module (Subterm term (outer value)) -> m value)
-> (Module (Subterm term (outer value)) -> m value)
analyzeModule :: (Module (Subterm term (outer effects value)) -> m effects value)
-> (Module (Subterm term (outer effects value)) -> m effects value)
-- | Isolate the given action with an empty global environment and exports.
isolate :: m a -> m a
isolate :: m effects a -> m effects a
isolate = withEnv mempty . withExports mempty
@ -57,8 +57,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) ~ effects
, MonadAnalysis location term value (m effects)
, Effects location term value m ~ effects
, MonadAnalysis location term value effects m
, RunEffects effects a
)
=> m effects a
@ -69,8 +69,8 @@ runAnalysis = X.run
-- | An abstraction over analyses.
data SomeAnalysis m result where
SomeAnalysis :: ( Effectful m
, effects ~ Effects location term value (m effects)
, MonadAnalysis location term value (m effects)
, effects ~ Effects location term value m
, MonadAnalysis location term value effects m
, RunEffects effects a
)
=> m effects a

View File

@ -1,27 +1,57 @@
{-# LANGUAGE ConstrainedClassMethods, DataKinds, FunctionalDependencies, RankNTypes, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE ConstrainedClassMethods, FunctionalDependencies, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
module Control.Abstract.Evaluator
( MonadEvaluator(..)
, MonadEnvironment(..)
-- State
, EvaluatorState(..)
-- Environment
, getEnv
, putEnv
, modifyEnv
, withEnv
, defaultEnvironment
, withDefaultEnvironment
, fullEnvironment
, localEnv
, localize
, lookupEnv
, lookupWith
-- Exports
, getExports
, putExports
, modifyExports
, addExport
, fullEnvironment
, MonadHeap(..)
, withExports
-- Heap
, getHeap
, putHeap
, modifyHeap
, localize
, lookupHeap
, assign
, MonadModuleTable(..)
-- Module tables
, getModuleTable
, putModuleTable
, modifyModuleTable
, askModuleTable
, localModuleTable
, getLoadStack
, putLoadStack
, modifyLoadStack
, MonadControl(..)
, MonadResume(..)
, MonadExc(..)
, currentModule
-- Control
, label
, goto
-- Exceptions
, throwResumable
, throwException
, catchException
) where
import Control.Effect
import Control.Monad.Effect.Exception as Exception
import Control.Monad.Effect.Fail
import Control.Monad.Effect.Reader
import Control.Monad.Effect.Resumable as Resumable
import Control.Monad.Effect.State
import Data.Abstract.Address
import Data.Abstract.Configuration
import Data.Abstract.Environment as Env
@ -30,7 +60,12 @@ import Data.Abstract.FreeVariables
import Data.Abstract.Heap
import Data.Abstract.Module
import Data.Abstract.ModuleTable
import Data.Abstract.Origin
import Data.Empty
import qualified Data.IntMap as IntMap
import Data.Semigroup.Reducer
import Lens.Micro
import Prelude hiding (fail)
import Prologue
-- | A 'Monad' providing the basic essentials for evaluation.
@ -39,161 +74,265 @@ import Prologue
-- - environments binding names to addresses
-- - a heap mapping addresses to (possibly sets of) values
-- - tables of modules available for import
class ( MonadControl term m
, MonadEnvironment location value m
, MonadFail m
, MonadModuleTable location term value m
, MonadHeap location value m
class ( Effectful m
, Member Fail effects
, Member (Reader (Environment location value)) effects
, Member (Reader (ModuleTable [Module term])) effects
, Member (Reader (SomeOrigin term)) effects
, Member (State (EvaluatorState location term value)) effects
, Monad (m effects)
)
=> MonadEvaluator location term value m | m -> location, m -> term, m -> value where
=> MonadEvaluator location term value effects m | m effects -> location term value where
-- | Get the current 'Configuration' with a passed-in term.
getConfiguration :: Ord location => term -> m (Configuration location term value)
getConfiguration :: Ord location => term -> m effects (Configuration location term value)
-- | A 'Monad' abstracting local and global environments.
class Monad m => MonadEnvironment location value m | m -> value, m -> location where
-- | Retrieve the environment.
getEnv :: m (Environment location value)
-- | Set the environment.
putEnv :: Environment location value -> m ()
-- | Sets the environment for the lifetime of the given action.
withEnv :: Environment location value -> m a -> m a
-- | Retrieve the default environment.
defaultEnvironment :: m (Environment location value)
-- State
-- | Set the default environment for the lifetime of an action.
-- Usually only invoked in a top-level evaluation function.
withDefaultEnvironment :: Environment location value -> m a -> m a
data EvaluatorState location term value = EvaluatorState
{ environment :: Environment location value
, heap :: Heap location value
, modules :: ModuleTable (Environment location value, value)
, loadStack :: LoadStack
, exports :: Exports location value
, jumps :: IntMap.IntMap term
, origin :: SomeOrigin term
}
-- | Get the global export state.
getExports :: m (Exports location value)
-- | Set the global export state.
putExports :: Exports location value -> m ()
-- | Sets the global export state for the lifetime of the given action.
withExports :: Exports location value -> m a -> m a
deriving instance (Eq (Cell location value), Eq location, Eq term, Eq value, Eq (Base term ())) => Eq (EvaluatorState location term value)
deriving instance (Ord (Cell location value), Ord location, Ord term, Ord value, Ord (Base term ())) => Ord (EvaluatorState location term value)
deriving instance (Show (Cell location value), Show location, Show term, Show value, Show (Base term ())) => Show (EvaluatorState location term value)
-- | Run an action with a locally-modified environment.
localEnv :: (Environment location value -> Environment location value) -> m a -> m a
instance (Ord location, Semigroup (Cell location value)) => Semigroup (EvaluatorState location term value) where
EvaluatorState e1 h1 m1 l1 x1 j1 o1 <> EvaluatorState e2 h2 m2 l2 x2 j2 o2 = EvaluatorState (e1 <> e2) (h1 <> h2) (m1 <> m2) (l1 <> l2) (x1 <> x2) (j1 <> j2) (o1 <> o2)
-- | Look a 'Name' up in the current environment, trying the default environment if no value is found.
lookupEnv :: Name -> m (Maybe (Address location value))
lookupEnv name = (<|>) <$> (Env.lookup name <$> getEnv) <*> (Env.lookup name <$> defaultEnvironment)
instance (Ord location, Semigroup (Cell location value)) => Empty (EvaluatorState location term value) where
empty = EvaluatorState mempty mempty mempty mempty mempty mempty mempty
-- | Look up a 'Name' in the environment, running an action with the resolved address (if any).
lookupWith :: (Address location value -> m a) -> Name -> m (Maybe a)
lookupWith with name = do
addr <- lookupEnv name
maybe (pure Nothing) (fmap Just . with) addr
-- | Run a computation in a new local environment.
localize :: MonadEnvironment location value m => m a -> m a
localize = localEnv id
-- Lenses
_environment :: Lens' (EvaluatorState location term value) (Environment location value)
_environment = lens environment (\ s e -> s {environment = e})
_heap :: Lens' (EvaluatorState location term value) (Heap location value)
_heap = lens heap (\ s h -> s {heap = h})
_modules :: Lens' (EvaluatorState location term value) (ModuleTable (Environment location value, value))
_modules = lens modules (\ s m -> s {modules = m})
_loadStack :: Lens' (EvaluatorState location term value) LoadStack
_loadStack = lens loadStack (\ s l -> s {loadStack = l})
_exports :: Lens' (EvaluatorState location term value) (Exports location value)
_exports = lens exports (\ s e -> s {exports = e})
_jumps :: Lens' (EvaluatorState location term value) (IntMap.IntMap term)
_jumps = lens jumps (\ s j -> s {jumps = j})
_origin :: Lens' (EvaluatorState location term value) (SomeOrigin term)
_origin = lens origin (\ s o -> s {origin = o})
(.=) :: MonadEvaluator location term value effects m => ASetter (EvaluatorState location term value) (EvaluatorState location term value) a b -> b -> m effects ()
lens .= val = raise (modify' (lens .~ val))
view :: MonadEvaluator location term value effects m => Getting a (EvaluatorState location term value) a -> m effects a
view lens = raise (gets (^. lens))
localEvaluatorState :: MonadEvaluator location term value effects m => Lens' (EvaluatorState location term value) prj -> (prj -> prj) -> m effects a -> m effects a
localEvaluatorState lens f action = do
original <- view lens
lens .= f original
v <- action
v <$ lens .= original
-- Environment
-- | Retrieve the environment.
getEnv :: MonadEvaluator location term value effects m => m effects (Environment location value)
getEnv = view _environment
-- | Set the environment.
putEnv :: MonadEvaluator location term value effects m => Environment location value -> m effects ()
putEnv = (_environment .=)
-- | Update the global environment.
modifyEnv :: MonadEnvironment location value m => (Environment location value -> Environment location value) -> m ()
modifyEnv :: MonadEvaluator location term value effects m => (Environment location value -> Environment location value) -> m effects ()
modifyEnv f = do
env <- getEnv
putEnv $! f env
-- | Sets the environment for the lifetime of the given action.
withEnv :: MonadEvaluator location term value effects m => Environment location value -> m effects a -> m effects a
withEnv s = localEvaluatorState _environment (const s)
-- | Retrieve the default environment.
defaultEnvironment :: MonadEvaluator location term value effects m => m effects (Environment location value)
defaultEnvironment = raise ask
-- | Set the default environment for the lifetime of an action.
-- Usually only invoked in a top-level evaluation function.
withDefaultEnvironment :: MonadEvaluator location term value effects m => Environment location value -> m effects a -> m effects a
withDefaultEnvironment e = raise . local (const e) . lower
-- | Obtain an environment that is the composition of the current and default environments.
-- Useful for debugging.
fullEnvironment :: MonadEvaluator location term value effects m => m effects (Environment location value)
fullEnvironment = mappend <$> getEnv <*> defaultEnvironment
-- | Run an action with a locally-modified environment.
localEnv :: MonadEvaluator location term value effects m => (Environment location value -> Environment location value) -> m effects a -> m effects a
localEnv f a = do
modifyEnv (f . Env.push)
result <- a
result <$ modifyEnv Env.pop
-- | Run a computation in a new local environment.
localize :: MonadEvaluator location term value effects m => m effects a -> m effects a
localize = localEnv id
-- | Look a 'Name' up in the current environment, trying the default environment if no value is found.
lookupEnv :: MonadEvaluator location term value effects m => Name -> m effects (Maybe (Address location value))
lookupEnv name = (<|>) <$> (Env.lookup name <$> getEnv) <*> (Env.lookup name <$> defaultEnvironment)
-- | Look up a 'Name' in the environment, running an action with the resolved address (if any).
lookupWith :: MonadEvaluator location term value effects m => (Address location value -> m effects a) -> Name -> m effects (Maybe a)
lookupWith with name = do
addr <- lookupEnv name
maybe (pure Nothing) (fmap Just . with) addr
-- Exports
-- | Get the global export state.
getExports :: MonadEvaluator location term value effects m => m effects (Exports location value)
getExports = view _exports
-- | Set the global export state.
putExports :: MonadEvaluator location term value effects m => Exports location value -> m effects ()
putExports = (_exports .=)
-- | Update the global export state.
modifyExports :: MonadEnvironment location value m => (Exports location value -> Exports location value) -> m ()
modifyExports :: MonadEvaluator location term value effects m => (Exports location value -> Exports location value) -> m effects ()
modifyExports f = do
exports <- getExports
putExports $! f exports
-- | Add an export to the global export state.
addExport :: MonadEnvironment location value m => Name -> Name -> Maybe (Address location value) -> m ()
addExport :: MonadEvaluator location term value effects m => Name -> Name -> Maybe (Address location value) -> m effects ()
addExport name alias = modifyExports . Export.insert name alias
-- | Obtain an environment that is the composition of the current and default environments.
-- Useful for debugging.
fullEnvironment :: MonadEnvironment location value m => m (Environment location value)
fullEnvironment = mappend <$> getEnv <*> defaultEnvironment
-- | Sets the global export state for the lifetime of the given action.
withExports :: MonadEvaluator location term value effects m => Exports location value -> m effects a -> m effects a
withExports s = localEvaluatorState _exports (const s)
-- | A 'Monad' abstracting a heap of values.
class Monad m => MonadHeap location value m | m -> value, m -> location where
-- | Retrieve the heap.
getHeap :: m (Heap location value)
-- | Set the heap.
putHeap :: Heap location value -> m ()
-- Heap
-- | Retrieve the heap.
getHeap :: MonadEvaluator location term value effects m => m effects (Heap location value)
getHeap = view _heap
-- | Set the heap.
putHeap :: MonadEvaluator location term value effects m => Heap location value -> m effects ()
putHeap = (_heap .=)
-- | Update the heap.
modifyHeap :: MonadHeap location value m => (Heap location value -> Heap location value) -> m ()
modifyHeap :: MonadEvaluator location term value effects m => (Heap location value -> Heap location value) -> m effects ()
modifyHeap f = do
s <- getHeap
putHeap $! f s
-- | Look up the cell for the given 'Address' in the 'Heap'.
lookupHeap :: (MonadHeap location value m, Ord location) => Address location value -> m (Maybe (Cell location value))
lookupHeap :: (MonadEvaluator location term value effects m, Ord location) => Address location value -> m effects (Maybe (Cell location value))
lookupHeap = flip fmap getHeap . heapLookup
-- | Write a value to the given 'Address' in the 'Store'.
assign :: ( Ord location
, MonadHeap location value m
, MonadEvaluator location term value effects m
, Reducer value (Cell location value)
)
=> Address location value
-> value
-> m ()
-> m effects ()
assign address = modifyHeap . heapInsert address
-- | A 'Monad' abstracting tables of modules available for import.
class Monad m => MonadModuleTable location term value m | m -> location, m -> term, m -> value where
-- | Retrieve the table of evaluated modules.
getModuleTable :: m (ModuleTable (Environment location value, value))
-- | Set the table of evaluated modules.
putModuleTable :: ModuleTable (Environment location value, value) -> m ()
-- Module table
-- | Retrieve the table of unevaluated modules.
askModuleTable :: m (ModuleTable [Module term])
-- | Run an action with a locally-modified table of unevaluated modules.
localModuleTable :: (ModuleTable [Module term] -> ModuleTable [Module term]) -> m a -> m a
-- | Retrieve the table of evaluated modules.
getModuleTable :: MonadEvaluator location term value effects m => m effects (ModuleTable (Environment location value, value))
getModuleTable = view _modules
-- | Retrieve the module load stack
getLoadStack :: m LoadStack
-- | Set the module load stack
putLoadStack :: LoadStack -> m ()
-- | Get the currently evaluating 'ModuleInfo'.
currentModule :: m ModuleInfo
-- | Set the table of evaluated modules.
putModuleTable :: MonadEvaluator location term value effects m => ModuleTable (Environment location value, value) -> m effects ()
putModuleTable = (_modules .=)
-- | Update the evaluated module table.
modifyModuleTable :: MonadModuleTable location term value m => (ModuleTable (Environment location value, value) -> ModuleTable (Environment location value, value)) -> m ()
modifyModuleTable :: MonadEvaluator location term value effects m => (ModuleTable (Environment location value, value) -> ModuleTable (Environment location value, value)) -> m effects ()
modifyModuleTable f = do
table <- getModuleTable
putModuleTable $! f table
-- | Retrieve the table of unevaluated modules.
askModuleTable :: MonadEvaluator location term value effects m => m effects (ModuleTable [Module term])
askModuleTable = raise ask
-- | Run an action with a locally-modified table of unevaluated modules.
localModuleTable :: MonadEvaluator location term value effects m => (ModuleTable [Module term] -> ModuleTable [Module term]) -> m effects a -> m effects a
localModuleTable f a = raise (local f (lower a))
-- | Retrieve the module load stack
getLoadStack :: MonadEvaluator location term value effects m => m effects LoadStack
getLoadStack = view _loadStack
-- | Set the module load stack
putLoadStack :: MonadEvaluator location term value effects m => LoadStack -> m effects ()
putLoadStack = (_loadStack .=)
-- | Update the module load stack.
modifyLoadStack :: MonadModuleTable location term value m => (LoadStack -> LoadStack) -> m ()
modifyLoadStack :: MonadEvaluator location term value effects m => (LoadStack -> LoadStack) -> m effects ()
modifyLoadStack f = do
stack <- getLoadStack
putLoadStack $! f stack
-- | A 'Monad' abstracting jumps in imperative control.
class Monad m => MonadControl term m where
-- | Allocate a 'Label' for the given @term@.
--
-- Labels must be allocated before being jumped to with 'goto', but are suitable for nonlocal jumps; thus, they can be used to implement coroutines, exception handling, call with current continuation, and other esoteric control mechanisms.
label :: term -> m Label
-- | “Jump” to a previously-allocated 'Label' (retrieving the @term@ at which it points, which can then be evaluated in e.g. a 'MonadAnalysis' instance).
goto :: Label -> m term
-- | Get the currently evaluating 'ModuleInfo'.
currentModule :: forall location term value effects m . MonadEvaluator location term value effects m => m effects ModuleInfo
currentModule = do
o <- raise ask
maybeM (raise (fail "unable to get currentModule")) $ withSomeOrigin (originModule @term) o
-- | 'Monad's which can throw exceptions of type @exc v@ which can be resumed with a value of type @v@.
class Monad m => MonadResume exc m where
throwResumable :: exc v -> m v
catchResumable :: m v -> (forall v1. exc v1 -> m v) -> m v
-- Control
instance (Effectful m1, Member (Resumable exc) effects, Monad (m1 effects)) => MonadResume exc (m1 effects) where
throwResumable = raise . Resumable.throwError
catchResumable c f = raise (Resumable.catchError (lower c) (lower . f))
-- | Allocate a 'Label' for the given @term@.
--
-- Labels must be allocated before being jumped to with 'goto', but are suitable for nonlocal jumps; thus, they can be used to implement coroutines, exception handling, call with current continuation, and other esoteric control mechanisms.
label :: MonadEvaluator location term value effects m => term -> m effects Label
label term = do
m <- view _jumps
let i = IntMap.size m
_jumps .= IntMap.insert i term m
pure i
class Monad m => MonadExc exc m where
throwException :: exc -> m v
catchException :: m v -> (exc -> m v) -> m v
-- | “Jump” to a previously-allocated 'Label' (retrieving the @term@ at which it points, which can then be evaluated in e.g. a 'MonadAnalysis' instance).
goto :: MonadEvaluator location term value effects m => Label -> m effects term
goto label = IntMap.lookup label <$> view _jumps >>= maybe (raise (fail ("unknown label: " <> show label))) pure
instance (Effectful m1, Member (Exc exc) effects, Monad (m1 effects)) => MonadExc exc (m1 effects) where
throwException = raise . Exception.throwError
catchException c f = raise (Exception.catchError (lower c) (lower . f))
-- Exceptions
throwResumable :: (Member (Resumable exc) effects, Effectful m) => exc v -> m effects v
throwResumable = raise . Resumable.throwError
throwException :: (Member (Exc exc) effects, Effectful m) => exc -> m effects a
throwException = raise . Exception.throwError
catchException :: (Member (Exc exc) effects, Effectful m) => m effects v -> (exc -> m effects v) -> m effects v
catchException action handler = raise (lower action `Exception.catchError` (lower . handler))

View File

@ -1,4 +1,4 @@
{-# LANGUAGE FunctionalDependencies, GADTs, Rank2Types, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, Rank2Types #-}
module Control.Abstract.Value
( MonadValue(..)
, Comparator(..)
@ -34,151 +34,150 @@ data Comparator
-- | 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.
class (Monad m, Show value) => MonadValue location value m | m value -> location where
class (Monad (m effects), Show value) => MonadValue location value (effects :: [* -> *]) m | m effects value -> location where
-- | Construct an abstract unit value.
-- TODO: This might be the same as the empty tuple for some value types
unit :: m value
unit :: m effects value
-- | Construct an abstract hole.
hole :: m value
hole :: m effects value
-- | Construct an abstract integral value.
integer :: Prelude.Integer -> m value
integer :: Prelude.Integer -> m effects value
-- | Lift a unary operator over a 'Num' to a function on 'value's.
liftNumeric :: (forall a . Num a => a -> a)
-> (value -> m value)
-> (value -> m effects value)
-- | Lift a pair of binary operators to a function on 'value's.
-- You usually pass the same operator as both arguments, except in the cases where
-- Haskell provides different functions for integral and fractional operations, such
-- as division, exponentiation, and modulus.
liftNumeric2 :: (forall a b. Number a -> Number b -> SomeNumber)
-> (value -> value -> m value)
-> (value -> value -> m effects value)
-- | Lift a Comparator (usually wrapping a function like == or <=) to a function on values.
liftComparison :: Comparator -> (value -> value -> m value)
liftComparison :: Comparator -> (value -> value -> m effects value)
-- | Lift a unary bitwise operator to values. This is usually 'complement'.
liftBitwise :: (forall a . Bits a => a -> a)
-> (value -> m value)
-> (value -> m effects value)
-- | Lift a binary bitwise operator to values. The Integral constraint is
-- necessary to satisfy implementation details of Haskell left/right shift,
-- but it's fine, since these are only ever operating on integral values.
liftBitwise2 :: (forall a . (Integral a, Bits a) => a -> a -> a)
-> (value -> value -> m value)
-> (value -> value -> m effects value)
-- | Construct an abstract boolean value.
boolean :: Bool -> m value
boolean :: Bool -> m effects value
-- | Construct an abstract string value.
string :: ByteString -> m value
string :: ByteString -> m effects value
-- | Construct a self-evaluating symbol value.
-- TODO: Should these be interned in some table to provide stronger uniqueness guarantees?
symbol :: ByteString -> m value
symbol :: ByteString -> m effects value
-- | Construct a floating-point value.
float :: Scientific -> m value
float :: Scientific -> m effects value
-- | Construct a rational value.
rational :: Prelude.Rational -> m value
rational :: Prelude.Rational -> m effects value
-- | Construct an N-ary tuple of multiple (possibly-disjoint) values
multiple :: [value] -> m value
multiple :: [value] -> m effects value
-- | Construct an array of zero or more values.
array :: [value] -> m value
array :: [value] -> m effects value
-- | Construct a key-value pair for use in a hash.
kvPair :: value -> value -> m value
kvPair :: value -> value -> m effects value
-- | Extract the contents of a key-value pair as a tuple.
asPair :: value -> m (value, value)
asPair :: value -> m effects (value, value)
-- | Construct a hash out of pairs.
hash :: [(value, value)] -> m value
hash :: [(value, value)] -> m effects value
-- | Extract a 'ByteString' from a given value.
asString :: value -> m ByteString
asString :: value -> m effects ByteString
-- | Eliminate boolean values. TODO: s/boolean/truthy
ifthenelse :: value -> m value -> m value -> m value
ifthenelse :: value -> m effects value -> m effects value -> m effects value
-- | Extract a 'Bool' from a given value.
asBool :: value -> m Bool
asBool :: value -> m effects Bool
-- | Construct the nil/null datatype.
null :: m value
null :: m effects value
isHole :: value -> m Bool
isHole :: value -> m effects Bool
-- | Build a class value from a name and environment.
klass :: Name -- ^ The new class's identifier
-> [value] -- ^ A list of superclasses
-> Environment location value -- ^ The environment to capture
-> m value
-> m effects value
-- | Build a namespace value from a name and environment stack
--
-- Namespaces model closures with monoidal environments.
namespace :: Name -- ^ The namespace's identifier
-> Environment location value -- ^ The environment to mappend
-> m value
-> m effects value
-- | Extract the environment from any scoped object (e.g. classes, namespaces, etc).
scopedEnvironment :: value -> m (Environment location value)
scopedEnvironment :: value -> m effects (Environment location value)
-- | Evaluate an abstraction (a binder like a lambda or method definition).
lambda :: (FreeVariables term, MonadControl term m) => [Name] -> Subterm term (m value) -> m value
lambda :: (FreeVariables term, MonadEvaluator location term value effects m) => [Name] -> Subterm term (m effects value) -> m effects value
-- | Evaluate an application (like a function call).
call :: value -> [m value] -> m value
call :: value -> [m effects value] -> m effects value
-- | 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 :: (m value -> m value) -> m value
loop :: (m effects value -> m effects value) -> m effects value
-- | Attempt to extract a 'Prelude.Bool' from a given value.
forLoop :: (MonadEnvironment location value m, MonadValue location value m)
=> m value -- ^ Initial statement
-> m value -- ^ Condition
-> m value -- ^ Increment/stepper
-> m value -- ^ Body
-> m value
forLoop :: (MonadEvaluator location term value effects m, MonadValue location value effects m)
=> m effects value -- ^ Initial statement
-> m effects value -- ^ Condition
-> m effects value -- ^ Increment/stepper
-> m effects value -- ^ Body
-> m effects value
forLoop initial cond step body =
localize (initial *> while cond (body *> step))
-- | The fundamental looping primitive, built on top of ifthenelse.
while :: MonadValue location value m
=> m value
-> m value
-> m value
while :: MonadValue location value effects m
=> m effects value
-> m effects value
-> m effects value
while cond body = loop $ \ continue -> do
this <- cond
ifthenelse this (body *> continue) unit
-- | Do-while loop, built on top of while.
doWhile :: MonadValue location value m
=> m value
-> m value
-> m value
doWhile :: MonadValue location value effects m
=> m effects value
-> m effects value
-> m effects value
doWhile body cond = loop $ \ continue -> body *> do
this <- cond
ifthenelse this continue unit
makeNamespace :: ( MonadValue location value m
, MonadEnvironment location value m
, MonadHeap location value m
makeNamespace :: ( MonadValue location value effects m
, MonadEvaluator location term value effects m
, Ord location
, Reducer value (Cell location value)
)
=> Name
-> Address location value
-> [value]
-> m value
-> m effects value
makeNamespace name addr supers = do
superEnv <- mconcat <$> traverse scopedEnvironment supers
namespaceEnv <- Env.head <$> getEnv

View File

@ -11,17 +11,13 @@ data Fresh a where
-- | Request a fresh variable name.
Fresh :: Fresh Int
-- | 'Monad's offering a (resettable) sequence of guaranteed-fresh type variables.
class Monad m => MonadFresh m where
-- | Get a fresh variable name, guaranteed unused (since the last 'reset').
fresh :: m 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 :: Int -> m ()
instance (Fresh :< fs) => MonadFresh (Eff fs) where
fresh = send Fresh
reset = send . Reset
-- | 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.

View File

@ -28,6 +28,7 @@ module Data.Abstract.Evaluatable
import Control.Abstract.Addressable as X
import Control.Abstract.Analysis as X
import qualified Control.Monad.Effect.Exception as Exc
import Data.Abstract.Address
import Data.Abstract.Declarations as X
import Data.Abstract.Environment as X
@ -44,21 +45,23 @@ import Data.Semigroup.Reducer hiding (unit)
import Data.Term
import Prologue
type MonadEvaluatable location term value m =
( Evaluatable (Base term)
type MonadEvaluatable location term value effects m =
( Declarations term
, Effectful m
, Evaluatable (Base term)
, FreeVariables term
, Declarations term
, MonadAddressable location m
, MonadAnalysis location term value m
, MonadResume (Unspecialized value) m
, MonadResume (ValueError location value) m
, MonadResume (LoadError term value) m
, MonadResume (EvalError value) m
, MonadResume (ResolutionError value) m
, MonadResume (AddressError location value) m
, MonadExc (ReturnThrow value) m
, MonadExc (LoopThrow value) m
, MonadValue location value m
, Member (Exc.Exc (ReturnThrow value)) effects
, 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
, Member (Resumable (AddressError location value)) effects
, MonadAddressable location effects m
, MonadAnalysis location term value effects m
, MonadValue location value effects m
, Recursive term
, Reducer value (Cell location value)
, Show location
@ -112,7 +115,7 @@ data EvalError value resume where
-- | Look up and dereference the given 'Name', throwing an exception for free variables.
variable :: MonadEvaluatable location term value m => Name -> m value
variable :: MonadEvaluatable location term value effects m => Name -> m effects value
variable name = lookupWith deref name >>= maybeM (throwResumable (FreeVariableError name))
deriving instance Eq (EvalError a b)
@ -130,16 +133,16 @@ instance Eq1 (EvalError term) where
liftEq _ _ _ = False
throwValueError :: MonadEvaluatable location term value m => ValueError location value resume -> m resume
throwValueError :: MonadEvaluatable location term value effects m => ValueError location value resume -> m effects resume
throwValueError = throwResumable
throwLoadError :: MonadEvaluatable location term value m => LoadError term value resume -> m resume
throwLoadError :: MonadEvaluatable location term value effects m => LoadError term value resume -> m effects resume
throwLoadError = throwResumable
throwEvalError :: MonadEvaluatable location term value m => EvalError value resume -> m resume
throwEvalError :: MonadEvaluatable location term value effects m => EvalError value resume -> m effects resume
throwEvalError = throwResumable
throwLoop :: MonadEvaluatable location term value m => LoopThrow value -> m a
throwLoop :: MonadEvaluatable location term value effects m => LoopThrow value -> m effects a
throwLoop = throwException
data Unspecialized a b where
@ -155,9 +158,9 @@ instance Show1 (Unspecialized a) where
-- | The 'Evaluatable' class defines the necessary interface for a term to be evaluated. While a default definition of 'eval' is given, instances with computational content must implement 'eval' to perform their small-step operational semantics.
class Evaluatable constr where
eval :: MonadEvaluatable location term value m
=> SubtermAlgebra constr term (m value)
default eval :: (MonadResume (Unspecialized value) m, Show1 constr) => SubtermAlgebra constr term (m value)
eval :: MonadEvaluatable location term value effects m
=> SubtermAlgebra constr term (m effects value)
default eval :: (MonadEvaluatable location term value effects m, Show1 constr) => SubtermAlgebra constr term (m effects value)
eval expr = throwResumable (Unspecialized ("Eval unspecialized for " ++ liftShowsPrec (const (const id)) (const id) 0 expr ""))
@ -181,9 +184,9 @@ instance Evaluatable [] where
eval = maybe unit (runApp . foldMap1 (App . subtermValue)) . nonEmpty
-- Resolve a list of module paths to a possible module table entry.
resolve :: MonadEvaluatable location term value m
resolve :: MonadEvaluatable location term value effects m
=> [FilePath]
-> m (Maybe ModulePath)
-> m effects (Maybe ModulePath)
resolve names = do
tbl <- askModuleTable
pure $ find (`ModuleTable.member` tbl) names
@ -191,25 +194,25 @@ resolve names = do
traceResolve :: (Show a, Show b) => a -> b -> c -> c
traceResolve name path = trace ("resolved " <> show name <> " -> " <> show path)
listModulesInDir :: MonadEvaluatable location term value m
listModulesInDir :: MonadEvaluatable location term value effects m
=> FilePath
-> m [ModulePath]
-> m effects [ModulePath]
listModulesInDir dir = ModuleTable.modulePathsInDir dir <$> askModuleTable
-- | Require/import another module by name and return it's environment and value.
--
-- Looks up the term's name in the cache of evaluated modules first, returns if found, otherwise loads/evaluates the module.
require :: MonadEvaluatable location term value m
require :: MonadEvaluatable location term value effects m
=> ModulePath
-> m (Environment location value, value)
-> m effects (Environment location value, value)
require name = getModuleTable >>= maybeM (load name) . ModuleTable.lookup name
-- | Load another module by name and return it's environment and value.
--
-- Always loads/evaluates.
load :: MonadEvaluatable location term value m
load :: MonadEvaluatable location term value effects m
=> ModulePath
-> m (Environment location value, value)
-> m effects (Environment location value, value)
load name = askModuleTable >>= maybeM notFound . ModuleTable.lookup name >>= evalAndCache
where
notFound = throwLoadError (LoadError name)
@ -249,30 +252,27 @@ load name = askModuleTable >>= maybeM notFound . ModuleTable.lookup name >>= eva
-- | Evaluate a term to a value using the semantics of the current analysis.
--
-- This should always be called when e.g. evaluating the bodies of closures instead of explicitly folding either 'eval' or 'analyzeTerm' over subterms, except in 'MonadAnalysis' instances themselves. On the other hand, top-level evaluation should be performed using 'evaluateModule'.
evaluateTerm :: MonadEvaluatable location term value m
evaluateTerm :: MonadEvaluatable location term value effects m
=> term
-> m value
-> m effects value
evaluateTerm = foldSubterms (analyzeTerm eval)
-- | Evaluate a (root-level) term to a value using the semantics of the current analysis. This should be used to evaluate single-term programs, or (via 'evaluateModules') the entry point of multi-term programs.
evaluateModule :: MonadEvaluatable location term value m
evaluateModule :: MonadEvaluatable location term value effects m
=> Module term
-> m value
-> m effects value
evaluateModule m = analyzeModule (subtermValue . moduleBody) (fmap (Subterm <*> evaluateTerm) m)
-- | Evaluate a given package.
evaluatePackage :: ( Effectful m
, Member (Reader (SomeOrigin term)) effects
, MonadEvaluatable location term value (m effects)
)
evaluatePackage :: MonadEvaluatable location term value effects m
=> Package term
-> m effects [value]
evaluatePackage p = pushOrigin (packageOrigin p) (evaluatePackageBody (packageBody p))
-- | Evaluate a given package body (module table and entry points).
evaluatePackageBody :: MonadEvaluatable location term value m
evaluatePackageBody :: MonadEvaluatable location term value effects m
=> PackageBody term
-> m [value]
-> m effects [value]
evaluatePackageBody body = withPrelude (packagePrelude body) $
localModuleTable (<> packageModules body) (traverse evaluateEntryPoint (ModuleTable.toPairs (packageEntryPoints body)))
where

View File

@ -19,10 +19,10 @@ instance (Location location, Ord (Base term ())) => Location (Located location t
instance ( Effectful m
, Member (Reader (SomeOrigin term)) effects
, MonadAddressable location (m effects)
, MonadAddressable location effects m
, Ord (Base term ())
)
=> MonadAddressable (Located location term) (m effects) where
=> MonadAddressable (Located location term) effects m where
derefCell (Address (Located loc _)) = derefCell (Address loc)
allocLoc name = Located <$> allocLoc name <*> raise ask

View File

@ -1,4 +1,5 @@
{-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the MonadValue instance, which requires MonadEvaluator to resolve its functional dependency.
module Data.Abstract.Type
( Type (..)
, TypeError (..)
@ -58,7 +59,7 @@ instance Eq1 TypeError where
liftEq _ _ _ = False
-- | Unify two 'Type's.
unify :: MonadResume TypeError m => Type -> Type -> m Type
unify :: (Effectful m, Applicative (m effects), Member (Resumable TypeError) effects) => Type -> Type -> m effects Type
unify (a1 :-> b1) (a2 :-> b2) = (:->) <$> unify a1 a2 <*> unify b1 b2
unify a Null = pure a
unify Null b = pure b
@ -70,22 +71,18 @@ unify t1 t2
| t1 == t2 = pure t2
| otherwise = throwResumable (UnificationError t1 t2)
instance Ord location => ValueRoots location Type where
valueRoots _ = mempty
-- | Discard the value arguments (if any), constructing a 'Type' instead.
instance ( Alternative m
, MonadAddressable location m
, MonadEnvironment location Type m
, MonadFail m
, MonadFresh m
, MonadHeap location Type m
, MonadResume TypeError m
instance ( Alternative (m effects)
, Member Fresh effects
, Member (Resumable TypeError) effects
, MonadAddressable location effects m
, MonadEvaluator location term Type effects m
, Reducer Type (Cell location Type)
)
=> MonadValue location Type m where
=> MonadValue location Type effects m where
lambda names (Subterm _ body) = do
(env, tvars) <- foldr (\ name rest -> do
a <- alloc name
@ -151,7 +148,9 @@ instance ( Alternative m
call op params = do
tvar <- fresh
paramTypes <- sequenceA params
_ :-> ret <- op `unify` (Product paramTypes :-> Var tvar)
pure ret
unified <- op `unify` (Product paramTypes :-> Var tvar)
case unified of
_ :-> ret -> pure ret
_ -> raise (fail "unification with a function produced something other than a function")
loop f = f empty

View File

@ -1,4 +1,4 @@
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances, ScopedTypeVariables #-}
{-# LANGUAGE ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}
module Data.Abstract.Value where
import Control.Abstract.Analysis
@ -198,7 +198,7 @@ instance Ord location => ValueRoots location (Value location) where
-- | Construct a 'Value' wrapping the value arguments (if any).
instance forall location term m. (Monad m, MonadEvaluatable location term (Value location) m) => MonadValue location (Value location) m where
instance (Monad (m effects), MonadEvaluatable location term (Value location) effects m) => MonadValue location (Value location) effects m where
hole = pure . injValue $ Hole
unit = pure . injValue $ Unit
integer = pure . injValue . Integer . Number.Integer
@ -277,7 +277,7 @@ instance forall location term m. (Monad m, MonadEvaluatable location term (Value
| otherwise = throwValueError (Numeric2Error left right)
where
-- Dispatch whatever's contained inside a 'Number.SomeNumber' to its appropriate 'MonadValue' ctor
specialize :: MonadValue location value m => Number.SomeNumber -> m value
specialize :: MonadValue location value effects m => Number.SomeNumber -> m effects value
specialize (Number.SomeNumber (Number.Integer i)) = integer i
specialize (Number.SomeNumber (Number.Ratio r)) = rational r
specialize (Number.SomeNumber (Number.Decimal d)) = float d
@ -295,7 +295,7 @@ instance forall location term m. (Monad m, MonadEvaluatable location term (Value
where
-- Explicit type signature is necessary here because we're passing all sorts of things
-- to these comparison functions.
go :: (Ord a, MonadValue location value m) => a -> a -> m value
go :: (Ord a, MonadValue location value effects m) => a -> a -> m effects value
go l r = case comparator of
Concrete f -> boolean (f l r)
Generalized -> integer (orderingToInt (compare l r))
@ -331,13 +331,13 @@ instance forall location term m. (Monad m, MonadEvaluatable location term (Value
localEnv (mappend bindings) (evalClosure label)
Nothing -> throwValueError (CallError op)
where
evalClosure :: Label -> m (Value location)
evalClosure :: Label -> m effects (Value location)
evalClosure lab = catchException (goto lab >>= evaluateTerm) handleReturn
handleReturn :: ReturnThrow (Value location) -> m (Value location)
handleReturn :: ReturnThrow (Value location) -> m effects (Value location)
handleReturn (Ret v) = pure v
loop x = catchException (fix x) handleLoop where
handleLoop :: LoopThrow (Value location) -> m (Value location)
handleLoop :: LoopThrow (Value location) -> m effects (Value location)
handleLoop (Brk v) = pure v
handleLoop Con = loop x

View File

@ -3,16 +3,15 @@ module Data.Scientific.Exts
, parseScientific
) where
import Prelude hiding (filter, null, takeWhile)
import Control.Applicative
import Control.Monad
import Control.Monad hiding (fail)
import Data.Attoparsec.ByteString.Char8
import Data.ByteString.Char8 hiding (readInt, takeWhile)
import Data.Char (isOctDigit)
import Data.Scientific
import Data.Semigroup
import Numeric
import Prelude hiding (fail, filter, null, takeWhile)
import Prologue hiding (null)
import Text.Read (readMaybe)
parseScientific :: ByteString -> Either String Scientific
@ -38,9 +37,9 @@ parser = signed (choice [hex, oct, bin, dec]) where
-- The ending stanza. Note the explicit endOfInput call to ensure we haven't left any dangling input.
done = skipWhile (inClass "iIjJlL") *> endOfInput
-- Wrapper around readMaybe. Analogous to maybeFail in the Prologue, but no need to pull that in.
-- Wrapper around readMaybe.
attempt :: Read a => String -> Parser a
attempt str = maybe (fail ("No parse: " <> str)) pure (readMaybe str)
attempt str = maybeM (fail ("No parse: " <> str)) (readMaybe str)
-- Parse a hex value, leaning on the parser provided by Attoparsec.
hex = fromIntegral <$> (string "0x" *> hexadecimal @Integer)

View File

@ -22,7 +22,7 @@ defaultAlias :: ImportPath -> Name
defaultAlias = name . BC.pack . takeFileName . unPath
-- TODO: need to delineate between relative and absolute Go imports
resolveGoImport :: MonadEvaluatable location term value m => FilePath -> m [ModulePath]
resolveGoImport :: MonadEvaluatable location term value effects m => FilePath -> m effects [ModulePath]
resolveGoImport relImportPath = do
ModuleInfo{..} <- currentModule
let relRootDir = takeDirectory modulePath

View File

@ -34,13 +34,13 @@ instance Evaluatable VariableName
-- file, the complete contents of the included file are treated as though it
-- were defined inside that function.
resolvePHPName :: MonadEvaluatable location term value m => ByteString -> m ModulePath
resolvePHPName n = resolve [name] >>= maybeFail notFound
resolvePHPName :: MonadEvaluatable location term value effects m => ByteString -> m effects ModulePath
resolvePHPName n = resolve [name] >>= maybeM (raise (fail notFound))
where name = toName n
notFound = "Unable to resolve: " <> name
toName = BC.unpack . dropRelativePrefix . stripQuotes
doInclude :: MonadEvaluatable location term value m => Subterm t (m value) -> m value
doInclude :: MonadEvaluatable location term value effects m => Subterm t (m effects value) -> m effects value
doInclude pathTerm = do
name <- subtermValue pathTerm >>= asString
path <- resolvePHPName name
@ -48,7 +48,7 @@ doInclude pathTerm = do
modifyEnv (mappend importedEnv)
pure v
doIncludeOnce :: MonadEvaluatable location term value m => Subterm t (m value) -> m value
doIncludeOnce :: MonadEvaluatable location term value effects m => Subterm t (m effects value) -> m effects value
doIncludeOnce pathTerm = do
name <- subtermValue pathTerm >>= asString
path <- resolvePHPName name
@ -366,7 +366,7 @@ instance Evaluatable Namespace where
eval Namespace{..} = go names
where
names = freeVariables (subterm namespaceName)
go [] = fail "expected at least one free variable in namespaceName, found none"
go [] = raise (fail "expected at least one free variable in namespaceName, found none")
-- The last name creates a closure over the namespace body.
go [name] = letrec' name $ \addr ->
subtermValue namespaceBody *> makeNamespace name addr []

View File

@ -51,7 +51,7 @@ relativeQualifiedName prefix paths = RelativeQualifiedName (BC.unpack prefix) (J
-- Subsequent imports of `parent.two` or `parent.three` will execute
-- `parent/two/__init__.py` and
-- `parent/three/__init__.py` respectively.
resolvePythonModules :: MonadEvaluatable location term value m => QualifiedName -> m (NonEmpty ModulePath)
resolvePythonModules :: MonadEvaluatable location term value effects m => QualifiedName -> m effects (NonEmpty ModulePath)
resolvePythonModules q = do
relRootDir <- rootDir q <$> currentModule
for (moduleNames q) $ \name -> do
@ -74,7 +74,7 @@ resolvePythonModules q = do
let searchPaths = [ path </> "__init__.py"
, path <.> ".py"
]
resolve searchPaths >>= maybeFail (notFound searchPaths)
resolve searchPaths >>= maybeM (raise (fail (notFound searchPaths)))
friendlyName :: QualifiedName -> String
friendlyName (QualifiedName xs) = intercalate "." (NonEmpty.toList xs)
@ -121,7 +121,7 @@ instance Show1 QualifiedImport where liftShowsPrec = genericLiftShowsPrec
-- import a.b.c
instance Evaluatable QualifiedImport where
eval (QualifiedImport (RelativeQualifiedName _ _)) = fail "technically this is not allowed in python"
eval (QualifiedImport (RelativeQualifiedName _ _)) = raise (fail "technically this is not allowed in python")
eval (QualifiedImport name@(QualifiedName qualifiedName)) = do
modulePaths <- resolvePythonModules name
go (NonEmpty.zip (FV.name . BC.pack <$> qualifiedName) modulePaths)

View File

@ -16,14 +16,14 @@ import System.FilePath.Posix
-- TODO: Fully sort out ruby require/load mechanics
--
-- require "json"
resolveRubyName :: forall value term location m. MonadEvaluatable location term value m => ByteString -> m ModulePath
resolveRubyName :: forall value term location effects m. MonadEvaluatable location term value effects m => ByteString -> m effects ModulePath
resolveRubyName name = do
let name' = cleanNameOrPath name
modulePath <- resolve [name' <.> "rb"]
maybe (throwResumable @(ResolutionError value) $ RubyError name') pure modulePath
-- load "/root/src/file.rb"
resolveRubyPath :: forall value term location m. MonadEvaluatable location term value m => ByteString -> m ModulePath
resolveRubyPath :: forall value term location effects m. MonadEvaluatable location term value effects m => ByteString -> m effects ModulePath
resolveRubyPath path = do
let name' = cleanNameOrPath path
modulePath <- resolve [name']
@ -68,9 +68,9 @@ instance Evaluatable Require where
modifyEnv (`mergeNewer` importedEnv)
pure v -- Returns True if the file was loaded, False if it was already loaded. http://ruby-doc.org/core-2.5.0/Kernel.html#method-i-require
doRequire :: MonadEvaluatable location term value m
doRequire :: MonadEvaluatable location term value effects m
=> ModulePath
-> m (Environment location value, value)
-> m effects (Environment location value, value)
doRequire name = do
moduleTable <- getModuleTable
case ModuleTable.lookup name moduleTable of
@ -93,9 +93,9 @@ instance Evaluatable Load where
path <- subtermValue x >>= asString
shouldWrap <- subtermValue wrap >>= asBool
doLoad path shouldWrap
eval (Load _) = fail "invalid argument supplied to load, path is required"
eval (Load _) = raise (fail "invalid argument supplied to load, path is required")
doLoad :: MonadEvaluatable location term value m => ByteString -> Bool -> m value
doLoad :: MonadEvaluatable location term value effects m => ByteString -> Bool -> m effects value
doLoad path shouldWrap = do
path' <- resolveRubyPath path
(importedEnv, _) <- traceResolve path path' $ isolate (load path')

View File

@ -31,7 +31,7 @@ toName = FV.name . BC.pack . unPath
-- Node.js resolution algorithm: https://nodejs.org/api/modules.html#modules_all_together
-- TypeScript has a couple of different strategies, but the main one mimics Node.js.
resolveWithNodejsStrategy :: forall value term location m. MonadEvaluatable location term value m => ImportPath -> [String] -> m ModulePath
resolveWithNodejsStrategy :: MonadEvaluatable location term value effects m => ImportPath -> [String] -> m effects ModulePath
resolveWithNodejsStrategy (ImportPath path Relative) exts = resolveRelativePath path exts
resolveWithNodejsStrategy (ImportPath path NonRelative) exts = resolveNonRelativePath path exts
@ -42,7 +42,7 @@ resolveWithNodejsStrategy (ImportPath path NonRelative) exts = resolveNonRelativ
-- /root/src/moduleB.ts
-- /root/src/moduleB/package.json (if it specifies a "types" property)
-- /root/src/moduleB/index.ts
resolveRelativePath :: forall value term location m. MonadEvaluatable location term value m => FilePath -> [String] -> m ModulePath
resolveRelativePath :: forall value term location effects m. MonadEvaluatable location term value effects m => FilePath -> [String] -> m effects ModulePath
resolveRelativePath relImportPath exts = do
ModuleInfo{..} <- currentModule
let relRootDir = takeDirectory modulePath
@ -61,7 +61,7 @@ resolveRelativePath relImportPath exts = do
--
-- /root/node_modules/moduleB.ts, etc
-- /node_modules/moduleB.ts, etc
resolveNonRelativePath :: forall value term location m. MonadEvaluatable location term value m => FilePath -> [String] -> m ModulePath
resolveNonRelativePath :: forall value term location effects m. MonadEvaluatable location term value effects m => FilePath -> [String] -> m effects ModulePath
resolveNonRelativePath name exts = do
ModuleInfo{..} <- currentModule
go "." modulePath mempty
@ -76,7 +76,7 @@ resolveNonRelativePath name exts = do
Right m -> traceResolve name m $ pure m
notFound _ = throwResumable @(ResolutionError value) $ TypeScriptError name
resolveTSModule :: MonadEvaluatable location term value m => FilePath -> [String] -> m (Either [FilePath] ModulePath)
resolveTSModule :: MonadEvaluatable location term value effects m => FilePath -> [String] -> m effects (Either [FilePath] ModulePath)
resolveTSModule path exts = maybe (Left searchPaths) Right <$> resolve searchPaths
where searchPaths =
((path <.>) <$> exts)
@ -91,7 +91,7 @@ typescriptExtensions = ["ts", "tsx", "d.ts"]
javascriptExtensions :: [String]
javascriptExtensions = ["js"]
evalRequire :: MonadEvaluatable location term value m => ModulePath -> Name -> m value
evalRequire :: MonadEvaluatable location term value effects m => ModulePath -> Name -> m effects value
evalRequire modulePath alias = letrec' alias $ \addr -> do
(importedEnv, _) <- isolate (require modulePath)
modifyEnv (mappend importedEnv)

View File

@ -3,7 +3,6 @@ module Prologue
( module X
, foldMapA
, maybeM
, maybeFail
, maybeLast
, fromMaybeLast
) where
@ -73,7 +72,3 @@ fromMaybeLast b = fromMaybe b . getLast . foldMap (Last . Just)
-- | Extract the 'Just' of a 'Maybe' in an 'Applicative' context or, given 'Nothing', run the provided action.
maybeM :: Applicative f => f a -> Maybe a -> f a
maybeM f = maybe f pure
-- | Either extract the 'Just' of a 'Maybe' or invoke 'fail' with the provided string.
maybeFail :: MonadFail m => String -> Maybe a -> m a
maybeFail s = maybeM (X.fail s)

View File

@ -1,5 +1,5 @@
-- MonoLocalBinds is to silence a warning about a simplifiable constraint.
{-# LANGUAGE DataKinds, MonoLocalBinds, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
{-# LANGUAGE MonoLocalBinds, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
{-# OPTIONS_GHC -Wno-missing-signatures #-}
module Semantic.Util where

View File

@ -12,7 +12,7 @@ module SpecHelpers (
, TestEvaluating
, ) where
import Analysis.Abstract.Evaluating as X (EvaluatingState(..))
import Control.Abstract.Evaluator as X (EvaluatorState(..))
import Data.Abstract.Address as X
import Data.Abstract.FreeVariables as X hiding (dropExtension)
import Data.Abstract.Heap as X