{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} module Main where import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.Options import Test.Tasty.Runners import G2.Config import G2.Interface import G2.Language as G2 import G2.Liquid.Interface import Control.Exception import Data.Maybe import Data.Proxy import Data.Tagged import qualified Data.Text as T import System.Environment import System.FilePath import Type.Reflection (Typeable) import PeanoTest import HigherOrderMathTest import GetNthTest import DefuncTest import CaseTest import Expr import Typing import InputOutputTest import Reqs import TestUtils -- Run with no arguments for default test cases. -- All default test cases should pass. -- Run with flag '--test-options="todo yes"' to run test cases corresponding to to-be-fixed bugs. main :: IO () main = do as <- getArgs let todo = "--todo" `elem` as defaultMainWithIngredients (defaultIngredients ++ [TestReporter [ Option (Proxy :: Proxy ToDo) ] (\_ _ -> Just (\_ -> return (\_ -> return False))) ]) =<< if todo then todoTests else tests tests :: IO TestTree tests = return . testGroup "Tests" =<< sequence [ sampleTests , liquidTests , testFileTests , baseTests , primTests , exprTests , typingTests ] timeout :: Timeout timeout = mkTimeout 1 -- Test based on examples that are also good for demos sampleTests :: IO TestTree sampleTests = return . testGroup "Samples" =<< sequence [ checkExpr "tests/Samples/Peano.hs" 900 Nothing (Just "equalsFour") "add" 3 [RForAll $ not . peano_4_out, AtLeast 10] , checkExpr "tests/Samples/Peano.hs" 900 (Just "fstIsEvenAddToFour") (Just "fstIsTwo") "add" 3 [RExists peano_0_4, RExists peano_4_0, Exactly 2] , checkExpr "tests/Samples/Peano.hs" 1200 (Just "multiplyToFour") (Just "equalsFour") "add" 3 [RExists peano_1_4_5, RExists peano_4_1_5, Exactly 2] , checkExpr "tests/Samples/Peano.hs" 750 (Just "eqEachOtherAndAddTo4") Nothing "add" 3 [RForAll peano_2_2, Exactly 1] , checkExpr "tests/Samples/Peano.hs" 600 (Just "equalsFour") Nothing "add" 3 [RExists peano_0_4, RExists peano_1_3, RExists peano_2_2, RExists peano_3_1, RExists peano_4_0, Exactly 5] , checkExpr "tests/Samples/Peano.hs" 750 (Just "equalsFour") Nothing "multiply" 3 [RExists peano_1_4, RExists peano_2_2, RExists peano_4_1, Exactly 3] , checkExpr "tests/Samples/HigherOrderMath.hs" 800 (Just "isTrue0") Nothing "notNegativeAt0NegativeAt1" 2 [RExists negativeSquareRes, AtLeast 1] , checkExpr "tests/Samples/HigherOrderMath.hs" 600 (Just "isTrue1") Nothing "fixed" 3 [RExists abs2NonNeg, RExists squareRes, RExists fourthPowerRes, RForAll allabs2NonNeg, AtLeast 4] , checkExpr "tests/Samples/HigherOrderMath.hs" 600 Nothing Nothing "fixed" 3 [RExists abs2NonNeg, RExists squareRes, RExists fourthPowerRes, AtLeast 4] , checkExpr "tests/Samples/HigherOrderMath.hs" 600 (Just "isTrue2") Nothing "sameFloatArgLarger" 3 [RExists addRes, RExists subRes, AtLeast 2] , checkExpr "tests/Samples/HigherOrderMath.hs" 600 Nothing Nothing "functionSatisfies" 4 [RExists functionSatisfiesRes, AtLeast 1] , checkExpr "tests/Samples/HigherOrderMath.hs" 1000 Nothing Nothing "approxSqrt" 3 [AtLeast 2] -- The below test fails because Z3 returns unknown. -- , checkExpr "tests/Samples/HigherOrderMath.hs" 1200 (Just "isTrue2") Nothing "sameFloatArgLarger" 2 [RExists approxSqrtRes, RExists pythagoreanRes, AtLeast 2] , checkExpr "tests/Samples/McCarthy91.hs" 1000 (Just "lessThan91") Nothing "mccarthy" 2 [RForAll (\[App _ (Lit (LitInt x)), _] -> x <= 100), AtLeast 1] , checkExpr "tests/Samples/McCarthy91.hs" 400 (Just "greaterThan10Less") Nothing "mccarthy" 2 [RForAll (\[App _ (Lit (LitInt x)), _] -> x > 100), AtLeast 1] , checkExpr "tests/Samples/McCarthy91.hs" 1000 (Just "lessThanNot91") Nothing "mccarthy" 2 [Exactly 0] , checkExpr "tests/Samples/McCarthy91.hs" 1000 (Just "greaterThanNot10Less") Nothing "mccarthy" 2 [Exactly 0] , checkExpr "tests/Samples/GetNth.hs" 600 Nothing Nothing "getNth" 3 [AtLeast 10, RForAll getNthTest] , checkExpr "tests/Samples/GetNthPoly.hs" 600 Nothing Nothing "getNthInt" 3 [AtLeast 10, RForAll getNthErrTest] , checkExpr "tests/Samples/GetNthPoly.hs" 600 Nothing Nothing "getNthX" 3 [AtLeast 10, RForAll getNthErrGenTest] , checkExpr "tests/Samples/GetNthPoly.hs" 600 Nothing Nothing "getNthPeano" 3 [AtLeast 10, RForAll getNthErrGenTest] -- 533 , checkExpr "tests/Samples/GetNthPoly.hs" 600 Nothing Nothing "getNthCListInt" 3 [AtLeast 10, RForAll getNthErrGenTest2'] , checkExpr "tests/Samples/GetNthPoly.hs" 600 Nothing Nothing "getNthCListX" 3 [AtLeast 10, RForAll getNthErrGenTest2] , checkExpr "tests/Samples/GetNthPoly.hs" 1000 Nothing Nothing "getNth" 4 [AtLeast 10] , checkExpr "tests/Samples/GetNthPoly.hs" 1000 Nothing Nothing "cfmapInt" 3 [AtLeast 10, RForAll cfmapTest] , checkExpr "tests/Samples/GetNthPoly.hs" 1600 Nothing Nothing "cfmapIntX" 3 [AtLeast 10, RForAll cfmapTest] , checkExpr "tests/Samples/GetNthPoly.hs" 600 Nothing Nothing "cfmapIntCListInt" 3 [AtLeast 2, RForAll cfmapTest] , checkExprReaches "tests/Samples/GetNthErr.hs" 800 Nothing Nothing (Just "error") "getNth" 3 [AtLeast 8, RForAll errors] , checkExpr "tests/Samples/FoldlUses.hs" 1600 Nothing Nothing "sum" 2 [AtLeast 3] , checkExpr "tests/Samples/FoldlUses.hs" 1000 Nothing Nothing "dotProd" 3 [AtLeast 3] , checkExpr "tests/Samples/FoldlUsesPoly.hs" 600 Nothing Nothing "sumMinAndMax" 5 [AtLeast 10] , checkExpr "tests/Samples/FoldlUsesPoly.hs" 400 Nothing Nothing "maxes" 7 [AtLeast 10] , checkExpr "tests/Samples/FoldlUsesPoly.hs" 400 Nothing Nothing "switchInt" 2 [AtLeast 1] , checkExpr "tests/Samples/FoldlUsesPoly.hs" 400 Nothing Nothing "getInInt" 2 [AtLeast 1] , checkExpr "tests/Samples/FoldlUsesPoly.hs" 400 Nothing Nothing "switchP" 6 [AtLeast 1] ] liquidTests :: IO TestTree liquidTests = return . testGroup "Liquid" =<< sequence [ checkLiquid "tests/Liquid/SimpleMath.hs" "abs2" 2000 2 [RForAll (\[x, y] -> isDouble x ((==) 0) && isDouble y ((==) 0)), Exactly 1] , checkLiquid "tests/Liquid/SimpleMath.hs" "add" 800 3 [RForAll (\[x, y, z] -> isInt x $ \x' -> isInt y $ \y' -> isInt z $ \z' -> x' > z' || y' > z'), AtLeast 1] , checkLiquid "tests/Liquid/SimpleMath.hs" "subToPos" 1000 3 [RForAll (\[x, y, z] -> isInt x $ \x' -> isInt y $ \y' -> isInt z $ \z' -> x' > 0 && x' >= y' && z' <= 0), AtLeast 1] , checkLiquidWithNoCutOff "tests/Liquid/SimpleMath.hs" "fib" 4000 2 [RForAll (\[x, y] -> isInt x $ \x' -> isInt y $ \y' -> x' > y'), AtLeast 3] , checkLiquidWithNoCutOff "tests/Liquid/SimpleMath.hs" "fib'" 6000 2 [RForAll (\[x, y] -> isInt x $ \x' -> isInt y $ \y' -> x' > y'), AtLeast 3] , checkLiquid "tests/Liquid/SimpleMath.hs" "xSqPlusYSq" 1000 3 [RForAll (\[x, y, z] -> isInt x $ \x' -> isInt y $ \y' -> isInt z $ \z' -> x' + y' >= z'), AtLeast 1] , checkLiquid "tests/Liquid/SimplePoly.hs" "snd2Int" 800 3 [RForAll (\[x, y, z] -> isInt x $ \x' -> isInt y $ \y' -> isInt z $ \z' -> x' /= y' && y' == z'), Exactly 1] , checkLiquid "tests/Liquid/SimplePoly.hs" "sumPair" 800 2 [AtLeast 1, RForAll (\[App (App _ x) y, z] -> isInt x $ \x' -> isInt y $ \y' -> isInt z $ \z' -> x' > z' || y' > z')] , checkLiquid "tests/Liquid/SimplePoly.hs" "switchInt" 600 2 [Exactly 1, RForAll (\[App (App _ x) _, App (App _ _) y] -> getIntB x $ \ x' -> getIntB y $ \ y' -> x' == y')] , checkLiquid "tests/Liquid/Peano.hs" "add" 1400 3 [RForAll (\[x, y, _] -> x `eqIgT` zeroPeano || y `eqIgT` zeroPeano), AtLeast 5] , checkLiquid "tests/Liquid/Peano.hs" "fromInt" 600 2 [RForAll (\[x, y] -> isInt x (\x' -> x' == 0) && y `eqIgT` zeroPeano), AtLeast 1] , checkLiquidWithNoCutOff "tests/Liquid/GetNth.hs" "getNthInt" 2700 3 [AtLeast 3, RForAll getNthErrors] , checkLiquidWithCutOff "tests/Liquid/GetNth.hs" "sumC" 2000 1000 2 [AtLeast 3, RForAll (\[_, y] -> isInt y $ (==) 0)] , checkLiquidWithNoCutOff "tests/Liquid/GetNth.hs" "getNth" 2700 4 [AtLeast 3] , checkLiquidWithCutOff "tests/Liquid/GetNth.hs" "sumCList" 2000 1000 4 [AtLeast 3] , checkLiquid "tests/Liquid/DataRefTest.hs" "addMaybe" 1000 3 [AtLeast 1, RForAll (\[_, y, z] -> isInt y $ \y' -> appNthArgIs z (\z' -> isInt z' $ \z'' -> z'' <= y') 2)] , checkLiquid "tests/Liquid/DataRefTest.hs" "addMaybe2" 2000 3 [AtLeast 1, RForAll (\[x, _, _] -> appNthArgIs x (\x' -> isInt x' $ \x'' -> x'' >= 0) 2) , RForAll (\[_, y, z] -> isInt y $ \y' -> appNthArgIs z (\z' -> isInt z' $ \z'' -> z'' <= y') 2)] , checkLiquid "tests/Liquid/DataRefTest.hs" "getLeftInts" 2000 2 [AtLeast 1, RForAll (\[x, _] -> dcInAppHasName "Right" x 3)] , checkLiquid "tests/Liquid/DataRefTest.hs" "sumSameInts" 2000 3 [AtLeast 1, RForAll (\[x, y, _] -> dcInAppHasName "Right" x 3 && dcInAppHasName "Left" y 3)] , checkLiquid "tests/Liquid/DataRefTest.hs" "sub1" 1200 4 [AtLeast 1] , checkLiquid "tests/Liquid/NumOrd.hs" "subTuple" 1200 3 [AtLeast 1] , checkLiquid "tests/Liquid/CommentMeasures.hs" "d" 1000 2 [AtLeast 1] , checkLiquid "tests/Liquid/CommentMeasures.hs" "unpackCP'" 100000 2 [Exactly 0] , checkLiquid "tests/Liquid/CommentMeasures.hs" "unpackBool" 1000 2 [AtLeast 1, RForAll (\[_, r] -> getBoolB r (== False))] , checkLiquid "tests/Liquid/CommentMeasures.hs" "sumSameOneOfs" 100000 3 [Exactly 0] , checkLiquid "tests/Liquid/CommentMeasures.hs" "gets2As" 2000 3 [AtLeast 1, RExists (\[x, y, _] -> buriedDCName "B" x && buriedDCName "B" y)] , checkLiquid "tests/Liquid/CommentMeasures.hs" "gets2As'" 1000 3 [AtLeast 1, RExists (\[x, y, _] -> buriedDCName "A" x && buriedDCName "B" y) , RExists (\[x, y, _] -> buriedDCName "B" x && buriedDCName "A" y)] , checkLiquid "tests/Liquid/CommentMeasures.hs" "ge4gt5" 1000 2 [AtLeast 1, RForAll (\[x, y] -> appNth x 1 $ \x' -> isInt x' $ \x'' -> isInt y $ \y' -> x'' == 4 && y' == 5)] , checkLiquid "tests/Liquid/ConcatList.hs" "concat2" 800 3 [AtLeast 2] , checkLiquid "tests/Liquid/ConcatList.hs" "concat3" 800 3 [AtLeast 2] , checkLiquid "tests/Liquid/ConcatList.hs" "concat5" 1600 3 [AtLeast 1] , checkLiquidWithConfig "tests/Liquid/Tests/Group3.lhs" "f" 1 (mkConfigTestWithMap {steps = 2200}) [AtLeast 1] , checkLiquid "tests/Liquid/Nonused.hs" "g" 2000 1 [AtLeast 1] -- , checkLiquid "tests/Liquid/HigherOrderRef.hs" "f1" 2000 3 [Exactly 0] -- , checkLiquid "tests/Liquid/HigherOrderRef.hs" "f2" 2000 3 [AtLeast 4, RForAll (\[_, x, y] -> x == y)] -- , checkLiquid "tests/Liquid/HigherOrderRef.hs" "f3" 2000 3 [Exactly 0] -- , checkLiquid "tests/Liquid/HigherOrderRef.hs" "f4" 2000 3 [AtLeast 4, RForAll (\[_, x, _] -> isInt x $ \x' -> x' == 0)] -- , checkLiquid "tests/Liquid/HigherOrderRef.hs" "f5" 2000 3 [Exactly 0] -- , checkLiquid "tests/Liquid/HigherOrderRef.hs" "f6" 2000 3 [AtLeast 10] -- , checkLiquid "tests/Liquid/HigherOrderRef.hs" "f7" 2000 3 [AtLeast 10, RForAll (\[x, _, y] -> isInt x $ \x' -> isInt y $ \y' -> x' == y')] -- , checkLiquid "tests/Liquid/HigherOrderRef.hs" "f8" 2000 3 [AtLeast 10] -- , checkLiquid "tests/Liquid/HigherOrderRef.hs" "callf" 2000 3 [AtLeast 1] -- , checkLiquid "tests/Liquid/Error/Error1.hs" "f" 600 2 [AtLeast 1] , checkLiquid "tests/Liquid/Error/Error2.hs" "f1" 2000 4 [AtLeast 1] , checkLiquid "tests/Liquid/ZipWith.lhs" "distance" 1000 4 [AtLeast 3] , checkLiquid "tests/Liquid/HigherOrder2.hs" "f" 2000 2 [Exactly 0] , checkLiquid "tests/Liquid/HigherOrder2.hs" "h" 2000 2 [AtLeast 1] , checkLiquid "tests/Liquid/Ordering.hs" "oneOrOther" 1000 2 [Exactly 0] , checkLiquid "tests/Liquid/AddKV.lhs" "empty" 1000 3 [Exactly 0] , checkLiquid "tests/Liquid/PropSize.hs" "prop_size" 2000 1 [AtLeast 1] , checkLiquid "tests/Liquid/PropSize2.hs" "prop_size" 2000 1 [AtLeast 1] , checkLiquidWithConfig "tests/Liquid/WhereFuncs.lhs" "f" 3 (mkConfigTestWithMap {steps = 1000}) [Exactly 0] , checkLiquidWithConfig "tests/Liquid/WhereFuncs.lhs" "g" 3 (mkConfigTestWithMap {steps = 1000}) [Exactly 0] , checkLiquid "tests/Liquid/PropConcat.lhs" "prop_concat" 1000 1 [AtLeast 1] , checkLiquid "tests/Liquid/Distance.lhs" "distance" 1000 4 [AtLeast 1] , checkLiquid "tests/Liquid/MultModules/CallZ.lhs" "callZ" 1000 3 [AtLeast 1] , checkAbsLiquid "tests/Liquid/AddToEven.hs" "f" 2000 1 [ AtLeast 1 , RForAll $ \[i] r [(FuncCall { funcName = Name n _ _ _, returns = fcr }) ] -> n == "g" && isInt i (\i' -> i' `mod` 2 == 0 && isInt r (\r' -> isInt fcr (\fcr' -> r' == i' + fcr')))] , checkLiquid "tests/Liquid/ListTests.lhs" "r" 1000 1 [Exactly 0] , checkLiquid "tests/Liquid/ListTests.lhs" "prop_map" 1500 3 [AtLeast 3] , checkLiquid "tests/Liquid/ListTests.lhs" "prop_concat_1" 1500 1 [AtLeast 1] , checkAbsLiquid "tests/Liquid/ListTests2.lhs" "prop_map" 2000 4 [ AtLeast 3 , RForAll (\[_, _, f, _] _ [(FuncCall { funcName = Name n _ _ _, arguments = [_, _, _, _, f', _] }) ] -> n == "map" && f == f') ] , checkAbsLiquid "tests/Liquid/ListTests2.lhs" "replicate" 2000 3 [ AtLeast 3 , RForAll (\[_, nA, aA] _ [(FuncCall { funcName = Name n _ _ _, arguments = [_, _, nA', aA'] }) ] -> n == "replicate" && nA == nA' && aA == aA') ] , checkAbsLiquid "tests/Liquid/ListTests2.lhs" "prop_size" 2000 0 [ AtLeast 1 , RForAll (\[] _ [(FuncCall { funcName = Name n _ _ _, returns = r }) ] -> n == "length2" && getIntB r (/= 3)) ] , checkLiquid "tests/Liquid/MapReduceTest2.lhs" "mapReduce" 1500 3 [Exactly 0] , checkLiquid "tests/Liquid/MeasErr.hs" "f" 1500 2 [Exactly 0] , checkAbsLiquid "tests/Liquid/Replicate.hs" "replicate" 2000 3 [ AtLeast 1 , RExists (\_ _ [(FuncCall { funcName = Name n _ _ _ }) ] -> n == "foldl") ] , checkAbsLiquid "tests/Liquid/Replicate.hs" "r" 2000 2 [ AtLeast 1 , RExists (\_ _ [(FuncCall { funcName = Name n _ _ _ }) ] -> n == "foldl") ] , checkAbsLiquid "tests/Liquid/AbsTypeClass.hs" "callF" 1000 1 [ AtLeast 1 , RExists (\_ _ [(FuncCall { funcName = Name n _ _ _ }) ] -> n == "f") ] , checkAbsLiquid "tests/Liquid/AbsTypeClassVerified.hs" "callF" 10000 1 [ Exactly 0 ] ] -- Tests that are intended to ensure a specific feature works, but that are not neccessarily interesting beyond that testFileTests :: IO TestTree testFileTests = return . testGroup "TestFiles" =<< sequence [ checkExpr "tests/TestFiles/IfTest.hs" 400 Nothing Nothing "f" 3 [RForAll (\[App _ (Lit (LitInt x)), App _ (Lit (LitInt y)), App _ (Lit (LitInt r))] -> if x == y then r == x + y else r == y), AtLeast 2] , checkExpr "tests/TestFiles/AssumeAssert.hs" 400 Nothing (Just "assertGt5") "outShouldBeGt5" 2 [Exactly 0] , checkExpr "tests/TestFiles/AssumeAssert.hs" 400 Nothing (Just "assertGt5") "outShouldBeGe5" 2 [AtLeast 1] , checkExpr "tests/TestFiles/AssumeAssert.hs" 400 (Just "assumeGt5") (Just "assertGt5") "outShouldBeGt5" 2 [Exactly 0] , checkExpr "tests/TestFiles/AssumeAssert.hs" 400 (Just "assumeGt5") (Just "assertGt5") "outShouldBeGe5" 2 [Exactly 0] , checkExpr "tests/TestFiles/CheckSq.hs" 400 Nothing Nothing "checkSq" 2 [AtLeast 2, RExists (\[x, _] -> isInt x (\x' -> x' == 3))] , checkExpr "tests/TestFiles/Defunc1.hs" 400 Nothing Nothing "f" 2 [RExists defunc1Add1, RExists defunc1Multiply2, RExists defuncB, AtLeast 3] , checkExpr "tests/TestFiles/Defunc1.hs" 400 Nothing Nothing "x" 2 [AtLeast 1] , checkExpr "tests/TestFiles/Defunc1.hs" 600 Nothing Nothing "mapYInt" 3 [AtLeast 1] , checkExpr "tests/TestFiles/Defunc1.hs" 600 Nothing Nothing "makeMoney" 3 [AtLeast 3] , checkExpr "tests/TestFiles/Defunc1.hs" 1600 Nothing Nothing "compZZ" 4 [AtLeast 2, RForAll (\[_, _, _, x] -> getBoolB x not)] , checkExpr "tests/TestFiles/Defunc1.hs" 1600 Nothing Nothing "compZZ2" 4 [AtLeast 2, RForAll (\[_, _, _, x] -> getBoolB x not)] , checkExpr "tests/TestFiles/Defunc2.hs" 400 Nothing Nothing "funcMap" 3 [RForAll defunc2Check, AtLeast 30] , checkExpr "tests/TestFiles/MultCase.hs" 400 Nothing Nothing "f" 2 [ RExists (\[App _ (Lit (LitInt x)), y] -> x == 2 && getBoolB y id) , RExists (\[App _ (Lit (LitInt x)), y] -> x == 1 && getBoolB y id) , RExists (\[App _ (Lit (LitInt x)), y] -> x /= 2 && x /= 1 && getBoolB y not)] , checkExpr "tests/TestFiles/LetFloating/LetFloating.hs" 400 (Just "output6") Nothing "f" 2 [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x == 6)] , checkExpr "tests/TestFiles/LetFloating/LetFloating2.hs" 400 (Just "output16") Nothing "f" 2 [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x == 15)] , checkExpr "tests/TestFiles/LetFloating/LetFloating3.hs" 600 (Just "output32") Nothing "f" 2 [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x == 4)] , checkExpr "tests/TestFiles/LetFloating/LetFloating4.hs" 400 (Just "output12") Nothing "f" 2 [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x == 11)] , checkExpr "tests/TestFiles/LetFloating/LetFloating5.hs" 400 (Just "output19") Nothing "f" 3 [AtLeast 1, RForAll (\[App _ (Lit (LitInt x)), App _ (Lit (LitInt y)), _] -> x + y + 1 == 19)] , checkExpr "tests/TestFiles/LetFloating/LetFloating6.hs" 400 (Just "output32") Nothing "f" 2 [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x == 25)] , checkExpr "tests/TestFiles/TypeClass/TypeClass1.hs" 400 Nothing Nothing "f" 2 [RExists (\[x, y] -> x == y), Exactly 1] , checkExpr "tests/TestFiles/TypeClass/TypeClass2.hs" 400 Nothing Nothing "f" 2 [RExists (\[x, y] -> x == y), Exactly 1] , checkExpr "tests/TestFiles/TypeClass/TypeClass3.hs" 400 Nothing Nothing "f" 2 [RExists (\[x, y] -> getIntB x $ \x' -> getIntB y $ \y' -> x' + 8 == y'), Exactly 1] , checkExprWithConfig "tests/TestFiles/TypeClass/TypeClass4.hs" Nothing Nothing Nothing "f" 1 (mkConfigTestWithMap {steps = 1000}) [AtLeast 1] , checkExpr "tests/TestFiles/TypeClass/HKTypeClass1.hs" 400 (Just "largeJ") Nothing "extractJ" 2 [RForAll (\[x, ly@(App _ (Lit (LitInt y)))] -> appNthArgIs x (ly ==) 2 && y > 100), Exactly 1] , checkExpr "tests/TestFiles/TypeClass/HKTypeClass1.hs" 400 (Just "largeE") Nothing "extractE" 2 [RForAll (\[x, ly@(App _ (Lit (LitInt y)))] -> appNthArgIs x (ly ==) 4 && y > 100), Exactly 1] , checkExpr "tests/TestFiles/TypeClass/HKTypeClass1.hs" 400 Nothing Nothing "changeJ" 3 [RForAll (\[_, x, y] -> dcInAppHasName "J" x 2 && (dcInAppHasName "J" y 2 || isError y)), AtLeast 2] , checkExpr "tests/TestFiles/Case1.hs" 400 Nothing Nothing "f" 2 [ RExists (\[App _ (Lit (LitInt x)), y] -> x < 0 && dcHasName "A" y) , RExists (\[App _ (Lit (LitInt x)), y] -> x >= 0 && dcHasName "C" y), Exactly 2] , checkExpr "tests/TestFiles/Case2.hs" 400 Nothing Nothing "f" 2 [ RExists exists1 , RExists exists2 , RExists exists3 , RExists exists4 , AtLeast 4] , checkExpr "tests/TestFiles/Guards.hs" 400 (Just "g") Nothing "f" 2 [AtLeast 1, RExists (\[dc, _] -> getBoolB dc id)] , checkExpr "tests/TestFiles/Infinite.hs" 400 (Just "g") Nothing "f" 2 [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x <= 100 && x /= 80)] , checkExpr "tests/TestFiles/Strictness1.hs" 400 Nothing Nothing "f" 1 [AtLeast 1, RExists (\[(App x (App _ (Lit (LitInt y))))] -> dcHasName "A" x && y == 9)] , checkExpr "tests/TestFiles/Where1.hs" 400 Nothing Nothing "f" 2 [ RExists (\[App _ (Lit (LitInt x)), App _ (Lit (LitInt y))] -> x == 4 && y == 1) , RExists (\[App _ (Lit (LitInt x)), App _ (Lit (LitInt y))] -> x /= 4 && y == 1) ] , checkExpr "tests/TestFiles/Error/Error1.hs" 400 Nothing Nothing "f" 2 [AtLeast 1, RForAll(errors)] , checkExpr "tests/TestFiles/Error/Error1.hs" 400 Nothing Nothing "g" 2 [AtLeast 1, RForAll(errors)] , checkExpr "tests/TestFiles/Error/Error2.hs" 400 Nothing Nothing "f" 1 [AtLeast 1, RForAll(errors)] , checkExpr "tests/TestFiles/Error/Error3.hs" 400 Nothing Nothing "f" 2 [AtLeast 1, RForAll(errors)] , checkExpr "tests/TestFiles/Error/Error3.hs" 400 Nothing Nothing "g" 2 [AtLeast 1, RForAll(not . errors)] , checkExpr "tests/TestFiles/Error/Undefined1.hs" 400 Nothing Nothing "undefined1" 2 [AtLeast 1, RForAll(errors)] , checkExpr "tests/TestFiles/Error/Undefined1.hs" 400 Nothing Nothing "undefined2" 2 [AtLeast 1, RForAll(errors)] , checkExpr "tests/TestFiles/BadNames1.hs" 400 Nothing Nothing "abs'" 2 [Exactly 2] , checkExpr "tests/TestFiles/BadNames1.hs" 400 Nothing Nothing "xswitch" 2 [AtLeast 10] , checkExpr "tests/TestFiles/PolyDataTy1.hs" 400 Nothing Nothing "f" 3 [Exactly 2, RExists (\[x, _, y] -> x == y), RExists (\[_, App _ x, y] -> x == y)] , checkExpr "tests/TestFiles/PolyDataTy1.hs" 400 Nothing Nothing "getFstXIntInt" 2 [AtLeast 2, RExists (\[x, y] -> isApp x && isError y)] , checkExpr "tests/TestFiles/PolyDataTy1.hs" 400 Nothing Nothing "sum" 2 [AtLeast 3, RExists (\[x, y] -> isApp x && isError y)] , checkExpr "tests/TestFiles/MultiSplit.hs" 1000 (Just "equals1") Nothing "f" 3 [Exactly 0] , checkExpr "tests/TestFiles/MatchesFunc1.hs" 400 Nothing Nothing "f" 2 [RExists (\[x, y] -> getIntB x $ \x' -> getIntB y $ \y' -> y' == 6 + x'), AtLeast 1] , checkExpr "tests/TestFiles/RecordFields1.hs" 400 Nothing Nothing "f" 2 [RExists (\[x, y] -> appNthArgIs x notCast 0 && appNthArgIs x (\x' -> getIntB x' $ \x'' -> getIntB y $ \y' -> x'' + 1 == y') 1), Exactly 1] , checkExpr "tests/TestFiles/RecordFields1.hs" 400 Nothing Nothing "fCall" 1 [RExists (\[x] -> isInt x ((==) 35)), Exactly 1] , checkExpr "tests/TestFiles/RecordFields1.hs" 400 Nothing Nothing "g" 2 [ RExists (\[x, y] -> appNthArgIs x (dcHasName "A") 2 && appNthArgIs y (dcHasName "B") 2) , RExists (\[x, y] -> appNthArgIs x (dcHasName "B") 2 && appNthArgIs y (dcHasName "C") 2) , RExists (\[x, y] -> appNthArgIs x (dcHasName "C") 2 && appNthArgIs y (dcHasName "A") 2) , Exactly 3] , checkExpr "tests/TestFiles/Deriving/DerivingSimple.hs" 400 Nothing Nothing "eq" 3 [AtLeast 2, RForAll (\[_, _, x] -> isBool x)] , checkExpr "tests/TestFiles/Deriving/DerivingSimple.hs" 400 Nothing Nothing "lt" 3 [AtLeast 2, RForAll (\[_, _, x] -> isBool x)] , checkExpr "tests/TestFiles/Deriving/DerivingComp.hs" 800 Nothing Nothing "eq" 3 [AtLeast 2, RForAll (\[_, _, x] -> isBool x)] , checkExpr "tests/TestFiles/Deriving/DerivingComp.hs" 800 Nothing Nothing "lt" 3 [AtLeast 2, RForAll (\[_, _, x] -> isBool x)] , checkExpr "tests/TestFiles/Coercions/Age.hs" 400 Nothing Nothing "born" 1 [ Exactly 1 , RForAll (\[x] -> inCast x (\x' -> appNthArgIs x' (Lit (LitInt 0) ==) 1) (\(t1 :~ t2) -> isIntT t1 && typeNameIs t2 "Age"))] , checkExpr "tests/TestFiles/Coercions/Age.hs" 400 Nothing Nothing "yearPasses" 2 [ AtLeast 1 , RForAll (\[x, y] -> inCast x (const True) (\(_ :~ t2) -> typeNameIs t2 "Age") && inCast y (const True) (\(_ :~ t2) -> typeNameIs t2 "Age") )] , checkExpr "tests/TestFiles/Coercions/Age.hs" 400 Nothing Nothing "age" 2 [ AtLeast 1 , RForAll (\[x, y] -> inCast x (const True) (\(_ :~ t2) -> typeNameIs t2 "Age") && isInt y (const True))] , checkExpr "tests/TestFiles/Coercions/Age.hs" 400 Nothing Nothing "diffAge" 3 [ AtLeast 1 , RForAll (\[x, y, z] -> inCast x (const True) (\(_ :~ t2) -> typeNameIs t2 "Age") && inCast y (const True) (\(_ :~ t2) -> typeNameIs t2 "Age") && inCast z (const True) (\(_ :~ t2) -> typeNameIs t2 "Years"))] , checkExpr "tests/TestFiles/Coercions/Age.hs" 400 Nothing Nothing "yearBefore" 2 [ AtLeast 5 ] , checkExpr "tests/TestFiles/Coercions/NewType1.hs" 400 Nothing Nothing "add1N4" 2 [ Exactly 1 , RForAll (\[x, y] -> inCast x (const True) (\(_ :~ t2) -> typeNameIs t2 "N4") && inCast y (const True) (\(_ :~ t2) -> typeNameIs t2 "N4"))] , checkExpr "tests/TestFiles/Coercions/NewType1.hs" 400 Nothing Nothing "f" 2 [ Exactly 1 , RForAll (\[x, y] -> inCast x (const True) (\(_ :~ t2) -> typeNameIs t2 "NewX") && dcHasName "X" y)] , checkExpr "tests/TestFiles/Coercions/NewType1.hs" 400 Nothing Nothing "g" 2 [ Exactly 1 , RForAll (\[x, y] -> dcHasName "X" x && inCast y (const True) (\(_ :~ t2) -> typeNameIs t2 "NewX"))] , checkExpr "tests/TestFiles/Coercions/NewType1.hs" 400 Nothing Nothing "mapWInt" 3 [ AtLeast 2 , RForAll (\[_, x, y] -> isError y || (inCast x (const True) (\(_ :~ t2) -> typeNameIs t2 "W") && inCast x (const True) (\(_ :~ t2) -> typeNameIs t2 "W"))) ] , checkExpr "tests/TestFiles/Coercions/NewType1.hs" 400 Nothing Nothing "appLeftFloat" 3 [ AtLeast 2 , RExists (\[_, _, y] -> inCast y (\y' -> dcInAppHasName "L" y' 3) (const True)) , RExists (\[_, _, y] -> inCast y (\y' -> dcInAppHasName "R" y' 3) (const True))] , checkExpr "tests/TestFiles/Coercions/NewType1.hs" 400 Nothing Nothing "getLIntFloat" 2 [ AtLeast 2 , RExists (\[_, y] -> isInt y (const True)) , RExists (\[_, y] -> isError y)] , checkExpr "tests/TestFiles/Coercions/NewType1.hs" 400 Nothing Nothing "getRIntFloat" 2 [ AtLeast 2 , RExists (\[_, y] -> isFloat y (const True)) , RExists (\[_, y] -> isError y)] , checkExpr "tests/TestFiles/Coercions/NewType1.hs" 400 Nothing Nothing "getCIntFloatDouble" 2 [ AtLeast 2 , RExists (\[_, y] -> isFloat y (const True)) , RExists (\[_, y] -> isError y)] , checkExpr "tests/TestFiles/Coercions/NewType1.hs" 400 Nothing Nothing "getRIntFloatX'" 2 [ AtLeast 2 , RExists (\[x, y] -> inCast x (\x' -> dcInAppHasName "TR" x' 4) (const True) && isInt y (const True)) , RExists (\[_, y] -> isError y)] , checkInputOutput "tests/TestFiles/Coercions/BadCoerce.hs" "BadCoerce" "f" 400 3 [AtLeast 1] , checkExpr "tests/TestFiles/Expr.hs" 400 Nothing Nothing "leadingLams" 2 [AtLeast 5, RForAll (\[_, y] -> noUndefined y)] , checkInputOutput "tests/TestFiles/Strings/Strings1.hs" "Strings1" "con" 300 3 [AtLeast 10] , checkInputOutput "tests/TestFiles/Strings/Strings1.hs" "Strings1" "eq" 700 3 [AtLeast 10] , checkInputOutput "tests/TestFiles/Strings/Strings1.hs" "Strings1" "eqGt1" 700 3 [AtLeast 10] , checkInputOutput "tests/TestFiles/Strings/Strings1.hs" "Strings1" "capABC" 150 2 [AtLeast 10] , checkInputOutput "tests/TestFiles/Strings/Strings1.hs" "Strings1" "appendEq" 500 2 [AtLeast 5] , checkExpr "tests/TestFiles/Strings/Strings1.hs" 1000 Nothing Nothing "exclaimEq" 3 [AtLeast 5, RExists (\[_, _, r] -> dcHasName "True" r)] , checkInputOutput "tests/TestFiles/BadDC.hs" "BadDC" "f" 400 2 [AtLeast 5] , checkInputOutput "tests/TestFiles/BadDC.hs" "BadDC" "g" 400 2 [AtLeast 3] -- , checkInputOutput "tests/TestFiles/BadBool.hs" "BadBool" "f" 1400 4 [AtLeast 1] -- , checkExpr "tests/TestFiles/Coercions/GADT.hs" 400 Nothing Nothing "g" 2 [ AtLeast 2 -- , RExists (\[x, y] -> x == Lit (LitInt 0) && y == App (Data (PrimCon I)) (Lit (LitInt 0))) -- , RExists (\[x, _] -> x /= Lit (LitInt 0))] -- , checkExpr "tests/TestFiles/HigherOrderList.hs" 400 Nothing Nothing "g" 3 [AtLeast 10] ] baseTests :: IO TestTree baseTests = return . testGroup "Base" =<< sequence [ checkInputOutput "tests/Samples/Peano.hs" "Peano" "add" 400 3 [AtLeast 4] , checkInputOutput "tests/BaseTests/ListTests.hs" "ListTests" "test" 1000 2 [AtLeast 1] , checkInputOutput "tests/BaseTests/ListTests.hs" "ListTests" "maxMap" 1000 2 [AtLeast 4] , checkInputOutput "tests/BaseTests/ListTests.hs" "ListTests" "minTest" 1000 2 [AtLeast 2] , checkInputOutput "tests/BaseTests/ListTests.hs" "ListTests" "foldrTest2" 1000 2 [AtLeast 1] , checkInputOutput "tests/BaseTests/Tuples.hs" "Tuples" "addTupleElems" 1000 2 [AtLeast 2] , checkInputOutput "tests/BaseTests/MaybeTest.hs" "MaybeTest" "sumN" 1000 4 [AtLeast 6] , checkInputOutput "tests/BaseTests/MaybeTest.hs" "MaybeTest" "lengthN" 1000 5 [AtLeast 6] , checkInputOutput "tests/BaseTests/Other.hs" "Other" "check4VeryEasy2" 600 1 [AtLeast 1] ] primTests :: IO TestTree primTests = return . testGroup "Prims" =<< sequence [ checkInputOutput "tests/Prim/Prim2.hs" "Prim2" "quotI1" 1000 3 [AtLeast 4] , checkInputOutput "tests/Prim/Prim2.hs" "Prim2" "quotI2" 1000 3 [AtLeast 4] , checkInputOutput "tests/Prim/Prim2.hs" "Prim2" "remI1" 1000 3 [AtLeast 4] , checkInputOutput "tests/Prim/Prim2.hs" "Prim2" "remI2" 1000 3 [AtLeast 3] , checkInputOutput "tests/Prim/Prim2.hs" "Prim2" "p1List" 300000 1 [AtLeast 1] , checkInputOutput "tests/Prim/Prim2.hs" "Prim2" "p2List" 700000 1 [AtLeast 1] , checkInputOutput "tests/Prim/Prim2.hs" "Prim2" "integerToFloatList" 150000 1 [AtLeast 1] , checkInputOutput "tests/Prim/Prim3.hs" "Prim3" "int2FloatTest" 1000 2 [AtLeast 1] , checkInputOutput "tests/Prim/Prim3.hs" "Prim3" "int2DoubleTest" 1000 2 [AtLeast 1] ] -- To Do Tests -------------- todoTests :: IO TestTree todoTests = return . testGroup "To Do" =<< sequence [ checkLiquid "tests/Liquid/TyApps.hs" "goodGet" 1000 4 [Exactly 0] , checkLiquid "tests/Liquid/TyApps.hs" "getPosInt" 1000 4 [ AtLeast 1 , RForAll (\[_, _, (App _ x), y] -> getIntB x $ \x' -> getIntB y $ \y' -> x' == y' && y' == 10)] , checkLiquid "tests/Liquid/TyApps.hs" "getPos" 1000 4 [ AtLeast 1 , RExists (\[_, _, (App _ x), y] -> getIntB x $ \x' -> getIntB y $ \y' -> x' == y' && y' == 10)] , checkLiquid "tests/Liquid/FoldrTests.hs" "max2" 1000 2 [Exactly 0] , checkLiquid "tests/Liquid/FoldrTests.hs" "max3" 1000 2 [Exactly 0] , checkLiquid "tests/Liquid/SimpleAnnot.hs" "simpleF" 1000 1 [Exactly 0] , checkLiquid "tests/Liquid/Ordering.hs" "lt" 1000 2 [AtLeast 1] , checkLiquid "tests/Liquid/Ordering.hs" "gt" 1000 2 [AtLeast 1] , checkLiquid "tests/Liquid/WhereFuncs2.hs" "hCalls" 1000 3 [AtLeast 1] , checkLiquid "tests/Liquid/WhereFuncs2.hs" "i" 1000 2 [AtLeast 1] , checkAbsLiquid "tests/Liquid/AddToEvenWhere.hs" "f" 2000 1 [ AtLeast 1 , RForAll (\[i] r [(FuncCall { funcName = Name n _ _ _, returns = r' }) ] -> n == "g" && isInt i (\i' -> i' `mod` 2 == 0) && r == r' )] , checkLiquid "tests/Liquid/ListTests.lhs" "concat" 1000 2 [AtLeast 3] , checkLiquidWithConfig "tests/Liquid/MapReduceTest.lhs" "mapReduce" 2 (mkConfigTestWithMap {steps = 1500})[Exactly 0] , checkLiquid "tests/Liquid/NearestTest.lhs" "nearest" 1500 1 [Exactly 1] , checkExpr "tests/TestFiles/TypeClass/TypeClass5.hs" 800 Nothing Nothing "run" 2 [AtLeast 1] , checkExpr "tests/TestFiles/TypeClass/TypeClass5.hs" 800 Nothing Nothing "run2" 2 [AtLeast 0] , checkInputOutput "tests/Prim/Prim2.hs" "Prim2" "sqrtList" 10000 1 [AtLeast 1] , checkInputOutput "tests/BaseTests/MaybeTest.hs" "MaybeTest" "average" 2000 5 [AtLeast 6] , checkInputOutput "tests/BaseTests/MaybeTest.hs" "MaybeTest" "averageF" 2000 2 [AtLeast 6] , checkInputOutput "tests/BaseTests/MaybeTest.hs" "MaybeTest" "maybeAvg" 200 4 [AtLeast 6] , checkInputOutput "tests/Prim/Prim3.hs" "Prim3" "float2IntTest" 1000 2 [AtLeast 1] , checkInputOutput "tests/Prim/Prim3.hs" "Prim3" "double2IntTest" 1000 2 [AtLeast 1] ] data ToDo = RunMain | RunToDo deriving (Eq, Typeable) instance IsOption ToDo where defaultValue = RunMain parseValue s = let ws = words s in if "y" `elem` ws || "yes" `elem` ws then Just RunToDo else Nothing optionName = Tagged "todo" optionHelp = Tagged "Specifies whether to run the main, passing tests, or the todo tests." -- Generic helpers for tests ---------------------------- checkExpr :: String -> Int -> Maybe String -> Maybe String -> String -> Int -> [Reqs ([Expr] -> Bool)] -> IO TestTree checkExpr src stps m_assume m_assert entry i reqList = checkExprReaches src stps m_assume m_assert Nothing entry i reqList checkExprReaches :: String -> Int -> Maybe String -> Maybe String -> Maybe String -> String -> Int -> [Reqs ([Expr] -> Bool)] -> IO TestTree checkExprReaches src stps m_assume m_assert m_reaches entry i reqList = do checkExprWithConfig src m_assume m_assert m_reaches entry i (mkConfigTest {steps = stps}) reqList checkExprWithConfig :: String -> Maybe String -> Maybe String -> Maybe String -> String -> Int -> Config -> [Reqs ([Expr] -> Bool)] -> IO TestTree checkExprWithConfig src m_assume m_assert m_reaches entry i config reqList = do res <- testFile src m_assume m_assert m_reaches entry config let ch = case res of Left _ -> False Right exprs -> checkExprGen (map (\(inp, out) -> inp ++ [out]) exprs) i reqList return . testCase src $ assertBool ("Assume/Assert for file " ++ src ++ " with functions [" ++ (fromMaybe "" m_assume) ++ "] " ++ "[" ++ (fromMaybe "" m_assert) ++ "] " ++ entry ++ " failed.\n") ch testFile :: String -> Maybe String -> Maybe String -> Maybe String -> String -> Config -> IO (Either SomeException [([Expr], Expr)]) testFile src m_assume m_assert m_reaches entry config = try (testFileWithConfig src m_assume m_assert m_reaches entry config) testFileWithConfig :: String -> Maybe String -> Maybe String -> Maybe String -> String -> Config -> IO [([Expr], Expr)] testFileWithConfig src m_assume m_assert m_reaches entry config = do let proj = takeDirectory src r <- doTimeout (timeLimit config) $ runG2FromFile [proj] [src] [] (fmap T.pack m_assume) (fmap T.pack m_assert) (fmap T.pack m_reaches) (isJust m_assert || isJust m_reaches) (T.pack entry) config let (states, _) = maybe (error "Timeout") fst r return $ map (\(ExecRes { conc_args = i, conc_out = o}) -> (i, o)) states checkLiquidWithNoCutOff :: FilePath -> String -> Int -> Int -> [Reqs ([Expr] -> Bool)] -> IO TestTree checkLiquidWithNoCutOff fp entry stps i reqList = checkLiquidWithConfig fp entry i (mkConfigTest {steps = stps, cut_off = stps}) reqList checkLiquid :: FilePath -> String -> Int -> Int -> [Reqs ([Expr] -> Bool)] -> IO TestTree checkLiquid fp entry stps i reqList = checkLiquidWithConfig fp entry i (mkConfigTest {steps = stps}) reqList checkLiquidWithCutOff :: FilePath -> String -> Int -> Int -> Int -> [Reqs ([Expr] -> Bool)] -> IO TestTree checkLiquidWithCutOff fp entry stps co i reqList = checkLiquidWithConfig fp entry i (mkConfigTest {steps = stps, cut_off = co}) reqList checkLiquidWithConfig :: FilePath -> String -> Int -> Config -> [Reqs ([Expr] -> Bool)] -> IO TestTree checkLiquidWithConfig fp entry i config reqList = do res <- findCounterExamples' fp (T.pack entry) [] [] config let (ch, r) = case res of Nothing -> (False, Right ()) Just (Left e) -> (False, Left e) Just (Right exprs) -> (checkExprGen (map (\(ExecRes { conc_args = inp, conc_out = out}) -> inp ++ [out]) exprs ) i reqList, Right ()) return . testCase fp $ assertBool ("Liquid test for file " ++ fp ++ " with function " ++ entry ++ " failed.\n" ++ show r) ch checkAbsLiquid :: FilePath -> String -> Int -> Int -> [Reqs ([Expr] -> Expr -> [FuncCall] -> Bool)] -> IO TestTree checkAbsLiquid fp entry stps i reqList = checkAbsLiquidWithConfig fp entry i (mkConfigTest {steps = stps}) reqList checkAbsLiquidWithConfig :: FilePath -> String -> Int -> Config -> [Reqs ([Expr] -> Expr -> [FuncCall] -> Bool)] -> IO TestTree checkAbsLiquidWithConfig fp entry i config reqList = do res <- findCounterExamples' fp (T.pack entry) [] [] config let (ch, r) = case res of Nothing -> (False, Right []) Just (Left e) -> (False, Left e) Just (Right exprs) -> let te = checkAbsLHExprGen (map (\(ExecRes { final_state = s, conc_args = inp, conc_out = out}) -> (s, inp, out) ) exprs ) i reqList in (null te, Right te) return . testCase fp $ assertBool ("Liquid test for file " ++ fp ++ " with function " ++ entry ++ " failed.\n" ++ show r) ch findCounterExamples' :: FilePath -> T.Text -> [FilePath] -> [FilePath] -> Config -> IO (Maybe (Either SomeException [ExecRes [FuncCall]])) findCounterExamples' fp entry libs lhlibs config = let proj = takeDirectory fp in doTimeout (timeLimit config) $ try (return . fst. fst =<< findCounterExamples [proj] [fp] entry libs lhlibs config) errors :: [Expr] -> Bool errors e = case last e of Prim Error _ -> True _ -> False