Commit 0676b3ec authored by Sven Keidel's avatar Sven Keidel

fix pcf tests

parent c7cc105b
Pipeline #15731 failed with stages
in 12 minutes and 57 seconds
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
......@@ -17,7 +18,7 @@ class ArrowJoinContext cache a b c where
type Widening cache a :: *
joinContexts' :: Widening cache a -> IterationStrategy c (cache a b, a) b
joinContexts :: (ArrowState (cache a b) c, ArrowJoinContext cache a b c) => Widening cache a -> IterationStrategy c a b
joinContexts :: forall a cache b c. (ArrowState (cache a b) c, ArrowJoinContext cache a b c) => Widening cache a -> IterationStrategy c a b
joinContexts widen f = proc a -> do
cache <- get -< ()
joinContexts' widen (proc (cache,a) -> do
......
......@@ -22,9 +22,11 @@ module IntervalAnalysis where
import Prelude hiding (Bounded,fail,(.),exp)
import Control.Category
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Fix as Fix
import Control.Arrow.Fix.Context as Context
import Control.Arrow.Trans
import Control.Arrow.Environment as Env
import Control.Arrow.Order
......@@ -33,9 +35,10 @@ import Control.Arrow.Transformer.Abstract.Environment
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.Chaotic
import Control.Arrow.Transformer.Abstract.Fix.Trace
import Control.Arrow.Transformer.Abstract.Fix.ContextSensitive.CallSite
import Control.Arrow.Transformer.Abstract.Fix.ContextSensitive.Cache
import Control.Arrow.Transformer.Abstract.Fix.Context
import Control.Arrow.Transformer.Abstract.Fix.Stack
import Control.Arrow.Transformer.Abstract.Fix.Cache.Group
import Control.Arrow.Transformer.Abstract.Fix.Cache.ContextSensitive
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Monad.State hiding (lift,fail)
......@@ -47,7 +50,6 @@ import Data.Label
import Data.Order
import Data.Text (Text)
import Data.Utils
import Data.Proxy
import Data.Abstract.StrongMap(Map)
import qualified Data.Abstract.StrongMap as SM
......@@ -62,10 +64,10 @@ import qualified Data.Abstract.Terminating as T
import Data.Abstract.Closure (Closure)
import qualified Data.Abstract.Closure as C
import Data.Abstract.DiscretePowerset (Pow)
import Data.Abstract.CallString(CallString)
import GHC.Exts(IsString(..))
import GHC.Generics(Generic)
import GHC.TypeLits(KnownNat)
import Text.Printf
import Syntax (Expr(..),apply)
......@@ -81,39 +83,40 @@ data Val = NumVal IV | ClosureVal (Closure Expr Env) | TypeError (Pow String) de
-- | Run the abstract interpreter for an 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.
evalInterval :: forall k. (KnownNat k, ?bound :: IV) => Proxy k -> [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow String) Val)
evalInterval _ env0 e = snd $
run (Generic.eval ::
evalInterval :: (?sensitivity :: Int, ?bound :: IV) => [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow String) Val)
evalInterval env0 e = snd $
run (Generic.eval ::
Fix'
(ValueT Val
(EnvT Text Val
(ErrorT (Pow String)
(TerminatingT
(FixT _ _
(ChaoticT _ _
(CallSiteT k (Expr,Label)
(TraceT
(CacheT _ (Expr,Label) _ _ (->)))))))))) Expr Val)
(ChaoticT _
(StackT Stack _
(CacheT (Group (Cache (CallString _))) _ _
(ContextT (CallString _)
(->)))))))))) Expr Val)
iterationStrategy
widenEnv
(T.widening (E.widening W.finite widenVal))
(SM.fromList env0,e0)
where
e0 = generate e
vars = variables e0
iterationStrategy = Fix.filter apply
$ pruneEnv
$ Fix.trace
$ iterateInner
. joinContexts @((Expr,Label),Env) @(Group (Cache (CallString (Expr,Label)))) widenEnv
. callsiteSensitive ?sensitivity fst
. iterateInner
widenEnv = SM.widening widenVal
widenVal = widening (W.bounded ?bound I.widening)
pruneEnv strat f = proc ((exp,lab),env) -> do
pruneEnv f = proc ((exp,lab),env) -> do
case M.lookup exp vars of
Just (scope,used) -> strat f -< ((exp,lab),SM.delete (scope `H.difference` used) env)
Nothing -> strat f -< ((exp,lab),env)
Just (scope,used) -> f -< ((exp,lab),SM.delete (scope `H.difference` used) env)
Nothing -> f -< ((exp,lab),env)
instance (IsString e, ArrowChoice c, ArrowFail e c) => IsNum Val (ValueT Val c) where
type Join y (ValueT Val c) = ArrowComplete y (ValueT Val c)
......
......@@ -86,7 +86,7 @@ instance Show Expr where
app_prec = 10
lam_prec = 9
instance HasLabel Expr Label where
instance HasLabel Expr where
label e = case e of
Var _ l -> l
Lam _ _ l -> l
......
......@@ -3,9 +3,6 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
......@@ -33,7 +30,8 @@ import Control.Arrow.Transformer.FreeVars
import Control.Arrow.Transformer.Abstract.Environment(EnvT)
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.StackWidening.Cache
import Control.Arrow.Transformer.Abstract.Fix.Cache
import Control.Arrow.Transformer.Abstract.Fix.Cache.Basic
import Data.Empty
import Data.HashMap.Lazy(HashMap)
......@@ -47,7 +45,7 @@ import Data.Abstract.Widening as W
import Data.Maybe
import Data.Profunctor
import Data.Identifiable
import GHC.Exts(IsString(..))
import Syntax (Expr(..),apply)
......@@ -68,15 +66,15 @@ variables e =
(FreeVarsT Text
(EnvT Text Val
(FixT _ _
(CacheT _ _
(CacheT Cache _ _
(->))))))) Expr Val)
iterationStrategy
W.finite
(empty,e)
where
iterationStrategy = Fix.filter apply $ record
iterationStrategy = Fix.filter apply record
record :: (Identifiable a, Arrow c, Profunctor c) => IterationStrategy (CacheT a b c) a b
record :: (Identifiable a, Arrow c, Profunctor c) => IterationStrategy (CacheT Cache a b c) a b
record (CacheT f) = CacheT $ proc a -> do
b <- f -< a
modify' (\((a,b),Cache cache) -> ((),Cache (M.insert a (Stable,b) cache))) -< (a,b)
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
module IntervalAnalysisSpec where
import Prelude hiding (succ,pred)
import Data.Proxy
import Data.Abstract.DiscretePowerset(Pow)
import Data.Abstract.Error hiding (toEither)
import qualified Data.Abstract.Interval as I
......@@ -27,37 +24,38 @@ main = hspec spec
spec :: Spec
spec = do
return ()
let ?bound = I.Interval (-100) 100 in
sharedSpec (\env e -> toEither $ evalInterval (Proxy @3) env e) (NumVal . fromIntegral)
let ?bound = I.Interval (-100) 100; ?sensitivity = 3 in sharedSpec (\env e -> toEither $ evalInterval env e) (NumVal . fromIntegral)
describe "behavior specific to interval analysis" $ do
it "should execute both branches on IfZero on interval containing zero" $
let ?bound = I.Interval (-100) 100
in evalInterval (Proxy @1) [("x", num (-5) 5)]
?sensitivity = 1
in evalInterval [("x", num (-5) 5)]
(ifZero "x" (succ zero) (pred zero))
`shouldBe` Terminating (Success (num (-1) 1))
it "should compute 0 + -1 + 1 = 0" $
let ?bound = I.Interval (-100) 100
in evalInterval (Proxy @1) [] (succ (pred zero)) `shouldBe`
?sensitivity = 1
in evalInterval [] (succ (pred zero)) `shouldBe`
Terminating (Success (num 0 0))
it "should analyse addition correctly" $
let ?bound = I.Interval 0 5
?sensitivity = 2
in do
evalInterval (Proxy @2) [] (app (app add zero) two) `shouldBe` Terminating (Success (num 2 2))
evalInterval (Proxy @2) [] (app (app add one) two) `shouldBe` Terminating (Success (num 3 3))
evalInterval [] (app (app add zero) two) `shouldBe` Terminating (Success (num 2 2))
evalInterval [] (app (app add one) two) `shouldBe` Terminating (Success (num 3 3))
pendingWith "This test bad: Addition is not defined for negative numbers."
evalInterval (Proxy @1) [("x", num 0 1)] (app (app add "x") two) `shouldBe` Terminating (Success (num 2 3))
evalInterval [("x", num 0 1)] (app (app add "x") two) `shouldBe` Terminating (Success (num 2 3))
it "should terminate for the non-terminating program" $
let ?bound = I.Interval 0 5
in do evalInterval (Proxy @2) [] (fix (lam "x" "x")) `shouldSatisfy`
?sensitivity = 2
in do evalInterval [] (fix (lam "x" "x")) `shouldSatisfy`
\c -> case c of Terminating (Success (ClosureVal _)) -> True; _ -> False
evalInterval (Proxy @2) [] (fix (lam "f" (lam "x" (app "f" "x")))) `shouldSatisfy`
evalInterval [] (fix (lam "f" (lam "x" (app "f" "x")))) `shouldSatisfy`
\c -> case c of Terminating (Success (ClosureVal _)) -> True; _ -> False
where
......
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