Chaotic.hs 3.82 KB
Newer Older
1
2
3
4
5
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImplicitParams #-}
6
{-# LANGUAGE OverloadedStrings #-}
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
{-# 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.Chaotic where

23
import           Prelude hiding (not,Bounded,fail,(.),exp,read,IO)
24
25

import           Control.Category
Sven Keidel's avatar
Sven Keidel committed
26
import           Control.Arrow
27
import           Control.Arrow.Environment as Env
28
import qualified Control.Arrow.Fix as Fix
29
import           Control.Arrow.Fix.Chaotic(innermost,outermost)
30
import qualified Control.Arrow.Fix.Context as Ctx
31
import qualified Control.Arrow.Trans as Trans
32
33
34
35
36
import           Control.Arrow.Transformer.Value
import           Control.Arrow.Transformer.Abstract.FiniteEnvStore
import           Control.Arrow.Transformer.Abstract.LogError
import           Control.Arrow.Transformer.Abstract.Fix
import           Control.Arrow.Transformer.Abstract.Fix.Component as Comp
37
import           Control.Arrow.Transformer.Abstract.Fix.CallSite
38
import           Control.Arrow.Transformer.Abstract.Fix.Stack as Stack
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
42
import           Control.Arrow.Transformer.Abstract.Fix.ControlFlow
import           Control.Arrow.Transformer.Abstract.Terminating
43

Sven Keidel's avatar
Sven Keidel committed
44
import           Data.Empty
45
46
47
48
49
50
51
import           Data.Label
import           Data.Text (Text)

import qualified Data.Abstract.Widening as W
import           Data.Abstract.Terminating(Terminating)

import           TypedAnalysis
52
import           Syntax (LExpr,Expr(App))
53
54
import           GenericInterpreter as Generic

55
type InterpT c x y =
56
57
  (ValueT Val
    (TerminatingT
58
      (LogErrorT Text
59
        (EnvStoreT Text Addr Val
Sven Keidel's avatar
Sven Keidel committed
60
          (FixT
61
            (MetricsT Metric.Monotone In
Sven Keidel's avatar
Sven Keidel committed
62
63
64
             (ComponentT Comp.Component  In
               (StackT Stack.Stack In
                 (CacheT Cache.Monotone In Out
65
                   (CallSiteT Label
66
67
                     (ControlFlowT Expr
                       c))))))))))) x y
68

69
evalChaotic :: (?sensitivity :: Int) => Fix.FixpointCombinator _ In Out -> [(Text,Addr)] -> [LExpr] -> (CFG Expr, (Metric.Monotone In, Out'))
Sven Keidel's avatar
Sven Keidel committed
70
evalChaotic iterationStrat env0 e =
Sven Keidel's avatar
Sven Keidel committed
71
  let ?fixpointAlgorithm = transform $
72
        Fix.fixpointAlgorithm $
Sven Keidel's avatar
Sven Keidel committed
73
        -- Fix.trace printIn printOut .
74
        Fix.filter isApplication (Ctx.recordCallSite ?sensitivity (\(_,(_,exprs)) -> label $ head exprs)) . 
Sven Keidel's avatar
Sven Keidel committed
75
76
        Fix.recordEvaluated .
        -- CFlow.recordControlFlowGraph' (\(_,(_,exprs)) -> case exprs of e':_ -> Just e'; _ -> Nothing) .
77
        -- Fix.filter' isFunctionBody (Fix.trace printIn printOut . chaotic iterationStrat)
78
        Fix.filter' isFunctionBody iterationStrat in
79
  second snd $ Trans.run (extend' (Generic.runFixed :: InterpT (->) [Expr] Val)) (empty,(empty,(env0,e0)))
Sven Keidel's avatar
Sven Keidel committed
80
  where
81
    e0 = generate (sequence e)
82
{-# INLINE evalChaotic #-}
83

84
evalInner :: Eval
85
86
87
evalInner =
  let ?cacheWidening = (storeErrWidening, W.finite) in
  evalChaotic innermost
88
89

evalOuter :: Eval
90
91
92
evalOuter =
  let ?cacheWidening = (storeErrWidening, W.finite) in
  evalChaotic outermost
93

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

97
evalOuter':: Eval'
Sven Keidel's avatar
Sven Keidel committed
98
evalOuter' exprs = let (metrics,(cfg,res)) = evalOuter [] exprs in (metrics,(cfg,snd res))
99

Sven Keidel's avatar
Sven Keidel committed
100
eval' :: (?sensitivity :: Int) => [(Text,Addr)] -> [LExpr] -> (Errors,Terminating Val)
Sven Keidel's avatar
Sven Keidel committed
101
eval' env exprs = snd $ snd $ snd $ evalInner env exprs