{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Main where
import qualified Control.Concurrent.STM as STM
import qualified Data.Functor.Compose as Functor
import qualified Data.IntMap as IntMap
import Control.Monad (when)
import qualified Control.Monad.State as State
import Control.Monad.Trans.Class (lift)
import Data.List (isSuffixOf)
import Prelude hiding (log)
import Data.Maybe (fromMaybe)
import Data.Monoid (Sum(..))
import Data.Proxy
import Data.Tagged
import Control.Applicative
import Options.Applicative
import System.Directory
import System.Exit
import System.FilePath
import System.IO
import System.IO.Error
import System.Process
import Text.Printf
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.Ingredients.Rerun
import Test.Tasty.Options
import Test.Tasty.Runners
import Test.Tasty.Runners.AntXML
main :: IO ()
main = do
lfDir <- findLiquidFixpointDir
run lfDir =<< group "Tests" [unitTests lfDir]
where
run lfDir = defaultMainWithIngredients
[ testRunner lfDir
, includingOptions [ Option (Proxy :: Proxy FixpointOpts) ]
]
-- | Searches for the directory of liquid-fixpoint.cabal and changes to it
findLiquidFixpointDir :: IO FilePath
findLiquidFixpointDir = do
dir0 <- getCurrentDirectory
let candidates = [dir0, dir0 </> "liquid-fixpoint"]
findCabalDir :: [FilePath] -> IO (Maybe FilePath)
findCabalDir [] = return Nothing
findCabalDir (d:xs) = do
let cabalFile = d </> "liquid-fixpoint.cabal"
exists <- doesFileExist cabalFile
if exists then
return (Just d)
else
findCabalDir xs
mDir <- findCabalDir candidates
case mDir of
Just d -> return d
Nothing -> error "Could not find liquid-fixpoint.cabal"
testRunner :: FilePath -> Ingredient
testRunner lfDir = rerunningTests
[ listingTests
, combineReporters (myConsoleReporter lfDir) antXMLRunner
, myConsoleReporter lfDir
]
myConsoleReporter :: FilePath -> Ingredient
myConsoleReporter lfDir = combineReporters consoleTestReporter (loggingTestReporter lfDir)
-- | Combine two @TestReporter@s into one.
--
-- Runs the reporters in sequence, so it's best to start with the one
-- that will produce incremental output, e.g. 'consoleTestReporter'.
combineReporters :: Ingredient -> Ingredient -> Ingredient
combineReporters (TestReporter opts1 run1) (TestReporter opts2 run2)
= TestReporter (opts1 ++ opts2) $ \opts tree -> do
f1 <- run1 opts tree
f2 <- run2 opts tree
return $ \smap -> f1 smap >> f2 smap
combineReporters _ _ = error "combineReporters needs TestReporters"
unitTests :: FilePath -> IO TestTree
unitTests lfDir
= group "Unit" [
testGroup "native-pos" <$> dirTests nativeCmd "tests/pos" skipNativePos ExitSuccess
, testGroup "native-neg" <$> dirTests nativeCmd "tests/neg" ["float.fq"] (ExitFailure 1)
, testGroup "elim-crash" <$> dirTests nativeCmd "tests/crash" [] (ExitFailure 1)
, testGroup "elim-pos1" <$> dirTests elimCmd "tests/pos" [] ExitSuccess
, testGroup "elim-pos2" <$> dirTests elimCmd "tests/elim" [] ExitSuccess
, testGroup "elim-neg" <$> dirTests elimCmd "tests/neg" ["float.fq"] (ExitFailure 1)
, testGroup "elim-crash" <$> dirTests elimCmd "tests/crash" [] (ExitFailure 1)
, testGroup "cvc5-pos" <$> dirTests cvc5Cmd "tests/pos" skipNativePos ExitSuccess
, testGroup "proof" <$> dirTests elimCmd "tests/proof" [] ExitSuccess
, testGroup "rankN" <$> dirTests elimCmd "tests/rankNTypes" [] ExitSuccess
, testGroup "horn-pos-el" <$> dirTests elimSaveCmd "tests/horn/pos" [] ExitSuccess
, testGroup "horn-pos-cvc5" <$> dirTests cvc5Cmd "tests/horn/pos" [] ExitSuccess
, testGroup "horn-neg-el" <$> dirTests elimSaveCmd "tests/horn/neg" [] (ExitFailure 1)
, testGroup "horn-neg-cvc5" <$> dirTests cvc5Cmd "tests/horn/neg" [] (ExitFailure 1)
, testGroup "horn-json-pos-el" <$> dirJsonTests elimCmd "tests/horn/pos/.liquid" [] ExitSuccess
, testGroup "horn-json-neg-el" <$> dirJsonTests elimCmd "tests/horn/neg/.liquid" [] (ExitFailure 1)
, testGroup "horn-smt2-pos-el" <$> dirHornTests elimCmd "tests/horn/pos/.liquid" [] ExitSuccess
, testGroup "horn-smt2-neg-el" <$> dirHornTests elimCmd "tests/horn/neg/.liquid" [] (ExitFailure 1)
, testGroup "horn-pos-na" <$> dirTests nativeCmd "tests/horn/pos" [] ExitSuccess
, testGroup "horn-neg-na" <$> dirTests nativeCmd "tests/horn/neg" [] (ExitFailure 1)
]
where
dirTests = dirTests' isTest
dirJsonTests = dirTests' ("horn.json" `isSuffixOf`)
dirHornTests = dirTests' ("horn.smt2" `isSuffixOf`)
dirTests' :: (FilePath -> Bool) -> TestCmd -> FilePath -> [FilePath] -> ExitCode -> IO [TestTree]
dirTests' isT testCmd root ignored code = do
let absRoot = lfDir </> root
files <- walkDirectory absRoot
let tests = [ rel | f <- files, isT f, let rel = makeRelative absRoot f, rel `notElem` ignored ]
return $ mkTest testCmd code absRoot <$> tests
isTest :: FilePath -> Bool
isTest f = takeExtension f `elem` [".fq", ".smt2"]
skipNativePos :: [FilePath]
skipNativePos = ["NonLinear-pack.fq"]
newtype FixpointOpts = LO String deriving (Show, Read, Eq, Ord)
instance Semigroup FixpointOpts where
(LO "") <> y = y
x <> (LO "") = x
(LO x) <> (LO y) = LO $ x ++ (' ' : y)
instance Monoid FixpointOpts where
mempty = LO ""
mappend = (<>)
instance IsOption FixpointOpts where
defaultValue = LO ""
parseValue = Just . LO
optionName = return "fixpoint-opts"
optionHelp = return "Extra options to pass to fixpoint"
optionCLParser =
option (fmap LO str)
( long (untag (optionName :: Tagged FixpointOpts String))
<> help (untag (optionHelp :: Tagged FixpointOpts String))
)
---------------------------------------------------------------------------
mkTest :: TestCmd -> ExitCode -> FilePath -> FilePath -> TestTree
---------------------------------------------------------------------------
mkTest testCmd code dir file
=
askOption $ \opts ->
testCase file $
if test `elem` knownToFail
then do
printf "%s is known to fail: SKIPPING" test
assertEqual "" True True
else do
createDirectoryIfMissing True $ takeDirectory log
c <- withFile log WriteMode $ \h -> do
let cmd = testCmd opts "fixpoint" dir file
(_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}
waitForProcess ph
when (code /= c) $
readFile log >>= putStrLn
assertEqual "Wrong exit code" code c
where
test = dir </> file
log = let (d,f) = splitFileName file in dir </> d </> ".liquid" </> f <.> "log"
knownToFail :: [a]
knownToFail = []
---------------------------------------------------------------------------
type TestCmd = FixpointOpts -> FilePath -> FilePath -> FilePath -> String
nativeCmd :: TestCmd
nativeCmd (LO opts) bin dir file =
printf "cd %s && %s %s %s" dir bin opts file
elimCmd :: TestCmd
elimCmd (LO opts) bin dir file =
printf "cd %s && %s --eliminate=some %s %s" dir bin opts file
elimSaveCmd :: TestCmd
elimSaveCmd (LO opts) bin dir file =
printf "cd %s && %s --save --eliminate=some %s %s" dir bin opts file
cvc5Cmd :: TestCmd
cvc5Cmd (LO opts) bin dir file =
printf "cd %s && %s --solver=cvc5 %s %s" dir bin opts file
cvc5SaveCmd :: TestCmd
cvc5SaveCmd (LO opts) bin dir file =
printf "cd %s && %s --save --solver=cvc5 %s %s" dir bin opts file
----------------------------------------------------------------------------------------
-- Generic Helpers
----------------------------------------------------------------------------------------
group :: Monad f => TestName -> [f TestTree] -> f TestTree
group n xs = testGroup n <$> sequence xs
----------------------------------------------------------------------------------------
walkDirectory :: FilePath -> IO [FilePath]
----------------------------------------------------------------------------------------
walkDirectory root
= do (ds,fs) <- partitionM doesDirectoryExist . candidates =<< (getDirectoryContents root `catchIOError` const (return []))
(fs++) <$> concatMapM walkDirectory ds
where
candidates fs = [root </> f | f@(c:_) <- fs, not (isExtSeparator c)]
partitionM :: Monad m => (a -> m Bool) -> [a] -> m ([a],[a])
partitionM f = go [] []
where
go ls rs [] = return (ls,rs)
go ls rs (x:xs) = do b <- f x
if b then go (x:ls) rs xs
else go ls (x:rs) xs
-- isDirectory :: FilePath -> IO Bool
-- isDirectory = fmap Posix.isDirectory . Posix.getFileStatus
concatMapM :: Applicative m => (a -> m [b]) -> [a] -> m [b]
concatMapM _ [] = pure []
concatMapM f (x:xs) = (++) <$> f x <*> concatMapM f xs
-- this is largely based on ocharles' test runner at
-- https://github.com/ocharles/tasty-ant-xml/blob/master/Test/Tasty/Runners/AntXML.hs#L65
loggingTestReporter :: FilePath -> Ingredient
loggingTestReporter lfDir = TestReporter [] $ \opts tree -> Just $ \smap -> do
let
runTest _ testName _ = Traversal $ Functor.Compose $ do
i <- State.get
summary <- lift $ STM.atomically $ do
status <- STM.readTVar $
fromMaybe (error "Attempted to lookup test by index outside bounds") $
IntMap.lookup i smap
let mkSuccess time = [(testName, time, True)]
mkFailure time = [(testName, time, False)]
case status of
-- If the test is done, generate a summary for it
Done result
| resultSuccessful result
-> pure (mkSuccess (resultTime result))
| otherwise
-> pure (mkFailure (resultTime result))
-- Otherwise the test has either not been started or is currently
-- executing
_ -> STM.retry
Const summary <$ State.modify (+ 1)
runGroup _ group' children = Traversal $ Functor.Compose $ do
Const soFar <- Functor.getCompose $ getTraversal $ mconcat children
pure $ Const $ map (\(n,t,s) -> (group' </> n,t,s)) soFar
computeFailures :: StatusMap -> IO Int
computeFailures = fmap getSum . getApp . foldMap (\var -> Ap $
(\r -> Sum $ if resultSuccessful r then 0 else 1) <$> getResultFromTVar var)
getResultFromTVar :: STM.TVar Status -> IO Result
getResultFromTVar var =
STM.atomically $ do
status <- STM.readTVar var
case status of
Done r -> return r
_ -> STM.retry
(Const summary, _tests) <-
flip State.runStateT 0 $ Functor.getCompose $ getTraversal $
foldTestTree
trivialFold { foldSingle = runTest, foldGroup = runGroup }
opts
tree
return $ \_elapsedTime -> do
-- don't use the `time` package, major api differences between ghc 708 and 710
-- build header
ref <- gitRef
timestamp <- gitTimestamp
epochTime <- gitEpochTimestamp
hash <- gitHash
let hdr = unlines [ref ++ " : " ++ hash,
"Timestamp: " ++ timestamp,
"Epoch Timestamp: " ++ epochTime,
headerDelim,
"test, time(s), result"]
let smry = lfDir </> "tests" </> "logs" </> "cur" </> "summary.csv"
writeFile smry $ unlines
$ hdr
: map (\(n, t, r) -> printf "%s, %0.4f, %s" n t (show r)) summary
(==0) <$> computeFailures smap
gitTimestamp :: IO String
gitTimestamp = do
res <- gitProcess ["show", "--format=\"%ci\"", "--quiet"]
return $ filter notNoise res
gitEpochTimestamp :: IO String
gitEpochTimestamp = do
res <- gitProcess ["show", "--format=\"%ct\"", "--quiet"]
return $ filter notNoise res
gitHash :: IO String
gitHash = do
res <- gitProcess ["show", "--format=\"%H\"", "--quiet"]
return $ filter notNoise res
gitRef :: IO String
gitRef = do
res <- gitProcess ["show", "--format=\"%d\"", "--quiet"]
return $ filter notNoise res
-- | Calls `git` for info; returns `"plain"` if we are not in a git directory.
gitProcess :: [String] -> IO String
gitProcess args = readProcess "git" args [] `catchIOError` const (return "plain")
notNoise :: Char -> Bool
notNoise a = a /= '\"' && a /= '\n' && a /= '\r'
headerDelim :: String
headerDelim = replicate 80 '-'