what4 1.7 → 1.7.1.0
raw patch · 17 files changed
+519/−157 lines, 17 filesdep −ghc-primdep −utf8-stringdep ~basedep ~parameterized-utilsdep ~prettyprinternew-uploader
Dependencies removed: ghc-prim, utf8-string
Dependency ranges changed: base, parameterized-utils, prettyprinter, tasty, tasty-hunit, temporary
Files
- CHANGES.md +9/−0
- src/What4/BaseTypes.hs +10/−2
- src/What4/Concretize.hs +118/−0
- src/What4/Expr/Builder.hs +165/−119
- src/What4/Expr/GroundEval.hs +23/−1
- src/What4/Interface.hs +4/−0
- src/What4/Internal.hs +25/−0
- src/What4/InterpretedFloatingPoint.hs +9/−1
- src/What4/Protocol/SMTLib2/Parse.hs +8/−3
- src/What4/Protocol/SMTWriter.hs +27/−17
- src/What4/Solver/DReal.hs +9/−4
- src/What4/Utils/ResolveBounds/BV.hs +3/−0
- src/What4/Utils/Streams.hs +6/−3
- test/ExprBuilderSMTLib2.hs +23/−0
- test/ExprsTest.hs +6/−2
- test/PrinterTests.hs +60/−0
- what4.cabal +14/−5
CHANGES.md view
@@ -1,3 +1,12 @@+# 1.7.1 (November 2025)++* Add `asGround :: IsExpr e => e tp -> Maybe (GroundValue tp)`+* Add `What4.Concretize`, a module for concretizing symbolic values using models+ from solvers.+* Expose `ExprBuilder`'s uninterpreted function cache+* Fix a bug in which `sbvToInteger` could erroneously throw an `arithmetic+ underflow` exception when called on a length-1 signed bitvector.+ # 1.7 (March 2025) * The `BoolMap` parameter of `ConjPred` is now a `ConjMap`. This is a `newtype`
src/What4/BaseTypes.hs view
@@ -22,6 +22,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}@@ -30,6 +31,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}+ module What4.BaseTypes ( -- * BaseType data kind type BaseType@@ -289,13 +291,19 @@ instance ShowF BaseTypeRepr instance Pretty (FloatPrecisionRepr fpp) where- pretty = viaShow+ pretty (FloatingPointPrecisionRepr exp' sig) = + parens ("FloatingPrecision" <+> (pretty $ natValue exp') <+> (pretty $ natValue sig))+ instance Show (FloatPrecisionRepr fpp) where showsPrec = $(structuralShowsPrec [t|FloatPrecisionRepr|]) instance ShowF FloatPrecisionRepr +-- | Prints string type reprs, matching the syntax of crucible atoms https://github.com/GaloisInc/crucible/blob/a2502010cab0de44ec4c3b802453dc1009181d6b/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs#L148-L151 instance Pretty (StringInfoRepr si) where- pretty = viaShow+ pretty UnicodeRepr = "Unicode"+ pretty Char16Repr = "Char16"+ pretty Char8Repr = "Char8"+ instance Show (StringInfoRepr si) where showsPrec = $(structuralShowsPrec [t|StringInfoRepr|]) instance ShowF StringInfoRepr
+ src/What4/Concretize.hs view
@@ -0,0 +1,118 @@+-----------------------------------------------------------------------+-- |+-- Module : What4.Concretize+-- Description : Concretize values+-- Copyright : (c) Galois, Inc 2024+-- License : BSD3+-- Maintainer : Langston Barrett <langston@galois.com>+-- Stability : provisional+--+-- In our terminology, concretization is the process of (1) obtaining a+-- model from an SMT solver and (2) requesting the value of a particular set+-- of symbolic expressions in said model. The operation (2) alone is called+-- "grounding", see "What4.GroundEval".+-----------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}++module What4.Concretize+ ( ConcretizationFailure(..)+ , concretize+ , UniqueConcretizationFailure(..)+ , uniquelyConcretize+ ) where++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++-- | Reasons why attempting to resolve a symbolic expression as ground can fail.+data ConcretizationFailure+ = SolverUnknown+ -- ^ Querying the SMT solver yielded @UNKNOWN@.+ | UnsatInitialAssumptions+ -- ^ Querying the SMT solver for an initial model of the expression failed+ -- due to the initial assumptions in scope being unsatisfiable.+ deriving Show++-- | Get a 'WEG.GroundValue' for a 'WI.SymExpr' by asking an online solver for+-- a model.+--+-- In contrast with 'uniquelyConcretize', this function returns the value of the+-- 'WI.SymExpr' in just one of potentially many distinct models. See the Haddock+-- on 'uniquelyConcretize' for a further comparison.+concretize ::+ ( sym ~ WEB.ExprBuilder scope st fs+ , WPO.OnlineSolver solver+ ) =>+ WPO.SolverProcess scope solver ->+ -- | The symbolic term to query from the model+ WI.SymExpr sym tp ->+ IO (Either ConcretizationFailure (WEG.GroundValue tp))+concretize sp val =+ case WEG.asGround val of+ Just gVal -> pure (Right gVal)+ Nothing -> do+ WPO.inNewFrame sp $ do+ msat <- WPO.checkAndGetModel sp "Ground value using model"+ case msat of+ WSat.Unknown -> pure $ Left SolverUnknown+ WSat.Unsat {} -> pure $ Left UnsatInitialAssumptions+ WSat.Sat mdl -> Right <$> WEG.groundEval mdl val++data UniqueConcretizationFailure+ = GroundingFailure ConcretizationFailure+ | MultipleModels+ -- ^ There are multiple possible models for the expression, which means it+ -- is truly symbolic and therefore unable to be uniquely concretized.+ deriving Show++-- | Attempt to resolve the given 'WI.SymExpr' to a unique concrete value using+-- an online SMT solver connection.+--+-- The implementation of this function (1) asks for a model from the solver.+-- If it gets one, it (2) adds a blocking clause and asks for another. If there+-- was only one model, concretize the initial value and return it with 'Right'.+-- Otherwise, return an explanation of why concretization failed with 'Left'.+-- This behavior is contrasted with 'concretize', which just does (1).+uniquelyConcretize ::+ ( sym ~ WEB.ExprBuilder scope st fs+ , WPO.OnlineSolver solver+ ) =>+ -- | The symbolic backend+ sym ->+ WPO.SolverProcess scope solver ->+ -- | The symbolic term to concretize+ WI.SymExpr sym tp ->+ IO (Either UniqueConcretizationFailure (WEG.GroundValue tp))+uniquelyConcretize sym sp val =+ case WEG.asGround val of+ Just gVal -> pure (Right gVal)+ Nothing -> do+ -- First, check to see if there is a model of the symbolic value.+ concVal_ <- concretize sp val+ case concVal_ of+ Left e -> pure (Left (GroundingFailure e))+ Right concVal -> do+ -- We found a model, so check to see if this is the only possible+ -- model for this symbolic value. We do this by adding a blocking+ -- clause that assumes the `SymExpr` is /not/ equal to the model we+ -- found in the previous step. If this is unsatisfiable, the SymExpr+ -- can only be equal to that model, so we can conclude it is concrete.+ -- If it is satisfiable, on the other hand, the `SymExpr` can be+ -- multiple values, so it is truly symbolic.+ WPO.inNewFrame sp $ do+ injectedConcVal <- WEG.groundToSym sym (WI.exprType val) concVal+ eq <- WI.isEq sym val injectedConcVal+ block <- WI.notPred sym eq+ WPS.assume (WPO.solverConn sp) block+ msat' <- WPO.checkAndGetModel sp "Concretize value (with blocking clause)"+ case msat' of+ WSat.Unknown -> pure $ Left $ GroundingFailure $ SolverUnknown+ WSat.Sat _mdl -> pure $ Left $ MultipleModels+ WSat.Unsat {} -> pure $ Right concVal -- There is a single concrete result
src/What4/Expr/Builder.hs view
@@ -80,6 +80,7 @@ , stopCaching , exprBuilderSplitConfig , exprBuilderFreshConfig+ , uninterpFnCache, UninterpFunCache -- * Specialized representations , bvUnary@@ -414,7 +415,7 @@ , sbVarBindings :: !(IORef (SymbolVarBimap t)) - , sbUninterpFnCache :: !(IORef (Map (SolverSymbol, Some (Ctx.Assignment BaseTypeRepr)) (SomeSymFn (ExprBuilder t st fs))))+ , sbUninterpFnCache :: !(IORef (UninterpFunCache t st fs)) -- | Cache for Matlab functions , sbMatlabFnCache :: !(PH.HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))@@ -426,6 +427,11 @@ , sbFloatMode :: !(FloatModeRepr fm) } +-- | Keep track of uninterpred functions we've already made+type UninterpFunCache t st fs =+ Map SolverSymbol (PM.MapF (Assignment BaseTypeRepr)+ (SymFnWrapper (ExprBuilder t st fs)))+ type instance SymFn (ExprBuilder t st fs) = ExprSymFn t type instance SymExpr (ExprBuilder t st fs) = Expr t type instance BoundVar (ExprBuilder t st fs) = ExprBoundVar t@@ -446,6 +452,9 @@ pushMuxOps :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseBoolType) pushMuxOps = to sbPushMuxOps +uninterpFnCache :: Getter (ExprBuilder t st fs) (IORef (UninterpFunCache t st fs))+uninterpFnCache = to sbUninterpFnCache+ -- | 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@@ -1655,54 +1664,74 @@ Expr t (SR.SemiRingBase sr) -> IO (Expr t (SR.SemiRingBase sr)) semiRingIte sym sr c x y- -- evaluate as constants- | Just True <- asConstantPred c = return x- | Just False <- asConstantPred c = return y-- -- reduce negations- | Just (NotPred c') <- asApp c+ | Just (IteNot c') <- reduceIte c x y = semiRingIte sym sr c' y x-- -- remove the ite if the then and else cases are the same- | x == y = return x+ | Just (IteReduced e) <- reduceIte c x y+ = return e -- Try to extract common sum information. | (z, x',y') <- WSum.extractCommon (asWeightedSum sr x) (asWeightedSum sr y) , not (WSum.isZero sr z) = do xr <- semiRingSum sym x' yr <- semiRingSum sym y'- let sz = 1 + iteSize xr + iteSize yr- r <- sbMakeExpr sym (BaseIte (SR.semiRingBase sr) sz c xr yr)+ r <- baseIte sym c xr yr semiRingSum sym $! WSum.addVar sr z r -- final fallback, create the ite term- | otherwise =- let sz = 1 + iteSize x + iteSize y in- sbMakeExpr sym (BaseIte (SR.semiRingBase sr) sz c x y)+ | otherwise+ = baseIte sym c x y +data ReduceIteResult t bt+ = -- | We had @ite (not p)@, so reverse the branches and try again+ IteNot (Expr t BaseBoolType)+ | IteReduced (Expr t bt) -mkIte ::- ExprBuilder t st fs ->+-- | Perform common rewrites on @ite@ expressions+reduceIte :: Expr t BaseBoolType -> Expr t bt -> Expr t bt ->- IO (Expr t bt)-mkIte sym c x y- -- evaluate as constants- | Just True <- asConstantPred c = return x- | Just False <- asConstantPred c = return y+ Maybe (ReduceIteResult t bt)+reduceIte c x y+ | Just b <- asConstantPred c+ = if b then Just (IteReduced x) else Just (IteReduced y) - -- reduce negations- | Just (NotPred c') <- asApp c- = mkIte sym c' y x+ -- remove the ite if the then and else cases are the same+ | x == y+ = Just (IteReduced x) - -- remove the ite if the then and else cases are the same- | x == y = return x+ | Just (NotPred c') <- asApp c+ = Just (IteNot c') | otherwise =- let sz = 1 + iteSize x + iteSize y in- sbMakeExpr sym (BaseIte (exprType x) sz c x y)+ Nothing +mkIte ::+ ExprBuilder t st fs ->+ Expr t BaseBoolType ->+ Expr t bt ->+ Expr t bt ->+ IO (Expr t bt)+mkIte sym c x y =+ case reduceIte c x y of+ Just (IteNot c') -> baseIte sym c' y x+ Just (IteReduced e) -> pure e+ Nothing -> baseIte sym c x y++-- | Construct 'BaseIte'.+--+-- 'Ex.assert's that the if-then-else is not trivially reducible.+baseIte ::+ ExprBuilder t st fs ->+ Expr t BaseBoolType ->+ Expr t x ->+ Expr t x ->+ IO (Expr t x)+baseIte sym c x y =+ Ex.assert (isNothing (reduceIte c x y)) $ do+ let sz = 1 + iteSize x + iteSize y+ sbMakeExpr sym $ BaseIte (exprType x) sz c x y+ semiRingLe :: ExprBuilder t st fs -> SR.OrderedSemiRingRepr sr ->@@ -1753,7 +1782,10 @@ where sr = SR.orderedSemiRing osr +-- Note: requires that the equality is not trivially reducible, and asserts as+-- much (by calling 'baseEq'). semiRingEq ::+ Abstractable (SR.SemiRingBase sr) => ExprBuilder t st fs -> SR.SemiRingRepr sr -> (Expr t (SR.SemiRingBase sr) -> Expr t (SR.SemiRingBase sr) -> IO (Expr t BaseBoolType))@@ -1762,9 +1794,6 @@ Expr t (SR.SemiRingBase sr) -> IO (Expr t BaseBoolType) semiRingEq sym sr rec x y- -- Check for syntactic equality.- | x == y = return (truePred sym)- -- Push some equalities under if/then/else | SemiRingLiteral _ _ _ <- x , Just (BaseIte _ _ c a b) <- asApp y@@ -1781,10 +1810,9 @@ (Just a, Just b) -> return $! backendPred sym (SR.eq sr a b) _ -> do xr <- semiRingSum sym x' yr <- semiRingSum sym y'- sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min xr yr) (max xr yr)+ baseEq sym xr yr - | otherwise =- sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min x y) (max x y)+ | otherwise = baseEq sym x y semiRingAdd :: forall t st fs sr.@@ -2079,8 +2107,8 @@ = sbMakeExpr sym (NotPred x) eqPred sym x y- | x == y- = return (truePred sym)+ | Just b <- checkEq x y+ = return $ backendPred sym b | Just (NotPred x') <- asApp x = xorPred sym x' y@@ -2094,7 +2122,7 @@ (Just True, _) -> return y (_, Just False) -> notPred sym x (_, Just True) -> return x- _ -> sbMakeExpr sym $ BaseEq BaseBoolRepr (min x y) (max x y)+ _ -> baseEq sym x y xorPred sym x y = notPred sym =<< eqPred sym x y @@ -2159,24 +2187,15 @@ = notPred sym =<< conjPred sym (BM.ConjMap (BM.fromVars [asNegAtom a, asNegAtom b])) itePred sb c x y+ | Just (IteNot c') <- reduceIte c x y = itePred sb c' y x+ | Just (IteReduced e) <- reduceIte c x y = return e+ -- ite c c y = c || y | c == x = orPred sb c y -- ite c x c = c && x | c == y = andPred sb c x - -- ite c x x = x- | x == y = return x-- -- ite 1 x y = x- | Just True <- asConstantPred c = return x-- -- ite 0 x y = y- | Just False <- asConstantPred c = return y-- -- ite !c x y = ite c y x- | Just (NotPred c') <- asApp c = itePred sb c' y x- -- ite c 1 y = c || y | Just True <- asConstantPred x = orPred sb c y @@ -2190,9 +2209,7 @@ | Just False <- asConstantPred y = andPred sb c x -- Default case- | otherwise =- let sz = 1 + iteSize x + iteSize y in- sbMakeExpr sb $ BaseIte BaseBoolRepr sz c x y+ | otherwise = baseIte sb c x y ---------------------------------------------------------------------- -- Integer operations.@@ -2208,8 +2225,7 @@ intIte sym c x y = semiRingIte sym SR.SemiRingIntegerRepr c x y intEq sym x y- -- Use range check- | Just b <- rangeCheckEq (exprAbsValue x) (exprAbsValue y)+ | Just b <- checkEq x y = return $ backendPred sym b -- Reduce to bitvector equality, when possible@@ -2705,6 +2721,9 @@ | otherwise = sbMakeExpr sym $ BVFill w p bvIte sym c x y+ | Just (IteNot c') <- reduceIte c x y = bvIte sym c' y x+ | Just (IteReduced e) <- reduceIte c x y = return e+ | Just (BVFill w px) <- asApp x , Just (BVFill _w py) <- asApp y = do z <- itePred sym c px py@@ -2740,18 +2759,16 @@ Just (Some flv) -> semiRingIte sym (SR.SemiRingBVRepr flv (bvWidth x)) c x y Nothing ->- mkIte sym c x y)+ baseIte sym c x y) bvEq sym x y- | x == y = return $! truePred sym+ | Just b <- checkEq x y+ = return $ backendPred sym b | Just (BVFill _ px) <- asApp x , Just (BVFill _ py) <- asApp y = eqPred sym px py - | Just b <- BVD.eq (exprAbsValue x) (exprAbsValue y) = do- return $! backendPred sym b- -- Push some equalities under if/then/else | SemiRingLiteral _ _ _ <- x , Just (BaseIte _ _ c a b) <- asApp y@@ -2772,7 +2789,7 @@ (Just a, Just b) -> return $! backendPred sym (SR.eq sr a b) _ -> do xr <- semiRingSum sym x' yr <- semiRingSum sym y'- sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min xr yr) (max xr yr)+ baseEq sym xr yr | otherwise = do ut <- CFG.getOpt (sbUnaryThreshold sym)@@ -2781,7 +2798,7 @@ , Just uy <- asUnaryBV sym y -> UnaryBV.eq sym ux uy | otherwise- -> sbMakeExpr sym $ BaseEq (BaseBVRepr (bvWidth x)) (min x y) (max x y)+ -> baseEq sym x y bvSlt sym x y | Just xc <- asBV x@@ -3228,11 +3245,7 @@ BaseStructRepr flds -> sbMakeExpr sym $ StructField s i (flds Ctx.! i) - structIte sym p x y- | Just True <- asConstantPred p = return x- | Just False <- asConstantPred p = return y- | x == y = return x- | otherwise = mkIte sym p x y+ structIte = mkIte -------------------------------------------------------------------- -- String operations@@ -3243,23 +3256,9 @@ do l <- curProgramLoc sym return $! StringExpr s l - stringEq sym x y- | Just x' <- asString x- , Just y' <- asString y- = return $! backendPred sym (isJust (testEquality x' y'))- stringEq sym x y- = sbMakeExpr sym $ BaseEq (BaseStringRepr (stringInfo x)) x y+ stringEq = mkEq - stringIte _sym c x y- | Just c' <- asConstantPred c- = if c' then return x else return y- stringIte _sym _c x y- | Just x' <- asString x- , Just y' <- asString y- , isJust (testEquality x' y')- = return x- stringIte sym c x y- = mkIte sym c x y+ stringIte = mkIte stringIndexOf sym x y k | Just x' <- asString x@@ -3460,34 +3459,33 @@ else sbMakeExpr sym $ ArrayMap idx_tps baseRepr new_map def_map - arrayIte sym p x y = do- pmo <- CFG.getOpt (sbPushMuxOps sym)- if -- Extract all concrete updates out.- | not pmo- , ArrayMapView mx x' <- viewArrayMap x- , ArrayMapView my y' <- viewArrayMap y- , not (AUM.null mx) || not (AUM.null my) -> do- case exprType x of- BaseArrayRepr idxRepr bRepr -> do- let both_fn _ u v = baseTypeIte sym p u v- left_fn idx u = do- v <- sbConcreteLookup sym y' (Just idx) =<< symbolicIndices sym idx- both_fn idx u v- right_fn idx v = do- u <- sbConcreteLookup sym x' (Just idx) =<< symbolicIndices sym idx- both_fn idx u v- mz <- AUM.mergeM bRepr both_fn left_fn right_fn mx my- z' <- arrayIte sym p x' y'+ arrayIte sym p x y+ | Just (IteNot p') <- reduceIte p x y = arrayIte sym p' y x+ | Just (IteReduced e) <- reduceIte p x y = return e+ | otherwise = do+ pmo <- CFG.getOpt (sbPushMuxOps sym)+ if -- Extract all concrete updates out.+ | not pmo+ , ArrayMapView mx x' <- viewArrayMap x+ , ArrayMapView my y' <- viewArrayMap y+ , not (AUM.null mx) || not (AUM.null my) -> do+ case exprType x of+ BaseArrayRepr idxRepr bRepr -> do+ let both_fn _ u v = baseTypeIte sym p u v+ left_fn idx u = do+ v <- sbConcreteLookup sym y' (Just idx) =<< symbolicIndices sym idx+ both_fn idx u v+ right_fn idx v = do+ u <- sbConcreteLookup sym x' (Just idx) =<< symbolicIndices sym idx+ both_fn idx u v+ mz <- AUM.mergeM bRepr both_fn left_fn right_fn mx my+ z' <- arrayIte sym p x' y' - sbMakeExpr sym $ ArrayMap idxRepr bRepr mz z'+ sbMakeExpr sym $ ArrayMap idxRepr bRepr mz z' - | otherwise -> mkIte sym p x y+ | otherwise -> baseIte sym p x y - arrayEq sym x y- | x == y =- return $! truePred sym- | otherwise =- sbMakeExpr sym $! BaseEq (exprType x) x y+ arrayEq = mkEq arrayTrueOnEntries sym f a | Just True <- exprAbsValue a =@@ -3625,8 +3623,7 @@ realZero = sbZero realEq sym x y- -- Use range check- | Just b <- ravCheckEq (exprAbsValue x) (exprAbsValue y)+ | Just b <- checkEq x y = return $ backendPred sym b -- Reduce to integer equality, when possible@@ -4639,18 +4636,14 @@ -> IO (SymFn sym args ret) cachedUninterpFn sym fn_name arg_types ret_type handler = do fn_cache <- readIORef $ sbUninterpFnCache sym- case Map.lookup fn_key fn_cache of- Just (SomeSymFn fn)- | Just Refl <- testEquality (fnArgTypes fn) arg_types- , Just Refl <- testEquality (fnReturnType fn) ret_type- -> return fn- | otherwise- -> fail "Duplicate uninterpreted function declaration."+ case Map.lookup fn_name fn_cache >>= PM.lookup (arg_types Ctx.:> ret_type) of+ Just (SymFnWrapper fn) -> pure fn Nothing -> do fn <- handler sym fn_name arg_types ret_type- atomicModifyIORef' (sbUninterpFnCache sym) (\m -> (Map.insert fn_key (SomeSymFn fn) m, ()))+ let updArgs = PM.insert (arg_types Ctx.:> ret_type) (SymFnWrapper fn)+ updCache = Map.alter (Just . updArgs . fromMaybe PM.empty) fn_name+ _ <- atomicModifyIORef' (sbUninterpFnCache sym) (\m -> (updCache m, ())) return fn- where fn_key = (fn_name, Some (arg_types Ctx.:> ret_type)) mkUninterpFnApp :: (sym ~ ExprBuilder t st fs)@@ -4677,3 +4670,56 @@ let arg_types = fmapFC exprType args fn <- freshTotalUninterpFn sym fn_name arg_types ret_type applySymFn sym fn args++-- | Check if two symbolic values are known to be equal (@Just True@) or known+-- to be unequal (@Just False@).+checkEq ::+ Abstractable x =>+ Expr t x ->+ Expr t x ->+ Maybe Bool+checkEq x y+ | x == y = Just True++ | Just x' <- asConcrete x+ , Just y' <- asConcrete y = Just (x' == y')++ | otherwise+ = avCheckEq (exprType x) (exprAbsValue x) (exprAbsValue y)+-- This function is inlined into contexts where the type is known, hence it will+-- be specialized.+{-# INLINE checkEq #-}++mkEq ::+ Abstractable x =>+ ExprBuilder t st fs ->+ Expr t x ->+ Expr t x ->+ IO (Expr t BaseBoolType)+mkEq sym x y+ | Just b <- checkEq x y+ = return $ backendPred sym b++ | otherwise+ = sbMakeExpr sym $ BaseEq (exprType x) x y+-- This function is inlined into contexts where the type is known, hence it will+-- be specialized.+{-# INLINE mkEq #-}++-- | Construct 'BaseEq'.+--+-- Sorts the operands so that the lesser is the left hand side of the equality.+-- This helps normalize equality expressions so that rewrites such as @x = y+-- and x = y ==> true@ are more easily applied without worrying about symmetry+-- of equality.+--+-- 'Ex.assert's that the two values are not easily known to be (dis)equal.+baseEq ::+ Abstractable x =>+ ExprBuilder t st fs ->+ Expr t x ->+ Expr t x ->+ IO (Expr t BaseBoolType)+baseEq sym x y =+ Ex.assert (isNothing (checkEq x y)) $+ sbMakeExpr sym $ BaseEq (exprType x) (min x y) (max x y)
src/What4/Expr/GroundEval.hs view
@@ -9,6 +9,8 @@ -- -- Given a collection of assignments to the symbolic values appearing in -- an expression, this module computes the ground value.+--+-- See also "What4.Concretize". ------------------------------------------------------------------------ {-# LANGUAGE CPP #-}@@ -24,8 +26,9 @@ module What4.Expr.GroundEval ( -- * Ground evaluation GroundValue- , GroundValueWrapper(..)+ , asGround , groundToSym+ , GroundValueWrapper(..) , GroundArray(..) , lookupArray , GroundEvalFn(..)@@ -82,6 +85,25 @@ GroundValue (BaseStringType si) = StringLiteral si GroundValue (BaseArrayType idx b) = GroundArray idx b GroundValue (BaseStructType ctx) = Ctx.Assignment GroundValueWrapper ctx++-- | Return a ground representation of a value, if it is ground.+--+-- c.f. 'What4.Interface.asConcrete'.+asGround :: IsExpr e => e tp -> Maybe (GroundValue tp)+asGround x =+ case exprType x of+ BaseBoolRepr -> asConstantPred x+ BaseIntegerRepr -> asInteger x+ BaseRealRepr -> asRational x+ BaseStringRepr _si -> asString x+ BaseComplexRepr -> asComplex x+ BaseBVRepr _w -> asBV x+ BaseFloatRepr _fpp -> asFloat x+ BaseStructRepr _ -> asStruct x >>= traverseFC (fmap GVW . asGround)+ BaseArrayRepr _idx _tp -> do+ def <- asConstantArray x+ groundDef <- asGround def+ pure (ArrayConcrete groundDef Map.empty) -- | Inject a 'GroundValue' back into a 'SymExpr'. --
src/What4/Interface.hs view
@@ -3199,6 +3199,8 @@ -- | Return a concrete representation of a value, if it -- is concrete.+--+-- c.f. 'What4.GroundEval.asGround'. asConcrete :: IsExpr e => e tp -> Maybe (ConcreteVal tp) asConcrete x = case exprType x of@@ -3218,6 +3220,8 @@ pure (ConcreteArray idx c_def Map.empty) -- | Create a literal symbolic value from a concrete value.+--+-- c.f. 'What4.Expr.GroundEval.groundToSym' concreteToSym :: IsExprBuilder sym => sym -> ConcreteVal tp -> IO (SymExpr sym tp) concreteToSym sym = \case ConcreteBool True -> return (truePred sym)
+ src/What4/Internal.hs view
@@ -0,0 +1,25 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeApplications #-}++-- | Items in this module should /not/ be considered part of What4's API, they+-- are exported only for the sake of the test suite.+module What4.Internal+ ( assertionsEnabled+ ) where++import qualified Control.Exception as X+import Data.Functor ((<&>))++-- | Check if assertions are enabled.+--+-- Note [Asserts]: When optimizations are enabled, GHC compiles 'X.assert' to+-- a no-op. However, Cabal enables @-O1@ by default. Therefore, if we want our+-- assertions to be checked by our test suite, we must carefully ensure that we+-- pass the correct flags to GHC for the @lib:what4@ target. We verify that we+-- have done so by asserting as much in the test suite.+assertionsEnabled :: IO Bool+assertionsEnabled = do+ X.try @X.AssertionFailed (X.assert False (pure ())) <&>+ \case+ Left _ -> True+ Right () -> False
src/What4/InterpretedFloatingPoint.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}@@ -99,8 +100,15 @@ instance Hashable (FloatInfoRepr fi) where hashWithSalt = $(structuralHashWithSalt [t|FloatInfoRepr|] []) +-- | Prints float type reprs, matching the atoms in crucible https://github.com/GaloisInc/crucible/blob/a2502010cab0de44ec4c3b802453dc1009181d6b/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs#L153-L159 instance Pretty (FloatInfoRepr fi) where- pretty = viaShow+ pretty HalfFloatRepr = "Half"+ pretty SingleFloatRepr = "Float"+ pretty DoubleFloatRepr = "Double"+ pretty QuadFloatRepr = "Quad"+ pretty X86_80FloatRepr = "X86_80"+ pretty DoubleDoubleFloatRepr = "DoubleDouble"+ instance Show (FloatInfoRepr fi) where showsPrec = $(structuralShowsPrec [t|FloatInfoRepr|]) instance ShowF FloatInfoRepr
src/What4/Protocol/SMTLib2/Parse.hs view
@@ -42,18 +42,23 @@ import Control.Monad (when) import Control.Monad.Reader (ReaderT(..)) import qualified Data.ByteString as BS-import qualified Data.ByteString.UTF8 as UTF8 import Data.Char import Data.HashSet (HashSet) import qualified Data.HashSet as HSet import Data.Ratio import Data.String+import qualified Data.Text as Text+import Data.Text.Encoding (decodeUtf8With)+import Data.Text.Encoding.Error (lenientDecode) import Data.Word import System.IO c2b :: Char -> Word8 c2b = fromIntegral . fromEnum +decode :: BS.ByteString -> String+decode = Text.unpack . decodeUtf8With lenientDecode+ ------------------------------------------------------------------------ -- Parser definitions @@ -162,7 +167,7 @@ matchChar '"' l <- takeChars (/= '"') matchChar '"'- pure $ UTF8.toString l+ pure $ decode l -- | Defines common operations for parsing SMTLIB results. class CanParse a where@@ -309,7 +314,7 @@ case filter (\(m,_p) -> m == w) actions of [] -> do w' <- takeChars (\c -> c `notElem` ['\r', '\n'])- fail $ "Unsupported keyword: " ++ UTF8.toString (w <> w')+ fail $ "Unsupported keyword: " ++ decode (w <> w') [(_,p)] -> p _:_:_ -> fail $ "internal error: Duplicate keywords " ++ show w
src/What4/Protocol/SMTWriter.hs view
@@ -1598,31 +1598,41 @@ => NatRepr w -> v -> v-bvIntTerm w x = sumExpr ((\i -> digit (i-1)) <$> [1..natValue w])- where digit :: Natural -> v+bvIntTerm w x = sumExpr digits+ where -- Precondition: 1 <= w. This is upheld by the `1 <= w` constraint in+ -- bvIntTerm's type signature.+ digits :: [v]+ digits = (\i -> digit (i-1)) <$> [1..natValue w]++ digit :: Natural -> v digit d = ite (bvTestBit w d x) (fromInteger (2^d)) 0 -sbvIntTerm :: SupportTermOps v+-- @sbvIntTerm w x@ builds an integer term that has the same value as the+-- signed integer value of the bitvector @x@. This is done by explicitly+-- decomposing the positional notation of the bitvector into a sum of powers of+-- 2, plus an offset to ensure that the number is signed appropriately.+sbvIntTerm :: forall v w+ . (SupportTermOps v, 1 <= w) => NatRepr w -> v -> v-sbvIntTerm w0 x0 = sumExpr (signed_offset : go w0 x0 (natValue w0 - 2))- where signed_offset = ite (bvTestBit w0 (natValue w0 - 1) x0)- (fromInteger (negate (2^(widthVal w0 - 1))))- 0- go :: SupportTermOps v => NatRepr w -> v -> Natural -> [v]- go w x n- | n > 0 = digit w x n : go w x (n-1)- | n == 0 = [digit w x 0]- | otherwise = [] -- this branch should only be called in the degenerate case- -- of length 1 signed bitvectors+sbvIntTerm w x = sumExpr (signedOffset : digits)+ where -- Precondition: 1 <= w. This is upheld by the `1 <= w` constraint in+ -- sbvIntTerm's type signature.+ signedOffset :: v+ signedOffset = ite (bvTestBit w (natValue w - 1) x)+ (fromInteger (negate (2^(widthVal w - 1))))+ 0 - digit :: SupportTermOps v => NatRepr w -> v -> Natural -> v- digit w x d = ite (bvTestBit w d x)- (fromInteger (2^d))- 0+ digits :: [v]+ digits = (\i -> digit (i-1)) <$> [1..natValue w]++ digit :: SupportTermOps v => Natural -> v+ digit d = ite (bvTestBit w d x)+ (fromInteger (2^d))+ 0 unsupportedTerm :: MonadFail m => Expr t tp -> m a unsupportedTerm e =
src/What4/Solver/DReal.hs view
@@ -31,10 +31,12 @@ import Control.Lens(folded) import Control.Monad import Data.Attoparsec.ByteString.Char8 hiding (try)-import qualified Data.ByteString.UTF8 as UTF8+import Data.ByteString (ByteString) import Data.Map (Map) import qualified Data.Map as Map-import Data.Text.Encoding ( decodeUtf8 )+import Data.Text (unpack)+import Data.Text.Encoding ( decodeUtf8, decodeUtf8With )+import Data.Text.Encoding.Error (lenientDecode) import Data.Text.Lazy (Text) import qualified Data.Text.Lazy as Text import qualified Data.Text.Lazy.Builder as Builder@@ -62,6 +64,9 @@ import What4.Utils.Streams (logErrorStream) import What4.Utils.HandleReader +decode :: ByteString -> String+decode = unpack . decodeUtf8With lenientDecode+ data DReal = DReal deriving Show -- | Path to dReal@@ -260,7 +265,7 @@ , do _ <- char '[' sign <- option 1 (char '-' >> return (-1)) num <- takeWhile1 (\c -> c `elem` ("0123456789+-eE." :: String))- case readFloat (UTF8.toString num) of+ case readFloat (decode num) of (x,""):_ -> return $ Just (sign * x) _ -> fail "expected rational bound" ]@@ -271,7 +276,7 @@ , do sign <- option 1 (char '-' >> return (-1)) num <- takeWhile1 (\c -> c `elem` ("0123456789+-eE." :: String)) _ <- char ']'- case readFloat (UTF8.toString num) of+ case readFloat (decode num) of (x,""):_ -> return $ Just (sign * x) _ -> fail "expected rational bound" ]
src/What4/Utils/ResolveBounds/BV.hs view
@@ -87,6 +87,9 @@ -- 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'.+--+-- For just resolving a bitvector as concrete without searching for bounds, see+-- 'What4.Concretize.uniquelyConcretize'. resolveSymBV :: forall w sym solver scope st fs . ( 1 PN.<= w
src/What4/Utils/Streams.hs view
@@ -11,11 +11,14 @@ ( logErrorStream ) where -import qualified Data.ByteString.UTF8 as UTF8+import Data.ByteString (ByteString)+import Data.Text (unpack)+import Data.Text.Encoding (decodeUtf8With)+import Data.Text.Encoding.Error (lenientDecode) import qualified System.IO.Streams as Streams -- | Write from input stream to a logging function.-logErrorStream :: Streams.InputStream UTF8.ByteString+logErrorStream :: Streams.InputStream ByteString -> (String -> IO ()) -- ^ Logging function -> IO () logErrorStream err_stream logFn = do@@ -23,5 +26,5 @@ let write_err Nothing = return () write_err (Just b) = logFn b err_output <- Streams.makeOutputStream write_err- lns <- Streams.map UTF8.toString =<< Streams.lines err_stream+ lns <- Streams.map (unpack . decodeUtf8With lenientDecode) =<< Streams.lines err_stream Streams.connect lns err_output
test/ExprBuilderSMTLib2.hs view
@@ -1094,6 +1094,26 @@ _ -> fail "expected satisfible model" +-- | A regression test for #315.+issue315Test ::+ OnlineSolver solver =>+ SimpleExprBuilder t fs ->+ SolverProcess t solver ->+ IO ()+issue315Test sym solver = do+ let w = knownNat @61+ x <- freshConstant sym (safeSymbol "x") (BaseBVRepr w)+ xsi <- sbvToInteger sym x+ xi <- bvToInteger sym x+ p <- intEq sym xsi xi++ checkSatisfiableWithModel solver "test" p $ \case+ Sat fn ->+ do xEval <- groundEval fn x+ (xEval == 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" $@@ -1256,6 +1276,7 @@ , testCase "Z3 multidim array"$ withOnlineZ3 multidimArrayTest , testCase "Z3 #182 test case" $ withOnlineZ3 issue182Test+ , testCase "Z3 #315 test case" $ withOnlineZ3 issue315Test , arrayCopyTest , arraySetTest@@ -1306,6 +1327,7 @@ , cvcTestCase "multidim array"$ withCVC multidimArrayTest , cvcTestCase "#182 test case" $ withCVC issue182Test+ , cvcTestCase "#315 test case" $ withCVC issue315Test ] let cvc4Tests = cvcTests CVC4 let cvc5Tests = cvcTests CVC5@@ -1319,6 +1341,7 @@ , testCase "Yices pair" $ withYices pairTest , testCase "Yices rounding" $ withYices roundingTest , testCase "Yices #182 test case" $ withYices issue182Test+ , testCase "Yices #315 test case" $ withYices issue315Test ] let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id else fmap (ignoreTestBecause (nm <> " not present"))
test/ExprsTest.hs view
@@ -32,6 +32,7 @@ import What4.Concrete import What4.Expr import What4.Interface+import What4.Internal (assertionsEnabled) import Bool (boolTests) @@ -377,8 +378,11 @@ main :: IO () main = defaultMain $ testGroup "What4 Expressions"- [- testIntDivModProps+ [ -- See Note [Asserts] in what4+ testCase "assertions enabled" $ do+ assertsEnabled <- assertionsEnabled+ assertBool "assertions should be enabled" assertsEnabled+ , testIntDivModProps , testBvIsNeg , testInt , testProperty "stringEmpty" $ property $ do
+ test/PrinterTests.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE DataKinds #-}++import Data.Parameterized (knownNat)+import Prettyprinter+import Test.Tasty+import Test.Tasty.HUnit+import What4.BaseTypes (FloatPrecisionRepr (FloatingPointPrecisionRepr), NatRepr, StringInfoRepr (Char16Repr, Char8Repr, UnicodeRepr))+import What4.InterpretedFloatingPoint (FloatInfoRepr (DoubleDoubleFloatRepr, DoubleFloatRepr, HalfFloatRepr, QuadFloatRepr, SingleFloatRepr, X86_80FloatRepr))++testPrettyPrint :: (Pretty a) => String -> a -> String -> TestTree+testPrettyPrint tcName obj expected =+ testCase tcName $+ let s = show $ pretty obj+ in assertEqual "Should be equal" expected s++testPrintHalfFloatRepr :: TestTree+testPrintHalfFloatRepr = testPrettyPrint "Print half repr" HalfFloatRepr "Half"++testPrintFloatInfoRepr :: TestTree+testPrintFloatInfoRepr = testPrettyPrint "Print single repr" SingleFloatRepr "Float"++testPrintDoubleInfoRepr :: TestTree+testPrintDoubleInfoRepr = testPrettyPrint "Print double repr" DoubleFloatRepr "Double"++testPrintQuadInfoRepr :: TestTree+testPrintQuadInfoRepr = testPrettyPrint "Print quad repr" QuadFloatRepr "Quad"++testPrintX86_80InfoRepr :: TestTree+testPrintX86_80InfoRepr = testPrettyPrint "Print X86_80 repr" X86_80FloatRepr "X86_80"++testPrintDoubleDoubleInfoRepr :: TestTree+testPrintDoubleDoubleInfoRepr = testPrettyPrint "Print double double repr" DoubleDoubleFloatRepr "DoubleDouble"++five :: NatRepr 5+five = knownNat++eleven :: NatRepr 11+eleven = knownNat++main :: IO ()+main =+ defaultMain $+ testGroup "printers" $+ [ testGroup "Float printers" $+ [ testPrintFloatInfoRepr,+ testPrintHalfFloatRepr,+ testPrintDoubleInfoRepr,+ testPrintQuadInfoRepr,+ testPrintX86_80InfoRepr,+ testPrintDoubleDoubleInfoRepr+ ],+ testGroup "String repr printers" $+ [ testPrettyPrint "Print unicode repr" UnicodeRepr "Unicode",+ testPrettyPrint "Print char16 repr" Char16Repr "Char16",+ testPrettyPrint "Print char8 repr" Char8Repr "Char8"+ ],+ testGroup "Float precision repr prints" $+ [ testPrettyPrint "Print float precision repr" (FloatingPointPrecisionRepr five eleven) "(FloatingPrecision 5 11)"+ ]+ ]
what4.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.4 Name: what4-Version: 1.7+Version: 1.7.1.0 Author: Galois Inc. Maintainer: rscott@galois.com, kquick@galois.com Copyright: (c) Galois, Inc 2014-2023@@ -124,20 +124,17 @@ s-cargot >= 0.1 && < 0.2, scientific >= 0.3.6, stm,- temporary >= 1.2, template-haskell, text >= 1.2.4.0 && < 2.2, th-lift >= 0.8.2 && < 0.9, th-lift-instances >= 0.1 && < 0.2,- time >= 1.8 && < 1.13,+ time >= 1.8 && < 1.15, transformers >= 0.4, unliftio >= 0.2 && < 0.3, unordered-containers >= 0.2.10,- utf8-string >= 1.0.1, vector >= 0.12.1, versions >= 6.0.2 && < 6.1, zenc >= 0.1.0 && < 0.2.0,- ghc-prim >= 0.5.2 default-extensions: NondecreasingIndentation@@ -147,10 +144,12 @@ exposed-modules: What4.BaseTypes What4.Concrete+ What4.Concretize What4.Config What4.FunctionName What4.IndexLit What4.Interface+ What4.Internal What4.InterpretedFloatingPoint What4.FloatMode What4.LabeledPred@@ -302,6 +301,16 @@ , prettyprinter , tasty-checklist >= 1.0 && < 1.1 , text++test-suite printer-test+ import: bldflags, testdefs-hunit+ main-is: PrinterTests.hs+ type: exitcode-stdio-1.0+ build-depends:+ base,+ prettyprinter,+ tasty,+ tasty-hunit test-suite online-solver-test import: bldflags, testdefs-hunit