{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} module Main where import Test.Tasty import Test.Tasty.HUnit ( testCase, assertBool, assertFailure ) import Test.Tasty.Options import Test.Tasty.Runners import G2.Config import G2.Interface import G2.Language as G2 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 Simplifications import Typing import UnionFindTests import UFMapTests import RewriteVerify.RewriteVerifyTest import G2.Translation import InputOutputTest import Reqs import TestUtils import qualified Data.Map.Lazy as M -- 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 :: TestTree tests = testGroup "Tests" [ sampleTests , testFileTests , extensionTests , baseTests , primTests , ioTests , exprTests , typingTests , simplificationTests , ufMapQuickcheck , unionFindQuickcheck , rewriteTests ] timeout :: Timeout timeout = mkTimeout 1 -- Test based on examples that are also good for demos sampleTests :: TestTree sampleTests = testGroup "Samples" [ checkExprAssert "tests/Samples/Peano.hs" 900 (Just "equalsFour") "add" [RForAll $ not . peano_4_out, AtLeast 10] , checkExprAssumeAssert "tests/Samples/Peano.hs" 900 (Just "fstIsEvenAddToFour") (Just "fstIsTwo") "add" [RExists peano_0_4, RExists peano_4_0, Exactly 2] , checkExprAssumeAssert "tests/Samples/Peano.hs" 1200 (Just "multiplyToFour") (Just "equalsFour") "add" [RExists peano_1_4_5, RExists peano_4_1_5, Exactly 2] , checkExprAssumeAssert "tests/Samples/Peano.hs" 750 (Just "eqEachOtherAndAddTo4") Nothing "add" [RForAll peano_2_2, Exactly 1] , checkExprAssumeAssert "tests/Samples/Peano.hs" 600 (Just "equalsFour") Nothing "add" [ RExists peano_0_4 , RExists peano_1_3 , RExists peano_2_2 , RExists peano_3_1 , RExists peano_4_0 , Exactly 5] , checkExprAssumeAssert "tests/Samples/Peano.hs" 750 (Just "equalsFour") Nothing "multiply" [ RExists peano_1_4 , RExists peano_2_2 , RExists peano_4_1 , Exactly 3] , checkExprAssume "tests/Samples/HigherOrderMath.hs" 800 (Just "isTrue0") "notNegativeAt0NegativeAt1" [RExists negativeSquareRes, AtLeast 1] , checkExprAssume "tests/Samples/HigherOrderMath.hs" 600 (Just "isTrue1") "fixed" [ RExists abs2NonNeg , RExists squareRes , RExists fourthPowerRes , RForAll allabs2NonNeg , AtLeast 4] , checkExpr "tests/Samples/HigherOrderMath.hs" 600 "fixed" [ RExists abs2NonNeg , RExists squareRes , RExists fourthPowerRes , AtLeast 4] , checkExprAssumeAssert "tests/Samples/HigherOrderMath.hs" 600 (Just "isTrue2") Nothing "sameFloatArgLarger" [ RExists addRes , RExists subRes , AtLeast 2] , checkExpr "tests/Samples/HigherOrderMath.hs" 600 "functionSatisfies" [RExists functionSatisfiesRes, AtLeast 1] , checkExpr "tests/Samples/HigherOrderMath.hs" 1000 "approxSqrt" [AtLeast 2] -- The below test fails because Z3 returns unknown. -- , checkExprAssume "tests/Samples/HigherOrderMath.hs" 1200 (Just "isTrue2") "sameFloatArgLarger" 2 -- [ RExists approxSqrtRes -- , RExists pythagoreanRes -- , AtLeast 2] , checkExprAssumeAssert "tests/Samples/McCarthy91.hs" 1000 (Just "lessThan91") Nothing "mccarthy" [ RForAll (\[App _ (Lit (LitInt x)), _] -> x <= 100) , AtLeast 1] , checkExprAssumeAssert "tests/Samples/McCarthy91.hs" 400 (Just "greaterThan10Less") Nothing "mccarthy" [ RForAll (\[App _ (Lit (LitInt x)), _] -> x > 100) , AtLeast 1] , checkExprAssumeAssert "tests/Samples/McCarthy91.hs" 1000 (Just "lessThanNot91") Nothing "mccarthy" [Exactly 0] , checkExprAssumeAssert "tests/Samples/McCarthy91.hs" 1000 (Just "greaterThanNot10Less") Nothing "mccarthy" [Exactly 0] , checkInputOutput "tests/Samples/GetNth.hs" "getNth" 600 [AtLeast 10] , checkInputOutputs "tests/Samples/GetNthPoly.hs" [ ("getNthInt", 600, [AtLeast 10]) , ("getNthX", 600, [AtLeast 10]) , ("getNthPeano", 600, [AtLeast 10]) , ("getNthCListInt", 600, [AtLeast 10]) , ("getNthCListX", 600, [AtLeast 10]) , ("getNth", 1000, [AtLeast 10]) , ("cfmapInt", 1000, [AtLeast 10]) , ("cfmapIntX", 1600, [AtLeast 10]) , ("cfmapIntCListInt", 600, [AtLeast 2]) ] , checkExprReaches "tests/Samples/GetNthErr.hs" 800 Nothing Nothing (Just "error") "getNth" [AtLeast 8, RForAll errors] , checkInputOutputs "tests/Samples/FoldlUses.hs" [ ("sum_foldl", 1600, [AtLeast 3]) , ("dotProd", 1000, [AtLeast 3]) ] , checkInputOutputs "tests/Samples/FoldlUsesPoly.hs" [ ("sumMinAndMax", 600, [AtLeast 10]) , ("maxes", 400, [AtLeast 10]) , ("switchInt", 400, [AtLeast 1]) , ("getInInt", 400, [AtLeast 1]) , ("switchP", 400, [AtLeast 1]) ] , checkInputOutput "tests/Samples/NQueens.hs" "allQueensSafe" 2000 [AtLeast 14] ] -- Tests that are intended to ensure a specific feature works, but that are not neccessarily interesting beyond that testFileTests :: TestTree testFileTests = testGroup "TestFiles" [ checkExpr "tests/TestFiles/IfTest.hs" 400 "f" [ 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] , checkExprAssert "tests/TestFiles/AssumeAssert.hs" 400 (Just "assertGt5") "outShouldBeGt5" [Exactly 0] , checkExprAssert "tests/TestFiles/AssumeAssert.hs" 400 (Just "assertGt5") "outShouldBeGe5" [AtLeast 1] , checkExprAssumeAssert "tests/TestFiles/AssumeAssert.hs" 400 (Just "assumeGt5") (Just "assertGt5") "outShouldBeGt5" [Exactly 0] , checkExprAssumeAssert "tests/TestFiles/AssumeAssert.hs" 400 (Just "assumeGt5") (Just "assertGt5") "outShouldBeGe5" [Exactly 0] , checkInputOutputs "tests/TestFiles/Char.hs" [ ("char", 400, [Exactly 2]) ] , checkExpr "tests/TestFiles/CheckSq.hs" 400 "checkSq" [AtLeast 2, RExists (\[x, _] -> isInt x (\x' -> x' == 3 || x' == -3))] , checkExpr "tests/TestFiles/Defunc1.hs" 400 "f" [RExists defunc1Add1, RExists defunc1Multiply2, RExists defuncB, AtLeast 3] , checkInputOutputs "tests/TestFiles/Defunc1.hs" [ ("x", 400, [AtLeast 1]) , ("mapYInt", 600, [AtLeast 1]) , ("makeMoney", 600, [AtLeast 2]) , ("compZZ", 1600, [AtLeast 2]) , ("compZZ2", 1600, [AtLeast 2]) ] , checkInputOutput "tests/TestFiles/Defunc2.hs" "funcMap" 400 [AtLeast 30] , checkExpr "tests/TestFiles/MultCase.hs" 400 "f" [ 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)] , checkExprAssumeAssert "tests/TestFiles/LetFloating/LetFloating.hs" 400 (Just "output6") Nothing "f" [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x == 6)] , checkExprAssumeAssert "tests/TestFiles/LetFloating/LetFloating2.hs" 400 (Just "output16") Nothing "f" [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x == 15)] , checkExprAssumeAssert "tests/TestFiles/LetFloating/LetFloating3.hs" 600 (Just "output32") Nothing "f" [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x == 4)] , checkExprAssumeAssert "tests/TestFiles/LetFloating/LetFloating4.hs" 400 (Just "output12") Nothing "f" [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x == 11)] , checkExprAssumeAssert "tests/TestFiles/LetFloating/LetFloating5.hs" 400 (Just "output19") Nothing "f" [AtLeast 1, RForAll (\[App _ (Lit (LitInt x)), App _ (Lit (LitInt y)), _] -> x + y + 1 == 19)] , checkExprAssumeAssert "tests/TestFiles/LetFloating/LetFloating6.hs" 400 (Just "output32") Nothing "f" [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x == 25)] , checkExpr "tests/TestFiles/TypeClass/TypeClass1.hs" 400 "f" [RExists (\[x, y] -> x == y), Exactly 1] , checkExpr "tests/TestFiles/TypeClass/TypeClass2.hs" 400 "f" [RExists (\[x, y] -> x == y), Exactly 1] , checkExpr "tests/TestFiles/TypeClass/TypeClass3.hs" 400 "f" [RExists (\[x, y] -> getIntB x $ \x' -> getIntB y $ \y' -> x' + 8 == y'), Exactly 1] , checkExpr "tests/TestFiles/TypeClass/TypeClass4.hs" 1000 "f" [AtLeast 1] , checkExprAssumeAssert "tests/TestFiles/TypeClass/HKTypeClass1.hs" 400 (Just "largeJ") Nothing "extractJ" [RForAll (\[x, ly@(App _ (Lit (LitInt y)))] -> appNthArgIs x (ly ==) 2 && y > 100), Exactly 1] , checkExprAssumeAssert "tests/TestFiles/TypeClass/HKTypeClass1.hs" 400 (Just "largeE") Nothing "extractE" [RForAll (\[x, ly@(App _ (Lit (LitInt y)))] -> appNthArgIs x (ly ==) 4 && y > 100), Exactly 1] , checkExpr "tests/TestFiles/TypeClass/HKTypeClass1.hs" 400 "changeJ" [RForAll (\[_, x, y] -> dcInAppHasName "J" x 2 && (dcInAppHasName "J" y 2 || isError y)), AtLeast 2] , checkExpr "tests/TestFiles/Case1.hs" 400 "f" [ 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 "f" [ RExists exists1 , RExists exists2 , RExists exists3 , RExists exists4 , AtLeast 4] , checkExprAssumeAssert "tests/TestFiles/Guards.hs" 400 (Just "g") Nothing "f" [AtLeast 1, RExists (\[dc, _] -> getBoolB dc id)] , checkExprAssumeAssert "tests/TestFiles/Infinite.hs" 400 (Just "g") Nothing "f" [AtLeast 1, RExists (\[App _ (Lit (LitInt x)), _] -> x <= 100 && x /= 80)] , checkExpr "tests/TestFiles/Strictness1.hs" 400 "f" [AtLeast 1, RExists (\[(App x (App _ (Lit (LitInt y))))] -> dcHasName "A" x && y == 9)] , checkExpr "tests/TestFiles/Where1.hs" 400 "f" [ 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) ] , checkInputOutputs "tests/TestFiles/Error/Error1.hs" [ ("f", 400, [AtLeast 1]) , ("g", 400, [AtLeast 1]) , ("f", 400, [AtLeast 1]) , ("f", 400, [AtLeast 1]) , ("g", 400, [AtLeast 1]) ] , checkInputOutputs "tests/TestFiles/Error/Undefined1.hs" [ ("undefined1", 400, [AtLeast 1]) , ("undefined2", 400, [AtLeast 1])] , checkInputOutput "tests/TestFiles/Error/IrrefutError.hs" "f" 400 [AtLeast 2] , checkInputOutputs "tests/TestFiles/BadNames1.hs" [ ("abs'", 400, [Exactly 2]) , ("xswitch", 400, [AtLeast 10]) ] , checkInputOutputs "tests/TestFiles/ListCallStack.hs" [ ("indexOf", 400, [AtLeast 2]) , ("headOf", 400, [AtLeast 2]) , ("tailOf", 400, [AtLeast 2]) , ("lastOf", 400, [AtLeast 2]) , ("initOf", 400, [AtLeast 2]) , ("cycleOf", 400, [AtLeast 2]) ] , checkExpr "tests/TestFiles/PolyDataTy1.hs" 400 "f" [Exactly 2, RExists (\[x, _, y] -> x == y), RExists (\[_, App _ x, y] -> x == y)] , checkExpr "tests/TestFiles/PolyDataTy1.hs" 400 "getFstXIntInt" [AtLeast 2, RExists (\[x, y] -> isApp x && isError y)] , checkExpr "tests/TestFiles/PolyDataTy1.hs" 400 "sum" [AtLeast 3, RExists (\[x, y] -> isApp x && isError y)] , checkExprAssumeAssert "tests/TestFiles/MultiSplit.hs" 1000 (Just "equals1") Nothing "f" [Exactly 0] , checkExpr "tests/TestFiles/MatchesFunc1.hs" 400 "f" [RExists (\[x, y] -> getIntB x $ \x' -> getIntB y $ \y' -> y' == 6 + x'), AtLeast 1] , checkInputOutput "tests/TestFiles/Read.hs" "concRead" 20000 [Exactly 1] , checkExpr "tests/TestFiles/RecordFields1.hs" 400 "f" [ 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 "fCall" [RExists (\[x] -> isInt x ((==) 35)), Exactly 1] , checkExpr "tests/TestFiles/RecordFields1.hs" 400 "g" [ 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] , checkInputOutputs "tests/TestFiles/Deriving/DerivingSimple.hs" [ ("eq", 400, [AtLeast 2]) , ("lt", 400, [AtLeast 2]) ] , checkInputOutputs "tests/TestFiles/Deriving/DerivingComp.hs" [ ("eq", 800, [AtLeast 2]) , ("lt", 800, [AtLeast 2]) ] , checkInputOutputs "tests/TestFiles/Coercions/Age.hs" [ ("born", 400, [Exactly 1]) , ("yearPasses", 400, [AtLeast 1]) , ("age", 400, [AtLeast 1]) , ("diffAge", 400, [AtLeast 1]) , ("yearBefore", 400, [AtLeast 5])] , checkInputOutputs "tests/TestFiles/Coercions/NewType1.hs" [ ("add1N4", 400, [Exactly 1]) , ("f", 400, [Exactly 1]) , ("g", 400, [Exactly 1]) , ("mapWInt", 400, [AtLeast 2]) , ("appLeftFloat", 400, [AtLeast 2]) , ("getLIntFloat", 400, [AtLeast 2]) , ("getRIntFloat", 400, [AtLeast 2]) , ("getCIntFloatDouble", 400, [AtLeast 2]) , ("getRIntFloatX'", 400, [AtLeast 2])] , checkInputOutput "tests/TestFiles/Coercions/BadCoerce.hs" "f" 400 [AtLeast 1] , checkInputOutput "tests/TestFiles/Expr.hs" "leadingLams" 400 [AtLeast 5] , checkExprAssume "tests/TestFiles/Subseq.hs" 1200 (Just "assume") "subseqTest" [AtLeast 1] , checkInputOutputs "tests/TestFiles/Strings/Strings1.hs" [ ("con", 300, [AtLeast 10]) , ("eq", 700, [AtLeast 10]) , ("eqGt1", 700, [AtLeast 10]) , ("capABC", 200, [AtLeast 10]) , ("appendEq", 500, [AtLeast 5]) ] , checkExpr "tests/TestFiles/Strings/Strings1.hs" 1000 "exclaimEq" [AtLeast 5, RExists (\[_, _, r] -> dcHasName "True" r)] , checkExpr "tests/TestFiles/Sets/SetInsert.hs" 700 "prop" [AtLeast 3] , checkInputOutputs "tests/TestFiles/BadDC.hs" [ ("f", 400, [AtLeast 5]) , ("g", 400, [AtLeast 3]) ] , checkInputOutputsTemplate "tests/HigherOrder/HigherOrder.hs" [ ("f", 50, [AtLeast 5]) , ("h", 100, [AtLeast 3]) , ("assoc", 200, [AtLeast 5]) , ("sf", 150, [AtLeast 5]) , ("thirdOrder", 75, [AtLeast 10]) , ("tupleTestMono", 175, [AtLeast 10])] , checkInputOutputsTemplate "tests/HigherOrder/PolyHigherOrder.hs" [ ("f", 50, [AtLeast 5]) , ("h", 200, [AtLeast 3]) , ("assoc", 200, [AtLeast 5]) , ("sf", 150, [AtLeast 5]) , ("tupleTest", 175, [AtLeast 8])] , checkInputOutputsNonRedTemp "tests/HigherOrder/HigherOrder.hs" [ ("f", 200, [Exactly 3]) , ("h", 150, [Exactly 2]) , ("assoc", 200, [Exactly 2]) , ("sf", 200, [Exactly 2]) , ("thirdOrder", 300, [Exactly 2]) , ("thirdOrder2", 300, [Exactly 3]) , ("tupleTestMono", 175, [Exactly 2])] -- , checkInputOutput "tests/TestFiles/BadBool.hs" "BadBool" "f" 1400 [AtLeast 1] -- , checkExprAssumeAssert "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))] -- , checkExprAssumeAssert "tests/TestFiles/HigherOrderList.hs" 400 Nothing Nothing "g" [AtLeast 10] , checkExpr "tests/TestFiles/MkSymbolic.hs" 1500 "f" [ Exactly 9 ] , checkInputOutputs "tests/TestFiles/Show.hs" [ ("show1", 1000, [Exactly 1]) , ("show2", 1000, [Exactly 1]) , ("show3", 1000, [AtLeast 3]) , ("show4", 1000, [Exactly 2]) , ("show5", 1300, [AtLeast 12]) , ("checkWS", 1000, [Exactly 5]) ] ] extensionTests :: TestTree extensionTests = testGroup "Extensions" [ checkInputOutputs "tests/TestFiles/Extensions/PatternSynonyms1.hs" [ ("isNineInt", 400, [AtLeast 2]) , ("isNineInteger", 400, [AtLeast 2]) , ("isNineFloat", 400, [AtLeast 2]) , ("isFunc", 400, [AtLeast 2]) , ("funcArg", 400, [AtLeast 2]) , ("consArrow", 400, [AtLeast 2]) ] , checkInputOutputs "tests/TestFiles/Extensions/ViewPatterns1.hs" [ ("shapeToNumSides", 4000, [Exactly 4]) ] , checkInputOutputs "tests/TestFiles/Extensions/FlexibleContexts1.hs" [ ("callF", 400, [AtLeast 2]) , ("callF2", 400, [AtLeast 2]) , ("callF3", 400, [AtLeast 2]) , ("callG", 400, [AtLeast 1]) , ("callG2", 400, [AtLeast 1]) ] ] baseTests :: TestTree baseTests = testGroup "Base" [ checkInputOutput "tests/Samples/Peano.hs" "add" 400 [AtLeast 4] , checkInputOutputs "tests/BaseTests/ListTests.hs" [ ("test", 1000, [AtLeast 1]) , ("maxMap", 1000, [AtLeast 4]) , ("minTest", 1000, [AtLeast 2]) , ("foldrTest2", 1000, [AtLeast 1]) ] , checkInputOutput "tests/BaseTests/Tuples.hs" "addTupleElems" 1000 [AtLeast 2] , checkInputOutputs "tests/BaseTests/MaybeTest.hs" [ ("headMaybeInt", 1000, [AtLeast 2]) , ("sumN", 1000, [AtLeast 6]) , ("lengthN", 1000, [AtLeast 6]) ] , checkInputOutput "tests/BaseTests/Other.hs" "check4VeryEasy2" 600 [AtLeast 1] ] primTests :: TestTree primTests = testGroup "Prims" [ checkInputOutputs "tests/Prim/Prim2.hs" [ ("quotI1", 1000, [AtLeast 4]) , ("quotI2", 1000, [AtLeast 4]) , ("remI1", 1000, [AtLeast 4]) , ("remI2", 1000, [AtLeast 3]) , ("remI3", 1000, [AtLeast 1]) , ("remI4", 1000, [AtLeast 1]) , ("p1List", 300000, [AtLeast 1]) , ("p2List", 700000, [AtLeast 1]) , ("integerToFloatList", 150000, [AtLeast 1]) ] , checkInputOutputs "tests/Prim/Prim3.hs" [ ("int2FloatTest", 1000, [AtLeast 1]) , ("int2DoubleTest", 1000, [AtLeast 1]) ] , checkInputOutputs "tests/Prim/Prim4.hs" [ ("divIntTest", 1500, [AtLeast 4]) , ("divIntegerTest", 1500, [AtLeast 1]) , ("divIntegerTest2", 1500, [AtLeast 4]) , ("divFloatTest", 1500, [AtLeast 1]) ] , checkInputOutputs "tests/Prim/DataTag.hs" [ ("dataToTag1", 1000, [Exactly 1]) , ("dataToTag2", 1000, [AtLeast 1]) , ("dataToTag3", 1000, [Exactly 5]) , ("tagToEnum1", 1000, [AtLeast 1]) , ("tagToEnum3", 1000, [AtLeast 4]) , ("tagToEnum4", 1000, [AtLeast 4]) , ("tagToEnum5", 1000, [Exactly 1]) , ("tagToEnum6", 1000, [AtLeast 4]) ] , checkExpr "tests/Prim/DataTag.hs" 1000 "tagToEnum2" [Exactly 1, RForAll (\[r] -> isError r)] , checkInputOutputs "tests/Prim/Chr.hs" [ ("lowerLetters", 9000, [AtLeast 1]) , ("allLetters", 20000, [AtLeast 1]) , ("printBasedOnChr", 1500, [AtLeast 7]) , ("printBasedOnOrd", 1500, [AtLeast 7]) ] ] ioTests :: TestTree ioTests = testGroup "IO" [ checkInputOutput "tests/IO/UnsafePerformIO1.hs" "f" 1000 [Exactly 1] ] -- To Do Tests -------------- todoTests :: TestTree todoTests = testGroup "To Do" [ checkExpr "tests/TestFiles/TypeClass/TypeClass5.hs" 800 "run" [AtLeast 1] , checkExpr "tests/TestFiles/TypeClass/TypeClass5.hs" 800 "run2" [AtLeast 0] , checkInputOutput "tests/Prim/Prim2.hs" "sqrtList" 10000 [AtLeast 1] , checkInputOutputs "tests/BaseTests/MaybeTest.hs" [ ("average", 2000, [AtLeast 6]) , ("averageF", 2000, [AtLeast 6]) , ("maybeAvg", 200, [AtLeast 6]) ] , checkInputOutputs "tests/Prim/Prim3.hs" [ ("float2IntTest", 1000, [AtLeast 1]) , ("double2IntTest", 1000, [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 -> String -> [Reqs ([Expr] -> Bool)] -> TestTree checkExpr src stps entry reqList = checkExprReaches src stps Nothing Nothing Nothing entry reqList checkExprAssume :: String -> Int -> Maybe String -> String -> [Reqs ([Expr] -> Bool)] -> TestTree checkExprAssume src stps m_assume entry reqList = checkExprReaches src stps m_assume Nothing Nothing entry reqList checkExprAssert :: String -> Int -> Maybe String -> String -> [Reqs ([Expr] -> Bool)] -> TestTree checkExprAssert src stps m_assert entry reqList = checkExprReaches src stps Nothing m_assert Nothing entry reqList checkExprAssumeAssert :: String -> Int -> Maybe String -> Maybe String -> String -> [Reqs ([Expr] -> Bool)] -> TestTree checkExprAssumeAssert src stps m_assume m_assert entry reqList = checkExprReaches src stps m_assume m_assert Nothing entry reqList checkExprReaches :: String -> Int -> Maybe String -> Maybe String -> Maybe String -> String -> [Reqs ([Expr] -> Bool)] -> TestTree checkExprReaches src stps m_assume m_assert m_reaches entry reqList = do checkExprWithConfig src m_assume m_assert m_reaches entry reqList (do config <- mkConfigTestIO return $ config {steps = stps}) checkExprWithMap :: String -> Int -> Maybe String -> Maybe String -> Maybe String -> String -> [Reqs ([Expr] -> Bool)] -> TestTree checkExprWithMap src stps m_assume m_assert m_reaches entry reqList = do checkExprWithConfig src m_assume m_assert m_reaches entry reqList (do config <- mkConfigTestWithMapIO return $ config {steps = stps}) checkExprWithSet :: String -> Int -> Maybe String -> Maybe String -> Maybe String -> String -> [Reqs ([Expr] -> Bool)] -> TestTree checkExprWithSet src stps m_assume m_assert m_reaches entry reqList = do checkExprWithConfig src m_assume m_assert m_reaches entry reqList (do config <- mkConfigTestWithSetIO return $ config {steps = stps}) checkExprWithConfig :: String -> Maybe String -> Maybe String -> Maybe String -> String -> [Reqs ([Expr] -> Bool)] -> IO Config -> TestTree checkExprWithConfig src m_assume m_assert m_reaches entry reqList config_f = do testCase src (do config <- config_f res <- testFile src m_assume m_assert m_reaches entry config let ch = case res of Left _ -> False Right exprs -> null $ checkExprGen (map (\(inp, out) -> inp ++ [out]) exprs) reqList assertBool ("Assume/Assert for file " ++ src ++ " with functions [" ++ (fromMaybe "" m_assume) ++ "] " ++ "[" ++ (fromMaybe "" m_assert) ++ "] " ++ entry ++ " failed.\n" ++ show res) ch ) -- 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) simplTranslationConfig config let (states, _) = maybe (error "Timeout") fst r return $ map (\(ExecRes { conc_args = i, conc_out = o}) -> (i, o)) states -- For mergeState unit tests checkFn :: Either String Bool -> String -> IO TestTree checkFn f testName = do let res = f case res of Left e -> return . testCase testName $ assertFailure e Right _ -> return . testCase testName $ return () checkFnIO :: IO (Either String Bool) -> String -> IO TestTree checkFnIO f testName = do res <- f case res of Left e -> return . testCase testName $ assertFailure e Right _ -> return . testCase testName $ return () errors :: [Expr] -> Bool errors e = case last e of Prim Error _ -> True _ -> False