From c3d01b66025d098ae95c40c0c46fa75a172c2378 Mon Sep 17 00:00:00 2001 From: Patrick Thomson Date: Tue, 6 Mar 2018 11:21:04 -0500 Subject: [PATCH] Resuscitate the caching evaluator. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The caching analysis had been disabled, as it was still written in the open-interpreter style. This patch restores it, defining a `CachingAnalysis` newtype that uses nondeterministic but convergent caching in its `MonadAnalysis` instance. This also defines an `embedSubterm` helper that is useful in defining new analysis passes. Thanks to @robrix for 🍐! --- semantic.cabal | 8 +- src/Analysis/Abstract/Caching.hs | 233 +++++++++++++++++----------- src/Analysis/Abstract/Collecting.hs | 3 +- src/Analysis/Abstract/Dead.hs | 2 +- src/Control/Abstract/Evaluator.hs | 5 +- src/Data/Algebra.hs | 9 +- src/Semantic/Util.hs | 6 +- 7 files changed, 167 insertions(+), 99 deletions(-) diff --git a/semantic.cabal b/semantic.cabal index 4f63a5871..7cf2314e3 100644 --- a/semantic.cabal +++ b/semantic.cabal @@ -15,9 +15,9 @@ library hs-source-dirs: src exposed-modules: -- Analyses & term annotations - -- Analysis.Abstract.Caching + Analysis.Abstract.Caching -- , Analysis.Abstract.Collecting - Analysis.Abstract.Dead + , Analysis.Abstract.Dead , Analysis.Abstract.Evaluating -- , Analysis.Abstract.Tracing , Analysis.ConstructorName @@ -37,10 +37,10 @@ library -- Control flow , Control.Effect -- Effects used for program analysis - -- , Control.Monad.Effect.Cache + , Control.Monad.Effect.Cache , Control.Monad.Effect.Fresh -- , Control.Monad.Effect.GC - -- , Control.Monad.Effect.NonDet + , Control.Monad.Effect.NonDet -- , Control.Monad.Effect.Trace -- Datatypes for abstract interpretation , Data.Abstract.Address diff --git a/src/Analysis/Abstract/Caching.hs b/src/Analysis/Abstract/Caching.hs index caed10ff0..6c09e0add 100644 --- a/src/Analysis/Abstract/Caching.hs +++ b/src/Analysis/Abstract/Caching.hs @@ -1,16 +1,14 @@ -{-# LANGUAGE ConstraintKinds, DataKinds, ScopedTypeVariables, TypeApplications #-} -module Analysis.Abstract.Caching where +{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, UndecidableInstances #-} +module Analysis.Abstract.Caching + ( evaluateCache ) + where import Prologue import Data.Monoid (Alt(..)) -import Analysis.Abstract.Collecting +import Control.Abstract.Evaluator import Control.Effect -import Control.Monad.Effect.Addressable -import Control.Monad.Effect.Cache -import Control.Monad.Effect.Env import Control.Monad.Effect.Fail import Control.Monad.Effect.Fresh -import Control.Monad.Effect.Internal hiding (run) import Control.Monad.Effect.NonDet import Control.Monad.Effect.Reader import Control.Monad.Effect.State @@ -18,108 +16,107 @@ import Data.Abstract.Address import Data.Abstract.Cache import Data.Abstract.Configuration import Data.Abstract.Environment -import Data.Abstract.Eval +import Data.Abstract.Evaluatable +import Data.Abstract.Linker import Data.Abstract.Live import Data.Abstract.Store import Data.Abstract.Value import qualified Data.Set as Set -- | The effects necessary for caching analyses. -type Caching t v +type CachingEffects t v = '[ Fresh -- For 'MonadFresh'. , Reader (Live (LocationFor v) v) -- For 'MonadGC'. , Reader (Environment (LocationFor v) v) -- For 'MonadEnv'. + , State (Environment (LocationFor v) v) -- For 'MonadEvaluator'. , Fail -- For 'MonadFail'. , NonDetEff -- For 'Alternative' & 'MonadNonDet'. , State (Store (LocationFor v) v) -- For 'MonadStore'. , Reader (Cache (LocationFor v) t v) -- For 'MonadCacheIn'. , State (Cache (LocationFor v) t v) -- For 'MonadCacheOut'. + , Reader (Linker t) -- Cache of unevaluated modules + , State (Linker v) -- Cache of evaluated modules ] --- | A constraint synonym for the interfaces necessary for caching analyses. -type MonadCaching t v m - = ( MonadEnv v m - , MonadStore v m - , MonadCacheIn t v m - , MonadCacheOut t v m - , MonadGC v m - , Alternative m - ) +newtype CachingAnalysis term value a = CachingAnalysis { runCachingAnalysis :: Evaluator (CachingEffects term value) term value a } + deriving (Alternative, Applicative, Functor, Monad, MonadFail, MonadFresh, MonadNonDet) + +deriving instance MonadEvaluator term value (CachingAnalysis term value) + +-- TODO: reabstract these later on + +askCache :: CachingAnalysis t v (Cache (LocationFor v) t v) +askCache = CachingAnalysis (Evaluator ask) + +localCache :: (Cache (LocationFor v) t v -> Cache (LocationFor v) t v) -> CachingAnalysis t v a -> CachingAnalysis t v a +localCache f (CachingAnalysis (Evaluator a)) = CachingAnalysis (Evaluator (local f a)) + +asksCache :: (Cache (LocationFor v) t v -> a) -> CachingAnalysis t v a +asksCache f = f <$> askCache + +getsCache :: (Cache (LocationFor v) t v -> a) -> CachingAnalysis t v a +getsCache f = f <$> getCache + +getCache :: CachingAnalysis t v (Cache (LocationFor v) t v) +getCache = CachingAnalysis (Evaluator get) + +putCache :: Cache (LocationFor v) t v -> CachingAnalysis t v () +putCache v = CachingAnalysis (Evaluator (put v)) + +modifyCache :: (Cache (LocationFor v) t v -> Cache (LocationFor v) t v) -> CachingAnalysis t v () +modifyCache f = fmap f getCache >>= putCache + +-- | This instance coinductively iterates the analysis of a term until the results converge. +instance ( Corecursive t + , Ord t + , Ord v + , Ord (Cell (LocationFor v) v) + , Evaluatable (Base t) + , Foldable (Cell (LocationFor v)) + , FreeVariables t + , MonadAddressable (LocationFor v) v (CachingAnalysis t v) + , MonadValue t v (CachingAnalysis t v) + , Recursive t + , Semigroup (Cell (LocationFor v) v) + ) + => MonadAnalysis t v (CachingAnalysis t v) where + evaluateTerm = foldSubterms $ \e -> do + c <- getConfiguration (embedSubterm e) + -- Convergence here is predicated upon an Eq instance, not α-equivalence + cache <- converge (\ prevCache -> do + putCache (mempty :: Cache (LocationFor v) t v) + putStore (configurationStore 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 + -- to corral all the nondeterminism that happens in this @eval@ invocation, so + -- that it doesn't "leak" to the calling context and diverge + -- (otherwise this would never complete). + _ <- localCache (const prevCache) (gather Set.singleton (memoizeEval e)) + getCache) mempty + maybe empty scatter (cacheLookup c cache) -- | Coinductively-cached evaluation. -evalCache :: forall v term - . ( Ord v - , Ord term - , Ord (LocationFor v) - , Ord (Cell (LocationFor v) v) - , Foldable (Cell (LocationFor v)) - , Functor (Base term) - , Recursive term - , Addressable (LocationFor v) (Eff (Caching term v)) - , Semigroup (Cell (LocationFor v) v) - , ValueRoots (LocationFor v) v - , Eval term v (Eff (Caching term v)) (Base term) - ) - => term - -> Final (Caching term v) v -evalCache e = run @(Caching term v) (fixCache (fix (evCache (evCollect (\ recur yield -> eval recur yield . project)))) pure e) - - --- | Evaluation of a single iteration of an analysis, given a 'MonadCacheIn' instance as an oracle for results and a 'MonadCacheOut' instance to record computed results in. -evCache :: forall t v m - . ( Ord (LocationFor v) - , Ord t - , Ord v - , Ord (Cell (LocationFor v) v) - , MonadCaching t v m - ) - => (((v -> m v) -> t -> m v) -> (v -> m v) -> t -> m v) - -> ((v -> m v) -> t -> m v) - -> (v -> m v) -> t -> m v -evCache ev0 ev' yield e = do - c <- getConfiguration e - cached <- getsCache (cacheLookup c) - case cached of - Just pairs -> scatter pairs - Nothing -> do - pairs <- asksCache (fromMaybe mempty . cacheLookup c) - modifyCache (cacheSet c pairs) - v <- ev0 ev' yield e - store' <- getStore - modifyCache (cacheInsert c (v, store')) - pure v - --- | Coinductively iterate the analysis of a term until the results converge. -fixCache :: forall t v m - . ( Ord (LocationFor v) - , Ord t - , Ord v - , Ord (Cell (LocationFor v) v) - , MonadCaching t v m - , MonadNonDet m - , MonadFresh m - ) - => ((v -> m v) -> t -> m v) - -> (v -> m v) -> t -> m v -fixCache ev' yield e = do - c <- getConfiguration e - cache <- converge (\ prevCache -> do - putCache (mempty :: Cache (LocationFor v) t v) - putStore (configurationStore c) - reset 0 - _ <- localCache (const prevCache) (gather Set.singleton (ev' yield e)) - getCache) mempty - maybe empty scatter (cacheLookup c cache) - --- | Get the current 'Configuration' with a passed-in term. -getConfiguration :: (MonadEnv v m, MonadGC v m, MonadStore v m) => t -> m (Configuration (LocationFor v) t v) -getConfiguration term = Configuration term <$> askRoots <*> askEnv <*> getStore - - --- | Nondeterministically write each of a collection of stores & return their associated results. -scatter :: (Alternative m, Foldable t, MonadStore a m) => t (a, Store (LocationFor a) a) -> m a -scatter = getAlt . foldMap (\ (value, store') -> Alt (putStore store' *> pure value)) +evaluateCache :: forall v term + . ( Ord v + , Ord term + , Ord (LocationFor v) + , Ord (Cell (LocationFor v) v) + , Corecursive term + , Evaluatable (Base term) + , FreeVariables term + , Foldable (Cell (LocationFor v)) + , Functor (Base term) + , Recursive term + , MonadAddressable (LocationFor v) v (CachingAnalysis term v) + , MonadValue term v (CachingAnalysis term v) + , Semigroup (Cell (LocationFor v) v) + , ValueRoots (LocationFor v) v + ) + => term + -> Final (CachingEffects term v) v +evaluateCache = run @(CachingEffects term v) . runEvaluator . runCachingAnalysis . evaluateTerm -- | Iterate a monadic action starting from some initial seed until the results converge. -- @@ -135,3 +132,59 @@ converge f = loop pure x else loop x' + +-- | Get the current 'Configuration' with a passed-in term. +getConfiguration :: Ord (LocationFor v) => t -> CachingAnalysis t v (Configuration (LocationFor v) t v) +getConfiguration term = Configuration term mempty <$> askLocalEnv <*> getStore + +-- | Nondeterministically write each of a collection of stores & return their associated results. +scatter :: (Alternative m, Foldable t, MonadEvaluator term v m) => t (a, Store (LocationFor v) v) -> m a +scatter = getAlt . foldMap (\ (value, store') -> Alt (putStore store' *> pure value)) + +-- | Evaluation of a single iteration of an analysis, given a 'MonadCacheIn' instance as an oracle for results and a 'MonadCacheOut' instance to record computed results in. +memoizeEval :: forall v term + . ( Ord v + , Ord term + , Ord (LocationFor v) + , Ord (Cell (LocationFor v) v) + , Corecursive term + , Evaluatable (Base term) + , FreeVariables term + , Foldable (Cell (LocationFor v)) + , Functor (Base term) + , Recursive term + , MonadAddressable (LocationFor v) v (CachingAnalysis term v) + , MonadValue term v (CachingAnalysis term v) + , Semigroup (Cell (LocationFor v) v) + ) + => SubtermAlgebra (Base term) term (CachingAnalysis term v v) +memoizeEval e = do + c <- getConfiguration (embedSubterm e) + cached <- getsCache (cacheLookup c) + case cached of + Just pairs -> scatter pairs + Nothing -> do + pairs <- asksCache (fromMaybe mempty . cacheLookup c) + modifyCache (cacheSet c pairs) + v <- eval e + store' <- getStore + modifyCache (cacheInsert c (v, store')) + pure v + +{- + + +-- | Evaluation of a single iteration of an analysis, given a 'MonadCacheIn' instance as an oracle for results and a 'MonadCacheOut' instance to record computed results in. +evCache :: forall t v m + . ( Ord (LocationFor v) + , Ord t + , Ord v + , Ord (Cell (LocationFor v) v) + , MonadCaching t v m + ) + => (((v -> m v) -> t -> m v) -> (v -> m v) -> t -> m v) + -> ((v -> m v) -> t -> m v) + -> (v -> m v) -> t -> m v + + +-} diff --git a/src/Analysis/Abstract/Collecting.hs b/src/Analysis/Abstract/Collecting.hs index 3544dc02b..b265d5ff7 100644 --- a/src/Analysis/Abstract/Collecting.hs +++ b/src/Analysis/Abstract/Collecting.hs @@ -2,6 +2,7 @@ module Analysis.Abstract.Collecting where import Prologue +import Control.Abstract.Evaluator import Control.Monad.Effect.GC import Data.Abstract.Address import Data.Abstract.Live @@ -12,7 +13,7 @@ import Data.Abstract.Value evCollect :: forall t v m . ( Ord (LocationFor v) , Foldable (Cell (LocationFor v)) - , MonadStore v m + , MonadEvaluator t v m , MonadGC v m , ValueRoots (LocationFor v) v ) diff --git a/src/Analysis/Abstract/Dead.hs b/src/Analysis/Abstract/Dead.hs index c5e8c387f..b9889b91a 100644 --- a/src/Analysis/Abstract/Dead.hs +++ b/src/Analysis/Abstract/Dead.hs @@ -80,5 +80,5 @@ instance ( Corecursive t ) => MonadAnalysis t v (DeadCodeAnalysis t v) where evaluateTerm = foldSubterms (\ term -> do - revive (embed (subterm <$> term)) + revive (embedSubterm term) eval term) diff --git a/src/Control/Abstract/Evaluator.hs b/src/Control/Abstract/Evaluator.hs index 5ed3ae46f..8c056bfd4 100644 --- a/src/Control/Abstract/Evaluator.hs +++ b/src/Control/Abstract/Evaluator.hs @@ -5,7 +5,7 @@ import Control.Applicative import Control.Monad.Effect import Control.Monad.Effect.Fail import Control.Monad.Effect.Fresh -import Control.Monad.Effect.NonDetEff +import Control.Monad.Effect.NonDet import Control.Monad.Effect.Reader import Control.Monad.Effect.State import Data.Abstract.Linker @@ -67,6 +67,8 @@ instance Members '[ Fail askModuleTable = Evaluator ask localModuleTable f a = Evaluator (local f (runEvaluator a)) +putStore :: MonadEvaluator t value m => StoreFor value -> m () +putStore = modifyStore . const -- | An evaluator of @term@s to @value@s, producing incremental results of type @a@ using a list of @effects@. newtype Evaluator effects term value a = Evaluator { runEvaluator :: Eff effects a } @@ -74,4 +76,5 @@ newtype Evaluator effects term value a = Evaluator { runEvaluator :: Eff effects deriving instance Member Fail effects => MonadFail (Evaluator effects term value) deriving instance Member NonDetEff effects => Alternative (Evaluator effects term value) +deriving instance Member NonDetEff effects => MonadNonDet (Evaluator effects term value) deriving instance Member Fresh effects => MonadFresh (Evaluator effects term value) diff --git a/src/Data/Algebra.hs b/src/Data/Algebra.hs index 955ce1c2f..28c0ee134 100644 --- a/src/Data/Algebra.hs +++ b/src/Data/Algebra.hs @@ -6,6 +6,7 @@ module Data.Algebra , OpenRAlgebra , Subterm(..) , SubtermAlgebra +, embedSubterm , foldSubterms , fToR , fToOpenR @@ -13,7 +14,10 @@ module Data.Algebra , openFToOpenR ) where -import Data.Functor.Foldable (Base, Recursive(project)) +import Data.Functor.Foldable ( Base + , Corecursive(embed) + , Recursive(project) + ) -- | An F-algebra on some 'Recursive' type @t@. -- @@ -51,6 +55,9 @@ type SubtermAlgebra f t a = f (Subterm t a) -> a foldSubterms :: Recursive t => SubtermAlgebra (Base t) t a -> t -> a foldSubterms algebra = go where go = algebra . fmap (Subterm <*> go) . project +-- | Extract a term from said term's 'Base' functor populated with 'Subterm' fields. +embedSubterm :: Corecursive t => Base t (Subterm t a) -> t +embedSubterm e = embed (subterm <$> e) -- | Promote an 'FAlgebra' into an 'RAlgebra' (by dropping the original parameter). fToR :: Functor (Base t) => FAlgebra (Base t) a -> RAlgebra (Base t) t a diff --git a/src/Semantic/Util.hs b/src/Semantic/Util.hs index aae481164..1e7c249fa 100644 --- a/src/Semantic/Util.hs +++ b/src/Semantic/Util.hs @@ -3,10 +3,12 @@ module Semantic.Util where import Prologue +import Analysis.Abstract.Caching import Analysis.Abstract.Evaluating import Analysis.Declaration import Control.Monad.IO.Class import Data.Abstract.Address +import Data.Abstract.Type import Data.Abstract.Value import Data.AST import Data.Blob @@ -40,8 +42,10 @@ evaluateRubyFiles paths = do (t:ts) <- runTask $ traverse (parse rubyParser) blobs pure $ evaluates @RubyValue (zip bs ts) (b, t) - -- Python +typecheckPythonFile path = evaluateCache @Type <$> + (file path >>= runTask . parse pythonParser) + evaluatePythonFile path = evaluate @PythonValue <$> (file path >>= runTask . parse pythonParser)