diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 0fee9866..a80ee1fe 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -45,11 +45,6 @@ jobs: - name: Cabal update shell: bash run: nix-shell -p cabal-install --run 'cabal update' - - name: Cabal check - shell: bash - run: | - cd what4 - nix-shell -p cabal-install --run 'cabal check' - name: Setup Environment Vars run: | GHC=haskell.compiler.ghc$(echo ${{ matrix.ghc }} | sed -e s,\\.,,g) @@ -90,7 +85,7 @@ jobs: # LD_LIBRARY_PATH manipulation may be removed for all steps. run: | cd what4 - $NS 'LD_LIBRARY_PATH="$ZLIB_LOC:$LD_LIBRARY_PATH" cabal configure -fSTPTestDisable -fdRealTestDisable -fsolverTests --extra-lib-dirs="$ZLIB_LOC"' + $NS 'LD_LIBRARY_PATH="$ZLIB_LOC:$LD_LIBRARY_PATH" cabal configure --enable-tests -fSTPTestDisable -fdRealTestDisable -fsolverTests --extra-lib-dirs="$ZLIB_LOC"' - name: Build shell: bash run: | diff --git a/what4/src/What4/Config.hs b/what4/src/What4/Config.hs index 8e593d88..f2ff105a 100644 --- a/what4/src/What4/Config.hs +++ b/what4/src/What4/Config.hs @@ -87,6 +87,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module What4.Config ( -- * Names of properties @@ -100,6 +101,9 @@ module What4.Config -- * Option settings , OptionSetting(..) , Opt(..) + , setUnicodeOpt + , setIntegerOpt + , setBoolOpt -- * Defining option styles , OptionStyle(..) @@ -112,6 +116,9 @@ module What4.Config , optWarn , optErr , checkOptSetResult + , OptSetFailure(..) + , OptGetFailure(..) + , OptCreateFailure(..) -- ** Option style templates , Bound(..) @@ -136,6 +143,8 @@ module What4.Config , optV , optU , optUV + , copyOpt + , deprecatedOpt -- * Building and manipulating configurations , Config @@ -157,29 +166,26 @@ module What4.Config , verbosityLogger ) where -#if !MIN_VERSION_base(4,13,0) -import Control.Monad.Fail( MonadFail ) -#endif - -import Control.Applicative (Const(..)) +import Control.Applicative ( Const(..), (<|>) ) import Control.Concurrent.MVar -import Control.Exception import Control.Lens ((&)) -import Control.Monad.Identity +import qualified Control.Lens.Combinators as LC +import Control.Monad.Catch import Control.Monad.IO.Class +import Control.Monad.Identity import Control.Monad.Writer.Strict hiding ((<>)) -import Data.Kind -import Data.Maybe -import Data.Typeable import Data.Foldable (toList) +import Data.Kind import Data.List.NonEmpty (NonEmpty(..)) +import Data.Map (Map) +import qualified Data.Map.Strict as Map +import Data.Maybe +import Data.Parameterized.Classes import Data.Parameterized.Some import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.Set (Set) import qualified Data.Set as Set -import Data.Map (Map) -import qualified Data.Map.Strict as Map import Data.Text (Text) import qualified Data.Text as Text import Data.Void @@ -305,6 +311,12 @@ data OptionSetting (tp :: BaseType) = } +instance Show (OptionSetting tp) where + show = (<> " option setting") . + LC.cons '\'' . flip LC.snoc '\'' . + show . optionSettingName +instance ShowF OptionSetting + -- | An option defines some metadata about how a configuration option behaves. -- It contains a base type representation, which defines the runtime type -- that is expected for setting and querying this option at runtime. @@ -427,7 +439,7 @@ realWithRangeOptSty lo hi = realOptSty & set_opt_onset vf vf _ (ConcreteReal x) | checkBound lo hi x = return optOK | otherwise = return $ optErr $ - prettyRational x <+> "out of range, expected real value in " + prettyRational x <+> "out of range, expected real value in" <+> docInterval lo hi -- | Option style for real-valued options with a lower bound @@ -447,7 +459,7 @@ integerWithRangeOptSty lo hi = integerOptSty & set_opt_onset vf vf _ (ConcreteInteger x) | checkBound lo hi x = return optOK | otherwise = return $ optErr $ - pretty x <+> "out of range, expected integer value in " + pretty x <+> "out of range, expected integer value in" <+> docInterval lo hi -- | Option style for integer-valued options with a lower bound @@ -469,9 +481,9 @@ enumOptSty elts = stringOptSty & set_opt_onset vf vf _ (ConcreteString (UnicodeLiteral x)) | x `Set.member` elts = return optOK | otherwise = return $ optErr $ - "invalid setting" <+> dquotes (pretty x) <+> - ", expected one of:" <+> - align (sep (map pretty $ Set.toList elts)) + "invalid setting" <+> dquotes (pretty x) <> + ", expected one of these enums:" <+> + align (sep (punctuate comma (map pretty $ Set.toList elts))) -- | A configuration syle for options that must be one of a fixed set of text values. -- Associated with each string is a validation/callback action that will be run @@ -488,12 +500,73 @@ listOptSty values = stringOptSty & set_opt_onset vf vf _ (ConcreteString (UnicodeLiteral x)) = fromMaybe (return $ optErr $ - "invalid setting" <+> dquotes (pretty x) <+> - ", expected one of:" <+> + "invalid setting" <+> dquotes (pretty x) <> + ", expected one from this list:" <+> align (sep (map (pretty . fst) $ Map.toList values))) (Map.lookup x values) +-- | Used as a wrapper for an option that has been deprecated. If the +-- option is actually set (as opposed to just using the default value) +-- then this will emit an OptionSetResult warning that time, optionally +-- mentioning the replacement option (if specified). +-- +-- There are three cases of deprecation: +-- 1. Removing an option that no longer applies +-- 2. Changing the name or heirarchical position of an option. +-- 3. #2 and also changing the type. +-- 4. Replacing an option by multiple new options (e.g. split url option +-- into hostname and port options) +-- +-- In the case of #1, the option will presumably be ignored by the +-- code and the warnings are provided to allow the user to clean the +-- option from their configurations. +-- +-- In the case of #2, the old option and the new option will share the +-- same value storage: changes to one can be seen via the other and +-- vice versa. The code can be switched over to reference the new +-- option entirely, and user configurations setting the old option +-- will still work until they have been updated and the definition of +-- the old option is removed entirely. +-- +-- NOTE: in order to support #2, the newer option should be declared +-- (via 'insertOption') *before* the option it deprecates. +-- +-- In the case of #3, it is not possible to share storage space, so +-- during the deprecation period, the code using the option config +-- value must check both locations and decide which value to utilize. +-- +-- Case #4 is an enhanced form of #3 and #2, and is generally treated +-- as #3, but adds the consideration that deprecation warnings will +-- need to advise about multiple new options. The inverse of #4 +-- (multiple options being combined to a single newer option) is just +-- treated as separate deprecations. +-- +-- NOTE: in order to support #4, the newer options should all be +-- declared (via 'insertOption') *before* the options they deprecate. +-- +-- Nested deprecations are valid, and replacement warnings are +-- automatically transitive to the newest options. +-- +-- Any user-supplied value for the old option will result in warnings +-- emitted to the OptionSetResult for all four cases. Code should +-- ensure that these warnings are appropriately communicated to the +-- user to allow configuration updates to occur. +-- +-- Note that for #1 and #2, the overhead burden of continuing to +-- define the deprecated option is very small, so actual removal of +-- the older config can be delayed indefinitely. + +deprecatedOpt :: [ConfigDesc] -> ConfigDesc -> ConfigDesc +deprecatedOpt newerOpt (ConfigDesc o sty desc oldRepl) = + let -- note: description and setter not modified here in case this + -- is called again to declare additional replacements (viz. case + -- #2 above). These will be modified in the 'insertOption' function. + newRepl :: Maybe [ConfigDesc] + newRepl = (newerOpt <>) <$> (oldRepl <|> Just []) + in ConfigDesc o sty desc newRepl + + -- | A configuration style for options that are expected to be paths to an executable -- image. Configuration options with this style generate a warning message if set to a -- value that cannot be resolved to an absolute path to an executable file in the @@ -517,7 +590,14 @@ executablePathOptSty = stringOptSty & set_opt_onset vf -- an @OptionStyle@ describing the sort of option it is, and an optional -- help message describing the semantics of this option. data ConfigDesc where - ConfigDesc :: ConfigOption tp -> OptionStyle tp -> Maybe (Doc Void) -> ConfigDesc + ConfigDesc :: ConfigOption tp -- describes option name and type + -> OptionStyle tp -- option validators, help info, type and default + -> Maybe (Doc Void) -- help text + -> Maybe [ConfigDesc] -- Deprecation and newer replacements + -> ConfigDesc + +instance Show ConfigDesc where + show (ConfigDesc o _ _ _) = show o -- | The most general method for constructing a normal `ConfigDesc`. mkOpt :: ConfigOption tp -- ^ Fixes the name and the type of this option @@ -525,7 +605,7 @@ mkOpt :: ConfigOption tp -- ^ Fixes the name and the type of this option -> Maybe (Doc Void) -- ^ Help text -> Maybe (ConcreteVal tp) -- ^ A default value for this option -> ConfigDesc -mkOpt o sty h def = ConfigDesc o sty{ opt_default_value = def } h +mkOpt o sty h def = ConfigDesc o sty{ opt_default_value = def } h Nothing -- | Construct an option using a default style with a given initial value opt :: Pretty help @@ -582,13 +662,28 @@ optUV o vf h = mkOpt o (defaultOpt (configOptionType o) Nothing -> return optOK Just z -> return $ optErr $ pretty z +-- | The copyOpt creates a duplicate ConfigDesc under a different +-- name. This is typically used to taking a common operation and +-- modify the prefix to apply it to a more specialized role +-- (e.g. solver.strict_parsing --> solver.z3.strict_parsing). The +-- style and help text of the input ConfigDesc are preserved, but any +-- deprecation is discarded. +copyOpt :: (Text -> Text) -> ConfigDesc -> ConfigDesc +copyOpt modName (ConfigDesc o@(ConfigOption ty _) sty h _) = + let newName = case splitPath (modName (configOptionText o)) of + Just ps -> ps + Nothing -> error "new config option must not be empty" + in ConfigDesc (ConfigOption ty newName) sty h Nothing + + + ------------------------------------------------------------------------ -- ConfigState data ConfigLeaf where ConfigLeaf :: !(OptionStyle tp) {- Style for this option -} -> - MVar (Maybe (ConcreteVal tp)) {- State of the option -} -> + MVar (Maybe (ConcreteVal tp)) {- State of the option -} -> Maybe (Doc Void) {- Help text for the option -} -> ConfigLeaf @@ -619,7 +714,8 @@ adjustConfigTrie [] f (Just (ConfigTrie x m)) = g <$> f x adjustConfigMap :: Functor t => Text -> [Text] -> (Maybe ConfigLeaf -> t (Maybe ConfigLeaf)) -> ConfigMap -> t ConfigMap adjustConfigMap a as f = Map.alterF (adjustConfigTrie as f) a --- | Traverse an entire @ConfigMap@. The first argument is +-- | Traverse an entire @ConfigMap@. The first argument is the +-- reversed heirarchical location of the starting map entry location. traverseConfigMap :: Applicative t => [Text] {- ^ A REVERSED LIST of the name segments that represent the context from the root to the current @ConfigMap@. -} -> @@ -650,19 +746,145 @@ traverseSubtree ps0 f = go ps0 [] where go [] revPath = traverseConfigMap revPath f go (p:ps) revPath = Map.alterF (traverse g) p - where g (ConfigTrie x m) = ConfigTrie x <$> go ps (p:revPath) m + where g (ConfigTrie x m) = ConfigTrie <$> here x <*> go ps (p:revPath) m + here = traverse (f (reverse (p:revPath))) --- | Add an option to the given @ConfigMap@. -insertOption :: (MonadIO m, MonadFail m) => ConfigDesc -> ConfigMap -> m ConfigMap -insertOption (ConfigDesc (ConfigOption _tp (p:|ps)) sty h) m = adjustConfigMap p ps f m +-- | Add an option to the given @ConfigMap@ or throws an +-- 'OptCreateFailure' exception on error. +-- +-- Inserting an option multiple times is idempotent under equivalency +-- modulo the opt_onset in the option's style, otherwise it is an +-- error. +insertOption :: (MonadIO m, MonadThrow m) + => ConfigMap -> ConfigDesc -> m ConfigMap +insertOption m d@(ConfigDesc o@(ConfigOption _tp (p:|ps)) sty h newRepls) = + adjustConfigMap p ps f m where - f Nothing = - do ref <- liftIO (newMVar (opt_default_value sty)) - return (Just (ConfigLeaf sty ref h)) - f (Just _) = fail ("Option " ++ showPath ++ " already exists") + f Nothing = + let addOnSetWarning warning oldSty = + let newSty = set_opt_onset depF oldSty + oldVF = opt_onset oldSty + depF oldV newV = + do v <- oldVF oldV newV + return (v <> optWarn warning) + in newSty + deprHelp depMsg ontoHelp = + let hMod oldHelp = vsep [ oldHelp, "*** DEPRECATED! ***", depMsg ] + in hMod <$> ontoHelp + newRefs tySep = hsep . punctuate comma . + map (\(n, ConfigLeaf s _ _) -> optRef tySep n s) + optRef tySep nm s = hcat [ pretty (show nm), tySep + , pretty (show (opt_type s)) + ] + in case newRepls of + -- not deprecated + Nothing -> + do ref <- liftIO (newMVar (opt_default_value sty)) + return (Just (ConfigLeaf sty ref h)) - showPath = Text.unpack (Text.intercalate "." (p:ps)) + -- deprecation case #1 (removal) + Just [] -> + do ref <- liftIO (newMVar (opt_default_value sty)) + let sty' = addOnSetWarning + ("DEPRECATED CONFIG OPTION WILL BE IGNORED: " <> + pretty (show o) <> + " (no longer valid)") + sty + hmsg = "Option '" <> pretty (show o) <> "' is no longer valid." + return (Just (ConfigLeaf sty' ref (deprHelp hmsg h))) + + Just n -> do + let newer = + let returnFnd fnd loc lf = + if name loc == fnd + then Const [Just (fnd, lf)] + else Const [Nothing] + name parts = Text.intercalate "." parts + lookupNewer (ConfigDesc (ConfigOption _ (t:|ts)) _sty _h new2) = + case new2 of + Nothing -> getConst $ traverseConfigMap [] (returnFnd (name (t:ts))) m + Just n2 -> concat (lookupNewer <$> n2) + in lookupNewer <$> n + chkMissing opts = + if not (null opts) && null (catMaybes opts) + then throwM $ OptCreateFailure d $ + "replacement options must be inserted into" <> + " Config before this deprecated option" + else return opts + newOpts <- catMaybes . concat <$> mapM chkMissing newer + + case newOpts of + + -- deprecation case #1 (removal) + [] -> + do ref <- liftIO (newMVar (opt_default_value sty)) + let sty' = addOnSetWarning + ("DEPRECATED CONFIG OPTION WILL BE IGNORED: " <> + pretty (show o) <> + " (no longer valid)") + sty + hmsg = "Option '" <> pretty (show o) <> "' is no longer valid." + return (Just (ConfigLeaf sty' ref (deprHelp hmsg h))) + + -- deprecation case #2 (renamed) + ((nm, ConfigLeaf sty' v _):[]) + | Just Refl <- testEquality (opt_type sty) (opt_type sty') -> + do let updSty = addOnSetWarning + ("DEPRECATED CONFIG OPTION USED: " <> + pretty (show o) <> + " (renamed to: " <> pretty nm <> ")") + hmsg = "Suggest replacing '" <> pretty (show o) <> + "' with '" <> pretty nm <> "'." + return (Just (ConfigLeaf (updSty sty) v (deprHelp hmsg h))) + + -- deprecation case #3 (renamed and re-typed) + (new1:[]) -> + do ref <- liftIO (newMVar (opt_default_value sty)) + let updSty = addOnSetWarning + ("DEPRECATED CONFIG OPTION USED: " <> + optRef "::" o sty <> + " (changed to: " <> + newRefs "::" [new1] <> + "); this value may be ignored") + hmsg = "Suggest converting '" <> + optRef " of type " o sty <> + " to " <> + newRefs " of type " [new1] + return (Just (ConfigLeaf (updSty sty) ref (deprHelp hmsg h))) + + -- deprecation case #4 (split to multiple options) + newMulti -> + do ref <- liftIO (newMVar (opt_default_value sty)) + let updSty = addOnSetWarning + ("DEPRECATED CONFIG OPTION USED: " <> + optRef "::" o sty <> + " (replaced by: " <> + newRefs "::" newMulti <> + "); this value may be ignored") + hmsg = "Suggest converting " <> + optRef " of type " o sty <> + " to: " <> (newRefs " of type " newMulti) + return (Just (ConfigLeaf (updSty sty) ref (deprHelp hmsg h))) + + f (Just existing@(ConfigLeaf sty' _ h')) = + case testEquality (opt_type sty) (opt_type sty') of + Just Refl -> + if and [ show (opt_help sty) == show (opt_help sty') + , opt_default_value sty == opt_default_value sty' + -- Note opt_onset in sty is ignored/dropped + , show h == show h' + ] + then return $ Just existing + else throwM $ OptCreateFailure d "already exists" + Nothing -> throwM $ OptCreateFailure d + (pretty $ "already exists with type " <> show (opt_type sty')) + +data OptCreateFailure = OptCreateFailure ConfigDesc (Doc Void) +instance Exception OptCreateFailure +instance Show OptCreateFailure where + show (OptCreateFailure cfgdesc msg) = + "Failed to create option " <> show cfgdesc <> ": " <> show msg ------------------------------------------------------------------------ @@ -682,13 +904,14 @@ initialConfig initVerbosity ts = do extendConfig (builtInOpts initVerbosity ++ ts) cfg return cfg --- | Extend an existing configuration with new options. An error will be --- raised if any of the given options clash with options that already exists. +-- | Extend an existing configuration with new options. An +-- 'OptCreateFailure' exception will be raised if any of the given +-- options clash with options that already exists. extendConfig :: [ConfigDesc] -> Config -> IO () extendConfig ts (Config cfg) = - modifyMVar_ cfg (\m -> foldM (flip insertOption) m ts) + modifyMVar_ cfg (\m -> foldM insertOption m ts) -- | Verbosity of the simulator. This option controls how much -- informational and debugging output is generated. @@ -726,24 +949,44 @@ class Opt (tp :: BaseType) (a :: Type) | tp -> a where trySetOpt :: OptionSetting tp -> a -> IO OptionSetResult -- | Set the value of an option. Return any generated warnings. - -- Throw an exception if a validation error occurs. + -- Throws an OptSetFailure exception if a validation error occurs. setOpt :: OptionSetting tp -> a -> IO [Doc Void] - setOpt x v = trySetOpt x v >>= checkOptSetResult + setOpt x v = trySetOpt x v >>= checkOptSetResult x -- | Get the current value of an option. Throw an exception -- if the option is not currently set. getOpt :: OptionSetting tp -> IO a - getOpt x = maybe (fail msg) return =<< getMaybeOpt x - where msg = "Option is not set: " ++ show (optionSettingName x) + getOpt x = maybe (throwM $ OptGetFailure (OSet $ Some x) "not set") return + =<< getMaybeOpt x -- | Throw an exception if the given @OptionSetResult@ indidcates -- an error. Otherwise, return any generated warnings. -checkOptSetResult :: OptionSetResult -> IO [Doc Void] -checkOptSetResult res = +checkOptSetResult :: OptionSetting tp -> OptionSetResult -> IO [Doc Void] +checkOptSetResult optset res = case optionSetError res of - Just msg -> fail (show msg) + Just msg -> throwM $ OptSetFailure (Some optset) msg Nothing -> return (toList (optionSetWarnings res)) +data OptSetFailure = OptSetFailure (Some OptionSetting) (Doc Void) +instance Exception OptSetFailure +instance Show OptSetFailure where + show (OptSetFailure optset msg) = + "Failed to set " <> show optset <> ": " <> show msg + +data OptRef = OName Text | OSet (Some OptionSetting) | OCfg (Some ConfigOption) +instance Show OptRef where + show = \case + OName t -> show t + OSet (Some s) -> show s + OCfg (Some c) -> show c + +data OptGetFailure = OptGetFailure OptRef (Doc Void) +instance Exception OptGetFailure +instance Show OptGetFailure where + show (OptGetFailure optref msg) = + "Failed to get " <> (show optref) <> ": " <> show msg + + instance Opt (BaseStringType Unicode) Text where getMaybeOpt x = fmap (fromUnicodeLit . fromConcreteString) <$> getOption x trySetOpt x v = setOption x (ConcreteString (UnicodeLiteral v)) @@ -756,6 +999,47 @@ instance Opt BaseBoolType Bool where getMaybeOpt x = fmap fromConcreteBool <$> getOption x trySetOpt x v = setOption x (ConcreteBool v) +instance Opt BaseRealType Rational where + getMaybeOpt x = fmap fromConcreteReal <$> getOption x + trySetOpt x v = setOption x (ConcreteReal v) + +-- | Given a unicode text value, set the named option to that value or +-- generate an OptSetFailure exception if the option is not a unicode +-- text valued option. +setUnicodeOpt :: Some OptionSetting -> Text -> IO [Doc Void] +setUnicodeOpt (Some optset) val = + let tyOpt = configOptionType (optionSettingName optset) + in case testEquality tyOpt (BaseStringRepr UnicodeRepr) of + Just Refl -> setOpt optset val + Nothing -> + checkOptSetResult optset $ optErr $ + "option type is a" <+> pretty tyOpt <+> "but given a text string" + +-- | Given an integer value, set the named option to that value or +-- generate an OptSetFailure exception if the option is not an integer +-- valued option. +setIntegerOpt :: Some OptionSetting -> Integer -> IO [Doc Void] +setIntegerOpt (Some optset) val = + let tyOpt = configOptionType (optionSettingName optset) + in case testEquality tyOpt BaseIntegerRepr of + Just Refl -> setOpt optset val + Nothing -> + checkOptSetResult optset $ optErr $ + "option type is a" <+> pretty tyOpt <+> "but given an integer" + +-- | Given a boolean value, set the named option to that value or +-- generate an OptSetFailure exception if the option is not a boolean +-- valued option. +setBoolOpt :: Some OptionSetting -> Bool -> IO [Doc Void] +setBoolOpt (Some optset) val = + let tyOpt = configOptionType (optionSettingName optset) + in case testEquality tyOpt BaseBoolRepr of + Just Refl -> setOpt optset val + Nothing -> + checkOptSetResult optset $ optErr $ + "option type is a" <+> pretty tyOpt <+> "but given a boolean" + + -- | Given a @ConfigOption@ name, produce an @OptionSetting@ -- object for accessing and setting the value of that option. -- @@ -768,7 +1052,7 @@ getOptionSetting :: getOptionSetting o@(ConfigOption tp (p:|ps)) (Config cfg) = readMVar cfg >>= getConst . adjustConfigMap p ps f where - f Nothing = Const (fail $ "Option not found: " ++ show o) + f Nothing = Const (throwM $ OptGetFailure (OCfg $ Some o) "not found") f (Just x) = Const (leafToSetting x) leafToSetting (ConfigLeaf sty ref _h) @@ -781,8 +1065,11 @@ getOptionSetting o@(ConfigOption tp (p:|ps)) (Config cfg) = let new = if (isJust (optionSetError res)) then old else (Just v) new `seq` return (new, res) } - | otherwise = fail ("Type mismatch retrieving option " ++ show o ++ - "\nExpected: " ++ show tp ++ " but found " ++ show (opt_type sty)) + | otherwise = throwM $ OptGetFailure (OCfg $ Some o) + (pretty $ "Type mismatch: " <> + "expected '" <> show tp <> + "' but found '" <> show (opt_type sty) <> "'" + ) -- | Given a text name, produce an @OptionSetting@ -- object for accessing and setting the value of that option. @@ -794,10 +1081,12 @@ getOptionSettingFromText :: IO (Some OptionSetting) getOptionSettingFromText nm (Config cfg) = case splitPath nm of - Nothing -> fail "Illegal empty name for option" + Nothing -> throwM $ OptGetFailure (OName "") "Illegal empty name for option" Just (p:|ps) -> readMVar cfg >>= (getConst . adjustConfigMap p ps (f (p:|ps))) where - f (p:|ps) Nothing = Const (fail $ "Option not found: " ++ (Text.unpack (Text.intercalate "." (p:ps)))) + f (p:|ps) Nothing = Const (throwM $ OptGetFailure + (OName (Text.intercalate "." (p:ps))) + "not found") f path (Just x) = Const (leafToSetting path x) leafToSetting path (ConfigLeaf sty ref _h) = return $ @@ -815,6 +1104,12 @@ getOptionSettingFromText nm (Config cfg) = data ConfigValue where ConfigValue :: ConfigOption tp -> ConcreteVal tp -> ConfigValue +instance Pretty ConfigValue where + pretty (ConfigValue option val) = + ppSetting (configOptionNameParts option) (Just val) + <+> "::" <+> pretty (configOptionType option) + + -- | Given the name of a subtree, return all -- the currently-set configurtion values in that subtree. -- @@ -825,9 +1120,10 @@ getConfigValues :: IO [ConfigValue] getConfigValues prefix (Config cfg) = do m <- readMVar cfg - let ps = Text.splitOn "." prefix + let ps = dropWhile Text.null $ Text.splitOn "." prefix f :: [Text] -> ConfigLeaf -> WriterT (Seq ConfigValue) IO ConfigLeaf - f [] _ = fail $ "getConfigValues: illegal empty option name" + f [] _ = throwM $ OptGetFailure (OName prefix) + "illegal empty option prefix name" f (p:path) l@(ConfigLeaf sty ref _h) = do liftIO (readMVar ref) >>= \case Just x -> tell (Seq.singleton (ConfigValue (ConfigOption (opt_type sty) (p:|path)) x)) @@ -845,7 +1141,7 @@ ppOption :: [Text] -> OptionStyle tp -> Maybe (ConcreteVal tp) -> Maybe (Doc Voi ppOption nm sty x help = vcat [ group $ fillCat [ppSetting nm x, indent 2 (opt_help sty)] - , maybe mempty (indent 2) help + , maybe mempty (indent 4) help ] ppConfigLeaf :: [Text] -> ConfigLeaf -> IO (Doc Void) @@ -854,7 +1150,7 @@ ppConfigLeaf nm (ConfigLeaf sty ref help) = return $ ppOption nm sty x help -- | Given the name of a subtree, compute help text for --- all the options avaliable in that subtree. +-- all the options available in that subtree. -- -- If the subtree name is empty, the entire tree will be traversed. configHelp :: @@ -863,7 +1159,7 @@ configHelp :: IO [Doc Void] configHelp prefix (Config cfg) = do m <- readMVar cfg - let ps = Text.splitOn "." prefix + let ps = dropWhile Text.null $ Text.splitOn "." prefix f :: [Text] -> ConfigLeaf -> WriterT (Seq (Doc Void)) IO ConfigLeaf f nm leaf = do d <- liftIO (ppConfigLeaf nm leaf) tell (Seq.singleton d) diff --git a/what4/src/What4/Protocol/Online.hs b/what4/src/What4/Protocol/Online.hs index 065f2918..14a3544c 100644 --- a/what4/src/What4/Protocol/Online.hs +++ b/what4/src/What4/Protocol/Online.hs @@ -18,6 +18,8 @@ module What4.Protocol.Online ( OnlineSolver(..) , AnOnlineSolver(..) , SolverProcess(..) + , solverStdin + , solverResponse , SolverGoalTimeout(..) , getGoalTimeoutInSeconds , ErrorBehavior(..) @@ -134,12 +136,6 @@ data SolverProcess scope solver = SolverProcess , solverHandle :: !ProcessHandle -- ^ Handle to the solver process - , solverStdin :: !(Streams.OutputStream Text) - -- ^ Standard in for the solver process. - - , solverResponse :: !(Streams.InputStream Text) - -- ^ Wrap the solver's stdout, for easier parsing of responses. - , solverErrorBehavior :: !ErrorBehavior -- ^ Indicate this solver's behavior following an error response @@ -176,6 +172,15 @@ data SolverProcess scope solver = SolverProcess } +-- | Standard input stream for the solver process. +solverStdin :: (SolverProcess t solver) -> (Streams.OutputStream Text) +solverStdin = connHandle . solverConn + +-- | The solver's stdout, for easier parsing of responses. +solverResponse :: (SolverProcess t solver) -> (Streams.InputStream Text) +solverResponse = connInputHandle . solverConn + + -- | An impolite way to shut down a solver. Prefer to use -- `shutdownSolverProcess`, unless the solver is unresponsive -- or in some unrecoverable error state. @@ -396,7 +401,7 @@ getUnsatAssumptions proc = unless (supportedFeatures conn `hasProblemFeature` useUnsatAssumptions) $ fail $ show $ pretty (smtWriterName conn) <+> pretty "is not configured to produce UNSAT assumption lists" addCommandNoAck conn (getUnsatAssumptionsCommand conn) - smtUnsatAssumptionsResult conn (solverResponse proc) + smtUnsatAssumptionsResult conn conn -- | After an unsatisfiable check-sat command, compute a set of the named assertions -- that (together with all the unnamed assertions) form an unsatisfiable core. @@ -407,14 +412,13 @@ getUnsatCore proc = unless (supportedFeatures conn `hasProblemFeature` useUnsatCores) $ fail $ show $ pretty (smtWriterName conn) <+> pretty "is not configured to produce UNSAT cores" addCommandNoAck conn (getUnsatCoreCommand conn) - smtUnsatCoreResult conn (solverResponse proc) + smtUnsatCoreResult conn conn -- | Get the sat result from a previous SAT command. getSatResult :: SMTReadWriter s => SolverProcess t s -> IO (SatResult () ()) getSatResult yp = do let ph = solverHandle yp - let err_reader = solverStderr yp - sat_result <- tryJust filterAsync (smtSatResult yp (solverResponse yp)) + sat_result <- tryJust filterAsync (smtSatResult yp (solverConn yp)) case sat_result of Right ok -> return ok @@ -422,7 +426,7 @@ getSatResult yp = do do -- Interrupt process terminateProcess ph - txt <- readAllLines err_reader + txt <- readAllLines $ solverStderr yp -- Wait for process to end ec <- waitForProcess ph diff --git a/what4/src/What4/Protocol/SExp.hs b/what4/src/What4/Protocol/SExp.hs index 83f23797..c120d0fd 100644 --- a/what4/src/What4/Protocol/SExp.hs +++ b/what4/src/What4/Protocol/SExp.hs @@ -13,6 +13,7 @@ returned by SMT solvers. module What4.Protocol.SExp ( SExp(..) , parseSExp + , parseSExpBody , stringToSExp , parseNextWord , asAtomList @@ -61,16 +62,29 @@ isTokenChar c = not (isSpace c) readToken :: Parser Text readToken = takeWhile1 isTokenChar +-- | Parses an SExp. If the input is a string (recognized by the +-- 'readString' argument), return that as an 'SString'; if the input +-- is a single token, return that as an 'SAtom'. + parseSExp :: Parser Text {- ^ A parser for string literals -} -> Parser SExp parseSExp readString = do skipSpaceOrNewline - msum [ char '(' *> skipSpaceOrNewline *> (SApp <$> many (parseSExp readString)) <* skipSpaceOrNewline <* char ')' + msum [ char '(' *> parseSExpBody readString , SString <$> readString , SAtom <$> readToken ] +-- | Parses the body of an SExp after the opening '(' has already been +-- parsed. + +parseSExpBody :: + Parser Text {- ^ A parser for string literals -} -> + Parser SExp +parseSExpBody readString = + skipSpaceOrNewline *> (SApp <$> many (parseSExp readString)) <* skipSpaceOrNewline <* char ')' + stringToSExp :: MonadFail m => Parser Text {- ^ A parser for string literals -} -> String -> @@ -96,4 +110,4 @@ asAtomList (SApp xs) = go xs go [] = Just [] go (SAtom a:ys) = (a:) <$> go ys go _ = Nothing -asAtomList _ = Nothing \ No newline at end of file +asAtomList _ = Nothing diff --git a/what4/src/What4/Protocol/SMTLib2.hs b/what4/src/What4/Protocol/SMTLib2.hs index 6d611621..6eb8bea1 100644 --- a/what4/src/What4/Protocol/SMTLib2.hs +++ b/what4/src/What4/Protocol/SMTLib2.hs @@ -47,6 +47,7 @@ module What4.Protocol.SMTLib2 , nameResult , setProduceModels , smtLibEvalFuns + , smtlib2Options -- * Logic , SMT2.Logic(..) , SMT2.qf_bv @@ -90,7 +91,6 @@ import Control.Monad.Fail( MonadFail ) import Control.Applicative import Control.Exception import Control.Monad.State.Strict -import qualified Data.Attoparsec.Text as AT import qualified Data.BitVector.Sized as BV import qualified Data.Bits as Bits import Data.ByteString (ByteString) @@ -121,7 +121,6 @@ import Numeric.Natural import qualified System.Exit as Exit import qualified System.IO as IO import qualified System.IO.Streams as Streams -import qualified System.IO.Streams.Attoparsec.Text as Streams import Data.Versions (Version(..)) import qualified Data.Versions as Versions import qualified Prettyprinter as PP @@ -130,6 +129,7 @@ import LibBF( bfToBits ) import Prelude hiding (writeFile) import What4.BaseTypes +import qualified What4.Config as CFG import qualified What4.Expr.Builder as B import What4.Expr.GroundEval import qualified What4.Interface as I @@ -139,6 +139,7 @@ import What4.Protocol.ReadDecimal import What4.Protocol.SExp import What4.Protocol.SMTLib2.Syntax (Term, term_app, un_app, bin_app) +import What4.Protocol.SMTLib2.Response import qualified What4.Protocol.SMTLib2.Syntax as SMT2 hiding (Term) import qualified What4.Protocol.SMTWriter as SMTWriter import What4.Protocol.SMTWriter hiding (assume, Term) @@ -154,6 +155,10 @@ all_supported :: SMT2.Logic all_supported = SMT2.allSupported {-# DEPRECATED all_supported "Use allSupported" #-} + +smtlib2Options :: [CFG.ConfigDesc] +smtlib2Options = smtParseOptions + ------------------------------------------------------------------------ -- Floating point @@ -565,6 +570,8 @@ newWriter :: a -- (may be the @nullInput@ stream if no responses are expected) -> AcknowledgementAction t (Writer a) -- ^ Action to run for consuming acknowledgement messages + -> ResponseStrictness + -- ^ Be strict in parsing SMT solver responses? -> String -- ^ Name of solver for reporting purposes. -> Bool @@ -577,13 +584,13 @@ newWriter :: a -> B.SymbolVarBimap t -- ^ Variable bindings for names. -> IO (WriterConn t (Writer a)) -newWriter _ h in_h ack solver_name permitDefineFun arithOption quantSupport bindings = do +newWriter _ h in_h ack isStrict solver_name permitDefineFun arithOption quantSupport bindings = do r <- newIORef Set.empty let initWriter = Writer { declaredTuples = r } - conn <- newWriterConn h in_h ack solver_name arithOption bindings initWriter + conn <- newWriterConn h in_h ack solver_name isStrict arithOption bindings initWriter return $! conn { supportFunctionDefs = permitDefineFun , supportQuantifiers = quantSupport } @@ -813,17 +820,6 @@ data Session t a = Session , sessionResponse :: !(Streams.InputStream Text) } -parseSMTLib2String :: AT.Parser Text -parseSMTLib2String = AT.char '\"' >> go - where - go :: AT.Parser Text - go = do xs <- AT.takeWhile (not . (=='\"')) - _ <- AT.char '\"' - (do _ <- AT.char '\"' - ys <- go - return (xs <> "\"" <> ys) - ) <|> return xs - -- | Get a value from a solver (must be called after checkSat) runGetValue :: SMTLib2Tweaks a => Session t a @@ -831,11 +827,10 @@ runGetValue :: SMTLib2Tweaks a -> IO SExp runGetValue s e = do writeGetValue (sessionWriter s) [ e ] - msexp <- try $ Streams.parseFromStream (parseSExp parseSMTLib2String) (sessionResponse s) - case msexp of - Left Streams.ParseException{} -> fail $ "Could not parse solver value." - Right (SApp [SApp [_, b]]) -> return b - Right sexp -> fail $ "Could not parse solver value:\n " ++ show sexp + let valRsp = \case + AckSuccessSExp (SApp [SApp [_, b]]) -> Just b + _ -> Nothing + getLimitedSolverResponse "get value" valRsp (sessionWriter s) (SMT2.getValue [e]) -- | This function runs a check sat command runCheckSat :: forall b t a. @@ -849,7 +844,7 @@ runCheckSat s doEval = do let w = sessionWriter s r = sessionResponse s addCommands w (checkCommands w) - res <- smtSatResult w r + res <- smtSatResult w w case res of Unsat x -> doEval (Unsat x) Unknown -> doEval Unknown @@ -857,93 +852,39 @@ runCheckSat s doEval = do evalFn <- smtExprGroundEvalFn w (smtEvalFuns w r) doEval (Sat (evalFn, Nothing)) --- | Called when methods in the following instance encounter an exception -throwSMTLib2ParseError :: (Exception e) => Text -> SMT2.Command -> e -> m a -throwSMTLib2ParseError what cmd e = - throw $ SMTLib2ParseError [cmd] $ Text.unlines - [ Text.unwords ["Could not parse result from", what, "."] - , "*** Exception: " <> Text.pack (displayException e) - ] - instance SMTLib2Tweaks a => SMTReadWriter (Writer a) where smtEvalFuns w s = smtLibEvalFuns Session { sessionWriter = w , sessionResponse = s } smtSatResult p s = - do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) - case mb of - Left (SomeException e) -> - fail $ unlines [ "Could not parse check_sat result." - , "*** Exception: " ++ displayException e - ] - Right (SAtom "unsat") -> return (Unsat ()) - Right (SAtom "sat") -> return (Sat ()) - Right (SAtom "unknown") -> return Unknown - Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error (head $ reverse (checkCommands p)) msg) - Right res -> throw $ SMTLib2ParseError (checkCommands p) (Text.pack (show res)) + let satRsp = \case + AckSat -> Just $ Sat () + AckUnsat -> Just $ Unsat () + AckUnknown -> Just Unknown + _ -> Nothing + in getLimitedSolverResponse "sat result" satRsp s + (head $ reverse $ checkCommands p) smtUnsatAssumptionsResult p s = - do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) - let cmd = getUnsatAssumptionsCommand p - case mb of - Right (asNegAtomList -> Just as) -> return as - Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error cmd msg) - Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res))) - Left (SomeException e) -> - throwSMTLib2ParseError "unsat assumptions" cmd e + let unsatAssumpRsp = \case + AckSuccessSExp (asNegAtomList -> Just as) -> Just as + _ -> Nothing + cmd = getUnsatAssumptionsCommand p + in getLimitedSolverResponse "unsat assumptions" unsatAssumpRsp s cmd smtUnsatCoreResult p s = - do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) - let cmd = getUnsatCoreCommand p - case mb of - Right (asAtomList -> Just nms) -> return nms - Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error cmd msg) - Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res))) - Left (SomeException e) -> - throwSMTLib2ParseError "unsat core" cmd e + let unsatCoreRsp = \case + AckSuccessSExp (asAtomList -> Just nms) -> Just nms + _ -> Nothing + cmd = getUnsatCoreCommand p + in getLimitedSolverResponse "unsat core" unsatCoreRsp s cmd -data SMTLib2Exception - = SMTLib2Unsupported SMT2.Command - | SMTLib2Error SMT2.Command Text - | SMTLib2ParseError [SMT2.Command] Text - -instance Show SMTLib2Exception where - show (SMTLib2Unsupported (SMT2.Cmd cmd)) = - unlines - [ "unsupported command:" - , " " ++ Lazy.unpack (Builder.toLazyText cmd) - ] - show (SMTLib2Error (SMT2.Cmd cmd) msg) = - unlines - [ "Solver reported an error:" - , " " ++ Text.unpack msg - , "in response to command:" - , " " ++ Lazy.unpack (Builder.toLazyText cmd) - ] - show (SMTLib2ParseError cmds msg) = - unlines $ - [ "Could not parse solver response:" - , " " ++ Text.unpack msg - , "in response to commands:" - ] ++ map cmdToString cmds - where cmdToString (SMT2.Cmd cmd) = - " " ++ Lazy.unpack (Builder.toLazyText cmd) - -instance Exception SMTLib2Exception - smtAckResult :: AcknowledgementAction t (Writer a) -smtAckResult = AckAction $ \conn cmd -> - do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) (connInputHandle conn)) - case mb of - Right (SAtom "success") -> return () - Right (SAtom "unsupported") -> throw (SMTLib2Unsupported cmd) - Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error cmd msg) - Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res))) - Left (SomeException e) -> throw $ SMTLib2ParseError [cmd] $ Text.pack $ - unlines [ "Could not parse acknowledgement result." - , "*** Exception: " ++ displayException e - ] +smtAckResult = AckAction $ getLimitedSolverResponse "get ack" $ \case + AckSuccess -> Just () + _ -> Nothing + smtLibEvalFuns :: forall t a. SMTLib2Tweaks a => Session t a -> SMTEvalFunctions (Writer a) @@ -977,8 +918,8 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where defaultFeatures :: a -> ProblemFeatures - getErrorBehavior :: a -> WriterConn t (Writer a) -> Streams.InputStream Text -> IO ErrorBehavior - getErrorBehavior _ _ _ = return ImmediateExit + getErrorBehavior :: a -> WriterConn t (Writer a) -> IO ErrorBehavior + getErrorBehavior _ _ = return ImmediateExit supportsResetAssertions :: a -> Bool supportsResetAssertions _ = False @@ -989,12 +930,16 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures -> + -- | strictness override configuration + Maybe (CFG.ConfigOption I.BaseBoolType) -> B.ExprBuilder t st fs -> Streams.OutputStream Text -> Streams.InputStream Text -> IO (WriterConn t (Writer a)) - newDefaultWriter solver ack feats sym h in_h = - newWriter solver h in_h ack (show solver) True feats True + newDefaultWriter solver ack feats strictOpt sym h in_h = do + let cfg = I.getConfiguration sym + strictness <- parserStrictness strictOpt strictSMTParsing cfg + newWriter solver h in_h ack strictness (show solver) True feats True =<< B.getSymbolVarBimap sym -- | Run the solver in a session. @@ -1002,6 +947,8 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures + -> Maybe (CFG.ConfigOption I.BaseBoolType) + -- ^ strictness override configuration -> B.ExprBuilder t st fs -> FilePath -- ^ Path to solver executable @@ -1009,7 +956,7 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where -> (Session t a -> IO b) -- ^ Action to run -> IO b - withSolver solver ack feats sym path logData action = do + withSolver solver ack feats strictOpt sym path logData action = do args <- defaultSolverArgs solver sym withProcessHandles path args Nothing $ \hdls@(in_h, out_h, err_h, _ph) -> do @@ -1018,7 +965,7 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where demuxProcessHandles in_h out_h err_h (fmap (\x -> ("; ", x)) $ logHandle logData) - writer <- newDefaultWriter solver ack feats sym in_stream out_stream + writer <- newDefaultWriter solver ack feats strictOpt sym in_stream out_stream let s = Session { sessionWriter = writer , sessionResponse = out_stream @@ -1044,19 +991,21 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures + -> Maybe (CFG.ConfigOption I.BaseBoolType) + -- ^ strictness override configuration -> B.ExprBuilder t st fs -> LogData -> [B.BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b - runSolverInOverride solver ack feats sym logData predicates cont = do + runSolverInOverride solver ack feats strictOpt sym logData predicates cont = do I.logSolverEvent sym (I.SolverStartSATQuery $ I.SolverStartSATQueryRec { I.satQuerySolverName = show solver , I.satQueryReason = logReason logData }) path <- defaultSolverPath solver sym - withSolver solver ack feats sym path (logData{logVerbosity=2}) $ \session -> do + withSolver solver ack feats strictOpt sym path (logData{logVerbosity=2}) $ \session -> do -- Assume the predicates hold. forM_ predicates (SMTWriter.assume (sessionWriter session)) -- Run check SAT and get the model back. @@ -1076,15 +1025,19 @@ writeDefaultSMT2 :: SMTLib2Tweaks a -- ^ Name of solver for reporting. -> ProblemFeatures -- ^ Features supported by solver + -> Maybe (CFG.ConfigOption I.BaseBoolType) + -- ^ strictness override configuration -> B.ExprBuilder t st fs -> IO.Handle -> [B.BoolExpr t] -> IO () -writeDefaultSMT2 a nm feat sym h ps = do +writeDefaultSMT2 a nm feat strictOpt sym h ps = do bindings <- B.getSymbolVarBimap sym str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h null_in <- Streams.nullInput - c <- newWriter a str null_in nullAcknowledgementAction nm True feat True bindings + let cfg = I.getConfiguration sym + strictness <- parserStrictness strictOpt strictSMTParsing cfg + c <- newWriter a str null_in nullAcknowledgementAction strictness nm True feat True bindings setProduceModels c True forM_ ps (SMTWriter.assume c) writeCheckSat c @@ -1097,10 +1050,12 @@ startSolver -- ^ Action for acknowledging command responses -> (WriterConn t (Writer a) -> IO ()) -- ^ Action for setting start-up-time options and logic -> ProblemFeatures + -> Maybe (CFG.ConfigOption I.BaseBoolType) + -- ^ strictness override configuration -> Maybe IO.Handle -> B.ExprBuilder t st fs -> IO (SolverProcess t (Writer a)) -startSolver solver ack setup feats auxOutput sym = do +startSolver solver ack setup feats strictOpt auxOutput sym = do path <- defaultSolverPath solver sym args <- defaultSolverArgs solver sym hdls@(in_h, out_h, err_h, ph) <- startProcess path args Nothing @@ -1110,13 +1065,13 @@ startSolver solver ack setup feats auxOutput sym = do (fmap (\x -> ("; ", x)) auxOutput) -- Create writer - writer <- newDefaultWriter solver ack feats sym in_stream out_stream + writer <- newDefaultWriter solver ack feats strictOpt sym in_stream out_stream -- Set solver logic and solver-specific options setup writer -- Query the solver for it's error behavior - errBeh <- getErrorBehavior solver writer out_stream + errBeh <- getErrorBehavior solver writer earlyUnsatRef <- newIORef Nothing @@ -1126,11 +1081,9 @@ startSolver solver ack setup feats auxOutput sym = do return $! SolverProcess { solverConn = writer , solverCleanupCallback = cleanupProcess hdls - , solverStdin = in_stream , solverStderr = err_reader , solverHandle = ph , solverErrorBehavior = errBeh - , solverResponse = out_stream , solverEvalFuns = smtEvalFuns writer out_stream , solverLogFn = I.logSolverEvent sym , solverName = show solver @@ -1192,45 +1145,42 @@ ppSolverVersionError err = na Nothing = "n/a" -- | Get the result of a version query -nameResult :: Streams.InputStream Text -> IO Text -nameResult s = - let cmd = SMT2.getName - in - tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) >>= - \case - Right (SApp [SAtom ":name", SString nm]) -> pure nm - Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error cmd msg) - Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res))) - Left (SomeException e) -> - throwSMTLib2ParseError "name query" cmd e +nameResult :: WriterConn t a -> IO Text +nameResult conn = + getLimitedSolverResponse "solver name" + (\case + RspName nm -> Just nm + _ -> Nothing + ) + conn SMT2.getName -- | Query the solver's error behavior setting queryErrorBehavior :: SMTLib2Tweaks a => - WriterConn t (Writer a) -> Streams.InputStream Text -> IO ErrorBehavior -queryErrorBehavior conn resp = + WriterConn t (Writer a) -> IO ErrorBehavior +queryErrorBehavior conn = do let cmd = SMT2.getErrorBehavior writeCommand conn cmd - tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) resp) >>= - \case - Right (SApp [SAtom ":error-behavior", SAtom "continued-execution"]) -> return ContinueOnError - Right (SApp [SAtom ":error-behavior", SAtom "immediate-exit"]) -> return ImmediateExit - Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res))) - Left (SomeException e) -> throwSMTLib2ParseError "error behavior query" cmd e + getLimitedSolverResponse "error behavior" + (\case + RspErrBehavior bh -> case bh of + "continued-execution" -> return ContinueOnError + "immediate-exit" -> return ImmediateExit + _ -> throw $ SMTLib2ResponseUnrecognized cmd bh + _ -> Nothing + ) conn cmd -- | Get the result of a version query -versionResult :: Streams.InputStream Text -> IO Text -versionResult s = - let cmd = SMT2.getVersion - in - tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) >>= - \case - Right (SApp [SAtom ":version", SString v]) -> pure v - Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error cmd msg) - Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res))) - Left (SomeException e) -> - throwSMTLib2ParseError "version query" cmd e +versionResult :: WriterConn t a -> IO Text +versionResult conn = + getLimitedSolverResponse "solver version" + (\case + RspVersion v -> Just v + _ -> Nothing + ) + conn SMT2.getVersion + -- | Ensure the solver's version falls within a known-good range. checkSolverVersion' :: SMTLib2Tweaks solver => @@ -1246,7 +1196,7 @@ checkSolverVersion' boundsMap proc = Nothing -> done Just bnds -> do getVersion conn - res <- versionResult (solverResponse proc) + res <- versionResult $ solverConn proc case Versions.version res of Left e -> pure (Left (UnparseableVersion e)) Right actualVer -> diff --git a/what4/src/What4/Protocol/SMTLib2/Response.hs b/what4/src/What4/Protocol/SMTLib2/Response.hs new file mode 100644 index 00000000..8f3021ec --- /dev/null +++ b/what4/src/What4/Protocol/SMTLib2/Response.hs @@ -0,0 +1,241 @@ +{-| +This module defines types and operations for parsing SMTLib2 solver responses. + +These are high-level responses, as describe in +@https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf@, +page 47, Figure 3.9. + +This parser is designed to be the top level handling for solver +responses, and to be used in conjuction with +What4.Protocol.SMTLib2.Parse and What4.Protocol.SExp with the latter +handling detailed parsing of specific constructs returned in the body +of the general response. +-} + +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} + +module What4.Protocol.SMTLib2.Response + ( + SMTResponse(..) + , SMTLib2Exception(..) + , getSolverResponse + , getLimitedSolverResponse + , smtParseOptions + , strictSMTParsing + , strictSMTParseOpt + ) +where + +import Control.Applicative +import Control.Exception +import qualified Data.Attoparsec.Text as AT +import Data.Text ( Text ) +import qualified Data.Text as Text +import qualified Data.Text.Lazy as Lazy +import qualified Data.Text.Lazy.Builder as Builder +import qualified Prettyprinter.Util as PPU +import qualified System.IO.Streams as Streams +import qualified System.IO.Streams.Attoparsec.Text as AStreams + +import qualified What4.BaseTypes as BT +import qualified What4.Config as CFG +import What4.Protocol.SExp +import qualified What4.Protocol.SMTLib2.Syntax as SMT2 +import qualified What4.Protocol.SMTWriter as SMTWriter +import What4.Utils.Process ( filterAsync ) + + +strictSMTParsing :: CFG.ConfigOption BT.BaseBoolType +strictSMTParsing = CFG.configOption BT.BaseBoolRepr "solver.strict_parsing" + +strictSMTParseOpt :: CFG.ConfigDesc +strictSMTParseOpt = + CFG.mkOpt strictSMTParsing CFG.boolOptSty + (Just $ PPU.reflow $ + Text.concat ["Strictly parse SMT responses and fail on" + , "unrecognized data (the default)." + , "This might need to be disabled when running" + , "the SMT solver in verbose mode." + ]) + Nothing + +smtParseOptions :: [CFG.ConfigDesc] +smtParseOptions = [ strictSMTParseOpt ] + + +data SMTResponse = AckSuccess + | AckUnsupported + | AckError Text + | AckSat + | AckUnsat + | AckUnknown + | RspName Text + | RspVersion Text + | RspErrBehavior Text + | RspOutOfMemory + | RspRsnIncomplete + | RspUnkReason SExp + | AckSuccessSExp SExp + | AckSkipped Text SMTResponse + deriving (Eq, Show) + +-- | Called to get a response from the SMT connection. + +getSolverResponse :: SMTWriter.WriterConn t h + -> IO (Either SomeException SMTResponse) +getSolverResponse conn = do + mb <- tryJust filterAsync + (AStreams.parseFromStream + (rspParser (SMTWriter.strictParsing conn)) + (SMTWriter.connInputHandle conn)) + return mb + + +-- | Gets a limited set of responses, throwing an exception when a +-- response is not matched by the filter. Also throws exceptions for +-- standard error results. The passed command and intent arguments +-- are only used for marking error messages. +-- +-- Callers which do not want exceptions thrown for standard error +-- conditions should feel free to use 'getSolverResponse' and handle +-- all response cases themselves. + +getLimitedSolverResponse :: String + -> (SMTResponse -> Maybe a) + -> SMTWriter.WriterConn t h + -> SMT2.Command + -> IO a +getLimitedSolverResponse intent handleResponse conn cmd = + let validateResp rsp = + case rsp of + AckUnsupported -> throw (SMTLib2Unsupported cmd) + (AckError msg) -> throw (SMTLib2Error cmd msg) + (AckSkipped line rest) -> validateResp rest + _ -> case handleResponse rsp of + Just x -> return x + Nothing -> throw $ SMTLib2InvalidResponse cmd intent rsp + in getSolverResponse conn >>= \case + Right rsp -> validateResp rsp + Left (SomeException e) -> do + curInp <- Streams.read (SMTWriter.connInputHandle conn) + throw $ SMTLib2ParseError intent [cmd] $ Text.pack $ + unlines [ "Solver response parsing failure." + , "*** Exception: " ++ displayException e + , "Attempting to parse input for " <> intent <> ":" + , show curInp + ] + + +rspParser :: SMTWriter.ResponseStrictness -> AT.Parser SMTResponse +rspParser strictness = + let lexeme p = skipSpaceOrNewline *> p + parens p = AT.char '(' *> p <* AT.char ')' + errParser = parens $ lexeme (AT.string "error") + *> (AckError <$> lexeme parseSMTLib2String) + specific_success_response = check_sat_response <|> get_info_response + check_sat_response = (AckSat <$ AT.string "sat") + <|> (AckUnsat <$ AT.string "unsat") + <|> (AckUnknown <$ AT.string "unknown") + get_info_response = parens info_response + info_response = errBhvParser + <|> nameParser + <|> unkReasonParser + <|> versionParser + nameParser = lexeme (AT.string ":name") + *> lexeme (RspName <$> parseSMTLib2String) + versionParser = lexeme (AT.string ":version") + *> lexeme (RspVersion <$> parseSMTLib2String) + errBhvParser = lexeme (AT.string ":error-behavior") + *> lexeme (RspErrBehavior <$> + (AT.string "continued-execution" + <|> AT.string "immediate-exit") + -- Explicit error instead of generic + -- fallback since :error-behavior was + -- matched but behavior type was not. + <|> throw (SMTLib2ResponseUnrecognized + SMT2.getErrorBehavior + "bad :error-behavior value") + ) + unkReasonParser = + lexeme (AT.string ":reason-unknown") + *> lexeme (RspOutOfMemory <$ AT.string "memout" + <|> RspRsnIncomplete <$ AT.string "incomplete" + <|> (AT.char '(' *> (RspUnkReason <$> parseSExpBody parseSMTLib2String)) + -- already matched :reason-unknown, so any other + -- arguments to that are errors. + <|> throw (SMTLib2ResponseUnrecognized + (SMT2.Cmd "reason?") + "bad :reason-unknown value") + ) + in skipSpaceOrNewline *> + ((AckSuccess <$ AT.string "success") + <|> (AckUnsupported <$ AT.string "unsupported") + <|> specific_success_response + <|> errParser + <|> (AT.char '(' *> (AckSuccessSExp <$> parseSExpBody parseSMTLib2String)) + -- sometimes verbose output mode will generate interim text + -- before the actual ack; the following skips lines of input + -- that aren't recognized. + <|> (case strictness of + SMTWriter.Strict -> empty + SMTWriter.Lenient -> AckSkipped + <$> AT.takeWhile1 (not . AT.isEndOfLine) + <*> (rspParser strictness)) + ) + +parseSMTLib2String :: AT.Parser Text +parseSMTLib2String = AT.char '\"' >> go + where + go :: AT.Parser Text + go = do xs <- AT.takeWhile (not . (=='\"')) + _ <- AT.char '\"' + (do _ <- AT.char '\"' + ys <- go + return (xs <> "\"" <> ys) + ) <|> return xs + +---------------------------------------------------------------------- + +data SMTLib2Exception + = SMTLib2Unsupported SMT2.Command + | SMTLib2Error SMT2.Command Text + | SMTLib2ParseError SMTLib2Intent [SMT2.Command] Text + | SMTLib2ResponseUnrecognized SMT2.Command Text + | SMTLib2InvalidResponse SMT2.Command SMTLib2Intent SMTResponse + +type SMTLib2Intent = String + +instance Show SMTLib2Exception where + show = + let showCmd (SMT2.Cmd c) = Lazy.unpack $ Builder.toLazyText c + in unlines . \case + (SMTLib2Unsupported cmd) -> + [ "unsupported command:" + , " " <> showCmd cmd + ] + (SMTLib2Error cmd msg) -> + [ "Solver reported an error:" + , " " ++ Text.unpack msg + , "in response to command:" + , " " <> showCmd cmd + ] + (SMTLib2ParseError intent cmds msg) -> + [ "Could not parse solver response:" + , " " ++ Text.unpack msg + , "in response to commands for " <> intent <> ":" + ] ++ map showCmd cmds + (SMTLib2ResponseUnrecognized cmd rsp) -> + [ "Unrecognized response from solver:" + , " " <> Text.unpack rsp + , "in response to command:" + , " " <> showCmd cmd + ] + (SMTLib2InvalidResponse cmd intent rsp) -> + [ "Received parsed and understood but unexpected response from solver:" + , " " <> show rsp + , "in response to command for " <> intent <> ":" + , " " <> showCmd cmd + ] + +instance Exception SMTLib2Exception diff --git a/what4/src/What4/Protocol/SMTWriter.hs b/what4/src/What4/Protocol/SMTWriter.hs index d1fa985d..1b0fdd86 100644 --- a/what4/src/What4/Protocol/SMTWriter.hs +++ b/what4/src/What4/Protocol/SMTWriter.hs @@ -57,6 +57,7 @@ module What4.Protocol.SMTWriter , supportFunctionArguments , supportQuantifiers , supportedFeatures + , strictParsing , connHandle , connInputHandle , smtWriterName @@ -82,6 +83,8 @@ module What4.Protocol.SMTWriter , assumeFormulaWithFreshName , DefineStyle(..) , AcknowledgementAction(..) + , ResponseStrictness(..) + , parserStrictness , nullAcknowledgementAction -- * SMTWriter operations , assume @@ -102,7 +105,7 @@ import Control.Monad.Fail( MonadFail ) #endif import Control.Exception -import Control.Lens hiding ((.>)) +import Control.Lens hiding ((.>), Strict) import Control.Monad.Extra import Control.Monad.IO.Class import Control.Monad.Reader @@ -138,15 +141,16 @@ import System.IO.Streams (OutputStream, InputStream) import qualified System.IO.Streams as Streams import What4.BaseTypes -import What4.Interface (RoundingMode(..), stringInfo) -import What4.ProblemFeatures +import qualified What4.Config as CFG import qualified What4.Expr.ArrayUpdateMap as AUM import qualified What4.Expr.BoolMap as BM import What4.Expr.Builder import What4.Expr.GroundEval import qualified What4.Expr.StringSeq as SSeq -import qualified What4.Expr.WeightedSum as WSum import qualified What4.Expr.UnaryBV as UnaryBV +import qualified What4.Expr.WeightedSum as WSum +import What4.Interface (RoundingMode(..), stringInfo) +import What4.ProblemFeatures import What4.ProgramLoc import What4.SatResult import qualified What4.SemiRing as SR @@ -589,6 +593,7 @@ data StackEntry t (h :: Type) = StackEntry data WriterConn t (h :: Type) = WriterConn { smtWriterName :: !String -- ^ Name of writer for error reporting purposes. + , connHandle :: !(OutputStream Text) -- ^ Handle to write to @@ -612,6 +617,9 @@ data WriterConn t (h :: Type) = -- indices. , supportQuantifiers :: !Bool -- ^ Allow the SMT writer to generate problems with quantifiers. + , strictParsing :: !ResponseStrictness + -- ^ Be strict in parsing SMTLib2 responses; no + -- verbosity or variants allowed , supportedFeatures :: !ProblemFeatures -- ^ Indicates features supported by the solver. , entryStack :: !(IORef [StackEntry t h]) @@ -701,6 +709,8 @@ newWriterConn :: OutputStream Text -- ^ An action to consume solver acknowledgement responses -> String -- ^ Name of solver for reporting purposes. + -> ResponseStrictness + -- ^ Be strict in parsing responses? -> ProblemFeatures -- ^ Indicates what features are supported by the solver. -> SymbolVarBimap t @@ -708,7 +718,7 @@ newWriterConn :: OutputStream Text -- canonical name (if any). -> cs -- ^ State information specific to the type of connection -> IO (WriterConn t cs) -newWriterConn h in_h ack solver_name features bindings cs = do +newWriterConn h in_h ack solver_name beStrict features bindings cs = do entry <- newStackEntry stk_ref <- newIORef [entry] r <- newIORef emptyState @@ -718,6 +728,7 @@ newWriterConn h in_h ack solver_name features bindings cs = do , supportFunctionDefs = False , supportFunctionArguments = False , supportQuantifiers = False + , strictParsing = beStrict , supportedFeatures = features , entryStack = stk_ref , stateRef = r @@ -726,6 +737,29 @@ newWriterConn h in_h ack solver_name features bindings cs = do , consumeAcknowledgement = ack } +-- | Strictness level for parsing solver responses. +data ResponseStrictness + = Lenient -- ^ allows other output preceeding recognized solver responses + | Strict -- ^ parse _only_ recognized solver responses; fail on anything else + deriving (Eq, Show) + +-- | Given an optional override configuration option, return the SMT +-- response parsing strictness that should be applied based on the +-- override or thedefault strictSMTParsing configuration. +parserStrictness :: Maybe (CFG.ConfigOption BaseBoolType) + -> CFG.ConfigOption BaseBoolType + -> CFG.Config + -> IO ResponseStrictness +parserStrictness overrideOpt strictOpt cfg = do + ovr <- case overrideOpt of + Nothing -> return Nothing + Just o -> CFG.getMaybeOpt =<< CFG.getOptionSetting o cfg + optval <- case ovr of + Just v -> return $ Just v + Nothing -> CFG.getMaybeOpt =<< CFG.getOptionSetting strictOpt cfg + return $ maybe Strict (\c -> if c then Strict else Lenient) optval + + -- | Status to indicate when term value will be uncached. data TermLifetime = DeleteNever @@ -2865,16 +2899,16 @@ class SMTWriter h => SMTReadWriter h where WriterConn t h -> Streams.InputStream Text -> SMTEvalFunctions h -- | Parse a set result from the solver's response. - smtSatResult :: f h -> Streams.InputStream Text -> IO (SatResult () ()) + smtSatResult :: f h -> WriterConn t h -> IO (SatResult () ()) -- | Parse a list of names of assumptions that form an unsatisfiable core. -- These correspond to previously-named assertions. - smtUnsatCoreResult :: f h -> Streams.InputStream Text -> IO [Text] + smtUnsatCoreResult :: f h -> WriterConn t h -> IO [Text] -- | Parse a list of names of assumptions that form an unsatisfiable core. -- The boolean indicates the polarity of the atom: true for an ordinary -- atom, false for a negated atom. - smtUnsatAssumptionsResult :: f h -> Streams.InputStream Text -> IO [(Bool,Text)] + smtUnsatAssumptionsResult :: f h -> WriterConn t h -> IO [(Bool,Text)] -- | Return the terms associated with the given ground index variables. diff --git a/what4/src/What4/Solver.hs b/what4/src/What4/Solver.hs index 558138a0..082e468b 100644 --- a/what4/src/What4/Solver.hs +++ b/what4/src/What4/Solver.hs @@ -45,6 +45,7 @@ module What4.Solver , CVC4(..) , cvc4Adapter , cvc4Path + , cvc4Timeout , runCVC4InOverride , writeCVC4SMT2File , withCVC4 @@ -71,6 +72,9 @@ module What4.Solver -- * Yices , yicesAdapter , yicesPath + , yicesEnableMCSat + , yicesEnableInteractive + , yicesGoalTimeout , runYicesInOverride , writeYicesFile , yicesOptions @@ -79,6 +83,7 @@ module What4.Solver -- * Z3 , Z3(..) , z3Path + , z3Timeout , z3Adapter , runZ3InOverride , withZ3 diff --git a/what4/src/What4/Solver/Adapter.hs b/what4/src/What4/Solver/Adapter.hs index 05ca05bb..3c305ec9 100644 --- a/what4/src/What4/Solver/Adapter.hs +++ b/what4/src/What4/Solver/Adapter.hs @@ -112,8 +112,16 @@ defaultWriteSMTLIB2Features .|. useSymbolicArrays defaultSolverAdapter :: ConfigOption (BaseStringType Unicode) -defaultSolverAdapter = configOption (BaseStringRepr UnicodeRepr) "default_solver" +defaultSolverAdapter = configOption (BaseStringRepr UnicodeRepr) "solver.default" +deprecatedDefaultSolverAdapterConfig :: ConfigOption (BaseStringType Unicode) +deprecatedDefaultSolverAdapterConfig = configOption (BaseStringRepr UnicodeRepr) "default_solver" + + +-- Given a list of solver adapters, returns a tuple of the full set of +-- solver config options for all adapters (plus a configuration to +-- specify the default adapter) and an IO operation that will return +-- current default adapter when executed. solverAdapterOptions :: [SolverAdapter st] -> @@ -121,7 +129,7 @@ solverAdapterOptions :: solverAdapterOptions [] = fail "No solver adapters specified!" solverAdapterOptions xs@(def:_) = do ref <- newIORef def - let opts = sty ref : concatMap solver_adapter_config_options xs + let opts = sty ref : sty' ref : concatMap solver_adapter_config_options xs return (opts, readIORef ref) where @@ -131,6 +139,11 @@ solverAdapterOptions xs@(def:_) = (listOptSty (vals ref)) (Just (PP.pretty "Indicates which solver to use for check-sat queries")) (Just (ConcreteString (UnicodeLiteral (T.pack (solver_adapter_name def))))) + sty' ref = deprecatedOpt [sty ref] $ + mkOpt deprecatedDefaultSolverAdapterConfig + (listOptSty (vals ref)) + (Just (PP.pretty "Indicates which solver to use for check-sat queries.")) + (Just (ConcreteString (UnicodeLiteral (T.pack (solver_adapter_name def))))) -- | Test the ability to interact with a solver by peforming a check-sat query -- on a trivially unsatisfiable problem. diff --git a/what4/src/What4/Solver/Boolector.hs b/what4/src/What4/Solver/Boolector.hs index 633ade95..c8c80b13 100644 --- a/what4/src/What4/Solver/Boolector.hs +++ b/what4/src/What4/Solver/Boolector.hs @@ -30,35 +30,46 @@ import Control.Monad import Data.Bits ( (.|.) ) import What4.BaseTypes -import What4.Config import What4.Concrete -import What4.Interface -import What4.ProblemFeatures -import What4.SatResult +import What4.Config import What4.Expr.Builder import What4.Expr.GroundEval -import What4.Solver.Adapter +import What4.Interface +import What4.ProblemFeatures import What4.Protocol.Online import qualified What4.Protocol.SMTLib2 as SMT2 +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) +import What4.SatResult +import What4.Solver.Adapter import What4.Utils.Process - - data Boolector = Boolector deriving Show -- | Path to boolector boolectorPath :: ConfigOption (BaseStringType Unicode) -boolectorPath = configOption knownRepr "boolector_path" +boolectorPath = configOption knownRepr "solver.boolector.path" + +boolectorPathOLD :: ConfigOption (BaseStringType Unicode) +boolectorPathOLD = configOption knownRepr "boolector_path" + +-- | Control strict parsing for Boolector solver responses (defaults +-- to solver.strict-parsing option setting). +boolectorStrictParsing :: ConfigOption BaseBoolType +boolectorStrictParsing = configOption knownRepr "solver.boolector.strict_parsing" boolectorOptions :: [ConfigDesc] boolectorOptions = - [ mkOpt - boolectorPath - executablePathOptSty - (Just "Path to boolector executable") - (Just (ConcreteString "boolector")) - ] + let bpOpt co = mkOpt + co + executablePathOptSty + (Just "Path to boolector executable") + (Just (ConcreteString "boolector")) + bp = bpOpt boolectorPath + bp2 = deprecatedOpt [bp] $ bpOpt boolectorPathOLD + in [ bp, bp2 + , copyOpt (const $ configOptionText boolectorStrictParsing) strictSMTParseOpt + ] <> SMT2.smtlib2Options boolectorAdapter :: SolverAdapter st boolectorAdapter = @@ -68,6 +79,7 @@ boolectorAdapter = , solver_adapter_check_sat = runBoolectorInOverride , solver_adapter_write_smt2 = SMT2.writeDefaultSMT2 () "Boolector" defaultWriteSMTLIB2Features + (Just boolectorStrictParsing) } instance SMT2.SMTLib2Tweaks Boolector where @@ -80,7 +92,8 @@ runBoolectorInOverride :: (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a runBoolectorInOverride = - SMT2.runSolverInOverride Boolector SMT2.nullAcknowledgementAction boolectorFeatures + SMT2.runSolverInOverride Boolector SMT2.nullAcknowledgementAction + boolectorFeatures (Just boolectorStrictParsing) -- | Run Boolector in a session. Boolector will be configured to produce models, but -- otherwise left with the default configuration. @@ -92,7 +105,8 @@ withBoolector -> (SMT2.Session t Boolector -> IO a) -- ^ Action to run -> IO a -withBoolector = SMT2.withSolver Boolector SMT2.nullAcknowledgementAction boolectorFeatures +withBoolector = SMT2.withSolver Boolector SMT2.nullAcknowledgementAction + boolectorFeatures (Just boolectorStrictParsing) boolectorFeatures :: ProblemFeatures @@ -120,5 +134,7 @@ setInteractiveLogicAndOptions writer = do SMT2.setLogic writer SMT2.allSupported instance OnlineSolver (SMT2.Writer Boolector) where - startSolverProcess = SMT2.startSolver Boolector SMT2.smtAckResult setInteractiveLogicAndOptions + startSolverProcess feat = SMT2.startSolver Boolector SMT2.smtAckResult + setInteractiveLogicAndOptions feat + (Just boolectorStrictParsing) shutdownSolverProcess = SMT2.shutdownSolver Boolector diff --git a/what4/src/What4/Solver/CVC4.hs b/what4/src/What4/Solver/CVC4.hs index 39ffa95b..059215f9 100644 --- a/what4/src/What4/Solver/CVC4.hs +++ b/what4/src/What4/Solver/CVC4.hs @@ -35,18 +35,20 @@ import System.IO import qualified System.IO.Streams as Streams import What4.BaseTypes -import What4.Config -import What4.Solver.Adapter import What4.Concrete -import What4.Interface -import What4.ProblemFeatures -import What4.SatResult +import What4.Config import What4.Expr.Builder import What4.Expr.GroundEval +import What4.Interface +import What4.ProblemFeatures import What4.Protocol.Online import qualified What4.Protocol.SMTLib2 as SMT2 +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) +import qualified What4.Protocol.SMTLib2.Response as RSP import qualified What4.Protocol.SMTLib2.Syntax as Syntax import What4.Protocol.SMTWriter +import What4.SatResult +import What4.Solver.Adapter import What4.Utils.Process @@ -58,27 +60,49 @@ data CVC4 = CVC4 deriving Show -- | Path to cvc4 cvc4Path :: ConfigOption (BaseStringType Unicode) -cvc4Path = configOption knownRepr "cvc4_path" +cvc4Path = configOption knownRepr "solver.cvc4.path" + +cvc4PathOLD :: ConfigOption (BaseStringType Unicode) +cvc4PathOLD = configOption knownRepr "cvc4_path" cvc4RandomSeed :: ConfigOption BaseIntegerType -cvc4RandomSeed = configOption knownRepr "cvc4.random-seed" +cvc4RandomSeed = configOption knownRepr "solver.cvc4.random-seed" + +cvc4RandomSeedOLD :: ConfigOption BaseIntegerType +cvc4RandomSeedOLD = configOption knownRepr "cvc4.random-seed" -- | Per-check timeout, in milliseconds (zero is none) cvc4Timeout :: ConfigOption BaseIntegerType -cvc4Timeout = configOption knownRepr "cvc4_timeout" +cvc4Timeout = configOption knownRepr "solver.cvc4.timeout" + +cvc4TimeoutOLD :: ConfigOption BaseIntegerType +cvc4TimeoutOLD = configOption knownRepr "cvc4_timeout" + +-- | Control strict parsing for Boolector solver responses (defaults +-- to solver.strict-parsing option setting). +cvc4StrictParsing :: ConfigOption BaseBoolType +cvc4StrictParsing = configOption knownRepr "solver.cvc4.strict_parsing" cvc4Options :: [ConfigDesc] cvc4Options = - [ mkOpt cvc4Path - executablePathOptSty - (Just "Path to CVC4 executable") - (Just (ConcreteString "cvc4")) - , intWithRangeOpt cvc4RandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1) - , mkOpt cvc4Timeout - integerOptSty - (Just "Per-check timeout in milliseconds (zero is none)") - (Just (ConcreteInteger 0)) - ] + let pathOpt co = mkOpt co + executablePathOptSty + (Just "Path to CVC4 executable") + (Just (ConcreteString "cvc4")) + p1 = pathOpt cvc4Path + r1 = intWithRangeOpt cvc4RandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1) + tmOpt co = mkOpt co + integerOptSty + (Just "Per-check timeout in milliseconds (zero is none)") + (Just (ConcreteInteger 0)) + t1 = tmOpt cvc4Timeout + in [ p1, r1, t1 + , copyOpt (const $ configOptionText cvc4StrictParsing) strictSMTParseOpt + , deprecatedOpt [p1] $ pathOpt cvc4PathOLD + , deprecatedOpt [r1] $ intWithRangeOpt cvc4RandomSeedOLD + (negate (2^(30::Int)-1)) (2^(30::Int)-1) + , deprecatedOpt [t1] $ tmOpt cvc4TimeoutOLD + ] <> SMT2.smtlib2Options cvc4Adapter :: SolverAdapter st cvc4Adapter = @@ -130,7 +154,11 @@ writeMultiAsmpCVC4SMT2File sym h ps = do bindings <- getSymbolVarBimap sym out_str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h in_str <- Streams.nullInput - c <- SMT2.newWriter CVC4 out_str in_str nullAcknowledgementAction "CVC4" + let cfg = getConfiguration sym + strictness <- maybe Strict + (\c -> if fromConcreteBool c then Strict else Lenient) <$> + (getOption =<< getOptionSetting RSP.strictSMTParsing cfg) + c <- SMT2.newWriter CVC4 out_str in_str nullAcknowledgementAction strictness "CVC4" True cvc4Features True bindings SMT2.setLogic c SMT2.allSupported SMT2.setProduceModels c True @@ -174,7 +202,8 @@ runCVC4InOverride -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a -runCVC4InOverride = SMT2.runSolverInOverride CVC4 nullAcknowledgementAction (SMT2.defaultFeatures CVC4) +runCVC4InOverride = SMT2.runSolverInOverride CVC4 nullAcknowledgementAction + (SMT2.defaultFeatures CVC4) (Just cvc4StrictParsing) -- | Run CVC4 in a session. CVC4 will be configured to produce models, but -- otherwise left with the default configuration. @@ -186,7 +215,8 @@ withCVC4 -> (SMT2.Session t CVC4 -> IO a) -- ^ Action to run -> IO a -withCVC4 = SMT2.withSolver CVC4 nullAcknowledgementAction (SMT2.defaultFeatures CVC4) +withCVC4 = SMT2.withSolver CVC4 nullAcknowledgementAction + (SMT2.defaultFeatures CVC4) (Just cvc4StrictParsing) setInteractiveLogicAndOptions :: SMT2.SMTLib2Tweaks a => @@ -207,7 +237,8 @@ setInteractiveLogicAndOptions writer = do instance OnlineSolver (SMT2.Writer CVC4) where startSolverProcess feat mbIOh sym = do - sp <- SMT2.startSolver CVC4 SMT2.smtAckResult setInteractiveLogicAndOptions feat mbIOh sym + sp <- SMT2.startSolver CVC4 SMT2.smtAckResult setInteractiveLogicAndOptions + feat (Just cvc4StrictParsing) mbIOh sym timeout <- SolverGoalTimeout <$> (getOpt =<< getOptionSetting cvc4Timeout (getConfiguration sym)) return $ sp { solverGoalTimeout = timeout } diff --git a/what4/src/What4/Solver/DReal.hs b/what4/src/What4/Solver/DReal.hs index 31da1ffa..22f326c9 100644 --- a/what4/src/What4/Solver/DReal.hs +++ b/what4/src/What4/Solver/DReal.hs @@ -56,6 +56,7 @@ import What4.SatResult import What4.Expr.Builder import What4.Expr.GroundEval import qualified What4.Protocol.SMTLib2 as SMT2 +import qualified What4.Protocol.SMTLib2.Response as RSP import qualified What4.Protocol.SMTWriter as SMTWriter import What4.Utils.Process import What4.Utils.Streams (logErrorStream) @@ -65,16 +66,21 @@ data DReal = DReal deriving Show -- | Path to dReal drealPath :: ConfigOption (BaseStringType Unicode) -drealPath = configOption knownRepr "dreal_path" +drealPath = configOption knownRepr "solver.dreal.path" + +drealPathOLD :: ConfigOption (BaseStringType Unicode) +drealPathOLD = configOption knownRepr "dreal_path" drealOptions :: [ConfigDesc] drealOptions = - [ mkOpt - drealPath - executablePathOptSty - (Just "Path to dReal executable") - (Just (ConcreteString "dreal")) - ] + let dpOpt co = mkOpt co + executablePathOptSty + (Just "Path to dReal executable") + (Just (ConcreteString "dreal")) + dp = dpOpt drealPath + in [ dp + , deprecatedOpt [dp] $ dpOpt drealPathOLD + ] <> SMT2.smtlib2Options drealAdapter :: SolverAdapter st drealAdapter = @@ -106,7 +112,13 @@ writeDRealSMT2File sym h ps = do bindings <- getSymbolVarBimap sym out_str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h in_str <- Streams.nullInput - c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction "dReal" + let cfg = getConfiguration sym + strictness <- maybe SMTWriter.Strict + (\c -> if fromConcreteBool c + then SMTWriter.Strict + else SMTWriter.Lenient) <$> + (getOption =<< getOptionSetting RSP.strictSMTParsing cfg) + c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction strictness "dReal" False useComputableReals False bindings SMT2.setProduceModels c True SMT2.setLogic c (SMT2.Logic "QF_NRA") @@ -299,7 +311,14 @@ runDRealInOverride sym logData ps modelFn = do in_str <- Streams.nullInput - c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction "dReal" + let cfg = getConfiguration sym + strictness <- maybe SMTWriter.Strict + (\c -> if fromConcreteBool c + then SMTWriter.Strict + else SMTWriter.Lenient) <$> + (getOption =<< getOptionSetting RSP.strictSMTParsing cfg) + + c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction strictness "dReal" False useComputableReals False bindings -- Set the dReal default logic diff --git a/what4/src/What4/Solver/ExternalABC.hs b/what4/src/What4/Solver/ExternalABC.hs index f86bcf94..5f389a78 100644 --- a/what4/src/What4/Solver/ExternalABC.hs +++ b/what4/src/What4/Solver/ExternalABC.hs @@ -35,6 +35,7 @@ import What4.Expr.GroundEval import What4.Interface import What4.ProblemFeatures import qualified What4.Protocol.SMTLib2 as SMT2 +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) import What4.Protocol.SMTWriter import What4.SatResult import What4.Solver.Adapter @@ -44,16 +45,27 @@ data ExternalABC = ExternalABC deriving Show -- | Path to ABC abcPath :: ConfigOption (BaseStringType Unicode) -abcPath = configOption knownRepr "abc_path" +abcPath = configOption knownRepr "solver.abc.path" + +abcPathOLD :: ConfigOption (BaseStringType Unicode) +abcPathOLD = configOption knownRepr "abc_path" + +-- | Control strict parsing for ABC solver responses (defaults +-- to solver.strict-parsing option setting). +abcStrictParsing :: ConfigOption BaseBoolType +abcStrictParsing = configOption knownRepr "solver.abc.strict_parsing" abcOptions :: [ConfigDesc] abcOptions = - [ mkOpt - abcPath - executablePathOptSty - (Just "ABC executable path") - (Just (ConcreteString "abc")) - ] + let optPath co = mkOpt co + executablePathOptSty + (Just "ABC executable path") + (Just (ConcreteString "abc")) + p = optPath abcPath + in [ p + , copyOpt (const $ configOptionText abcStrictParsing) strictSMTParseOpt + , deprecatedOpt [p] $ optPath abcPathOLD + ] <> SMT2.smtlib2Options externalABCAdapter :: SolverAdapter st externalABCAdapter = @@ -95,6 +107,7 @@ writeABCSMT2File -> [BoolExpr t] -> IO () writeABCSMT2File = SMT2.writeDefaultSMT2 ExternalABC "ABC" abcFeatures + (Just abcStrictParsing) instance SMT2.SMTLib2GenericSolver ExternalABC where defaultSolverPath _ = findSolverPath abcPath . getConfiguration @@ -114,3 +127,4 @@ runExternalABCInOverride -> IO a runExternalABCInOverride = SMT2.runSolverInOverride ExternalABC nullAcknowledgementAction abcFeatures + (Just abcStrictParsing) diff --git a/what4/src/What4/Solver/STP.hs b/what4/src/What4/Solver/STP.hs index c8c2d1bd..2226c04a 100644 --- a/what4/src/What4/Solver/STP.hs +++ b/what4/src/What4/Solver/STP.hs @@ -25,26 +25,38 @@ module What4.Solver.STP import Data.Bits import What4.BaseTypes -import What4.Config import What4.Concrete -import What4.Interface -import What4.ProblemFeatures -import What4.SatResult +import What4.Config import What4.Expr.Builder import What4.Expr.GroundEval -import What4.Solver.Adapter +import What4.Interface +import What4.ProblemFeatures import What4.Protocol.Online import qualified What4.Protocol.SMTLib2 as SMT2 +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) +import What4.SatResult +import What4.Solver.Adapter import What4.Utils.Process data STP = STP deriving Show -- | Path to stp stpPath :: ConfigOption (BaseStringType Unicode) -stpPath = configOption knownRepr "stp_path" +stpPath = configOption knownRepr "solver.stp.path" + +stpPathOLD :: ConfigOption (BaseStringType Unicode) +stpPathOLD = configOption knownRepr "stp_path" stpRandomSeed :: ConfigOption BaseIntegerType -stpRandomSeed = configOption knownRepr "stp.random-seed" +stpRandomSeed = configOption knownRepr "solver.stp.random-seed" + +stpRandomSeedOLD :: ConfigOption BaseIntegerType +stpRandomSeedOLD = configOption knownRepr "stp.random-seed" + +-- | Control strict parsing for Boolector solver responses (defaults +-- to solver.strict-parsing option setting). +stpStrictParsing :: ConfigOption BaseBoolType +stpStrictParsing = configOption knownRepr "solver.stp.strict_parsing" intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc intWithRangeOpt nm lo hi = mkOpt nm sty Nothing Nothing @@ -52,12 +64,19 @@ intWithRangeOpt nm lo hi = mkOpt nm sty Nothing Nothing stpOptions :: [ConfigDesc] stpOptions = - [ mkOpt stpPath - executablePathOptSty - (Just "Path to STP executable.") - (Just (ConcreteString "stp")) - , intWithRangeOpt stpRandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1) - ] + let mkPath co = mkOpt co + executablePathOptSty + (Just "Path to STP executable.") + (Just (ConcreteString "stp")) + p1 = mkPath stpPath + randbitval = 2^(30 :: Int)-1 + r1 = intWithRangeOpt stpRandomSeed (negate randbitval) randbitval + in [ p1, r1 + , copyOpt (const $ configOptionText stpStrictParsing) strictSMTParseOpt + , deprecatedOpt [p1] $ mkPath stpPathOLD + , deprecatedOpt [r1] $ intWithRangeOpt stpRandomSeedOLD + (negate randbitval) randbitval + ] <> SMT2.smtlib2Options stpAdapter :: SolverAdapter st stpAdapter = @@ -67,6 +86,7 @@ stpAdapter = , solver_adapter_check_sat = runSTPInOverride , solver_adapter_write_smt2 = SMT2.writeDefaultSMT2 STP "STP" defaultWriteSMTLIB2Features + (Just stpStrictParsing) } instance SMT2.SMTLib2Tweaks STP where @@ -83,9 +103,6 @@ instance SMT2.SMTLib2GenericSolver STP where SMT2.setProduceModels writer True SMT2.setLogic writer SMT2.qf_bv - newDefaultWriter solver ack feats sym h in_h = - SMT2.newWriter solver h in_h ack (show solver) True feats False - =<< getSymbolVarBimap sym stpFeatures :: ProblemFeatures stpFeatures = useIntegerArithmetic .|. useBitvectors @@ -96,7 +113,8 @@ runSTPInOverride -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a -runSTPInOverride = SMT2.runSolverInOverride STP SMT2.nullAcknowledgementAction (SMT2.defaultFeatures STP) +runSTPInOverride = SMT2.runSolverInOverride STP SMT2.nullAcknowledgementAction + (SMT2.defaultFeatures STP) (Just stpStrictParsing) -- | Run STP in a session. STP will be configured to produce models, buth -- otherwise left with the default configuration. @@ -108,7 +126,8 @@ withSTP -> (SMT2.Session t STP -> IO a) -- ^ Action to run -> IO a -withSTP = SMT2.withSolver STP SMT2.nullAcknowledgementAction (SMT2.defaultFeatures STP) +withSTP = SMT2.withSolver STP SMT2.nullAcknowledgementAction + (SMT2.defaultFeatures STP) (Just stpStrictParsing) setInteractiveLogicAndOptions :: SMT2.SMTLib2Tweaks a => @@ -125,5 +144,7 @@ setInteractiveLogicAndOptions writer = do -- SMT2.setOption writer "global-declarations" "true" instance OnlineSolver (SMT2.Writer STP) where - startSolverProcess = SMT2.startSolver STP SMT2.smtAckResult setInteractiveLogicAndOptions + startSolverProcess feat = SMT2.startSolver STP SMT2.smtAckResult + setInteractiveLogicAndOptions feat + (Just stpStrictParsing) shutdownSolverProcess = SMT2.shutdownSolver STP diff --git a/what4/src/What4/Solver/Yices.hs b/what4/src/What4/Solver/Yices.hs index 8e42d856..d0c101d6 100644 --- a/what4/src/What4/Solver/Yices.hs +++ b/what4/src/What4/Solver/Yices.hs @@ -64,7 +64,7 @@ module What4.Solver.Yices ) where #if !MIN_VERSION_base(4,13,0) -import Control.Monad.Fail( MonadFail ) +import Control.Monad.Fail ( MonadFail ) #endif import Control.Applicative @@ -102,25 +102,26 @@ import qualified System.IO.Streams.Attoparsec.Text as Streams import qualified Prettyprinter as PP import What4.BaseTypes -import What4.Config -import What4.Solver.Adapter import What4.Concrete -import What4.Interface -import What4.ProblemFeatures -import What4.SatResult +import What4.Config import qualified What4.Expr.Builder as B import What4.Expr.GroundEval import What4.Expr.VarIdentification -import What4.Protocol.SExp -import What4.Protocol.SMTLib2 (writeDefaultSMT2) -import What4.Protocol.SMTWriter as SMTWriter +import What4.Interface +import What4.ProblemFeatures import What4.Protocol.Online import qualified What4.Protocol.PolyRoot as Root +import What4.Protocol.SExp +import What4.Protocol.SMTLib2 (writeDefaultSMT2) +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) +import What4.Protocol.SMTWriter as SMTWriter +import What4.SatResult +import What4.Solver.Adapter import What4.Utils.HandleReader import What4.Utils.Process -import Prelude -import GHC.Stack +import Prelude +import GHC.Stack -- | This is a tag used to indicate that a 'WriterConn' is a connection -- to a specific Yices process. @@ -451,7 +452,7 @@ newConnection stream in_stream ack reqFeatures timeout bindings = do , yicesTimeout = timeout , yicesUnitDeclared = unitRef } - conn <- newWriterConn stream in_stream (ack earlyUnsatRef) nm features' bindings c + conn <- newWriterConn stream in_stream (ack earlyUnsatRef) nm Strict features' bindings c return $! conn { supportFunctionDefs = True , supportFunctionArguments = True , supportQuantifiers = efSolver @@ -561,7 +562,7 @@ instance SMTReadWriter Connection where smtSatResult _ = getSatResponse smtUnsatAssumptionsResult _ s = - do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) s) + do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) (connInputHandle s)) let cmd = safeCmd "(show-unsat-assumptions)" case mb of Right (asNegAtomList -> Just as) -> return as @@ -573,7 +574,7 @@ instance SMTReadWriter Connection where ] smtUnsatCoreResult _ s = - do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) s) + do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) (connInputHandle s)) let cmd = safeCmd "(show-unsat-core)" case mb of Right (asAtomList -> Just nms) -> return nms @@ -693,10 +694,8 @@ yicesStartSolver features auxOutput sym = do -- FIXME return $! SolverProcess { solverConn = conn , solverCleanupCallback = cleanupProcess hdls - , solverStdin = in_stream' , solverStderr = err_reader , solverHandle = ph - , solverResponse = out_stream , solverErrorBehavior = ContinueOnError , solverEvalFuns = smtEvalFuns conn out_stream , solverLogFn = logSolverEvent sym @@ -764,9 +763,9 @@ getAckResponse resps = -- | Get the sat result from a previous SAT command. -- Throws an exception if something goes wrong. -getSatResponse :: Streams.InputStream Text -> IO (SatResult () ()) -getSatResponse resps = - do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) resps) +getSatResponse :: WriterConn t Connection -> IO (SatResult () ()) +getSatResponse conn = + do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) (connInputHandle conn)) case mb of Right (SAtom "unsat") -> return (Unsat ()) Right (SAtom "sat") -> return (Sat ()) @@ -905,49 +904,72 @@ yicesAdapter = runYicesInOverride sym logData ps (cont . runIdentity . traverseSatResult (\x -> pure (x,Nothing)) pure) , solver_adapter_write_smt2 = - writeDefaultSMT2 () "YICES" yicesSMT2Features + writeDefaultSMT2 () "YICES" yicesSMT2Features (Just yicesStrictParsing) } -- | Path to yices yicesPath :: ConfigOption (BaseStringType Unicode) -yicesPath = configOption knownRepr "yices_path" +yicesPath = configOption knownRepr "solver.yices.path" + +yicesPathOLD :: ConfigOption (BaseStringType Unicode) +yicesPathOLD = configOption knownRepr "yices_path" -- | Enable the MC-SAT solver yicesEnableMCSat :: ConfigOption BaseBoolType -yicesEnableMCSat = configOption knownRepr "yices_enable-mcsat" +yicesEnableMCSat = configOption knownRepr "solver.yices.enable-mcsat" + +yicesEnableMCSatOLD :: ConfigOption BaseBoolType +yicesEnableMCSatOLD = configOption knownRepr "yices_enable-mcsat" -- | Enable interactive mode (necessary for per-goal timeouts) yicesEnableInteractive :: ConfigOption BaseBoolType -yicesEnableInteractive = configOption knownRepr "yices_enable-interactive" +yicesEnableInteractive = configOption knownRepr "solver.yices.enable-interactive" + +yicesEnableInteractiveOLD :: ConfigOption BaseBoolType +yicesEnableInteractiveOLD = configOption knownRepr "yices_enable-interactive" -- | Set a per-goal timeout in seconds. yicesGoalTimeout :: ConfigOption BaseIntegerType -yicesGoalTimeout = configOption knownRepr "yices_goal-timeout" +yicesGoalTimeout = configOption knownRepr "solver.yices.goal-timeout" + +yicesGoalTimeoutOLD :: ConfigOption BaseIntegerType +yicesGoalTimeoutOLD = configOption knownRepr "yices_goal-timeout" + +-- | Control strict parsing for Yices solver responses (defaults +-- to solver.strict-parsing option setting). +yicesStrictParsing :: ConfigOption BaseBoolType +yicesStrictParsing = configOption knownRepr "solver.yices.strict_parsing" yicesOptions :: [ConfigDesc] yicesOptions = - [ mkOpt - yicesPath - executablePathOptSty - (Just "Yices executable path") - (Just (ConcreteString "yices")) - , mkOpt - yicesEnableMCSat - boolOptSty - (Just "Enable the Yices MCSAT solving engine") - (Just (ConcreteBool False)) - , mkOpt - yicesEnableInteractive - boolOptSty - (Just "Enable Yices interactive mode (needed to support timeouts)") - (Just (ConcreteBool False)) - , mkOpt - yicesGoalTimeout - integerOptSty - (Just "Set a per-goal timeout") - (Just (ConcreteInteger 0)) - ] - ++ yicesInternalOptions + let mkPath co = mkOpt co + executablePathOptSty + (Just "Yices executable path") + (Just (ConcreteString "yices")) + mkMCSat co = mkOpt co + boolOptSty + (Just "Enable the Yices MCSAT solving engine") + (Just (ConcreteBool False)) + mkIntr co = mkOpt co + boolOptSty + (Just "Enable Yices interactive mode (needed to support timeouts)") + (Just (ConcreteBool False)) + mkTmout co = mkOpt co + integerOptSty + (Just "Set a per-goal timeout") + (Just (ConcreteInteger 0)) + p = mkPath yicesPath + m = mkMCSat yicesEnableMCSat + i = mkIntr yicesEnableInteractive + t = mkTmout yicesGoalTimeout + in [ p, m, i, t + , copyOpt (const $ configOptionText yicesStrictParsing) strictSMTParseOpt + , deprecatedOpt [p] $ mkPath yicesPathOLD + , deprecatedOpt [m] $ mkMCSat yicesEnableMCSatOLD + , deprecatedOpt [i] $ mkIntr yicesEnableInteractiveOLD + , deprecatedOpt [t] $ mkTmout yicesGoalTimeoutOLD + ] + ++ yicesInternalOptions yicesBranchingChoices :: Set Text yicesBranchingChoices = Set.fromList @@ -967,8 +989,12 @@ yicesEFGenModes = Set.fromList , "projection" ] -booleanOpt :: String -> ConfigDesc -booleanOpt nm = booleanOpt' (configOption BaseBoolRepr ("yices."++nm)) +booleanOpt :: String -> [ConfigDesc] +booleanOpt nm = + let b = booleanOpt' (configOption BaseBoolRepr ("solver.yices."++nm)) + in [ b + , deprecatedOpt [b] $ booleanOpt' (configOption BaseBoolRepr ("yices."++nm)) + ] booleanOpt' :: ConfigOption BaseBoolType -> ConfigDesc booleanOpt' o = @@ -977,36 +1003,52 @@ booleanOpt' o = Nothing Nothing -floatWithRangeOpt :: String -> Rational -> Rational -> ConfigDesc +floatWithRangeOpt :: String -> Rational -> Rational -> [ConfigDesc] floatWithRangeOpt nm lo hi = - mkOpt (configOption BaseRealRepr $ "yices."++nm) - (realWithRangeOptSty (Inclusive lo) (Inclusive hi)) - Nothing - Nothing + let mkO n = mkOpt (configOption BaseRealRepr $ n++nm) + (realWithRangeOptSty (Inclusive lo) (Inclusive hi)) + Nothing + Nothing + f = mkO "solver.yices." + in [ f + , deprecatedOpt [f] $ mkO "yices." + ] -floatWithMinOpt :: String -> Bound Rational -> ConfigDesc +floatWithMinOpt :: String -> Bound Rational -> [ConfigDesc] floatWithMinOpt nm lo = - mkOpt (configOption BaseRealRepr $ "yices."++nm) - (realWithMinOptSty lo) - Nothing - Nothing + let mkO n = mkOpt (configOption BaseRealRepr $ n++nm) + (realWithMinOptSty lo) + Nothing + Nothing + f = mkO "solver.yices." + in [ f + , deprecatedOpt [f] $ mkO "yices." + ] -intWithRangeOpt :: String -> Integer -> Integer -> ConfigDesc +intWithRangeOpt :: String -> Integer -> Integer -> [ConfigDesc] intWithRangeOpt nm lo hi = - mkOpt (configOption BaseIntegerRepr $ "yices."++nm) - (integerWithRangeOptSty (Inclusive lo) (Inclusive hi)) - Nothing - Nothing + let mkO n = mkOpt (configOption BaseIntegerRepr $ n++nm) + (integerWithRangeOptSty (Inclusive lo) (Inclusive hi)) + Nothing + Nothing + i = mkO "solver.yices." + in [ i + , deprecatedOpt [i] $ mkO "yices." + ] -enumOpt :: String -> Set Text -> ConfigDesc +enumOpt :: String -> Set Text -> [ConfigDesc] enumOpt nm xs = - mkOpt (configOption (BaseStringRepr UnicodeRepr) $ "yices."++nm) - (enumOptSty xs) - Nothing - Nothing + let mkO n = mkOpt (configOption (BaseStringRepr UnicodeRepr) $ n++nm) + (enumOptSty xs) + Nothing + Nothing + e = mkO "solver.yices." + in [ e + , deprecatedOpt [e] $ mkO "yices." + ] yicesInternalOptions :: [ConfigDesc] -yicesInternalOptions = +yicesInternalOptions = concat [ booleanOpt "var-elim" , booleanOpt "arith-elim" , booleanOpt "flatten" @@ -1155,8 +1197,6 @@ runYicesInOverride sym logData conditions resultFn = do let yp = SolverProcess { solverConn = c , solverCleanupCallback = cleanupProcess hdls , solverHandle = ph - , solverStdin = in_stream - , solverResponse = out_stream , solverErrorBehavior = ImmediateExit , solverStderr = err_reader , solverEvalFuns = smtEvalFuns c out_stream diff --git a/what4/src/What4/Solver/Z3.hs b/what4/src/What4/Solver/Z3.hs index d6b86b0e..a30722e8 100644 --- a/what4/src/What4/Solver/Z3.hs +++ b/what4/src/What4/Solver/Z3.hs @@ -41,6 +41,7 @@ import What4.Interface import What4.ProblemFeatures import What4.Protocol.Online import qualified What4.Protocol.SMTLib2 as SMT2 +import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) import qualified What4.Protocol.SMTLib2.Syntax as SMT2Syntax import What4.Protocol.SMTWriter import What4.SatResult @@ -51,25 +52,41 @@ data Z3 = Z3 deriving Show -- | Path to Z3 z3Path :: ConfigOption (BaseStringType Unicode) -z3Path = configOption knownRepr "z3_path" +z3Path = configOption knownRepr "solver.z3.path" + +z3PathOLD :: ConfigOption (BaseStringType Unicode) +z3PathOLD = configOption knownRepr "z3_path" -- | Per-check timeout, in milliseconds (zero is none) z3Timeout :: ConfigOption BaseIntegerType -z3Timeout = configOption knownRepr "z3_timeout" +z3Timeout = configOption knownRepr "solver.z3.timeout" + +z3TimeoutOLD :: ConfigOption BaseIntegerType +z3TimeoutOLD = configOption knownRepr "z3_timeout" + +-- | Strict parsing specifically for Z3 interaction? If set, +-- overrides solver.strict_parsing, otherwise defaults to +-- solver.strict_parsing. +z3StrictParsing :: ConfigOption BaseBoolType +z3StrictParsing = configOption knownRepr "solver.z3.strict_parsing" z3Options :: [ConfigDesc] z3Options = - [ mkOpt - z3Path - executablePathOptSty - (Just "Z3 executable path") - (Just (ConcreteString "z3")) - , mkOpt - z3Timeout - integerOptSty - (Just "Per-check timeout in milliseconds (zero is none)") - (Just (ConcreteInteger 0)) - ] + let mkPath co = mkOpt co + executablePathOptSty + (Just "Z3 executable path") + (Just (ConcreteString "z3")) + mkTmo co = mkOpt co + integerOptSty + (Just "Per-check timeout in milliseconds (zero is none)") + (Just (ConcreteInteger 0)) + p = mkPath z3Path + t = mkTmo z3Timeout + in [ p, t + , copyOpt (const $ configOptionText z3StrictParsing) strictSMTParseOpt + , deprecatedOpt [p] $ mkPath z3PathOLD + , deprecatedOpt [t] $ mkTmo z3TimeoutOLD + ] <> SMT2.smtlib2Options z3Adapter :: SolverAdapter st z3Adapter = @@ -128,7 +145,7 @@ writeZ3SMT2File -> Handle -> [BoolExpr t] -> IO () -writeZ3SMT2File = SMT2.writeDefaultSMT2 Z3 "Z3" z3Features +writeZ3SMT2File = SMT2.writeDefaultSMT2 Z3 "Z3" z3Features (Just z3StrictParsing) instance SMT2.SMTLib2GenericSolver Z3 where defaultSolverPath _ = findSolverPath z3Path . getConfiguration @@ -162,7 +179,8 @@ runZ3InOverride -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a -runZ3InOverride = SMT2.runSolverInOverride Z3 nullAcknowledgementAction z3Features +runZ3InOverride = SMT2.runSolverInOverride Z3 nullAcknowledgementAction + z3Features (Just z3StrictParsing) -- | Run Z3 in a session. Z3 will be configured to produce models, but -- otherwise left with the default configuration. @@ -174,7 +192,8 @@ withZ3 -> (SMT2.Session t Z3 -> IO a) -- ^ Action to run -> IO a -withZ3 = SMT2.withSolver Z3 nullAcknowledgementAction z3Features +withZ3 = SMT2.withSolver Z3 nullAcknowledgementAction + z3Features (Just z3StrictParsing) setInteractiveLogicAndOptions :: @@ -196,7 +215,8 @@ setInteractiveLogicAndOptions writer = do instance OnlineSolver (SMT2.Writer Z3) where startSolverProcess feat mbIOh sym = do - sp <- SMT2.startSolver Z3 SMT2.smtAckResult setInteractiveLogicAndOptions feat mbIOh sym + sp <- SMT2.startSolver Z3 SMT2.smtAckResult setInteractiveLogicAndOptions feat + (Just z3StrictParsing) mbIOh sym timeout <- SolverGoalTimeout <$> (getOpt =<< getOptionSetting z3Timeout (getConfiguration sym)) return $ sp { solverGoalTimeout = timeout } diff --git a/what4/test/AdapterTest.hs b/what4/test/AdapterTest.hs index ceabbbf6..c56f55f6 100644 --- a/what4/test/AdapterTest.hs +++ b/what4/test/AdapterTest.hs @@ -12,26 +12,31 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} -import Control.Exception ( displayException, try, SomeException ) -import Control.Lens (folded) -import Control.Monad ( forM, unless, void ) -import Control.Monad.Except ( runExceptT ) -import Data.BitVector.Sized ( mkBV ) -import Data.Char ( toLower ) -import System.Exit ( ExitCode(..) ) -import System.Process ( readProcessWithExitCode ) +import Control.Exception ( displayException, try, SomeException(..), fromException ) +import Control.Lens (folded) +import Control.Monad ( forM, unless, void ) +import Control.Monad.Except ( runExceptT ) +import Data.BitVector.Sized ( mkBV ) +import Data.Char ( toLower ) +import qualified Data.List as L +import Data.Text ( pack ) +import System.Exit ( ExitCode(..) ) +import System.Process ( readProcessWithExitCode ) -import Test.Tasty -import Test.Tasty.HUnit +import Test.Tasty +import Test.Tasty.HUnit -import Data.Parameterized.Nonce -import Data.Parameterized.Some +import Data.Parameterized.Nonce +import Data.Parameterized.Some -import What4.Config -import What4.Interface -import What4.Expr -import What4.Solver -import What4.Protocol.VerilogWriter +import qualified What4.BaseTypes as BT +import What4.Config +import What4.Expr +import What4.Interface +import What4.Protocol.SMTLib2.Response ( strictSMTParsing ) +import What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness(..) ) +import What4.Protocol.VerilogWriter +import What4.Solver data State t = State @@ -69,6 +74,459 @@ mkSmokeTest adpt = testCase (solver_adapter_name adpt) $ Nothing -> return () Just ex -> fail $ displayException ex + +---------------------------------------------------------------------- + +mkConfigTests :: [SolverAdapter State] -> [TestTree] +mkConfigTests adapters = + [ + testGroup "deprecated configs" (deprecatedConfigTests adapters) + , testGroup "strict parsing config" (strictParseConfigTests adapters) + ] + where + wantOptSetFailure withText res = case res of + Right r -> + assertFailure ("Expected '" <> withText <> + "' but completed successfully with: " <> show r) + Left err -> + case fromException err of + Just (e :: OptSetFailure) -> + withText `L.isInfixOf` (show e) @? + ("Expected '" <> withText <> "' exception error but got: " <> + show e) + _ -> assertFailure $ + "Expected OptSetFailure exception but got: " <> show err + wantOptGetFailure withText res = case res of + Right r -> + assertFailure ("Expected '" <> withText <> + "' but completed successfully with: " <> show r) + Left err -> + case fromException err of + Just (e :: OptGetFailure) -> + withText `L.isInfixOf` (show e) @? + ("Expected '" <> withText <> "' exception error but got: " <> + show e) + _ -> assertFailure $ + "Expected OptGetFailure exception but got: " <> show err + withAdapters :: [SolverAdapter State] + -> (forall t . ExprBuilder t State (Flags FloatUninterpreted) -> IO a) + -> IO a + withAdapters adptrs op = do + (cfgs, _getDefAdapter) <- solverAdapterOptions adptrs + withIONonceGenerator $ \gen -> + do sym <- newExprBuilder FloatUninterpretedRepr State gen + extendConfig cfgs (getConfiguration sym) + op sym + + cmpUnderSomes :: Some OptionSetting -> Some OptionSetting -> IO () + cmpUnderSomes (Some setterX) (Some setterY) = + case testEquality + (configOptionType (optionSettingName setterX)) + (BaseStringRepr UnicodeRepr) of + Just Refl -> + case testEquality + (configOptionType (optionSettingName setterY)) + (BaseStringRepr UnicodeRepr) of + Just Refl -> do vX <- getMaybeOpt setterX + vY <- getMaybeOpt setterY + vX @=? vY + Nothing -> assertFailure "second some is not a unicode string" + Nothing -> assertFailure "first some is not a unicode string" + + cmpUnderSomesI :: Some OptionSetting -> Some OptionSetting -> IO () + cmpUnderSomesI (Some setterX) (Some setterY) = + case testEquality BaseIntegerRepr + (configOptionType (optionSettingName setterX)) of + Just Refl -> + case testEquality BaseIntegerRepr + (configOptionType (optionSettingName setterY)) of + Just Refl -> do vX <- getMaybeOpt setterX + vY <- getMaybeOpt setterY + vX @=? vY + Nothing -> assertFailure "second some is not an integer" + Nothing -> assertFailure "first some is not an integer" + + cmpUnderSome :: Some OptionSetting + -> OptionSetting (BaseStringType Unicode) -> IO () + cmpUnderSome (Some setterX) setterY = + case testEquality + (configOptionType (optionSettingName setterX)) + (BaseStringRepr UnicodeRepr) of + Just Refl -> do vX <- getMaybeOpt setterX + vY <- getMaybeOpt setterY + vX @=? vY + Nothing -> assertFailure "first some is not a unicode string" + + cmpUnderSomeI :: Some OptionSetting + -> OptionSetting BaseIntegerType -> IO () + cmpUnderSomeI (Some setterX) setterY = + case testEquality BaseIntegerRepr + (configOptionType (optionSettingName setterX)) of + Just Refl -> do vX <- getMaybeOpt setterX + vY <- getMaybeOpt setterY + vX @=? vY + Nothing -> assertFailure "first some is not an integer" + + cmpUnderSomeB :: Some OptionSetting + -> OptionSetting BaseBoolType -> IO () + cmpUnderSomeB (Some setterX) setterY = + case testEquality BaseBoolRepr + (configOptionType (optionSettingName setterX)) of + Just Refl -> do vX <- getMaybeOpt setterX + vY <- getMaybeOpt setterY + vX @=? vY + Nothing -> assertFailure "first some is not a boolean" + + strictParseConfigTests adaptrs = + let mkPCTest adaptr = + testGroup (solver_adapter_name adaptr) $ + let setCommonStrictness cfg v = do + setter <- getOptionSetting strictSMTParsing cfg + show <$> setOpt setter v >>= (@?= "[]") + setSpecificStrictness cfg v = do + setter <- getOptionSettingFromText (pack cfgName) cfg + show <$> setBoolOpt setter v >>= (@?= "[]") + cfgName = "solver." <> (toLower <$> (solver_adapter_name adaptr)) <> ".strict_parsing" + in [ + testCase "default val" $ + withAdapters adaptrs $ \sym -> do + let cfg = getConfiguration sym + strictOpt = Just $ configOption knownRepr cfgName + parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Strict) + + , testCase "common val" $ + withAdapters adaptrs $ \sym -> do + let cfg = getConfiguration sym + strictOpt = Just $ configOption knownRepr cfgName + setCommonStrictness cfg False + parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Lenient) + + , testCase "strict val" $ + withAdapters adaptrs $ \sym -> do + let cfg = getConfiguration sym + strictOpt = Just $ configOption knownRepr cfgName + setSpecificStrictness cfg False + parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Lenient) + + , testCase "strict overrides common val" $ + withAdapters adaptrs $ \sym -> do + let cfg = getConfiguration sym + strictOpt = Just $ configOption knownRepr cfgName + setCommonStrictness cfg False + setSpecificStrictness cfg True + parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Strict) + + ] + in fmap mkPCTest adaptrs + + deprecatedConfigTests adaptrs = + [ + + testCaseSteps "deprecated default_solver is equivalent to solver.default" $ + -- n.b. requires at least 2 entries in the adaptrs list + \step -> withAdapters adaptrs $ \sym -> do + step "Get OptionSetters, regular and deprecated, Text and ConfigOption" + settera <- getOptionSettingFromText "solver.default" + (getConfiguration sym) + setterb <- getOptionSettingFromText "default_solver" + (getConfiguration sym) + settera' <- getOptionSetting defaultSolverAdapter + (getConfiguration sym) + step "Get (same) initial value from regular and deprecated" + cmpUnderSomes settera setterb + step "Get (same) initial value from Text and ConfigOption identification" + cmpUnderSome settera settera' + v0 <- getMaybeOpt settera' + + step "Update the value via deprecated" + res1 <- try $ setUnicodeOpt setterb $ + pack $ solver_adapter_name $ last adaptrs + case res1 of + Right warns -> fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: default_solver (renamed to: solver.default)" + ] + Left (SomeException e) -> assertFailure $ show e + -- Get (same) updated value from regular and deprecated + cmpUnderSomes settera setterb + v1 <- getMaybeOpt settera' + (v0 /= v1) @? ("Update from " <> show v0 <> " failed for " <> + show (fmap solver_adapter_name adaptrs)) + + step "Update the value via regular (text identification)" + res2 <- try $ setUnicodeOpt settera $ + pack $ solver_adapter_name $ head adaptrs + case res2 of + Right warns -> fmap show warns @?= [] + Left (SomeException e) -> assertFailure $ show e + v2 <- getMaybeOpt settera' + v0 @=? v2 + + step "Update the value via regular (ConfigOption identification)" + res3 <- try $ setOpt settera' $ + pack $ solver_adapter_name $ last $ take 2 adaptrs + case res3 of + Right warns -> fmap show warns @?= [] + Left (SomeException e) -> assertFailure $ show e + v3 <- getMaybeOpt settera' + (v0 /= v3) @? ("Update from " <> show v0 <> " failed for " <> + show (fmap solver_adapter_name adaptrs)) + + step "Attempt invalid update via deprecated" + wantOptSetFailure "invalid setting" =<< + try (setUnicodeOpt setterb "foo") + v4 <- getMaybeOpt settera' + v3 @=? v4 + + step "Reset to original value" + res4 <- try $ setOpt settera' $ + pack $ solver_adapter_name $ head adaptrs + case res4 of + Right warns -> fmap show warns @?= [] + Left (SomeException e) -> assertFailure $ show e + v5 <- getMaybeOpt settera' + v0 @=? v5 + cmpUnderSome settera settera' + + , testCase "deprecated boolector_path is equivalent to solver.boolector.path" $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "boolector_path" + (getConfiguration sym) + setterb <- getOptionSetting boolectorPath + (getConfiguration sym) + cmpUnderSome settera setterb + res1 <- try $ setUnicodeOpt settera "/foo/bar" + case res1 of + Right warns -> fmap show warns @?= + [ "Could not find: /foo/bar" + , "DEPRECATED CONFIG OPTION USED: boolector_path (renamed to: solver.boolector.path)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSome settera setterb + + , testCase "deprecated cvc4_path is equivalent to solver.cvc4.path" $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "cvc4_path" + (getConfiguration sym) + setterb <- getOptionSetting cvc4Path + (getConfiguration sym) + cmpUnderSome settera setterb + res1 <- try $ setUnicodeOpt settera "/foo/bar" + case res1 of + Right warns -> fmap show warns @?= + [ "Could not find: /foo/bar" + , "DEPRECATED CONFIG OPTION USED: cvc4_path (renamed to: solver.cvc4.path)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSome settera setterb + + , testCase "deprecated cvc4_timeout is equivalent to solver.cvc4.timeout" $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "cvc4_timeout" + (getConfiguration sym) + setterb <- getOptionSetting cvc4Timeout + (getConfiguration sym) + cmpUnderSomeI settera setterb + res1 <- try $ setIntegerOpt settera 42 + case res1 of + Right warns -> fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: cvc4_timeout (renamed to: solver.cvc4.timeout)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSomeI settera setterb + + , testCase "deprecated stp.random-seed is equivalent to solver.stp.random-seed" $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "cvc4.random-seed" + (getConfiguration sym) + setterb <- getOptionSettingFromText "solver.cvc4.random-seed" + (getConfiguration sym) + cmpUnderSomesI settera setterb + res1 <- try $ setIntegerOpt settera 99 + case res1 of + Right warns -> fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: cvc4.random-seed (renamed to: solver.cvc4.random-seed)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSomesI settera setterb + + , testCase "deprecated dreal_path is equivalent to solver.dreal.path" $ + withAdapters adaptrs $ \sym -> do +#ifdef TEST_DREAL + settera <- getOptionSettingFromText "dreal_path" + (getConfiguration sym) + setterb <- getOptionSetting drealPath + (getConfiguration sym) + cmpUnderSome settera setterb + res1 <- try $ setUnicodeOpt settera "/foo/bar" + case res1 of + Right warns -> fmap show warns @?= + [ "Could not find: /foo/bar" + , "DEPRECATED CONFIG OPTION USED: dreal_path (renamed to: solver.dreal.path)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSome settera setterb +#else + settera <- try $ getOptionSettingFromText "dreal_path" + (getConfiguration sym) + wantOptGetFailure "not found" settera +#endif + + , testCase "deprecated abc_path is equivalent to solver.abc.path" $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "abc_path" + (getConfiguration sym) + setterb <- getOptionSetting abcPath + (getConfiguration sym) + cmpUnderSome settera setterb + res1 <- try $ setUnicodeOpt settera "/foo/bar" + case res1 of + Right warns -> fmap show warns @?= + [ "Could not find: /foo/bar" + , "DEPRECATED CONFIG OPTION USED: abc_path (renamed to: solver.abc.path)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSome settera setterb + + , testCase "deprecated stp_path is equivalent to solver.stp.path" $ + withAdapters adaptrs $ \sym -> do +#ifdef TEST_STP + settera <- getOptionSettingFromText "stp_path" + (getConfiguration sym) + setterb <- getOptionSetting stpPath + (getConfiguration sym) + cmpUnderSome settera setterb + res1 <- try $ setUnicodeOpt settera "/foo/bar" + case res1 of + Right warns -> fmap show warns @?= + [ "Could not find: /foo/bar" + , "DEPRECATED CONFIG OPTION USED: stp_path (renamed to: solver.stp.path)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSome settera setterb +#else + settera <- try $ getOptionSettingFromText "stp_path" + (getConfiguration sym) + wantOptGetFailure "not found" settera +#endif + + , testCase "deprecated stp.random-seed is equivalent to solver.stp.random-seed" $ + withAdapters adaptrs $ \sym -> do +#ifdef TEST_STP + settera <- getOptionSettingFromText "stp.random-seed" + (getConfiguration sym) + setterb <- getOptionSettingFromText "solver.stp.random-seed" + (getConfiguration sym) + cmpUnderSomesI settera setterb + res1 <- try $ setIntegerOpt settera 99 + case res1 of + Right warns -> fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: stp.random-seed (renamed to: solver.stp.random-seed)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSomesI settera setterb +#else + settera <- try $ getOptionSettingFromText "stp.random-seed" + (getConfiguration sym) + wantOptGetFailure "not found" settera +#endif + + , testCase "deprecated yices_path is equivalent to solver.yices.path" $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "yices_path" + (getConfiguration sym) + setterb <- getOptionSetting yicesPath + (getConfiguration sym) + cmpUnderSome settera setterb + res1 <- try $ setUnicodeOpt settera "/foo/bar" + case res1 of + Right warns -> fmap show warns @?= + [ "Could not find: /foo/bar" + , "DEPRECATED CONFIG OPTION USED: yices_path (renamed to: solver.yices.path)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSome settera setterb + + , testCase "deprecated yices_enable-interactive is equivalent to solver.yices.en.." $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "yices_enable-interactive" + (getConfiguration sym) + setterb <- getOptionSetting yicesEnableInteractive + (getConfiguration sym) + cmpUnderSomeB settera setterb + res1 <- try $ setBoolOpt settera True + case res1 of + Right warns -> fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: yices_enable-interactive (renamed to: solver.yices.enable-interactive)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSomeB settera setterb + + , testCase "deprecated yices_enable-mcsat is equivalent to solver.yices.enable-mcsat" $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "yices_enable-mcsat" + (getConfiguration sym) + setterb <- getOptionSetting yicesEnableMCSat + (getConfiguration sym) + cmpUnderSomeB settera setterb + res1 <- try $ setBoolOpt settera True + case res1 of + Right warns -> fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: yices_enable-mcsat (renamed to: solver.yices.enable-mcsat)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSomeB settera setterb + + , testCase "deprecated yices_goal-timeout is equivalent to solver.yices.goal-timeout" $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "yices_goal-timeout" + (getConfiguration sym) + setterb <- getOptionSetting yicesGoalTimeout + (getConfiguration sym) + cmpUnderSomeI settera setterb + res1 <- try $ setIntegerOpt settera 123 + case res1 of + Right warns -> fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: yices_goal-timeout (renamed to: solver.yices.goal-timeout)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSomeI settera setterb + + , testCase "deprecated z3_path is equivalent to solver.z3.path" $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "z3_path" + (getConfiguration sym) + setterb <- getOptionSetting z3Path + (getConfiguration sym) + cmpUnderSome settera setterb + res1 <- try $ setUnicodeOpt settera "/bar/foo" + case res1 of + Right warns -> fmap show warns @?= + [ "Could not find: /bar/foo" + , "DEPRECATED CONFIG OPTION USED: z3_path (renamed to: solver.z3.path)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSome settera setterb + + , testCase "deprecated z3_timeout is equivalent to solver.z3.timeout" $ + withAdapters adaptrs $ \sym -> do + settera <- getOptionSettingFromText "z3_timeout" + (getConfiguration sym) + setterb <- getOptionSetting z3Timeout + (getConfiguration sym) + cmpUnderSomeI settera setterb + res1 <- try $ setIntegerOpt settera 123 + case res1 of + Right warns -> fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: z3_timeout (renamed to: solver.z3.timeout)" + ] + Left (SomeException e) -> assertFailure $ show e + cmpUnderSomeI settera setterb + + ] + + +---------------------------------------------------------------------- + nonlinearRealTest :: SolverAdapter State -> TestTree nonlinearRealTest adpt = testCase (solver_adapter_name adpt) $ withSym adpt $ \sym -> @@ -192,7 +650,12 @@ verilogTest = testCase "verilogTest" $ withIONonceGenerator $ \gen -> getSolverVersion :: String -> IO String getSolverVersion solver = do - try (readProcessWithExitCode (toLower <$> solver) ["--version"] "") >>= \case + let args = case toLower <$> solver of + -- n.b. abc will return a non-zero exit code if asked + -- for command usage. + "abc" -> ["s", "-q", "version;quit"] + _ -> ["--version"] + try (readProcessWithExitCode (toLower <$> solver) args "") >>= \case Right (r,o,e) -> if r == ExitSuccess then let ol = lines o in @@ -215,6 +678,7 @@ main = do localOption (mkTimeout (10 * 1000 * 1000)) $ testGroup "AdapterTests" [ testGroup "SmokeTest" $ map mkSmokeTest allAdapters + , testGroup "Config Tests" $ mkConfigTests allAdapters , testGroup "QuickStart" $ map mkQuickstartTest allAdapters , testGroup "nonlinear reals" $ map nonlinearRealTest -- NB: nonlinear arith expected to fail for STP and Boolector diff --git a/what4/test/ConfigTest.hs b/what4/test/ConfigTest.hs new file mode 100644 index 00000000..1d71acb9 --- /dev/null +++ b/what4/test/ConfigTest.hs @@ -0,0 +1,599 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +import Control.Exception ( displayException, try, SomeException(..), fromException ) +import qualified Data.List as L +import Data.Parameterized.Context ( pattern Empty, pattern (:>) ) +import Data.Parameterized.Some +import Data.Ratio ( (%) ) +import qualified Data.Set as Set +import qualified Data.Text as T +import Data.Void +import qualified Prettyprinter as PP + +import Test.Tasty +import Test.Tasty.Checklist +import Test.Tasty.HUnit + +import What4.BaseTypes +import What4.Concrete +import What4.Config + + +testSetAndGet :: [TestTree] +testSetAndGet = + [ + testCase "create multiple options" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr" + o2 = configOption BaseIntegerRepr "optint" + o3 = configOption BaseBoolRepr "optbool" + o1' = mkOpt o1 stringOptSty Nothing Nothing + o2' = mkOpt o2 integerOptSty Nothing Nothing + o3' = mkOpt o3 boolOptSty Nothing Nothing + extendConfig [o3', o2', o1'] cfg + + , testCase "create conflicting options" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "mainopt" + o2 = configOption BaseIntegerRepr "mainopt" + o1' = mkOpt o1 stringOptSty Nothing Nothing + o2' = mkOpt o2 integerOptSty Nothing Nothing + res <- try $ extendConfig [o2', o1'] cfg + wantOptCreateFailure "already exists with type" res + + , testCase "create conflicting options at different levels" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "mainopt" + o2 = configOption BaseIntegerRepr "main.mainopt" + o1' = mkOpt o1 stringOptSty Nothing Nothing + o2' = mkOpt o2 integerOptSty Nothing Nothing + res <- try @SomeException $ extendConfig [o2', o1'] cfg + case res of + Right () -> return () + Left e -> assertFailure $ "Unexpected exception: " <> displayException e + + , testCase "create duplicate unicode options" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "mainopt" + o2 = configOption (BaseStringRepr UnicodeRepr) "mainopt" + o1' = mkOpt o1 stringOptSty Nothing Nothing + o2' = mkOpt o2 stringOptSty Nothing Nothing + res <- try @SomeException $ extendConfig [o2', o1'] cfg + case res of + Right () -> return () + Left e -> assertFailure $ "Unexpected exception: " <> displayException e + + , testCaseSteps "get unset value, no default" $ \step -> do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr" + o2 = configOption BaseIntegerRepr "optint" + o3 = configOption BaseBoolRepr "optbool" + o1' = mkOpt o1 stringOptSty Nothing Nothing + o2' = mkOpt o2 integerOptSty Nothing Nothing + o3' = mkOpt o3 boolOptSty Nothing Nothing + extendConfig [o3', o2', o1'] cfg + access1 <- getOptionSetting o1 cfg + access2 <- getOptionSetting o2 cfg + access3 <- getOptionSetting o3 cfg + + step "get unset string opt" + v1 <- getMaybeOpt access1 + Nothing @=? v1 + res1 <- try $ getOpt access1 + wantOptGetFailure "not set" res1 + + step "get unset integer opt" + v2 <- getMaybeOpt access2 + Nothing @=? v2 + res2 <- try $ getOpt access2 + wantOptGetFailure "not set" res2 + + step "get unset bool opt" + v3 <- getMaybeOpt access3 + Nothing @=? v3 + res3 <- try $ getOpt access3 + wantOptGetFailure "not set" res3 + + , testCaseSteps "get unset value, with default" $ \step -> do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr" + o2 = configOption BaseIntegerRepr "optint" + o3 = configOption BaseBoolRepr "optbool" + o1' = mkOpt o1 stringOptSty Nothing (Just $ ConcreteString "strval") + o2' = mkOpt o2 integerOptSty Nothing (Just $ ConcreteInteger 11) + o3' = mkOpt o3 boolOptSty Nothing (Just $ ConcreteBool True) + extendConfig [o3', o2', o1'] cfg + access1 <- getOptionSetting o1 cfg + access2 <- getOptionSetting o2 cfg + access3 <- getOptionSetting o3 cfg + step "get unset default string opt" + v1 <- getMaybeOpt access1 + Just "strval" @=? v1 + step "get unset default integer opt" + v2 <- getMaybeOpt access2 + Just 11 @=? v2 + step "get unset default bool opt" + v3 <- getMaybeOpt access3 + Just True @=? v3 + + , testCaseSteps "get set value, with default" $ \step -> do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr" + o2 = configOption BaseIntegerRepr "optint" + o3 = configOption BaseBoolRepr "optbool" + o1' = mkOpt o1 stringOptSty Nothing (Just $ ConcreteString "strval") + o2' = mkOpt o2 integerOptSty Nothing (Just $ ConcreteInteger 11) + o3' = mkOpt o3 boolOptSty Nothing (Just $ ConcreteBool True) + extendConfig [o3', o2', o1'] cfg + access1 <- getOptionSetting o1 cfg + access2 <- getOptionSetting o2 cfg + access3 <- getOptionSetting o3 cfg + + step "set string opt" + res1 <- setOpt access1 "flibberty" + show <$> res1 @?= [] + + step "set bool opt" + res2 <- setOpt access3 False + show <$> res2 @?= [] + + step "set integer opt" + res3 <- setOpt access2 9945 + show <$> res3 @?= [] + + step "get string opt" + v1 <- getMaybeOpt access1 + Just "flibberty" @=? v1 + step "get integer opt" + v2 <- getMaybeOpt access2 + Just 9945 @=? v2 + step "get bool opt" + v3 <- getMaybeOpt access3 + Just False @=? v3 + + , testCaseSteps "set invalid values" $ \step -> do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr" + o2 = configOption BaseIntegerRepr "optint" + o3 = configOption BaseRealRepr "optbool" + -- n.b. the default values are not checked by the style! + o1' = mkOpt o1 (enumOptSty + (Set.fromList ["eeny", "meeny", "miny", "mo" ])) + Nothing (Just $ ConcreteString "strval") + o2' = mkOpt o2 (integerWithRangeOptSty Unbounded (Inclusive 10)) + Nothing (Just $ ConcreteInteger 11) + o3' = mkOpt o3 (realWithMinOptSty (Exclusive 1.23)) + Nothing (Just $ ConcreteReal 0.0) + extendConfig [o3', o2', o1'] cfg + access1 <- getOptionSetting o1 cfg + access2 <- getOptionSetting o2 cfg + access3 <- getOptionSetting o3 cfg + + step "initial defaults" + getMaybeOpt access1 >>= (@?= Just "strval") + getMaybeOpt access2 >>= (@?= Just 11) + getMaybeOpt access3 >>= (@?= Just (0 % 1 :: Rational)) + + step "set string opt invalidly" + -- Note: the strong typing prevents both of the following + -- setOpt access1 32 + -- setOpt access1 False + res1 <- try $ setOpt access1 "frobozz" + wantOptSetFailure "invalid setting \"frobozz\"" res1 + wantOptSetFailure "eeny, meeny, miny, mo" res1 + (try @SomeException $ setOpt access1 "meeny") >>= \case + Right [] -> return () + Right w -> assertFailure $ "Unexpected warnings: " <> show w + Left e -> assertFailure $ "Unexpected exception: " <> displayException e + + step "set integer opt invalidly" + wantOptSetFailure "out of range" =<< (try $ setOpt access2 11) + wantOptSetFailure "expected integer value in (-∞, 10]" =<< (try $ setOpt access2 11) + (try @SomeException $ setOpt access2 10) >>= \case + Right [] -> return () + Right w -> assertFailure $ "Unexpected warnings: " <> show w + Left e -> assertFailure $ "Unexpected exception: " <> displayException e + (try @SomeException $ setOpt access2 (-3)) >>= \case + Right [] -> return () + Right w -> assertFailure $ "Unexpected warnings: " <> show w + Left e -> assertFailure $ "Unexpected exception: " <> displayException e + + step "set real opt invalidly" + wantOptSetFailure "out of range" =<< (try $ setOpt access3 (0 % 3)) + wantOptSetFailure "expected real value in (123 % 100, +∞)" + =<< (try $ setOpt access3 (0 % 3)) + wantOptSetFailure "out of range" =<< (try $ setOpt access3 (1229 % 1000)) + wantOptSetFailure "out of range" =<< (try $ setOpt access3 (123 % 100)) + (try @SomeException $ setOpt access3 (123001 % 100000)) >>= \case + Right [] -> return () + Right w -> assertFailure $ "Unexpected warnings: " <> show w + Left e -> assertFailure $ "Unexpected exception: " <> displayException e + + , testCaseSteps "get and set option values by name" $ \step -> + withChecklist "multiple values" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "main.optstr" + o2 = configOption BaseIntegerRepr "main.set.cfg.optint" + o3 = configOption BaseBoolRepr "main.set.cfg.optbool" + o4 = configOption BaseIntegerRepr "alt.optint" + o1' = mkOpt o1 stringOptSty Nothing (Just $ ConcreteString "strval") + o2' = mkOpt o2 integerOptSty Nothing (Just $ ConcreteInteger 11) + o3' = mkOpt o3 boolOptSty Nothing (Just $ ConcreteBool True) + o4' = mkOpt o4 integerOptSty Nothing (Just $ ConcreteInteger 88) + extendConfig [o4', o3', o2', o1'] cfg + accessSome1 <- getOptionSettingFromText "main.optstr" cfg + accessSome2 <- getOptionSettingFromText "main.set.cfg.optint" cfg + accessSome3 <- getOptionSettingFromText "main.set.cfg.optbool" cfg + accessSome4 <- getOptionSettingFromText "alt.optint" cfg + + access1 <- getOptionSetting o1 cfg + access2 <- getOptionSetting o2 cfg + access3 <- getOptionSetting o3 cfg + access4 <- getOptionSetting o4 cfg + + step "getting with a Some OptionSetter requires type verification" + let cmpUnderSome :: Some OptionSetting -> T.Text -> IO () + cmpUnderSome (Some getter) v = + case testEquality + (configOptionType (optionSettingName getter)) + (BaseStringRepr UnicodeRepr) of + Just Refl -> do vt <- getMaybeOpt getter + Just v @=? vt + Nothing -> assertFailure "invalid option type" + cmpUnderSome accessSome1 "strval" + + step "setting using special setting functions" + let goodNoWarn f s v = + (try @SomeException $ f s v) >>= \case + Right [] -> return () + Right w -> assertFailure $ "Unexpected warnings: " <> show w + Left e -> assertFailure $ "Unexpected exception: " <> displayException e + goodNoWarn setUnicodeOpt accessSome1 "wild carrots" + goodNoWarn setIntegerOpt accessSome2 31 + goodNoWarn setIntegerOpt accessSome4 42 + goodNoWarn setBoolOpt accessSome3 False + + step "verify set values" + (Just "wild carrots" @=?) =<< getMaybeOpt access1 + (Just 31 @=?) =<< getMaybeOpt access2 + (Just False @=?) =<< getMaybeOpt access3 + (Just 42 @=?) =<< getMaybeOpt access4 + + step "cannot set values with wrong types" + -- Note that using an OptionSetting allows compile-time + -- elimination, but using a (Some OptionSetting) requires + -- run-time type witnessing and validation + wantOptSetFailure "type is a BaseStringRepr" + =<< (try $ setIntegerOpt accessSome1 54) + wantOptSetFailure "but given an integer" + =<< (try $ setIntegerOpt accessSome1 54) + + wantOptSetFailure "type is a BaseStringRepr" + =<< (try $ setBoolOpt accessSome1 True) + wantOptSetFailure "but given a boolean" + =<< (try $ setBoolOpt accessSome1 True) + + wantOptSetFailure "type is a BaseIntegerRepr" + =<< (try $ setUnicodeOpt accessSome2 "fresh tomatoes") + wantOptSetFailure "but given a text string" + =<< (try $ setUnicodeOpt accessSome2 "fresh tomatoes") + + + , testCaseSteps "get multiple values at once" $ \step -> + withChecklist "multiple values" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "main.optstr" + o2 = configOption BaseIntegerRepr "main.set.cfg.optint" + o3 = configOption BaseBoolRepr "main.set.cfg.optbool" + o4 = configOption BaseIntegerRepr "alt.optint" + o1' = mkOpt o1 stringOptSty Nothing (Just $ ConcreteString "strval") + o2' = mkOpt o2 integerOptSty Nothing (Just $ ConcreteInteger 11) + o3' = mkOpt o3 boolOptSty Nothing (Just $ ConcreteBool True) + o4' = mkOpt o4 integerOptSty Nothing (Just $ ConcreteInteger 88) + extendConfig [o4', o3', o2', o1'] cfg + access1 <- getOptionSetting o1 cfg + access3 <- getOptionSetting o3 cfg + access4 <- getOptionSetting o4 cfg + + step "set string opt" + res1 <- setOpt access1 "flibberty" + show <$> res1 @?= [] + + step "set bool opt" + res2 <- setOpt access3 False + show <$> res2 @?= [] + + step "set alt int opt" + res4 <- setOpt access4 789 + show <$> res4 @?= [] + + step "get main config values" + res <- getConfigValues "main.set" cfg + let msg = show . PP.pretty <$> res + msg `checkValues` + (Empty + :> Val "num values" length 2 + :> Val "bool" (any (L.isInfixOf "main.set.cfg.optbool = False")) True + :> Val "int" (any (L.isInfixOf "main.set.cfg.optint = 11")) True + ) + + step "get all config values" + resAll <- getConfigValues "" cfg + let msgAll = show . PP.pretty <$> resAll + msgAll `checkValues` + (Empty + :> Val "num values" length 5 + :> Val "bool" (any (L.isInfixOf "main.set.cfg.optbool = False")) True + :> Val "int" (any (L.isInfixOf "main.set.cfg.optint = 11")) True + :> Val "alt int" (any (L.isInfixOf "alt.optint = 789")) True + :> Val "str" (any (L.isInfixOf "main.optstr = \"flibberty\"")) True + :> Val "verbosity" (any (L.isInfixOf "verbosity = 0")) True + ) + + step "get specific config value" + resOne <- getConfigValues "alt.optint" cfg + let msgOne = show . PP.pretty <$> resOne + msgOne `checkValues` + (Empty + :> Val "num values" length 1 + :> Val "alt int" (any (L.isInfixOf "alt.optint = 789")) True + ) + + step "get unknown config value" + resNope <- getConfigValues "fargle.bargle" cfg + let msgNope = show . PP.pretty <$> resNope + msgNope `checkValues` (Empty :> Val "num values" length 0) + + + ] + +testDeprecated :: [TestTree] +testDeprecated = + [ + testCase "deprecation removal (case #1)" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "hello" + o1' = mkOpt o1 stringOptSty (Just "greeting") Nothing + extendConfig [deprecatedOpt [] o1'] cfg + setter <- getOptionSetting o1 cfg + res <- try $ setOpt setter "eh?" + case res of + Right warns -> + fmap show warns @?= + [ "DEPRECATED CONFIG OPTION WILL BE IGNORED: hello (no longer valid)" + ] + Left (SomeException e) -> assertFailure $ show e + + , testCase "deprecation rename (case #2)" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "hi" + o2 = configOption (BaseStringRepr UnicodeRepr) "hello" + o1' = deprecatedOpt [o2'] $ + mkOpt o1 stringOptSty (Just "greeting") Nothing + o2' = mkOpt o2 stringOptSty (Just "greeting") Nothing + extendConfig [o2', o1'] cfg + setter <- getOptionSetting o1 cfg + res <- try $ setOpt setter "eh?" + case res of + Right warns -> + fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: hi (renamed to: hello)" + ] + Left (SomeException e) -> assertFailure $ show e + + , testCase "deprecation rename (case #2), wrong order" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "yo" + o2 = configOption (BaseStringRepr UnicodeRepr) "hello" + o1' = deprecatedOpt [o2'] $ + mkOpt o1 stringOptSty (Just "greeting") Nothing + o2' = mkOpt o2 stringOptSty (Just "greeting") Nothing + res <- try $ extendConfig [o1', o2'] cfg + wantOptCreateFailure + "replacement options must be inserted into Config \ + \before this deprecated option" + res + + , testCase "deprecation rename and re-typed (case #3)" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr" + o2 = configOption BaseIntegerRepr "optnum" + o1' = deprecatedOpt [o2'] $ + mkOpt o1 stringOptSty (Just "some opt") Nothing + o2' = mkOpt o2 integerOptSty (Just "some other opt") Nothing + extendConfig [o2', o1'] cfg + setter <- getOptionSetting o1 cfg + res <- try $ setOpt setter "eh?" + case res of + Right warns -> + fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: optstr::BaseStringRepr UnicodeRepr (changed to: \"optnum\"::BaseIntegerRepr); this value may be ignored" + ] + Left (SomeException e) -> assertFailure $ show e + + , testCase "deprecation, multiple replacements (case #4)" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "url" + o2 = configOption (BaseStringRepr UnicodeRepr) "hostname" + o3 = configOption BaseIntegerRepr "port" + o1' = deprecatedOpt [o2', o3'] $ + mkOpt o1 stringOptSty (Just "some opt") Nothing + o2' = mkOpt o2 stringOptSty (Just "some other opt") Nothing + o3' = mkOpt o3 integerOptSty (Just "some other opt") Nothing + extendConfig [o3', o2', o1'] cfg + setter <- getOptionSetting o1 cfg + res <- try $ setOpt setter "here?" + case res of + Right warns -> + fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: url::BaseStringRepr UnicodeRepr (replaced by: \"hostname\"::BaseStringRepr UnicodeRepr, \"port\"::BaseIntegerRepr); this value may be ignored" + ] + Left (SomeException e) -> assertFailure $ show e + + , testCase "deprecation, multiple + removed/split (case #4,(#1,#3))" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "url" + o2 = configOption (BaseStringRepr UnicodeRepr) "hostname" + o3 = configOption BaseIntegerRepr "port" + o4 = configOption (BaseStringRepr UnicodeRepr) "host" + o5 = configOption (BaseStringRepr UnicodeRepr) "domain" + o1' = deprecatedOpt [o2', o3'] $ + mkOpt o1 stringOptSty (Just "some opt") Nothing + o2' = deprecatedOpt [o4', o5'] $ + mkOpt o2 stringOptSty (Just "some other opt") Nothing + o3' = deprecatedOpt [] $ + mkOpt o3 integerOptSty (Just "some other opt") Nothing + o4' = mkOpt o4 stringOptSty (Nothing) Nothing + o5' = mkOpt o5 stringOptSty (Just "some opt") (Just $ ConcreteString "cow.barn") + extendConfig [ o4', o5', o2', o3', o1' ] cfg + setter <- getOptionSetting o1 cfg + res <- try $ setOpt setter "here?" + case res of + Right warns -> + fmap show warns @?= + [ "DEPRECATED CONFIG OPTION USED: url::BaseStringRepr UnicodeRepr (replaced by: \"host\"::BaseStringRepr UnicodeRepr, \"domain\"::BaseStringRepr UnicodeRepr); this value may be ignored" + ] + Left (SomeException e) -> assertFailure $ show e + + ] + +testHelp :: [TestTree] +testHelp = + [ + testCase "builtin-only config help" $ + withChecklist "builtins" $ do + cfg <- initialConfig 0 [] + help <- configHelp "" cfg + help `checkValues` + (Empty + :> Val "num" length 1 + :> Val "verbosity" (L.isInfixOf "verbosity =" . show . head) True + ) + + + , testCaseSteps "three item (1 deprecated) config help" $ \step -> + withChecklist "three items" $ do + cfg <- initialConfig 0 [] + let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr" + o2 = configOption BaseIntegerRepr "optnum" + o3 = configOption BaseIntegerRepr "foo.bar.baz.num" + o1' = mkOpt o1 stringOptSty (Just "some opt") Nothing + o2' = mkOpt o2 integerOptSty (Just "some other opt") Nothing + o3' = mkOpt o3 integerOptSty (Just "foo stuff") Nothing + helpIncludes txts = any (\h -> all (\t -> L.isInfixOf t (show h)) txts) + extendConfig [o2', deprecatedOpt [o2'] o1', o3'] cfg + setter2 <- getOptionSetting o2 cfg + setRes <- setOpt setter2 13 + setRes `checkValues` (Empty :> Val "no warnings" null True) + + step "all help" + help <- configHelp "" cfg + help `checkValues` + (Empty + :> Val "num" length 4 + :> Val "verbosity" (helpIncludes ["verbosity ="]) True + :> Val "option 1" (helpIncludes ["optstr" + , "some opt" + , "DEPRECATED!" + , "Suggest" + , "to \"optnum\"" + ]) True + :> Val "option 2" (helpIncludes ["optnum", "= 13", "some other opt"]) True + :> Val "option 3" (helpIncludes ["foo.bar.baz.num", "foo stuff"]) True + ) + + step "sub help" + subHelp <- configHelp "foo.bar" cfg + subHelp `checkValues` + (Empty + :> Val "num" length 1 + :> Val "option 3" (helpIncludes ["foo.bar.baz.num", "foo stuff"]) True + ) + + step "specific help" + spec <- configHelp "optstr" cfg + spec `checkValues` + (Empty + :> Val "num" length 1 + :> Val "spec name" (helpIncludes ["optstr"]) True + :> Val "spec opt help" (helpIncludes ["some opt"]) True + :> Val "spec opt help deprecated" (helpIncludes [ "DEPRECATED!" + , "Suggest" + , "to \"optnum\"" + ]) True + ) + + step "specific sub help" + subspec <- configHelp "foo.bar.baz.num" cfg + subspec `checkValues` + (Empty + :> Val "num" length 1 + :> Val "option 3" (helpIncludes ["foo.bar.baz.num", "foo stuff"]) True + ) + + ] + +instance TestShow (PP.Doc Void) where testShow = show +instance TestShow [PP.Doc Void] where testShow = testShowList +instance TestShow [String] where testShow = testShowList + +wantOptCreateFailure :: Show a => String -> Either SomeException a -> IO () +wantOptCreateFailure withText res = case res of + Right r -> + assertFailure ("Expected '" <> withText <> + "' but completed successfully with: " <> show r) + Left err -> + case fromException err of + Just (e :: OptCreateFailure) -> + withText `L.isInfixOf` (show e) @? + ("Expected '" <> withText <> "' exception error but got: " <> + displayException e) + _ -> assertFailure $ + "Expected OptCreateFailure exception but got: " <> + displayException err + +wantOptSetFailure :: Show a => String -> Either SomeException a -> IO () +wantOptSetFailure withText res = case res of + Right r -> + assertFailure ("Expected '" <> withText <> + "' but completed successfully with: " <> show r) + Left err -> + case fromException err of + Just (e :: OptSetFailure) -> + withText `L.isInfixOf` (show e) @? + ("Expected '" <> withText <> "' exception error but got: " <> + displayException e) + _ -> assertFailure $ + "Expected OptSetFailure exception but got: " <> + displayException err + +wantOptGetFailure :: Show a => String -> Either SomeException a -> IO () +wantOptGetFailure withText res = case res of + Right r -> + assertFailure ("Expected '" <> withText <> + "' but completed successfully with: " <> show r) + Left err -> + case fromException err of + Just (e :: OptGetFailure) -> + withText `L.isInfixOf` (show e) @? + ("Expected '" <> withText <> "' exception error but got: " <> + displayException e) + _ -> assertFailure $ + "Expected OptGetFailure exception but got: " <> + displayException err + + +main :: IO () +main = defaultMain $ + testGroup "ConfigTests" + [ testGroup "Set and get" $ testSetAndGet + , testGroup "Deprecated Configs" $ testDeprecated + , testGroup "Config help" $ testHelp + ] diff --git a/what4/test/ExprBuilderSMTLib2.hs b/what4/test/ExprBuilderSMTLib2.hs index fa52a561..4015a610 100644 --- a/what4/test/ExprBuilderSMTLib2.hs +++ b/what4/test/ExprBuilderSMTLib2.hs @@ -885,12 +885,12 @@ testSolverInfo = testGroup "solver info queries" $ [ testCase "test get solver version" $ withOnlineZ3 $ \_ proc -> do let conn = solverConn proc getVersion conn - _ <- versionResult (solverResponse proc) + _ <- versionResult conn pure () , testCase "test get solver name" $ withOnlineZ3 $ \_ proc -> do let conn = solverConn proc getName conn - nm <- nameResult (solverResponse proc) + nm <- nameResult conn nm @?= "Z3" ] diff --git a/what4/test/OnlineSolverTest.hs b/what4/test/OnlineSolverTest.hs index 3ed7cb2c..55beee42 100644 --- a/what4/test/OnlineSolverTest.hs +++ b/what4/test/OnlineSolverTest.hs @@ -214,7 +214,12 @@ quickstartTestAlt (nm, AnOnlineSolver (Proxy :: Proxy s), features, opts) = test getSolverVersion :: String -> IO String getSolverVersion solver = - try (readProcessWithExitCode (toLower <$> solver) ["--version"] "") >>= \case + let args = case toLower <$> solver of + -- n.b. abc will return a non-zero exit code if asked + -- for command usage. + "abc" -> ["s", "-q", "version;quit"] + _ -> ["--version"] + in try (readProcessWithExitCode (toLower <$> solver) args "") >>= \case Right (r,o,e) -> if r == ExitSuccess then let ol = lines o in diff --git a/what4/test/SolverParserTest.hs b/what4/test/SolverParserTest.hs new file mode 100644 index 00000000..6d824749 --- /dev/null +++ b/what4/test/SolverParserTest.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} + +import Control.Monad.Catch ( SomeException, try ) +import qualified Data.Text.IO as TIO +import Numeric.Natural +import qualified System.IO.Streams as Streams + +import Test.Tasty +import Test.Tasty.HUnit +import Test.Tasty.Ingredients +import Test.Tasty.Sugar + +import What4.Expr.Builder ( emptySymbolVarBimap ) +import What4.ProblemFeatures ( noFeatures ) +import What4.Protocol.SMTLib2.Response ( SMTResponse, getLimitedSolverResponse ) +import qualified What4.Protocol.SMTLib2.Syntax as SMT2 +import What4.Protocol.SMTWriter + + +sugarCube :: CUBE +sugarCube = mkCUBE { inputDir = "test/responses" + , rootName = "*.rsp" + , expectedSuffix = ".exp" + , validParams = [ ("parsing", Just ["strict", "lenient"]) + ] + } + +ingredients :: [Ingredient] +ingredients = includingOptions sugarOptions : + sugarIngredients [sugarCube] <> + defaultIngredients + + +main :: IO () +main = do testSweets <- findSugar sugarCube + defaultMainWithIngredients ingredients . + testGroup "solver response tests" =<< + withSugarGroups testSweets testGroup mkTest + +mkTest :: Sweets -> Natural -> Expectation -> IO [TestTree] +mkTest s n e = do + expect <- readFile $ expectedFile e + let strictness = + let strictVal pmtch = + if paramMatchVal "strict" pmtch + then Strict + else if paramMatchVal "lenient" pmtch + then Lenient + else error "Invalid strictness specification" + in maybe Strict strictVal $ lookup "parsing" $ expParamsMatch e + return + [ + testCase (rootMatchName s <> " #" <> show n) $ do + inpStrm <- Streams.makeInputStream $ Just <$> TIO.readFile (rootFile s) + outStrm <- Streams.makeOutputStream $ \_ -> error "output not supported for test" + w <- newWriterConn + outStrm + inpStrm + (AckAction $ undefined) + "test-solver" + strictness + noFeatures + emptySymbolVarBimap + () + actual <- try $ getLimitedSolverResponse "test resp" Just w (SMT2.Cmd "test cmd") + expect @=? show (actual :: Either SomeException SMTResponse) + ] diff --git a/what4/test/responses/err-behav-continue.exp b/what4/test/responses/err-behav-continue.exp new file mode 100644 index 00000000..8bd3800e --- /dev/null +++ b/what4/test/responses/err-behav-continue.exp @@ -0,0 +1 @@ +Right (RspErrBehavior "continued-execution") \ No newline at end of file diff --git a/what4/test/responses/err-behav-continue.rsp b/what4/test/responses/err-behav-continue.rsp new file mode 100644 index 00000000..d46d97ec --- /dev/null +++ b/what4/test/responses/err-behav-continue.rsp @@ -0,0 +1 @@ +(:error-behavior continued-execution) diff --git a/what4/test/responses/err-behav-unrec.exp b/what4/test/responses/err-behav-unrec.exp new file mode 100644 index 00000000..6b1caed7 --- /dev/null +++ b/what4/test/responses/err-behav-unrec.exp @@ -0,0 +1,12 @@ +Left Could not parse solver response: + Solver response parsing failure. +*** Exception: Unrecognized response from solver: + bad :error-behavior value +in response to command: + (get-info :error-behavior) + +Attempting to parse input for test resp: +Just "(:error-behavior freak-out)\n" + +in response to commands for test resp: +test cmd diff --git a/what4/test/responses/err-behav-unrec.rsp b/what4/test/responses/err-behav-unrec.rsp new file mode 100644 index 00000000..468dd0de --- /dev/null +++ b/what4/test/responses/err-behav-unrec.rsp @@ -0,0 +1 @@ +(:error-behavior freak-out) diff --git a/what4/test/responses/error_bad.exp b/what4/test/responses/error_bad.exp new file mode 100644 index 00000000..14bcab7e --- /dev/null +++ b/what4/test/responses/error_bad.exp @@ -0,0 +1,4 @@ +Left Solver reported an error: + this is bad +in response to command: + test cmd diff --git a/what4/test/responses/error_bad.rsp b/what4/test/responses/error_bad.rsp new file mode 100644 index 00000000..c8aac067 --- /dev/null +++ b/what4/test/responses/error_bad.rsp @@ -0,0 +1 @@ +(error "this is bad") diff --git a/what4/test/responses/minisat_verbose_success.exp b/what4/test/responses/minisat_verbose_success.exp new file mode 100644 index 00000000..b907d30a --- /dev/null +++ b/what4/test/responses/minisat_verbose_success.exp @@ -0,0 +1 @@ +Right AckSuccess \ No newline at end of file diff --git a/what4/test/responses/minisat_verbose_success.rsp b/what4/test/responses/minisat_verbose_success.rsp new file mode 100644 index 00000000..4c64a5e7 --- /dev/null +++ b/what4/test/responses/minisat_verbose_success.rsp @@ -0,0 +1,2 @@ +minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy. +success diff --git a/what4/test/responses/minisat_verbose_success.strict.exp b/what4/test/responses/minisat_verbose_success.strict.exp new file mode 100644 index 00000000..bf18823b --- /dev/null +++ b/what4/test/responses/minisat_verbose_success.strict.exp @@ -0,0 +1,8 @@ +Left Could not parse solver response: + Solver response parsing failure. +*** Exception: Parse exception: Failed reading: empty +Attempting to parse input for test resp: +Just "minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy.\nsuccess\n" + +in response to commands for test resp: +test cmd diff --git a/what4/test/responses/name.exp b/what4/test/responses/name.exp new file mode 100644 index 00000000..bb0d942b --- /dev/null +++ b/what4/test/responses/name.exp @@ -0,0 +1 @@ +Right (RspName "fancy solver #12") \ No newline at end of file diff --git a/what4/test/responses/name.rsp b/what4/test/responses/name.rsp new file mode 100644 index 00000000..394e7769 --- /dev/null +++ b/what4/test/responses/name.rsp @@ -0,0 +1 @@ +(:name "fancy solver #12") diff --git a/what4/test/responses/rsnunk-bad.exp b/what4/test/responses/rsnunk-bad.exp new file mode 100644 index 00000000..dda7d813 --- /dev/null +++ b/what4/test/responses/rsnunk-bad.exp @@ -0,0 +1,12 @@ +Left Could not parse solver response: + Solver response parsing failure. +*** Exception: Unrecognized response from solver: + bad :reason-unknown value +in response to command: + reason? + +Attempting to parse input for test resp: +Just "(:reason-unknown foo bar baz)\n" + +in response to commands for test resp: +test cmd diff --git a/what4/test/responses/rsnunk-bad.rsp b/what4/test/responses/rsnunk-bad.rsp new file mode 100644 index 00000000..c579efae --- /dev/null +++ b/what4/test/responses/rsnunk-bad.rsp @@ -0,0 +1 @@ +(:reason-unknown foo bar baz) diff --git a/what4/test/responses/rsnunk-incomplete.exp b/what4/test/responses/rsnunk-incomplete.exp new file mode 100644 index 00000000..10a2719c --- /dev/null +++ b/what4/test/responses/rsnunk-incomplete.exp @@ -0,0 +1 @@ +Right RspRsnIncomplete \ No newline at end of file diff --git a/what4/test/responses/rsnunk-incomplete.rsp b/what4/test/responses/rsnunk-incomplete.rsp new file mode 100644 index 00000000..14a54dfa --- /dev/null +++ b/what4/test/responses/rsnunk-incomplete.rsp @@ -0,0 +1 @@ +(:reason-unknown incomplete) diff --git a/what4/test/responses/rsnunk-memout.exp b/what4/test/responses/rsnunk-memout.exp new file mode 100644 index 00000000..74856a40 --- /dev/null +++ b/what4/test/responses/rsnunk-memout.exp @@ -0,0 +1 @@ +Right RspOutOfMemory \ No newline at end of file diff --git a/what4/test/responses/rsnunk-memout.rsp b/what4/test/responses/rsnunk-memout.rsp new file mode 100644 index 00000000..f1997531 --- /dev/null +++ b/what4/test/responses/rsnunk-memout.rsp @@ -0,0 +1 @@ +(:reason-unknown memout) diff --git a/what4/test/responses/rsnunk-sexp.exp b/what4/test/responses/rsnunk-sexp.exp new file mode 100644 index 00000000..8c286023 --- /dev/null +++ b/what4/test/responses/rsnunk-sexp.exp @@ -0,0 +1 @@ +Right (RspUnkReason (SApp [SAtom "foo",SAtom "bar",SAtom "baz"])) \ No newline at end of file diff --git a/what4/test/responses/rsnunk-sexp.rsp b/what4/test/responses/rsnunk-sexp.rsp new file mode 100644 index 00000000..5f33da3c --- /dev/null +++ b/what4/test/responses/rsnunk-sexp.rsp @@ -0,0 +1 @@ +(:reason-unknown (foo bar baz)) diff --git a/what4/test/responses/sat.exp b/what4/test/responses/sat.exp new file mode 100644 index 00000000..41dceadc --- /dev/null +++ b/what4/test/responses/sat.exp @@ -0,0 +1 @@ +Right AckSat \ No newline at end of file diff --git a/what4/test/responses/sat.rsp b/what4/test/responses/sat.rsp new file mode 100644 index 00000000..6b8a2c3d --- /dev/null +++ b/what4/test/responses/sat.rsp @@ -0,0 +1 @@ +sat diff --git a/what4/test/responses/success.exp b/what4/test/responses/success.exp new file mode 100644 index 00000000..b907d30a --- /dev/null +++ b/what4/test/responses/success.exp @@ -0,0 +1 @@ +Right AckSuccess \ No newline at end of file diff --git a/what4/test/responses/success.rsp b/what4/test/responses/success.rsp new file mode 100644 index 00000000..2e9ba477 --- /dev/null +++ b/what4/test/responses/success.rsp @@ -0,0 +1 @@ +success diff --git a/what4/test/responses/unknown.exp b/what4/test/responses/unknown.exp new file mode 100644 index 00000000..86172f19 --- /dev/null +++ b/what4/test/responses/unknown.exp @@ -0,0 +1 @@ +Right AckUnknown \ No newline at end of file diff --git a/what4/test/responses/unknown.rsp b/what4/test/responses/unknown.rsp new file mode 100644 index 00000000..35466456 --- /dev/null +++ b/what4/test/responses/unknown.rsp @@ -0,0 +1 @@ +unknown diff --git a/what4/test/responses/unsat.exp b/what4/test/responses/unsat.exp new file mode 100644 index 00000000..e94655d0 --- /dev/null +++ b/what4/test/responses/unsat.exp @@ -0,0 +1 @@ +Right AckUnsat \ No newline at end of file diff --git a/what4/test/responses/unsat.rsp b/what4/test/responses/unsat.rsp new file mode 100644 index 00000000..3f65111b --- /dev/null +++ b/what4/test/responses/unsat.rsp @@ -0,0 +1 @@ +unsat diff --git a/what4/test/responses/unsupported.exp b/what4/test/responses/unsupported.exp new file mode 100644 index 00000000..89edc494 --- /dev/null +++ b/what4/test/responses/unsupported.exp @@ -0,0 +1,2 @@ +Left unsupported command: + test cmd diff --git a/what4/test/responses/unsupported.rsp b/what4/test/responses/unsupported.rsp new file mode 100644 index 00000000..ad7ccf7a --- /dev/null +++ b/what4/test/responses/unsupported.rsp @@ -0,0 +1 @@ +unsupported diff --git a/what4/test/responses/version.exp b/what4/test/responses/version.exp new file mode 100644 index 00000000..a0cbd66c --- /dev/null +++ b/what4/test/responses/version.exp @@ -0,0 +1 @@ +Right (RspVersion "1.8") \ No newline at end of file diff --git a/what4/test/responses/version.rsp b/what4/test/responses/version.rsp new file mode 100644 index 00000000..c05d324f --- /dev/null +++ b/what4/test/responses/version.rsp @@ -0,0 +1 @@ +(:version "1.8") diff --git a/what4/what4.cabal b/what4/what4.cabal index 3f7dda81..df6c0fa8 100644 --- a/what4/what4.cabal +++ b/what4/what4.cabal @@ -177,6 +177,7 @@ library What4.Protocol.Online What4.Protocol.SMTLib2 What4.Protocol.SMTLib2.Parse + What4.Protocol.SMTLib2.Response What4.Protocol.SMTLib2.Syntax What4.Protocol.SMTWriter What4.Protocol.ReadDecimal @@ -249,6 +250,16 @@ test-suite adapter-test text, versions +test-suite config-test + import: bldflags, testdefs-hunit + type: exitcode-stdio-1.0 + main-is: ConfigTest.hs + build-depends: containers + , parameterized-utils + , prettyprinter + , tasty-checklist >= 1.0 && < 1.1 + , text + test-suite online-solver-test import: bldflags, testdefs-hunit type: exitcode-stdio-1.0 @@ -344,3 +355,15 @@ test-suite template_tests build-depends: bv-sized , libBF , transformers + + +test-suite solver_parsing_tests + import: bldflags, testdefs-hunit + type: exitcode-stdio-1.0 + main-is : SolverParserTest.hs + build-depends: contravariant + , exceptions + , io-streams + , lumberjack + , tasty-sugar >= 1.1 && < 1.2 + , text