Chaotic.hs 3.79 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(IterationStrategy,chaotic,innermost',outermost')
30
import qualified Control.Arrow.Fix.Context as Ctx
31
import qualified Control.Arrow.Trans as Trans
32
import           Control.Arrow.Transformer.Value
33
import           Control.Arrow.Transformer.Abstract.FiniteEnvStore
34
35
36
37
import           Control.Arrow.Transformer.Abstract.LogError
import           Control.Arrow.Transformer.Abstract.Fix
import           Control.Arrow.Transformer.Abstract.Fix.Component as Comp
import           Control.Arrow.Transformer.Abstract.Fix.Context
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
60
          (FixT
61
            (MetricsT Metric.Monotone In
Sven Keidel's avatar
Sven Keidel committed
62
             (ComponentT Comp.Component  In
63
               (StackT Stack.Stack In
Sven Keidel's avatar
Sven Keidel committed
64
65
                 (CacheT Cache.Monotone In Out
                   (ContextT Ctx
66
                     (ControlFlowT Expr
67
                       c))))))))))) x y
Tomislav Pree's avatar
Tomislav Pree committed
68

Tomislav Pree's avatar
Tomislav Pree committed
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
evalChaotic :: (?sensitivity :: Int) => IterationStrategy _ In Out -> [(Text,Addr)] -> [LExpr] -> (CFG Expr, (Metric.Monotone In, Out'))
evalChaotic iterationStrat env0 e =
  let ?cacheWidening = (storeErrWidening, W.finite) in
  let ?fixpointAlgorithm = transform $
        Fix.fixpointAlgorithm $
        -- Fix.trace printIn printOut .
        Ctx.recordCallsite ?sensitivity (\(_,(_,exprs)) -> case exprs of App _ _ l:_ -> Just l; _ -> Nothing) .
        Fix.recordEvaluated .
        -- CFlow.recordControlFlowGraph' (\(_,(_,exprs)) -> case exprs of e':_ -> Just e'; _ -> Nothing) .
        -- Fix.filter' isFunctionBody (Fix.trace printIn printOut . chaotic iterationStrat)
        Fix.filter' isFunctionBody (chaotic iterationStrat) in
  second snd $ Trans.run (extend' (Generic.runFixed :: InterpT (->) [Expr] Val)) (empty,(empty,(env0,e0)))
  where
    e0 = generate (sequence e)
{-# INLINE evalChaotic #-}

evalInner :: Eval
evalInner = evalChaotic innermost'

evalOuter :: Eval
evalOuter = evalChaotic outermost'

evalInner' :: Eval'
evalInner' exprs = let (metrics,(cfg,res)) = evalInner [] exprs in (metrics,(cfg,snd res))

evalOuter':: Eval'
evalOuter' exprs = let (metrics,(cfg,res)) = evalOuter [] exprs in (metrics,(cfg,snd res))

eval' :: (?sensitivity :: Int) => [(Text,Addr)] -> [LExpr] -> (Errors,Terminating Val)
eval' env exprs = snd $ snd $ snd $ evalInner env exprs