Commit 88370e6b authored by Sven Keidel's avatar Sven Keidel

fix unsound chaotic fixpoint iteration

parent 06ec9f0e
Pipeline #31411 passed with stages
in 68 minutes and 11 seconds
......@@ -8,7 +8,7 @@ module Control.Arrow.Fix.Chaotic where
import Prelude hiding (head,iterate,map)
import Control.Arrow
import Control.Arrow hiding (loop)
import Control.Arrow.Trans
import Control.Arrow.Fix
import Control.Arrow.Fix.Stack as Stack
......@@ -36,13 +36,20 @@ chaotic :: forall a b c. (ArrowStack a c, ArrowCache a b c, ArrowChoice c) => Fi
chaotic f = proc a -> do
m <- Cache.lookup -< a
case m of
Just (_,b) -> returnA -< b
Nothing -> do
Cache.initialize -< a
iterate -< a
Just (Stable,b) -> returnA -< b
Just (Unstable,b) -> do
loop <- Stack.elem -< a
if loop
then returnA -< b
else Stack.push iterate -< a
Nothing -> do
loop <- Stack.elem -< a
if loop
then initialize -< a
else Stack.push iterate -< a
where
iterate = proc a -> do
b <- Stack.push f -< a
b <- f -< a
(stable,b') <- Cache.update -< (a,b)
case stable of
Stable -> returnA -< b'
......@@ -52,17 +59,10 @@ chaotic f = proc a -> do
-- | Iterate on the innermost fixpoint component.
iterateInner :: forall a b c. (Identifiable a, ArrowChaotic a c, ArrowStack a c, ArrowCache a b c, ArrowChoice c) => FixpointCombinator c a b
{-# INLINE iterateInner #-}
iterateInner f = proc a -> do
m <- Cache.lookup -< a
case m of
Just (Stable,b) -> returnA -< b
Just (Unstable,b) -> setComponent -< (mempty { head = H.singleton a }, b)
Nothing -> do
Cache.initialize -< a
iterate -< a
iterateInner f = detectLoop iterate
where
iterate = proc a -> do
(component,b) <- getComponent (Stack.push f) -< a
(component,b) <- getComponent f -< a
-- The call did not depend on any unstable calls. This means
-- we are done and don't need to iterate.
......@@ -87,17 +87,10 @@ iterateInner f = proc a -> do
-- | Iterate on the outermost fixpoint component.
iterateOuter :: forall a b c. (Identifiable a, ArrowChaotic a c, ArrowStack a c, ArrowCache a b c, ArrowChoice c) => FixpointCombinator c a b
{-# INLINE iterateOuter #-}
iterateOuter f = proc a -> do
m <- Cache.lookup -< a
case m of
Just (Stable,b) -> returnA -< b
Just (Unstable,b) -> setComponent -< (mempty { head = H.singleton a }, b)
Nothing -> do
Cache.initialize -< a
iterate -< a
iterateOuter f = detectLoop iterate
where
iterate = proc a -> do
(component,b) <- getComponent (Stack.push f) -< a
(component,b) <- getComponent f -< a
case () of
-- The call did not depend on any unstable calls. This means
-- we are done and don't need to iterate.
......@@ -128,6 +121,25 @@ iterateOuter f = proc a -> do
setComponent -< (component { head = H.delete a (head component)
, body = H.insert a (body component) }, b)
detectLoop :: (Identifiable a, ArrowChaotic a c, ArrowStack a c, ArrowCache a b c, ArrowChoice c) => c a b -> c a b
detectLoop iterate = proc a -> do
m <- Cache.lookup -< a
case m of
Just (Stable,b) -> returnA -< b
Just (Unstable,b) -> do
loop <- Stack.elem -< a
if loop
then setComponent -< (mempty { head = H.singleton a }, b)
else Stack.push iterate -< a
Nothing -> do
loop <- Stack.elem -< a
if loop
then do
b <- Cache.initialize -< a
setComponent -< (mempty { head = H.singleton a }, b)
else Stack.push iterate -< a
{-# INLINE detectLoop #-}
data Component a = Component { head :: HashSet a, body :: HashSet a } deriving (Eq)
instance Identifiable a => PreOrd (Component a) where
......
......@@ -19,14 +19,17 @@ import Text.Printf
class (Arrow c, Profunctor c) => ArrowStack a c | c -> a where
push :: c a b -> c a b
elem :: c a Bool
elems :: c () [a]
peek :: c () (Maybe a)
size :: c () Int
default elem :: (c ~ t c', ArrowLift t, ArrowStack a c') => c a Bool
default elems :: (c ~ t c', ArrowLift t, ArrowStack a c') => c () [a]
default peek :: (c ~ t c', ArrowLift t, ArrowStack a c') => c () (Maybe a)
default size :: (c ~ t c', ArrowLift t, ArrowStack a c') => c () Int
elem = lift' elem
elems = lift' elems
peek = lift' peek
size = lift' size
......@@ -69,13 +72,13 @@ reuseFirst = reuse find
reuseByMetric :: (PreOrd a, Ord n, ArrowChoice c, ArrowStack a c) => Metric a n -> FixpointCombinator c a b
reuseByMetric metric = reuse find
where
find a xs = elem <$> foldMap (\a' -> if a a' then Just (Measured a' (metric a a')) else Nothing) xs
find a xs = element <$> foldMap (\a' -> if a a' then Just (Measured a' (metric a a')) else Nothing) xs
{-# INLINE reuseByMetric #-}
data Measured a n = Measured { elem :: a, measured :: n }
data Measured a n = Measured { element :: a, measured :: n }
instance (Show a, Show n) => Show (Measured a n) where
show m = printf "%s@%s" (show (elem m)) (show (measured m))
show m = printf "%s@%s" (show (element m)) (show (measured m))
instance Ord n => Semigroup (Measured a n) where
m1 <> m2
......
......@@ -225,26 +225,37 @@ newCache f = lift $ \widen ->
------ Monotone Cache ------
data Monotone a b where
Monotone :: s -> Monotone s s
Monotone :: s -> HashMap a b -> Monotone (s,a) (s,b)
type instance Widening (Monotone s s) = W.Widening s
type instance Widening (Monotone (s,a) (s,b)) = (W.Widening s,W.Widening b)
instance IsEmpty s => IsEmpty (Monotone s s) where
empty = Monotone empty
instance IsEmpty s => IsEmpty (Monotone (s,a) (s,b)) where
empty = Monotone empty empty
instance Show s => Show (Monotone s s) where
show (Monotone s) = show s
instance (Show s, Show a, Show b) => Show (Monotone (s,a) (s,b)) where
show (Monotone s m) = show (s,m)
instance (Arrow c, Profunctor c) => ArrowParallel (CacheT Monotone a b c) where
nextIteration = id
{-# INLINE nextIteration #-}
instance (ArrowChoice c, Profunctor c) => ArrowCache s s (CacheT Monotone s s c) where
initialize = id
lookup = CacheT $ proc s -> returnA -< Just (Unstable, s)
update = CacheT $ askConst $ \widening -> modify' $ \((_,sNew), Monotone sOld) ->
let y@(_,sWiden) = widening sOld sNew
in (y,Monotone sWiden)
instance (Identifiable a, LowerBounded b, ArrowChoice c, Profunctor c) => ArrowCache (s,a) (s,b) (CacheT Monotone (s,a) (s,b) c) where
initialize = CacheT $ modify' $ \((s,a),Monotone s' cache) ->
let cache' = M.insertWith (\_ _old -> _old) a bottom cache
b = M.lookupDefault bottom a cache
in ((s,b),Monotone s' cache')
lookup = CacheT $ proc (s,a) -> do
m <- get -< ()
case m of
Monotone _ cache ->
returnA -< (\b -> (Unstable,(s,b))) <$> M.lookup a cache
update = CacheT $ askConst $ \(widenS,widenB) -> modify' $ \(((_,a),(sNew,b)),Monotone sOld cache) ->
let (stable1,sWiden) = widenS sOld sNew
in case M.lookup a cache of
Just b' ->
let ~(stable2,b'') = widenB b' b
in ((stable1 stable2, (sWiden,b'')), Monotone sWiden (M.insert a b'' cache))
Nothing -> ((Unstable,(sWiden,b)),Monotone sWiden (M.insert a b cache))
write = CacheT $ proc _ -> returnA -< ()
setStable = CacheT $ proc _ -> returnA -< ()
{-# INLINE initialize #-}
......
......@@ -28,6 +28,9 @@ import Data.Profunctor
import Data.Profunctor.Unsafe ((.#))
import Data.Coerce
import Data.Empty
import Data.HashSet (HashSet)
import qualified Data.HashSet as Set
import Data.Identifiable
newtype StackT stack a c x y = StackT (ReaderT (stack a) c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowJoin,ArrowComplete z,
......@@ -35,18 +38,25 @@ newtype StackT stack a c x y = StackT (ReaderT (stack a) c x y)
ArrowParallel,ArrowControlFlow stmt)
data Stack a = Stack
{ elems :: [a]
{ elems :: HashSet a
, stack :: [a]
, size :: !Int
}
instance IsEmpty (Stack a) where
empty = Stack { elems = [], size = 0 }
empty = Stack { elems = empty, stack = empty, size = 0 }
{-# INLINE empty #-}
instance (Arrow c, Profunctor c) => ArrowStack a (StackT Stack a c) where
push f = lift $ proc (st,a) -> unlift f -< (st { elems = a : elems st, size = size st + 1 }, a)
peek = lift $ proc (st,()) -> returnA -< case elems st of [] -> Nothing; (x:_) -> Just x
elems = lift $ proc (st,()) -> returnA -< elems st
instance (Identifiable a, Arrow c, Profunctor c) => ArrowStack a (StackT Stack a c) where
push f = lift $ proc (st,a) -> do
let st' = st { elems = Set.insert a (elems st)
, stack = a : stack st
, size = size st + 1
}
unlift f -< (st', a)
elem = lift $ proc (st,a) -> returnA -< Set.member a (elems st)
peek = lift $ proc (st,()) -> returnA -< case stack st of [] -> Nothing; (x:_) -> Just x
elems = lift $ proc (st,()) -> returnA -< stack st
size = lift $ proc (st,()) -> returnA -< size st
{-# INLINE peek #-}
{-# INLINE push #-}
......
......@@ -24,7 +24,7 @@ import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Environment(extend')
import Control.Arrow.Fix
import Control.Arrow.Fix.Parallel(parallel)
import Control.Arrow.Fix.Chaotic(chaotic)
import qualified Control.Arrow.Fix.Context as Ctx
import Control.Arrow.Trans
import Control.Arrow.Closure (ArrowClosure,IsClosure(..))
......@@ -34,10 +34,11 @@ import Control.Arrow.Transformer.Value
import Control.Arrow.Transformer.Abstract.FiniteEnvironment
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.Chaotic
import Control.Arrow.Transformer.Abstract.Fix.Context
import Control.Arrow.Transformer.Abstract.Fix.Stack
-- import Control.Arrow.Transformer.Abstract.Fix.Trace
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable(CacheT,Cache,Parallel,Monotone,type (**),Group)
import Control.Arrow.Transformer.Abstract.Fix.Trace
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable(CacheT,Monotone)
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Monad.State hiding (lift,fail)
......@@ -101,10 +102,10 @@ evalInterval env0 e = snd $
(TerminatingT
(EnvT Text Addr Val
(FixT _ _
(-- ChaoticT In
(ChaoticT In
(-- TraceT
(StackT Stack In
(CacheT (Monotone ** Parallel (Group Cache)) In Out
(CacheT Monotone In Out
(ContextT Ctx
(->))))))))))) Expr Val))
(alloc, widenVal)
......@@ -122,7 +123,7 @@ evalInterval env0 e = snd $
-- traceShow .
-- traceCache show .
Ctx.recordCallsite ?sensitivity (\(_,(_,expr)) -> case expr of App _ _ l -> Just l; _ -> Nothing) .
filter apply parallel
filter apply chaotic
widenVal :: Widening Val
widenVal = widening (I.bounded ?bound)
......
......@@ -51,7 +51,7 @@ spec = do
evalInterval' [("x", num 0 1)] (let_ [("add",add)] (app "add" ["x",two]))
-- Most precise would be [2,3], however, the analysis does not refine
-- `x` and therefore introduces some imprecision.
`shouldBe` Terminating (Success (num 2 5))
`shouldBe` Terminating (Success (num 2 7))
it "context sensitivity" $
let diamond = let_ [("second",second),("id",id)] (app "second" [app "id" [one],app "id" [two]]) in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment