Commit c148cca1 authored by Sven Keidel's avatar Sven Keidel

fix while language

parent e13bf32b
......@@ -7,8 +7,9 @@
{-# LANGUAGE TypeFamilies #-}
module Control.Arrow.Environment where
import Prelude hiding (lookup,fail)
import Prelude hiding (lookup,fail,id)
import Control.Category
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Utils
......@@ -37,12 +38,16 @@ class Arrow c => ArrowEnv var val env c | c -> var, c -> val, c -> env where
-- | Simpler version of environment lookup.
lookup' :: (Join c ((val,var),var) val, Show var, IsString e, ArrowFail e c, ArrowEnv var val env c) => c var val
lookup' = proc var ->
lookup' = lookup'' id
lookup'' :: (Join c ((val,var),var) y, Show var, IsString e, ArrowFail e c, ArrowEnv var val env c) => c val y -> c var y
lookup'' f = proc var ->
lookup
(proc (val,_) -> returnA -< val)
(proc var -> fail -< fromString $ printf "Variable %s not bound" (show var))
(proc (val,_) -> f -< val)
(proc var -> fail -< fromString $ printf "Variable %s not bound" (show var))
-< (var,var)
-- | Run a computation in an extended environment.
extendEnv' :: ArrowEnv var val env c => c a b -> c (var,val,a) b
extendEnv' f = proc (x,y,a) -> do
......
......@@ -69,7 +69,7 @@ deriving instance ArrowChoice c => ArrowChoice (EnvT var val c)
deriving instance ArrowState s c => ArrowState s (EnvT var val c)
deriving instance ArrowFail e c => ArrowFail e (EnvT var val c)
deriving instance ArrowExcept e c => ArrowExcept e (EnvT var val c)
deriving instance ArrowStore var val c => ArrowStore var val (EnvT var val c)
deriving instance ArrowStore var val c => ArrowStore var val (EnvT var' val' c)
deriving instance ArrowConst x c => ArrowConst x (EnvT var val c)
deriving instance PreOrd (c (Map var val,x) y) => PreOrd (EnvT var val c x y)
......
......@@ -67,10 +67,10 @@ runFixT :: (Arrow c, Complete b) => FixT SW.Unit a b c x y -> c x (Terminating y
runFixT f = runFixT' SW.finite W.finite f
runFixT' :: (Monoid (s a),Arrow c) => StackWidening s a -> Widening b -> FixT s a b c x y -> c x (Terminating y)
runFixT' sw w f = runFixT'' sw mempty w f >>^ snd
runFixT' sw w f = runFixT'' sw w f >>^ snd
runFixT'' :: Arrow c => StackWidening s a -> s a -> Widening b -> FixT s a b c x y -> c x (Map a (Terminating b), Terminating y)
runFixT'' sw s0 w (FixT f) = (\x -> (((s0,M.empty),M.empty),x)) ^>> f (sw,w)
runFixT'' :: (Monoid (s a),Arrow c) => StackWidening s a -> Widening b -> FixT s a b c x y -> c x (Map a (Terminating b), Terminating y)
runFixT'' sw w (FixT f) = (\x -> (((mempty,M.empty),M.empty),x)) ^>> f (sw,w)
liftFixT :: Arrow c => c x y -> FixT s a b c x y
liftFixT f = FixT $ \_ -> ((\((_,o),x) -> (o,x)) ^>> second (f >>^ Terminating))
......
......@@ -11,8 +11,9 @@
{-# LANGUAGE ScopedTypeVariables #-}
module Control.Arrow.Transformer.Abstract.ReachingDefinitions(
ReachingDefsT(..),
reachingDefs,
runReachingDefs,
reachingDefsT,
runReachingDefsT,
runReachingDefsT',
) where
import Prelude hiding ((.),read,id)
......@@ -40,16 +41,19 @@ import qualified Data.Abstract.DiscretePowerset as P
newtype ReachingDefsT lab c x y = ReachingDefsT (ReaderT (Maybe lab) c x y)
reachingDefs :: Arrow c => c (Maybe lab,x) y -> ReachingDefsT lab c x y
reachingDefs = ReachingDefsT . ReaderT
reachingDefsT :: Arrow c => c (Maybe lab,x) y -> ReachingDefsT lab c x y
reachingDefsT = ReachingDefsT . ReaderT
runReachingDefs :: Arrow c => ReachingDefsT lab c x y -> c (Maybe lab,x) y
runReachingDefs (ReachingDefsT (ReaderT f)) = f
runReachingDefsT :: Arrow c => ReachingDefsT lab c x y -> c (Maybe lab,x) y
runReachingDefsT (ReachingDefsT (ReaderT f)) = f
runReachingDefsT' :: Arrow c => ReachingDefsT lab c x y -> c x y
runReachingDefsT' f = (\x -> (Nothing,x)) ^>> runReachingDefsT f
instance (Identifiable var, Identifiable lab, ArrowStore var (val,Pow lab) c) => ArrowStore var val (ReachingDefsT lab c) where
type Join (ReachingDefsT lab c) ((val,x),x) y = Store.Join c (((val,Pow lab),(Maybe lab,x)), (Maybe lab,x)) y
read (ReachingDefsT f) (ReachingDefsT g) = ReachingDefsT $ read ((\((v,_::Pow lab),x) -> (v,x)) ^>> f) g
write = reachingDefs $ proc (lab,(var,val)) ->
write = reachingDefsT $ proc (lab,(var,val)) ->
write -< (var,(val,P.fromMaybe lab))
type instance Fix x y (ReachingDefsT lab c) = ReachingDefsT lab (Fix x y c)
......@@ -60,13 +64,13 @@ instance (HasLabel x lab, Arrow c, ArrowFix x y c) => ArrowFix x y (ReachingDefs
wrap = lift
unwrap :: HasLabel x lab => ReachingDefsT lab c x y -> c x y
unwrap f' = (Just . label &&& id) ^>> runReachingDefs f'
unwrap f' = (Just . label &&& id) ^>> runReachingDefsT f'
instance ArrowApply c => ArrowApply (ReachingDefsT lab c) where
app = ReachingDefsT ((\(ReachingDefsT f,x) -> (f,x)) ^>> app)
instance ArrowLift (ReachingDefsT lab) where
lift f = reachingDefs (snd ^>> f)
lift f = reachingDefsT (snd ^>> f)
instance ArrowReader r c => ArrowReader r (ReachingDefsT lab c) where
ask = lift ask
......
......@@ -34,14 +34,14 @@ import Data.Hashable
newtype StoreT var val c x y = StoreT (StateT (Map var val) c x y)
runStore :: StoreT var val c x y -> c (Map var val, x) (Map var val, y)
runStore (StoreT (StateT f)) = f
runStoreT :: StoreT var val c x y -> c (Map var val, x) (Map var val, y)
runStoreT (StoreT (StateT f)) = f
evalStore :: Arrow c => StoreT var val c x y -> c (Map var val, x) y
evalStore f = runStore f >>> pi2
evalStoreT :: Arrow c => StoreT var val c x y -> c (Map var val, x) y
evalStoreT f = runStoreT f >>> pi2
execStore :: Arrow c => StoreT var val c x y -> c (Map var val, x) (Map var val)
execStore f = runStore f >>> pi1
execStoreT :: Arrow c => StoreT var val c x y -> c (Map var val, x) (Map var val)
execStoreT f = runStoreT f >>> pi1
instance (Identifiable var, ArrowChoice c) => ArrowStore var val (StoreT var val c) where
type Join (StoreT var val c) ((val,x),x) y = Complete (c (Map var val, ((val, x), x)) (Map var val, y))
......
......@@ -11,8 +11,8 @@ module Control.Arrow.Transformer.Concrete.Environment where
import Prelude hiding ((.),read)
import Data.Identifiable
import Data.Concrete.Environment (Env)
import qualified Data.Concrete.Environment as E
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Control.Category
......@@ -29,23 +29,23 @@ import Control.Arrow.Environment
import Control.Arrow.Fix
-- | Arrow transformer that adds an environment to a computation.
newtype EnvT var val c x y = EnvT (ReaderT (Env var val) c x y)
newtype EnvT var val c x y = EnvT (ReaderT (HashMap var val) c x y)
runEnvT :: (Arrow c) => EnvT var val c x y -> c (Env var val,x) y
runEnvT :: (Arrow c) => EnvT var val c x y -> c (HashMap var val,x) y
runEnvT (EnvT (ReaderT f)) = f
runEnvT' :: (Arrow c, Identifiable var) => EnvT var val c x y -> c ([(var,val)],x) y
runEnvT' f = first E.fromList ^>> runEnvT f
runEnvT' f = first M.fromList ^>> runEnvT f
instance (Identifiable var, ArrowChoice c) => ArrowEnv var val (Env var val) (EnvT var val c) where
instance (Identifiable var, ArrowChoice c) => ArrowEnv var val (HashMap var val) (EnvT var val c) where
type Join (EnvT var val c) x y = ()
lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- ask -< ()
case E.lookup var env of
case M.lookup var env of
Just val -> f -< (val,x)
Nothing -> g -< x
getEnv = EnvT ask
extendEnv = arr $ \(x,y,env) -> E.insert x y env
extendEnv = arr $ \(x,y,env) -> M.insert x y env
localEnv (EnvT f) = EnvT (local f)
instance ArrowApply c => ArrowApply (EnvT var val c) where
......@@ -63,7 +63,7 @@ deriving instance ArrowState s c => ArrowState s (EnvT var val c)
deriving instance ArrowFail e c => ArrowFail e (EnvT var val c)
deriving instance ArrowExcept e c => ArrowExcept e (EnvT var val c)
deriving instance ArrowConst r c => ArrowConst r (EnvT var val c)
deriving instance ArrowStore var val c => ArrowStore var val (EnvT var val c)
deriving instance ArrowStore var val c => ArrowStore var val (EnvT var' val' c)
type instance Fix x y (EnvT var val c) = EnvT var val (Fix (Env var val,x) y c)
deriving instance ArrowFix (Env var val,x) y c => ArrowFix x y (EnvT var val c)
type instance Fix x y (EnvT var val c) = EnvT var val (Fix (HashMap var val,x) y c)
deriving instance ArrowFix (HashMap var val,x) y c => ArrowFix x y (EnvT var val c)
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Data.Concrete.Environment(Env,empty,lookup,insert,insertWith,fromList,toList) where
import Prelude hiding (lookup)
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as H
import Data.Hashable
import Data.Identifiable
import Text.Printf
newtype Env a b = Env (HashMap a b) deriving (Eq,Functor,Foldable,Traversable,Hashable)
instance (Show a,Show b) => Show (Env a b) where
show (Env h)
| H.null h = "[]"
| otherwise = "[" ++ init (unwords [ printf "%s -> %s," (show k) (show v) | (k,v) <- H.toList h]) ++ "]"
empty :: Env a b
empty = Env H.empty
lookup :: Identifiable a => a -> Env a b -> Maybe b
lookup a (Env m) = H.lookup a m
insert :: Identifiable a => a -> b -> Env a b -> Env a b
insert a b (Env m) = Env (H.insert a b m)
insertWith :: Identifiable a => (b -> b -> b) -> a -> b -> Env a b -> Env a b
insertWith f a b (Env m) = Env (H.insertWith f a b m)
fromList :: Identifiable a => [(a,b)] -> Env a b
fromList = Env . H.fromList
toList :: Env a b -> [(a,b)]
toList (Env e) = H.toList e
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Data.Concrete.Store(Store,subsetKeys,empty,lookup,insert,insertWith,adjust,(!),keys,toList,fromList) where
import Prelude hiding (lookup)
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as H
import Data.HashSet (HashSet)
import qualified Data.HashSet as S
import Data.Hashable
import Data.Identifiable
import Text.Printf
newtype Store a b = Store (HashMap a b) deriving (Eq,Functor,Foldable,Traversable,Hashable)
instance (Show a,Show b) => Show (Store a b) where
show (Store h)
| H.null h = "[]"
| otherwise = "[" ++ init (unwords [ printf "%s -> %s," (show k) (show v) | (k,v) <- H.toList h]) ++ "]"
subsetKeys :: Identifiable a => HashMap a b -> HashMap a b -> Bool
subsetKeys m1 m2 = subset (S.fromMap (H.map (const ()) m1)) (S.fromMap (H.map (const ()) m2))
subset :: Identifiable a => HashSet a -> HashSet a -> Bool
subset s1 s2 = S.size (S.intersection s1 s2) == S.size s1
empty :: Store a b
empty = Store H.empty
lookup :: Identifiable a => a -> Store a b -> Maybe b
lookup a (Store m) = H.lookup a m
insert :: Identifiable a => a -> b -> Store a b -> Store a b
insert a b (Store m) = Store (H.insert a b m)
insertWith :: Identifiable a => (b -> b -> b) -> a -> b -> Store a b -> Store a b
insertWith f a b (Store m) = Store (H.insertWith f a b m)
adjust :: Identifiable a => (b -> b) -> a -> Store a b -> Store a b
adjust f a (Store m) = Store (H.adjust f a m)
(!) :: Identifiable a => Store a b -> a -> b
Store m ! a = m H.! a
keys :: Store a b -> [a]
keys (Store m) = H.keys m
toList :: Store a b -> [(a,b)]
toList (Store m) = H.toList m
fromList :: Identifiable a => [(a,b)] -> Store a b
fromList l = Store (H.fromList l)
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Data.Label where
import Data.Hashable
import Data.Order
import Data.Abstract.FreeCompletion
import Control.Monad.State
-- Retrieves label from expression.
......@@ -15,6 +18,13 @@ newtype Label = Label { labelVal :: Int }
instance Show Label where
show (Label l) = show l
instance PreOrd Label where
() = (==)
instance Complete (FreeCompletion Label) where
Lower l1 Lower l2 | l1 == l2 = Lower l1
_ _ = Top
fresh :: State Label Label
fresh = state (\l -> (l,l+1))
......
......@@ -35,10 +35,8 @@ library
Data.CallString,
Data.Concrete.Boolean,
Data.Concrete.Environment,
Data.Concrete.Error,
Data.Concrete.Powerset,
Data.Concrete.Store,
Data.Abstract.Either,
Data.Abstract.Equality,
......
......@@ -110,7 +110,7 @@ spec = do
0 -> fail -< ()
_ -> f -< (n-1)
in it "should fail, but update the fixpoint cache" $
runFixT'' SW.finite SW.Unit W.finite (runFailureT recurseFail) 5
runFixT'' SW.finite W.finite (runFailureT recurseFail) 5
`shouldBe` (S.fromList [(n,Terminating (Fail ())) | n <- [0..5]], return (Fail ()))
describe "the analysis of a stateful program" $
......@@ -124,7 +124,7 @@ spec = do
s' <- get -< ()
put -< s'+ I.Interval 1 1
in it "should cache the state of the program" $
runFixT'' SW.finite SW.Unit W.finite (runStateT timesTwo) (0,5) `shouldBe`
runFixT'' SW.finite W.finite (runStateT timesTwo) (0,5) `shouldBe`
(S.fromList [((fromIntegral n,5-fromIntegral n),
return (10-fromIntegral n,())) | n <- [0..5::Int]],
return (10,()))
......
......@@ -23,7 +23,7 @@ import Control.Arrow.Transformer.Concrete.Fixpoint
import Control.Monad.State hiding (fail)
import Data.Concrete.Error
import Data.Concrete.Environment (Env)
import Data.HashMap.Lazy (HashMap)
import Data.Hashable
import Data.Text (Text)
import Data.Label
......@@ -33,24 +33,29 @@ import GHC.Generics
import Syntax (Expr(..))
import GenericInterpreter
data Closure = Closure Expr (Env Text Val) deriving (Eq,Generic)
data Closure = Closure Expr (HashMap 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 (EnvT Text Val (FailureT String (->)) x y)
-- | Takes an arrow computation and executes it.
runInterp :: Interp x y -> [(Text,Val)] -> x -> Error String y
runInterp (Interp f) env x = runFix (runFailureT (runEnvT' f)) (env,x)
-- | The concrete interpreter function for PCF. The function is
-- implemented by instantiating the shared semantics with the concrete
-- interpreter arrow `Interp`.
evalConcrete :: [(Text,Val)] -> State Label Expr -> Error String Val
evalConcrete env e = runInterp eval env (generate e)
evalConcrete env e =
runFix
(runFailureT
(runEnvT'
(runConcreteT
eval)))
(env,generate e)
-- | Arrow transformer that implements the concrete value semantics
newtype ConcreteT c x y = ConcreteT { runConcreteT :: c x y }
deriving (Category,Arrow,ArrowChoice,ArrowFail e)
deriving instance ArrowFix x y c => ArrowFix x y (ConcreteT c)
deriving instance ArrowEnv var Val env c => ArrowEnv var Val env (ConcreteT c)
-- | Concrete instance of the interface for value operations.
instance IsVal Val Interp where
instance (ArrowChoice c, ArrowFail String c) => IsVal Val (ConcreteT c) where
succ = proc x -> case x of
NumVal n -> returnA -< NumVal (n + 1)
_ -> fail -< "Expected a number as argument for 'succ'"
......@@ -60,28 +65,19 @@ instance IsVal Val Interp where
zero = arr $ const (NumVal 0)
-- | Concrete instance of the interface for closure operations.
instance IsClosure Val (Env Text Val) Interp where
instance (ArrowChoice c, ArrowFail String c) => IsClosure Val (HashMap Text Val) (ConcreteT c) where
closure = arr $ \(e, env) -> ClosureVal $ Closure e env
applyClosure f = proc (fun, arg) -> case fun of
ClosureVal (Closure e env) -> f -< ((e,env),arg)
NumVal _ -> fail -< "Expected a closure"
instance ArrowCond Val Interp where
type Join Interp x y = ()
instance (ArrowChoice c, ArrowFail String c) => ArrowCond Val (ConcreteT c) where
type Join (ConcreteT c) x y = ()
if_ f g = proc (v1, (x, y)) -> case v1 of
NumVal 0 -> f -< x
NumVal _ -> g -< y
_ -> fail -< "Expected a number as condition for 'ifZero'"
-- All other instances for the concrete interpreter arrow can be
-- derived from the instances of the underlying arrow transformers.
deriving instance Category Interp
deriving instance Arrow Interp
deriving instance ArrowChoice Interp
deriving instance ArrowFail String Interp
deriving instance ArrowEnv Text Val (Env Text Val) Interp
deriving instance ArrowFix Expr Val Interp
instance Hashable Closure
instance Hashable Val
instance Show Closure where
......
......@@ -13,7 +13,7 @@
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-partial-type-signatures #-}
-- | k-CFA analysis for PCF where numbers are approximated by intervals.
module IntervalAnalysis where
......@@ -68,43 +68,39 @@ 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)
-- | Interpreter arrow for the k-CFA / interval analysis.
newtype Interp s x y =
Interp (
Fix Expr Val -- type of the fixpoint cache
(EnvT Text Addr Val -- threads the environment and store
(ContourT Label -- records the k-bounded call stack used for address allocation
(FailureT String -- allows to fail with an error message
(FixT s () ()
(->))))) x y)
-- | Run an interpreter computation on inputs. The arguments are the
-- | 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.
runInterp :: Interp _ x y -> IV -> Int -> [(Text,Val)] -> x -> Terminating (Error String y)
runInterp (Interp f) b k env x =
evalInterval :: (?bound :: IV) => Int -> [(Text,Val)] -> State Label Expr -> Terminating (Error String Val)
evalInterval k env e = -- runInterp eval ?bound k env (generate e)
runFixT' stackWiden (E.widening widenVal)
(runFailureT
(runContourT k
(runEnvT alloc
f)))
(env,x)
(runIntervalT
(eval ::
Fix Expr Val
(IntervalT
(EnvT Text Addr Val
(ContourT Label
(FailureT String
(FixT s () ()
(->)))))) Expr Val)))))
(env,generate e)
where
widenVal = widening (W.bounded b top)
stackWiden = SW.categorize categorizeExpression
widenVal = widening (W.bounded ?bound top)
stackWiden = SW.categorize (Iso (\(ev,ex) -> (ex,ev)) (\(ex,ev) -> (ev,ex)))
$ 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)
newtype IntervalT c x y = IntervalT { runIntervalT :: c x y } deriving (Category,Arrow,ArrowChoice,ArrowFail e, PreOrd, Complete, LowerBounded)
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 IsVal Val (Interp s) where
instance (ArrowChoice c, ArrowFail String c) => IsVal Val (IntervalT c) where
succ = proc x -> case x of
Top -> returnA -< Top
NumVal n -> returnA -< NumVal $ n + 1 -- uses the `Num` instance of intervals
......@@ -115,8 +111,8 @@ instance IsVal Val (Interp s) where
ClosureVal _ -> fail -< "Expected a number as argument for 'pred'"
zero = proc _ -> returnA -< (NumVal 0)
instance ArrowCond Val (Interp s) where
type Join (Interp s) x y = Complete (Interp s x y)
instance (ArrowChoice c, ArrowFail String c) => ArrowCond Val (IntervalT c) where
type Join (IntervalT c) x y = Complete (IntervalT c x y)
if_ f g = proc v -> case v of
(Top, (x,y)) -> joined f g -< (x,y)
(NumVal (I.Interval i1 i2), (x, y))
......@@ -125,7 +121,8 @@ instance ArrowCond Val (Interp s) where
| 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
instance (ArrowChoice c, ArrowFail String c, LowerBounded (IntervalT c () Val), Complete (IntervalT c (((Expr, F.Map Text Addr Val),Val),[((Expr, F.Map Text Addr Val), Val)]) Val))
=> 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
......@@ -134,16 +131,6 @@ instance IsClosure Val (F.Map Text Addr Val) (Interp s) where
lubA (proc ((e,env),arg) -> f -< ((e,env),arg)) -< [ (c,arg) | c <- toList cls]
NumVal _ -> fail -< "Expected a closure"
deriving instance Category (Interp s)
deriving instance Arrow (Interp s)
deriving instance ArrowChoice (Interp s)
deriving instance ArrowFail String (Interp s)
deriving instance ArrowEnv Text Val (F.Map Text Addr Val) (Interp s)
deriving instance ArrowFix Expr Val (Interp s)
deriving instance PreOrd y => PreOrd (Interp s x y)
deriving instance Complete y => Complete (Interp s x y)
deriving instance PreOrd y => LowerBounded (Interp s x y)
instance PreOrd Val where
_ Top = True
NumVal n1 NumVal n2 = n1 n2
......
......@@ -3,7 +3,7 @@ module ConcreteSpec where
import Prelude hiding (succ,pred)
import SharedSpecs
import ConcreteSemantics
import ConcreteInterpreter
import Data.Concrete.Error
import Syntax
import Test.Hspec
......
......@@ -5,10 +5,8 @@ module IntervalAnalysisSpec where
import Prelude hiding (succ,pred)
import SharedSpecs
import Data.Abstract.Bounded
import Data.Abstract.PropagateError hiding (toEither)
import Data.Abstract.Failure hiding (toEither)
import qualified Data.Abstract.Interval as I
import Data.Abstract.InfiniteNumbers
import Data.Abstract.Terminating hiding (toEither)
import IntervalAnalysis
import Syntax
......@@ -20,7 +18,7 @@ main = hspec spec
spec :: Spec
spec = do
let ?bound = I.Interval (-100) 100 in
sharedSpec (\env e -> toEither $ evalInterval 3 env e) (NumVal . bounded . fromIntegral)
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" $
......@@ -35,17 +33,11 @@ spec = do
Terminating (Success (num 0 0))
it "should analyse addition correctly" $
-- evalInterval 0 lim [] (App (App add five) two) `shouldBe` Success Top
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))
-- The problem is that the check for `IfZero` does not improve the
-- value for the first parameter of `add` in the environment. This means that
-- at some point addition is called with add [-1,0] [2,2] and [-1,0] fails the bound check and the top interval is returned.
evalInterval 10 [("x", num 0 1)] (app (app add "x") two) `shouldBe`
Terminating (Success (num NegInfinity Infinity))
evalInterval 10 [("x", num 0 1)] (app (app add "x") two) `shouldBe` Terminating (Success (num 2 7))
it "should terminate for the non-terminating program" $
let ?bound = I.Interval 0 5
......@@ -60,7 +52,7 @@ spec = do
one = succ zero
two = succ one
num i j = NumVal $ bounded $ I.Interval i j
num i j = NumVal $ I.Interval i j
toEither :: Terminating (Error String a) -> Either String a
toEither (Terminating (Fail e)) = Left e
......
......@@ -2,7 +2,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module SharedSemantics where
module GenericInterpreter where
import Prelude hiding (lookup, and, or, not, div, read)
......@@ -10,12 +10,12 @@ import Data.Label
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Conditional
import Control.Arrow.Conditional as Cond
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Environment
import Control.Arrow.Environment as Env
import Control.Arrow.Random
import Control.Arrow.Store
import Control.Arrow.Store as Store
import Control.Arrow.Utils
import Data.Text (Text)
......@@ -26,13 +26,14 @@ import Syntax
type Prog = [Statement]
eval :: (Show addr, ArrowChoice c, ArrowRand v c,
ArrowEnv Text addr env c, ArrowStore (addr,Label) v c,
ArrowFail e c, IsString e, IsVal v c)
ArrowEnv Text addr env c, ArrowStore addr v c,
ArrowFail e c, IsString e, IsVal v c,
Env.Join c ((addr, Text),Text) v,
Store.Join c ((v, addr),addr) v
)
=> c Expr v
eval = proc e -> case e of
Var x l -> do
addr <- lookup' -< x
read' -< (addr,l)
Var x _ -> lookup'' read' -< x
BoolLit b l -> boolLit -< (b,l)