From 66d5a1dfe8bc83203d40aa9d4603438d533bc7bb Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 26 Oct 2018 13:03:14 -0400 Subject: [PATCH] Run nondeterminism locally in flow-sensitive analysis. --- src/Analysis/Abstract/Caching/FlowSensitive.hs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/Analysis/Abstract/Caching/FlowSensitive.hs b/src/Analysis/Abstract/Caching/FlowSensitive.hs index 23120d1f9..63de56b6c 100644 --- a/src/Analysis/Abstract/Caching/FlowSensitive.hs +++ b/src/Analysis/Abstract/Caching/FlowSensitive.hs @@ -89,10 +89,13 @@ convergingModules :: ( AbstractValue term address value m , Member (Env address) sig , Member (State (Heap address value)) sig , Carrier sig m + , Effect sig ) - => Open (Module term -> Evaluator term address value m address) -convergingModules recur m = do - c <- getConfiguration (moduleBody m) + => (Module (Either prelude term) -> Evaluator term address value (AltC Maybe (Eff m)) address) + -> (Module (Either prelude term) -> Evaluator term address value m address) +convergingModules recur m@(Module _ (Left _)) = raiseHandler runNonDet (recur m) >>= maybeM empty +convergingModules recur m@(Module _ (Right term)) = do + c <- getConfiguration term -- Convergence here is predicated upon an Eq instance, not α-equivalence cache <- converge lowerBound (\ prevCache -> isolateCache $ do putHeap (configurationHeap c) @@ -104,8 +107,7 @@ convergingModules recur m = do -- 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 @()@. - -- FIXME: do we actually need to gather here? - withOracle prevCache (recur m)) + withOracle prevCache (raiseHandler runNonDet (recur m))) address =<< maybe empty scatter (cacheLookup c cache) -- | Iterate a monadic action starting from some initial seed until the results converge.