diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2018-2022 Galois Inc. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in + the documentation and/or other materials provided with the + distribution. + + * Neither the name of Galois, Inc. nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/crux.cabal b/crux.cabal new file mode 100644 --- /dev/null +++ b/crux.cabal @@ -0,0 +1,100 @@ +Cabal-version: 2.2 +Name: crux +Version: 0.7 +Copyright: (c) Galois, Inc. 2018-2022 +Author: sweirich@galois.com +Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com +License: BSD-3-Clause +License-file: LICENSE +Build-type: Simple +Category: Language +Synopsis: Simple top-level library for Crucible Simulation +Description: + The Crux library provides the common elements for running a Crucible + simulation on specific source files, with various options. This + library is used by specific instances of Crux tools that provide a + command-line interface to Crucible-based simulation and + verification, usually by embedding verification specifications in + the source language. + +source-repository head + type: git + location: https://github.com/GaloisInc/crucible + subdir: crux + +library + + build-depends: + base >= 4 && < 5, + aeson < 2.3, + async, + attoparsec, + bv-sized >= 1.0.0, + bytestring, + containers, + contravariant >= 1.5 && < 1.6, + crucible, + directory, + filepath, + generic-lens, + lens, + libBF >= 0.6 && < 0.7, + lumberjack >= 1.0 && < 1.1, + parameterized-utils >= 1.0 && < 2.2, + prettyprinter >= 1.7.0, + split >= 0.2, + terminal-size, + text, + time >= 1.9 && < 2.0, + vector >= 0.7, + what4 >= 0.4.1, + ansi-terminal, + Glob >= 0.10 && < 0.11, + raw-strings-qq, + simple-get-opt < 0.5, + config-value, + config-schema >= 1.2.2.0, + semigroupoids, + xml, + yaml >= 0.11 && < 0.12 + + hs-source-dirs: src + + exposed-modules: + Crux, + Crux.Types, + Crux.FormatOut, + Crux.Goal, + Crux.Log, + Crux.ProgressBar, + Crux.Report, + Crux.Model, + Crux.Loops, + Crux.Config, + Crux.Config.Load, + Crux.Config.Doc, + Crux.Config.Common, + Crux.Config.Solver, + Crux.Overrides, + Crux.SVCOMP, + Crux.SVCOMP.Witness, + Crux.UI.JS, + Crux.Version + + other-modules: + Crux.UI.Jquery, + Crux.UI.IndexHtml + Paths_crux + + autogen-modules: + Paths_crux + + ghc-options: -Wall + -Wcompat + -Werror=incomplete-patterns + -Werror=missing-methods + -Werror=overlapping-patterns + -Wpartial-fields + -Wincomplete-uni-patterns + ghc-prof-options: -O2 + default-language: Haskell2010 diff --git a/src/Crux.hs b/src/Crux.hs new file mode 100644 --- /dev/null +++ b/src/Crux.hs @@ -0,0 +1,738 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# Language RankNTypes, ImplicitParams, TypeApplications, MultiWayIf #-} +{-# Language OverloadedStrings, FlexibleContexts, ScopedTypeVariables #-} + +{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-} + +module Crux + ( runSimulator + , postprocessSimResult + , loadOptions + , mkOutputConfig + , defaultOutputConfig + , SimulatorCallbacks(..) + , SimulatorHooks(..) + , RunnableState(..) + , pattern RunnableState + , Explainer + , CruxOptions(..) + , SomeOnlineSolver(..) + , Crux(..) + , module Crux.Config + , module Crux.Log + ) where + +import qualified Control.Exception as Ex +import Control.Lens +import Control.Monad ( unless, void, when ) +import qualified Data.Aeson as JSON +import Data.Foldable +import Data.Functor.Contravariant ( (>$<) ) +import Data.Functor.Contravariant.Divisible ( divide ) +import Data.Generics.Product.Fields (field) +import Data.IORef +import Data.Maybe ( fromMaybe ) +import qualified Data.Sequence as Seq +import Data.Text (Text) +import qualified Data.Text as T +import Data.Version (Version) +import Data.Void (Void) +import qualified Lumberjack as LJ +import Prettyprinter +import qualified System.Console.ANSI as AC +import System.Console.Terminal.Size (Window(Window), size) +import System.Directory (createDirectoryIfMissing) +import System.Exit (exitSuccess, ExitCode(..), exitFailure, exitWith) +import System.FilePath (()) +import System.IO ( Handle, hPutStr, stdout, stderr ) + +import Data.Parameterized.Classes +import Data.Parameterized.Nonce (newIONonceGenerator, NonceGenerator) +import Data.Parameterized.Some ( Some(..) ) + +import Lang.Crucible.Backend +import Lang.Crucible.Backend.Online +import qualified Lang.Crucible.Backend.Simple as CBS +import Lang.Crucible.CFG.Extension +import Lang.Crucible.Simulator +import Lang.Crucible.Simulator.BoundedExec +import Lang.Crucible.Simulator.BoundedRecursion +import Lang.Crucible.Simulator.PathSatisfiability +import Lang.Crucible.Simulator.PathSplitting +import Lang.Crucible.Simulator.PositionTracking +import Lang.Crucible.Simulator.Profiling +import Lang.Crucible.Types + + +import What4.Config (setOpt, getOptionSetting, verbosity, extendConfig) +import qualified What4.Expr as WE +import What4.FunctionName (FunctionName) +import What4.Interface (IsExprBuilder, getConfiguration) +import What4.InterpretedFloatingPoint (IsInterpretedFloatExprBuilder) +import What4.Protocol.Online (OnlineSolver) +import qualified What4.Solver as WS +import What4.Solver.CVC4 (cvc4Timeout) +import What4.Solver.CVC5 (cvc5Timeout) +import What4.Solver.Yices (yicesEnableMCSat, yicesGoalTimeout) +import What4.Solver.Z3 (z3Timeout) + +import Crux.Config +import Crux.Config.Common +import Crux.Config.Doc +import qualified Crux.Config.Load as Cfg +import qualified Crux.Config.Solver as CCS +import Crux.FormatOut ( sayWhatFailedGoals, sayWhatResultStatus ) +import Crux.Goal +import Crux.Log -- for the export list +import Crux.Log as Log +import Crux.Report +import Crux.Types + +pattern RunnableState :: forall sym . () => forall ext personality . (IsSyntaxExtension ext) => ExecState (personality sym) sym ext (RegEntry sym UnitType) -> RunnableState sym +pattern RunnableState es = RunnableStateWithExtensions es [] + +-- | A crucible @ExecState@ that is ready to be passed into the simulator. +-- This will usually, but not necessarily, be an @InitialState@. +data RunnableState sym where + RunnableStateWithExtensions :: (IsSyntaxExtension ext) + => ExecState (personality sym) sym ext (RegEntry sym UnitType) + -> [ExecutionFeature (personality sym) sym ext (RegEntry sym UnitType)] + -> RunnableState sym + +-- | Individual crux tools will generally call the @runSimulator@ combinator to +-- handle the nitty-gritty of setting up and running the simulator. Tools +-- provide @SimulatorCallbacks@ to hook into the simulation process at three +-- points: +-- +-- * Before simulation begins, to set up global variables, register override +-- functions, construct the initial program entry point, and generally do +-- any necessary language-specific setup (i.e., to produce a 'RunnableState') +-- * When simulation ends with an assertion failure ('Explainer') +-- * When simulation ends, regardless of the outcome, to interpret the results. +-- +-- All of these callbacks have access to the symbolic backend. +newtype SimulatorCallbacks msgs r + = SimulatorCallbacks + { getSimulatorCallbacks :: + forall sym bak t st fs. + ( IsSymBackend sym bak + , Logs msgs + , sym ~ WE.ExprBuilder t st fs + ) => + IO (SimulatorHooks sym bak t r) + } + + +-- | A GADT to capture the online solver constraints when we need them +data SomeOnlineSolver sym bak where + SomeOnlineSolver :: ( sym ~ WE.ExprBuilder scope st fs + , bak ~ OnlineBackend solver scope st fs + , IsSymBackend sym bak + , OnlineSolver solver + ) => bak -> SomeOnlineSolver sym bak + +-- | See 'SimulatorCallbacks' +data SimulatorHooks sym bak t r = + SimulatorHooks + { setupHook :: bak -> Maybe (SomeOnlineSolver sym bak) -> IO (RunnableState sym) + , onErrorHook :: bak -> IO (Explainer sym t Void) + , resultHook :: bak -> CruxSimulationResult -> IO r + } + +-- | Given the result of a simulation and proof run, report the overall +-- status, generate user-consumable reports and compute the exit code. +postprocessSimResult :: + Logs msgs => + Bool -> CruxOptions -> CruxSimulationResult -> IO ExitCode +postprocessSimResult showFailedGoals opts res = + do -- print goals that failed and overall result + logSimResult showFailedGoals res + + -- Generate report + generateReport opts res + + return $! computeExitCode res + + +-- | Load crux generic and the provided options, and provide them to +-- the given continuation. +-- +-- IMPORTANT: This processes options like @help@ and @version@, which +-- just print something and exit, so this function may never call +-- its continuation. +loadOptions :: + SupportsCruxLogMessage msgs => + (Maybe OutputOptions -> OutputConfig msgs) -> + Text {- ^ Name -} -> + Version -> + Config opts -> + (Logs msgs => (CruxOptions, opts) -> IO a) -> + IO a +loadOptions mkOutCfg nm ver config cont = + do let optSpec = cfgJoin cruxOptions config + (copts, opts) <- Cfg.loadConfig nm optSpec + case opts of + Cfg.ShowHelp -> + do let ?outputConfig = mkOutCfg (Just (defaultOutputOptions copts)) + showHelp nm optSpec + exitSuccess + Cfg.ShowVersion -> + do let ?outputConfig = mkOutCfg (Just (defaultOutputOptions copts)) + showVersion nm ver + exitSuccess + Cfg.Options (cruxWithoutColorOptions, os) files -> + do let crux = set (field @"outputOptions" . field @"colorOptions") copts cruxWithoutColorOptions + let ?outputConfig = mkOutCfg (Just (outputOptions crux)) + crux' <- postprocessOptions crux { inputFiles = files ++ inputFiles crux } + cont (crux', os) + + `Ex.catch` \(e :: Ex.SomeException) -> + do let ?outputConfig = mkOutCfg Nothing + case (Ex.fromException e :: Maybe ExitCode) of + Just exitCode -> exitWith exitCode + Nothing -> logException e >> exitFailure + + +showHelp :: + Logs msgs => + SupportsCruxLogMessage msgs => + Text -> Config opts -> IO () +showHelp nm cfg = do + -- Ideally, this would be done in the log handler. We will soon try to change + -- the logging mechanism so thaat it prefers 'Doc' over 'Text' so that layout + -- decisions can be delayed to the log handlers. + outWidth <- maybe 80 (\(Window _ w) -> w) <$> size + let opts = LayoutOptions $ AvailablePerLine outWidth 0.98 + sayCrux (Log.Help (LogDoc (layoutPretty opts (configDocs nm cfg)))) + + +showVersion :: + Logs msgs => + SupportsCruxLogMessage msgs => + Text -> Version -> IO () +showVersion nm ver = sayCrux (Log.Version nm ver) + + +-- | Create an OutputConfig for Crux, based on an indication of whether colored +-- output should be used, the normal and error output handles, and the parsed +-- CruxOptions. +-- +-- If no CruxOptions are available (i.e. Nothing, as used in the preliminary +-- portions of loadOptions), then a default output stance is applied; the +-- default stance is described along with the individual option below. +-- +-- The following CruxOptions affect the generated OutputConfig: +-- +-- * noColorsErr (default stance: False when the error handle supports +-- colors, as reported by System.Console.ANSI.hSupportsANSIColor) +-- * noColorsOut (default stance: False when the output handle supports +-- colors, as reported by System.Console.ANSI.hSupportsANSIColor) +-- * printFailures (default stance: True) +-- * quietMode (default stance: False) +-- * simVerbose (default stance: False) +mkOutputConfig :: + JSON.ToJSON msgs => + (Handle, Bool) -> (Handle, Bool) -> + (msgs -> SayWhat) -> Maybe OutputOptions -> + OutputConfig msgs +mkOutputConfig (outHandle, outWantsColor) (errHandle, errWantsColor) logMessageToSayWhat opts = + let consensusBetween wants maybeRefuses = wants && not (fromMaybe False maybeRefuses) + copts = colorOptions <$> opts + outSpec = (outHandle, consensusBetween outWantsColor (Cfg.noColorsOut <$> copts)) + errSpec@(_, errShouldColor) = (errHandle, consensusBetween errWantsColor (Cfg.noColorsErr <$> copts)) + lgWhat = let la = LJ.LogAction $ logToStd outSpec errSpec + -- TODO simVerbose may not be the best setting to use here... + baseline = if maybe False ((> 1) . simVerbose) opts + then Noisily + else Simply + in if beQuiet + then logfltr OK >$< la + else logfltr baseline >$< la + beQuiet = maybe False quietMode opts + logfltr allowed = \case + SayNothing -> SayNothing + w@(SayWhat lvl _ _) -> if lvl >= allowed then w else SayNothing + SayMore m1 m2 -> case (logfltr allowed m1, logfltr allowed m2) of + (SayNothing, SayNothing) -> SayNothing + (SayNothing, m) -> m + (m, SayNothing) -> m + (m1', m2') -> SayMore m1' m2' + + printFails = maybe True printFailures opts + printVars = maybe False printSymbolicVars opts + lgGoal = sayWhatFailedGoals printFails printVars >$< lgWhat + splitResults r@(CruxSimulationResult _cmpl gls) = (snd <$> gls, r) + in OutputConfig + { _outputHandle = outHandle + , _quiet = beQuiet + , _logMsg = logMessageToSayWhat >$< lgWhat + , _logExc = let seeRed = AC.hSetSGR errHandle + [ AC.SetConsoleIntensity AC.BoldIntensity + , AC.SetColor AC.Foreground AC.Vivid AC.Red] + seeCalm = AC.hSetSGR errHandle [AC.Reset] + dispExc = hPutStr errHandle . Ex.displayException + in if errShouldColor + then LJ.LogAction $ \e -> Ex.bracket_ seeRed seeCalm $ dispExc e + else LJ.LogAction $ dispExc + , _logSimResult = \showDetails -> + if showDetails + then divide splitResults + lgGoal + (sayWhatResultStatus >$< lgWhat) + else sayWhatResultStatus >$< lgWhat + , _logGoal = Seq.singleton >$< lgGoal + } + +defaultOutputConfig :: + JSON.ToJSON msgs => + (msgs -> SayWhat) -> IO (Maybe OutputOptions -> OutputConfig msgs) +defaultOutputConfig logMessagesToSayWhat = do + outWantsColor <- AC.hSupportsANSIColor stdout + errWantsColor <- AC.hSupportsANSIColor stderr + return $ Crux.mkOutputConfig (stdout, outWantsColor) (stderr, errWantsColor) logMessagesToSayWhat + + +-------------------------------------------------------------------------------- + +-- | For a given configuration, compute the 'FloatModeRepr' +-- +-- Note that this needs to be CPS-ed because of the type parameter to the float +-- mode. Also note that we can't use this function in +-- 'withSelectedOnlineBackend', unfortunately, because that function requires a +-- 'IsInterpretedFloatExprBuilder' constraint that we don't seem to have a way +-- to capture in this CPS-ed style. +withFloatRepr :: + CCS.HasDefaultFloatRepr solver => + st s -> + CruxOptions -> + [solver] -> + (forall fm . + IsInterpretedFloatExprBuilder (WE.ExprBuilder s st (WE.Flags fm)) => + WE.FloatModeRepr fm -> + IO a) -> + IO a +withFloatRepr st cruxOpts selectedSolvers k = + case floatMode cruxOpts of + "real" -> k WE.FloatRealRepr + "ieee" -> k WE.FloatIEEERepr + "uninterpreted" -> k WE.FloatUninterpretedRepr + "default" -> case selectedSolvers of + [oneSolver] -> CCS.withDefaultFloatRepr st oneSolver k + _ -> k WE.FloatUninterpretedRepr + fm -> fail ("Unknown floating point mode: " ++ fm ++ "; expected one of [real|ieee|uninterpreted|default]") + +-- | Parse through the options structure to determine which online backend to +-- instantiate (including the chosen floating point mode). +-- +-- The choice of solver is provided as a separate argument (the +-- 'CCS.SolverOnline'). This function dispatches primarily on floating point +-- mode. An explicit floating point mode can be provided if it has to match +-- another solver that has already started. This code is slightly complicated +-- and duplicated because it is very hard to quantify over 'FloatModeRepr's in +-- such a way that captures the necessary 'IsInterpretedFloatExprBuilder' +-- constraints. +withSelectedOnlineBackend :: forall msgs scope st a. + Logs msgs => + SupportsCruxLogMessage msgs => + CruxOptions -> + NonceGenerator IO scope -> + CCS.SolverOnline -> + Maybe String -> + st scope -> + -- The string is an optional explicitly-requested float mode that supersedes the choice in + -- the configuration (probably due to using two different online connections) + (forall solver fm . + ( OnlineSolver solver + , IsInterpretedFloatExprBuilder (WE.ExprBuilder scope st (WE.Flags fm)) + ) => + (OnlineBackend solver scope st (WE.Flags fm) -> IO a)) -> + IO a +withSelectedOnlineBackend cruxOpts nonceGen selectedSolver maybeExplicitFloatMode initSt k = + case fromMaybe (floatMode cruxOpts) maybeExplicitFloatMode of + "real" -> withOnlineBackendFM WE.FloatRealRepr + "ieee" -> withOnlineBackendFM WE.FloatIEEERepr + "uninterpreted" -> withOnlineBackendFM WE.FloatUninterpretedRepr + "default" -> + case selectedSolver of + CCS.Yices -> withOnlineBackendFM WE.FloatRealRepr + CCS.CVC4 -> withOnlineBackendFM WE.FloatRealRepr + CCS.CVC5 -> withOnlineBackendFM WE.FloatRealRepr + CCS.STP -> withOnlineBackendFM WE.FloatRealRepr + CCS.Z3 -> withOnlineBackendFM WE.FloatIEEERepr + fm -> fail ("Unknown floating point mode: " ++ fm ++ "; expected one of [real|ieee|uninterpreted|default]") + + where + withOnlineBackendFM :: + IsInterpretedFloatExprBuilder (WE.ExprBuilder scope st (WE.Flags fm)) => + WE.FloatModeRepr fm -> + IO a + withOnlineBackendFM fm = + do sym <- WE.newExprBuilder fm initSt nonceGen + withSelectedOnlineBackend' cruxOpts selectedSolver sym k + +withSelectedOnlineBackend' :: + Logs msgs => + SupportsCruxLogMessage msgs => + IsInterpretedFloatExprBuilder (WE.ExprBuilder scope st fs) => + + CruxOptions -> + CCS.SolverOnline -> + WE.ExprBuilder scope st fs -> + (forall solver. + OnlineSolver solver => + (OnlineBackend solver scope st fs -> IO a)) -> + IO a +withSelectedOnlineBackend' cruxOpts selectedSolver sym k = + let unsatCoreFeat | unsatCores cruxOpts + , not (yicesMCSat cruxOpts) = ProduceUnsatCores + | otherwise = NoUnsatFeatures + extraFeatures = onlineProblemFeatures cruxOpts + + in case selectedSolver of + CCS.Yices -> withYicesOnlineBackend sym unsatCoreFeat extraFeatures $ \bak -> do + symCfg sym yicesEnableMCSat (yicesMCSat cruxOpts) + case goalTimeout cruxOpts of + Just s -> symCfg sym yicesGoalTimeout (floor s) + Nothing -> return () + k bak + CCS.CVC4 -> withCVC4OnlineBackend sym unsatCoreFeat extraFeatures $ \bak -> do + case goalTimeout cruxOpts of + Just s -> symCfg sym cvc4Timeout (floor (s * 1000)) + Nothing -> return () + k bak + CCS.CVC5 -> withCVC5OnlineBackend sym unsatCoreFeat extraFeatures $ \bak -> do + case goalTimeout cruxOpts of + Just s -> symCfg sym cvc5Timeout (floor (s * 1000)) + Nothing -> return () + k bak + CCS.Z3 -> withZ3OnlineBackend sym unsatCoreFeat extraFeatures $ \bak -> do + case goalTimeout cruxOpts of + Just s -> symCfg sym z3Timeout (floor (s * 1000)) + Nothing -> return () + k bak + CCS.STP -> do + -- We don't have a timeout option for STP + case goalTimeout cruxOpts of + Just _ -> sayCrux (Log.UnsupportedTimeoutFor "STP") + Nothing -> return () + withSTPOnlineBackend sym k + +data ProfData sym = ProfData + { inFrame :: forall a. FunctionName -> IO a -> IO a + , profExecFeatures :: [GenericExecutionFeature sym] + , writeProf :: IO () + } + +noProfiling :: ProfData sym +noProfiling = ProfData + { inFrame = \_ x -> x + , profExecFeatures = [] + , writeProf = pure () + } + +setupProfiling :: IsSymInterface sym => sym -> CruxOptions -> IO (ProfData sym) +setupProfiling sym cruxOpts = + do tbl <- newProfilingTable + + when (profileSolver cruxOpts) $ + startRecordingSolverEvents sym tbl + + let profSource = case inputFiles cruxOpts of + [f] -> f + _ -> "multiple files" + + profOutFile = outDir cruxOpts "report_data.js" + saveProf = writeProfileReport profOutFile "crux profile" profSource + profOpts = ProfilingOptions + { periodicProfileInterval = profileOutputInterval cruxOpts + , periodicProfileAction = saveProf + } + + profFilt = EventFilter + { recordProfiling = profileCrucibleFunctions cruxOpts + , recordCoverage = branchCoverage cruxOpts + } + + pfs <- execFeatureIf (profileCrucibleFunctions cruxOpts || branchCoverage cruxOpts) + (profilingFeature tbl profFilt (Just profOpts)) + + pure ProfData + { inFrame = \str -> inProfilingFrame tbl str Nothing + , profExecFeatures = pfs + , writeProf = saveProf tbl + } + +execFeatureIf :: + Bool -> + IO (GenericExecutionFeature sym) -> + IO [GenericExecutionFeature sym] +execFeatureIf b m = if b then (:[]) <$> m else pure [] + +execFeatureMaybe :: + Maybe a -> + (a -> IO (GenericExecutionFeature sym)) -> + IO [GenericExecutionFeature sym] +execFeatureMaybe mb m = + case mb of + Nothing -> pure [] + Just a -> (:[]) <$> m a + + +-- | Common setup for all solver connections +setupSolver :: (IsExprBuilder sym, sym ~ WE.ExprBuilder t st fs) => CruxOptions -> Maybe FilePath -> sym -> IO () +setupSolver cruxOpts mInteractionFile sym = do + mapM_ (symCfg sym solverInteractionFile) (fmap T.pack mInteractionFile) + + -- Turn on hash-consing, if enabled + when (hashConsing cruxOpts) (WE.startCaching sym) + + let outOpts = outputOptions cruxOpts + -- The simulator verbosity is one less than our verbosity. + -- In this way, we can say things, without the simulator also + -- being verbose + symCfg sym verbosity $ toInteger $ if simVerbose outOpts > 1 + then simVerbose outOpts - 1 + else 0 + +-- | Common code for initializing all of the requested execution features +-- +-- This function is a bit funny because one feature, path satisfiability +-- checking, requires on online solver while the others do not. In order to +-- maximally reuse code, we pass in the necessary online constraints as an extra +-- argument when we have them available (i.e., when we build an online solver) +-- and elide them otherwise. +setupExecutionFeatures :: IsSymBackend sym bak + => CruxOptions + -> bak + -> Maybe (SomeOnlineSolver sym bak) + -> IO + ([GenericExecutionFeature sym], ProfData sym) +setupExecutionFeatures cruxOpts bak maybeOnline = do + let sym = backendGetSym bak + -- Setup profiling + let profiling = isProfiling cruxOpts + profInfo <- if profiling then setupProfiling sym cruxOpts + else pure noProfiling + + -- Global timeout + tfs <- execFeatureMaybe (globalTimeout cruxOpts) timeoutFeature + + -- Loop bound + bfs <- execFeatureMaybe (loopBound cruxOpts) $ \i -> + boundedExecFeature (\_ -> return (Just i)) True {- side cond: yes -} + + -- Recursion bound + rfs <- execFeatureMaybe (recursionBound cruxOpts) $ \i -> + boundedRecursionFeature (\_ -> return (Just i)) True {- side cond: yes -} + + -- Check path satisfiability + psat_fs <- case maybeOnline of + Just (SomeOnlineSolver _bak) -> + do enableOpt <- getOptionSetting enableOnlineBackend (getConfiguration sym) + _ <- setOpt enableOpt (checkPathSat cruxOpts) + execFeatureIf (checkPathSat cruxOpts) + $ pathSatisfiabilityFeature sym (considerSatisfiability bak) + Nothing -> return [] + + -- Position tracking + trackfs <- positionTrackingFeature sym + + return (concat [tfs, profExecFeatures profInfo, bfs, rfs, psat_fs, [trackfs]], profInfo) + +-- | Select the What4 solver adapter for the user's solver choice (used for +-- offline solvers) +withSolverAdapter :: CCS.SolverOffline -> (WS.SolverAdapter st -> a) -> a +withSolverAdapter solverOff k = + case solverOff of + CCS.Boolector -> k WS.boolectorAdapter + CCS.DReal -> k WS.drealAdapter + CCS.SolverOnline CCS.CVC4 -> k WS.cvc4Adapter + CCS.SolverOnline CCS.CVC5 -> k WS.cvc5Adapter + CCS.SolverOnline CCS.STP -> k WS.stpAdapter + CCS.SolverOnline CCS.Yices -> k WS.yicesAdapter + CCS.SolverOnline CCS.Z3 -> k WS.z3Adapter + +withSolverAdapters :: [CCS.SolverOffline] -> ([WS.SolverAdapter st] -> a) -> a +withSolverAdapters solverOffs k = + foldr go base solverOffs $ [] + where + base adapters = k adapters + go nextOff withAdapters adapters = withSolverAdapter nextOff (\adapter -> withAdapters (adapter:adapters)) + +-- | Parse through all of the user-provided options and start up the verification process +-- +-- This figures out which solvers need to be run, and in which modes. It takes +-- as arguments some of the results of common setup code. It also tries to +-- minimize code duplication between the different verification paths (e.g., +-- online vs offline solving). +runSimulator :: + Logs msgs => + SupportsCruxLogMessage msgs => + CruxOptions -> + SimulatorCallbacks msgs r -> + IO r +runSimulator cruxOpts simCallback = do + sayCrux (Log.Checking (inputFiles cruxOpts)) + createDirectoryIfMissing True (outDir cruxOpts) + Some (nonceGen :: NonceGenerator IO s) <- newIONonceGenerator + case CCS.parseSolverConfig cruxOpts of + + Right (CCS.SingleOnlineSolver onSolver) -> + withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing WE.EmptyExprBuilderState $ \bak -> do + let monline = Just (SomeOnlineSolver bak) + setupSolver cruxOpts (pathSatSolverOutput cruxOpts) (backendGetSym bak) + (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts bak monline + doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline (proveGoalsOnline bak) + + Right (CCS.OnlineSolverWithOfflineGoals onSolver offSolver) -> + withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing WE.EmptyExprBuilderState $ \bak -> do + let monline = Just (SomeOnlineSolver bak) + setupSolver cruxOpts (pathSatSolverOutput cruxOpts) (backendGetSym bak) + (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts bak monline + withSolverAdapter offSolver $ \adapter -> do + -- We have to add the configuration options from the solver adapter, + -- since they weren't included in the symbolic backend configuration + -- with the initial setup of the online solver (since it could have + -- been a different solver) + unless (CCS.sameSolver onSolver offSolver) $ + extendConfig (WS.solver_adapter_config_options adapter) (getConfiguration (backendGetSym bak)) + doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline (proveGoalsOffline [adapter]) + + Right (CCS.OnlyOfflineSolvers offSolvers) -> + withFloatRepr (WE.EmptyExprBuilderState @s) cruxOpts offSolvers $ \floatRepr -> do + withSolverAdapters offSolvers $ \adapters -> do + sym <- WE.newExprBuilder floatRepr WE.EmptyExprBuilderState nonceGen + bak <- CBS.newSimpleBackend sym + setupSolver cruxOpts Nothing sym + -- Since we have a bare SimpleBackend here, we have to initialize it + -- with the options taken from the solver adapter (e.g., solver path) + extendConfig (WS.solver_adapter_config_options =<< adapters) (getConfiguration sym) + (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts bak Nothing + doSimWithResults cruxOpts simCallback bak execFeatures profInfo Nothing (proveGoalsOffline adapters) + + Right (CCS.OnlineSolverWithSeparateOnlineGoals pathSolver goalSolver) -> + -- This case is probably the most complicated because it needs two + -- separate online solvers. The two must agree on the floating point + -- mode. + withSelectedOnlineBackend cruxOpts nonceGen pathSolver Nothing WE.EmptyExprBuilderState $ \pathSatBak -> do + let sym = backendGetSym pathSatBak + setupSolver cruxOpts (pathSatSolverOutput cruxOpts) sym + (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts pathSatBak (Just (SomeOnlineSolver pathSatBak)) + withSelectedOnlineBackend' cruxOpts goalSolver sym $ \goalBak -> do + doSimWithResults cruxOpts simCallback pathSatBak execFeatures profInfo (Just (SomeOnlineSolver pathSatBak)) (proveGoalsOnline goalBak) + + Left rsns -> fail ("Invalid solver configuration:\n" ++ unlines rsns) + + +-- | Core invocation of the symbolic execution engine +-- +-- This is separated out so that we don't have to duplicate the code sequence in +-- 'runSimulator'. The strategy used to ultimately discharge proof obligations +-- is a parameter to allow this code to use either an online or offline solver +-- connection. +-- +-- The main work in this function is setting up appropriate solver frames and +-- traversing the goals tree, as well as handling some reporting. +doSimWithResults :: + forall sym bak r t st fs msgs. + sym ~ WE.ExprBuilder t st fs => + IsSymBackend sym bak => + Logs msgs => + SupportsCruxLogMessage msgs => + CruxOptions -> + SimulatorCallbacks msgs r -> + bak -> + [GenericExecutionFeature sym] -> + ProfData sym -> + Maybe (SomeOnlineSolver sym bak) -> + ProverCallback sym + {- ^ The function to use to prove goals; this is intended to be + one of 'proveGoalsOffline' or 'proveGoalsOnline' -} -> + IO r +doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline goalProver = do + compRef <- newIORef ProgramComplete + glsRef <- newIORef Seq.empty + + frm <- pushAssumptionFrame bak + + SimulatorHooks setup onError interpretResult <- + getSimulatorCallbacks simCallback + inFrame profInfo "" $ do + -- perform tool-specific setup + RunnableStateWithExtensions initSt exts <- setup bak monline + explainFailure <- onError bak + + -- execute the simulator + case pathStrategy cruxOpts of + AlwaysMergePaths -> + do res <- executeCrucible (map genericToExecutionFeature execFeatures ++ exts) initSt + void $ resultCont compRef glsRef frm explainFailure (Result res) + SplitAndExploreDepthFirst -> + do (i,ws) <- executeCrucibleDFSPaths + (map genericToExecutionFeature execFeatures ++ exts) + initSt + (resultCont compRef glsRef frm explainFailure . Result) + sayCrux (Log.TotalPathsExplored i) + unless (null ws) $ + sayCrux (Log.PathsUnexplored (Seq.length ws)) + + sayCrux Log.SimulationComplete + when (isProfiling cruxOpts) $ writeProf profInfo + result <- CruxSimulationResult <$> readIORef compRef <*> readIORef glsRef + interpretResult bak result + + where + failfast = proofGoalsFailFast cruxOpts + + resultCont :: + IORef ProgramCompleteness + -> IORef (Seq.Seq (ProcessedGoals, ProvedGoals)) + -> FrameIdentifier + -> (Maybe (WE.GroundEvalFn t) -> LabeledPred (WE.Expr t BaseBoolType) SimError -> IO (Doc Void)) + -> Result personality (WE.ExprBuilder t st fs) + -> IO Bool + resultCont compRef glsRef frm explainFailure (Result res) = + do timedOut <- + case res of + TimeoutResult {} -> + do sayCrux Log.SimulationTimedOut + writeIORef compRef ProgramIncomplete + return True + _ -> return False + popUntilAssumptionFrame bak frm + let ctx = execResultContext res + inFrame profInfo "" $ do + todo <- getProofObligations bak + sayCrux $ Log.ProofObligations (LogProofObligation <$> maybe [] goalsToList todo) + when (isJust todo) $ sayCrux Log.AttemptingProvingVCs + (nms, proved) <- goalProver cruxOpts ctx explainFailure todo + mgt <- provedGoalsTree (backendGetSym bak) proved + case mgt of + Nothing -> return (not timedOut) + Just gt -> + do modifyIORef glsRef (Seq.|> (nms,gt)) + return (not (timedOut || (failfast && disprovedGoals nms > 0))) + +isProfiling :: CruxOptions -> Bool +isProfiling cruxOpts = + profileCrucibleFunctions cruxOpts || profileSolver cruxOpts || branchCoverage cruxOpts + +computeExitCode :: CruxSimulationResult -> ExitCode +computeExitCode (CruxSimulationResult cmpl gls) = maximum . (base:) . fmap f . toList $ gls + where + base = case cmpl of + ProgramComplete -> ExitSuccess + ProgramIncomplete -> ExitFailure 1 + f (nms,_gl) = + let tot = totalProcessedGoals nms + proved = provedGoals nms + in if proved == tot then + ExitSuccess + else + ExitFailure 1 diff --git a/src/Crux/Config.hs b/src/Crux/Config.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Config.hs @@ -0,0 +1,145 @@ +{-# Language MultiWayIf, OverloadedStrings, RankNTypes #-} +-- | This module deals with loading configurations. +module Crux.Config + ( -- * Writing configurations + Config(..), cfgJoin + + -- ** Configuration files + , SectionsSpec, section, sectionMaybe + , yesOrNoSpec, stringSpec, numSpec, fractionalSpec + , oneOrList, fileSpec, dirSpec, listSpec + + -- ** Environment variables + , EnvDescr(..), mapEnvDescr, liftEnvDescr, liftOptDescr + + -- ** Command line options + , OptDescr(..), ArgDescr(..), OptSetter + , mapOptDescr, mapArgDescr + , parsePosNum + ) where + +import Control.Lens (Lens', set, view) +import Data.Text (Text) +import Data.Maybe (fromMaybe) +import Text.Read(readMaybe) + +import SimpleGetOpt +import Config.Schema + + +{- | Loading options from multiple sources. First we load configuration +from a file, then we consider environment variables, and finally we +update using the command line flags. If there is no configuration file +provided, then this is equivalent to having an empty configuration file, +so the config file schema should be able to cope with missing settings. -} + +data Config opts = Config + { cfgFile :: SectionsSpec opts + -- ^ Configuration file settings (and, implicitly, defaults). + + , cfgEnv :: [ EnvDescr opts ] + -- ^ Settings from environment variables + + , cfgCmdLineFlag :: [ OptDescr opts ] + -- ^ Command line flags. + } + +-- | How the value of an environment variable contributes to the options. +data EnvDescr opts = + EnvVar { evName :: String -- ^ Name of variable + , evDoc :: String -- ^ Documentation + , evValue :: String -> OptSetter opts -- ^ How it affects the options + } + +-- | Lifts an 'EnvDescr' for some smaller type 'b' into an 'EnvDescr' with the +-- same name and documentation, but operating over a larger type 'a'. Useful +-- for embedding the options of another executable within an executable with +-- possibly additional options. +liftEnvDescr :: Lens' a b -> EnvDescr b -> EnvDescr a +liftEnvDescr lens envDescr = + envDescr { evValue = liftOptSetter lens . evValue envDescr } + +-- | Lifts an 'OptDescr' for some smaller type 'b' into an 'OptDescr' with the +-- same name and documentation, but operating over a larger type 'a'. Useful +-- for embedding the options of another executable within an executable with +-- possibly additional options. +liftOptDescr :: Lens' a b -> OptDescr b -> OptDescr a +liftOptDescr lens (Option a b c d) = Option a b c (liftArgDescr lens d) + +liftArgDescr :: Lens' a b -> ArgDescr b -> ArgDescr a +liftArgDescr lens (NoArg s) = NoArg (liftOptSetter lens s) +liftArgDescr lens (ReqArg v s) = ReqArg v (liftOptSetter lens . s) +liftArgDescr lens (OptArg v s) = OptArg v (liftOptSetter lens . s) + +liftOptSetter :: Lens' a b -> OptSetter b -> OptSetter a +liftOptSetter lens v o = flip (set lens) o <$> v (view lens o) + + +cfgJoin :: Config a -> Config b -> Config (a,b) +cfgJoin cfg1 cfg2 = Config + { cfgFile = (,) <$> cfgFile cfg1 <*> cfgFile cfg2 + , cfgEnv = map (mapEnvDescr inFst) (cfgEnv cfg1) ++ + map (mapEnvDescr inSnd) (cfgEnv cfg2) + , cfgCmdLineFlag = map (mapOptDescr inFst) (cfgCmdLineFlag cfg1) ++ + map (mapOptDescr inSnd) (cfgCmdLineFlag cfg2) + } + +inFst :: OptSetter a -> OptSetter (a,b) +inFst f = \(a,b) -> do a' <- f a + pure (a',b) + +inSnd :: OptSetter b -> OptSetter (a,b) +inSnd f = \(a,b) -> do b' <- f b + pure (a,b') + +-------------------------------------------------------------------------------- + + +-- | An option that can be configured in the file. +section :: Text {- ^ Option name -} -> + ValueSpec a {- ^ What type of value we expect -} -> + a {- ^ Default value to use if option not specified -} -> + Text {-^ Documentation -} -> + SectionsSpec a +section nm spec def doc = fromMaybe def <$> optSection' nm spec doc + +sectionMaybe :: Text {- ^ Option name -} -> + ValueSpec a {- ^ What type of value we expect -} -> + Text {- ^ Documentation -} -> + SectionsSpec (Maybe a) +sectionMaybe = optSection' + +fileSpec :: ValueSpec FilePath +fileSpec = namedSpec "FILE" stringSpec + +dirSpec :: ValueSpec FilePath +dirSpec = namedSpec "DIR" stringSpec + +-------------------------------------------------------------------------------- + + + +-------------------------------------------------------------------------------- + +mapEnvDescr :: (OptSetter a -> OptSetter b) -> EnvDescr a -> EnvDescr b +mapEnvDescr f e = e { evValue = f . evValue e } + +mapArgDescr :: (OptSetter a -> OptSetter b) -> ArgDescr a -> ArgDescr b +mapArgDescr g ad = + case ad of + NoArg os -> NoArg (g os) + ReqArg s f -> ReqArg s (g . f) + OptArg s f -> OptArg s (g . f) + +mapOptDescr :: (OptSetter a -> OptSetter b) -> OptDescr a -> OptDescr b +mapOptDescr f o = o { optArgument = mapArgDescr f (optArgument o) } + + + + +parsePosNum :: (Read a, Num a, Ord a) => + String -> (a -> opts -> opts) -> String -> OptSetter opts +parsePosNum thing mk = \txt opts -> + case readMaybe txt of + Just a | a >= 0 -> Right (mk a opts) + _ -> Left ("Invalid " ++ thing) diff --git a/src/Crux/Config/Common.hs b/src/Crux/Config/Common.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Config/Common.hs @@ -0,0 +1,561 @@ +{-# 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) diff --git a/src/Crux/Config/Doc.hs b/src/Crux/Config/Doc.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Config/Doc.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Crux.Config.Doc (configDocs) where + +import Config.Schema (sectionsSpec,generateDocs) +import Data.Function ( on ) +import qualified Data.List as L +import Data.Text ( Text ) +import qualified Data.Text as T +import Prettyprinter +import Prettyprinter.Util ( reflow ) +import SimpleGetOpt ( OptSpec(..) ) + +import Crux.Config +import Crux.Config.Load (commandLineOptions) + +configDocs :: Text -> Config opts -> Doc ann +configDocs nm cfg = + vcat [ heading "Command line flags:" + , indent 2 $ cmdLineDocs $ commandLineOptions cfg + , envVarDocs cfg + , heading "Configuration file format:" + , nest 2 (viaShow $ generateDocs (sectionsSpec nm (cfgFile cfg))) + ] + +cmdLineDocs :: OptSpec a -> Doc ann +cmdLineDocs opts = + vcat [ nest 2 $ vcat $ "Parameters:" : ppParams + , mempty + , nest 2 $ vcat $ "Flags:" : ppFlags + ] + where + ppParams = let maxLen = maximum $ (length . fst) <$> progParamDocs opts + in map (ppParam maxLen) $ progParamDocs opts + ppParam l (n,d) = let pad = max 0 $ l - length d + in hcat [ pretty n + , pretty $ T.replicate (pad + 4) " " + , nest 2 $ reflow $ T.pack d ] + ppFlags = let flagset = fmap ppFlag $ L.sortBy (compare `on` optSort) $ progOptions opts + optSort o = (L.sort $ optShortFlags o <> "zzzzz", L.sort $ optLongFlags o) + lengths = fmap (maximum . fmap T.length) $ L.transpose flagset + textLen (l,t) = let f = T.replicate (max 0 $ l - T.length t) " " in t <> f + sizedCols = fmap (fmap textLen . zip lengths) $ flagset + padLast = align . reflow + prettyLine = hcat . fst . foldr (\c (p,g) -> (g c : space : p, pretty)) ([], padLast) + in fmap prettyLine sizedCols + ppFlag :: OptDescr a -> [Text] + ppFlag od = let sfs = if null (optShortFlags od) then "" + else let each = + let f = case optArgument od of + NoArg _ -> T.singleton + ReqArg a _ -> (\c -> T.singleton c <> " " <> T.pack a) + OptArg a _ -> (\c -> T.singleton c <> " [" <> T.pack a <> "]") + in f <$> optShortFlags od + in "-" <> T.intercalate ",-" each + lfs = if null (optLongFlags od) then "" + else let each = + let f = case optArgument od of + NoArg _ -> T.pack + ReqArg a _ -> (\s -> T.pack s <> "=" <> T.pack a) + OptArg a _ -> (\s -> T.pack s <> "=[" <> T.pack a <> "]") + in f <$> optLongFlags od + in "--" <> T.intercalate ",--" each + in [ sfs, lfs, T.pack $ optDescription od ] + + +envVarDocs :: Config a -> Doc ann +envVarDocs cfg + | null vs = mempty + | otherwise = vcat [ heading "Environment variables:" + , indent 2 (vcat (map pp vs)) + ] + where + vs = cfgEnv cfg + m = maximum (map (length . evName) vs) + pp v = pretty (n ++ replicate (1 + m - length n) ' ') <+> (pretty $ evDoc v) + where n = evName v + +heading :: String -> Doc ann +heading x = vcat [ mempty + , pretty x + , pretty (replicate (length x) '=') + , mempty ] diff --git a/src/Crux/Config/Load.hs b/src/Crux/Config/Load.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Config/Load.hs @@ -0,0 +1,195 @@ +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DataKinds #-} +{-# Language DeriveGeneric, MultiWayIf, OverloadedStrings #-} +-- | This module deals with loading configurations. +module Crux.Config.Load where + + +import Control.Lens (set) +import Control.Monad(foldM, (<=<)) +import Control.Exception(Exception(..),catch,catches,throwIO, Handler(..)) +import Data.Generics.Product.Fields (field, setField) +import Data.Text (Text) +import GHC.Generics (Generic) + +import System.Environment + +import SimpleGetOpt +import Config +import Config.Schema +import Config.Schema.Load.Error(ErrorAnnotation(..)) + +import Crux.Config + +-- | The result of loading a configuration. +data Options opts = + ShowHelp {- XXX: Add help strings -} -- ^ Show help and exit + | ShowVersion -- ^ Show version and exit + | Options opts [FilePath] -- ^ We loaded some options + + +data ColorOptions = ColorOptions + { noColorsErr :: Bool + , noColorsOut :: Bool + } + deriving (Generic) + +defaultColorOptions :: ColorOptions +defaultColorOptions = allColors + +allColors :: ColorOptions +allColors = ColorOptions + { noColorsErr = False + , noColorsOut = False + } + +noColors :: ColorOptions +noColors = ColorOptions + { noColorsErr = True + , noColorsOut = True + } + + +-- | Command line options processed before loading the configuration file. +data EarlyConfig opts = EarlyConfig + { showHelp :: Bool -- ^ Describe options & quit + , showVersion :: Bool -- ^ Show tool version & quit + , configFile :: Maybe FilePath + -- ^ Load configuratoin from here. + -- Other command line options override the settings in the file. + , colorOptions :: ColorOptions + , options :: OptSetter opts + , files :: [FilePath] + } + deriving (Generic) + + +commandLineOptions :: Config opts -> OptSpec (EarlyConfig opts) +commandLineOptions cfg = OptSpec + { progDefaults = EarlyConfig + { showHelp = False + , showVersion = False + , configFile = Nothing + , colorOptions = defaultColorOptions + , options = Right + , files = [] + } + + , progOptions = + [ Option "h?" ["help"] + "Print this help message" + $ NoArg $ \opts -> Right opts { showHelp = True } + + , Option "V" ["version"] + "Show the version of the tool" + $ NoArg $ \opts -> Right opts { showVersion = True } + + , Option "" ["config"] + "Load configuration from this file." + $ ReqArg "FILE" $ \f opts -> Right opts { configFile = Just f } + + , Option [] ["no-colors-err"] + "Suppress color codes in the errors" + $ NoArg $ Right . set (field @"colorOptions" . field @"noColorsErr") True + + , Option [] ["no-colors-out"] + "Suppress color codes in the output" + $ NoArg $ Right . set (field @"colorOptions" . field @"noColorsOut") True + + , Option [] ["no-colors"] + "Suppress color codes in both the output and the errors" + $ NoArg $ Right . setField @"colorOptions" noColors + + ] ++ map (mapOptDescr delayOpt) (cfgCmdLineFlag cfg) + + , progParamDocs = [("FILES", "Input files to process.")] + , progParams = \f opts -> Right opts { files = f : files opts } + } + + +delayOpt :: OptSetter opts -> OptSetter (EarlyConfig opts) +delayOpt f opts = Right opts { options = f <=< options opts } + + + +data ConfigFileLoc = + NoConfgFile + | AtPosition Position + deriving Show + +instance ErrorAnnotation ConfigFileLoc where + displayAnnotation a = + case a of + NoConfgFile -> "(no configuration file)" + AtPosition p -> displayAnnotation p + +data ConfigError = + FailedToReadFile IOError + | FailedToParseFile ParseError + | FailedToProcessFile (ValueSpecMismatch ConfigFileLoc) + | InvalidEnvVar String String String -- ^ variable, value, error message + | InvalidCommandLine [String] + deriving Show + +instance Exception ConfigError where + displayException = ppConfigError + +ppConfigError :: ConfigError -> String +ppConfigError (FailedToReadFile ioe) = + "Failed to read config file: " ++ displayException ioe +ppConfigError (FailedToParseFile pe) = + "Failed to parse config file: " ++ displayException pe +ppConfigError (FailedToProcessFile vsm) = + "Failed to check config file: " ++ displayException vsm +ppConfigError (InvalidEnvVar var val msg) = + unwords ["Environment variable", var, "has invalid value", val ++ ":", msg] +ppConfigError (InvalidCommandLine msg) = + unlines ("Invalid command line option:" : msg) + +-- | Merges command-line options, environment variable options, and +-- configuration file options (in that order) to get the overall +-- Options configuration for running Crux. Throws 'ConfigError' on +-- failure. +loadConfig :: Text -> Config opts -> IO (ColorOptions, Options opts) +loadConfig nm cfg = + do earlyOpts <- getOptsX (commandLineOptions cfg) `catch` + \(GetOptException errs) -> throwIO (InvalidCommandLine errs) + let copts = colorOptions earlyOpts + if | showHelp earlyOpts -> pure (copts, ShowHelp) + | showVersion earlyOpts -> pure (copts, ShowVersion) + | otherwise -> + do opts <- fromFile nm cfg (configFile earlyOpts) + opts1 <- foldM fromEnv opts (cfgEnv cfg) + case options earlyOpts opts1 of + Left err -> throwIO (InvalidCommandLine [err]) + Right opts2 -> pure (copts, Options opts2 (reverse (files earlyOpts))) + + +-- | Load settings from a file, or from an empty configuration value. +fromFile :: Text -> Config opts -> Maybe FilePath -> IO opts +fromFile nm cfg mbFile = + do let spec = sectionsSpec nm (cfgFile cfg) + case mbFile of + + Nothing -> -- no file, use an empty value + case loadValue spec (Sections NoConfgFile []) of + Left err -> throwIO (FailedToProcessFile err) + Right opts -> pure opts + + Just file -> + loadValueFromFile spec file + `catches` [ Handler (throwIO . FailedToReadFile) + , Handler (throwIO . FailedToParseFile) + , Handler (throwIO . FailedToProcessFile) + ] + + +-- | Modify the options using an environment variable. +fromEnv :: opts -> EnvDescr opts -> IO opts +fromEnv opts v = + do mb <- lookupEnv (evName v) + case mb of + Just s -> case evValue v s opts of + Right opts1 -> pure opts1 + Left err -> throwIO (InvalidEnvVar (evName v) s err) + Nothing -> pure opts diff --git a/src/Crux/Config/Solver.hs b/src/Crux/Config/Solver.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Config/Solver.hs @@ -0,0 +1,220 @@ +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} +module Crux.Config.Solver ( + parseSolverConfig, + SolverConfig(..), + SolverOnline(..), + SolverOffline(..), + HasDefaultFloatRepr(..), + sameSolver + ) where + +import Control.Applicative ( (<|>), empty, Alternative ) +import Data.List.Split (wordsBy) +import qualified Data.Foldable as F +import qualified Data.Traversable as T +import Text.Printf ( printf ) +import qualified What4.Expr.Builder as WEB +import qualified What4.InterpretedFloatingPoint as WIF + +import qualified Crux.Config.Common as CCC + +data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP + deriving (Eq, Ord, Show) +data SolverOffline = SolverOnline SolverOnline | Boolector | DReal + deriving (Eq, Ord, Show) + +class HasDefaultFloatRepr solver where + withDefaultFloatRepr :: + st s -> + solver -> + (forall fm. (WIF.IsInterpretedFloatExprBuilder (WEB.ExprBuilder s st (WEB.Flags fm))) => WEB.FloatModeRepr fm -> a) -> + a + +instance HasDefaultFloatRepr SolverOnline where + withDefaultFloatRepr _ s k = + case s of + CVC4 -> k WEB.FloatRealRepr + CVC5 -> k WEB.FloatRealRepr + STP -> k WEB.FloatRealRepr + Yices -> k WEB.FloatRealRepr + Z3 -> k WEB.FloatIEEERepr + +instance HasDefaultFloatRepr SolverOffline where + withDefaultFloatRepr st s k = + case s of + SolverOnline s' -> withDefaultFloatRepr st s' k + Boolector -> k WEB.FloatUninterpretedRepr + DReal -> k WEB.FloatRealRepr + +-- | Test to see if an online and offline solver are actually the same +sameSolver :: SolverOnline -> SolverOffline -> Bool +sameSolver o f = + case f of + SolverOnline s' -> o == s' + _ -> False + +data SolverConfig = SingleOnlineSolver SolverOnline + -- ^ Use a single online solver for both path satisfiability + -- checking and goal discharge + + | OnlineSolverWithOfflineGoals SolverOnline SolverOffline + -- ^ Use an online solver for path satisfiability checking and + -- use an offline solver for goal discharge + + | OnlineSolverWithSeparateOnlineGoals SolverOnline SolverOnline + -- ^ Use one online solver connection for path satisfiability + -- checking and a separate online solver connection for goal + -- discharge. INVARIANT: the solvers must be distinct. + + | OnlyOfflineSolvers [SolverOffline] + -- ^ Try any of a number of offline solvers with no support + -- for path satisfiability checking + +-- | A type that contains a validated instance of a value or a list of messages +-- describing why it was not valid +-- +-- This is basically `Either [String] a` but with instances that accumulate +-- error messages across alternatives unless there is a success. +data Validated a = Invalid [String] | Validated a + deriving (Show, Functor, F.Foldable, T.Traversable) + +validatedToEither :: Validated a -> Either [String] a +validatedToEither v = + case v of + Invalid rsns -> Left rsns + Validated a -> Right a + +instance Applicative Validated where + pure = Validated + Validated f <*> Validated a = Validated (f a) + Validated _f <*> Invalid rsns = Invalid rsns + Invalid rsns1 <*> Invalid rsns2 = Invalid (rsns1 <> rsns2) + Invalid rsns <*> Validated _ = Invalid rsns + +instance Alternative Validated where + empty = Invalid [] + Validated a <|> _ = Validated a + Invalid rsns1 <|> Invalid rsns2 = Invalid (rsns1 <> rsns2) + Invalid _ <|> Validated a = Validated a + +invalid :: String -> Validated a +invalid rsn = Invalid [rsn] + +-- | Boolector and DReal only support offline solving (for our purposes), so +-- attempt to parse them from the given string +asOnlyOfflineSolver :: String -> Validated SolverOffline +asOnlyOfflineSolver s = + case s of + "dreal" -> pure DReal + "boolector" -> pure Boolector + _ -> invalid (printf "%s is not an offline-only solver (expected dreal or boolector)" s) + +-- | Solvers that can be used in offline mode +asAnyOfflineSolver :: String -> Validated SolverOffline +asAnyOfflineSolver s = case s of + "dreal" -> pure DReal + "boolector" -> pure Boolector + "z3" -> pure (SolverOnline Z3) + "yices" -> pure (SolverOnline Yices) + "cvc4" -> pure (SolverOnline CVC4) + "cvc5" -> pure (SolverOnline CVC5) + "stp" -> pure (SolverOnline STP) + _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, or stp)" s) + +asManyOfflineSolvers :: String -> Validated [SolverOffline] +asManyOfflineSolvers s + | s == "all" = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp" + | length solvers > 1 = traverse asAnyOfflineSolver solvers + | otherwise = invalid (printf "%s is not a valid solver list (expected 'all' or a comma separated list of solvers)" s) + where + solvers = wordsBy (== ',') s + +-- | Attempt to parse the string as one of our solvers that supports online mode +asOnlineSolver :: String -> Validated SolverOnline +asOnlineSolver s = + case s of + "yices" -> pure Yices + "cvc4" -> pure CVC4 + "cvc5" -> pure CVC5 + "z3" -> pure Z3 + "stp" -> pure STP + _ -> invalid (printf "%s is not a valid online solver (expected yices, cvc4, cvc5, z3, or stp)" s) + +-- | Examine a 'CCC.CruxOptions' and determine what solver configuration to use for +-- symbolic execution. This can fail if an invalid solver configuration is +-- requested by the user. +-- +-- The high level logic is that: +-- +-- * If a user specifies only a single solver with the --solver option, that is +-- used as an online solver if possible for path sat checking (if requested) +-- and goal discharge. +-- * If the user specifies an explicit --path-sat-solver, that solver is used +-- for path satisfiability checking (if requested) while the solver specified +-- with --solver is used for goal discharge. +-- * The goal solver can be entirely offline (if it doesn't support online +-- mode) or if the user requests that it be used in offline mode with the +-- --force-offline-goal-solving option. +parseSolverConfig :: CCC.CruxOptions -> Either [String] SolverConfig +parseSolverConfig cruxOpts = validatedToEither $ + case (CCC.pathSatSolver cruxOpts, CCC.checkPathSat cruxOpts, CCC.forceOfflineGoalSolving cruxOpts) of + (Nothing, True, False) -> + -- No separate path sat checker was requested, but we do have to check + -- path satisfiability. That means that we have to use the one solver + -- specified and it must be one that supports online solving + trySingleOnline + (Nothing, True, True) -> + -- The user requested path satisfiability checking (using an online + -- solver), but also wants to force goals to be discharged using the same + -- solver in offline mode. + OnlineSolverWithOfflineGoals <$> asOnlineSolver (CCC.solver cruxOpts) <*> asAnyOfflineSolver (CCC.solver cruxOpts) + (Just _, False, False) -> + -- The user specified a separate path sat checking solver, but did not + -- request path satisfiability checking; we'll treat that as not asking + -- for path satisfiability checking and just use a single online solver + tryOnlyOffline <|> trySingleOnline + (Just _, False, True) -> + -- The user requested a separate path sat checking solver, but did not + -- request path satisfiability checking. They also requested that a + -- separate solver be used for each goal (offline mode). We'll use the + -- specified solver as the only solver purely in offline mode. + tryAnyOffline <|> tryManyOffline + (Nothing, False, False) -> + -- This is currently the same as the previous case, but the user + -- explicitly selected no path sat checking + tryOnlyOffline <|> trySingleOnline + (Nothing, False, True) -> + -- This is the same as the `(Just _, False, True)` case since we were just + -- ignoring the unused path sat solver option. + tryAnyOffline <|> tryManyOffline + (Just onSolver, True, False) -> + -- The user requested path sat checking and specified a solver + -- + -- NOTE: We can still use the goal solver in online mode if it is supported + + -- In this case, the user requested a goal solver that is only usable as + -- an offline solver + (OnlineSolverWithOfflineGoals <$> asOnlineSolver onSolver <*> asOnlyOfflineSolver (CCC.solver cruxOpts)) <|> + -- In this case, the requested solver can be used in online mode so we + -- use it as such + (onlineWithOnlineGoals <$> asOnlineSolver onSolver <*> asOnlineSolver (CCC.solver cruxOpts)) + + (Just onSolver, True, True) -> + -- In this case, the user requested separate solvers for path sat checking + -- and goal discharge, but further requested that we force goals to be + -- discharged with an offline solver. + OnlineSolverWithOfflineGoals <$> asOnlineSolver onSolver <*> asAnyOfflineSolver (CCC.solver cruxOpts) + where + tryAnyOffline = OnlyOfflineSolvers . pure <$> asAnyOfflineSolver (CCC.solver cruxOpts) + tryOnlyOffline = OnlyOfflineSolvers . pure <$> asOnlyOfflineSolver (CCC.solver cruxOpts) + trySingleOnline = SingleOnlineSolver <$> asOnlineSolver (CCC.solver cruxOpts) + tryManyOffline = OnlyOfflineSolvers <$> asManyOfflineSolvers (CCC.solver cruxOpts) + + onlineWithOnlineGoals s1 s2 + | s1 == s2 = SingleOnlineSolver s1 + | otherwise = OnlineSolverWithSeparateOnlineGoals s1 s2 diff --git a/src/Crux/FormatOut.hs b/src/Crux/FormatOut.hs new file mode 100644 --- /dev/null +++ b/src/Crux/FormatOut.hs @@ -0,0 +1,122 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE OverloadedStrings #-} +-- | This module provides various default formatters for outputting +-- information in human readable form. Alternative versions should be +-- used where appropriate. + +module Crux.FormatOut + ( + sayWhatResultStatus + , sayWhatFailedGoals + ) +where + +import qualified Data.BitVector.Sized as BV +import Data.Foldable ( toList ) +import Data.Sequence (Seq) +import qualified Data.Text as Text (Text) +import Prettyprinter ( (<+>) ) +import qualified Prettyprinter as PP +import qualified Prettyprinter.Render.Text as PPR + +import What4.Expr (GroundValueWrapper(..), GroundValue) +import What4.BaseTypes +import What4.ProgramLoc + +import Lang.Crucible.Backend (CrucibleEvent(..)) +import qualified Lang.Crucible.Simulator.SimError as CSE + +import Crux.Types + +sayWhatResultStatus :: CruxSimulationResult -> SayWhat +sayWhatResultStatus (CruxSimulationResult cmpl gls) = + let tot = sum (totalProcessedGoals . fst <$> gls) + proved = sum (provedGoals . fst <$> gls) + disproved = sum (disprovedGoals . fst <$> gls) + incomplete = sum (incompleteGoals . fst <$> gls) + unknown = tot - (proved + disproved + incomplete) + goalSummary = if tot == 0 then + "All goals discharged through internal simplification." + else + PP.nest 2 $ + PP.vcat [ "Goal status:" + , "Total:" <+> PP.pretty tot + , "Proved:" <+> PP.pretty proved + , "Disproved:" <+> PP.pretty disproved + , "Incomplete:" <+> PP.pretty incomplete + , "Unknown:" <+> PP.pretty unknown + ] + in SayMore + (SayWhat Simply "Crux" $ ppToText goalSummary) + $ if | disproved > 0 -> + SayWhat Fail "Crux" "Overall status: Invalid." + | incomplete > 0 || cmpl == ProgramIncomplete -> + SayWhat Warn "Crux" "Overall status: Unknown (incomplete)." + | unknown > 0 -> SayWhat Warn "Crux" "Overall status: Unknown." + | proved == tot -> SayWhat OK "Crux" "Overall status: Valid." + | otherwise -> + SayWhat Fail "Crux" "Internal error computing overall status." + +sayWhatFailedGoals :: Bool -> Bool -> Seq ProvedGoals -> SayWhat +sayWhatFailedGoals skipIncompl showVars allGls = + if null allDocs + then SayNothing + else SayWhat Fail "Crux" $ ppToText $ PP.vsep allDocs + where + failedDoc = \case + Branch gls1 gls2 -> failedDoc gls1 <> failedDoc gls2 + ProvedGoal{} -> [] + NotProvedGoal _asmps err ex _locs mdl s -> + if | skipIncompl, CSE.SimError _ (CSE.ResourceExhausted _) <- err -> [] + | Just (_m,evs) <- mdl -> + [ PP.nest 2 $ PP.vcat ( + [ "Found counterexample for verification goal" + -- n.b. prefer the prepared pretty explanation, but + -- if not available, use the NotProved information. + -- Don't show both: they tend to be duplications. + , if null (show ex) then PP.viaShow err else ex + ] -- if `showVars` is set, print the sequence of symbolic + -- variable events that led to this failure + ++ if showVars then + ["Symbolic variables:", PP.indent 2 (PP.vcat (ppVars evs))] + else [] + -- print abducts, if any + ++ if s /= [] then + let numFacts = length s + -- NB: If you update the contents of this error + -- message, make sure to update the corresponding + -- regexes that check for this in + -- crux-llvm/test/Test.hs. + herald = PP.plural + "The following fact" + ("One of the following" + PP.<+> PP.viaShow numFacts + PP.<+> "facts") + numFacts PP.<+> "would entail the goal" in + herald : (map (\x -> PP.pretty ('*' : ' ' : x)) s) + else [])] + | otherwise -> + [ PP.nest 2 $ PP.vcat [ "Failed to prove verification goal", ex ] ] + + ppVars evs = + do CreateVariableEvent loc nm tpr (GVW v) <- evs + pure (ppVarEvent loc nm tpr v) + + ppVarEvent loc nm tpr v = + PP.pretty nm PP.<+> "=" PP.<+> ppVal tpr v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc) + + ppVal :: BaseTypeRepr tp -> GroundValue tp -> PP.Doc ann + ppVal tpr v = case tpr of + BaseBVRepr _w -> PP.viaShow (BV.asUnsigned v) + BaseFloatRepr _fpp -> PP.viaShow v + BaseRealRepr -> PP.viaShow v + _ -> "" PP.<+> PP.viaShow tpr + + allDocs = mconcat (failedDoc <$> toList allGls) + + + +ppToText :: PP.Doc ann -> Text.Text +ppToText = PPR.renderStrict . PP.layoutPretty PP.defaultLayoutOptions diff --git a/src/Crux/Goal.hs b/src/Crux/Goal.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Goal.hs @@ -0,0 +1,564 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# Language ImplicitParams #-} +{-# Language MultiWayIf #-} +{-# Language PatternSynonyms #-} +{-# Language ScopedTypeVariables #-} +{-# Language TypeFamilies #-} +{-# Language TypeOperators #-} +{-# Language ViewPatterns #-} + +module Crux.Goal where + +import Control.Concurrent.Async (async, asyncThreadId, waitAnyCatch) +import Control.Exception (throwTo, SomeException, displayException) +import Control.Lens ((^.), view) + +import Control.Monad (forM, forM_, unless, when) +import Data.Either (partitionEithers) +import Data.IORef +import Data.Maybe (fromMaybe) +import qualified Data.Map as Map +import qualified Data.Parameterized.Map as MapF +import qualified Data.Text as Text +import Data.Void +import Prettyprinter +import System.Exit (ExitCode(ExitSuccess)) +import System.FilePath ((<.>), splitExtension) +import System.IO (Handle, IOMode(..), withFile) +import qualified System.Timeout as ST + +import What4.Interface (notPred, getConfiguration, IsExprBuilder) +import What4.Config (setOpt, getOptionSetting, Opt, ConfigOption) +import What4.ProgramLoc (ProgramLoc) +import What4.SatResult(SatResult(..)) +import What4.Expr (ExprBuilder, GroundEvalFn(..), BoolExpr, GroundValueWrapper(..)) +import What4.Protocol.Online( OnlineSolver, SolverProcess, inNewFrame, inNewFrame2Open + , inNewFrame2Close, solverEvalFuns, solverConn + , check, getUnsatCore, getAbducts ) +import What4.Protocol.SMTWriter( SMTReadWriter, mkFormula, assumeFormulaWithFreshName + , assumeFormula, smtExprGroundEvalFn ) +import qualified What4.Solver as WS +import Lang.Crucible.Backend +import Lang.Crucible.Backend.Online + ( OnlineBackend, withSolverProcess, enableOnlineBackend, solverInteractionFile ) +import Lang.Crucible.Simulator.SimError + ( SimError(..), SimErrorReason(..) ) +import Lang.Crucible.Simulator.ExecutionTree + (ctxSymInterface) +import Lang.Crucible.Panic (panic) + +import Crux.Types +import Crux.Model +import Crux.Log as Log +import Crux.Config.Common +import Crux.ProgressBar + + +symCfg :: (IsExprBuilder sym, Opt t a) => sym -> ConfigOption t -> a -> IO () +symCfg sym x y = + do opt <- getOptionSetting x (getConfiguration sym) + _ <- setOpt opt y + pure () + + +-- | Simplify the proved goals. +provedGoalsTree :: forall sym. + ( IsSymInterface sym + ) => + sym -> + Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)) -> + IO (Maybe ProvedGoals) +provedGoalsTree sym = traverse (go mempty) + where + go :: Assumptions sym -> + Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym) -> + IO ProvedGoals + go asmps gs = + case gs of + Assuming as gs1 -> go (asmps <> as) gs1 + Prove (p,locs,r) -> proveToGoal sym asmps p locs r + ProveConj g1 g2 -> Branch <$> go asmps g1 <*> go asmps g2 + +proveToGoal :: + (IsSymInterface sym) => + sym -> + Assumptions sym -> + Assertion sym -> + [ProgramLoc] -> + ProofResult sym -> + IO ProvedGoals +proveToGoal sym allAsmps p locs pr = + case pr of + NotProved ex cex s -> + do as <- flattenAssumptions sym allAsmps + return (NotProvedGoal (map showAsmp as) (showGoal p) ex locs cex s) + Proved xs -> + case partitionEithers xs of + (asmps, []) -> return (ProvedGoal (map showAsmp asmps) (showGoal p) locs True) + (asmps, _:_) -> return (ProvedGoal (map showAsmp asmps) (showGoal p) locs False) + + where + showAsmp x = forgetAssumption x + showGoal x = x^.labeledPredMsg + + +countGoals :: Goals a b -> Int +countGoals gs = + case gs of + Assuming _ gs1 -> countGoals gs1 + Prove _ -> 1 + ProveConj g1 g2 -> countGoals g1 + countGoals g2 + +isResourceExhausted :: LabeledPred p SimError -> Bool +isResourceExhausted (view labeledPredMsg -> SimError _ (ResourceExhausted _)) = True +isResourceExhausted _ = False + +updateProcessedGoals :: + LabeledPred p SimError -> + ProofResult a -> + ProcessedGoals -> + ProcessedGoals +updateProcessedGoals _ (Proved _) pgs = + pgs{ totalProcessedGoals = 1 + totalProcessedGoals pgs + , provedGoals = 1 + provedGoals pgs + } + +updateProcessedGoals res (NotProved _ _ _) pgs | isResourceExhausted res = + pgs{ totalProcessedGoals = 1 + totalProcessedGoals pgs + , incompleteGoals = 1 + incompleteGoals pgs + } + +updateProcessedGoals _ (NotProved _ (Just _) _) pgs = + pgs{ totalProcessedGoals = 1 + totalProcessedGoals pgs + , disprovedGoals = 1 + disprovedGoals pgs + } + +updateProcessedGoals _ (NotProved _ Nothing _) pgs = + pgs{ totalProcessedGoals = 1 + totalProcessedGoals pgs } + +-- | A function that can be used to generate a pretty explanation of a +-- simulation error. + +type Explainer sym t ann = Maybe (GroundEvalFn t) + -> LPred sym SimError + -> IO (Doc ann) + +type ProverCallback sym = + forall ext personality t st fs. + (sym ~ ExprBuilder t st fs) => + CruxOptions -> + SimCtxt personality sym ext -> + Explainer sym t Void -> + Maybe (Goals (Assumptions sym) (Assertion sym)) -> + IO (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) + +-- | Discharge a tree of proof obligations ('Goals') by using a non-online solver +-- +-- This function traverses the 'Goals' tree while keeping track of a collection +-- of assumptions in scope for each goal. For each proof goal encountered in +-- the tree, it creates a fresh solver connection using the provided solver +-- adapter. +-- +-- This is in contrast to 'proveGoalsOnline', which uses an online solver +-- connection with scoped assumption frames. This function allows using a wider +-- variety of solvers (i.e., ones that don't have support for online solving) +-- and would in principle enable parallel goal evaluation (though the tree +-- structure makes that a bit trickier, it isn't too hard). +-- +-- Note that this function uses the same symbolic backend ('ExprBuilder') as the +-- symbolic execution phase, which should not be a problem. +proveGoalsOffline :: forall st sym p t fs personality msgs. + ( sym ~ ExprBuilder t st fs + , Logs msgs + , SupportsCruxLogMessage msgs + ) => + [WS.SolverAdapter st] -> + CruxOptions -> + SimCtxt personality sym p -> + (Maybe (GroundEvalFn t) -> Assertion sym -> IO (Doc Void)) -> + Maybe (Goals (Assumptions sym) (Assertion sym)) -> + IO (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) +proveGoalsOffline _adapter _opts _ctx _explainFailure Nothing = return (ProcessedGoals 0 0 0 0, Nothing) +proveGoalsOffline adapters opts ctx explainFailure (Just gs0) = do + goalNum <- newIORef (ProcessedGoals 0 0 0 0) + (start,end,finish) <- proverMilestoneCallbacks gs0 + gs <- go (start,end) goalNum mempty gs0 + nms <- readIORef goalNum + finish + return (nms, Just gs) + + where + sym = ctx^.ctxSymInterface + + failfast = proofGoalsFailFast opts + + go :: SupportsCruxLogMessage msgs + => (ProverMilestoneStartGoal, ProverMilestoneEndGoal) + -> IORef ProcessedGoals + -> Assumptions sym + -> Goals (Assumptions sym) (Assertion sym) + -> IO (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)) + go (start,end) goalNum assumptionsInScope gs = + case gs of + Assuming ps gs1 -> do + res <- go (start,end) goalNum (assumptionsInScope <> ps) gs1 + return (Assuming ps res) + + ProveConj g1 g2 -> do + g1' <- go (start,end) goalNum assumptionsInScope g1 + numDisproved <- disprovedGoals <$> readIORef goalNum + if failfast && numDisproved > 0 + then return g1' + else ProveConj g1' <$> go (start,end) goalNum assumptionsInScope g2 + + Prove p -> do + goalNumber <- totalProcessedGoals <$> readIORef goalNum + start goalNumber + + -- Conjoin all of the in-scope assumptions, the goal, then negate and + -- check sat with the adapter + assumptions <- assumptionsPred sym assumptionsInScope + goal <- notPred sym (p ^. labeledPred) + + res <- dispatchSolversOnGoalAsync (goalTimeout opts) adapters + (runOneSolver p assumptionsInScope assumptions goal goalNumber) + end goalNumber + case res of + Right Nothing -> do + let details = NotProved "(timeout)" Nothing [] + let locs = assumptionsTopLevelLocs assumptionsInScope + modifyIORef' goalNum (updateProcessedGoals p details) + return (Prove (p, locs, details)) + + Right (Just (locs,details)) -> do + modifyIORef' goalNum (updateProcessedGoals p details) + case details of + NotProved _ (Just _) _ -> + when (failfast && not (isResourceExhausted p)) $ + sayCrux Log.FoundCounterExample + _ -> return () + return (Prove (p, locs, details)) + Left es -> do + modifyIORef' goalNum (updateProcessedGoals p (NotProved mempty Nothing [])) + let allExceptions = unlines (displayException <$> es) + fail allExceptions + + runOneSolver :: Assertion sym + -> Assumptions sym + -> BoolExpr t + -> BoolExpr t + -> Integer + -> WS.SolverAdapter st + -> IO ([ProgramLoc], ProofResult sym) + runOneSolver p assumptionsInScope assumptions goal goalNumber adapter = + -- Create a file to a single offline solver interaction, assuming the user + -- has selected this option. A single Crux session might invoke an offline + -- solver multiple times, so each file has unique suffixes to indicate the + -- goal number and which solver in particular was used to solve the goal. + -- (Recall that a Crux user can choose multiple offline solvers, so it is + -- important to indicate which solver was picked for each goal.) + withMaybeOfflineSolverOutputHandle (offlineSolverOutput opts) $ \mbLogHandle -> + let logData = WS.defaultLogData { WS.logHandle = mbLogHandle } in + WS.solver_adapter_check_sat adapter (ctx ^. ctxSymInterface) logData [assumptions, goal] $ \satRes -> + case satRes of + Unsat _ -> do + -- NOTE: We don't have an easy way to get an unsat core here + -- because we don't have a solver connection. + as <- flattenAssumptions sym assumptionsInScope + let core = fmap Left as ++ [ Right p ] + let locs = assumptionsTopLevelLocs assumptionsInScope + return (locs, Proved core) + Sat (evalFn, _) -> do + evs <- concretizeEvents (groundEval evalFn) assumptionsInScope + let vals = evalModelFromEvents evs + explain <- explainFailure (Just evalFn) p + let locs = map eventLoc evs + return (locs, NotProved explain (Just (vals,evs)) []) + Unknown -> do + explain <- explainFailure Nothing p + let locs = assumptionsTopLevelLocs assumptionsInScope + return (locs, NotProved explain Nothing []) + where + -- Create a handle for a file based on the template. For instance, if + -- the template is @solver-output.smt2@, then create a file named + -- @solver-output--.smt2@. + withOfflineSolverOutputHandle :: FilePath -> (Handle -> IO r) -> IO r + withOfflineSolverOutputHandle template k = + let (templateName, templateExt) = splitExtension template + fileName = templateName ++ "-" ++ show goalNumber + ++ "-" ++ WS.solver_adapter_name adapter + <.> templateExt in + withFile fileName WriteMode k + + -- Lift @withOfflineSolverOutputHandle@ to a @Maybe FilePath@ argument. + withMaybeOfflineSolverOutputHandle :: + Maybe FilePath -> (Maybe Handle -> IO r) -> IO r + withMaybeOfflineSolverOutputHandle mbTemplate k = + case mbTemplate of + Just template -> withOfflineSolverOutputHandle template (k . Just) + Nothing -> k Nothing + +evalModelFromEvents :: [CrucibleEvent GroundValueWrapper] -> ModelView +evalModelFromEvents evs = ModelView (foldl f (modelVals emptyModelView) evs) + where + f m (CreateVariableEvent loc nm tpr (GVW v)) = MapF.insertWith jn tpr (Vals [Entry nm loc v]) m + f m _ = m + + jn (Vals new) (Vals old) = Vals (old++new) + +dispatchSolversOnGoalAsync :: forall a b s time. + (RealFrac time) + => Maybe time + -> [WS.SolverAdapter s] + -> (WS.SolverAdapter s -> IO (b,ProofResult a)) + -> IO (Either [SomeException] (Maybe (b,ProofResult a))) +dispatchSolversOnGoalAsync mtimeoutSeconds adapters withAdapter = do + asyncs <- forM adapters (async . withAdapter) + await asyncs [] + where + await [] es = return $ Left es + await as es = do + mresult <- withTimeout $ waitAnyCatch as + case mresult of + Just (a, result) -> do + let as' = filter (/= a) as + case result of + Left exc -> + await as' (exc : es) + Right (x, r@(Proved _)) -> do + mapM_ kill as' + return $ Right (Just (x,r)) + Right (x,r@(NotProved _ (Just _) _)) -> do + mapM_ kill as' + return $ Right (Just (x,r)) + Right _ -> + await as' es + Nothing -> do + mapM_ kill as + return $ Right $ Nothing + + withTimeout action + | Just seconds <- mtimeoutSeconds = ST.timeout (round seconds * 1000000) action + | otherwise = Just <$> action + + -- `cancel` from async blocks until the canceled thread has terminated. + kill a = throwTo (asyncThreadId a) ExitSuccess + + +-- | Returns three actions, called respectively when the proving process for a +-- goal is started, when it is ended, and when the final goal is solved. These +-- handlers should handle all necessary output / notifications to external +-- observers, based on the run options. +proverMilestoneCallbacks :: + Log.Logs msgs => + Log.SupportsCruxLogMessage msgs => + Goals asmp ast -> IO ProverMilestoneCallbacks +proverMilestoneCallbacks goals = do + (start, end, finish) <- + if view quiet ?outputConfig then + return silentProverMilestoneCallbacks + else + prepStatus "Checking: " (countGoals goals) + return + ( start <> sayCrux . Log.StartedGoal + , end <> sayCrux . Log.EndedGoal + , finish + ) + + +-- | Prove a collection of goals. The result is a goal tree, where +-- each goal is annotated with the outcome of the proof. +-- +-- NOTE: This function takes an explicit symbolic backend as an argument, even +-- though the symbolic backend used for symbolic execution is available in the +-- 'SimCtxt'. We do that so that we can use separate solvers for path +-- satisfiability checking and goal discharge. +proveGoalsOnline :: + forall sym personality p msgs goalSolver s st fs. + ( sym ~ ExprBuilder s st fs + , OnlineSolver goalSolver + , Logs msgs + , SupportsCruxLogMessage msgs + ) => + OnlineBackend goalSolver s st fs -> + CruxOptions -> + SimCtxt personality sym p -> + (Maybe (GroundEvalFn s) -> Assertion sym -> IO (Doc Void)) -> + Maybe (Goals (Assumptions sym) (Assertion sym)) -> + IO (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) +proveGoalsOnline _ _opts _ctxt _explainFailure Nothing = + return (ProcessedGoals 0 0 0 0, Nothing) + +proveGoalsOnline bak opts _ctxt explainFailure (Just gs0) = + do + -- send solver interactions to the correct file + mapM_ (symCfg sym solverInteractionFile) (fmap Text.pack (onlineSolverOutput opts)) + -- initial goal count + goalNum <- newIORef (ProcessedGoals 0 0 0 0) + -- nameMap is a mutable ref to a map from Text to Either (Assumption sym) (Assertion sym) + nameMap <- newIORef Map.empty + when (unsatCores opts && yicesMCSat opts) $ + sayCrux Log.SkippingUnsatCoresBecauseMCSatEnabled + -- callbacks for starting a goal, ending a goal, and finishing all goals + (start,end,finish) <- proverMilestoneCallbacks gs0 + -- make sure online features are enabled + enableOpt <- getOptionSetting enableOnlineBackend (getConfiguration sym) + _ <- setOpt enableOpt True + -- @go@ traverses a proof tree, processing/solving each goal as it traverses it. + -- It also updates goal count and nameMap + res <- withSolverProcess bak (panic "proveGoalsOnline" ["Online solving not enabled!"]) $ \sp -> + inNewFrame sp (go (start,end) sp mempty goalNum gs0 nameMap) + nms <- readIORef goalNum + finish + return (nms, Just res) + + where + sym = backendGetSym bak + + bindName nm p nameMap = modifyIORef nameMap (Map.insert nm p) + + hasUnsatCores = unsatCores opts && not (yicesMCSat opts) + + howManyAbducts = fromMaybe 0 (getNAbducts opts) + + usingAbducts = howManyAbducts > 0 + + failfast = proofGoalsFailFast opts + + go (start,end) sp assumptionsInScope gn gs nameMap = do + -- traverse goal tree + case gs of + -- case: assumption in context for all the contained goals + Assuming asms gs1 -> + do ps <- flattenAssumptions sym asms + forM_ ps $ \asm -> + unless (trivialAssumption asm) $ + -- extract predicate from assumption + do let p = assumptionPred asm + -- create formula, assert to SMT solver, create new name and add to nameMap + nm <- doAssume =<< mkFormula conn p + bindName nm (Left asm) nameMap + -- recursive call + res <- go (start,end) sp (assumptionsInScope <> asms) gn gs1 nameMap + return (Assuming (mconcat (map singleAssumption ps)) res) + -- case: proof obligation in the context of all previously-made assumptions + Prove p -> + -- number of processed goals gives goal number to prove + do goalNumber <- totalProcessedGoals <$> readIORef gn + start goalNumber + -- negate goal, create formula + t <- mkFormula conn =<< notPred sym (p ^. labeledPred) + -- assert formula to SMT solver, create new name and add to nameMap. + -- This is done in a new assertion frame if abduction is turned on since + -- this assertion would need to be removed before asking for abducts + let inNewFrame2ForAbducts = + if usingAbducts then inNewFrame2 sp else id + ret <- inNewFrame2ForAbducts $ do + nm <- doAssume t + bindName nm (Right p) nameMap + -- check-sat with SMT solver, pattern match on result + res <- check sp "proof" + case res of + Unsat () -> + -- build unsat core, which is the entire assertion set by default + do namemap <- readIORef nameMap + core <- if hasUnsatCores then + map (lookupnm namemap) <$> getUnsatCore sp + -- default unsat core: entire assertion set + else return (Map.elems namemap) + let locs = assumptionsTopLevelLocs assumptionsInScope + return $ UnsatResult core locs + Sat () -> + do -- evaluate counter-example + f <- smtExprGroundEvalFn conn (solverEvalFuns sp) + evs <- concretizeEvents (groundEval f) assumptionsInScope + explain <- explainFailure (Just f) p + return $ SatResult explain evs + Unknown -> + do explain <- explainFailure Nothing p + let locs = assumptionsTopLevelLocs assumptionsInScope + return $ UnknownResult explain locs + end goalNumber + smtResultToGoals p ret + -- case: conjunction of goals + ProveConj g1 g2 -> + do g1' <- inNewFrame sp (go (start,end) sp assumptionsInScope gn g1 nameMap) + -- NB, we don't need 'inNewFrame' here because + -- we don't need to back up to this point again. + if failfast then + do numDisproved <- disprovedGoals <$> readIORef gn + if numDisproved > 0 then + return g1' + else + ProveConj g1' <$> go (start,end) sp assumptionsInScope gn g2 nameMap + else + ProveConj g1' <$> go (start,end) sp assumptionsInScope gn g2 nameMap + + where + conn = solverConn sp + + lookupnm namemap x = + fromMaybe (error $ "Named predicate " ++ show x ++ " not found!") + (Map.lookup x namemap) + + doAssume formula = do + namemap <- readIORef nameMap + if hasUnsatCores + then assumeFormulaWithFreshName conn formula + else assumeFormula conn formula >> return (Text.pack ("x" ++ show (Map.size namemap))) + + -- Convert an 'SMTResult' to a 'ProofResult'. This function should be + -- called /after/ 'inNewFrame2' so that the abducts can be queried properly + -- in the SatResult case. + smtResultToGoals :: LabeledPred (BoolExpr s) SimError + -> SMTResult sym + -> IO ( Goals asmp (LabeledPred (BoolExpr s) SimError + , [ProgramLoc] + , ProofResult sym) + ) + smtResultToGoals p smtRes = do + (locs, gt) <- case smtRes of + UnsatResult core locs -> do + let pr = Proved core + return (locs, pr) + SatResult explain evs -> do + let vals = evalModelFromEvents evs + abds <- if usingAbducts then + getAbducts sp (fromIntegral howManyAbducts) "abd" (p ^. labeledPred) + else + return [] + let gt = NotProved explain (Just (vals,evs)) abds + when (failfast && not (isResourceExhausted p)) $ + sayCrux Log.FoundCounterExample + let locs = map eventLoc evs + return (locs, gt) + UnknownResult explain locs -> do + let gt = NotProved explain Nothing [] + return (locs, gt) + + -- update goal count + modifyIORef' gn (updateProcessedGoals p gt) + return (Prove (p, locs, gt)) + +-- | Like 'inNewFrame', but specifically for frame @2@. This is used for the +-- purpose of generating abducts. + +-- TODO: Upstream this to @what4@ (Issue what4#218). +inNewFrame2 :: SMTReadWriter solver => SolverProcess scope solver -> IO a -> IO a +inNewFrame2 sp action = do + inNewFrame2Open sp + val <- action + inNewFrame2Close sp + return val + +-- | An intermediate data structure used in 'proveGoalsOnline'. This can be +-- thought of as a halfway point between a 'SatResult' and a 'ProofResult'. +data SMTResult sym + = UnsatResult [Either (Assumption sym) (Assertion sym)] + [ProgramLoc] + | SatResult (Doc Void) + [CrucibleEvent GroundValueWrapper] + | UnknownResult (Doc Void) + [ProgramLoc] diff --git a/src/Crux/Log.hs b/src/Crux/Log.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Log.hs @@ -0,0 +1,363 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module Crux.Log ( + -- * Output Configuration + Logs, + OutputConfig(..) + , outputHandle + , quiet + -- * Standard output API functions + , CruxLogMessage(..) + , LogDoc(..) + , LogProofObligation(..) + , SayWhat(..) + , SayLevel(..) + , SupportsCruxLogMessage + , cruxLogMessageToSayWhat + , cruxLogTag + , logException + , logGoal + , logSimResult + , say + , sayCrux + , withCruxLogMessage + -- * Low-level output API functions + , output + , outputLn + -- * Converting and emitting output + , logToStd + ) where + +import Control.Exception ( SomeException, bracket_, ) +import Control.Lens ( Getter, view ) +import qualified Data.Aeson as JSON +import Data.Aeson.TH ( deriveToJSON ) +import qualified Data.Text as T +import Data.Text.IO as TIO ( hPutStr, hPutStrLn ) +import Data.Version ( Version, showVersion ) +import Data.Word ( Word64 ) +import GHC.Generics ( Generic ) +import qualified Lumberjack as LJ +import Prettyprinter ( SimpleDocStream ) +import Prettyprinter.Render.Text ( renderStrict ) +import System.Console.ANSI + ( Color(..), ColorIntensity(..), ConsoleIntensity(..), ConsoleLayer(..) + , SGR(..), hSetSGR ) +import System.IO ( Handle, hPutStr, hPutStrLn ) + +import Crux.Types + ( CruxSimulationResult, ProvedGoals, SayLevel(..), SayWhat(..) ) +import Crux.Version ( version ) +import Lang.Crucible.Backend ( ProofGoal(..), ProofObligation ) +import What4.Expr.Builder ( ExprBuilder ) +import What4.LabeledPred ( labeledPred, labeledPredMsg ) + +---------------------------------------------------------------------- +-- Various functions used by the main code to generate logging output + +newtype LogDoc = LogDoc (SimpleDocStream ()) + +instance JSON.ToJSON LogDoc where + toJSON (LogDoc doc) = JSON.String (renderStrict doc) + +-- | A version of 'ProofObligation' that supports a 'ToJSON' instance. +data LogProofObligation = + forall t st fs. + LogProofObligation (ProofObligation (ExprBuilder t st fs)) + +instance JSON.ToJSON LogProofObligation where + -- for now, we only need the goal in the IDE + toJSON (LogProofObligation g) = + let + goal = proofGoal g + in + JSON.object [ "labeledPred" JSON..= show (view labeledPred goal) + , "labeledPredMsg" JSON..= show (view labeledPredMsg goal) + ] + +-- | All messages that Crux wants to output should be listed here. +-- +-- Messages ought to be serializable to JSON so that they have a somewhat +-- portable machine-readable representation. Some tools may rely on the +-- serialization format, so be sure to check with consumers before changing the +-- 'ToJSON' instance. +-- +-- Other crux-based tools are encouraged to create their own: +-- +-- * log message datatype 'LogMessage', similar to 'CruxLogMessage' below, +-- +-- * constraint synonym 'SupportsLogMessage' similar to +-- 'SupportsCruxLogMessage' below, +-- +-- * constraint dispatcher 'withLogMessage' similar to +-- 'withCruxLogMessage' below, +-- +-- * logger method 'say' similar to 'sayCrux' below, +-- +-- * default log message converter 'LogMessageToSayWhat' similar to +-- 'cruxLogMessageToSayWhat'. +-- +-- The default log message converter can be used to decide how messages are +-- displayed to the standard output for a human consumer. Automated tools may +-- prefer to filter and encode log messages in some machine-readable format and +-- exchange it over a separate channel. +data CruxLogMessage + = AttemptingProvingVCs + | Checking [FilePath] + | DisablingBranchCoverageRequiresPathSatisfiability + | DisablingProfilingIncompatibleWithPathSplitting + | EndedGoal Integer + | FoundCounterExample + | Help LogDoc + | PathsUnexplored Int + | ProofObligations [LogProofObligation] + | SimulationComplete + | SimulationTimedOut + | SkippingUnsatCoresBecauseMCSatEnabled + | StartedGoal Integer + | TotalPathsExplored Word64 + | UnsupportedTimeoutFor String -- ^ name of the backend + | Version T.Text Version + deriving (Generic) + +$(deriveToJSON JSON.defaultOptions ''CruxLogMessage) + + +type SupportsCruxLogMessage msgs = + ( ?injectCruxLogMessage :: CruxLogMessage -> msgs ) + +withCruxLogMessage :: + (SupportsCruxLogMessage CruxLogMessage => a) -> a +withCruxLogMessage a = + let ?injectCruxLogMessage = id in a + + +cruxLogTag :: T.Text +cruxLogTag = "Crux" + + +cruxNoisily :: T.Text -> SayWhat +cruxNoisily = SayWhat Noisily cruxLogTag + +cruxOK :: T.Text -> SayWhat +cruxOK = SayWhat OK cruxLogTag + +cruxSimply :: T.Text -> SayWhat +cruxSimply = SayWhat Simply cruxLogTag + +cruxWarn :: T.Text -> SayWhat +cruxWarn = SayWhat Warn cruxLogTag + + +cruxLogMessageToSayWhat :: CruxLogMessage -> SayWhat + +cruxLogMessageToSayWhat AttemptingProvingVCs = + cruxSimply "Attempting to prove verification conditions." + +cruxLogMessageToSayWhat (Checking files) = + cruxNoisily ("Checking " <> T.intercalate ", " (T.pack <$> files)) + +cruxLogMessageToSayWhat DisablingBranchCoverageRequiresPathSatisfiability = + cruxWarn + "Branch coverage requires enabling path satisfiability checking. Coverage measurement is disabled!" + +cruxLogMessageToSayWhat DisablingProfilingIncompatibleWithPathSplitting = + cruxWarn + "Path splitting strategies are incompatible with Crucible profiling. Profiling is disabled!" + +-- for now, this message is only for IDE consumers +cruxLogMessageToSayWhat (EndedGoal {}) = SayNothing + +cruxLogMessageToSayWhat FoundCounterExample = + cruxOK "Counterexample found, skipping remaining goals" + +cruxLogMessageToSayWhat (Help (LogDoc doc)) = + cruxOK (renderStrict doc) + +cruxLogMessageToSayWhat (PathsUnexplored numberOfPaths) = + cruxWarn + ( T.unwords + [ T.pack $ show numberOfPaths, + "paths remaining not explored: program might not be fully verified" + ] + ) + +-- for now, this message is only for IDE consumers +cruxLogMessageToSayWhat (ProofObligations {}) = SayNothing + +cruxLogMessageToSayWhat SimulationComplete = + cruxNoisily "Simulation complete." + +cruxLogMessageToSayWhat SimulationTimedOut = + cruxWarn + "Simulation timed out! Program might not be fully verified!" + +cruxLogMessageToSayWhat SkippingUnsatCoresBecauseMCSatEnabled = + cruxWarn "Warning: skipping unsat cores because MC-SAT is enabled." + +-- for now, this message is only for IDE consumers +cruxLogMessageToSayWhat (StartedGoal {}) = SayNothing + +cruxLogMessageToSayWhat (TotalPathsExplored i) = + cruxSimply ("Total paths explored: " <> T.pack (show i)) + +cruxLogMessageToSayWhat (UnsupportedTimeoutFor backend) = + cruxWarn + (T.pack ("Goal timeout requested but not supported by " <> backend)) + +cruxLogMessageToSayWhat (Version nm ver) = + cruxOK + ( T.pack + ( unwords + [ "version: " <> version <> ",", + T.unpack nm, + "version: " <> (showVersion ver) + ] + ) + ) + +-- | Main function used to log/output a general text message of some kind +say :: + Logs msgs => + ( ?injectMessage :: msg -> msgs ) => + msg -> IO () +say = LJ.writeLog (view logMsg ?outputConfig) . ?injectMessage + +sayCrux :: + Logs msgs => + SupportsCruxLogMessage msgs => + CruxLogMessage -> IO () +sayCrux msg = + let ?injectMessage = ?injectCruxLogMessage in + say msg + +-- | Function used to log/output exception information +logException :: Logs msgs => SomeException -> IO () +logException = LJ.writeLog (_logExc ?outputConfig) + +-- | Function used to output the summary result for a completed +-- simulation. If the flag is true, show the details of each failed +-- goal before showing the summary. +logSimResult :: Logs msgs => Bool -> CruxSimulationResult -> IO () +logSimResult showFailedGoals = LJ.writeLog (_logSimResult ?outputConfig showFailedGoals) + +-- | Function used to output any individual goal proof failures from a simulation +logGoal :: Logs msgs => ProvedGoals -> IO () +logGoal = LJ.writeLog (_logGoal ?outputConfig) + + +---------------------------------------------------------------------- +-- Logging types and constraints + +-- | The Logs constraint should be applied for any function that will +-- use the main logging functions: says, logException, logSimResult, +-- or logGoal. +type Logs msgs = ( ?outputConfig :: OutputConfig msgs ) + +-- | Global options for Crux's main. These are not CruxOptions because +-- they are expected to be set directly by main, rather than by a +-- user's command-line options. They exist primarily to improve the +-- testability of the code. +-- +-- The Crux mkOutputConfig is recommended as a helper function for +-- creating this object, although it can be initialized directly if +-- needed. +data OutputConfig msgs = + OutputConfig { _outputHandle :: Handle + , _quiet :: Bool + , _logMsg :: LJ.LogAction IO msgs + , _logExc :: LJ.LogAction IO SomeException + , _logSimResult :: Bool -> LJ.LogAction IO CruxSimulationResult + -- ^ True to show individual goals, false for summary only + , _logGoal :: LJ.LogAction IO ProvedGoals + } + +-- | Some client code will want to output to the main output stream +-- directly instead of using the logging/output functions above. It +-- can either get the _outputHandle directly or it can use the +-- output/outputLn functions below. +outputHandle :: Getter (OutputConfig msgs) Handle +outputHandle f o = o <$ f (_outputHandle o) + +-- | Lens to allow client code to determine if running in quiet mode. +quiet :: Getter (OutputConfig msgs) Bool +quiet f o = o <$ f (_quiet o) + +logMsg :: Getter (OutputConfig msgs) (LJ.LogAction IO msgs) +logMsg f o = o <$ f (_logMsg o) + + +---------------------------------------------------------------------- +-- Logging default implementations (can be over-ridden by different +-- front end configurations). + +-- | This is the default logging output function for a SayWhat +-- message. It will emit the information with possible coloring (if +-- enabled via the first argument) to the proper handle (normal output +-- goes to the first handle, error output goes to the second handle, +-- and the same handle may be used for both). +-- +-- Front-ends that don't have specific output needs can simply use +-- this function. Alternative output functions can be used where +-- useful (e.g. JSON output). +logToStd :: (Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO () +logToStd outSpec errSpec = \case + SayWhat lvl frm msg -> + let sayer = case lvl of + OK -> colOut Green outSpec + Warn -> colOut Yellow errSpec + Fail -> colOut Red errSpec + Simply -> straightOut outSpec + Noisily -> straightOut outSpec + colOut clr (hndl, True) l = + do bracket_ + (hSetSGR hndl [ SetConsoleIntensity BoldIntensity + , SetColor Foreground Vivid clr]) + (hSetSGR hndl [Reset]) + (TIO.hPutStr hndl $ "[" <> frm <> "] ") + TIO.hPutStrLn hndl l + colOut _ hSpec@(_, False) l = straightOut hSpec l + straightOut (hndl, _) l = do TIO.hPutStr hndl $ "[" <> frm <> "] " + TIO.hPutStrLn hndl l + in mapM_ sayer $ T.lines msg + SayMore s1 s2 -> do logToStd outSpec errSpec s1 + logToStd outSpec errSpec s2 + SayNothing -> return () + + +---------------------------------------------------------------------- +-- Direct Output + +-- | This function emits output to the normal output handle (specified +-- at initialization time). This function is not recommended for +-- general use (the 'says', 'logException', 'logSimResult', 'logGoal', +-- etc. are preferred), but can be used by code needing more control +-- over the output formatting. +-- +-- This function does _not_ emit a newline at the end of the output. + +output :: Logs msgs => String -> IO () +output str = System.IO.hPutStr (view outputHandle ?outputConfig) str + +-- | This function emits output to the normal output handle (specified +-- at initialization time). This function is not recommended for +-- general use (the 'says', 'logException', 'logSimResult', 'logGoal', +-- etc. are preferred), but can be used by code needing more control +-- over the output formatting. +-- +-- This function emits a newline at the end of the output. + +outputLn :: Logs msgs => String -> IO () +outputLn str = System.IO.hPutStrLn (view outputHandle ?outputConfig) str diff --git a/src/Crux/Loops.hs b/src/Crux/Loops.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Loops.hs @@ -0,0 +1,40 @@ +module Crux.Loops where + +import qualified Data.Map as Map + +data Tree a = Node { node :: a, children :: Forest a } + deriving Show + +type Forest a = [Tree a] + +findLoops :: Eq a => [a] -> Forest a +findLoops = go [] + where + go prev steps = + case steps of + [] -> reverse prev + x : xs -> + case break ((x ==) . node) prev of + (inner,_:prev') -> go (Node x [] : Node x (reverse inner) : prev') xs + _ -> go (Node x [] : prev) xs + + +annotate :: Ord a => Forest a -> [ ([Int],a) ] +annotate = go [] Map.empty [] [] + where + go ns iters prevIters rest todo = + case todo of + [] -> rest + tree : trees -> + let a = node tree + n = Map.findWithDefault 1 a iters + ns' = n : ns + rest' = go ns (Map.insert a (n+1) iters) prevIters rest trees + in (reverse ns', a) : + go ns' Map.empty (iters : prevIters) rest' (children tree) + + +annotateLoops :: Ord a => [a] -> [ ([Int],a) ] +annotateLoops = annotate . findLoops + + diff --git a/src/Crux/Model.hs b/src/Crux/Model.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Model.hs @@ -0,0 +1,91 @@ +-- | This file is almost exactly the same as crucible-c/src/Model.hs + +{-# Language DataKinds #-} +{-# Language PolyKinds #-} +{-# Language Rank2Types #-} +{-# Language TypeFamilies #-} +{-# Language TypeApplications #-} +{-# Language TypeOperators #-} +{-# Language ScopedTypeVariables #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Crux.Model where + +import Data.BitVector.Sized (BV) +import qualified Data.BitVector.Sized as BV +import Data.Maybe (fromMaybe) +import qualified Data.Parameterized.Map as MapF +import qualified Numeric as N +import LibBF (BigFloat) +import qualified LibBF as BF + +import Lang.Crucible.Types + +import Crux.UI.JS +import Crux.Types + + +emptyModelView :: ModelView +emptyModelView = ModelView $ MapF.empty + +-------------------------------------------------------------------------------- + +toDouble :: Rational -> Double +toDouble = fromRational + + +showBVLiteral :: (1 <= w) => NatRepr w -> BV w -> String +showBVLiteral w bv = + (if x < 0 then "-0x" else "0x") ++ N.showHex i (if natValue w == 64 then "L" else "") + where + x = BV.asSigned w bv + i = abs x + +showFloatLiteral :: BigFloat -> String +showFloatLiteral x + | BF.bfIsNaN x = "NAN" + | BF.bfIsInf x = if BF.bfIsNeg x then "-INFINITY" else "INFINITY" + | BF.bfIsZero x = if BF.bfIsNeg x then "-0.0f" else "0.0f" + -- NB, 24 bits of precision for float + | otherwise = BF.bfToString 16 (BF.showFree (Just 24) <> BF.addPrefix) x ++ "f" + +showDoubleLiteral :: BigFloat -> String +showDoubleLiteral x + | BF.bfIsNaN x = "(double) NAN" + | BF.bfIsInf x = if BF.bfIsNeg x then "- ((double) INFINITY)" else "(double) INFINITY" + | BF.bfIsZero x = if BF.bfIsNeg x then "-0.0" else "0.0" + -- NB, 53 bits of precision for double + | otherwise = BF.bfToString 16 (BF.showFree (Just 53) <> BF.addPrefix) x + +valsJS :: BaseTypeRepr ty -> Vals ty -> IO [JS] +valsJS ty (Vals xs) = + let showEnt = case ty of + BaseBVRepr n -> showEnt' (showBVLiteral n) n + BaseFloatRepr (FloatingPointPrecisionRepr eb sb) + | Just Refl <- testEquality eb (knownNat @8) + , Just Refl <- testEquality sb (knownNat @24) + -> showEnt' showFloatLiteral (32 :: Int) + BaseFloatRepr (FloatingPointPrecisionRepr eb sb) + | Just Refl <- testEquality eb (knownNat @11) + , Just Refl <- testEquality sb (knownNat @53) + -> showEnt' showDoubleLiteral (64 :: Int) + BaseRealRepr -> showEnt' (show . toDouble) (knownNat @64) + _ -> error ("Type not implemented: " ++ show ty) + + in mapM showEnt xs + + where + showEnt' :: Show b => (a -> String) -> b -> Entry a -> IO JS + showEnt' repr n e = + do l <- fromMaybe jsNull <$> jsLoc (entryLoc e) + pure $ jsObj + [ "name" ~> jsStr (entryName e) + , "loc" ~> l + , "val" ~> jsStr (repr (entryValue e)) + , "bits" ~> jsStr (show n) + ] + +modelJS :: ModelView -> IO JS +modelJS m = + jsList . concat <$> sequence (MapF.foldrWithKey (\k v xs -> valsJS k v : xs) [] (modelVals m)) diff --git a/src/Crux/Overrides.hs b/src/Crux/Overrides.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Overrides.hs @@ -0,0 +1,90 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} + +module Crux.Overrides + ( mkFresh + , mkFreshFloat + , baseFreshOverride + , baseFreshOverride' + ) where + +import qualified Data.Parameterized.Context as Ctx + +import What4.BaseTypes (BaseTypeRepr) +import qualified What4.Interface as W4 +import qualified What4.InterpretedFloatingPoint as W4 + +import qualified Lang.Crucible.Backend as C +import qualified Lang.Crucible.Simulator.RegValue as C +import qualified Lang.Crucible.Types as C +import qualified Lang.Crucible.Simulator.OverrideSim as C + +import Crux.Types (OverM) +import Control.Monad.IO.Class (liftIO) + +-- | Create a fresh constant ('W4.freshConstant') with the given base type +mkFresh :: + C.IsSymInterface sym => + W4.SolverSymbol -> + BaseTypeRepr ty -> + OverM personality sym ext (C.RegValue sym (C.BaseToType ty)) +mkFresh name ty = + C.ovrWithBackend $ \bak -> + do let sym = C.backendGetSym bak + elt <- liftIO (W4.freshConstant sym name ty) + loc <- liftIO $ W4.getCurrentProgramLoc sym + let ev = C.CreateVariableEvent loc (show name) ty elt + liftIO $ C.addAssumptions bak (C.singleEvent ev) + return elt + +-- | Create a fresh float constant ('W4.freshFloatConstant') +mkFreshFloat :: + C.IsSymInterface sym => + W4.SolverSymbol -> + C.FloatInfoRepr fi -> + OverM personality sym ext (C.RegValue sym (C.FloatType fi)) +mkFreshFloat name fi = + C.ovrWithBackend $ \bak -> + do let sym = C.backendGetSym bak + elt <- liftIO $ W4.freshFloatConstant sym name fi + loc <- liftIO $ W4.getCurrentProgramLoc sym + let ev = C.CreateVariableEvent loc (show name) (W4.iFloatBaseTypeRepr sym fi) elt + liftIO $ C.addAssumptions bak (C.singleEvent ev) + return elt + +-- | Build an override that takes a string and returns a fresh constant with +-- that string as its name. +baseFreshOverride :: + C.IsSymInterface sym => + W4.BaseTypeRepr bty -> + -- | The language's string type (e.g., @LLVMPointerType@ for LLVM) + C.TypeRepr stringTy -> + -- | Get the variable name as a concrete string from the override arguments + (C.RegValue' sym stringTy -> OverM p sym ext W4.SolverSymbol) -> + C.TypedOverride (p sym) sym ext (C.EmptyCtx C.::> stringTy) (C.BaseToType bty) +baseFreshOverride bty sty getStr = + C.TypedOverride + { C.typedOverrideHandler = \(Ctx.Empty Ctx.:> strVal) -> do + str <- getStr strVal + mkFresh str bty + , C.typedOverrideArgs = Ctx.Empty Ctx.:> sty + , C.typedOverrideRet = C.baseToType bty + } + +-- | Build an override that takes no arguments and returns a fresh +-- constant that uses the given name. Generally, frontends should prefer +-- 'baseFreshOverride', to allow users to specify variable names. +baseFreshOverride' :: + C.IsSymInterface sym => + -- | Variable name + W4.SolverSymbol -> + W4.BaseTypeRepr bty -> + C.TypedOverride (p sym) sym ext C.EmptyCtx (C.BaseToType bty) +baseFreshOverride' nm bty = + C.TypedOverride + { C.typedOverrideHandler = \Ctx.Empty -> mkFresh nm bty + , C.typedOverrideArgs = Ctx.Empty + , C.typedOverrideRet = C.baseToType bty + } diff --git a/src/Crux/ProgressBar.hs b/src/Crux/ProgressBar.hs new file mode 100644 --- /dev/null +++ b/src/Crux/ProgressBar.hs @@ -0,0 +1,81 @@ +module Crux.ProgressBar where + +import System.IO +import System.Console.ANSI +import Control.Monad(zipWithM) + +-- | Callback called with index when a goal is started +type ProverMilestoneStartGoal = Integer -> IO () + +-- | Callback called with index when a goal has ended +type ProverMilestoneEndGoal = Integer -> IO () + +-- | Callback called when all goals have ended +type ProverMilestoneFinish = IO () + +-- | Set of three callbacks called by the prover to let loggers indicate +-- progress of the proving process. +type ProverMilestoneCallbacks = + ( ProverMilestoneStartGoal + , ProverMilestoneEndGoal + , ProverMilestoneFinish + ) + +silentProverMilestoneCallbacks :: ProverMilestoneCallbacks +silentProverMilestoneCallbacks = + (const (return ()), const (return ()), return ()) + +prepStatus :: String -> Int -> IO ProverMilestoneCallbacks +prepStatus pref tot = + do ansi <- hSupportsANSI stdout + if ansi then + return (start,end,finish) + else + return silentProverMilestoneCallbacks + + where + start n = do hSaveCursor stdout + hPutStr stdout (msg n) + hFlush stdout + end _n = do hRestoreCursor stdout + hFlush stdout + + finish = do hClearLine stdout + hFlush stdout + + totS = show tot + totW = length totS + sh x = let y = show x + in replicate (totW - length y) ' ' ++ y + + msg n = pref ++ sh (n::Integer) ++ " / " ++ totS + + + +withProgressBar' :: String -> [a] -> (a -> IO b) -> IO [b] +withProgressBar' pref xs f = + do (start,end,finish) <- prepStatus pref (length xs) + let one n a = + do start n + b <- f a + end n + return b + zipWithM one [ 1 .. ] xs <* finish + +withProgressBar :: Int -> [a] -> (a -> IO b) -> IO [b] +withProgressBar w xs f = + do prt "|" + go 0 0 xs [] + where + prt x = do putStr x + hFlush stdout + + step = fromIntegral w / fromIntegral (length xs) :: Float + go shown loc todo done = + do let new = floor loc - shown + prt (replicate (floor loc - shown) '=') + case todo of + [] -> prt "|\n" >> return (reverse done) + a : as -> + do b <- f a + go (shown + new) (loc + step) as (b : done) diff --git a/src/Crux/Report.hs b/src/Crux/Report.hs new file mode 100644 --- /dev/null +++ b/src/Crux/Report.hs @@ -0,0 +1,247 @@ +-- from: crucible-c/src/Report.hs + +{-# Language LambdaCase #-} +{-# Language OverloadedStrings #-} +module Crux.Report where + +import Data.Void (Void) +import System.FilePath +import System.Directory (createDirectoryIfMissing, canonicalizePath) +import System.IO +import qualified Data.Foldable as Fold +import Data.Functor.Const +import Data.List (partition) +import Data.Maybe (fromMaybe) +import qualified Data.Sequence as Seq +import Data.Sequence (Seq) +import qualified Data.Set as Set +import qualified Data.Text as Text +import Control.Exception (catch, SomeException(..)) +import Control.Monad (forM_) +import Prettyprinter (Doc) + +import qualified Data.Text.IO as T + +import Lang.Crucible.Simulator.SimError +import Lang.Crucible.Backend +import What4.ProgramLoc +import What4.Expr (GroundValueWrapper) + +import Crux.Types +import Crux.Config.Common +import Crux.Loops +import Crux.Model ( modelJS ) + +-- Note these should be data files. However, cabal-new build doesn't make it easy for the installation +-- to find data files, so they are embedded as Text constants instead. + +import Crux.UI.JS +import Crux.UI.Jquery (jquery) -- ui/jquery.min.js +import Crux.UI.IndexHtml (indexHtml) -- ui/index.html + + +generateReport :: CruxOptions -> CruxSimulationResult -> IO () +generateReport opts res + | outDir opts == "" || skipReport opts = return () + | otherwise = + do let xs = cruxSimResultGoals res + goals = map snd $ Fold.toList xs + referencedFiles = Set.toList (Set.fromList (inputFiles opts) <> foldMap provedGoalFiles goals) + createDirectoryIfMissing True (outDir opts) + maybeGenerateSource opts referencedFiles + scs <- renderSideConds opts goals + let contents = renderJS (jsList scs) + -- Due to CORS restrictions, the only current way of statically loading local data + -- is by including a + + + + + +
+ +|] diff --git a/src/Crux/UI/JS.hs b/src/Crux/UI/JS.hs new file mode 100644 --- /dev/null +++ b/src/Crux/UI/JS.hs @@ -0,0 +1,60 @@ +{-# Language MultiWayIf #-} +{-# Language OverloadedStrings #-} +-- | Utilites for generating JSON +module Crux.UI.JS where + +import Data.Text(unpack) +import Data.List(intercalate) +import Data.Maybe(fromMaybe) +import System.Directory( canonicalizePath ) + +import What4.ProgramLoc + +jsLoc :: ProgramLoc -> IO (Maybe JS) +jsLoc x = + case plSourceLoc x of + SourcePos f l c -> + do let fstr = unpack f + fabsolute <- + if | null fstr -> pure "" + | otherwise -> canonicalizePath fstr + pure $ Just $ jsObj + [ "file" ~> jsStr fabsolute + , "line" ~> jsStr (show l) + , "col" ~> jsStr (show c) + ] + _ -> pure Nothing + +-------------------------------------------------------------------------------- +newtype JS = JS { renderJS :: String } + +jsList :: [JS] -> JS +jsList xs = JS $ "[" ++ intercalate "," [ x | JS x <- xs ] ++ "]" + +infix 1 ~> + +(~>) :: a -> b -> (a,b) +(~>) = (,) + +jsObj :: [(String,JS)] -> JS +jsObj xs = + JS $ "{" ++ intercalate "," [ show x ++ ": " ++ v | (x,JS v) <- xs ] ++ "}" + +jsBool :: Bool -> JS +jsBool b = JS (if b then "true" else "false") + +jsStr :: String -> JS +jsStr = JS . show + +jsNull :: JS +jsNull = JS "null" + +jsMaybe :: Maybe JS -> JS +jsMaybe = fromMaybe jsNull + +jsNum :: Show a => a -> JS +jsNum = JS . show + + +--------------------------------------------------- + diff --git a/src/Crux/UI/Jquery.hs b/src/Crux/UI/Jquery.hs new file mode 100644 --- /dev/null +++ b/src/Crux/UI/Jquery.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} + + +module Crux.UI.Jquery where + +import Data.Text (Text) +-- raw-strings-qq +import Text.RawString.QQ + + +jquery :: Text +jquery = [r| +/*! jQuery v3.3.1 | (c) JS Foundation and other contributors | jquery.org/license */ +!function(e,t){"use strict";"object"==typeof module&&"object"==typeof module.exports?module.exports=e.document?t(e,!0):function(e){if(!e.document)throw new Error("jQuery requires a window with a document");return t(e)}:t(e)}("undefined"!=typeof window?window:this,function(e,t){"use strict";var n=[],r=e.document,i=Object.getPrototypeOf,o=n.slice,a=n.concat,s=n.push,u=n.indexOf,l={},c=l.toString,f=l.hasOwnProperty,p=f.toString,d=p.call(Object),h={},g=function e(t){return"function"==typeof t&&"number"!=typeof t.nodeType},y=function e(t){return null!=t&&t===t.window},v={type:!0,src:!0,noModule:!0};function m(e,t,n){var i,o=(t=t||r).createElement("script");if(o.text=e,n)for(i in v)n[i]&&(o[i]=n[i]);t.head.appendChild(o).parentNode.removeChild(o)}function x(e){return null==e?e+"":"object"==typeof e||"function"==typeof e?l[c.call(e)]||"object":typeof e}var b="3.3.1",w=function(e,t){return new w.fn.init(e,t)},T=/^[\s\uFEFF\xA0]+|[\s\uFEFF\xA0]+$/g;w.fn=w.prototype={jquery:"3.3.1",constructor:w,length:0,toArray:function(){return o.call(this)},get:function(e){return null==e?o.call(this):e<0?this[e+this.length]:this[e]},pushStack:function(e){var t=w.merge(this.constructor(),e);return t.prevObject=this,t},each:function(e){return w.each(this,e)},map:function(e){return this.pushStack(w.map(this,function(t,n){return e.call(t,n,t)}))},slice:function(){return this.pushStack(o.apply(this,arguments))},first:function(){return this.eq(0)},last:function(){return this.eq(-1)},eq:function(e){var t=this.length,n=+e+(e<0?t:0);return this.pushStack(n>=0&&n0&&t-1 in e)}var E=function(e){var t,n,r,i,o,a,s,u,l,c,f,p,d,h,g,y,v,m,x,b="sizzle"+1*new Date,w=e.document,T=0,C=0,E=ae(),k=ae(),S=ae(),D=function(e,t){return e===t&&(f=!0),0},N={}.hasOwnProperty,A=[],j=A.pop,q=A.push,L=A.push,H=A.slice,O=function(e,t){for(var n=0,r=e.length;n+~]|"+M+")"+M+"*"),z=new RegExp("="+M+"*([^\\]'\"]*?)"+M+"*\\]","g"),X=new RegExp(W),U=new RegExp("^"+R+"$"),V={ID:new RegExp("^#("+R+")"),CLASS:new RegExp("^\\.("+R+")"),TAG:new RegExp("^("+R+"|[*])"),ATTR:new RegExp("^"+I),PSEUDO:new RegExp("^"+W),CHILD:new RegExp("^:(only|first|last|nth|nth-last)-(child|of-type)(?:\\("+M+"*(even|odd|(([+-]|)(\\d*)n|)"+M+"*(?:([+-]|)"+M+"*(\\d+)|))"+M+"*\\)|)","i"),bool:new RegExp("^(?:"+P+")$","i"),needsContext:new RegExp("^"+M+"*[>+~]|:(even|odd|eq|gt|lt|nth|first|last)(?:\\("+M+"*((?:-\\d)?\\d*)"+M+"*\\)|)(?=[^-]|$)","i")},G=/^(?:input|select|textarea|button)$/i,Y=/^h\d$/i,Q=/^[^{]+\{\s*\[native \w/,J=/^(?:#([\w-]+)|(\w+)|\.([\w-]+))$/,K=/[+~]/,Z=new RegExp("\\\\([\\da-f]{1,6}"+M+"?|("+M+")|.)","ig"),ee=function(e,t,n){var r="0x"+t-65536;return r!==r||n?t:r<0?String.fromCharCode(r+65536):String.fromCharCode(r>>10|55296,1023&r|56320)},te=/([\0-\x1f\x7f]|^-?\d)|^-$|[^\0-\x1f\x7f-\uFFFF\w-]/g,ne=function(e,t){return t?"\0"===e?"\ufffd":e.slice(0,-1)+"\\"+e.charCodeAt(e.length-1).toString(16)+" ":"\\"+e},re=function(){p()},ie=me(function(e){return!0===e.disabled&&("form"in e||"label"in e)},{dir:"parentNode",next:"legend"});try{L.apply(A=H.call(w.childNodes),w.childNodes),A[w.childNodes.length].nodeType}catch(e){L={apply:A.length?function(e,t){q.apply(e,H.call(t))}:function(e,t){var n=e.length,r=0;while(e[n++]=t[r++]);e.length=n-1}}}function oe(e,t,r,i){var o,s,l,c,f,h,v,m=t&&t.ownerDocument,T=t?t.nodeType:9;if(r=r||[],"string"!=typeof e||!e||1!==T&&9!==T&&11!==T)return r;if(!i&&((t?t.ownerDocument||t:w)!==d&&p(t),t=t||d,g)){if(11!==T&&(f=J.exec(e)))if(o=f[1]){if(9===T){if(!(l=t.getElementById(o)))return r;if(l.id===o)return r.push(l),r}else if(m&&(l=m.getElementById(o))&&x(t,l)&&l.id===o)return r.push(l),r}else{if(f[2])return L.apply(r,t.getElementsByTagName(e)),r;if((o=f[3])&&n.getElementsByClassName&&t.getElementsByClassName)return L.apply(r,t.getElementsByClassName(o)),r}if(n.qsa&&!S[e+" "]&&(!y||!y.test(e))){if(1!==T)m=t,v=e;else if("object"!==t.nodeName.toLowerCase()){(c=t.getAttribute("id"))?c=c.replace(te,ne):t.setAttribute("id",c=b),s=(h=a(e)).length;while(s--)h[s]="#"+c+" "+ve(h[s]);v=h.join(","),m=K.test(e)&&ge(t.parentNode)||t}if(v)try{return L.apply(r,m.querySelectorAll(v)),r}catch(e){}finally{c===b&&t.removeAttribute("id")}}}return u(e.replace(B,"$1"),t,r,i)}function ae(){var e=[];function t(n,i){return e.push(n+" ")>r.cacheLength&&delete t[e.shift()],t[n+" "]=i}return t}function se(e){return e[b]=!0,e}function ue(e){var t=d.createElement("fieldset");try{return!!e(t)}catch(e){return!1}finally{t.parentNode&&t.parentNode.removeChild(t),t=null}}function le(e,t){var n=e.split("|"),i=n.length;while(i--)r.attrHandle[n[i]]=t}function ce(e,t){var n=t&&e,r=n&&1===e.nodeType&&1===t.nodeType&&e.sourceIndex-t.sourceIndex;if(r)return r;if(n)while(n=n.nextSibling)if(n===t)return-1;return e?1:-1}function fe(e){return function(t){return"input"===t.nodeName.toLowerCase()&&t.type===e}}function pe(e){return function(t){var n=t.nodeName.toLowerCase();return("input"===n||"button"===n)&&t.type===e}}function de(e){return function(t){return"form"in t?t.parentNode&&!1===t.disabled?"label"in t?"label"in t.parentNode?t.parentNode.disabled===e:t.disabled===e:t.isDisabled===e||t.isDisabled!==!e&&ie(t)===e:t.disabled===e:"label"in t&&t.disabled===e}}function he(e){return se(function(t){return t=+t,se(function(n,r){var i,o=e([],n.length,t),a=o.length;while(a--)n[i=o[a]]&&(n[i]=!(r[i]=n[i]))})})}function ge(e){return e&&"undefined"!=typeof e.getElementsByTagName&&e}n=oe.support={},o=oe.isXML=function(e){var t=e&&(e.ownerDocument||e).documentElement;return!!t&&"HTML"!==t.nodeName},p=oe.setDocument=function(e){var t,i,a=e?e.ownerDocument||e:w;return a!==d&&9===a.nodeType&&a.documentElement?(d=a,h=d.documentElement,g=!o(d),w!==d&&(i=d.defaultView)&&i.top!==i&&(i.addEventListener?i.addEventListener("unload",re,!1):i.attachEvent&&i.attachEvent("onunload",re)),n.attributes=ue(function(e){return e.className="i",!e.getAttribute("className")}),n.getElementsByTagName=ue(function(e){return e.appendChild(d.createComment("")),!e.getElementsByTagName("*").length}),n.getElementsByClassName=Q.test(d.getElementsByClassName),n.getById=ue(function(e){return h.appendChild(e).id=b,!d.getElementsByName||!d.getElementsByName(b).length}),n.getById?(r.filter.ID=function(e){var t=e.replace(Z,ee);return function(e){return e.getAttribute("id")===t}},r.find.ID=function(e,t){if("undefined"!=typeof t.getElementById&&g){var n=t.getElementById(e);return n?[n]:[]}}):(r.filter.ID=function(e){var t=e.replace(Z,ee);return function(e){var n="undefined"!=typeof e.getAttributeNode&&e.getAttributeNode("id");return n&&n.value===t}},r.find.ID=function(e,t){if("undefined"!=typeof t.getElementById&&g){var n,r,i,o=t.getElementById(e);if(o){if((n=o.getAttributeNode("id"))&&n.value===e)return[o];i=t.getElementsByName(e),r=0;while(o=i[r++])if((n=o.getAttributeNode("id"))&&n.value===e)return[o]}return[]}}),r.find.TAG=n.getElementsByTagName?function(e,t){return"undefined"!=typeof t.getElementsByTagName?t.getElementsByTagName(e):n.qsa?t.querySelectorAll(e):void 0}:function(e,t){var n,r=[],i=0,o=t.getElementsByTagName(e);if("*"===e){while(n=o[i++])1===n.nodeType&&r.push(n);return r}return o},r.find.CLASS=n.getElementsByClassName&&function(e,t){if("undefined"!=typeof t.getElementsByClassName&&g)return t.getElementsByClassName(e)},v=[],y=[],(n.qsa=Q.test(d.querySelectorAll))&&(ue(function(e){h.appendChild(e).innerHTML="",e.querySelectorAll("[msallowcapture^='']").length&&y.push("[*^$]="+M+"*(?:''|\"\")"),e.querySelectorAll("[selected]").length||y.push("\\["+M+"*(?:value|"+P+")"),e.querySelectorAll("[id~="+b+"-]").length||y.push("~="),e.querySelectorAll(":checked").length||y.push(":checked"),e.querySelectorAll("a#"+b+"+*").length||y.push(".#.+[+~]")}),ue(function(e){e.innerHTML="";var t=d.createElement("input");t.setAttribute("type","hidden"),e.appendChild(t).setAttribute("name","D"),e.querySelectorAll("[name=d]").length&&y.push("name"+M+"*[*^$|!~]?="),2!==e.querySelectorAll(":enabled").length&&y.push(":enabled",":disabled"),h.appendChild(e).disabled=!0,2!==e.querySelectorAll(":disabled").length&&y.push(":enabled",":disabled"),e.querySelectorAll("*,:x"),y.push(",.*:")})),(n.matchesSelector=Q.test(m=h.matches||h.webkitMatchesSelector||h.mozMatchesSelector||h.oMatchesSelector||h.msMatchesSelector))&&ue(function(e){n.disconnectedMatch=m.call(e,"*"),m.call(e,"[s!='']:x"),v.push("!=",W)}),y=y.length&&new RegExp(y.join("|")),v=v.length&&new RegExp(v.join("|")),t=Q.test(h.compareDocumentPosition),x=t||Q.test(h.contains)?function(e,t){var n=9===e.nodeType?e.documentElement:e,r=t&&t.parentNode;return e===r||!(!r||1!==r.nodeType||!(n.contains?n.contains(r):e.compareDocumentPosition&&16&e.compareDocumentPosition(r)))}:function(e,t){if(t)while(t=t.parentNode)if(t===e)return!0;return!1},D=t?function(e,t){if(e===t)return f=!0,0;var r=!e.compareDocumentPosition-!t.compareDocumentPosition;return r||(1&(r=(e.ownerDocument||e)===(t.ownerDocument||t)?e.compareDocumentPosition(t):1)||!n.sortDetached&&t.compareDocumentPosition(e)===r?e===d||e.ownerDocument===w&&x(w,e)?-1:t===d||t.ownerDocument===w&&x(w,t)?1:c?O(c,e)-O(c,t):0:4&r?-1:1)}:function(e,t){if(e===t)return f=!0,0;var n,r=0,i=e.parentNode,o=t.parentNode,a=[e],s=[t];if(!i||!o)return e===d?-1:t===d?1:i?-1:o?1:c?O(c,e)-O(c,t):0;if(i===o)return ce(e,t);n=e;while(n=n.parentNode)a.unshift(n);n=t;while(n=n.parentNode)s.unshift(n);while(a[r]===s[r])r++;return r?ce(a[r],s[r]):a[r]===w?-1:s[r]===w?1:0},d):d},oe.matches=function(e,t){return oe(e,null,null,t)},oe.matchesSelector=function(e,t){if((e.ownerDocument||e)!==d&&p(e),t=t.replace(z,"='$1']"),n.matchesSelector&&g&&!S[t+" "]&&(!v||!v.test(t))&&(!y||!y.test(t)))try{var r=m.call(e,t);if(r||n.disconnectedMatch||e.document&&11!==e.document.nodeType)return r}catch(e){}return oe(t,d,null,[e]).length>0},oe.contains=function(e,t){return(e.ownerDocument||e)!==d&&p(e),x(e,t)},oe.attr=function(e,t){(e.ownerDocument||e)!==d&&p(e);var i=r.attrHandle[t.toLowerCase()],o=i&&N.call(r.attrHandle,t.toLowerCase())?i(e,t,!g):void 0;return void 0!==o?o:n.attributes||!g?e.getAttribute(t):(o=e.getAttributeNode(t))&&o.specified?o.value:null},oe.escape=function(e){return(e+"").replace(te,ne)},oe.error=function(e){throw new Error("Syntax error, unrecognized expression: "+e)},oe.uniqueSort=function(e){var t,r=[],i=0,o=0;if(f=!n.detectDuplicates,c=!n.sortStable&&e.slice(0),e.sort(D),f){while(t=e[o++])t===e[o]&&(i=r.push(o));while(i--)e.splice(r[i],1)}return c=null,e},i=oe.getText=function(e){var t,n="",r=0,o=e.nodeType;if(o){if(1===o||9===o||11===o){if("string"==typeof e.textContent)return e.textContent;for(e=e.firstChild;e;e=e.nextSibling)n+=i(e)}else if(3===o||4===o)return e.nodeValue}else while(t=e[r++])n+=i(t);return n},(r=oe.selectors={cacheLength:50,createPseudo:se,match:V,attrHandle:{},find:{},relative:{">":{dir:"parentNode",first:!0}," ":{dir:"parentNode"},"+":{dir:"previousSibling",first:!0},"~":{dir:"previousSibling"}},preFilter:{ATTR:function(e){return e[1]=e[1].replace(Z,ee),e[3]=(e[3]||e[4]||e[5]||"").replace(Z,ee),"~="===e[2]&&(e[3]=" "+e[3]+" "),e.slice(0,4)},CHILD:function(e){return e[1]=e[1].toLowerCase(),"nth"===e[1].slice(0,3)?(e[3]||oe.error(e[0]),e[4]=+(e[4]?e[5]+(e[6]||1):2*("even"===e[3]||"odd"===e[3])),e[5]=+(e[7]+e[8]||"odd"===e[3])):e[3]&&oe.error(e[0]),e},PSEUDO:function(e){var t,n=!e[6]&&e[2];return V.CHILD.test(e[0])?null:(e[3]?e[2]=e[4]||e[5]||"":n&&X.test(n)&&(t=a(n,!0))&&(t=n.indexOf(")",n.length-t)-n.length)&&(e[0]=e[0].slice(0,t),e[2]=n.slice(0,t)),e.slice(0,3))}},filter:{TAG:function(e){var t=e.replace(Z,ee).toLowerCase();return"*"===e?function(){return!0}:function(e){return e.nodeName&&e.nodeName.toLowerCase()===t}},CLASS:function(e){var t=E[e+" "];return t||(t=new RegExp("(^|"+M+")"+e+"("+M+"|$)"))&&E(e,function(e){return t.test("string"==typeof e.className&&e.className||"undefined"!=typeof e.getAttribute&&e.getAttribute("class")||"")})},ATTR:function(e,t,n){return function(r){var i=oe.attr(r,e);return null==i?"!="===t:!t||(i+="","="===t?i===n:"!="===t?i!==n:"^="===t?n&&0===i.indexOf(n):"*="===t?n&&i.indexOf(n)>-1:"$="===t?n&&i.slice(-n.length)===n:"~="===t?(" "+i.replace($," ")+" ").indexOf(n)>-1:"|="===t&&(i===n||i.slice(0,n.length+1)===n+"-"))}},CHILD:function(e,t,n,r,i){var o="nth"!==e.slice(0,3),a="last"!==e.slice(-4),s="of-type"===t;return 1===r&&0===i?function(e){return!!e.parentNode}:function(t,n,u){var l,c,f,p,d,h,g=o!==a?"nextSibling":"previousSibling",y=t.parentNode,v=s&&t.nodeName.toLowerCase(),m=!u&&!s,x=!1;if(y){if(o){while(g){p=t;while(p=p[g])if(s?p.nodeName.toLowerCase()===v:1===p.nodeType)return!1;h=g="only"===e&&!h&&"nextSibling"}return!0}if(h=[a?y.firstChild:y.lastChild],a&&m){x=(d=(l=(c=(f=(p=y)[b]||(p[b]={}))[p.uniqueID]||(f[p.uniqueID]={}))[e]||[])[0]===T&&l[1])&&l[2],p=d&&y.childNodes[d];while(p=++d&&p&&p[g]||(x=d=0)||h.pop())if(1===p.nodeType&&++x&&p===t){c[e]=[T,d,x];break}}else if(m&&(x=d=(l=(c=(f=(p=t)[b]||(p[b]={}))[p.uniqueID]||(f[p.uniqueID]={}))[e]||[])[0]===T&&l[1]),!1===x)while(p=++d&&p&&p[g]||(x=d=0)||h.pop())if((s?p.nodeName.toLowerCase()===v:1===p.nodeType)&&++x&&(m&&((c=(f=p[b]||(p[b]={}))[p.uniqueID]||(f[p.uniqueID]={}))[e]=[T,x]),p===t))break;return(x-=i)===r||x%r==0&&x/r>=0}}},PSEUDO:function(e,t){var n,i=r.pseudos[e]||r.setFilters[e.toLowerCase()]||oe.error("unsupported pseudo: "+e);return i[b]?i(t):i.length>1?(n=[e,e,"",t],r.setFilters.hasOwnProperty(e.toLowerCase())?se(function(e,n){var r,o=i(e,t),a=o.length;while(a--)e[r=O(e,o[a])]=!(n[r]=o[a])}):function(e){return i(e,0,n)}):i}},pseudos:{not:se(function(e){var t=[],n=[],r=s(e.replace(B,"$1"));return r[b]?se(function(e,t,n,i){var o,a=r(e,null,i,[]),s=e.length;while(s--)(o=a[s])&&(e[s]=!(t[s]=o))}):function(e,i,o){return t[0]=e,r(t,null,o,n),t[0]=null,!n.pop()}}),has:se(function(e){return function(t){return oe(e,t).length>0}}),contains:se(function(e){return e=e.replace(Z,ee),function(t){return(t.textContent||t.innerText||i(t)).indexOf(e)>-1}}),lang:se(function(e){return U.test(e||"")||oe.error("unsupported lang: "+e),e=e.replace(Z,ee).toLowerCase(),function(t){var n;do{if(n=g?t.lang:t.getAttribute("xml:lang")||t.getAttribute("lang"))return(n=n.toLowerCase())===e||0===n.indexOf(e+"-")}while((t=t.parentNode)&&1===t.nodeType);return!1}}),target:function(t){var n=e.location&&e.location.hash;return n&&n.slice(1)===t.id},root:function(e){return e===h},focus:function(e){return e===d.activeElement&&(!d.hasFocus||d.hasFocus())&&!!(e.type||e.href||~e.tabIndex)},enabled:de(!1),disabled:de(!0),checked:function(e){var t=e.nodeName.toLowerCase();return"input"===t&&!!e.checked||"option"===t&&!!e.selected},selected:function(e){return e.parentNode&&e.parentNode.selectedIndex,!0===e.selected},empty:function(e){for(e=e.firstChild;e;e=e.nextSibling)if(e.nodeType<6)return!1;return!0},parent:function(e){return!r.pseudos.empty(e)},header:function(e){return Y.test(e.nodeName)},input:function(e){return G.test(e.nodeName)},button:function(e){var t=e.nodeName.toLowerCase();return"input"===t&&"button"===e.type||"button"===t},text:function(e){var t;return"input"===e.nodeName.toLowerCase()&&"text"===e.type&&(null==(t=e.getAttribute("type"))||"text"===t.toLowerCase())},first:he(function(){return[0]}),last:he(function(e,t){return[t-1]}),eq:he(function(e,t,n){return[n<0?n+t:n]}),even:he(function(e,t){for(var n=0;n=0;)e.push(r);return e}),gt:he(function(e,t,n){for(var r=n<0?n+t:n;++r1?function(t,n,r){var i=e.length;while(i--)if(!e[i](t,n,r))return!1;return!0}:e[0]}function be(e,t,n){for(var r=0,i=t.length;r-1&&(o[l]=!(a[l]=f))}}else v=we(v===a?v.splice(h,v.length):v),i?i(null,a,v,u):L.apply(a,v)})}function Ce(e){for(var t,n,i,o=e.length,a=r.relative[e[0].type],s=a||r.relative[" "],u=a?1:0,c=me(function(e){return e===t},s,!0),f=me(function(e){return O(t,e)>-1},s,!0),p=[function(e,n,r){var i=!a&&(r||n!==l)||((t=n).nodeType?c(e,n,r):f(e,n,r));return t=null,i}];u1&&xe(p),u>1&&ve(e.slice(0,u-1).concat({value:" "===e[u-2].type?"*":""})).replace(B,"$1"),n,u0,i=e.length>0,o=function(o,a,s,u,c){var f,h,y,v=0,m="0",x=o&&[],b=[],w=l,C=o||i&&r.find.TAG("*",c),E=T+=null==w?1:Math.random()||.1,k=C.length;for(c&&(l=a===d||a||c);m!==k&&null!=(f=C[m]);m++){if(i&&f){h=0,a||f.ownerDocument===d||(p(f),s=!g);while(y=e[h++])if(y(f,a||d,s)){u.push(f);break}c&&(T=E)}n&&((f=!y&&f)&&v--,o&&x.push(f))}if(v+=m,n&&m!==v){h=0;while(y=t[h++])y(x,b,a,s);if(o){if(v>0)while(m--)x[m]||b[m]||(b[m]=j.call(u));b=we(b)}L.apply(u,b),c&&!o&&b.length>0&&v+t.length>1&&oe.uniqueSort(u)}return c&&(T=E,l=w),x};return n?se(o):o}return s=oe.compile=function(e,t){var n,r=[],i=[],o=S[e+" "];if(!o){t||(t=a(e)),n=t.length;while(n--)(o=Ce(t[n]))[b]?r.push(o):i.push(o);(o=S(e,Ee(i,r))).selector=e}return o},u=oe.select=function(e,t,n,i){var o,u,l,c,f,p="function"==typeof e&&e,d=!i&&a(e=p.selector||e);if(n=n||[],1===d.length){if((u=d[0]=d[0].slice(0)).length>2&&"ID"===(l=u[0]).type&&9===t.nodeType&&g&&r.relative[u[1].type]){if(!(t=(r.find.ID(l.matches[0].replace(Z,ee),t)||[])[0]))return n;p&&(t=t.parentNode),e=e.slice(u.shift().value.length)}o=V.needsContext.test(e)?0:u.length;while(o--){if(l=u[o],r.relative[c=l.type])break;if((f=r.find[c])&&(i=f(l.matches[0].replace(Z,ee),K.test(u[0].type)&&ge(t.parentNode)||t))){if(u.splice(o,1),!(e=i.length&&ve(u)))return L.apply(n,i),n;break}}}return(p||s(e,d))(i,t,!g,n,!t||K.test(e)&&ge(t.parentNode)||t),n},n.sortStable=b.split("").sort(D).join("")===b,n.detectDuplicates=!!f,p(),n.sortDetached=ue(function(e){return 1&e.compareDocumentPosition(d.createElement("fieldset"))}),ue(function(e){return e.innerHTML="","#"===e.firstChild.getAttribute("href")})||le("type|href|height|width",function(e,t,n){if(!n)return e.getAttribute(t,"type"===t.toLowerCase()?1:2)}),n.attributes&&ue(function(e){return e.innerHTML="",e.firstChild.setAttribute("value",""),""===e.firstChild.getAttribute("value")})||le("value",function(e,t,n){if(!n&&"input"===e.nodeName.toLowerCase())return e.defaultValue}),ue(function(e){return null==e.getAttribute("disabled")})||le(P,function(e,t,n){var r;if(!n)return!0===e[t]?t.toLowerCase():(r=e.getAttributeNode(t))&&r.specified?r.value:null}),oe}(e);w.find=E,w.expr=E.selectors,w.expr[":"]=w.expr.pseudos,w.uniqueSort=w.unique=E.uniqueSort,w.text=E.getText,w.isXMLDoc=E.isXML,w.contains=E.contains,w.escapeSelector=E.escape;var k=function(e,t,n){var r=[],i=void 0!==n;while((e=e[t])&&9!==e.nodeType)if(1===e.nodeType){if(i&&w(e).is(n))break;r.push(e)}return r},S=function(e,t){for(var n=[];e;e=e.nextSibling)1===e.nodeType&&e!==t&&n.push(e);return n},D=w.expr.match.needsContext;function N(e,t){return e.nodeName&&e.nodeName.toLowerCase()===t.toLowerCase()}var A=/^<([a-z][^\/\0>:\x20\t\r\n\f]*)[\x20\t\r\n\f]*\/?>(?:<\/\1>|)$/i;function j(e,t,n){return g(t)?w.grep(e,function(e,r){return!!t.call(e,r,e)!==n}):t.nodeType?w.grep(e,function(e){return e===t!==n}):"string"!=typeof t?w.grep(e,function(e){return u.call(t,e)>-1!==n}):w.filter(t,e,n)}w.filter=function(e,t,n){var r=t[0];return n&&(e=":not("+e+")"),1===t.length&&1===r.nodeType?w.find.matchesSelector(r,e)?[r]:[]:w.find.matches(e,w.grep(t,function(e){return 1===e.nodeType}))},w.fn.extend({find:function(e){var t,n,r=this.length,i=this;if("string"!=typeof e)return this.pushStack(w(e).filter(function(){for(t=0;t1?w.uniqueSort(n):n},filter:function(e){return this.pushStack(j(this,e||[],!1))},not:function(e){return this.pushStack(j(this,e||[],!0))},is:function(e){return!!j(this,"string"==typeof e&&D.test(e)?w(e):e||[],!1).length}});var q,L=/^(?:\s*(<[\w\W]+>)[^>]*|#([\w-]+))$/;(w.fn.init=function(e,t,n){var i,o;if(!e)return this;if(n=n||q,"string"==typeof e){if(!(i="<"===e[0]&&">"===e[e.length-1]&&e.length>=3?[null,e,null]:L.exec(e))||!i[1]&&t)return!t||t.jquery?(t||n).find(e):this.constructor(t).find(e);if(i[1]){if(t=t instanceof w?t[0]:t,w.merge(this,w.parseHTML(i[1],t&&t.nodeType?t.ownerDocument||t:r,!0)),A.test(i[1])&&w.isPlainObject(t))for(i in t)g(this[i])?this[i](t[i]):this.attr(i,t[i]);return this}return(o=r.getElementById(i[2]))&&(this[0]=o,this.length=1),this}return e.nodeType?(this[0]=e,this.length=1,this):g(e)?void 0!==n.ready?n.ready(e):e(w):w.makeArray(e,this)}).prototype=w.fn,q=w(r);var H=/^(?:parents|prev(?:Until|All))/,O={children:!0,contents:!0,next:!0,prev:!0};w.fn.extend({has:function(e){var t=w(e,this),n=t.length;return this.filter(function(){for(var e=0;e-1:1===n.nodeType&&w.find.matchesSelector(n,e))){o.push(n);break}return this.pushStack(o.length>1?w.uniqueSort(o):o)},index:function(e){return e?"string"==typeof e?u.call(w(e),this[0]):u.call(this,e.jquery?e[0]:e):this[0]&&this[0].parentNode?this.first().prevAll().length:-1},add:function(e,t){return this.pushStack(w.uniqueSort(w.merge(this.get(),w(e,t))))},addBack:function(e){return this.add(null==e?this.prevObject:this.prevObject.filter(e))}});function P(e,t){while((e=e[t])&&1!==e.nodeType);return e}w.each({parent:function(e){var t=e.parentNode;return t&&11!==t.nodeType?t:null},parents:function(e){return k(e,"parentNode")},parentsUntil:function(e,t,n){return k(e,"parentNode",n)},next:function(e){return P(e,"nextSibling")},prev:function(e){return P(e,"previousSibling")},nextAll:function(e){return k(e,"nextSibling")},prevAll:function(e){return k(e,"previousSibling")},nextUntil:function(e,t,n){return k(e,"nextSibling",n)},prevUntil:function(e,t,n){return k(e,"previousSibling",n)},siblings:function(e){return S((e.parentNode||{}).firstChild,e)},children:function(e){return S(e.firstChild)},contents:function(e){return N(e,"iframe")?e.contentDocument:(N(e,"template")&&(e=e.content||e),w.merge([],e.childNodes))}},function(e,t){w.fn[e]=function(n,r){var i=w.map(this,t,n);return"Until"!==e.slice(-5)&&(r=n),r&&"string"==typeof r&&(i=w.filter(r,i)),this.length>1&&(O[e]||w.uniqueSort(i),H.test(e)&&i.reverse()),this.pushStack(i)}});var M=/[^\x20\t\r\n\f]+/g;function R(e){var t={};return w.each(e.match(M)||[],function(e,n){t[n]=!0}),t}w.Callbacks=function(e){e="string"==typeof e?R(e):w.extend({},e);var t,n,r,i,o=[],a=[],s=-1,u=function(){for(i=i||e.once,r=t=!0;a.length;s=-1){n=a.shift();while(++s-1)o.splice(n,1),n<=s&&s--}),this},has:function(e){return e?w.inArray(e,o)>-1:o.length>0},empty:function(){return o&&(o=[]),this},disable:function(){return i=a=[],o=n="",this},disabled:function(){return!o},lock:function(){return i=a=[],n||t||(o=n=""),this},locked:function(){return!!i},fireWith:function(e,n){return i||(n=[e,(n=n||[]).slice?n.slice():n],a.push(n),t||u()),this},fire:function(){return l.fireWith(this,arguments),this},fired:function(){return!!r}};return l};function I(e){return e}function W(e){throw e}function $(e,t,n,r){var i;try{e&&g(i=e.promise)?i.call(e).done(t).fail(n):e&&g(i=e.then)?i.call(e,t,n):t.apply(void 0,[e].slice(r))}catch(e){n.apply(void 0,[e])}}w.extend({Deferred:function(t){var n=[["notify","progress",w.Callbacks("memory"),w.Callbacks("memory"),2],["resolve","done",w.Callbacks("once memory"),w.Callbacks("once memory"),0,"resolved"],["reject","fail",w.Callbacks("once memory"),w.Callbacks("once memory"),1,"rejected"]],r="pending",i={state:function(){return r},always:function(){return o.done(arguments).fail(arguments),this},"catch":function(e){return i.then(null,e)},pipe:function(){var e=arguments;return w.Deferred(function(t){w.each(n,function(n,r){var i=g(e[r[4]])&&e[r[4]];o[r[1]](function(){var e=i&&i.apply(this,arguments);e&&g(e.promise)?e.promise().progress(t.notify).done(t.resolve).fail(t.reject):t[r[0]+"With"](this,i?[e]:arguments)})}),e=null}).promise()},then:function(t,r,i){var o=0;function a(t,n,r,i){return function(){var s=this,u=arguments,l=function(){var e,l;if(!(t=o&&(r!==W&&(s=void 0,u=[e]),n.rejectWith(s,u))}};t?c():(w.Deferred.getStackHook&&(c.stackTrace=w.Deferred.getStackHook()),e.setTimeout(c))}}return w.Deferred(function(e){n[0][3].add(a(0,e,g(i)?i:I,e.notifyWith)),n[1][3].add(a(0,e,g(t)?t:I)),n[2][3].add(a(0,e,g(r)?r:W))}).promise()},promise:function(e){return null!=e?w.extend(e,i):i}},o={};return w.each(n,function(e,t){var a=t[2],s=t[5];i[t[1]]=a.add,s&&a.add(function(){r=s},n[3-e][2].disable,n[3-e][3].disable,n[0][2].lock,n[0][3].lock),a.add(t[3].fire),o[t[0]]=function(){return o[t[0]+"With"](this===o?void 0:this,arguments),this},o[t[0]+"With"]=a.fireWith}),i.promise(o),t&&t.call(o,o),o},when:function(e){var t=arguments.length,n=t,r=Array(n),i=o.call(arguments),a=w.Deferred(),s=function(e){return function(n){r[e]=this,i[e]=arguments.length>1?o.call(arguments):n,--t||a.resolveWith(r,i)}};if(t<=1&&($(e,a.done(s(n)).resolve,a.reject,!t),"pending"===a.state()||g(i[n]&&i[n].then)))return a.then();while(n--)$(i[n],s(n),a.reject);return a.promise()}});var B=/^(Eval|Internal|Range|Reference|Syntax|Type|URI)Error$/;w.Deferred.exceptionHook=function(t,n){e.console&&e.console.warn&&t&&B.test(t.name)&&e.console.warn("jQuery.Deferred exception: "+t.message,t.stack,n)},w.readyException=function(t){e.setTimeout(function(){throw t})};var F=w.Deferred();w.fn.ready=function(e){return F.then(e)["catch"](function(e){w.readyException(e)}),this},w.extend({isReady:!1,readyWait:1,ready:function(e){(!0===e?--w.readyWait:w.isReady)||(w.isReady=!0,!0!==e&&--w.readyWait>0||F.resolveWith(r,[w]))}}),w.ready.then=F.then;function _(){r.removeEventListener("DOMContentLoaded",_),e.removeEventListener("load",_),w.ready()}"complete"===r.readyState||"loading"!==r.readyState&&!r.documentElement.doScroll?e.setTimeout(w.ready):(r.addEventListener("DOMContentLoaded",_),e.addEventListener("load",_));var z=function(e,t,n,r,i,o,a){var s=0,u=e.length,l=null==n;if("object"===x(n)){i=!0;for(s in n)z(e,t,s,n[s],!0,o,a)}else if(void 0!==r&&(i=!0,g(r)||(a=!0),l&&(a?(t.call(e,r),t=null):(l=t,t=function(e,t,n){return l.call(w(e),n)})),t))for(;s1,null,!0)},removeData:function(e){return this.each(function(){K.remove(this,e)})}}),w.extend({queue:function(e,t,n){var r;if(e)return t=(t||"fx")+"queue",r=J.get(e,t),n&&(!r||Array.isArray(n)?r=J.access(e,t,w.makeArray(n)):r.push(n)),r||[]},dequeue:function(e,t){t=t||"fx";var n=w.queue(e,t),r=n.length,i=n.shift(),o=w._queueHooks(e,t),a=function(){w.dequeue(e,t)};"inprogress"===i&&(i=n.shift(),r--),i&&("fx"===t&&n.unshift("inprogress"),delete o.stop,i.call(e,a,o)),!r&&o&&o.empty.fire()},_queueHooks:function(e,t){var n=t+"queueHooks";return J.get(e,n)||J.access(e,n,{empty:w.Callbacks("once memory").add(function(){J.remove(e,[t+"queue",n])})})}}),w.fn.extend({queue:function(e,t){var n=2;return"string"!=typeof e&&(t=e,e="fx",n--),arguments.length\x20\t\r\n\f]+)/i,he=/^$|^module$|\/(?:java|ecma)script/i,ge={option:[1,""],thead:[1,"","
"],col:[2,"","
"],tr:[2,"","
"],td:[3,"","
"],_default:[0,"",""]};ge.optgroup=ge.option,ge.tbody=ge.tfoot=ge.colgroup=ge.caption=ge.thead,ge.th=ge.td;function ye(e,t){var n;return n="undefined"!=typeof e.getElementsByTagName?e.getElementsByTagName(t||"*"):"undefined"!=typeof e.querySelectorAll?e.querySelectorAll(t||"*"):[],void 0===t||t&&N(e,t)?w.merge([e],n):n}function ve(e,t){for(var n=0,r=e.length;n-1)i&&i.push(o);else if(l=w.contains(o.ownerDocument,o),a=ye(f.appendChild(o),"script"),l&&ve(a),n){c=0;while(o=a[c++])he.test(o.type||"")&&n.push(o)}return f}!function(){var e=r.createDocumentFragment().appendChild(r.createElement("div")),t=r.createElement("input");t.setAttribute("type","radio"),t.setAttribute("checked","checked"),t.setAttribute("name","t"),e.appendChild(t),h.checkClone=e.cloneNode(!0).cloneNode(!0).lastChild.checked,e.innerHTML="",h.noCloneChecked=!!e.cloneNode(!0).lastChild.defaultValue}();var be=r.documentElement,we=/^key/,Te=/^(?:mouse|pointer|contextmenu|drag|drop)|click/,Ce=/^([^.]*)(?:\.(.+)|)/;function Ee(){return!0}function ke(){return!1}function Se(){try{return r.activeElement}catch(e){}}function De(e,t,n,r,i,o){var a,s;if("object"==typeof t){"string"!=typeof n&&(r=r||n,n=void 0);for(s in t)De(e,s,n,r,t[s],o);return e}if(null==r&&null==i?(i=n,r=n=void 0):null==i&&("string"==typeof n?(i=r,r=void 0):(i=r,r=n,n=void 0)),!1===i)i=ke;else if(!i)return e;return 1===o&&(a=i,(i=function(e){return w().off(e),a.apply(this,arguments)}).guid=a.guid||(a.guid=w.guid++)),e.each(function(){w.event.add(this,t,i,r,n)})}w.event={global:{},add:function(e,t,n,r,i){var o,a,s,u,l,c,f,p,d,h,g,y=J.get(e);if(y){n.handler&&(n=(o=n).handler,i=o.selector),i&&w.find.matchesSelector(be,i),n.guid||(n.guid=w.guid++),(u=y.events)||(u=y.events={}),(a=y.handle)||(a=y.handle=function(t){return"undefined"!=typeof w&&w.event.triggered!==t.type?w.event.dispatch.apply(e,arguments):void 0}),l=(t=(t||"").match(M)||[""]).length;while(l--)d=g=(s=Ce.exec(t[l])||[])[1],h=(s[2]||"").split(".").sort(),d&&(f=w.event.special[d]||{},d=(i?f.delegateType:f.bindType)||d,f=w.event.special[d]||{},c=w.extend({type:d,origType:g,data:r,handler:n,guid:n.guid,selector:i,needsContext:i&&w.expr.match.needsContext.test(i),namespace:h.join(".")},o),(p=u[d])||((p=u[d]=[]).delegateCount=0,f.setup&&!1!==f.setup.call(e,r,h,a)||e.addEventListener&&e.addEventListener(d,a)),f.add&&(f.add.call(e,c),c.handler.guid||(c.handler.guid=n.guid)),i?p.splice(p.delegateCount++,0,c):p.push(c),w.event.global[d]=!0)}},remove:function(e,t,n,r,i){var o,a,s,u,l,c,f,p,d,h,g,y=J.hasData(e)&&J.get(e);if(y&&(u=y.events)){l=(t=(t||"").match(M)||[""]).length;while(l--)if(s=Ce.exec(t[l])||[],d=g=s[1],h=(s[2]||"").split(".").sort(),d){f=w.event.special[d]||{},p=u[d=(r?f.delegateType:f.bindType)||d]||[],s=s[2]&&new RegExp("(^|\\.)"+h.join("\\.(?:.*\\.|)")+"(\\.|$)"),a=o=p.length;while(o--)c=p[o],!i&&g!==c.origType||n&&n.guid!==c.guid||s&&!s.test(c.namespace)||r&&r!==c.selector&&("**"!==r||!c.selector)||(p.splice(o,1),c.selector&&p.delegateCount--,f.remove&&f.remove.call(e,c));a&&!p.length&&(f.teardown&&!1!==f.teardown.call(e,h,y.handle)||w.removeEvent(e,d,y.handle),delete u[d])}else for(d in u)w.event.remove(e,d+t[l],n,r,!0);w.isEmptyObject(u)&&J.remove(e,"handle events")}},dispatch:function(e){var t=w.event.fix(e),n,r,i,o,a,s,u=new Array(arguments.length),l=(J.get(this,"events")||{})[t.type]||[],c=w.event.special[t.type]||{};for(u[0]=t,n=1;n=1))for(;l!==this;l=l.parentNode||this)if(1===l.nodeType&&("click"!==e.type||!0!==l.disabled)){for(o=[],a={},n=0;n-1:w.find(i,this,null,[l]).length),a[i]&&o.push(r);o.length&&s.push({elem:l,handlers:o})}return l=this,u\x20\t\r\n\f]*)[^>]*)\/>/gi,Ae=/\s*$/g;function Le(e,t){return N(e,"table")&&N(11!==t.nodeType?t:t.firstChild,"tr")?w(e).children("tbody")[0]||e:e}function He(e){return e.type=(null!==e.getAttribute("type"))+"/"+e.type,e}function Oe(e){return"true/"===(e.type||"").slice(0,5)?e.type=e.type.slice(5):e.removeAttribute("type"),e}function Pe(e,t){var n,r,i,o,a,s,u,l;if(1===t.nodeType){if(J.hasData(e)&&(o=J.access(e),a=J.set(t,o),l=o.events)){delete a.handle,a.events={};for(i in l)for(n=0,r=l[i].length;n1&&"string"==typeof y&&!h.checkClone&&je.test(y))return e.each(function(i){var o=e.eq(i);v&&(t[0]=y.call(this,i,o.html())),Re(o,t,n,r)});if(p&&(i=xe(t,e[0].ownerDocument,!1,e,r),o=i.firstChild,1===i.childNodes.length&&(i=o),o||r)){for(u=(s=w.map(ye(i,"script"),He)).length;f")},clone:function(e,t,n){var r,i,o,a,s=e.cloneNode(!0),u=w.contains(e.ownerDocument,e);if(!(h.noCloneChecked||1!==e.nodeType&&11!==e.nodeType||w.isXMLDoc(e)))for(a=ye(s),r=0,i=(o=ye(e)).length;r0&&ve(a,!u&&ye(e,"script")),s},cleanData:function(e){for(var t,n,r,i=w.event.special,o=0;void 0!==(n=e[o]);o++)if(Y(n)){if(t=n[J.expando]){if(t.events)for(r in t.events)i[r]?w.event.remove(n,r):w.removeEvent(n,r,t.handle);n[J.expando]=void 0}n[K.expando]&&(n[K.expando]=void 0)}}}),w.fn.extend({detach:function(e){return Ie(this,e,!0)},remove:function(e){return Ie(this,e)},text:function(e){return z(this,function(e){return void 0===e?w.text(this):this.empty().each(function(){1!==this.nodeType&&11!==this.nodeType&&9!==this.nodeType||(this.textContent=e)})},null,e,arguments.length)},append:function(){return Re(this,arguments,function(e){1!==this.nodeType&&11!==this.nodeType&&9!==this.nodeType||Le(this,e).appendChild(e)})},prepend:function(){return Re(this,arguments,function(e){if(1===this.nodeType||11===this.nodeType||9===this.nodeType){var t=Le(this,e);t.insertBefore(e,t.firstChild)}})},before:function(){return Re(this,arguments,function(e){this.parentNode&&this.parentNode.insertBefore(e,this)})},after:function(){return Re(this,arguments,function(e){this.parentNode&&this.parentNode.insertBefore(e,this.nextSibling)})},empty:function(){for(var e,t=0;null!=(e=this[t]);t++)1===e.nodeType&&(w.cleanData(ye(e,!1)),e.textContent="");return this},clone:function(e,t){return e=null!=e&&e,t=null==t?e:t,this.map(function(){return w.clone(this,e,t)})},html:function(e){return z(this,function(e){var t=this[0]||{},n=0,r=this.length;if(void 0===e&&1===t.nodeType)return t.innerHTML;if("string"==typeof e&&!Ae.test(e)&&!ge[(de.exec(e)||["",""])[1].toLowerCase()]){e=w.htmlPrefilter(e);try{for(;n=0&&(u+=Math.max(0,Math.ceil(e["offset"+t[0].toUpperCase()+t.slice(1)]-o-u-s-.5))),u}function et(e,t,n){var r=$e(e),i=Fe(e,t,r),o="border-box"===w.css(e,"boxSizing",!1,r),a=o;if(We.test(i)){if(!n)return i;i="auto"}return a=a&&(h.boxSizingReliable()||i===e.style[t]),("auto"===i||!parseFloat(i)&&"inline"===w.css(e,"display",!1,r))&&(i=e["offset"+t[0].toUpperCase()+t.slice(1)],a=!0),(i=parseFloat(i)||0)+Ze(e,t,n||(o?"border":"content"),a,r,i)+"px"}w.extend({cssHooks:{opacity:{get:function(e,t){if(t){var n=Fe(e,"opacity");return""===n?"1":n}}}},cssNumber:{animationIterationCount:!0,columnCount:!0,fillOpacity:!0,flexGrow:!0,flexShrink:!0,fontWeight:!0,lineHeight:!0,opacity:!0,order:!0,orphans:!0,widows:!0,zIndex:!0,zoom:!0},cssProps:{},style:function(e,t,n,r){if(e&&3!==e.nodeType&&8!==e.nodeType&&e.style){var i,o,a,s=G(t),u=Xe.test(t),l=e.style;if(u||(t=Je(s)),a=w.cssHooks[t]||w.cssHooks[s],void 0===n)return a&&"get"in a&&void 0!==(i=a.get(e,!1,r))?i:l[t];"string"==(o=typeof n)&&(i=ie.exec(n))&&i[1]&&(n=ue(e,t,i),o="number"),null!=n&&n===n&&("number"===o&&(n+=i&&i[3]||(w.cssNumber[s]?"":"px")),h.clearCloneStyle||""!==n||0!==t.indexOf("background")||(l[t]="inherit"),a&&"set"in a&&void 0===(n=a.set(e,n,r))||(u?l.setProperty(t,n):l[t]=n))}},css:function(e,t,n,r){var i,o,a,s=G(t);return Xe.test(t)||(t=Je(s)),(a=w.cssHooks[t]||w.cssHooks[s])&&"get"in a&&(i=a.get(e,!0,n)),void 0===i&&(i=Fe(e,t,r)),"normal"===i&&t in Ve&&(i=Ve[t]),""===n||n?(o=parseFloat(i),!0===n||isFinite(o)?o||0:i):i}}),w.each(["height","width"],function(e,t){w.cssHooks[t]={get:function(e,n,r){if(n)return!ze.test(w.css(e,"display"))||e.getClientRects().length&&e.getBoundingClientRect().width?et(e,t,r):se(e,Ue,function(){return et(e,t,r)})},set:function(e,n,r){var i,o=$e(e),a="border-box"===w.css(e,"boxSizing",!1,o),s=r&&Ze(e,t,r,a,o);return a&&h.scrollboxSize()===o.position&&(s-=Math.ceil(e["offset"+t[0].toUpperCase()+t.slice(1)]-parseFloat(o[t])-Ze(e,t,"border",!1,o)-.5)),s&&(i=ie.exec(n))&&"px"!==(i[3]||"px")&&(e.style[t]=n,n=w.css(e,t)),Ke(e,n,s)}}}),w.cssHooks.marginLeft=_e(h.reliableMarginLeft,function(e,t){if(t)return(parseFloat(Fe(e,"marginLeft"))||e.getBoundingClientRect().left-se(e,{marginLeft:0},function(){return e.getBoundingClientRect().left}))+"px"}),w.each({margin:"",padding:"",border:"Width"},function(e,t){w.cssHooks[e+t]={expand:function(n){for(var r=0,i={},o="string"==typeof n?n.split(" "):[n];r<4;r++)i[e+oe[r]+t]=o[r]||o[r-2]||o[0];return i}},"margin"!==e&&(w.cssHooks[e+t].set=Ke)}),w.fn.extend({css:function(e,t){return z(this,function(e,t,n){var r,i,o={},a=0;if(Array.isArray(t)){for(r=$e(e),i=t.length;a1)}});function tt(e,t,n,r,i){return new tt.prototype.init(e,t,n,r,i)}w.Tween=tt,tt.prototype={constructor:tt,init:function(e,t,n,r,i,o){this.elem=e,this.prop=n,this.easing=i||w.easing._default,this.options=t,this.start=this.now=this.cur(),this.end=r,this.unit=o||(w.cssNumber[n]?"":"px")},cur:function(){var e=tt.propHooks[this.prop];return e&&e.get?e.get(this):tt.propHooks._default.get(this)},run:function(e){var t,n=tt.propHooks[this.prop];return this.options.duration?this.pos=t=w.easing[this.easing](e,this.options.duration*e,0,1,this.options.duration):this.pos=t=e,this.now=(this.end-this.start)*t+this.start,this.options.step&&this.options.step.call(this.elem,this.now,this),n&&n.set?n.set(this):tt.propHooks._default.set(this),this}},tt.prototype.init.prototype=tt.prototype,tt.propHooks={_default:{get:function(e){var t;return 1!==e.elem.nodeType||null!=e.elem[e.prop]&&null==e.elem.style[e.prop]?e.elem[e.prop]:(t=w.css(e.elem,e.prop,""))&&"auto"!==t?t:0},set:function(e){w.fx.step[e.prop]?w.fx.step[e.prop](e):1!==e.elem.nodeType||null==e.elem.style[w.cssProps[e.prop]]&&!w.cssHooks[e.prop]?e.elem[e.prop]=e.now:w.style(e.elem,e.prop,e.now+e.unit)}}},tt.propHooks.scrollTop=tt.propHooks.scrollLeft={set:function(e){e.elem.nodeType&&e.elem.parentNode&&(e.elem[e.prop]=e.now)}},w.easing={linear:function(e){return e},swing:function(e){return.5-Math.cos(e*Math.PI)/2},_default:"swing"},w.fx=tt.prototype.init,w.fx.step={};var nt,rt,it=/^(?:toggle|show|hide)$/,ot=/queueHooks$/;function at(){rt&&(!1===r.hidden&&e.requestAnimationFrame?e.requestAnimationFrame(at):e.setTimeout(at,w.fx.interval),w.fx.tick())}function st(){return e.setTimeout(function(){nt=void 0}),nt=Date.now()}function ut(e,t){var n,r=0,i={height:e};for(t=t?1:0;r<4;r+=2-t)i["margin"+(n=oe[r])]=i["padding"+n]=e;return t&&(i.opacity=i.width=e),i}function lt(e,t,n){for(var r,i=(pt.tweeners[t]||[]).concat(pt.tweeners["*"]),o=0,a=i.length;o1)},removeAttr:function(e){return this.each(function(){w.removeAttr(this,e)})}}),w.extend({attr:function(e,t,n){var r,i,o=e.nodeType;if(3!==o&&8!==o&&2!==o)return"undefined"==typeof e.getAttribute?w.prop(e,t,n):(1===o&&w.isXMLDoc(e)||(i=w.attrHooks[t.toLowerCase()]||(w.expr.match.bool.test(t)?dt:void 0)),void 0!==n?null===n?void w.removeAttr(e,t):i&&"set"in i&&void 0!==(r=i.set(e,n,t))?r:(e.setAttribute(t,n+""),n):i&&"get"in i&&null!==(r=i.get(e,t))?r:null==(r=w.find.attr(e,t))?void 0:r)},attrHooks:{type:{set:function(e,t){if(!h.radioValue&&"radio"===t&&N(e,"input")){var n=e.value;return e.setAttribute("type",t),n&&(e.value=n),t}}}},removeAttr:function(e,t){var n,r=0,i=t&&t.match(M);if(i&&1===e.nodeType)while(n=i[r++])e.removeAttribute(n)}}),dt={set:function(e,t,n){return!1===t?w.removeAttr(e,n):e.setAttribute(n,n),n}},w.each(w.expr.match.bool.source.match(/\w+/g),function(e,t){var n=ht[t]||w.find.attr;ht[t]=function(e,t,r){var i,o,a=t.toLowerCase();return r||(o=ht[a],ht[a]=i,i=null!=n(e,t,r)?a:null,ht[a]=o),i}});var gt=/^(?:input|select|textarea|button)$/i,yt=/^(?:a|area)$/i;w.fn.extend({prop:function(e,t){return z(this,w.prop,e,t,arguments.length>1)},removeProp:function(e){return this.each(function(){delete this[w.propFix[e]||e]})}}),w.extend({prop:function(e,t,n){var r,i,o=e.nodeType;if(3!==o&&8!==o&&2!==o)return 1===o&&w.isXMLDoc(e)||(t=w.propFix[t]||t,i=w.propHooks[t]),void 0!==n?i&&"set"in i&&void 0!==(r=i.set(e,n,t))?r:e[t]=n:i&&"get"in i&&null!==(r=i.get(e,t))?r:e[t]},propHooks:{tabIndex:{get:function(e){var t=w.find.attr(e,"tabindex");return t?parseInt(t,10):gt.test(e.nodeName)||yt.test(e.nodeName)&&e.href?0:-1}}},propFix:{"for":"htmlFor","class":"className"}}),h.optSelected||(w.propHooks.selected={get:function(e){var t=e.parentNode;return t&&t.parentNode&&t.parentNode.selectedIndex,null},set:function(e){var t=e.parentNode;t&&(t.selectedIndex,t.parentNode&&t.parentNode.selectedIndex)}}),w.each(["tabIndex","readOnly","maxLength","cellSpacing","cellPadding","rowSpan","colSpan","useMap","frameBorder","contentEditable"],function(){w.propFix[this.toLowerCase()]=this});function vt(e){return(e.match(M)||[]).join(" ")}function mt(e){return e.getAttribute&&e.getAttribute("class")||""}function xt(e){return Array.isArray(e)?e:"string"==typeof e?e.match(M)||[]:[]}w.fn.extend({addClass:function(e){var t,n,r,i,o,a,s,u=0;if(g(e))return this.each(function(t){w(this).addClass(e.call(this,t,mt(this)))});if((t=xt(e)).length)while(n=this[u++])if(i=mt(n),r=1===n.nodeType&&" "+vt(i)+" "){a=0;while(o=t[a++])r.indexOf(" "+o+" ")<0&&(r+=o+" ");i!==(s=vt(r))&&n.setAttribute("class",s)}return this},removeClass:function(e){var t,n,r,i,o,a,s,u=0;if(g(e))return this.each(function(t){w(this).removeClass(e.call(this,t,mt(this)))});if(!arguments.length)return this.attr("class","");if((t=xt(e)).length)while(n=this[u++])if(i=mt(n),r=1===n.nodeType&&" "+vt(i)+" "){a=0;while(o=t[a++])while(r.indexOf(" "+o+" ")>-1)r=r.replace(" "+o+" "," ");i!==(s=vt(r))&&n.setAttribute("class",s)}return this},toggleClass:function(e,t){var n=typeof e,r="string"===n||Array.isArray(e);return"boolean"==typeof t&&r?t?this.addClass(e):this.removeClass(e):g(e)?this.each(function(n){w(this).toggleClass(e.call(this,n,mt(this),t),t)}):this.each(function(){var t,i,o,a;if(r){i=0,o=w(this),a=xt(e);while(t=a[i++])o.hasClass(t)?o.removeClass(t):o.addClass(t)}else void 0!==e&&"boolean"!==n||((t=mt(this))&&J.set(this,"__className__",t),this.setAttribute&&this.setAttribute("class",t||!1===e?"":J.get(this,"__className__")||""))})},hasClass:function(e){var t,n,r=0;t=" "+e+" ";while(n=this[r++])if(1===n.nodeType&&(" "+vt(mt(n))+" ").indexOf(t)>-1)return!0;return!1}});var bt=/\r/g;w.fn.extend({val:function(e){var t,n,r,i=this[0];{if(arguments.length)return r=g(e),this.each(function(n){var i;1===this.nodeType&&(null==(i=r?e.call(this,n,w(this).val()):e)?i="":"number"==typeof i?i+="":Array.isArray(i)&&(i=w.map(i,function(e){return null==e?"":e+""})),(t=w.valHooks[this.type]||w.valHooks[this.nodeName.toLowerCase()])&&"set"in t&&void 0!==t.set(this,i,"value")||(this.value=i))});if(i)return(t=w.valHooks[i.type]||w.valHooks[i.nodeName.toLowerCase()])&&"get"in t&&void 0!==(n=t.get(i,"value"))?n:"string"==typeof(n=i.value)?n.replace(bt,""):null==n?"":n}}}),w.extend({valHooks:{option:{get:function(e){var t=w.find.attr(e,"value");return null!=t?t:vt(w.text(e))}},select:{get:function(e){var t,n,r,i=e.options,o=e.selectedIndex,a="select-one"===e.type,s=a?null:[],u=a?o+1:i.length;for(r=o<0?u:a?o:0;r-1)&&(n=!0);return n||(e.selectedIndex=-1),o}}}}),w.each(["radio","checkbox"],function(){w.valHooks[this]={set:function(e,t){if(Array.isArray(t))return e.checked=w.inArray(w(e).val(),t)>-1}},h.checkOn||(w.valHooks[this].get=function(e){return null===e.getAttribute("value")?"on":e.value})}),h.focusin="onfocusin"in e;var wt=/^(?:focusinfocus|focusoutblur)$/,Tt=function(e){e.stopPropagation()};w.extend(w.event,{trigger:function(t,n,i,o){var a,s,u,l,c,p,d,h,v=[i||r],m=f.call(t,"type")?t.type:t,x=f.call(t,"namespace")?t.namespace.split("."):[];if(s=h=u=i=i||r,3!==i.nodeType&&8!==i.nodeType&&!wt.test(m+w.event.triggered)&&(m.indexOf(".")>-1&&(m=(x=m.split(".")).shift(),x.sort()),c=m.indexOf(":")<0&&"on"+m,t=t[w.expando]?t:new w.Event(m,"object"==typeof t&&t),t.isTrigger=o?2:3,t.namespace=x.join("."),t.rnamespace=t.namespace?new RegExp("(^|\\.)"+x.join("\\.(?:.*\\.|)")+"(\\.|$)"):null,t.result=void 0,t.target||(t.target=i),n=null==n?[t]:w.makeArray(n,[t]),d=w.event.special[m]||{},o||!d.trigger||!1!==d.trigger.apply(i,n))){if(!o&&!d.noBubble&&!y(i)){for(l=d.delegateType||m,wt.test(l+m)||(s=s.parentNode);s;s=s.parentNode)v.push(s),u=s;u===(i.ownerDocument||r)&&v.push(u.defaultView||u.parentWindow||e)}a=0;while((s=v[a++])&&!t.isPropagationStopped())h=s,t.type=a>1?l:d.bindType||m,(p=(J.get(s,"events")||{})[t.type]&&J.get(s,"handle"))&&p.apply(s,n),(p=c&&s[c])&&p.apply&&Y(s)&&(t.result=p.apply(s,n),!1===t.result&&t.preventDefault());return t.type=m,o||t.isDefaultPrevented()||d._default&&!1!==d._default.apply(v.pop(),n)||!Y(i)||c&&g(i[m])&&!y(i)&&((u=i[c])&&(i[c]=null),w.event.triggered=m,t.isPropagationStopped()&&h.addEventListener(m,Tt),i[m](),t.isPropagationStopped()&&h.removeEventListener(m,Tt),w.event.triggered=void 0,u&&(i[c]=u)),t.result}},simulate:function(e,t,n){var r=w.extend(new w.Event,n,{type:e,isSimulated:!0});w.event.trigger(r,null,t)}}),w.fn.extend({trigger:function(e,t){return this.each(function(){w.event.trigger(e,t,this)})},triggerHandler:function(e,t){var n=this[0];if(n)return w.event.trigger(e,t,n,!0)}}),h.focusin||w.each({focus:"focusin",blur:"focusout"},function(e,t){var n=function(e){w.event.simulate(t,e.target,w.event.fix(e))};w.event.special[t]={setup:function(){var r=this.ownerDocument||this,i=J.access(r,t);i||r.addEventListener(e,n,!0),J.access(r,t,(i||0)+1)},teardown:function(){var r=this.ownerDocument||this,i=J.access(r,t)-1;i?J.access(r,t,i):(r.removeEventListener(e,n,!0),J.remove(r,t))}}});var Ct=e.location,Et=Date.now(),kt=/\?/;w.parseXML=function(t){var n;if(!t||"string"!=typeof t)return null;try{n=(new e.DOMParser).parseFromString(t,"text/xml")}catch(e){n=void 0}return n&&!n.getElementsByTagName("parsererror").length||w.error("Invalid XML: "+t),n};var St=/\[\]$/,Dt=/\r?\n/g,Nt=/^(?:submit|button|image|reset|file)$/i,At=/^(?:input|select|textarea|keygen)/i;function jt(e,t,n,r){var i;if(Array.isArray(t))w.each(t,function(t,i){n||St.test(e)?r(e,i):jt(e+"["+("object"==typeof i&&null!=i?t:"")+"]",i,n,r)});else if(n||"object"!==x(t))r(e,t);else for(i in t)jt(e+"["+i+"]",t[i],n,r)}w.param=function(e,t){var n,r=[],i=function(e,t){var n=g(t)?t():t;r[r.length]=encodeURIComponent(e)+"="+encodeURIComponent(null==n?"":n)};if(Array.isArray(e)||e.jquery&&!w.isPlainObject(e))w.each(e,function(){i(this.name,this.value)});else for(n in e)jt(n,e[n],t,i);return r.join("&")},w.fn.extend({serialize:function(){return w.param(this.serializeArray())},serializeArray:function(){return this.map(function(){var e=w.prop(this,"elements");return e?w.makeArray(e):this}).filter(function(){var e=this.type;return this.name&&!w(this).is(":disabled")&&At.test(this.nodeName)&&!Nt.test(e)&&(this.checked||!pe.test(e))}).map(function(e,t){var n=w(this).val();return null==n?null:Array.isArray(n)?w.map(n,function(e){return{name:t.name,value:e.replace(Dt,"\r\n")}}):{name:t.name,value:n.replace(Dt,"\r\n")}}).get()}});var qt=/%20/g,Lt=/#.*$/,Ht=/([?&])_=[^&]*/,Ot=/^(.*?):[ \t]*([^\r\n]*)$/gm,Pt=/^(?:about|app|app-storage|.+-extension|file|res|widget):$/,Mt=/^(?:GET|HEAD)$/,Rt=/^\/\//,It={},Wt={},$t="*/".concat("*"),Bt=r.createElement("a");Bt.href=Ct.href;function Ft(e){return function(t,n){"string"!=typeof t&&(n=t,t="*");var r,i=0,o=t.toLowerCase().match(M)||[];if(g(n))while(r=o[i++])"+"===r[0]?(r=r.slice(1)||"*",(e[r]=e[r]||[]).unshift(n)):(e[r]=e[r]||[]).push(n)}}function _t(e,t,n,r){var i={},o=e===Wt;function a(s){var u;return i[s]=!0,w.each(e[s]||[],function(e,s){var l=s(t,n,r);return"string"!=typeof l||o||i[l]?o?!(u=l):void 0:(t.dataTypes.unshift(l),a(l),!1)}),u}return a(t.dataTypes[0])||!i["*"]&&a("*")}function zt(e,t){var n,r,i=w.ajaxSettings.flatOptions||{};for(n in t)void 0!==t[n]&&((i[n]?e:r||(r={}))[n]=t[n]);return r&&w.extend(!0,e,r),e}function Xt(e,t,n){var r,i,o,a,s=e.contents,u=e.dataTypes;while("*"===u[0])u.shift(),void 0===r&&(r=e.mimeType||t.getResponseHeader("Content-Type"));if(r)for(i in s)if(s[i]&&s[i].test(r)){u.unshift(i);break}if(u[0]in n)o=u[0];else{for(i in n){if(!u[0]||e.converters[i+" "+u[0]]){o=i;break}a||(a=i)}o=o||a}if(o)return o!==u[0]&&u.unshift(o),n[o]}function Ut(e,t,n,r){var i,o,a,s,u,l={},c=e.dataTypes.slice();if(c[1])for(a in e.converters)l[a.toLowerCase()]=e.converters[a];o=c.shift();while(o)if(e.responseFields[o]&&(n[e.responseFields[o]]=t),!u&&r&&e.dataFilter&&(t=e.dataFilter(t,e.dataType)),u=o,o=c.shift())if("*"===o)o=u;else if("*"!==u&&u!==o){if(!(a=l[u+" "+o]||l["* "+o]))for(i in l)if((s=i.split(" "))[1]===o&&(a=l[u+" "+s[0]]||l["* "+s[0]])){!0===a?a=l[i]:!0!==l[i]&&(o=s[0],c.unshift(s[1]));break}if(!0!==a)if(a&&e["throws"])t=a(t);else try{t=a(t)}catch(e){return{state:"parsererror",error:a?e:"No conversion from "+u+" to "+o}}}return{state:"success",data:t}}w.extend({active:0,lastModified:{},etag:{},ajaxSettings:{url:Ct.href,type:"GET",isLocal:Pt.test(Ct.protocol),global:!0,processData:!0,async:!0,contentType:"application/x-www-form-urlencoded; charset=UTF-8",accepts:{"*":$t,text:"text/plain",html:"text/html",xml:"application/xml, text/xml",json:"application/json, text/javascript"},contents:{xml:/\bxml\b/,html:/\bhtml/,json:/\bjson\b/},responseFields:{xml:"responseXML",text:"responseText",json:"responseJSON"},converters:{"* text":String,"text html":!0,"text json":JSON.parse,"text xml":w.parseXML},flatOptions:{url:!0,context:!0}},ajaxSetup:function(e,t){return t?zt(zt(e,w.ajaxSettings),t):zt(w.ajaxSettings,e)},ajaxPrefilter:Ft(It),ajaxTransport:Ft(Wt),ajax:function(t,n){"object"==typeof t&&(n=t,t=void 0),n=n||{};var i,o,a,s,u,l,c,f,p,d,h=w.ajaxSetup({},n),g=h.context||h,y=h.context&&(g.nodeType||g.jquery)?w(g):w.event,v=w.Deferred(),m=w.Callbacks("once memory"),x=h.statusCode||{},b={},T={},C="canceled",E={readyState:0,getResponseHeader:function(e){var t;if(c){if(!s){s={};while(t=Ot.exec(a))s[t[1].toLowerCase()]=t[2]}t=s[e.toLowerCase()]}return null==t?null:t},getAllResponseHeaders:function(){return c?a:null},setRequestHeader:function(e,t){return null==c&&(e=T[e.toLowerCase()]=T[e.toLowerCase()]||e,b[e]=t),this},overrideMimeType:function(e){return null==c&&(h.mimeType=e),this},statusCode:function(e){var t;if(e)if(c)E.always(e[E.status]);else for(t in e)x[t]=[x[t],e[t]];return this},abort:function(e){var t=e||C;return i&&i.abort(t),k(0,t),this}};if(v.promise(E),h.url=((t||h.url||Ct.href)+"").replace(Rt,Ct.protocol+"//"),h.type=n.method||n.type||h.method||h.type,h.dataTypes=(h.dataType||"*").toLowerCase().match(M)||[""],null==h.crossDomain){l=r.createElement("a");try{l.href=h.url,l.href=l.href,h.crossDomain=Bt.protocol+"//"+Bt.host!=l.protocol+"//"+l.host}catch(e){h.crossDomain=!0}}if(h.data&&h.processData&&"string"!=typeof h.data&&(h.data=w.param(h.data,h.traditional)),_t(It,h,n,E),c)return E;(f=w.event&&h.global)&&0==w.active++&&w.event.trigger("ajaxStart"),h.type=h.type.toUpperCase(),h.hasContent=!Mt.test(h.type),o=h.url.replace(Lt,""),h.hasContent?h.data&&h.processData&&0===(h.contentType||"").indexOf("application/x-www-form-urlencoded")&&(h.data=h.data.replace(qt,"+")):(d=h.url.slice(o.length),h.data&&(h.processData||"string"==typeof h.data)&&(o+=(kt.test(o)?"&":"?")+h.data,delete h.data),!1===h.cache&&(o=o.replace(Ht,"$1"),d=(kt.test(o)?"&":"?")+"_="+Et+++d),h.url=o+d),h.ifModified&&(w.lastModified[o]&&E.setRequestHeader("If-Modified-Since",w.lastModified[o]),w.etag[o]&&E.setRequestHeader("If-None-Match",w.etag[o])),(h.data&&h.hasContent&&!1!==h.contentType||n.contentType)&&E.setRequestHeader("Content-Type",h.contentType),E.setRequestHeader("Accept",h.dataTypes[0]&&h.accepts[h.dataTypes[0]]?h.accepts[h.dataTypes[0]]+("*"!==h.dataTypes[0]?", "+$t+"; q=0.01":""):h.accepts["*"]);for(p in h.headers)E.setRequestHeader(p,h.headers[p]);if(h.beforeSend&&(!1===h.beforeSend.call(g,E,h)||c))return E.abort();if(C="abort",m.add(h.complete),E.done(h.success),E.fail(h.error),i=_t(Wt,h,n,E)){if(E.readyState=1,f&&y.trigger("ajaxSend",[E,h]),c)return E;h.async&&h.timeout>0&&(u=e.setTimeout(function(){E.abort("timeout")},h.timeout));try{c=!1,i.send(b,k)}catch(e){if(c)throw e;k(-1,e)}}else k(-1,"No Transport");function k(t,n,r,s){var l,p,d,b,T,C=n;c||(c=!0,u&&e.clearTimeout(u),i=void 0,a=s||"",E.readyState=t>0?4:0,l=t>=200&&t<300||304===t,r&&(b=Xt(h,E,r)),b=Ut(h,b,E,l),l?(h.ifModified&&((T=E.getResponseHeader("Last-Modified"))&&(w.lastModified[o]=T),(T=E.getResponseHeader("etag"))&&(w.etag[o]=T)),204===t||"HEAD"===h.type?C="nocontent":304===t?C="notmodified":(C=b.state,p=b.data,l=!(d=b.error))):(d=C,!t&&C||(C="error",t<0&&(t=0))),E.status=t,E.statusText=(n||C)+"",l?v.resolveWith(g,[p,C,E]):v.rejectWith(g,[E,C,d]),E.statusCode(x),x=void 0,f&&y.trigger(l?"ajaxSuccess":"ajaxError",[E,h,l?p:d]),m.fireWith(g,[E,C]),f&&(y.trigger("ajaxComplete",[E,h]),--w.active||w.event.trigger("ajaxStop")))}return E},getJSON:function(e,t,n){return w.get(e,t,n,"json")},getScript:function(e,t){return w.get(e,void 0,t,"script")}}),w.each(["get","post"],function(e,t){w[t]=function(e,n,r,i){return g(n)&&(i=i||r,r=n,n=void 0),w.ajax(w.extend({url:e,type:t,dataType:i,data:n,success:r},w.isPlainObject(e)&&e))}}),w._evalUrl=function(e){return w.ajax({url:e,type:"GET",dataType:"script",cache:!0,async:!1,global:!1,"throws":!0})},w.fn.extend({wrapAll:function(e){var t;return this[0]&&(g(e)&&(e=e.call(this[0])),t=w(e,this[0].ownerDocument).eq(0).clone(!0),this[0].parentNode&&t.insertBefore(this[0]),t.map(function(){var e=this;while(e.firstElementChild)e=e.firstElementChild;return e}).append(this)),this},wrapInner:function(e){return g(e)?this.each(function(t){w(this).wrapInner(e.call(this,t))}):this.each(function(){var t=w(this),n=t.contents();n.length?n.wrapAll(e):t.append(e)})},wrap:function(e){var t=g(e);return this.each(function(n){w(this).wrapAll(t?e.call(this,n):e)})},unwrap:function(e){return this.parent(e).not("body").each(function(){w(this).replaceWith(this.childNodes)}),this}}),w.expr.pseudos.hidden=function(e){return!w.expr.pseudos.visible(e)},w.expr.pseudos.visible=function(e){return!!(e.offsetWidth||e.offsetHeight||e.getClientRects().length)},w.ajaxSettings.xhr=function(){try{return new e.XMLHttpRequest}catch(e){}};var Vt={0:200,1223:204},Gt=w.ajaxSettings.xhr();h.cors=!!Gt&&"withCredentials"in Gt,h.ajax=Gt=!!Gt,w.ajaxTransport(function(t){var n,r;if(h.cors||Gt&&!t.crossDomain)return{send:function(i,o){var a,s=t.xhr();if(s.open(t.type,t.url,t.async,t.username,t.password),t.xhrFields)for(a in t.xhrFields)s[a]=t.xhrFields[a];t.mimeType&&s.overrideMimeType&&s.overrideMimeType(t.mimeType),t.crossDomain||i["X-Requested-With"]||(i["X-Requested-With"]="XMLHttpRequest");for(a in i)s.setRequestHeader(a,i[a]);n=function(e){return function(){n&&(n=r=s.onload=s.onerror=s.onabort=s.ontimeout=s.onreadystatechange=null,"abort"===e?s.abort():"error"===e?"number"!=typeof s.status?o(0,"error"):o(s.status,s.statusText):o(Vt[s.status]||s.status,s.statusText,"text"!==(s.responseType||"text")||"string"!=typeof s.responseText?{binary:s.response}:{text:s.responseText},s.getAllResponseHeaders()))}},s.onload=n(),r=s.onerror=s.ontimeout=n("error"),void 0!==s.onabort?s.onabort=r:s.onreadystatechange=function(){4===s.readyState&&e.setTimeout(function(){n&&r()})},n=n("abort");try{s.send(t.hasContent&&t.data||null)}catch(e){if(n)throw e}},abort:function(){n&&n()}}}),w.ajaxPrefilter(function(e){e.crossDomain&&(e.contents.script=!1)}),w.ajaxSetup({accepts:{script:"text/javascript, application/javascript, application/ecmascript, application/x-ecmascript"},contents:{script:/\b(?:java|ecma)script\b/},converters:{"text script":function(e){return w.globalEval(e),e}}}),w.ajaxPrefilter("script",function(e){void 0===e.cache&&(e.cache=!1),e.crossDomain&&(e.type="GET")}),w.ajaxTransport("script",function(e){if(e.crossDomain){var t,n;return{send:function(i,o){t=w("