github/semantic
1
1
Fork 0
mirror of https://github.com/github/semantic.git synced 2025-01-06 23:46:21 +03:00
Code Issues Projects Releases Wiki Activity

Run nondeterminism locally in flow-sensitive analysis.

Browse Source
This commit is contained in:
Rob Rix 2018-10-26 13:03:14 -04:00
parent f0925ad0cf
commit 66d5a1dfe8
1 changed files with 7 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/Analysis/Abstract/Caching/FlowSensitive.hs
View File

@ -89,10 +89,13 @@ convergingModules :: ( AbstractValue term address value m
, Member (Env address) sig , Member (Env address) sig
, Member (State (Heap address value)) sig , Member (State (Heap address value)) sig
, Carrier sig m , Carrier sig m
, Effect sig
) )
=> Open (Module term -> Evaluator term address value m address) => (Module (Either prelude term) -> Evaluator term address value (AltC Maybe (Eff m)) address)
convergingModules recur m = do -> (Module (Either prelude term) -> Evaluator term address value m address)
c <- getConfiguration (moduleBody m) 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 -- Convergence here is predicated upon an Eq instance, not α-equivalence
cache <- converge lowerBound (\ prevCache -> isolateCache $ do cache <- converge lowerBound (\ prevCache -> isolateCache $ do
putHeap (configurationHeap c) putHeap (configurationHeap c)
@ -104,8 +107,7 @@ convergingModules recur m = do
-- that it doesn't "leak" to the calling context and diverge (otherwise this -- 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 -- would never complete). We don’t need to use the values, so we 'gather' the
-- nondeterministic values into @()@. -- nondeterministic values into @()@.
-- FIXME: do we actually need to gather here? withOracle prevCache (raiseHandler runNonDet (recur m)))
withOracle prevCache (recur m))
address =<< maybe empty scatter (cacheLookup c cache) address =<< maybe empty scatter (cacheLookup c cache)
-- | Iterate a monadic action starting from some initial seed until the results converge. -- | Iterate a monadic action starting from some initial seed until the results converge.