module G2.Config.Config ( Mode (..) , SMTSolver (..) , HigherOrderSolver (..) , IncludePath , Config (..) , BoolDef (..) , mkConfig , strArg , boolArg) where import Data.Char import Data.List import qualified Data.Map as M import System.Directory data Mode = Regular | Liquid deriving (Eq, Show, Read) data SMTSolver = ConZ3 | ConCVC4 deriving (Eq, Show, Read) data HigherOrderSolver = AllFuncs | SingleFunc deriving (Eq, Show, Read) type IncludePath = FilePath data Config = Config { mode :: Mode , baseInclude :: [IncludePath] , base :: [FilePath] -- ^ Filepath(s) to base libraries. Get compiled in order from left to right , extraDefaultInclude :: [IncludePath] , extraDefaultMods :: [FilePath] , logStates :: Maybe String -- ^ If Just, dumps all thes states into the given folder , maxOutputs :: Maybe Int -- ^ Maximum number of examples/counterexamples to output. TODO: Currently works only with LiquidHaskell , printCurrExpr :: Bool -- ^ Controls whether the curr expr is printed , printExprEnv :: Bool -- ^ Controls whether the expr env is printed , printRelExprEnv :: Bool -- ^ Controls whether the portion of the expr env relevant to the curr expr and path constraints is printed , printPathCons :: Bool -- ^ Controls whether path constraints are printed , returnsTrue :: Bool -- ^ If True, shows only those inputs that do not return True , higherOrderSolver :: HigherOrderSolver -- ^ How to try and solve higher order functions , smt :: SMTSolver -- ^ Sets the SMT solver to solve constraints with , steps :: Int -- ^ How many steps to take when running States , cut_off :: Int -- ^ How many steps to take after finding an equally good equiv state, in LH mode , switch_after :: Int --- ^ How many steps to take in a single step, in LH mode , strict :: Bool -- ^ Should the function output be strictly evaluated? , timeLimit :: Int -- ^ Seconds , validate :: Bool -- ^ If True, HPC is run on G2's output, to measure code coverage. TODO: Currently doesn't work -- , baseLibs :: [BaseLib] } -- mkConfigDef :: Config -- mkConfigDef = mkConfig [] M.empty baseRoot :: IO FilePath baseRoot = do g2Dir <- getHomeDirectory >>= \f -> return $ f ++ "/.g2" return $ g2Dir ++ "/base-4.9.1.0" mkConfig :: String -> [String] -> M.Map String [String] -> Config mkConfig homedir as m = Config { mode = Regular , baseInclude = baseIncludeDef (strArg "base" as m id homedir) , base = baseDef (strArg "base" as m id homedir) , extraDefaultInclude = extraDefaultIncludePaths (strArg "extra-base-inc" as m id homedir) , extraDefaultMods = extraDefaultPaths (strArg "extra-base" as m id homedir) , logStates = strArg "log-states" as m Just Nothing , maxOutputs = strArg "max-outputs" as m (Just . read) Nothing , printCurrExpr = boolArg "print-ce" as m Off , printExprEnv = boolArg "print-eenv" as m Off , printPathCons = boolArg "print-pc" as m Off , printRelExprEnv = boolArg "print-rel-eenv" as m Off , returnsTrue = boolArg "returns-true" as m Off , higherOrderSolver = strArg "higher-order" as m higherOrderSolArg SingleFunc , smt = strArg "smt" as m smtSolverArg ConZ3 , steps = strArg "n" as m read 1000 , cut_off = strArg "cut-off" as m read 600 , switch_after = strArg "switch-after" as m read 300 , strict = boolArg "strict" as m On , timeLimit = strArg "time" as m read 300 , validate = boolArg "validate" as m Off -- , baseLibs = [BasePrelude, BaseException] } baseIncludeDef :: FilePath -> [FilePath] baseIncludeDef root = [ root ++ "/.g2/base-4.9.1.0/Control/Exception/" , root ++ "/.g2/base-4.9.1.0/" , root ++ "/.g2/base-4.9.1.0/" , root ++ "/.g2/base-4.9.1.0/Data/Internal/" ] baseDef :: FilePath -> [FilePath] baseDef root = [ root ++ "/.g2/base-4.9.1.0/Control/Exception/Base.hs" , root ++ "/.g2/base-4.9.1.0/Prelude.hs" , root ++ "/.g2/base-4.9.1.0/Control/Monad.hs" , root ++ "/.g2/base-4.9.1.0/Data/Internal/Map.hs" ] extraDefaultIncludePaths :: FilePath -> [FilePath] extraDefaultIncludePaths root = [ root ++ "/.g2/G2Stubs/src/" ] extraDefaultPaths :: FilePath -> [FilePath] extraDefaultPaths root = [ root ++ "/.g2/G2Stubs/src/G2/QuasiQuotes/G2Rep.hs" ] smtSolverArg :: String -> SMTSolver smtSolverArg = smtSolverArg' . map toLower smtSolverArg' :: String -> SMTSolver smtSolverArg' "z3" = ConZ3 smtSolverArg' "cvc4" = ConCVC4 smtSolverArg' _ = error "Unrecognized SMT solver." higherOrderSolArg :: String -> HigherOrderSolver higherOrderSolArg = higherOrderSolArg' . map toLower higherOrderSolArg' :: String -> HigherOrderSolver higherOrderSolArg' "all" = AllFuncs higherOrderSolArg' "single" = SingleFunc higherOrderSolArg' _ = error "Unrecognized higher order solver." data BoolDef = On | Off deriving (Eq, Show) -- If the given string is on the command line, returns True -- If --no-[str] is on the command line, returns False -- otherwise, looks in the config file, and if there is not option there, -- uses the default to decide boolArg :: String -> [String] -> M.Map String [String] -> BoolDef -> Bool boolArg s a m bd = let d = if bd == On then True else False in if "--" ++ s `elem` a then True else if "--no-" ++ s `elem` a then False else case M.lookup s m of Just st -> strToBool st d Nothing -> d strToBool :: [String] -> Bool -> Bool strToBool [s] b | s' == "true" = True | s' == "1" = True | s' == "false" = False | s' == "0" = False | otherwise = b where s' = map toLower s strToBool _ b = b --Converts strings arguments to arbitrary types strArg :: String -> [String] -> M.Map String [String] -> (String -> a) -> a -> a strArg s a m f d = case elemIndex ("--" ++ s) a of Just i -> if i >= length a then error ("Invalid use of " ++ s) else f (a !! (i + 1)) Nothing -> case M.lookup s m of Just st -> strToArg st f d Nothing -> d strToArg :: [String] -> (String -> a) -> a -> a strToArg [s] f _ = f s strToArg _ _ d = d strArgs :: String -> [String] -> M.Map String [String] -> (String -> a) -> [a] -> [a] strArgs s a m f d = case elemIndex ("--" ++ s) a of Just i -> if i >= length a then error ("Invalid use of " ++ s) else [f (a !! (i + 1))] Nothing -> case M.lookup s m of Just st -> strsToArgs st f Nothing -> d strsToArgs :: [String] -> (String -> a) -> [a] strsToArgs = flip map