Verified Commit e49ba202 authored by Sven Keidel's avatar Sven Keidel
Browse files

remove duplicate tests

parent 61196e52
Pipeline #61989 passed with stages
in 46 minutes and 57 seconds
{-# LANGUAGE Arrows #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fsimpl-tick-factor=200 -fno-warn-redundant-constraints -fno-warn-partial-type-signatures #-}
module ContextSensitivitySpec where
import Prelude hiding (lookup,Bounded,fail,Bool)
import TestPrograms hiding (Fun(..))
import Control.Monad(forM_)
import Control.Arrow
import Control.Arrow.Fix as F
import Control.Arrow.Fix.Context(ArrowContext,callsiteSensitive)
import Control.Arrow.Fix.Chaotic
import qualified Control.Arrow.Trans as Arrow
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.Component
import Control.Arrow.Transformer.Abstract.Fix.Stack
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable as Cache hiding (Widening)
import Control.Arrow.Transformer.Abstract.Fix.Context
import qualified Data.Abstract.Boolean as Abs
import Data.Abstract.Terminating (Terminating)
import qualified Data.Abstract.Terminating as T
import Data.Abstract.Widening (Widening)
import qualified Data.Abstract.Widening as W
import Data.Abstract.CallString
import Data.Boolean
import Data.Identifiable
import Data.Order
import Data.Hashable
import Data.Text.Prettyprint.Doc
import GHC.Generics
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec =
-- do
--describe "Parallel" (sharedSpec (\f -> snd . Arrow.run (toParallel f) (S.stackWidening ?stackWiden (S.parallel (T.widening ?widen)))))
describe "Chaotic" $ do
describe "inner component" $
callsiteSpec $ \f a ->
let ?contextWidening = ?widenA
?cacheWidening = T.widening ?widenB in
let ?fixpointAlgorithm = fixpointAlgorithm (callsiteSensitive ?sensitivity fst . chaotic innermost) in
snd $ Arrow.run (f :: ChaoticT _ _ _) a
describe "outer component" $
callsiteSpec $ \f a ->
let ?contextWidening = ?widenA
?cacheWidening = T.widening ?widenB in
let ?fixpointAlgorithm = fixpointAlgorithm (callsiteSensitive ?sensitivity fst . chaotic outermost) in
snd $ Arrow.run (f :: ChaoticT _ _ _) a
data Val = Num IV | Unit | Top deriving (Show,Eq,Generic,Hashable)
instance Pretty Val where pretty = viaShow
type Line = Int
{-# INLINE callsiteSpec #-}
callsiteSpec :: (forall lab a b.
(Show lab, Show a, Show b, Identifiable lab, Identifiable a, PreOrd lab, PreOrd a, Complete b,
?sensitivity :: Int, ?widenA :: Widening a, ?widenB :: Widening b)
=> Arr (lab,a) b -> (lab,a) -> Terminating b) -> Spec
callsiteSpec run = do
describe "diamond" $ do
let diamond :: Arr ((Line,Fun),Val) Val
diamond = fix $ \call -> proc ((_,fun),x) -> case fun of
Main -> do
call -< ((1,Fun1),Num (iv 1 1))
call -< ((2,Fun2),Num (iv 2 2))
call -< ((3,Fun1),Num (iv 3 3))
Fun1 ->
call -< ((4,Id),x)
Fun2 ->
call -< ((5,Id),x)
Id ->
returnA -< x
let ?widenA = W.finite
let ?widenB = W.finite
it "context insensitive" $
let ?sensitivity = 0 in
run diamond ((0,Main),Unit) `shouldBe` return Top
it "1-callsite sensitive" $
let ?sensitivity = 1 in
run diamond ((0,Main),Unit) `shouldBe` return (Num (iv 1 3))
it "2-callsite sensitive" $
let ?sensitivity = 2 in
run diamond ((0,Main),Unit) `shouldBe` return (Num (iv 3 3))
describe "mutual recursive functions" $ do
let ?widenA = W.finite
let ?widenB = W.finite
let runTests :: (?sensitivity :: Int) => [(EvenOdd,Int,Abs.Bool)] -> IO ()
runTests l = forM_ l $ \(eo,arg,res) ->
run evenOdd (eo,iv (fromIntegral arg) (fromIntegral arg)) `shouldBe` return res
it "context insensitive" $ do
let ?sensitivity = 0
runTests [
(Even,1,false), (Odd,1,true),
(Even,2,top), (Odd,2,top)
]
it "1-callsite sensitive" $ do
let ?sensitivity = 1
runTests [
(Even,1,false), (Odd,1,true),
(Even,2,true), (Odd,2,false),
(Even,3,top) , (Odd,3,top)
]
it "2-callsite sensitive" $ do
let ?sensitivity = 2
runTests [
(Even,1,false), (Odd,1,true),
(Even,2,true), (Odd,2,false),
(Even,3,false), (Odd,3,true),
(Even,4,top), (Odd,4,top)
]
instance PreOrd Val where
_ Top = True
Num x Num y = x y
Unit Unit = True
_ _ = False
instance Complete Val where
Num x Num y = Num (x y)
Unit Unit = Unit
_ _ = Top
data Fun = Main | Fun1 | Fun2 | Id deriving (Show,Eq,Generic)
instance Hashable Fun
instance PreOrd Fun where
e1 e2 = e1 == e2
type ChaoticT lab a b =
TerminatingT
(FixT
(ComponentT Component (lab,a)
(StackT Stack (lab,a)
(CacheT (Context (Cache.Proj2 (CtxCache (CallString lab))) Cache) (lab,a) (Terminating b)
(ContextT (CallString lab)
(->)))))) (lab,a) b
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module FixpointSpec where
import Prelude hiding (id,(.),lookup,Bounded,fail,iterate)
import TestPrograms
import Control.Category
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Fix.Stack (ArrowStack,ArrowStackDepth,ArrowStackElements,widenInput,maxDepth,reuseByMetric)
import qualified Control.Arrow.Fix.Stack as Stack
import Control.Arrow.Fix.Cache (ArrowCache,ArrowParallelCache)
import qualified Control.Arrow.Fix.Cache as Cache
import Control.Arrow.Fix.Chaotic (ArrowInComponent,chaotic,innermost,outermost)
import Control.Arrow.Fix.Parallel (parallel,adi)
import qualified Control.Arrow.Trans as Arrow
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.Metrics
import Control.Arrow.Transformer.Abstract.Fix.Component
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable hiding (Widening)
import Control.Arrow.Transformer.Abstract.Fix.Stack
import Data.Identifiable
import qualified Data.Metric as M
import Data.Abstract.InfiniteNumbers
import qualified Data.Abstract.Interval as I
import Data.Abstract.Terminating (Terminating)
import qualified Data.Abstract.Terminating as T
import Data.Abstract.Widening (Widening)
import qualified Data.Abstract.Widening as W
import Data.Text.Prettyprint.Doc
import Data.Order
import Text.Printf
import Test.Hspec hiding (parallel)
main :: IO ()
main = hspec spec
metricFile :: String
metricFile = "fixpoint.csv"
spec :: Spec
spec =
beforeAll (writeFile metricFile (printf "Function,Algorithm,%s\n" csvHeader)) $ do
describe "Parallel" $ fixpointSpec "parallel" (runParallel parallel)
describe "ADI" $ fixpointSpec "adi" (runParallel adi)
describe "Chaotic" $ do
describe "innermost component" $ fixpointSpec "innermost" (runChaotic (chaotic innermost))
describe "outermost component" $ fixpointSpec "outermost" (runChaotic (chaotic outermost))
fixpointSpec :: String -> (forall a b. (Pretty a, Pretty b, Identifiable a, Complete b, ?strat :: Strat a b, ?widen :: Widening b) => Arr a b -> a -> (Metrics a,Terminating b)) -> Spec
fixpointSpec algName eval = sharedSpec $ \name f a -> do
let (metrics,res) = eval f a
let csv = printf "\"%s%s\",%s,%s\n" name (show (pretty a)) algName (toCSV metrics)
appendFile metricFile csv
return res
{-# INLINE fixpointSpec #-}
sharedSpec :: (forall a b. (Pretty a, Pretty b, Identifiable a, PreOrd a, Complete b, ?strat :: Strat a b, ?widen :: Widening b)
=> String -> Arr a b -> a -> IO (Terminating b)) -> Spec
sharedSpec run = do
describe "fibonacci" $ do
it "fib[5,10] should be [5,55]" $
let ?strat = Strat id in
let ?widen = W.finite in
run "fib" fib (iv 5 10) `shouldBe'` return (iv 5 55)
it "fib[100,110] with widening should be [0,∞]" $
let ?strat = Strat (widenInput I.widening) in
let ?widen = I.widening in
run "fib" fib (iv 100 110) `shouldBe'` return (iv 0 Infinity)
it "fib[1,∞] should be [1,∞]" $
let ?strat = Strat (reuseByMetric euclid) in
let ?widen = I.widening in
run "fib" fib (iv 1 Infinity) `shouldBe'` return (iv 1 Infinity)
describe "factorial" $ do
it "fact[5,10] should be [5!,10!] = [12,3628800]" $
let ?strat = Strat id in
let ?widen = W.finite in
run "fact" fact (iv 5 10) `shouldBe'` return (iv 120 3628800)
it "fact[10,15] with stack depth 3 should be [10,15] * [9,14] * [8,13] * [1,∞] = [720,∞]" $
let ?strat = Strat (maxDepth 3 (widenInput I.widening)) in
let ?widen = I.widening in
run "fact" fact (iv 10 15) `shouldBe'` return (iv 720 Infinity)
it "fact[0,∞] should be [1,∞]" $
let ?strat = Strat id in
let ?widen = I.widening in
run "fact" fact (iv 0 Infinity) `shouldBe'` return (iv 1 Infinity)
describe "ackermann" $ do
it "ack([0,3],[0,3]) should be [1,61] " $
let ?strat = Strat id in
let ?widen = W.finite in
run "ackermann" ackermann (iv 0 3, iv 0 3) `shouldBe'` return (iv 1 61)
it "ack([0,∞],[0,∞]) with euclidian reuseByMetric should be [1,∞] " $
let ?strat = Strat (reuseByMetric (euclid M.** euclid)) in
let ?widen = I.widening in
run "ackermann" ackermann (iv 0 Infinity, iv 0 Infinity) `shouldBe'` return (iv 1 Infinity)
describe "even odd" $
it "even([0,∞]) should be top" $
let ?strat = Strat (reuseByMetric (M.unit M.** euclid)) in
let ?widen = W.finite in
run "even" evenOdd (Even,iv 0 Infinity) `shouldBe'` top
describe "diverge" $
it "should terminate with bottom" $
let ?strat = Strat id in
let ?widen = W.finite in
run "diverge" diverge 5 `shouldBe'` bottom
where
shouldBe' f g = do
x <- f
x `shouldBe` g
{-# INLINE shouldBe' #-}
{-# INLINE sharedSpec #-}
type ParallelT a b =
TerminatingT
(FixT
(MetricsT Metrics a
(StackT Stack a
(CacheT (Parallel Cache) a (Terminating b) (->))))) a b
runParallel :: forall a b.
(forall x y c. (Pretty x, Pretty y, Identifiable x, ArrowChoice c,
ArrowStack x c, ArrowStackDepth c, ArrowStackElements x c,
ArrowParallelCache x y c, ArrowCache x y c,
?cacheWidening :: Cache.Widening c) =>
(FixpointCombinator c x y -> FixpointCombinator c x y) -> FixpointAlgorithm (c x y))
-> ((Pretty a, Pretty b, Identifiable a, Complete b,
?strat :: Strat a b, ?widen :: Widening b) =>
Arr a b -> a -> (Metrics a,Terminating b))
runParallel algorithm f a =
let ?cacheWidening = T.widening ?widen in
let ?fixpointAlgorithm = algorithm (\update -> getStrat ?strat . update . Stack.push') in
snd $ Arrow.run (f :: ParallelT a b) a
{-# INLINE runParallel #-}
type ChaoticT a b =
TerminatingT
(FixT
(MetricsT Metrics a
(ComponentT Component a
(StackT Stack a
(CacheT Cache a (Terminating b) (->)))))) a b
runChaotic :: forall a b.
(forall x y c. (Pretty x, Pretty y, Identifiable x, ArrowChoice c,
ArrowStack x c, ArrowStackDepth c, ArrowStackElements x c,
ArrowInComponent x c, ArrowCache x y c,
?cacheWidening :: Cache.Widening c) =>
FixpointCombinator c x y)
-> ((Pretty a, Pretty b, Identifiable a, Complete b,
?strat :: Strat a b, ?widen :: Widening b) =>
Arr a b -> a -> (Metrics a,Terminating b))
runChaotic algorithm f a =
let ?cacheWidening = T.widening ?widen in
let ?fixpointAlgorithm = fixpointAlgorithm (getStrat ?strat . algorithm) in
snd $ Arrow.run (f :: ChaoticT a b) a
{-# INLINE runChaotic #-}
{-# LANGUAGE OverloadedLists #-}
module FlatEnvironmentSpec where
import Prelude hiding (Maybe(..))
import qualified Data.Abstract.Environment.Flat as Env
import Data.Abstract.Closure
import Data.Abstract.Maybe
import Data.Order
import Test.Hspec
type Env = Env.Env String (Closure Int)
spec :: Spec
spec = do
it "Env.fromList should create a mutual recursive environment" $ do
let env = Env.fromList [ ("foo", closure 1 ())
, ("bar", closure 2 ())] :: Env
Env.lookup "foo" env `shouldBe` Just (closure 1 env)
Env.lookup "bar" env `shouldBe` Just (closure 2 env)
it "inserting closures into empty environment should not create a recursive binding" $ do
let env1 = Env.insertNonRec "foo" (closure 1 ()) Env.empty :: Env
env2 = Env.insertNonRec "bar" (closure 2 ()) env1
Env.lookup "foo" env2 `shouldBe` Just (closure 1 (Env.mask [] env2))
Env.lookup "bar" env2 `shouldBe` Just (closure 2 (Env.mask ["foo"] env2))
it "inserting a recursive closure into an environment should not change the original bindings" $ do
let env1 = Env.fromList [ ("foo", closure 1 ())
, ("bar", closure 2 ())] :: Env
env2 = Env.insertRec [("baz", closure 3 ())] env1
Env.lookup "foo" env2 `shouldBe` Just (closure 1 (Env.mask ["foo", "bar"] env2))
Env.lookup "bar" env2 `shouldBe` Just (closure 2 (Env.mask ["foo", "bar"] env2))
Env.lookup "baz" env2 `shouldBe` Just (closure 3 env2)
it "inserting a binding into the environment twice should keep the environment the same" $ do
let env1 = Env.fromList [ ("foo", closure 1 ())
, ("bar", closure 2 ())] :: Env
env2 = Env.insertRec [("biz", closure 4 ())]
$ Env.insertRec [("baz", closure 3 ())] env1
env3 = Env.insertRec [("biz", closure 4 ())]
$ Env.insertRec [("baz", closure 3 ())] env2
env2 `shouldBe` env3
it "least upper bound of environments should combine closures" $ do
let env1 = Env.fromList [ ("foo", closure 1 ())
, ("bar", closure 2 ())] :: Env
env2 = Env.fromList [ ("foo", closure 3 ())
, ("baz", closure 4 ()) ] :: Env
env = env1 env2
Env.lookup "foo" env `shouldBe` Just [ (1,Env.mask ["foo", "bar"] env)
, (3,Env.mask ["foo", "baz"] env)
]
Env.lookup "bar" env `shouldBe` JustNothing (closure 2 (Env.mask ["foo", "bar"] env))
Env.lookup "baz" env `shouldBe` JustNothing (closure 4 (Env.mask ["foo", "baz"] env))
{-# LANGUAGE OverloadedLists #-}
module GrammarEnvironmentSpec where
import qualified Data.Abstract.Environment.Grammar as Env
import Data.Concrete.Closure
import Test.Hspec
type Env = Env.Env String (Closure Int)
spec :: Spec
spec = do
it "Env.fromList should create a mutual recursive environment" $ do
let env = Env.fromList [ ("foo", Closure 1 ())
, ("bar", Closure 2 ())] :: Env
Env.lookup "foo" env `shouldBe` Just (Closure 1 env)
Env.lookup "bar" env `shouldBe` Just (Closure 2 env)
it "inserting closures into empty environment should not create a recursive binding" $ do
let env1 = Env.insert "foo" (Closure 1) Env.empty :: Env
env2 = Env.insert "bar" (Closure 2) env1
Env.lookup "foo" env2 `shouldBe` Just (Closure 1 Env.empty)
Env.lookup "bar" env2 `shouldBe` Just (Closure 2 env1)
it "inserting a recursive closure into an environment should not change the original bindings" $ do
let env1 = Env.fromList [ ("foo", Closure 1 ())
, ("bar", Closure 2 ())] :: Env
env2 = Env.insertRec "baz" (Closure 3) env1
Env.lookup "foo" env2 `shouldBe` Just (Closure 1 env1)
Env.lookup "bar" env2 `shouldBe` Just (Closure 2 env1)
Env.lookup "baz" env2 `shouldBe` Just (Closure 3 env2)
it "inserting a binding into the environment twice should keep the environment the same" $ do
let env1 = Env.fromList [ ("foo", Closure 1 ())
, ("bar", Closure 2 ())] :: Env
env2 = Env.insertRec "biz" (Closure 4)
$ Env.insertRec "baz" (Closure 3) env1
env3 = Env.insertRec "biz" (Closure 4)
$ Env.insertRec "baz" (Closure 3) env2
env2 `shouldBe` env3
it "union of environments should be left biased" $ do
let env1 = Env.fromList [ ("foo", Closure 1 ())
, ("bar", Closure 2 ())] :: Env
env2 = Env.fromList [ ("foo", Closure 3 ())
, ("baz", Closure 4 ())] :: Env
env = Env.union env1 env2
Env.lookup "foo" env `shouldBe` Just (Closure 1 env1)
Env.lookup "bar" env `shouldBe` Just (Closure 2 env1)
Env.lookup "baz" env `shouldBe` Just (Closure 4 env2)
{-# LANGUAGE OverloadedLists #-}
module MapSpec where
import Prelude hiding (lookup,Maybe(..))
import Data.Order
import Data.Abstract.Maybe
import Data.Abstract.Map
import Data.Abstract.Sign
import Test.Hspec
import Text.Printf
spec :: Spec
spec =
let m1,m2,m3,m4 :: Map String Sign
m1 = [("x",Negative), ("y",Positive)]
m2 = [("x",Positive), ("z",Zero)]
m3 = [("x",Top),("y",Positive),("z",Zero)]
m4 = []
in do
it "lookup x ([x -> -, y -> +] U [x -> +, z -> 0]) = Just T" $ do
lookup "x" (m1 m2) `shouldBe` Just Top
it "lookup y ([x -> -, y -> +] U [x -> +, z -> 0]) = JustNothing +" $ do
lookup "y" (m1 m2) `shouldBe` JustNothing Positive
it "lookup z ([x -> -, y -> +] U [x -> +, z -> 0]) = JustNothing 0" $ do
lookup "z" (m1 m2) `shouldBe` JustNothing Zero
it "[x -> -, y -> +] <= [x -> -, y -> +] U [x -> +, z -> 0]" $ do
m1 `shouldBeLessThan` (m1 m2)
it "[x -> +, z -> 0] <= [x -> -, y -> +] U [x -> +, z -> 0]" $ do
m2 `shouldBeLessThan` (m1 m2)
it "[x -> T, y -> +, z -> 0] <= [x -> -, y -> +] U [x -> +, z -> 0]" $ do
m3 `shouldBeLessThan` (m1 m2)
it "Map.<= is reflexive" $ do
m4 `shouldBeLessThan` m4
m1 `shouldBeLessThan` m1
m2 `shouldBeLessThan` m2
m3 `shouldBeLessThan` m3
(m1 m2) `shouldBeLessThan` (m1 m2)
where
shouldBeLessThan :: (Show a, PreOrd a) => a -> a -> Expectation
shouldBeLessThan a b
| a b = return ()
| otherwise = expectationFailure $ printf "%s </= %s" (show a) (show b)
{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
This diff is collapsed.
module UtilsSpec(main, spec) where
import Control.Arrow
import Data.List(sort)
import Data.Utils
import GHC.Exts
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec =
describe "Powersets" $ do
it "powComplement [1,2,3]" $
map (sort *** sort) (toList (powComplement [1,2,3::Int])) `shouldMatchList`
[ ([1,2,3],[])
, ([2,3],[1])
, ([1,3],[2])
, ([3],[1,2])
, ([1,2],[3])
, ([2],[1,3])
, ([1],[2,3])
, ([],[1,2,3])
]
it "powComplementN 3 [1,2]" $
map (map sort) (toList (powComplementN 3 [1,2::Int])) `shouldMatchList`
[ [[1,2],[],[]]
, [[1],[2],[]]
, [[1],[],[2]]
, [[2],[1],[]]
, [[2],[],[1]]
, [[],[1,2],[]]
, [[],[1],[2]]
, [[],[2],[1]]
, [[],[],[1,2]]
]
it "powComplementPick [[A,B],[C,D],[E,F]]" $
map (map sort) (toList (powComplementPick [["A","B"],["C","D"],["E","F"]])) `shouldMatchList`
[ [["A","B"],[],[]]
, [["A"],["D"],[]]
, [["A"],[],["F"]]
, [["B"],["C"],[]]
, [["B"],[],["E"]]
, [[],["C","D"],[]]
, [[],["C"],["F"]]
, [[],["D"],["E"]]
, [[],[],["E","F"]]
]
it "powComplementPick [[A,B]]" $
map (map sort) (toList (powComplementPick [["A","B"]])) `shouldMatchList` [[["A","B"]]]
it "powComplementPick [[]]" $
toList (powComplementPick [[] :: [Int]]) `shouldMatchList` [[[]]]
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