{-# LANGUAGE ApplicativeDo #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE DataKinds #-} module Crux.Config.Common ( OutputOptions(..), CruxOptions(..), PathStrategy(..), cruxOptions, defaultOutputOptions, postprocessOptions, ) where import Control.Lens (set) import Data.Functor.Alt import Data.Generics.Product.Fields (field) import Data.Time(DiffTime, NominalDiffTime) import Data.Maybe(fromMaybe) import Data.Char(toLower) import Data.Word (Word64) import Data.Text (pack) import GHC.Generics (Generic) import System.Directory ( createDirectoryIfMissing ) import Crux.Config import Crux.Config.Load (ColorOptions(..)) import Crux.Log as Log import Config.Schema import What4.ProblemFeatures data PathStrategy = AlwaysMergePaths | SplitAndExploreDepthFirst pathStrategySpec :: ValueSpec PathStrategy pathStrategySpec = (AlwaysMergePaths <$ atomSpec "always-merge") (SplitAndExploreDepthFirst <$ atomSpec "split-dfs") postprocessOptions :: Logs msgs => SupportsCruxLogMessage msgs => CruxOptions -> IO CruxOptions postprocessOptions = checkPathStrategyInteractions >> checkPathSatInteractions >> checkBldDir checkPathStrategyInteractions :: Logs msgs => SupportsCruxLogMessage msgs => CruxOptions -> IO CruxOptions checkPathStrategyInteractions crux = case pathStrategy crux of AlwaysMergePaths -> return crux SplitAndExploreDepthFirst | profileCrucibleFunctions crux || branchCoverage crux -> do sayCrux Log.DisablingProfilingIncompatibleWithPathSplitting return crux { profileCrucibleFunctions = False, branchCoverage = False } | otherwise -> return crux checkPathSatInteractions :: Logs msgs => SupportsCruxLogMessage msgs => CruxOptions -> IO CruxOptions checkPathSatInteractions crux = case checkPathSat crux of True -> return crux False | branchCoverage crux -> do sayCrux Log.DisablingBranchCoverageRequiresPathSatisfiability return crux { branchCoverage = False } | otherwise -> return crux checkBldDir :: CruxOptions -> IO CruxOptions checkBldDir crux = do createDirectoryIfMissing True $ bldDir crux return crux data OutputOptions = OutputOptions { colorOptions :: ColorOptions , printFailures :: Bool -- ^ Print errors regarding failed verification goals , printSymbolicVars :: Bool -- ^ Print values assigned to symbolic variables -- when printing failed verification goals , simVerbose :: Int -- ^ Level of verbosity for the symbolic simulation , quietMode :: Bool -- ^ If true, produce minimal output } deriving (Generic) defaultOutputOptions :: ColorOptions -> OutputOptions defaultOutputOptions copts = OutputOptions { colorOptions = copts , printFailures = False , printSymbolicVars = False , quietMode = False , simVerbose = 0 } -- | Common options for Crux-based binaries. data CruxOptions = CruxOptions { inputFiles :: [FilePath] -- ^ the files to analyze , outDir :: FilePath -- ^ Write results in this location. -- If empty, then do not produce any analysis results. , bldDir :: FilePath -- ^ Directory for writing files generated from the inputFiles set -- (e.g. building C sources into LLVM bitcode files) for analysis. , checkPathSat :: Bool -- ^ Should we enable path satisfiability checking? , profileCrucibleFunctions :: Bool , profileSolver :: Bool , branchCoverage :: Bool , pathStrategy :: PathStrategy , globalTimeout :: Maybe NominalDiffTime , goalTimeout :: Maybe DiffTime , profileOutputInterval :: NominalDiffTime , loopBound :: Maybe Word64 -- ^ Should we artifically bound the number of loop iterations , recursionBound :: Maybe Word64 -- ^ Should we artifically bound the number of recursive calls to functions? , makeCexes :: Bool -- ^ Should we construct counter-example executables , unsatCores :: Bool -- ^ Should we attempt to compute unsatisfiable cores for successful -- proofs? , getNAbducts :: Maybe Word64 -- ^ How many abducts should we get from the solver for sat results? -- Only works with cvc5 , solver :: String -- ^ Solver to use to discharge proof obligations , pathSatSolver :: Maybe String -- ^ A separate solver to use for path satisfiability checking if that -- feature is enabled and if the path satisfiability checking solver should -- differ from the solver used to discharge proof obligations (default: use -- the proof obligation solver) , forceOfflineGoalSolving :: Bool -- ^ Force goals to be verified using an offline solver instance, even if it -- would have been possible to use the same solver in online mode , pathSatSolverOutput :: Maybe FilePath -- ^ The file to store the interaction session between the path -- satisfiability checker and the solver (if path satisfiability checking is -- enabled) , onlineSolverOutput :: Maybe FilePath -- ^ The file to store the interaction with the online goal solver (if -- solving is being performed online) , offlineSolverOutput :: Maybe FilePath -- ^ A template to use for files to store interactions with offline goal -- solvers (if solving is being performed offline). , yicesMCSat :: Bool -- ^ Should the MC-SAT Yices solver be enabled (disables unsat cores; default: no) , floatMode :: String -- ^ Tells the solver which representation to use for floating point values. , proofGoalsFailFast :: Bool -- ^ If true, stop attempting to prove goals as soon as one is disproved , skipReport :: Bool -- ^ Don't produce the HTML reports that describe the verification task , skipSuccessReports :: Bool -- ^ Skip reporting on successful proof obligations , skipIncompleteReports :: Bool -- ^ Skip reporting on goals that arise from resource exhaustion , hashConsing :: Bool -- ^ Turn on hash-consing in the symbolic expression backend , onlineProblemFeatures :: ProblemFeatures -- ^ Problem Features to force in online solvers , outputOptions :: OutputOptions -- ^ Output options grouped together for easy transfer to the logger } deriving (Generic) cruxOptions :: Config CruxOptions cruxOptions = Config { cfgFile = do inputFiles <- section "files" (oneOrList fileSpec) [] "Input files to process." outDir <- section "output-directory" dirSpec "" "Save results in this directory." bldDir <- section "build-dir" dirSpec "crux-build" "Directory in which to create files generated from the inputFiles." checkPathSat <- section "path-sat" yesOrNoSpec False "Enable path satisfiability checking (default: no)." profileCrucibleFunctions <- section "profile-crucible" yesOrNoSpec False "Profile crucible function entry/exit. (default: no)" profileSolver <- section "profile-solver" yesOrNoSpec False "Profile solver events. (default: no)" branchCoverage <- section "branch-coverage" yesOrNoSpec False "Record branch coverage information. (default: no)" profileOutputInterval <- section "profiling-period" fractionalSpec 5 "Time between intermediate profile data reports (default: 5 seconds)" globalTimeout <- sectionMaybe "timeout" fractionalSpec "Stop executing the simulator after this many seconds." goalTimeout <- sectionMaybe "goal-timeout" fractionalSpec "Stop trying to prove a goal after this many seconds." loopBound <- sectionMaybe "iteration-bound" numSpec "Bound all loops to at most this many iterations." recursionBound <- sectionMaybe "recursion-bound" numSpec "Bound the number of recursive calls to at most this many calls." pathStrategy <- section "path-strategy" pathStrategySpec AlwaysMergePaths "Simulator strategy for path exploration." makeCexes <- section "make-executables" yesOrNoSpec True "Should we generate counter-example executables. (default: yes)" unsatCores <- section "unsat-cores" yesOrNoSpec True "Should we attempt to compute unsatisfiable cores for successfult proofs (default: yes)" getNAbducts <- sectionMaybe "get-abducts" numSpec "How many abducts should we get from the solver for sat results? Only works with cvc5, 0 otherwise." solver <- section "solver" stringSpec "yices" (pack $ "Select the solver to use to discharge proof obligations. " ++ "May be a single solver, a comma-separated list of solvers, or the string \"all\". " ++ "Specifying multiple solvers requires the --force-offline-goal-solving option. " ++ "(default: \"yices\")") pathSatSolver <- sectionMaybe "path-sat-solver" stringSpec "Select the solver to use for path satisfiability checking (if different from `solver` and required by the `path-sat` option). (default: use `solver`)" forceOfflineGoalSolving <- section "force-offline-goal-solving" yesOrNoSpec False "Force goals to be solved using an offline solver, even if the selected solver could have been used in online mode (default: no)" pathSatSolverOutput <- sectionMaybe "path-sat-solver-output" stringSpec "The file to store the interaction with the path satisfiability solver (if enabled and different from the main solver) (default: none)" onlineSolverOutput <- sectionMaybe "online-solver-output" stringSpec "The file to store the interaction with the online goal solver (if any) (default: none)" offlineSolverOutput <- sectionMaybe "offine-solver-output" stringSpec (pack offlineSolverOutputHelp) simVerbose <- section "sim-verbose" numSpec 1 "Verbosity of simulators. (default: 1)" yicesMCSat <- section "mcsat" yesOrNoSpec False "Enable the MC-SAT solver in Yices (disables unsat cores) (default: no)" floatMode <- section "floating-point" stringSpec "default" (pack $ "Select floating point representation," ++ " i.e. one of [real|ieee|uninterpreted|default]. " ++ "Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.") hashConsing <- section "hash-consing" yesOrNoSpec False "Enable hash-consing in the symbolic expression backend" printFailures <- section "print-failures" yesOrNoSpec True "Print error messages regarding failed verification goals" printSymbolicVars <- section "print-symbolic-vars" yesOrNoSpec False ("Print values assigned to symbolic variables " <> "when printing failed verification goals") skipReport <- section "skip-report" yesOrNoSpec False "Skip producing the HTML report after verification" skipSuccessReports <- section "skip-success-reports" yesOrNoSpec False "Skip reporting on successful proof obligations" skipIncompleteReports <- section "skip-incomplete-reports" yesOrNoSpec False "Skip reporting on proof obligations that arise from timeouts and resource exhaustion" noColors <- section "no-colors" yesOrNoSpec False "Suppress color codes in both the output and the errors" noColorsErr <- section "no-colors-err" yesOrNoSpec False "Suppress color codes in the errors" noColorsOut <- section "no-colors-out" yesOrNoSpec False "Suppress color codes in the output" quietMode <- section "quiet-mode" yesOrNoSpec False "If true, produce minimal output" proofGoalsFailFast <- section "proof-goals-fail-fast" yesOrNoSpec False "If true, stop attempting to prove goals as soon as one of them is disproved" onlineProblemFeatures <- pure noFeatures pure CruxOptions { outputOptions = OutputOptions { colorOptions = ColorOptions { noColorsErr = noColorsErr || noColors , noColorsOut = noColorsOut || noColors }, .. }, .. } , cfgEnv = [ EnvVar "BLDDIR" "Directory for writing build files generated from the input files." $ \v opts -> Right opts { bldDir = v } ] , cfgCmdLineFlag = [ Option "d" ["sim-verbose"] "Set simulator verbosity level." $ ReqArg "NUM" $ parsePosNum "NUM" $ \v -> set (field @"outputOptions" . field @"simVerbose") v , Option [] ["path-sat"] "Enable path satisfiability checking" $ NoArg $ \opts -> Right opts { checkPathSat = True } , Option [] ["output-directory"] "Location for reports. If unset, no reports will be generated." $ ReqArg "DIR" $ \v opts -> Right opts { outDir = v } , Option [] ["profile-crucible"] "Enable profiling of crucible function entry/exit" $ NoArg $ \opts -> Right opts { profileCrucibleFunctions = True } , Option [] ["profile-solver"] "Enable profiling of solver events" $ NoArg $ \opts -> Right opts { profileSolver = True } , Option [] ["branch-coverage"] "Record branch coverage information" $ NoArg $ \opts -> Right opts { branchCoverage = True } , Option "t" ["timeout"] "Stop executing the simulator after this many seconds (default: 60)" $ OptArg "SECS" $ dflt "60" $ parseNominalDiffTime "seconds" $ \v opts -> opts { globalTimeout = Just v } , Option [] ["goal-timeout"] "Stop trying to prove each goal after this many seconds (default: 10)." $ OptArg "SECS" $ dflt "10" $ parseDiffTime "seconds" $ \v opts -> opts { goalTimeout = Just v } , Option "" ["path-strategy"] "Strategy to use for exploring paths ('always-merge' or 'split-dfs')" $ ReqArg "strategy" $ parsePathStrategy $ \strat opts -> opts{ pathStrategy = strat } , Option "p" ["profiling-period"] "Time between intermediate profile data reports (default: 5 seconds)" $ OptArg "SECS" $ dflt "5" $ parseNominalDiffTime "seconds" $ \v opts -> opts { profileOutputInterval = v } , Option "i" ["iteration-bound"] "Bound all loops to at most this many iterations" $ ReqArg "ITER" $ parsePosNum "iterations" $ \v opts -> opts { loopBound = Just v } , Option "r" ["recursion-bound"] "Bound all recursive calls to at most this many calls" $ ReqArg "CALLS" $ parsePosNum "calls" $ \v opts -> opts { recursionBound = Just v } , Option "x" ["no-execs"] "Disable generating counter-example executables" $ NoArg $ \opts -> Right opts { makeCexes = False } , Option [] ["no-unsat-cores"] "Disable computing unsat cores for successful proofs" $ NoArg $ \opts -> Right opts { unsatCores = False } , Option "n" ["get-abducts"] "Get these many abducts. Only works with cvc5, 0 otherwise." $ ReqArg "ABDUCTS" $ parsePosNum "abducts" $ \v opts -> opts { getNAbducts = Just v } , Option "s" ["solver"] ("Select the solver to use to discharge proof obligations. " ++ "May be a single solver, a comma-separated list of solvers, or the string \"all\". " ++ "Specifying multiple solvers requires the --force-offline-goal-solving option. " ++ "(default: \"yices\")") $ ReqArg "SOLVER" $ \v opts -> Right opts { solver = map toLower v } , Option [] ["path-sat-solver"] "Select the solver to use for path satisfiability checking (if different from `solver` and required by the `path-sat` option). (default: use `solver`)" $ OptArg "SOLVER" $ \ms opts -> Right opts { pathSatSolver = ms } , Option [] ["force-offline-goal-solving"] "Force goals to be solved using an offline solver, even if the selected solver could have been used in online mode (default: no)" $ NoArg $ \opts -> Right opts { forceOfflineGoalSolving = True } , Option [] ["path-sat-solver-output"] "The file to store the interaction with the path satisfiability solver (if enabled and different from the main solver) (default: none)" $ ReqArg "FILE" $ \f opts -> Right opts { pathSatSolverOutput = Just f } , Option [] ["online-solver-output"] "The file to store the interaction with the online goal solver (if any) (default: none)" $ ReqArg "FILE" $ \f opts -> Right opts { onlineSolverOutput = Just f } , Option [] ["offline-solver-output"] offlineSolverOutputHelp $ ReqArg "FILE" $ \f opts -> Right opts { offlineSolverOutput = Just f } , Option [] ["mcsat"] "Enable the MC-SAT solver in Yices (disables unsat cores)" $ NoArg $ \opts -> Right opts { yicesMCSat = True } , Option [] ["skip-report"] "Skip producing the HTML report following verificaion" $ NoArg $ \opts -> Right opts { skipReport = True } , Option [] ["skip-success-reports"] "Skip reporting on successful proof obligations" $ NoArg $ \opts -> Right opts { skipSuccessReports = True } , Option [] ["skip-incomplete-reports"] "Skip reporting on proof obligations that arise from timeouts and resource exhaustion" $ NoArg $ \opts -> Right opts { skipIncompleteReports = True } , Option [] ["hash-consing"] "Enable hash-consing in the symbolic expression backend" $ NoArg $ \opts -> Right opts{ hashConsing = True } , Option [] ["skip-print-failures"] "Skip printing messages related to failed verification goals" $ NoArg $ Right . set (field @"outputOptions" . field @"printFailures") False , Option [] ["fail-fast"] "Stop attempting to prove goals as soon as one of them is disproved" $ NoArg $ \opts -> Right opts { proofGoalsFailFast = True } , Option "q" ["quiet"] "Quiet mode; produce minimal output" $ NoArg $ Right . set (field @"outputOptions" . field @"quietMode") True , Option "f" ["floating-point"] ("Select floating point representation," ++ " i.e. one of [real|ieee|uninterpreted|default]. " ++ "Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.") $ ReqArg "FPREP" $ \v opts -> Right opts { floatMode = map toLower v } ] } offlineSolverOutputHelp :: String offlineSolverOutputHelp = unlines [ "A template to use for files to store interactions with offline goal solvers" , "(if any) (default: none). For example, if the template is `offline-output.smt2`," , "then each file will be named `offline-output--.smt2," , "where is the number of the goal that was proven (starting at 0)" , "and is the name of the solver used to dispatch that goal." ] dflt :: String -> (String -> OptSetter opts) -> (Maybe String -> OptSetter opts) dflt x p mb = p (fromMaybe x mb) parseDiffTime :: String -> (DiffTime -> opts -> opts) -> String -> OptSetter opts parseDiffTime thing mk = parsePosNum thing (\a opts -> mk (cvt a) opts) where cvt :: Double -> DiffTime cvt = fromRational . toRational parseNominalDiffTime :: String -> (NominalDiffTime -> opts -> opts) -> String -> OptSetter opts parseNominalDiffTime thing mk = parsePosNum thing (\a opts -> mk (cvt a) opts) where cvt :: Double -> NominalDiffTime cvt = fromRational . toRational parsePathStrategy :: (PathStrategy -> opts -> opts) -> String -> OptSetter opts parsePathStrategy mk "always-merge" opts = Right $ mk AlwaysMergePaths opts parsePathStrategy mk "split-dfs" opts = Right $ mk SplitAndExploreDepthFirst opts parsePathStrategy _mk nm _opts = Left ("Unknown path strategy: " ++ show nm)