Merge branch 'master' into gorzell-container

2024-12-20 05:11:44 +03:00 · 2018-03-16 13:15:42 +01:00 · 2018-03-16 13:15:42 +01:00 · 165697d927
commit 165697d927
parent 598230738c 2cae3739dc
29 changed files with 406 additions and 259 deletions
--- a/semantic.cabal
+++ b/semantic.cabal
@ -20,6 +20,7 @@ library
                     , Analysis.Abstract.Dead
                     , Analysis.Abstract.Evaluating
                     , Analysis.Abstract.Tracing
+                     , Analysis.CallGraph
                     , Analysis.ConstructorName
                     , Analysis.CyclomaticComplexity
                     , Analysis.Decorator
@ -46,10 +47,10 @@ library
                     , Data.Abstract.Environment
                     , Data.Abstract.Evaluatable
                     , Data.Abstract.FreeVariables
+                     , Data.Abstract.Heap
                     , Data.Abstract.Live
                     , Data.Abstract.ModuleTable
                     , Data.Abstract.Number
-                     , Data.Abstract.Store
                     , Data.Abstract.Type
                     , Data.Abstract.Value
                     -- General datatype definitions & generic algorithms
--- a/src/Analysis/Abstract/Caching.hs
+++ b/src/Analysis/Abstract/Caching.hs
@ -6,9 +6,8 @@ module Analysis.Abstract.Caching
 import Control.Abstract.Analysis
 import Data.Abstract.Cache
 import Data.Abstract.Configuration
-import Data.Abstract.Store
+import Data.Abstract.Heap
 import Data.Abstract.Value
-import Data.Monoid (Alt (..))
 import Prologue

 -- | The effects necessary for caching analyses.
@ -26,22 +25,23 @@ type CacheFor term value = Cache (LocationFor value) term value
 newtype Caching m term value (effects :: [* -> *]) a = Caching (m term value effects a)
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

+deriving instance MonadControl term (m term value effects) => MonadControl term (Caching m term value effects)
 deriving instance MonadEnvironment value (m term value effects) => MonadEnvironment value (Caching m term value effects)
-deriving instance MonadStore value (m term value effects) => MonadStore value (Caching m term value effects)
+deriving instance MonadHeap value (m term value effects) => MonadHeap value (Caching m term value effects)
 deriving instance MonadModuleTable term value (m term value effects) => MonadModuleTable term value (Caching m term value effects)
 deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (Caching m term value effects)

 -- | Functionality used to perform caching analysis. This is not exported, and exists primarily for organizational reasons.
 class MonadEvaluator term value m => MonadCaching term value m where
  -- | Look up the set of values for a given configuration in the in-cache.
-  consultOracle :: ConfigurationFor term value -> m (Set (value, StoreFor value))
+  consultOracle :: ConfigurationFor term value -> m (Set (value, HeapFor value))
  -- | Run an action with the given in-cache.
  withOracle :: CacheFor term value -> m a -> m a

  -- | Look up the set of values for a given configuration in the out-cache.
-  lookupCache :: ConfigurationFor term value -> m (Maybe (Set (value, StoreFor value)))
-  -- | Run an action, caching its result and 'Store' under the given configuration.
-  caching :: ConfigurationFor term value -> Set (value, StoreFor value) -> m value -> m value
+  lookupCache :: ConfigurationFor term value -> m (Maybe (Set (value, HeapFor value)))
+  -- | Run an action, caching its result and 'Heap' under the given configuration.
+  caching :: ConfigurationFor term value -> Set (value, HeapFor value) -> m value -> m value

  -- | Run an action starting from an empty out-cache, and return the out-cache afterwards.
  isolateCache :: m a -> m (CacheFor term value)
