----------------------------------------------------------------------------- -- | -- Module : Utils.SBVTestFramework -- Copyright : (c) Jeffrey Young -- Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- Various goodies for benchmarking SBV ----------------------------------------------------------------------------- {-# LANGUAGE OverloadedStrings #-} module Utils.SBVBenchFramework ( mkExecString , mkFileName , module Data.SBV , timeStamp , getDate , dateStamp , benchResultsFile , classifier , overheadClassifier , filterOverhead ) where import qualified Data.List as L import System.Process (showCommandForUser) import System.Random import Data.Char (isSpace) import System.FilePath ((), (<.>)) import Data.Time.Clock import Data.Time.Calendar import Data.SBV -- | make the string to call executable from the command line. All the heavy -- lifting is done by 'System.Process.showCommandForUser', the rest is just -- projections out of 'Data.SBV.SMTConfig' mkExecString :: SMTConfig -> FilePath -> String mkExecString config inputFile = showCommandForUser exec $ inputFile:opts where smtSolver = solver config exec = executable smtSolver opts' = options smtSolver config opts = L.delete "-in" opts' -- remove opt for interactive mode so -- that this plays nice with -- criterion environments -- | simple wrapper to create random file names. mkFileName :: IO String mkFileName = do gen <- newStdGen return . take 32 $ randomRs ('a','z') gen -- | Get (year, month, day) getDate :: IO (Integer, Int, Int) getDate = toGregorian . utctDay <$> getCurrentTime dateStamp :: IO String dateStamp = (\(y,m,d) -> show y ++ "-" ++ show m ++ "-" ++ show d) <$> getDate -- | Construct a timestamp timeStamp :: IO String timeStamp = fmap (spaceTo '-') . show <$> getCurrentTime spaceTo :: Char -> Char -> Char spaceTo c x | isSpace x = c | otherwise = x -- | Construct a benchmark file name. The input name should be a time stamp or -- whatever you want to name the benchmark benchResultsFile :: FilePath -> FilePath benchResultsFile nm = "SBVBenchSuite" "BenchResults" nm <.> "csv" -- | The classifier takes a line of text and chunks it into (group-name, -- benchmark-name), for example: classifier :: Char -> String -> Maybe (String, String) classifier e nm = Just $ last chunks where is :: [Int] is = L.elemIndices e nm chunks = [(a, tail b) | (a, b) <- fmap (`L.splitAt` nm) is] -- | We live with some code duplication due to the way overhead benchmarks apply -- the "standalone" and "sbv" labels. By abstracting for overhead benchmarks -- these labels will be appended to the description string. This is counter to -- the assumptions of the bench-show package, thus we define a specialty -- classifier to handle the overhead case overheadClassifier :: Char -> String -> Maybe (String, String) overheadClassifier e nm = Just $ last $ fmap (\(a,b) -> (tail b, a)) chunks where is :: [Int] is = L.elemIndices e nm chunks = fmap (`L.splitAt` nm) is -- | a helper function to remove benchmarks where the over head benchmark -- doesn't work or failed for some reason. This will write a filtered version -- and return the file path to that filtered version. filterOverhead :: Char -> FilePath -> IO FilePath filterOverhead e fp = do (header:file) <- L.lines <$> readFile fp -- only keep instances of 3 or greater. This number -- comes from splitting benchmark output by '/'. -- Because our groups are separated by '//' and the -- overhead by '/' an overhead run will have >3 splits, -- but a normal benchmark will only have two from '//' let filteredContent = filter ((>=3) . length . L.elemIndices e) file filteredFilePath = fp ++ "_filtered" writeFile filteredFilePath (concat $ header:filteredContent) return filteredFilePath