Commit 213fe823 authored by Sven Keidel's avatar Sven Keidel

fix pcf and while analyses

parent a81e1636
Pipeline #26907 canceled with stages
in 17 minutes and 58 seconds
......@@ -34,6 +34,7 @@ import Control.Arrow.Fix
import Control.Arrow.Order
import Control.Arrow.Utils
import Data.Abstract.Widening (Widening)
import Data.Abstract.Closure (Closure)
import qualified Data.Abstract.Closure as Cls
......@@ -48,7 +49,7 @@ import Data.Profunctor.Unsafe((.#))
import Data.Coerce
type Alloc var addr val c = EnvT var addr val c (var,val) addr
newtype EnvT var addr val c x y = EnvT (ConstT (Alloc var addr val c) (ReaderT (HashMap var addr) (StateT (HashMap addr val) c)) x y)
newtype EnvT var addr val c x y = EnvT (ConstT (Alloc var addr val c, Widening val) (ReaderT (HashMap var addr) (StateT (HashMap addr val) c)) x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowTrans, ArrowLowerBounded,
ArrowFail e, ArrowExcept e, ArrowStore var' val', ArrowRun, ArrowCont,
ArrowContext ctx)
......@@ -61,16 +62,16 @@ instance (Identifiable var, Identifiable addr, Complete val, ArrowEffectCommutat
case do { addr <- Map.lookup var env; Map.lookup addr store } of
P.Just val -> f -< (val,x)
P.Nothing -> g -< x
extend (EnvT f) = EnvT $ askConst $ \(EnvT alloc) -> proc (var,val,x) -> do
extend (EnvT f) = EnvT $ askConst $ \(EnvT alloc,widening) -> proc (var,val,x) -> do
env <- Reader.ask -< ()
store <- State.get -< ()
case Map.lookup var env of
P.Just addr -> do
State.put -< Map.insertWith () addr val store
State.put -< Map.insertWith (\old new -> snd (widening old new)) addr val store
f -< x
P.Nothing -> do
addr <- alloc -< (var,val)
State.put -< Map.insertWith () addr val store
State.put -< Map.insertWith (\old new -> snd (widening old new)) addr val store
Reader.local f -< (Map.insert var addr env, x)
{-# INLINE lookup #-}
{-# INLINE extend #-}
......@@ -88,12 +89,12 @@ instance (Identifiable var, Identifiable addr, Identifiable expr, ArrowEffectCom
{-# INLINE apply #-}
instance (Identifiable var, Identifiable addr, Complete val, IsClosure val (HashSet (HashMap var addr)), ArrowEffectCommutative c, ArrowChoice c, Profunctor c) => ArrowLetRec var val (EnvT var addr val c) where
letRec (EnvT f) = EnvT $ askConst $ \(EnvT alloc) -> proc (bindings,x) -> do
letRec (EnvT f) = EnvT $ askConst $ \(EnvT alloc,widening) -> proc (bindings,x) -> do
env <- Reader.ask -< ()
addrs <- map alloc -< bindings
let env' = Map.fromList [ (var,addr) | ((var,_), addr) <- zip bindings addrs ] `Map.union` env
vals = Map.fromList [ (addr, setEnvironment (Set.singleton env') val) | (addr, (_,val)) <- zip addrs bindings ]
State.modify' (\(vals,store) -> ((), vals store)) -< vals
State.modify' (\(vals,store) -> ((), Map.unionWith (\old new -> snd (widening old new)) store vals)) -< vals
Reader.local f -< (env',x)
{-# INLINE letRec #-}
......
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
......@@ -73,17 +74,24 @@ withBounds1 f (Interval i1 i2) = Interval (min (f i1) (f i2)) (max (f i1) (f i2)
withBounds2 :: Ord n => (n -> n -> n) -> Interval n -> Interval n -> Interval n
withBounds2 f (Interval i1 i2) (Interval j1 j2) =
Interval (minimum [ f x y | x <- [i1,i2], y <- [j1,j2]])
Interval (minimum [ f x y | x <- [i1,i2], y <- [j1,j2]])
(maximum [ f x y | x <- [i1,i2], y <- [j1,j2]])
instance (Ord n, Bounded n) => UpperBounded (Interval n) where
top = Interval minBound maxBound
widening :: Ord n => Widening (Interval (InfiniteNumber n))
widening (Interval i1 i2) (Interval j1 j2) =
widening :: Ord n => Interval n -> Widening (Interval (InfiniteNumber n))
widening (Interval lowerBound upperBound) (Interval i1 i2) (Interval j1 j2) =
(if j1 P./= i1 || j2 P./= i2 then Unstable else Stable,
Interval (if j1 P./= i1 then NegInfinity else j1)
(if j2 P./= i2 then Infinity else i2))
Interval (if | lower P.< Number lowerBound -> NegInfinity
| Number upperBound P.< lower -> Number upperBound
| otherwise -> lower)
(if | Number upperBound P.< upper -> Infinity
| upper P.< Number lowerBound -> Number lowerBound
| otherwise -> upper))
where
lower = min i1 j1
upper = max i2 j2
metric :: Metric m n -> Metric (Interval m) (Product n n)
metric m (Interval i1 i2) (Interval j1 j2) = Product (m i1 j1) (m i2 j2)
......
......@@ -9,6 +9,7 @@ import Data.Order
import Data.Abstract.FreeCompletion
import Control.Monad.State
import Control.DeepSeq
import Text.Printf
-- Retrieves label from expression.
class HasLabel x where
......@@ -18,7 +19,7 @@ newtype Label = Label { labelVal :: Int }
deriving (Ord,Eq,Hashable,Num,NFData)
instance Show Label where
show (Label l) = show l
show (Label l) = printf "#%d" l
instance PreOrd Label where
() = (==)
......
......@@ -19,8 +19,10 @@ module IntervalAnalysis where
import Prelude hiding (Bounded,fail,(.),exp)
import Control.Category
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Environment(extend')
import Control.Arrow.Fix
import Control.Arrow.Fix.Combinator as Fix
import qualified Control.Arrow.Fix.Context as Ctx
......@@ -35,7 +37,7 @@ 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.Cache
import Control.Arrow.Transformer.Abstract.Fix.Cache(CacheT,Cache,Monotone,type (**),Group)
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Monad.State hiding (lift,fail)
......@@ -90,9 +92,9 @@ type Out = (Store, Terminating (Error (Pow String) Val))
-- | Run the abstract interpreter for an interval analysis. The arguments are the
-- maximum interval bound, the depth @k@ of the longest call string,
-- an environment, and the input of the computation.
evalInterval :: (?sensitivity :: Int, ?bound :: IV) => [(Text,Val)] -> State Label Expr -> (Store, Terminating (Error (Pow String) Val))
evalInterval :: (?sensitivity :: Int, ?bound :: Interval Int) => [(Text,Val)] -> State Label Expr -> (Store, Terminating (Error (Pow String) Val))
evalInterval env0 e = snd $
run (Generic.eval ::
run (extend' (Generic.eval ::
Fix'
(ValueT Val
(ErrorT (Pow String)
......@@ -102,25 +104,30 @@ evalInterval env0 e = snd $
(ChaoticT In
(StackT Stack In
(CacheT (Monotone ** Group Cache) In Out
(ContextT Ctx In
(->)))))))))) Expr Val)
alloc
(ContextT Ctx
(->)))))))))) Expr Val))
(alloc, widenVal)
iterationStrategy
(widenStore widenVal, T.widening (E.widening W.finite widenVal))
(Map.empty,(Map.empty,e0))
(Map.empty,(Map.empty,(env0,e0)))
where
e0 = generate e
alloc = proc (var,val) -> do
ctx <- Ctx.askContext @Ctx @In -< ()
alloc = proc (var,_) -> do
ctx <- Ctx.askContext @Ctx -< ()
returnA -< (var,ctx)
iterationStrategy =
Fix.filter apply
Fix.iterateInner
-- Fix.traceShow .
Fix.recordCallsite ?sensitivity (\(_,(_,expr)) -> case expr of App _ _ l -> Just l; _ -> Nothing) .
Fix.filter apply Fix.iterateInner
widenVal :: Widening Val
widenVal = widening (W.bounded ?bound I.widening)
widenVal = widening (I.widening ?bound)
evalInterval' :: (?sensitivity :: Int, ?bound :: Interval Int) => [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow String) Val)
evalInterval' env expr = snd $ evalInterval env expr
{-# INLINE evalInterval' #-}
instance (IsString e, ArrowChoice c, ArrowFail e c) => IsVal Val (ValueT Val c) where
type Join y (ValueT Val c) = ArrowComplete y (ValueT Val c)
......
......@@ -3,11 +3,12 @@
{-# LANGUAGE OverloadedStrings #-}
module IntervalAnalysisSpec where
import Prelude hiding (succ,pred)
import Prelude hiding (succ,pred,id)
import Data.Abstract.DiscretePowerset(Pow)
import Data.Abstract.Error hiding (toEither)
import qualified Data.Abstract.Interval as I
import Data.Abstract.InfiniteNumbers
import Data.Abstract.Terminating hiding (toEither)
import Test.Hspec
......@@ -24,41 +25,50 @@ main = hspec spec
spec :: Spec
spec = do
let ?bound = I.Interval (-100) 100; ?sensitivity = 3 in sharedSpec (toEither . evalInterval []) (NumVal . fromIntegral)
let ?bound = I.Interval (-100) 100; ?sensitivity = 3 in sharedSpec (toEither . evalInterval' []) (NumVal . fromIntegral)
describe "behavior specific to interval analysis" $ do
it "should execute both branches on IfZero on interval containing zero" $
let ?bound = I.Interval (-100) 100
?sensitivity = 1
in evalInterval [("x", num (-5) 5)]
in evalInterval' [("x", num (-5) 5)]
(ifZero "x" (succ zero) (pred zero))
`shouldBe` Terminating (Success (num (-1) 1))
it "should compute 0 + -1 + 1 = 0" $
let ?bound = I.Interval (-100) 100
?sensitivity = 1
in evalInterval [] (succ (pred zero)) `shouldBe`
in evalInterval' [] (succ (pred zero)) `shouldBe`
Terminating (Success (num 0 0))
it "should analyse addition correctly" $
let ?bound = I.Interval 0 5
?sensitivity = 2
in do
evalInterval [] (let_ [("add",add)] (app "add" [zero,two])) `shouldBe` Terminating (Success (num 2 2))
pendingWith "Flat environments are imprecise: they are widened immediately and not with a widening operator."
evalInterval [] (let_ [("add",add)] (app "add" [one,two])) `shouldBe` Terminating (Success (num 3 3))
evalInterval [("x", num 0 1)] (let_ [("add",add)] (app "add" ["x",two])) `shouldBe` Terminating (Success (num 2 3))
evalInterval' [] (let_ [("add",add)] (app "add" [zero,two])) `shouldBe` Terminating (Success (num 2 2))
evalInterval' [] (let_ [("add",add)] (app "add" [one,two])) `shouldBe` Terminating (Success (num 3 3))
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 Infinity))
it "context sensitivity" $
let diamond = let_ [("second",second),("id",id)] (app "second" [app "id" [one],app "id" [two]]) in
let ?bound = I.Interval 0 5 in do
let ?sensitivity = 0 in evalInterval' [] diamond `shouldBe` Terminating (Success (num 1 2))
let ?sensitivity = 1 in evalInterval' [] diamond `shouldBe` Terminating (Success (num 2 2))
it "should terminate for the non-terminating program" $
let ?bound = I.Interval 0 5
?sensitivity = 2
in evalInterval [] (let_ [("id", lam ["x"] "x"),
in evalInterval' [] (let_ [("id", lam ["x"] "x"),
("fix",lam ["x"] (app "fix" ["x"]))]
(app "fix" ["id"]))
`shouldBe` NonTerminating
where
id = lam ["x"] "x"
second = lam ["_","y"] "y"
add = lam ["x","y"] $ ifZero "x" "y" (succ (app "add" [pred "x","y"]))
one = succ zero
......
......@@ -40,7 +40,7 @@ import Control.Arrow.Transformer.Abstract.Except
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.Cache
import Control.Arrow.Transformer.Abstract.Fix.Cache hiding (Widening)
import Control.Arrow.Transformer.Abstract.Fix.Stack
import Control.Arrow.Transformer.Abstract.Store
import Control.Arrow.Transformer.Abstract.Terminating
......@@ -93,7 +93,7 @@ newtype Exception = Exception (Map Text Val) deriving (PreOrd,Complete,Show,Eq)
-- 'Generic.run' with the components for fixpoint computation
-- ('FixT'), termination ('TerminatingT'), failure ('ErrorT'), store
-- ('StoreT'), environments ('EnvT'), and values ('IntervalT').
run :: (?bound :: IV) => Int -> [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (Except Exception (M.Map Addr Val)))
run :: (?bound :: Interval Int) => Int -> [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (Except Exception (M.Map Addr Val)))
run k env ss = fmap (fmap (fmap fst)) <$> snd $
Trans.run
(Generic.run ::
......@@ -107,19 +107,19 @@ run k env ss = fmap (fmap (fmap fst)) <$> snd $
(FixT _ _
(ChaoticT _
(StackT Stack _
(CacheT (Group Cache) (_,_) _
(ContextT (CallString _) _
(CacheT (Context (Proj2 (CtxCache (CallString lab))) (Group Cache)) (_,_) _
(ContextT (CallString _)
(->)))))))))))) [Statement] ())
iterationStrategy
widenResult
(widenEnvStore,widenResult)
(M.empty,(SM.fromList env, generate (sequence ss)))
where
iterationStrategy = Fix.filter whileLoops
$ Fix.callsiteSensitive @(((Expr,Statement,Label),[Statement]),(_,_)) k (thrd . fst . fst) widenEnvStore
$ Fix.callsiteSensitive @(((Expr,Statement,Label),[Statement]),(_,_)) k (thrd . fst . fst)
. Fix.iterateInner
widenEnvStore = M.widening widenVal W.** SM.widening W.finite
widenVal = widening (W.bounded ?bound I.widening)
widenVal = widening (I.widening ?bound)
widenExc (Exception m1) (Exception m2) = Exception <$> M.widening widenVal m1 m2
widenResult = T.widening $ E.widening W.finite (Exc.widening widenExc (M.widening widenVal W.** W.finite))
thrd (_,_,z) = z
......
......@@ -52,12 +52,14 @@ import Control.Arrow.Transformer.Abstract.Fix.Context
import Control.Arrow.Transformer.Abstract.Fix.Cache
import Control.Arrow.Transformer.Abstract.Fix.Stack
type FixCache lab = Context (Proj2 (CtxCache (CallString lab))) (Group Cache)
-- | Calculates the entry sets of which definitions may be reached for
-- each statment. The analysis instantiates the generic interpreter
-- 'Generic.run' with analysis components for fixpoint computation
-- ('FixT'), termination ('TerminatingT'), failure ('ErrorT'), store
-- ('StoreT'), environments ('EnvT'), and values ('IntervalT')
run :: (?bound :: IV) => Int -> [LStatement] -> [(Label, M.Map Text (Pow Label))]
run :: (?bound :: I.Interval Int) => Int -> [LStatement] -> [(Label, M.Map Text (Pow Label))]
run k lstmts =
L.sortOn fst $
......@@ -88,11 +90,11 @@ run k lstmts =
(FixT _ _
(ChaoticT _
(StackT Stack _
(CacheT (Group Cache) (_,_) _
(ContextT (CallString _) _
(CacheT (FixCache lab) (_,_) _
(ContextT (CallString _)
(->))))))))))))) [Statement] ())
iterationStrategy
widenResult
(widenEnvStore, widenResult)
(M.empty,(SM.empty,stmts))
where
......@@ -100,12 +102,12 @@ run k lstmts =
iterationStrategy = Fix.transform (iso' (\(store,(env,stmt)) -> (stmt,(env,store)))
(\(stmt,(env,store)) -> (store,(env,stmt))))
$ Fix.reuseExact
. Fix.callsiteSensitive' @([Statement],(_,_)) k (statementLabel . fst) widenEnvStore
. Fix.callsiteSensitive' @([Statement],(_,_)) k (statementLabel . fst)
. Fix.iterateInner
statementLabel st = case st of (s:_) -> Just (label s); [] -> Nothing
widenEnvStore = SM.widening W.finite W.** M.widening (widenVal W.** W.finite)
widenVal = widening (W.bounded ?bound I.widening)
widenVal = widening (I.widening ?bound)
widenExc (Exception m1) (Exception m2) = Exception <$> M.widening widenVal m1 m2
widenResult = T.widening $ E.widening W.finite (Exc.widening widenExc (M.widening (widenVal W.** W.finite) W.** W.finite))
......@@ -116,9 +118,10 @@ combineMaps env store = M.fromList [ (a,c) | (a,b) <- fromJust (SM.toList env)
dropValues :: M.Map a (v,l) -> M.Map a l
dropValues = M.map snd
toMap :: (Identifiable k, Identifiable a) => Group Cache (k,a) b -> HashMap (k,a) (Stable,b)
toMap (Groups groups) = Map.fromList [ ((k,a),(s,b)) | (k,Cache cache) <- Map.toList groups
, (a,(s,b)) <- Map.toList cache ]
toMap :: (Identifiable k, Identifiable a) => FixCache lab (k,a) b -> HashMap (k,a) (Stable,b)
toMap (Context _ (Groups groups)) =
Map.fromList [ ((k,a),(s,b)) | (k,Cache cache) <- Map.toList groups
, (a,(s,b)) <- Map.toList cache ]
joinOnKey :: (Identifiable k',Complete v') => (k -> v -> Maybe (k',v')) -> HashMap k v -> HashMap k' v'
joinOnKey pred = Map.foldlWithKey' (\m k v -> case pred k v of
......
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