@ -61,7 +61,7 @@ instance ( Effectful (m term value)
  lookupCache configuration = raise (cacheLookup configuration <$> get)
  caching configuration values action = do
    raise (modify (cacheSet configuration values))
-    result <- (,) <$> action <*> getStore
+    result <- (,) <$> action <*> getHeap
    raise (modify (cacheInsert configuration result))
    pure (fst result)

@ -97,7 +97,7 @@ instance ( Corecursive term
    c <- getConfiguration e
    -- Convergence here is predicated upon an Eq instance, not α-equivalence
    cache <- converge (\ prevCache -> isolateCache $ do
-      putStore (configurationStore c)
+      putHeap (configurationHeap c)
      -- We need to reset fresh generation so that this invocation converges.
      reset 0
      -- This is subtle: though the calling context supports nondeterminism, we want
@ -124,5 +124,5 @@ converge f = loop
            loop x'

 -- | Nondeterministically write each of a collection of stores & return their associated results.
-scatter :: (Alternative m, Foldable t, MonadEvaluator term value m) => t (a, Store (LocationFor value) value) -> m a
-scatter = getAlt . foldMap (\ (value, store') -> Alt (putStore store' *> pure value))
+scatter :: (Alternative m, Foldable t, MonadEvaluator term value m) => t (a, Heap (LocationFor value) value) -> m a
+scatter = foldMapA (\ (value, heap') -> putHeap heap' *> pure value)
--- a/src/Analysis/Abstract/Collecting.hs
+++ b/src/Analysis/Abstract/Collecting.hs
@ -6,16 +6,17 @@ module Analysis.Abstract.Collecting
 import Control.Abstract.Analysis
 import Data.Abstract.Address
 import Data.Abstract.Configuration
+import Data.Abstract.Heap
 import Data.Abstract.Live
-import Data.Abstract.Store
 import Data.Abstract.Value
 import Prologue

 newtype Collecting m term value (effects :: [* -> *]) a = Collecting (m term value effects a)
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

+deriving instance MonadControl term (m term value effects) => MonadControl term (Collecting m term value effects)
 deriving instance MonadEnvironment value (m term value effects) => MonadEnvironment value (Collecting m term value effects)
-deriving instance MonadStore value (m term value effects) => MonadStore value (Collecting m term value effects)
+deriving instance MonadHeap value (m term value effects) => MonadHeap value (Collecting m term value effects)
 deriving instance MonadModuleTable term value (m term value effects) => MonadModuleTable term value (Collecting m term value effects)

 instance ( Effectful (m term value)
@ -23,7 +24,7 @@ instance ( Effectful (m term value)
         , MonadEvaluator term value (m term value effects)
         )
         => MonadEvaluator term value (Collecting m term value effects) where
-  getConfiguration term = Configuration term <$> askRoots <*> askLocalEnv <*> getStore
+  getConfiguration term = Configuration term <$> askRoots <*> askLocalEnv <*> getHeap


 instance ( Effectful (m term value)
@ -42,7 +43,7 @@ instance ( Effectful (m term value)
  analyzeTerm term = do
    roots <- askRoots
    v <- liftAnalyze analyzeTerm term
-    modifyStore (gc (roots <> valueRoots v))
+    modifyHeap (gc (roots <> valueRoots v))
    pure v


@ -55,27 +56,27 @@ askRoots = raise ask
 -- extraRoots roots = raise . local (<> roots) . lower


-- | Collect any addresses in the store not rooted in or reachable from the given 'Live' set.
+-- | Collect any addresses in the heap not rooted in or reachable from the given 'Live' set.
 gc :: ( Ord (LocationFor value)
      , Foldable (Cell (LocationFor value))
      , ValueRoots value
      )
   => LiveFor value -- ^ The set of addresses to consider rooted.
-   -> StoreFor value -- ^ A store to collect unreachable addresses within.
-   -> StoreFor value -- ^ A garbage-collected store.
-gc roots store = storeRestrict store (reachable roots store)
+   -> HeapFor value -- ^ A heap to collect unreachable addresses within.
+   -> HeapFor value -- ^ A garbage-collected heap.
+gc roots heap = heapRestrict heap (reachable roots heap)

-- | Compute the set of addresses reachable from a given root set in a given store.
+-- | Compute the set of addresses reachable from a given root set in a given heap.
 reachable :: ( Ord (LocationFor value)
             , Foldable (Cell (LocationFor value))
             , ValueRoots value
             )
          => LiveFor value -- ^ The set of root addresses.
-          -> StoreFor value -- ^ The store to trace addresses through.
+          -> HeapFor value -- ^ The heap to trace addresses through.
          -> LiveFor value -- ^ The set of addresses reachable from the root set.
-reachable roots store = go mempty roots
+reachable roots heap = go mempty roots
  where go seen set = case liveSplit set of
          Nothing -> seen
-          Just (a, as) -> go (liveInsert a seen) (case storeLookupAll a store of
+          Just (a, as) -> go (liveInsert a seen) (case heapLookupAll a heap of
            Just values -> liveDifference (foldr ((<>) . valueRoots) mempty values <> as) seen
            _           -> seen)
--- a/src/Analysis/Abstract/Dead.hs
+++ b/src/Analysis/Abstract/Dead.hs
@ -12,8 +12,9 @@ import Prologue
 newtype DeadCode m term value (effects :: [* -> *]) a = DeadCode (m term value effects a)
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

+deriving instance MonadControl term (m term value effects) => MonadControl term (DeadCode m term value effects)
 deriving instance MonadEnvironment value (m term value effects) => MonadEnvironment value (DeadCode m term value effects)
-deriving instance MonadStore value (m term value effects) => MonadStore value (DeadCode m term value effects)
+deriving instance MonadHeap value (m term value effects) => MonadHeap value (DeadCode m term value effects)
 deriving instance MonadModuleTable term value (m term value effects) => MonadModuleTable term value (DeadCode m term value effects)
 deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (DeadCode m term value effects)

--- a/src/Analysis/Abstract/Evaluating.hs
+++ b/src/Analysis/Abstract/Evaluating.hs
@ -18,6 +18,7 @@ import Data.Abstract.Address
 import Data.Abstract.ModuleTable
 import Data.Abstract.Value
 import Data.Blob
+import qualified Data.IntMap as IntMap
 import Data.Language
 import Data.List.Split (splitWhen)
 import Prelude hiding (fail)
@ -32,7 +33,7 @@ evaluate :: forall value term effects
            , Evaluatable (Base term)
            , FreeVariables term
            , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-            , MonadValue term value (Evaluating term value effects)
+            , MonadValue value (Evaluating term value effects)
            , Recursive term
            )
         => term
@ -45,7 +46,7 @@ evaluates :: forall value term effects
             , Evaluatable (Base term)
             , FreeVariables term
             , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-             , MonadValue term value (Evaluating term value effects)
+             , MonadValue value (Evaluating term value effects)
             , Recursive term
             )
          => [(Blob, term)] -- List of (blob, term) pairs that make up the program to be evaluated
@ -70,7 +71,6 @@ withModules Blob{..} pairs = localModuleTable (const moduleTable)
 newtype Evaluating term value effects a = Evaluating (Eff effects a)
  deriving (Applicative, Functor, Effectful, Monad)

-
 deriving instance Member Fail      effects => MonadFail   (Evaluating term value effects)
 deriving instance Member Fresh     effects => MonadFresh  (Evaluating term value effects)
 deriving instance Member NonDetEff effects => Alternative (Evaluating term value effects)
@ -81,13 +81,23 @@ type EvaluatingEffects term value
  = '[ Fail                                        -- Failure with an error message
     , Reader (EnvironmentFor value)               -- Local environment (e.g. binding over a closure)
     , State  (EnvironmentFor value)               -- Global (imperative) environment
-     , State  (StoreFor value)                     -- The heap
+     , State  (HeapFor value)                     -- The heap
     , Reader (ModuleTable [term])                 -- Cache of unevaluated modules
     , State  (ModuleTable (EnvironmentFor value)) -- Cache of evaluated modules

     , State (Map Name (Name, Maybe (Address (LocationFor value) value))) -- Set of exports
+     , State (IntMap.IntMap term) -- For jumps
     ]

+instance Members '[Fail, State (IntMap.IntMap term)] effects => MonadControl term (Evaluating term value effects) where
+  label term = do
+    m <- raise get
+    let i = IntMap.size m
+    raise (put (IntMap.insert i term m))
+    pure i
+
+  goto label = IntMap.lookup label <$> raise get >>= maybe (fail ("unknown label: " <> show label)) pure
+
 instance Members '[State (Map Name (Name, Maybe (Address (LocationFor value) value))), Reader (EnvironmentFor value), State (EnvironmentFor value)] effects => MonadEnvironment value (Evaluating term value effects) where
  getGlobalEnv = raise get
  putGlobalEnv = raise . put
@ -100,9 +110,9 @@ instance Members '[State (Map Name (Name, Maybe (Address (LocationFor value) val
  askLocalEnv = raise ask
  localEnv f a = raise (local f (lower a))

-instance Member (State (StoreFor value)) effects => MonadStore value (Evaluating term value effects) where
-  getStore = raise get
-  putStore = raise . put
+instance Member (State (HeapFor value)) effects => MonadHeap value (Evaluating term value effects) where
+  getHeap = raise get
+  putHeap = raise . put

 instance Members '[Reader (ModuleTable [term]), State (ModuleTable (EnvironmentFor value))] effects => MonadModuleTable term value (Evaluating term value effects) where
  getModuleTable = raise get
@ -112,13 +122,13 @@ instance Members '[Reader (ModuleTable [term]), State (ModuleTable (EnvironmentF
  localModuleTable f a = raise (local f (lower a))

 instance Members (EvaluatingEffects term value) effects => MonadEvaluator term value (Evaluating term value effects) where
-  getConfiguration term = Configuration term mempty <$> askLocalEnv <*> getStore
+  getConfiguration term = Configuration term mempty <$> askLocalEnv <*> getHeap

 instance ( Evaluatable (Base term)
         , FreeVariables term
         , Members (EvaluatingEffects term value) effects
         , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-         , MonadValue term value (Evaluating term value effects)
+         , MonadValue value (Evaluating term value effects)
         , Recursive term
         )
         => MonadAnalysis term value (Evaluating term value effects) where
--- a/src/Analysis/Abstract/Tracing.hs
+++ b/src/Analysis/Abstract/Tracing.hs
@ -17,8 +17,9 @@ import Prologue hiding (trace)
 newtype Tracing (trace :: * -> *) m term value (effects :: [* -> *]) a = Tracing (m term value effects a)
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

+deriving instance MonadControl term (m term value effects) => MonadControl term (Tracing trace m term value effects)
 deriving instance MonadEnvironment value (m term value effects) => MonadEnvironment value (Tracing trace m term value effects)
-deriving instance MonadStore value (m term value effects) => MonadStore value (Tracing trace m term value effects)
+deriving instance MonadHeap value (m term value effects) => MonadHeap value (Tracing trace m term value effects)
 deriving instance MonadModuleTable term value (m term value effects) => MonadModuleTable term value (Tracing trace m term value effects)
 deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (Tracing trace m term value effects)

--- a/src/Analysis/CallGraph.hs
+++ b/src/Analysis/CallGraph.hs
@ -0,0 +1,109 @@
+{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies, UndecidableInstances #-}
+module Analysis.CallGraph
+( CallGraph(..)
+, renderCallGraph
+, buildCallGraph
+, CallGraphAlgebra(..)
+) where
+
+import qualified Algebra.Graph as G
+import Algebra.Graph.Class
+import Algebra.Graph.Export.Dot
+import Data.Abstract.FreeVariables
+import Data.Set (member)
+import qualified Data.Syntax as Syntax
+import qualified Data.Syntax.Declaration as Declaration
+import Data.Term
+import Prologue hiding (empty)
+
+-- | The graph of function definitions to symbols used in a given program.
+newtype CallGraph = CallGraph { unCallGraph :: G.Graph Name }
+  deriving (Eq, Graph, Show)
+
+-- | Build the 'CallGraph' for a 'Term' recursively.
+buildCallGraph :: (CallGraphAlgebra syntax, Foldable syntax, FreeVariables1 syntax, Functor syntax) => Term syntax ann -> Set Name -> CallGraph
+buildCallGraph = foldSubterms callGraphAlgebra
+
+
+-- | Render a 'CallGraph' to a 'ByteString' in DOT notation.
+renderCallGraph :: CallGraph -> ByteString
+renderCallGraph = export (defaultStyle friendlyName) . unCallGraph
+
+
+-- | Types which contribute to a 'CallGraph'. There is exactly one instance of this typeclass; customizing the 'CallGraph's for a new type is done by defining an instance of 'CustomCallGraphAlgebra' instead.
+--
+--   This typeclass employs the Advanced Overlap techniques designed by Oleg Kiselyov & Simon Peyton Jones: https://wiki.haskell.org/GHC/AdvancedOverlap.
+class CallGraphAlgebra syntax where
+  -- | A 'SubtermAlgebra' computing the 'CallGraph' for a piece of @syntax@.
+  callGraphAlgebra :: FreeVariables term => syntax (Subterm term (Set Name -> CallGraph)) -> Set Name -> CallGraph
+
+instance (CallGraphAlgebraStrategy syntax ~ strategy, CallGraphAlgebraWithStrategy strategy syntax) => CallGraphAlgebra syntax where
+  callGraphAlgebra = callGraphAlgebraWithStrategy (Proxy :: Proxy strategy)
+
+
+-- | Types whose contribution to a 'CallGraph' is customized. If an instance’s definition is not being used, ensure that the type is mapped to 'Custom' in the 'CallGraphAlgebraStrategy'.
+class CustomCallGraphAlgebra syntax where
+  customCallGraphAlgebra :: FreeVariables term => syntax (Subterm term (Set Name -> CallGraph)) -> Set Name -> CallGraph
+
+-- | 'Declaration.Function's produce a vertex for their name, with edges to any free variables in their body.
+instance CustomCallGraphAlgebra Declaration.Function where
+  customCallGraphAlgebra Declaration.Function{..} bound = foldMap vertex (freeVariables (subterm functionName)) `connect` subtermValue functionBody (foldMap (freeVariables . subterm) functionParameters <> bound)
+
+-- | 'Declaration.Method's produce a vertex for their name, with edges to any free variables in their body.
+instance CustomCallGraphAlgebra Declaration.Method where
+  customCallGraphAlgebra Declaration.Method{..} bound = foldMap vertex (freeVariables (subterm methodName)) `connect` subtermValue methodBody (foldMap (freeVariables . subterm) methodParameters <> bound)
+
+-- | 'Syntax.Identifier's produce a vertex iff it’s unbound in the 'Set'.
+instance CustomCallGraphAlgebra Syntax.Identifier where
+  customCallGraphAlgebra (Syntax.Identifier name) bound
+    | name `member` bound = empty
+    | otherwise           = vertex name
+
+instance Apply CallGraphAlgebra syntaxes => CustomCallGraphAlgebra (Union syntaxes) where
+  customCallGraphAlgebra = Prologue.apply (Proxy :: Proxy CallGraphAlgebra) callGraphAlgebra
+
+instance CallGraphAlgebra syntax => CustomCallGraphAlgebra (TermF syntax a) where
+  customCallGraphAlgebra = callGraphAlgebra . termFOut
+
+
+-- | The mechanism selecting 'Default'/'Custom' implementations for 'callGraphAlgebra' depending on the @syntax@ type.
+class CallGraphAlgebraWithStrategy (strategy :: Strategy) syntax where
+  callGraphAlgebraWithStrategy :: FreeVariables term => proxy strategy -> syntax (Subterm term (Set Name -> CallGraph)) -> Set Name -> CallGraph
+
+-- | The 'Default' definition of 'callGraphAlgebra' combines all of the 'CallGraph's within the @syntax@ 'Monoid'ally.
+instance Foldable syntax => CallGraphAlgebraWithStrategy 'Default syntax where
+  callGraphAlgebraWithStrategy _ = foldMap subtermValue
+
+-- | The 'Custom' strategy calls out to the 'customCallGraphAlgebra' method.
+instance CustomCallGraphAlgebra syntax => CallGraphAlgebraWithStrategy 'Custom syntax where
+  callGraphAlgebraWithStrategy _ = customCallGraphAlgebra
+
+
+-- | Which instance of 'CustomCallGraphAlgebra' to use for a given @syntax@ type.
+data Strategy = Default | Custom
+
+-- | A mapping of @syntax@ types onto 'Strategy's.
+type family CallGraphAlgebraStrategy syntax where
+  CallGraphAlgebraStrategy Declaration.Function = 'Custom
+  CallGraphAlgebraStrategy Declaration.Method = 'Custom
+  CallGraphAlgebraStrategy Syntax.Identifier = 'Custom
+  CallGraphAlgebraStrategy (Union fs) = 'Custom
+  CallGraphAlgebraStrategy (TermF f a) = 'Custom
+  CallGraphAlgebraStrategy a = 'Default
+
+
+instance Monoid CallGraph where
+  mempty = empty
+  mappend = overlay
+
+instance Ord CallGraph where
+  compare (CallGraph G.Empty)           (CallGraph G.Empty)           = EQ
+  compare (CallGraph G.Empty)           _                             = LT
+  compare _                             (CallGraph G.Empty)           = GT
+  compare (CallGraph (G.Vertex a))      (CallGraph (G.Vertex b))      = compare a b
+  compare (CallGraph (G.Vertex _))      _                             = LT
+  compare _                             (CallGraph (G.Vertex _))      = GT
+  compare (CallGraph (G.Overlay a1 a2)) (CallGraph (G.Overlay b1 b2)) = (compare `on` CallGraph) a1 b1 <> (compare `on` CallGraph) a2 b2
+  compare (CallGraph (G.Overlay _  _))  _                             = LT
+  compare _                             (CallGraph (G.Overlay _ _))   = GT
+  compare (CallGraph (G.Connect a1 a2)) (CallGraph (G.Connect b1 b2)) = (compare `on` CallGraph) a1 b1 <> (compare `on` CallGraph) a2 b2
--- a/src/Control/Abstract/Addressable.hs
+++ b/src/Control/Abstract/Addressable.hs
@ -7,58 +7,36 @@ import Control.Monad ((<=<))
 import Data.Abstract.Address
 import Data.Abstract.Environment
 import Data.Abstract.FreeVariables
-import Data.Abstract.Store
+import Data.Abstract.Heap
 import Data.Abstract.Value
-import Data.Foldable (asum, toList)
-import Data.Semigroup
 import Data.Semigroup.Reducer
 import Prelude hiding (fail)
+import Prologue

-- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Store.
+-- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Heap.
 class (Monad m, Ord l, l ~ LocationFor value, Reducer value (Cell l value)) => MonadAddressable l value m where
  deref :: Address l value -> m value

  alloc :: Name -> m (Address l value)

-- | Look up or allocate an address for a 'Name' free in a given term & assign it a given value, returning the 'Name' paired with the address.
--
--   The term is expected to contain one and only one free 'Name', meaning that care should be taken to apply this only to e.g. identifiers.
-lookupOrAlloc :: ( FreeVariables term
-                 , MonadAddressable (LocationFor value) value m
-                 , MonadStore value m
-                 , Semigroup (CellFor value)
-                 )
-                 => term
-                 -> value
-                 -> EnvironmentFor value
-                 -> m (Name, Address (LocationFor value) value)
-lookupOrAlloc term = let [name] = toList (freeVariables term) in
-                         lookupOrAlloc' name
-
-- | Look up or allocate an address for a 'Name' & assign it a given value, returning the 'Name' paired with the address.
-lookupOrAlloc' :: ( Semigroup (CellFor value)
-                  , MonadAddressable (LocationFor value) value m
-                  , MonadStore value m
+-- | Look up or allocate an address for a 'Name'.
+lookupOrAlloc :: ( MonadAddressable (LocationFor value) value m
+                 , MonadEnvironment value m
                 )
                 => Name
-                  -> value
-                  -> EnvironmentFor value
-                  -> m (Name, Address (LocationFor value) value)
-lookupOrAlloc' name v env = do
-  a <- maybe (alloc name) pure (envLookup name env)
-  assign a v
-  pure (name, a)
+                 -> m (Address (LocationFor value) value)
+lookupOrAlloc name = lookupLocalEnv name >>= maybe (alloc name) pure


 letrec :: ( MonadAddressable (LocationFor value) value m
          , MonadEnvironment value m
-          , MonadStore value m
+          , MonadHeap value m
          )
       => Name
       -> m value
       -> m (value, Address (LocationFor value) value)
 letrec name body = do
-  addr <- alloc name
+  addr <- lookupOrAlloc name
  v <- localEnv (envInsert name addr) body
  assign addr v
  pure (v, addr)
@ -67,18 +45,20 @@ 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, LocationFor value ~ Precise, MonadStore value m) => MonadAddressable Precise value m where
-  deref = maybe uninitializedAddress (pure . unLatest) <=< flip fmap getStore . storeLookup
-    where
-      -- | 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 => m a
-      uninitializedAddress = fail "uninitialized address"
-
-  alloc _ = fmap (Address . Precise . storeSize) getStore
+instance (MonadFail m, LocationFor value ~ Precise, MonadHeap value m) => MonadAddressable Precise value m where
+  deref = derefWith (pure . unLatest)
+  alloc _ = fmap (Address . Precise . heapSize) getHeap


 -- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically.
-instance (Alternative m, LocationFor value ~ Monovariant, MonadStore value m, Ord value) => MonadAddressable Monovariant value m where
-  deref = asum . maybe [] (map pure . toList) <=< flip fmap getStore . storeLookup
-
+instance (Alternative m, LocationFor value ~ Monovariant, MonadFail m, MonadHeap value m, Ord value) => MonadAddressable Monovariant value m where
+  deref = derefWith (foldMapA pure)
  alloc = pure . Address . Monovariant
+
+-- | Dereference the given 'Address' in the heap, using the supplied function to act on the cell, or failing if the address is uninitialized.
+derefWith :: (MonadFail m, MonadHeap value m, Ord (LocationFor value)) => (CellFor value -> m a) -> Address (LocationFor value) value -> m a
+derefWith with = maybe uninitializedAddress with <=< lookupHeap
+
+-- | 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 => m a
+uninitializedAddress = fail "uninitialized address"
--- a/src/Control/Abstract/Evaluator.hs
+++ b/src/Control/Abstract/Evaluator.hs
@ -3,18 +3,21 @@ module Control.Abstract.Evaluator
 ( MonadEvaluator(..)
 , MonadEnvironment(..)
 , modifyGlobalEnv
-, MonadStore(..)
-, modifyStore
+, MonadHeap(..)
+, modifyHeap
+, lookupHeap
 , assign
 , MonadModuleTable(..)
 , modifyModuleTable
+, MonadControl(..)
 ) where

 import Data.Abstract.Address
 import Data.Abstract.Configuration
+import Data.Abstract.Environment
 import Data.Abstract.FreeVariables
+import Data.Abstract.Heap
 import Data.Abstract.ModuleTable
-import Data.Abstract.Store
 import Data.Abstract.Value
 import Data.Semigroup.Reducer
 import Prelude hiding (fail)
@ -26,10 +29,11 @@ import Prologue
 --   - environments binding names to addresses
 --   - a heap mapping addresses to (possibly sets of) values
 --   - tables of modules available for import
-class ( MonadEnvironment value m
+class ( MonadControl term m
+      , MonadEnvironment value m
      , MonadFail m
      , MonadModuleTable term value m
-      , MonadStore value m
+      , MonadHeap value m
      )
      => MonadEvaluator term value m | m -> term, m -> value where
  -- | Get the current 'Configuration' with a passed-in term.
@ -55,6 +59,16 @@ class Monad m => MonadEnvironment value m | m -> value where
  -- | Run an action with a locally-modified environment.
  localEnv :: (EnvironmentFor value -> EnvironmentFor value) -> m a -> m a

+  -- | Look a 'Name' up in the local environment.
+  lookupLocalEnv :: Name -> m (Maybe (Address (LocationFor value) value))
+  lookupLocalEnv name = envLookup name <$> askLocalEnv
+
+  -- | Look up a 'Name' in the local environment, running an action with the resolved address (if any).
+  lookupWith :: (Address (LocationFor value) value -> m value) -> Name -> m (Maybe value)
+  lookupWith with name = do
+    addr <- lookupLocalEnv name
+    maybe (pure Nothing) (fmap Just . with) addr
+
 -- | Update the global environment.
 modifyGlobalEnv :: MonadEnvironment value m => (EnvironmentFor value -> EnvironmentFor value) -> m  ()
 modifyGlobalEnv f = do
@ -63,27 +77,31 @@ modifyGlobalEnv f = do


 -- | A 'Monad' abstracting a heap of values.
-class Monad m => MonadStore value m | m -> value where
+class Monad m => MonadHeap value m | m -> value where
  -- | Retrieve the heap.
-  getStore :: m (StoreFor value)
+  getHeap :: m (HeapFor value)
  -- | Set the heap.
-  putStore :: StoreFor value -> m ()
+  putHeap :: HeapFor value -> m ()

 -- | Update the heap.
-modifyStore :: MonadStore value m => (StoreFor value -> StoreFor value) -> m ()
-modifyStore f = do
-  s <- getStore
-  putStore $! f s
+modifyHeap :: MonadHeap value m => (HeapFor value -> HeapFor value) -> m ()
+modifyHeap f = do
+  s <- getHeap
+  putHeap $! f s
+
+-- | Look up the cell for the given 'Address' in the 'Heap'.
+lookupHeap :: (MonadHeap value m, Ord (LocationFor value)) => Address (LocationFor value) value -> m (Maybe (CellFor value))
+lookupHeap = flip fmap getHeap . heapLookup

 -- | Write a value to the given 'Address' in the 'Store'.
 assign :: ( Ord (LocationFor value)
-          , MonadStore value m
+          , MonadHeap value m
          , Reducer value (CellFor value)
          )
       => Address (LocationFor value) value
       -> value
       -> m ()
-assign address = modifyStore . storeInsert address
+assign address = modifyHeap . heapInsert address


 -- | A 'Monad' abstracting tables of modules available for import.
@ -103,3 +121,13 @@ modifyModuleTable :: MonadModuleTable term value m => (ModuleTable (EnvironmentF
 modifyModuleTable f = do
  table <- getModuleTable
  putModuleTable $! f table
+
+
+-- | 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
--- a/src/Control/Abstract/Value.hs
+++ b/src/Control/Abstract/Value.hs
@ -26,7 +26,7 @@ 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 (MonadAnalysis term value m, Show value) => MonadValue term value m where
+class (Monad m, Show value) => MonadValue value m where
  -- | Construct an abstract unit value.
  --   TODO: This might be the same as the empty tuple for some value types
  unit :: m value
@ -67,11 +67,14 @@ class (MonadAnalysis term value m, Show value) => MonadValue term value m where
  -- | Construct an N-ary tuple of multiple (possibly-disjoint) values
  multiple :: [value] -> m value

+  -- | Construct an array of zero or more values.
+  array :: [value] -> m value
+
  -- | Eliminate boolean values. TODO: s/boolean/truthy
  ifthenelse :: value -> m a -> m a -> m a

  -- | Evaluate an abstraction (a binder like a lambda or method definition).
-  abstract :: [Name] -> Subterm term (m value) -> m value
+  abstract :: (FreeVariables term, MonadControl term m) => [Name] -> Subterm term (m value) -> m value
  -- | Evaluate an application (like a function call).
  apply :: value -> [m value] -> m value

@ -81,10 +84,10 @@ class (MonadAnalysis term value m, Show value) => MonadValue term value m where
  loop :: (m value -> m value) -> m value

 -- | Attempt to extract a 'Prelude.Bool' from a given value.
-toBool :: MonadValue term value m => value -> m Bool
+toBool :: MonadValue value m => value -> m Bool
 toBool v = ifthenelse v (pure True) (pure False)

-forLoop :: MonadValue term value m
+forLoop :: (MonadEnvironment value m, MonadValue value m)
        => m value -- | Initial statement
        -> m value -- | Condition
        -> m value -- | Increment/stepper
@ -96,7 +99,7 @@ forLoop initial cond step body = do
  localEnv (mappend env) (while cond (body *> step))

 -- | The fundamental looping primitive, built on top of ifthenelse.
-while :: MonadValue term value m
+while :: MonadValue value m
      => m value
      -> m value
      -> m value
@ -105,7 +108,7 @@ while cond body = loop $ \ continue -> do
  ifthenelse this (body *> continue) unit

 -- | Do-while loop, built on top of while.
-doWhile :: MonadValue term value m
+doWhile :: MonadValue value m
        => m value
        -> m value
        -> m value
@ -114,13 +117,12 @@ doWhile body cond = loop $ \ continue -> body *> do
  ifthenelse this continue unit

 -- | Construct a 'Value' wrapping the value arguments (if any).
-instance ( FreeVariables term
-         , MonadAddressable location (Value location term) m
-         , MonadAnalysis term (Value location term) m
+instance ( Monad m
+         , MonadAddressable location Value m
+         , MonadAnalysis term Value m
         , Show location
-         , Show term
         )
-         => MonadValue term (Value location term) m where
+         => MonadValue Value m where

  unit     = pure . injValue $ Value.Unit
  integer  = pure . injValue . Value.Integer . Number.Integer
@ -132,6 +134,8 @@ instance ( FreeVariables term

  multiple = pure . injValue . Value.Tuple

+  array    = pure . injValue . Value.Array
+
  ifthenelse cond if' else'
    | Just (Boolean b) <- prjValue cond = if b then if' else else'
    | otherwise = fail ("not defined for non-boolean conditions: " <> show cond)
@ -155,7 +159,7 @@ instance ( FreeVariables term
    | otherwise = fail ("Invalid operands to liftNumeric2: " <> show pair)
      where
        -- Dispatch whatever's contained inside a 'SomeNumber' to its appropriate 'MonadValue' ctor
-        specialize :: MonadValue term value m => SomeNumber -> m value
+        specialize :: MonadValue value m => SomeNumber -> m value
        specialize (SomeNumber (Number.Integer i)) = integer i
        specialize (SomeNumber (Ratio r))          = rational r
        specialize (SomeNumber (Decimal d))        = float d
@ -173,7 +177,7 @@ instance ( FreeVariables term
      where
        -- Explicit type signature is necessary here because we're passing all sorts of things
        -- to these comparison functions.
-        go :: (Ord a, MonadValue term value m) => a -> a -> m value
+        go :: (Ord a, MonadValue value m) => a -> a -> m value
        go l r = case comparator of
          Concrete f  -> boolean (f l r)
          Generalized -> integer (orderingToInt (compare l r))
@ -184,21 +188,23 @@ instance ( FreeVariables term

        pair = (left, right)

-  abstract names (Subterm body _) = injValue . Closure names body . bindEnv (foldr Set.delete (freeVariables body) names) <$> askLocalEnv
+  abstract names (Subterm body _) = do
+    l <- label body
+    injValue . Closure names l . bindEnv (foldr Set.delete (freeVariables body) names) <$> askLocalEnv

  apply op params = do
-    Closure names body env <- maybe (fail ("expected a closure, got: " <> show op)) pure (prjValue op)
+    Closure names label env <- maybe (fail ("expected a closure, got: " <> show op)) pure (prjValue op)
    bindings <- foldr (\ (name, param) rest -> do
      v <- param
      a <- alloc name
      assign a v
      envInsert name a <$> rest) (pure env) (zip names params)
-    localEnv (mappend bindings) (evaluateTerm body)
+    localEnv (mappend bindings) (goto label >>= evaluateTerm)

  loop = fix

-- | Discard the value arguments (if any), constructing a 'Type.Type' instead.
-instance (Alternative m, MonadAnalysis term Type m, MonadFresh m) => MonadValue term Type m where
+-- | Discard the value arguments (if any), constructing a 'Type' instead.
+instance (Alternative m, MonadEnvironment Type m, MonadFail m, MonadFresh m, MonadHeap Type m) => MonadValue Type m where
  abstract names (Subterm _ body) = do
    (env, tvars) <- foldr (\ name rest -> do
      a <- alloc name
@ -217,6 +223,7 @@ instance (Alternative m, MonadAnalysis term Type m, MonadFresh m) => MonadValue
  symbol _   = pure Type.Symbol
  rational _ = pure Type.Rational
  multiple   = pure . Type.Product
+  array      = pure . Type.Array

  ifthenelse cond if' else' = unify cond Bool *> (if' <|> else')

--- a/src/Data/Abstract/Cache.hs
+++ b/src/Data/Abstract/Cache.hs
@ -3,30 +3,30 @@ module Data.Abstract.Cache where

 import Data.Abstract.Address
 import Data.Abstract.Configuration
-import Data.Abstract.Store
+import Data.Abstract.Heap
 import Data.Map.Monoidal as Monoidal
 import Prologue

-- | A map of 'Configuration's to 'Set's of resulting values & 'Store's.
-newtype Cache l t v = Cache { unCache :: Monoidal.Map (Configuration l t v) (Set (v, Store l v)) }
+-- | A map of 'Configuration's to 'Set's of resulting values & 'Heap's.
+newtype Cache l t v = Cache { unCache :: Monoidal.Map (Configuration l t v) (Set (v, Heap l v)) }

 deriving instance (Eq l, Eq t, Eq v, Eq (Cell l v)) => Eq (Cache l t v)
 deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Ord (Cache l t v)
 deriving instance (Show l, Show t, Show v, Show (Cell l v)) => Show (Cache l t v)
 deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Semigroup (Cache l t v)
 deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Monoid (Cache l t v)
-deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Reducer (Configuration l t v, (v, Store l v)) (Cache l t v)
+deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Reducer (Configuration l t v, (v, Heap l v)) (Cache l t v)

-- | Look up the resulting value & 'Store' for a given 'Configuration'.
-cacheLookup :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Cache l t v -> Maybe (Set (v, Store l v))
+-- | Look up the resulting value & 'Heap' for a given 'Configuration'.
+cacheLookup :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Cache l t v -> Maybe (Set (v, Heap l v))
 cacheLookup key = Monoidal.lookup key . unCache

-- | Set the resulting value & 'Store' for a given 'Configuration', overwriting any previous entry.
-cacheSet :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Set (v, Store l v) -> Cache l t v -> Cache l t v
+-- | Set the resulting value & 'Heap' for a given 'Configuration', overwriting any previous entry.
+cacheSet :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Set (v, Heap l v) -> Cache l t v -> Cache l t v
 cacheSet key value = Cache . Monoidal.insert key value . unCache

-- | Insert the resulting value & 'Store' for a given 'Configuration', appending onto any previous entry.
-cacheInsert :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> (v, Store l v) -> Cache l t v -> Cache l t v
+-- | Insert the resulting value & 'Heap' for a given 'Configuration', appending onto any previous entry.
+cacheInsert :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> (v, Heap l v) -> Cache l t v -> Cache l t v
 cacheInsert = curry cons


@ -40,7 +40,7 @@ instance (Show l, Show t, Show1 (Cell l)) => Show1 (Cache l t) where
  liftShowsPrec spV slV d = showsUnaryWith (liftShowsPrec2 spKey slKey (liftShowsPrec spPair slPair) (liftShowList spPair slPair)) "Cache" d . unCache
      where spKey = liftShowsPrec spV slV
            slKey = liftShowList spV slV
-            spPair = liftShowsPrec2 spV slV spStore slStore
-            slPair = liftShowList2 spV slV spStore slStore
-            spStore = liftShowsPrec spV slV
-            slStore = liftShowList  spV slV
+            spPair = liftShowsPrec2 spV slV spHeap slHeap
+            slPair = liftShowList2 spV slV spHeap slHeap
+            spHeap = liftShowsPrec spV slV
+            slHeap = liftShowList  spV slV
--- a/src/Data/Abstract/Configuration.hs
+++ b/src/Data/Abstract/Configuration.hs
@ -3,8 +3,8 @@ module Data.Abstract.Configuration where

 import Data.Abstract.Address
 import Data.Abstract.Environment
+import Data.Abstract.Heap
 import Data.Abstract.Live
-import Data.Abstract.Store
 import Data.Abstract.Value
 import Prologue

@ -17,7 +17,7 @@ data Configuration l t v
    { configurationTerm        :: t               -- ^ The “instruction,” i.e. the current term to evaluate.
    , configurationRoots       :: Live l v        -- ^ The set of rooted addresses.
    , configurationEnvironment :: Environment l v -- ^ The environment binding any free variables in 'configurationTerm'.
-    , configurationStore       :: Store l v       -- ^ The store of values.
+    , configurationHeap        :: Heap l v        -- ^ The heap of values.
    }
    deriving (Generic1)

--- a/src/Data/Abstract/Environment.hs
+++ b/src/Data/Abstract/Environment.hs
@ -40,7 +40,7 @@ bindExports aliases env = Environment pairs
 --
 --   Unbound names are silently dropped.
 envRoots :: (Ord l, Foldable t) => Environment l a -> t Name -> Live l a
-envRoots env = foldr ((<>) . maybe mempty liveSingleton . flip envLookup env) mempty
+envRoots env = foldMap (maybe mempty liveSingleton . flip envLookup env)

 envAll :: (Ord l) => Environment l a -> Live l a
 envAll (Environment env) = Live $ Set.fromList (Map.elems env)
--- a/src/Data/Abstract/Evaluatable.hs
+++ b/src/Data/Abstract/Evaluatable.hs
@ -26,7 +26,7 @@ class Evaluatable constr where
  eval :: ( FreeVariables term
          , MonadAddressable (LocationFor value) value m
          , MonadAnalysis term value m
-          , MonadValue term value m
+          , MonadValue value m
          )
       => SubtermAlgebra constr term (m value)
  default eval :: (MonadFail m, Show1 constr) => SubtermAlgebra constr term (m value)
@ -60,6 +60,6 @@ instance MonadEnvironment value m => Semigroup (Imperative m a) where
    env <- getGlobalEnv
    localEnv (<> env) b

-instance MonadValue term value m => Monoid (Imperative m value) where
+instance (MonadEnvironment value m, MonadValue value m) => Monoid (Imperative m value) where
  mempty = Imperative unit
  mappend = (<>)
--- a/src/Data/Abstract/FreeVariables.hs
+++ b/src/Data/Abstract/FreeVariables.hs
@ -19,6 +19,11 @@ friendlyName :: Name -> ByteString
 friendlyName xs = intercalate "." (NonEmpty.toList xs)


+-- | The type of labels.
+--   TODO: This should be rolled into 'Name' and tracked in the environment, both so that we can abstract over labels like any other location, and so that we can garbage collect unreachable labels.
+type Label = Int
+
+
 -- | Types which can contain unbound variables.
 class FreeVariables term where
  -- | The set of free variables in the given value.
--- a/src/Data/Abstract/Heap.hs
+++ b/src/Data/Abstract/Heap.hs
@ -0,0 +1,45 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, UndecidableInstances #-}
+module Data.Abstract.Heap where
+
+import Data.Abstract.Address
+import Data.Abstract.Live
+import qualified Data.Map.Monoidal as Monoidal
+import Data.Semigroup.Reducer
+import Prologue
+
+-- | A map of addresses onto cells holding their values.
+newtype Heap l a = Heap { unStore :: Monoidal.Map l (Cell l a) }
+  deriving (Generic1)
+
+deriving instance (Eq l, Eq (Cell l a)) => Eq (Heap l a)
+deriving instance (Ord l, Ord (Cell l a)) => Ord (Heap l a)
+deriving instance (Show l, Show (Cell l a)) => Show (Heap l a)
+instance (Eq l, Eq1 (Cell l)) => Eq1 (Heap l) where liftEq = genericLiftEq
+instance (Ord l, Ord1 (Cell l)) => Ord1 (Heap l) where liftCompare = genericLiftCompare
+instance (Show l, Show1 (Cell l)) => Show1 (Heap l) where liftShowsPrec = genericLiftShowsPrec
+deriving instance Foldable (Cell l) => Foldable (Heap l)
+deriving instance Functor (Cell l) => Functor (Heap l)
+deriving instance Traversable (Cell l) => Traversable (Heap l)
+deriving instance (Ord l, Semigroup (Cell l a)) => Semigroup (Heap l a)
+deriving instance (Ord l, Semigroup (Cell l a)) => Monoid (Heap l a)
+deriving instance (Ord l, Reducer a (Cell l a)) => Reducer (l, a) (Heap l a)
+
+-- | Look up the cell of values for an 'Address' in a 'Heap', if any.
+heapLookup :: Ord l => Address l a -> Heap l a -> Maybe (Cell l a)
+heapLookup (Address address) = Monoidal.lookup address . unStore
+
+-- | Look up the list of values stored for a given address, if any.
+heapLookupAll :: (Ord l, Foldable (Cell l)) => Address l a -> Heap l a -> Maybe [a]
+heapLookupAll address = fmap toList . heapLookup address
+
+-- | Append a value onto the cell for a given address, inserting a new cell if none existed.
+heapInsert :: (Ord l, Reducer a (Cell l a)) => Address l a -> a -> Heap l a -> Heap l a
+heapInsert (Address address) value = flip snoc (address, value)
+
+-- | The number of addresses extant in a 'Heap'.
+heapSize :: Heap l a -> Int
+heapSize = Monoidal.size . unStore
+
+-- | Restrict a 'Heap' to only those 'Address'es in the given 'Live' set (in essence garbage collecting the rest).
+heapRestrict :: Ord l => Heap l a -> Live l a -> Heap l a
+heapRestrict (Heap m) roots = Heap (Monoidal.filterWithKey (\ address _ -> Address address `liveMember` roots) m)
--- a/src/Data/Abstract/Store.hs
+++ b/src/Data/Abstract/Store.hs
@ -1,45 +0,0 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, UndecidableInstances #-}
-module Data.Abstract.Store where
-
-import Data.Abstract.Address
-import Data.Abstract.Live
-import qualified Data.Map.Monoidal as Monoidal
-import Data.Semigroup.Reducer
-import Prologue
-
-- | A map of addresses onto cells holding their values.
-newtype Store l a = Store { unStore :: Monoidal.Map l (Cell l a) }
-  deriving (Generic1)
-
-deriving instance (Eq l, Eq (Cell l a)) => Eq (Store l a)
-deriving instance (Ord l, Ord (Cell l a)) => Ord (Store l a)
-deriving instance (Show l, Show (Cell l a)) => Show (Store l a)
-instance (Eq l, Eq1 (Cell l)) => Eq1 (Store l) where liftEq = genericLiftEq
-instance (Ord l, Ord1 (Cell l)) => Ord1 (Store l) where liftCompare = genericLiftCompare
-instance (Show l, Show1 (Cell l)) => Show1 (Store l) where liftShowsPrec = genericLiftShowsPrec
-deriving instance Foldable (Cell l) => Foldable (Store l)
-deriving instance Functor (Cell l) => Functor (Store l)
-deriving instance Traversable (Cell l) => Traversable (Store l)
-deriving instance (Ord l, Semigroup (Cell l a)) => Semigroup (Store l a)
-deriving instance (Ord l, Semigroup (Cell l a)) => Monoid (Store l a)
-deriving instance (Ord l, Reducer a (Cell l a)) => Reducer (l, a) (Store l a)
-
-- | Look up the cell of values for an 'Address' in a 'Store', if any.
-storeLookup :: Ord l => Address l a -> Store l a -> Maybe (Cell l a)
-storeLookup (Address address) = Monoidal.lookup address . unStore
-
-- | Look up the list of values stored for a given address, if any.
-storeLookupAll :: (Ord l, Foldable (Cell l)) => Address l a -> Store l a -> Maybe [a]
-storeLookupAll address = fmap toList . storeLookup address
-
-- | Append a value onto the cell for a given address, inserting a new cell if none existed.
-storeInsert :: (Ord l, Reducer a (Cell l a)) => Address l a -> a -> Store l a -> Store l a
-storeInsert (Address address) value = flip snoc (address, value)
-
-- | The number of addresses extant in a 'Store'.
-storeSize :: Store l a -> Int
-storeSize = Monoidal.size . unStore
-
-- | Restrict a 'Store' to only those 'Address'es in the given 'Live' set (in essence garbage collecting the rest).
-storeRestrict :: Ord l => Store l a -> Live l a -> Store l a
-storeRestrict (Store m) roots = Store (Monoidal.filterWithKey (\ address _ -> Address address `liveMember` roots) m)
--- a/src/Data/Abstract/Type.hs
+++ b/src/Data/Abstract/Type.hs
@ -19,6 +19,7 @@ data Type
  | Type :-> Type  -- ^ Binary function types.
  | Var TName      -- ^ A type variable.
  | Product [Type] -- ^ N-ary products.
+  | Array [Type]   -- ^ Arrays. Note that this is heterogenous.
  deriving (Eq, Ord, Show)

 -- TODO: À la carte representation of types.
--- a/src/Data/Abstract/Value.hs
+++ b/src/Data/Abstract/Value.hs
@ -1,10 +1,10 @@
-{-# LANGUAGE ConstraintKinds, DataKinds, FunctionalDependencies, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
+{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
 module Data.Abstract.Value where

 import Data.Abstract.Address
 import Data.Abstract.Environment
-import Data.Abstract.Store
 import Data.Abstract.FreeVariables
+import Data.Abstract.Heap
 import Data.Abstract.Live
 import Data.Abstract.Number
 import qualified Data.Abstract.Type as Type
@ -13,46 +13,47 @@ import Prologue
 import Prelude hiding (Float, Integer, String, Rational, fail)
 import qualified Prelude

-type ValueConstructors location term
-  = '[Closure location term
-    , Unit
+type ValueConstructors
+  = '[Array
    , Boolean
+    , Closure
    , Float
    , Integer
    , String
    , Rational
    , Symbol
    , Tuple
+    , Unit
    ]

 -- | Open union of primitive values that terms can be evaluated to.
 --   Fix by another name.
-newtype Value location term = Value { deValue :: Union (ValueConstructors location term) (Value location term) }
+newtype Value = Value { deValue :: Union ValueConstructors Value }
  deriving (Eq, Show, Ord)

 -- | Identical to 'inj', but wraps the resulting sub-entity in a 'Value'.
-injValue :: (f :< ValueConstructors location term) => f (Value location term) -> Value location term
+injValue :: (f :< ValueConstructors) => f Value -> Value
 injValue = Value . inj

 -- | Identical to 'prj', but unwraps the argument out of its 'Value' wrapper.
-prjValue :: (f :< ValueConstructors location term) => Value location term -> Maybe (f (Value location term))
+prjValue :: (f :< ValueConstructors) => Value -> Maybe (f Value)
 prjValue = prj . deValue

 -- | Convenience function for projecting two values.
-prjPair :: ( f :< ValueConstructors loc term1 , g :< ValueConstructors loc term2)
-        => (Value loc term1, Value loc term2)
-        -> Maybe (f (Value loc term1), g (Value loc term2))
+prjPair :: (f :< ValueConstructors , g :< ValueConstructors)
+        => (Value, Value)
+        -> Maybe (f Value, g Value)
 prjPair = bitraverse prjValue prjValue

 -- TODO: Parameterize Value by the set of constructors s.t. each language can have a distinct value union.

-- | A function value consisting of a list of parameters, the body of the function, and an environment of bindings captured by the body.
-data Closure location term value = Closure [Name] term (Environment location value)
+-- | A function value consisting of a list of parameter 'Name's, a 'Label' to jump to the body of the function, and an 'Environment' of bindings captured by the body.
+data Closure value = Closure [Name] Label (Environment Precise value)
  deriving (Eq, Generic1, Ord, Show)

-instance (Eq location, Eq term) => Eq1 (Closure location term) where liftEq = genericLiftEq
-instance (Ord location, Ord term) => Ord1 (Closure location term) where liftCompare = genericLiftCompare
-instance (Show location, Show term) => Show1 (Closure location term) where liftShowsPrec = genericLiftShowsPrec
+instance Eq1 Closure where liftEq = genericLiftEq
+instance Ord1 Closure where liftCompare = genericLiftCompare
+instance Show1 Closure where liftShowsPrec = genericLiftShowsPrec

 -- | The unit value. Typically used to represent the result of imperative statements.
 data Unit value = Unit
@ -111,10 +112,9 @@ instance Eq1 Float where liftEq = genericLiftEq
 instance Ord1 Float where liftCompare = genericLiftCompare
 instance Show1 Float where liftShowsPrec = genericLiftShowsPrec

-- Zero or more values.
+-- | Zero or more values. Fixed-size at interpretation time.
 --   TODO: Investigate whether we should use Vector for this.
 --   TODO: Should we have a Some type over a nonemmpty list? Or does this merit one?
-
 newtype Tuple value = Tuple [value]
  deriving (Eq, Generic1, Ord, Show)

@ -122,11 +122,20 @@ instance Eq1 Tuple where liftEq = genericLiftEq
 instance Ord1 Tuple where liftCompare = genericLiftCompare
 instance Show1 Tuple where liftShowsPrec = genericLiftShowsPrec

+-- | Zero or more values. Dynamically resized as needed at interpretation time.
+--   TODO: Vector? Seq?
+newtype Array value = Array [value]
+  deriving (Eq, Generic1, Ord, Show)
+
+instance Eq1 Array where liftEq = genericLiftEq
+instance Ord1 Array where liftCompare = genericLiftCompare
+instance Show1 Array where liftShowsPrec = genericLiftShowsPrec
+
 -- | The environment for an abstract value type.
 type EnvironmentFor v = Environment (LocationFor v) v

-- | The store for an abstract value type.
-type StoreFor v = Store (LocationFor v) v
+-- | The 'Heap' for an abstract value type.
+type HeapFor value = Heap (LocationFor value) value

 -- | The cell for an abstract value type.
 type CellFor value = Cell (LocationFor value) value
@ -135,18 +144,18 @@ type CellFor value = Cell (LocationFor value) value
 type LiveFor value = Live (LocationFor value) value

 -- | The location type (the body of 'Address'es) which should be used for an abstract value type.
-type family LocationFor value :: * where
-  LocationFor (Value location term) = location
-  LocationFor Type.Type = Monovariant
+type family LocationFor value :: *
+type instance LocationFor Value = Precise
+type instance LocationFor Type.Type = Monovariant

 -- | Value types, e.g. closures, which can root a set of addresses.
 class ValueRoots value where
  -- | Compute the set of addresses rooted by a given value.
  valueRoots :: value -> LiveFor value

-instance Ord location => ValueRoots (Value location term) where
+instance ValueRoots Value where
  valueRoots v
-    | Just (Closure _ body env) <- prjValue v = envAll env `const` (body :: term)
+    | Just (Closure _ _ env) <- prjValue v = envAll env
    | otherwise                            = mempty

 instance ValueRoots Type.Type where
--- a/src/Data/Syntax.hs
+++ b/src/Data/Syntax.hs
@ -2,7 +2,6 @@
 module Data.Syntax where

 import Control.Monad.Fail
-import Data.Abstract.Environment
 import Data.Abstract.Evaluatable
 import Data.AST
 import Data.Range
@ -108,9 +107,7 @@ instance Ord1 Identifier where liftCompare = genericLiftCompare
 instance Show1 Identifier where liftShowsPrec = genericLiftShowsPrec

 instance Evaluatable Identifier where
-  eval (Identifier name) = do
-    env <- askLocalEnv
-    maybe (fail ("free variable: " <> show name)) deref (envLookup name env)
+  eval (Identifier name) = lookupWith deref name >>= maybe (fail ("free variable: " <> show name)) pure

 instance FreeVariables1 Identifier where
  liftFreeVariables _ (Identifier x) = Set.singleton x
--- a/src/Data/Syntax/Literal.hs
+++ b/src/Data/Syntax/Literal.hs
@ -205,9 +205,8 @@ instance Eq1 Array where liftEq = genericLiftEq
 instance Ord1 Array where liftCompare = genericLiftCompare
 instance Show1 Array where liftShowsPrec = genericLiftShowsPrec

-- TODO: Implement Eval instance for Array
-instance Evaluatable Array
-
+instance Evaluatable Array where
+  eval (Array a) = array =<< traverse subtermValue a

 newtype Hash a = Hash { hashElements :: [a] }
  deriving (Diffable, Eq, Foldable, Functor, GAlign, Generic1, Mergeable, Ord, Show, Traversable, FreeVariables1)
--- a/src/Data/Syntax/Statement.hs
+++ b/src/Data/Syntax/Statement.hs
@ -94,10 +94,11 @@ instance Show1 Assignment where liftShowsPrec = genericLiftShowsPrec
 instance Evaluatable Assignment where
  eval Assignment{..} = do
    v <- subtermValue assignmentValue
-    (var, a) <- askLocalEnv >>= lookupOrAlloc (subterm assignmentTarget) v
-
-    modifyGlobalEnv (envInsert var a)
+    addr <- lookupOrAlloc name
+    assign addr v
+    modifyGlobalEnv (envInsert name addr)
    pure v
+    where name = freeVariable (subterm assignmentTarget)

 -- | Post increment operator (e.g. 1++ in Go, or i++ in C).
 newtype PostIncrement a = PostIncrement a
--- a/src/Language/Go/Syntax.hs
+++ b/src/Language/Go/Syntax.hs
@ -1,9 +1,9 @@
 {-# LANGUAGE DeriveAnyClass #-}
 module Language.Go.Syntax where

-import Prologue
-import Data.Abstract.Evaluatable
+import Data.Abstract.Evaluatable hiding (Label)
 import Diffing.Algorithm
+import Prologue

 -- A composite literal in Go
 data Composite a = Composite { compositeType :: !a, compositeElement :: !a }
--- a/src/Prologue.hs
+++ b/src/Prologue.hs
@ -1,7 +1,8 @@
 {-# LANGUAGE UndecidableInstances #-}
-module Prologue (
-  module X
-, ) where
+module Prologue
+( module X
+, foldMapA
+) where


 import Data.Bifunctor.Join as X
@ -11,6 +12,7 @@ import Data.IntMap as X (IntMap)
 import Data.IntSet as X (IntSet)
 import Data.Ix as X (Ix(..))
 import Data.Map as X (Map)
+import Data.Monoid (Alt(..))
 import Data.Maybe as X
 import Data.Sequence as X (Seq)
 import Data.Set as X (Set)
@ -67,3 +69,7 @@ import Data.Hashable as X (
 -- Generics
 import GHC.Generics as X hiding (moduleName)
 import GHC.Stack as X
+
+-- | Fold a collection by mapping each element onto an 'Alternative' action.
+foldMapA :: (Alternative m, Foldable t) => (b -> m a) -> t b -> m a
+foldMapA f = getAlt . foldMap (Alt . f)
--- a/src/Semantic/Util.hs
+++ b/src/Semantic/Util.hs
@ -14,7 +14,6 @@ import Data.Abstract.Evaluatable
 import Data.Abstract.Address
 import Data.Abstract.Type
 import Data.Abstract.Value
-import Data.AST
 import Data.Blob
 import Data.Diff
 import Data.Range
@ -31,66 +30,58 @@ import Semantic.Task

 import qualified Language.Go.Assignment as Go
 import qualified Language.Python.Assignment as Python
-import qualified Language.Ruby.Assignment as Ruby
 import qualified Language.TypeScript.Assignment as TypeScript

-type PreciseValue a = Value Precise (Term (Union a) (Record Location))
-
-type GoValue         = PreciseValue Go.Syntax
-type RubyValue       = PreciseValue Ruby.Syntax
-type PythonValue     = PreciseValue Python.Syntax
-type TypeScriptValue = PreciseValue TypeScript.Syntax
-
 -- Ruby
-evaluateRubyFile = evaluateFile @RubyValue rubyParser
-evaluateRubyFiles = evaluateFiles @RubyValue rubyParser
+evaluateRubyFile = evaluateFile rubyParser
+evaluateRubyFiles = evaluateFiles rubyParser

 -- Go
-evaluateGoFile = evaluateFile @GoValue goParser
-evaluateGoFiles = evaluateFiles @GoValue goParser
+evaluateGoFile = evaluateFile goParser
+evaluateGoFiles = evaluateFiles goParser
 typecheckGoFile path = runAnalysis @(Caching Evaluating Go.Term Type) . evaluateModule . snd <$> parseFile goParser path

 -- Python
-evaluatePythonFile path = evaluate @PythonValue . snd <$> parseFile pythonParser path
-evaluatePythonFiles = evaluateFiles @PythonValue pythonParser
+evaluatePythonFile path = evaluate . snd <$> parseFile pythonParser path
+evaluatePythonFiles = evaluateFiles pythonParser
 typecheckPythonFile path = runAnalysis @(Caching Evaluating Python.Term Type) . evaluateModule . snd <$> parseFile pythonParser path
-tracePythonFile path = runAnalysis @(Tracing [] Evaluating Python.Term PythonValue) . evaluateModule . snd <$> parseFile pythonParser path
-evaluateDeadTracePythonFile path = runAnalysis @(DeadCode (Tracing [] Evaluating) Python.Term PythonValue) . evaluateModule . snd <$> parseFile pythonParser path
+tracePythonFile path = runAnalysis @(Tracing [] Evaluating Python.Term Value) . evaluateModule . snd <$> parseFile pythonParser path
+evaluateDeadTracePythonFile path = runAnalysis @(DeadCode (Tracing [] Evaluating) Python.Term Value) . evaluateModule . snd <$> parseFile pythonParser path

 -- TypeScript
 typecheckTypeScriptFile path = runAnalysis @(Caching Evaluating TypeScript.Term Type) . evaluateModule . snd <$> parseFile typescriptParser path
-evaluateTypeScriptFile = evaluateFile @TypeScriptValue typescriptParser
-evaluateTypeScriptFiles = evaluateFiles @TypeScriptValue typescriptParser
+evaluateTypeScriptFile = evaluateFile typescriptParser
+evaluateTypeScriptFiles = evaluateFiles typescriptParser

 -- Evalute a single file.
-evaluateFile :: forall value term effects
+evaluateFile :: forall term effects
             .  ( Evaluatable (Base term)
                , FreeVariables term
-                , effects ~ RequiredEffects term value (Evaluating term value effects)
-                , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-                , MonadValue term value (Evaluating term value effects)
+                , effects ~ RequiredEffects term Value (Evaluating term Value effects)
+                , MonadAddressable Precise Value (Evaluating term Value effects)
+                , MonadValue Value (Evaluating term Value effects)
                , Recursive term
                )
             => Parser term
             -> FilePath
-             -> IO (Final effects value)
-evaluateFile parser path = runAnalysis @(Evaluating term value) . evaluateModule . snd <$> parseFile parser path
+             -> IO (Final effects Value)
+evaluateFile parser path = evaluate . snd <$> parseFile parser path

 -- Evaluate a list of files (head of file list is considered the entry point).
-evaluateFiles :: forall value term effects
+evaluateFiles :: forall term effects
              .  ( Evaluatable (Base term)
                 , FreeVariables term
-                 , effects ~ RequiredEffects term value (Evaluating term value effects)
-                 , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-                 , MonadValue term value (Evaluating term value effects)
+                 , effects ~ RequiredEffects term Value (Evaluating term Value effects)
+                 , MonadAddressable Precise Value (Evaluating term Value effects)
+                 , MonadValue Value (Evaluating term Value effects)
                 , Recursive term
                 )
              => Parser term
              -> [FilePath]
-              -> IO (Final effects value)
+              -> IO (Final effects Value)
 evaluateFiles parser paths = do
  entry:xs <- traverse (parseFile parser) paths
-  pure $ evaluates @value xs entry
+  pure $ evaluates @Value xs entry

 -- Read and parse a file.
 parseFile :: Parser term -> FilePath -> IO (Blob, term)
--- a/test/Analysis/Go/Spec.hs
+++ b/test/Analysis/Go/Spec.hs
@ -33,8 +33,8 @@ spec = parallel $ do
  where
    addr = Address . Precise
    fixtures = "test/fixtures/go/analysis/"
-    evaluate entry = snd . fst . fst . fst <$>
-      evaluateFiles @GoValue goParser
+    evaluate entry = snd . fst . fst . fst . fst <$>
+      evaluateFiles goParser
        [ fixtures <> entry
        , fixtures <> "foo/foo.go"
        , fixtures <> "bar/bar.go"
--- a/test/Analysis/Python/Spec.hs
+++ b/test/Analysis/Python/Spec.hs
@ -37,8 +37,8 @@ spec = parallel $ do
  where
    addr = Address . Precise
    fixtures = "test/fixtures/python/analysis/"
-    evaluate entry = snd . fst . fst . fst <$>
-      evaluateFiles @PythonValue pythonParser
+    evaluate entry = snd . fst . fst . fst . fst <$>
+      evaluateFiles pythonParser
      [ fixtures <> entry
      , fixtures <> "a.py"
      , fixtures <> "b/c.py"
--- a/test/Analysis/TypeScript/Spec.hs
+++ b/test/Analysis/TypeScript/Spec.hs
@ -34,8 +34,8 @@ spec = parallel $ do
  where
    addr = Address . Precise
    fixtures = "test/fixtures/typescript/analysis/"
-    evaluate entry = snd . fst . fst . fst <$>
-      evaluateFiles @TypeScriptValue typescriptParser
+    evaluate entry = snd . fst . fst . fst . fst <$>
+      evaluateFiles typescriptParser
        [ fixtures <> entry
        , fixtures <> "a.ts"
        , fixtures <> "foo.ts"
--- a/test/SpecHelpers.hs
+++ b/test/SpecHelpers.hs
@ -12,8 +12,8 @@ module SpecHelpers (
 import Data.Abstract.Address as X
 import Data.Abstract.Environment as X
 import Data.Abstract.FreeVariables as X
+import Data.Abstract.Heap as X
 import Data.Abstract.ModuleTable as X
-import Data.Abstract.Store as X
 import Data.Blob as X
 import Data.Functor.Listable as X
 import Data.Language as X