fix no-colors for help/version

crucible-concurrency/crucible-concurrency.cabal

@@ -35,6 +35,7 @@ library
                      , crucible
                      , crucible-syntax
                      , crux
+                     , generic-lens
                      , lens
                      , megaparsec
                      , mtl

crucible-concurrency/src/Cruces/ExploreCrux.hs

@@ -4,15 +4,19 @@ Description      : Wrappers for driving Crucibles with Crux
 Copyright        : (c) Galois, Inc 2021
 Maintainer       : Alexander Bakst <[email protected]>
 -}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeApplications #-}
+
 module Cruces.ExploreCrux where
 
 import           Control.Monad.IO.Class
 import           Control.Monad (when)
 import           Control.Lens
+import           Data.Generics.Product.Fields (field, setField)
 import qualified Data.Vector as V
 import qualified Data.Map.Strict as Map
 import           System.IO (Handle)
@@ -29,6 +33,7 @@ import           Lang.Crucible.CFG.Extension (IsSyntaxExtension)
 import           Lang.Crucible.Backend
 
 import qualified Crux
+import qualified Crux.Config.Common as Crux
 
 import           Crucibles.SchedulingAlgorithm hiding (_exec, exec)
 import           Crucibles.Execution
@@ -120,9 +125,9 @@ exploreOvr symOnline cruxOpts mainAct =
         do sym <- getSymInterface
            ctx <- use stateContext
            todo <- liftIO $ getProofObligations sym
-           let cruxOpts' = cruxOpts { Crux.quietMode = True, Crux.simVerbose = 0 }
+           let cruxOpts' = over (field @"outputOptions") (setField @"quietMode" True . setField @"simVerbose" 0) cruxOpts
            mkOutCfg <- liftIO $ Crux.defaultOutputConfig Crux.cruxLogMessageToSayWhat
