Commit 8e1a89ba authored by Sven Keidel's avatar Sven Keidel

create new control-flow analysis for PCF that does not use contours

parent c1e59648
......@@ -42,7 +42,7 @@ runEnvT = unlift
runEnvT' :: (Arrow c, Profunctor c, Identifiable var) => EnvT var val c x y -> c ([(var,val)],x) y
runEnvT' f = first M.fromList ^>> runEnvT f
instance (Show var, Identifiable var, ArrowChoice c,Profunctor c) => ArrowEnv var val (Map var val) (EnvT var val c) where
instance (Identifiable var, ArrowChoice c,Profunctor c) => ArrowEnv var val (Map var val) (EnvT var val c) where
type Join (EnvT var val c) x y = (Complete (c (Map var val,x) y))
lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- ask -< ()
......
......@@ -15,8 +15,10 @@ import Control.Arrow.Conditional as Cond
import Data.Text (Text)
import GHC.Exts(IsString(..))
-- | Shared interpreter for PCF.
eval :: (ArrowChoice c, ArrowFix Expr v c, ArrowEnv Text v env c, ArrowFail String c,
eval :: (ArrowChoice c, ArrowFix Expr v c, ArrowEnv Text v env c, ArrowFail e c, IsString e,
ArrowCond v c, IsVal v c, IsClosure v env c, Env.Join c ((v,Text),Text) v, Cond.Join c (Expr,Expr) v)
=> c Expr v
eval = fix $ \ev -> proc e0 -> case e0 of
......@@ -43,16 +45,17 @@ eval = fix $ \ev -> proc e0 -> case e0 of
env <- getEnv -< ()
arg <- closure -< (Y e l, env)
applyClosure' ev -< (fun, arg)
Apply e _ -> ev -< e
where
-- Helper function used to apply closure or a suspended fixpoint computation to its argument.
applyClosure' ev = applyClosure $ proc ((e,env),arg) -> case e of
Lam x body _ -> do
Lam x body l -> do
env' <- extendEnv -< (x,arg,env)
localEnv ev -< (env', body)
localEnv ev -< (env', Apply body l)
Y e' l -> do
fun' <- localEnv ev -< (env, Y e' l)
applyClosure' ev -< (fun',arg)
_ -> fail -< "found unexpected epxression in closure: " ++ show e
_ -> fail -< fromString $ "found unexpected epxression in closure: " ++ show e
-- | Interface for numeric operations
class Arrow c => IsVal v c | c -> v where
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
......@@ -10,6 +9,7 @@
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeOperators #-}
......@@ -23,7 +23,6 @@ import Prelude hiding (Bounded,fail,(.),exp)
import Control.Category
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Trans
......@@ -31,8 +30,8 @@ import Control.Arrow.Conditional as Cond
import Control.Arrow.Environment
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Abstract.Contour
import Control.Arrow.Transformer.Abstract.BoundedEnvironment
import Control.Arrow.Transformer.Abstract.Failure
import Control.Arrow.Transformer.Abstract.Environment
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Monad.State hiding (lift,fail)
......@@ -46,9 +45,8 @@ import qualified Data.Lens as L
import Data.Abstract.Map(Map)
import qualified Data.Abstract.Map as M
import qualified Data.Abstract.FiniteMap as F
import Data.Abstract.Failure (Failure)
import qualified Data.Abstract.Failure as E
import Data.Abstract.Error (Error)
import qualified Data.Abstract.Error as E
import Data.Abstract.InfiniteNumbers
import Data.Abstract.Interval (Interval)
import qualified Data.Abstract.Interval as I
......@@ -56,9 +54,10 @@ import qualified Data.Abstract.Widening as W
import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating(Terminating)
import qualified Data.Abstract.Terminating as T
import Data.Abstract.DiscretePowerset(Pow)
import GHC.Generics(Generic)
import GHC.Exts(toList)
import GHC.Exts(IsString(..),toList)
import Syntax (Expr(..))
import GenericInterpreter
......@@ -66,9 +65,9 @@ import GenericInterpreter
-- | Abstract closures are expressions paired with an abstract
-- environment, consisting of a mapping from variables to addresses
-- and a mapping from addresses to stores.
newtype Closure = Closure (Map Expr (F.Map Text Addr Val)) deriving (Eq,Generic,PreOrd,Complete,Show)
newtype Closure = Closure (Map Expr (Map Text Val)) deriving (Eq,Generic,PreOrd,Complete,Show)
type Env = F.Map Text (Text, CallString Label) Val
type Env = Map Text Val
-- | Numeric values are approximated with bounded intervals, closure
-- values are approximated with a set of abstract closures.
......@@ -80,32 +79,30 @@ type Addr = (Text,CallString Label)
-- | Run the abstract interpreter for the k-CFA / 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 :: (?bound :: IV) => Int -> [(Text,Val)] -> State Label Expr -> Terminating (Failure String Val)
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 widenVal))
runFixT stackWiden (T.widening (E.widening W.finite widenVal))
(runTerminatingT
(runFailureT
(runContourT k
(runEnvT alloc
(runIntervalT
(eval ::
Fix Expr Val
(IntervalT
(EnvT Text Addr Val
(ContourT Label
(FailureT String
(TerminatingT
(FixT _ () () (->))))))) Expr Val))))))
(env0,generate e)
(runErrorT
(runEnvT
(runIntervalT
(eval ::
Fix Expr Val
(IntervalT
(EnvT Text Val
(ErrorT (Pow String)
(TerminatingT
(FixT _ () () (->)))))) Expr Val)))))
(M.fromList env0,generate e)
where
widenVal = widening (W.bounded ?bound I.widening)
stackWiden :: SW.StackWidening _ (Env,Expr)
stackWiden = SW.filter (\(_,ex) -> case ex of App {} -> True; Y {} -> True; _ -> False)
stackWiden = SW.filter (\(_,ex) -> case ex of Apply {} -> True; _ -> False)
$ SW.groupBy (L.iso' (\(env,exp) -> (exp,env)) (\(exp,env) -> (env,exp)))
$ SW.stack
$ SW.maxSize 3
$ SW.reuseFirst
$ SW.fromWidening (F.widening widenVal)
$ SW.maxSize k
$ SW.fromWidening (M.widening widenVal)
newtype IntervalT c x y = IntervalT { runIntervalT :: c x y } deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowFail e,ArrowJoin)
type instance Fix x y (IntervalT c) = IntervalT (Fix x y c)
......@@ -118,7 +115,7 @@ instance ArrowTrans IntervalT where
lift = IntervalT
unlift = runIntervalT
instance (ArrowChoice c, ArrowFail String c, ArrowJoin c) => IsVal Val (IntervalT c) where
instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowJoin c) => IsVal Val (IntervalT c) where
succ = proc x -> case x of
Top -> (returnA -< NumVal top) <> (fail -< "Expected a number as argument for 'succ'")
NumVal n -> returnA -< NumVal $ n + 1 -- uses the `Num` instance of intervals
......@@ -129,7 +126,7 @@ instance (ArrowChoice c, ArrowFail String c, ArrowJoin c) => IsVal Val (Interval
ClosureVal _ -> fail -< "Expected a number as argument for 'pred'"
zero = proc _ -> returnA -< (NumVal 0)
instance (ArrowChoice c, ArrowJoin c, ArrowFail String c) => ArrowCond Val (IntervalT c) where
instance (IsString e, ArrowChoice c, ArrowJoin c, ArrowFail e c) => ArrowCond Val (IntervalT c) where
type Join (IntervalT c) x y = Complete y
if_ f g = proc v -> case v of
(Top, (x,y)) -> (f -< x) <> (g -< y) <> (fail -< "Expected a number as condition for 'ifZero'")
......@@ -139,8 +136,8 @@ instance (ArrowChoice c, ArrowJoin c, ArrowFail String c) => ArrowCond Val (Inte
| otherwise -> (f -< x) <> (g -< y) -- case the interval contains zero and other numbers.
(ClosureVal _, _) -> fail -< "Expected a number as condition for 'ifZero'"
instance (ArrowChoice c, ArrowFail String c, ArrowJoin c)
=> IsClosure Val (F.Map Text Addr Val) (IntervalT c) where
instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowJoin c)
=> IsClosure Val (Map Text Val) (IntervalT c) where
closure = arr $ \(e, env) -> ClosureVal (Closure [(e,env)])
applyClosure f = proc (fun, arg) -> case fun of
Top -> returnA -< Top
......@@ -162,16 +159,13 @@ instance Complete Val where
widening :: W.Widening IV -> W.Widening Val
widening w (NumVal x) (NumVal y) = second NumVal (x `w` y)
widening w (ClosureVal (Closure cs)) (ClosureVal (Closure cs')) =
second (ClosureVal . Closure) $ M.widening (F.widening (widening w)) cs cs'
second (ClosureVal . Closure) $ M.widening (M.widening (widening w)) cs cs'
widening _ Top Top = (W.Stable,Top)
widening _ _ _ = (W.Instable,Top)
instance UpperBounded Val where
top = Top
instance HasLabel (F.Map Text Addr Val,Expr) Label where
label (_,e) = label e
instance Hashable Closure
instance Hashable Val
instance Show Val where
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-partial-type-signatures #-}
-- | k-CFA analysis for PCF where numbers are approximated by intervals.
module KCFA where
import Prelude hiding (Bounded,fail,(.),exp)
import Control.Category
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Conditional as Cond
import Control.Arrow.Environment
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Abstract.Contour
import Control.Arrow.Transformer.Abstract.BoundedEnvironment
import Control.Arrow.Transformer.Abstract.Failure
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Monad.State hiding (lift,fail)
import Data.Hashable
import Data.Label
import Data.Order
import Data.Text (Text)
import Data.Profunctor
import qualified Data.Lens as L
import Data.Abstract.Map(Map)
import qualified Data.Abstract.Map as M
import qualified Data.Abstract.FiniteMap as F
import Data.Abstract.Failure (Failure)
import qualified Data.Abstract.Failure as E
import Data.Abstract.InfiniteNumbers
import Data.Abstract.Interval (Interval)
import qualified Data.Abstract.Interval as I
import qualified Data.Abstract.Widening as W
import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating(Terminating)
import qualified Data.Abstract.Terminating as T
import GHC.Generics(Generic)
import GHC.Exts(toList)
import Syntax (Expr(..))
import GenericInterpreter
-- | Abstract closures are expressions paired with an abstract
-- environment, consisting of a mapping from variables to addresses
-- and a mapping from addresses to stores.
newtype Closure = Closure (Map Expr (F.Map Text Addr Val)) deriving (Eq,Generic,PreOrd,Complete,Show)
type Env = F.Map Text (Text, CallString Label) Val
-- | Numeric values are approximated with bounded intervals, closure
-- values are approximated with a set of abstract closures.
data Val = NumVal IV | ClosureVal Closure | Top deriving (Eq, Generic)
-- | Addresses for this analysis are variables paired with the k-bounded call string.
type Addr = (Text,CallString Label)
-- | Run the abstract interpreter for the k-CFA / 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 :: (?bound :: IV) => Int -> [(Text,Val)] -> State Label Expr -> Terminating (Failure String Val)
evalInterval k env0 e = -- runInterp eval ?bound k env (generate e)
runFixT stackWiden (T.widening (E.widening widenVal))
(runTerminatingT
(runFailureT
(runContourT k
(runEnvT alloc
(runIntervalT
(eval ::
Fix Expr Val
(IntervalT
(EnvT Text Addr Val
(ContourT Label
(FailureT String
(TerminatingT
(FixT _ () () (->))))))) Expr Val))))))
(env0,generate e)
where
widenVal = widening (W.bounded ?bound I.widening)
stackWiden :: SW.StackWidening _ (Env,Expr)
stackWiden = SW.filter (\(_,ex) -> case ex of Apply {} -> True; _ -> False)
$ SW.groupBy (L.iso' (\(env,exp) -> (exp,env)) (\(exp,env) -> (env,exp)))
$ SW.stack
$ SW.maxSize 3
$ SW.reuseFirst
$ SW.fromWidening (F.widening widenVal)
newtype IntervalT c x y = IntervalT { runIntervalT :: c x y } deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowFail e,ArrowJoin)
type instance Fix x y (IntervalT c) = IntervalT (Fix x y c)
deriving instance ArrowFix x y c => ArrowFix x y (IntervalT c)
deriving instance ArrowEnv var val env c => ArrowEnv var val env (IntervalT c)
instance ArrowTrans IntervalT where
type Dom IntervalT x y = x
type Cod IntervalT x y = y
lift = IntervalT
unlift = runIntervalT
instance (ArrowChoice c, ArrowFail String c, ArrowJoin c) => IsVal Val (IntervalT c) where
succ = proc x -> case x of
Top -> (returnA -< NumVal top) <> (fail -< "Expected a number as argument for 'succ'")
NumVal n -> returnA -< NumVal $ n + 1 -- uses the `Num` instance of intervals
ClosureVal _ -> fail -< "Expected a number as argument for 'succ'"
pred = proc x -> case x of
Top -> (returnA -< NumVal top) <> (fail -< "Expected a number as argument for 'pred'")
NumVal n -> returnA -< NumVal $ n - 1
ClosureVal _ -> fail -< "Expected a number as argument for 'pred'"
zero = proc _ -> returnA -< (NumVal 0)
instance (ArrowChoice c, ArrowJoin c, ArrowFail String c) => ArrowCond Val (IntervalT c) where
type Join (IntervalT c) x y = Complete y
if_ f g = proc v -> case v of
(Top, (x,y)) -> (f -< x) <> (g -< y) <> (fail -< "Expected a number as condition for 'ifZero'")
(NumVal (I.Interval i1 i2), (x, y))
| (i1, i2) == (0, 0) -> f -< x -- case the interval is exactly zero
| i1 > 0 || i2 < 0 -> g -< y -- case the interval does not contain zero
| otherwise -> (f -< x) <> (g -< y) -- case the interval contains zero and other numbers.
(ClosureVal _, _) -> fail -< "Expected a number as condition for 'ifZero'"
instance (ArrowChoice c, ArrowFail String c, ArrowJoin c)
=> IsClosure Val (F.Map Text Addr Val) (IntervalT c) where
closure = arr $ \(e, env) -> ClosureVal (Closure [(e,env)])
applyClosure f = proc (fun, arg) -> case fun of
Top -> returnA -< Top
ClosureVal (Closure cls) ->
-- Apply the interpreter function `f` on all closures and join their results.
(| joinList (returnA -< Top) (\(e,env) -> f -< ((e,env),arg)) |)
(toList cls)
NumVal _ -> fail -< "Expected a closure"
instance PreOrd Val where
_ Top = True
NumVal n1 NumVal n2 = n1 n2
ClosureVal c1 ClosureVal c2 = c1 c2
_ _ = False
instance Complete Val where
() = W.toJoin widening ()
widening :: W.Widening IV -> W.Widening Val
widening w (NumVal x) (NumVal y) = second NumVal (x `w` y)
widening w (ClosureVal (Closure cs)) (ClosureVal (Closure cs')) =
second (ClosureVal . Closure) $ M.widening (F.widening (widening w)) cs cs'
widening _ Top Top = (W.Stable,Top)
widening _ _ _ = (W.Instable,Top)
instance UpperBounded Val where
top = Top
instance HasLabel (F.Map Text Addr Val,Expr) Label where
label (_,e) = label e
instance Hashable Closure
instance Hashable Val
instance Show Val where
show (NumVal iv) = show iv
show (ClosureVal cls) = show cls
show Top = "⊤"
type IV = Interval (InfiniteNumber Int)
......@@ -21,6 +21,7 @@ data Expr
| Pred Expr Label
| IfZero Expr Expr Expr Label
| Y Expr Label
| Apply Expr Label
deriving (Eq)
-- Smart constructors that build labeled PCF expressions.
......@@ -57,6 +58,7 @@ instance Show Expr where
Succ e _ -> showParen (d > app_prec) $ showString "succ " . showsPrec (app_prec + 1) e
Pred e _ -> showParen (d > app_prec) $ showString "pred " . showsPrec (app_prec + 1) e
Y e _ -> showParen (d > app_prec) $ showString "Y " . showsPrec (app_prec + 1) e
Apply e _ -> showParen (d > app_prec) $ showsPrec (app_prec + 1) e
IfZero e1 e2 e3 _ -> showParen (d > app_prec)
$ showString "ifZero "
. showsPrec (app_prec + 1) e1
......@@ -87,6 +89,7 @@ instance HasLabel Expr Label where
Pred _ l -> l
IfZero _ _ _ l -> l
Y _ l -> l
Apply _ l -> l
instance IsString (State Label Expr) where
fromString = var . fromString
......@@ -100,3 +103,4 @@ instance Hashable Expr where
hashWithSalt s (Pred e _) = s `hashWithSalt` (5::Int) `hashWithSalt` e
hashWithSalt s (IfZero e1 e2 e3 _) = s `hashWithSalt` (6::Int) `hashWithSalt` e1 `hashWithSalt` e2 `hashWithSalt` e3
hashWithSalt s (Y e _) = s `hashWithSalt` (7::Int) `hashWithSalt` e
hashWithSalt s (Apply e _) = s `hashWithSalt` (8::Int) `hashWithSalt` e
......@@ -5,12 +5,14 @@ module IntervalAnalysisSpec where
import Prelude hiding (succ,pred)
import SharedSpecs
import Data.Abstract.Failure hiding (toEither)
import Data.Abstract.DiscretePowerset(Pow)
import Data.Abstract.Error hiding (toEither)
import qualified Data.Abstract.Interval as I
import Data.Abstract.Terminating hiding (toEither)
import IntervalAnalysis
import Syntax
import Test.Hspec
import GHC.Exts(toList)
main :: IO ()
main = hspec spec
......@@ -37,7 +39,7 @@ spec = do
in do
evalInterval 10 [] (app (app add zero) two) `shouldBe` Terminating (Success (num 2 2))
evalInterval 10 [] (app (app add one) two) `shouldBe` Terminating (Success (num 3 3))
evalInterval 10 [("x", num 0 1)] (app (app add "x") two) `shouldBe` Terminating (Success (num 2 7))
evalInterval 10 [("x", num 0 1)] (app (app add "x") two) `shouldBe` Terminating (Success (num 2 3))
it "should terminate for the non-terminating program" $
let ?bound = I.Interval 0 5
......@@ -54,7 +56,7 @@ spec = do
num i j = NumVal $ I.Interval i j
toEither :: Terminating (Failure String a) -> Either String a
toEither (Terminating (Fail e)) = Left e
toEither :: Terminating (Error (Pow String) a) -> Either String a
toEither (Terminating (Fail e)) = Left (unwords (toList e))
toEither (Terminating (Success x)) = Right x
toEither NonTerminating = Left "NonTerminating"
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ImplicitParams #-}
module KCFASpec where
import Prelude hiding (succ,pred)
import SharedSpecs
import Data.Abstract.DiscretePowerset(Pow)
import Data.Abstract.Error hiding (toEither)
import qualified Data.Abstract.Interval as I
import Data.Abstract.Terminating hiding (toEither)
import IntervalAnalysis
import Syntax
import Test.Hspec
import GHC.Exts(toList)
main :: IO ()
main = hspec spec
spec :: Spec
spec = do
let ?bound = I.Interval (-100) 100 in
sharedSpec (\env e -> toEither $ evalInterval 3 env e) (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
in evalInterval 3 [("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
in evalInterval 3 [] (succ (pred zero)) `shouldBe`
Terminating (Success (num 0 0))
it "should analyse addition correctly" $
let ?bound = I.Interval 0 5
in do
evalInterval 10 [] (app (app add zero) two) `shouldBe` Terminating (Success (num 2 2))
evalInterval 10 [] (app (app add one) two) `shouldBe` Terminating (Success (num 3 3))
evalInterval 10 [("x", num 0 1)] (app (app add "x") two) `shouldBe` Terminating (Success (num 2 3))
it "should terminate for the non-terminating program" $
let ?bound = I.Interval 0 5
in do evalInterval 5 [] (fix (lam "x" "x")) `shouldSatisfy`
\c -> case c of Terminating (Success (ClosureVal _)) -> True; _ -> False
evalInterval 5 [] (fix (lam "f" (lam "x" (app "f" "x")))) `shouldSatisfy`
\c -> case c of Terminating (Success (ClosureVal _)) -> True; _ -> False
where
add = fix $ lam "add" $ lam "x" $ lam "y" $ ifZero "x" "y" (succ (app (app "add" (pred "x")) "y"))
one = succ zero
two = succ one
num i j = NumVal $ I.Interval i j
toEither :: Terminating (Error (Pow String) a) -> Either String a
toEither (Terminating (Fail e)) = Left (unwords (toList e))
toEither (Terminating (Success x)) = Right x
toEither NonTerminating = Left "NonTerminating"
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