Verified Commit d960f2c4 authored by Sven Keidel's avatar Sven Keidel
Browse files

fix fixpoint algorithm for k-CFA

parent a4f506b1
Pipeline #29209 failed with stages
in 66 minutes and 47 seconds
{-# OPTIONS_GHC -funfolding-use-threshold=1500 -fsimpl-tick-factor=200 #-}
module Main where
import Prelude hiding (id,(.),lookup,Bounded,Bool(..),fail)
import TestPrograms
import Control.Category
import Control.Arrow.Fix.Combinator
import Control.Arrow.Trans
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.Chaotic
import Control.Arrow.Transformer.Abstract.Fix.Cache hiding (Widening)
import Data.Identifiable
import qualified Data.Metric as M
import Data.Abstract.InfiniteNumbers
import qualified Data.Abstract.Interval as I
import Data.Abstract.Terminating (Terminating)
import qualified Data.Abstract.Terminating as T
import Data.Abstract.Widening (Widening)
import qualified Data.Abstract.Widening as W
import Criterion
import Criterion.Main
type Simple a b = TerminatingT (FixT a (Terminating b) (CacheT Cache a (Terminating b) (->))) a b
type Advanced a b = TerminatingT (FixT a (Terminating b) (ChaoticT a (CacheT Cache a (Terminating b) (->)))) a b
{-# SPECIALIZE fib :: Simple IV IV #-}
{-# SPECIALIZE fib :: Advanced IV IV #-}
{-# SPECIALIZE fact :: Simple IV IV #-}
{-# SPECIALIZE fact :: Advanced IV IV #-}
main :: IO ()
main = do
defaultMain
[
bgroup "fibonacci" [
fibonacci (iv 5 10),
fibonacci (iv 10 15),
fibonacci (iv 15 20)
],
bgroup "factorial" [
factorial (iv 5 10),
factorial (iv 10 15),
factorial (iv 15 20)
]
]
where
fibonacci arg =
bgroup (show arg) [
bench "simple" $ nf fibSimple arg,
bench "inner" $ nf fibInner arg,
bench "outer" $ nf fibOuter arg
]
fibSimple = snd . run (fib :: Simple IV IV) chaotic W.finite
fibInner = snd . run (fib :: Advanced IV IV) iterateInner W.finite
fibOuter = snd . run (fib :: Advanced IV IV) iterateOuter W.finite
factorial arg =
bgroup (show arg) [
bench "simple" $ nf factSimple arg,
bench "inner" $ nf factInner arg,
bench "outer" $ nf factOuter arg
]
factSimple = snd . run (fact :: Simple IV IV) chaotic W.finite
factInner = snd . run (fact :: Advanced IV IV) iterateInner W.finite
factOuter = snd . run (fact :: Advanced IV IV) iterateOuter W.finite
-- describe "fibonacci" $ do
-- it "fib[5,10] should be [5,55]" $
-- let ?strat = Strat id in
-- let ?widen = W.finite in
-- run "fib" fib (iv 5 10) `shouldBe'` return (iv 5 55)
-- it "fib[100,110] with widening should be [0,∞]" $
-- let ?strat = Strat (widenInput I.widening) in
-- let ?widen = I.widening in
-- run "fib" fib (iv 100 110) `shouldBe'` return (iv 0 Infinity)
-- it "fib[1,∞] should be [0,∞]" $
-- let ?strat = Strat (reuseByMetric euclid) in
-- let ?widen = I.widening in
-- run "fib" fib (iv 0 Infinity) `shouldBe'` return (iv 0 Infinity)
-- describe "factorial" $ do
-- it "fact[5,10] should be [5!,10!] = [12,3628800]" $
-- let ?strat = Strat id in
-- let ?widen = W.finite in
-- run "fact" fact (iv 5 10) `shouldBe'` return (iv 120 3628800)
-- it "fact[10,15] with stack size 3 should be [10,15] * [9,14] * [8,13] * [1,∞] = [720,∞]" $
-- let ?strat = Strat (maxSize 3 (widenInput I.widening)) in
-- let ?widen = I.widening in
-- run "fact" fact (iv 10 15) `shouldBe'` return (iv 720 Infinity)
-- it "fact[0,∞] should be [1,∞]" $
-- let ?strat = Strat id in
-- let ?widen = I.widening in
-- run "fact" fact (iv 0 Infinity) `shouldBe'` return (iv 1 Infinity)
-- describe "ackermann" $ do
-- it "ack([0,3],[0,3]) should be [1,61] " $
-- let ?strat = Strat id in
-- let ?widen = W.finite in
-- run "ackermann" ackermann (iv 0 3, iv 0 3) `shouldBe'` return (iv 1 61)
-- it "ack([0,∞],[0,∞]) with euclidian reuseByMetric should be [1,∞] " $
-- let ?strat = Strat (reuseByMetric (euclid M.** euclid)) in
-- let ?widen = I.widening in do
-- pendingWith "FIXME: reuseByMetric is broken"
-- run "ackermann" ackermann (iv 0 Infinity, iv 0 Infinity) `shouldBe'` return (iv 1 Infinity)
-- describe "even odd" $
-- it "even([0,∞]) should be top" $
-- let ?strat = Strat (reuseByMetric (M.unit M.** euclid)) in
-- let ?widen = W.finite in
-- run "even" evenOdd (Even,iv 0 Infinity) `shouldBe'` top
-- describe "diverge" $
-- it "should terminate with bottom" $
-- let ?strat = Strat id in
-- let ?widen = W.finite in
-- run "diverge" diverge 5 `shouldBe'` bottom
-- where
-- shouldBe' f g = do
-- x <- f
-- x `shouldBe` g
-- {-# INLINE shouldBe' #-}
-- {-# INLINE sharedSpec #-}
......@@ -35,6 +35,7 @@ tests:
main: Spec.hs
source-dirs:
- test
- test-programs
dependencies:
- sturdy-lib
- hspec
......@@ -42,9 +43,20 @@ tests:
benchmarks:
arrow-transformers:
source-dirs:
- bench
main: ArrowTransformerBench.hs
source-dirs:
- bench/transformer
dependencies:
- sturdy-lib
- criterion
- dump-core
ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html -O2
fixpoint:
main: FixpointBench.hs
source-dirs:
- bench/fixpoint
- test-programs
dependencies:
- sturdy-lib
- criterion
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
......@@ -6,11 +7,19 @@
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Control.Arrow.Fix(Fix,Fix',ArrowFix(..)) where
module Control.Arrow.Fix(Fix,Fix',ArrowFix(..),FixpointCombinator,transform,filter,trace,trace',traceShow,traceCache) where
import Prelude hiding (filter,pred)
import Control.Arrow
import Control.Arrow.State (ArrowState)
import qualified Control.Arrow.State as State
import Control.Arrow.Trans
import Data.Profunctor
import Data.Lens(Iso',from,get,Prism',getMaybe,set)
import qualified Debug.Trace as Debug
import Text.Printf
-- | Type family that computes the type of the fixpoint.
type family Fix (c :: * -> * -> *) x y :: * -> * -> *
......@@ -28,3 +37,43 @@ class ArrowFix c where
type instance Fix (->) x y = (->)
instance ArrowFix (x -> y) where
fix f = f (fix f)
type FixpointCombinator c x y = c x y -> c x y
transform :: Profunctor c => Iso' a a' -> FixpointCombinator c a' b -> FixpointCombinator c a b
transform iso strat f = lmap (get iso)
$ strat
$ lmap (get (from iso)) f
{-# INLINE transform #-}
filter :: forall a a' b c. (Profunctor c, ArrowChoice c, ArrowApply c) => Prism' a a' -> FixpointCombinator c a' b -> FixpointCombinator c a b
filter pred strat f = proc a -> case getMaybe pred a of
Just a' -> strat (lmap (\x -> set pred x a) f) -<< a'
Nothing -> f -< a
{-# INLINE filter #-}
trace :: (Arrow c) => (a -> String) -> (b -> String) -> FixpointCombinator c a b
trace showA showB f = proc x -> do
y <- f -< Debug.trace (printf "CALL\n%s\n\n" (showA x)) x
returnA -< Debug.trace (printf "RETURN\n%s\n%s\n\n" (showA x) (showB y)) y
{-# INLINE trace #-}
trace' :: (Eq a, ArrowApply c) => (a -> String) -> (b -> String) -> FixpointCombinator c a b -> FixpointCombinator c a b
trace' showA showB strat f = proc x -> do
y <- strat (proc x' -> f -< Debug.trace (if x == x'
then printf "CALL\n%s\n\n" (showA x)
else printf "CALL\n%s~>\n%s\n\n" (showA x) (showA x')) x') -<< x
returnA -< Debug.trace (printf "RETURN\n%s\n%s\n\n" (showA x) (showB y)) y
{-# INLINE trace' #-}
traceShow :: (Show a, Show b, Arrow c) => FixpointCombinator c a b
traceShow = trace show show
{-# INLINE traceShow #-}
traceCache :: ArrowState cache c => (cache -> String) -> FixpointCombinator c a b
traceCache showCache f = proc a -> do
cache <- State.get -< ()
b <- f -< Debug.trace (printf "CACHE %s\n\n" (showCache cache)) a
cache' <- State.get -< ()
returnA -< Debug.trace (printf "CACHE %s\n\n" (showCache cache')) b
{-# INLINE traceCache #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Control.Arrow.Fix.Chaotic where
import Prelude hiding (head)
import Prelude hiding (head,iterate,map)
import Control.Arrow
import Control.Arrow.Trans
import Control.Arrow.Fix
import Control.Arrow.Fix.Stack as Stack
import Control.Arrow.Fix.Cache as Cache
import Control.Arrow.Utils(map)
import Data.Abstract.Stable
import Data.HashSet (HashSet)
import qualified Data.HashSet as H
import Data.Identifiable
......@@ -15,9 +25,108 @@ import Data.Order
import Text.Printf
class (Arrow c, Profunctor c) => ArrowChaotic a c | c -> a where
iterate :: c (a,b) b
setComponent :: c (Component a,y) y
withComponent :: c x y -> c (x,y,Component a) y -> c x y
getComponent :: c x y -> c x (Component a,y)
default setComponent :: (c ~ t c', ArrowLift t, ArrowChaotic a c') => c (Component a,y) y
setComponent = lift' setComponent
{-# INLINE setComponent #-}
chaotic :: forall a b c. (ArrowStack a c, ArrowCache a b c, ArrowChoice c) => FixpointCombinator c a b
chaotic f = proc a -> do
m <- Cache.lookup -< a
case m of
Just (_,b) -> returnA -< b
Nothing -> do
Cache.initialize -< a
iterate -< a
where
iterate = proc a -> do
b <- Stack.push f -< a
(stable,b') <- Cache.update -< (a,b)
case stable of
Stable -> returnA -< b'
Unstable -> iterate -< a
{-# INLINE chaotic #-}
-- | 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
where
iterate = proc a -> do
(component,b) <- getComponent (Stack.push f) -< a
-- The call did not depend on any unstable calls. This means
-- we are done and don't need to iterate.
if H.null (head component)
then do
Cache.write -< (a,b,Stable)
returnA -< b
else do
(stable,bNew) <- Cache.update -< (a,b)
case stable of
Stable ->
if head component == H.singleton a
then do
map Cache.setStable -< (Stable,) <$> H.toList (body component)
returnA -< bNew
else do
Cache.setStable -< (Unstable,a)
setComponent -< (component { head = H.delete a (head component)
, body = H.insert a (body component) }, bNew)
Unstable -> iterate -< a
-- | 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
where
iterate = proc a -> do
(component,b) <- getComponent (Stack.push f) -< a
case () of
-- The call did not depend on any unstable calls. This means
-- we are done and don't need to iterate.
() | H.null (head component) -> do
Cache.write -< (a,b,Stable)
returnA -< b
-- We are at the head of a fixpoint component. This means, we
-- have to iterate until the head stabilized.
| head component == H.singleton a -> do
(stable,bNew) <- Cache.update -< (a,b)
case stable of
-- If the head of a fixpoint component is stable, set
-- all elements in the body of the component as stable
-- too and return.
Stable -> do
map Cache.setStable -< H.toList $ H.map (Stable,) (body component)
returnA -< bNew
-- If the head of a fixpoint component is not stable, keep iterating.
Unstable ->
iterate -< a
-- We are inside an fixpoint component, but its head has not stabilized.
| otherwise -> do
Cache.write -< (a,b,Unstable)
setComponent -< (component { head = H.delete a (head component)
, body = H.insert a (body component) }, b)
data Component a = Component { head :: HashSet a, body :: HashSet a } deriving (Eq)
......
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Arrows #-}
module Control.Arrow.Fix.Combinator
( FixpointCombinator
, iterateInner
, iterateOuter
, transform
, filter
, reuseFirst
, reuseExact
, reuseByMetric
, reuseStableByMetric
, maxSize
, widenInput
, callsiteSensitive
, callsiteSensitive'
, recordCallsite
, trace
, trace'
, traceCache
, traceCtx
, traceShow
)
where
import Prelude hiding ((.),pred,lookup,filter,head,iterate,map)
import Control.Category
import Control.Arrow hiding (loop)
import Control.Arrow.State(ArrowState)
import qualified Control.Arrow.State as State
import Control.Arrow.Fix.Stack (ArrowStack)
import qualified Control.Arrow.Fix.Stack as Stack
import Control.Arrow.Fix.Context (ArrowContext,ArrowJoinContext)
import qualified Control.Arrow.Fix.Context as Ctx
import Control.Arrow.Fix.Reuse as Reuse
import Control.Arrow.Fix.Cache as Cache
import Control.Arrow.Fix.Chaotic
import Control.Arrow.Utils (map)
import Data.Abstract.Widening as W
import Data.Abstract.Stable
import Data.Abstract.CallString as CallString
import Data.Order
import Data.Metric
import Data.Monoid (First(..))
import Data.Profunctor
import Data.Lens (Iso',from,Prism',getMaybe,get,set)
import Data.Identifiable
import qualified Data.HashSet as H
import Text.Printf
import qualified Debug.Trace as Debug
type FixpointCombinator c x y = c x y -> c x y
-- | Iterate on the innermost fixpoint component.
iterateInner :: forall a b c. (Identifiable a, ArrowStack a c, ArrowChaotic a c, ArrowCache a b c, ArrowChoice c) => FixpointCombinator c a b
{-# INLINE iterateInner #-}
iterateInner = detectLoop . go
where
go f = withComponent f $ proc (a,b,component) ->
-- The call did not depend on any unstable calls. This means
-- we are done and don't need to iterate.
if H.null (head component)
then do
Cache.write -< (a,b,Stable)
returnA -< b
else do
(stable,bNew) <- Cache.update -< (a,b)
case stable of
Stable ->
if head component == H.singleton a
then do
map Cache.setStable -< (Stable,) <$> H.toList (body component)
setComponent -< (mempty, bNew)
else do
setStable -< (Unstable,a)
setComponent -< (component { head = H.delete a (head component)
, body = H.insert a (body component) }, bNew)
Unstable -> go f -< a
-- | Iterate on the outermost fixpoint component.
iterateOuter :: forall a b c. (Identifiable a, ArrowStack a c, ArrowChaotic a c, ArrowCache a b c, ArrowChoice c) => FixpointCombinator c a b
{-# INLINE iterateOuter #-}
iterateOuter = detectLoop . go
where
go f = withComponent f $ proc (a,b,component) -> case () of
-- The call did not depend on any unstable calls. This means
-- we are done and don't need to iterate.
() | H.null (head component) -> do
Cache.write -< (a,b,Stable)
setComponent -< (mempty,b)
-- We are at the head of a fixpoint component. This means, we
-- have to iterate until the head stabilized.
| head component == H.singleton a -> do
(stable,bNew) <- Cache.update -< (a,b)
case stable of
-- If the head of a fixpoint component is stable, set
-- all elements in the body of the component as stable
-- too and return.
Stable -> do
map Cache.setStable -< H.toList $ H.map (Stable,) (body component)
setComponent -< (mempty, bNew)
-- If the head of a fixpoint component is not stable, keep iterating.
Unstable ->
go f -< a
-- We are inside an fixpoint component, but its head has not stabilized.
| otherwise -> do
Cache.write -< (a,b,Unstable)
setComponent -< (Component { head = H.delete a (head component),
body = H.insert a (body component) }, b)
detectLoop :: (ArrowStack a c, ArrowCache a b c, ArrowChaotic a c, ArrowChoice c) => FixpointCombinator c a b
detectLoop f = proc a -> do
loop <- Stack.elem -< a
if loop
then do
m <- Cache.lookup -< a
case m of
Just (Stable,b) -> returnA -< b
Just (Unstable,b) -> iterate -< (a, b)
Nothing -> do
b <- initialize -< a
iterate -< (a, b)
else Stack.push f -< a
{-# INLINE detectLoop #-}
transform :: Profunctor c => Iso' a a' -> FixpointCombinator c a' b -> FixpointCombinator c a b
transform iso strat f = lmap (get iso)
$ strat
$ lmap (get (from iso)) f
{-# INLINE transform #-}
filter :: forall a a' b c. (Profunctor c, ArrowChoice c, ArrowApply c) => Prism' a a' -> FixpointCombinator c a' b -> FixpointCombinator c a b
filter pred strat f = proc a -> case getMaybe pred a of
Just a' -> strat (lmap (\x -> set pred x a) f) -<< a'
Nothing -> f -< a
{-# INLINE filter #-}
reuseFirst :: (PreOrd a, ArrowChoice c, ArrowReuse a b c) => Stable -> FixpointCombinator c a b
reuseFirst s f = proc a -> do
m <- reuse s (\a a' s' b' m -> case m of
First (Just _) -> m
First Nothing
| a a' -> First (Just (a',b',s'))
| otherwise -> m) -< a
case getFirst m of
Just (_,b,Stable) -> returnA -< b
Just (a',_,Unstable) -> f -< a'
Nothing -> f -< a
{-# INLINE reuseFirst #-}
reuseExact :: (ArrowChoice c, ArrowCache a b c) => FixpointCombinator c a b
reuseExact f = proc a -> do
m <- lookup -< a
case m of
Just (Stable,b) -> returnA -< b
_ -> f -< a
{-# INLINE reuseExact #-}
reuseByMetric :: (PreOrd a, Ord n, ArrowChoice c, ArrowReuse a b c) => Metric a n -> FixpointCombinator c a b
reuseByMetric metric = reuseByMetric_ (\s a a' -> Product s (metric a a')) Unstable
{-# INLINE reuseByMetric #-}
reuseStableByMetric :: (PreOrd a, Ord n, ArrowChoice c, ArrowReuse a b c) => Metric a n -> FixpointCombinator c a b
reuseStableByMetric metric = reuseByMetric_ (const metric) Stable
{-# INLINE reuseStableByMetric #-}
reuseByMetric_ :: (PreOrd a, Ord n, ArrowChoice c, ArrowReuse a b c) => (Stable -> Metric a n) -> Stable -> FixpointCombinator c a b
reuseByMetric_ metric s f = proc a -> do
m <- reuse s (\a a' s' b' m ->
if a a'
then m <> Just (Measured { input = a', output = b', isStable = s', measured = metric s' a a' })
else m) -< a
case m of
Just Measured { isStable = Stable, output = b } -> returnA -< b
Just Measured { isStable = Unstable, input = a' } -> f -< a'
Nothing -> f -< a
{-# INLINE reuseByMetric_ #-}
data Measured a b n = Measured { input :: a, output :: b, isStable :: Stable, measured :: n }
instance (Show a, Show b, Show n) => Show (Measured a b n) where
show m = printf "%s@%s" (show (output m)) (show (measured m))
instance Ord n => Semigroup (Measured a b n) where
m1 <> m2
| measured m1 <= measured m2 = m1
| otherwise = m2
{-# INLINE (<>) #-}
maxSize :: (ArrowChoice c, ArrowStack a c) => Int -> FixpointCombinator c a b -> FixpointCombinator c a b
maxSize limit strat f = proc a -> do
n <- Stack.size -< ()
if n < limit
then f -< a
else strat f -< a
{-# INLINE maxSize #-}
widenInput :: (Complete a, ArrowStack a c) => W.Widening a -> FixpointCombinator c a b
widenInput widen f = proc a -> do