From b5485e8ab882d5b8fefe7c0628970376652c4b21 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 4 May 2018 19:24:07 -0400 Subject: [PATCH] Rephrase Caching as cachingTerms, convergingModules, and caching handlers. --- src/Analysis/Abstract/Caching.hs | 155 ++++++++++++++----------------- 1 file changed, 68 insertions(+), 87 deletions(-) diff --git a/src/Analysis/Abstract/Caching.hs b/src/Analysis/Abstract/Caching.hs index 2f6b2fd40..066f54b70 100644 --- a/src/Analysis/Abstract/Caching.hs +++ b/src/Analysis/Abstract/Caching.hs @@ -1,12 +1,12 @@ -{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-} -{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the Interpreter instance’s Evaluator constraint +{-# LANGUAGE GADTs, TypeOperators #-} module Analysis.Abstract.Caching -( Caching +( cachingTerms +, convergingModules +, caching ) where -import Control.Abstract.Analysis +import Control.Abstract.Evaluator import Control.Monad.Effect hiding (interpret) -import Data.Abstract.Address import Data.Abstract.Cache import Data.Abstract.Configuration import Data.Abstract.Live @@ -14,92 +14,84 @@ import Data.Abstract.Module import Data.Semilattice.Lower import Prologue --- | A (coinductively-)cached analysis suitable for guaranteeing termination of (suitably finitized) analyses over recursive programs. -newtype Caching m (effects :: [* -> *]) a = Caching { runCaching :: m effects a } - deriving (Alternative, Applicative, Functor, Effectful, Monad) - -deriving instance Evaluator location term value m => Evaluator location term value (Caching m) - -- | Look up the set of values for a given configuration in the in-cache. -consultOracle :: (Cacheable location term value, Effectful m, Member (Reader (Cache location term value)) effects) => Configuration location term value -> m effects (Set (value, Heap location value)) +consultOracle :: (Cacheable location term value, Member (Reader (Cache location term value)) effects) => Configuration location term value -> Evaluator location term value effects (Set (value, Heap location value)) consultOracle configuration = raise (fromMaybe mempty . cacheLookup configuration <$> ask) -- | Run an action with the given in-cache. -withOracle :: (Effectful m, Member (Reader (Cache location term value)) effects) => Cache location term value -> m effects a -> m effects a +withOracle :: Member (Reader (Cache location term value)) effects => Cache location term value -> Evaluator location term value effects a -> Evaluator location term value effects a withOracle cache = raiseHandler (local (const cache)) -- | Look up the set of values for a given configuration in the out-cache. -lookupCache :: (Cacheable location term value, Effectful m, Member (State (Cache location term value)) effects) => Configuration location term value -> m effects (Maybe (Set (value, Heap location value))) +lookupCache :: (Cacheable location term value, Member (State (Cache location term value)) effects) => Configuration location term value -> Evaluator location term value effects (Maybe (Set (value, Heap location value))) lookupCache configuration = raise (cacheLookup configuration <$> get) -- | Run an action, caching its result and 'Heap' under the given configuration. -caching :: (Cacheable location term value, Effectful m, Member (State (Cache location term value)) effects, Member (State (Heap location value)) effects, Monad (m effects)) => Configuration location term value -> Set (value, Heap location value) -> m effects value -> m effects value -caching configuration values action = do +cachingConfiguration :: (Cacheable location term value, Member (State (Cache location term value)) effects, Member (State (Heap location value)) effects, Monad (Evaluator location term value effects)) => Configuration location term value -> Set (value, Heap location value) -> Evaluator location term value effects value -> Evaluator location term value effects value +cachingConfiguration configuration values action = do raise (modify (cacheSet configuration values)) result <- (,) <$> action <*> raise get raise (modify (cacheInsert configuration result)) pure (fst result) -putCache :: (Effectful m, Member (State (Cache location term value)) effects) => Cache location term value -> m effects () +putCache :: (Member (State (Cache location term value)) effects) => Cache location term value -> Evaluator location term value effects () putCache = raise . put -- | Run an action starting from an empty out-cache, and return the out-cache afterwards. -isolateCache :: forall location term value m effects a . (Applicative (m effects), Effectful m, Member (State (Cache location term value)) effects) => m effects a -> m effects (Cache location term value) -isolateCache action = putCache @m @location @term @value lowerBound *> action *> raise get +isolateCache :: Member (State (Cache location term value)) effects => Evaluator location term value effects a -> Evaluator location term value effects (Cache location term value) +isolateCache action = putCache lowerBound *> action *> raise get -instance ( Alternative (m outer) - , AnalyzeTerm location term value inner outer m - , Cacheable location term value - , Corecursive term - , Effectful m - , Member Fresh outer - , Member NonDet outer - , Member (Reader (Cache location term value)) outer - , Member (Reader (Live location value)) outer - , Member (State (Cache location term value)) outer - , Member (State (Environment location value)) outer - , Member (State (Heap location value)) outer - ) - => AnalyzeTerm location term value inner outer (Caching m) where - -- Analyze a term using the in-cache as an oracle & storing the results of the analysis in the out-cache. - analyzeTerm recur e = do - c <- getConfiguration (embedSubterm e) - cached <- lookupCache c - case cached of - Just pairs -> scatter pairs - Nothing -> do - pairs <- consultOracle c - caching c pairs (Caching (analyzeTerm (runCaching . recur) e)) -instance ( Alternative (m outer) - , AnalyzeModule location term value inner outer m - , Cacheable location term value - , Corecursive term - , Effectful m - , Member Fresh outer - , Member NonDet outer - , Member (Reader (Cache location term value)) outer - , Member (Reader (Live location value)) outer - , Member (State (Cache location term value)) outer - , Member (State (Environment location value)) outer - , Member (State (Heap location value)) outer - ) - => AnalyzeModule location term value inner outer (Caching m) where - analyzeModule recur m = do - c <- getConfiguration (subterm (moduleBody m)) - -- Convergence here is predicated upon an Eq instance, not α-equivalence - cache <- converge (\ prevCache -> isolateCache $ do - 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 - -- to corral all the nondeterminism that happens in this @eval@ invocation, so - -- that it doesn't "leak" to the calling context and diverge (otherwise this - -- would never complete). We don’t need to use the values, so we 'gather' the - -- nondeterministic values into @()@. - withOracle prevCache (raiseHandler (gather (const ())) (Caching (analyzeModule (runCaching . recur) m)))) mempty - maybe empty scatter (cacheLookup c cache) +-- | Analyze a term using the in-cache as an oracle & storing the results of the analysis in the out-cache. +cachingTerms :: ( Cacheable location term value + , Corecursive term + , Members '[ Fresh + , NonDet + , Reader (Cache location term value) + , Reader (Live location value) + , State (Cache location term value) + , State (Environment location value) + , State (Heap location value) + ] effects + ) + => SubtermAlgebra (Base term) term (Evaluator location term value effects value) + -> SubtermAlgebra (Base term) term (Evaluator location term value effects value) +cachingTerms recur term = do + c <- getConfiguration (embedSubterm term) + cached <- lookupCache c + case cached of + Just pairs -> scatter pairs + Nothing -> do + pairs <- consultOracle c + cachingConfiguration c pairs (recur term) + +convergingModules :: ( Cacheable location term value + , Members '[ Fresh + , NonDet + , Reader (Cache location term value) + , Reader (Live location value) + , State (Cache location term value) + , State (Environment location value) + , State (Heap location value) + ] effects + ) + => SubtermAlgebra Module term (Evaluator location term value effects value) + -> SubtermAlgebra Module term (Evaluator location term value effects value) +convergingModules recur m = do + c <- getConfiguration (subterm (moduleBody m)) + -- Convergence here is predicated upon an Eq instance, not α-equivalence + cache <- converge (\ prevCache -> isolateCache $ do + 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 + -- to corral all the nondeterminism that happens in this @eval@ invocation, so + -- that it doesn't "leak" to the calling context and diverge (otherwise this + -- would never complete). We don’t need to use the values, so we 'gather' the + -- nondeterministic values into @()@. + withOracle prevCache (raiseHandler (gather (const ())) (recur m))) lowerBound + maybe empty scatter (cacheLookup c cache) reset :: (Effectful m, Member Fresh effects) => Int -> m effects a -> m effects a @@ -121,23 +113,12 @@ converge f = loop loop x' -- | Nondeterministically write each of a collection of stores & return their associated results. -scatter :: (Alternative (m effects), Evaluator location term value m, Foldable t, Member (State (Heap location value)) effects) => t (a, Heap location value) -> m effects a +scatter :: (Foldable t, Members '[NonDet, State (Heap location value)] effects) => t (a, Heap location value) -> Evaluator location term value effects a scatter = foldMapA (\ (value, heap') -> putHeap heap' $> value) -instance ( Interpreter m effects - , Evaluator location term value m - , Ord (Cell location value) - , Ord location - , Ord term - , Ord value - ) - => Interpreter (Caching m) (NonDet ': Reader (Cache location term value) ': State (Cache location term value) ': effects) where - type Result (Caching m) (NonDet ': Reader (Cache location term value) ': State (Cache location term value) ': effects) result = Result m effects ([result], Cache location term value) - interpret - = interpret - . runCaching - . raiseHandler - ( flip runState mempty - . flip runReader mempty - . makeChoiceA @[]) +caching :: Alternative f => Evaluator location term value (NonDet ': Reader (Cache location term value) ': State (Cache location term value) ': effects) a -> Evaluator location term value effects (f a, Cache location term value) +caching + = handleState lowerBound + . handleReader lowerBound + . raiseHandler makeChoiceA