Commit e13bf32b authored by Sven Keidel's avatar Sven Keidel

fix pcf analyses

parent 32fed9f3
......@@ -2,9 +2,11 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Abstract.FiniteMap where
import Prelude hiding (lookup)
import Prelude hiding (lookup,Either(..),id,(.))
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as H
......@@ -12,16 +14,18 @@ import qualified Data.HashMap.Lazy as H
import Data.Identifiable
import Data.Order
import Data.Hashable
import Data.Maybe (maybeToList)
import Data.Abstract.There
import qualified Data.Abstract.Maybe as M
import Data.Abstract.Widening
import qualified Data.Abstract.Widening as W
import Control.Arrow
import Control.Arrow.Alloc
import Text.Printf
newtype Map x addr y = Map (HashMap x addr, HashMap addr (There,y)) deriving (Eq,Hashable)
instance (Show x,Show addr,Show y) => Show (Map x addr y) where
......@@ -33,8 +37,22 @@ instance (Show x,Show addr,Show y) => Show (Map x addr y) where
instance (Identifiable x, Identifiable addr, PreOrd y) => PreOrd (Map x addr y) where
m1 m2 = keys m1 == keys m2 && all (\k -> lookup k m1 lookup k m2) (keys m1)
m1 m2 = keys m1 == keys m2 && all (\k -> lookup k m1 lookup k m2) (keys m1)
Map (e,s) m2 = all (\(k,(t,v)) -> (case t of Must -> M.Just v; May -> M.JustNothing v) lookup k m2)
[ (a,b) | (a,addr) <- H.toList e, b <- maybeToList (H.lookup addr s) ]
instance (Identifiable x, Identifiable addr, Complete y) => Complete (Map x addr y) where
() = widening ()
widening :: (Identifiable x,Identifiable addr) => Widening y -> Widening (Map x addr y)
widening w (Map (e1,s1)) (Map (e2,s2)) = Map (e,s)
where
e = H.union e1 e2
s = H.fromList $ flip map (H.keys e) $ \x -> case (H.lookup x e1,H.lookup x e2) of
(Just a1, Just a2) -> (a1, (W.finite W.** w) (s1 H.! a1) (s2 H.! a2))
(Just a1, Nothing) -> (a1, s1 H.! a1)
(Nothing, Just a2) -> (a2, s2 H.! a2)
(Nothing, Nothing) -> error "cannot happen"
empty :: Map x addr y
empty = (Map (H.empty,H.empty))
......@@ -68,3 +86,5 @@ insert :: (Identifiable x, Identifiable addr, Complete y, ArrowChoice c, ArrowAl
insert = insertBy alloc
toList :: (Identifiable x, Identifiable addr) => Map x addr y -> [(x,y)]
toList (Map (e,s)) = [ (a,b)| (a,addr) <- H.toList e, (_,b) <- maybeToList (H.lookup addr s) ]
......@@ -4,8 +4,10 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
-- | Concrete semantics of PCF.
module ConcreteSemantics where
module ConcreteInterpreter where
import Prelude hiding (fail)
......@@ -29,13 +31,13 @@ import Data.Label
import GHC.Generics
import Syntax (Expr(..))
import SharedSemantics
import GenericInterpreter
data Closure = Closure Expr (Env Text Val) deriving (Eq,Generic)
data Val = NumVal Int | ClosureVal Closure deriving (Eq,Generic)
-- | The interpreter arrow for the concrete semantics that encapsulates the passing of the enviornment and the propagation of failure.
newtype Interp x y = Interp (Fix Expr Val (EnvT Text Val (FailureT String (->))) x y)
newtype Interp x y = Interp (EnvT Text Val (FailureT String (->)) x y)
-- | Takes an arrow computation and executes it.
runInterp :: Interp x y -> [(Text,Val)] -> x -> Error String y
......@@ -64,7 +66,8 @@ instance IsClosure Val (Env Text Val) Interp where
ClosureVal (Closure e env) -> f -< ((e,env),arg)
NumVal _ -> fail -< "Expected a closure"
instance ArrowCond Val x y z Interp where
instance ArrowCond Val Interp where
type Join Interp x y = ()
if_ f g = proc (v1, (x, y)) -> case v1 of
NumVal 0 -> f -< x
NumVal _ -> g -< y
......
......@@ -2,7 +2,7 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
module SharedSemantics where
module GenericInterpreter where
import Prelude hiding (succ, pred, fail)
import Syntax (Expr(..))
......@@ -10,14 +10,14 @@ import Syntax (Expr(..))
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Fail
import Control.Arrow.Environment
import Control.Arrow.Conditional
import Control.Arrow.Environment as Env
import Control.Arrow.Conditional as Cond
import Data.Text (Text)
-- | Shared interpreter for PCF.
eval :: (ArrowChoice c, ArrowFix Expr v c, ArrowEnv Text v env c, ArrowFail String c,
ArrowCond v Expr Expr v c, IsVal v c, IsClosure v env c)
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
Var x _ -> lookup' -< x
......
......@@ -9,6 +9,10 @@
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | k-CFA analysis for PCF where numbers are approximated by intervals.
module IntervalAnalysis where
......@@ -19,31 +23,26 @@ import Control.Category
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Fail
import Control.Arrow.Const
import Control.Arrow.Fix
import Control.Arrow.Conditional
import Control.Arrow.Conditional as Cond
import Control.Arrow.Environment
import Control.Arrow.Transformer.Abstract.Contour
import Control.Arrow.Transformer.Abstract.BoundedEnvironment
import Control.Arrow.Transformer.Abstract.Failure
import Control.Arrow.Transformer.Abstract.Fixpoint
import Control.Arrow.Transformer.Const
import Control.Monad.State hiding (lift,fail)
import Data.Foldable (toList)
import Data.Hashable
import Data.Label
import Data.Order
import Data.Monoidal(Iso(..))
import Data.Text (Text)
import Data.Abstract.Powerset(Pow)
import Data.Abstract.PreciseStore(Store)
import qualified Data.Abstract.PreciseStore as S
import Data.Abstract.Map(Map)
import qualified Data.Abstract.Map as M
import qualified Data.Abstract.FiniteMap as F
import Data.Abstract.Failure (Error)
import qualified Data.Abstract.Failure as E
import Data.Abstract.Environment (Env)
import qualified Data.Abstract.Environment as M
import Data.Abstract.InfiniteNumbers
import Data.Abstract.Interval (Interval)
import qualified Data.Abstract.Interval as I
......@@ -52,14 +51,15 @@ import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating(Terminating)
import GHC.Generics
import GHC.Exts(toList)
import Syntax (Expr)
import SharedSemantics
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 (Store Expr (F.Map Text Addr Val)) deriving (Eq,Generic,PreOrd,Show)
newtype Closure = Closure (Map Expr (F.Map Text Addr Val)) deriving (Eq,Generic,PreOrd,Complete,Show)
-- | Numeric values are approximated with bounded intervals, closure
-- values are approximated with a set of abstract closures.
......@@ -78,24 +78,28 @@ newtype Interp s x y =
(FixT s () ()
(->))))) x y)
widening :: W.Widening IV -> W.Widening Val
widening w _ Top = Top
widening w (NumVal x) (NumVal y) = NumVal (x `w` y)
widening w (ClosureVal (Closure cs)) (ClosureVal (Closure cs')) = ClosureVal $ Closure $ S.widening _ cs cs'
-- | Run an interpreter computation on inputs. The arguments are the
-- maximum interval bound, the depth `k` of the longest call string,
-- an environment, and the input of the computation.
runInterp :: Interp SW.Unit x y -> IV -> Int -> [(Text,Val)] -> x -> Terminating (Error String y)
runInterp :: Interp _ x y -> IV -> Int -> [(Text,Val)] -> x -> Terminating (Error String y)
runInterp (Interp f) b k env x =
runFixT' _ (E.widening (widening _))
runFixT' stackWiden (E.widening widenVal)
(runFailureT
(runContourT k
(runEnvT alloc
f)))
(env,x)
where
widenVal = widening (W.bounded b top)
stackWiden = SW.categorize categorizeExpression
$ SW.stack
$ SW.maxSize 3
$ SW.reuse (\_ l -> head l)
$ SW.fromWidening (F.widening widenVal)
categorizeExpression = Iso (\(ev,ex) -> (ex,ev)) (\(ex,ev) -> (ev,ex))
-- | The top-level interpreter functions that executes the analysis.
evalInterval :: (?bound :: IV) => Int -> [(Text,Val)] -> State Label Expr -> Terminating (Error String Val)
evalInterval k env e = runInterp eval ?bound k env (generate e)
......@@ -107,26 +111,27 @@ instance IsVal Val (Interp s) where
ClosureVal _ -> fail -< "Expected a number as argument for 'succ'"
pred = proc x -> case x of
Top -> returnA -< Top
NumVal n -> returnA -< NumVal $ n + negate 1
NumVal n -> returnA -< NumVal $ n - 1
ClosureVal _ -> fail -< "Expected a number as argument for 'pred'"
zero = proc _ -> returnA -< (NumVal 0)
instance (Complete z, UpperBounded z) => ArrowCond Val x y z (Interp s) where
instance ArrowCond Val (Interp s) where
type Join (Interp s) x y = Complete (Interp s x y)
if_ f g = proc v -> case v of
(Top, _) -> returnA -< top
(Top, (x,y)) -> joined f g -< (x,y)
(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.
| (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 -> joined f g -< (x,y) -- case the interval contains zero and other numbers.
(ClosureVal _, _) -> fail -< "Expected a number as condition for 'ifZero'"
instance IsClosure Val (F.Map Text Addr Val) (Interp s) where
closure = arr $ \(e, env) -> ClosureVal (return (Closure e env))
closure = arr $ \(e, env) -> ClosureVal (Closure [(e,env)])
applyClosure f = proc (fun, arg) -> case fun of
Top -> returnA -< Top
ClosureVal cls ->
ClosureVal (Closure cls) ->
-- Apply the interpreter function `f` on all closures and join their results.
lubA (proc (Closure e env,arg) -> f -< ((e,env),arg)) -< [ (c,arg) | c <- toList cls]
lubA (proc ((e,env),arg) -> f -< ((e,env),arg)) -< [ (c,arg) | c <- toList cls]
NumVal _ -> fail -< "Expected a closure"
deriving instance Category (Interp s)
......@@ -146,16 +151,13 @@ instance PreOrd Val where
_ _ = False
instance Complete Val where
Top _ = Top
_ Top = Top
NumVal x NumVal y = NumVal (x y)
ClosureVal x ClosureVal y = ClosureVal (x y)
_ _ = Top
-- instance Widening Val where
-- -- Only intervals require widening, everything else has finite height.
-- NumVal x ▽ NumVal y = NumVal (x ▽ y)
-- x ▽ y = x ⊔ y
() = widening ()
widening :: W.Widening IV -> W.Widening Val
widening w (NumVal x) (NumVal y) = NumVal (x `w` y)
widening w (ClosureVal (Closure cs)) (ClosureVal (Closure cs')) =
ClosureVal $ Closure $ M.widening (F.widening (widening w)) cs cs'
widening _ _ _ = Top
instance UpperBounded Val where
top = Top
......
......@@ -12,8 +12,8 @@ cabal-version: >=1.10
library
ghc-options: -Wall
exposed-modules: Syntax,
SharedSemantics,
ConcreteSemantics,
GenericInterpreter,
ConcreteInterpreter,
IntervalAnalysis
-- SignAnalysis
build-depends: base,
......
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