Commit a65c6a33 authored by Sven Keidel's avatar Sven Keidel

fix iteration strategy of pcf and the while language

parent ed800cb2
Pipeline #12995 failed with stage
in 19 minutes and 38 seconds
......@@ -51,19 +51,20 @@ import Data.Abstract.InfiniteNumbers
import Data.Abstract.Interval (Interval)
import qualified Data.Abstract.Interval as I
import qualified Data.Abstract.Widening as W
import Data.Abstract.StackWidening(StackWidening)
import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating(Terminating)
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.Cache (Cache)
import qualified Data.Abstract.Cache as Cache
import Data.Abstract.IterationStrategy(IterationStrategy)
import qualified Data.Abstract.IterationStrategy as S
import GHC.Generics(Generic)
import GHC.Exts(IsString(..))
import Syntax (Expr(..))
import Syntax (Expr(..),apply)
import GenericInterpreter
type Env = F.Map Text (Text, CallString Label) Val
......@@ -79,8 +80,8 @@ type Addr = (Text,CallString Label)
-- maximum interval bound, the depth @k@ of the longest call string,
-- an environment, and the input of the computation.
evalInterval :: (?bound :: IV) => Int -> [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow String) Val)
evalInterval k env0 e = -- runInterp eval ?bound k env (generate e)
runFixT stackWiden Cache.stabilized (T.widening (E.widening W.finite widenVal))
evalInterval k env0 e =
runFixT iterationStrategy
(runTerminatingT
(runErrorT
(runContourT k
......@@ -93,17 +94,21 @@ evalInterval k env0 e = -- runInterp eval ?bound k env (generate e)
(ContourT Label
(ErrorT (Pow String)
(TerminatingT
(FixT _ Cache () () (->))))))) Expr Val))))))
(FixT _ _ () () (->))))))) Expr Val))))))
(env0,generate e)
where
widenVal = widening (W.bounded ?bound I.widening)
stackWiden :: SW.StackWidening _ (Env,Expr)
stackWiden = SW.filter (\(_,ex) -> case ex of Apply {} -> True; _ -> False)
$ SW.groupBy (L.iso' (\(env,exp) -> (exp,env)) (\(exp,env) -> (env,exp)))
$ SW.stack
iterationStrategy :: IterationStrategy _ _ (Env,Expr) _
iterationStrategy = S.filter apply
$ S.chaotic stackWiden (T.widening (E.widening W.finite widenVal))
stackWiden :: StackWidening _ (Env,(Expr,Label))
stackWiden = SW.groupBy (L.iso' (\(env,exp) -> (exp,env)) (\(exp,env) -> (env,exp)))
$ SW.reuseFirst
$ SW.maxSize 3
$ SW.fromWidening (F.widening widenVal)
$ SW.finite
widenVal = widening (W.bounded ?bound I.widening)
newtype IntervalT c x y = IntervalT { runIntervalT :: c x y } deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowFail e,ArrowJoin)
type instance Fix x y (IntervalT c) = IntervalT (Fix x y c)
......
......@@ -3,10 +3,12 @@
{-# LANGUAGE MultiParamTypeClasses #-}
module Syntax where
import Data.Text(Text,unpack)
import Data.Hashable
import Data.Label
import Data.String
import Data.Text(Text,unpack)
import Data.Hashable
import Data.Label
import Data.String
import Data.Lens (Prism')
import qualified Data.Lens as L
import Control.Monad.State
......@@ -104,3 +106,9 @@ instance Hashable Expr where
hashWithSalt s (IfZero e1 e2 e3 _) = s `hashWithSalt` (6::Int) `hashWithSalt` e1 `hashWithSalt` e2 `hashWithSalt` e3
hashWithSalt s (Y e _) = s `hashWithSalt` (7::Int) `hashWithSalt` e
hashWithSalt s (Apply e _) = s `hashWithSalt` (8::Int) `hashWithSalt` e
apply :: Prism' (env,Expr) (env,(Expr,Label))
apply = L.prism' (\(env,(e',l)) -> (env,Apply e' l))
(\(env,e) -> case e of
Apply e' l -> Just (env,(e',l))
_ -> Nothing)
......@@ -38,11 +38,10 @@ import Data.Abstract.FreeCompletion(FreeCompletion)
import Data.Abstract.InfiniteNumbers
import Data.Abstract.DiscretePowerset (Pow)
import qualified Data.Abstract.Widening as W
import qualified Data.Abstract.StackWidening as S
import qualified Data.Abstract.IterationStrategy as S
import qualified Data.Abstract.StackWidening as SW
import qualified Data.Abstract.Ordering as O
import qualified Data.Abstract.Equality as E
import Data.Abstract.Cache (Cache)
import qualified Data.Abstract.Cache as Cache
import qualified Data.Lens as L
import Data.Profunctor
......@@ -80,7 +79,7 @@ data Val = BoolVal Bool | NumVal IV | Top deriving (Eq,Generic)
run :: (?bound :: IV) => Int -> [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (M.Map Addr Val))
run k env ss =
fmap fst <$>
runFixT stackWiden Cache.stabilized widenTerm
runFixT iterationStrategy
(runTerminatingT
(runErrorT
(runStoreT
......@@ -92,21 +91,22 @@ run k env ss =
(EnvT Text Addr
(StoreT Addr Val
(ErrorT (Pow String)
(TerminatingT
(FixT _ Cache () () (->))))))) [Statement] ()))))))
(TerminatingT
(FixT _ _ () () (->))))))) [Statement] ()))))))
(M.empty,(SM.fromList env, generate <$> ss))
where
iterationStrategy = S.filter (L.second (L.second whileLoops))
$ S.chaotic stackWiden widenResult
stackWiden = SW.groupBy (L.iso (\(store,(ev,stmts)) -> (stmts,(ev,store))) (\(stmts,(ev,store)) -> (store,(ev,stmts))))
$ SW.maxSize k
$ SW.reuseFirst
$ SW.fromWidening (SM.widening W.finite W.** M.widening widenVal)
$ SW.finite
widenVal = widening (W.bounded ?bound I.widening)
widenTerm = T.widening $ E.widening W.finite (M.widening widenVal W.** W.finite)
stackWiden = S.filter' (L.second (L.second whileLoops))
$ S.groupBy (L.iso (\(store,(ev,stmts)) -> (stmts,(ev,store))) (\(stmts,(ev,store)) -> (store,(ev,stmts))))
$ S.stack
$ S.maxSize k
$ S.reuseFirst
$ S.fromWidening (SM.widening W.finite W.** M.widening widenVal)
widenResult = T.widening $ E.widening W.finite (M.widening widenVal W.** W.finite)
newtype IntervalT c x y = IntervalT { runIntervalT :: c x y } deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowFail e,ArrowEnv var val env,ArrowStore var val,ArrowJoin,PreOrd,Complete)
type instance Fix x y (IntervalT c) = IntervalT (Fix x y c)
......
......@@ -24,15 +24,15 @@ import qualified Data.Abstract.StrongMap as SM
import Data.Abstract.Terminating
import Data.Abstract.FreeCompletion(FreeCompletion)
import Data.Abstract.DiscretePowerset(Pow)
import qualified Data.Abstract.IterationStrategy as S
import qualified Data.Abstract.StackWidening as SW
import qualified Data.Abstract.Widening as W
import Data.Abstract.Cache(Cache)
import qualified Data.Abstract.Cache as Cache
import Data.Order
import Data.Label
import Data.Text (Text)
import Data.Profunctor
import qualified Data.Lens as L
import Control.Category
import Control.Arrow
......@@ -58,7 +58,7 @@ type Val = ()
run :: [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (M.Map Addr Val))
run env ss =
fmap fst <$>
runFixT SW.finite Cache.stabilized W.finite
runFixT iterationStrategy
(runTerminatingT
(runErrorT
(runStoreT
......@@ -71,8 +71,11 @@ run env ss =
(StoreT Addr Val
(ErrorT (Pow String)
(TerminatingT
(FixT _ Cache () () (->))))))) [Statement] ()))))))
(FixT _ _ () () (->))))))) [Statement] ()))))))
(M.empty,(SM.fromList env,generate <$> ss))
where
iterationStrategy = S.filter (L.second (L.second whileLoops))
$ S.chaotic SW.finite W.finite
newtype UnitT c x y = UnitT { runUnitT :: c x y }
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowFail e,ArrowEnv var val env,ArrowStore var val,ArrowJoin,PreOrd,Complete)
......
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