fixed building without fast; fixed abstract interp with simple nums -> some...

fixed building without fast; fixed abstract interp with simple nums -> some issue widenStore (intersect ???)
parent f5f7de85
"fib[5,10]",parallel,2,1,0,2
"fib[100,110]",parallel,3,5,16,6
"fib[0,∞]",parallel,3,2,5,3
"fact[5,10]",parallel,2,1,0,2
"fact[10,15]",parallel,3,5,5,6
"fact[0,∞]",parallel,2,3,3,4
"ackermann([0,3],[0,3])",parallel,2,1,0,2
"ackermann([0,∞],[0,∞])",parallel,2,1,5,2
"even(Even,[0,∞])",parallel,2,1,2,2
"diverge5",parallel,2,3,3,4
"fib[5,10]",Chaotic.simple,1,0,37,32
"fib[100,110]",Chaotic.simple,1,1,8,5
"fib[0,∞]",Chaotic.simple,1,1,5,3
"fact[5,10]",Chaotic.simple,1,0,9,20
"fact[10,15]",Chaotic.simple,1,1,6,9
"fact[0,∞]",Chaotic.simple,1,1,3,4
"ackermann([0,3],[0,3])",Chaotic.simple,1,0,491,372
"ackermann([0,∞],[0,∞])",Chaotic.simple,1,1,5,2
"even(Even,[0,∞])",Chaotic.simple,1,1,3,4
"diverge5",Chaotic.simple,1,1,6,11
"fib[5,10]",Chaotic.inner,1,0,11,16
"fib[100,110]",Chaotic.inner,1,1,6,4
"fib[0,∞]",Chaotic.inner,1,1,5,3
"fact[5,10]",Chaotic.inner,1,0,0,10
"fact[10,15]",Chaotic.inner,1,1,3,6
"fact[0,∞]",Chaotic.inner,1,1,2,3
"ackermann([0,3],[0,3])",Chaotic.inner,1,0,153,186
"ackermann([0,∞],[0,∞])",Chaotic.inner,1,1,5,2
"even(Even,[0,∞])",Chaotic.inner,1,1,5,6
"diverge5",Chaotic.inner,1,1,1,6
"fib[5,10]",Chaotic.outer,1,0,11,16
"fib[100,110]",Chaotic.outer,1,1,6,4
"fib[0,∞]",Chaotic.outer,1,1,5,3
"fact[5,10]",Chaotic.outer,1,0,0,10
"fact[10,15]",Chaotic.outer,1,1,3,6
"fact[0,∞]",Chaotic.outer,1,1,2,3
"ackermann([0,3],[0,3])",Chaotic.outer,1,0,153,186
"ackermann([0,∞],[0,∞])",Chaotic.outer,1,1,5,2
"even(Even,[0,∞])",Chaotic.outer,1,1,3,4
"diverge5",Chaotic.outer,1,1,1,6
......@@ -259,7 +259,7 @@ instance (Identifiable a, LowerBounded b, ArrowChoice c, Profunctor c) => ArrowC
write = CacheT $ proc _ -> returnA -< ()
setStable = CacheT $ proc _ -> returnA -< ()
{-# INLINE initialize #-}
{-# INLINE lookup #-}
-- {-# INLINE lookup #-} -- !!!!!!!!!!!! CAUSES GHC PANIC, when building without --fast
{-# INLINE write #-}
{-# INLINE update #-}
{-# INLINE setStable #-}
......
......@@ -24,7 +24,7 @@ import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Environment(extend')
import Control.Arrow.Fix
import Control.Arrow.Fix.Chaotic(chaotic,iterateInner)
import Control.Arrow.Fix.Chaotic(chaotic)
import qualified Control.Arrow.Fix.Context as Ctx
import Control.Arrow.Trans
import Control.Arrow.Closure (ArrowClosure,IsClosure(..))
......@@ -37,8 +37,8 @@ import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.Chaotic
import Control.Arrow.Transformer.Abstract.Fix.Context
import Control.Arrow.Transformer.Abstract.Fix.Stack
import Control.Arrow.Transformer.Abstract.Fix.Trace
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable(CacheT,Monotone)
import Control.Arrow.Transformer.Abstract.Fix.Trace()
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable hiding (Widening)
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Monad.State hiding (lift,fail)
......@@ -120,10 +120,10 @@ evalInterval env0 e = snd $
returnA -< (var,ctx)
iterationStrategy =
traceShow .
-- traceShow .
-- traceCache show .
Ctx.recordCallsite ?sensitivity (\(_,(_,expr)) -> case expr of App _ _ l -> Just l; _ -> Nothing) .
filter apply iterateInner -- chaotic
filter apply chaotic
widenVal :: Widening Val
widenVal = widening (I.bounded ?bound)
......
scheme/graph_files/gabriel/cpstak.png

91.9 KB | W: | H:

scheme/graph_files/gabriel/cpstak.png

161 KB | W: | H:

scheme/graph_files/gabriel/cpstak.png
scheme/graph_files/gabriel/cpstak.png
scheme/graph_files/gabriel/cpstak.png
scheme/graph_files/gabriel/cpstak.png
  • 2-up
  • Swipe
  • Onion skin
scheme/graph_files/gabriel/divrec.png

103 KB | W: | H:

scheme/graph_files/gabriel/divrec.png

61.7 KB | W: | H:

scheme/graph_files/gabriel/divrec.png
scheme/graph_files/gabriel/divrec.png
scheme/graph_files/gabriel/divrec.png
scheme/graph_files/gabriel/divrec.png
  • 2-up
  • Swipe
  • Onion skin
scheme/graph_files/gabriel/takl.png

276 KB | W: | H:

scheme/graph_files/gabriel/takl.png

287 KB | W: | H:

scheme/graph_files/gabriel/takl.png
scheme/graph_files/gabriel/takl.png
scheme/graph_files/gabriel/takl.png
scheme/graph_files/gabriel/takl.png
  • 2-up
  • Swipe
  • Onion skin
scheme/graph_files/scala-am/rsa.png

342 KB | W: | H:

scheme/graph_files/scala-am/rsa.png

323 KB | W: | H:

scheme/graph_files/scala-am/rsa.png
scheme/graph_files/scala-am/rsa.png
scheme/graph_files/scala-am/rsa.png
scheme/graph_files/scala-am/rsa.png
  • 2-up
  • Swipe
  • Onion skin
scheme/graph_files/test_subtraction.png

37.1 KB | W: | H:

scheme/graph_files/test_subtraction.png

27.7 KB | W: | H:

scheme/graph_files/test_subtraction.png
scheme/graph_files/test_subtraction.png
scheme/graph_files/test_subtraction.png
scheme/graph_files/test_subtraction.png
  • 2-up
  • Swipe
  • Onion skin
#lang scheme
(define (factorial n)
(if (= 0 n)
1
(* n (factorial (+ n 1)))))
(factorial 2)
\ No newline at end of file
(if (null? n)
(factorial (car (cons n '())))
(factorial (car (cons n '())))))
(factorial '(1))
\ No newline at end of file
#lang scheme
(- 2 1 1 4)
\ No newline at end of file
(define x 0)
(set! x 12)
x
......@@ -212,7 +212,7 @@ evalInterval env0 e = run (extend' (Generic.run_ ::
(->))))))))))) [Expr] Val))
(alloc, widening)
iterationStrategy
(widenStore widening, T.widening (E.widening W.finite widening))
(W.finite, T.widening (E.widening W.finite widening)) --something is wrong with widenStore
(Map.empty,(Map.empty,(env0,e0)))
where
e0 = generate (sequence e)
......
......@@ -187,8 +187,8 @@ type Out' = (Gr Expr (),
-- | 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 :: (?sensitivity :: Int, ?bound :: Int) => [(Text,Val)] -> [State Label Expr] -> Out'
evalInterval env0 e = run (extend' (Generic.run_ ::
evalInterval :: (?sensitivity :: Int) => Int -> [(Text,Val)] -> [State Label Expr] -> Out'
evalInterval bound env0 e = run (extend' (Generic.run_ ::
Fix'
(ValueT Val
(ErrorT (Pow String)
......@@ -201,9 +201,12 @@ evalInterval env0 e = run (extend' (Generic.run_ ::
(ContextT Ctx
(ControlFlowT Expr -- unter fixT liften
(->))))))))))) [Expr] Val))
(alloc, finite)
iterationStrategy
(finite, finite)
-- (alloc, widenVal)
-- iterationStrategy
-- (widenStore widenVal, T.widening (E.widening W.finite widenVal))
(alloc, widenVal)
iterationStrategy
(widenStore widenVal, T.widening (E.widening W.finite widenVal))
(Map.empty,(Map.empty,(env0,e0)))
where
e0 = generate (sequence e)
......@@ -218,20 +221,20 @@ evalInterval env0 e = run (extend' (Generic.run_ ::
Ctx.recordCallsite ?sensitivity (\(_,(_,exprs)) -> case exprs of [App _ _ l] -> Just l; _ -> Nothing) .
-- CF.recordControlFlowGraph' (\(_,(_,exprs)) -> case exprs of [App x y z] -> Just (App x y z); _ -> Nothing) .
CF.recordControlFlowGraph (\(_,(_,exprs)) -> head exprs) .
Fix.filter apply chaotic -- iterateInner --chaotic -- parallel -- iterateInner
Fix.filter apply iterateInner -- parallel -- iterateInner --chaotic -- parallel -- iterateInner
widenVal :: Widening Val
widenVal = widening (numGuardTop' ?bound)
widenVal = widening (numGuardTop' 100)
-- widenVal = finite
evalInterval' :: (?sensitivity :: Int, ?bound :: Int) => [(Text,Val)] -> [State Label Expr] -> Terminating (Error (Pow String) Val)
evalInterval' env exprs = snd $ snd $ snd $ evalInterval env exprs
evalInterval' :: (?sensitivity :: Int) => Int -> [(Text,Val)] -> [State Label Expr] -> Terminating (Error (Pow String) Val)
evalInterval' bound env exprs = snd $ snd $ snd $ evalInterval bound env exprs
{-# INLINE evalInterval' #-}
evalInterval'' :: (?sensitivity :: Int, ?bound :: Int) => [State Label Expr] -> (Gr Expr (), Terminating (Error (Pow String) Val))
evalInterval'' exprs =
let res = evalInterval [] exprs in (fst res, snd $ snd $ snd res)
evalInterval'' :: (?sensitivity :: Int) => Int -> [State Label Expr] -> (Gr Expr (), Terminating (Error (Pow String) Val))
evalInterval'' bound exprs =
let res = evalInterval bound [] exprs in (fst res, snd $ snd $ snd res)
{-# INLINE evalInterval'' #-}
......@@ -507,10 +510,10 @@ checkNum' op = proc vs -> if any op vs
else returnA -< BoolVal B.False
widening :: Widening Val -> Widening Val
-- widening bound (IntVal xs) (IntVal ys) = bound (IntVal xs) (IntVal ys)
-- widening bound (FloatVal xs) (FloatVal ys) = bound (FloatVal xs) (FloatVal ys)
widening _ (IntVal xs) (IntVal ys) = (Stable, IntVal (xs ys))
widening _ (FloatVal xs) (FloatVal ys) = (Stable, FloatVal (xs ys))
widening bound (IntVal xs) (IntVal ys) = bound (IntVal xs) (IntVal ys)
widening bound (FloatVal xs) (FloatVal ys) = bound (FloatVal xs) (FloatVal ys)
-- widening _ (IntVal xs) (IntVal ys) = (Stable, IntVal (xs ⊔ ys))
-- widening _ (FloatVal xs) (FloatVal ys) = (Stable, FloatVal (xs ⊔ ys))
widening _ (BoolVal x) (BoolVal y) = second BoolVal (B.widening x y)
widening _ (ClosureVal cs) (ClosureVal cs') = second ClosureVal $ C.widening W.finite cs cs'
widening _ StringVal StringVal = (Stable, StringVal)
......@@ -545,14 +548,14 @@ widenList _ _ =[ TypeError $ singleton "error when unifying lists, should not ha
numGuardTop' :: Int -> Widening Val
numGuardTop' bound (IntVal xs) (IntVal ys) = do
if any (> bound) (toList xs) || any (> bound) (toList ys)
then (Stable, TypeError "numvals reached upperbound")
then (Unstable, TypeError "numvals reached upperbound")
else (Stable, IntVal (xs <> ys))
numGuardTop' bound (FloatVal xs) (FloatVal ys) = do
let bound' = fromIntegral bound
if any (> bound') (toList xs) || any (> bound') (toList ys)
then (Stable, TypeError "numvals reached upperbound")
then (Unstable, TypeError "numvals reached upperbound")
else (Stable, FloatVal (xs <> ys))
numGuardTop' _ _ _ = (Stable, TypeError "expected elem of type num")
numGuardTop' _ _ _ = (Unstable, TypeError "expected elem of type num")
-- OPERATION HELPER ------------------------------------------------------------
......
......@@ -79,6 +79,7 @@ spec = do
describe "Gabriel-Benchmarks" $ do
it "cpstak" $ do
-- pending
let inFile = "gabriel//cpstak"
let expRes = Terminating (Success NumVal)
helper_test inFile expRes
......@@ -101,6 +102,7 @@ spec = do
helper_test inFile expRes
it "takl" $ do
-- pending
let inFile = "gabriel//takl"
let expRes = Terminating (Success $ BoolVal B.Top)
helper_test inFile expRes
......@@ -113,16 +115,19 @@ spec = do
helper_test inFile expRes
it "gcipd" $ do
-- pending
let inFile = "scala-am//gcipd"
let expRes = Terminating (Success NumVal)
helper_test inFile expRes
it "nqueens" $ do
-- pending
let inFile = "scala-am//nqueens"
let expRes = Terminating (Success NumVal)
helper_test inFile expRes
it "rsa" $ do
-- pending
let inFile = "scala-am//rsa"
let expRes = Terminating (Fail $ Pow.singleton "Expected elements of type num for op| [List [Num],Num]" <> "Scheme-Error")
helper_test inFile expRes
......
......@@ -41,21 +41,21 @@ spec = do
it "context sensitivity" $
let diamond = [if_ "w" "x" "y"] in do
let env = [("w", BoolVal B.Top), ("x", IntVal (Pow.singleton 1)), ("y", IntVal(Pow.singleton 2))]
let ?sensitivity = 0 in evalInterval' env diamond `shouldBe` Terminating (Success $ IntVal $ fromList [1,2])
let ?sensitivity = 1 in evalInterval' env diamond `shouldBe` Terminating (Success $ IntVal $ fromList [1,2])
let ?sensitivity = 0 in evalInterval' ?bound env diamond `shouldBe` Terminating (Success $ IntVal $ fromList [1,2])
let ?sensitivity = 1 in evalInterval' ?bound env diamond `shouldBe` Terminating (Success $ IntVal $ fromList [1,2])
it "should analyze let expression" $
let expr = [let_ [("x", lit $ S.Number 1)] ["x"]] in do
let ?sensitivity = 0 in evalInterval' [] expr `shouldBe` Terminating (Success $ IntVal $ fromList [1])
let ?sensitivity = 1 in evalInterval' [] expr `shouldBe` Terminating (Success $ IntVal $ fromList [1])
let ?sensitivity = 0 in evalInterval' ?bound [] expr `shouldBe` Terminating (Success $ IntVal $ fromList [1])
let ?sensitivity = 1 in evalInterval' ?bound [] expr `shouldBe` Terminating (Success $ IntVal $ fromList [1])
it "should analyze define" $
let exprs = [define "x" (lit $ S.Number 1),
set "x" (lit $ S.Number 2),
set "x" (lit $ S.Number 3),
"x"] in do
let ?sensitivity = 0 in evalInterval' [] exprs `shouldBe` Terminating (Success $ IntVal $ fromList [1,2,3])
let ?sensitivity = 2 in evalInterval' [] exprs `shouldBe` Terminating (Success $ IntVal $ fromList [1,2,3])
let ?sensitivity = 0 in evalInterval' ?bound [] exprs `shouldBe` Terminating (Success $ IntVal $ fromList [1,2,3])
let ?sensitivity = 2 in evalInterval' ?bound [] exprs `shouldBe` Terminating (Success $ IntVal $ fromList [1,2,3])
it "should return top for unifying two different types" $
......@@ -63,13 +63,13 @@ spec = do
set "x" (lit $ S.Number 2),
set "x" (lit $ S.Bool True),
"x"] in do
let ?sensitivity = 0 in evalInterval' [] exprs `shouldBe` Terminating (Success $ TypeError "cannot unify True and Int: {1, 2}")
let ?sensitivity = 2 in evalInterval' [] exprs `shouldBe` Terminating (Success $ TypeError "cannot unify True and Int: {1, 2}")
let ?sensitivity = 0 in evalInterval' ?bound [] exprs `shouldBe` Terminating (Success $ TypeError "cannot unify True and Int: {1, 2}")
let ?sensitivity = 2 in evalInterval' ?bound [] exprs `shouldBe` Terminating (Success $ TypeError "cannot unify True and Int: {1, 2}")
it "should terminate for the non-terminating program LetRec" $
let ?sensitivity = 2
in evalInterval' [] [let_rec [("id", lam ["x"] ["x"]),
in evalInterval' ?bound [] [let_rec [("id", lam ["x"] ["x"]),
("fix",lam ["x"] [app "fix" ["x"]])]
[app "fix" ["id"]]]
`shouldBe` NonTerminating
......@@ -79,7 +79,7 @@ spec = do
-----------------GABRIEL BENCHMARKS---------------------------------------------
describe "Gabriel-Benchmarks" $ do
let ?bound = 1000
let ?bound = 100
let ?sensitivity = 0
it "cpstak" $ do
pendingWith "takes to long"
......@@ -104,6 +104,7 @@ spec = do
helper_test inFile expRes
it "takl" $ do
pendingWith "takes too long"
let inFile = "gabriel//takl"
-- pendingWith "returns False instead of top/true because NV dont compare yet"
let expRes = Terminating (Success $ BoolVal B.Top)
......@@ -111,14 +112,16 @@ spec = do
-------------------SCALA-AM BENCHMARKS------------------------------------------
describe "Scala-AM-Benchmarks" $ do
let ?bound = 1000
let ?bound = 10
let ?sensitivity = 0
it "collatz" $ do
pendingWith "takes too long"
let inFile = "scala-am//collatz"
let expRes = Terminating (Success $ IntVal $ fromList [6])
helper_test inFile expRes
it "gcipd" $ do
pendingWith "takes too long"
let inFile = "scala-am//gcipd"
let expRes = Terminating (Success $ IntVal $ fromList [36])
helper_test inFile expRes
......@@ -231,7 +234,7 @@ helper_test inFile expRes = do
Right a ->
case match a of
Right b -> do
let (graph, res) = evalInterval'' [let_rec (getTopDefinesLam b) (getBody b)]
let (graph, res) = evalInterval'' ?bound [let_rec (getTopDefinesLam b) (getBody b)]
_ <- draw_graph inFile graph
res`shouldBe` expRes
Left b -> print b
......
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