Common.hs

{-# 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

  , debug                    :: Bool
    -- ^ Drop into the Crucible debugger before simulation begins

  }
  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

          debug <-
            section "debug" yesOrNoSpec False
            "Drop into the Crucible debugger before simulation begins"

          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 }

      , Option [] ["debug"]
        "Drop into the Crucible debugger before simulation begins"
        $ NoArg $ \opts -> Right opts { debug = True }
      ]
  }

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-<goal number>-<solver name>.smt2,"
  , "where <goal number> is the number of the goal that was proven (starting at 0)"
  , "and <solver name> 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)