Commit 9aa77196 authored by Sven Keidel's avatar Sven Keidel

fix PCF

parent d27a4be2
......@@ -23,13 +23,15 @@ 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.Environment
import Control.Arrow.Transformer.Abstract.Contour
import Control.Arrow.Transformer.Abstract.BoundedEnvironment
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Terminating
......@@ -42,8 +44,7 @@ import Data.Text (Text)
import Data.Profunctor
import qualified Data.Lens as L
import Data.Abstract.WeakMap(Map)
import qualified Data.Abstract.WeakMap as M
import qualified Data.Abstract.FiniteMap as F
import Data.Abstract.Error (Error)
import qualified Data.Abstract.Error as E
import Data.Abstract.InfiniteNumbers
......@@ -53,65 +54,65 @@ 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 Data.Abstract.Closure(Closure)
import Data.Abstract.Closure (Closure)
import qualified Data.Abstract.Closure as C
import Data.Abstract.DiscretePowerset (Pow)
import GHC.Generics(Generic)
import GHC.Exts(IsString(..))
import Syntax (Expr(..))
import GenericInterpreter
type Env = Map Text Val
data Val = NumVal IV | ClosureVal (Closure Expr Env) | Top deriving (Eq, Generic)
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 ()
type Env = F.Map Text (Text, CallString Label) Val
widening :: W.Widening IV -> W.Widening Val
widening w (NumVal x) (NumVal y) = second NumVal (x `w` y)
widening w (ClosureVal cs) (ClosureVal cs') = second ClosureVal $ C.widening (M.widening (widening w)) cs cs'
widening _ Top Top = (W.Stable,Top)
widening _ _ _ = (W.Instable,Top)
-- | Numeric values are approximated with bounded intervals, closure
-- values are approximated with a set of abstract closures.
data Val = NumVal IV | ClosureVal (Closure Expr Env) | Top deriving (Eq, Generic)
instance UpperBounded Val where
top = Top
-- | Addresses for this analysis are variables paired with the k-bounded call string.
type Addr = (Text,CallString Label)
-- | The abstract interpreter for Interval analysis.
-- | 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 (Error (Pow String) Val)
evalInterval k env0 e =
evalInterval k env0 e = -- runInterp eval ?bound k env (generate e)
runFixT stackWiden (T.widening (E.widening W.finite widenVal))
(runTerminatingT
(runErrorT
(runEnvT
(runIntervalT
(eval ::
Fix Expr Val
(IntervalT
(EnvT Text Val
(ErrorT (Pow String)
(TerminatingT
(FixT _ () () (->)))))) Expr Val)))))
(M.fromList env0,generate e)
(runContourT k
(runEnvT alloc
(runIntervalT
(eval ::
Fix Expr Val
(IntervalT
(EnvT Text Addr Val
(ContourT Label
(ErrorT (Pow 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.reuseFirst
$ SW.maxSize k
$ SW.fromWidening (M.widening widenVal)
widenVal = widening (W.bounded ?bound I.widening)
$ SW.maxSize 3
$ 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 (IsString e, ArrowChoice c, ArrowFail e c, ArrowJoin c) => IsVal Val (IntervalT c) where
succ = proc x -> case x of
......@@ -135,13 +136,34 @@ instance (IsString e, ArrowChoice c, ArrowJoin c, ArrowFail e c) => ArrowCond Va
(ClosureVal _, _) -> fail -< "Expected a number as condition for 'ifZero'"
instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowJoin c)
=> IsClosure Val (Map Text Val) (IntervalT c) where
=> IsClosure Val (F.Map Text Addr Val) (IntervalT c) where
closure = arr $ \(e, env) -> ClosureVal (C.closure e env)
applyClosure f = proc (fun, arg) -> case fun of
Top -> (returnA -< Top) <> (fail -< "Expected a closure")
ClosureVal cls -> (| C.apply (\(e,env) -> f -< ((e,env),arg)) |) 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 cs) (ClosureVal cs') =
second ClosureVal $ C.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 Val
instance Show Val where
......@@ -150,12 +172,3 @@ instance Show Val where
show Top = "⊤"
type IV = Interval (InfiniteNumber Int)
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
{-# 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)
......@@ -39,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 3))
evalInterval 10 [("x", num 0 1)] (app (app add "x") two) `shouldBe` Terminating (Success (num 2 6))
it "should terminate for the non-terminating program" $
let ?bound = I.Interval 0 5
......
{-# 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