g2-0.2.0.0: tests_lh/LHTest.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
module Main where
import Test.Tasty
import Test.Tasty.HUnit
import GetNthTest
import PeanoTest
import LHReqs
import TestUtils
import UnionPoly
import G2.Config as G2
import G2.Interface
import G2.Language
import G2.Liquid.Config
import G2.Liquid.Helpers
import G2.Liquid.Interface
import G2.Liquid.Inference.Interface
import G2.Liquid.Inference.Config
import G2.Liquid.Inference.G2Calls
import G2.Translation
import Control.Exception
import Data.Time.Clock
import Data.Either
import qualified Data.Map.Lazy as M
import qualified Data.Text as T
import System.FilePath
import G2.Liquid.Types
import qualified System.IO as T
import Language.Haskell.Liquid.UX.CmdLine hiding (config)
-- 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
defaultMainWithIngredients
defaultIngredients
tests
tests :: TestTree
tests = testGroup "All Tests"
[ liquidTests
, posInfTests
, negInfTests
, cexInfTests
, unionPolyTests ]
liquidTests :: TestTree
liquidTests = testGroup "Liquid"
[
checkLiquids "tests_lh/Liquid/SimpleMath.hs"
[ ("abs2", 2000, [RForAll (\[x, y] -> isDouble x ((==) 0) && isDouble y ((==) 0)), Exactly 1])
, ("add", 800, [RForAll (\[x, y, z] -> isInt x $ \x' -> isInt y $ \y' -> isInt z $ \z' -> x' > z' || y' > z'), AtLeast 1])
, ("subToPos", 1000, [ RForAll (\[x, y, z] -> isInt x $ \x' -> isInt y $ \y' -> isInt z $ \z' -> x' > 0 && x' >= y' && z' <= 0), AtLeast 1])]
, checkLiquidWithNoCutOff "tests_lh/Liquid/SimpleMath.hs"
[ ("fib", 4000, [RForAll (\[x, y] -> isInt x $ \x' -> isInt y $ \y' -> x' > y'), AtLeast 3])
, ("fib'", 6000, [RForAll (\[x, y] -> isInt x $ \x' -> isInt y $ \y' -> x' > y'), AtLeast 3])
, ("xSqPlusYSq", 1000 , [RForAll (\[x, y, z] -> isInt x $ \x' -> isInt y $ \y' -> isInt z $ \z' -> x' + y' >= z'), AtLeast 1])
]
, checkLiquids "tests_lh/Liquid/SimplePoly.hs"
[ ("snd2Int", 800, [ RForAll (\[x, y, z] -> isInt x $ \x' -> isInt y $ \y' -> isInt z $ \z' -> x' /= y' && y' == z'), Exactly 1])
, ("sumPair", 800, [ AtLeast 1, RForAll (\[App (App _ x) y, z] -> isInt x $ \x' -> isInt y $ \y' -> isInt z $ \z' -> x' > z' || y' > z')])
, ("switchInt", 600, [ Exactly 1, RForAll (\[App (App _ x) _, App (App _ _) y] -> getIntB x $ \ x' -> getIntB y $ \ y' -> x' == y')]) ]
, checkLiquids "tests_lh/Liquid/Peano.hs"
[ ("add", 1400, [RForAll (\[x, y, _] -> x `eqIgT` zeroPeano || y `eqIgT` zeroPeano), AtLeast 5])
, ("fromInt", 600, [RForAll (\[x, y] -> isInt x (\x' -> x' == 0) && y `eqIgT` zeroPeano), AtLeast 1])
]
, checkLiquidWithNoCutOff "tests_lh/Liquid/GetNth.hs"
[ ("getNthInt", 2700, [AtLeast 3, RForAll getNthErrors])
, ("getNth", 2700, [AtLeast 3]) ]
, checkLiquidWithCutOff "tests_lh/Liquid/GetNth.hs" "sumC" 2000000 1000
[AtLeast 3, RForAll (\[_, y] -> isInt y $ (==) 0)]
, checkLiquidWithCutOff "tests_lh/Liquid/GetNth.hs" "sumCList" 2000000 1000 [AtLeast 3]
, checkLiquids "tests_lh/Liquid/DataRefTest.hs"
[ ("addMaybe", 1000, [AtLeast 1, RForAll (\[_, y, z] -> isInt y $ \y' -> appNthArgIs z (\z' -> isInt z' $ \z'' -> z'' <= y') 2)])
, ("addMaybe2", 2000, [ 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)])
, ("getLeftInts", 2000, [AtLeast 1, RForAll (\[x, _] -> dcInAppHasName "Right" x 3)])
, ("sumSameInts", 2000, [AtLeast 1, RForAll (\[x, y, _] -> dcInAppHasName "Right" x 3 && dcInAppHasName "Left" y 3)])
, ("sub1", 1200, [AtLeast 1]) ]
, checkLiquid "tests_lh/Liquid/NumOrd.hs" "subTuple" 1200 [AtLeast 1]
, checkLiquids "tests_lh/Liquid/CommentMeasures.hs"
[ ("d", 1000, [AtLeast 1])
, ("unpackCP'", 100000, [Exactly 0])
, ("unpackBool", 1000, [AtLeast 1, RForAll (\[_, r] -> getBoolB r (== False))])
, ("sumSameOneOfs", 100000, [Exactly 0])
, ("gets2As", 2000, [AtLeast 1, RExists (\[x, y, _] -> buriedDCName "B" x && buriedDCName "B" y)])
, ("gets2As'", 1000, [AtLeast 1, RExists (\[x, y, _] -> buriedDCName "A" x && buriedDCName "B" y)
, RExists (\[x, y, _] -> buriedDCName "B" x && buriedDCName "A" y)])
, ("ge4gt5", 1000, [AtLeast 1, RForAll (\[x, y] -> appNth x 1 $ \x' -> isInt x' $ \x'' -> isInt y $ \y' -> x'' == 4 && y' == 5)])
]
, checkLiquids "tests_lh/Liquid/ConcatList.hs"
[ ("concat2", 800, [AtLeast 2])
, ("concat3", 800, [AtLeast 2])
, ("concat5", 1600, [AtLeast 1])]
, checkLiquid "tests_lh/Liquid/Tests/Group3.lhs" "f" 2200 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Nonused.hs" "g" 2000 [AtLeast 1]
-- , checkLiquid "tests_lh/Liquid/HigherOrderRef.hs" "f1" 2000 [Exactly 0]
-- , checkLiquid "tests_lh/Liquid/HigherOrderRef.hs" "f2" 2000 [AtLeast 4, RForAll (\[_, x, y] -> x == y)]
-- , checkLiquid "tests_lh/Liquid/HigherOrderRef.hs" "f3" 2000 [Exactly 0]
-- , checkLiquid "tests_lh/Liquid/HigherOrderRef.hs" "f4" 2000
-- [AtLeast 4, RForAll (\[_, x, _] -> isInt x $ \x' -> x' == 0)]
-- , checkLiquid "tests_lh/Liquid/HigherOrderRef.hs" "f5" 2000 [Exactly 0]
-- , checkLiquid "tests_lh/Liquid/HigherOrderRef.hs" "f6" 2000 [AtLeast 10]
-- , checkLiquid "tests_lh/Liquid/HigherOrderRef.hs" "f7" 2000
-- [AtLeast 10, RForAll (\[x, _, y] -> isInt x $ \x' -> isInt y $ \y' -> x' == y')]
-- , checkLiquid "tests_lh/Liquid/HigherOrderRef.hs" "f8" 2000 [AtLeast 10]
-- , checkLiquid "tests_lh/Liquid/HigherOrderRef.hs" "callf" 2000 [AtLeast 1]
-- , checkLiquid "tests_lh/Liquid/Error/Error1.hs" "f" 600 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Error/Error2.hs" "f1" 2000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/ZipWith.lhs" "distance" 1000 [AtLeast 3]
, checkLiquids "tests_lh/Liquid/HigherOrder2.hs"
[ ("f", 2000, [Exactly 0])
, ("h", 2000, [AtLeast 1])]
, checkLiquid "tests_lh/Liquid/HigherOrder3.hs" "m" 600 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Ordering.hs" "oneOrOther" 1000 [Exactly 0]
, checkLiquid "tests_lh/Liquid/AddKV.lhs" "empty" 1000 [Exactly 0]
, checkLiquid "tests_lh/Liquid/PropSize.hs" "prop_size" 2000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/PropSize2.hs" "prop_size" 2000 [AtLeast 1]
, checkLiquids "tests_lh/Liquid/WhereFuncs.lhs" [ ("f", 1000, [Exactly 0])
, ("g", 1000, [Exactly 0])]
, checkLiquid "tests_lh/Liquid/PropConcat.lhs" "prop_concat" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Distance.lhs" "distance" 1000 [AtLeast 1]
-- The below test generates a LiquidHaskell error with newer LiquidHaskell versions
-- , checkLiquid "tests_lh/Liquid/MultModules/CallZ.lhs" "callZ" 1000 [AtLeast 1]
, checkAbsLiquid "tests_lh/Liquid/AddToEven.hs" "f" 2500
[ 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')))]
, checkAbsLiquid "tests_lh/Liquid/AddToEven4.hs" "f" 2000 [ AtLeast 1]
, checkAbsLiquid "tests_lh/Liquid/Concat.hs" "prop_concat" 1000 [ AtLeast 1]
, checkLiquids "tests_lh/Liquid/ListTests.lhs"
[ ("r", 1000, [Exactly 0])
, ("prop_map", 1500, [AtLeast 3])
, ("prop_concat_1", 1500, [AtLeast 1])
]
, checkAbsLiquid "tests_lh/Liquid/ListTests2.lhs" "prop_map" 2000
[ AtLeast 2
, RForAll (\_ _ [(FuncCall { funcName = Name n _ _ _ }) ] -> n == "map") ]
, checkAbsLiquid "tests_lh/Liquid/ListTests2.lhs" "prop_size" 2000
[ AtLeast 1
, RForAll (\[] _ [(FuncCall { funcName = Name n _ _ _, returns = r }) ]
-> n == "length2" && getIntB r (/= 3)) ]
, checkLiquid "tests_lh/Liquid/MapReduceTest2.lhs" "mapReduce" 1500 [AtLeast 1]
-- The below test generates a LiquidHaskell error with LiquidHaskell 8.2.2 version
-- , checkLiquid "tests_lh/Liquid/MeasErr.hs" "f" 1500 [Exactly 0]
, checkAbsLiquid "tests_lh/Liquid/PropRep.hs" "prop_rep" 2000
[ AtLeast 1 ]
, checkAbsLiquid "tests_lh/Liquid/Replicate.hs" "replicate" 2000
[ AtLeast 1
, RExists (\_ _ [(FuncCall { funcName = Name n _ _ _ }) ] -> n == "foldl") ]
, checkAbsLiquid "tests_lh/Liquid/Replicate.hs" "r" 2000
[ AtLeast 1
, RExists (\_ _ [(FuncCall { funcName = Name n _ _ _ }) ] -> n == "foldl") ]
, checkAbsLiquid "tests_lh/Liquid/AbsTypeClass.hs" "callF" 1000
[ AtLeast 1
, RExists (\_ _ [(FuncCall { funcName = Name n _ _ _ }) ] -> n == "f") ]
, checkAbsLiquid "tests_lh/Liquid/AbsTypeClassVerified.hs" "callF" 10000 [ Exactly 0 ]
, checkLiquid "tests_lh/Liquid/Tree.hs" "sumPosTree" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Error4.hs" "extractRights" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/PostFalse.hs" "f" 2000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/TypeSym.hs" "f" 500 []
, checkLiquid "tests_lh/Liquid/CorrectDict.hs" "f" 2000 [AtLeast 1]
, checkAbsLiquid "tests_lh/Liquid/ZipWith3.hs" "prop_zipWith" 400 [ AtLeast 3]
, checkAbsLiquid "tests_lh/Liquid/Length.hs" "prop_size" 1000
[ AtLeast 1
, RForAll (\_ _ [ _ ] -> True)]
, checkLiquidWithConfig "tests_lh/Liquid/NestedLength.hs" [("nested", 1000, [AtLeast 1])]
mkConfigTestIO
(return $ (mkLHConfigDirect [] M.empty) { add_tyvars = True })
, checkLiquidWithConfig "tests_lh/Liquid/AddTyVars.hs"
[ ("f", 400, [AtLeast 1])
, ("g", 400, [AtLeast 1])
, ("h", 400, [AtLeast 1])]
mkConfigTestIO
(return $ (mkLHConfigDirect [] M.empty) { add_tyvars = True })
, checkLiquid "tests_lh/Liquid/Polymorphism/Poly1.hs" "f" 1000 [Exactly 0]
, checkLiquid "tests_lh/Liquid/Polymorphism/Poly2.hs" "f" 600 [Exactly 0]
, checkLiquid "tests_lh/Liquid/Sets/Sets1.hs" "prop_union_assoc" 2000 [AtLeast 2]
, checkLiquid "tests_lh/Liquid/Sets/Sets1.hs" "prop_intersection_comm" 1000 [AtLeast 5]
, checkLiquid "tests_lh/Liquid/Sets/Sets2.hs" "badIdList" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Sets/Sets2.hs" "append" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Sets/Sets3.hs" "filter" 1800 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Sets/Sets4.hs" "isin" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Sets/Sets5.hs" "f" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Sets/Sets6.hs" "f" 2000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Sets/Sets7.hs" "insertSort" 3000 [AtLeast 1]
-- Higher Order Functions
, checkLiquid "tests_lh/Liquid/HigherOrder/IntFuncArg.hs" "caller" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/HigherOrder/HigherOrderPre.hs" "test" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/HigherOrder/HigherOrder2.hs" "f" 2000 [Exactly 0]
-- IO
, checkLiquid "tests_lh/Liquid/IO/IO1.hs" "f" 1000 [Exactly 0]
, checkLiquid "tests_lh/Liquid/IO/IO2.hs" "f" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/IO/IO3.hs" "f" 1400 [AtLeast 1]
-- Abstract counterexamples
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly3.hs" "f" 800
[ AtLeast 4
, RForAll (\_ _ [ FuncCall { funcName = Name n _ _ _} ] -> n == "fil")]
, checkLiquid "tests_lh/Liquid/Polymorphism/Poly4.hs" "f" 600 [Exactly 0]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly5.hs" "call" 600 [AtLeast 1]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly6.hs" "f" 1000
[ AtLeast 1
, RForAll (\_ _ [ FuncCall { returns = r } ] ->
case r of { Prim Undefined _-> False; _ -> True})
]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly7.hs" "prop_f" 2000 [AtLeast 1]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly8.hs" "prop" 2000
[ AtLeast 1
, RForAll (\_ _ [ FuncCall { funcName = Name n _ _ _ } ] -> n == "func")]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly9.hs" "prop" 2000
[ AtLeast 1
, RForAll (\_ _ [ FuncCall { funcName = Name n _ _ _ } ] -> n == "func")]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly10.hs" "prop" 2000
[ AtLeast 1 ]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly11.hs" "call" 700
[ AtLeast 1
, RForAll (\_ _ [ FuncCall { funcName = Name n _ _ _ } ] -> n == "higher")]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly12.hs" "prop" 3000
[ AtLeast 1
, RForAll (\_ _ [ FuncCall { funcName = Name n _ _ _ } ] -> n == "map")]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly13.hs" "call" 1000
[ AtLeast 1
, RForAll (\_ _ [ FuncCall { funcName = Name n _ _ _ } ] -> n == "f")]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly14.hs" "initCall" 1000 [ AtLeast 1]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly15.hs" "call" 1000 [ AtLeast 1]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly16.hs" "call" 1000
[ AtLeast 1
, RForAll (\ _ _ [ FuncCall { arguments = [_, _, ar] } ] -> case ar of Prim _ _ -> False; _ -> True )]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly17.hs" "empty2" 1000 [ AtLeast 1]
, checkAbsLiquid "tests_lh/Liquid/Polymorphism/Poly18.hs" "f" 500 [ AtLeast 1]
]
posInfTests :: TestTree
posInfTests = testGroup "Tests"
[ posTestInference "tests_lh/test_files/Pos/HigherOrder.hs"
, posTestInference "tests_lh/test_files/Pos/HigherOrder2.hs"
-- , posTestInferenceWithTimeOut 240 5 "tests_lh/test_files/Pos/HigherOrder3.hs"
-- , posTestInference "tests_lh/test_files/Pos/HigherOrder4.hs"
, posTestInference "tests_lh/test_files/Pos/Test1.hs"
, posTestInference "tests_lh/test_files/Pos/Test2.hs"
, posTestInference "tests_lh/test_files/Pos/Test3.hs"
, posTestInference "tests_lh/test_files/Pos/Test4.hs"
, posTestInference "tests_lh/test_files/Pos/Test5.hs"
, posTestInference "tests_lh/test_files/Pos/Test6.hs"
, posTestInference "tests_lh/test_files/Pos/Test7.hs"
, posTestInference "tests_lh/test_files/Pos/Test8.hs"
, posTestInference "tests_lh/test_files/Pos/Test9.hs"
, posTestInference "tests_lh/test_files/Pos/Test10.hs"
, posTestInference "tests_lh/test_files/Pos/Test11.hs"
, posTestInference "tests_lh/test_files/Pos/Test12.hs"
, posTestInference "tests_lh/test_files/Pos/Test13.hs"
, posTestInference "tests_lh/test_files/Pos/Test14.hs"
, posTestInference "tests_lh/test_files/Pos/Test15.hs"
, posTestInference "tests_lh/test_files/Pos/Test16.hs"
, posTestInference "tests_lh/test_files/Pos/Test17.hs"
, posTestInference "tests_lh/test_files/Pos/Test18.hs"
, posTestInference "tests_lh/test_files/Pos/Test19.hs"
, posTestInference "tests_lh/test_files/Pos/Test20.hs"
, posTestInference "tests_lh/test_files/Pos/Test21.hs"
, posTestInference "tests_lh/test_files/Pos/Test22.hs"
-- , posTestInference "tests_lh/test_files/Pos/Test23.hs"
, posTestInference "tests_lh/test_files/Pos/Test24.hs"
, posTestInference "tests_lh/test_files/Pos/Test25.hs"
, posTestInference "tests_lh/test_files/Pos/Test26.hs"
, posTestInference "tests_lh/test_files/Pos/Test27.hs"
, posTestInference "tests_lh/test_files/Pos/Test28.hs"
, posTestInference "tests_lh/test_files/Pos/Test29.hs"
, posTestInference "tests_lh/test_files/Pos/Test30.hs"
, posTestInference "tests_lh/test_files/Pos/Test31.hs"
, posTestInference "tests_lh/test_files/Pos/Test32.hs"
, posTestInference "tests_lh/test_files/Pos/Test33.hs"
, posTestInference "tests_lh/test_files/Pos/Test34.hs"
, posTestInference "tests_lh/test_files/Pos/Test35.hs"
, posTestInference "tests_lh/test_files/Pos/Test36.hs"
, posTestInference "tests_lh/test_files/Pos/Test37.hs"
-- , posTestInferenceWithTimeOut 240 15 "tests_lh/test_files/Pos/Test38.hs"
, posTestInference "tests_lh/test_files/Pos/Test39.hs"
, posTestInference "tests_lh/test_files/Pos/Test40.hs"
, posTestInference "tests_lh/test_files/Pos/Test41.hs"
, posTestInference "tests_lh/test_files/Pos/Test42.hs"
, posTestInference "tests_lh/test_files/Pos/Test43.hs"
, posTestInference "tests_lh/test_files/Pos/Test44.hs"
, posTestInference "tests_lh/test_files/Pos/Test45.hs"
, posTestInference "tests_lh/test_files/Pos/Test46.hs"
, posTestInference "tests_lh/test_files/Pos/Test47.hs"
, posTestInference "tests_lh/test_files/Pos/Test48.hs"
, posTestInference "tests_lh/test_files/Pos/Test49.hs"
, posTestInference "tests_lh/test_files/Pos/Test50.hs"
, posTestInference "tests_lh/test_files/Pos/Sets1.hs"
, posTestInference "tests_lh/test_files/Pos/Sets2.hs"
, posTestInference "tests_lh/test_files/Pos/Sets3.hs"
, posTestInference "tests_lh/test_files/Pos/Sets4.hs"
, posTestInference "tests_lh/test_files/Pos/Sets5.hs"
, posTestInference "tests_lh/test_files/Pos/Sets6.hs"
, posTestInference "tests_lh/test_files/Pos/Sets7.hs"
, posTestInference "tests_lh/test_files/Pos/Sets8.hs"
, posTestInference "tests_lh/test_files/Pos/Sets9.hs"
-- , posTestInference "tests_lh/test_files/Pos/Sets10.hs"
, posTestInference "tests_lh/test_files/Pos/MeasComp1.hs"
, posTestInference "tests_lh/test_files/Pos/MeasComp2.hs"
, posTestInference "tests_lh/test_files/Pos/MeasComp3.hs" ]
negInfTests :: TestTree
negInfTests = testGroup "Tests"
[ negTestInference "tests_lh/test_files/Neg/Test1.hs"
, negTestInference "tests_lh/test_files/Neg/Test2.hs"
, negTestInference "tests_lh/test_files/Neg/Test3.hs"
, negTestInference "tests_lh/test_files/Neg/Test4.hs"
, negTestInference "tests_lh/test_files/Neg/Test5.hs"
, negTestInference "tests_lh/test_files/Neg/Test6.hs" ]
cexInfTests :: TestTree
cexInfTests = testGroup "Tests"
[ cexTest "tests_lh/test_files/CEx/CEx1.hs" "zipWith"
, cexTest "tests_lh/test_files/CEx/CEx2.hs" "mapReduce"
, cexTest "tests_lh/test_files/CEx/CEx3.hs" "kmeans1" ]
todoTests :: TestTree
todoTests = testGroup "To Do"
[
checkLiquid "tests_lh/Liquid/TyApps.hs" "goodGet" 1000 [Exactly 0]
, checkLiquid "tests_lh/Liquid/TyApps.hs" "getPosInt" 1000
[ AtLeast 1
, RForAll (\[_, _, (App _ x), y] -> getIntB x $ \x' -> getIntB y $ \y' -> x' == y' && y' == 10)]
, checkLiquid "tests_lh/Liquid/TyApps.hs" "getPos" 1000
[ AtLeast 1
, RExists (\[_, _, (App _ x), y] -> getIntB x $ \x' -> getIntB y $ \y' -> x' == y' && y' == 10)]
, checkLiquid "tests_lh/Liquid/FoldrTests.hs" "max2" 1000 [Exactly 0]
, checkLiquid "tests_lh/Liquid/FoldrTests.hs" "max3" 1000 [Exactly 0]
, checkLiquid "tests_lh/Liquid/SimpleAnnot.hs" "simpleF" 1000 [Exactly 0]
, checkLiquid "tests_lh/Liquid/Ordering.hs" "lt" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/Ordering.hs" "gt" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/WhereFuncs2.hs" "hCalls" 1000 [AtLeast 1]
, checkLiquid "tests_lh/Liquid/WhereFuncs2.hs" "i" 1000 [AtLeast 1]
, checkAbsLiquid "tests_lh/Liquid/AddToEvenWhere.hs" "f" 2000
[ AtLeast 1
, RForAll (\[i] r [(FuncCall { funcName = Name n _ _ _, returns = r' }) ]
-> n == "g" && isInt i (\i' -> i' `mod` 2 == 0) && r == r' )]
, checkLiquid "tests_lh/Liquid/ListTests.lhs" "concat" 1000 [AtLeast 3]
, checkLiquid "tests_lh/Liquid/MapReduceTest.lhs" "mapReduce" 1500
[Exactly 0]
, checkLiquid "tests_lh/Liquid/NearestTest.lhs" "nearest" 1500 [Exactly 1]
, checkAbsLiquid "tests_lh/Liquid/ListTests2.lhs" "replicate" 2000
[ AtLeast 3
, RForAll (\[_, nA, aA] _ [(FuncCall { funcName = Name n _ _ _, arguments = [_, _, nA', aA'] }) ]
-> n == "replicate" && nA == nA' && aA == aA') ]
]
-------------------------------------------------
-- CEx Gen tests
-------------------------------------------------
checkLiquidWithNoCutOff :: FilePath -> [(String, Int, [Reqs ([Expr] -> Bool)])] -> TestTree
checkLiquidWithNoCutOff fp tests = do
let lhconfig = mkLHConfigDirect [] M.empty
checkLiquidWithConfig fp tests
mkConfigTestIO
(return lhconfig { cut_off = maximum $ map (\(_, stps, _) -> stps) tests })
checkLiquid :: FilePath -> String -> Int -> [Reqs ([Expr] -> Bool)] -> TestTree
checkLiquid fp entry stps req = do
let lhconfig = mkLHConfigDirect [] M.empty
checkLiquidWithConfig fp [(entry, stps, req)]
mkConfigTestIO
(return lhconfig)
checkLiquids :: FilePath -> [(String, Int, [Reqs ([Expr] -> Bool)])] -> TestTree
checkLiquids fp tests = do
let lhconfig = mkLHConfigDirect [] M.empty
checkLiquidWithConfig fp tests
mkConfigTestIO
(return lhconfig)
checkLiquidWithSet :: FilePath -> [(String, Int, [Reqs ([Expr] -> Bool)])] -> TestTree
checkLiquidWithSet fp tests = do
let lhconfig = mkLHConfigDirect [] M.empty
checkLiquidWithConfig fp tests
mkConfigTestWithSetIO
(return lhconfig)
checkLiquidWithCutOff :: FilePath -> String -> Int -> Int -> [Reqs ([Expr] -> Bool)] -> TestTree
checkLiquidWithCutOff fp entry stps co reqList = do
let lhconfig = mkLHConfigDirect [] M.empty
checkLiquidWithConfig fp [(entry, stps, reqList)]
mkConfigTestIO
(return lhconfig { cut_off = co })
checkLiquidWithMap :: FilePath -> [(String, Int, [Reqs ([Expr] -> Bool)])] -> TestTree
checkLiquidWithMap fp tests = do
let lhconfig = mkLHConfigDirect [] M.empty
checkLiquidWithConfig fp tests
mkConfigTestWithMapIO
(return lhconfig)
checkLiquidWithConfig :: FilePath -> [(String, Int, [Reqs ([Expr] -> Bool)])] -> IO Config -> IO LHConfig -> TestTree
checkLiquidWithConfig fp tests config_f lhconfig_f =
withResource
(do
config <- config_f
g2_lh_config <- lhconfig_f
lh_config <- getOpts []
let config' = config { mode = Liquid }
let proj = takeDirectory fp
ghci <- try $ getGHCInfos lh_config [proj] [fp] :: IO (Either SomeException [GhcInfo])
let ghci' = case ghci of
Right g_c -> g_c
Left e -> error $ "ERROR OCCURRED IN LIQUIDHASKELL\n" ++ show e
tgt_trans <- translateLoaded [proj] [fp] (simplTranslationConfig { simpl = False }) config'
return (tgt_trans, ghci', config', g2_lh_config)
)
(\_ -> return ())
$ \loaded ->
testGroup
fp
$ map (\(entry, stps, reqList) ->
testCase (fp ++ " " ++ entry) (do
(tgt_trans, ghci, config, lh_config) <- loaded
let config' = config { steps = stps }
res <- doTimeout (timeLimit config)
$ (try (return . fst. fst =<< runLHCore (T.pack entry) tgt_trans ghci config' lh_config)
:: IO (Either SomeException [ExecRes AbstractedInfo]))
let (ch, r) = case res of
Nothing -> (False, Right [Time])
Just (Left e) -> (False, Left e)
Just (Right exprs) ->
let
r_ = checkExprGen
(map (\(ExecRes { conc_args = inp, conc_out = out}) -> inp ++ [out]) exprs)
reqList
in
(null r_, Right r_)
assertBool ("Liquid test for file " ++ fp ++
" with function " ++ entry ++ " failed.\n" ++ show r) ch
)
) tests
checkAbsLiquid :: FilePath -> String -> Int -> [Reqs ([Expr] -> Expr -> [FuncCall] -> Bool)] -> TestTree
checkAbsLiquid fp entry stps reqList = do
let lhconfig = mkLHConfigDirect [] M.empty
checkAbsLiquidWithConfig fp entry reqList
(do config <- mkConfigTestIO
return $ config {steps = stps} )
(return lhconfig)
checkAbsLiquidWithConfig :: FilePath
-> String
-> [Reqs ([Expr]
-> Expr
-> [FuncCall]
-> Bool)]
-> IO Config
-> IO LHConfig
-> TestTree
checkAbsLiquidWithConfig fp entry reqList config_f lhconfig_f = do
testCase fp (do
config <- config_f
lhconfig <- lhconfig_f
res <- findCounterExamples' fp (T.pack entry) config lhconfig
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
) reqList
in
(null te, Right te)
assertBool ("Liquid test for file " ++ fp ++
" with function " ++ entry ++ " failed.\n" ++ show r) ch
)
findCounterExamples' :: FilePath
-> T.Text
-> Config
-> LHConfig
-> IO (Maybe (Either SomeException [ExecRes AbstractedInfo]))
findCounterExamples' fp entry config lhconfig =
let
proj = takeDirectory fp
in
doTimeout (timeLimit config)
$ try (return . fst. fst =<< findCounterExamples [proj] [fp] entry config lhconfig)
-------------------------------------------------
-- Inference tests
-------------------------------------------------
posTestInferenceWithTimeOut :: Int -> NominalDiffTime -> FilePath -> TestTree
posTestInferenceWithTimeOut to to_se fp = do
testCase ("Inference " ++ fp) (do
config <- G2.getConfigDirect
let infconfig = (mkInferenceConfigDirect []) { timeout_se = to_se }
let lhconfig = mkLHConfigDirect [] M.empty
res <- doTimeout to $ inferenceCheck infconfig config lhconfig [] [fp]
assertBool ("Inference for " ++ fp ++ " failed.") $ maybe False (isRight . snd) res
)
posTestInference :: FilePath -> TestTree
posTestInference = posTestInferenceWithTimeOut 120 5
negTestInference :: FilePath -> TestTree
negTestInference fp = do
testCase ("Inference " ++ fp) (do
config <- G2.getConfigDirect
let infconfig = mkInferenceConfigDirect []
let lhconfig = mkLHConfigDirect [] M.empty
res <- doTimeout 90 $ inferenceCheck infconfig config lhconfig [] [fp]
assertBool ("Inference for " ++ fp ++ " failed.") $ maybe False (isLeft . snd) res
)
cexTest :: FilePath -> String -> TestTree
cexTest fp func =
testCase ("Inference " ++ fp) (do
config <- G2.getConfigDirect
let infconfig = (mkInferenceConfigDirect []) { timeout_se = 10 }
let lhconfig = mkLHConfigDirect [] M.empty
res <- doTimeout 25 $ runLHInferenceAll infconfig config lhconfig (T.pack func) [] [fp]
assertBool ("Counterexample generation for " ++ func ++ " in " ++ fp ++ " failed.") $ maybe False (not . null . fst) res
)