Commit d27a4be2 authored by Sven Keidel's avatar Sven Keidel

extract abstract closures into library

parent 8e1a89ba
...@@ -33,5 +33,11 @@ joinList empty f = proc (e,(l,s)) -> case l of ...@@ -33,5 +33,11 @@ joinList empty f = proc (e,(l,s)) -> case l of
[x] -> f -< (e,(x,s)) [x] -> f -< (e,(x,s))
(x:xs) -> (f -< (e,(x,s))) <> (joinList empty f -< (e,(xs,s))) (x:xs) -> (f -< (e,(x,s))) <> (joinList empty f -< (e,(xs,s)))
joinList1 :: (ArrowChoice c, ArrowJoin c, Complete y) => c (e,(x,s)) y -> c (e,([x],s)) y
joinList1 f = proc (e,(l,s)) -> case l of
[] -> returnA -< error "empty list"
[x] -> f -< (e,(x,s))
(x:xs) -> (f -< (e,(x,s))) <> (joinList1 f -< (e,(xs,s)))
instance ArrowJoin (->) where instance ArrowJoin (->) where
joinWith lub f g = \x -> lub (f x) (g x) joinWith lub f g = \x -> lub (f x) (g x)
...@@ -13,8 +13,8 @@ import Prelude hiding ((.),read,Maybe(..)) ...@@ -13,8 +13,8 @@ import Prelude hiding ((.),read,Maybe(..))
import Data.Order import Data.Order
import Data.Identifiable import Data.Identifiable
import Data.Abstract.Maybe import Data.Abstract.Maybe
import Data.Abstract.Map (Map) import Data.Abstract.WeakMap (Map)
import qualified Data.Abstract.Map as M import qualified Data.Abstract.WeakMap as M
import Control.Category import Control.Category
import Control.Arrow import Control.Arrow
...@@ -42,11 +42,11 @@ runEnvT = unlift ...@@ -42,11 +42,11 @@ runEnvT = unlift
runEnvT' :: (Arrow c, Profunctor c, Identifiable var) => EnvT var val c x y -> c ([(var,val)],x) y 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 runEnvT' f = first M.fromList ^>> runEnvT f
instance (Identifiable var, ArrowChoice c,Profunctor c) => ArrowEnv var val (Map var val) (EnvT var val c) where instance (Identifiable var, UpperBounded val, 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)) 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 lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- ask -< () env <- ask -< ()
case M.lookup var env of case M.lookup' var env of
Just val -> f -< (val,x) Just val -> f -< (val,x)
JustNothing val -> joined f g -< ((val,x),x) JustNothing val -> joined f g -< ((val,x),x)
Nothing -> g -< x Nothing -> g -< x
......
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Data.Abstract.Closure(Closure,closure,apply,widening) where
import Control.DeepSeq
import Control.Arrow
import Control.Arrow.Abstract.Join
import Data.Profunctor
import Data.HashMap.Lazy(HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Hashable(Hashable)
import Data.Identifiable
import Data.Order
import Data.Coerce
import Data.Abstract.Widening
import Data.Foldable
import Text.Printf
newtype Closure expr env = Closure (HashMap expr env)
deriving (Eq,Hashable,NFData)
instance (Identifiable expr, PreOrd env) => PreOrd (Closure expr env) where
() = withCls $ \m1 m2 -> and $ M.intersectionWith () m1 m2
instance (Identifiable expr, Complete env) => Complete (Closure expr env) where
() = withCls $ M.unionWith ()
instance (Show a,Show b) => Show (Closure a b) where
show (Closure h)
| M.null h = "{}"
| otherwise = "{" ++ init (unwords [ printf "%s -> %s," (show k) (show v) | (k,v) <- M.toList h]) ++ "}"
closure :: Identifiable expr => expr -> env -> Closure expr env
closure expr env = Closure $ M.singleton expr env
apply :: (ArrowJoin c, ArrowChoice c, Profunctor c, Complete y)
=> c (e,((expr,env),s)) y -> c (e,(Closure expr env,s)) y
apply f = lmap (second $ first $ withCls M.toList) (joinList1 f)
widening :: Identifiable expr => Widening env -> Widening (Closure expr env)
widening w = withCls $ \m1 m2 ->
(fold $ M.intersectionWith (\x y -> fst (w x y)) m1 m2,
M.unionWith (\x y -> snd (w x y)) m1 m2)
withCls :: Coercible x x' => (HashMap expr env -> x') -> (Closure expr env -> x)
withCls = coerce
{-# INLINE withCls #-}
...@@ -29,7 +29,6 @@ import Control.Arrow.Trans ...@@ -29,7 +29,6 @@ import Control.Arrow.Trans
import Control.Arrow.Conditional as Cond import Control.Arrow.Conditional as Cond
import Control.Arrow.Environment import Control.Arrow.Environment
import Control.Arrow.Abstract.Join import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Abstract.Contour
import Control.Arrow.Transformer.Abstract.Environment import Control.Arrow.Transformer.Abstract.Environment
import Control.Arrow.Transformer.Abstract.Error import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Fix import Control.Arrow.Transformer.Abstract.Fix
...@@ -43,8 +42,8 @@ import Data.Text (Text) ...@@ -43,8 +42,8 @@ import Data.Text (Text)
import Data.Profunctor import Data.Profunctor
import qualified Data.Lens as L import qualified Data.Lens as L
import Data.Abstract.Map(Map) import Data.Abstract.WeakMap(Map)
import qualified Data.Abstract.Map as M import qualified Data.Abstract.WeakMap as M
import Data.Abstract.Error (Error) import Data.Abstract.Error (Error)
import qualified Data.Abstract.Error as E import qualified Data.Abstract.Error as E
import Data.Abstract.InfiniteNumbers import Data.Abstract.InfiniteNumbers
...@@ -55,47 +54,53 @@ import qualified Data.Abstract.StackWidening as SW ...@@ -55,47 +54,53 @@ import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating(Terminating) import Data.Abstract.Terminating(Terminating)
import qualified Data.Abstract.Terminating as T import qualified Data.Abstract.Terminating as T
import Data.Abstract.DiscretePowerset(Pow) import Data.Abstract.DiscretePowerset(Pow)
import Data.Abstract.Closure(Closure)
import qualified Data.Abstract.Closure as C
import GHC.Generics(Generic) import GHC.Generics(Generic)
import GHC.Exts(IsString(..),toList) import GHC.Exts(IsString(..))
import Syntax (Expr(..)) import Syntax (Expr(..))
import GenericInterpreter 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 (Map Text Val)) deriving (Eq,Generic,PreOrd,Complete,Show)
type Env = Map Text Val 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
-- | Numeric values are approximated with bounded intervals, closure instance Complete Val where
-- values are approximated with a set of abstract closures. () = W.toJoin widening ()
data Val = NumVal IV | ClosureVal Closure | Top deriving (Eq, Generic)
-- | Addresses for this analysis are variables paired with the k-bounded call string. widening :: W.Widening IV -> W.Widening Val
type Addr = (Text,CallString Label) 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)
-- | Run the abstract interpreter for the k-CFA / Interval analysis. The arguments are the instance UpperBounded Val where
-- maximum interval bound, the depth @k@ of the longest call string, top = Top
-- an environment, and the input of the computation.
-- | The abstract interpreter for Interval analysis.
evalInterval :: (?bound :: IV) => Int -> [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow 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) evalInterval k env0 e =
runFixT stackWiden (T.widening (E.widening W.finite widenVal)) runFixT stackWiden (T.widening (E.widening W.finite widenVal))
(runTerminatingT (runTerminatingT
(runErrorT (runErrorT
(runEnvT (runEnvT
(runIntervalT (runIntervalT
(eval :: (eval ::
Fix Expr Val Fix Expr Val
(IntervalT (IntervalT
(EnvT Text Val (EnvT Text Val
(ErrorT (Pow String) (ErrorT (Pow String)
(TerminatingT (TerminatingT
(FixT _ () () (->)))))) Expr Val))))) (FixT _ () () (->)))))) Expr Val)))))
(M.fromList env0,generate e) (M.fromList env0,generate e)
where where
widenVal = widening (W.bounded ?bound I.widening)
stackWiden :: SW.StackWidening _ (Env,Expr) stackWiden :: SW.StackWidening _ (Env,Expr)
stackWiden = SW.filter (\(_,ex) -> case ex of Apply {} -> 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.groupBy (L.iso' (\(env,exp) -> (exp,env)) (\(exp,env) -> (env,exp)))
...@@ -104,16 +109,9 @@ evalInterval k env0 e = -- runInterp eval ?bound k env (generate e) ...@@ -104,16 +109,9 @@ evalInterval k env0 e = -- runInterp eval ?bound k env (generate e)
$ SW.maxSize k $ SW.maxSize k
$ SW.fromWidening (M.widening widenVal) $ SW.fromWidening (M.widening widenVal)
newtype IntervalT c x y = IntervalT { runIntervalT :: c x y } deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowFail e,ArrowJoin) widenVal = widening (W.bounded ?bound I.widening)
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 newtype IntervalT c x y = IntervalT { runIntervalT :: c x y } deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowFail e,ArrowJoin)
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 instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowJoin c) => IsVal Val (IntervalT c) where
succ = proc x -> case x of succ = proc x -> case x of
...@@ -138,35 +136,13 @@ instance (IsString e, ArrowChoice c, ArrowJoin c, ArrowFail e c) => ArrowCond Va ...@@ -138,35 +136,13 @@ instance (IsString e, ArrowChoice c, ArrowJoin c, ArrowFail e c) => ArrowCond Va
instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowJoin c) instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowJoin c)
=> IsClosure Val (Map Text Val) (IntervalT c) where => IsClosure Val (Map Text Val) (IntervalT c) where
closure = arr $ \(e, env) -> ClosureVal (Closure [(e,env)]) closure = arr $ \(e, env) -> ClosureVal (C.closure e env)
applyClosure f = proc (fun, arg) -> case fun of applyClosure f = proc (fun, arg) -> case fun of
Top -> returnA -< Top Top -> (returnA -< Top) <> (fail -< "Expected a closure")
ClosureVal (Closure cls) -> ClosureVal cls -> (| C.apply (\(e,env) -> f -< ((e,env),arg)) |) 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" 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 (M.widening (widening w)) cs cs'
widening _ Top Top = (W.Stable,Top)
widening _ _ _ = (W.Instable,Top)
instance UpperBounded Val where
top = Top
instance Hashable Closure
instance Hashable Val instance Hashable Val
instance Show Val where instance Show Val where
show (NumVal iv) = show iv show (NumVal iv) = show iv
...@@ -174,3 +150,12 @@ instance Show Val where ...@@ -174,3 +150,12 @@ instance Show Val where
show Top = "⊤" show Top = "⊤"
type IV = Interval (InfiniteNumber Int) 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
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