packages feed

crux (empty) → 0.7

raw patch · 23 files changed

+4955/−0 lines, 23 filesdep +Globdep +aesondep +ansi-terminal

Dependencies added: Glob, aeson, ansi-terminal, async, attoparsec, base, bv-sized, bytestring, config-schema, config-value, containers, contravariant, crucible, directory, filepath, generic-lens, lens, libBF, lumberjack, parameterized-utils, prettyprinter, raw-strings-qq, semigroupoids, simple-get-opt, split, terminal-size, text, time, vector, what4, xml, yaml

Files

+ LICENSE view
@@ -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.
+ crux.cabal view
@@ -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
+ src/Crux.hs view
@@ -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 "<Crux>" $ 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 "<Prove Goals>" $ 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
+ src/Crux/Config.hs view
@@ -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)
+ src/Crux/Config/Common.hs view
@@ -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-<goal number>-<solver name>.smt2,"+  , "where <goal number> is the number of the goal that was proven (starting at 0)"+  , "and <solver name> is the name of the solver used to dispatch that goal."+  ]++dflt :: String -> (String -> OptSetter opts) -> (Maybe String -> OptSetter opts)+dflt x p mb = p (fromMaybe x mb)++parseDiffTime ::+  String -> (DiffTime -> opts -> opts) -> String -> OptSetter opts+parseDiffTime thing mk =+  parsePosNum thing (\a opts -> mk (cvt a) opts)+  where cvt :: Double -> DiffTime+        cvt = fromRational . toRational++parseNominalDiffTime ::+  String -> (NominalDiffTime -> opts -> opts) -> String -> OptSetter opts+parseNominalDiffTime thing mk =+  parsePosNum thing (\a opts -> mk (cvt a) opts)+  where cvt :: Double -> NominalDiffTime+        cvt = fromRational . toRational++parsePathStrategy ::+  (PathStrategy -> opts -> opts) -> String -> OptSetter opts+parsePathStrategy mk "always-merge" opts = Right $ mk AlwaysMergePaths opts+parsePathStrategy mk "split-dfs"    opts = Right $ mk SplitAndExploreDepthFirst opts+parsePathStrategy _mk nm _opts = Left ("Unknown path strategy: " ++ show nm)
+ src/Crux/Config/Doc.hs view
@@ -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 ]
+ src/Crux/Config/Load.hs view
@@ -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
+ src/Crux/Config/Solver.hs view
@@ -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
+ src/Crux/FormatOut.hs view
@@ -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+    _ -> "<unknown>" PP.<+> PP.viaShow tpr++  allDocs = mconcat (failedDoc <$> toList allGls)++++ppToText :: PP.Doc ann -> Text.Text+ppToText = PPR.renderStrict . PP.layoutPretty PP.defaultLayoutOptions
+ src/Crux/Goal.hs view
@@ -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-<goal number>-<solver name>.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]
+ src/Crux/Log.hs view
@@ -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 '<Tool>LogMessage', similar to 'CruxLogMessage' below,+--+-- * constraint synonym 'Supports<Tool>LogMessage' similar to+-- 'SupportsCruxLogMessage' below,+--+-- * constraint dispatcher 'with<Tool>LogMessage' similar to+-- 'withCruxLogMessage' below,+--+-- * logger method 'say<Tool>' similar to 'sayCrux' below,+--+-- * default log message converter '<Tool>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
+ src/Crux/Loops.hs view
@@ -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++
+ src/Crux/Model.hs view
@@ -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))
+ src/Crux/Overrides.hs view
@@ -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+  }
+ src/Crux/ProgressBar.hs view
@@ -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)
+ src/Crux/Report.hs view
@@ -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 <script> with the contents we want.+       writeFile (outDir opts </> "report.js") $ "var goals = " ++ contents+       -- However, for some purposes, having a JSON file is more practical.+       writeFile (outDir opts </> "report.json") contents+       T.writeFile (outDir opts </> "index.html") indexHtml+       T.writeFile (outDir opts </> "jquery.min.js") jquery+++-- TODO: get the extensions from the Language configuration+-- XXX: currently we just use the file name as a label for the file,+-- but if files come from different directores this may lead to clashes,+-- so we should do something smarter (e.g., drop only the prefix that+-- is common to all files).+maybeGenerateSource :: CruxOptions -> [FilePath] -> IO ()+maybeGenerateSource opts files =+  do let exts = [".c", ".i", ".cc", ".cpp", ".cxx", ".C", ".ii", ".h", ".hpp", ".hxx", ".hh"]+         renderFiles = filter ((`elem` exts) . takeExtension) files+     h <- openFile (outDir opts </> "source.js") WriteMode+     hPutStrLn h "var sources = ["+     forM_ renderFiles $ \file -> do+       absFile <- canonicalizePath file+       txt <- readFile absFile+       hPutStr h $ "{\"label\":" ++ show (takeFileName absFile) ++ ","+       hPutStr h $ "\"name\":" ++ show absFile ++ ","+       hPutStr h $ "\"lines\":" ++ show (lines txt)+       hPutStrLn h "},"+     hPutStrLn h "]"+     hClose h+  `catch` \(SomeException {}) -> return ()+++-- | Return a list of all program locations referenced in a set of+-- proved goals.+provedGoalLocs :: ProvedGoals -> [ProgramLoc]+provedGoalLocs = concatMap Fold.toList . provedGoalTraces++-- | Return a list of all of the traces referenced in a set of proved goals.+--+-- This returns a sequence-of-sequences because a single 'ProvedGoals' can+-- involve many 'Branch'es, which mirror the branching structure of the program+-- execution that led to each individual 'ProvedGoal' or 'NotProvedGoal'.+provedGoalTraces :: ProvedGoals -> Seq (Seq ProgramLoc)+provedGoalTraces =+  \case+    Branch pgs1 pgs2 -> provedGoalTraces pgs1 <> provedGoalTraces pgs2+    ProvedGoal _ err locs _ ->+      Seq.singleton (Seq.fromList locs Seq.|> simErrorLoc err)+    NotProvedGoal _ err _ locs _ _ ->+      Seq.singleton (Seq.fromList locs Seq.|> simErrorLoc err)++-- | Return a list of all files referenced in a set of proved goals.+provedGoalFiles :: ProvedGoals -> Set.Set FilePath+provedGoalFiles = Fold.foldl' ins mempty . map plSourceLoc . provedGoalLocs+  where+    ins s (SourcePos f _ _) = Set.insert (Text.unpack f) s+    ins s (BinaryPos f _) = Set.insert (Text.unpack f) s+    ins s _ = s++renderSideConds :: CruxOptions -> [ProvedGoals] -> IO [ JS ]+renderSideConds opts = concatMapM go+  where+  concatMapM f xs = concat <$> mapM f xs++  flatBranch (Branch x y : more) = flatBranch (x : y : more)+  flatBranch (x : more)          = x : flatBranch more+  flatBranch []                  = []++  isGoal x = case x of+               ProvedGoal {} -> True+               NotProvedGoal {} -> True+               Branch{} -> False++  go gs =+    case gs of+      Branch g1 g2 ->+        let (now,rest) = partition isGoal (flatBranch [g1,g2]) in+          (++) <$> concatMapM go now <*> concatMapM go rest++      ProvedGoal asmps conc locs triv+        | skipSuccessReports opts -> pure []+        | otherwise -> jsProvedGoal locs asmps conc triv++      NotProvedGoal asmps conc explain locs cex _+        | skipIncompleteReports opts+        , SimError _ (ResourceExhausted _) <- conc+        -> pure []++        | otherwise -> jsNotProvedGoal locs asmps conc explain cex+++removeRepeats :: Eq a => [a] -> [a]+removeRepeats = removeRepeatsBy (==)++removeRepeatsBy :: (a -> a -> Bool) -> [a] -> [a]+removeRepeatsBy f = go+  where+    go [] = []+    go [x] = [x]+    go (x:y:zs)+      | f x y = go (y:zs)+      | otherwise = x : go (y:zs)++jsPath :: [ProgramLoc] -> IO [ JS ]+jsPath locs = concat <$> mapM mkStep locs'+    where+      locs'      = annotateLoops (removeRepeats locs)+      mkStep (a,l) =+       jsLoc l >>= \case+         Nothing -> return []+         Just l' ->+           return [jsObj+             [ "loop" ~> jsList (map jsNum a)+             , "loc"  ~> l'+             ]]++jsProvedGoal ::+  [ ProgramLoc ] ->+  [ CrucibleAssumption (Const ()) ] ->+  SimError ->+  Bool ->+  IO [JS]+jsProvedGoal locs asmps conc triv =+  do loc <- fromMaybe jsNull <$> jsLoc (simErrorLoc conc)+     asmps' <- mapM mkAsmp asmps+     path   <- jsPath locs+     pure [jsObj+       [ "status"          ~> jsStr "ok"+       , "goal"            ~> goalReason+       , "details-short"   ~> goalDetails+       , "location"        ~> loc+       , "assumptions"     ~> jsList asmps'+       , "trivial"         ~> jsBool triv+       , "path"            ~> jsList path+       ]]+  where+  mkAsmp asmp =+    do l <- fromMaybe jsNull <$> jsLoc (assumptionLoc asmp)+       pure $ jsObj+         [ "loc" ~> l+         , "text" ~> jsStr (show (ppAssumption (\_ -> mempty) asmp))+         ]++  goalReason  = jsStr (simErrorReasonMsg (simErrorReason conc))+  goalDetails+     | null msg  = jsNull+     | otherwise = jsStr msg+    where msg = simErrorDetailsMsg (simErrorReason conc)+++jsNotProvedGoal ::+  [ ProgramLoc ] ->+  [ CrucibleAssumption (Const ()) ] ->+  SimError ->+  Doc Void ->+  Maybe (ModelView, [CrucibleEvent GroundValueWrapper]) ->+  IO [JS]+jsNotProvedGoal locs asmps conc explain cex =+  do loc <- fromMaybe jsNull <$> jsLoc (simErrorLoc conc)+     asmps' <- mapM mkAsmp asmps+     ex <- case cex of+             Just (m,_) -> modelJS m+             _          -> pure jsNull+     path <- jsPath locs+     pure [jsObj+       [ "status"          ~> status+       , "counter-example" ~> ex+       , "goal"            ~> goalReason+       , "details-short"   ~> goalDetails+       , "location"        ~> loc+       , "assumptions"     ~> jsList asmps'+       , "trivial"         ~> jsBool False+       , "path"            ~> jsList path+       , "details-long"    ~> jsStr (show explain)+       ]]+  where+  status = case cex of+             Just _+               | ResourceExhausted _ <- simErrorReason conc -> jsStr "unknown"+               | otherwise -> jsStr "fail"+             Nothing -> jsStr "unknown"++  mkAsmp asmp =+    do l <- fromMaybe jsNull <$> jsLoc (assumptionLoc asmp)+       pure $ jsObj+         [ "loc" ~> l+         , "text" ~> jsStr (show (ppAssumption (\_ -> mempty) asmp))+         ]++  goalReason  = jsStr (simErrorReasonMsg (simErrorReason conc))+  goalDetails+     | null msg  = jsNull+     | otherwise = jsStr msg+    where msg = simErrorDetailsMsg (simErrorReason conc)
+ src/Crux/SVCOMP.hs view
@@ -0,0 +1,352 @@+-- | This module provides various helper functionality+--   for participating in the SV-COMP comptetion, including+--   parsing comptetion set files, configuration data,+--   reporting results, etc.++{-# LANGUAGE ApplicativeDo #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}+module Crux.SVCOMP where++import           Config.Schema+import           Control.Applicative+import           Data.Aeson (ToJSON)+import qualified Data.Attoparsec.Text as Atto+import           Data.Functor.Identity (Identity(..))+import           Data.Kind (Type)+import           Data.Map (Map)+import qualified Data.Map as Map+import           Data.Text (Text)+import qualified Data.Text as Text+import qualified Data.Text.IO as Text+import qualified Data.Yaml as Yaml+import           GHC.Generics (Generic)+import           System.FilePath+import qualified System.FilePath.Glob as Glob+import qualified Data.Vector as V++#if MIN_VERSION_aeson(2,0,0)+import qualified Data.Aeson.KeyMap as KM+#else+import qualified Data.HashMap.Strict as HM+#endif++import Crux.Config+import Crux.Config.Common+++data SVCOMPOptions (f :: Type -> Type) = SVCOMPOptions+  { svcompBlacklist :: [FilePath]+      -- ^ Benchmarks to skip when evaluating in SV-COMP mode++  , svcompArch :: f Arch+      -- ^ The architecture assumed for the verification task++  , svcompSpec :: f FilePath+      -- ^ The file containing the specification text used to verify the program. Likely a .prp file.++  , svcompWitnessOutput :: FilePath+      -- ^ Write the witness automaton to this filename+  }++data Arch = Arch32 | Arch64+  deriving (Show,Eq,Ord)++archSpec :: ValueSpec Arch+archSpec =+  (Arch32 <$ atomSpec "32bit") <!>+  (Arch64 <$ atomSpec "64bit")++parseArch :: (Arch -> opts -> opts) -> String -> OptSetter opts+parseArch mk = \txt opts ->+  case txt of+    "32bit" -> Right (mk Arch32 opts)+    "64bit" -> Right (mk Arch64 opts)+    _       -> Left "Invalid architecture"++-- | We cannot verify an SV-COMP program without knowing the architecture and+-- the specification. Unfortunately, Crux's command-line argument parser makes+-- it somewhat awkward to require certain arguments (without defaults). As a+-- hacky workaround, we parse the command-line arguments for the+-- architecture/specification as if they were optional and later check here to+-- see if they were actually provided, throwing an error if they were not+-- provided.+processSVCOMPOptions :: SVCOMPOptions Maybe -> IO (SVCOMPOptions Identity)+processSVCOMPOptions+    (SVCOMPOptions{ svcompArch, svcompSpec+                  , svcompBlacklist, svcompWitnessOutput}) = do+  svcompArch' <- process "svcomp-arch" svcompArch+  svcompSpec' <- process "svcomp-spec" svcompSpec+  pure $ SVCOMPOptions{ svcompArch = svcompArch', svcompSpec = svcompSpec'+                      , svcompBlacklist, svcompWitnessOutput }+  where+    process :: String -> Maybe a -> IO (Identity a)+    process optName = maybe (fail $ "A value for --" ++ optName ++ " must be provided") (pure . Identity)++svcompOptions :: Config (SVCOMPOptions Maybe)+svcompOptions = Config+  { cfgFile =+      do svcompBlacklist <-+           section "svcomp-blacklist" (listSpec stringSpec) []+           "SV-COMP benchmark tasks to skip"++         svcompArch <-+           sectionMaybe "svcomp-arch" archSpec+           "The architecture assumed for the verification task."++         svcompSpec <-+           sectionMaybe "svcomp-spec" fileSpec+           "The file containing the specification text used to verify the program. Likely a .prp file."++         svcompWitnessOutput <-+           section "svcomp-witness-output" fileSpec "witness.graphml"+           (Text.unwords [ "The file name to which the witness automaton file should be written"+                         , "(default: witness.graphml)."+                         ])++         return SVCOMPOptions{ .. }++  , cfgEnv = []++  , cfgCmdLineFlag =+      [ Option [] ["svcomp-arch"]+        "The architecture assumed for the verification task."+        $ ReqArg "`32bit` or `64bit`"+        $ parseArch+        $ \a opts -> opts{ svcompArch = Just a }++      , Option [] ["svcomp-spec"]+        "The file containing the specification text used to verify the program. Likely a .prp file."+        $ ReqArg "FILE"+        $ \f opts -> Right opts{ svcompSpec = Just f }++      , Option [] ["svcomp-witness-output"]+        (unwords [ "The file name to which the witness automaton file should be written"+                 , "(default: witness.graphml)."+                 ])+        $ ReqArg "FILE"+        $ \f opts -> Right opts{ svcompWitnessOutput = f }+      ]+  }++propertyVerdict :: VerificationTask -> Maybe Bool+propertyVerdict task = foldl f Nothing (verificationProperties task)+ where+ comb b Nothing  = Just b+ comb b (Just x) = Just $! b && x++ f v (CheckNoError _nm, Just b)  = comb b v+ f v (CheckValidFree, Just b)    = comb b v+ f v (CheckValidDeref, Just b)   = comb b v+ f v (CheckDefBehavior, Just b)  = comb b v+ f v (CheckNoOverflow, Just b)   = comb b v+ f v _ = v++data ComputedVerdict+  = Verified+  | Falsified+  | Unknown+ deriving (Eq, Generic, Ord, Show, ToJSON)++data BenchmarkSet =+  BenchmarkSet+  { benchmarkName :: Text+  , benchmarkTasks :: [VerificationTask]+  }+ deriving (Show,Eq,Ord)++data SVCompProperty+  = CheckNoError Text+  | CheckValidFree+  | CheckValidDeref+  | CheckValidMemtrack+  | CheckValidMemCleanup+  | CheckDefBehavior+  | CheckNoOverflow+  | CheckTerminates+  | CoverageFQL Text+ deriving (Show,Eq,Ord,Generic,ToJSON)++data SVCompLanguage+  = C CDataModel+  | Java+ deriving (Show,Eq,Ord)++data CDataModel = ILP32 | LP64+ deriving (Show,Eq,Ord)++data VerificationTask =+  VerificationTask+  { verificationSourceFile :: FilePath+  , verificationInputFiles :: [FilePath]+  , verificationProperties :: [(SVCompProperty, Maybe Bool)]+  , verificationLanguage   :: SVCompLanguage+  }+ deriving (Show,Eq,Ord)++checkParse :: Atto.Parser SVCompProperty+checkParse = Atto.skipSpace *> Atto.string "init(main())," *> Atto.skipSpace *> ltl+ where+ ltl = Atto.string "LTL(" *> Atto.skipSpace *> go <* Atto.skipSpace <* Atto.string ")" <* Atto.skipSpace+ go = Atto.choice+      [ CheckNoError <$> (Atto.string "G ! call(" *> bracketedText <* ")")+      , pure CheckTerminates      <* Atto.string "F end"+      , pure CheckValidFree       <* Atto.string "G valid-free"+      , pure CheckValidDeref      <* Atto.string "G valid-deref"+      , pure CheckValidMemtrack   <* Atto.string "G valid-memtrack"+      , pure CheckValidMemCleanup <* Atto.string "G valid-memcleanup"+      , pure CheckNoOverflow      <* Atto.string "G ! overflow"+      , pure CheckDefBehavior     <* Atto.string "G def-behavior"+      ]++coverParse :: Atto.Parser SVCompProperty+coverParse = CoverageFQL <$> (Atto.skipSpace *> Atto.string "init(main())," *> Atto.skipSpace *> bracketedText)++bracketedText :: Atto.Parser Text+bracketedText =+ do xs <- Atto.takeTill (\x -> x `elem` ['(',')'])+    (do _ <- Atto.char '('+        ys <- bracketedText+        _ <- Atto.char ')'+        zs <- bracketedText+        return (xs <> "(" <> ys <> ")" <> zs)+     ) <|> (return xs)+++propParse :: Atto.Parser SVCompProperty+propParse = Atto.skipSpace *> Atto.choice+  [ Atto.string "CHECK(" *> checkParse <* ")"+  , Atto.string "COVER(" *> coverParse <* ")"+  ]++loadVerificationTask :: FilePath -> IO VerificationTask+loadVerificationTask fp =+   Yaml.decodeFileEither fp >>= \case+     Left err -> fail $ unlines ["Failure parsing YAML file: " ++ show fp, show err]+     Right a  -> decodeVT a+ where+ decodeVT :: Yaml.Value -> IO VerificationTask+ decodeVT (Yaml.Object o) =+  do case lookupKM "format_version" o of+       Just (Yaml.String "2.0") -> return ()+       _ -> fail $ unwords ["Expected verification task version 2.0 while parsing", show fp]++     fs <- case lookupKM "input_files" o of+             Just v -> getStrs v+             Nothing -> fail $ unwords ["No 'input_files' section while parsing", show fp]++     ps <- case lookupKM "properties" o of+             Just v -> getProps v+             Nothing -> fail $ unwords ["No 'properties' section while parsing", show fp]++     lang <- case lookupKM "options" o of+               Just v -> getLang v+               Nothing -> fail $ unwords ["No 'options' section while parsing", show fp]++     return VerificationTask+            { verificationSourceFile = fp+            , verificationInputFiles = fs+            , verificationProperties = ps+            , verificationLanguage   = lang+            }+ decodeVT v = fail $ unwords ["Expected Yaml object but got:", show v, "when parsing", show fp]+++ decodeProp p =+   case Atto.parseOnly propParse p of+     Left msg -> fail $ unlines [ "Could not parse property:"+                                , Text.unpack p+                                , msg+                                ]++     Right p' -> return p'++ getStrs (Yaml.String f) = return [Text.unpack f]+ getStrs (Yaml.Array xs) = concat <$> V.mapM getStrs xs+ getStrs v = fail $ unwords ["expected strings, but got:", show v]++ getProp (Yaml.Object o) =+   do propf <- case lookupKM "property_file" o of+                 Just (Yaml.String f) -> return (Text.unpack f)+                 _ -> fail $ unwords ["expected string value in 'property_file' while parsing", show fp]++      prop <- decodeProp =<< Text.readFile (takeDirectory fp </> propf)++      verdict <- case lookupKM "expected_verdict" o of+                   Nothing -> return Nothing+                   Just (Yaml.Bool b) -> return (Just b)+                   Just (Yaml.String "true") -> return (Just True)+                   Just (Yaml.String "false") -> return (Just False)+                   Just _ -> fail $ unwords ["expected boolean value in 'expected_verdict' while parsing", show fp]++      return (prop, verdict)++ getProp _v = fail $ unwords ["expected object in 'properties' section when parsing", show fp]++ getProps (Yaml.Array xs) = mapM getProp (V.toList xs)+ getProps _v = fail $ unwords ["expected property array in 'properties' section when parsing", show fp]++ getLang (Yaml.Object o) =+   case lookupKM "language" o of+     Just (Yaml.String "C")    -> getCDataModel o+     Just (Yaml.String "Java") -> return Java+     _ -> fail $ unwords ["expected 'C' or 'Java' in 'language' while parsing", show fp]++ getLang _v = fail $ unwords ["expected object in 'options' section when parsing", show fp]++ getCDataModel o =+   case lookupKM "data_model" o of+     Just (Yaml.String "ILP32") -> return (C ILP32)+     Just (Yaml.String "LP64")  -> return (C LP64)+     _ -> fail $ unwords ["expected 'ILP32' or 'LP64' in 'data_model' while parsing", show fp]++ -- TODO: When the ecosystem widely uses aeson-2.0.0.0 or later, remove this CPP.+#if MIN_VERSION_aeson(2,0,0)+ lookupKM = KM.lookup+#else+ lookupKM = HM.lookup+#endif++compilePats :: [Text] -> [Glob.Pattern]+compilePats xs =+  let xs' = filter (not . Text.null) $ map Text.strip xs+   in map (Glob.compile . Text.unpack) xs'++loadSVCOMPBenchmarks :: CruxOptions -> IO [BenchmarkSet]+loadSVCOMPBenchmarks cruxOpts = mapM loadBenchmarkSet (inputFiles cruxOpts)++loadBenchmarkSet :: FilePath -> IO BenchmarkSet+loadBenchmarkSet fp =+  do let dir  = takeDirectory fp+         base = takeBaseName fp+         set  = dir </> base <> ".set"++     pats <- compilePats . Text.lines <$> Text.readFile set+     fs <- concat <$> Glob.globDir pats dir+     tasks <- mapM loadVerificationTask fs++     return BenchmarkSet+            { benchmarkName = Text.pack base+            , benchmarkTasks = tasks+            }+++type TaskMap = Map VerificationTask [BenchmarkSet]++-- | There is significant overlap between the various verification tasks found in+--   different benchmark sets in the SV-COMP repository.  This operation collects+--   together all the potentially duplicated tasks found in a collection of benchmark sets+--   and places them in a map, ensuring there is at most one reference to each one.+--   The tasks are the keys of the map; the benchmark set(s) that referenced a given task+--   are stored in the elements the map.+deduplicateTasks :: [BenchmarkSet] -> TaskMap+deduplicateTasks = Map.unionsWith (++) . map f+  where+  f bs = Map.fromList+           [ (t, [bs]) | t <- benchmarkTasks bs ]
+ src/Crux/SVCOMP/Witness.hs view
@@ -0,0 +1,345 @@+-- | This module defines a data type for SV-COMP witness automatons, as+--   specified in https://github.com/sosy-lab/sv-witnesses.++{-# Language NamedFieldPuns #-}+module Crux.SVCOMP.Witness+  ( Witness(..), WitnessNode(..), WitnessEdge(..)+  , WitnessType(..), SourceCodeLang(..), Control(..), GraphMLAttrType(..)+  , mkNode, mkNodeId, mkEdge+  , ppWitness+  ) where++import           Data.ByteString (ByteString)+import qualified Data.ByteString.Char8 as B (unpack)+import qualified Data.List as L (intercalate)+import           Data.Maybe (catMaybes)+import           Data.Time.Format.ISO8601 (iso8601Show)+import           Data.Time.LocalTime (LocalTime(..), TimeOfDay(..), ZonedTime(..))+import           Text.XML.Light++import Crux.SVCOMP (Arch(..))++-- | A witness automaton. Adheres to the format specified in+-- https://github.com/sosy-lab/sv-witnesses/tree/a592b52c4034423d42bed2059addbc6d8f1fa443#data-elements.+data Witness = Witness+  { witnessType           :: WitnessType+  , witnessSourceCodeLang :: SourceCodeLang+  , witnessProducer       :: String+  , witnessSpecification  :: String+  , witnessProgramFile    :: FilePath+  , witnessProgramHash    :: ByteString+  , witnessArchitecture   :: Arch+  , witnessCreationTime   :: ZonedTime+  , witnessNodes          :: [WitnessNode]+  , witnessEdges          :: [WitnessEdge]+  }+  deriving Show++data WitnessNode = WitnessNode+  { nodeId             :: Id+  , nodeEntry          :: Maybe Bool+  , nodeSink           :: Maybe Bool+  , nodeViolation      :: Maybe Bool+  , nodeInvariant      :: Maybe String+  , nodeInvariantScope :: Maybe String+  }+  deriving Show++mkNode :: Int -> WitnessNode+mkNode i = WitnessNode+  { nodeId             = mkNodeId i+  , nodeEntry          = Nothing+  , nodeSink           = Nothing+  , nodeViolation      = Nothing+  , nodeInvariant      = Nothing+  , nodeInvariantScope = Nothing+  }++mkNodeId :: Int -> Id+mkNodeId i = "N" ++ show i++data WitnessEdge = WitnessEdge+  { edgeSource                   :: Id+  , edgeTarget                   :: Id+  , edgeAssumption               :: Maybe Assumption+  , edgeAssumptionScope          :: Maybe String+  , edgeAssumptionResultFunction :: Maybe String+  , edgeControl                  :: Maybe Control+  , edgeStartLine                :: Maybe Int+  , edgeEndLine                  :: Maybe Int+  , edgeStartOffset              :: Maybe Int+  , edgeEndOffset                :: Maybe Int+  , edgeEnterLoopHead            :: Maybe Bool+  , edgeEnterFunction            :: Maybe String+  , edgeReturnFromFunction       :: Maybe String+  , edgeThreadId                 :: Maybe String+  , edgeCreateThread             :: Maybe String++    -- crux-llvm–specific extensions+  , edgeStartColumn              :: Maybe Int+      -- Not to be confused with startoffset, which records the total number+      -- of characters from the very start of the program. This, on the other+      -- hand, simply records the number of characters from the start of the+      -- current line, which I find to be a nice debugging tool.+  }+  deriving Show++mkEdge :: Int -> Int -> WitnessEdge+mkEdge source target = WitnessEdge+  { edgeSource                   = mkNodeId source+  , edgeTarget                   = mkNodeId target+  , edgeAssumption               = Nothing+  , edgeAssumptionScope          = Nothing+  , edgeAssumptionResultFunction = Nothing+  , edgeControl                  = Nothing+  , edgeStartLine                = Nothing+  , edgeEndLine                  = Nothing+  , edgeStartOffset              = Nothing+  , edgeEndOffset                = Nothing+  , edgeEnterLoopHead            = Nothing+  , edgeEnterFunction            = Nothing+  , edgeReturnFromFunction       = Nothing+  , edgeThreadId                 = Nothing+  , edgeCreateThread             = Nothing++    -- crux-llvm–specific extensions+  , edgeStartColumn              = Nothing+  }++data WitnessType+  = CorrectnessWitness+  | ViolationWitness+  deriving Show++ppWitnessType :: WitnessType -> String+ppWitnessType witnessType =+  case witnessType of+    CorrectnessWitness -> "correctness_witness"+    ViolationWitness   -> "violation_witness"++data SourceCodeLang+  = C+  | Java+  deriving Show++ppSourceCodeLang :: SourceCodeLang -> String+ppSourceCodeLang sourceCodeLang =+  case sourceCodeLang of+    C    -> "C"+    Java -> "Java"++ppArch :: Arch -> String+ppArch arch =+  case arch of+    Arch32 -> "32bit"+    Arch64 -> "64bit"++newtype Assumption = Assumption [String]+  deriving Show++ppAssumption :: Assumption -> String+ppAssumption (Assumption exprs) =+  L.intercalate ";" exprs++data Control+  = ConditionTrue+  | ConditionFalse+  deriving Show++ppControl :: Control -> String+ppControl control =+  case control of+    ConditionTrue  -> "condition-true"+    ConditionFalse -> "condition-false"++data GraphMLAttrType+  = Boolean+  | Int+  | Long+  | Float+  | Double+  | String+  deriving Show++ppGraphMLAttrType :: GraphMLAttrType -> String+ppGraphMLAttrType ty =+  case ty of+    Boolean -> "boolean"+    Int     -> "int"+    Long    -> "long"+    Float   -> "float"+    Double  -> "double"+    String  -> "string"++data GraphMLAttrDomain+  = Graph+  | Node+  | Edge+  | All+  deriving Show++ppGraphMLAttrDomain :: GraphMLAttrDomain -> String+ppGraphMLAttrDomain domain =+  case domain of+    Graph -> "graph"+    Node  -> "node"+    Edge  -> "edge"+    All   -> "all"++ppBool :: Bool -> String+ppBool b =+  case b of+    False -> "false"+    True  -> "true"++ppByteString :: ByteString -> String+ppByteString = B.unpack++ppInt :: Int -> String+ppInt = show++ppString :: String -> String+ppString = id++ppZonedTime :: ZonedTime -> String+ppZonedTime = iso8601Show . roundNearestSecond+  where+    -- Round to the nearest second to ensure that we do not print out seconds+    -- with a decimal component. This is an unforunate hack to work around+    -- https://github.com/sosy-lab/sv-witnesses/issues/40.+    roundNearestSecond :: ZonedTime -> ZonedTime+    roundNearestSecond zt@ZonedTime{ zonedTimeToLocalTime =+                       lt@LocalTime{ localTimeOfDay =+                       tod@TimeOfDay{ todSec = sec }}} =+      zt{ zonedTimeToLocalTime =+      lt{ localTimeOfDay =+      tod{ todSec = fromInteger (round sec) }}}++type Id = String++dataNode :: String -> (a -> String) -> a -> Element+dataNode keyVal ppThing thing =+  add_attr (Attr{attrKey = unqual "key", attrVal = keyVal}) $+  unode "data" $+    ppThing thing++ppWitness :: Witness -> String+ppWitness witness =+  unlines [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"+          , ppElement $ unode "graph" witness+          ]++instance Node Witness where+  node n Witness{ witnessType, witnessSourceCodeLang, witnessProducer+                , witnessSpecification, witnessProgramFile, witnessProgramHash+                , witnessArchitecture, witnessCreationTime+                , witnessNodes, witnessEdges+                } =+    add_attrs [ Attr{ attrKey = unqual "xmlns"+                    , attrVal = "http://graphml.graphdrawing.org/xmlns"+                    }+              , Attr{ attrKey = unqual "xmlns:xsi"+                    , attrVal = "http://www.w3.org/2001/XMLSchema-instance"+                    }+              , Attr{ attrKey = unqual "xsi:schemaLocation"+                    , attrVal = "http://graphml.graphdrawing.org/xmlns http://graphml.graphdrawing.org/xmlns/1.0/graphml.xsd"+                    }+              ] $+    unode "graphml" $+      [ keyNode "witness-type"   String Graph+      , keyNode "sourcecodelang" String Graph+      , keyNode "producer"       String Graph+      , keyNode "specification"  String Graph+      , keyNode "programfile"    String Graph+      , keyNode "programhash"    String Graph+      , keyNode "architecture"   String Graph+      , keyNode "creationtime"   String Graph++      , keyNode "entry"           Boolean Node+      , keyNode "sink"            Boolean Node+      , keyNode "violation"       Boolean Node+      , keyNode "invariant"       String  Node+      , keyNode "invariant.scope" String  Node++      , keyNode "assumption"                String  Edge+      , keyNode "assumption.scope"          String  Edge+      , keyNode "assumption.resultfunction" String  Edge+      , keyNode "control"                   String  Edge+      , keyNode "startline"                 Int     Edge+      , keyNode "endline"                   Int     Edge+      , keyNode "startoffset"               Int     Edge+      , keyNode "endoffset"                 Int     Edge+      , keyNode "enterLoopHead"             Boolean Edge+      , keyNode "enterFunction"             String  Edge+      , keyNode "returnFromFunction"        String  Edge+      , keyNode "threadId"                  String  Edge+      , keyNode "createThread"              String  Edge+        -- crux-llvm–specific extensions+      , keyNode "startcolumn"               Int     Edge++      , add_attr (Attr{attrKey = unqual "edgedefault", attrVal = "directed"}) $+        node n $+          [ dataNode "witness-type"   ppWitnessType    witnessType+          , dataNode "sourcecodelang" ppSourceCodeLang witnessSourceCodeLang+          , dataNode "producer"       ppString         witnessProducer+          , dataNode "specification"  ppString         witnessSpecification+          , dataNode "programfile"    ppString         witnessProgramFile+          , dataNode "programhash"    ppByteString     witnessProgramHash+          , dataNode "architecture"   ppArch           witnessArchitecture+          , dataNode "creationtime"   ppZonedTime      witnessCreationTime+          ] ++ map (unode "node") witnessNodes+            ++ map (unode "edge") witnessEdges+      ]+    where+      keyNode :: Id -> GraphMLAttrType -> GraphMLAttrDomain -> Element+      keyNode name ty domain =+        add_attrs [ Attr{attrKey = unqual "id",        attrVal = name}+                  , Attr{attrKey = unqual "attr.name", attrVal = name}+                  , Attr{attrKey = unqual "attr.type", attrVal = ppGraphMLAttrType ty}+                  , Attr{attrKey = unqual "for",       attrVal = ppGraphMLAttrDomain domain}+                  ] $+        case ty of+          Boolean -> unode "key" [unode "default" (ppBool False)]+          _       -> unode "key" ()++instance Node WitnessNode where+  node n WitnessNode{ nodeId, nodeEntry, nodeSink+                    , nodeViolation, nodeInvariant, nodeInvariantScope+                    } =+    add_attr (Attr{attrKey = unqual "id", attrVal = nodeId}) $+    node n $ catMaybes+      [ dataNode "entry"           ppBool   <$> nodeEntry+      , dataNode "sink"            ppBool   <$> nodeSink+      , dataNode "violation"       ppBool   <$> nodeViolation+      , dataNode "invariant"       ppString <$> nodeInvariant+      , dataNode "invariant.scope" ppString <$> nodeInvariantScope+      ]++instance Node WitnessEdge where+  node n WitnessEdge{ edgeSource, edgeTarget+                    , edgeAssumption, edgeAssumptionScope, edgeAssumptionResultFunction+                    , edgeControl, edgeStartLine, edgeEndLine, edgeStartOffset, edgeEndOffset+                    , edgeEnterLoopHead, edgeEnterFunction, edgeReturnFromFunction+                    , edgeThreadId, edgeCreateThread+                      -- crux-llvm–specific extensions+                    , edgeStartColumn+                    } =+    add_attrs [ Attr{attrKey = unqual "source", attrVal = edgeSource}+              , Attr{attrKey = unqual "target", attrVal = edgeTarget}+              ] $+    node n $ catMaybes+      [ dataNode "assumption"                ppAssumption <$> edgeAssumption+      , dataNode "assumption.scope"          ppString     <$> edgeAssumptionScope+      , dataNode "assumption.resultfunction" ppString     <$> edgeAssumptionResultFunction+      , dataNode "control"                   ppControl    <$> edgeControl+      , dataNode "startline"                 ppInt        <$> edgeStartLine+      , dataNode "endline"                   ppInt        <$> edgeEndLine+      , dataNode "startoffset"               ppInt        <$> edgeStartOffset+      , dataNode "endoffset"                 ppInt        <$> edgeEndOffset+      , dataNode "enterLoopHead"             ppBool       <$> edgeEnterLoopHead+      , dataNode "enterFunction"             ppString     <$> edgeEnterFunction+      , dataNode "returnFromFunction"        ppString     <$> edgeReturnFromFunction+      , dataNode "threadId"                  ppString     <$> edgeThreadId+      , dataNode "createThread"              ppString     <$> edgeCreateThread+      , dataNode "startcolumn"               ppInt        <$> edgeStartColumn+      ]
+ src/Crux/Types.hs view
@@ -0,0 +1,146 @@+{-# Language DeriveFunctor, RankNTypes, ConstraintKinds, TypeFamilies, ScopedTypeVariables, GADTs #-}+module Crux.Types where++import           Data.Functor.Const+import           Data.Parameterized.Map (MapF)+import           Data.Sequence (Seq)+import           Data.Text ( Text )+import           Data.Void+import           Prettyprinter++import           What4.Expr (GroundValue,GroundValueWrapper)+import           What4.Interface (Pred)+import           What4.ProgramLoc++import           Lang.Crucible.Backend+import           Lang.Crucible.Simulator+import           Lang.Crucible.Types++-- | A simulator context+type SimCtxt personality sym p = SimContext (personality sym) sym p++-- | The instance of the override monad we use,+-- when we don't care about the context of the surrounding function.+type OverM personality sym ext a =+  forall r args ret.+  OverrideSim+    (personality sym)  -- Extra data available in overrides (frontend-specific)+    sym                -- The symbolic backend (usually a what4 ExprBuilder in some form)+    ext                -- The Crucible syntax extension for the target language+    r+    args+    ret+    a++-- | This is the instance of the 'OverrideSim' monad that we use.+type Fun personality sym ext args ret =+  forall r.+  OverrideSim+    (personality sym)+    sym                                    -- the backend+    ext+    r+    args+    ret+    (RegValue sym ret)++data Result personality sym where+  Result :: (ExecResult (personality sym) sym ext (RegEntry sym UnitType)) -> Result personality sym+++data ProcessedGoals =+  ProcessedGoals { totalProcessedGoals :: !Integer+                 , provedGoals :: !Integer+                 , disprovedGoals :: !Integer+                 , incompleteGoals :: !Integer+                 }++data ProofResult sym+   = Proved [Either (Assumption sym) (Assertion sym)]+   | NotProved (Doc Void) (Maybe (ModelView, [CrucibleEvent GroundValueWrapper])) [String]+     -- ^ The first argument is an explanation of the failure and+     -- counter example as provided by the Explainer (if any), the+     -- second maybe a model for the counter-example, and the third +     -- is a list of abducts provided which may be empty++type LPred sym   = LabeledPred (Pred sym)++data ProvedGoals+  = Branch ProvedGoals ProvedGoals+  | NotProvedGoal+         [CrucibleAssumption (Const ())]+         SimError+         (Doc Void)+         [ProgramLoc]+         (Maybe (ModelView, [CrucibleEvent GroundValueWrapper]))+         [String]+  | ProvedGoal+         [CrucibleAssumption (Const ())]+         SimError+         [ProgramLoc]+         Bool+    -- ^ Keeps only the explanations for the relevant assumptions.+    --+    --   * The array of (AssumptionReason,String) is the set of+    --     assumptions for this Goal.+    --+    --   * The (SimError,String) is information about the failure,+    --     with the specific SimError (Lang.Crucible.Simulator) and a+    --     string representation of the Crucible term that encountered+    --     the error.+    --+    --   * The 'Bool' (third argument) indicates if the goal is+    --     trivial (i.e., the assumptions are inconsistent)+++data ProgramCompleteness+ = ProgramComplete+ | ProgramIncomplete+ deriving (Eq,Ord,Show)++++data CruxSimulationResult =+  CruxSimulationResult+  { cruxSimResultCompleteness :: ProgramCompleteness+  , cruxSimResultGoals        :: Seq (ProcessedGoals, ProvedGoals)+  }+++-- | A dummy datatype that can be used for the "personality"+--   type parameter.+data Crux sym = CruxPersonality+++-- | A list of named GroundValues of the same type (used to+-- report SMT models in a portable way -- see the ModelView+-- datatype).+newtype Vals ty     = Vals [ Entry (GroundValue ty) ]++-- | A named value of type @a@ with a program+-- location. Used to describe and report models from SMT+-- queries (see Model and ModelView datatypes).+data Entry a        = Entry { entryName :: String+                            , entryLoc :: ProgramLoc+                            , entryValue :: a+                            }++-- | A portable/concrete view of a model's contents, organized by+-- crucible type. I.e., each crucible type is associated+-- with the list of entries (i.e. named GroundValues) at+-- that type for the given model, used to describe the+-- conditions under which an SMT query is satisfiable.+newtype ModelView = ModelView { modelVals :: MapF BaseTypeRepr Vals }++----------------------------------------------------------------------+-- Various things that can be logged/output++-- | Specify some general text that should be presented (to the user).+data SayWhat = SayWhat SayLevel Text Text  -- ^ fields are: Level From Message+             | SayMore SayWhat SayWhat+             | SayNothing++-- | Specify the verbosity/severity level of a message.  These are in+-- ordinal order for possible filtering, and higher levels may be sent+-- to a different location (e.g. stderr v.s. stdout).+data SayLevel = Noisily | Simply | OK | Warn | Fail deriving (Eq, Ord)
+ src/Crux/UI/IndexHtml.hs view
@@ -0,0 +1,358 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes #-}++module Crux.UI.IndexHtml where++import           Data.Text (Text)+-- raw-strings-qq+import Text.RawString.QQ+++indexHtml :: Text+indexHtml = [r|+<!DOCTYPE html>+<html>+<head>+<meta charset="UTF-8">++<script src="jquery.min.js"></script>+<script src="source.js"></script>+<script src="report.js"></script>+<script>++var fileObjs = {}+var nextId = 0++function getFile(loc) {+  var obj = fileObjs[loc.file]+  return obj ? $(obj.dom) : $([])+}++function getLine(loc) { return getFile(loc).find('#line-' + loc.line) }++function showFile(name) {+  var obj = fileObjs[name]+  if (!obj) return++  $('.source-file').hide()+  $('.file-btn').removeClass('selected')+  obj.dom.show()+  obj.btn.addClass('selected')+}++function drawSourceFile(file) {+  var obj = fileObjs[file.name]+  if (!obj) {+    obj = { id: 'file_' + nextId }+    ++nextId+    fileObjs[file.name] = obj+  }++  var dom = drawLines(file.lines)+            .attr('id',obj.id)+            .addClass('source-file')+  dom.hide()++  var btn = $('<div/>')+            .text(file.label)+            .addClass('clickable file-btn')+  obj.dom = dom+  obj.btn = btn++  btn.click(function() { showFile(file.name) })++  return { btn: btn, dom: dom }+}++function drawLines(lines) {+  var i+  var dom = $('<ol/>')+  for (i = 0; i < lines.length; ++i) {+    var li = $('<li/>').attr('id','line-' + (i+1))+                       .addClass('line')+                       .text(lines[i])+    dom.append(li)+  }+  return dom+}+++function drawStatus(status) {+  return $('<div/>')+         .addClass('tag')+         .text(status)+                    .addClass('highlight-' + status)+}++function drawCounterExample(e) {+  if (e === null) return+  jQuery.each(e, function(ix,v) {+    getLine(v.loc).append($('<span/>')+                  .addClass('ctr-example').text(v.val))+  })+}++++function drawPath(path) {+  $('.path').remove()+  jQuery.each(path,function(ix,step) {+    var branch = step.loc+    var ln = getLine(branch)++    var pre = ""+    if (step.loop.length > 1) {+      pre = "("+      for (i = 0; i < step.loop.length - 1; ++i) {+        pre += step.loop[i]+        pre += (i === step.loop.length - 2) ? ')' : ','+      }+   }++    var tag = $('<span/>')+              .addClass('path')+              .append( $('<span/>').text(pre + step.loop[step.loop.length-1])+                     , $('<sup/>').text(ix+1)+                     )+    ln.append(tag)+  })+}++function summarizePath(path) {+  var it = $('<div/>')+  var fst = true+  jQuery.each(path,function(ix,branch) {+    let msg = (fst ? '' : ', ') + branch.line + '(' + branch.tgt + ')'+    it.append($('<span/>').text(msg))+    fst = false+  })+  return it+}++++function drawGoals() {+  var dom = $('<div>').addClass('goals')++  if (goals.length === 0) dom.append($('<span/>').text('Nothing to prove.'))++  jQuery.each(goals, function(gNum,g) {+    var li = $('<div/>')+            .addClass('clickable')+            .append( drawStatus(g.status)+                   , $('<abbr/>')+                       .text(g.goal)+                       .attr('title', g['details-short'])+                   )+    li.click(function() {+      var errPane = $('#error-pane')+      errPane.empty()+      if( g['details-long'] ) {+        errPane.append( $('<pre/>').text(g['details-long']) )+      } else {+        errPane.append( $('<pre/>').text(g['details-short']) )+      }++      $('.highlight-assumed').removeClass('highlight-assumed')+      $('.selected').removeClass('selected')+      li.addClass('selected')+      $('.ctr-example').remove()+      $('.asmp-lab').remove()+      $('.line').removeClass('highlight-line-ok')+                .removeClass('highlight-line-fail')+                .removeClass('highlight-line-unknown')+                .removeClass('highlight-assumed')+     jQuery.each(g.assumptions, function(ix,a) {+        var lnName = a.loc+        if (!lnName) return true+        if (!lnName.file) return true++         var obj = fileObjs[lnName.file]+         if(obj) obj.btn.addClass('highlight-assumed')++        if (lnName.file !== g.location.file || lnName.line !== g.location.line) {+          var ln = getLine(lnName)+          ln.addClass('highlight-assumed')++          // var note = $('<div/>')+          //            .addClass('asmp-lab')+          //            .text(a.text)+          // ln.append(note)+        }+      })+      if (g.location !== null) {+        showFile(g.location.file)+        var it = getLine(g.location)+        it.addClass('highlight-line-' + g.status)+        it[0].scrollIntoView({behavior:'smooth', block:'center'})+      }+      drawCounterExample(g['counter-example'])+      if(g.path) drawPath(g.path)+    })+    dom.append(li)+  })++  return dom+}++$(document).ready(function() {+  var i+  var srcPane = $('#source-pane')+  var filePane = $('#file-pane')+  jQuery.each(sources, function(ix,file) {+    ui = drawSourceFile(file)+    srcPane.append(ui.dom)+    filePane.append(ui.btn)+  })++  $('#nav-bar').append(drawGoals())+})+</script>+<style>+html { height: 100%; padding: 0; margin: 0; }+body { height: 100%; padding: 0; margin: 0; }++.clickable {+  cursor: pointer;+}++#nav-bar {+  width: 25%;+  float: left;+  height: 90%;+  overflow: auto;+}++#right-pane {+  float: right;+  width: 74%;+}++#source-pane {+  font-family: monospace;+  white-space: pre;+  height: 90%;+  overflow: auto;+  font-size: normal;+}++#error-pane {+  font-family: monospace;+  max-height: 20vh;+  font-size: small;+  overflow: auto;+}++.file-btn {+  border: 1px solid black;+  border-radius: 5px;+  display: inline-block;+  margin: 2px;+  padding: 2px;+}+++ol.source-file {+  counter-reset: item;+  padding: 0;+}++ol.source-file>li {+  list-style-type: none;+  counter-increment: item;+}++ol.source-file>li:hover {+  background-color: #ccf;+}++ol.source-file>li:before {+  display: inline-block;+  width: 4em;+  text-align: right;+  content: counter(item);+  margin-right: 1em;+  font-size: small;+  font-style: italic;+  color: #999;+}++.goals { margin: 5px; }++.highlight-ok      { background-color: green !important; color: white; }+.highlight-fail    { background-color: red !important;  color: white; }+.highlight-unknown { background-color: yellow !important; color: black; }+.highlight-assumed { background-color: cyan; color: black; }++.highlight-line-ok      { background-color: green !important; color: lightgrey; }+.highlight-line-fail    { background-color: red !important;  color: lightgrey; }+.highlight-line-unknown { background-color: yellow !important; color: black; }++.ctr-example {+  margin: 5px;+  background-color: #ff0000;+  color: white;+  font-weight: bold;+  padding-left: 2px;+  padding-right: 2px;+  border-radius: 5px;+  font-size: smaller;+}++.asmp-lab {+  border: 1px solid black;+  margin: 5px;+  background-color: #eee;+  padding-left: 2px;+  padding-right: 2px;+  border-radius: 5px;+  font-size: smaller;+}++.selected {+  background-color: #ccf;+}++.path {+  margin-right: 1em;+}++.path>span {+  font-weight: bold;+  background-color: orange;+  border-radius: 10px;+  margin: 2px;+  padding: 2px;+}++.path>sup {+  color: #666;+  font-style: italic;+  font-size: small;+  font-weight: normal;+}++.tag {+  font-weight: bold;+  font-family: monospace;+  display: inline-block;+  margin: 2px;+  padding: 2px;+  padding-left: 4px;+  padding-right: 4px;+  text-align: center;+  border-radius: 2px;+  width: 4em;+}++</style>+</head>+<body><div id="nav-bar"></div+><div id="right-pane"+  ><div id="error-pane"></div+  ><div id="file-pane"></div+  ><div id="source-pane"></div+></div+></body>+</html>+|]
+ src/Crux/UI/JS.hs view
@@ -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+++---------------------------------------------------+
+ src/Crux/UI/Jquery.hs view
@@ -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&&n<t?[this[n]]:[])},end:function(){return this.prevObject||this.constructor()},push:s,sort:n.sort,splice:n.splice},w.extend=w.fn.extend=function(){var e,t,n,r,i,o,a=arguments[0]||{},s=1,u=arguments.length,l=!1;for("boolean"==typeof a&&(l=a,a=arguments[s]||{},s++),"object"==typeof a||g(a)||(a={}),s===u&&(a=this,s--);s<u;s++)if(null!=(e=arguments[s]))for(t in e)n=a[t],a!==(r=e[t])&&(l&&r&&(w.isPlainObject(r)||(i=Array.isArray(r)))?(i?(i=!1,o=n&&Array.isArray(n)?n:[]):o=n&&w.isPlainObject(n)?n:{},a[t]=w.extend(l,o,r)):void 0!==r&&(a[t]=r));return a},w.extend({expando:"jQuery"+("3.3.1"+Math.random()).replace(/\D/g,""),isReady:!0,error:function(e){throw new Error(e)},noop:function(){},isPlainObject:function(e){var t,n;return!(!e||"[object Object]"!==c.call(e))&&(!(t=i(e))||"function"==typeof(n=f.call(t,"constructor")&&t.constructor)&&p.call(n)===d)},isEmptyObject:function(e){var t;for(t in e)return!1;return!0},globalEval:function(e){m(e)},each:function(e,t){var n,r=0;if(C(e)){for(n=e.length;r<n;r++)if(!1===t.call(e[r],r,e[r]))break}else for(r in e)if(!1===t.call(e[r],r,e[r]))break;return e},trim:function(e){return null==e?"":(e+"").replace(T,"")},makeArray:function(e,t){var n=t||[];return null!=e&&(C(Object(e))?w.merge(n,"string"==typeof e?[e]:e):s.call(n,e)),n},inArray:function(e,t,n){return null==t?-1:u.call(t,e,n)},merge:function(e,t){for(var n=+t.length,r=0,i=e.length;r<n;r++)e[i++]=t[r];return e.length=i,e},grep:function(e,t,n){for(var r,i=[],o=0,a=e.length,s=!n;o<a;o++)(r=!t(e[o],o))!==s&&i.push(e[o]);return i},map:function(e,t,n){var r,i,o=0,s=[];if(C(e))for(r=e.length;o<r;o++)null!=(i=t(e[o],o,n))&&s.push(i);else for(o in e)null!=(i=t(e[o],o,n))&&s.push(i);return a.apply([],s)},guid:1,support:h}),"function"==typeof Symbol&&(w.fn[Symbol.iterator]=n[Symbol.iterator]),w.each("Boolean Number String Function Array Date RegExp Object Error Symbol".split(" "),function(e,t){l["[object "+t+"]"]=t.toLowerCase()});function C(e){var t=!!e&&"length"in e&&e.length,n=x(e);return!g(e)&&!y(e)&&("array"===n||0===t||"number"==typeof t&&t>0&&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<r;n++)if(e[n]===t)return n;return-1},P="checked|selected|async|autofocus|autoplay|controls|defer|disabled|hidden|ismap|loop|multiple|open|readonly|required|scoped",M="[\\x20\\t\\r\\n\\f]",R="(?:\\\\.|[\\w-]|[^\0-\\xa0])+",I="\\["+M+"*("+R+")(?:"+M+"*([*^$|!~]?=)"+M+"*(?:'((?:\\\\.|[^\\\\'])*)'|\"((?:\\\\.|[^\\\\\"])*)\"|("+R+"))|)"+M+"*\\]",W=":("+R+")(?:\\((('((?:\\\\.|[^\\\\'])*)'|\"((?:\\\\.|[^\\\\\"])*)\")|((?:\\\\.|[^\\\\()[\\]]|"+I+")*)|.*)\\)|)",$=new RegExp(M+"+","g"),B=new RegExp("^"+M+"+|((?:^|[^\\\\])(?:\\\\.)*)"+M+"+$","g"),F=new RegExp("^"+M+"*,"+M+"*"),_=new RegExp("^"+M+"*([>+~]|"+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="<a id='"+b+"'></a><select id='"+b+"-\r\\' msallowcapture=''><option selected=''></option></select>",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="<a href='' disabled='disabled'></a><select disabled='disabled'><option/></select>";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<t;n+=2)e.push(n);return e}),odd:he(function(e,t){for(var n=1;n<t;n+=2)e.push(n);return e}),lt:he(function(e,t,n){for(var r=n<0?n+t:n;--r>=0;)e.push(r);return e}),gt:he(function(e,t,n){for(var r=n<0?n+t:n;++r<t;)e.push(r);return e})}}).pseudos.nth=r.pseudos.eq;for(t in{radio:!0,checkbox:!0,file:!0,password:!0,image:!0})r.pseudos[t]=fe(t);for(t in{submit:!0,reset:!0})r.pseudos[t]=pe(t);function ye(){}ye.prototype=r.filters=r.pseudos,r.setFilters=new ye,a=oe.tokenize=function(e,t){var n,i,o,a,s,u,l,c=k[e+" "];if(c)return t?0:c.slice(0);s=e,u=[],l=r.preFilter;while(s){n&&!(i=F.exec(s))||(i&&(s=s.slice(i[0].length)||s),u.push(o=[])),n=!1,(i=_.exec(s))&&(n=i.shift(),o.push({value:n,type:i[0].replace(B," ")}),s=s.slice(n.length));for(a in r.filter)!(i=V[a].exec(s))||l[a]&&!(i=l[a](i))||(n=i.shift(),o.push({value:n,type:a,matches:i}),s=s.slice(n.length));if(!n)break}return t?s.length:s?oe.error(e):k(e,u).slice(0)};function ve(e){for(var t=0,n=e.length,r="";t<n;t++)r+=e[t].value;return r}function me(e,t,n){var r=t.dir,i=t.next,o=i||r,a=n&&"parentNode"===o,s=C++;return t.first?function(t,n,i){while(t=t[r])if(1===t.nodeType||a)return e(t,n,i);return!1}:function(t,n,u){var l,c,f,p=[T,s];if(u){while(t=t[r])if((1===t.nodeType||a)&&e(t,n,u))return!0}else while(t=t[r])if(1===t.nodeType||a)if(f=t[b]||(t[b]={}),c=f[t.uniqueID]||(f[t.uniqueID]={}),i&&i===t.nodeName.toLowerCase())t=t[r]||t;else{if((l=c[o])&&l[0]===T&&l[1]===s)return p[2]=l[2];if(c[o]=p,p[2]=e(t,n,u))return!0}return!1}}function xe(e){return e.length>1?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<i;r++)oe(e,t[r],n);return n}function we(e,t,n,r,i){for(var o,a=[],s=0,u=e.length,l=null!=t;s<u;s++)(o=e[s])&&(n&&!n(o,r,i)||(a.push(o),l&&t.push(s)));return a}function Te(e,t,n,r,i,o){return r&&!r[b]&&(r=Te(r)),i&&!i[b]&&(i=Te(i,o)),se(function(o,a,s,u){var l,c,f,p=[],d=[],h=a.length,g=o||be(t||"*",s.nodeType?[s]:s,[]),y=!e||!o&&t?g:we(g,p,e,s,u),v=n?i||(o?e:h||r)?[]:a:y;if(n&&n(y,v,s,u),r){l=we(v,d),r(l,[],s,u),c=l.length;while(c--)(f=l[c])&&(v[d[c]]=!(y[d[c]]=f))}if(o){if(i||e){if(i){l=[],c=v.length;while(c--)(f=v[c])&&l.push(y[c]=f);i(null,v=[],l,u)}c=v.length;while(c--)(f=v[c])&&(l=i?O(o,f):p[c])>-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}];u<o;u++)if(n=r.relative[e[u].type])p=[me(xe(p),n)];else{if((n=r.filter[e[u].type].apply(null,e[u].matches))[b]){for(i=++u;i<o;i++)if(r.relative[e[i].type])break;return Te(u>1&&xe(p),u>1&&ve(e.slice(0,u-1).concat({value:" "===e[u-2].type?"*":""})).replace(B,"$1"),n,u<i&&Ce(e.slice(u,i)),i<o&&Ce(e=e.slice(i)),i<o&&ve(e))}p.push(n)}return xe(p)}function Ee(e,t){var n=t.length>0,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="<a href='#'></a>","#"===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="<input/>",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;t<r;t++)if(w.contains(i[t],this))return!0}));for(n=this.pushStack([]),t=0;t<r;t++)w.find(e,i[t],n);return r>1?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<n;e++)if(w.contains(this,t[e]))return!0})},closest:function(e,t){var n,r=0,i=this.length,o=[],a="string"!=typeof e&&w(e);if(!D.test(e))for(;r<i;r++)for(n=this[r];n&&n!==t;n=n.parentNode)if(n.nodeType<11&&(a?a.index(n)>-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<o.length)!1===o[s].apply(n[0],n[1])&&e.stopOnFalse&&(s=o.length,n=!1)}e.memory||(n=!1),t=!1,i&&(o=n?[]:"")},l={add:function(){return o&&(n&&!t&&(s=o.length-1,a.push(n)),function t(n){w.each(n,function(n,r){g(r)?e.unique&&l.has(r)||o.push(r):r&&r.length&&"string"!==x(r)&&t(r)})}(arguments),n&&!t&&u()),this},remove:function(){return w.each(arguments,function(e,t){var n;while((n=w.inArray(t,o,n))>-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)){if((e=r.apply(s,u))===n.promise())throw new TypeError("Thenable self-resolution");l=e&&("object"==typeof e||"function"==typeof e)&&e.then,g(l)?i?l.call(e,a(o,n,I,i),a(o,n,W,i)):(o++,l.call(e,a(o,n,I,i),a(o,n,W,i),a(o,n,I,n.notifyWith))):(r!==I&&(s=void 0,u=[e]),(i||n.resolveWith)(s,u))}},c=i?l:function(){try{l()}catch(e){w.Deferred.exceptionHook&&w.Deferred.exceptionHook(e,c.stackTrace),t+1>=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(;s<u;s++)t(e[s],n,a?r:r.call(e[s],s,t(e[s],n)));return i?e:l?t.call(e):u?t(e[0],n):o},X=/^-ms-/,U=/-([a-z])/g;function V(e,t){return t.toUpperCase()}function G(e){return e.replace(X,"ms-").replace(U,V)}var Y=function(e){return 1===e.nodeType||9===e.nodeType||!+e.nodeType};function Q(){this.expando=w.expando+Q.uid++}Q.uid=1,Q.prototype={cache:function(e){var t=e[this.expando];return t||(t={},Y(e)&&(e.nodeType?e[this.expando]=t:Object.defineProperty(e,this.expando,{value:t,configurable:!0}))),t},set:function(e,t,n){var r,i=this.cache(e);if("string"==typeof t)i[G(t)]=n;else for(r in t)i[G(r)]=t[r];return i},get:function(e,t){return void 0===t?this.cache(e):e[this.expando]&&e[this.expando][G(t)]},access:function(e,t,n){return void 0===t||t&&"string"==typeof t&&void 0===n?this.get(e,t):(this.set(e,t,n),void 0!==n?n:t)},remove:function(e,t){var n,r=e[this.expando];if(void 0!==r){if(void 0!==t){n=(t=Array.isArray(t)?t.map(G):(t=G(t))in r?[t]:t.match(M)||[]).length;while(n--)delete r[t[n]]}(void 0===t||w.isEmptyObject(r))&&(e.nodeType?e[this.expando]=void 0:delete e[this.expando])}},hasData:function(e){var t=e[this.expando];return void 0!==t&&!w.isEmptyObject(t)}};var J=new Q,K=new Q,Z=/^(?:\{[\w\W]*\}|\[[\w\W]*\])$/,ee=/[A-Z]/g;function te(e){return"true"===e||"false"!==e&&("null"===e?null:e===+e+""?+e:Z.test(e)?JSON.parse(e):e)}function ne(e,t,n){var r;if(void 0===n&&1===e.nodeType)if(r="data-"+t.replace(ee,"-$&").toLowerCase(),"string"==typeof(n=e.getAttribute(r))){try{n=te(n)}catch(e){}K.set(e,t,n)}else n=void 0;return n}w.extend({hasData:function(e){return K.hasData(e)||J.hasData(e)},data:function(e,t,n){return K.access(e,t,n)},removeData:function(e,t){K.remove(e,t)},_data:function(e,t,n){return J.access(e,t,n)},_removeData:function(e,t){J.remove(e,t)}}),w.fn.extend({data:function(e,t){var n,r,i,o=this[0],a=o&&o.attributes;if(void 0===e){if(this.length&&(i=K.get(o),1===o.nodeType&&!J.get(o,"hasDataAttrs"))){n=a.length;while(n--)a[n]&&0===(r=a[n].name).indexOf("data-")&&(r=G(r.slice(5)),ne(o,r,i[r]));J.set(o,"hasDataAttrs",!0)}return i}return"object"==typeof e?this.each(function(){K.set(this,e)}):z(this,function(t){var n;if(o&&void 0===t){if(void 0!==(n=K.get(o,e)))return n;if(void 0!==(n=ne(o,e)))return n}else this.each(function(){K.set(this,e,t)})},null,t,arguments.length>1,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<n?w.queue(this[0],e):void 0===t?this:this.each(function(){var n=w.queue(this,e,t);w._queueHooks(this,e),"fx"===e&&"inprogress"!==n[0]&&w.dequeue(this,e)})},dequeue:function(e){return this.each(function(){w.dequeue(this,e)})},clearQueue:function(e){return this.queue(e||"fx",[])},promise:function(e,t){var n,r=1,i=w.Deferred(),o=this,a=this.length,s=function(){--r||i.resolveWith(o,[o])};"string"!=typeof e&&(t=e,e=void 0),e=e||"fx";while(a--)(n=J.get(o[a],e+"queueHooks"))&&n.empty&&(r++,n.empty.add(s));return s(),i.promise(t)}});var re=/[+-]?(?:\d*\.|)\d+(?:[eE][+-]?\d+|)/.source,ie=new RegExp("^(?:([+-])=|)("+re+")([a-z%]*)$","i"),oe=["Top","Right","Bottom","Left"],ae=function(e,t){return"none"===(e=t||e).style.display||""===e.style.display&&w.contains(e.ownerDocument,e)&&"none"===w.css(e,"display")},se=function(e,t,n,r){var i,o,a={};for(o in t)a[o]=e.style[o],e.style[o]=t[o];i=n.apply(e,r||[]);for(o in t)e.style[o]=a[o];return i};function ue(e,t,n,r){var i,o,a=20,s=r?function(){return r.cur()}:function(){return w.css(e,t,"")},u=s(),l=n&&n[3]||(w.cssNumber[t]?"":"px"),c=(w.cssNumber[t]||"px"!==l&&+u)&&ie.exec(w.css(e,t));if(c&&c[3]!==l){u/=2,l=l||c[3],c=+u||1;while(a--)w.style(e,t,c+l),(1-o)*(1-(o=s()/u||.5))<=0&&(a=0),c/=o;c*=2,w.style(e,t,c+l),n=n||[]}return n&&(c=+c||+u||0,i=n[1]?c+(n[1]+1)*n[2]:+n[2],r&&(r.unit=l,r.start=c,r.end=i)),i}var le={};function ce(e){var t,n=e.ownerDocument,r=e.nodeName,i=le[r];return i||(t=n.body.appendChild(n.createElement(r)),i=w.css(t,"display"),t.parentNode.removeChild(t),"none"===i&&(i="block"),le[r]=i,i)}function fe(e,t){for(var n,r,i=[],o=0,a=e.length;o<a;o++)(r=e[o]).style&&(n=r.style.display,t?("none"===n&&(i[o]=J.get(r,"display")||null,i[o]||(r.style.display="")),""===r.style.display&&ae(r)&&(i[o]=ce(r))):"none"!==n&&(i[o]="none",J.set(r,"display",n)));for(o=0;o<a;o++)null!=i[o]&&(e[o].style.display=i[o]);return e}w.fn.extend({show:function(){return fe(this,!0)},hide:function(){return fe(this)},toggle:function(e){return"boolean"==typeof e?e?this.show():this.hide():this.each(function(){ae(this)?w(this).show():w(this).hide()})}});var pe=/^(?:checkbox|radio)$/i,de=/<([a-z][^\/\0>\x20\t\r\n\f]+)/i,he=/^$|^module$|\/(?:java|ecma)script/i,ge={option:[1,"<select multiple='multiple'>","</select>"],thead:[1,"<table>","</table>"],col:[2,"<table><colgroup>","</colgroup></table>"],tr:[2,"<table><tbody>","</tbody></table>"],td:[3,"<table><tbody><tr>","</tr></tbody></table>"],_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<r;n++)J.set(e[n],"globalEval",!t||J.get(t[n],"globalEval"))}var me=/<|&#?\w+;/;function xe(e,t,n,r,i){for(var o,a,s,u,l,c,f=t.createDocumentFragment(),p=[],d=0,h=e.length;d<h;d++)if((o=e[d])||0===o)if("object"===x(o))w.merge(p,o.nodeType?[o]:o);else if(me.test(o)){a=a||f.appendChild(t.createElement("div")),s=(de.exec(o)||["",""])[1].toLowerCase(),u=ge[s]||ge._default,a.innerHTML=u[1]+w.htmlPrefilter(o)+u[2],c=u[0];while(c--)a=a.lastChild;w.merge(p,a.childNodes),(a=f.firstChild).textContent=""}else p.push(t.createTextNode(o));f.textContent="",d=0;while(o=p[d++])if(r&&w.inArray(o,r)>-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="<textarea>x</textarea>",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<arguments.length;n++)u[n]=arguments[n];if(t.delegateTarget=this,!c.preDispatch||!1!==c.preDispatch.call(this,t)){s=w.event.handlers.call(this,t,l),n=0;while((o=s[n++])&&!t.isPropagationStopped()){t.currentTarget=o.elem,r=0;while((a=o.handlers[r++])&&!t.isImmediatePropagationStopped())t.rnamespace&&!t.rnamespace.test(a.namespace)||(t.handleObj=a,t.data=a.data,void 0!==(i=((w.event.special[a.origType]||{}).handle||a.handler).apply(o.elem,u))&&!1===(t.result=i)&&(t.preventDefault(),t.stopPropagation()))}return c.postDispatch&&c.postDispatch.call(this,t),t.result}},handlers:function(e,t){var n,r,i,o,a,s=[],u=t.delegateCount,l=e.target;if(u&&l.nodeType&&!("click"===e.type&&e.button>=1))for(;l!==this;l=l.parentNode||this)if(1===l.nodeType&&("click"!==e.type||!0!==l.disabled)){for(o=[],a={},n=0;n<u;n++)void 0===a[i=(r=t[n]).selector+" "]&&(a[i]=r.needsContext?w(i,this).index(l)>-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<t.length&&s.push({elem:l,handlers:t.slice(u)}),s},addProp:function(e,t){Object.defineProperty(w.Event.prototype,e,{enumerable:!0,configurable:!0,get:g(t)?function(){if(this.originalEvent)return t(this.originalEvent)}:function(){if(this.originalEvent)return this.originalEvent[e]},set:function(t){Object.defineProperty(this,e,{enumerable:!0,configurable:!0,writable:!0,value:t})}})},fix:function(e){return e[w.expando]?e:new w.Event(e)},special:{load:{noBubble:!0},focus:{trigger:function(){if(this!==Se()&&this.focus)return this.focus(),!1},delegateType:"focusin"},blur:{trigger:function(){if(this===Se()&&this.blur)return this.blur(),!1},delegateType:"focusout"},click:{trigger:function(){if("checkbox"===this.type&&this.click&&N(this,"input"))return this.click(),!1},_default:function(e){return N(e.target,"a")}},beforeunload:{postDispatch:function(e){void 0!==e.result&&e.originalEvent&&(e.originalEvent.returnValue=e.result)}}}},w.removeEvent=function(e,t,n){e.removeEventListener&&e.removeEventListener(t,n)},w.Event=function(e,t){if(!(this instanceof w.Event))return new w.Event(e,t);e&&e.type?(this.originalEvent=e,this.type=e.type,this.isDefaultPrevented=e.defaultPrevented||void 0===e.defaultPrevented&&!1===e.returnValue?Ee:ke,this.target=e.target&&3===e.target.nodeType?e.target.parentNode:e.target,this.currentTarget=e.currentTarget,this.relatedTarget=e.relatedTarget):this.type=e,t&&w.extend(this,t),this.timeStamp=e&&e.timeStamp||Date.now(),this[w.expando]=!0},w.Event.prototype={constructor:w.Event,isDefaultPrevented:ke,isPropagationStopped:ke,isImmediatePropagationStopped:ke,isSimulated:!1,preventDefault:function(){var e=this.originalEvent;this.isDefaultPrevented=Ee,e&&!this.isSimulated&&e.preventDefault()},stopPropagation:function(){var e=this.originalEvent;this.isPropagationStopped=Ee,e&&!this.isSimulated&&e.stopPropagation()},stopImmediatePropagation:function(){var e=this.originalEvent;this.isImmediatePropagationStopped=Ee,e&&!this.isSimulated&&e.stopImmediatePropagation(),this.stopPropagation()}},w.each({altKey:!0,bubbles:!0,cancelable:!0,changedTouches:!0,ctrlKey:!0,detail:!0,eventPhase:!0,metaKey:!0,pageX:!0,pageY:!0,shiftKey:!0,view:!0,"char":!0,charCode:!0,key:!0,keyCode:!0,button:!0,buttons:!0,clientX:!0,clientY:!0,offsetX:!0,offsetY:!0,pointerId:!0,pointerType:!0,screenX:!0,screenY:!0,targetTouches:!0,toElement:!0,touches:!0,which:function(e){var t=e.button;return null==e.which&&we.test(e.type)?null!=e.charCode?e.charCode:e.keyCode:!e.which&&void 0!==t&&Te.test(e.type)?1&t?1:2&t?3:4&t?2:0:e.which}},w.event.addProp),w.each({mouseenter:"mouseover",mouseleave:"mouseout",pointerenter:"pointerover",pointerleave:"pointerout"},function(e,t){w.event.special[e]={delegateType:t,bindType:t,handle:function(e){var n,r=this,i=e.relatedTarget,o=e.handleObj;return i&&(i===r||w.contains(r,i))||(e.type=o.origType,n=o.handler.apply(this,arguments),e.type=t),n}}}),w.fn.extend({on:function(e,t,n,r){return De(this,e,t,n,r)},one:function(e,t,n,r){return De(this,e,t,n,r,1)},off:function(e,t,n){var r,i;if(e&&e.preventDefault&&e.handleObj)return r=e.handleObj,w(e.delegateTarget).off(r.namespace?r.origType+"."+r.namespace:r.origType,r.selector,r.handler),this;if("object"==typeof e){for(i in e)this.off(i,t,e[i]);return this}return!1!==t&&"function"!=typeof t||(n=t,t=void 0),!1===n&&(n=ke),this.each(function(){w.event.remove(this,e,n,t)})}});var Ne=/<(?!area|br|col|embed|hr|img|input|link|meta|param)(([a-z][^\/\0>\x20\t\r\n\f]*)[^>]*)\/>/gi,Ae=/<script|<style|<link/i,je=/checked\s*(?:[^=]|=\s*.checked.)/i,qe=/^\s*<!(?:\[CDATA\[|--)|(?:\]\]|--)>\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;n<r;n++)w.event.add(t,i,l[i][n])}K.hasData(e)&&(s=K.access(e),u=w.extend({},s),K.set(t,u))}}function Me(e,t){var n=t.nodeName.toLowerCase();"input"===n&&pe.test(e.type)?t.checked=e.checked:"input"!==n&&"textarea"!==n||(t.defaultValue=e.defaultValue)}function Re(e,t,n,r){t=a.apply([],t);var i,o,s,u,l,c,f=0,p=e.length,d=p-1,y=t[0],v=g(y);if(v||p>1&&"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<p;f++)l=i,f!==d&&(l=w.clone(l,!0,!0),u&&w.merge(s,ye(l,"script"))),n.call(e[f],l,f);if(u)for(c=s[s.length-1].ownerDocument,w.map(s,Oe),f=0;f<u;f++)l=s[f],he.test(l.type||"")&&!J.access(l,"globalEval")&&w.contains(c,l)&&(l.src&&"module"!==(l.type||"").toLowerCase()?w._evalUrl&&w._evalUrl(l.src):m(l.textContent.replace(qe,""),c,l))}return e}function Ie(e,t,n){for(var r,i=t?w.filter(t,e):e,o=0;null!=(r=i[o]);o++)n||1!==r.nodeType||w.cleanData(ye(r)),r.parentNode&&(n&&w.contains(r.ownerDocument,r)&&ve(ye(r,"script")),r.parentNode.removeChild(r));return e}w.extend({htmlPrefilter:function(e){return e.replace(Ne,"<$1></$2>")},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;r<i;r++)Me(o[r],a[r]);if(t)if(n)for(o=o||ye(e),a=a||ye(s),r=0,i=o.length;r<i;r++)Pe(o[r],a[r]);else Pe(e,s);return(a=ye(s,"script")).length>0&&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<r;n++)1===(t=this[n]||{}).nodeType&&(w.cleanData(ye(t,!1)),t.innerHTML=e);t=0}catch(e){}}t&&this.empty().append(e)},null,e,arguments.length)},replaceWith:function(){var e=[];return Re(this,arguments,function(t){var n=this.parentNode;w.inArray(this,e)<0&&(w.cleanData(ye(this)),n&&n.replaceChild(t,this))},e)}}),w.each({appendTo:"append",prependTo:"prepend",insertBefore:"before",insertAfter:"after",replaceAll:"replaceWith"},function(e,t){w.fn[e]=function(e){for(var n,r=[],i=w(e),o=i.length-1,a=0;a<=o;a++)n=a===o?this:this.clone(!0),w(i[a])[t](n),s.apply(r,n.get());return this.pushStack(r)}});var We=new RegExp("^("+re+")(?!px)[a-z%]+$","i"),$e=function(t){var n=t.ownerDocument.defaultView;return n&&n.opener||(n=e),n.getComputedStyle(t)},Be=new RegExp(oe.join("|"),"i");!function(){function t(){if(c){l.style.cssText="position:absolute;left:-11111px;width:60px;margin-top:1px;padding:0;border:0",c.style.cssText="position:relative;display:block;box-sizing:border-box;overflow:scroll;margin:auto;border:1px;padding:1px;width:60%;top:1%",be.appendChild(l).appendChild(c);var t=e.getComputedStyle(c);i="1%"!==t.top,u=12===n(t.marginLeft),c.style.right="60%",s=36===n(t.right),o=36===n(t.width),c.style.position="absolute",a=36===c.offsetWidth||"absolute",be.removeChild(l),c=null}}function n(e){return Math.round(parseFloat(e))}var i,o,a,s,u,l=r.createElement("div"),c=r.createElement("div");c.style&&(c.style.backgroundClip="content-box",c.cloneNode(!0).style.backgroundClip="",h.clearCloneStyle="content-box"===c.style.backgroundClip,w.extend(h,{boxSizingReliable:function(){return t(),o},pixelBoxStyles:function(){return t(),s},pixelPosition:function(){return t(),i},reliableMarginLeft:function(){return t(),u},scrollboxSize:function(){return t(),a}}))}();function Fe(e,t,n){var r,i,o,a,s=e.style;return(n=n||$e(e))&&(""!==(a=n.getPropertyValue(t)||n[t])||w.contains(e.ownerDocument,e)||(a=w.style(e,t)),!h.pixelBoxStyles()&&We.test(a)&&Be.test(t)&&(r=s.width,i=s.minWidth,o=s.maxWidth,s.minWidth=s.maxWidth=s.width=a,a=n.width,s.width=r,s.minWidth=i,s.maxWidth=o)),void 0!==a?a+"":a}function _e(e,t){return{get:function(){if(!e())return(this.get=t).apply(this,arguments);delete this.get}}}var ze=/^(none|table(?!-c[ea]).+)/,Xe=/^--/,Ue={position:"absolute",visibility:"hidden",display:"block"},Ve={letterSpacing:"0",fontWeight:"400"},Ge=["Webkit","Moz","ms"],Ye=r.createElement("div").style;function Qe(e){if(e in Ye)return e;var t=e[0].toUpperCase()+e.slice(1),n=Ge.length;while(n--)if((e=Ge[n]+t)in Ye)return e}function Je(e){var t=w.cssProps[e];return t||(t=w.cssProps[e]=Qe(e)||e),t}function Ke(e,t,n){var r=ie.exec(t);return r?Math.max(0,r[2]-(n||0))+(r[3]||"px"):t}function Ze(e,t,n,r,i,o){var a="width"===t?1:0,s=0,u=0;if(n===(r?"border":"content"))return 0;for(;a<4;a+=2)"margin"===n&&(u+=w.css(e,n+oe[a],!0,i)),r?("content"===n&&(u-=w.css(e,"padding"+oe[a],!0,i)),"margin"!==n&&(u-=w.css(e,"border"+oe[a]+"Width",!0,i))):(u+=w.css(e,"padding"+oe[a],!0,i),"padding"!==n?u+=w.css(e,"border"+oe[a]+"Width",!0,i):s+=w.css(e,"border"+oe[a]+"Width",!0,i));return!r&&o>=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;a<i;a++)o[t[a]]=w.css(e,t[a],!1,r);return o}return void 0!==n?w.style(e,t,n):w.css(e,t)},e,t,arguments.length>1)}});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;o<a;o++)if(r=i[o].call(n,t,e))return r}function ct(e,t,n){var r,i,o,a,s,u,l,c,f="width"in t||"height"in t,p=this,d={},h=e.style,g=e.nodeType&&ae(e),y=J.get(e,"fxshow");n.queue||(null==(a=w._queueHooks(e,"fx")).unqueued&&(a.unqueued=0,s=a.empty.fire,a.empty.fire=function(){a.unqueued||s()}),a.unqueued++,p.always(function(){p.always(function(){a.unqueued--,w.queue(e,"fx").length||a.empty.fire()})}));for(r in t)if(i=t[r],it.test(i)){if(delete t[r],o=o||"toggle"===i,i===(g?"hide":"show")){if("show"!==i||!y||void 0===y[r])continue;g=!0}d[r]=y&&y[r]||w.style(e,r)}if((u=!w.isEmptyObject(t))||!w.isEmptyObject(d)){f&&1===e.nodeType&&(n.overflow=[h.overflow,h.overflowX,h.overflowY],null==(l=y&&y.display)&&(l=J.get(e,"display")),"none"===(c=w.css(e,"display"))&&(l?c=l:(fe([e],!0),l=e.style.display||l,c=w.css(e,"display"),fe([e]))),("inline"===c||"inline-block"===c&&null!=l)&&"none"===w.css(e,"float")&&(u||(p.done(function(){h.display=l}),null==l&&(c=h.display,l="none"===c?"":c)),h.display="inline-block")),n.overflow&&(h.overflow="hidden",p.always(function(){h.overflow=n.overflow[0],h.overflowX=n.overflow[1],h.overflowY=n.overflow[2]})),u=!1;for(r in d)u||(y?"hidden"in y&&(g=y.hidden):y=J.access(e,"fxshow",{display:l}),o&&(y.hidden=!g),g&&fe([e],!0),p.done(function(){g||fe([e]),J.remove(e,"fxshow");for(r in d)w.style(e,r,d[r])})),u=lt(g?y[r]:0,r,p),r in y||(y[r]=u.start,g&&(u.end=u.start,u.start=0))}}function ft(e,t){var n,r,i,o,a;for(n in e)if(r=G(n),i=t[r],o=e[n],Array.isArray(o)&&(i=o[1],o=e[n]=o[0]),n!==r&&(e[r]=o,delete e[n]),(a=w.cssHooks[r])&&"expand"in a){o=a.expand(o),delete e[r];for(n in o)n in e||(e[n]=o[n],t[n]=i)}else t[r]=i}function pt(e,t,n){var r,i,o=0,a=pt.prefilters.length,s=w.Deferred().always(function(){delete u.elem}),u=function(){if(i)return!1;for(var t=nt||st(),n=Math.max(0,l.startTime+l.duration-t),r=1-(n/l.duration||0),o=0,a=l.tweens.length;o<a;o++)l.tweens[o].run(r);return s.notifyWith(e,[l,r,n]),r<1&&a?n:(a||s.notifyWith(e,[l,1,0]),s.resolveWith(e,[l]),!1)},l=s.promise({elem:e,props:w.extend({},t),opts:w.extend(!0,{specialEasing:{},easing:w.easing._default},n),originalProperties:t,originalOptions:n,startTime:nt||st(),duration:n.duration,tweens:[],createTween:function(t,n){var r=w.Tween(e,l.opts,t,n,l.opts.specialEasing[t]||l.opts.easing);return l.tweens.push(r),r},stop:function(t){var n=0,r=t?l.tweens.length:0;if(i)return this;for(i=!0;n<r;n++)l.tweens[n].run(1);return t?(s.notifyWith(e,[l,1,0]),s.resolveWith(e,[l,t])):s.rejectWith(e,[l,t]),this}}),c=l.props;for(ft(c,l.opts.specialEasing);o<a;o++)if(r=pt.prefilters[o].call(l,e,c,l.opts))return g(r.stop)&&(w._queueHooks(l.elem,l.opts.queue).stop=r.stop.bind(r)),r;return w.map(c,lt,l),g(l.opts.start)&&l.opts.start.call(e,l),l.progress(l.opts.progress).done(l.opts.done,l.opts.complete).fail(l.opts.fail).always(l.opts.always),w.fx.timer(w.extend(u,{elem:e,anim:l,queue:l.opts.queue})),l}w.Animation=w.extend(pt,{tweeners:{"*":[function(e,t){var n=this.createTween(e,t);return ue(n.elem,e,ie.exec(t),n),n}]},tweener:function(e,t){g(e)?(t=e,e=["*"]):e=e.match(M);for(var n,r=0,i=e.length;r<i;r++)n=e[r],pt.tweeners[n]=pt.tweeners[n]||[],pt.tweeners[n].unshift(t)},prefilters:[ct],prefilter:function(e,t){t?pt.prefilters.unshift(e):pt.prefilters.push(e)}}),w.speed=function(e,t,n){var r=e&&"object"==typeof e?w.extend({},e):{complete:n||!n&&t||g(e)&&e,duration:e,easing:n&&t||t&&!g(t)&&t};return w.fx.off?r.duration=0:"number"!=typeof r.duration&&(r.duration in w.fx.speeds?r.duration=w.fx.speeds[r.duration]:r.duration=w.fx.speeds._default),null!=r.queue&&!0!==r.queue||(r.queue="fx"),r.old=r.complete,r.complete=function(){g(r.old)&&r.old.call(this),r.queue&&w.dequeue(this,r.queue)},r},w.fn.extend({fadeTo:function(e,t,n,r){return this.filter(ae).css("opacity",0).show().end().animate({opacity:t},e,n,r)},animate:function(e,t,n,r){var i=w.isEmptyObject(e),o=w.speed(t,n,r),a=function(){var t=pt(this,w.extend({},e),o);(i||J.get(this,"finish"))&&t.stop(!0)};return a.finish=a,i||!1===o.queue?this.each(a):this.queue(o.queue,a)},stop:function(e,t,n){var r=function(e){var t=e.stop;delete e.stop,t(n)};return"string"!=typeof e&&(n=t,t=e,e=void 0),t&&!1!==e&&this.queue(e||"fx",[]),this.each(function(){var t=!0,i=null!=e&&e+"queueHooks",o=w.timers,a=J.get(this);if(i)a[i]&&a[i].stop&&r(a[i]);else for(i in a)a[i]&&a[i].stop&&ot.test(i)&&r(a[i]);for(i=o.length;i--;)o[i].elem!==this||null!=e&&o[i].queue!==e||(o[i].anim.stop(n),t=!1,o.splice(i,1));!t&&n||w.dequeue(this,e)})},finish:function(e){return!1!==e&&(e=e||"fx"),this.each(function(){var t,n=J.get(this),r=n[e+"queue"],i=n[e+"queueHooks"],o=w.timers,a=r?r.length:0;for(n.finish=!0,w.queue(this,e,[]),i&&i.stop&&i.stop.call(this,!0),t=o.length;t--;)o[t].elem===this&&o[t].queue===e&&(o[t].anim.stop(!0),o.splice(t,1));for(t=0;t<a;t++)r[t]&&r[t].finish&&r[t].finish.call(this);delete n.finish})}}),w.each(["toggle","show","hide"],function(e,t){var n=w.fn[t];w.fn[t]=function(e,r,i){return null==e||"boolean"==typeof e?n.apply(this,arguments):this.animate(ut(t,!0),e,r,i)}}),w.each({slideDown:ut("show"),slideUp:ut("hide"),slideToggle:ut("toggle"),fadeIn:{opacity:"show"},fadeOut:{opacity:"hide"},fadeToggle:{opacity:"toggle"}},function(e,t){w.fn[e]=function(e,n,r){return this.animate(t,e,n,r)}}),w.timers=[],w.fx.tick=function(){var e,t=0,n=w.timers;for(nt=Date.now();t<n.length;t++)(e=n[t])()||n[t]!==e||n.splice(t--,1);n.length||w.fx.stop(),nt=void 0},w.fx.timer=function(e){w.timers.push(e),w.fx.start()},w.fx.interval=13,w.fx.start=function(){rt||(rt=!0,at())},w.fx.stop=function(){rt=null},w.fx.speeds={slow:600,fast:200,_default:400},w.fn.delay=function(t,n){return t=w.fx?w.fx.speeds[t]||t:t,n=n||"fx",this.queue(n,function(n,r){var i=e.setTimeout(n,t);r.stop=function(){e.clearTimeout(i)}})},function(){var e=r.createElement("input"),t=r.createElement("select").appendChild(r.createElement("option"));e.type="checkbox",h.checkOn=""!==e.value,h.optSelected=t.selected,(e=r.createElement("input")).value="t",e.type="radio",h.radioValue="t"===e.value}();var dt,ht=w.expr.attrHandle;w.fn.extend({attr:function(e,t){return z(this,w.attr,e,t,arguments.length>1)},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<u;r++)if(((n=i[r]).selected||r===o)&&!n.disabled&&(!n.parentNode.disabled||!N(n.parentNode,"optgroup"))){if(t=w(n).val(),a)return t;s.push(t)}return s},set:function(e,t){var n,r,i=e.options,o=w.makeArray(t),a=i.length;while(a--)((r=i[a]).selected=w.inArray(w.valHooks.option.get(r),o)>-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("<script>").prop({charset:e.scriptCharset,src:e.url}).on("load error",n=function(e){t.remove(),n=null,e&&o("error"===e.type?404:200,e.type)}),r.head.appendChild(t[0])},abort:function(){n&&n()}}}});var Yt=[],Qt=/(=)\?(?=&|$)|\?\?/;w.ajaxSetup({jsonp:"callback",jsonpCallback:function(){var e=Yt.pop()||w.expando+"_"+Et++;return this[e]=!0,e}}),w.ajaxPrefilter("json jsonp",function(t,n,r){var i,o,a,s=!1!==t.jsonp&&(Qt.test(t.url)?"url":"string"==typeof t.data&&0===(t.contentType||"").indexOf("application/x-www-form-urlencoded")&&Qt.test(t.data)&&"data");if(s||"jsonp"===t.dataTypes[0])return i=t.jsonpCallback=g(t.jsonpCallback)?t.jsonpCallback():t.jsonpCallback,s?t[s]=t[s].replace(Qt,"$1"+i):!1!==t.jsonp&&(t.url+=(kt.test(t.url)?"&":"?")+t.jsonp+"="+i),t.converters["script json"]=function(){return a||w.error(i+" was not called"),a[0]},t.dataTypes[0]="json",o=e[i],e[i]=function(){a=arguments},r.always(function(){void 0===o?w(e).removeProp(i):e[i]=o,t[i]&&(t.jsonpCallback=n.jsonpCallback,Yt.push(i)),a&&g(o)&&o(a[0]),a=o=void 0}),"script"}),h.createHTMLDocument=function(){var e=r.implementation.createHTMLDocument("").body;return e.innerHTML="<form></form><form></form>",2===e.childNodes.length}(),w.parseHTML=function(e,t,n){if("string"!=typeof e)return[];"boolean"==typeof t&&(n=t,t=!1);var i,o,a;return t||(h.createHTMLDocument?((i=(t=r.implementation.createHTMLDocument("")).createElement("base")).href=r.location.href,t.head.appendChild(i)):t=r),o=A.exec(e),a=!n&&[],o?[t.createElement(o[1])]:(o=xe([e],t,a),a&&a.length&&w(a).remove(),w.merge([],o.childNodes))},w.fn.load=function(e,t,n){var r,i,o,a=this,s=e.indexOf(" ");return s>-1&&(r=vt(e.slice(s)),e=e.slice(0,s)),g(t)?(n=t,t=void 0):t&&"object"==typeof t&&(i="POST"),a.length>0&&w.ajax({url:e,type:i||"GET",dataType:"html",data:t}).done(function(e){o=arguments,a.html(r?w("<div>").append(w.parseHTML(e)).find(r):e)}).always(n&&function(e,t){a.each(function(){n.apply(this,o||[e.responseText,t,e])})}),this},w.each(["ajaxStart","ajaxStop","ajaxComplete","ajaxError","ajaxSuccess","ajaxSend"],function(e,t){w.fn[t]=function(e){return this.on(t,e)}}),w.expr.pseudos.animated=function(e){return w.grep(w.timers,function(t){return e===t.elem}).length},w.offset={setOffset:function(e,t,n){var r,i,o,a,s,u,l,c=w.css(e,"position"),f=w(e),p={};"static"===c&&(e.style.position="relative"),s=f.offset(),o=w.css(e,"top"),u=w.css(e,"left"),(l=("absolute"===c||"fixed"===c)&&(o+u).indexOf("auto")>-1)?(a=(r=f.position()).top,i=r.left):(a=parseFloat(o)||0,i=parseFloat(u)||0),g(t)&&(t=t.call(e,n,w.extend({},s))),null!=t.top&&(p.top=t.top-s.top+a),null!=t.left&&(p.left=t.left-s.left+i),"using"in t?t.using.call(e,p):f.css(p)}},w.fn.extend({offset:function(e){if(arguments.length)return void 0===e?this:this.each(function(t){w.offset.setOffset(this,e,t)});var t,n,r=this[0];if(r)return r.getClientRects().length?(t=r.getBoundingClientRect(),n=r.ownerDocument.defaultView,{top:t.top+n.pageYOffset,left:t.left+n.pageXOffset}):{top:0,left:0}},position:function(){if(this[0]){var e,t,n,r=this[0],i={top:0,left:0};if("fixed"===w.css(r,"position"))t=r.getBoundingClientRect();else{t=this.offset(),n=r.ownerDocument,e=r.offsetParent||n.documentElement;while(e&&(e===n.body||e===n.documentElement)&&"static"===w.css(e,"position"))e=e.parentNode;e&&e!==r&&1===e.nodeType&&((i=w(e).offset()).top+=w.css(e,"borderTopWidth",!0),i.left+=w.css(e,"borderLeftWidth",!0))}return{top:t.top-i.top-w.css(r,"marginTop",!0),left:t.left-i.left-w.css(r,"marginLeft",!0)}}},offsetParent:function(){return this.map(function(){var e=this.offsetParent;while(e&&"static"===w.css(e,"position"))e=e.offsetParent;return e||be})}}),w.each({scrollLeft:"pageXOffset",scrollTop:"pageYOffset"},function(e,t){var n="pageYOffset"===t;w.fn[e]=function(r){return z(this,function(e,r,i){var o;if(y(e)?o=e:9===e.nodeType&&(o=e.defaultView),void 0===i)return o?o[t]:e[r];o?o.scrollTo(n?o.pageXOffset:i,n?i:o.pageYOffset):e[r]=i},e,r,arguments.length)}}),w.each(["top","left"],function(e,t){w.cssHooks[t]=_e(h.pixelPosition,function(e,n){if(n)return n=Fe(e,t),We.test(n)?w(e).position()[t]+"px":n})}),w.each({Height:"height",Width:"width"},function(e,t){w.each({padding:"inner"+e,content:t,"":"outer"+e},function(n,r){w.fn[r]=function(i,o){var a=arguments.length&&(n||"boolean"!=typeof i),s=n||(!0===i||!0===o?"margin":"border");return z(this,function(t,n,i){var o;return y(t)?0===r.indexOf("outer")?t["inner"+e]:t.document.documentElement["client"+e]:9===t.nodeType?(o=t.documentElement,Math.max(t.body["scroll"+e],o["scroll"+e],t.body["offset"+e],o["offset"+e],o["client"+e])):void 0===i?w.css(t,n,s):w.style(t,n,i,s)},t,a?i:void 0,a)}})}),w.each("blur focus focusin focusout resize scroll click dblclick mousedown mouseup mousemove mouseover mouseout mouseenter mouseleave change select submit keydown keypress keyup contextmenu".split(" "),function(e,t){w.fn[t]=function(e,n){return arguments.length>0?this.on(t,null,e,n):this.trigger(t)}}),w.fn.extend({hover:function(e,t){return this.mouseenter(e).mouseleave(t||e)}}),w.fn.extend({bind:function(e,t,n){return this.on(e,null,t,n)},unbind:function(e,t){return this.off(e,null,t)},delegate:function(e,t,n,r){return this.on(t,e,n,r)},undelegate:function(e,t,n){return 1===arguments.length?this.off(e,"**"):this.off(t,e||"**",n)}}),w.proxy=function(e,t){var n,r,i;if("string"==typeof t&&(n=e[t],t=e,e=n),g(e))return r=o.call(arguments,2),i=function(){return e.apply(t||this,r.concat(o.call(arguments)))},i.guid=e.guid=e.guid||w.guid++,i},w.holdReady=function(e){e?w.readyWait++:w.ready(!0)},w.isArray=Array.isArray,w.parseJSON=JSON.parse,w.nodeName=N,w.isFunction=g,w.isWindow=y,w.camelCase=G,w.type=x,w.now=Date.now,w.isNumeric=function(e){var t=w.type(e);return("number"===t||"string"===t)&&!isNaN(e-parseFloat(e))},"function"==typeof define&&define.amd&&define("jquery",[],function(){return w});var Jt=e.jQuery,Kt=e.$;return w.noConflict=function(t){return e.$===w&&(e.$=Kt),t&&e.jQuery===w&&(e.jQuery=Jt),w},t||(e.jQuery=e.$=w),w});|]
+ src/Crux/Version.hs view
@@ -0,0 +1,9 @@+module Crux.Version where++import Data.Version (showVersion)+import qualified Paths_crux (version)++version :: String+version = showVersion Paths_crux.version++