{-# 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 "cvc5-spec" <$> dirTests cvc5Cmd "tests/cvc5" 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 '-'