Commit 441661b8 authored by Sven Keidel's avatar Sven Keidel

merge stack widening and fixpoint caching strategy

parent c203290d
Pipeline #12902 failed with stage
in 16 minutes and 25 seconds
......@@ -28,73 +28,59 @@ import Control.Arrow.Transformer.State
import Data.Identifiable
import Data.Order
import Data.HashSet (HashSet)
import qualified Data.HashSet as H
import Data.Profunctor
import Data.Coerce
import Data.Abstract.Cache (IsCache,CachingStrategy,RecomputeOrCached(..))
import qualified Data.Abstract.Cache as Cache
import Data.Abstract.StackWidening (StackWidening,Loop(..))
import Data.Abstract.Widening (Stable(..),Widening)
import Data.Abstract.IterationStrategy
type Component a = HashSet a
newtype FixT stack cache a b c x y = FixT { unFixT ::
ConstT (StackWidening stack a,CachingStrategy cache a b,Widening b)
(ReaderT (stack a) (StateT (Component a,cache a b) c)) x y }
ConstT (IterationStrategy stack cache a b)
(ReaderT (stack a b) (StateT (cache a b) c)) x y }
deriving (Profunctor,Category,Arrow,ArrowChoice)
runFixT :: (Identifiable a,PreOrd b,Monoid (stack a),IsCache cache a b,ArrowChoice c, Profunctor c)
=> StackWidening stack a -> CachingStrategy cache a b -> Widening b -> FixT stack cache a b c x y -> c x y
runFixT stackWiden cachingStrat widen (FixT f) =
dimap (\x -> ((H.empty,Cache.empty),(mempty,x))) snd $
runStateT $ runReaderT $ runConstT (stackWiden,cachingStrat,widen) f
runFixT :: (Identifiable a, PreOrd b, IsEmpty (stack a b), IsEmpty (cache a b), ArrowChoice c, Profunctor c)
=> IterationStrategy stack cache a b -> FixT stack cache a b c x y -> c x y
runFixT iterationStrat (FixT f) =
dimap (\x -> (empty,(empty,x))) snd $
runStateT $ runReaderT $ runConstT (iterationStrat) f
type instance Fix x y (FixT stack cache () () c) = FixT stack cache x y c
instance (Identifiable a, LowerBounded b, Profunctor c,IsCache cache a b,ArrowChoice c,ArrowApply c) => ArrowFix a b (FixT stack cache a b c) where
fix f = cached $ stackWidening $ proc (loop,x) -> do
-- Apply a stack widening operator to the input value.
-- The stack widening operator ensures that the abstract
-- interpreter does not recurse infinitely deep and detects
-- signals if the interpreter is in a loop. See
-- `Data.Abstract.StackWidening` for details.
instance (Identifiable a, LowerBounded b, Profunctor c,ArrowChoice c,ArrowApply c) => ArrowFix a b (FixT stack cache a b c) where
fix f =
-- The iteration strategy ensures that the abstract interpreter
-- terminates, soundly approximates the fixpoint and avoids
-- unnecessary computation.
iterationStrategy $ proc strat -> do
case loop of
NoLoop ->
-- If there is no loop, keep recursing.
case strat of
-- The evaluation of some expressions, such as arithmetic
-- expressions, always terminates. In this case, we simply keep
-- recursing.
Compute x ->
f (fix f) -< x
MaybeLoop ->
-- If we may be in a loop, continue recursing and check
-- afterwards if the cached value has stabilized, otherwise keep
-- iterating.
-- The evaluation of some other expressions, such as loops, may
-- may not terminate. Because these expressions may recursively
-- depend on themselves, we need to iterate on these
-- expressions, until the result stabilized.
ComputeAndIterate x upd ->
let iterate = proc () -> do
y <- f (fix f) -< x
member <- inComponent -< x
deleteFromComponent -< x
if member
then do
-- Updates the cached value by applying a widening
-- operator on the old and the new `y` value. The
-- widening operator also signals if the cached
-- value stabilized, i.e., did not grow.
(stable,yNew) <- update -< (x,y)
-- If we did not reach a fixpoint of f(x'), keep iterating.
case stable of
Instable -> iterate -< ()
Stable -> returnA -< yNew
else returnA -< y
y <- f (fix f) -< x
r <- update -< (y,upd)
case r of
Return y' -> returnA -< y'
Iterate -> iterate -< ()
in iterate -<< ()
Loop -> do
-- If we are in a loop, return the cached value or bottom otherwise.
-- Furthermore, add x' to the current component.
addToComponent -< x
lookupInit -< x
-- We may return an unstable result to avoid non-termination
-- when evaluating an recursive program, Of course this is only
-- sound if we iterate on the result until it stabilized.
-- Alternatively, we can avoid redundant evaluation by
-- returning a cached value instead of recomputing it.
Cached _ y -> returnA -< y
instance (Identifiable a, ArrowJoin c, ArrowChoice c) => ArrowJoin (FixT stack cache a b c) where
-- | The join operation of the 'FixT' arrow *does not* join the
......@@ -123,32 +109,16 @@ instance (Arrow c, Profunctor c) => ArrowDeduplicate x y (FixT stack cache a b c
dedup f = f
----- Helper functions -----
cached :: (ArrowChoice c,Profunctor c) => FixT stack cache a b c a b -> FixT stack cache a b c a b
cached (FixT f) = FixT $ askConst $ \(_,cachingStrat,_) -> proc a -> do
r <- modify' (\(a,(comp,cache)) -> let (r,cache') = cachingStrat a cache in (r,(comp,cache'))) -< a
case r of
Recompute a' -> f -< a'
Cached b -> returnA -< b
stackWidening :: (Arrow c,Profunctor c) => FixT stack cache a b c (Loop,a) b -> FixT stack cache a b c a b
stackWidening (FixT f) = FixT $ askConst $ \(stackWiden,_,_) -> proc x -> do
stack <- ask -< ()
let (stack',(loop,x')) = stackWiden stack x
local f -< (stack',(loop,x'))
update :: (Identifiable a, IsCache cache a b, Arrow c, Profunctor c) => FixT stack cache a b c (a,b) (Stable,b)
update = FixT $ askConst $ \(_,_,widening) -> modify' $ \((a,b),(comp,cache)) -> let ((st,b'),cache') = Cache.update widening a b cache in ((st,b'),(comp,cache'))
lookupInit :: (Identifiable a, IsCache cache a b, Arrow c, Profunctor c) => FixT stack cache a b c a b
lookupInit = FixT $ modify' $ \(a,(comp,cache)) -> let (b,cache') = Cache.lookupInit a cache in (b,(comp,cache'))
inComponent :: (Identifiable a, Arrow c, Profunctor c) => FixT stack cache a b c a Bool
inComponent = FixT $ proc x -> do
(comp,_) <- get -< ()
returnA -< not (H.null comp) && H.member x comp
deleteFromComponent :: (Identifiable a, Arrow c, Profunctor c) => FixT stack chache a b c a ()
deleteFromComponent = FixT $ modify' $ \(x,(comp,cache)) -> ((),(H.delete x comp,cache))
addToComponent :: (Identifiable a, Arrow c, Profunctor c) => FixT stack cache a b c a ()
addToComponent = FixT $ modify' $ \(x,(comp,cache)) -> ((),(H.insert x comp,cache))
iterationStrategy :: (Arrow c,Profunctor c) => FixT stack cache a b c (Compute cache a b) b -> FixT stack cache a b c a b
iterationStrategy (FixT f) = FixT $ askConst $ \iterationStrat ->
modify (proc (x,cache) -> do
stack <- ask -< ()
let (strat,(stack',cache')) = iterationStrat x (stack,cache)
returnA -< ((stack',strat),cache')
)
>>>
local f
update :: (Identifiable a, Arrow c, Profunctor c) => FixT stack cache a b c (b,Update cache a b) (Iterate b)
update = FixT $ modify' $ \((b,upd),cache) -> upd b cache
{-# INLINE update #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Data.Abstract.Cache where
import Prelude hiding (lookup)
import Data.Identifiable
import Data.Order
import Data.Abstract.Widening
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
data RecomputeOrCached a b = Recompute a | Cached b
type CachingStrategy cache a b = a -> cache a b -> (RecomputeOrCached a b,cache a b)
class (Identifiable a, LowerBounded b) => IsCache cache a b where
empty :: cache a b
lookup :: a -> cache a b -> Maybe (Stable,b)
lookupInit :: a -> cache a b -> (b,cache a b)
update :: Widening b -> a -> b -> cache a b -> ((Stable,b),cache a b)
newtype Cache a b = Cache (HashMap a (Stable,b))
instance (Identifiable a, LowerBounded b) => IsCache Cache a b where
empty = Cache M.empty
lookup a (Cache m) = M.lookup a m
lookupInit a (Cache m) = let m' = M.insertWith (\_ old -> old) a (Instable,bottom) m in (snd (m' M.! a), Cache m')
update widen x y (Cache cache) = case M.lookup x cache of
Just (_,yOld) -> let yNew = widen yOld y in (yNew,Cache (M.insert x yNew cache))
Nothing -> ((Instable,y),Cache (M.insert x (Instable,y) cache))
stabilized :: IsCache cache a b => CachingStrategy cache a b
stabilized a cache = case lookup a cache of
Just (Stable,b) -> (Cached b,cache)
_ -> (Recompute a,cache)
recompute :: IsCache cache a b => CachingStrategy cache a b
recompute a cache = (Recompute a,cache)
This diff is collapsed.
{-# LANGUAGE MultiParamTypeClasses #-}
module Data.Abstract.Stack where
class IsStack stack a b where
push :: a -> stack a b -> stack a b
peek :: stack a b -> Maybe a
This diff is collapsed.
......@@ -26,15 +26,14 @@ 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 Data.Abstract.StackWidening (StackWidening)
import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Cache (Cache)
import qualified Data.Abstract.Cache as C
import Data.Abstract.IterationStrategy (IterationStrategy,IsEmpty)
import qualified Data.Abstract.IterationStrategy as S
import Data.Order
import Data.Hashable
import Data.Profunctor
import Data.Lens (iso')
-- import Data.Lens (iso')
import GHC.Generics
......@@ -43,13 +42,13 @@ import Test.Hspec
main :: IO ()
main = hspec spec
type Arr s x y = Fix x y (TerminatingT (FixT s Cache () () (->))) x y
type Arr s c x y = Fix x y (TerminatingT (FixT s c () () (->))) x y
type IV = Interval (InfiniteNumber Int)
spec :: Spec
spec = do
describe "fibonacci" $
let fib :: Show (s IV) => Arr s IV IV
let fib :: Arr s c IV IV
fib = fix $ \f ->
ifLowerThan 0
(proc _ -> returnA -< I.Interval 0 0)
......@@ -61,44 +60,42 @@ spec = do
in do
it "fib[5,10] should be [5,55]" $
let ?stackWiden = SW.finite in
let ?widen = W.finite in
let ?strat = S.finite in
run fib (iv 5 10) `shouldBe` return (iv 5 55)
it "fib[100,110] with stack size 3 should be [0,∞]" $
let ?stackWiden = SW.stack (SW.maxSize 3 (SW.reuseFirst (SW.fromWidening I.widening))) in
it "fib[100,110] with widening should be [0,∞]" $
let ?widen = I.widening in
run fib (iv 100 110) `shouldBe` return (iv 0 Infinity)
let ?strat = S.fromWidening I.widening $ cached
in run fib (iv 100 110) `shouldBe` return (iv 0 Infinity)
it "fib[1,∞] should be [0,∞]" $
let ?stackWiden = SW.stack $ SW.reuseFirst $ SW.finite' in
let ?widen = I.widening in
run fib (iv 0 Infinity) `shouldBe` return (iv 0 Infinity)
let ?strat = S.reuseFirst $ cached
in run fib (iv 0 Infinity) `shouldBe` return (iv 0 Infinity)
describe "factorial" $
let fact :: Show (s IV) => Arr s IV IV
let fact :: Arr s c IV IV
fact = fix $ \f ->
ifLowerThan 1 (proc _ -> returnA -< iv 1 1)
(proc n -> do x <- f -< (n - iv 1 1)
returnA -< n * x)
in do
it "fact[5,10] should be [5!,10!] = [12,3628800]" $
let ?stackWiden = SW.finite in
let ?widen = W.finite in
let ?strat = S.finite in
run fact (iv 5 10) `shouldBe` return (iv 120 3628800)
it "fact[10,15] with stack size 3 should be [1,∞] * [8,13] * [9,14] * [10,15] = [720,∞]" $
let ?stackWiden = (SW.stack (SW.maxSize 3 (SW.fromWidening I.widening))) in
let ?widen = I.widening in
run fact (iv 10 15) `shouldBe` return (iv 720 Infinity)
let ?strat = S.maxSize 3 cached $ S.fromWidening I.widening $ cached
in run fact (iv 10 15) `shouldBe` return (iv 720 Infinity)
it "fact[0,∞] should be [1,∞]" $
let ?stackWiden = SW.stack $ SW.reuseFirst $ SW.finite' in
let ?widen = I.widening in
run fact (iv 0 Infinity) `shouldBe` return (iv 1 Infinity)
let ?strat = S.reuseFirst $ cached
in run fact (iv 0 Infinity) `shouldBe` return (iv 1 Infinity)
describe "ackermann" $
let ackermann :: Show (s (IV,IV)) => Arr s (IV,IV) IV
let ackermann :: Arr s c (IV,IV) IV
ackermann = fix $ \f -> proc (m,n) ->
ifLowerThan 0
(proc _ -> returnA -< n + iv 1 1)
......@@ -109,22 +106,21 @@ spec = do
-<< m
in do
it "ack([0,3],[0,3]) should be [1,61] " $
let ?stackWiden = SW.finite in
let ?widen = W.finite in
let ?strat = S.finite in
run ackermann (iv 0 3, iv 0 3) `shouldBe` return (iv 1 61)
it "ack([0,3],[0,3]) with stack size 3 should be [1,∞]" $
let ?stackWiden = SW.stack $ SW.maxSize 3 $ SW.topOut' (iv 0 Infinity, iv 0 Infinity) in
it "ack([0,3],[0,3]) with stack reuse should be [1,∞]" $
let ?widen = I.widening in
run ackermann (iv 0 3, iv 0 3) `shouldBe` return (iv 1 Infinity)
let ?strat = S.reuseFirst $ cached
in run ackermann (iv 0 3, iv 0 3) `shouldBe` return (iv 1 Infinity)
it "ack([0,∞],[0,∞]) should be [1,∞] " $
let ?stackWiden = SW.stack $ SW.reuseFirst $ SW.fromWidening (I.widening W.** I.widening) in
let ?widen = I.widening in
run ackermann (iv 0 Infinity, iv 0 Infinity) `shouldBe` return (iv 1 Infinity)
let ?strat = S.reuseFirst $ cached
in run ackermann (iv 0 Infinity, iv 0 Infinity) `shouldBe` return (iv 1 Infinity)
describe "mutual recursive functions" $
let evenOdd :: Show (s (EvenOdd,IV)) => Arr s (EvenOdd,IV) Bool
let evenOdd :: Arr s c (EvenOdd,IV) Bool
evenOdd = fix $ \f -> proc (e,x) -> case e of
Even -> ifLowerThan 0 (proc _ -> returnA -< true)
(ifLowerThan 1 (proc _ -> returnA -< false)
......@@ -134,27 +130,28 @@ spec = do
(proc x -> f -< (Even,x-I.Interval 1 1))) -< x
in
it "even([0,∞]) should be top" $
let ?stackWiden = SW.groupBy (iso' id id)
$ SW.stack
$ SW.maxSize 3
$ SW.reuseFirst
$ SW.finite'
in let ?widen = W.finite in
run evenOdd (Even,iv 0 Infinity) `shouldBe` top
let ?widen = W.finite in
let ?strat = cached
in run evenOdd (Even,iv 0 Infinity) `shouldBe` top
describe "non-terminating function" $
let diverge :: Show (s Int) => Arr s Int Sign
let diverge :: Arr s c Int Sign
diverge = fix $ \f -> proc n -> case n of
0 -> f -< 0
_ -> f -< (n-1)
in it "should terminate with bottom" $
let ?stackWiden = SW.stack $ SW.reuseFirst $ SW.finite' in
let ?widen = W.finite in
let ?strat = S.reuseFirst $ cached
in
run diverge 5 `shouldBe` bottom
where
run :: (Identifiable a, Complete b, Monoid (s a), ?stackWiden :: StackWidening s a, ?widen :: Widening b) => Arr s a b -> a -> Terminating b
run f a = runFixT ?stackWiden C.stabilized (T.widening ?widen) (runTerminatingT f) a
run :: (Identifiable a, Complete b, IsEmpty (stack a (Terminating b)), IsEmpty (cache a (Terminating b)), ?strat :: IterationStrategy stack cache a (Terminating b))
=> Arr stack cache a b -> a -> Terminating b
run f a = runFixT ?strat (runTerminatingT f) a
cached :: (Show a, Show b, Identifiable a,PreOrd b,?widen :: Widening b) => IterationStrategy S.Stack S.Cache a (Terminating b)
cached = S.cached (T.widening ?widen)
ifLowerThan :: (Num n, Ord n, ArrowChoice c, Profunctor c, Complete (c (Interval n, Interval n) x)) => n -> c (Interval n) x -> c (Interval n) x -> c (Interval n) x
ifLowerThan l f g = proc x -> case x of
......@@ -169,3 +166,5 @@ spec = do
data EvenOdd = Even | Odd deriving (Eq,Generic,Show)
instance Hashable EvenOdd
instance PreOrd EvenOdd where
e1 e2 = e1 == e2
......@@ -57,6 +57,8 @@ import qualified Data.Abstract.Terminating as T
import Data.Abstract.Closure (Closure)
import qualified Data.Abstract.Closure as C
import Data.Abstract.DiscretePowerset (Pow)
import Data.Abstract.Cache (Cache)
import qualified Data.Abstract.Cache as Cache
import GHC.Generics(Generic)
import GHC.Exts(IsString(..))
......@@ -78,7 +80,7 @@ type Addr = (Text,CallString Label)
-- an environment, and the input of the computation.
evalInterval :: (?bound :: IV) => Int -> [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow String) Val)
evalInterval k env0 e = -- runInterp eval ?bound k env (generate e)
runFixT stackWiden (T.widening (E.widening W.finite widenVal))
runFixT stackWiden Cache.stabilized (T.widening (E.widening W.finite widenVal))
(runTerminatingT
(runErrorT
(runContourT k
......@@ -91,7 +93,7 @@ evalInterval k env0 e = -- runInterp eval ?bound k env (generate e)
(ContourT Label
(ErrorT (Pow String)
(TerminatingT
(FixT _ () () (->))))))) Expr Val))))))
(FixT _ Cache () () (->))))))) Expr Val))))))
(env0,generate e)
where
widenVal = widening (W.bounded ?bound I.widening)
......
......@@ -68,6 +68,8 @@ import Data.Abstract.Widening as W
import Data.Abstract.DiscretePowerset(Pow)
import Data.Abstract.TreeGrammar
import qualified Data.Abstract.TreeGrammar.Terminal as Term
import Data.Abstract.Cache
import qualified Data.Abstract.Cache as Cache
import qualified Test.QuickCheck as Q
import Text.Printf
......@@ -90,12 +92,12 @@ type Interp s a b =
(ErrorT (Pow String)
(CompletionT
(TerminatingT
(FixT s () ()
(FixT s Cache () ()
(->))))))))) a b
runInterp :: Interp _ a b -> Int -> StratEnv -> TermEnv -> a -> Terminating (FreeCompletion (Error (Pow String) (Except () (TermEnv, b))))
runInterp f i senv0 tenv0 a =
runFixT stackWidening (T.widening grammarWidening)
runFixT stackWidening Cache.stabilized (T.widening grammarWidening)
(runTerminatingT
(runCompletionT
(runErrorT
......
......@@ -53,6 +53,8 @@ import Data.Abstract.Error as F
import qualified Data.Abstract.Maybe as A
import Data.Abstract.DiscretePowerset(Pow)
import qualified Data.Abstract.DiscretePowerset as P
import Data.Abstract.Cache(Cache)
import qualified Data.Abstract.Cache as Cache
-- import qualified Data.Concrete.Powerset as C
-- import qualified Data.Concrete.Error as CE
-- import qualified Data.Concrete.Failure as CF
......@@ -90,7 +92,7 @@ type Interp s x y =
(ErrorT TypeError
(CompletionT
(TerminatingT
(FixT s () ()
(FixT s Cache () ()
(->)))))))))) x y
runInterp :: forall x y. Interp _ x y -> Int -> Int -> StratEnv -> Context -> TermEnv -> x -> Terminating (FreeCompletion (Error (Pow String) (Except () (TermEnv,y))))
......@@ -98,10 +100,7 @@ runInterp f k l senv0 ctx tenv0 a =
if not $ M.null (Ctx.filterInconsistentConstructors ctx)
then error $ printf "Invalid constructor singnatures %s" (show $ Ctx.filterInconsistentConstructors ctx)
else
runFixT' (\((te,(_,(s,t))),(te',(_,(s',t')))) -> printf "strat = %s -> %s, sort = %s -> %s, env = %s -> %s" (show s) (show s') (show t) (show t') (show te) (show te'))
show
stackWidening
(T.widening resultWidening)
runFixT stackWidening Cache.recompute (T.widening resultWidening)
(runTerminatingT
(runCompletionT
(runErrorT
......@@ -225,8 +224,7 @@ instance (ArrowChoice c, ArrowApply c, ArrowJoin c, ArrowConst Context c, ArrowF
then (returnA -< Term Top (context t)) <> (throw -< ()) -- cannot deduct target sort from sort Lexical
else throw -< ()
mapSubterms f = proc s -> do
ctx <- askConst -< ()
mapSubterms f = askConst $ \ctx -> proc s -> do
(| joinList
(typeError -< printf "Sort %s not found in context." (show s))
(\(c,ts) -> do
......@@ -234,8 +232,7 @@ instance (ArrowChoice c, ArrowApply c, ArrowJoin c, ArrowConst Context c, ArrowF
cons -< (c,ts')) |)
([ (c',sortsToTerms ss ctx) | (c',Signature ss _) <- (Ctx.lookupSort ctx (sort s))])
cons = proc (c, ss) -> do
ctx <- askConst -< ()
cons = askConst $ \ctx -> proc (c, ss) -> do
case c of
"Cons" -> case ss of
[Term a _,Term s _] ->
......@@ -252,13 +249,8 @@ instance (ArrowChoice c, ArrowApply c, ArrowJoin c, ArrowConst Context c, ArrowF
then typeError -< printf "Could not construct term %s. Could not find the constructor %s in the context." (show (c,ss)) (show c)
else returnA -< t
numberLiteral = proc _ -> do
ctx <- askConst -< ()
returnA -< Term Numerical ctx
stringLiteral = proc _ -> do
ctx <- askConst -< ()
returnA -< Term Lexical ctx
numberLiteral = askConst $ \ctx -> arr $ \_ -> Term Numerical ctx
stringLiteral = askConst $ \ctx -> arr $ \_ -> Term Lexical ctx
instance ArrowTrans SortT where
type Dom SortT x y = x
......@@ -284,8 +276,7 @@ instance (ArrowChoice c, ArrowJoin c, ArrowState TermEnv c, ArrowConst Context c
getTermEnv = get
putTermEnv = put
emptyTermEnv = lmap (\() -> S.empty) put
lookupTermVar f g = proc (v,env,ex) -> do
ctx <- askConst -< ()
lookupTermVar f g = askConst $ \ctx -> proc (v,env,ex) ->
case S.lookup v (Term Top ctx) env of
A.Just t -> f -< t
A.Nothing -> g -< ex
......
......@@ -41,6 +41,8 @@ import qualified Data.Abstract.Widening as W
import qualified Data.Abstract.StackWidening as S
import qualified Data.Abstract.Ordering as O
import qualified Data.Abstract.Equality as E
import Data.Abstract.Cache (Cache)
import qualified Data.Abstract.Cache as Cache
import qualified Data.Lens as L
import Data.Profunctor
......@@ -78,7 +80,7 @@ data Val = BoolVal Bool | NumVal IV | Top deriving (Eq,Generic)
run :: (?bound :: IV) => Int -> [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (M.Map Addr Val))
run k env ss =
fmap fst <$>
runFixT stackWiden widenTerm
runFixT stackWiden Cache.stabilized widenTerm
(runTerminatingT
(runErrorT
(runStoreT
......@@ -91,7 +93,7 @@ run k env ss =
(StoreT Addr Val
(ErrorT (Pow String)
(TerminatingT
(FixT _ () () (->))))))) [Statement] ()))))))
(FixT _ Cache () () (->))))))) [Statement] ()))))))
(M.empty,(SM.fromList env, generate <$> ss))
where
......
......@@ -26,6 +26,8 @@ import Data.Abstract.FreeCompletion(FreeCompletion)
import Data.Abstract.DiscretePowerset(Pow)
import qualified Data.Abstract.StackWidening as SW
import qualified Data.Abstract.Widening as W
import Data.Abstract.Cache(Cache)
import qualified Data.Abstract.Cache as Cache
import Data.Order
import Data.Label
......@@ -56,7 +58,7 @@ type Val = ()
run :: [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (M.Map Addr Val))
run env ss =
fmap fst <$>
runFixT SW.finite W.finite
runFixT SW.finite Cache.stabilized W.finite
(runTerminatingT
(runErrorT
(runStoreT
......@@ -69,7 +71,7 @@ run env ss =
(StoreT Addr Val
(ErrorT (Pow String)
(TerminatingT
(FixT _ () () (->))))))) [Statement] ()))))))
(FixT _ Cache () () (->))))))) [Statement] ()))))))
(M.empty,(SM.fromList env,generate <$> ss))
newtype UnitT c x y = UnitT { runUnitT :: c x y }
......
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