-           let ?outputConfig = mkOutCfg (Just cruxOpts')
+           let ?outputConfig = mkOutCfg (Just (Crux.outputOptions cruxOpts'))
            (processed, _) <- liftIO $ proveGoalsOnline sym cruxOpts' ctx (\_ _ -> return mempty) todo
            let provedAll = totalProcessedGoals processed == provedGoals processed
            when provedAll $ liftIO $ clearProofObligations sym

crucible-go/tool/Main.hs

@@ -15,6 +15,7 @@ import Lang.Crucible.Simulator
 
 -- crux
 import qualified Crux
+import qualified Crux.Config.Common as Crux
 
 -- Go
 import Language.Go.Parser
@@ -40,7 +41,7 @@ cruxGoConfig = Crux.Config
 simulateGo :: Crux.CruxOptions -> GoOptions -> Crux.SimulatorCallback msgs
 simulateGo copts _opts = Crux.SimulatorCallback $ \sym _maybeOnline -> do
    let files = Crux.inputFiles copts
-   let verbosity = Crux.simVerbose copts
+   let verbosity = Crux.simVerbose (Crux.outputOptions copts)
    file <- case files of
              [f] -> return f
              _ -> fail "crux-go requires a single file name as an argument"

crucible-jvm/crucible-jvm.cabal

@@ -99,4 +99,3 @@ library
   ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
   ghc-prof-options: -O2 -fprof-auto-top
   default-language: Haskell2010
-

crucible-jvm/tool/Main.hs

@@ -178,7 +178,7 @@ cruxJVMConfig = Crux.Config
 simulateJVM :: Crux.CruxOptions -> JVMOptions -> Crux.SimulatorCallback msgs
 simulateJVM copts opts = Crux.SimulatorCallback $ \sym _maybeOnline -> do
    let files = Crux.inputFiles copts
-   let verbosity = Crux.simVerbose copts
+   let verbosity = Crux.simVerbose (Crux.outputOptions copts)
    file <- case files of
              [file] -> return file
              _ -> fail "crux-jvm requires a single file name as an argument"

crux-llvm/for-ide/Main.hs

@@ -7,7 +7,7 @@ module Main (main) where
 import Control.Lens (makeLenses, set, view)
 import Crux (OutputConfig)
 import qualified Crux
-import Crux.Config.Common (CruxOptions)
+import Crux.Config.Common (OutputOptions)
 import Crux.LLVM.Config (LLVMOptions, llvmCruxConfig)
 import CruxLLVMMain
   ( CruxLLVMLogging,
@@ -74,7 +74,7 @@ forIDEConfig = do
       }
 
 mainWithOutputConfig ::
-  (Maybe CruxOptions -> OutputConfig CruxLLVMLogging) -> IO ExitCode
+  (Maybe OutputOptions -> OutputConfig CruxLLVMLogging) -> IO ExitCode
 mainWithOutputConfig mkOutCfg =
   CruxLLVMMain.withCruxLLVMLogging $
     do

crux-llvm/for-ide/unix/RealMain.hs

@@ -2,7 +2,7 @@ module RealMain (makeMain) where
 
 import Control.Monad (void)
 import Crux.Log ( OutputConfig )
-import Crux.Config.Common (CruxOptions)
+import Crux.Config.Common (OutputOptions)
 import CruxLLVMMain ( CruxLLVMLogging, defaultOutputConfig )
 import System.Exit (ExitCode, exitWith)
 import System.Posix.Process (getProcessGroupID)
@@ -25,7 +25,7 @@ installSIGTERMHandler =
     handler gid = signalProcessGroup sigTERM gid
 
 makeMain ::
-  ((Maybe CruxOptions -> OutputConfig CruxLLVMLogging) -> IO ExitCode) ->
+  ((Maybe OutputOptions -> OutputConfig CruxLLVMLogging) -> IO ExitCode) ->
   IO ()
 makeMain mainWithOutputConfig =
   do

crux-llvm/src/CruxLLVMMain.hs

@@ -28,7 +28,7 @@ import           System.IO ( Handle )
 -- crux
 import qualified Crux
 import qualified Crux.Log as Log
-import           Crux.Config.Common (CruxOptions(..))
+import           Crux.Config.Common (CruxOptions(..), OutputOptions)
 
 -- local
 import           Crux.LLVM.Config
@@ -51,7 +51,7 @@ cruxLLVMLoggingToSayWhat :: CruxLLVMLogging -> Crux.SayWhat
 cruxLLVMLoggingToSayWhat (LoggingCrux msg) = Log.cruxLogMessageToSayWhat msg
 cruxLLVMLoggingToSayWhat (LoggingCruxLLVM msg) = Log.cruxLLVMLogMessageToSayWhat msg
 
-defaultOutputConfig :: IO (Maybe CruxOptions -> Log.OutputConfig CruxLLVMLogging)
+defaultOutputConfig :: IO (Maybe OutputOptions -> Log.OutputConfig CruxLLVMLogging)
 defaultOutputConfig = Crux.defaultOutputConfig cruxLLVMLoggingToSayWhat
 
 withCruxLLVMLogging ::
@@ -67,7 +67,7 @@ withCruxLLVMLogging a =
   in a
 
 mainWithOutputConfig ::
-  (Maybe CruxOptions -> Log.OutputConfig CruxLLVMLogging) ->
+  (Maybe OutputOptions -> Log.OutputConfig CruxLLVMLogging) ->
   IO ExitCode
 mainWithOutputConfig mkOutCfg = withCruxLLVMLogging $ do
   cfg <- llvmCruxConfig

crux-llvm/svcomp/Main.hs

@@ -51,7 +51,7 @@ import Lang.Crucible.Backend ( CrucibleEvent(..) )
 
 -- crux
 import qualified Crux
-import Crux.Config.Common ( CruxOptions(..) )
+import Crux.Config.Common ( CruxOptions(..), outputOptions )
 import qualified Crux.Log as Log
 import Crux.Report
 import Crux.SVCOMP hiding (SVCompLanguage(..))
@@ -134,7 +134,7 @@ processInputFiles cruxOpts llvmOpts svOpts =
     evaluateBitCode :: FilePath -> FilePath -> IO ()
     evaluateBitCode inputFile bcFile = withSVCompLogging $ do
       mkOutCfg <- Crux.defaultOutputConfig svCompLoggingToSayWhat
-      let ?outputConfig = mkOutCfg (Just cruxOpts)
+      let ?outputConfig = mkOutCfg (Just (outputOptions cruxOpts))
       mres <- try $
                do res <- Crux.runSimulator cruxOpts (simulateLLVMFile bcFile llvmOpts)
                   generateReport cruxOpts res

crux-mir/src/Mir/Language.hs

@@ -84,6 +84,7 @@ import qualified What4.FunctionName                    as W4
 
 -- crux
 import qualified Crux
+import qualified Crux.Config.Common as Crux
 import qualified Crux.Log as Log
 import qualified Crux.Model as Crux
 import qualified Crux.UI.JS as Crux
@@ -112,7 +113,7 @@ import           Mir.TransTy
 import           Mir.Concurrency
 import           Paths_crux_mir (version)
 
-defaultOutputConfig :: IO (Maybe Crux.CruxOptions -> OutputConfig MirLogging)
+defaultOutputConfig :: IO (Maybe Crux.OutputOptions -> OutputConfig MirLogging)
 defaultOutputConfig = Crux.defaultOutputConfig mirLoggingToSayWhat
 
 main :: IO ()
@@ -151,7 +152,7 @@ withMirLogging computation =
         ?injectMirLogMessage = LoggingMir
      in computation
 
-mainWithOutputConfig :: (Maybe Crux.CruxOptions -> OutputConfig MirLogging)
+mainWithOutputConfig :: (Maybe Crux.OutputOptions -> OutputConfig MirLogging)
                      -> BindExtraOverridesFn -> IO ExitCode
 mainWithOutputConfig mkOutCfg bindExtra =
     withMirLogging $
@@ -203,7 +204,7 @@ runTestsWithExtraOverrides ::
     (Crux.CruxOptions, MIROptions) ->
     IO ExitCode
 runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do
-    let ?debug              = Crux.simVerbose cruxOpts
+    let ?debug              = Crux.simVerbose (Crux.outputOptions cruxOpts)
     --let ?assertFalseOnError = assertFalse mirOpts
     let ?assertFalseOnError = True
     let ?printCrucible      = printCrucible mirOpts
@@ -356,7 +357,7 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do
           case simTest symOnline fnName of
             SomeTestOvr testFn features personality -> do
               let outH = view outputHandle ?outputConfig
-              setSimulatorVerbosity (Crux.simVerbose cruxOpts) sym
+              setSimulatorVerbosity (Crux.simVerbose (Crux.outputOptions cruxOpts)) sym
               let simCtx = C.initSimContext sym mirIntrinsicTypes halloc outH
                       (C.FnBindings C.emptyHandleMap) mirExtImpl personality
               return (Crux.RunnableStateWithExtensions

crux-mir/test/Test.hs

@@ -78,20 +78,23 @@ runCrux rustFile outHandle mode =
     -- regression (#627).  This keeps CI from breaking while we investigate.
     -- TODO: revert the timeout to 180 once performance is fixed
     let quiet = True
-    let options = (defaultCruxOptions { Crux.inputFiles = [rustFile],
-                                        Crux.simVerbose = 0,
+    let outOpts = (Crux.outputOptions defaultCruxOptions)
+                    { Crux.simVerbose = 0
+                    , Crux.quietMode = quiet
+                    }
+    let options = (defaultCruxOptions { Crux.outputOptions = outOpts,
+                                        Crux.inputFiles = [rustFile],
                                         Crux.globalTimeout = Just 600,
                                         Crux.goalTimeout = Just 600,
                                         Crux.solver = "z3",
-                                        Crux.quietMode = quiet,
                                         Crux.checkPathSat = (mode == RcmCoverage),
                                         Crux.outDir = case mode of
                                             RcmCoverage -> getOutputDir rustFile
                                             _ -> "",
                                         Crux.branchCoverage = (mode == RcmCoverage) } ,
                    Mir.defaultMirOptions { Mir.printResultOnly = (mode == RcmConcrete) })
     let ?outputConfig = Crux.mkOutputConfig (outHandle, False) (outHandle, False) Mir.mirLoggingToSayWhat $
-                        Just (fst options)
+                        Just (Crux.outputOptions (fst options))
     _exitCode <- Mir.runTests options
     return ()
 

crux/crux.cabal

@@ -34,6 +34,7 @@ library
     crucible,
     directory,
     filepath,
+    generic-lens,
     haskeline >= 0.7,
     lens,
     libBF >= 0.6 && < 0.7,

crux/src/Crux.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE NoMonoLocalBinds #-}
@@ -33,6 +34,7 @@ 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           Data.Proxy ( Proxy(..) )
@@ -145,26 +147,27 @@ postprocessSimResult showFailedGoals opts res =
 --   its continuation.
 loadOptions ::
   SupportsCruxLogMessage msgs =>
-  (Maybe CruxOptions -> OutputConfig 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
-     opts <- Cfg.loadConfig nm optSpec
+     (copts, opts) <- Cfg.loadConfig nm optSpec
      case opts of
        Cfg.ShowHelp ->
-          do let ?outputConfig = mkOutCfg Nothing
+          do let ?outputConfig = mkOutCfg (Just (defaultOutputOptions copts))
              showHelp nm optSpec
              exitSuccess
        Cfg.ShowVersion ->
-          do let ?outputConfig = mkOutCfg Nothing
+          do let ?outputConfig = mkOutCfg (Just (defaultOutputOptions copts))
              showVersion nm ver
              exitSuccess
-       Cfg.Options (crux, os) files ->
-          do let ?outputConfig = mkOutCfg (Just crux)
+       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)
 
@@ -215,12 +218,13 @@ showVersion nm ver = sayCrux (Log.Version nm ver)
 mkOutputConfig ::
   JSON.ToJSON msgs =>
   (Handle, Bool) -> (Handle, Bool) ->
-  (msgs -> SayWhat) -> Maybe CruxOptions ->
+  (msgs -> SayWhat) -> Maybe OutputOptions ->
   OutputConfig msgs
 mkOutputConfig (outHandle, outWantsColor) (errHandle, errWantsColor) logMessageToSayWhat opts =
-  let consensusBetween wants maybeRefuses = wants && not (maybe False maybeRefuses opts)
-      outSpec = (outHandle, consensusBetween outWantsColor noColorsOut)
-      errSpec@(_, errShouldColor) = (errHandle, consensusBetween errWantsColor noColorsErr)
+  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
@@ -266,7 +270,7 @@ mkOutputConfig (outHandle, outWantsColor) (errHandle, errWantsColor) logMessageT
 
 defaultOutputConfig ::
   JSON.ToJSON msgs =>
-  (msgs -> SayWhat) -> IO (Maybe CruxOptions -> OutputConfig msgs)
+  (msgs -> SayWhat) -> IO (Maybe OutputOptions -> OutputConfig msgs)
 defaultOutputConfig logMessagesToSayWhat = do
   outWantsColor <- AC.hSupportsANSIColor stdout
   errWantsColor <- AC.hSupportsANSIColor stderr
@@ -453,11 +457,12 @@ setupSolver cruxOpts mInteractionFile sym = do
   -- Turn on hash-consing, if enabled
   when (hashConsing cruxOpts) (WEB.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 cruxOpts > 1
-                                       then simVerbose cruxOpts - 1
+  symCfg sym verbosity $ toInteger $ if simVerbose outOpts > 1
+                                       then simVerbose outOpts - 1
                                        else 0
 
 -- | A GADT to capture the online solver constraints when we need them