diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,13 @@ ## NEXT +## 0.9.6.3.7 (2026-06-04) + +- Migrate from cmdargs to base:System.Console.GetOpt + [#842](https://github.com/ucsd-progsys/liquid-fixpoint/pull/842) + [#843](https://github.com/ucsd-progsys/liquid-fixpoint/pull/843) + [#844](https://github.com/ucsd-progsys/liquid-fixpoint/pull/844) + ## 0.9.6.3.6 (2026-05-06) - Drop dependency on lens-family [#841](http://github.com/ucsd-progsys/liquid-fixpoint/pull/841) diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal --- a/liquid-fixpoint.cabal +++ b/liquid-fixpoint.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquid-fixpoint -version: 0.9.6.3.6 +version: 0.9.6.3.7 synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description: This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint @@ -121,6 +121,7 @@ Language.Fixpoint.Utils.Progress Language.Fixpoint.Utils.Statistics Language.Fixpoint.Utils.Trie + Language.Fixpoint.Verbosity Text.PrettyPrint.HughesPJ.Compat other-modules: Paths_liquid_fixpoint autogen-modules: Paths_liquid_fixpoint @@ -136,7 +137,6 @@ , boxes , bytestring >= 0.10.2.1 , cereal - , cmdargs , containers , deepseq , directory diff --git a/src/Language/Fixpoint/Horn/Solve.hs b/src/Language/Fixpoint/Horn/Solve.hs --- a/src/Language/Fixpoint/Horn/Solve.hs +++ b/src/Language/Fixpoint/Horn/Solve.hs @@ -22,7 +22,7 @@ import Text.PrettyPrint.HughesPJ.Compat ( render ) import Language.Fixpoint.Horn.Info ( hornFInfo ) -import System.Console.CmdArgs.Verbosity ( whenLoud ) +import Language.Fixpoint.Verbosity ( whenLoud ) import qualified Data.Aeson as Aeson -- import Debug.Trace (traceM) diff --git a/src/Language/Fixpoint/Horn/Transformations.hs b/src/Language/Fixpoint/Horn/Transformations.hs --- a/src/Language/Fixpoint/Horn/Transformations.hs +++ b/src/Language/Fixpoint/Horn/Transformations.hs @@ -34,7 +34,7 @@ import Control.Monad.State import Data.Maybe (catMaybes, mapMaybe, fromMaybe) import Language.Fixpoint.Types.Visitor as V -import System.Console.CmdArgs.Verbosity +import Language.Fixpoint.Verbosity import Data.Bifunctor (first, second) import System.IO (hFlush, stdout) -- import qualified Debug.Trace as DBG diff --git a/src/Language/Fixpoint/Misc.hs b/src/Language/Fixpoint/Misc.hs --- a/src/Language/Fixpoint/Misc.hs +++ b/src/Language/Fixpoint/Misc.hs @@ -31,7 +31,7 @@ import Data.Unique import Debug.Trace (trace) import System.Console.ANSI -import System.Console.CmdArgs.Verbosity (whenLoud) +import Language.Fixpoint.Verbosity (whenLoud) import System.Process (system) import System.Directory (createDirectoryIfMissing) import System.FilePath (takeDirectory) diff --git a/src/Language/Fixpoint/Smt/Interface.hs b/src/Language/Fixpoint/Smt/Interface.hs --- a/src/Language/Fixpoint/Smt/Interface.hs +++ b/src/Language/Fixpoint/Smt/Interface.hs @@ -92,7 +92,7 @@ -- import Data.Text.Format import qualified Data.Text.Lazy.IO as LTIO import System.Directory -import System.Console.CmdArgs.Verbosity +import Language.Fixpoint.Verbosity import System.FilePath import System.IO import qualified Data.Attoparsec.Text as A diff --git a/src/Language/Fixpoint/Solver.hs b/src/Language/Fixpoint/Solver.hs --- a/src/Language/Fixpoint/Solver.hs +++ b/src/Language/Fixpoint/Solver.hs @@ -32,7 +32,7 @@ import qualified Data.Text.Lazy.IO as LT import qualified Data.Text.Lazy.Encoding as LT import System.Exit (ExitCode (..)) -import System.Console.CmdArgs.Verbosity (whenNormal, whenLoud) +import Language.Fixpoint.Verbosity (whenNormal, whenLoud) import Control.Monad (when) import Control.Exception (SomeException, catch) import Control.Exception.Compat diff --git a/src/Language/Fixpoint/Solver/EnvironmentReduction.hs b/src/Language/Fixpoint/Solver/EnvironmentReduction.hs --- a/src/Language/Fixpoint/Solver/EnvironmentReduction.hs +++ b/src/Language/Fixpoint/Solver/EnvironmentReduction.hs @@ -585,6 +585,8 @@ view :: Lens' s a -> s -> a view l s = getConst (l Const s) +infixr 4 %~ + (%~) :: Lens' s a -> (a -> a) -> s -> s (%~) l f s = runIdentity (l (Identity . f) s) @@ -600,7 +602,7 @@ substBindingsSimplifyingWith simplifier vLens p env = -- Circular program here. This should terminate as long as the -- bindings introduced by ANF don't form cycles. - let env' = HashMap.map (vLens %~ (simplifier . inlineInSortedReft (srLookup filteredEnv))) env + let env' = HashMap.map (vLens %~ simplifier . inlineInSortedReft (srLookup filteredEnv)) env filteredEnv = HashMap.filterWithKey (\sym _v -> p sym) env' in env' where diff --git a/src/Language/Fixpoint/Solver/Solve.hs b/src/Language/Fixpoint/Solver/Solve.hs --- a/src/Language/Fixpoint/Solver/Solve.hs +++ b/src/Language/Fixpoint/Solver/Solve.hs @@ -32,7 +32,7 @@ import Language.Fixpoint.Graph import Text.PrettyPrint.HughesPJ import Text.Printf -import System.Console.CmdArgs.Verbosity -- (whenNormal, whenLoud) +import Language.Fixpoint.Verbosity import Control.DeepSeq import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S diff --git a/src/Language/Fixpoint/Types/Config.hs b/src/Language/Fixpoint/Types/Config.hs --- a/src/Language/Fixpoint/Types/Config.hs +++ b/src/Language/Fixpoint/Types/Config.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE UndecidableInstances #-} @@ -41,8 +40,10 @@ import Data.Serialize (Serialize (..)) import Control.DeepSeq import GHC.Generics -import System.Console.CmdArgs -import System.Console.CmdArgs.Explicit +import System.Console.GetOpt +import Language.Fixpoint.Verbosity (Verbosity (..), setVerbosity, whenNormal) +import System.Environment (getArgs) +import System.Exit (exitFailure, exitSuccess) import qualified Language.Fixpoint.Conditional.Z3 as Conditional.Z3 import Language.Fixpoint.Utils.Files @@ -51,16 +52,6 @@ import Paths_liquid_fixpoint (version) -------------------------------------------------------------------------------- -withPragmas :: Config -> [String] -> IO Config --------------------------------------------------------------------------------- -withPragmas c s = - processValueIO - config { modeValue = (modeValue config) { cmdArgsValue = c } } - s - >>= - cmdArgsApply - --------------------------------------------------------------------------------- -- | Configuration Options ----------------------------------------------------- -------------------------------------------------------------------------------- @@ -104,7 +95,7 @@ , etabeta :: Bool -- ^ Eta expand and beta reduce terms to aid PLE , localRewrites :: Bool -- ^ Eta expand and beta reduce terms to aid PLE , saveBfqOnError :: Bool -- ^ save FInfo as .bfq only on verification failure - , interpreter :: Bool -- ^ Do not use the interpreter to assist PLE + , interpreter :: Bool -- ^ Use the interpreter to assist PLE , noEnvReduction :: Bool -- ^ Don't use environment reduction , inlineANFBinds :: Bool -- ^ Inline ANF bindings. -- Sometimes improves performance and sometimes worsens it. @@ -119,18 +110,12 @@ , explicitKvars :: Bool -- ^ use explicitly declared kvars (horn style) which disables several "defensive simplifications" , sortedSolution :: Bool -- ^ leave sorts in the solution , saveDir :: Maybe FilePath -- ^ output directory for --save generated files (default: .liquid/ next to source) - } deriving (Eq,Data,Typeable,Show,Generic) - -instance Default Config where - def = defConfig + } deriving (Eq,Show,Generic) --------------------------------------------------------------------------------------- data RESTOrdering = RESTKBO | RESTLPO | RESTRPO | RESTFuel Int - deriving (Eq, Data, Typeable, Generic) - -instance Default RESTOrdering where - def = RESTRPO + deriving (Eq, Generic) instance Show RESTOrdering where show RESTKBO = "kbo" @@ -150,7 +135,7 @@ --------------------------------------------------------------------------------------- data SMTSolver = Z3 | Z3mem | Cvc4 | Cvc5 | Mathsat - deriving (Eq, Data, Typeable, Generic) + deriving (Eq, Generic) data ElabFlags = ElabFlags { elabSetBag :: Bool, elabExplicitKvars :: Bool } @@ -164,9 +149,6 @@ solverFlags :: Config -> ElabFlags solverFlags cfg = mkElabFlags (solver cfg) (explicitKvars cfg) -instance Default SMTSolver where - def = if Conditional.Z3.builtWithZ3AsALibrary then Z3mem else Z3 - instance Show SMTSolver where show Z3 = "z3" show Z3mem = "z3 API" @@ -183,15 +165,12 @@ -- Both = scrape all concrete predicates (i.e. "rhs" + "lhs") data Scrape = No | Head | Both - deriving (Eq, Data, Typeable, Generic) + deriving (Eq, Generic) instance Serialize Scrape instance S.Store Scrape instance NFData Scrape -instance Default Scrape where - def = No - instance Show Scrape where show No = "no" show Head = "head" @@ -211,16 +190,13 @@ | All | Horn | Existentials - deriving (Eq, Data, Typeable, Generic) + deriving (Eq, Generic) instance Serialize Eliminate instance S.Store Eliminate instance NFData SMTSolver instance NFData Eliminate -instance Default Eliminate where - def = None - instance Show Eliminate where show None = "none" show Some = "some" @@ -235,95 +211,310 @@ --------------------------------------------------------------------------------------- defConfig :: Config -defConfig = Config { - srcFile = "out" &= args &= typFile - , defunction = False &= help "Allow higher order binders into fixpoint environment" - , solver = def &= help "Name of SMT Solver" - , linear = False &= help "Use uninterpreted integer multiplication and division" - , noStringTheory = False &= help "Disable use of string theory by SMT" - , allowHO = False &= help "Allow higher order binders into fixpoint environment" - , allowHOqs = False &= help "Allow higher order qualifiers" - , eliminate = None &= help "Eliminate KVars [none = quals for all-kvars, cuts = quals for cut-kvars, all = eliminate all-kvars (TRUE for cuts)]" - , scrape = def &= help "Scrape qualifiers from constraint (Horn format only) [ no = do not, head = scrape from heads, both = scrape from everywhere ]" - , elimBound = Nothing &= name "elimBound" &= help "(alpha) Maximum eliminate-chain depth" - , smtTimeout = Nothing &= name "smtTimeout" &= help "SMT timeout in msec" - , elimStats = False &= help "(alpha) Print eliminate stats" - , solverStats = False &= help "Print solver stats" - , save = False &= help "Save Query as .fq and .bfq files" - , saveBfqOnError = False &= help "Save Query as .bfq file only when verification fails" - &= name "save-bfq-on-error" - &= explicit - , saveDir = Nothing - &= name "save-dir" - &= help "Output directory for --save generated files (default: .liquid/ next to source)" - &= opt (Nothing :: Maybe FilePath) - &= explicit - &= typDir - , metadata = False &= help "Print meta-data associated with constraints" - , stats = False &= help "Compute constraint statistics" - , etaElim = False &= help "Eta elimination in function definition" - , parts = False &= help "Partition constraints into indepdendent .fq files" - , cores = def &= help "(numeric) Number of threads to use" - , minPartSize = defaultMinPartSize &= help "(numeric) Minimum partition size when solving in parallel" - , maxPartSize = defaultMaxPartSize &= help "(numeric) Maximum partiton size when solving in parallel." - , minimize = False &= help "Delta debug to minimize fq file (unsat with min constraints)" - , minimizeQs = False &= help "Delta debug to minimize fq file (sat with min qualifiers)" - , minimizeKs = False &= help "Delta debug to minimize fq file (sat with max kvars replaced by True)" - , minimalSol = False &= help "Shrink fixpoint by removing implied qualifiers" - , autoKuts = False &= help "Ignore given Kut vars, compute from scratch" - , nonLinCuts = False &= help "Treat non-linear kvars as cuts" - , noslice = False &= help "Disable non-concrete KVar slicing" - , rewriteAxioms = False &= name "ple" &= help "Allow axiom instantiation via rewriting (PLE)" - , pleUndecGuards = - False - &= name "ple-with-undecided-guards" - &= help "Unfold invocations with undecided guards in PLE" - &= explicit - , interpreter = - False - &= name "interpreter" - &= help "Use the interpreter to assist PLE" - , etabeta = False &= help "Use eta expansion and beta reduction to aid PLE" - , localRewrites = False &= help "Perform local rewrites inside PLE" - , noEnvReduction = False &= help "Don't perform environment reduction" - , inlineANFBinds = False &= help (unwords - [ "Inline ANF bindings." - , "Sometimes improves performance and sometimes worsens it." - , "Disabled by --noenvreduction" - ]) - , checkCstr = [] &= help "Only check these specific constraint-ids" - , extensionality = False &= help "Allow extensional interpretation of extensionality" - , rwTermination = False &= help "Enable rewrite divergence checker" - , stdin = False &= help "Read input query from stdin" - , json = False &= help "Render result in JSON" - , fuel = Nothing &= help "Maximum fuel (per-function unfoldings) for PLE" - , restOrdering = "rpo" &= help "Ordering Constraint Algebra to use for REST" - , explicitKvars = False &= help "Use explicitly declared kvars (horn style) which disables several defensive simplifications" - , sortedSolution = False &= help "Leave elaborated sorts in the solution (only for machine consumption)" +defConfig = Config + { srcFile = "out" + , defunction = False + , solver = if Conditional.Z3.builtWithZ3AsALibrary then Z3mem else Z3 + , linear = False + , noStringTheory = False + , allowHO = False + , allowHOqs = False + , eliminate = None + , scrape = No + , elimBound = Nothing + , smtTimeout = Nothing + , elimStats = False + , solverStats = False + , save = False + , saveBfqOnError = False + , saveDir = Nothing + , metadata = False + , stats = False + , etaElim = False + , parts = False + , cores = Nothing + , minPartSize = defaultMinPartSize + , maxPartSize = defaultMaxPartSize + , minimize = False + , minimizeQs = False + , minimizeKs = False + , minimalSol = False + , autoKuts = False + , nonLinCuts = False + , noslice = False + , rewriteAxioms = False + , pleUndecGuards = False + , interpreter = False + , etabeta = False + , localRewrites = False + , noEnvReduction = False + , inlineANFBinds = False + , checkCstr = [] + , extensionality = False + , rwTermination = False + , stdin = False + , json = False + , fuel = Nothing + , restOrdering = "rpo" + , explicitKvars = False + , sortedSolution = False } - &= verbosity - &= program "fixpoint" - &= help "Predicate Abstraction Based Horn-Clause Solver" - &= summary summaryInfo - &= details [ "Predicate Abstraction Based Horn-Clause Solver" - , "" - , "To check a file foo.fq type:" - , " fixpoint foo.fq" - ] +-- | An individual parsed flag (modifier to Config, verbosity change, or exit). +data FxFlag + = FxMod (Config -> Config) + | FxVerbosity Verbosity + | FxHelp + | FxVersion + | FxNumericVersion + +-- | All command-line options for fixpoint. +fxOptions :: [OptDescr FxFlag] +fxOptions = + [ Option [] ["defunction", "defunct"] (NoArg (FxMod $ \c -> c { defunction = True })) + "Allow higher order binders into fixpoint environment" + , opt0 "linear" (\c -> c { linear = True }) + "Use uninterpreted integer multiplication and division" + , opt0 "no-string-theory" (\c -> c { noStringTheory = True }) + "Disable use of string theory by SMT" + , opt0 "allowho" (\c -> c { allowHO = True }) + "Allow higher order binders into fixpoint environment" + , opt0 "allowhoqs" (\c -> c { allowHOqs = True }) + "Allow higher order qualifiers" + , Option [] ["eliminate"] (ReqArg setEliminate "ELIM") + ( unlines + [ "Eliminate KVars [" ++ L.intercalate " | " + ["none", "some", "all", "horn", "existentials"] ++ "]" + , " none: quals for all-kvars" + , " some: ??" + , " all: eliminate all-kvars (TRUE for cuts)" + , " horn: ??" + , " existentials: ??" + ] + ) + , Option [] ["scrape"] (ReqArg setScrape "SCRAPE") + (unlines + [ "Scrape qualifiers from constraint [" ++ L.intercalate " | " + ["no", "head", "both"] ++ "]" + , " no: do not" + , " head: scrape from heads" + , " both: scrape from everywhere" + ] + ) + , Option [] ["solver"] (ReqArg setSolver "SOLVER") + ("SMT solver [" ++ L.intercalate " | " ["z3", "z3mem", "cvc4", "cvc5", "mathsat"] ++ "]") + , Option [] ["elimBound"] (ReqArg (\s -> FxMod $ \c -> c { elimBound = parseInt "elimBound" s }) "N") + "(alpha) Maximum eliminate-chain depth" + , Option [] ["smtTimeout"] (ReqArg (\s -> FxMod $ \c -> c { smtTimeout = parseInt "smtTimeout" s }) "N") + "SMT timeout in msec" + , opt0 "elim-stats" (\c -> c { elimStats = True }) + "(alpha) Print eliminate stats" + , opt0 "solver-stats" (\c -> c { solverStats = True }) + "Print solver stats" + , opt0 "save" (\c -> c { save = True }) + "Save Query as .fq and .bfq files" + , Option [] ["save-bfq-on-error"] (NoArg (FxMod $ \c -> c { saveBfqOnError = True })) + "Save Query as .bfq file only when verification fails" + , Option [] ["save-dir"] (ReqArg setSaveDir "DIR") + "Output directory for --save generated files (default: .liquid/ next to source)" + , opt0 "metadata" (\c -> c { metadata = True }) + "Print meta-data associated with constraints" + , opt0 "stats" (\c -> c { stats = True }) + "Compute constraint statistics" + , Option [] ["eta-elim", "etaelim"] (NoArg (FxMod $ \c -> c { etaElim = True })) + "Eta elimination in function definition" + , opt0 "parts" (\c -> c { parts = True }) + "Partition constraints into independent .fq files" + , Option [] ["cores"] (ReqArg (\s -> FxMod $ \c -> c { cores = parseInt "cores" s }) "N") + "(numeric) Number of threads to use" + , Option [] ["min-part-size"] (ReqArg (\s -> FxMod $ \c -> c { minPartSize = read s }) "N") + "(numeric) Minimum partition size when solving in parallel" + , Option [] ["max-part-size"] (ReqArg (\s -> FxMod $ \c -> c { maxPartSize = read s }) "N") + "(numeric) Maximum partition size when solving in parallel" + , opt0 "minimize" (\c -> c { minimize = True }) + "Delta debug to minimize fq file (unsat with min constraints)" + , opt0 "minimize-qs" (\c -> c { minimizeQs = True }) + "Delta debug to minimize fq file (sat with min qualifiers)" + , opt0 "minimize-ks" (\c -> c { minimizeKs = True }) + "Delta debug to minimize fq file (sat with max kvars replaced by True)" + , opt0 "minimal-sol" (\c -> c { minimalSol = True }) + "Shrink fixpoint by removing implied qualifiers" + , opt0 "auto-kuts" (\c -> c { autoKuts = True }) + "Ignore given Kut vars, compute from scratch" + , opt0 "non-lin-cuts" (\c -> c { nonLinCuts = True }) + "Treat non-linear kvars as cuts" + , opt0 "noslice" (\c -> c { noslice = True }) + "Disable non-concrete KVar slicing" + , Option [] ["ple", "rewrite", "rewrite-axioms"] (NoArg (FxMod $ \c -> c { rewriteAxioms = True })) + "Allow axiom instantiation via rewriting (PLE)" + , Option [] ["ple-with-undecided-guards"] (NoArg (FxMod $ \c -> c { pleUndecGuards = True })) + "Unfold invocations with undecided guards in PLE" + -- Accept optional =true/=false for backward compatibility with cmdargs Bool encoding + , Option [] ["interpreter"] (OptArg (parseBoolOpt interpreter (\b c -> c { interpreter = b })) "BOOL") + "Use the interpreter to assist PLE" + , opt0 "etabeta" (\c -> c { etabeta = True }) + "Use eta expansion and beta reduction to aid PLE" + , Option [] ["local-rewrites", "localrewrites"] (NoArg (FxMod $ \c -> c { localRewrites = True })) + "Perform local rewrites inside PLE" + , opt0 "no-env-reduction" (\c -> c { noEnvReduction = True }) + "Don't perform environment reduction" + , opt0 "inline-anf-binds" (\c -> c { inlineANFBinds = True }) + "Inline ANF bindings (sometimes improves performance, sometimes worsens it)" + , Option [] ["check-cstr"] (ReqArg (\s -> FxMod $ \c -> c { checkCstr = checkCstr c ++ [read s] }) "ID") + "Only check these specific constraint-ids (repeat for multiple)" + , opt0 "extensionality" (\c -> c { extensionality = True }) + "Allow extensional interpretation of function equality" + , opt0 "rw-termination" (\c -> c { rwTermination = True }) + "Enable rewrite divergence checker" + , opt0 "stdin" (\c -> c { stdin = True }) + "Read input query from stdin" + , opt0 "json" (\c -> c { json = True }) + "Render result in JSON" + , Option [] ["fuel"] (ReqArg (\s -> FxMod $ \c -> c { fuel = parseInt "fuel" s }) "N") + "Maximum fuel (per-function unfoldings) for PLE" + , Option [] ["rest-ordering"] (ReqArg (\s -> FxMod $ \c -> c { restOrdering = s }) "ORD") + "Ordering constraint algebra to use for REST" + , opt0 "explicit-kvars" (\c -> c { explicitKvars = True }) + "Use explicitly declared kvars (horn style) which disables several defensive simplifications" + , opt0 "sorted-solution" (\c -> c { sortedSolution = True }) + "Leave elaborated sorts in the solution (only for machine consumption)" + , Option "v" ["verbose"] (NoArg (FxVerbosity Loud)) + "Be more verbose" + , Option "q" ["quiet"] (NoArg (FxVerbosity Quiet)) + "Be quiet (suppress normal output)" + , Option "h?" ["help"] (NoArg FxHelp) + "Show this help message" + , Option "V" ["version"] (NoArg FxVersion) + "Show version" + , Option [] ["numeric-version"] (NoArg FxNumericVersion) + "Print numeric version and exit" + ] + where + opt0 name f desc = + Option [] [name] (NoArg (FxMod f)) desc + + -- Parse an optional =true/=false/=True/=False argument (cmdargs Bool compat) + parseBoolOpt :: (Config -> Bool) -> (Bool -> Config -> Config) -> Maybe String -> FxFlag + parseBoolOpt _ setter Nothing = FxMod (setter True) + parseBoolOpt _ setter (Just "true") = FxMod (setter True) + parseBoolOpt _ setter (Just "True") = FxMod (setter True) + parseBoolOpt _ setter (Just "false") = FxMod (setter False) + parseBoolOpt _ setter (Just "False") = FxMod (setter False) + parseBoolOpt getDef _setter (Just s) = + error $ "Expected true/false, got: " ++ s ++ " (current default: " ++ show (getDef defConfig) ++ ")" + + setSolver s = FxMod $ \c -> c { solver = parseSolver s } + setEliminate s = FxMod $ \c -> c { eliminate = parseEliminate s } + setScrape s = FxMod $ \c -> c { scrape = parseScrape s } + setSaveDir s = FxMod $ \c -> c { saveDir = Just s } + + parseSolver "z3" = Z3 + parseSolver "z3mem" = Z3mem + parseSolver "cvc4" = Cvc4 + parseSolver "cvc5" = Cvc5 + parseSolver "mathsat" = Mathsat + parseSolver s = error $ "Unknown solver: " ++ s + + parseEliminate "none" = None + parseEliminate "some" = Some + parseEliminate "all" = All + parseEliminate "horn" = Horn + parseEliminate "existentials" = Existentials + parseEliminate s = error $ "Unknown eliminate mode: " ++ s + + parseScrape "no" = No + parseScrape "head" = Head + parseScrape "both" = Both + parseScrape s = error $ "Unknown scrape mode: " ++ s + + parseInt _ s = Just (read s) + +-- | Apply a list of parsed flags to a base Config; return updated config and +-- verbosity change (if any). +applyFxFlags :: Config -> [FxFlag] -> IO Config +applyFxFlags base flags = do + mapM_ applyVerbosity flags + return $! L.foldl' applyMod base flags + where + applyMod c (FxMod f) = f c + applyMod c _ = c + applyVerbosity (FxVerbosity vb) = setVerbosity vb + applyVerbosity _ = return () + +-------------------------------------------------------------------------------- +withPragmas :: Config -> [String] -> IO Config +-------------------------------------------------------------------------------- +withPragmas base tokens = + case getOpt Permute fxOptions tokens of + (flags, _, []) -> do + -- We make fixpoint fail when given --version of --help pragmas to make + -- it harder to miss that a file is not being checked. + handleExits flags exitFailure (formatHelp fxOptions) summaryInfo + applyFxFlags base flags + (_, _, optErrs) -> ioError $ userError $ + concat optErrs ++ "\nUse --help for usage information." + +-------------------------------------------------------------------------------- + summaryInfo :: String -summaryInfo = "fixpoint " ++ showVersion version ++ " " ++ "(" ++ $(gitHash) ++ ")" -config :: Mode (CmdArgs Config) -config = cmdArgsMode defConfig +summaryInfo = "fixpoint " ++ showVersion version ++ " " ++ "(" ++ $(gitHash) ++ ")" getOpts :: IO Config getOpts = do - md <- cmdArgs defConfig - whenNormal (putStrLn banner) - return md + args <- getArgs + case getOpt Permute fxOptions args of + (flags, files, []) -> do + cfg <- applyFxFlags defConfig flags + let srcF = case files of { (f:_) -> f; [] -> srcFile defConfig } + cfg' = cfg { srcFile = srcF } + whenBanner flags $ whenNormal (putStrLn banner) + handleExits flags exitSuccess (formatHelp fxOptions) summaryInfo + return cfg' + (_, _, optErrs) -> ioError $ userError $ + concat optErrs ++ "\nUse --help for usage information." +whenBanner :: [FxFlag] -> IO () -> IO () +whenBanner (FxNumericVersion:_) _ = return () +whenBanner (_:flags) act = whenBanner flags act +whenBanner [] act = act + +handleExits :: [FxFlag] -> IO () -> String -> String -> IO () +handleExits flags termination helpText ver = mapM_ go flags + where + go FxHelp = putStr helpText >> termination + go FxVersion = putStrLn ver >> termination + go FxNumericVersion = putStrLn (showVersion version) >> termination + go _ = return () + +formatHelp :: [OptDescr a] -> String +formatHelp opts = + unlines $ + [ "Usage: fixpoint [OPTIONS] FILE.fq" + , "" + , " Predicate Abstraction Based Horn-Clause Solver" + , "" + , "Options:" + , "" + ] + ++ L.intersperse "" (map fmtOpt opts) + where + fmtOpt :: OptDescr a -> String + fmtOpt (Option short long argDesc desc) = + let shortStr = case short of + [] -> "" + (c:_) -> "-" ++ [c] + longStrs = map ("--" ++) long + argStr = case argDesc of + NoArg _ -> "" + ReqArg _ m -> " " ++ m + OptArg _ m -> "[=" ++ m ++ "]" + indentedDesc = unlines $ map (" " ++) $ lines desc + synopsis = L.intercalate ", " $ + [shortStr | not (null shortStr)] ++ longStrs + in " " ++ synopsis ++ argStr ++ "\n\n" ++ indentedDesc + banner :: String -banner = "\n\nLiquid-Fixpoint Copyright 2009-25 Regents of the University of California.\n" +banner = "\nLiquid-Fixpoint Copyright 2009-25 Regents of the University of California.\n" ++ "All Rights Reserved.\n" restOC :: Config -> RESTOrdering diff --git a/src/Language/Fixpoint/Verbosity.hs b/src/Language/Fixpoint/Verbosity.hs new file mode 100644 --- /dev/null +++ b/src/Language/Fixpoint/Verbosity.hs @@ -0,0 +1,45 @@ +-- | Global verbosity IORef, replacing the one provided by @cmdargs@. +-- Use 'setVerbosity' after option parsing to control all 'whenLoud' / +-- 'whenNormal' guards throughout the solver. +module Language.Fixpoint.Verbosity + ( Verbosity (..) + , setVerbosity + , getVerbosity + , whenLoud + , whenNormal + , isNormal + , isLoud + ) where + +import Control.Monad (when) +import Data.IORef (IORef, newIORef, readIORef, writeIORef) +import System.IO.Unsafe (unsafePerformIO) + +data Verbosity = Quiet | Normal | Loud + deriving (Eq, Ord, Show) + +{-# NOINLINE verbosityRef #-} +verbosityRef :: IORef Verbosity +verbosityRef = unsafePerformIO (newIORef Normal) + +setVerbosity :: Verbosity -> IO () +setVerbosity = writeIORef verbosityRef + +getVerbosity :: IO Verbosity +getVerbosity = readIORef verbosityRef + +whenLoud :: IO () -> IO () +whenLoud act = do + v <- getVerbosity + when (v >= Loud) act + +whenNormal :: IO () -> IO () +whenNormal act = do + v <- getVerbosity + when (v >= Normal) act + +isNormal :: IO Bool +isNormal = (>= Normal) <$> getVerbosity + +isLoud :: IO Bool +isLoud = (>= Loud) <$> getVerbosity diff --git a/tests/neg/numeric-version.fq b/tests/neg/numeric-version.fq new file mode 100644 --- /dev/null +++ b/tests/neg/numeric-version.fq @@ -0,0 +1,1 @@ +fixpoint "--numeric-version" diff --git a/tests/test.hs b/tests/test.hs --- a/tests/test.hs +++ b/tests/test.hs @@ -10,7 +10,7 @@ import Control.Monad (when) import qualified Control.Monad.State as State import Control.Monad.Trans.Class (lift) -import Data.List (isSuffixOf) +import Data.List (dropWhileEnd, isSuffixOf) import Prelude hiding (log) import Data.Maybe (fromMaybe) import Data.Monoid (Sum(..)) @@ -112,6 +112,14 @@ , dirHornTests "horn-smt2-pos-el" elimCmd "tests/logs/cur/horn-pos-el" [] [] ExitSuccess , dirHornTests "horn-smt2-neg-el" elimCmd "tests/logs/cur/horn-neg-el" [] [] (ExitFailure 1) ] + , return $ testGroup "flags" + [ testCase "--numeric-version" $ do + (code, out, _) <- readProcessWithExitCode "fixpoint" ["--numeric-version"] "" + assertEqual "Wrong exit code" ExitSuccess code + let ver = dropWhileEnd (== '\n') out + assertBool ("Expected a version number like X.Y.Z, got: " ++ show ver) + (not (null ver) && all isNumericSegment (splitOn '.' ver)) + ] ] where posOptions = ["--save-bfq-on-error"] @@ -210,6 +218,19 @@ group :: Monad f => TestName -> [f TestTree] -> f TestTree group n xs = testGroup n <$> sequence xs + +-- | Split a string on a delimiter character. +splitOn :: Char -> String -> [String] +splitOn _ [] = [""] +splitOn d (c:cs) + | c == d = "" : splitOn d cs + | otherwise = case splitOn d cs of + (w:ws) -> (c:w) : ws + [] -> [c:""] + +-- | A numeric version segment is a non-empty string of digits. +isNumericSegment :: String -> Bool +isNumericSegment s = not (null s) && all (\c -> c >= '0' && c <= '9') s ---------------------------------------------------------------------------------------- walkDirectory :: FilePath -> IO [FilePath] diff --git a/unix/Language/Fixpoint/Utils/Progress.hs b/unix/Language/Fixpoint/Utils/Progress.hs --- a/unix/Language/Fixpoint/Utils/Progress.hs +++ b/unix/Language/Fixpoint/Utils/Progress.hs @@ -10,7 +10,7 @@ import Control.Monad (when) import System.IO.Unsafe (unsafePerformIO) -import System.Console.CmdArgs.Verbosity (isNormal, getVerbosity, Verbosity(..)) +import Language.Fixpoint.Verbosity (isNormal, getVerbosity, Verbosity(..)) import Data.IORef import System.Console.AsciiProgress -- import Language.Fixpoint.Misc (traceShow)