Parallel.hs 3.55 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC
  -fspecialise-aggressively
  -flate-specialise
  -fsimpl-tick-factor=500
  -fno-warn-orphans
  -fno-warn-partial-type-signatures
#-}
module TypedAnalysis.Parallel where

import           Prelude hiding (not,Bounded,fail,(.),exp,read)

import           Control.Category
25
import           Control.Arrow
26
import           Control.Arrow.Environment as Env
27
28
29
import           Control.Arrow.Fix(FixpointAlgorithm,FixpointCombinator)
import qualified Control.Arrow.Fix as Fix
import           Control.Arrow.Fix.Cache(ArrowCache,ArrowParallelCache,Widening)
30
31
import           Control.Arrow.Fix.Parallel as Par
import qualified Control.Arrow.Fix.Context as Ctx
32
import qualified Control.Arrow.Trans as Trans
33
34
35
36
37
import           Control.Arrow.Transformer.Value
import           Control.Arrow.Transformer.Abstract.FiniteEnvStore
import           Control.Arrow.Transformer.Abstract.LogError
import           Control.Arrow.Transformer.Abstract.Terminating
import           Control.Arrow.Transformer.Abstract.Fix
38
import           Control.Arrow.Transformer.Abstract.Fix.CallSite
39
import           Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable as Cache
40
import           Control.Arrow.Transformer.Abstract.Fix.Metrics as Metric
Sven Keidel's avatar
Sven Keidel committed
41
import           Control.Arrow.Transformer.Abstract.Fix.ControlFlow
42
-- import           Control.Arrow.Transformer.Abstract.Fix.Trace
43
44
45

import           Control.Monad.State hiding (lift,fail)

Sven Keidel's avatar
Sven Keidel committed
46
import           Data.Empty
47
48
import           Data.Label
import           Data.Text (Text)
49
-- import           Data.Text.Prettyprint.Doc
50
51
52
53

import qualified Data.Abstract.Widening as W


54
import           Syntax (Expr(App))
55
import qualified GenericInterpreter as Generic
56
57
import           TypedAnalysis

58
type Interp x y =
59
60
  ValueT Val
    (TerminatingT
61
      (LogErrorT Text
62
        (EnvStoreT Text Addr Val
Sven Keidel's avatar
Sven Keidel committed
63
          (FixT
64
            (MetricsT Metric.Monotone In
Sven Keidel's avatar
Sven Keidel committed
65
              (CacheT (Parallel Cache.Monotone) In Out
66
                (CallSiteT Label
Sven Keidel's avatar
Sven Keidel committed
67
68
                  (ControlFlowT Expr
                    (->))))))))) x y
69

70
eval :: (?sensitivity :: Int)
Sven Keidel's avatar
Sven Keidel committed
71
     => (forall c. (?cacheWidening :: Widening c, ArrowChoice c, ArrowCache In Out c, ArrowParallelCache In Out c) =>
72
                   (FixpointCombinator c In Out -> FixpointCombinator c In Out) -> FixpointAlgorithm (c In Out))
73
     -> [(Text,Addr)] -> [State Label Expr] -> (CFG Expr, (Metric.Monotone In, Out'))
Sven Keidel's avatar
Sven Keidel committed
74
eval algo env0 e =
Sven Keidel's avatar
Sven Keidel committed
75
76
  let ?cacheWidening = (storeErrWidening, W.finite) in
  let ?fixpointAlgorithm = transform $ algo $ \update_ ->
77
        -- Fix.trace printIn printOut .
78
        Fix.filter isApplication (Ctx.recordCallSite ?sensitivity (\(_,(_,exprs)) -> label $ head exprs)) . 
Sven Keidel's avatar
Sven Keidel committed
79
        Fix.recordEvaluated .
Sven Keidel's avatar
Sven Keidel committed
80
81
82
        Fix.filter' isFunctionBody update_ in
  second snd $ Trans.run (extend' (Generic.runFixed :: Interp [Expr] Val)) (empty,(empty,(env0,e0)))
  where
Sven Keidel's avatar
Sven Keidel committed
83
    e0 = generate (sequence e)
84
{-# INLINE eval #-}
85

86
87
88
89
90
evalParallel :: Eval
evalParallel = eval Par.parallel

evalADI :: Eval
evalADI = eval Par.adi
91

92
evalParallel':: Eval'
Sven Keidel's avatar
Sven Keidel committed
93
evalParallel' exprs = let (metrics,(cfg,res)) = evalParallel [] exprs in (metrics,(cfg,snd res))
94

95
evalADI':: Eval'
Sven Keidel's avatar
Sven Keidel committed
96
evalADI' exprs = let (metrics,(cfg,res)) = evalADI [] exprs in (metrics,(cfg,snd res))