Commit 75f7893c authored by Sven Keidel's avatar Sven Keidel

fix and polish Reaching Definition Analysis

parent 2c56d898
Pipeline #13295 failed with stages
in 23 minutes and 52 seconds
......@@ -49,7 +49,7 @@ import Data.Profunctor
newtype EnvT var addr val c x y = EnvT ( ConstT (c (var,val,Map var addr val) addr) (ReaderT (Map var addr val) c) x y )
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowState s, ArrowFail e, ArrowExcept e, ArrowJoin)
runEnvT :: (Show var, Identifiable var, Identifiable addr, Complete val, ArrowChoice c, Profunctor c)
runEnvT :: (Show var, Identifiable var, Identifiable addr, Complete val, ArrowJoin c, ArrowChoice c, Profunctor c)
=> c (var,val,Map var addr val) addr -> EnvT var addr val c x y -> c ([(var,val)],x) y
runEnvT alloc f =
let EnvT f' = proc (bs,x) -> do
......@@ -67,9 +67,9 @@ instance ArrowTrans (EnvT var addr val) where
instance ArrowLift (EnvT var addr val) where
lift' f = EnvT (lift' (lift' f))
instance (Identifiable var, Identifiable addr, Complete val, ArrowChoice c, Profunctor c) =>
instance (Identifiable var, Identifiable addr, Complete val, ArrowChoice c, ArrowJoin c, Profunctor c) =>
ArrowEnv var val (Map var addr val) (EnvT var addr val c) where
type Join (EnvT var addr val c) x y = (ArrowJoin c, Complete y)
type Join (EnvT var addr val c) x y = (Complete y)
lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- ask -< ()
case do M.lookup var env of
......
......@@ -42,8 +42,8 @@ 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 (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 = (ArrowJoin c, Complete y)
instance (Identifiable var, UpperBounded val, ArrowChoice c, ArrowJoin c, Profunctor c) => ArrowEnv var val (Map var val) (EnvT var val c) where
type Join (EnvT var val c) x y = (Complete y)
lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- ask -< ()
case M.lookup' var env of
......
......@@ -40,14 +40,14 @@ runExceptT :: ExceptT e c x y -> c x (Except e y)
runExceptT = coerce
instance (ArrowChoice c, Complete e, ArrowJoin c) => ArrowExcept e (ExceptT e c) where
type Join (ExceptT e c) (y,(x,e)) z = Complete (c (y,(x,e)) (Except e z))
type Join (ExceptT e c) (y,(x,e)) z = Complete (Except e z)
throw = lift $ arr Fail
try f g h = lift $ proc x -> do
e <- unlift f -< x
case e of
Success y -> unlift g -< y
Fail er -> unlift h -< (x,er)
SuccessOrFail er y -> joined (unlift g) (unlift h) -< (y,(x,er))
SuccessOrFail er y -> (unlift g -< y) <> (unlift h -< (x,er))
instance (Complete e, ArrowJoin c, ArrowChoice c, ArrowApply c, Profunctor c) => ArrowApply (ExceptT e c) where app = lift $ lmap (first unlift) app
type instance Fix x y (ExceptT e c) = ExceptT e (Fix (Dom (ExceptT e) x y) (Cod (ExceptT e) x y) c)
......
......@@ -9,7 +9,7 @@
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
module Control.Arrow.Transformer.Abstract.Fix(FixT,runFixT) where
module Control.Arrow.Transformer.Abstract.Fix(FixT,runFixT,runFixT') where
import Prelude hiding (id,(.),const,head,iterate,lookup)
......@@ -33,7 +33,11 @@ newtype FixT a b c x y = FixT { unFixT :: ConstT (IterationStrategy c a b) c x y
runFixT :: (Identifiable a, PreOrd b, Profunctor c, ArrowRun t)
=> IterationStrategy (t c) a b -> FixT a b (t c) x y -> c x y
runFixT iterationStrat (FixT f) = run (runConstT (iterationStrat) f)
runFixT iterationStrat f = run (runFixT' iterationStrat f)
runFixT' :: (Identifiable a, PreOrd b)
=> IterationStrategy c a b -> FixT a b c x y -> c x y
runFixT' iterationStrat (FixT f) = (runConstT iterationStrat f)
type instance Fix x y (FixT () () c) = FixT x y c
instance (Identifiable a, LowerBounded b, Profunctor c,ArrowChoice c,ArrowApply c) => ArrowFix a b (FixT a b c) where
......
......@@ -47,8 +47,8 @@ evalStoreT f = runStoreT f >>> pi2
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, Profunctor c, Complete val) => ArrowStore var val (StoreT var val c) where
type Join (StoreT var val c) ((val,x),x) y = (ArrowJoin c, Complete y)
instance (Identifiable var, ArrowChoice c, ArrowJoin c, Profunctor c, Complete val) => ArrowStore var val (StoreT var val c) where
type Join (StoreT var val c) ((val,x),x) y = Complete y
read (StoreT f) (StoreT g) = StoreT $ proc (var,x) -> do
s <- get -< ()
case M.lookup var s of
......
......@@ -26,8 +26,7 @@ import qualified Data.Concrete.Error as C
import GHC.Generics (Generic, Generic1)
-- | Failure is an Either-like type with the special ordering Failure ⊑ Success.
-- Left and Right of the regular Either type, on the other hand are incomparable.
-- | Error is an Either-like type with the ordering Success ⊑ Failure.
data Error e a = Fail e | Success a
deriving (Eq, Functor, Generic, Generic1, NFData, NFData1)
......
......@@ -136,13 +136,15 @@ instance Identifiable a => Monoid (Component a) where
mempty = Component { head = H.empty, body = H.empty }
c1 `mappend` c2 = Component { head = head c1 <> head c2, body = body c1 <> body c2 }
newtype ChaoticT s a b c x y = ChaoticT (WriterT (Component a) (StateT (HashMap a (b,Stable)) (ReaderT (Stack a,s a) c)) x y) deriving (Profunctor,Category,Arrow,ArrowChoice)
newtype ChaoticT s a b c x y = ChaoticT (WriterT (Component a) (StateT (HashMap a (b,Stable)) (ReaderT (Stack a,s a) c)) x y)
deriving (Profunctor,Category,Arrow,ArrowChoice)
runChaoticT :: (IsEmpty (s a), Profunctor c) => ChaoticT s a b c x y -> c x (HashMap a (b,Stable),y)
runChaoticT (ChaoticT f) = dimap (\a -> (empty,(M.empty,a))) (second snd) (runReaderT (runStateT (runWriterT f)))
instance (Identifiable a,Profunctor c,ArrowApply c) => ArrowApply (ChaoticT s a b c) where app = ChaoticT (lmap (first coerce) app)
instance (Identifiable a,Profunctor c,Arrow c) => ArrowJoin (ChaoticT s a b c) where
joinWith _lub (ChaoticT f) (ChaoticT g) = ChaoticT $ rmap (uncurry _lub) (f &&& g)
-- deriving instance PreOrd (ChaoticT s a b c)
instance (IsEmpty (s a)) => ArrowRun (ChaoticT s a b) where
run (ChaoticT f) = dimap (\a -> (empty,(M.empty,a))) (snd . snd) (runReaderT (runStateT (runWriterT f)))
instance (Identifiable a,Profunctor c,Arrow c) => ArrowJoin (ChaoticT s a b c) where
joinWith _lub (ChaoticT f) (ChaoticT g) = ChaoticT $ rmap (uncurry _lub) (f &&& g)
chaotic :: (Identifiable a, LowerBounded b, Profunctor c, ArrowChoice c, ArrowApply c) => StackWidening s a -> Widening b -> IterationStrategy (ChaoticT s a b c) a b
chaotic stackWiden widen (ChaoticT (WriterT (StateT f))) = ChaoticT $ WriterT $ StateT $ stackWidening $ proc (stack,cache,a) -> do
......
......@@ -31,7 +31,6 @@ import Control.Arrow.Fix
import Control.Arrow.Environment
import Control.Arrow.Store
import Control.Arrow.Alloc
import Control.Arrow.Conditional as Cond
import Control.Arrow.Random
import Control.Arrow.Transformer.Concrete.Failure
import Control.Arrow.Transformer.Concrete.Environment
......@@ -71,6 +70,8 @@ instance (ArrowChoice c, Profunctor c) => ArrowAlloc (Text,Val,Label) Addr (Conc
alloc = arr $ \(_,_,l) -> l
instance (ArrowChoice c, ArrowFail String c) => IsVal Val (ConcreteT c) where
type Join (ConcreteT c) x y = ()
boolLit = arr (\(b,_) -> BoolVal b)
and = proc (v1,v2,_) -> case (v1,v2) of
(BoolVal b1,BoolVal b2) -> returnA -< BoolVal (b1 && b2)
......@@ -101,9 +102,6 @@ instance (ArrowChoice c, ArrowFail String c) => IsVal Val (ConcreteT c) where
lt = proc (v1,v2,_) -> case (v1,v2) of
(NumVal n1,NumVal n2) -> returnA -< BoolVal (n1 P.< n2)
_ -> fail -< "Expected two numbers as arguments for 'lt'"
instance (ArrowChoice c, ArrowFail String c) => ArrowCond Val (ConcreteT c) where
type Join (ConcreteT c) x y = ()
if_ f1 f2 = proc (v,(x,y)) -> case v of
BoolVal True -> f1 -< x
BoolVal False -> f2 -< y
......
......@@ -2,26 +2,29 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
module GenericInterpreter where
import Prelude hiding (lookup, and, or, not, div, read)
import Prelude hiding (lookup, and, or, not, div, read)
import Data.Label
import Data.Label
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Conditional as Cond
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Environment as Env
import Control.Arrow.Random
import Control.Arrow.Store as Store
import Control.Arrow.Utils
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Environment(ArrowEnv,lookup,lookup'',extendEnv')
import qualified Control.Arrow.Environment as Env
import Control.Arrow.Random
import Control.Arrow.Store(ArrowStore,read',write)
import qualified Control.Arrow.Store as Store
import Control.Arrow.Utils
import Data.Text (Text)
import Data.String
import Data.Text (Text)
import Data.String
import Syntax
import Syntax
import GHC.Exts
type Prog = [Statement]
......@@ -76,11 +79,11 @@ eval = proc e -> case e of
run :: (Show addr, ArrowChoice c, ArrowFix [Statement] () c,
ArrowEnv Text addr env c, ArrowStore addr v c,
ArrowAlloc (Text,v,Label) addr c, ArrowFail e c,
ArrowCond v c, ArrowRand v c, IsString e, IsVal v c,
ArrowRand v c, IsString e, IsVal v c,
Env.Join c ((addr, Text),Text) v,
Env.Join c ((addr, (Text,v,Label)), (Text,v,Label)) addr,
Store.Join c ((v, addr),addr) v,
Cond.Join c ([Statement],[Statement]) ()
Join c ([Statement],[Statement]) ()
)
=> c [Statement] ()
run = fix $ \run' -> proc stmts -> case stmts of
......@@ -102,6 +105,8 @@ run = fix $ \run' -> proc stmts -> case stmts of
returnA -< ()
class Arrow c => IsVal v c | c -> v where
type family Join (c :: * -> * -> *) x y :: Constraint
boolLit :: c (Bool,Label) v
and :: c (v,v,Label) v
or :: c (v,v,Label) v
......@@ -113,4 +118,5 @@ class Arrow c => IsVal v c | c -> v where
div :: c (v,v,Label) v
eq :: c (v,v,Label) v
lt :: c (v,v,Label) v
if_ :: Join c (x,y) z => c x z -> c y z -> c (v, (x, y)) z
......@@ -55,7 +55,6 @@ import Data.Text (Text)
import Control.Category
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Conditional
import Control.Arrow.Environment
import Control.Arrow.Fail
import Control.Arrow.Fix
......@@ -92,8 +91,8 @@ run k env ss =
(StoreT Addr Val
(ErrorT (Pow String)
(TerminatingT
(FixT _ _ () () (->))))))) [Statement] ()))))))
(M.empty,(SM.fromList env, generate <$> ss))
(FixT () () _)))))) [Statement] ()))))))
(M.empty,(SM.fromList env, generate (sequence ss)))
where
iterationStrategy = S.filter (L.second (L.second whileLoops))
......@@ -116,6 +115,8 @@ instance (ArrowChoice c, Profunctor c) => ArrowAlloc (Text,Val,Label) Addr (Inte
alloc = arr $ \(_,_,l) -> return l
instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowJoin c) => IsVal Val (IntervalT c) where
type Join (IntervalT c) (x,y) z = Complete z
boolLit = arr $ \(b,_) -> case b of
P.True -> BoolVal B.True
P.False -> BoolVal B.False
......@@ -159,9 +160,6 @@ instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowJoin c) => IsVal Val (I
(NumVal n1,NumVal n2) -> returnA -< BoolVal (n1 O.< n2)
_ | v1 == Top || v2 == Top -> (returnA -< BoolVal top) <> (fail -< "Expected two numbers as arguments for 'lt'")
_ -> fail -< "Expected two numbers as arguments for 'lt'"
instance (IsString e, ArrowChoice c,ArrowFail e c, ArrowJoin c) => ArrowCond Val (IntervalT c) where
type Join (IntervalT c) (x,y) z = Complete z
if_ f1 f2 = proc (v,(x,y)) -> case v of
BoolVal B.True -> f1 -< x
BoolVal B.False -> f2 -< y
......
......@@ -2,65 +2,111 @@
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ImplicitParams #-}
{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-partial-type-signatures #-}
module ReachingDefinitionsAnalysis where
-- import Syntax
-- import qualified GenericInterpreter as Generic
-- import UnitSemantics
-- import Data.Text (Text)
-- import Data.Label
-- import qualified Data.List as L
-- import Data.HashMap.Lazy (HashMap)
-- import qualified Data.HashMap.Lazy as M
-- import qualified Data.Abstract.Map as SM
-- import qualified Data.Abstract.WeakMap as WM
-- import Data.Abstract.DiscretePowerset(Pow)
-- import qualified Data.Abstract.StackWidening as SW
-- import qualified Data.Abstract.Widening as W
-- import Control.Arrow.Fix
-- import Control.Arrow.Transformer.Abstract.ReachingDefinitions
-- import Control.Arrow.Transformer.Abstract.Environment
-- import Control.Arrow.Transformer.Abstract.Store
-- import Control.Arrow.Transformer.Abstract.Error
-- import Control.Arrow.Transformer.Abstract.Fix
-- -- | Calculates the entry sets of which definitions may be reached for each statment.
-- run :: [Statement] -> [(Statement,HashMap Text (Pow Label))]
-- run stmts =
-- L.sortOn ((label :: Statement -> Label) . fst) $
-- M.toList $
-- -- Joins the reaching definitions for each statement for all call context.
-- -- Filters out statements created during execution that are not part
-- -- of the input program.
-- M.mapMaybe (\((store,(env,st)),_) -> case st of
-- stmt:_ | stmt `elem` blocks stmts -> Just (stmt, [ (a,c) | (a,b) <- (WM.toList env), Just (_,c) <- [SM.unsafeLookup b store]])
-- _ -> Nothing) $
-- -- get the fixpoint cache
-- fst $
-- -- Run the computation
-- runFixT'' SW.finite W.finite
-- (runErrorT
-- (runStoreT
-- (runReachingDefsT'
-- (runEnvT
-- (runUnitT
-- (Generic.run ::
-- Fix [Statement] ()
-- (UnitT
-- (EnvT Text Addr
-- (ReachingDefsT Label
-- (StoreT Addr (Val, Pow Label)
-- (ErrorT (Pow String)
-- (FixT _ () () (->))))))) [Statement] ()))))))
-- (SM.empty,(WM.empty,stmts))
-- instance HasLabel (x,[Statement]) Label where
-- label (_,ss) = label (head ss)
-- deriving instance IsVal val c => IsVal val (ReachingDefsT Label c)
import Prelude hiding (pred)
import Syntax
import qualified GenericInterpreter as Generic
import IntervalAnalysis
import Data.Text (Text)
import Data.Label
import qualified Data.List as L
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as Map
import qualified Data.Lens as L
import Data.Order
import Data.Maybe
import qualified Data.Abstract.Error as E
import qualified Data.Abstract.StrongMap as SM
import qualified Data.Abstract.Map as M
import Data.Abstract.DiscretePowerset(Pow)
import qualified Data.Abstract.StackWidening as SW
import qualified Data.Abstract.Widening as W
import qualified Data.Abstract.IterationStrategy as S
import qualified Data.Abstract.Interval as I
import qualified Data.Abstract.Terminating as T
import Data.Identifiable
import Control.Arrow.Fix
import Control.Arrow.Transformer.Abstract.ReachingDefinitions
import Control.Arrow.Transformer.Abstract.Environment
import Control.Arrow.Transformer.Abstract.Store
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Arrow.Transformer.Abstract.Fix
-- | Calculates the entry sets of which definitions may be reached for each statment.
run :: (?bound :: IV) => Int -> [LStatement] -> [(Label, M.Map Text (Pow Label))]
run k lstmts =
L.sortOn fst $
Map.toList $
-- Joins the reaching definitions for each statement for all call context.
-- Filters out statements created during execution that are not part
-- of the input program.
joinOnKey (\(store,(env,st)) _ -> case st of
stmt:_ | stmt `elem` blocks stmts ->
Just (label stmt, dropValues (combineMaps env store))
_ -> Nothing) $
-- get the fixpoint cache
fst $
-- Run the computation
S.runChaoticT
(runFixT' iterationStrategy
(runTerminatingT
(runErrorT
(runStoreT
(runReachingDefsT'
(runEnvT
(runIntervalT
(Generic.run ::
Fix [Statement] ()
(IntervalT
(EnvT Text Addr
(ReachingDefsT Label
(StoreT Addr (Val, Pow Label)
(ErrorT (Pow String)
(TerminatingT
(FixT () () _))))))) [Statement] ()))))))))
(M.empty,(SM.empty,stmts))
where
stmts = generate (sequence lstmts)
iterationStrategy = S.chaotic stackWiden widenResult
stackWiden = SW.groupBy (L.iso (\(store,(ev,sts)) -> (sts,(ev,store)))
(\(sts,(ev,store)) -> (store,(ev,sts))))
$ SW.maxSize k
$ SW.reuseFirst
$ SW.fromWidening (SM.widening W.finite W.** M.widening (widenVal W.** W.finite))
$ SW.finite
widenVal = widening (W.bounded ?bound I.widening)
widenResult = T.widening $ E.widening W.finite (M.widening (widenVal W.** W.finite) W.** W.finite)
combineMaps :: (Identifiable k, Identifiable a) => SM.Map k a -> M.Map a v -> M.Map k v
combineMaps env store = M.fromList [ (a,c) | (a,b) <- fromJust (SM.toList env)
, Just c <- [M.unsafeLookup b store]]
dropValues :: M.Map a (v,l) -> M.Map a l
dropValues = M.map snd
joinOnKey :: (Identifiable k',Complete v') => (k -> v -> Maybe (k',v')) -> HashMap k v -> HashMap k' v'
joinOnKey pred = Map.foldlWithKey' (\m k v -> case pred k v of
Just (k',v') -> Map.insertWith () k' v' m
Nothing -> m
) Map.empty
instance HasLabel (x,[Statement]) Label where
label (_,ss) = label (head ss)
......@@ -135,10 +135,10 @@ data Statement
instance Show Statement where
showsPrec _ e0 = case e0 of
Assign x e _ -> showString (unpack x) . showString " := " . shows e
While e body _ -> showString "while" . showParen True (shows e) . showString " " . shows body
If e ifB elseB _ -> showString "if" . showParen True (shows e) . showString " " . shows ifB . showString " " . shows elseB
Begin ss _ -> shows ss
Assign x e l -> shows l . showString ": " . showString (unpack x) . showString " := " . shows e
While e body l -> shows l . showString ": " . showString "while" . showParen True (shows e) . showString " " . shows body
If e ifB elseB l -> shows l . showString ": " . showString "if" . showParen True (shows e) . showString " " . shows ifB . showString " " . shows elseB
Begin ss l -> shows l . showString ": " . showString "{" . shows ss . showString "}"
type LStatement = State Label Statement
......@@ -154,10 +154,14 @@ whileLoops = L.prism' (\((c,b,l),ss) -> While c b l:ss)
_ -> Nothing)
ifExpr :: State Label Expr -> [State Label Statement] -> [State Label Statement] -> State Label Statement
ifExpr cond ifBranch elseBranch = If <$> cond <*> begin ifBranch <*> begin elseBranch <*> fresh
ifExpr cond ifBranch elseBranch = do
l <- fresh
If <$> cond <*> begin ifBranch <*> begin elseBranch <*> pure l
begin :: [LStatement] -> LStatement
begin ss = Begin <$> sequence ss <*> fresh
begin ss = do
l <- fresh
Begin <$> sequence ss <*> pure l
(=:) :: Text -> State Label Expr -> State Label Statement
x =: e = Assign x <$> e <*> fresh
......
......@@ -41,7 +41,6 @@ import Control.Arrow.Fix
import Control.Arrow.Fail
import Control.Arrow.Environment
import Control.Arrow.Store
import Control.Arrow.Conditional as Cond
import Control.Arrow.Random
import Control.Arrow.Abstract.Join
......@@ -71,7 +70,7 @@ run env ss =
(StoreT Addr Val
(ErrorT (Pow String)
(TerminatingT
(FixT _ _ () () (->))))))) [Statement] ()))))))
(FixT () () _)))))) [Statement] ()))))))
(M.empty,(SM.fromList env,generate <$> ss))
where
iterationStrategy = S.filter (L.second (L.second whileLoops))
......@@ -85,7 +84,8 @@ deriving instance ArrowFix x y c => ArrowFix x y (UnitT c)
instance (ArrowChoice c,Profunctor c) => ArrowAlloc (Text,Val,Label) Addr (UnitT c) where
alloc = arr $ \(_,_,l) -> return l
instance ArrowChoice c => IsVal Val (UnitT c) where
instance (ArrowChoice c, ArrowJoin c) => IsVal Val (UnitT c) where
type Join (UnitT c) x y = Complete y
boolLit = arr (const ())
and = arr (const ())
or = arr (const ())
......@@ -97,10 +97,7 @@ instance ArrowChoice c => IsVal Val (UnitT c) where
div = arr (const ())
eq = arr (const ())
lt = arr (const ())
if_ f1 f2 = proc (_,(x,y)) -> (f1 -< x) <> (f2 -< y)
instance (ArrowChoice c,Profunctor c) => ArrowRand Val (UnitT c) where
random = arr (const ())
instance (ArrowChoice c, ArrowJoin c) => ArrowCond Val (UnitT c) where
type Join (UnitT c) x y = Complete y
if_ f1 f2 = proc (_,(x,y)) -> (f1 -< x) <> (f2 -< y)
......@@ -52,7 +52,7 @@ spec = do
it "x := 1; y := 1; while(x < 3){x:= x + 1; i := 1, while(i < 2) {y := y + 1}}" $ do
let ?bound = I.Interval (-500) 500
let res = run 10 [("x",0),("y",1)] ["x" =: 1, "y" =: 1, while ("x" < 3) ["x" =: "x" + 1, "i" =: 1, while ("i" < 2) ["i" =: "i" + 1, "y" =: "y" + 1 ]]]
res `shouldBe` Terminating (Success [(0, num 3 3),(1,num 3 3),(9,num 2 2)])
res `shouldBe` Terminating (Success [(0, num 3 3),(1,num 3 3),(14,num 2 2)])
where
num i j = NumVal (I.Interval i j)
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE ImplicitParams #-}
module ReachingDefinitionsSpec(main,spec) where
import Prelude hiding ((<))
-- import Syntax
-- import ReachingDefinitionsAnalysis
-- import Data.Label
import Syntax
import ReachingDefinitionsAnalysis
import Data.Abstract.Interval as I
import Test.Hspec
......@@ -13,17 +14,83 @@ main :: IO ()
main = hspec spec
spec :: Spec
spec =
it "x:=5; y:=1; while(x>1){y:=x*y; x:=x-1}; z := y" $ do
pendingWith "need to extend fixpoint caching"
-- let stmts = generate (sequence ["x" =: 5, "y" =: 1, while (1 < "x") ["y" =: "x" * "y", "x" =: "x" - 1], "z" =: "y"])
-- run stmts `shouldContain`
-- zip (blocks stmts) [
-- -- Entry
-- [], -- 1: x:=5
-- [("x",[1])], -- 3: y:=1
-- [("x",[1,15]),("y",[3,11])], -- while(1 < x) {...}
-- [("x",[1,15]),("y",[3,11])], -- 11: y:=x*x
-- [("x",[1,15]),("y",[11])], -- 15: x:=x-1
-- [("x",[1,15]),("y",[3,11])] -- z:=y
-- ]
spec = do
it "x:=2; y:=4; x:=1; z:=0; if(x==y) {z:=y} {z:=y*y}; x:=z" $
let ?bound = I.Interval (-500) 500 in
let stmts = [
"x" =: 2,
"y" =: 4,
"x" =: 1,
"z" =: 0,
ifExpr ("x" ~= "y") [
"z" =: "y"
] [
"z" =: "y" * "y"
],
"x" =: "z"
]
in run 10 stmts `shouldMatchList` [
-- Entry-Set
(1, []), -- x := 2
(3, [("x",[1])]), -- y := 4
(5, [("x",[1]), ("y",[3])]), -- x := 1
(7, [("x",[5]), ("y",[3])]), -- z := 0
(8, [("x",[5]), ("y",[3]), ("z",[7])]), -- if (x == y) {
-- z := y // is never executed.
-- } else {
(19,[("x",[5]), ("y",[3]), ("z",[7])]), -- z := y * y
-- }
(21,[("x",[5]), ("y",[3]), ("z",[19])]) -- x := z
]
it "x:=5; y:=1; while(1<x){y:=x*y; x:=x-1}; z := y" $
let ?bound = I.Interval (-500) 500 in
let stmts = ["x" =: 5,
"y" =: 1,
while (1 < "x") [
"y" =: "x" * "y",
"x" =: "x" - 1
],
"z" =: "y"
]
in run 10 stmts `shouldMatchList` [
-- Entry-Set
(1, []), -- x:=5
(3, [("x",[1])]), -- y:=1
(4, [("x",[1,16]),("y",[3,12])]), -- while(1 < x) {
(12,[("x",[1,16]),("y",[3,12])]), -- y:=x*x
(16,[("x",[1,16]),("y",[12])]), -- x:=x-1
-- }
(18,[("x",[16]), ("y",[12])]) -- z:=y
]
it "x := 1; y := 1; while(x < 3){x:= x + 1; i := 1, while(i < 2) {y := y + 1}}; z:=y" $
let ?bound = I.Interval (-500) 500 in
let stmts = [
"x" =: 1,
"y" =: 1,
while ("x" < 3) [
"x" =: "x" + 1,
"i" =: 1,
while ("i" < 2) [
"i" =: "i" + 1,
"y" =: "y" + 1
]
],
"z" =: "y"
]
in run 10 stmts `shouldMatchList` [
-- Entry-Set
(1, []), -- x := 1
(3, [("x",[1])]), -- y := 1
(4, [("x",[1,12]),("y",[3,27])]), -- while(x < 3) {
(12,[("x",[1,12]),("y",[3,27])]), -- x := x + 1
(14,[("x",[12]), ("y",[3,27])]), -- i := 1
(15,[("x",[12]), ("y",[3,27]), ("i",[23,14])]), -- while(i < 2) {
(23,[("x",[12]), ("y",[3,27]), ("i",[14])]), -- i := i + 1
(27,[("x",[12]), ("y",[3,27]), ("i",[23])]), -- y := y + 1 } }
(29,[("x",[12]), ("y",[27])]) -- z := y
]
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