what4 1.2.1 → 1.3
raw patch · 60 files changed
+3817/−1061 lines, 60 filesdep +asyncdep +clockdep +concurrent-extradep −extradep ~exceptionsdep ~hashabledep ~prettyprinternew-uploader
Dependencies added: async, clock, concurrent-extra, tasty-expected-failure, units, units-defs
Dependencies removed: extra
Dependency ranges changed: exceptions, hashable, prettyprinter, process, tasty-checklist, tasty-hedgehog
Files
- CHANGES.md +87/−0
- README.md +5/−6
- doc/QuickStart.hs +3/−4
- doc/implementation.md +25/−0
- src/Test/Verification.hs +2/−2
- src/What4/BaseTypes.hs +6/−0
- src/What4/Concrete.hs +13/−7
- src/What4/Config.hs +65/−29
- src/What4/Expr.hs +16/−0
- src/What4/Expr/Allocator.hs +201/−0
- src/What4/Expr/App.hs +132/−53
- src/What4/Expr/AppTheory.hs +7/−9
- src/What4/Expr/ArrayUpdateMap.hs +1/−1
- src/What4/Expr/BoolMap.hs +1/−1
- src/What4/Expr/Builder.hs +356/−277
- src/What4/Expr/GroundEval.hs +104/−32
- src/What4/Expr/MATLAB.hs +4/−0
- src/What4/Expr/StringSeq.hs +1/−1
- src/What4/Expr/UnaryBV.hs +2/−0
- src/What4/Expr/VarIdentification.hs +26/−22
- src/What4/Expr/WeightedSum.hs +10/−4
- src/What4/FloatMode.hs +76/−0
- src/What4/Interface.hs +157/−26
- src/What4/InterpretedFloatingPoint.hs +43/−0
- src/What4/LabeledPred.hs +3/−1
- src/What4/ProblemFeatures.hs +17/−0
- src/What4/Protocol/Online.hs +102/−19
- src/What4/Protocol/SMTLib2.hs +110/−48
- src/What4/Protocol/SMTLib2/Response.hs +19/−8
- src/What4/Protocol/SMTLib2/Syntax.hs +10/−10
- src/What4/Protocol/SMTWriter.hs +142/−65
- src/What4/Protocol/VerilogWriter/ABCVerilog.hs +2/−1
- src/What4/Protocol/VerilogWriter/Backend.hs +5/−10
- src/What4/SemiRing.hs +8/−2
- src/What4/Solver.hs +4/−0
- src/What4/Solver/Boolector.hs +19/−4
- src/What4/Solver/CVC4.hs +9/−6
- src/What4/Solver/STP.hs +18/−4
- src/What4/Solver/Yices.hs +32/−12
- src/What4/Solver/Z3.hs +18/−5
- src/What4/SpecialFunctions.hs +443/−0
- src/What4/Utils/AbstractDomains.hs +87/−24
- src/What4/Utils/AnnotatedMap.hs +10/−0
- src/What4/Utils/OnlyIntRepr.hs +3/−0
- src/What4/Utils/Process.hs +2/−1
- src/What4/Utils/ResolveBounds/BV.hs +339/−0
- test/AdapterTest.hs +54/−54
- test/ExprBuilderSMTLib2.hs +449/−138
- test/ExprsTest.hs +3/−5
- test/GenWhat4Expr.hs +113/−46
- test/HH/VerifyBindings.hs +1/−1
- test/IteExprs.hs +3/−4
- test/OnlineSolverTest.hs +328/−84
- test/ProbeSolvers.hs +55/−0
- test/TestTemplate.hs +3/−4
- test/hedgehog/Test/Tasty/Hedgehog/Alt.hs +29/−0
- test/responses/err-behav-unrec.exp +1/−9
- test/responses/minisat_verbose_success.strict.exp +1/−8
- test/responses/rsnunk-bad.exp +1/−9
- what4.cabal +31/−5
CHANGES.md view
@@ -1,3 +1,90 @@+# 1.3 (April 2022)++* Allow building with GHC 9.2.++* According to+ [this discussion](https://github.com/ghc-proposals/ghc-proposals/discussions/440),+ the `forall` identifier will be claimed, and `forall` made into a+ full keyword. Therefore, the `forall` and `exists` combinators of+ `What4.Protocol.SMTLib2.Syntax` have been+ renamed into `forall_` and `exists_`.++* Add operations for increased control over the scope of+ configuration options, both in the `What4.Config` and+ `What4.Expr.Builder` modules.++* Previously, the `exprCounter`, `sbUserState`, `sbUnaryThreshold`, and+ `sbCacheStartSize` fields of `ExprBuilder` were directly exposed; in+ principle this allows users to modify them, which was not intended+ in some cases. These have been uniformly renamed to remove the `sb`+ prefix, and exposed as `Getter` or `Lens` values instead, as+ appropriate.++* The `sbBVDomainRangeLimit` fields of `ExprBuilder` was obsolete and+ has been removed.++* Allow building with `hashable-1.4.*`:+ * Add `Eq` instances for all data types with `Hashable` instances that+ were missing corresponding `Eq` instances. This is required since+ `hashable-1.4.0.0` adds an `Eq` superclass to `Hashable`.+ * Some `Hashable` instances now have extra constraints to match the+ constraints in their corresponding `Eq` instances. For example,+ the `Hashable` instance for `SymNat` now has an extra `TestEquality`+ constraint to match its `Eq` instance.++* Add an `unsafeSetAbstractValue` function to the `IsExpr` class which allows+ one to manually set the `AbstractValue` used in a symbolic expression.+ As the name suggests, this function is unsound in the general case, so use+ this with caution.++* Add a `What4.Utils.ResolveBounds.BV` module, which provides a `resolveSymBV`+ function that checks if a `SymBV` is concrete. If it is not concrete, it+ returns the lower and upper version bounds, as determined by querying an+ online SMT solver.++* Add `arrayCopy`, `arraySet`, and `arrayRangeEq` methods to `IsExprBuilder`.++* Add a `getUnannotatedTerm` method to `IsExprBuilder` for retrieving the+ original, unannotated term out of an annotated term.++* `IsExprBuilder` now has `floatSpecialFunction{,0,1,2}`+ and `realSpecialFunction{,0,1,2}` methods which allow the use of special+ values or functions such as `pi`, trigonometric functions, exponentials, or+ logarithms. Similarly, `IsInterpretedFloatExprBuilder` now has+ `iFloatSpecialFunction{,0,1,2}` methods. Although little solver support+ exists for special functions, `what4` may be able to prove properties about+ them in limited cases.+ * The `realPi`, `realLog`, `realExp`, `realSin`, `realCos`, `realTan`,+ `realSinh`, `realCosh`, `realTanh`, and `realAtan2` methods of+ `IsExprBuilder` now have default implementations in terms of+ `realSpecialFunction{,0,1,2}`.++* Add an `exprUninterpConstants` method to `IsSymExprBuilder` which returns the+ set of uninterpreted constants in a symbolic expression.++* Add a `natToIntegerPure` function which behaves like `natToInteger` but+ without using `IO`.++* `asConcrete` now supports concretizing float expressions by way of the new+ `ConcreteFloat` constructor in `ConcreteVal`.++* Add a `z3Tactic` configuration option to `What4.Solver.Z3` that allows+ specifying a custom tactic to pass to `z3`.++* `safeSymbol` now replaces exclamation marks (`!`) with underscores (`_`) so+ that the generated names are legal in Verilog.++* Add `Foldable`, `Traversable`, and `Show` instances for `LabeledPred`.++* Fix a bug in which `what4` would generate incorrect SMTLib code for array+ lookups and updates when using the CVC4 backend.++* Fix a bug in which `what4` would incorrectly attempt to configure Boolector+ 3.2.2 or later.++* Fix a bug in which strings containing `\u` or ending with `\` would be+ escaped incorrectly.+ # 1.2.1 (June 2021) * Include test suite data in the Hackage tarball.
README.md view
@@ -57,7 +57,8 @@ import What4.Config (extendConfig) import What4.Expr ( ExprBuilder, FloatModeRepr(..), newExprBuilder- , BoolExpr, GroundValue, groundEval )+ , BoolExpr, GroundValue, groundEval+ , EmptyExprBuilderState(..) ) import What4.Interface ( BaseTypeRepr(..), getConfiguration , freshConstant, safeSymbol@@ -75,8 +76,6 @@ point to your Z3.) ```-data BuilderState st = EmptyState- z3executable :: FilePath z3executable = "z3" ```@@ -87,7 +86,7 @@ main :: IO () main = do Some ng <- newIONonceGenerator- sym <- newExprBuilder FloatIEEERepr EmptyState ng+ sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng ``` Most of the functions in `What4.Interface`, the module for building up@@ -271,10 +270,10 @@ encounter such a situation, please open a ticket, as our goal is to work correctly on as wide a collection of solvers as is reasonable. -- Z3 versions 4.8.7, 4.8.8, and 4.8.9+- Z3 versions 4.8.7 through 4.8.12 - Yices 2.6.1 and 2.6.2 - CVC4 1.7 and 1.8-- Boolector 3.2.1+- Boolector 3.2.1 and 3.2.2 - STP 2.3.3 (However, note https://github.com/stp/stp/issues/363, which prevents effective retrieval of model values. This should be resolved by the next release)
doc/QuickStart.hs view
@@ -10,7 +10,8 @@ import What4.Config (extendConfig) import What4.Expr ( ExprBuilder, FloatModeRepr(..), newExprBuilder- , BoolExpr, GroundValue, groundEval )+ , BoolExpr, GroundValue, groundEval+ , EmptyExprBuilderState(..) ) import What4.Interface ( BaseTypeRepr(..), getConfiguration , freshConstant, safeSymbol@@ -21,15 +22,13 @@ (assume, sessionWriter, runCheckSat) -data BuilderState st = EmptyState- z3executable :: FilePath z3executable = "z3" main :: IO () main = do Some ng <- newIONonceGenerator- sym <- newExprBuilder FloatIEEERepr EmptyState ng+ sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng -- This line is necessary for working with z3. extendConfig z3Options (getConfiguration sym)
doc/implementation.md view
@@ -123,3 +123,28 @@ A future version of Yices may provide the ability to specify normal keyboard interrupt handling via command-line parameters.++## Configuration++What4 configuration utilizes a configuration management that allows+different modules to locally define their configuration options.+Configuration options are identified by a name which contains+period-separated strings to differentiate different configuration+namespaces.++The overall configuration is stored in the `sym` parameter, and can be+retrieved by the `getConfiguration` function and extended via the+`extendConfig` function. Each configuration has an `OptionStyle` that+associates a validation function with the configuration; setting a+configuration value returns an indication of whether an error+occurred, along with zero or more warnings for the configuration.++Each module can define its own set of configuration options, and must+contrive to extend the global configuration with its options at+startup time.++This configuration mechanism is designed to allow client libraries and+executables to extend the configuration with their own configuration+parameters.++For more information, see src/What4/Config.hs.
src/Test/Verification.hs view
@@ -178,12 +178,12 @@ -- | A test generator that returns an 'Int' value between the -- specified (inclusive) bounds. chooseInt :: (Int, Int) -> Gen Int-chooseInt r = Gen (asks genChooseInt >>= lift . ($r))+chooseInt r = Gen (asks genChooseInt >>= lift . ($ r)) -- | A test generator that returns an 'Integer' value between the -- specified (inclusive) bounds. chooseInteger :: (Integer, Integer) -> Gen Integer-chooseInteger r = Gen (asks genChooseInteger >>= lift . ($r))+chooseInteger r = Gen (asks genChooseInteger >>= lift . ($ r)) -- | A test generator that returns the current shrink size of the -- generator functionality.
src/What4/BaseTypes.hs view
@@ -311,6 +311,8 @@ ) ] )+instance Eq (BaseTypeRepr bt) where+ x == y = isJust (testEquality x y) instance OrdF BaseTypeRepr where compareF = $(structuralTypeOrd [t|BaseTypeRepr|]@@ -328,6 +330,8 @@ testEquality = $(structuralTypeEquality [t|FloatPrecisionRepr|] [(TypeApp (ConType [t|NatRepr|]) AnyType, [|testEquality|])] )+instance Eq (FloatPrecisionRepr fpp) where+ x == y = isJust (testEquality x y) instance OrdF FloatPrecisionRepr where compareF = $(structuralTypeOrd [t|FloatPrecisionRepr|] [(TypeApp (ConType [t|NatRepr|]) AnyType, [|compareF|])]@@ -335,5 +339,7 @@ instance TestEquality StringInfoRepr where testEquality = $(structuralTypeEquality [t|StringInfoRepr|] [])+instance Eq (StringInfoRepr si) where+ x == y = isJust (testEquality x y) instance OrdF StringInfoRepr where compareF = $(structuralTypeOrd [t|StringInfoRepr|] [])
src/What4/Concrete.hs view
@@ -49,6 +49,7 @@ import qualified Data.List as List import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map+import LibBF (BigFloat) import qualified Numeric as N import qualified Prettyprinter as PP @@ -68,6 +69,7 @@ ConcreteBool :: Bool -> ConcreteVal BaseBoolType ConcreteInteger :: Integer -> ConcreteVal BaseIntegerType ConcreteReal :: Rational -> ConcreteVal BaseRealType+ ConcreteFloat :: FloatPrecisionRepr fpp -> BigFloat -> ConcreteVal (BaseFloatType fpp) ConcreteString :: StringLiteral si -> ConcreteVal (BaseStringType si) ConcreteComplex :: Complex Rational -> ConcreteVal BaseComplexType ConcreteBV ::@@ -106,13 +108,14 @@ -- | Compute the type representative for a concrete value. concreteType :: ConcreteVal tp -> BaseTypeRepr tp concreteType = \case- ConcreteBool{} -> BaseBoolRepr- ConcreteInteger{} -> BaseIntegerRepr- ConcreteReal{} -> BaseRealRepr- ConcreteString s -> BaseStringRepr (stringLiteralInfo s)- ConcreteComplex{} -> BaseComplexRepr- ConcreteBV w _ -> BaseBVRepr w- ConcreteStruct xs -> BaseStructRepr (fmapFC concreteType xs)+ ConcreteBool{} -> BaseBoolRepr+ ConcreteInteger{} -> BaseIntegerRepr+ ConcreteReal{} -> BaseRealRepr+ ConcreteFloat fpp _ -> BaseFloatRepr fpp+ ConcreteString s -> BaseStringRepr (stringLiteralInfo s)+ ConcreteComplex{} -> BaseComplexRepr+ ConcreteBV w _ -> BaseBVRepr w+ ConcreteStruct xs -> BaseStructRepr (fmapFC concreteType xs) ConcreteArray idxTy def _ -> BaseArrayRepr idxTy (concreteType def) $(return [])@@ -123,6 +126,7 @@ , (ConType [t|Ctx.Assignment|] `TypeApp` AnyType `TypeApp` AnyType, [|testEqualityFC testEquality|]) , (ConType [t|ConcreteVal|] `TypeApp` AnyType, [|testEquality|]) , (ConType [t|StringLiteral|] `TypeApp` AnyType, [|testEquality|])+ , (ConType [t|FloatPrecisionRepr|] `TypeApp` AnyType, [|testEquality|]) , (ConType [t|Map|] `TypeApp` AnyType `TypeApp` AnyType, [|\x y -> if x == y then Just Refl else Nothing|]) ]) @@ -135,6 +139,7 @@ , (ConType [t|Ctx.Assignment|] `TypeApp` AnyType `TypeApp` AnyType, [|compareFC compareF|]) , (ConType [t|ConcreteVal|] `TypeApp` AnyType, [|compareF|]) , (ConType [t|StringLiteral|] `TypeApp` AnyType, [|compareF|])+ , (ConType [t|FloatPrecisionRepr|] `TypeApp` AnyType, [|compareF|]) , (ConType [t|Map|] `TypeApp` AnyType `TypeApp` AnyType, [|\x y -> fromOrdering (compare x y)|]) ]) @@ -151,6 +156,7 @@ ConcreteBool x -> PP.pretty x ConcreteInteger x -> PP.pretty x ConcreteReal x -> ppRational x+ ConcreteFloat _fpp bf -> PP.viaShow bf ConcreteString x -> PP.viaShow x ConcreteBV w x -> PP.pretty ("0x" ++ (N.showHex (BV.asUnsigned x) (":[" ++ show w ++ "]"))) ConcreteComplex (r :+ i) -> PP.pretty "complex(" PP.<> ppRational r PP.<> PP.pretty ", " PP.<> ppRational i PP.<> PP.pretty ")"
src/What4/Config.hs view
@@ -47,7 +47,7 @@ -- to install. A configuration may be later extended with additional -- options by using the `extendConfig` operation. ----- Example use (assuming the you wanted to use the z3 solver):+-- Example use (assuming you wanted to use the z3 solver): -- -- > import What4.Solver -- >@@ -66,14 +66,16 @@ -- (i.e., to undo extendConfig) -- ----- Note regarding concurrency: the configuration data structures in this--- module are implemented using MVars, and may safely be used in a multithreaded--- way; configuration changes made in one thread will be visible to others--- in a properly synchronized way. Of course, if one desires to isolate--- configuration changes in different threads from each other, separate--- configuration objects are required. As noted in the documentation for--- 'opt_onset', the validation procedures for options should not--- look up the value of other options, or deadlock may occur.+-- Note regarding concurrency: the configuration data structures in+-- this module are implemented using MVars, and may safely be used in+-- a multithreaded way; configuration changes made in one thread will+-- be visible to others in a properly synchronized way. Of course, if+-- one desires to isolate configuration changes in different threads+-- from each other, separate configuration objects are required. The+-- @splitConfig@ operation may be useful to partially isolate+-- configuration objects. As noted in the documentation for+-- 'opt_onset', the validation procedures for options should not look+-- up the value of other options, or deadlock may occur. ------------------------------------------------------------------------------ {-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-}@@ -150,6 +152,8 @@ , Config , initialConfig , extendConfig+ , tryExtendConfig+ , splitConfig , getOptionSetting , getOptionSettingFromText@@ -168,6 +172,7 @@ import Control.Applicative ( Const(..), (<|>) ) import Control.Concurrent.MVar+import qualified Control.Concurrent.ReadWriteVar as RWV import Control.Lens ((&)) import qualified Control.Lens.Combinators as LC import Control.Monad.Catch@@ -750,14 +755,25 @@ here = traverse (f (reverse (p:revPath))) +-- | Add an option to the given @ConfigMap@. If the+-- option cannot be added (because it already exists+-- in the map) the map is instead returned unchanged.+tryInsertOption ::+ (MonadIO m, MonadCatch m) =>+ ConfigMap -> ConfigDesc -> m ConfigMap+tryInsertOption m d =+ catch (insertOption m d)+ (\OptCreateFailure{} -> return 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 ::+ (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@@ -881,6 +897,7 @@ (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) =@@ -890,29 +907,47 @@ ------------------------------------------------------------------------ -- Config --- | The main configuration datatype. It consists of an MVar+-- | The main configuration datatype. It consists of a Read/Write var -- containing the actual configuration data.-newtype Config = Config (MVar ConfigMap)+newtype Config = Config (RWV.RWVar ConfigMap) -- | Construct a new configuration from the given configuration -- descriptions.-initialConfig :: Integer -- ^ Initial value for the `verbosity` option- -> [ConfigDesc] -- ^ Option descriptions to install- -> IO (Config)+initialConfig ::+ Integer {- ^ Initial value for the `verbosity` option -} ->+ [ConfigDesc] {- ^ Option descriptions to install -} ->+ IO (Config) initialConfig initVerbosity ts = do- cfg <- Config <$> newMVar Map.empty+ cfg <- Config <$> RWV.new Map.empty extendConfig (builtInOpts initVerbosity ++ ts) cfg return cfg -- | 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 :: [ConfigDesc] -> Config -> IO () extendConfig ts (Config cfg) =- modifyMVar_ cfg (\m -> foldM insertOption m ts)+ RWV.modify_ cfg (\m -> foldM insertOption m ts) ++-- | Extend an existing configuration with new options. If any+-- of the given options are already present in the configuration,+-- nothing is done for that option and it is silently skipped.+tryExtendConfig :: [ConfigDesc] -> Config -> IO ()+tryExtendConfig ts (Config cfg) =+ RWV.modify_ cfg (\m -> foldM tryInsertOption m ts)++-- | Create a new configuration object that shares the option+-- settings currently in the given input config. However,+-- any options added to either configuration using @extendConfig@+-- will not be propagated to the other.+--+-- Option settings that already exist in the input configuration+-- will be shared between both; changes to those options will be+-- visible in both configurations.+splitConfig :: Config -> IO Config+splitConfig (Config cfg) = Config <$> (RWV.with cfg RWV.new)+ -- | Verbosity of the simulator. This option controls how much -- informational and debugging output is generated. -- 0 yields low information output; 5 is extremely chatty.@@ -959,7 +994,7 @@ getOpt x = maybe (throwM $ OptGetFailure (OSet $ Some x) "not set") return =<< getMaybeOpt x --- | Throw an exception if the given @OptionSetResult@ indidcates+-- | Throw an exception if the given @OptionSetResult@ indicates -- an error. Otherwise, return any generated warnings. checkOptSetResult :: OptionSetting tp -> OptionSetResult -> IO [Doc Void] checkOptSetResult optset res =@@ -1050,7 +1085,8 @@ Config -> IO (OptionSetting tp) getOptionSetting o@(ConfigOption tp (p:|ps)) (Config cfg) =- readMVar cfg >>= getConst . adjustConfigMap p ps f+ RWV.with cfg (getConst . adjustConfigMap p ps f)+ where f Nothing = Const (throwM $ OptGetFailure (OCfg $ Some o) "not found") f (Just x) = Const (leafToSetting x)@@ -1082,7 +1118,7 @@ getOptionSettingFromText nm (Config cfg) = case splitPath nm of Nothing -> throwM $ OptGetFailure (OName "") "Illegal empty name for option"- Just (p:|ps) -> readMVar cfg >>= (getConst . adjustConfigMap p ps (f (p:|ps)))+ Just (p:|ps) -> RWV.with cfg (getConst . adjustConfigMap p ps (f (p:|ps))) where f (p:|ps) Nothing = Const (throwM $ OptGetFailure (OName (Text.intercalate "." (p:ps)))@@ -1111,7 +1147,7 @@ -- | Given the name of a subtree, return all--- the currently-set configurtion values in that subtree.+-- the currently-set configuration values in that subtree. -- -- If the subtree name is empty, the entire tree will be traversed. getConfigValues ::@@ -1119,8 +1155,8 @@ Config -> IO [ConfigValue] getConfigValues prefix (Config cfg) =- do m <- readMVar cfg- let ps = dropWhile Text.null $ Text.splitOn "." prefix+ RWV.with cfg $ \m ->+ do let ps = dropWhile Text.null $ Text.splitOn "." prefix f :: [Text] -> ConfigLeaf -> WriterT (Seq ConfigValue) IO ConfigLeaf f [] _ = throwM $ OptGetFailure (OName prefix) "illegal empty option prefix name"@@ -1158,8 +1194,8 @@ Config -> IO [Doc Void] configHelp prefix (Config cfg) =- do m <- readMVar cfg- let ps = dropWhile Text.null $ Text.splitOn "." prefix+ RWV.with cfg $ \m ->+ do 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)
src/What4/Expr.hs view
@@ -13,6 +13,16 @@ ( -- * Expression builder ExprBuilder , newExprBuilder+ , startCaching+ , stopCaching+ , userState+ , exprCounter+ , curProgramLoc+ , unaryThreshold+ , cacheStartSize+ , exprBuilderSplitConfig+ , exprBuilderFreshConfig+ , EmptyExprBuilderState(..) -- * Flags , FloatMode@@ -97,3 +107,9 @@ import What4.Expr.GroundEval import What4.Expr.WeightedSum import What4.Expr.UnaryBV+++-- | A \"dummy\" data type that can be used for the+-- user state field of an 'ExprBuilder' when there+-- is no other interesting state to track.+data EmptyExprBuilderState t = EmptyExprBuilderState
+ src/What4/Expr/Allocator.hs view
@@ -0,0 +1,201 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}++{-|+Module : What4.Expr.Allocator+Description : Expression allocators for controlling hash-consing+Copyright : (c) Galois Inc, 2015-2022+License : BSD3+Maintainer : rdockins@galois.com+-}+module What4.Expr.Allocator+( ExprAllocator(..)+, newStorage+, newCachedStorage++, cacheStartSizeOption+, cacheStartSizeDesc+, cacheTerms+, cacheOptDesc+) where++import Control.Lens ( (&) )+import Control.Monad.ST (stToIO)+import Data.IORef++import qualified Data.Parameterized.HashTable as PH+import Data.Parameterized.Nonce++import What4.BaseTypes+import What4.Concrete+import What4.Config as CFG+import What4.Expr.App+import What4.ProgramLoc+import What4.Utils.AbstractDomains++------------------------------------------------------------------------+-- Cache start size++-- | Starting size for element cache when caching is enabled.+-- The default value is 100000 elements.+--+-- This option is named \"backend.cache_start_size\"+cacheStartSizeOption :: ConfigOption BaseIntegerType+cacheStartSizeOption = configOption BaseIntegerRepr "backend.cache_start_size"++-- | The configuration option for setting the size of the initial hash set+-- used by simple builder (measured in number of elements).+cacheStartSizeDesc :: ConfigDesc+cacheStartSizeDesc = mkOpt cacheStartSizeOption sty help (Just (ConcreteInteger 100000))+ where sty = integerWithMinOptSty (CFG.Inclusive 0)+ help = Just "Starting size for element cache"++------------------------------------------------------------------------+-- Cache terms++-- | Indicates if we should cache terms. When enabled, hash-consing+-- is used to find and deduplicate common subexpressions.+-- Toggling this option from disabled to enabled will allocate a new+-- hash table; toggling it from enabled to disabled will discard+-- the current hash table. The default value for this option is `False`.+--+-- This option is named \"use_cache\"+cacheTerms :: ConfigOption BaseBoolType+cacheTerms = configOption BaseBoolRepr "use_cache"++cacheOptStyle ::+ NonceGenerator IO t ->+ IORef (ExprAllocator t) ->+ OptionSetting BaseIntegerType ->+ OptionStyle BaseBoolType+cacheOptStyle gen storageRef szSetting =+ boolOptSty & set_opt_onset+ (\mb b -> f (fmap fromConcreteBool mb) (fromConcreteBool b) >> return optOK)+ where+ f :: Maybe Bool -> Bool -> IO ()+ f mb b | mb /= Just b = if b then start else stop+ | otherwise = return ()++ stop = do s <- newStorage gen+ atomicWriteIORef storageRef s++ start = do sz <- getOpt szSetting+ s <- newCachedStorage gen (fromInteger sz)+ atomicWriteIORef storageRef s++cacheOptDesc ::+ NonceGenerator IO t ->+ IORef (ExprAllocator t) ->+ OptionSetting BaseIntegerType ->+ ConfigDesc+cacheOptDesc gen storageRef szSetting =+ mkOpt+ cacheTerms+ (cacheOptStyle gen storageRef szSetting)+ (Just "Use hash-consing during term construction")+ (Just (ConcreteBool False))+++------------------------------------------------------------------------+-- | ExprAllocator provides an interface for creating expressions from+-- an applications.+-- Parameter @t@ is a phantom type brand used to track nonces.+data ExprAllocator t+ = ExprAllocator { appExpr :: forall tp+ . ProgramLoc+ -> App (Expr t) tp+ -> AbstractValue tp+ -> IO (Expr t tp)+ , nonceExpr :: forall tp+ . ProgramLoc+ -> NonceApp t (Expr t) tp+ -> AbstractValue tp+ -> IO (Expr t tp)+ }+++------------------------------------------------------------------------+-- Uncached storage++-- | Create a new storage that does not do hash consing.+newStorage :: NonceGenerator IO t -> IO (ExprAllocator t)+newStorage g = do+ return $! ExprAllocator { appExpr = uncachedExprFn g+ , nonceExpr = uncachedNonceExpr g+ }++uncachedExprFn :: NonceGenerator IO t+ -> ProgramLoc+ -> App (Expr t) tp+ -> AbstractValue tp+ -> IO (Expr t tp)+uncachedExprFn g pc a v = do+ n <- freshNonce g+ return $! mkExpr n pc a v++uncachedNonceExpr :: NonceGenerator IO t+ -> ProgramLoc+ -> NonceApp t (Expr t) tp+ -> AbstractValue tp+ -> IO (Expr t tp)+uncachedNonceExpr g pc p v = do+ n <- freshNonce g+ return $! NonceAppExpr $ NonceAppExprCtor { nonceExprId = n+ , nonceExprLoc = pc+ , nonceExprApp = p+ , nonceExprAbsValue = v+ }++------------------------------------------------------------------------+-- Cached storage++cachedNonceExpr :: NonceGenerator IO t+ -> PH.HashTable PH.RealWorld (NonceApp t (Expr t)) (Expr t)+ -> ProgramLoc+ -> NonceApp t (Expr t) tp+ -> AbstractValue tp+ -> IO (Expr t tp)+cachedNonceExpr g h pc p v = do+ me <- stToIO $ PH.lookup h p+ case me of+ Just e -> return e+ Nothing -> do+ n <- freshNonce g+ let e = NonceAppExpr $ NonceAppExprCtor { nonceExprId = n+ , nonceExprLoc = pc+ , nonceExprApp = p+ , nonceExprAbsValue = v+ }+ seq e $ stToIO $ PH.insert h p e+ return e+++cachedAppExpr :: forall t tp+ . NonceGenerator IO t+ -> PH.HashTable PH.RealWorld (App (Expr t)) (Expr t)+ -> ProgramLoc+ -> App (Expr t) tp+ -> AbstractValue tp+ -> IO (Expr t tp)+cachedAppExpr g h pc a v = do+ me <- stToIO $ PH.lookup h a+ case me of+ Just e -> return e+ Nothing -> do+ n <- freshNonce g+ let e = mkExpr n pc a v+ seq e $ stToIO $ PH.insert h a e+ return e++-- | Create a storage that does hash consing.+newCachedStorage :: forall t+ . NonceGenerator IO t+ -> Int+ -> IO (ExprAllocator t)+newCachedStorage g sz = stToIO $ do+ appCache <- PH.newSized sz+ predCache <- PH.newSized sz+ return $ ExprAllocator { appExpr = cachedAppExpr g appCache+ , nonceExpr = cachedNonceExpr g predCache+ }+
src/What4/Expr/App.hs view
@@ -78,6 +78,7 @@ import What4.Interface import What4.ProgramLoc import qualified What4.SemiRing as SR+import qualified What4.SpecialFunctions as SFn import qualified What4.Expr.ArrayUpdateMap as AUM import What4.Expr.BoolMap (BoolMap, Polarity(..), BoolMapView(..), Wrap(..)) import qualified What4.Expr.BoolMap as BM@@ -157,6 +158,7 @@ newtype BVOrSet e w = BVOrSet (AM.AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()) + -- | Type @'App' e tp@ encodes the top-level application of an 'Expr' -- expression. It includes first-order expression forms that do not -- bind variables (contrast with 'NonceApp').@@ -234,16 +236,10 @@ ------------------------------------------------------------------------ -- Operations that introduce irrational numbers. - Pi :: App e BaseRealType-- RealSin :: !(e BaseRealType) -> App e BaseRealType- RealCos :: !(e BaseRealType) -> App e BaseRealType- RealATan2 :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType- RealSinh :: !(e BaseRealType) -> App e BaseRealType- RealCosh :: !(e BaseRealType) -> App e BaseRealType-- RealExp :: !(e BaseRealType) -> App e BaseRealType- RealLog :: !(e BaseRealType) -> App e BaseRealType+ RealSpecialFunction ::+ !(SFn.SpecialFunction args) ->+ !(SFn.SpecialFnArgs e BaseRealType args) ->+ App e (BaseRealType) -------------------------------- -- Bitvector operations@@ -498,6 +494,12 @@ -> App e (BaseBVType w) FloatToReal :: !(e (BaseFloatType fpp)) -> App e BaseRealType + FloatSpecialFunction ::+ !(FloatPrecisionRepr fpp) ->+ !(SFn.SpecialFunction args) ->+ !(SFn.SpecialFnArgs e (BaseFloatType fpp) args) ->+ App e (BaseFloatType fpp)+ ------------------------------------------------------------------------ -- Array operations @@ -529,6 +531,43 @@ -> !(Ctx.Assignment e (i::>tp)) -> App e b + CopyArray ::+ (1 <= w) =>+ !(NatRepr w) ->+ !(BaseTypeRepr a) ->+ !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) {- @dest_arr@ -} ->+ !(e (BaseBVType w)) {- @dest_idx@ -} ->+ !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) {- @src_arr@ -} ->+ !(e (BaseBVType w)) {- @src_idx@ -} ->+ !(e (BaseBVType w)) {- @len@ -} ->+ !(e (BaseBVType w)) {- @dest_idx + len@ -} ->+ !(e (BaseBVType w)) {- @src_idx + len@ -} ->+ App e (BaseArrayType (SingleCtx (BaseBVType w)) a)++ SetArray ::+ (1 <= w) =>+ !(NatRepr w) ->+ !(BaseTypeRepr a) ->+ !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) {- @arr@ -} ->+ !(e (BaseBVType w)) {- @idx@ -} ->+ !(e a) {- @val@ -}->+ !(e (BaseBVType w)) {- @len@ -} ->+ !(e (BaseBVType w)) {- @idx + len@ -} ->+ App e (BaseArrayType (SingleCtx (BaseBVType w)) a)++ EqualArrayRange ::+ (1 <= w) =>+ !(NatRepr w) ->+ !(BaseTypeRepr a) ->+ !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) {- @lhs_arr@ -} ->+ !(e (BaseBVType w)) {- @lhs_idx@ -} ->+ !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) {- @rhs_arr@ -} ->+ !(e (BaseBVType w)) {- @rhs_idx@ -} ->+ !(e (BaseBVType w)) {- @len@ -} ->+ !(e (BaseBVType w)) {- @lhs_idx + len@ -} ->+ !(e (BaseBVType w)) {- @rhs_idx + len@ -} ->+ App e BaseBoolType+ ------------------------------------------------------------------------ -- Conversions. @@ -776,8 +815,11 @@ , [| BM.traverseVars |] ) , ( ConType [t|Ctx.Assignment|] `TypeApp` AnyType `TypeApp` AnyType- , [|traverseFC|]+ , [| traverseFC |] )+ , ( ConType [t|SFn.SpecialFnArgs|] `TypeApp` AnyType `TypeApp` AnyType `TypeApp` AnyType+ , [| SFn.traverseSpecialFnArgs |]+ ) ] ) @@ -805,6 +847,8 @@ , [|testEquality|]) , (ConType [t|SR.OrderedSemiRingRepr|] `TypeApp` AnyType , [|testEquality|])+ , (ConType [t|SFn.SpecialFunction|] `TypeApp` AnyType+ , [|testEquality|]) , (ConType [t|WSum.WeightedSum|] `TypeApp` AnyType `TypeApp` AnyType , [|testEquality|]) , (ConType [t|SemiRingProduct|] `TypeApp` AnyType `TypeApp` AnyType@@ -847,23 +891,22 @@ IntDiv {} -> True IntMod {} -> True IntDivisible {} -> True+ RealDiv {} -> True RealSqrt {} -> True- RealSin {} -> True- RealCos {} -> True- RealATan2 {} -> True- RealSinh {} -> True- RealCosh {} -> True- RealExp {} -> True- RealLog {} -> True+ RealSpecialFunction{} -> True+ BVUdiv {} -> True BVUrem {} -> True BVSdiv {} -> True BVSrem {} -> True+ FloatSqrt {} -> True FloatMul {} -> True FloatDiv {} -> True FloatRem {} -> True+ FloatSpecialFunction{} -> True+ _ -> False @@ -894,7 +937,7 @@ ] ) -instance HashableF e => HashableF (NonceApp t e) where+instance (HashableF e, TestEquality e) => HashableF (NonceApp t e) where hashWithSaltF = $(structuralHashWithSalt [t|NonceApp|] [ (DataArg 1 `TypeApp` AnyType, [|hashWithSaltF|]) ]) @@ -1057,7 +1100,17 @@ printSymExpr = pretty + unsafeSetAbstractValue av e =+ case e of+ SemiRingLiteral{} -> e+ BoolExpr{} -> e+ FloatExpr{} -> e+ StringExpr{} -> e+ AppExpr ae -> AppExpr (ae{appExprAbsValue = av})+ NonceAppExpr nae -> NonceAppExpr (nae{nonceExprAbsValue = av})+ BoundVarExpr ebv -> BoundVarExpr (ebv{bvarAbstractValue = Just av}) + asSemiRingLit :: SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> Maybe (SR.Coefficient sr) asSemiRingLit sr (SemiRingLiteral sr' x _loc) | Just Refl <- testEquality sr sr'@@ -1655,6 +1708,9 @@ | otherwise = Nothing +instance Eq (ExprSymFn t args tp) where+ x == y = isJust (testExprSymFnEq x y)+ instance Hashable (ExprSymFn t args tp) where hashWithSalt s f = s `hashWithSalt` symFnId f @@ -1755,15 +1811,7 @@ FloorReal{} -> knownRepr CeilReal{} -> knownRepr - Pi -> knownRepr- RealSin{} -> knownRepr- RealCos{} -> knownRepr- RealATan2{} -> knownRepr- RealSinh{} -> knownRepr- RealCosh{} -> knownRepr-- RealExp{} -> knownRepr- RealLog{} -> knownRepr+ RealSpecialFunction{} -> knownRepr BVUnaryTerm u -> BaseBVRepr (UnaryBV.width u) BVOrBits w _ -> BaseBVRepr w@@ -1814,11 +1862,15 @@ FloatToBV w _ _ -> BaseBVRepr w FloatToSBV w _ _ -> BaseBVRepr w FloatToReal{} -> knownRepr+ FloatSpecialFunction fpp _ _ -> BaseFloatRepr fpp ArrayMap idx b _ _ -> BaseArrayRepr idx b ConstantArray idx b _ -> BaseArrayRepr idx b SelectArray b _ _ -> b UpdateArray b itp _ _ _ -> BaseArrayRepr itp b+ CopyArray w a_repr _ _ _ _ _ _ _ -> BaseArrayRepr (singleton (BaseBVRepr w)) a_repr+ SetArray w a_repr _ _ _ _ _ -> BaseArrayRepr (singleton (BaseBVRepr w)) a_repr+ EqualArrayRange _ _ _ _ _ _ _ _ _ -> knownRepr IntegerToReal{} -> knownRepr BVToInteger{} -> knownRepr@@ -1902,15 +1954,18 @@ RealDiv _ _ -> ravUnbounded RealSqrt _ -> ravUnbounded- Pi -> ravConcreteRange 3.14 3.15- RealSin _ -> ravConcreteRange (-1) 1- RealCos _ -> ravConcreteRange (-1) 1- RealATan2 _ _ -> ravUnbounded- RealSinh _ -> ravUnbounded- RealCosh _ -> ravUnbounded- RealExp _ -> ravUnbounded- RealLog _ -> ravUnbounded + RealSpecialFunction fn _ ->+ case fn of+ SFn.Pi -> ravConcreteRange 3.14 3.15+ -- TODO, other constants...++ SFn.Sin -> ravConcreteRange (-1) 1+ SFn.Cos -> ravConcreteRange (-1) 1++ -- TODO, is there other interesting range information?+ _ -> ravUnbounded+ BVUnaryTerm u -> UnaryBV.domain asConstantPred u BVConcat _ x y -> BVD.concat (bvWidth x) (f x) (bvWidth y) (f y) @@ -1963,6 +2018,7 @@ FloatToBV w _ _ -> BVD.any w FloatToSBV w _ _ -> BVD.any w FloatToReal{} -> ravUnbounded+ FloatSpecialFunction{} -> () ArrayMap _ bRepr m d -> withAbstractable bRepr $@@ -1973,6 +2029,11 @@ SelectArray _bRepr a _i -> f a -- FIXME? UpdateArray bRepr _ a _i v -> withAbstractable bRepr $ avJoin bRepr (f a) (f v)+ CopyArray _ a_repr dest_arr _dest_idx src_arr _src_idx _len _dest_end_idx _src_end_idx ->+ withAbstractable a_repr $ avJoin a_repr (f dest_arr) (f src_arr)+ SetArray _ a_repr arr _idx val _len _end_idx ->+ withAbstractable a_repr $ avJoin a_repr (f arr) (f val)+ EqualArrayRange{} -> Nothing IntegerToReal x -> RAV (mapRange toRational (f x)) (Just True) BVToInteger x -> valueRange (Inclusive lx) (Inclusive ux)@@ -2068,14 +2129,8 @@ RealDiv x y -> realDiv sym x y RealSqrt x -> realSqrt sym x - Pi -> realPi sym- RealSin x -> realSin sym x- RealCos x -> realCos sym x- RealATan2 y x -> realAtan2 sym y x- RealSinh x -> realSinh sym x- RealCosh x -> realCosh sym x- RealExp x -> realExp sym x- RealLog x -> realLog sym x+ RealSpecialFunction fn (SFn.SpecialFnArgs args) ->+ realSpecialFunction sym fn args BVOrBits w bs -> case bvOrToList bs of@@ -2133,12 +2188,19 @@ FloatToBV w r x -> floatToBV sym w r x FloatToSBV w r x -> floatToSBV sym w r x FloatToReal x -> floatToReal sym x+ FloatSpecialFunction fpp fn (SFn.SpecialFnArgs args) ->+ floatSpecialFunction sym fpp fn args ArrayMap _ _ m def_map -> arrayUpdateAtIdxLits sym m def_map ConstantArray idx_tp _ e -> constantArray sym idx_tp e SelectArray _ a i -> arrayLookup sym a i UpdateArray _ _ a i v -> arrayUpdate sym a i v+ CopyArray _ _ dest_arr dest_idx src_arr src_idx len _ _ ->+ arrayCopy sym dest_arr dest_idx src_arr src_idx len+ SetArray _ _ arr idx val len _ -> arraySet sym arr idx val len+ EqualArrayRange _ _ x_arr x_idx y_arr y_idx len _ _ ->+ arrayRangeEq sym x_arr x_idx y_arr y_idx len IntegerToReal x -> integerToReal sym x RealToInteger x -> realToInteger sym x@@ -2346,15 +2408,8 @@ RealDiv x y -> ppSExpr "divReal" [x, y] RealSqrt x -> ppSExpr "sqrt" [x] - Pi -> prettyApp "pi" []- RealSin x -> ppSExpr "sin" [x]- RealCos x -> ppSExpr "cos" [x]- RealATan2 x y -> ppSExpr "atan2" [x, y]- RealSinh x -> ppSExpr "sinh" [x]- RealCosh x -> ppSExpr "cosh" [x]-- RealExp x -> ppSExpr "exp" [x]- RealLog x -> ppSExpr "log" [x]+ RealSpecialFunction fn (SFn.SpecialFnArgs xs) ->+ prettyApp (Text.pack (show fn)) (toListFC (\ (SFn.SpecialFnArg x) -> exprPrettyArg x) xs) -------------------------------- -- Bitvector operations@@ -2417,6 +2472,8 @@ FloatToBV _ r x -> ppSExpr (Text.pack $ "floatToBV " <> show r) [x] FloatToSBV _ r x -> ppSExpr (Text.pack $ "floatToSBV " <> show r) [x] FloatToReal x -> ppSExpr "floatToReal " [x]+ FloatSpecialFunction _fpp fn (SFn.SpecialFnArgs args) ->+ prettyApp (Text.pack (show fn)) (toListFC (\ (SFn.SpecialFnArg x) -> exprPrettyArg x) args) ------------------------------------- -- Arrays@@ -2430,6 +2487,28 @@ prettyApp "select" (exprPrettyArg a : exprPrettyIndices i) UpdateArray _ _ a i v -> prettyApp "update" ([exprPrettyArg a] ++ exprPrettyIndices i ++ [exprPrettyArg v])+ CopyArray _ _ dest_arr dest_idx src_arr src_idx len _ _ ->+ prettyApp+ "arrayCopy"+ [ exprPrettyArg dest_arr+ , exprPrettyArg dest_idx+ , exprPrettyArg src_arr+ , exprPrettyArg src_idx+ , exprPrettyArg len+ ]+ SetArray _ _ arr idx val len _ ->+ prettyApp+ "arraySet"+ [exprPrettyArg arr, exprPrettyArg idx, exprPrettyArg val, exprPrettyArg len]+ EqualArrayRange _ _ x_arr x_idx y_arr y_idx len _ _ ->+ prettyApp+ "arrayRangeEq"+ [ exprPrettyArg x_arr+ , exprPrettyArg x_idx+ , exprPrettyArg y_arr+ , exprPrettyArg y_idx+ , exprPrettyArg len+ ] ------------------------------------------------------------------------ -- Conversions.
src/What4/Expr/AppTheory.hs view
@@ -16,8 +16,8 @@ , typeTheory ) where +import What4.Expr.App import What4.BaseTypes-import What4.Expr.Builder import qualified What4.SemiRing as SR import qualified What4.Expr.WeightedSum as WSum @@ -116,14 +116,7 @@ ---------------------------- -- Computable number operations- Pi -> ComputableArithTheory- RealSin{} -> ComputableArithTheory- RealCos{} -> ComputableArithTheory- RealATan2{} -> ComputableArithTheory- RealSinh{} -> ComputableArithTheory- RealCosh{} -> ComputableArithTheory- RealExp{} -> ComputableArithTheory- RealLog{} -> ComputableArithTheory+ RealSpecialFunction{} -> ComputableArithTheory ---------------------------- -- Bitvector operations@@ -179,6 +172,8 @@ FloatToSBV{} -> FloatingPointTheory FloatToReal{} -> FloatingPointTheory + FloatSpecialFunction{} -> ComputableArithTheory -- TODO? is this right?+ -------------------------------- -- Conversions. @@ -201,6 +196,9 @@ ConstantArray{} -> ArrayTheory SelectArray{} -> ArrayTheory UpdateArray{} -> ArrayTheory+ CopyArray{} -> ArrayTheory+ SetArray{} -> ArrayTheory+ EqualArrayRange{} -> ArrayTheory --------------------- -- String operations
src/What4/Expr/ArrayUpdateMap.hs view
@@ -65,7 +65,7 @@ instance TestEquality e => Eq (ArrayUpdateMap e ctx tp) where ArrayUpdateMap m1 == ArrayUpdateMap m2 = AM.eqBy (\ x y -> isJust $ testEquality x y) m1 m2 -instance Hashable (ArrayUpdateMap e ctx tp) where+instance TestEquality e => Hashable (ArrayUpdateMap e ctx tp) where hashWithSalt s (ArrayUpdateMap m) = case AM.annotation m of Nothing -> hashWithSalt s (111::Int)
src/What4/Expr/BoolMap.hs view
@@ -63,7 +63,7 @@ Wrap a == Wrap b = isJust $ testEquality a b instance OrdF f => Ord (Wrap f x) where compare (Wrap a) (Wrap b) = toOrdering $ compareF a b-instance HashableF f => Hashable (Wrap f x) where+instance (HashableF f, TestEquality f) => Hashable (Wrap f x) where hashWithSalt s (Wrap a) = hashWithSaltF s a -- | This data structure keeps track of a collection of expressions
src/What4/Expr/Builder.hs view
@@ -15,9 +15,10 @@ nonce values are generated atomically, and other IORefs used in this module are modified or written atomically, so modifications should propagate in the expected sequentially-consistent ways. Of course,-threads may still clobber state others have set (e.g., the current +threads may still clobber state others have set (e.g., the current program location) so the potential for truly multithreaded use is-somewhat limited.+somewhat limited. Consider the @exprBuilderFreshConfig@ or+@exprBuilderSplitConfig@ operations if this is a concern. -} {-# LANGUAGE CPP #-} {-# LANGUAGE BangPatterns #-}@@ -54,13 +55,14 @@ , sbMakeExpr , sbNonceExpr , curProgramLoc- , sbUnaryThreshold- , sbCacheStartSize- , sbBVDomainRangeLimit- , sbUserState+ , unaryThreshold+ , cacheStartSize+ , userState , exprCounter , startCaching , stopCaching+ , exprBuilderSplitConfig+ , exprBuilderFreshConfig -- * Specialized representations , bvUnary@@ -71,7 +73,6 @@ -- * configuration options , unaryThresholdOption- , bvdomainRangeLimitOption , cacheStartSizeOption , cacheTerms @@ -187,6 +188,7 @@ import Data.Bimap (Bimap) import qualified Data.Bimap as Bimap import qualified Data.Binary.IEEE754 as IEEE754+ import Data.Hashable import Data.IORef import Data.Kind@@ -211,11 +213,15 @@ import What4.BaseTypes import What4.Concrete import qualified What4.Config as CFG+import What4.FloatMode import What4.Interface import What4.InterpretedFloatingPoint import What4.ProgramLoc import qualified What4.SemiRing as SR+import qualified What4.SpecialFunctions as SFn import What4.Symbol++import What4.Expr.Allocator import What4.Expr.App import qualified What4.Expr.ArrayUpdateMap as AUM import What4.Expr.BoolMap (BoolMap, Polarity(..), BoolMapView(..))@@ -226,6 +232,7 @@ import qualified What4.Expr.StringSeq as SSeq import What4.Expr.UnaryBV (UnaryBV) import qualified What4.Expr.UnaryBV as UnaryBV+import qualified What4.Expr.VarIdentification as VI import What4.Utils.AbstractDomains import What4.Utils.Arithmetic@@ -317,81 +324,59 @@ ------------------------------------------------------------------------ -- ExprBuilder --- | Mode flag for how floating-point values should be interpreted.-data FloatMode where- FloatIEEE :: FloatMode- FloatUninterpreted :: FloatMode- FloatReal :: FloatMode-type FloatIEEE = 'FloatIEEE-type FloatUninterpreted = 'FloatUninterpreted-type FloatReal = 'FloatReal- data Flags (fi :: FloatMode) -data FloatModeRepr :: FloatMode -> Type where- FloatIEEERepr :: FloatModeRepr FloatIEEE- FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted- FloatRealRepr :: FloatModeRepr FloatReal--instance Show (FloatModeRepr fm) where- showsPrec _ FloatIEEERepr = showString "FloatIEEE"- showsPrec _ FloatUninterpretedRepr = showString "FloatUninterpreted"- showsPrec _ FloatRealRepr = showString "FloatReal"--instance ShowF FloatModeRepr--instance KnownRepr FloatModeRepr FloatIEEE where knownRepr = FloatIEEERepr-instance KnownRepr FloatModeRepr FloatUninterpreted where knownRepr = FloatUninterpretedRepr-instance KnownRepr FloatModeRepr FloatReal where knownRepr = FloatRealRepr--instance TestEquality FloatModeRepr where- testEquality FloatIEEERepr FloatIEEERepr = return Refl- testEquality FloatUninterpretedRepr FloatUninterpretedRepr = return Refl- testEquality FloatRealRepr FloatRealRepr = return Refl- testEquality _ _ = Nothing-- -- | Cache for storing dag terms. -- Parameter @t@ is a phantom type brand used to track nonces. data ExprBuilder t (st :: Type -> Type) (fs :: Type) = forall fm. (fs ~ (Flags fm)) => SB { sbTrue :: !(BoolExpr t) , sbFalse :: !(BoolExpr t)+ -- | Constant zero. , sbZero :: !(RealExpr t)+ -- | Configuration object for this symbolic backend , sbConfiguration :: !CFG.Config+ -- | Flag used to tell the backend whether to evaluate -- ground rational values as double precision floats when -- a function cannot be evaluated as a rational. , sbFloatReduce :: !Bool+ -- | The maximum number of distinct values a term may have and use the -- unary representation. , sbUnaryThreshold :: !(CFG.OptionSetting BaseIntegerType)- -- | The maximum number of distinct ranges in a BVDomain expression.- , sbBVDomainRangeLimit :: !(CFG.OptionSetting BaseIntegerType)+ -- | The starting size when building a new cache , sbCacheStartSize :: !(CFG.OptionSetting BaseIntegerType)+ -- | Counter to generate new unique identifiers for elements and functions.- , exprCounter :: !(NonceGenerator IO t)+ , sbExprCounter :: !(NonceGenerator IO t)+ -- | Reference to current allocator for expressions.- , curAllocator :: !(IORef (ExprAllocator t))+ , sbCurAllocator :: !(IORef (ExprAllocator t))+ -- | Number of times an 'Expr' for a non-linear operation has been -- created. , sbNonLinearOps :: !(IORef Integer)+ -- | The current program location , sbProgramLoc :: !(IORef ProgramLoc)- -- | Additional state maintained by the state manager++ -- | User-provided state , sbUserState :: !(st t) , sbVarBindings :: !(IORef (SymbolVarBimap t))+ , sbUninterpFnCache :: !(IORef (Map (SolverSymbol, Some (Ctx.Assignment BaseTypeRepr)) (SomeSymFn (ExprBuilder t st fs))))+ -- | Cache for Matlab functions- , sbMatlabFnCache- :: !(PH.HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))- , sbSolverLogger- :: !(IORef (Maybe (SolverEvent -> IO ())))+ , sbMatlabFnCache :: !(PH.HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))++ , sbSolverLogger :: !(IORef (Maybe (SolverEvent -> IO ())))+ -- | Flag dictating how floating-point values/operations are translated -- when passed to the solver. , sbFloatMode :: !(FloatModeRepr fm)@@ -402,109 +387,69 @@ type instance BoundVar (ExprBuilder t st fs) = ExprBoundVar t type instance SymAnnotation (ExprBuilder t st fs) = Nonce t ---------------------------------------------------------------------------- | ExprAllocator provides an interface for creating expressions from--- an applications.--- Parameter @t@ is a phantom type brand used to track nonces.-data ExprAllocator t- = ExprAllocator { appExpr :: forall tp- . ProgramLoc- -> App (Expr t) tp- -> AbstractValue tp- -> IO (Expr t tp)- , nonceExpr :: forall tp- . ProgramLoc- -> NonceApp t (Expr t) tp- -> AbstractValue tp- -> IO (Expr t tp)- }+exprCounter :: Getter (ExprBuilder t st fs) (NonceGenerator IO t)+exprCounter = to sbExprCounter +userState :: Lens' (ExprBuilder t st fs) (st t)+userState = lens sbUserState (\sym st -> sym{ sbUserState = st }) ---------------------------------------------------------------------------- Uncached storage+unaryThreshold :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseIntegerType)+unaryThreshold = to sbUnaryThreshold --- | Create a new storage that does not do hash consing.-newStorage :: NonceGenerator IO t -> IO (ExprAllocator t)-newStorage g = do- return $! ExprAllocator { appExpr = uncachedExprFn g- , nonceExpr = uncachedNonceExpr g- }+cacheStartSize :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseIntegerType)+cacheStartSize = to sbCacheStartSize -uncachedExprFn :: NonceGenerator IO t- -> ProgramLoc- -> App (Expr t) tp- -> AbstractValue tp- -> IO (Expr t tp)-uncachedExprFn g pc a v = do- n <- freshNonce g- return $! mkExpr n pc a v+-- | Return a new expr builder where the configuration object has+-- been "split" using the @splitConfig@ operation.+-- The returned sym will share any preexisting options with the+-- input sym, but any new options added with @extendConfig@+-- will not be shared. This may be useful if the expression builder+-- needs to be shared across threads, or sequentially for+-- separate use cases. Note, however, that hash consing settings,+-- solver loggers and the current program location will be shared.+exprBuilderSplitConfig :: ExprBuilder t st fs -> IO (ExprBuilder t st fs)+exprBuilderSplitConfig sym =+ do cfg' <- CFG.splitConfig (sbConfiguration sym)+ return sym{ sbConfiguration = cfg' } -uncachedNonceExpr :: NonceGenerator IO t- -> ProgramLoc- -> NonceApp t (Expr t) tp- -> AbstractValue tp- -> IO (Expr t tp)-uncachedNonceExpr g pc p v = do- n <- freshNonce g- return $! NonceAppExpr $ NonceAppExprCtor { nonceExprId = n- , nonceExprLoc = pc- , nonceExprApp = p- , nonceExprAbsValue = v- } ---------------------------------------------------------------------------- Cached storage--cachedNonceExpr :: NonceGenerator IO t- -> PH.HashTable RealWorld (NonceApp t (Expr t)) (Expr t)- -> ProgramLoc- -> NonceApp t (Expr t) tp- -> AbstractValue tp- -> IO (Expr t tp)-cachedNonceExpr g h pc p v = do- me <- stToIO $ PH.lookup h p- case me of- Just e -> return e- Nothing -> do- n <- freshNonce g- let e = NonceAppExpr $ NonceAppExprCtor { nonceExprId = n- , nonceExprLoc = pc- , nonceExprApp = p- , nonceExprAbsValue = v- }- seq e $ stToIO $ PH.insert h p e- return $! e-+-- | Return a new expr builder where all configuration settings have+-- been isolated from the original. The @Config@ object of the+-- output expr builder will have only the default options that are+-- installed via @newExprBuilder@, and configuration changes+-- to either expr builder will not be visible to the other.+-- This includes caching settings, the current program location,+-- and installed solver loggers.+exprBuilderFreshConfig :: ExprBuilder t st fs -> IO (ExprBuilder t st fs)+exprBuilderFreshConfig sym =+ do let gen = sbExprCounter sym+ es <- newStorage gen -cachedAppExpr :: forall t tp- . NonceGenerator IO t- -> PH.HashTable RealWorld (App (Expr t)) (Expr t)- -> ProgramLoc- -> App (Expr t) tp- -> AbstractValue tp- -> IO (Expr t tp)-cachedAppExpr g h pc a v = do- me <- stToIO $ PH.lookup h a- case me of- Just e -> return e- Nothing -> do- n <- freshNonce g- let e = mkExpr n pc a v- seq e $ stToIO $ PH.insert h a e- return e+ loc_ref <- newIORef initializationLoc+ storage_ref <- newIORef es+ logger_ref <- newIORef Nothing+ bindings_ref <- newIORef =<< readIORef (sbVarBindings sym) --- | Create a storage that does hash consing.-newCachedStorage :: forall t- . NonceGenerator IO t- -> Int- -> IO (ExprAllocator t)-newCachedStorage g sz = stToIO $ do- appCache <- PH.newSized sz- predCache <- PH.newSized sz- return $ ExprAllocator { appExpr = cachedAppExpr g appCache- , nonceExpr = cachedNonceExpr g predCache- }+ -- Set up configuration options+ cfg <- CFG.initialConfig 0+ [ unaryThresholdDesc+ , cacheStartSizeDesc+ ]+ unarySetting <- CFG.getOptionSetting unaryThresholdOption cfg+ cacheStartSetting <- CFG.getOptionSetting cacheStartSizeOption cfg+ CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg+ nonLinearOps <- newIORef 0 + return sym { sbConfiguration = cfg+ , sbFloatReduce = True+ , sbUnaryThreshold = unarySetting+ , sbCacheStartSize = cacheStartSetting+ , sbProgramLoc = loc_ref+ , sbCurAllocator = storage_ref+ , sbNonLinearOps = nonLinearOps+ , sbVarBindings = bindings_ref+ , sbSolverLogger = logger_ref+ } ------------------------------------------------------------------------ -- IdxCache@@ -603,7 +548,7 @@ -> NonceApp t (Expr t) tp -> IO (Expr t tp) sbNonceExpr sym a = do- s <- readIORef (curAllocator sym)+ s <- readIORef (sbCurAllocator sym) pc <- curProgramLoc sym nonceExpr s pc a (quantAbsEval exprAbsValue a) @@ -617,7 +562,7 @@ sbMakeExpr :: ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp) sbMakeExpr sym a = do- s <- readIORef (curAllocator sym)+ s <- readIORef (sbCurAllocator sym) pc <- curProgramLoc sym let v = abstractEval exprAbsValue a when (isNonLinearApp a) $@@ -661,10 +606,10 @@ -- | Create fresh index sbFreshIndex :: ExprBuilder t st fs -> IO (Nonce t (tp::BaseType))-sbFreshIndex sb = freshNonce (exprCounter sb)+sbFreshIndex sb = freshNonce (sbExprCounter sb) sbFreshSymFnNonce :: ExprBuilder t st fs -> IO (Nonce t (ctx:: Ctx BaseType))-sbFreshSymFnNonce sb = freshNonce (exprCounter sb)+sbFreshSymFnNonce sb = freshNonce (sbExprCounter sb) ------------------------------------------------------------------------ -- Configuration option for controlling the maximum number of value a unary@@ -683,80 +628,8 @@ where sty = CFG.integerWithMinOptSty (CFG.Inclusive 0) help = Just "Maximum number of values in unary bitvector encoding." ---------------------------------------------------------------------------- Configuration option for controlling how many disjoint ranges--- should be allowed in bitvector domains. --- | Maximum number of ranges in bitvector abstract domains.------ This option is named \"backend.bvdomain_range_limit\"-bvdomainRangeLimitOption :: CFG.ConfigOption BaseIntegerType-bvdomainRangeLimitOption = CFG.configOption BaseIntegerRepr "backend.bvdomain_range_limit" -bvdomainRangeLimitDesc :: CFG.ConfigDesc-bvdomainRangeLimitDesc = CFG.mkOpt bvdomainRangeLimitOption sty help (Just (ConcreteInteger 2))- where sty = CFG.integerWithMinOptSty (CFG.Inclusive 0)- help = Just "Maximum number of ranges in bitvector domains."----------------------------------------------------------------------------- Cache start size---- | Starting size for element cache when caching is enabled.------ This option is named \"backend.cache_start_size\"-cacheStartSizeOption :: CFG.ConfigOption BaseIntegerType-cacheStartSizeOption = CFG.configOption BaseIntegerRepr "backend.cache_start_size"---- | The configuration option for setting the size of the initial hash set--- used by simple builder-cacheStartSizeDesc :: CFG.ConfigDesc-cacheStartSizeDesc = CFG.mkOpt cacheStartSizeOption sty help (Just (ConcreteInteger 100000))- where sty = CFG.integerWithMinOptSty (CFG.Inclusive 0)- help = Just "Starting size for element cache"----------------------------------------------------------------------------- Cache terms---- | Indicates if we should cache terms. When enabled, hash-consing--- is used to find and deduplicate common subexpressions.------ This option is named \"use_cache\"-cacheTerms :: CFG.ConfigOption BaseBoolType-cacheTerms = CFG.configOption BaseBoolRepr "use_cache"--cacheOptStyle ::- NonceGenerator IO t ->- IORef (ExprAllocator t) ->- CFG.OptionSetting BaseIntegerType ->- CFG.OptionStyle BaseBoolType-cacheOptStyle gen storageRef szSetting =- CFG.boolOptSty & CFG.set_opt_onset- (\mb b -> f (fmap fromConcreteBool mb) (fromConcreteBool b) >> return CFG.optOK)- where- f :: Maybe Bool -> Bool -> IO ()- f mb b | mb /= Just b = if b then start else stop- | otherwise = return ()-- stop = do s <- newStorage gen- atomicWriteIORef storageRef s-- start = do sz <- CFG.getOpt szSetting- s <- newCachedStorage gen (fromInteger sz)- atomicWriteIORef storageRef s--cacheOptDesc ::- NonceGenerator IO t ->- IORef (ExprAllocator t) ->- CFG.OptionSetting BaseIntegerType ->- CFG.ConfigDesc-cacheOptDesc gen storageRef szSetting =- CFG.mkOpt- cacheTerms- (cacheOptStyle gen storageRef szSetting)- (Just "Use hash-consing during term construction")- (Just (ConcreteBool False))-- newExprBuilder :: FloatModeRepr fm -- ^ Float interpretation mode (i.e., how are floats translated for the solver).@@ -782,11 +655,9 @@ -- Set up configuration options cfg <- CFG.initialConfig 0 [ unaryThresholdDesc- , bvdomainRangeLimitDesc , cacheStartSizeDesc ] unarySetting <- CFG.getOptionSetting unaryThresholdOption cfg- domainRangeSetting <- CFG.getOptionSetting bvdomainRangeLimitOption cfg cacheStartSetting <- CFG.getOptionSetting cacheStartSizeOption cfg CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg nonLinearOps <- newIORef 0@@ -797,11 +668,10 @@ , sbConfiguration = cfg , sbFloatReduce = True , sbUnaryThreshold = unarySetting- , sbBVDomainRangeLimit = domainRangeSetting , sbCacheStartSize = cacheStartSetting , sbProgramLoc = loc_ref- , exprCounter = gen- , curAllocator = storage_ref+ , sbExprCounter = gen+ , sbCurAllocator = storage_ref , sbNonLinearOps = nonLinearOps , sbUserState = st , sbVarBindings = bindings_ref@@ -818,15 +688,15 @@ -- | Stop caching applications in backend. stopCaching :: ExprBuilder t st fs -> IO () stopCaching sb = do- s <- newStorage (exprCounter sb)- atomicWriteIORef (curAllocator sb) s+ s <- newStorage (sbExprCounter sb)+ atomicWriteIORef (sbCurAllocator sb) s -- | Restart caching applications in backend (clears cache if it is currently caching). startCaching :: ExprBuilder t st fs -> IO () startCaching sb = do sz <- CFG.getOpt (sbCacheStartSize sb)- s <- newCachedStorage (exprCounter sb) (fromInteger sz)- atomicWriteIORef (curAllocator sb) s+ s <- newCachedStorage (sbExprCounter sb) (fromInteger sz)+ atomicWriteIORef (sbCurAllocator sb) s bvBinDivOp :: (1 <= w) => (NatRepr w -> BV.BV w -> BV.BV w -> BV.BV w)@@ -1087,11 +957,77 @@ -- Lookups on constant arrays just return value | Just (ConstantArray _ _ v) <- asApp arr0 = do return v- -- Lookups on mux arrays just distribute over mux.- | Just (BaseIte _ _ p x y) <- asApp arr0 = do- xv <- sbConcreteLookup sym x mcidx idx- yv <- sbConcreteLookup sym y mcidx idx- baseTypeIte sym p xv yv++ -- A lookup in an array update with symbolic update index is (i) the update+ -- value when the difference between the lookup index and the update index+ -- is zero, or (ii) a lookup in the update base array when the difference+ -- is a concrete non-zero number. Computing the difference instead of+ -- checking equality is more accurate because it enables the semi-rings and+ -- abstract domains simplifications (for example, `x` - `x + 1` simplifies+ -- to `1`)+ | Just (UpdateArray range idx_tps arr update_idx v) <- asApp arr0+ , Ctx.Empty Ctx.:> BaseBVRepr{} <- idx_tps+ , Ctx.Empty Ctx.:> idx0 <- idx+ , Ctx.Empty Ctx.:> update_idx0 <- update_idx = do+ diff <- bvSub sym idx0 update_idx0+ is_diff_zero <- bvEq sym diff =<< bvLit sym (bvWidth diff) (BV.zero (bvWidth diff))+ case asConstantPred is_diff_zero of+ Just True -> return v+ Just False -> sbConcreteLookup sym arr mcidx idx+ _ -> do+ (sliced_arr, sliced_idx) <- sliceArrayLookupUpdate sym arr0 idx+ sbMakeExpr sym (SelectArray range sliced_arr sliced_idx)++ -- A lookup in an array copy is a lookup in the src array when inside the copy range+ | Just (CopyArray w _a_repr _dest_arr dest_begin_idx src_arr src_begin_idx _len dest_end_idx _src_end_idx) <- asApp arr0+ , Just (Empty :> (BVIndexLit _ lookup_idx_bv)) <- mcidx+ , lookup_idx_unsigned <- BV.asUnsigned lookup_idx_bv+ , Just dest_begin_idx_unsigned <- BV.asUnsigned <$> asBV dest_begin_idx+ , Just dest_end_idx_unsigned <- BV.asUnsigned <$> asBV dest_end_idx+ , dest_begin_idx_unsigned <= lookup_idx_unsigned+ , lookup_idx_unsigned < dest_end_idx_unsigned = do+ new_lookup_idx <- bvAdd sym src_begin_idx =<<+ (bvLit sym w $ BV.mkBV w $ lookup_idx_unsigned - dest_begin_idx_unsigned)+ arrayLookup sym src_arr $ singleton new_lookup_idx+ -- A lookup in an array copy is a lookup in the dest array when outside the copy range+ | Just (CopyArray _w _a_repr dest_arr dest_begin_idx _src_arr _src_begin_idx _len _dest_end_idx _src_end_idx) <- asApp arr0+ , Just (Empty :> (BVIndexLit _ lookup_idx_bv)) <- mcidx+ , lookup_idx_unsigned <- BV.asUnsigned lookup_idx_bv+ , Just dest_begin_idx_unsigned <- BV.asUnsigned <$> asBV dest_begin_idx+ , lookup_idx_unsigned < dest_begin_idx_unsigned =+ sbConcreteLookup sym dest_arr mcidx idx+ -- A lookup in an array copy is a lookup in the dest array when outside the copy range+ | Just (CopyArray _w _a_repr dest_arr _dest_begin_idx _src_arr _src_begin_idx _len dest_end_idx _src_end_idx) <- asApp arr0+ , Just (Empty :> (BVIndexLit _ lookup_idx_bv)) <- mcidx+ , lookup_idx_unsigned <- BV.asUnsigned lookup_idx_bv+ , Just dest_end_idx_unsigned <- BV.asUnsigned <$> asBV dest_end_idx+ , dest_end_idx_unsigned <= lookup_idx_unsigned =+ sbConcreteLookup sym dest_arr mcidx idx++ -- A lookup in an array set returns the value when inside the set range+ | Just (SetArray _w _a_repr _arr begin_idx val _len end_idx) <- asApp arr0+ , Just (Empty :> (BVIndexLit _ lookup_idx_bv)) <- mcidx+ , lookup_idx_unsigned <- BV.asUnsigned lookup_idx_bv+ , Just begin_idx_unsigned <- BV.asUnsigned <$> asBV begin_idx+ , Just end_idx_unsigned <- BV.asUnsigned <$> asBV end_idx+ , begin_idx_unsigned <= lookup_idx_unsigned+ , lookup_idx_unsigned < end_idx_unsigned =+ return val+ -- A lookup in an array set is a lookup in the inner array when outside the set range+ | Just (SetArray _w _a_repr arr begin_idx _val _len _end_idx) <- asApp arr0+ , Just (Empty :> (BVIndexLit _ lookup_idx_bv)) <- mcidx+ , lookup_idx_unsigned <- BV.asUnsigned lookup_idx_bv+ , Just begin_idx_unsigned <- BV.asUnsigned <$> asBV begin_idx+ , lookup_idx_unsigned < begin_idx_unsigned =+ sbConcreteLookup sym arr mcidx idx+ -- A lookup in an array set is a lookup in the inner array when outside the set range+ | Just (SetArray _w _a_repr arr _begin_idx _val _len end_idx) <- asApp arr0+ , Just (Empty :> (BVIndexLit _ lookup_idx_bv)) <- mcidx+ , lookup_idx_unsigned <- BV.asUnsigned lookup_idx_bv+ , Just end_idx_unsigned <- BV.asUnsigned <$> asBV end_idx+ , end_idx_unsigned <= lookup_idx_unsigned =+ sbConcreteLookup sym arr mcidx idx+ | Just (MapOverArrays f _ args) <- asNonceApp arr0 = do let eval :: ArrayResultWrapper (Expr t) (d::>tp) utp -> IO (Expr t utp)@@ -1100,9 +1036,96 @@ -- Create select index. | otherwise = do case exprType arr0 of- BaseArrayRepr _ range ->- sbMakeExpr sym (SelectArray range arr0 idx)+ BaseArrayRepr _ range -> do+ (sliced_arr, sliced_idx) <- sliceArrayLookupUpdate sym arr0 idx+ sbMakeExpr sym (SelectArray range sliced_arr sliced_idx) +-- | Simplify an array lookup expression by slicing the array w.r.t. the index.+--+-- Remove array update, copy and set operations at indices that are different+-- from the lookup index.+sliceArrayLookupUpdate ::+ ExprBuilder t st fs ->+ Expr t (BaseArrayType (d::>tp) range) ->+ Ctx.Assignment (Expr t) (d::>tp) ->+ IO (Expr t (BaseArrayType (d::>tp) range), Ctx.Assignment (Expr t) (d::>tp))+sliceArrayLookupUpdate sym arr0 lookup_idx+ | Just (ArrayMap _ _ entry_map arr) <- asApp arr0 =+ case asConcreteIndices lookup_idx of+ Just lookup_concrete_idx ->+ case AUM.lookup lookup_concrete_idx entry_map of+ Just val -> do+ arr_base <- arrayUpdateBase sym arr+ sliced_arr <- arrayUpdate sym arr_base lookup_idx val+ return (sliced_arr, lookup_idx)+ Nothing -> sliceArrayLookupUpdate sym arr lookup_idx+ Nothing ->+ return (arr0, lookup_idx)++ | Just (CopyArray _w _a_repr dest_arr dest_begin_idx src_arr src_begin_idx len dest_end_idx _src_end_idx) <- asApp arr0 = do+ p0 <- bvUle sym dest_begin_idx (Ctx.last lookup_idx)+ p1 <- bvUlt sym (Ctx.last lookup_idx) dest_end_idx+ case (asConstantPred p0, asConstantPred p1) of+ (Just True, Just True) -> do+ new_lookup_idx <- bvAdd sym src_begin_idx =<<+ bvSub sym (Ctx.last lookup_idx) dest_begin_idx+ sliceArrayLookupUpdate sym src_arr $ singleton new_lookup_idx+ (Just False, _) ->+ sliceArrayLookupUpdate sym dest_arr lookup_idx+ (_, Just False) ->+ sliceArrayLookupUpdate sym dest_arr lookup_idx+ _ -> do+ (sliced_dest_arr, sliced_dest_idx) <- sliceArrayLookupUpdate sym dest_arr lookup_idx+ sliced_dest_begin_idx <- bvAdd sym dest_begin_idx =<<+ bvSub sym (Ctx.last sliced_dest_idx) (Ctx.last lookup_idx)+ sliced_arr <- arrayCopy sym sliced_dest_arr sliced_dest_begin_idx src_arr src_begin_idx len+ return (sliced_arr, sliced_dest_idx)++ -- A lookup in an array set returns the value when inside the set range+ | Just (SetArray _w _a_repr arr begin_idx val len end_idx) <- asApp arr0 = do+ p0 <- bvUle sym begin_idx (Ctx.last lookup_idx)+ p1 <- bvUlt sym (Ctx.last lookup_idx) end_idx+ case (asConstantPred p0, asConstantPred p1) of+ (Just True, Just True) -> do+ arr_base <- arrayUpdateBase sym arr+ sliced_arr <- arrayUpdate sym arr_base lookup_idx val+ return (sliced_arr, lookup_idx)+ (Just False, _) ->+ sliceArrayLookupUpdate sym arr lookup_idx+ (_, Just False) ->+ sliceArrayLookupUpdate sym arr lookup_idx+ _ -> do+ (sliced_arr, sliced_idx) <- sliceArrayLookupUpdate sym arr lookup_idx+ sliced_begin_idx <- bvAdd sym begin_idx =<<+ bvSub sym (Ctx.last sliced_idx) (Ctx.last lookup_idx)+ sliced_arr' <- arraySet sym sliced_arr sliced_begin_idx val len+ return (sliced_arr', sliced_idx)++ -- Lookups on mux arrays just distribute over mux.+ | Just (BaseIte _ _ p x y) <- asApp arr0 = do+ (x', i') <- sliceArrayLookupUpdate sym x lookup_idx+ (y', j') <- sliceArrayLookupUpdate sym y lookup_idx+ sliced_arr <- baseTypeIte sym p x' y'+ sliced_idx <- Ctx.zipWithM (baseTypeIte sym p) i' j'+ return (sliced_arr, sliced_idx)++ | otherwise = return (arr0, lookup_idx)++arrayUpdateBase ::+ ExprBuilder t st fs ->+ Expr t (BaseArrayType (d::>tp) range) ->+ IO (Expr t (BaseArrayType (d::>tp) range))+arrayUpdateBase sym arr0 = case asApp arr0 of+ Just (UpdateArray _ _ arr _ _) -> arrayUpdateBase sym arr+ Just (ArrayMap _ _ _ arr) -> arrayUpdateBase sym arr+ Just (CopyArray _ _ arr _ _ _ _ _ _) -> arrayUpdateBase sym arr+ Just (SetArray _ _ arr _ _ _ _) -> arrayUpdateBase sym arr+ Just (BaseIte _ _ p x y) -> do+ x' <- arrayUpdateBase sym x+ y' <- arrayUpdateBase sym y+ baseTypeIte sym p x' y'+ _ -> return arr0+ ---------------------------------------------------------------------- -- Expression builder instances @@ -1583,7 +1606,7 @@ Just f -> f ev getStatistics sb = do- allocs <- countNoncesGenerated (exprCounter sb)+ allocs <- countNoncesGenerated (sbExprCounter sb) nonLinearOps <- readIORef (sbNonLinearOps sb) return $ Statistics { statAllocs = allocs , statNonLinearOps = nonLinearOps }@@ -1602,6 +1625,11 @@ NonceAppExpr (nonceExprApp -> Annotation _ n _) -> Just n _ -> Nothing + getUnannotatedTerm _sym e =+ case e of+ NonceAppExpr (nonceExprApp -> Annotation _ _ x) -> Just x+ _ -> Nothing+ ---------------------------------------------------------------------- -- Program location operations @@ -2910,6 +2938,22 @@ arrayLookup sym arr idx = sbConcreteLookup sym arr (asConcreteIndices idx) idx + arrayCopy sym dest_arr dest_idx src_arr src_idx len = case exprType dest_arr of+ (BaseArrayRepr _ a_repr) -> do+ dest_end_idx <- bvAdd sym dest_idx len+ src_end_idx <- bvAdd sym src_idx len+ sbMakeExpr sym (CopyArray (bvWidth dest_idx) a_repr dest_arr dest_idx src_arr src_idx len dest_end_idx src_end_idx)++ arraySet sym arr idx val len = do+ end_idx <- bvAdd sym idx len+ sbMakeExpr sym (SetArray (bvWidth idx) (exprType val) arr idx val len end_idx)++ arrayRangeEq sym x_arr x_idx y_arr y_idx len = case exprType x_arr of+ (BaseArrayRepr _ a_repr) -> do+ x_end_idx <- bvAdd sym x_idx len+ y_end_idx <- bvAdd sym y_idx len+ sbMakeExpr sym (EqualArrayRange (bvWidth x_idx) a_repr x_arr x_idx y_arr y_idx len x_end_idx y_end_idx)+ -- | Create an array from a map of concrete indices to values. arrayUpdateAtIdxLits sym m def_map = do BaseArrayRepr idx_tps baseRepr <- return $ exprType def_map@@ -3168,52 +3212,49 @@ | sbFloatReduce sym -> realLit sym (toRational (sqrt_dbl (fromRational r))) _ -> sbMakeExpr sym (RealSqrt x) - realPi sym = do- if sbFloatReduce sym then- realLit sym (toRational (pi :: Double))- else- sbMakeExpr sym Pi-- realSin sym x =- case asRational x of- Just 0 -> realLit sym 0- Just c | sbFloatReduce sym -> realLit sym (toRational (sin (toDouble c)))- _ -> sbMakeExpr sym (RealSin x)-- realCos sym x =- case asRational x of- Just 0 -> realLit sym 1- Just c | sbFloatReduce sym -> realLit sym (toRational (cos (toDouble c)))- _ -> sbMakeExpr sym (RealCos x)-- realAtan2 sb y x = do- case (asRational y, asRational x) of- (Just 0, _) -> realLit sb 0- (Just yc, Just xc) | xc /= 0, sbFloatReduce sb -> do- realLit sb (toRational (atan2 (toDouble yc) (toDouble xc)))- _ -> sbMakeExpr sb (RealATan2 y x)+ realSpecialFunction sym fn Empty+ | sbFloatReduce sym =+ case fn of+ SFn.Pi -> realLit sym (toRational (pi :: Double))+ -- TODO, other constants - realSinh sb x =- case asRational x of- Just 0 -> realLit sb 0- Just c | sbFloatReduce sb -> realLit sb (toRational (sinh (toDouble c)))- _ -> sbMakeExpr sb (RealSinh x)+ _ -> sbMakeExpr sym (RealSpecialFunction fn (SFn.SpecialFnArgs Empty)) - realCosh sb x =- case asRational x of- Just 0 -> realLit sb 1- Just c | sbFloatReduce sb -> realLit sb (toRational (cosh (toDouble c)))- _ -> sbMakeExpr sb (RealCosh x)+ realSpecialFunction sym fn args@(Empty :> SFn.SpecialFnArg x)+ | Just c <- asRational x =+ case fn of+ SFn.Sin+ | c == 0 -> realLit sym 0+ | sbFloatReduce sym -> realLit sym (toRational (sin (toDouble c)))+ SFn.Cos+ | c == 0 -> realLit sym 1+ | sbFloatReduce sym -> realLit sym (toRational (cos (toDouble c)))+ SFn.Sinh+ | c == 0 -> realLit sym 0+ | sbFloatReduce sym -> realLit sym (toRational (sinh (toDouble c)))+ SFn.Cosh+ | c == 0 -> realLit sym 1+ | sbFloatReduce sym -> realLit sym (toRational (cosh (toDouble c)))+ SFn.Exp+ | c == 0 -> realLit sym 1+ | sbFloatReduce sym -> realLit sym (toRational (exp (toDouble c)))+ SFn.Log+ | c > 0, sbFloatReduce sym -> realLit sym (toRational (log (toDouble c)))+ _ -> sbMakeExpr sym (RealSpecialFunction fn (SFn.SpecialFnArgs args)) - realExp sym x- | Just 0 <- asRational x = realLit sym 1- | Just c <- asRational x, sbFloatReduce sym = realLit sym (toRational (exp (toDouble c)))- | otherwise = sbMakeExpr sym (RealExp x)+ realSpecialFunction sym fn args@(Empty :> SFn.SpecialFnArg x :> SFn.SpecialFnArg y)+ | Just xc <- asRational x,+ Just yc <- asRational y =+ case fn of+ SFn.Arctan2+ | sbFloatReduce sym -> realLit sym (toRational (atan2 (toDouble xc) (toDouble yc)))+ SFn.Pow+ | yc == 0 -> realLit sym 1+ | sbFloatReduce sym ->+ realLit sym (toRational (toDouble xc ** toDouble yc))+ _ -> sbMakeExpr sym (RealSpecialFunction fn (SFn.SpecialFnArgs args)) - realLog sym x =- case asRational x of- Just c | c > 0, sbFloatReduce sym -> realLit sym (toRational (log (toDouble c)))- _ -> sbMakeExpr sym (RealLog x)+ realSpecialFunction sym fn args = sbMakeExpr sym (RealSpecialFunction fn (SFn.SpecialFnArgs args)) ---------------------------------------------------------------------- -- IEEE-754 floating-point operations@@ -3414,6 +3455,9 @@ | otherwise = sbMakeExpr sym (FloatToReal x) + floatSpecialFunction sym fpp fn args =+ sbMakeExpr sym (FloatSpecialFunction fpp fn (SFn.SpecialFnArgs args))+ ---------------------------------------------------------------------- -- Cplx operations @@ -3604,6 +3648,7 @@ iFloatToBV sym w _ x = realToBV sym x w iFloatToSBV sym w _ x = realToSBV sym x w iFloatToReal _ = return+ iFloatSpecialFunction sym _ fn args = realSpecialFunction sym fn args iFloatBaseTypeRepr _ _ = knownRepr type instance SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi =@@ -3684,6 +3729,10 @@ "uninterpreted_float_to_real" (Ctx.empty Ctx.:> x) knownRepr++ iFloatSpecialFunction sym fi fn args =+ floatUninterpSpecialFn sym (iFloatBaseTypeRepr sym fi) fn args+ iFloatBaseTypeRepr _ = floatInfoToBVTypeRepr floatUninterpArithBinOp@@ -3692,6 +3741,31 @@ let ret_type = exprType x in mkUninterpFnApp sym fn (Ctx.empty Ctx.:> x Ctx.:> y) ret_type +floatUninterpSpecialFn+ :: (e ~ Expr t)+ => ExprBuilder t sf tfs+ -> BaseTypeRepr bt+ -> SFn.SpecialFunction args+ -> Assignment (SFn.SpecialFnArg e bt) args+ -> IO (e bt)+floatUninterpSpecialFn sym btr fn Ctx.Empty =+ do fn_name <- unsafeUserSymbol ("uninterpreted_" ++ show fn)+ fn' <- cachedUninterpFn sym fn_name Ctx.Empty btr freshTotalUninterpFn+ applySymFn sym fn' Ctx.Empty++floatUninterpSpecialFn sym btr fn (Ctx.Empty Ctx.:> SFn.SpecialFnArg x) =+ do fn_name <- unsafeUserSymbol ("uninterpreted_" ++ show fn)+ fn' <- cachedUninterpFn sym fn_name (Ctx.Empty Ctx.:> btr) btr freshTotalUninterpFn+ applySymFn sym fn' (Ctx.Empty Ctx.:> x)++floatUninterpSpecialFn sym btr fn (Ctx.Empty Ctx.:> SFn.SpecialFnArg x Ctx.:> SFn.SpecialFnArg y) =+ do fn_name <- unsafeUserSymbol ("uninterpreted_" ++ show fn)+ fn' <- cachedUninterpFn sym fn_name (Ctx.Empty Ctx.:> btr Ctx.:> btr) btr freshTotalUninterpFn+ applySymFn sym fn' (Ctx.Empty Ctx.:> x Ctx.:> y)++floatUninterpSpecialFn _sym _btr fn _args =+ fail $ unwords ["Special function with unexpected arity", show fn]+ floatUninterpArithBinOpR :: (e ~ Expr t) => String@@ -3840,6 +3914,8 @@ iFloatToBV = floatToBV iFloatToSBV = floatToSBV iFloatToReal = floatToReal+ iFloatSpecialFunction sym fi fn args =+ floatSpecialFunction sym (floatInfoToPrecisionRepr fi) fn args iFloatBaseTypeRepr _ = BaseFloatRepr . floatInfoToPrecisionRepr @@ -3903,6 +3979,9 @@ v <- sbMakeBoundVar sym nm tp LatchVarKind Nothing updateVarBinding sym nm (VarSymbolBinding v) return $! BoundVarExpr v++ exprUninterpConstants _sym expr =+ (runST $ VI.collectVarInfo $ VI.recordExprVars VI.ExistsOnly expr) ^. VI.uninterpConstants freshBoundVar sym nm tp = sbMakeBoundVar sym nm tp QuantifierVarKind Nothing
src/What4/Expr/GroundEval.hs view
@@ -43,10 +43,11 @@ import Control.Monad.Trans.Class import Control.Monad.Trans.Maybe import qualified Data.BitVector.Sized as BV-import Data.List (foldl') import Data.List.NonEmpty (NonEmpty(..))+import Data.Foldable import qualified Data.Map.Strict as Map import Data.Maybe ( fromMaybe )+import Data.Parameterized.Ctx import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.NatRepr import Data.Parameterized.TraversableFC@@ -57,6 +58,7 @@ import What4.BaseTypes import What4.Interface import qualified What4.SemiRing as SR+import qualified What4.SpecialFunctions as SFn import qualified What4.Expr.ArrayUpdateMap as AUM import qualified What4.Expr.BoolMap as BM import What4.Expr.Builder@@ -109,6 +111,35 @@ lookupArray tps (ArrayConcrete base m) i = return $ fromMaybe base (Map.lookup i' m) where i' = fromMaybe (error "lookupArray: not valid indexLits") $ Ctx.zipWithM asIndexLit tps i +-- | Update a ground array.+updateArray ::+ Ctx.Assignment BaseTypeRepr idx ->+ GroundArray idx b ->+ Ctx.Assignment GroundValueWrapper idx ->+ GroundValue b ->+ IO (GroundArray idx b)+updateArray idx_tps arr idx val =+ case arr of+ ArrayMapping arr' -> return . ArrayMapping $ \x ->+ if indicesEq idx_tps idx x then pure val else arr' x+ ArrayConcrete d m -> do+ let idx' = fromMaybe (error "UpdateArray only supported on Nat and BV") $ Ctx.zipWithM asIndexLit idx_tps idx+ return $ ArrayConcrete d (Map.insert idx' val m)++ where indicesEq :: Ctx.Assignment BaseTypeRepr ctx+ -> Ctx.Assignment GroundValueWrapper ctx+ -> Ctx.Assignment GroundValueWrapper ctx+ -> Bool+ indicesEq tps x y =+ forallIndex (Ctx.size x) $ \j ->+ let GVW xj = x Ctx.! j+ GVW yj = y Ctx.! j+ tp = tps Ctx.! j+ in case tp of+ BaseIntegerRepr -> xj == yj+ BaseBVRepr _ -> xj == yj+ _ -> error $ "We do not yet support UpdateArray on " ++ show tp ++ " indices."+ asIndexLit :: BaseTypeRepr tp -> GroundValueWrapper tp -> Maybe (IndexLit tp) asIndexLit BaseIntegerRepr (GVW v) = return $ IntIndexLit v asIndexLit (BaseBVRepr w) (GVW v) = return $ BVIndexLit w v@@ -328,19 +359,32 @@ ------------------------------------------------------------------------ -- Operations that introduce irrational numbers. - Pi -> return $ fromDouble pi- RealSin x -> fromDouble . sin . toDouble <$> f x- RealCos x -> fromDouble . cos . toDouble <$> f x- RealATan2 x y -> do- xv <- f x- yv <- f y- return $ fromDouble (atan2 (toDouble xv) (toDouble yv))- RealSinh x -> fromDouble . sinh . toDouble <$> f x- RealCosh x -> fromDouble . cosh . toDouble <$> f x+ RealSpecialFunction fn (SFn.SpecialFnArgs args) ->+ let sf1 :: (Double -> Double) ->+ Ctx.Assignment (SFn.SpecialFnArg (Expr t) BaseRealType) (EmptyCtx ::> SFn.R) ->+ MaybeT IO (GroundValue BaseRealType)+ sf1 dfn (Ctx.Empty Ctx.:> SFn.SpecialFnArg x) = fromDouble . dfn . toDouble <$> f x - RealExp x -> fromDouble . exp . toDouble <$> f x- RealLog x -> fromDouble . log . toDouble <$> f x+ sf2 :: (Double -> Double -> Double) ->+ Ctx.Assignment (SFn.SpecialFnArg (Expr t) BaseRealType) (EmptyCtx ::> SFn.R ::> SFn.R) ->+ MaybeT IO (GroundValue BaseRealType)+ sf2 dfn (Ctx.Empty Ctx.:> SFn.SpecialFnArg x Ctx.:> SFn.SpecialFnArg y) =+ do xv <- f x+ yv <- f y+ return $ fromDouble (dfn (toDouble xv) (toDouble yv))+ in case fn of+ SFn.Pi -> return $ fromDouble pi+ SFn.Sin -> sf1 sin args+ SFn.Cos -> sf1 cos args+ SFn.Sinh -> sf1 sinh args+ SFn.Cosh -> sf1 cosh args+ SFn.Exp -> sf1 exp args+ SFn.Log -> sf1 log args+ SFn.Arctan2 -> sf2 atan2 args+ SFn.Pow -> sf2 (**) args + _ -> mzero -- TODO, other functions as well+ ------------------------------------------------------------------------ -- Bitvector Operations @@ -446,6 +490,8 @@ Just i | minSigned w <= i && i <= maxSigned w -> pure (BV.mkBV w i) _ -> mzero + FloatSpecialFunction _ _ _ -> mzero -- TODO? evaluate concretely?+ ------------------------------------------------------------------------ -- Array Operations @@ -476,27 +522,53 @@ arr <- f a idx <- traverseFC (\e -> GVW <$> f e) i v' <- f v- case arr of- ArrayMapping arr' -> return . ArrayMapping $ \x ->- if indicesEq idx_tps idx x then pure v' else arr' x- ArrayConcrete d m -> do- val <- f v- let idx' = fromMaybe (error "UpdateArray only supported on Nat and BV") $ Ctx.zipWithM asIndexLit idx_tps idx- return $ ArrayConcrete d (Map.insert idx' val m)+ lift $ updateArray idx_tps arr idx v' - where indicesEq :: Ctx.Assignment BaseTypeRepr ctx- -> Ctx.Assignment GroundValueWrapper ctx- -> Ctx.Assignment GroundValueWrapper ctx- -> Bool- indicesEq tps x y =- forallIndex (Ctx.size x) $ \j ->- let GVW xj = x Ctx.! j- GVW yj = y Ctx.! j- tp = tps Ctx.! j- in case tp of- BaseIntegerRepr -> xj == yj- BaseBVRepr _ -> xj == yj- _ -> error $ "We do not yet support UpdateArray on " ++ show tp ++ " indices."+ CopyArray w _ dest_arr dest_idx src_arr src_idx len _ _ -> do+ ground_dest_arr <- f dest_arr+ ground_dest_idx <- f dest_idx+ ground_src_arr <- f src_arr+ ground_src_idx <- f src_idx+ ground_len <- f len++ lift $ foldlM+ (\arr_acc (dest_i, src_i) ->+ updateArray (Ctx.singleton $ BaseBVRepr w) arr_acc (Ctx.singleton $ GVW dest_i)+ =<< lookupArray (Ctx.singleton $ BaseBVRepr w) ground_src_arr (Ctx.singleton $ GVW src_i))+ ground_dest_arr+ (zip+ (BV.enumFromToUnsigned ground_dest_idx (BV.sub w (BV.add w ground_dest_idx ground_len) (BV.mkBV w 1)))+ (BV.enumFromToUnsigned ground_src_idx (BV.sub w (BV.add w ground_src_idx ground_len) (BV.mkBV w 1))))++ SetArray w _ arr idx val len _ -> do+ ground_arr <- f arr+ ground_idx <- f idx+ ground_val <- f val+ ground_len <- f len++ lift $ foldlM+ (\arr_acc i ->+ updateArray (Ctx.singleton $ BaseBVRepr w) arr_acc (Ctx.singleton $ GVW i) ground_val)+ ground_arr+ (BV.enumFromToUnsigned ground_idx (BV.sub w (BV.add w ground_idx ground_len) (BV.mkBV w 1)))++ EqualArrayRange w a_repr lhs_arr lhs_idx rhs_arr rhs_idx len _ _ -> do+ ground_lhs_arr <- f lhs_arr+ ground_lhs_idx <- f lhs_idx+ ground_rhs_arr <- f rhs_arr+ ground_rhs_idx <- f rhs_idx+ ground_len <- f len++ foldlM+ (\acc (lhs_i, rhs_i) -> do+ ground_eq_res <- MaybeT $ groundEq a_repr <$>+ lookupArray (Ctx.singleton $ BaseBVRepr w) ground_lhs_arr (Ctx.singleton $ GVW lhs_i) <*>+ lookupArray (Ctx.singleton $ BaseBVRepr w) ground_rhs_arr (Ctx.singleton $ GVW rhs_i)+ return $ acc && ground_eq_res)+ True+ (zip+ (BV.enumFromToUnsigned ground_lhs_idx (BV.sub w (BV.add w ground_lhs_idx ground_len) (BV.mkBV w 1)))+ (BV.enumFromToUnsigned ground_rhs_idx (BV.sub w (BV.add w ground_rhs_idx ground_len) (BV.mkBV w 1)))) ------------------------------------------------------------------------ -- Conversions
src/What4/Expr/MATLAB.hs view
@@ -731,9 +731,13 @@ ] ) +instance TestEquality f => Eq (MatlabSolverFn f args tp) where+ x == y = isJust (testSolverFnEq x y)+ instance ( Hashable (f BaseRealType) , Hashable (f BaseIntegerType) , HashableF f+ , TestEquality f ) => Hashable (MatlabSolverFn f args tp) where hashWithSalt = $(structuralHashWithSalt [t|MatlabSolverFn|] [])
src/What4/Expr/StringSeq.hs view
@@ -106,7 +106,7 @@ instance (HasAbsValue e, HashableF e) => HashableF (StringSeq e) where hashWithSaltF s (StringSeq _si xs) = hashWithSalt s (sft_hash xs) -instance (HasAbsValue e, HashableF e) => Hashable (StringSeq e si) where+instance (HasAbsValue e, HashableF e, TestEquality e) => Hashable (StringSeq e si) where hashWithSalt = hashWithSaltF singleton :: (HasAbsValue e, HashableF e, IsExpr e) => StringInfoRepr si -> e (BaseStringType si) -> StringSeq e si
src/What4/Expr/UnaryBV.hs view
@@ -135,6 +135,8 @@ Just Refl else Nothing+instance Eq p => Eq (UnaryBV p n) where+ x == y = isJust (testEquality x y) instance Hashable p => Hashable (UnaryBV p n) where hashWithSalt s0 u = Map.foldlWithKey' go s0 (unaryBVMap u)
src/What4/Expr/VarIdentification.hs view
@@ -30,7 +30,7 @@ , varErrors -- * CollectedVarInfo generation , Scope(..)- , Polarity(..)+ , BM.Polarity(..) , VarRecorder , collectVarInfo , recordExprVars@@ -61,9 +61,10 @@ import Prettyprinter (Doc) import What4.BaseTypes+import What4.Expr.App import What4.Expr.AppTheory import qualified What4.Expr.BoolMap as BM-import What4.Expr.Builder+import What4.Interface import What4.ProblemFeatures import qualified What4.SemiRing as SR import What4.Utils.MonadST@@ -127,10 +128,10 @@ -- | Return variables needed to define element as a predicate predicateVarInfo :: Expr t BaseBoolType -> CollectedVarInfo t-predicateVarInfo e = runST $ collectVarInfo $ recordAssertionVars ExistsOnly Positive e+predicateVarInfo e = runST $ collectVarInfo $ recordAssertionVars ExistsOnly BM.Positive e newtype VarRecorder s t a- = VR { unVR :: ReaderT (H.HashTable s Word64 (Maybe Polarity))+ = VR { unVR :: ReaderT (H.HashTable s Word64 (Maybe BM.Polarity)) (StateT (CollectedVarInfo t) (ST s)) a }@@ -178,7 +179,7 @@ addExistVar :: Scope -- ^ Quantifier scope- -> Polarity -- ^ Polarity of variable+ -> BM.Polarity -- ^ Polarity of variable -> NonceAppExpr t BaseBoolType -- ^ Top term -> BoundQuant -- ^ Quantifier appearing in top term. -> ExprBoundVar t tp@@ -195,7 +196,7 @@ addExistVar ExistsForall _ _ _ _ _ = do fail $ "what4 does not allow existental variables to appear inside forall quantifier." -addForallVar :: Polarity -- ^ Polarity of formula+addForallVar :: BM.Polarity -- ^ Polarity of formula -> NonceAppExpr t BaseBoolType -- ^ Top term -> BoundQuant -- ^ Quantifier appearing in top term. -> ExprBoundVar t tp -- ^ Bound variable@@ -233,8 +234,8 @@ -- | Record variables in a predicate that we are checking satisfiability of. recordAssertionVars :: Scope -- ^ Scope of assertion- -> Polarity- -- ^ Polarity of this formula.+ -> BM.Polarity+ -- ^ BM.Polarity of this formula. -> Expr t BaseBoolType -- ^ Predicate to assert -> VarRecorder s t ()@@ -275,39 +276,39 @@ -- | This records asserted variables in an app expr. recurseAssertedNonceAppExprVars :: Scope- -> Polarity+ -> BM.Polarity -> NonceAppExpr t BaseBoolType -> VarRecorder s t () recurseAssertedNonceAppExprVars scope p ea0 = case nonceExprApp ea0 of Forall v x -> do case p of- Positive -> do+ BM.Positive -> do addFeatures useExistForall addForallVar p ea0 ForallBound v x- Negative ->+ BM.Negative -> addExistVar scope p ea0 ForallBound v x Exists v x -> do case p of- Positive ->+ BM.Positive -> addExistVar scope p ea0 ExistBound v x- Negative -> do+ BM.Negative -> do addFeatures useExistForall addForallVar p ea0 ExistBound v x _ -> recurseNonceAppVars scope ea0 -- | This records asserted variables in an app expr.-recurseAssertedAppExprVars :: Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()+recurseAssertedAppExprVars :: Scope -> BM.Polarity -> Expr t BaseBoolType -> VarRecorder s t () recurseAssertedAppExprVars scope p e = go e where go BoolExpr{} = return () go (asApp -> Just (NotPred x)) =- recordAssertionVars scope (negatePolarity p) x+ recordAssertionVars scope (BM.negatePolarity p) x go (asApp -> Just (ConjPred xs)) =- let pol (x,Positive) = recordAssertionVars scope p x- pol (x,Negative) = recordAssertionVars scope (negatePolarity p) x+ let pol (x,BM.Positive) = recordAssertionVars scope p x+ pol (x,BM.Negative) = recordAssertionVars scope (BM.negatePolarity p) x in case BM.viewBoolMap xs of BM.BoolMapUnit -> return ()@@ -361,10 +362,14 @@ recordFnVars :: ExprSymFn t args ret -> VarRecorder s t () recordFnVars f = do case symFnInfo f of- UninterpFnInfo{} -> return ()- DefinedFnInfo _ d _ -> recordExprVars ExistsForall d- MatlabSolverFnInfo _ _ d -> recordExprVars ExistsForall d-+ UninterpFnInfo{} ->+ addFeatures useUninterpFunctions+ DefinedFnInfo _ d _ ->+ do addFeatures useDefinedFunctions+ recordExprVars ExistsForall d+ MatlabSolverFnInfo _ _ d ->+ do addFeatures useDefinedFunctions+ recordExprVars ExistsForall d -- | Recurse through the variables in the element, adding bound variables -- as both exist and forall vars.@@ -386,7 +391,6 @@ ArrayTrueOnEntries f a -> do recordFnVars f recordExprVars scope a- FnApp f a -> do recordFnVars f traverseFC_ (recordExprVars scope) a
src/What4/Expr/WeightedSum.hs view
@@ -166,7 +166,7 @@ instance TestEquality f => Eq (WrapF f i) where (WrapF x) == (WrapF y) = isJust $ testEquality x y -instance HashableF f => Hashable (WrapF f i) where+instance (HashableF f, TestEquality f) => Hashable (WrapF f i) where hashWithSalt s (WrapF x) = hashWithSaltF s x traverseWrap :: Functor m => (f (SR.SemiRingBase i) -> m (g (SR.SemiRingBase i))) -> WrapF f i -> m (WrapF g i)@@ -303,6 +303,9 @@ unless (AM.eqBy (SR.occ_eq (prodRepr x)) (_prodMap x) (_prodMap y)) Nothing return Refl +instance OrdF f => Eq (SemiRingProduct f sr) where+ x == y = isJust (testEquality x y)+ instance OrdF f => TestEquality (WeightedSum f) where testEquality x y | sumMapHash x /= sumMapHash y = Nothing@@ -312,7 +315,10 @@ unless (AM.eqBy (SR.eq (sumRepr x)) (_sumMap x) (_sumMap y)) Nothing return Refl +instance OrdF f => Eq (WeightedSum f sr) where+ x == y = isJust (testEquality x y) + -- | Created a weighted sum directly from a map and constant. -- -- Note. When calling this, one should ensure map values equal to '0'@@ -482,10 +488,10 @@ | SR.eq sr c (SR.zero sr) = constant sr (SR.zero sr) | otherwise = unfilteredSum sr m' (SR.mul sr c (wsum^.sumOffset)) where- m' = runIdentity (AM.traverseMaybeWithKey f (wsum^.sumMap))+ m' = AM.mapMaybeWithKey f (wsum^.sumMap) f (WrapF t) _ x- | SR.eq sr (SR.zero sr) cx = return Nothing- | otherwise = return (Just (mkNote sr cx t, cx))+ | SR.eq sr (SR.zero sr) cx = Nothing+ | otherwise = Just (mkNote sr cx t, cx) where cx = SR.mul sr c x -- | Produce a weighted sum from a list of terms and an offset.
+ src/What4/FloatMode.hs view
@@ -0,0 +1,76 @@+-----------------------------------------------------------------------+-- |+-- Module : What4.FloatMode+-- Description : Mode values for controlling the "interpreted" floating point mode.+-- Copyright : (c) Galois, Inc 2014-2022+-- License : BSD3+-- Maintainer : rdockins@galois.com+-- Stability : provisional+--+-- Desired instances for the @IsInterpretedFloatExprBuilder@ class are selected+-- via the different mode values from this module.+------------------------------------------------------------------------+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+module What4.FloatMode+ ( type FloatMode+ , FloatModeRepr(..)+ , FloatIEEE+ , FloatUninterpreted+ , FloatReal+ ) where++import Data.Kind (Type)+import Data.Parameterized.Classes+++-- | Mode flag for how floating-point values should be interpreted.+data FloatMode where+ FloatIEEE :: FloatMode+ FloatUninterpreted :: FloatMode+ FloatReal :: FloatMode++-- | In this mode "interpreted" floating-point values are treated+-- as bit-precise IEEE-754 floats.+type FloatIEEE = 'FloatIEEE++-- | In this mode "interpreted" floating-point values are treated+-- as bitvectors of the appropriate width, and all operations on+-- them are translated as uninterpreted functions.+type FloatUninterpreted = 'FloatUninterpreted++-- | In this mode "interpreted" floating-point values are treated+-- as real-number values, to the extent possible. Expressions that+-- would result in infinities or NaN will yield unspecified values in+-- this mode, or directly produce runtime errors.+type FloatReal = 'FloatReal++data FloatModeRepr :: FloatMode -> Type where+ FloatIEEERepr :: FloatModeRepr FloatIEEE+ FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted+ FloatRealRepr :: FloatModeRepr FloatReal++instance Show (FloatModeRepr fm) where+ showsPrec _ FloatIEEERepr = showString "FloatIEEE"+ showsPrec _ FloatUninterpretedRepr = showString "FloatUninterpreted"+ showsPrec _ FloatRealRepr = showString "FloatReal"++instance ShowF FloatModeRepr++instance KnownRepr FloatModeRepr FloatIEEE where knownRepr = FloatIEEERepr+instance KnownRepr FloatModeRepr FloatUninterpreted where knownRepr = FloatUninterpretedRepr+instance KnownRepr FloatModeRepr FloatReal where knownRepr = FloatRealRepr++instance TestEquality FloatModeRepr where+ testEquality FloatIEEERepr FloatIEEERepr = return Refl+ testEquality FloatUninterpretedRepr FloatUninterpretedRepr = return Refl+ testEquality FloatRealRepr FloatRealRepr = return Refl+ testEquality _ _ = Nothing
src/What4/Interface.hs view
@@ -120,6 +120,7 @@ , natLe , natLt , natToInteger+ , natToIntegerPure , bvToNat , natToReal , integerToNat@@ -206,6 +207,7 @@ import qualified Data.Parameterized.Vector as Vector import Data.Ratio import Data.Scientific (Scientific)+import Data.Set (Set) import GHC.Generics (Generic) import Numeric.Natural import LibBF (BigFloat)@@ -218,6 +220,7 @@ import What4.ProgramLoc import What4.Concrete import What4.SatResult+import What4.SpecialFunctions import What4.Symbol import What4.Utils.AbstractDomains import What4.Utils.Arithmetic@@ -376,7 +379,25 @@ -- | Print a sym expression for debugging or display purposes. printSymExpr :: e tp -> Doc ann + -- | Set the abstract value of an expression. This is primarily useful for+ -- symbolic expressions where the domain is known to be narrower than what+ -- is contained in the expression. Setting the abstract value to use the+ -- narrower domain can, in some cases, allow the expression to be further+ -- simplified.+ --+ -- This is prefixed with @unsafe-@ because it has the potential to+ -- introduce unsoundness if the new abstract value does not accurately+ -- represent the domain of the expression. As such, the burden is on users+ -- of this function to ensure that the new abstract value is used soundly.+ --+ -- Note that composing expressions together can sometimes widen the abstract+ -- domains involved, so if you use this function to change an abstract value,+ -- be careful than subsequent operations do not widen away the value. As a+ -- potential safeguard, one can use 'annotateTerm' on the new expression to+ -- inhibit transformations that could change the abstract value.+ unsafeSetAbstractValue :: AbstractValue tp -> e tp -> e tp + newtype ArrayResultWrapper f idx tp = ArrayResultWrapper { unwrapArrayResult :: f (BaseArrayType idx tp) } @@ -492,6 +513,11 @@ natToInteger :: IsExprBuilder sym => sym -> SymNat sym -> IO (SymInteger sym) natToInteger _sym (SymNat x) = pure x +-- | Convert a natural number to an integer.+-- `natToInteger` is just this operation lifted into IO.+natToIntegerPure :: SymNat sym -> SymInteger sym+natToIntegerPure (SymNat x) = x+ -- | Convert the unsigned value of a bitvector to a natural. bvToNat :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymNat sym) -- The unsigned value of a bitvector is always nonnegative@@ -541,7 +567,7 @@ instance OrdF (SymExpr sym) => Ord (SymNat sym) where compare (SymNat x) (SymNat y) = toOrdering (compareF x y) -instance HashableF (SymExpr sym) => Hashable (SymNat sym) where+instance (HashableF (SymExpr sym), TestEquality (SymExpr sym)) => Hashable (SymNat sym) where hashWithSalt s (SymNat x) = hashWithSaltF s x ------------------------------------------------------------------------@@ -655,6 +681,10 @@ -- 'annotateTerm' returns the same annotation that 'annotateTerm' did. getAnnotation :: sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp) + -- | Project the original, unannotated term from an annotated term.+ -- This returns 'Nothing' for terms that do not have annotations.+ getUnannotatedTerm :: sym -> SymExpr sym tp -> Maybe (SymExpr sym tp)+ ---------------------------------------------------------------------- -- Boolean operations. @@ -1381,6 +1411,59 @@ -> Ctx.Assignment (SymExpr sym) (idx::>tp) -> IO (SymExpr sym b) + -- | Copy elements from the source array to the destination array.+ --+ -- @'arrayCopy' sym dest_arr dest_idx src_arr src_idx len@ copies the elements+ -- from @src_arr@ at indices @[src_idx .. (src_idx + len - 1)]@ into+ -- @dest_arr@ at indices @[dest_idx .. (dest_idx + len - 1)]@.+ --+ -- The result is undefined if either @dest_idx + len@ or @src_idx + len@+ -- wraps around.+ arrayCopy ::+ (1 <= w) =>+ sym ->+ SymArray sym (SingleCtx (BaseBVType w)) a {- ^ @dest_arr@ -} ->+ SymBV sym w {- ^ @dest_idx@ -} ->+ SymArray sym (SingleCtx (BaseBVType w)) a {- ^ @src_arr@ -} ->+ SymBV sym w {- ^ @src_idx@ -} ->+ SymBV sym w {- ^ @len@ -} ->+ IO (SymArray sym (SingleCtx (BaseBVType w)) a)++ -- | Set elements of the given array.+ --+ -- @'arraySet' sym arr idx val len@ sets the elements of @arr@ at indices+ -- @[idx .. (idx + len - 1)]@ to @val@.+ --+ -- The result is undefined if @idx + len@ wraps around.+ arraySet ::+ (1 <= w) =>+ sym ->+ SymArray sym (SingleCtx (BaseBVType w)) a {- ^ @arr@ -} ->+ SymBV sym w {- ^ @idx@ -} ->+ SymExpr sym a {- ^ @val@ -} ->+ SymBV sym w {- ^ @len@ -} ->+ IO (SymArray sym (SingleCtx (BaseBVType w)) a)++ -- | Check whether the lhs array and rhs array are equal at a range of+ -- indices.+ --+ -- @'arrayRangeEq' sym lhs_arr lhs_idx rhs_arr rhs_idx len@ checks whether the+ -- elements of @lhs_arr@ at indices @[lhs_idx .. (lhs_idx + len - 1)]@ and the+ -- elements of @rhs_arr@ at indices @[rhs_idx .. (rhs_idx + len - 1)]@ are+ -- equal.+ --+ -- The result is undefined if either @lhs_idx + len@ or @rhs_idx + len@+ -- wraps around.+ arrayRangeEq ::+ (1 <= w) =>+ sym ->+ SymArray sym (SingleCtx (BaseBVType w)) a {- ^ @lhs_arr@ -} ->+ SymBV sym w {- ^ @lhs_idx@ -} ->+ SymArray sym (SingleCtx (BaseBVType w)) a {- ^ @rhs_arr@ -} ->+ SymBV sym w {- ^ @rhs_idx@ -} ->+ SymBV sym w {- ^ @len@ -} ->+ IO (Pred sym)+ -- | Create an array from a map of concrete indices to values. -- -- This is implemented, but designed to be overridden for efficiency.@@ -1803,52 +1886,44 @@ -- if @x@ is negative. realSqrt :: sym -> SymReal sym -> IO (SymReal sym) - -- | @realAtan2 sym y x@ returns the arctangent of @y/x@ with a range- -- of @-pi@ to @pi@; this corresponds to the angle between the positive- -- x-axis and the line from the origin @(x,y)@.- --- -- When @x@ is @0@ this returns @pi/2 * sgn y@.- --- -- When @x@ and @y@ are both zero, this function is undefined.- realAtan2 :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)- -- | Return value denoting pi. realPi :: sym -> IO (SymReal sym)+ realPi sym = realSpecialFunction0 sym Pi -- | Natural logarithm. @realLog x@ is undefined -- for @x <= 0@. realLog :: sym -> SymReal sym -> IO (SymReal sym)+ realLog sym x = realSpecialFunction1 sym Log x -- | Natural exponentiation realExp :: sym -> SymReal sym -> IO (SymReal sym)+ realExp sym x = realSpecialFunction1 sym Exp x -- | Sine trig function realSin :: sym -> SymReal sym -> IO (SymReal sym)+ realSin sym x = realSpecialFunction1 sym Sin x -- | Cosine trig function realCos :: sym -> SymReal sym -> IO (SymReal sym)+ realCos sym x = realSpecialFunction1 sym Cos x -- | Tangent trig function. @realTan x@ is undefined -- when @cos x = 0@, i.e., when @x = pi/2 + k*pi@ for -- some integer @k@. realTan :: sym -> SymReal sym -> IO (SymReal sym)- realTan sym x = do- sin_x <- realSin sym x- cos_x <- realCos sym x- realDiv sym sin_x cos_x+ realTan sym x = realSpecialFunction1 sym Tan x -- | Hyperbolic sine realSinh :: sym -> SymReal sym -> IO (SymReal sym)+ realSinh sym x = realSpecialFunction1 sym Sinh x -- | Hyperbolic cosine realCosh :: sym -> SymReal sym -> IO (SymReal sym)+ realCosh sym x = realSpecialFunction1 sym Cosh x -- | Hyperbolic tangent realTanh :: sym -> SymReal sym -> IO (SymReal sym)- realTanh sym x = do- sinh_x <- realSinh sym x- cosh_x <- realCosh sym x- realDiv sym sinh_x cosh_x+ realTanh sym x = realSpecialFunction1 sym Tanh x -- | Return absolute value of the real number. realAbs :: sym -> SymReal sym -> IO (SymReal sym)@@ -1867,6 +1942,50 @@ y2 <- realSq sym y realSqrt sym =<< realAdd sym x2 y2 + -- | @realAtan2 sym y x@ returns the arctangent of @y/x@ with a range+ -- of @-pi@ to @pi@; this corresponds to the angle between the positive+ -- x-axis and the line from the origin @(x,y)@.+ --+ -- When @x@ is @0@ this returns @pi/2 * sgn y@.+ --+ -- When @x@ and @y@ are both zero, this function is undefined.+ realAtan2 :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)+ realAtan2 sym y x = realSpecialFunction2 sym Arctan2 y x++ -- | Apply a special function to real arguments+ realSpecialFunction+ :: sym+ -> SpecialFunction args+ -> Ctx.Assignment (SpecialFnArg (SymExpr sym) BaseRealType) args+ -> IO (SymReal sym)++ -- | Access a 0-arity special function constant+ realSpecialFunction0+ :: sym+ -> SpecialFunction EmptyCtx+ -> IO (SymReal sym)+ realSpecialFunction0 sym fn =+ realSpecialFunction sym fn Ctx.Empty++ -- | Apply a 1-argument special function+ realSpecialFunction1+ :: sym+ -> SpecialFunction (EmptyCtx ::> R)+ -> SymReal sym+ -> IO (SymReal sym)+ realSpecialFunction1 sym fn x =+ realSpecialFunction sym fn (Ctx.Empty Ctx.:> SpecialFnArg x)++ -- | Apply a 2-argument special function+ realSpecialFunction2+ :: sym+ -> SpecialFunction (EmptyCtx ::> R ::> R)+ -> SymReal sym+ -> SymReal sym+ -> IO (SymReal sym)+ realSpecialFunction2 sym fn x y =+ realSpecialFunction sym fn (Ctx.Empty Ctx.:> SpecialFnArg x Ctx.:> SpecialFnArg y)+ ---------------------------------------------------------------------- -- IEEE-754 floating-point operations -- | Return floating point number @+0@.@@ -2203,6 +2322,14 @@ -- | Convert a floating point number to a real number. floatToReal :: sym -> SymFloat sym fpp -> IO (SymReal sym) + -- | Apply a special function to floating-point arguments+ floatSpecialFunction+ :: sym+ -> FloatPrecisionRepr fpp+ -> SpecialFunction args+ -> Ctx.Assignment (SpecialFnArg (SymExpr sym) (BaseFloatType fpp)) args+ -> IO (SymFloat sym fpp)+ ---------------------------------------------------------------------- -- Cplx operations @@ -2667,7 +2794,10 @@ Maybe Rational {- ^ upper bound -} -> IO (SymReal sym) + -- | Return the set of uninterpreted constants in the given expression.+ exprUninterpConstants :: sym -> SymExpr sym tp -> Set (Some (BoundVar sym)) + ---------------------------------------------------------------------- -- Functions needs to support quantifiers. @@ -2963,14 +3093,14 @@ asConcrete :: IsExpr e => e tp -> Maybe (ConcreteVal tp) asConcrete x = case exprType x of- BaseBoolRepr -> ConcreteBool <$> asConstantPred x- BaseIntegerRepr -> ConcreteInteger <$> asInteger x- BaseRealRepr -> ConcreteReal <$> asRational x+ BaseBoolRepr -> ConcreteBool <$> asConstantPred x+ BaseIntegerRepr -> ConcreteInteger <$> asInteger x+ BaseRealRepr -> ConcreteReal <$> asRational x BaseStringRepr _si -> ConcreteString <$> asString x- BaseComplexRepr -> ConcreteComplex <$> asComplex x- BaseBVRepr w -> ConcreteBV w <$> asBV x- BaseFloatRepr _ -> Nothing- BaseStructRepr _ -> ConcreteStruct <$> (asStruct x >>= traverseFC asConcrete)+ BaseComplexRepr -> ConcreteComplex <$> asComplex x+ BaseBVRepr w -> ConcreteBV w <$> asBV x+ BaseFloatRepr fpp -> ConcreteFloat fpp <$> asFloat x+ BaseStructRepr _ -> ConcreteStruct <$> (asStruct x >>= traverseFC asConcrete) BaseArrayRepr idx _tp -> do def <- asConstantArray x c_def <- asConcrete def@@ -2985,6 +3115,7 @@ ConcreteBool False -> return (falsePred sym) ConcreteInteger x -> intLit sym x ConcreteReal x -> realLit sym x+ ConcreteFloat fpp bf -> floatLit sym fpp bf ConcreteString x -> stringLit sym x ConcreteComplex x -> mkComplexLit sym x ConcreteBV w x -> bvLit sym w x@@ -3010,7 +3141,7 @@ such that @p i@ is true. If @p i@ is true for no such value, then this returns the value @f h@. -} muxRange :: (IsExpr e, Monad m) =>- (Natural -> m (e BaseBoolType)) + (Natural -> m (e BaseBoolType)) {- ^ Returns predicate that holds if we have found the value we are looking for. It is assumed that the predicate must hold for a unique integer in the range.
src/What4/InterpretedFloatingPoint.hs view
@@ -46,6 +46,8 @@ import Data.Hashable import Data.Kind import Data.Parameterized.Classes+import Data.Parameterized.Context (Assignment, EmptyCtx, (::>))+import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.TH.GADT import Data.Ratio import Data.Word ( Word16, Word64 )@@ -54,6 +56,7 @@ import What4.BaseTypes import What4.Interface+import What4.SpecialFunctions -- | This data kind describes the types of floating-point formats. -- This consist of the standard IEEE 754-2008 binary floating point formats,@@ -104,6 +107,8 @@ instance TestEquality FloatInfoRepr where testEquality = $(structuralTypeEquality [t|FloatInfoRepr|] [])+instance Eq (FloatInfoRepr fi) where+ x == y = isJust (testEquality x y) instance OrdF FloatInfoRepr where compareF = $(structuralTypeOrd [t|FloatInfoRepr|] []) @@ -452,6 +457,44 @@ -> IO (SymBV sym w) -- | Convert a floating point number to a real number. iFloatToReal :: sym -> SymInterpretedFloat sym fi -> IO (SymReal sym)++ -- | Apply a special function to floating-point arguments+ iFloatSpecialFunction+ :: sym+ -> FloatInfoRepr fi+ -> SpecialFunction args+ -> Assignment (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args+ -> IO (SymInterpretedFloat sym fi)++ -- | Access a 0-arity special function constant+ iFloatSpecialFunction0+ :: sym+ -> FloatInfoRepr fi+ -> SpecialFunction EmptyCtx+ -> IO (SymInterpretedFloat sym fi)+ iFloatSpecialFunction0 sym fi fn =+ iFloatSpecialFunction sym fi fn Ctx.Empty++ -- | Apply a 1-argument special function+ iFloatSpecialFunction1+ :: sym+ -> FloatInfoRepr fi+ -> SpecialFunction (EmptyCtx ::> R)+ -> SymInterpretedFloat sym fi+ -> IO (SymInterpretedFloat sym fi)+ iFloatSpecialFunction1 sym fi fn x =+ iFloatSpecialFunction sym fi fn (Ctx.Empty Ctx.:> SpecialFnArg x)++ -- | Apply a 2-argument special function+ iFloatSpecialFunction2+ :: sym+ -> FloatInfoRepr fi+ -> SpecialFunction (EmptyCtx ::> R ::> R)+ -> SymInterpretedFloat sym fi+ -> SymInterpretedFloat sym fi+ -> IO (SymInterpretedFloat sym fi)+ iFloatSpecialFunction2 sym fi fn x y =+ iFloatSpecialFunction sym fi fn (Ctx.Empty Ctx.:> SpecialFnArg x Ctx.:> SpecialFnArg y) -- | The associated BaseType representative of the floating point -- interpretation for each format.
src/What4/LabeledPred.hs view
@@ -12,7 +12,9 @@ ------------------------------------------------------------------------ {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TemplateHaskell #-}@@ -47,7 +49,7 @@ -- | Message added when assumption/assertion was made. , _labeledPredMsg :: !msg }- deriving (Eq, Data, Functor, Generic, Generic1, Ord, Typeable)+ deriving (Eq, Data, Functor, Foldable, Generic, Generic1, Ord, Show, Traversable, Typeable) $(deriveBifunctor ''LabeledPred) $(deriveBifoldable ''LabeledPred)
src/What4/ProblemFeatures.hs view
@@ -22,6 +22,8 @@ -- 10 : Uses floating-point -- 11 : Computes UNSAT cores -- 12 : Computes UNSAT assumptions+-- 13 : Uses uninterpreted functions+-- 14 : Uses defined functions ------------------------------------------------------------------------ {-# LANGUAGE GeneralizedNewtypeDeriving #-}@@ -41,6 +43,8 @@ , useFloatingPoint , useUnsatCores , useUnsatAssumptions+ , useUninterpFunctions+ , useDefinedFunctions , hasProblemFeature ) where @@ -116,5 +120,18 @@ useUnsatAssumptions :: ProblemFeatures useUnsatAssumptions = ProblemFeatures 0x1000 +-- | Indicates if the solver is able and configured to use+-- uninterpreted functions.+useUninterpFunctions :: ProblemFeatures+useUninterpFunctions = ProblemFeatures 0x2000++-- | Indicates if the solver is able and configured to use+-- defined functions.+useDefinedFunctions :: ProblemFeatures+useDefinedFunctions = ProblemFeatures 0x4000++-- | Tests if one set of problem features subsumes another.+-- In particular, @hasProblemFeature x y@ is true iff+-- the set of features in @x@ is a superset of those in @y@. hasProblemFeature :: ProblemFeatures -> ProblemFeatures -> Bool hasProblemFeature x y = (x .&. y) == y
src/What4/Protocol/Online.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {- | Module : What4.Protocol.Online Description : Online solver interactions@@ -22,10 +23,12 @@ , solverResponse , SolverGoalTimeout(..) , getGoalTimeoutInSeconds+ , withLocalGoalTimeout , ErrorBehavior(..) , killSolver , push , pop+ , tryPop , reset , inNewFrame , inNewFrameWithVars@@ -41,23 +44,29 @@ , checkSatisfiableWithModel ) where -import Control.Exception- ( SomeException(..), catchJust, tryJust, displayException )+import Control.Concurrent ( threadDelay )+import Control.Concurrent.Async ( race )+import Control.Exception ( SomeException(..), catchJust, tryJust, displayException ) import Control.Monad ( unless ) import Control.Monad (void, forM, forM_)-import Control.Monad.Catch ( MonadMask, bracket_, onException )+import Control.Monad.Catch ( Exception, MonadMask, bracket_, catchIf+ , onException, throwM, fromException ) import Control.Monad.IO.Class ( MonadIO, liftIO )+import Data.IORef+#if MIN_VERSION_base(4,14,0)+#else+import qualified Data.List as L+#endif import Data.Parameterized.Some import Data.Proxy-import Data.IORef import Data.Text (Text) import qualified Data.Text.Lazy as LazyText import Prettyprinter import System.Exit import System.IO+import qualified System.IO.Error as IOE import qualified System.IO.Streams as Streams-import System.Process- (ProcessHandle, terminateProcess, waitForProcess)+import System.Process (ProcessHandle, terminateProcess, waitForProcess) import What4.Expr import What4.Interface (SolverEvent(..)@@ -117,7 +126,12 @@ -- a full second. in if msecs > 0 && secs == 0 then 1 else secs +instance Pretty SolverGoalTimeout where+ pretty (SolverGoalTimeout ms) = pretty ms <> pretty "msec" +instance Show SolverGoalTimeout where+ show = show . pretty+ -- | A live connection to a running solver process. -- -- This data structure should be used in a single-threaded@@ -169,6 +183,15 @@ -- ^ The amount of time (in seconds) that a solver should spend -- trying to satisfy any particular goal before giving up. A -- value of zero indicates no time limit.+ --+ -- Note that it is not sufficient to set just this value to+ -- control timeouts; this value is used as a reference for common+ -- code (e.g. SMTLIB2) to determine the timeout for the associated+ -- timer. When initialized, this field of the SolverProcess is+ -- initialized from a solver-specific timeout configuration+ -- (e.g. z3Timeout); the latter is the definitive reference for+ -- the timeout, and solver-specific code will likely use the the+ -- latter rather than this common field. } @@ -187,7 +210,11 @@ killSolver :: SolverProcess t solver -> IO () killSolver p = do catchJust filterAsync- (terminateProcess (solverHandle p))+ (terminateProcess (solverHandle p)+ -- some solvers emit stderr messages on SIGTERM+ >> readAllLines (solverStderr p)+ >> return ()+ ) (\(ex :: SomeException) -> hPutStrLn stderr $ displayException ex) void $ waitForProcess (solverHandle p) @@ -270,21 +297,32 @@ addCommand c (popCommand c) | otherwise -> writeIORef (solverEarlyUnsat p) $! (Just $! i-1) --- | Pop a previous solver assumption frame, but don't communicate--- the pop command to the solver. This is really only useful in--- error recovery code when we know the solver has already exited.-popStackOnly :: SolverProcess scope solver -> IO ()-popStackOnly p =- readIORef (solverEarlyUnsat p) >>= \case+-- | Pop a previous solver assumption frame, but allow this to fail if+-- the solver has exited.+tryPop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()+tryPop p =+ let trycmd conn = catchIf solverGone+ (addCommand conn (popCommand conn))+ (const $ throwM RunawaySolverTimeout)+#if MIN_VERSION_base(4,14,0)+ solverGone = IOE.isResourceVanishedError+#else+ solverGone = L.isInfixOf "resource vanished" . IOE.ioeGetErrorString+#endif+ in readIORef (solverEarlyUnsat p) >>= \case Nothing -> do let c = solverConn p popEntryStack c+ trycmd c Just i | i <= 1 -> do let c = solverConn p popEntryStack c writeIORef (solverEarlyUnsat p) Nothing+ trycmd c | otherwise -> writeIORef (solverEarlyUnsat p) $! (Just $! i-1) ++ -- | Perform an action in the scope of a solver assumption frame. inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver -> m a -> m a inNewFrame p action = inNewFrameWithVars p [] action@@ -300,13 +338,15 @@ case solverErrorBehavior p of ContinueOnError -> bracket_ (liftIO $ pushWithVars)- (liftIO $ pop p)+ (liftIO $ tryPop p) action ImmediateExit -> do liftIO $ pushWithVars- x <- (onException action (liftIO $ popStackOnly p))- liftIO $ pop p- return x+ onException (do x <- action+ liftIO $ pop p+ return x+ )+ (liftIO $ tryPop p) where conn = solverConn p pushWithVars = do@@ -384,7 +424,7 @@ Unknown -> return Unknown Sat () -> Sat <$> getModel yp --- | Following a successful check-sat command, build a ground evaulation function+-- | Following a successful check-sat command, build a ground evaluation function -- that will evaluate terms in the context of the current model. getModel :: SMTReadWriter solver => SolverProcess scope solver -> IO (GroundEvalFn scope) getModel p = smtExprGroundEvalFn (solverConn p)@@ -418,10 +458,17 @@ getSatResult :: SMTReadWriter s => SolverProcess t s -> IO (SatResult () ()) getSatResult yp = do let ph = solverHandle yp- sat_result <- tryJust filterAsync (smtSatResult yp (solverConn yp))+ let action = smtSatResult yp+ sat_result <- withLocalGoalTimeout yp action+ case sat_result of Right ok -> return ok + Left e@(SomeException _)+ | Just RunawaySolverTimeout <- fromException e -> do+ -- Deadman timeout fired, so this is effectively Incomplete+ return Unknown+ Left (SomeException e) -> do -- Interrupt process terminateProcess ph@@ -440,3 +487,39 @@ , "*** standard error:" , LazyText.unpack txt ]+++-- | If the solver cannot voluntarily limit itself to the requested+-- timeout period, this runs a local async process with a slightly+-- longer time period that will forcibly terminate the solver process+-- if it expires while the solver process is still running.+--+-- Note that this will require re-establishment of the solver process+-- and any associated context for any subsequent solver goal+-- evaluation.++withLocalGoalTimeout ::+ SolverProcess t s+ -> (WriterConn t s -> IO (SatResult () ()))+ -> IO (Either SomeException (SatResult () ()))+withLocalGoalTimeout solverProc action =+ if getGoalTimeoutInSeconds (solverGoalTimeout solverProc) == 0+ then do tryJust filterAsync (action $ solverConn solverProc)+ else let deadmanTimeoutPeriodMicroSeconds =+ (fromInteger $+ getGoalTimeoutInMilliSeconds (solverGoalTimeout solverProc)+ + 500 -- allow solver to honor timeout first+ ) * 1000 -- convert msec to usec+ deadmanTimer = threadDelay deadmanTimeoutPeriodMicroSeconds+ in+ do race deadmanTimer (action $ solverConn solverProc) >>= \case+ Left () -> do killSolver solverProc+ return $ Left $ SomeException RunawaySolverTimeout+ Right x -> return $ Right x+++-- | The RunawaySolverTimeout is thrown when the solver cannot+-- voluntarily limit itself to the requested solver-timeout period and+-- has subsequently been forcibly stopped.+data RunawaySolverTimeout = RunawaySolverTimeout deriving Show+instance Exception RunawaySolverTimeout
src/What4/Protocol/SMTLib2.hs view
@@ -92,13 +92,8 @@ import Control.Exception import Control.Monad.State.Strict import qualified Data.BitVector.Sized as BV-import qualified Data.Bits as Bits-import Data.ByteString (ByteString)-import qualified Data.ByteString as BS-import Data.Char (digitToInt, isPrint, isAscii)+import Data.Char (digitToInt, isAscii) import Data.IORef-import qualified Data.Text as Text-import qualified Data.Text.Lazy as Lazy import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Monoid@@ -112,6 +107,8 @@ import qualified Data.Set as Set import Data.String import Data.Text (Text)+import qualified Data.Text as Text+import qualified Data.Text.Lazy as Lazy import Data.Text.Lazy.Builder (Builder) import qualified Data.Text.Lazy.Builder as Builder import qualified Data.Text.Lazy.Builder.Int as Builder@@ -207,54 +204,114 @@ arrayStore :: Term -> Term -> Term -> Term arrayStore = SMT2.store -byteStringTerm :: ByteString -> Term-byteStringTerm bs = SMT2.T ("\"" <> BS.foldr f "\"" bs)+------------------------------------------------------------------------------------+-- String Escaping functions+--+-- The following functions implement the escaping and+-- escape parsing rules from SMTLib 2.6. Documentation+-- regarding this format is pasted below from the+-- specification document.+--+-- String literals+-- All double-quote-delimited string literals consisting of printable US ASCII+-- characters, i.e., those with Unicode code point from 0x00020 to 0x0007E.+-- We refer to these literals as _string constants_.+--+-- The restriction to printable US ASCII characters in string constants is for+-- simplicity since that set is universally supported. Arbitrary Unicode characters+-- can be represented with _escape sequences_ which can have one of the following+-- forms+-- \ud₃d₂d₁d₀+-- \u{d₀}+-- \u{d₁d₀}+-- \u{d₂d₁d₀}+-- \u{d₃d₂d₁d₀}+-- \u{d₄d₃d₂d₁d₀}+-- where each dᵢ is a hexadecimal digit and d₄ is restricted to the range 0-2.+-- These are the **only escape sequences** in this theory. See later.+-- In a later version, the restrictions above on the digits may be extended+-- to allow characters from all 17 Unicode planes.+--+-- Observe that the first form, \ud₃d₂d₁d₀, has exactly 4 hexadecimal digit,+-- following the common use of this form in some programming languages.+-- Unicode characters outside the range covered by \ud₃d₂d₁d₀ can be+-- represented with the long form \u{d₄d₃d₂d₁d₀}.+--+-- Also observe that programming language-specific escape sequences, such as+-- \n, \b, \r and so on, are _not_ escape sequences in this theory as they+-- are not fully standard across languages.++-- | Apply the SMTLib2.6 string escaping rules to a string literal.+textToTerm :: Text -> Term+textToTerm bs = SMT2.T ("\"" <> Text.foldr f "\"" bs) where- f w x+ inLiteralRange c = 0x20 <= fromEnum c && fromEnum c <= 0x7E++ f c x+ -- special case: the `"` character has a special case escaping mode which+ -- is encoded as `""` | '\"' == c = "\"\"" <> x- | isPrint c = Builder.singleton c <> x- | otherwise = "\\x" <> h1 <> h2 <> x- where- h1 = Builder.fromString (showHex (w `Bits.shiftR` 4) "")- h2 = Builder.fromString (showHex (w Bits..&. 0xF) "") - c :: Char- c = toEnum (fromEnum w)+ -- special case: always escape the `\` character as an explicit code point,+ -- so we don't have to do lookahead to discover if it is followed by a `u`+ | '\\' == c = "\\u{5c}" <> x + -- others characters in the "normal" ASCII range require no escaping+ | inLiteralRange c = Builder.singleton c <> x -unescapeText :: Text -> Maybe ByteString+ -- characters outside that range require escaping+ | otherwise = "\\u{" <> Builder.fromString (showHex (fromEnum c) "}") <> x++++-- | Parse SMTLIb2.6 escaping rules for strings.+--+-- Note! The escaping rule that uses the @\"\"@ sequence+-- to encode a double quote has already been resolved+-- by @parseSMTLIb2String@, so here we just need to+-- parse the @\\u@ escape forms.+unescapeText :: Text -> Maybe Text unescapeText = go mempty where- go bs t =+ go str t = case Text.uncons t of- Nothing -> Just bs+ Nothing -> Just str Just (c, t') | not (isAscii c) -> Nothing- | c == '\\' -> readEscape bs t'- | otherwise -> continue bs c t'+ | c == '\\' -> readEscape str t'+ | otherwise -> continue str c t' - continue bs c t = go (BS.snoc bs (toEnum (fromEnum c))) t+ continue str c t = go (Text.snoc str c) t - readEscape bs t =+ readEscape str t = case Text.uncons t of- Nothing -> Nothing+ Nothing -> Just (Text.snoc str '\\') Just (c, t')- | c == 'a' -> continue bs '\a' t'- | c == 'b' -> continue bs '\b' t'- | c == 'e' -> continue bs '\x1B' t'- | c == 'f' -> continue bs '\f' t'- | c == 'n' -> continue bs '\n' t'- | c == 'r' -> continue bs '\r' t'- | c == 't' -> continue bs '\t' t'- | c == 'v' -> continue bs '\v' t'- | c == 'x' -> readHexEscape bs t'- | otherwise -> continue bs c t'+ -- Note: the \u forms are the _only_ escape forms+ | c == 'u' -> readHexEscape str t'+ | otherwise -> continue (Text.snoc str '\\') c t' - readHexEscape bs t =- case readHex (Text.unpack (Text.take 2 t)) of- (n, []):_ | 0 <= n && n < 256 -> go (BS.snoc bs (toEnum n)) (Text.drop 2 t)+ readHexEscape str t =+ case Text.uncons t of+ Just (c, t')+ -- take until the closing brace+ | c == '{'+ , (ds, t'') <- Text.breakOn "}" t'+ , Just ('}',t''') <- Text.uncons t''+ -> readDigits str ds t'''++ -- take exactly four digits+ | (ds, t'') <- Text.splitAt 4 t'+ , Text.length ds == 4+ -> readDigits str ds t''+ _ -> Nothing + readDigits str ds t =+ case readHex (Text.unpack ds) of+ (n, []):_ -> continue str (toEnum n) t+ _ -> Nothing+ -- | This class exists so that solvers supporting the SMTLib2 format can support -- features that go slightly beyond the standard. --@@ -295,8 +352,8 @@ smtlib2StringSort :: SMT2.Sort smtlib2StringSort = SMT2.Sort "String" - smtlib2StringTerm :: ByteString -> Term- smtlib2StringTerm = byteStringTerm+ smtlib2StringTerm :: Text -> Term+ smtlib2StringTerm = textToTerm smtlib2StringLength :: Term -> Term smtlib2StringLength = SMT2.un_app "str.len"@@ -368,7 +425,7 @@ asSMT2Type RealTypeMap = SMT2.realSort asSMT2Type (BVTypeMap w) = SMT2.bvSort (natValue w) asSMT2Type (FloatTypeMap fpp) = SMT2.Sort $ mkFloatSymbol "FloatingPoint" (asSMTFloatPrecision fpp)-asSMT2Type Char8TypeMap = smtlib2StringSort @a+asSMT2Type UnicodeTypeMap = smtlib2StringSort @a asSMT2Type ComplexToStructTypeMap = smtlib2StructSort @a [ SMT2.realSort, SMT2.realSort ] asSMT2Type ComplexToArrayTypeMap =@@ -549,9 +606,11 @@ realDiv x y = x SMT2../ [y] realSin = un_app "sin" realCos = un_app "cos"+ realTan = un_app "tan" realATan2 = bin_app "atan2" realSinh = un_app "sinh" realCosh = un_app "cosh"+ realTanh = un_app "tanh" realExp = un_app "exp" realLog = un_app "log" @@ -598,8 +657,8 @@ type instance Command (Writer a) = SMT2.Command instance SMTLib2Tweaks a => SMTWriter (Writer a) where- forallExpr vars t = SMT2.forall (varBinding @a <$> vars) t- existsExpr vars t = SMT2.exists (varBinding @a <$> vars) t+ forallExpr vars t = SMT2.forall_ (varBinding @a <$> vars) t+ existsExpr vars t = SMT2.exists_ (varBinding @a <$> vars) t arrayConstant = case smtlib2arrayConstant @a of@@ -634,7 +693,7 @@ let resolveArg (var, Some tp) = (var, asSMT2Type @a tp) in SMT2.defineFun f (resolveArg <$> args) (asSMT2Type @a return_type) e - stringTerm bs = smtlib2StringTerm @a bs+ stringTerm str = smtlib2StringTerm @a str stringLength x = smtlib2StringLength @a x stringAppend xs = smtlib2StringAppend @a xs stringContains x y = smtlib2StringContains @a x y@@ -743,8 +802,8 @@ -- BGS: Is this correct? parseBVLitHelper _ = natBV 0 0 -parseStringSolverValue :: MonadFail m => SExp -> m ByteString-parseStringSolverValue (SString t) | Just bs <- unescapeText t = return bs+parseStringSolverValue :: MonadFail m => SExp -> m Text+parseStringSolverValue (SString t) | Just t' <- unescapeText t = return t' parseStringSolverValue x = fail ("Could not parse string solver value:\n " ++ show x) parseFloatSolverValue :: MonadFail m => FloatPrecisionRepr fpp@@ -757,7 +816,7 @@ (Just Refl, Just Refl) -> do -- eb' + 1 ~ 1 + eb' Refl <- return $ plusComm eb' (knownNat @1)- -- (eb' + 1) + sb' ~ eb' + (1 + sb') + -- (eb' + 1) + sb' ~ eb' + (1 + sb') Refl <- return $ plusAssoc eb' (knownNat @1) sb' return bv where bv = BV.concat (addNat (knownNat @1) eb) sb' (BV.concat knownNat eb sgn expt) sig@@ -1043,19 +1102,22 @@ writeCheckSat c writeExit c +-- n.b. commonly used for the startSolverProcess method of the+-- OnlineSolver class, so it's helpful for the type suffixes to align startSolver :: SMTLib2GenericSolver a => a -> AcknowledgementAction t (Writer a) -- ^ Action for acknowledging command responses -> (WriterConn t (Writer a) -> IO ()) -- ^ Action for setting start-up-time options and logic+ -> SolverGoalTimeout -> 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 strictOpt auxOutput sym = do+startSolver solver ack setup tmout 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@@ -1089,7 +1151,7 @@ , solverName = show solver , solverEarlyUnsat = earlyUnsatRef , solverSupportsResetAssertions = supportsResetAssertions solver- , solverGoalTimeout = SolverGoalTimeout 0 -- no timeout by default+ , solverGoalTimeout = tmout } shutdownSolver
src/What4/Protocol/SMTLib2/Response.hs view
@@ -30,6 +30,7 @@ import Control.Applicative import Control.Exception import qualified Data.Attoparsec.Text as AT+import Data.Maybe ( isJust ) import Data.Text ( Text ) import qualified Data.Text as Text import qualified Data.Text.Lazy as Lazy@@ -87,6 +88,10 @@ getSolverResponse conn = do mb <- tryJust filterAsync (AStreams.parseFromStream+ -- n.b. the parseFromStream with an attoparsec parser used+ -- here will throw+ -- System.IO.Streams.Attoparsec.ParseException on a parser+ -- failure; the rspParser throws some other parse errors (rspParser (SMTWriter.strictParsing conn)) (SMTWriter.connInputHandle conn)) return mb@@ -117,14 +122,20 @@ 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- ]+ Left se@(SomeException e)+ | isJust $ filterAsync se -> throw e+ | Just (AStreams.ParseException _) <- fromException se+ -> do -- Parser failed and left the unparseable input in the+ -- stream; extract it to show the user+ 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+ ]+ | otherwise -> throw e+ rspParser :: SMTWriter.ResponseStrictness -> AT.Parser SMTResponse
src/What4/Protocol/SMTLib2/Syntax.hs view
@@ -79,8 +79,8 @@ , eq , distinct , ite- , forall- , exists+ , forall_+ , exists_ , letBinder -- * @Ints@, @Reals@, @Reals_Ints@ theories , negate@@ -319,18 +319,18 @@ varBinding :: (Text,Sort) -> Builder varBinding (nm, tp) = "(" <> Builder.fromText nm <> " " <> unSort tp <> ")" --- | @forall vars t@ denotes a predicate that holds if @t@ for every valuation of the+-- | @forall_ vars t@ denotes a predicate that holds if @t@ for every valuation of the -- variables in @vars@.-forall :: [(Text, Sort)] -> Term -> Term-forall [] r = r-forall vars r =+forall_ :: [(Text, Sort)] -> Term -> Term+forall_ [] r = r+forall_ vars r = T $ app "forall" [builder_list (varBinding <$> vars), renderTerm r] --- | @exists vars t@ denotes a predicate that holds if @t@ for some valuation of the+-- | @exists_ vars t@ denotes a predicate that holds if @t@ for some valuation of the -- variables in @vars@.-exists :: [(Text, Sort)] -> Term -> Term-exists [] r = r-exists vars r =+exists_ :: [(Text, Sort)] -> Term -> Term+exists_ [] r = r+exists_ vars r = T $ app "exists" [builder_list (varBinding <$> vars), renderTerm r] letBinding :: (Text, Term) -> Builder
src/What4/Protocol/SMTWriter.hs view
@@ -101,20 +101,18 @@ ) where #if !MIN_VERSION_base(4,13,0)-import Control.Monad.Fail( MonadFail )+import Control.Monad.Fail ( MonadFail ) #endif import Control.Exception import Control.Lens hiding ((.>), Strict)-import Control.Monad.Extra import Control.Monad.IO.Class import Control.Monad.Reader import Control.Monad.ST import Control.Monad.State.Strict import Control.Monad.Trans.Maybe-import qualified Data.Bits as Bits import qualified Data.BitVector.Sized as BV-import Data.ByteString (ByteString)+import qualified Data.Bits as Bits import Data.IORef import Data.Kind import Data.List.NonEmpty (NonEmpty(..))@@ -128,10 +126,10 @@ import Data.Ratio import Data.Text (Text) import qualified Data.Text as Text+import qualified Data.Text.Lazy as Lazy import Data.Text.Lazy.Builder (Builder) import qualified Data.Text.Lazy.Builder as Builder import qualified Data.Text.Lazy.Builder.Int as Builder (decimal)-import qualified Data.Text.Lazy as Lazy import Data.Word import LibBF (BigFloat, bfFromBits) @@ -154,6 +152,7 @@ import What4.ProgramLoc import What4.SatResult import qualified What4.SemiRing as SR+import qualified What4.SpecialFunctions as SFn import What4.Symbol import What4.Utils.AbstractDomains import qualified What4.Utils.BVDomain as BVD@@ -174,7 +173,7 @@ RealTypeMap :: TypeMap BaseRealType BVTypeMap :: (1 <= w) => !(NatRepr w) -> TypeMap (BaseBVType w) FloatTypeMap :: !(FloatPrecisionRepr fpp) -> TypeMap (BaseFloatType fpp)- Char8TypeMap :: TypeMap (BaseStringType Char8)+ UnicodeTypeMap :: TypeMap (BaseStringType Unicode) -- A complex number mapped to an SMTLIB struct. ComplexToStructTypeMap:: TypeMap BaseComplexType@@ -211,7 +210,7 @@ show RealTypeMap = "RealTypeMap" show (BVTypeMap n) = "BVTypeMap " ++ show n show (FloatTypeMap x) = "FloatTypeMap " ++ show x- show Char8TypeMap = "Char8TypeMap"+ show UnicodeTypeMap = "UnicodeTypeMap" show (ComplexToStructTypeMap) = "ComplexToStructTypeMap" show ComplexToArrayTypeMap = "ComplexToArrayTypeMap" show (PrimArrayTypeMap ctx a) = "PrimArrayTypeMap " ++ showF ctx ++ " " ++ showF a@@ -226,7 +225,7 @@ testEquality BoolTypeMap BoolTypeMap = Just Refl testEquality IntegerTypeMap IntegerTypeMap = Just Refl testEquality RealTypeMap RealTypeMap = Just Refl- testEquality Char8TypeMap Char8TypeMap = Just Refl+ testEquality UnicodeTypeMap UnicodeTypeMap = Just Refl testEquality (FloatTypeMap x) (FloatTypeMap y) = do Refl <- testEquality x y return Refl@@ -429,17 +428,16 @@ realDiv :: v -> v -> v realSin :: v -> v- realCos :: v -> v+ realTan :: v -> v realATan2 :: v -> v -> v realSinh :: v -> v- realCosh :: v -> v+ realTanh :: v -> v realExp :: v -> v- realLog :: v -> v -- | Apply the arguments to the given function.@@ -787,6 +785,23 @@ cacheLookup conn lookup_action = readIORef (entryStack conn) >>= firstJustM lookup_action ++-- | Like 'findM', but also allows you to compute some additional information in the predicate.+firstJustM :: Monad m => (a -> m (Maybe b)) -> [a] -> m (Maybe b)+firstJustM _ [] = pure Nothing+firstJustM p (x:xs) = maybeM (firstJustM p xs) (pure . Just) (p x)+{-# INLINE firstJustM #-}++-- | Monadic generalisation of 'maybe'.+maybeM :: Monad m => m b -> (a -> m b) -> m (Maybe a) -> m b+maybeM n j x = maybe n j =<< x+{-# INLINE maybeM #-}++-- | Like 'when', but where the test can be monadic.+whenM :: Monad m => m Bool -> m () -> m ()+whenM b t = do b' <- b; when b' t+{-# INLINE whenM #-}+ cacheLookupExpr :: WriterConn t h -> Nonce t tp -> IO (Maybe (SMTExpr h tp)) cacheLookupExpr c n = cacheLookup c $ \entry -> lookupIdx (symExprCache entry) n@@ -915,7 +930,7 @@ structProj :: Ctx.Assignment TypeMap args -> Ctx.Index args tp -> Term h -> Term h -- | Produce a term representing a string literal- stringTerm :: ByteString -> Term h+ stringTerm :: Text -> Term h -- | Compute the length of a term stringLength :: Term h -> Term h@@ -1040,11 +1055,12 @@ RealTypeMap -> return () BVTypeMap _ -> return () FloatTypeMap _ -> return ()- Char8TypeMap -> return ()+ UnicodeTypeMap -> return () ComplexToStructTypeMap -> declareStructDatatype conn (Ctx.Empty Ctx.:> RealTypeMap Ctx.:> RealTypeMap) ComplexToArrayTypeMap -> return () PrimArrayTypeMap args ret -> do traverseFC_ (declareTypes conn) args+ declareStructDatatype conn args declareTypes conn ret FnArrayTypeMap args ret -> do traverseFC_ (declareTypes conn) args@@ -1164,7 +1180,7 @@ BaseFloatRepr fpp -> Right $! FloatTypeMap fpp BaseRealRepr -> Right RealTypeMap BaseIntegerRepr -> Right IntegerTypeMap- BaseStringRepr Char8Repr -> Right Char8TypeMap+ BaseStringRepr UnicodeRepr -> Right UnicodeTypeMap BaseStringRepr si -> Left (StringTypeUnsupported (Some si)) BaseComplexRepr | feat `hasProblemFeature` useStructs -> Right ComplexToStructTypeMap@@ -1282,7 +1298,7 @@ when (hi < maxUnsigned w) $ addSideCondition "bv_bitrange" $ (bvOr t (bvTerm w (BV.mkBV w hi))) .== (bvTerm w (BV.mkBV w hi)) -addPartialSideCond _ t (Char8TypeMap) (Just (StringAbs len)) =+addPartialSideCond _ t (UnicodeTypeMap) (Just (StringAbs len)) = do case rangeLowBound len of Inclusive lo -> addSideCondition "string length low range" $@@ -1741,9 +1757,9 @@ return $ SMTExpr (FloatTypeMap fpp) $ floatTerm fpp f mkExpr t@(StringExpr l _) = case l of- Char8Literal bs -> do+ UnicodeLiteral str -> do checkStringSupport t- return $ SMTExpr Char8TypeMap $ stringTerm @h bs+ return $ SMTExpr UnicodeTypeMap $ stringTerm @h str _ -> do conn <- asks scConn theoryUnsupported conn ("strings " ++ show (stringLiteralInfo l)) t@@ -1790,6 +1806,7 @@ -- | Convert an element to a base expression. mkBaseExpr :: SMTWriter h => Expr t tp -> SMTCollector t h (Term h) mkBaseExpr e = asBase <$> mkExpr e+{-# INLINE mkBaseExpr #-} -- | Convert structure to list. mkIndicesTerms :: SMTWriter h@@ -2118,37 +2135,30 @@ addSideCondition "real sqrt" $ v .>= 0 -- Return variable return nm- Pi -> do- unsupportedTerm i- RealSin xe -> do- checkComputableSupport i- x <- mkBaseExpr xe- freshBoundTerm RealTypeMap $ realSin x- RealCos xe -> do- checkComputableSupport i- x <- mkBaseExpr xe- freshBoundTerm RealTypeMap $ realCos x- RealATan2 xe ye -> do- checkComputableSupport i- x <- mkBaseExpr xe- y <- mkBaseExpr ye- freshBoundTerm RealTypeMap $ realATan2 x y- RealSinh xe -> do- checkComputableSupport i- x <- mkBaseExpr xe- freshBoundTerm RealTypeMap $ realSinh x- RealCosh xe -> do- checkComputableSupport i- x <- mkBaseExpr xe- freshBoundTerm RealTypeMap $ realCosh x- RealExp xe -> do- checkComputableSupport i- x <- mkBaseExpr xe- freshBoundTerm RealTypeMap $ realExp x- RealLog xe -> do++ RealSpecialFunction fn (SFn.SpecialFnArgs args) -> do checkComputableSupport i- x <- mkBaseExpr xe- freshBoundTerm RealTypeMap $ realLog x+ let sf1 :: (Term h -> Term h) ->+ Ctx.Assignment (SFn.SpecialFnArg (Expr t) BaseRealType) (Ctx.EmptyCtx Ctx.::> SFn.R) ->+ SMTCollector t h (SMTExpr h BaseRealType)+ sf1 tmfn (Ctx.Empty Ctx.:> SFn.SpecialFnArg xe) =+ freshBoundTerm RealTypeMap . tmfn =<< mkBaseExpr xe+ case fn of+ SFn.Sin -> sf1 realSin args+ SFn.Cos -> sf1 realCos args+ SFn.Tan -> sf1 realTan args+ SFn.Sinh -> sf1 realSinh args+ SFn.Cosh -> sf1 realCosh args+ SFn.Tanh -> sf1 realTanh args+ SFn.Exp -> sf1 realExp args+ SFn.Log -> sf1 realLog args+ SFn.Arctan2 ->+ case args of+ Ctx.Empty Ctx.:> SFn.SpecialFnArg ye Ctx.:> SFn.SpecialFnArg xe ->+ do y <- mkBaseExpr ye+ x <- mkBaseExpr xe+ freshBoundTerm RealTypeMap $ realATan2 y x+ _ -> unsupportedTerm i -- TODO? more functions? ------------------------------------------ -- Bitvector operations@@ -2311,7 +2321,7 @@ StringLength xe -> do case stringInfo xe of- Char8Repr -> do+ UnicodeRepr -> do checkStringSupport i x <- mkBaseExpr xe freshBoundTerm IntegerTypeMap $ stringLength @h x@@ -2319,7 +2329,7 @@ StringIndexOf xe ye ke -> case stringInfo xe of- Char8Repr -> do+ UnicodeRepr -> do checkStringSupport i x <- mkBaseExpr xe y <- mkBaseExpr ye@@ -2329,17 +2339,17 @@ StringSubstring _ xe offe lene -> case stringInfo xe of- Char8Repr -> do+ UnicodeRepr -> do checkStringSupport i x <- mkBaseExpr xe off <- mkBaseExpr offe len <- mkBaseExpr lene- freshBoundTerm Char8TypeMap $ stringSubstring @h x off len+ freshBoundTerm UnicodeTypeMap $ stringSubstring @h x off len si -> fail ("Unsupported symbolic string substring operation " ++ show si) StringContains xe ye -> case stringInfo xe of- Char8Repr -> do+ UnicodeRepr -> do checkStringSupport i x <- mkBaseExpr xe y <- mkBaseExpr ye@@ -2348,7 +2358,7 @@ StringIsPrefixOf xe ye -> case stringInfo xe of- Char8Repr -> do+ UnicodeRepr -> do checkStringSupport i x <- mkBaseExpr xe y <- mkBaseExpr ye@@ -2357,7 +2367,7 @@ StringIsSuffixOf xe ye -> case stringInfo xe of- Char8Repr -> do+ UnicodeRepr -> do checkStringSupport i x <- mkBaseExpr xe y <- mkBaseExpr ye@@ -2366,12 +2376,12 @@ StringAppend si xes -> case si of- Char8Repr -> do+ UnicodeRepr -> do checkStringSupport i- let f (SSeq.StringSeqLiteral l) = return $ stringTerm @h $ fromChar8Lit l+ let f (SSeq.StringSeqLiteral l) = return $ stringTerm @h $ fromUnicodeLit l f (SSeq.StringSeqTerm t) = mkBaseExpr t xs <- mapM f $ SSeq.toList xes- freshBoundTerm Char8TypeMap $ stringAppend @h xs+ freshBoundTerm UnicodeTypeMap $ stringAppend @h xs _ -> fail ("Unsupported symbolic string append operation " ++ show si) @@ -2492,6 +2502,7 @@ FloatToReal x -> do xe <- mkBaseExpr x freshBoundTerm RealTypeMap $ floatToReal xe+ FloatSpecialFunction{} -> unsupportedTerm i ------------------------------------------------------------------------ -- Array Operations@@ -2552,22 +2563,23 @@ else FnArrayTypeMap idx_types <- liftIO $ traverseFC (evalFirstClassTypeRepr conn (eltSource i)) idxRepr+ let tp = mkArray idx_types value_type+ -- make sure any referenced tuple types exist+ liftIO (declareTypes conn tp)+ case arrayConstant @h of Just constFn | otherwise -> do let idx_smt_types = toListFC Some idx_types- let tp = mkArray idx_types value_type freshBoundTerm tp $! constFn idx_smt_types (Some value_type) (asBase v) Nothing -> do when (not (supportFunctionDefs conn)) $ do fail $ show $ pretty (smtWriterName conn) <+> "cannot encode constant arrays."- -- Constant functions use unnamed variables.- let array_type = mkArray idx_types value_type -- Create names for index variables. args <- liftIO $ createTypeMapArgsForArray conn idx_types- SMTName array_type <$> freshBoundFn args value_type (asBase v)+ SMTName tp <$> freshBoundFn args value_type (asBase v) SelectArray _bRepr a idx -> do aexpr <- mkExpr a@@ -2597,6 +2609,70 @@ let expr = ite cond value base_array_value SMTName array_type <$> freshBoundFn args resType expr + CopyArray _w_repr _a_repr dest_arr dest_idx src_arr src_idx len _dest_end_idx _src_end_idx -> do+ dest_arr_typed_expr <- mkExpr dest_arr+ let arr_type = smtExprType dest_arr_typed_expr+ dest_idx_typed_expr <- mkExpr dest_idx+ let dest_idx_expr = asBase dest_idx_typed_expr+ let idx_type = smtExprType dest_idx_typed_expr+ src_arr_typed_expr <- mkExpr src_arr+ src_idx_expr <- mkBaseExpr src_idx+ len_expr <- mkBaseExpr len++ res <- freshConstant "array_copy" arr_type++ cr <- liftIO $ withConnEntryStack conn $ runInSandbox conn $ do+ i_expr <- asBase <$> freshConstant "i" idx_type+ return $ asBase (smt_array_select res [i_expr]) .==+ ite ((bvULe dest_idx_expr i_expr) .&& (bvULt i_expr (bvAdd dest_idx_expr len_expr)))+ (asBase (smt_array_select src_arr_typed_expr [bvAdd src_idx_expr (bvSub i_expr dest_idx_expr)]))+ (asBase (smt_array_select dest_arr_typed_expr [i_expr]))+ addSideCondition "array copy" $ forallResult cr+ addSideCondition "array copy" $ bvULt dest_idx_expr (bvAdd dest_idx_expr len_expr)+ addSideCondition "array copy" $ bvULt src_idx_expr (bvAdd src_idx_expr len_expr)++ return res++ SetArray _w_repr _a_repr arr idx val len _end_idx -> do+ arr_typed_expr <- mkExpr arr+ let arr_type = smtExprType arr_typed_expr+ idx_typed_expr <- mkExpr idx+ let idx_expr = asBase idx_typed_expr+ let idx_type = smtExprType idx_typed_expr+ val_expr <- mkBaseExpr val+ len_expr <- mkBaseExpr len++ res <- freshConstant "array_set" arr_type+ cr <- liftIO $ withConnEntryStack conn $ runInSandbox conn $ do+ i_expr <- asBase <$> freshConstant "i" idx_type+ return $ asBase (smt_array_select res [i_expr]) .==+ ite ((bvULe idx_expr i_expr) .&& (bvULt i_expr (bvAdd idx_expr len_expr)))+ val_expr+ (asBase (smt_array_select arr_typed_expr [i_expr]))+ addSideCondition "array set" $ forallResult cr+ addSideCondition "array set" $ bvULt idx_expr (bvAdd idx_expr len_expr)++ return res++ EqualArrayRange _w_repr _a_repr x_arr x_idx y_arr y_idx len _x_end_idx _y_end_idx -> do+ x_arr_typed_expr <- mkExpr x_arr+ x_idx_typed_expr <- mkExpr x_idx+ let x_idx_expr = asBase x_idx_typed_expr+ let idx_type = smtExprType x_idx_typed_expr+ y_arr_typed_expr <- mkExpr y_arr+ y_idx_expr <- mkBaseExpr y_idx+ len_expr <- mkBaseExpr len++ cr <- liftIO $ withConnEntryStack conn $ runInSandbox conn $ do+ i_expr <- asBase <$> freshConstant "i" idx_type+ return $ impliesExpr ((bvULe x_idx_expr i_expr) .&& (bvULt i_expr (bvAdd x_idx_expr len_expr)))+ ((asBase (smt_array_select x_arr_typed_expr [i_expr])) .==+ (asBase (smt_array_select y_arr_typed_expr [bvAdd y_idx_expr (bvSub i_expr x_idx_expr)])))+ addSideCondition "array range equal" $ bvULt x_idx_expr (bvAdd x_idx_expr len_expr)+ addSideCondition "array range equal" $ bvULt y_idx_expr (bvAdd y_idx_expr len_expr)++ freshBoundTerm BoolTypeMap $ forallResult cr+ ------------------------------------------------------------------------ -- Conversions. @@ -2868,7 +2944,8 @@ data SMTEvalFunctions h = SMTEvalFunctions { smtEvalBool :: Term h -> IO Bool -- ^ Given a SMT term for a Boolean value, this should- -- whether the term is assigned true or false.+ -- return an indication of whether the term is assigned+ -- true or false. , smtEvalBV :: forall w . NatRepr w -> Term h -> IO (BV.BV w) -- ^ Given a bitwidth, and a SMT term for a bitvector -- with that bitwidth, this should return an unsigned@@ -2887,7 +2964,7 @@ -- and codomain are both bitvectors. If 'Nothing', -- signifies that we should fall back to index-selection -- representation of arrays.- , smtEvalString :: Term h -> IO ByteString+ , smtEvalString :: Term h -> IO Text -- ^ Given a SMT term representing as sequence of bytes, -- return the value as a bytestring. }@@ -2923,7 +3000,7 @@ f i l = (r:l) where GVW v = vals Ctx.! i r = case tps Ctx.! i of- IntegerTypeMap -> rationalTerm (fromInteger v)+ IntegerTypeMap -> integerTerm v BVTypeMap w -> bvTerm w v _ -> error "Do not yet support other index types." @@ -2939,7 +3016,7 @@ getSolverVal _ smtFns RealTypeMap tm = smtEvalReal smtFns tm getSolverVal _ smtFns (FloatTypeMap fpp) tm = bfFromBits (fppOpts fpp RNE) . BV.asUnsigned <$> smtEvalFloat smtFns fpp tm-getSolverVal _ smtFns Char8TypeMap tm = Char8Literal <$> smtEvalString smtFns tm+getSolverVal _ smtFns UnicodeTypeMap tm = UnicodeLiteral <$> smtEvalString smtFns tm getSolverVal _ smtFns IntegerTypeMap tm = do r <- smtEvalReal smtFns tm when (denominator r /= 1) $ fail "Expected integer value."
src/What4/Protocol/VerilogWriter/ABCVerilog.hs view
@@ -16,6 +16,7 @@ import Data.Parameterized.NatRepr import Data.Parameterized.Some import Data.String+import qualified Data.Text as T import Data.Word import Prettyprinter import What4.BaseTypes@@ -48,7 +49,7 @@ typeDoc _ _ _ = "<type error>" identDoc :: Identifier -> Doc ()-identDoc = pretty+identDoc = pretty . T.replace "!" "_" lhsDoc :: LHS -> Doc () lhsDoc (LHS name) = identDoc name
src/What4/Protocol/VerilogWriter/Backend.hs view
@@ -192,16 +192,7 @@ RealSqrt _ -> doNotSupportError "real numbers" -- Irrational numbers- Pi -> doNotSupportError "real numbers"-- RealSin _ -> doNotSupportError "real numbers"- RealCos _ -> doNotSupportError "real numbers"- RealATan2 _ _ -> doNotSupportError "real numbers"- RealSinh _ -> doNotSupportError "real numbers"- RealCosh _ -> doNotSupportError "real numbers"-- RealExp _ -> doNotSupportError "real numbers"- RealLog _ -> doNotSupportError "real numbers"+ RealSpecialFunction{} -> doNotSupportError "real numbers" RoundEvenReal _ -> doNotSupportError "real numbers" -- Bitvector operations@@ -335,12 +326,16 @@ FloatToBV _ _ _ -> doNotSupportError "floats" FloatToSBV _ _ _ -> doNotSupportError "floats" FloatToReal _ -> doNotSupportError "floats"+ FloatSpecialFunction _ _ _ -> doNotSupportError "floats" -- Array operations ArrayMap _ _ _ _ -> doNotSupportError "arrays" ConstantArray _ _ _ -> doNotSupportError "arrays" UpdateArray _ _ _ _ _ -> doNotSupportError "arrays" SelectArray _ _ _ -> doNotSupportError "arrays"+ CopyArray _ _ _ _ _ _ _ _ _ -> doNotSupportError "arrays"+ SetArray _ _ _ _ _ _ _ -> doNotSupportError "arrays"+ EqualArrayRange _ _ _ _ _ _ _ _ _ -> doNotSupportError "arrays" -- Conversions IntegerToReal _ -> doNotSupportError "integers"
src/What4/SemiRing.hs view
@@ -71,13 +71,13 @@ , occ_count ) where -import GHC.TypeNats+import GHC.TypeNats (Nat) import qualified Data.BitVector.Sized as BV import Data.Kind import Data.Hashable import Data.Parameterized.Classes import Data.Parameterized.TH.GADT-import Numeric.Natural+import Numeric.Natural (Natural) import What4.BaseTypes @@ -233,9 +233,13 @@ instance TestEquality BVFlavorRepr where testEquality = $(structuralTypeEquality [t|BVFlavorRepr|] [])+instance Eq (BVFlavorRepr fv) where+ x == y = isJust (testEquality x y) instance TestEquality OrderedSemiRingRepr where testEquality = $(structuralTypeEquality [t|OrderedSemiRingRepr|] [])+instance Eq (OrderedSemiRingRepr sr) where+ x == y = isJust (testEquality x y) instance TestEquality SemiRingRepr where testEquality =@@ -243,6 +247,8 @@ [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|]) , (ConType [t|BVFlavorRepr|] `TypeApp` AnyType, [|testEquality|]) ])+instance Eq (SemiRingRepr sr) where+ x == y = isJust (testEquality x y) instance OrdF BVFlavorRepr where compareF = $(structuralTypeOrd [t|BVFlavorRepr|] [])
src/What4/Solver.hs view
@@ -36,6 +36,7 @@ , Boolector(..) , boolectorAdapter , boolectorPath+ , boolectorTimeout , runBoolectorInOverride , withBoolector , boolectorOptions@@ -64,6 +65,7 @@ , STP(..) , stpAdapter , stpPath+ , stpTimeout , runSTPInOverride , withSTP , stpOptions@@ -84,6 +86,8 @@ , Z3(..) , z3Path , z3Timeout+ , z3Tactic+ , z3TacticDefault , z3Adapter , runZ3InOverride , withZ3
src/What4/Solver/Boolector.hs view
@@ -19,6 +19,7 @@ module What4.Solver.Boolector ( Boolector(..) , boolectorPath+ , boolectorTimeout , boolectorOptions , boolectorAdapter , runBoolectorInOverride@@ -53,6 +54,10 @@ boolectorPathOLD :: ConfigOption (BaseStringType Unicode) boolectorPathOLD = configOption knownRepr "boolector_path" +-- | Per-check timeout, in milliseconds (zero is none)+boolectorTimeout :: ConfigOption BaseIntegerType+boolectorTimeout = configOption knownRepr "solver.boolector.timeout"+ -- | Control strict parsing for Boolector solver responses (defaults -- to solver.strict-parsing option setting). boolectorStrictParsing :: ConfigOption BaseBoolType@@ -65,9 +70,14 @@ executablePathOptSty (Just "Path to boolector executable") (Just (ConcreteString "boolector"))+ mkTmo co = mkOpt co+ integerOptSty+ (Just "Per-check timeout in milliseconds (zero is none)")+ (Just (ConcreteInteger 0)) bp = bpOpt boolectorPath bp2 = deprecatedOpt [bp] $ bpOpt boolectorPathOLD in [ bp, bp2+ , mkTmo boolectorTimeout , copyOpt (const $ configOptionText boolectorStrictParsing) strictSMTParseOpt ] <> SMT2.smtlib2Options @@ -115,7 +125,7 @@ instance SMT2.SMTLib2GenericSolver Boolector where defaultSolverPath _ = findSolverPath boolectorPath . getConfiguration- defaultSolverArgs _ _ = return ["--smt2", "--smt2-model", "--incremental", "--output-format=smt2", "-e=0"]+ defaultSolverArgs _ _ = return ["--smt2", "--incremental", "--output-format=smt2", "-e=0"] defaultFeatures _ = boolectorFeatures setDefaultLogicAndOptions writer = do SMT2.setLogic writer SMT2.allSupported@@ -134,7 +144,12 @@ SMT2.setLogic writer SMT2.allSupported instance OnlineSolver (SMT2.Writer Boolector) where- startSolverProcess feat = SMT2.startSolver Boolector SMT2.smtAckResult- setInteractiveLogicAndOptions feat- (Just boolectorStrictParsing)+ startSolverProcess feat mbIOh sym = do+ timeout <- SolverGoalTimeout <$>+ (getOpt =<< getOptionSetting boolectorTimeout (getConfiguration sym))+ SMT2.startSolver Boolector SMT2.smtAckResult+ setInteractiveLogicAndOptions+ timeout+ feat+ (Just boolectorStrictParsing) mbIOh sym shutdownSolverProcess = SMT2.shutdownSolver Boolector
src/What4/Solver/CVC4.hs view
@@ -117,6 +117,10 @@ indexType [i] = i indexType il = SMT2.smtlib2StructSort @CVC4 il +indexCtor :: [SMT2.Term] -> SMT2.Term+indexCtor [i] = i+indexCtor il = SMT2.smtlib2StructCtor @CVC4 il+ instance SMT2.SMTLib2Tweaks CVC4 where smtlib2tweaks = CVC4 @@ -124,15 +128,15 @@ smtlib2arrayConstant = Just $ \idx rtp v -> SMT2.arrayConst (indexType idx) rtp v+ smtlib2arraySelect a i = SMT2.arraySelect a (indexCtor i)+ smtlib2arrayUpdate a i = SMT2.arrayStore a (indexCtor i) smtlib2declareStructCmd _ = Nothing- smtlib2StructSort [] = Syntax.varSort "Tuple" smtlib2StructSort tps = Syntax.Sort $ "(Tuple" <> foldMap f tps <> ")" where f x = " " <> Syntax.unSort x smtlib2StructCtor args = Syntax.term_app "mkTuple" args- smtlib2StructProj _n i x = Syntax.term_app (Syntax.builder_list ["_", "tupSel", fromString (show i)]) [ x ] cvc4Features :: ProblemFeatures@@ -227,7 +231,7 @@ SMT2.setOption writer "print-success" "true" -- Tell CVC4 to produce models SMT2.setOption writer "produce-models" "true"- -- Tell CVC4 to make declaraions global, so they are not removed by 'pop' commands+ -- Tell CVC4 to make declarations global, so they are not removed by 'pop' commands SMT2.setOption writer "global-declarations" "true" -- Tell CVC4 to compute UNSAT cores, if that feature is enabled when (supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do@@ -237,10 +241,9 @@ instance OnlineSolver (SMT2.Writer CVC4) where startSolverProcess feat mbIOh sym = do- sp <- SMT2.startSolver CVC4 SMT2.smtAckResult setInteractiveLogicAndOptions- feat (Just cvc4StrictParsing) mbIOh sym timeout <- SolverGoalTimeout <$> (getOpt =<< getOptionSetting cvc4Timeout (getConfiguration sym))- return $ sp { solverGoalTimeout = timeout }+ SMT2.startSolver CVC4 SMT2.smtAckResult setInteractiveLogicAndOptions+ timeout feat (Just cvc4StrictParsing) mbIOh sym shutdownSolverProcess = SMT2.shutdownSolver CVC4
src/What4/Solver/STP.hs view
@@ -16,6 +16,7 @@ ( STP(..) , stpAdapter , stpPath+ , stpTimeout , stpOptions , stpFeatures , runSTPInOverride@@ -47,6 +48,10 @@ stpPathOLD :: ConfigOption (BaseStringType Unicode) stpPathOLD = configOption knownRepr "stp_path" +-- | Per-check timeout, in milliseconds (zero is none)+stpTimeout :: ConfigOption BaseIntegerType+stpTimeout = configOption knownRepr "solver.stp.timeout"+ stpRandomSeed :: ConfigOption BaseIntegerType stpRandomSeed = configOption knownRepr "solver.stp.random-seed" @@ -76,6 +81,8 @@ , deprecatedOpt [p1] $ mkPath stpPathOLD , deprecatedOpt [r1] $ intWithRangeOpt stpRandomSeedOLD (negate randbitval) randbitval+ , mkOpt stpTimeout integerOptSty (Just "Per-check timeout in milliseconds (zero is none)")+ (Just (ConcreteInteger 0)) ] <> SMT2.smtlib2Options stpAdapter :: SolverAdapter st@@ -139,12 +146,19 @@ -- Tell STP to produce models SMT2.setOption writer "produce-models" "true" - -- Tell STP to make declaraions global, so they are not removed by 'pop' commands+ -- Tell STP to make declarations global, so they are not removed by 'pop' commands -- TODO, add this command once https://github.com/stp/stp/issues/365 is closed -- SMT2.setOption writer "global-declarations" "true" instance OnlineSolver (SMT2.Writer STP) where- startSolverProcess feat = SMT2.startSolver STP SMT2.smtAckResult- setInteractiveLogicAndOptions feat- (Just stpStrictParsing)++ startSolverProcess feat mbIOh sym = do+ timeout <- SolverGoalTimeout <$>+ (getOpt =<< getOptionSetting stpTimeout (getConfiguration sym))+ SMT2.startSolver STP SMT2.smtAckResult+ setInteractiveLogicAndOptions+ timeout+ feat+ (Just stpStrictParsing) mbIOh sym+ shutdownSolverProcess = SMT2.shutdownSolver STP
src/What4/Solver/Yices.hs view
@@ -68,6 +68,8 @@ #endif import Control.Applicative+import Control.Concurrent ( threadDelay )+import Control.Concurrent.Async ( race ) import Control.Exception (assert, SomeException(..), tryJust, throw, displayException, Exception(..)) import Control.Lens ((^.), folded)@@ -277,9 +279,11 @@ realDiv x y = term_app "/" [x, y] realSin = errorComputableUnsupported realCos = errorComputableUnsupported+ realTan = errorComputableUnsupported realATan2 = errorComputableUnsupported realSinh = errorComputableUnsupported realCosh = errorComputableUnsupported+ realTanh = errorComputableUnsupported realExp = errorComputableUnsupported realLog = errorComputableUnsupported @@ -365,7 +369,7 @@ yicesType RealTypeMap = realType yicesType (BVTypeMap w) = YicesType (app "bitvector" [fromString (show w)]) yicesType (FloatTypeMap _) = floatFail-yicesType Char8TypeMap = stringFail+yicesType UnicodeTypeMap = stringFail yicesType ComplexToStructTypeMap = tupleType [realType, realType] yicesType ComplexToArrayTypeMap = fnType [boolType] realType yicesType (PrimArrayTypeMap i r) = fnType (toListFC yicesType i) (yicesType r)@@ -767,20 +771,36 @@ -- Throws an exception if something goes wrong. 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 ())- Right (SAtom "unknown") -> return Unknown- Right (SAtom "interrupted") -> return Unknown- Right res -> fail $+ let interpretSExpr = \case+ (SAtom "unsat") -> Unsat ()+ (SAtom "sat") -> Sat ()+ (SAtom "unknown") -> Unknown+ (SAtom "interrupted") -> Unknown+ res -> throw $ UnparseableYicesResponse $ unlines [ "Could not parse sat result." , " " ++ show res ]- Left (SomeException e) -> fail $- unlines [ "Could not parse sat result."- , "*** Exception: " ++ displayException e- ]+ tmo = getGoalTimeoutInSeconds $ yicesTimeout $ connState conn+ delay = 500 -- allow solver to honor timeout first+ msec2usec = (1000 *)+ deadman_tmo = msec2usec $ fromInteger (tmo + delay)+ deadmanTimer = threadDelay deadman_tmo+ action = Streams.parseFromStream (parseSExp parseYicesString)+ in if tmo == 0+ then tryJust filterAsync (action (connInputHandle conn)) >>= \case+ Right d -> return $ interpretSExpr d+ Left e -> fail $ unlines [ "Could not parse sat result."+ , "*** Exception: " ++ displayException e+ ]+ else race deadmanTimer (tryJust filterAsync $ action (connInputHandle conn)) >>= \case+ Right (Right x) -> return $ interpretSExpr x+ Left () -> return Unknown -- no response in timeout period+ Right (Left e) -> fail $ unlines [ "Could not parse sat result."+ , "*** Exception: " ++ displayException e+ ]++data UnparseableYicesResponse = UnparseableYicesResponse String deriving Show+instance Exception UnparseableYicesResponse type Eval scope ty = WriterConn scope Connection ->
src/What4/Solver/Z3.hs view
@@ -21,6 +21,8 @@ , z3Path , z3Timeout , z3Options+ , z3Tactic+ , z3TacticDefault , z3Features , runZ3InOverride , withZ3@@ -30,6 +32,8 @@ import Control.Monad ( when ) import Data.Bits import Data.String+import Data.Text (Text)+import qualified Data.Text as T import System.IO import What4.BaseTypes@@ -63,13 +67,19 @@ 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" +-- | Z3 tactic+z3Tactic :: ConfigOption (BaseStringType Unicode)+z3Tactic = configOption knownRepr "solver.z3.tactic"++z3TacticDefault :: Text+z3TacticDefault = ""+ z3Options :: [ConfigDesc] z3Options = let mkPath co = mkOpt co@@ -84,6 +94,7 @@ t = mkTmo z3Timeout in [ p, t , copyOpt (const $ configOptionText z3StrictParsing) strictSMTParseOpt+ , mkOpt z3Tactic stringOptSty (Just "Z3 tactic") (Just (ConcreteString (UnicodeLiteral z3TacticDefault))) , deprecatedOpt [p] $ mkPath z3PathOLD , deprecatedOpt [t] $ mkTmo z3TimeoutOLD ] <> SMT2.smtlib2Options@@ -156,7 +167,9 @@ let extraOpts = case timeout of Just (ConcreteInteger n) | n > 0 -> ["-t:" ++ show n] _ -> []- return $ ["-smt2", "-in"] ++ extraOpts+ tactic <- getOpt =<< getOptionSetting z3Tactic cfg+ let tacticOpt = if tactic /= z3TacticDefault then ["tactic.default_tactic=" ++ T.unpack tactic] else []+ return $ tacticOpt ++ ["-smt2", "-in"] ++ extraOpts getErrorBehavior _ = SMT2.queryErrorBehavior @@ -214,11 +227,11 @@ SMT2.setOption writer "produce-unsat-cores" "true" instance OnlineSolver (SMT2.Writer Z3) where+ startSolverProcess feat mbIOh sym = do- sp <- SMT2.startSolver Z3 SMT2.smtAckResult setInteractiveLogicAndOptions feat- (Just z3StrictParsing) mbIOh sym timeout <- SolverGoalTimeout <$> (getOpt =<< getOptionSetting z3Timeout (getConfiguration sym))- return $ sp { solverGoalTimeout = timeout }+ SMT2.startSolver Z3 SMT2.smtAckResult setInteractiveLogicAndOptions+ timeout feat (Just z3StrictParsing) mbIOh sym shutdownSolverProcess = SMT2.shutdownSolver Z3
+ src/What4/SpecialFunctions.hs view
@@ -0,0 +1,443 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++{-|+Module : What4.SpecialFunctions+Description : Utilities relating to special functions+Copyright : (c) Galois, Inc 2021+License : BSD3+Maintainer : Rob Dockins <rdockins@galois.com>++Utilties for representing and handling certain \"special\"+functions arising from analysis. Although many of these+functions are most properly understood as complex valued+functions on complex arguments, here we are primarily interested+in their restriction to real-valued functions or their+floating-point approximations.++The functions considered here include functions from+standard and hyperbolic trigonometry, exponential+and logarithmic functions, etc. Some of these functions+are defineable in terms of others (e.g. @tan(x) = sin(x)/cos(x)@+or expm1(x) = exp(x) - 1@) but are commonly implemented+separately in math libraries for increased precision.+Some popular constant values are also included.+-}++module What4.SpecialFunctions+ ( -- * Representation of special functions+ R+ , SpecialFunction(..)++ -- ** Symmetry properties of special functions+ , FunctionSymmetry(..)+ , specialFnSymmetry++ -- ** Packaging arguments to special functions+ , SpecialFnArg(..)+ , traverseSpecialFnArg+ , SpecialFnArgs(..)+ , traverseSpecialFnArgs++ -- ** Interval data for domain and range+ , RealPoint(..)+ , RealBound(..)+ , RealInterval(..)+ , specialFnDomain+ , specialFnRange+ ) where++import Data.Kind (Type)+import Data.Parameterized.Classes+import qualified Data.Parameterized.Context as Ctx+import Data.Parameterized.Context ( pattern (:>) )+import Data.Parameterized.Ctx+import Data.Parameterized.TH.GADT+import Data.Parameterized.TraversableFC++-- | Some special functions exhibit useful symmetries in their arguments.+-- A function @f@ is an odd function if @f(-x) = -f(x)@, and is even+-- if @f(-x) = f(x)@. We extend this notion to arguments of more than+-- one function by saying that a function is even/odd in its @i@th+-- argument if it is even/odd when the other arguments are fixed.+data FunctionSymmetry r+ = NoSymmetry+ | EvenFunction+ | OddFunction+ deriving (Show)+++-- | Phantom data index representing the real number line.+-- Used for specifying the arity of special functions.+data R++-- | Data type for representing \"special\" functions.+-- These include functions from standard and hyperbolic+-- trigonometry, exponential and logarithmic functions,+-- as well as other well-known mathematical functions.+--+-- Generally, little solver support exists for such functions+-- (although systems like dReal and Metatarski can prove some+-- properties). Nonetheless, we may have some information about+-- specific values these functions take, the domains on which they+-- are defined, or the range of values their outputs may take, or+-- specific relationships that may exists between these functions+-- (e.g., trig identities). This information may, in some+-- circumstances, be sufficent to prove properties of interest, even+-- if the functions cannot be represented in their entirety.+data SpecialFunction (args :: Ctx Type) where+ -- constant values involving Pi+ Pi :: SpecialFunction EmptyCtx -- pi+ HalfPi :: SpecialFunction EmptyCtx -- pi/2+ QuarterPi :: SpecialFunction EmptyCtx -- pi/4+ OneOverPi :: SpecialFunction EmptyCtx -- 1/pi+ TwoOverPi :: SpecialFunction EmptyCtx -- 2/pi+ TwoOverSqrt_Pi :: SpecialFunction EmptyCtx -- 2/sqrt(pi)++ -- constant root values+ Sqrt_2 :: SpecialFunction EmptyCtx -- sqrt(2)+ Sqrt_OneHalf :: SpecialFunction EmptyCtx -- sqrt(1/2)++ -- constant values involving exponentials and logarithms+ E :: SpecialFunction EmptyCtx -- e = exp(1)+ Log2_E :: SpecialFunction EmptyCtx -- log_2(e)+ Log10_E :: SpecialFunction EmptyCtx -- log_10(e)+ Ln_2 :: SpecialFunction EmptyCtx -- ln(2)+ Ln_10 :: SpecialFunction EmptyCtx -- ln(10)++ -- circular trigonometry functions+ Sin :: SpecialFunction (EmptyCtx ::> R) -- sin(x)+ Cos :: SpecialFunction (EmptyCtx ::> R) -- cos(x)+ Tan :: SpecialFunction (EmptyCtx ::> R) -- tan(x) = sin(x)/cos(x)+ Arcsin :: SpecialFunction (EmptyCtx ::> R) -- inverse sin+ Arccos :: SpecialFunction (EmptyCtx ::> R) -- inverse cos+ Arctan :: SpecialFunction (EmptyCtx ::> R) -- inverse tan++ -- hyperbolic trigonometry functions+ Sinh :: SpecialFunction (EmptyCtx ::> R) -- sinh(x) (hyperbolic sine)+ Cosh :: SpecialFunction (EmptyCtx ::> R) -- cosh(x)+ Tanh :: SpecialFunction (EmptyCtx ::> R) -- tanh(x)+ Arcsinh :: SpecialFunction (EmptyCtx ::> R) -- inverse sinh+ Arccosh :: SpecialFunction (EmptyCtx ::> R) -- inverse cosh+ Arctanh :: SpecialFunction (EmptyCtx ::> R) -- inverse tanh++ -- rectangular to polar coordinate conversion+ Hypot :: SpecialFunction (EmptyCtx ::> R ::> R) -- hypot(x,y) = sqrt(x^2 + y^2)+ Arctan2 :: SpecialFunction (EmptyCtx ::> R ::> R) -- atan2(y,x) = atan(y/x)++ -- exponential and logarithm functions+ Pow :: SpecialFunction (EmptyCtx ::> R ::> R) -- x^y+ Exp :: SpecialFunction (EmptyCtx ::> R) -- exp(x)+ Log :: SpecialFunction (EmptyCtx ::> R) -- ln(x)+ Expm1 :: SpecialFunction (EmptyCtx ::> R) -- exp(x) - 1+ Log1p :: SpecialFunction (EmptyCtx ::> R) -- ln(1+x)++ -- base 2 exponential and logarithm+ Exp2 :: SpecialFunction (EmptyCtx ::> R) -- 2^x+ Log2 :: SpecialFunction (EmptyCtx ::> R) -- log_2(x)++ -- base 10 exponential and logarithm+ Exp10 :: SpecialFunction (EmptyCtx ::> R) -- 10^x+ Log10 :: SpecialFunction (EmptyCtx ::> R) -- log_10(x)++instance Show (SpecialFunction args) where+ show fn = case fn of+ Pi -> "pi"+ HalfPi -> "halfPi"+ QuarterPi -> "quaterPi"+ OneOverPi -> "oneOverPi"+ TwoOverPi -> "twoOverPi"+ TwoOverSqrt_Pi -> "twoOverSqrt_Pi"+ Sqrt_2 -> "sqrt_2"+ Sqrt_OneHalf -> "sqrt_oneHalf"++ E -> "e"+ Log2_E -> "log2_e"+ Log10_E -> "log10_e"+ Ln_2 -> "ln_2"+ Ln_10 -> "ln_10"++ Sin -> "sin"+ Cos -> "cos"+ Tan -> "tan"+ Arcsin -> "arcsin"+ Arccos -> "arccos"+ Arctan -> "arctan"++ Sinh -> "sinh"+ Cosh -> "cosh"+ Tanh -> "tanh"+ Arcsinh -> "arcsinh"+ Arccosh -> "arccosh"+ Arctanh -> "arctanh"++ Hypot -> "hypot"+ Arctan2 -> "atan2"++ Pow -> "pow"+ Exp -> "exp"+ Log -> "ln"+ Expm1 -> "expm1"+ Log1p -> "log1p"+ Exp2 -> "exp2"+ Log2 -> "log2"+ Exp10 -> "exp10"+ Log10 -> "log10"++-- | Values that can appear in the definition of domain and+-- range intervals for special functions.+data RealPoint+ = Zero+ | NegOne+ | PosOne+ | NegInf+ | PosInf+ | NegPi+ | PosPi+ | NegHalfPi+ | PosHalfPi++instance Show RealPoint where+ show Zero = "0"+ show NegOne = "-1"+ show PosOne = "+1"+ show NegInf = "-∞"+ show PosInf = "+∞"+ show NegPi = "-π"+ show PosPi = "+π"+ show NegHalfPi = "-π/2"+ show PosHalfPi = "+π/2"++-- | The endpoint of an interval, which may be inclusive or exclusive.+data RealBound+ = Incl RealPoint+ | Excl RealPoint++-- | An interval on real values, or a point.+data RealInterval r where+ RealPoint :: SpecialFunction EmptyCtx -> RealInterval R+ RealInterval :: RealBound -> RealBound -> RealInterval R++instance Show (RealInterval r) where+ show (RealPoint x) = show x+ show (RealInterval lo hi) = lostr ++ ", " ++ histr+ where+ lostr = case lo of+ Incl x -> "[" ++ show x+ Excl x -> "(" ++ show x+ histr = case hi of+ Incl x -> show x ++ "]"+ Excl x -> show x ++ ")"++-- | Compute function symmetry information for the given special function.+specialFnSymmetry :: SpecialFunction args -> Ctx.Assignment FunctionSymmetry args+specialFnSymmetry fn = case fn of+ Pi -> Ctx.Empty+ HalfPi -> Ctx.Empty+ QuarterPi -> Ctx.Empty+ OneOverPi -> Ctx.Empty+ TwoOverPi -> Ctx.Empty+ TwoOverSqrt_Pi -> Ctx.Empty+ Sqrt_2 -> Ctx.Empty+ Sqrt_OneHalf -> Ctx.Empty+ E -> Ctx.Empty+ Log2_E -> Ctx.Empty+ Log10_E -> Ctx.Empty+ Ln_2 -> Ctx.Empty+ Ln_10 -> Ctx.Empty++ Sin -> Ctx.Empty :> OddFunction+ Cos -> Ctx.Empty :> EvenFunction+ Tan -> Ctx.Empty :> OddFunction+ Arcsin -> Ctx.Empty :> OddFunction+ Arccos -> Ctx.Empty :> NoSymmetry+ Arctan -> Ctx.Empty :> OddFunction++ Sinh -> Ctx.Empty :> OddFunction+ Cosh -> Ctx.Empty :> EvenFunction+ Tanh -> Ctx.Empty :> OddFunction+ Arcsinh -> Ctx.Empty :> OddFunction+ Arccosh -> Ctx.Empty :> NoSymmetry+ Arctanh -> Ctx.Empty :> OddFunction++ Pow -> Ctx.Empty :> NoSymmetry :> NoSymmetry+ Exp -> Ctx.Empty :> NoSymmetry+ Log -> Ctx.Empty :> NoSymmetry+ Expm1 -> Ctx.Empty :> NoSymmetry+ Log1p -> Ctx.Empty :> NoSymmetry+ Exp2 -> Ctx.Empty :> NoSymmetry+ Log2 -> Ctx.Empty :> NoSymmetry+ Exp10 -> Ctx.Empty :> NoSymmetry+ Log10 -> Ctx.Empty :> NoSymmetry++ Hypot -> Ctx.Empty :> EvenFunction :> EvenFunction+ Arctan2 -> Ctx.Empty :> OddFunction :> NoSymmetry+++-- | Compute the range of values that may be returned by the given special function+-- as its arguments take on the possible values of its domain. This may include+-- limiting values if the function's domain includes infinities; for example+-- @exp(-inf) = 0@.+specialFnRange :: SpecialFunction args -> RealInterval R+specialFnRange fn = case fn of+ Pi -> RealPoint Pi+ HalfPi -> RealPoint HalfPi+ QuarterPi -> RealPoint QuarterPi+ OneOverPi -> RealPoint OneOverPi+ TwoOverPi -> RealPoint TwoOverPi+ TwoOverSqrt_Pi -> RealPoint TwoOverSqrt_Pi+ Sqrt_2 -> RealPoint Sqrt_2+ Sqrt_OneHalf -> RealPoint Sqrt_OneHalf+ E -> RealPoint E+ Log2_E -> RealPoint Log2_E+ Log10_E -> RealPoint Log10_E+ Ln_2 -> RealPoint Ln_2+ Ln_10 -> RealPoint Ln_10++ Sin -> RealInterval (Incl NegOne) (Incl PosOne)+ Cos -> RealInterval (Incl NegOne) (Incl PosOne)+ Tan -> RealInterval (Incl NegInf) (Incl PosInf)++ Arcsin -> RealInterval (Incl NegHalfPi) (Incl PosHalfPi)+ Arccos -> RealInterval (Incl Zero) (Incl PosPi)+ Arctan -> RealInterval (Incl NegHalfPi) (Incl PosHalfPi)++ Sinh -> RealInterval (Incl NegInf) (Incl PosInf)+ Cosh -> RealInterval (Incl PosOne) (Incl PosInf)+ Tanh -> RealInterval (Incl NegOne) (Incl PosOne)+ Arcsinh -> RealInterval (Incl NegInf) (Incl PosInf)+ Arccosh -> RealInterval (Incl Zero) (Incl PosInf)+ Arctanh -> RealInterval (Incl NegInf) (Incl PosInf)++ Pow -> RealInterval (Incl NegInf) (Incl PosInf)+ Exp -> RealInterval (Incl Zero) (Incl PosInf)+ Log -> RealInterval (Incl NegInf) (Incl PosInf)+ Expm1 -> RealInterval (Incl NegOne) (Incl PosInf)+ Log1p -> RealInterval (Incl NegInf) (Incl PosInf)+ Exp2 -> RealInterval (Incl Zero) (Incl PosInf)+ Log2 -> RealInterval (Incl NegInf) (Incl PosInf)+ Exp10 -> RealInterval (Incl Zero) (Incl PosInf)+ Log10 -> RealInterval (Incl NegInf) (Incl PosInf)++ Hypot -> RealInterval (Incl Zero) (Incl PosInf)+ Arctan2 -> RealInterval (Incl NegPi) (Incl PosPi)+++-- | Compute the domain of the given special function. As a mathematical+-- entity, the value of the given function is not well-defined outside+-- its domain. In floating-point terms, a special function will return+-- a @NaN@ when evaluated on arguments outside its domain.+specialFnDomain :: SpecialFunction args -> Ctx.Assignment RealInterval args+specialFnDomain fn = case fn of+ Pi -> Ctx.Empty+ HalfPi -> Ctx.Empty+ QuarterPi -> Ctx.Empty+ OneOverPi -> Ctx.Empty+ TwoOverPi -> Ctx.Empty+ TwoOverSqrt_Pi -> Ctx.Empty+ Sqrt_2 -> Ctx.Empty+ Sqrt_OneHalf -> Ctx.Empty+ E -> Ctx.Empty+ Log2_E -> Ctx.Empty+ Log10_E -> Ctx.Empty+ Ln_2 -> Ctx.Empty+ Ln_10 -> Ctx.Empty++ Sin -> Ctx.Empty :> RealInterval (Excl NegInf) (Excl PosInf)+ Cos -> Ctx.Empty :> RealInterval (Excl NegInf) (Excl PosInf)+ Tan -> Ctx.Empty :> RealInterval (Excl NegInf) (Excl PosInf)+ Arcsin -> Ctx.Empty :> RealInterval (Incl NegOne) (Incl PosOne)+ Arccos -> Ctx.Empty :> RealInterval (Incl NegOne) (Incl PosOne)+ Arctan -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)++ Sinh -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ Cosh -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ Tanh -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ Arcsinh -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ Arccosh -> Ctx.Empty :> RealInterval (Incl PosOne) (Incl PosInf)+ Arctanh -> Ctx.Empty :> RealInterval (Incl NegOne) (Incl PosOne)++ Pow -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ :> RealInterval (Incl NegInf) (Incl PosInf)+ Exp -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ Log -> Ctx.Empty :> RealInterval (Incl Zero) (Incl PosInf)+ Expm1 -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ Log1p -> Ctx.Empty :> RealInterval (Incl NegOne) (Incl PosInf)+ Exp2 -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ Log2 -> Ctx.Empty :> RealInterval (Incl Zero) (Incl PosInf)+ Exp10 -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ Log10 -> Ctx.Empty :> RealInterval (Incl Zero) (Incl PosInf)++ Hypot -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ :> RealInterval (Incl NegInf) (Incl PosInf)+ Arctan2 -> Ctx.Empty :> RealInterval (Incl NegInf) (Incl PosInf)+ :> RealInterval (Incl NegInf) (Incl PosInf)++-- | Data type for wrapping the actual arguments to special functions.+data SpecialFnArg (e :: k -> Type) (tp::k) (r::Type) where+ SpecialFnArg :: e tp -> SpecialFnArg e tp R++-- | Data type for wrapping a collction of actual arguments to special functions.+newtype SpecialFnArgs (e :: k -> Type) (tp :: k) args =+ SpecialFnArgs (Ctx.Assignment (SpecialFnArg e tp) args)++$(return [])++instance HashableF SpecialFunction where+ hashWithSaltF = $(structuralHashWithSalt [t|SpecialFunction|] [])++instance Hashable (SpecialFunction args) where+ hashWithSalt = hashWithSaltF++instance TestEquality SpecialFunction where+ testEquality = $(structuralTypeEquality [t|SpecialFunction|] [])++instance Eq (SpecialFunction args) where+ x == y = isJust (testEquality x y)++instance OrdF SpecialFunction where+ compareF = $(structuralTypeOrd [t|SpecialFunction|] [])+++instance OrdF e => TestEquality (SpecialFnArg e tp) where+ testEquality (SpecialFnArg x) (SpecialFnArg y) =+ do Refl <- testEquality x y+ return Refl++instance OrdF e => OrdF (SpecialFnArg e tp) where+ compareF (SpecialFnArg x) (SpecialFnArg y) =+ case compareF x y of+ LTF -> LTF+ EQF -> EQF+ GTF -> GTF++instance HashableF e => HashableF (SpecialFnArg e tp) where+ hashWithSaltF s (SpecialFnArg x) = hashWithSaltF s x+++instance OrdF e => Eq (SpecialFnArgs e tp r) where+ SpecialFnArgs xs == SpecialFnArgs ys = xs == ys++instance OrdF e => Ord (SpecialFnArgs e tp r) where+ compare (SpecialFnArgs xs) (SpecialFnArgs ys) = compare xs ys++instance (HashableF e, OrdF e) => Hashable (SpecialFnArgs e tp args) where+ hashWithSalt s (SpecialFnArgs xs) = hashWithSaltF s xs+++traverseSpecialFnArg :: Applicative m =>+ (e tp -> m (f tp)) ->+ SpecialFnArg e tp r -> m (SpecialFnArg f tp r)+traverseSpecialFnArg f (SpecialFnArg x) = SpecialFnArg <$> f x++traverseSpecialFnArgs :: Applicative m =>+ (e tp -> m (f tp)) ->+ SpecialFnArgs e tp r -> m (SpecialFnArgs f tp r)+traverseSpecialFnArgs f (SpecialFnArgs xs) =+ SpecialFnArgs <$> traverseFC (traverseSpecialFnArg f) xs
src/What4/Utils/AbstractDomains.hs view
@@ -20,11 +20,13 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-} module What4.Utils.AbstractDomains ( ValueBound(..)@@ -32,6 +34,7 @@ , maxValueBound -- * ValueRange , ValueRange(..)+ , pattern MultiRange , unboundedRange , mapRange , rangeLowBound@@ -160,15 +163,52 @@ data ValueRange tp = SingleRange !tp -- ^ Indicates that range denotes a single value- | MultiRange !(ValueBound tp) !(ValueBound tp)- -- ^ Indicates that the number is somewhere between the given upper and lower bound.+ | UnboundedRange+ -- ^ The number is unconstrained.+ | MinRange !tp+ -- ^ The number is greater than or equal to the given lower bound.+ | MaxRange !tp+ -- ^ The number is less than or equal to the given upper bound.+ | IntervalRange !tp !tp+ -- ^ The number is between the given lower and upper bounds. +asMultiRange :: ValueRange tp -> Maybe (ValueBound tp, ValueBound tp)+asMultiRange r =+ case r of+ SingleRange _ -> Nothing+ UnboundedRange -> Just (Unbounded, Unbounded)+ MinRange lo -> Just (Inclusive lo, Unbounded)+ MaxRange hi -> Just (Unbounded, Inclusive hi)+ IntervalRange lo hi -> Just (Inclusive lo, Inclusive hi)++multiRange :: ValueBound tp -> ValueBound tp -> ValueRange tp+multiRange Unbounded Unbounded = UnboundedRange+multiRange Unbounded (Inclusive hi) = MaxRange hi+multiRange (Inclusive lo) Unbounded = MinRange lo+multiRange (Inclusive lo) (Inclusive hi) = IntervalRange lo hi++-- | Indicates that the number is somewhere between the given upper and lower bound.+pattern MultiRange :: ValueBound tp -> ValueBound tp -> ValueRange tp+pattern MultiRange lo hi <- (asMultiRange -> Just (lo, hi)) where+ MultiRange lo hi = multiRange lo hi++{-# COMPLETE SingleRange, MultiRange #-}+ intAbsRange :: ValueRange Integer -> ValueRange Integer-intAbsRange r = case r of- SingleRange x -> SingleRange (abs x)- MultiRange (Inclusive lo) hi | 0 <= lo -> MultiRange (Inclusive lo) hi- MultiRange lo (Inclusive hi) | hi <= 0 -> MultiRange (Inclusive (negate hi)) (negate <$> lo)- MultiRange lo hi -> MultiRange (Inclusive 0) ((\x y -> max (abs x) (abs y)) <$> lo <*> hi)+intAbsRange r =+ case r of+ SingleRange x -> SingleRange (abs x)+ UnboundedRange -> MinRange 0+ MinRange lo+ | 0 <= lo -> r+ | otherwise -> MinRange 0+ MaxRange hi+ | hi <= 0 -> MinRange (negate hi)+ | otherwise -> MinRange 0+ IntervalRange lo hi+ | 0 <= lo -> r+ | hi <= 0 -> IntervalRange (negate hi) (negate lo)+ | otherwise -> IntervalRange 0 (max (abs lo) (abs hi)) -- | Compute an abstract range for integer division. We are using the SMTLib -- division operation, where the division is floor when the divisor is positive@@ -240,11 +280,19 @@ addRange :: Num tp => ValueRange tp -> ValueRange tp -> ValueRange tp-addRange (SingleRange x) (SingleRange y) = SingleRange (x+y)-addRange (SingleRange x) (MultiRange ly uy) = MultiRange ((x+) <$> ly) ((x+) <$> uy)-addRange (MultiRange lx ux) (SingleRange y) = MultiRange ((y+) <$> lx) ((y+) <$> ux)-addRange (MultiRange lx ux) (MultiRange ly uy) =- MultiRange ((+) <$> lx <*> ly) ((+) <$> ux <*> uy)+addRange (SingleRange x) y = mapRange (x+) y+addRange x (SingleRange y) = mapRange (y+) x+addRange UnboundedRange _ = UnboundedRange+addRange _ UnboundedRange = UnboundedRange+addRange (MinRange _) (MaxRange _) = UnboundedRange+addRange (MaxRange _) (MinRange _) = UnboundedRange+addRange (MinRange lx) (MinRange ly) = MinRange (lx+ly)+addRange (MaxRange ux) (MaxRange uy) = MaxRange (ux+uy)+addRange (MinRange lx) (IntervalRange ly _) = MinRange (lx+ly)+addRange (IntervalRange lx _) (MinRange ly) = MinRange (lx+ly)+addRange (MaxRange ux) (IntervalRange _ uy) = MaxRange (ux+uy)+addRange (IntervalRange _ ux) (MaxRange uy) = MaxRange (ux+uy)+addRange (IntervalRange lx ux) (IntervalRange ly uy) = IntervalRange (lx+ly) (ux+uy) -- | Return 'Just True if the range only contains an integer, 'Just False' if it -- contains no integers, and 'Nothing' if the range contains both integers and@@ -258,16 +306,15 @@ rangeIsInteger _ = Nothing -- | Multiply a range by a scalar value-rangeScalarMul :: (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp-rangeScalarMul x (SingleRange y) = SingleRange (x*y)-rangeScalarMul x (MultiRange ly uy)- | x < 0 = MultiRange ((x*) <$> uy) ((x*) <$> ly)- | x == 0 = SingleRange 0- | otherwise = assert (x > 0) $ MultiRange ((x*) <$> ly) ((x*) <$> uy)+rangeScalarMul :: (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp+rangeScalarMul x r =+ case compare x 0 of+ LT -> mapAntiRange (x *) r+ EQ -> SingleRange 0+ GT -> mapRange (x *) r negateRange :: (Num tp) => ValueRange tp -> ValueRange tp-negateRange (SingleRange x) = SingleRange (negate x)-negateRange (MultiRange lo hi) = MultiRange (negate <$> hi) (negate <$> lo)+negateRange = mapAntiRange negate -- | Multiply two ranges together. mulRange :: (Ord tp, Num tp) => ValueRange tp -> ValueRange tp -> ValueRange tp@@ -372,13 +419,13 @@ -- | Defines a unbounded value range. unboundedRange :: ValueRange tp-unboundedRange = MultiRange Unbounded Unbounded+unboundedRange = UnboundedRange -- | Defines a unbounded value range. concreteRange :: Eq tp => tp -> tp -> ValueRange tp concreteRange x y | x == y = SingleRange x- | otherwise = MultiRange (Inclusive x) (Inclusive y)+ | otherwise = IntervalRange x y -- | Defines a value range containing a single element. singleRange :: tp -> ValueRange tp@@ -395,9 +442,25 @@ asSingleRange (SingleRange x) = Just x asSingleRange _ = Nothing +-- | Map a monotonic function over a range. mapRange :: (a -> b) -> ValueRange a -> ValueRange b-mapRange f (SingleRange x) = SingleRange (f x)-mapRange f (MultiRange l u) = MultiRange (f <$> l) (f <$> u)+mapRange f r =+ case r of+ SingleRange x -> SingleRange (f x)+ UnboundedRange -> UnboundedRange+ MinRange l -> MinRange (f l)+ MaxRange h -> MaxRange (f h)+ IntervalRange l h -> IntervalRange (f l) (f h)++-- | Map an anti-monotonic function over a range.+mapAntiRange :: (a -> b) -> ValueRange a -> ValueRange b+mapAntiRange f r =+ case r of+ SingleRange x -> SingleRange (f x)+ UnboundedRange -> UnboundedRange+ MinRange l -> MaxRange (f l)+ MaxRange h -> MinRange (f h)+ IntervalRange l h -> IntervalRange (f h) (f l) ------------------------------------------------------------------------ -- AbstractValue definition.
src/What4/Utils/AnnotatedMap.hs view
@@ -33,6 +33,7 @@ , unionWithKeyMaybe , filter , mapMaybe+ , mapMaybeWithKey , traverseMaybeWithKey , difference , mergeWithKey@@ -284,6 +285,15 @@ mapMaybe f (AnnotatedMap ft) = AnnotatedMap (mapMaybeFingerTree g ft) where g (Entry k v a) = Entry k v <$> f a++mapMaybeWithKey ::+ (Ord k, Semigroup v2) =>+ (k -> v1 -> a1 -> Maybe (v2, a2)) ->+ AnnotatedMap k v1 a1 -> AnnotatedMap k v2 a2+mapMaybeWithKey f (AnnotatedMap ft) =+ AnnotatedMap (mapMaybeFingerTree g ft)+ where+ g (Entry k v1 x1) = (\(v2, x2) -> Entry k v2 x2) <$> f k v1 x1 traverseMaybeWithKey :: (Applicative f, Ord k, Semigroup v2) =>
src/What4/Utils/OnlyIntRepr.hs view
@@ -25,6 +25,9 @@ instance TestEquality OnlyIntRepr where testEquality OnlyIntRepr OnlyIntRepr = Just Refl +instance Eq (OnlyIntRepr tp) where+ OnlyIntRepr == OnlyIntRepr = True+ instance Hashable (OnlyIntRepr tp) where hashWithSalt s OnlyIntRepr = s
src/What4/Utils/Process.hs view
@@ -93,6 +93,7 @@ , std_err = CreatePipe , create_group = False , cwd = mcwd+ , delegate_ctlc = True } createProcess create_proc >>= \case (Just in_h, Just out_h, Just err_h, ph) -> return (in_h, out_h, err_h, ph)@@ -102,7 +103,7 @@ ] ++ args -- | Filtering function for use with `catchJust` or `tryJust`--- that filters out asynch exceptions so they are rethrown+-- that filters out async exceptions so they are rethrown -- instead of captured filterAsync :: SomeException -> Maybe SomeException filterAsync e
+ src/What4/Utils/ResolveBounds/BV.hs view
@@ -0,0 +1,339 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}++{-|+Module : What4.Utils.ResolveBounds.BV+Description : Resolve the lower and upper bounds of a SymBV+Copyright : (c) Galois, Inc 2021+License : BSD3+Maintainer : Ryan Scott <rscott@galois.com>++A utility for using an 'WPO.OnlineSolver' to query if a 'WI.SymBV' is concrete+or symbolic, and if it is symbolic, what the lower and upper bounds are.+-}+module What4.Utils.ResolveBounds.BV+ ( resolveSymBV+ , SearchStrategy(..)+ , ResolvedSymBV(..)+ ) where++import Data.BitVector.Sized ( BV )+import qualified Data.BitVector.Sized as BV+import qualified Data.Parameterized.NatRepr as PN+import qualified Prettyprinter as PP++import qualified What4.Expr.Builder as WEB+import qualified What4.Expr.GroundEval as WEG+import qualified What4.Interface as WI+import qualified What4.Protocol.Online as WPO+import qualified What4.Protocol.SMTWriter as WPS+import qualified What4.SatResult as WSat+import qualified What4.Utils.BVDomain.Arith as WUBA++-- | The results of an 'WPO.OnlineSolver' trying to resolve a 'WI.SymBV' as+-- concrete.+data ResolvedSymBV w+ = BVConcrete (BV w)+ -- ^ A concrete bitvector, including its value as a 'BV'.+ | BVSymbolic (WUBA.Domain w)+ -- ^ A symbolic 'SymBV', including its lower and upper bounds as a+ -- 'WUBA.Domain'.++instance Show (ResolvedSymBV w) where+ showsPrec _p res =+ case res of+ BVConcrete bv ->+ showString "BVConcrete " . showsPrec 11 bv+ BVSymbolic d ->+ let (lb, ub) = WUBA.ubounds d in+ showString "BVSymbolic ["+ . showsPrec 11 lb+ . showString ", "+ . showsPrec 11 ub+ . showString "]"++-- | The strategy to use to search for lower and upper bounds in+-- 'resolveSymBV'.+data SearchStrategy+ = ExponentialSearch+ -- ^ After making an initial guess for a bound, increase (for upper bounds)+ -- or decrease (for lower bounds) the initial guess by an exponentially+ -- increasing amount (1, 2, 4, 8, ...) until the bound has been exceeded.+ -- At that point, back off from exponential search and use binary search+ -- until the bound has been determined.+ --+ -- For many use cases, this is a reasonable default.+ | BinarySearch+ -- ^ Use binary search to found each bound, using @0@ as the leftmost+ -- bounds of the search and 'BV.maxUnsigned' as the rightmost bounds of+ -- the search.++ -- Some possibilities for additional search strategies include:+ --+ -- - Using Z3's minimize/maximize commands. See+ -- https://github.com/GaloisInc/what4/issues/188+ --+ -- - A custom, user-specified strategy that uses callback(s) to guide the+ -- search at each iteration.++instance PP.Pretty SearchStrategy where+ pretty ExponentialSearch = PP.pretty "exponential search"+ pretty BinarySearch = PP.pretty "binary search"++-- | Use an 'WPO.OnlineSolver' to attempt to resolve a 'WI.SymBV' as concrete.+-- If it cannot, return the lower and upper bounds. This is primarly intended+-- for compound expressions whose bounds cannot trivially be determined by+-- using 'WI.signedBVBounds' or 'WI.unsignedBVBounds'.+resolveSymBV ::+ forall w sym solver scope st fs+ . ( 1 PN.<= w+ , sym ~ WEB.ExprBuilder scope st fs+ , WPO.OnlineSolver solver+ )+ => sym+ -> SearchStrategy+ -- ^ The strategy to use when searching for lower and upper bounds. For+ -- many use cases, 'ExponentialSearch' is a reasonable default.+ -> PN.NatRepr w+ -- ^ The bitvector width+ -> WPO.SolverProcess scope solver+ -- ^ The online solver process to use to search for lower and upper+ -- bounds.+ -> WI.SymBV sym w+ -- ^ The bitvector to resolve.+ -> IO (ResolvedSymBV w)+resolveSymBV sym searchStrat w proc symBV =+ -- First check, if the SymBV can be trivially resolved as concrete. If so,+ -- this can avoid the need to call out to the solver at all.+ case WI.asBV symBV of+ Just bv -> pure $ BVConcrete bv+ -- Otherwise, we need to consult the solver.+ Nothing -> do+ -- First, ask for a particular model of the SymBV...+ modelForBV <- WPO.inNewFrame proc $ do+ msat <- WPO.checkAndGetModel proc "resolveSymBV (check with initial assumptions)"+ model <- case msat of+ WSat.Unknown -> failUnknown+ WSat.Unsat{} -> fail "resolveSymBV: Initial assumptions are unsatisfiable"+ WSat.Sat model -> pure model+ WEG.groundEval model symBV+ -- ...next, check if this is the only possible model for this SymBV. We+ -- do this by adding a blocking clause that assumes the SymBV is /not/+ -- equal to the model we found in the previous step. If this is+ -- unsatisfiable, the SymBV can only be equal to that model, so we can+ -- conclude it is concrete. If it is satisfiable, on the other hand, the+ -- SymBV can be multiple values, so it is truly symbolic.+ isSymbolic <- WPO.inNewFrame proc $ do+ block <- WI.notPred sym =<< WI.bvEq sym symBV =<< WI.bvLit sym w modelForBV+ WPS.assume conn block+ msat <- WPO.check proc "resolveSymBV (check under assumption that model cannot happen)"+ case msat of+ WSat.Unknown -> failUnknown+ WSat.Sat{} -> pure True -- Truly symbolic+ WSat.Unsat{} -> pure False -- Concrete+ if isSymbolic+ then+ -- If we have a truly symbolic SymBV, search for its lower and upper+ -- bounds, using the model from the previous step as a starting point+ -- for the search.+ case searchStrat of+ ExponentialSearch -> do+ -- Use the model from the previous step as the initial guess for+ -- each bound+ lowerBound <- computeLowerBoundExponential modelForBV+ upperBound <- computeUpperBoundExponential modelForBV+ pure $ BVSymbolic $ WUBA.range w+ (BV.asUnsigned lowerBound) (BV.asUnsigned upperBound)+ BinarySearch -> do+ lowerBound <- computeLowerBoundBinary bvZero bvMaxUnsigned+ upperBound <- computeUpperBoundBinary bvZero bvMaxUnsigned+ pure $ BVSymbolic $ WUBA.range w+ (BV.asUnsigned lowerBound) (BV.asUnsigned upperBound)+ else pure $ BVConcrete modelForBV+ where+ conn :: WPS.WriterConn scope solver+ conn = WPO.solverConn proc++ failUnknown :: forall a. IO a+ failUnknown = fail "resolveSymBV: Resolving value yielded UNKNOWN"++ bvZero :: BV w+ bvZero = BV.zero w++ bvOne :: BV w+ bvOne = BV.one w++ bvTwo :: BV w+ bvTwo = BV.mkBV w 2++ bvMaxUnsigned :: BV w+ bvMaxUnsigned = BV.maxUnsigned w++ -- The general strategy for finding a bound is that we start searching+ -- from a particular value known to be within bounds. At each step, we+ -- change this value by exponentially increasing amount, then check if we+ -- have exceeded the bound by using the solver. If so, we then fall back to+ -- binary search to determine an exact bound. If we are within bounds, we+ -- repeat the process.+ --+ -- As an example, let's suppose we having a symbolic value with bounds of+ -- [0, 12], and we start searching for the upper bound at the value 1:+ --+ -- * In the first step, we add 1 to the starting value to get 2. We check+ -- if two has exceeded the upper bound using the solver. This is not the+ -- case, so we continue.+ -- * In the second step, we add 2 to the starting value. The result, 3,+ -- is within bounds.+ -- * We continue like this in the third and fourth steps, except that+ -- we add 4 and 8 to the starting value to get 5 and 9, respectively.+ -- * In the fifth step, we add 16 to the starting value. The result, 17,+ -- has exceeded the upper bound. We will now fall back to binary search,+ -- using the previous result (9) as the leftmost bounds of the search and+ -- the current result (17) as the rightmost bounds of the search.+ -- * Eventually, binary search discovers that 12 is the upper bound.+ --+ -- Note that at each step, we must also check to make sure that the amount+ -- to increase the starting value by does not cause a numeric overflow. If+ -- this would be the case, we fall back to binary search, using+ -- BV.maxUnsigned as the rightmost bounds of the search.+ --+ -- The process for finding a lower bound is quite similar, except that we+ -- /subtract/ an exponentially increasing amount from the starting value+ -- each time rather than adding it.++ computeLowerBoundExponential :: BV w -> IO (BV w)+ computeLowerBoundExponential start = go start bvOne+ where+ go :: BV w -> BV w -> IO (BV w)+ go previouslyTried diff+ | -- If the diff is larger than the starting value, then subtracting+ -- the diff from the starting value would cause underflow. Instead,+ -- just fall back to binary search, using 0 as the leftmost bounds+ -- of the search.+ start `BV.ult` diff+ = computeLowerBoundBinary bvZero previouslyTried++ | -- Otherwise, check if (start - diff) exceeds the lower bound for+ -- the symBV.+ otherwise+ = do let nextToTry = BV.sub w start diff+ exceedsLB <- checkExceedsLowerBound nextToTry+ if | -- If we have exceeded the lower bound, fall back to+ -- binary search.+ exceedsLB+ -> computeLowerBoundBinary nextToTry previouslyTried+ | -- Make sure that (diff * 2) doesn't overflow. If it+ -- would, fall back to binary search.+ BV.asUnsigned diff * 2 > BV.asUnsigned bvMaxUnsigned+ -> computeLowerBoundBinary bvZero nextToTry+ | -- Otherwise, keep exponentially searching.+ otherwise+ -> go nextToTry $ BV.mul w diff bvTwo++ -- Search for the upper bound of the SymBV. This function assumes the+ -- following invariants:+ --+ -- * l <= r+ --+ -- * The lower bound of the SymBV is somewhere within the range [l, r].+ computeLowerBoundBinary :: BV w -> BV w -> IO (BV w)+ computeLowerBoundBinary l r+ | -- If the leftmost and rightmost bounds are the same, we are done.+ l == r+ = pure l++ | -- If the leftmost and rightmost bounds of the search are 1 apart, we+ -- only have two possible choices for the lower bound. Consult the+ -- solver to determine which one is the lower bound.+ BV.sub w r l < bvTwo+ = do lExceedsLB <- checkExceedsLowerBound l+ pure $ if lExceedsLB then r else l++ | -- Otherwise, keep binary searching.+ otherwise+ = do let nextToTry = BV.mkBV w ((BV.asUnsigned l + BV.asUnsigned r) `div` 2)+ exceedsLB <- checkExceedsLowerBound nextToTry+ if exceedsLB+ then computeLowerBoundBinary nextToTry r+ else computeLowerBoundBinary l nextToTry++ checkExceedsLowerBound :: BV w -> IO Bool+ checkExceedsLowerBound bv = WPO.inNewFrame proc $ do+ leLowerBound <- WI.bvUle sym symBV =<< WI.bvLit sym w bv+ WPS.assume conn leLowerBound+ msat <- WPO.check proc "resolveSymBV (check if lower bound has been exceeded)"+ case msat of+ WSat.Unknown -> failUnknown+ WSat.Sat{} -> pure False+ WSat.Unsat{} -> pure True -- symBV cannot be <= this value,+ -- so the value must be strictly+ -- less than the lower bound.++ computeUpperBoundExponential :: BV w -> IO (BV w)+ computeUpperBoundExponential start = go start bvOne+ where+ go :: BV w -> BV w -> IO (BV w)+ go previouslyTried diff+ | -- Make sure that adding the diff to the starting value will not+ -- result in overflow. If it would, just fall back to binary+ -- search, using BV.maxUnsigned as the rightmost bounds of the+ -- search.+ BV.asUnsigned start + BV.asUnsigned diff > BV.asUnsigned bvMaxUnsigned+ = computeUpperBoundBinary previouslyTried bvMaxUnsigned++ | otherwise+ = do let nextToTry = BV.add w start diff+ exceedsUB <- checkExceedsUpperBound nextToTry+ if | -- If we have exceeded the upper bound, fall back to+ -- binary search.+ exceedsUB+ -> computeUpperBoundBinary previouslyTried nextToTry+ | -- Make sure that (diff * 2) doesn't overflow. If it+ -- would, fall back to binary search.+ BV.asUnsigned diff * 2 > BV.asUnsigned bvMaxUnsigned+ -> computeUpperBoundBinary nextToTry bvMaxUnsigned+ | -- Otherwise, keep exponentially searching.+ otherwise+ -> go nextToTry $ BV.mul w diff bvTwo++ -- Search for the upper bound of the SymBV. This function assumes the+ -- following invariants:+ --+ -- * l <= r+ --+ -- * The upper bound of the SymBV is somewhere within the range [l, r].+ computeUpperBoundBinary :: BV w -> BV w -> IO (BV w)+ computeUpperBoundBinary l r+ | -- If the leftmost and rightmost bounds are the same, we are done.+ l == r+ = pure l++ | -- If the leftmost and rightmost bounds of the search are 1 apart, we+ -- only have two possible choices for the upper bound. Consult the+ -- solver to determine which one is the upper bound.+ BV.sub w r l < bvTwo+ = do rExceedsUB <- checkExceedsUpperBound r+ pure $ if rExceedsUB then l else r++ | -- Otherwise, keep binary searching.+ otherwise+ = do let nextToTry = BV.mkBV w ((BV.asUnsigned l + BV.asUnsigned r) `div` 2)+ exceedsUB <- checkExceedsUpperBound nextToTry+ if exceedsUB+ then computeUpperBoundBinary l nextToTry+ else computeUpperBoundBinary nextToTry r++ checkExceedsUpperBound :: BV w -> IO Bool+ checkExceedsUpperBound bv = WPO.inNewFrame proc $ do+ geUpperBound <- WI.bvUge sym symBV =<< WI.bvLit sym w bv+ WPS.assume conn geUpperBound+ msat <- WPO.check proc "resolveSymBV (check if upper bound has been exceeded)"+ case msat of+ WSat.Unknown -> failUnknown+ WSat.Sat{} -> pure False+ WSat.Unsat{} -> pure True -- symBV cannot be >= this upper bound,+ -- so the value must be strictly+ -- greater than the upper bound.
test/AdapterTest.hs view
@@ -14,22 +14,23 @@ import Control.Exception ( displayException, try, SomeException(..), fromException ) import Control.Lens (folded)-import Control.Monad ( forM, unless, void )+import Control.Monad ( forM, unless ) import Control.Monad.Except ( runExceptT ) import Data.BitVector.Sized ( mkBV ) import Data.Char ( toLower ) import qualified Data.List as L+import Data.Maybe ( fromMaybe ) import Data.Text ( pack )-import System.Exit ( ExitCode(..) )-import System.Process ( readProcessWithExitCode )+import System.Environment ( lookupEnv ) +import ProbeSolvers import Test.Tasty+import Test.Tasty.ExpectedFailure import Test.Tasty.HUnit import Data.Parameterized.Nonce import Data.Parameterized.Some -import qualified What4.BaseTypes as BT import What4.Config import What4.Expr import What4.Interface@@ -38,9 +39,7 @@ import What4.Protocol.VerilogWriter import What4.Solver -data State t = State--allAdapters :: [SolverAdapter State]+allAdapters :: [SolverAdapter EmptyExprBuilderState] allAdapters = [ cvc4Adapter , yicesAdapter@@ -52,7 +51,7 @@ #endif ] <> drealAdpt -drealAdpt :: [SolverAdapter State]+drealAdpt :: [SolverAdapter EmptyExprBuilderState] #ifdef TEST_DREAL drealAdpt = [drealAdapter] #else@@ -60,13 +59,16 @@ #endif -withSym :: SolverAdapter State -> (forall t . ExprBuilder t State (Flags FloatUninterpreted) -> IO a) -> IO a+withSym ::+ SolverAdapter EmptyExprBuilderState ->+ (forall t . ExprBuilder t EmptyExprBuilderState (Flags FloatUninterpreted) -> IO a) ->+ IO a withSym adpt pred_gen = withIONonceGenerator $ \gen ->- do sym <- newExprBuilder FloatUninterpretedRepr State gen+ do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen extendConfig (solver_adapter_config_options adpt) (getConfiguration sym) pred_gen sym -mkSmokeTest :: SolverAdapter State -> TestTree+mkSmokeTest :: SolverAdapter EmptyExprBuilderState -> TestTree mkSmokeTest adpt = testCase (solver_adapter_name adpt) $ withSym adpt $ \sym -> do res <- smokeTest sym adpt@@ -77,7 +79,7 @@ ---------------------------------------------------------------------- -mkConfigTests :: [SolverAdapter State] -> [TestTree]+mkConfigTests :: [SolverAdapter EmptyExprBuilderState] -> [TestTree] mkConfigTests adapters = [ testGroup "deprecated configs" (deprecatedConfigTests adapters)@@ -108,13 +110,13 @@ show e) _ -> assertFailure $ "Expected OptGetFailure exception but got: " <> show err- withAdapters :: [SolverAdapter State]- -> (forall t . ExprBuilder t State (Flags FloatUninterpreted) -> IO a)+ withAdapters :: [SolverAdapter EmptyExprBuilderState]+ -> (forall t . ExprBuilder t EmptyExprBuilderState (Flags FloatUninterpreted) -> IO a) -> IO a withAdapters adptrs op = do (cfgs, _getDefAdapter) <- solverAdapterOptions adptrs withIONonceGenerator $ \gen ->- do sym <- newExprBuilder FloatUninterpretedRepr State gen+ do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen extendConfig cfgs (getConfiguration sym) op sym @@ -349,7 +351,9 @@ Left (SomeException e) -> assertFailure $ show e cmpUnderSomesI settera setterb - , testCase "deprecated dreal_path is equivalent to solver.dreal.path" $+ , (if "dreal" `elem` (solver_adapter_name <$> adapters)+ then id else ignoreTestBecause "dreal not available") $+ testCase "deprecated dreal_path is equivalent to solver.dreal.path" $ withAdapters adaptrs $ \sym -> do #ifdef TEST_DREAL settera <- getOptionSettingFromText "dreal_path"@@ -371,7 +375,9 @@ wantOptGetFailure "not found" settera #endif - , testCase "deprecated abc_path is equivalent to solver.abc.path" $+ , (if "abc" `elem` (solver_adapter_name <$> adapters)+ then id else ignoreTestBecause "abc not available") $+ testCase "deprecated abc_path is equivalent to solver.abc.path" $ withAdapters adaptrs $ \sym -> do settera <- getOptionSettingFromText "abc_path" (getConfiguration sym)@@ -387,7 +393,9 @@ Left (SomeException e) -> assertFailure $ show e cmpUnderSome settera setterb - , testCase "deprecated stp_path is equivalent to solver.stp.path" $+ , (if "stp" `elem` (solver_adapter_name <$> adapters)+ then id else ignoreTestBecause "stp not available") $+ testCase "deprecated stp_path is equivalent to solver.stp.path" $ withAdapters adaptrs $ \sym -> do #ifdef TEST_STP settera <- getOptionSettingFromText "stp_path"@@ -409,7 +417,9 @@ wantOptGetFailure "not found" settera #endif - , testCase "deprecated stp.random-seed is equivalent to solver.stp.random-seed" $+ , (if "stp" `elem` (solver_adapter_name <$> adapters)+ then id else ignoreTestBecause "stp not available") $+ testCase "deprecated stp.random-seed is equivalent to solver.stp.random-seed" $ withAdapters adaptrs $ \sym -> do #ifdef TEST_STP settera <- getOptionSettingFromText "stp.random-seed"@@ -527,8 +537,14 @@ ---------------------------------------------------------------------- -nonlinearRealTest :: SolverAdapter State -> TestTree-nonlinearRealTest adpt = testCase (solver_adapter_name adpt) $+nonlinearRealTest :: SolverAdapter EmptyExprBuilderState -> TestTree+nonlinearRealTest adpt =+ let wrap = if solver_adapter_name adpt `elem` [ "ABC", "boolector", "stp" ]+ then expectFailBecause+ (solver_adapter_name adpt+ <> " does not support this type of linear arithmetic term")+ else id+ in wrap $ testCase (solver_adapter_name adpt) $ withSym adpt $ \sym -> do x <- freshConstant sym (safeSymbol "a") BaseRealRepr y <- freshConstant sym (safeSymbol "b") BaseRealRepr@@ -564,8 +580,13 @@ ((-2) <= x2_y' && x2_y' <= (-1)) @? "correct bounds" -mkQuickstartTest :: SolverAdapter State -> TestTree-mkQuickstartTest adpt = testCase (solver_adapter_name adpt) $+mkQuickstartTest :: SolverAdapter EmptyExprBuilderState -> TestTree+mkQuickstartTest adpt =+ let wrap = if solver_adapter_name adpt == "stp"+ then ignoreTestBecause "STP cannot generate the model"+ else id+ in wrap $+ testCase (solver_adapter_name adpt) $ withSym adpt $ \sym -> do -- Let's determine if the following formula is satisfiable: -- f(p, q, r) = (p | !q) & (q | r) & (!p | !r) & (!p | !q | r)@@ -618,7 +639,7 @@ verilogTest :: TestTree verilogTest = testCase "verilogTest" $ withIONonceGenerator $ \gen ->- do sym <- newExprBuilder FloatUninterpretedRepr State gen+ do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen let w = knownNat @8 x <- freshConstant sym (safeSymbol "x") (BaseBVRepr w) one <- bvLit sym w (mkBV w 1)@@ -647,40 +668,19 @@ , "endmodule" ] -getSolverVersion :: String -> IO String-getSolverVersion solver = do- 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- return $ if null ol then (solver <> " v??") else head ol- else return $ solver <> " version error: " <> show r <> " /;/ " <> e- Left (err :: SomeException) -> return $ solver <> " invocation error: " <> show err---reportSolverVersions :: IO ()-reportSolverVersions = do putStrLn "SOLVER VERSIONS::"- void $ mapM rep allAdapters- where rep a = let s = solver_adapter_name a in disp s =<< getSolverVersion s- disp s v = putStrLn $ " Solver " <> s <> " == " <> v-- main :: IO () main = do- reportSolverVersions+ testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"+ let solverNames = SolverName . solver_adapter_name <$> allAdapters+ solvers <- reportSolverVersions testLevel (SolverName . solver_adapter_name)+ =<< (zip allAdapters <$> mapM getSolverVersion solverNames)+ let adapters = fst <$> solvers defaultMain $ 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- ([ cvc4Adapter, z3Adapter, yicesAdapter ] <> drealAdpt)+ [ testGroup "SmokeTest" $ map mkSmokeTest adapters+ , testGroup "Config Tests" $ mkConfigTests adapters+ , testGroup "QuickStart" $ map mkQuickstartTest adapters+ , testGroup "nonlinear reals" $ map nonlinearRealTest adapters , testGroup "Verilog" [verilogTest] ]
test/ExprBuilderSMTLib2.hs view
@@ -2,26 +2,40 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-}--import Test.Tasty-import Test.Tasty.HUnit+{-# OPTIONS_GHC -fno-warn-orphans #-} -- for TestShow instance +import ProbeSolvers+import Test.Tasty+import Test.Tasty.Checklist as TC+import Test.Tasty.ExpectedFailure+import Test.Tasty.Hedgehog.Alt+import Test.Tasty.HUnit import Control.Exception (bracket, try, finally, SomeException) import Control.Monad (void)+import Control.Monad.IO.Class (MonadIO(..)) import qualified Data.BitVector.Sized as BV-import qualified Data.ByteString as BS-import qualified Data.Map as Map import Data.Foldable+import qualified Data.Map as Map+import Data.Maybe ( fromMaybe )+import Data.Parameterized.Context ( pattern Empty, pattern (:>) )+import qualified Data.Text as Text+import qualified Hedgehog as H+import qualified Hedgehog.Gen as HGen+import qualified Hedgehog.Range as HRange+import qualified Prettyprinter as PP+import System.Environment ( lookupEnv ) import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Nonce@@ -29,26 +43,30 @@ import System.IO import LibBF -import What4.BaseTypes-import What4.Config-import What4.Expr-import What4.Interface-import What4.InterpretedFloatingPoint-import What4.Protocol.Online-import What4.Protocol.SMTLib2-import What4.SatResult-import What4.Solver.Adapter+import What4.BaseTypes+import What4.Config+import What4.Expr+import What4.Interface+import What4.InterpretedFloatingPoint+import What4.Protocol.Online+import What4.Protocol.SMTLib2+import What4.SatResult+import What4.Solver.Adapter import qualified What4.Solver.CVC4 as CVC4 import qualified What4.Solver.Z3 as Z3 import qualified What4.Solver.Yices as Yices-import What4.Utils.StringLiteral-import What4.Utils.Versions (ver, SolverBounds(..), emptySolverBounds)+import qualified What4.Utils.BVDomain as WUB+import qualified What4.Utils.BVDomain.Arith as WUBA+import qualified What4.Utils.ResolveBounds.BV as WURB+import What4.Utils.StringLiteral+import What4.Utils.Versions (ver, SolverBounds(..), emptySolverBounds) -data State t = State data SomePred = forall t . SomePred (BoolExpr t) deriving instance Show SomePred-type SimpleExprBuilder t fs = ExprBuilder t State fs+type SimpleExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs +instance TestShow Text.Text where testShow = show+instance TestShow (StringLiteral Unicode) where testShow = show debugOutputFiles :: Bool debugOutputFiles = False@@ -66,9 +84,9 @@ withSym :: FloatModeRepr fm -> (forall t . SimpleExprBuilder t (Flags fm) -> IO a) -> IO a withSym floatMode pred_gen = withIONonceGenerator $ \gen ->- pred_gen =<< newExprBuilder floatMode State gen+ pred_gen =<< newExprBuilder floatMode EmptyExprBuilderState gen -withYices :: (forall t. SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t Yices.Connection -> IO ()) -> IO ()+withYices :: (forall t. SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t Yices.Connection -> IO a) -> IO a withYices action = withSym FloatRealRepr $ \sym -> do extendConfig Yices.yicesOptions (getConfiguration sym) bracket@@ -80,7 +98,7 @@ withZ3 :: (forall t . SimpleExprBuilder t (Flags FloatIEEE) -> Session t Z3.Z3 -> IO ()) -> IO () withZ3 action = withIONonceGenerator $ \nonce_gen -> do- sym <- newExprBuilder FloatIEEERepr State nonce_gen+ sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState nonce_gen extendConfig Z3.z3Options (getConfiguration sym) Z3.withZ3 sym "z3" defaultLogData { logCallbackVerbose = (\_ -> putStrLn) } (action sym) @@ -360,6 +378,76 @@ e4 <- bvOrBits sym e2 e1 show e4 @?= show e3 +arrayCopyTest :: TestTree+arrayCopyTest = testCase "arrayCopy" $ withZ3 $ \sym s -> do+ a <- freshConstant sym (userSymbol' "a") (BaseArrayRepr (Ctx.singleton (BaseBVRepr $ knownNat @64)) (BaseBVRepr $ knownNat @8))+ b <- freshConstant sym (userSymbol' "b") knownRepr+ i <- freshConstant sym (userSymbol' "i") (BaseBVRepr $ knownNat @64)+ j <- freshConstant sym (userSymbol' "j") knownRepr+ k <- freshConstant sym (userSymbol' "k") knownRepr+ n <- freshConstant sym (userSymbol' "n") knownRepr++ copy_a_i_b_j_n <- arrayCopy sym a i b j n+ add_i_k <- bvAdd sym i k+ copy_a_i_b_j_n_at_add_i_k <- arrayLookup sym copy_a_i_b_j_n (Ctx.singleton add_i_k)+ add_j_k <- bvAdd sym j k+ b_at_add_j_k <- arrayLookup sym b (Ctx.singleton add_j_k)++ assume (sessionWriter s) =<< bvUle sym i =<< bvLit sym knownRepr (BV.mkBV knownNat 1024)+ assume (sessionWriter s) =<< bvUle sym j =<< bvLit sym knownRepr (BV.mkBV knownNat 1024)+ assume (sessionWriter s) =<< bvUle sym n =<< bvLit sym knownRepr (BV.mkBV knownNat 1024)++ assume (sessionWriter s) =<< bvNe sym copy_a_i_b_j_n_at_add_i_k b_at_add_j_k++ runCheckSat s $ \res -> isSat res @? "sat"++ assume (sessionWriter s) =<< bvUlt sym k n++ runCheckSat s $ \res -> isUnsat res @? "unsat"++arraySetTest :: TestTree+arraySetTest = testCase "arraySet" $ withZ3 $ \sym s -> do+ a <- freshConstant sym (userSymbol' "a") knownRepr+ i <- freshConstant sym (userSymbol' "i") (BaseBVRepr $ knownNat @64)+ j <- freshConstant sym (userSymbol' "j") knownRepr+ n <- freshConstant sym (userSymbol' "n") knownRepr+ v <- freshConstant sym (userSymbol' "v") (BaseBVRepr $ knownNat @8)++ set_a_i_v_n <- arraySet sym a i v n+ add_i_j <- bvAdd sym i j+ set_a_i_v_n_at_add_i_j <- arrayLookup sym set_a_i_v_n (Ctx.singleton add_i_j)++ assume (sessionWriter s) =<< bvUle sym i =<< bvLit sym knownRepr (BV.mkBV knownNat 1024)+ assume (sessionWriter s) =<< bvUle sym n =<< bvLit sym knownRepr (BV.mkBV knownNat 1024)++ assume (sessionWriter s) =<< bvNe sym v set_a_i_v_n_at_add_i_j++ runCheckSat s $ \res -> isSat res @? "sat"++ assume (sessionWriter s) =<< bvUlt sym j n++ runCheckSat s $ \res -> isUnsat res @? "unsat"++arrayCopySetTest :: TestTree+arrayCopySetTest = testCase "arrayCopy/arraySet" $ withZ3 $ \sym s -> do+ a <- freshConstant sym (userSymbol' "a") knownRepr+ i <- freshConstant sym (userSymbol' "i") (BaseBVRepr $ knownNat @64)+ n <- freshConstant sym (userSymbol' "n") knownRepr+ v <- freshConstant sym (userSymbol' "v") (BaseBVRepr $ knownNat @8)++ const_v <- constantArray sym (Ctx.singleton (BaseBVRepr $ knownNat @64)) v+ z <- bvLit sym knownRepr $ BV.mkBV knownNat 0+ copy_a_i_v_n <- arrayCopy sym a i const_v z n+ set_a_i_v_n <- arraySet sym a i v n++ assume (sessionWriter s) =<< bvUle sym i =<< bvLit sym knownRepr (BV.mkBV knownNat 1024)+ assume (sessionWriter s) =<< bvUle sym n =<< bvLit sym knownRepr (BV.mkBV knownNat 1024)++ p <- notPred sym =<< arrayEq sym copy_a_i_v_n set_a_i_v_n++ assume (sessionWriter s) p+ runCheckSat s $ \res -> isUnsat res @? "unsat"+ testUninterpretedFunctionScope :: TestTree testUninterpretedFunctionScope = testCase "uninterpreted function scope" $ withOnlineZ3 $ \sym s -> do@@ -627,15 +715,15 @@ SimpleExprBuilder t fs -> SolverProcess t solver -> IO ()-stringTest1 sym solver =- do let bsx = "asdf\nasdf"- let bsz = "qwe\x1crty"- let bsw = "QQ\"QQ"+stringTest1 sym solver = withChecklist "string1" $+ do let bsx = "asdf\nasdf" -- length 9+ let bsz = "qwe\x1c\&rty" -- length 7+ let bsw = "QQ\"QQ" -- length 5 - x <- stringLit sym (Char8Literal bsx)- y <- freshConstant sym (userSymbol' "str") (BaseStringRepr Char8Repr)- z <- stringLit sym (Char8Literal bsz)- w <- stringLit sym (Char8Literal bsw)+ x <- stringLit sym (UnicodeLiteral bsx)+ y <- freshConstant sym (userSymbol' "str") (BaseStringRepr UnicodeRepr)+ z <- stringLit sym (UnicodeLiteral bsz)+ w <- stringLit sym (UnicodeLiteral bsw) s <- stringConcat sym x =<< stringConcat sym y z s' <- stringConcat sym s w@@ -647,12 +735,15 @@ checkSatisfiableWithModel solver "test" p $ \case Sat fn ->- do Char8Literal slit <- groundEval fn s'+ do UnicodeLiteral slit <- groundEval fn s' llit <- groundEval fn n - (fromIntegral (BS.length slit) == llit) @? "model string length"- BS.isPrefixOf bsx slit @? "prefix check"- BS.isSuffixOf (bsz <> bsw) slit @? "suffix check"+ slit `checkValues`+ (Empty+ :> Val "model string length" (fromIntegral . Text.length) llit+ :> Got "expected prefix" (Text.isPrefixOf bsx)+ :> Got "expected suffix" (Text.isSuffixOf (bsz <> bsw))+ ) _ -> fail "expected satisfiable model" @@ -667,19 +758,19 @@ SimpleExprBuilder t fs -> SolverProcess t solver -> IO ()-stringTest2 sym solver =+stringTest2 sym solver = withChecklist "string2" $ do let bsx = "asdf\nasdf"- let bsz = "qwe\x1crty"+ let bsz = "qwe\x1c\&rty" let bsw = "QQ\"QQ" q <- freshConstant sym (userSymbol' "q") BaseBoolRepr - x <- stringLit sym (Char8Literal bsx)- z <- stringLit sym (Char8Literal bsz)- w <- stringLit sym (Char8Literal bsw)+ x <- stringLit sym (UnicodeLiteral bsx)+ z <- stringLit sym (UnicodeLiteral bsz)+ w <- stringLit sym (UnicodeLiteral bsw) - a <- freshConstant sym (userSymbol' "stra") (BaseStringRepr Char8Repr)- b <- freshConstant sym (userSymbol' "strb") (BaseStringRepr Char8Repr)+ a <- freshConstant sym (userSymbol' "stra") (BaseStringRepr UnicodeRepr)+ b <- freshConstant sym (userSymbol' "strb") (BaseStringRepr UnicodeRepr) ax <- stringConcat sym x a @@ -699,30 +790,30 @@ bzwlit <- groundEval fn bzw qlit <- groundEval fn q - qlit == False @? "correct ite"- axlit == bzwlit @? "equal strings"+ TC.check "correct ite" (False ==) qlit+ TC.check "equal strings" (axlit ==) bzwlit _ -> fail "expected satisfable model" -_stringTest3 ::- OnlineSolver solver =>+stringTest3 ::+ (OnlineSolver solver) => SimpleExprBuilder t fs -> SolverProcess t solver -> IO ()-_stringTest3 sym solver =- do let bsz = "qwe\x1crtyQQ\"QQ"- z <- stringLit sym (Char8Literal bsz)+stringTest3 sym solver = withChecklist "string3" $+ do let bsz = "qwe\x1c\&rtyQQ\"QQ"+ z <- stringLit sym (UnicodeLiteral bsz) - a <- freshConstant sym (userSymbol' "stra") (BaseStringRepr Char8Repr)- b <- freshConstant sym (userSymbol' "strb") (BaseStringRepr Char8Repr)- c <- freshConstant sym (userSymbol' "strc") (BaseStringRepr Char8Repr)+ a <- freshConstant sym (userSymbol' "stra") (BaseStringRepr UnicodeRepr)+ b <- freshConstant sym (userSymbol' "strb") (BaseStringRepr UnicodeRepr)+ c <- freshConstant sym (userSymbol' "strc") (BaseStringRepr UnicodeRepr) pfx <- stringIsPrefixOf sym a z sfx <- stringIsSuffixOf sym b z cnt1 <- stringContains sym z c- cnt2 <- notPred sym =<< stringContains sym c =<< stringLit sym (Char8Literal "Q")- cnt3 <- notPred sym =<< stringContains sym c =<< stringLit sym (Char8Literal "q")+ cnt2 <- notPred sym =<< stringContains sym c =<< stringLit sym (UnicodeLiteral "Q")+ cnt3 <- notPred sym =<< stringContains sym c =<< stringLit sym (UnicodeLiteral "q") cnt <- andPred sym cnt1 =<< andPred sym cnt2 cnt3 lena <- stringLength sym a@@ -742,13 +833,16 @@ checkSatisfiableWithModel solver "test" p $ \case Sat fn ->- do alit <- fromChar8Lit <$> groundEval fn a- blit <- fromChar8Lit <$> groundEval fn b- clit <- fromChar8Lit <$> groundEval fn c+ do alit <- fromUnicodeLit <$> groundEval fn a+ blit <- fromUnicodeLit <$> groundEval fn b+ clit <- fromUnicodeLit <$> groundEval fn c - alit == (BS.take 9 bsz) @? "correct prefix"- blit == (BS.drop (BS.length bsz - 9) bsz) @? "correct suffix"- clit == (BS.take 6 (BS.drop 1 bsz)) @? "correct middle"+ bsz `checkValues`+ (Empty+ :> Val "correct prefix" (Text.take 9) alit+ :> Val "correct suffix" (Text.reverse . Text.take 9 . Text.reverse) blit+ :> Val "correct middle" (Text.take 6 . Text.drop 1) clit+ ) _ -> fail "expected satisfable model" @@ -758,10 +852,10 @@ SimpleExprBuilder t fs -> SolverProcess t solver -> IO ()-stringTest4 sym solver =+stringTest4 sym solver = withChecklist "string4" $ do let bsx = "str"- x <- stringLit sym (Char8Literal bsx)- a <- freshConstant sym (userSymbol' "stra") (BaseStringRepr Char8Repr)+ x <- stringLit sym (UnicodeLiteral bsx)+ a <- freshConstant sym (userSymbol' "stra") (BaseStringRepr UnicodeRepr) i <- stringIndexOf sym a x =<< intLit sym 5 zero <- intLit sym 0@@ -769,11 +863,11 @@ checkSatisfiableWithModel solver "test" p $ \case Sat fn ->- do alit <- fromChar8Lit <$> groundEval fn a+ do alit <- fromUnicodeLit <$> groundEval fn a ilit <- groundEval fn i - BS.isPrefixOf bsx (BS.drop (fromIntegral ilit) alit) @? "correct index"- ilit >= 5 @? "index large enough"+ TC.check "correct index" (Text.isPrefixOf bsx) (Text.drop (fromIntegral ilit) alit)+ TC.check "index large enough" (>= 5) ilit _ -> fail "expected satisfable model" @@ -785,11 +879,11 @@ checkSatisfiableWithModel solver "test" q $ \case Sat fn ->- do alit <- fromChar8Lit <$> groundEval fn a+ do alit <- fromUnicodeLit <$> groundEval fn a ilit <- groundEval fn i - not (BS.isInfixOf bsx (BS.drop 5 alit)) @? "substring not found"- ilit == (-1) @? "expected neg one"+ TC.check "substring not found" (not . Text.isInfixOf bsx) (Text.drop 5 alit)+ TC.check "expected neg one index" (== (-1)) ilit _ -> fail "expected satisfable model" @@ -798,8 +892,8 @@ SimpleExprBuilder t fs -> SolverProcess t solver -> IO ()-stringTest5 sym solver =- do a <- freshConstant sym (userSymbol' "a") (BaseStringRepr Char8Repr)+stringTest5 sym solver = withChecklist "string5" $+ do a <- freshConstant sym (userSymbol' "a") (BaseStringRepr UnicodeRepr) off <- freshConstant sym (userSymbol' "off") BaseIntegerRepr len <- freshConstant sym (userSymbol' "len") BaseIntegerRepr @@ -809,7 +903,7 @@ let qlit = "qwerty" sub <- stringSubstring sym a off len- p1 <- stringEq sym sub =<< stringLit sym (Char8Literal qlit)+ p1 <- stringEq sym sub =<< stringLit sym (UnicodeLiteral qlit) p2 <- intLe sym n5 off p3 <- intLe sym n20 =<< stringLength sym a @@ -817,17 +911,97 @@ checkSatisfiableWithModel solver "test" p $ \case Sat fn ->- do alit <- fromChar8Lit <$> groundEval fn a+ do alit <- fromUnicodeLit <$> groundEval fn a offlit <- groundEval fn off lenlit <- groundEval fn len - let q = BS.take (fromIntegral lenlit) (BS.drop (fromIntegral offlit) alit)+ let q = Text.take (fromIntegral lenlit) (Text.drop (fromIntegral offlit) alit) - q == qlit @? "correct substring"+ TC.check "correct substring" (qlit ==) q _ -> fail "expected satisfable model" +-- This test verifies that we can correctly round-trip the+-- '\' character. It is a bit of a corner case, since it+-- is is involved in the codepoint escape sequences '\u{abcd}'.+stringTest6 ::+ OnlineSolver solver =>+ SimpleExprBuilder t fs ->+ SolverProcess t solver ->+ IO ()+stringTest6 sym solver = withChecklist "string6" $+ do let conn = solverConn solver+ x <- freshConstant sym (safeSymbol "x") (BaseStringRepr UnicodeRepr)+ l <- stringLength sym x+ intLit sym 1 >>= isEq sym l >>= assume conn+ stringLit sym (UnicodeLiteral (Text.pack "\\")) >>= isEq sym x >>= assume conn+ checkAndGetModel solver "test" >>= \case+ Sat ge -> do+ v <- groundEval ge x+ TC.check "correct string" (v ==) (UnicodeLiteral (Text.pack "\\"))+ _ -> fail "unsatisfiable"++-- This test asks the solver to produce a sequence of 200 unique characters+-- This helps to ensure that we can correclty recieve and send back to the+-- solver enough characters to exhaust the standard printable ASCII sequence,+-- which ensures that we are testing nontrivial escape sequences.+--+-- We don't verify that any particular string is returned because the solvers+-- make different choices about what characters to return.+stringTest7 ::+ OnlineSolver solver =>+ SimpleExprBuilder t fs ->+ SolverProcess t solver ->+ IO ()+stringTest7 sym solver = withChecklist "string6" $+ do chars <- getChars sym solver 200+ TC.check "correct number of characters" (length chars ==) 200++getChars ::+ OnlineSolver solver =>+ SimpleExprBuilder t fs ->+ SolverProcess t solver ->+ Integer ->+ IO [Char]+getChars sym solver bound = do+ let conn = solverConn solver+ -- Create string var and constrain its length to 1+ x <- freshConstant sym (safeSymbol "x") (BaseStringRepr UnicodeRepr)+ l <- stringLength sym x+ intLit sym 1 >>= isEq sym l >>= assume conn+ -- Recursively generate characters+ let getModelsRecursive n+ | n >= bound = return ""+ | otherwise =+ checkAndGetModel solver "test" >>= \case+ Sat ge -> do+ v <- groundEval ge x+ -- Exclude value+ stringLit sym v >>= isEq sym x >>= notPred sym >>= assume conn+ let c = Text.head $ fromUnicodeLit v+ cs <- getModelsRecursive (n+1)+ return (c:cs)+ _ -> return []++ cs <- getModelsRecursive 0+ return cs+++multidimArrayTest ::+ OnlineSolver solver =>+ SimpleExprBuilder t fs ->+ SolverProcess t solver ->+ IO ()+multidimArrayTest sym solver =+ do f <- freshConstant sym (userSymbol' "a") $+ BaseArrayRepr (Ctx.empty Ctx.:> BaseBoolRepr Ctx.:> BaseBoolRepr) BaseBoolRepr+ f' <- arrayUpdate sym f (Ctx.empty Ctx.:> falsePred sym Ctx.:> falsePred sym) (falsePred sym)+ p <- arrayLookup sym f' (Ctx.empty Ctx.:> truePred sym Ctx.:> truePred sym)+ checkSatisfiable solver "test" p >>= \case+ Sat _ -> return ()+ _ -> fail "expected satisfiable model"+ forallTest :: OnlineSolver solver => SimpleExprBuilder t fs ->@@ -879,6 +1053,32 @@ Unsat _ -> return () _ -> fail "expected UNSAT" +-- | A regression test for #182.+issue182Test ::+ OnlineSolver solver =>+ SimpleExprBuilder t fs ->+ SolverProcess t solver ->+ IO ()+issue182Test sym solver = do+ let w = knownNat @64+ arr <- freshConstant sym (safeSymbol "arr")+ (BaseArrayRepr (Ctx.Empty Ctx.:> BaseIntegerRepr)+ (BaseBVRepr w))+ idxInt <- intLit sym 0+ let idx = Ctx.Empty Ctx.:> idxInt+ let arrLookup = arrayLookup sym arr idx+ elt <- arrLookup+ bvZero <- bvLit sym w (BV.zero w)+ p <- bvEq sym elt bvZero++ checkSatisfiableWithModel solver "test" p $ \case+ Sat fn ->+ do elt' <- arrLookup+ eltEval <- groundEval fn elt'+ (eltEval == BV.zero w) @? "non-zero result"++ _ -> fail "expected satisfible model"+ -- | These tests simply ensure that no exceptions are raised. testSolverInfo :: TestTree testSolverInfo = testGroup "solver info queries" $@@ -924,79 +1124,190 @@ e1 <- bvLit sym knownRepr (BV.mkBV knownNat 128) e0 @?= e1 +-- Test unsafeSetAbstractValue on a simple symbolic expression+testUnsafeSetAbstractValue1 :: TestTree+testUnsafeSetAbstractValue1 = testCase "test unsafeSetAbstractValue1" $+ withSym FloatIEEERepr $ \sym -> do+ let w = knownNat @8++ e1A <- freshConstant sym (userSymbol' "x1") (BaseBVRepr w)+ let e1A' = unsafeSetAbstractValue (WUB.BVDArith (WUBA.range w 2 2)) e1A+ unsignedBVBounds e1A' @?= Just (2, 2)+ e1B <- bvAdd sym e1A' =<< bvLit sym w (BV.one w)+ case asBV e1B of+ Just bv -> bv @?= BV.mkBV w 3+ Nothing -> assertFailure $ unlines+ [ "unsafeSetAbstractValue doesn't work as expected for a"+ , "simple symbolic expression"+ ]++-- Test unsafeSetAbstractValue on a compound symbolic expression+testUnsafeSetAbstractValue2 :: TestTree+testUnsafeSetAbstractValue2 = testCase "test unsafeSetAbstractValue2" $+ withSym FloatIEEERepr $ \sym -> do+ let w = knownNat @8+ e2A <- freshConstant sym (userSymbol' "x2A") (BaseBVRepr w)+ e2B <- freshConstant sym (userSymbol' "x2B") (BaseBVRepr w)+ e2C <- bvAdd sym e2A e2B+ (_, e2C') <- annotateTerm sym $ unsafeSetAbstractValue (WUB.BVDArith (WUBA.range w 2 2)) e2C+ unsignedBVBounds e2C' @?= Just (2, 2)+ e2D <- bvAdd sym e2C' =<< bvLit sym w (BV.one w)+ case asBV e2D of+ Just bv -> bv @?= BV.mkBV w 3+ Nothing -> assertFailure $ unlines+ [ "unsafeSetAbstractValue doesn't work as expected for a"+ , "compound symbolic expression"+ ]++testResolveSymBV :: WURB.SearchStrategy -> TestTree+testResolveSymBV searchStrat =+ testProperty ("test resolveSymBV (" ++ show (PP.pretty searchStrat) ++ ")") $+ H.property $ do+ let w = knownNat @8+ lb <- H.forAll $ HGen.word8 $ HRange.constant 0 maxBound+ ub <- H.forAll $ HGen.word8 $ HRange.constant lb maxBound++ rbv <- liftIO $ withYices $ \sym proc -> do+ bv <- freshConstant sym (safeSymbol "bv") knownRepr+ p1 <- bvUge sym bv =<< bvLit sym w (BV.mkBV w (toInteger lb))+ p2 <- bvUle sym bv =<< bvLit sym w (BV.mkBV w (toInteger ub))+ p3 <- andPred sym p1 p2+ assume (solverConn proc) p3+ WURB.resolveSymBV sym searchStrat w proc bv++ case rbv of+ WURB.BVConcrete bv -> do+ let bv' = fromInteger $ BV.asUnsigned bv+ lb H.=== bv'+ ub H.=== bv'+ WURB.BVSymbolic bounds -> do+ let (lb', ub') = WUBA.ubounds bounds+ lb H.=== fromInteger lb'+ ub H.=== fromInteger ub'++----------------------------------------------------------------------++ main :: IO ()-main = defaultMain $ testGroup "Tests"- [ testInterpretedFloatReal- , testFloatUninterpreted- , testInterpretedFloatIEEE- , testFloatUnsat0- , testFloatUnsat1- , testFloatUnsat2- , testFloatSat0- , testFloatSat1- , testFloatToBinary- , testFloatFromBinary- , testFloatBinarySimplification- , testRealFloatBinarySimplification- , testFloatCastSimplification- , testFloatCastNoSimplification- , testBVSelectShl- , testBVSelectLshr- , testBVOrShlZext- , testUninterpretedFunctionScope- , testBVIteNesting- , testRotate1- , testRotate2- , testRotate3- , testSymbolPrimeCharZ3- , testBoundVarAsFree- , testSolverInfo- , testSolverVersion- , testBVDomainArithScale- , testBVSwap- , testBVBitreverse+main = do+ testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"+ let solverNames = SolverName <$> [ "cvc4", "yices", "z3" ]+ solvers <- reportSolverVersions testLevel id+ =<< (zip solverNames <$> mapM getSolverVersion solverNames)+ let z3Tests =+ let skipPre4_8_11 why =+ let shouldSkip = case lookup (SolverName "z3") solvers of+ Just (SolverVersion v) -> any (`elem` [ "4.8.8", "4.8.9", "4.8.10" ]) $ words v+ Nothing -> True+ in if shouldSkip then expectFailBecause why else id+ incompatZ3Strings = "unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.11"+ in+ [+ testUninterpretedFunctionScope+ , testRotate1+ , testRotate2+ , testRotate3+ , testBoundVarAsFree+ , testSolverInfo+ , testSolverVersion+ , testFloatUnsat0+ , testFloatUnsat1+ , testFloatUnsat2+ , testFloatSat0+ , testFloatSat1+ , testFloatToBinary+ , testFloatFromBinary+ , testBVIteNesting+ , testSymbolPrimeCharZ3+ , testCase "Z3 0-tuple" $ withOnlineZ3 zeroTupleTest+ , testCase "Z3 1-tuple" $ withOnlineZ3 oneTupleTest+ , testCase "Z3 pair" $ withOnlineZ3 pairTest+ , testCase "Z3 forall binder" $ withOnlineZ3 forallTest - , testCase "Yices 0-tuple" $ withYices zeroTupleTest- , testCase "Yices 1-tuple" $ withYices oneTupleTest- , testCase "Yices pair" $ withYices pairTest+ , skipPre4_8_11 incompatZ3Strings $ testCase "Z3 string1" $ withOnlineZ3 stringTest1+ , testCase "Z3 string2" $ withOnlineZ3 stringTest2+ , skipPre4_8_11 incompatZ3Strings $ testCase "Z3 string3" $ withOnlineZ3 stringTest3+ , skipPre4_8_11 incompatZ3Strings $ testCase "Z3 string4" $ withOnlineZ3 stringTest4+ , skipPre4_8_11 incompatZ3Strings $ testCase "Z3 string5" $ withOnlineZ3 stringTest5+ , skipPre4_8_11 incompatZ3Strings $ testCase "Z3 string6" $ withOnlineZ3 stringTest6+ -- this test apparently passes on older Z3 despite the escaping changes...+ , testCase "Z3 string7" $ withOnlineZ3 stringTest7 - , testCase "Z3 0-tuple" $ withOnlineZ3 zeroTupleTest- , testCase "Z3 1-tuple" $ withOnlineZ3 oneTupleTest- , testCase "Z3 pair" $ withOnlineZ3 pairTest+ , testCase "Z3 binder tuple1" $ withOnlineZ3 binderTupleTest1+ , testCase "Z3 binder tuple2" $ withOnlineZ3 binderTupleTest2 - -- TODO, enable this test when we figure out why it- -- doesnt work...- -- , testCase "CVC4 0-tuple" $ withCVC4 zeroTupleTest- , testCase "CVC4 1-tuple" $ withCVC4 oneTupleTest- , testCase "CVC4 pair" $ withCVC4 pairTest+ , testCase "Z3 rounding" $ withOnlineZ3 roundingTest - , testCase "Z3 forall binder" $ withOnlineZ3 forallTest- , testCase "CVC4 forall binder" $ withCVC4 forallTest+ , testCase "Z3 multidim array"$ withOnlineZ3 multidimArrayTest - , testCase "Z3 string1" $ withOnlineZ3 stringTest1- , testCase "Z3 string2" $ withOnlineZ3 stringTest2- -- TODO, reenable this test, or a similar one, once the following is fixed- -- https://github.com/GaloisInc/what4/issues/56- -- , testCase "Z3 string3" $ withOnlineZ3 stringTest3- , testCase "Z3 string4" $ withOnlineZ3 stringTest4- , testCase "Z3 string5" $ withOnlineZ3 stringTest5+ , testCase "Z3 #182 test case" $ withOnlineZ3 issue182Test - , testCase "CVC4 string1" $ withCVC4 stringTest1- , testCase "CVC4 string2" $ withCVC4 stringTest2+ , arrayCopyTest+ , arraySetTest+ , arrayCopySetTest+ ]+ let cvc4Tests =+ let skipPre1_8 why =+ let shouldSkip = case lookup (SolverName "cvc4") solvers of+ Just (SolverVersion v) -> any (`elem` [ "1.7" ]) $ words v+ Nothing -> True+ in if shouldSkip then expectFailBecause why else id+ unsuppStrings = "unicode and string escaping not supported for older CVC4 versions; upgrade to at least 1.8"+ in+ [+ ignoreTestBecause "This test stalls the solver for some reason; line-buffering issue?" $+ testCase "CVC4 0-tuple" $ withCVC4 zeroTupleTest+ , testCase "CVC4 1-tuple" $ withCVC4 oneTupleTest+ , testCase "CVC4 pair" $ withCVC4 pairTest+ , testCase "CVC4 forall binder" $ withCVC4 forallTest - -- TODO, reenable this test, or a similar one, once the following is fixed- -- https://github.com/GaloisInc/what4/issues/56- -- , testCase "CVC4 string3" $ withCVC4 stringTest3- , testCase "CVC4 string4" $ withCVC4 stringTest4- , testCase "CVC4 string5" $ withCVC4 stringTest5+ , testCase "CVC4 string1" $ withCVC4 stringTest1+ , testCase "CVC4 string2" $ withCVC4 stringTest2+ , skipPre1_8 unsuppStrings $ testCase "CVC4 string3" $ withCVC4 stringTest3+ , testCase "CVC4 string4" $ withCVC4 stringTest4+ , testCase "CVC4 string5" $ withCVC4 stringTest5+ , skipPre1_8 unsuppStrings $ testCase "CVC4 string6" $ withCVC4 stringTest6+ , testCase "CVC4 string7" $ withCVC4 stringTest7 - , testCase "Z3 binder tuple1" $ withOnlineZ3 binderTupleTest1- , testCase "Z3 binder tuple2" $ withOnlineZ3 binderTupleTest2+ , testCase "CVC4 binder tuple1" $ withCVC4 binderTupleTest1+ , testCase "CVC4 binder tuple2" $ withCVC4 binderTupleTest2 - , testCase "CVC4 binder tuple1" $ withCVC4 binderTupleTest1- , testCase "CVC4 binder tuple2" $ withCVC4 binderTupleTest2+ , testCase "CVC4 rounding" $ withCVC4 roundingTest - , testCase "Z3 rounding" $ withOnlineZ3 roundingTest- , testCase "Yices rounding" $ withYices roundingTest- , testCase "CVC4 rounding" $ withCVC4 roundingTest- ]+ , testCase "CVC4 multidim array"$ withCVC4 multidimArrayTest++ , testCase "CVC4 #182 test case" $ withCVC4 issue182Test+ ]+ let yicesTests =+ [+ testResolveSymBV WURB.ExponentialSearch+ , testResolveSymBV WURB.BinarySearch++ , testCase "Yices 0-tuple" $ withYices zeroTupleTest+ , testCase "Yices 1-tuple" $ withYices oneTupleTest+ , testCase "Yices pair" $ withYices pairTest+ , testCase "Yices rounding" $ withYices roundingTest+ , testCase "Yices #182 test case" $ withYices issue182Test+ ]+ let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id+ else fmap (ignoreTestBecause (nm <> " not present"))+ defaultMain $ testGroup "Tests" $+ [ testInterpretedFloatReal+ , testFloatUninterpreted+ , testInterpretedFloatIEEE+ , testFloatBinarySimplification+ , testRealFloatBinarySimplification+ , testFloatCastSimplification+ , testFloatCastNoSimplification+ , testBVSelectShl+ , testBVSelectLshr+ , testBVOrShlZext+ , testBVDomainArithScale+ , testBVSwap+ , testBVBitreverse+ , testUnsafeSetAbstractValue1+ , testUnsafeSetAbstractValue2+ ]+ <> (skipIfNotPresent "cvc4" cvc4Tests)+ <> (skipIfNotPresent "yices" yicesTests)+ <> (skipIfNotPresent "z3" z3Tests)
test/ExprsTest.hs view
@@ -28,18 +28,16 @@ import qualified Hedgehog.Range as Range import Test.Tasty import Test.Tasty.HUnit-import Test.Tasty.Hedgehog+import Test.Tasty.Hedgehog.Alt import What4.Concrete import What4.Expr import What4.Interface --data State t = State-type IteExprBuilder t fs = ExprBuilder t State fs+type IteExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs withTestSolver :: (forall t. IteExprBuilder t (Flags FloatIEEE) -> IO a) -> IO a withTestSolver f = withIONonceGenerator $ \nonce_gen ->- f =<< newExprBuilder FloatIEEERepr State nonce_gen+ f =<< newExprBuilder FloatIEEERepr EmptyExprBuilderState nonce_gen -- | Test natDiv and natMod properties described at their declaration
test/GenWhat4Expr.hs view
@@ -38,6 +38,7 @@ import Data.Bits import qualified Data.BitVector.Sized as BV+import Data.Maybe ( fromMaybe, isJust ) import Data.Word import GHC.Natural import GHC.TypeNats ( KnownNat )@@ -92,34 +93,73 @@ | TE_BV32 BV32TestExpr | TE_BV64 BV64TestExpr -isBoolTestExpr, isIntTestExpr,- isBV8TestExpr, isBV16TestExpr, isBV32TestExpr, isBV64TestExpr- :: TestExpr -> Bool+-- Projection functions that return Nothing if there is a constructor mismatch. -isBoolTestExpr = \case- TE_Bool _ -> True- _ -> False+boolTestExprMaybe :: TestExpr -> Maybe PredTestExpr+boolTestExprMaybe = \case+ TE_Bool p -> Just p+ _ -> Nothing -isIntTestExpr = \case- TE_Int _ -> True- _ -> False+intTestExprMaybe :: TestExpr -> Maybe IntTestExpr+intTestExprMaybe = \case+ TE_Int i -> Just i+ _ -> Nothing -isBV8TestExpr = \case- TE_BV8 _ -> True- _ -> False+bv8TestExprMaybe :: TestExpr -> Maybe BV8TestExpr+bv8TestExprMaybe = \case+ TE_BV8 bv8 -> Just bv8+ _ -> Nothing -isBV16TestExpr = \case- TE_BV16 _ -> True- _ -> False+bv16TestExprMaybe :: TestExpr -> Maybe BV16TestExpr+bv16TestExprMaybe = \case+ TE_BV16 bv16 -> Just bv16+ _ -> Nothing -isBV32TestExpr = \case- TE_BV32 _ -> True- _ -> False+bv32TestExprMaybe :: TestExpr -> Maybe BV32TestExpr+bv32TestExprMaybe = \case+ TE_BV32 bv32 -> Just bv32+ _ -> Nothing -isBV64TestExpr = \case- TE_BV64 _ -> True- _ -> False+bv64TestExprMaybe :: TestExpr -> Maybe BV64TestExpr+bv64TestExprMaybe = \case+ TE_BV64 bv64 -> Just bv64+ _ -> Nothing +-- Projection functions that `error` if there is a constructor mismatch.+-- Use these with caution.++fromBoolTestExpr :: HasCallStack => TestExpr -> PredTestExpr+fromBoolTestExpr = fromMaybe (error "Expected TE_Bool") . boolTestExprMaybe++fromIntTestExpr :: HasCallStack => TestExpr -> IntTestExpr+fromIntTestExpr = fromMaybe (error "Expected TE_Int") . intTestExprMaybe++fromBV8TestExpr :: HasCallStack => TestExpr -> BV8TestExpr+fromBV8TestExpr = fromMaybe (error "Expected TE_BV8") . bv8TestExprMaybe++fromBV16TestExpr :: HasCallStack => TestExpr -> BV16TestExpr+fromBV16TestExpr = fromMaybe (error "Expected TE_BV16") . bv16TestExprMaybe++fromBV32TestExpr :: HasCallStack => TestExpr -> BV32TestExpr+fromBV32TestExpr = fromMaybe (error "Expected TE_BV32") . bv32TestExprMaybe++fromBV64TestExpr :: HasCallStack => TestExpr -> BV64TestExpr+fromBV64TestExpr = fromMaybe (error "Expected TE_BV64") . bv64TestExprMaybe++-- Constructor predicates++isBoolTestExpr, isIntTestExpr,+ isBV8TestExpr, isBV16TestExpr, isBV32TestExpr, isBV64TestExpr+ :: TestExpr -> Bool++isBoolTestExpr = isJust . boolTestExprMaybe+isIntTestExpr = isJust . intTestExprMaybe+isBV8TestExpr = isJust . bv8TestExprMaybe+isBV16TestExpr = isJust . bv16TestExprMaybe+isBV32TestExpr = isJust . bv32TestExprMaybe+isBV64TestExpr = isJust . bv64TestExprMaybe++ ---------------------------------------------------------------------- data PredTestExpr =@@ -148,18 +188,30 @@ bv32Term = IGen.filterT isBV32TestExpr genBV32TestExpr bv64Term = IGen.filterT isBV64TestExpr genBV64TestExpr subBoolTerm2 gen = Gen.subterm2 boolTerm boolTerm- (\(TE_Bool x) (TE_Bool y) -> TE_Bool $ gen x y)+ (\xt yt -> let x = fromBoolTestExpr xt+ y = fromBoolTestExpr yt in+ TE_Bool $ gen x y) subBoolTerm3 gen = Gen.subterm3 boolTerm boolTerm boolTerm- (\(TE_Bool x) (TE_Bool y) (TE_Bool z) -> TE_Bool $ gen x y z)- subIntTerms2 gen = Gen.subterm2 intTerm intTerm (\(TE_Int x) (TE_Int y) -> TE_Bool $ gen x y)- -- subBV16Terms2 gen = Gen.subterm2 bv16Term bv16Term (\(TE_BV16 x) (TE_BV16 y) -> TE_Bool $ gen x y)- -- subBV8Terms2 gen = Gen.subterm2 bv8Term bv8Term (\(TE_BV8 x) (TE_BV8 y) -> TE_Bool $ gen x y)+ (\xt yt zt -> let x = fromBoolTestExpr xt+ y = fromBoolTestExpr yt+ z = fromBoolTestExpr zt in+ TE_Bool $ gen x y z)+ subIntTerms2 gen = Gen.subterm2 intTerm intTerm (\xt yt -> let x = fromIntTestExpr xt+ y = fromIntTestExpr yt in+ TE_Bool $ gen x y)+ -- subBV16Terms2 gen = Gen.subterm2 bv16Term bv16Term (\xt yt -> let x = fromBV16TestExpr xt+ -- y = fromBV16TestExpr yt in+ -- TE_Bool $ gen x y)+ -- subBV8Terms2 gen = Gen.subterm2 bv8Term bv8Term (\xt yt -> let x = fromBV8TestExpr xt+ -- y = fromBV8TestExpr yt in+ -- TE_Bool $ gen x y) in [ Gen.subterm genBoolCond- (\(TE_Bool itc) -> TE_Bool $ PredTest ("not " <> pdesc itc)- (not $ testval itc)- (\sym -> notPred sym =<< predexp itc sym))+ (\itct -> let itc = fromBoolTestExpr itct in+ TE_Bool $ PredTest ("not " <> pdesc itc)+ (not $ testval itc)+ (\sym -> notPred sym =<< predexp itc sym)) , subBoolTerm2 (\x y ->@@ -242,18 +294,20 @@ -- result if necessary. Also note that the testBitBV uses an -- actual Natural, not a What4 Nat, so the natval is used and the -- natexpr is ignored.- (\(TE_Int i) (TE_BV16 v) -> TE_Bool $ -- KWQ: bvsized- let ival = fromInteger (testval i `mod` 16) in+ (\it vt -> TE_Bool $ -- KWQ: bvsized+ let i = fromIntTestExpr it+ v = fromBV16TestExpr vt+ ival = fromInteger (testval i `mod` 16) in PredTest (pdesc v <> "[" <> show ival <> "]") (testBit (testval v) (fromEnum ival)) (\sym -> testBitBV sym ival =<< bvexpr v sym)) ]- ++ bvPredExprs bv8Term (\(TE_BV8 x) -> x) bv8expr 8- ++ bvPredExprs bv16Term (\(TE_BV16 x) -> x) bvexpr 16- ++ bvPredExprs bv32Term (\(TE_BV32 x) -> x) bv32expr 32- ++ bvPredExprs bv64Term (\(TE_BV64 x) -> x) bv64expr 64+ ++ bvPredExprs bv8Term fromBV8TestExpr bv8expr 8+ ++ bvPredExprs bv16Term fromBV16TestExpr bvexpr 16+ ++ bvPredExprs bv32Term fromBV32TestExpr bv32expr 32+ ++ bvPredExprs bv64Term fromBV64TestExpr bv64expr 64 bvPredExprs :: ( Monad m@@ -408,9 +462,14 @@ isIntNZTestExpr = \case TE_Int n -> testval n /= 0 _ -> False- subIntTerms2 gen = Gen.subterm2 intTerm intTerm (\(TE_Int x) (TE_Int y) -> TE_Int $ gen x y)+ subIntTerms2 gen = Gen.subterm2 intTerm intTerm+ (\xt yt -> let x = fromIntTestExpr xt+ y = fromIntTestExpr yt in+ TE_Int $ gen x y) subIntTerms2nz gen = Gen.subterm2 intTerm intTermNZ- (\(TE_Int x) (TE_Int y) -> TE_Int $ gen x y)+ (\xt yt -> let x = fromIntTestExpr xt+ y = fromIntTestExpr yt in+ TE_Int $ gen x y) in [ subIntTerms2 (\x y -> IntTestExpr (pdesc x <> " int.+ " <> pdesc y)@@ -453,7 +512,11 @@ , Gen.subterm3 (IGen.filterT isBoolTestExpr genBoolCond) intTerm intTerm- (\(TE_Bool c) (TE_Int x) (TE_Int y) -> TE_Int $ IntTestExpr+ (\ct xt yt ->+ let c = fromBoolTestExpr ct+ x = fromIntTestExpr xt+ y = fromIntTestExpr yt in+ TE_Int $ IntTestExpr (pdesc c <> " int.? " <> pdesc x <> " : " <> pdesc y) (if testval c then testval x else testval y) (\sym -> do c' <- predexp c sym@@ -677,7 +740,7 @@ let g8 = BVTermGen (IGen.filterT isBV8TestExpr genBV8TestExpr) TE_BV8- (\(TE_BV8 x) -> x)+ fromBV8TestExpr BV8TestExpr bv8expr 8@@ -685,7 +748,7 @@ g16 = BVTermGen (IGen.filterT isBV16TestExpr genBV16TestExpr) TE_BV16- (\(TE_BV16 x) -> x)+ fromBV16TestExpr BV16TestExpr bvexpr 16@@ -693,7 +756,7 @@ g32 = BVTermGen (IGen.filterT isBV32TestExpr genBV32TestExpr) TE_BV32- (\(TE_BV32 x) -> x)+ fromBV32TestExpr BV32TestExpr bv32expr 32@@ -701,7 +764,7 @@ g64 = BVTermGen (IGen.filterT isBV64TestExpr genBV64TestExpr) TE_BV64- (\(TE_BV64 x) -> x)+ fromBV64TestExpr BV64TestExpr bv64expr 64@@ -837,8 +900,9 @@ , Gen.subterm3 (IGen.filterT isBoolTestExpr genBoolCond) bvTerm bvTerm- (\(TE_Bool c) lt rt -> conTE $- let l = projTE lt+ (\ct lt rt -> conTE $+ let c = fromBoolTestExpr ct+ l = projTE lt r = projTE rt in teSubCon (unwords [pdesc c, pfx "?", pdesc l, ":", pdesc r])@@ -892,8 +956,10 @@ in Gen.subterm3 bvTerm intTerm boolTerm $ -- see Note [natTerm]- \bvt (TE_Int n) (TE_Bool b) ->+ \bvt nt bt -> let bv = projTE bvt+ n = fromIntTestExpr nt+ b = fromBoolTestExpr bt nval = fromInteger (testval n `mod` toInteger width) ival = fromIntegral nval :: Int in conTE $ teSubCon@@ -908,7 +974,8 @@ , let boolTerm = IGen.filterT isBoolTestExpr genBoolCond in Gen.subterm boolTerm $- \(TE_Bool b) ->+ \bt ->+ let b = fromBoolTestExpr bt in -- technically bvFill also takes a NatRepr for the output -- width, but due to the arrangement of these expression -- generators, it will just generate the size specified for
test/HH/VerifyBindings.hs view
@@ -8,7 +8,7 @@ import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range import Test.Tasty-import Test.Tasty.Hedgehog+import Test.Tasty.Hedgehog.Alt import qualified Test.Verification as V
test/IteExprs.hs view
@@ -30,18 +30,17 @@ import qualified Hedgehog.Internal.Gen as IGen import Test.Tasty import Test.Tasty.HUnit-import Test.Tasty.Hedgehog+import Test.Tasty.Hedgehog.Alt import What4.Concrete import What4.Expr import What4.Interface -data State t = State-type IteExprBuilder t fs = ExprBuilder t State fs+type IteExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs withTestSolver :: (forall t. IteExprBuilder t (Flags FloatIEEE) -> IO a) -> IO a withTestSolver f = withIONonceGenerator $ \nonce_gen ->- f =<< newExprBuilder FloatIEEERepr State nonce_gen+ f =<< newExprBuilder FloatIEEERepr EmptyExprBuilderState nonce_gen -- | What branch (arm) is expected from the ITE evaluation? data ExpITEArm = Then | Else
test/OnlineSolverTest.hs view
@@ -3,6 +3,7 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-}@@ -11,16 +12,29 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -fno-warn-orphans #-} -- for TestShow instance -import Control.Exception ( try, SomeException )+import Control.Concurrent ( threadDelay )+import Control.Concurrent.Async ( race ) import Control.Lens (folded)-import Control.Monad ( forM, void )-import Data.Char ( toLower )+import Control.Monad ( forM )+import Control.Monad.Catch ( MonadMask )+import Control.Monad.IO.Class ( MonadIO )+import Data.Either ( isLeft, isRight )+import qualified Data.List as L+import Data.Maybe ( fromMaybe )+import Data.Metrology ( (%), (#), (|<=|), (|*), (|<|), (|+|), qApprox )+import Data.Metrology.SI ( Time, milli, micro, nano, Second(..) )+import Data.Metrology.Show () import Data.Proxy-import System.Exit ( ExitCode(..) )-import System.Process ( readProcessWithExitCode )+import qualified Prettyprinter as PP+import System.Clock+import System.Environment ( lookupEnv ) +import ProbeSolvers import Test.Tasty+import qualified Test.Tasty.Checklist as TCL+import Test.Tasty.ExpectedFailure import Test.Tasty.HUnit import qualified Data.BitVector.Sized as BV@@ -36,23 +50,38 @@ import qualified What4.Protocol.SMTLib2 as SMT2 import qualified What4.Solver.Yices as Yices -data State t = State+type SolverTestData = (SolverName, AnOnlineSolver, ProblemFeatures, [ConfigDesc], Maybe (ConfigOption BaseIntegerType)) -allOnlineSolvers :: [(String, AnOnlineSolver, ProblemFeatures, [ConfigDesc])]+allOnlineSolvers :: [SolverTestData] allOnlineSolvers =- [ ("Z3", AnOnlineSolver @(SMT2.Writer Z3) Proxy, z3Features, z3Options)- , ("CVC4", AnOnlineSolver @(SMT2.Writer CVC4) Proxy, cvc4Features, cvc4Options)- , ("Yices", AnOnlineSolver @Yices.Connection Proxy, yicesDefaultFeatures, yicesOptions)- , ("Boolector", AnOnlineSolver @(SMT2.Writer Boolector) Proxy, boolectorFeatures, boolectorOptions)+ [ (SolverName "Z3"+ , AnOnlineSolver @(SMT2.Writer Z3) Proxy, z3Features, z3Options, Just z3Timeout)+ , (SolverName "CVC4"+ , AnOnlineSolver @(SMT2.Writer CVC4) Proxy, cvc4Features, cvc4Options, Just cvc4Timeout)+ , (SolverName "Yices"+ , AnOnlineSolver @Yices.Connection Proxy, yicesDefaultFeatures, yicesOptions, Just yicesGoalTimeout)+ , (SolverName "Boolector"+ , AnOnlineSolver @(SMT2.Writer Boolector) Proxy, boolectorFeatures, boolectorOptions, Just boolectorTimeout) #ifdef TEST_STP- , ("STP", AnOnlineSolver @(SMT2.Writer STP) Proxy, stpFeatures, stpOptions)+ , (SolverName "STP"+ , AnOnlineSolver @(SMT2.Writer STP) Proxy, stpFeatures, stpOptions, Just stpTimeout) #endif ] -mkSmokeTest :: (String, AnOnlineSolver, ProblemFeatures, [ConfigDesc]) -> TestTree-mkSmokeTest (nm, AnOnlineSolver (Proxy :: Proxy s), features, opts) = testCase nm $- withIONonceGenerator $ \gen ->- do sym <- newExprBuilder FloatUninterpretedRepr State gen+testSolverName :: SolverTestData -> SolverName+testSolverName (nm,_,_,_,_) = nm++instance TCL.TestShow [PP.Doc ann] where+ testShow = L.intercalate ", " . fmap show++-- The smoke test is a simple test to ensure that the solver can be+-- queried for a computable result and that the result can be obtained+-- in a reasonably quick amount of time with no cancel or timeouts+-- considerations.+mkSmokeTest :: (SolverTestData, SolverVersion) -> TestTree+mkSmokeTest ((SolverName nm, AnOnlineSolver (_ :: Proxy s), features, opts, _), _) =+ testCase nm $ withIONonceGenerator $ \gen ->+ do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen extendConfig opts (getConfiguration sym) proc <- startSolverProcess @s features Nothing sym let conn = solverConn proc@@ -126,12 +155,20 @@ return block --- Solve Formula1 using a frame (push/pop) for each of the good and--- bad cases-quickstartTest :: (String, AnOnlineSolver, ProblemFeatures, [ConfigDesc]) -> TestTree-quickstartTest (nm, AnOnlineSolver (Proxy :: Proxy s), features, opts) = testCaseSteps nm $ \step ->+-- Solve (the relatively simple) Formula1 using either frames+-- (push/pop) for each of the good and bad cases or else no frames and+-- resetting the solver between cases+quickstartTest :: Bool -> (SolverTestData,SolverVersion) -> TestTree+quickstartTest useFrames ((SolverName nm, AnOnlineSolver (Proxy :: Proxy s), features, opts, _timeoutOpt), SolverVersion sver) =+ let wrap = if nm == "STP"+ then ignoreTestBecause "STP cannot generate the model"+ else if nm == "CVC4" && any ("1.7" ==) (words sver)+ then ignoreTestBecause "CVC4 1.7 non-framed mode fails"+ else id+ in wrap $+ testCaseSteps nm $ \step -> withIONonceGenerator $ \gen ->- do sym <- newExprBuilder FloatUninterpretedRepr State gen+ do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen extendConfig opts (getConfiguration sym) (p,q,r,f) <- mkFormula1 sym@@ -140,109 +177,316 @@ proc <- startSolverProcess @s features Nothing sym let conn = solverConn proc + -- helpers for operating framed v.s. non-framed testing++ let startOnlineCheck :: (MonadMask m, MonadIO m, SMTReadWriter solver) => SolverProcess scope solver -> m b -> m b+ startOnlineCheck = if useFrames then inNewFrame else passThru+ resetOnlineCheck = if useFrames then doNothing else reset+ doNothing = const $ return ()+ passThru _ op = op+ checkType = if useFrames then "framed" else "direct"+ -- Check that formula f is satisfiable, and get the values from -- the model that satisifies it step "Check Satisfiability"- block <- inNewFrame proc $+ block <- startOnlineCheck proc $ do assume conn f- res <- check proc "framed formula1 satisfiable"+ res <- check proc $ checkType <> " formula1 satisfiable" case res of Unsat _ -> fail "Unsatisfiable" Unknown -> fail "Solver returned UNKNOWN"- Sat _ ->- checkFormula1Model sym p q r =<< getModel proc+ Sat _ -> checkFormula1Model sym p q r =<< getModel proc -- Now check that the formula is unsatisfiable when the blocking -- predicate is added. Re-use the existing solver connection + resetOnlineCheck proc+ step "Check Unsatisfiable"- inNewFrame proc $+ startOnlineCheck proc $ do assume conn f assume conn block- res <- check proc "framed formula1 unsatisfiable"+ res <- check proc $ checkType <> " formula1 unsatisfiable" case res of Unsat _ -> return () Unknown -> fail "Solver returned UNKNOWN" Sat _ -> fail "Should be a unique model!" +---------------------------------------------------------------------- --- Solve Formula1 directly, with a solver reset between good and bad cases-quickstartTestAlt :: (String, AnOnlineSolver, ProblemFeatures, [ConfigDesc]) -> TestTree-quickstartTestAlt (nm, AnOnlineSolver (Proxy :: Proxy s), features, opts) = testCaseSteps nm $ \step ->+-- This constructs a What4 formula that takes the solvers a+-- non-trivial amount of time to find a solution for. This is used+-- for running tests that are expected to be interrupted by a timeout,+-- although this formula should run to completion if unrestricted.+mkFormula2 :: IsSymExprBuilder sym => sym -> IO (Pred sym)+mkFormula2 sym = do+ p <- freshConstant sym (safeSymbol "p8") (BaseBVRepr (knownNat @8))+ q <- freshConstant sym (safeSymbol "q8") (BaseBVRepr (knownNat @8))+ r <- freshConstant sym (safeSymbol "r8") (BaseBVRepr (knownNat @8))+ zeroBV <- bvLit sym (knownNat @8) (BV.zero (knownNat))++ let bvGCD n a b = do+ isZero <- bvEq sym zeroBV b+ recurs <- if n == 0 then return a+ else bvGCD (n-1) b =<< (bvUrem sym a b)+ bvIte sym isZero a recurs++ -- String together some symbolic GCD calculations to make+ -- something that the solver takes a while to check. The goal+ -- here is something long enough that we can test various+ -- timeouts.+ gcd1 <- bvGCD (256 :: Int) p r+ gcd2 <- bvGCD (256 :: Int) q r+ gcdRes <- bvGCD (256 :: Int) gcd1 gcd2++ chk1 <- bvUle sym gcdRes p+ chk2 <- bvUle sym gcdRes q+ -- chk3 <- bvNe sym gcdRes zero+ -- chk4 <- bvEq sym gcdRes zero+ -- andPred sym chk1 =<< andPred sym chk2 chk3+ andAllOf sym folded [chk1, chk2] -- , chk3, chk4]++-- Attempt to solve an extensive formula (using frames: push/pop) that+-- should exceed the solver goal-timeout. This can be used to verify+-- that the goal-timeout is realized and that the solver is useable+-- for a goal _after_ the goal-timeout was reached.+longTimeTest :: SolverTestData -> Maybe Time -> IO Bool+longTimeTest (SolverName nm, AnOnlineSolver (Proxy :: Proxy s), features, opts, mb'timeoutOpt) goal_tmo =+ TCL.withChecklist "timer tests" $ withIONonceGenerator $ \gen ->- do sym <- newExprBuilder FloatUninterpretedRepr State gen+ do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen extendConfig opts (getConfiguration sym) - (p,q,r,f) <- mkFormula1 sym+ -- Configure a solver timeout in What4 if specified for this test.+ case goal_tmo of+ Nothing -> return ()+ Just t -> case mb'timeoutOpt of+ Nothing -> error $ "No goal timeout option for backend solver " <> nm+ Just timeoutOpt -> do+ tmOpt <- getOptionSetting timeoutOpt $ getConfiguration sym+ warnings <- setOpt tmOpt $ floor (t # milli Second)+ TCL.check "timer option set" null warnings - step "Start Solver"+ f <- mkFormula2 sym+ proc <- startSolverProcess @s features Nothing sym let conn = solverConn proc -- Check that formula f is satisfiable, and get the values from -- the model that satisifies it - step "Check Satisfiability"- block <-- do assume conn f- res <- check proc "direct formula1 satisfiable"- case res of- Unsat _ -> fail "Unsatisfiable"- Unknown -> fail "Solver returned UNKNOWN"- Sat _ ->- checkFormula1Model sym p q r =<< getModel proc+ do assume conn f+ check proc "direct formula2 satisfiable" >>= \case+ Unsat _ -> fail "Unsatisfiable"+ Unknown -> return False -- how a solver indicates a timeout+ Sat _ -> return True+-- checkFormula1Model sym p q r =<< getModel proc - -- Now check that the formula is unsatisfiable when the blocking- -- predicate is added. Re-use the existing solver connection - reset proc-- step "Check Unsatisfiable"- assume conn f- assume conn block- res <- check proc "direct formula1 unsatisfiable"- case res of- Unsat _ -> return ()- Unknown -> fail "Solver returned UNKNOWN"- Sat _ -> fail "Should be a unique model!"- ---------------------------------------------------------------------- --getSolverVersion :: String -> IO String-getSolverVersion solver =- 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- return $ if null ol then (solver <> " v??") else head ol- else return $ solver <> " version error: " <> show r <> " /;/ " <> e- Left (err :: SomeException) -> return $ solver <> " invocation error: " <> show err---reportSolverVersions :: IO ()-reportSolverVersions = do putStrLn "SOLVER VERSIONS::"- void $ mapM rep allOnlineSolvers- where rep (s,_,_,_) = disp s =<< getSolverVersion s- disp s v = putStrLn $ " Solver " <> s <> " == " <> v-- main :: IO () main = do- reportSolverVersions+ testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"+ versionedSolvers <- zip allOnlineSolvers+ <$> mapM (getSolverVersion . testSolverName) allOnlineSolvers+ solvers <- reportSolverVersions testLevel testSolverName versionedSolvers defaultMain $- localOption (mkTimeout (10 * 1000 * 1000)) $ testGroup "OnlineSolverTests" [- testGroup "SmokeTest" $ map mkSmokeTest allOnlineSolvers- , testGroup "QuickStart Framed" $ map quickstartTest allOnlineSolvers- , testGroup "QuickStart Direct" $ map quickstartTestAlt allOnlineSolvers+ testGroup "SmokeTest" $ map mkSmokeTest solvers+ , testGroup "QuickStart Framed" $ map (quickstartTest True) solvers+ , testGroup "QuickStart Direct" $ map (quickstartTest False) solvers+ , timeoutTests testLevel solvers ]++-- Test the effects of general timeouts on solver proofs+--+-- n.b. Approximate times obviously highly variant based on test+-- machine, etc. As long as they run consistently longer than the+-- useable threshold the tests should perform as expected.++timeoutTests :: TestLevel -> [(SolverTestData, SolverVersion)] -> TestTree+timeoutTests testLevel solvers =+ let+ -- Amount of time to use for timeouts in testing: can be edited+ -- to adjust the timeout threshold needed. This should be large+ -- enough to allow the solver to engage on the task, but smaller+ -- than the expected completion time by enough that the timeout+ -- will halt the test before it completes.+ --+ -- If the timeout is too short there is the risk that it's not a+ -- valid timeout test because of:+ --+ -- 1. machine speed variance+ -- 2. scheduling and solver startup variance+ -- 3. timer resolution and timeout-driven scheduling+ --+ -- If the timeout value is too large, then the solver may+ -- complete the proof more quickly than the timeout will fire.+ -- Also, people get bored. But in practice, this will likely be+ -- set to a number of seconds to allow complex solver solutions+ -- to be obtained.+ --+ -- What4 also includes a deadman timeout on solver activity: the+ -- testTimeout is passed to the solver for voluntary timeouts,+ -- but if the solver does not honor this time specification,+ -- what4 will terminated it via a longer deadman timeout (longer+ -- to avoid triggering it unless needed because it's more+ -- impactful due to killing the solver process itself).+ --+ -- This value should also be <= 60% of useableTimeThreshold to+ -- ensure that the solver runs for a siginificantly longer+ -- period than the test timeout will be set to.+ --+ -- This value can be adjusted by the developer as needed to+ -- reasonably validate timeout testing subject to the above+ -- considerations.+ testTimeout = 250 % milli Second++ -- Solvers must run for at least this amount of time to be+ -- useable for timeout tests. The test timeout value is+ -- determined by 'testTimeout', but if the solver does not run+ -- for at least the 'useableTimeThreshold' then the test result+ -- is likely to be indeterminate due to scheduling and timeout+ -- handling variance.+ --+ -- This value is only used for validating individual tests and+ -- does not control how long the actual tests run.+ --+ -- This value can be adjusted by the developer for cause.+ useableTimeThreshold = testTimeout+ |+| (500 % milli Second) -- What4 deadman timeout+ |+| (650 % milli Second) -- plus some extra time+ -- useableTimeThreshold = 4 % Second :: Time++ -- This is empirical data from previous runs of the "Test itself+ -- is valid and completes" test case; this data is used to guide+ -- the current evaluation; times here will be compared to the+ -- 'useableTimeThreshold' to verify that tests can be accurately+ -- run. This table may need to be updated periodically by the+ -- developer as solvers, What4 formulation, and machine speeds+ -- evolve.+ approxTestTimes :: [ (SolverName, Time) ]+ approxTestTimes = [ (SolverName "Z3", 2.27 % Second) -- Z3 4.8.10. Z3 is good at self timeout.+ , (SolverName "CVC4", 7.5 % Second) -- CVC4 1.8+ , (SolverName "Yices", 2.9 % Second) -- Yices 2.6.1+ , (SolverName "Boolector", 7.2 % Second) -- Boolector 3.2.1+ , (SolverName "STP", 1.35 % Second) -- STP 2.3.3+ ]++ -- This is the acceptable delta variation in time between the+ -- times in the approxTestTimes above and the actual test times.+ -- If difference between the two exceeds this amount then it+ -- represents a significant variation that should be attended+ -- to; either the values in the approxTestTimes needs to be+ -- updated to account for evolved functionality or the test+ -- formulas should be updated to ensure that reasonable timeout+ -- testing can be performed (or there is a significant+ -- performance regression or unexpected improvement in What4).+ --+ -- Note that when this test executable is run locally solo, a+ -- delta value of ~ 0.5 Second is sufficient. This test is+ -- disabled when run via CI (i.e. CI_TEST_LEVEL is not 0),+ -- because *all* test executables are run in parallel via `cabal+ -- test` on unpredictable VMs, so it's not possible to exert any+ -- timing constraints in that situation.+ --+ -- Increase this as needed: it doesn't really have a negative+ -- affect on the actual timing tests, but it does decrease+ -- sensitivity in test timing changes.++ acceptableTimeDelta = 55.0 -- percent variance allowed from expected++ --------------------------------------------------+ -- end of expected developer-adjustments above --+ --------------------------------------------------++ mkTimeoutTests (sti,sv) =+ let historical = fromMaybe (0.0 % Second)+ $ lookup (testSolverName sti) approxTestTimes+ snamestr (SolverName sname) = sname+ maybeSkipTest =+ case (testSolverName sti, sv) of+ -- CVC4 v1.7 generates a response _much_ too+ -- quickly (~0.25s). This doesn't allow timeout+ -- testing, and the speed suggests an improper+ -- result as well.+ (SolverName "CVC4", SolverVersion v) | "1.7" `elem` words v->+ ignoreTestBecause "solver completes too quickly"+ _ -> id+ in maybeSkipTest $ testGroup (snamestr $ testSolverName sti)+ [+ testCase ("Test itself is valid and completes (" <> show historical <> ")") $ do+ -- Verify that the solver will run to completion for+ -- this test if there is no time limit, and also that+ -- the approxTestTimes historical time is reasonably+ -- close to the actual time taken for this test.+ start <- getTime Monotonic+ longTimeTest sti Nothing @? "valid test"+ finish <- getTime Monotonic+ let deltaT = (fromInteger $ toNanoSecs $ diffTimeSpec start finish) % nano Second :: Time+ if testLevel == TestLevel "0"+ then assertBool+ ("actual duration of " <> show deltaT+ <> " is significantly different than expected"+ <> " (will not cause CI failure)")+ $ qApprox (historical |* (acceptableTimeDelta / 100.0)) deltaT historical+ else return ()++ , let maybeRunTest =+ let tooFast = unwords+ [ "solver runs test faster than reasonable"+ , "timing threshold; skipping"+ ]+ in if useableTimeThreshold |<| historical+ then id+ else ignoreTestBecause tooFast+ in maybeRunTest $ testCase "Test runs past timeout" $ do+ start <- getTime Monotonic+ rslt <- race+ (threadDelay (floor $ useableTimeThreshold # micro Second))+ (longTimeTest sti Nothing)+ finish <- getTime Monotonic+ let deltaT = (fromInteger $ toNanoSecs $ diffTimeSpec start finish) % nano Second :: Time+ isLeft rslt @? "solver is to fast for valid timeout testing"+ assertBool+ ("Solver check query not interruptible (" <>+ show deltaT <> " > expected " <> show useableTimeThreshold <> ")")+ $ qApprox (useableTimeThreshold |* (acceptableTimeDelta / 100.0)) deltaT useableTimeThreshold++ -- Verify that specifying a goal-timeout will stop once+ -- that timeout is reached (i.e. before the race timeout here).+ , let maybeRunTest =+ case (testSolverName sti, sv) of+ -- Z3 4.8.11 and 4.8.12 goal-timeouts don't+ -- consistently work properly. Occasionally it+ -- will abort but it generally seems to continue+ -- running and cannot be aborted by signals from+ -- the what4 parent process.+ (SolverName "Z3", SolverVersion v)+ | any (`elem` ["4.8.11", "4.8.12"]) (words v) ->+ expectFailBecause "goal timeouts feature not effective"+ _ -> id+ in maybeRunTest $ testCase ("Test with goal timeout (" <> show testTimeout <> ")") $ do+ rslt <- race+ (threadDelay (floor $ useableTimeThreshold # micro Second))+ (longTimeTest sti (Just testTimeout))+ isRight rslt @? "solver goal timeout didn't occur"+ assertEqual "solver didn't timeout on goal" (Right False) rslt+ -- TODO: ensure that the solver process is no longer using CPU time.+ ]++ in testGroup "Timeout Tests" $+ [+ testCase "valid test timeout" $+ -- Verify that the user-defineable 'testTimeout' is a+ -- reasonable value. If this fails, ignore all other test+ -- results and modify the 'testTimeout'.+ testTimeout |<=| useableTimeThreshold |* 0.60 @?+ "test timeout too large"++ ] <> map mkTimeoutTests solvers
+ test/ProbeSolvers.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}++module ProbeSolvers where++import Control.Exception ( try, SomeException )+import Data.Char ( toLower )+import qualified Data.List as L+import Data.Maybe ( catMaybes )+import System.Exit ( ExitCode(..) )+import System.Process ( readProcessWithExitCode )+++newtype TestLevel = TestLevel String deriving Eq+newtype SolverName = SolverName String deriving (Eq, Show)+newtype SolverVersion = SolverVersion String deriving (Eq, Show)++getSolverVersion :: SolverName -> IO (Either String SolverVersion)+getSolverVersion (SolverName solver) =+ 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+ return $ Right $ SolverVersion+ $ if null ol then (solver <> " v??") else head ol+ else return $ Left $ solver <> " version error: " <> show r <> " /;/ " <> e+ Left (err :: SomeException) -> return $ Left $ solver <> " invocation error: " <> show err+++reportSolverVersions :: TestLevel+ -> (solverinfo -> SolverName)+ -> [(solverinfo, Either String SolverVersion)]+ -> IO [(solverinfo, SolverVersion)]+reportSolverVersions testLevel getSolverName versionedSolvers =+ do putStrLn "SOLVER SELF-REPORTED VERSIONS::"+ catMaybes <$> mapM (rep testLevel) versionedSolvers+ where rep lvl (testsolver, versionInfo) = let s = getSolverName testsolver+ in disp lvl testsolver s versionInfo+ disp lvl solver (SolverName sname) = \case+ Right v@(SolverVersion ver) ->+ do putStrLn $ " Solver " <> sname <> " -> " <> ver+ return $ Just (solver, v)+ Left e -> if and [ "does not exist" `L.isInfixOf` e+ , lvl == TestLevel "0"++ ]+ then do putStrLn $ " Solver " <> sname <> " not found; skipping (would fail with CI_TEST_LEVEL=1)"+ return Nothing+ else do putStrLn $ " Solver " <> sname <> " error: " <> e+ return $ Just (solver, SolverVersion "v?")
test/TestTemplate.hs view
@@ -12,8 +12,8 @@ import Control.Exception import Control.Monad ((<=<)) -- , when)-import Control.Monad.Trans.Maybe import Control.Monad.IO.Class (liftIO)+import Control.Monad.Trans.Maybe import Data.Bits import Data.Parameterized.Map (MapF) import qualified Data.Parameterized.Map as MapF@@ -38,6 +38,7 @@ import What4.Protocol.Online (SolverProcess(..), OnlineSolver(..)) import qualified What4.Solver.CVC4 as CVC4 +import What4.Expr import What4.Expr.App (reduceApp) import What4.Expr.Builder import What4.Expr.GroundEval@@ -53,10 +54,8 @@ --import Debug.Trace (trace) -data State t = State - main :: IO () main = do let fpp = knownRepr :: FloatPrecisionRepr Prec32@@ -66,7 +65,7 @@ (do r <- roundingModes (Some <$> floatTemplates [r] 1 fpp)) - sym <- newExprBuilder FloatIEEERepr State globalNonceGenerator+ sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState globalNonceGenerator extendConfig CVC4.cvc4Options (getConfiguration sym) proc <- Online.startSolverProcess @(SMT2.Writer CVC4.CVC4) CVC4.cvc4Features Nothing sym
+ test/hedgehog/Test/Tasty/Hedgehog/Alt.hs view
@@ -0,0 +1,29 @@+-- | Like "Test.Tasty.Hedgehog", but instead exposing an alternative+-- implementation of 'testProperty' that does not induce deprecation warnings.+module Test.Tasty.Hedgehog.Alt+ ( module TTH+ , testProperty+ ) where++import Data.String (IsString(fromString))+import Hedgehog (Property)+import Test.Tasty (TestName, TestTree)+import Test.Tasty.Hedgehog as TTH hiding (testProperty)++-- | Create a 'T.TestTree' from a Hedgehog 'Property'.+--+-- Note that @tasty-hedgehog@'s version of 'testProperty' has been deprecated+-- in favor of 'testPropertyNamed', whose second argument is intended to+-- represent the name of a top-level 'Property' value to run in the event that+-- the test fails. See https://github.com/qfpl/tasty-hedgehog/pull/42.+--+-- That being said, @what4@ currently does not define any of the properties+-- that it tests as top-level values, and it would be a pretty significant+-- undertaking to migrate all of the properties to top-level values. In the+-- meantime, we avoid incurring deprecation warnings by defining our own+-- version of 'testProperty'. The downside to this workaround is that if a+-- property fails, the error message it will produce will likely suggest+-- running ill-formed Haskell code, so users will have to use context clues to+-- determine how to /actually/ reproduce the error.+testProperty :: TestName -> Property -> TestTree+testProperty name = testPropertyNamed name (fromString name)
test/responses/err-behav-unrec.exp view
@@ -1,12 +1,4 @@-Left Could not parse solver response:- Solver response parsing failure.-*** Exception: Unrecognized response from solver:+Left 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
test/responses/minisat_verbose_success.strict.exp view
@@ -1,8 +1,1 @@-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+Left Parse exception: Failed reading: empty
test/responses/rsnunk-bad.exp view
@@ -1,12 +1,4 @@-Left Could not parse solver response:- Solver response parsing failure.-*** Exception: Unrecognized response from solver:+Left 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
what4.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.4 Name: what4-Version: 1.2.1+Version: 1.3 Author: Galois Inc. Maintainer: jhendrix@galois.com, rdockins@galois.com Copyright: (c) Galois, Inc 2014-2021@@ -9,7 +9,7 @@ Build-type: Simple Homepage: https://github.com/GaloisInc/what4 Bug-reports: https://github.com/GaloisInc/what4/issues-Tested-with: GHC==8.6.5, GHC==8.8.4, GHC==8.10.4, GHC==9.0.1+Tested-with: GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.2 Category: Formal Methods, Theorem Provers, Symbolic Computation, SMT Synopsis: Solver-agnostic symbolic values support for issuing queries Description:@@ -79,8 +79,10 @@ common testdefs-hedgehog import: testdefs+ hs-source-dirs: test/hedgehog build-depends: hedgehog >= 1.0.2- , tasty-hedgehog+ , tasty-hedgehog >= 1.2+ other-modules: Test.Tasty.Hedgehog.Alt common testdefs-hunit import: testdefs@@ -90,19 +92,20 @@ import: bldflags build-depends: base >= 4.8 && < 5,+ async, attoparsec >= 0.13, bimap >= 0.2, bifunctors >= 5, bv-sized >= 1.0.0, bytestring >= 0.10, deriving-compat >= 0.5,+ concurrent-extra >= 0.7 && < 0.8, config-value >= 0.8 && < 0.9, containers >= 0.5.0.0, data-binary-ieee754, deepseq >= 1.3, directory >= 1.2.2, exceptions >= 0.10,- extra >= 1.6, filepath >= 1.3, fingertree >= 0.1.4, hashable >= 1.3,@@ -143,6 +146,7 @@ What4.IndexLit What4.Interface What4.InterpretedFloatingPoint+ What4.FloatMode What4.LabeledPred What4.Panic What4.Partial@@ -150,12 +154,14 @@ What4.ProgramLoc What4.SatResult What4.SemiRing+ What4.SpecialFunctions What4.Symbol What4.SFloat What4.SWord What4.WordMap What4.Expr+ What4.Expr.Allocator What4.Expr.App What4.Expr.ArrayUpdateMap What4.Expr.AppTheory@@ -210,6 +216,7 @@ What4.Utils.MonadST What4.Utils.OnlyIntRepr What4.Utils.Process+ What4.Utils.ResolveBounds.BV What4.Utils.Streams What4.Utils.StringLiteral What4.Utils.Word16String@@ -235,6 +242,8 @@ main-is: AdapterTest.hs + other-modules: ProbeSolvers+ if flag(solverTests) buildable: True if ! flag(dRealTestDisable)@@ -252,6 +261,7 @@ lens, mtl >= 2.2.1, process,+ tasty-expected-failure >= 0.12 && < 0.13, text, versions @@ -271,6 +281,8 @@ main-is: OnlineSolverTest.hs + other-modules: ProbeSolvers+ if flag(solverTests) buildable: True if ! flag(STPTestDisable)@@ -279,27 +291,41 @@ buildable: False build-depends:+ async, bv-sized, bytestring,+ clock, containers, data-binary-ieee754,+ exceptions, lens,+ prettyprinter, process,+ tasty-expected-failure >= 0.12 && < 0.13,+ tasty-checklist >= 1.0 && < 1.1, text,+ units,+ units-defs, versions test-suite expr-builder-smtlib2- import: bldflags, testdefs-hunit+ import: bldflags, testdefs-hedgehog, testdefs-hunit type: exitcode-stdio-1.0 main-is: ExprBuilderSMTLib2.hs + other-modules: ProbeSolvers+ build-depends: bv-sized, bytestring, containers, data-binary-ieee754, libBF,+ prettyprinter,+ process,+ tasty-expected-failure >= 0.12 && < 0.13,+ tasty-checklist >= 1.0.3 && < 1.1, text, versions