what4 1.5.1 → 1.6
raw patch · 19 files changed
+1007/−81 lines, 19 filesdep ~text
Dependency ranges changed: text
Files
- CHANGES.md +28/−0
- README.md +1/−0
- src/What4/Expr.hs +1/−0
- src/What4/Expr/App.hs +2/−2
- src/What4/Expr/Builder.hs +539/−42
- src/What4/Expr/MATLAB.hs +2/−2
- src/What4/Interface.hs +46/−5
- src/What4/Protocol/SMTLib2.hs +56/−4
- src/What4/Protocol/SMTWriter.hs +5/−3
- src/What4/Solver.hs +11/−0
- src/What4/Solver/Bitwuzla.hs +158/−0
- src/What4/Solver/Z3.hs +88/−9
- test/AdapterTest.hs +50/−3
- test/ConfigTest.hs +3/−1
- test/ExprBuilderSMTLib2.hs +3/−3
- test/InvariantSynthesis.hs +4/−3
- test/OnlineSolverTest.hs +3/−0
- test/ProbeSolvers.hs +3/−1
- what4.cabal +4/−3
CHANGES.md view
@@ -1,3 +1,31 @@+# 1.6 (May 2024)++* Allow building with GHC 9.8.++* Add more robust support for Constrained Horn Clause (CHC) solving:+ * The `IsSymExprBuilder` class now has two additional methods,+ `transformPredBV2LIA` and `transformSymFnLIA2BV`, which describe how to+ transform a bitvector (BV) predicate into a linear integer arithmetic (LIA)+ predicate and vice versa.+ * The `runZ3Horn` and `writeZ3HornSMT2File` functions now take an additional+ `Bool` argument. When this argument is `True`, Z3 will transform bitvector+ CHCs into linear integer arithmetic CHCs, which can sometimes help Z3 to+ solve CHC problems that it couldn't in a bitvector setting.++* Add support for the `bitwuzla` SMT solver.++* Add `bvZero` and `bvOne` functions, which are convenient shorthand for+ constructing bitvectors with the values `0` and `1`, respectively.++* Add `pushMuxOps` and `pushMuxOpsOption`. If this option is enabled, What4 will+ push certain `ExprBuilder` operations (e.g., `zext`) down to the branches of+ `ite` expressions. In some (but not all) circumstances, this can result in+ operations that are easier for SMT solvers to reason about.++* `annotateTerm` no longer adds annotations to bound variable expressions, which+ already have annotations attached to them. This should result in slightly+ better performance and better pretty-printing.+ # 1.5.1 (October 2023) * Require building with `versions >= 6.0.2`.
README.md view
@@ -280,6 +280,7 @@ - Yices 2.6.1 and 2.6.2 - CVC4 1.7 and 1.8 - CVC5 1.0.2+- Bitwuzla 0.3.0 - Boolector 3.2.1 and 3.2.2 - STP 2.3.3 (However, note https://github.com/stp/stp/issues/363, which prevents
src/What4/Expr.hs view
@@ -20,6 +20,7 @@ , curProgramLoc , unaryThreshold , cacheStartSize+ , pushMuxOps , exprBuilderSplitConfig , exprBuilderFreshConfig , EmptyExprBuilderState(..)
src/What4/Expr/App.hs view
@@ -2114,7 +2114,7 @@ SR.SemiRingRealRepr -> maybe (realLit sym 1) return =<< WSum.prodEvalM (realMul sym) return pd SR.SemiRingBVRepr SR.BVArithRepr w ->- maybe (bvLit sym w (BV.one w)) return =<< WSum.prodEvalM (bvMul sym) return pd+ maybe (bvOne sym w) return =<< WSum.prodEvalM (bvMul sym) return pd SR.SemiRingBVRepr SR.BVBitsRepr w -> maybe (bvLit sym w (BV.maxUnsigned w)) return =<< WSum.prodEvalM (bvAndBits sym) return pd @@ -2136,7 +2136,7 @@ BVOrBits w bs -> case bvOrToList bs of- [] -> bvLit sym w (BV.zero w)+ [] -> bvZero sym w (x:xs) -> foldM (bvOrBits sym) x xs BVTestBit i e -> testBitBV sym i e
src/What4/Expr/Builder.hs view
@@ -22,6 +22,7 @@ -} {-# LANGUAGE CPP #-} {-# LANGUAGE BangPatterns #-}+{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE EmptyCase #-}@@ -29,6 +30,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-}@@ -56,6 +58,7 @@ , sbNonceExpr , curProgramLoc , unaryThreshold+ , pushMuxOps , cacheStartSize , userState , exprCounter@@ -74,6 +77,7 @@ -- * configuration options , unaryThresholdOption , cacheStartSizeOption+ , pushMuxOpsOption , cacheTerms -- * Expr@@ -183,7 +187,8 @@ import qualified Control.Exception as Ex import Control.Lens hiding (asIndex, (:>), Empty) import Control.Monad-import Control.Monad.IO.Class+import Control.Monad.Except+import Control.Monad.Reader import Control.Monad.ST import Control.Monad.Trans.Writer.Strict (writer, runWriter) import qualified Data.BitVector.Sized as BV@@ -191,6 +196,8 @@ import qualified Data.Bimap as Bimap import Data.Hashable+import qualified Data.HashTable.Class as HC+import qualified Data.HashTable.IO as H import Data.IORef import Data.Kind import Data.List.NonEmpty (NonEmpty(..))@@ -331,6 +338,9 @@ compare (SomeExprSymFn fn1) (SomeExprSymFn fn2) = toOrdering $ fnCompare fn1 fn2 +instance Hashable (SomeExprSymFn t) where+ hashWithSalt s (SomeExprSymFn fn) = hashWithSalt s fn+ instance Show (SomeExprSymFn t) where show (SomeExprSymFn f) = show f @@ -366,6 +376,12 @@ -- | The starting size when building a new cache , sbCacheStartSize :: !(CFG.OptionSetting BaseIntegerType) + -- | If enabled, push certain 'ExprBuilder' operations (e.g., @zext@)+ -- down to the branches of @ite@ expressions. In some (but not all)+ -- circumstances, this can result in operations that are easier for+ -- SMT solvers to reason about.+ , sbPushMuxOps :: !(CFG.OptionSetting BaseBoolType)+ -- | Counter to generate new unique identifiers for elements and functions. , sbExprCounter :: !(NonceGenerator IO t) @@ -413,6 +429,9 @@ cacheStartSize :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseIntegerType) cacheStartSize = to sbCacheStartSize +pushMuxOps :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseBoolType)+pushMuxOps = to sbPushMuxOps+ -- | 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@@ -448,9 +467,11 @@ cfg <- CFG.initialConfig 0 [ unaryThresholdDesc , cacheStartSizeDesc+ , pushMuxOpsDesc ] unarySetting <- CFG.getOptionSetting unaryThresholdOption cfg cacheStartSetting <- CFG.getOptionSetting cacheStartSizeOption cfg+ pushMuxOpsSetting <- CFG.getOptionSetting pushMuxOpsOption cfg CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg nonLinearOps <- newIORef 0 @@ -458,6 +479,7 @@ , sbFloatReduce = True , sbUnaryThreshold = unarySetting , sbCacheStartSize = cacheStartSetting+ , sbPushMuxOps = pushMuxOpsSetting , sbProgramLoc = loc_ref , sbCurAllocator = storage_ref , sbNonLinearOps = nonLinearOps@@ -642,8 +664,29 @@ where sty = CFG.integerWithMinOptSty (CFG.Inclusive 0) help = Just "Maximum number of values in unary bitvector encoding." +------------------------------------------------------------------------+-- Configuration option for controlling whether to push certain ExprBuilder+-- operations (e.g., @zext@) down to the branches of @ite@ expressions. +-- | If this option enabled, push certain 'ExprBuilder' operations (e.g.,+-- @zext@) down to the branches of @ite@ expressions. In some (but not all)+-- circumstances, this can result in operations that are easier for SMT solvers+-- to reason about. The expressions that may be pushed down are determined on a+-- case-by-case basis in the 'IsExprBuilder' instance for 'ExprBuilder', but+-- this control applies to all such push-down checks.+--+-- This option is named \"backend.push_mux_ops\".+pushMuxOpsOption :: CFG.ConfigOption BaseBoolType+pushMuxOpsOption = CFG.configOption BaseBoolRepr "backend.push_mux_ops" +-- | The 'CFG.ConfigDesc' for 'pushMuxOpsOption'.+pushMuxOpsDesc :: CFG.ConfigDesc+pushMuxOpsDesc = CFG.mkOpt pushMuxOpsOption sty help (Just (ConcreteBool False))+ where sty = CFG.boolOptSty+ help = Just $+ "If this option enabled, push certain ExprBuilder operations " <>+ "(e.g., zext) down to the branches of ite expressions."+ newExprBuilder :: FloatModeRepr fm -- ^ Float interpretation mode (i.e., how are floats translated for the solver).@@ -670,9 +713,11 @@ cfg <- CFG.initialConfig 0 [ unaryThresholdDesc , cacheStartSizeDesc+ , pushMuxOpsDesc ] unarySetting <- CFG.getOptionSetting unaryThresholdOption cfg cacheStartSetting <- CFG.getOptionSetting cacheStartSizeOption cfg+ pushMuxOpsSetting <- CFG.getOptionSetting pushMuxOpsOption cfg CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg nonLinearOps <- newIORef 0 @@ -683,6 +728,7 @@ , sbFloatReduce = True , sbUnaryThreshold = unarySetting , sbCacheStartSize = cacheStartSetting+ , sbPushMuxOps = pushMuxOpsSetting , sbProgramLoc = loc_ref , sbExprCounter = gen , sbCurAllocator = storage_ref@@ -946,6 +992,351 @@ } evalBoundVars' tbls sym e ++-- | `ExprTransformer` and the associated code implement bidirectional bitvector+-- (BV) to/from linear integer arithmetic (LIA) transformations. This is done by+-- replacing all BV operations with LIA operations, replacing all BV variables+-- with LIA variables, and by replacing all BV function symbols with LIA+-- function symbols. The reverse transformation works the same way, but in+-- reverse. This transformation is not sound, but in practice it is useful.+--+-- This is used to implement `transformPredBV2LIA` and `transformSymFnLIA2BV`,+-- which in turn are used to implement @runZ3Horn@.+--+-- This is highly experimental and may be unstable.+newtype ExprTransformer t (tp1 :: BaseType) (tp2 :: BaseType) a =+ ExprTransformer (ExceptT String (ReaderT (ExprTransformerTables t tp1 tp2) IO) a)+ deriving (Functor, Applicative, Monad, MonadIO, MonadReader (ExprTransformerTables t tp1 tp2), MonadError String)++data ExprTransformerTables t (tp1 :: BaseType) (tp2 :: BaseType) = ExprTransformerTables+ { evalTables :: !(EvalHashTables t)+ , transformerSubst :: !(H.BasicHashTable (ExprBoundVar t tp1) (ExprBoundVar t tp2))+ , transformerFnSubst :: !(H.BasicHashTable (SomeExprSymFn t) (SomeExprSymFn t))+ }++runExprTransformer :: ExprTransformer t tp1 tp2 a -> ExprTransformerTables t tp1 tp2 -> IO (Either String a)+runExprTransformer (ExprTransformer action) = runReaderT (runExceptT action)++type BV2LIAExprTransformer t = ExprTransformer t (BaseBVType 64) BaseIntegerType+type LIA2BVExprTransformer t = ExprTransformer t BaseIntegerType (BaseBVType 64)+type HasTransformerConstraints t st fs tp1 tp2 =+ ( KnownRepr BaseTypeRepr tp1+ , KnownRepr BaseTypeRepr tp2+ , ?transformCmpTp1ToTp2 :: ExprBuilder t st fs -> Expr t BaseBoolType -> Maybe (ExprTransformer t tp1 tp2 (Expr t BaseBoolType))+ , ?transformExprTp1ToTp2 :: ExprBuilder t st fs -> Expr t tp1 -> ExprTransformer t tp1 tp2 (Expr t tp2)+ )++transformPred ::+ forall t st fs tp1 tp2 .+ HasTransformerConstraints t st fs tp1 tp2 =>+ ExprBuilder t st fs ->+ Expr t BaseBoolType ->+ ExprTransformer t tp1 tp2 (Expr t BaseBoolType)+transformPred sym e0 = exprTransformerCachedEval e0 $ case e0 of+ _ | Just action <- ?transformCmpTp1ToTp2 sym e0 -> action++ BoolExpr{} -> return e0++ AppExpr ae -> do+ let a = appExprApp ae+ a' <- traverseApp+ (\a'' -> case testEquality BaseBoolRepr (exprType a'') of+ Just Refl -> transformPred sym a''+ Nothing -> throwError $ "transformPred: unsupported non-boolean expression " ++ show a'')+ a+ if a == a' then+ return e0+ else+ liftIO $ reduceApp sym bvUnary a'++ NonceAppExpr ae -> do+ case nonceExprApp ae of+ Annotation tpr n a -> do+ a' <- transformPred sym a+ if a == a' then+ return e0+ else+ liftIO $ sbNonceExpr sym $ Annotation tpr n a'+ Forall v e -> do+ quantifier <- transformVarTp1ToTp2WithCont sym v (forallPred sym)+ -- Regenerate forallPred if e is changed by evaluation.+ runIfChanged e (transformPred sym) e0 $ liftIO . quantifier+ Exists v e -> do+ quantifier <- transformVarTp1ToTp2WithCont sym v (existsPred sym)+ -- Regenerate existsPred if e is changed by evaluation.+ runIfChanged e (transformPred sym) e0 $ liftIO . quantifier+ FnApp f a -> do+ (SomeExprSymFn f') <- transformFn sym $ SomeExprSymFn f+ (Some a') <- Ctx.fromList <$> mapM+ (\(Some a'') ->+ applyTp1ToTp2FunWithCont (?transformExprTp1ToTp2 sym) (transformPred sym) Some (exprType a'') a'')+ (toListFC Some a)+ case testEquality ((fmapFC exprType a') :> (fnReturnType f)) ((fnArgTypes f') :> (fnReturnType f')) of+ Just Refl -> liftIO $ applySymFn sym f' a'+ Nothing -> throwError $ "transformPred: unsupported FnApp " ++ show e0+ _ -> throwError $ "transformPred: unsupported NonceAppExpr " ++ show e0++ BoundVarExpr{} -> return e0++transformFn ::+ forall t st fs tp1 tp2 .+ HasTransformerConstraints t st fs tp1 tp2 =>+ ExprBuilder t st fs ->+ SomeExprSymFn t ->+ ExprTransformer t tp1 tp2 (SomeExprSymFn t)+transformFn sym (SomeExprSymFn f) = do+ inv_subst <- asks transformerFnSubst+ case symFnInfo f of+ UninterpFnInfo{}+ | Just Refl <- testEquality BaseBoolRepr (fnReturnType f) -> do+ (Some tps) <- Ctx.fromList <$> mapM+ (\(Some tp) -> applyTp1ToTp2FunWithCont (\_ -> return knownRepr) return Some tp tp)+ (toListFC Some $ fnArgTypes f)+ liftIO $ mutateInsertIO inv_subst (SomeExprSymFn f) $+ SomeExprSymFn <$> freshTotalUninterpFn sym (symFnName f) tps BaseBoolRepr+ | otherwise -> throwError $ "transformFn: unsupported UninterpFnInfo " ++ show f++ DefinedFnInfo vars e eval_fn+ | Just Refl <- testEquality BaseBoolRepr (fnReturnType f) -> do+ (Some vars') <- Ctx.fromList <$>+ mapM (\(Some v) -> transformVarTp1ToTp2WithCont sym v Some) (toListFC Some vars)+ e' <- transformPred sym e+ liftIO $ mutateInsertIO inv_subst (SomeExprSymFn f) $+ SomeExprSymFn <$> definedFn sym (symFnName f) vars' e' eval_fn+ | otherwise -> throwError $ "transformFn: unsupported DefinedFnInfo " ++ show f++ MatlabSolverFnInfo{} -> throwError $ "transformFn: unsupported MatlabSolverFnInfo " ++ show f++exprTransformerCachedEval ::+ Expr t tp -> ExprTransformer t tp1 tp2 (Expr t tp) -> ExprTransformer t tp1 tp2 (Expr t tp)+exprTransformerCachedEval e action = do+ tbls <- asks evalTables+ cachedEval (exprTable tbls) e action++transformCmpBV2LIA ::+ ExprBuilder t st fs ->+ Expr t BaseBoolType ->+ Maybe (BV2LIAExprTransformer t (Expr t BaseBoolType))+transformCmpBV2LIA sym e+ | Just (BaseEq _ x y) <- asApp e+ , Just Refl <- testEquality (BaseBVRepr $ knownNat @64) (exprType x) = Just $ do+ x' <- transformExprBV2LIA sym x+ y' <- transformExprBV2LIA sym y+ liftIO $ intEq sym x' y'++ | Just (BVUlt x y) <- asApp e+ , Just Refl <- testEquality (BaseBVRepr $ knownNat @64) (exprType x) = Just $ do+ x' <- transformExprBV2LIA sym x+ y' <- transformExprBV2LIA sym y+ liftIO $ intLt sym x' y'++ | Just (BVSlt x y) <- asApp e+ , Just Refl <- testEquality (BaseBVRepr $ knownNat @64) (exprType x) = Just $ do+ x' <- transformExprBV2LIA sym x+ y' <- transformExprBV2LIA sym y+ liftIO $ intLt sym x' y'++ | otherwise = Nothing++transformExprBV2LIA ::+ ExprBuilder t st fs ->+ Expr t (BaseBVType 64) ->+ BV2LIAExprTransformer t (Expr t BaseIntegerType)+transformExprBV2LIA sym e+ | Just semi_ring_sum <- asSemiRingSum (SR.SemiRingBVRepr SR.BVArithRepr (bvWidth e)) e =+ liftIO . semiRingSum sym =<<+ WSum.transformSum+ SR.SemiRingIntegerRepr+ (return . BV.asSigned (bvWidth e))+ (transformExprBV2LIA sym)+ semi_ring_sum++ | Just semi_ring_prod <- asSemiRingProd (SR.SemiRingBVRepr SR.BVArithRepr (bvWidth e)) e+ , Just e' <- WSum.asProdVar semi_ring_prod =+ transformExprBV2LIA sym e'++ | Just semi_ring_sum <- asSemiRingSum (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth e)) e+ , Just e' <- WSum.asVar semi_ring_sum =+ transformExprBV2LIA sym e'++ | Just semi_ring_prod <- asSemiRingProd (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth e)) e+ , Just e' <- WSum.asProdVar semi_ring_prod =+ transformExprBV2LIA sym e'++ | Just semi_ring_sum <- asSemiRingSum (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth e)) e+ , Just (c', e') <- WSum.asWeightedVar semi_ring_sum+ , Just semi_ring_sum' <- asSemiRingSum (SR.SemiRingBVRepr SR.BVArithRepr (bvWidth e')) e'+ , Just (c'', e'') <- WSum.asWeightedVar semi_ring_sum'+ , Just (BaseIte _ _ c a b) <- asApp e''+ , Just a_bv <- asBV a+ , Just b_bv <- asBV b = do+ x <- liftIO $ bvLit sym (bvWidth e) $ BV.xor c' $ BV.mul (bvWidth e) c'' a_bv+ y <- liftIO $ bvLit sym (bvWidth e) $ BV.xor c' $ BV.mul (bvWidth e) c'' b_bv+ transformExprBV2LIA sym =<< liftIO (bvIte sym c x y)++ | BoundVarExpr v <- e =+ BoundVarExpr <$> transformVarTp1ToTp2 sym v++ | Just (BaseIte _ _ c x y) <- asApp e = do+ let ?transformCmpTp1ToTp2 = transformCmpBV2LIA+ ?transformExprTp1ToTp2 = transformExprBV2LIA+ c' <- transformPred sym c+ x' <- transformExprBV2LIA sym x+ y' <- transformExprBV2LIA sym y+ liftIO $ intIte sym c' x' y'++ | Just (BVShl w x y) <- asApp e+ , Just y_bv <- asBV y = do+ e' <- liftIO $ bvMul sym x =<< bvLit sym w (BV.mkBV w $ 2 ^ BV.asUnsigned y_bv)+ transformExprBV2LIA sym e'++ | Just (BVLshr w x y) <- asApp e+ , Just y_bv <- asBV y = do+ e' <- liftIO $ bvUdiv sym x =<< bvLit sym w (BV.mkBV w $ 2 ^ BV.asUnsigned y_bv)+ transformExprBV2LIA sym e'++ | Just (BVUdiv _w x y) <- asApp e+ , Just y_bv <- asBV y = do+ x' <- transformExprBV2LIA sym x+ y' <- liftIO $ intLit sym $ BV.asUnsigned y_bv+ liftIO $ intDiv sym x' y'++ | Just (BVUrem _w x y) <- asApp e+ , Just y_bv <- asBV y = do+ x' <- transformExprBV2LIA sym x+ y' <- liftIO $ intLit sym $ BV.asUnsigned y_bv+ liftIO $ intMod sym x' y'++ | otherwise = throwError $ "transformExprBV2LIA: unsupported " ++ show e++transformCmpLIA2BV ::+ ExprBuilder t st fs ->+ Expr t BaseBoolType ->+ Maybe (LIA2BVExprTransformer t (Expr t BaseBoolType))+transformCmpLIA2BV sym e+ | Just (BaseEq BaseIntegerRepr x y) <- asApp e = Just $ do+ let (x_pos, x_neg) = asPositiveNegativeWeightedSum x+ let (y_pos, y_neg) = asPositiveNegativeWeightedSum y+ x' <- liftIO $ semiRingSum sym $ WSum.add SR.SemiRingIntegerRepr x_pos y_neg+ y' <- liftIO $ semiRingSum sym $ WSum.add SR.SemiRingIntegerRepr y_pos x_neg+ x'' <- transformExprLIA2BV sym x'+ y'' <- transformExprLIA2BV sym y'+ liftIO $ bvEq sym x'' y''++ | Just (SemiRingLe SR.OrderedSemiRingIntegerRepr x y) <- asApp e = Just $ do+ z <- liftIO $ intSub sym x y+ let (z_pos, z_neg) = asPositiveNegativeWeightedSum z+ x' <- liftIO . bvSemiRingZext sym (knownNat :: NatRepr 72)+ =<< transformExprLIA2BV sym+ =<< liftIO (semiRingSum sym z_pos)+ y' <- liftIO . bvSemiRingZext sym (knownNat :: NatRepr 72)+ =<< transformExprLIA2BV sym+ =<< liftIO (semiRingSum sym z_neg)+ liftIO $ bvUle sym x' y'++ | otherwise = Nothing++asPositiveNegativeWeightedSum ::+ Expr t BaseIntegerType ->+ (WSum.WeightedSum (Expr t) SR.SemiRingInteger, WSum.WeightedSum (Expr t) SR.SemiRingInteger)+asPositiveNegativeWeightedSum e = do+ let semi_ring_sum = asWeightedSum SR.SemiRingIntegerRepr e+ let positive_semi_ring_sum = runIdentity $ WSum.traverseCoeffs+ (return . max 0)+ semi_ring_sum+ let negative_semi_ring_sum = runIdentity $ WSum.traverseCoeffs+ (return . negate . min 0)+ semi_ring_sum+ (positive_semi_ring_sum, negative_semi_ring_sum)++transformExprLIA2BV ::+ ExprBuilder t st fs ->+ Expr t BaseIntegerType ->+ LIA2BVExprTransformer t (Expr t (BaseBVType 64))+transformExprLIA2BV sym e+ | Just semi_ring_sum <- asSemiRingSum SR.SemiRingIntegerRepr e =+ liftIO . semiRingSum sym =<<+ WSum.transformSum+ (SR.SemiRingBVRepr SR.BVArithRepr knownNat)+ (return . BV.mkBV knownNat)+ (transformExprLIA2BV sym)+ semi_ring_sum++ | BoundVarExpr v <- e =+ BoundVarExpr <$> transformVarTp1ToTp2 sym v++ | Just (BaseIte _ _ c x y) <- asApp e = do+ let ?transformCmpTp1ToTp2 = transformCmpLIA2BV+ ?transformExprTp1ToTp2 = transformExprLIA2BV+ c' <- transformPred sym c+ x' <- transformExprLIA2BV sym x+ y' <- transformExprLIA2BV sym y+ liftIO $ bvIte sym c' x' y'++ | otherwise = throwError $ "transformExprLIA2BV: unsupported " ++ show e++bvSemiRingZext :: (1 <= w, 1 <= w', w + 1 <= w')+ => ExprBuilder t st fs+ -> NatRepr w'+ -> Expr t (BaseBVType w)+ -> IO (Expr t (BaseBVType w'))+bvSemiRingZext sym w' e+ | Just semi_ring_sum <- asSemiRingSum (SR.SemiRingBVRepr SR.BVArithRepr (bvWidth e)) e =+ liftIO . semiRingSum sym =<<+ WSum.transformSum+ (SR.SemiRingBVRepr SR.BVArithRepr w')+ (return . BV.zext w')+ (bvZext sym w')+ semi_ring_sum+ | otherwise = bvZext sym w' e++transformVarTp1ToTp2WithCont ::+ forall t st fs tp tp1 tp2 a .+ (KnownRepr BaseTypeRepr tp1, KnownRepr BaseTypeRepr tp2) =>+ ExprBuilder t st fs ->+ ExprBoundVar t tp ->+ (forall tp' . ExprBoundVar t tp' -> a) ->+ ExprTransformer t tp1 tp2 a+transformVarTp1ToTp2WithCont sym v k = applyTp1ToTp2FunWithCont (transformVarTp1ToTp2 sym) return k (bvarType v) v++transformVarTp1ToTp2 ::+ (KnownRepr BaseTypeRepr tp1, KnownRepr BaseTypeRepr tp2) =>+ ExprBuilder t st fs ->+ ExprBoundVar t tp1 ->+ ExprTransformer t tp1 tp2 (ExprBoundVar t tp2)+transformVarTp1ToTp2 sym v = do+ tbl <- asks transformerSubst+ liftIO $ mutateInsertIO tbl v $ sbMakeBoundVar sym (bvarName v) knownRepr (bvarKind v) Nothing++applyTp1ToTp2FunWithCont ::+ forall t tp tp1 tp2 e a .+ (KnownRepr BaseTypeRepr tp1, KnownRepr BaseTypeRepr tp2, Show (e tp)) =>+ (e tp1 -> ExprTransformer t tp1 tp2 (e tp2)) ->+ (e BaseBoolType -> ExprTransformer t tp1 tp2 (e BaseBoolType)) ->+ (forall tp' . e tp' -> a) ->+ BaseTypeRepr tp ->+ e tp ->+ ExprTransformer t tp1 tp2 a+applyTp1ToTp2FunWithCont f g k tp e+ | Just Refl <- testEquality (knownRepr :: BaseTypeRepr tp1) tp =+ k <$> f e+ | Just Refl <- testEquality BaseBoolRepr tp =+ k <$> g e+ | otherwise = throwError $ "applyTp1ToTp2FunWithCont: unsupported " ++ show e++mutateInsertIO ::+ (HC.HashTable h, Eq k, Hashable k) =>+ H.IOHashTable h k v ->+ k ->+ IO v ->+ IO v+mutateInsertIO tbl k f = H.mutateIO tbl k $ \case+ Just v -> return (Just v, v)+ Nothing -> do+ v <- f+ return (Just v, v)++ -- | This attempts to lookup an entry in a symbolic array. -- -- It patterns maps on the array constructor.@@ -987,7 +1378,7 @@ , 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))+ is_diff_zero <- bvEq sym diff =<< bvZero sym (bvWidth diff) case asConstantPred is_diff_zero of Just True -> return v Just False -> sbConcreteLookup sym arr mcidx idx@@ -1630,6 +2021,7 @@ annotateTerm sym e = case e of+ BoundVarExpr (bvarId -> n) -> return (n, e) NonceAppExpr (nonceExprApp -> Annotation _ n _) -> return (n, e) _ -> do let tpr = exprType e@@ -1639,6 +2031,7 @@ getAnnotation _sym e = case e of+ BoundVarExpr (bvarId -> n) -> Just n NonceAppExpr (nonceExprApp -> Annotation _ n _) -> Just n _ -> Nothing @@ -2292,7 +2685,7 @@ bvFill sym w p | Just True <- asConstantPred p = bvLit sym w (BV.maxUnsigned w)- | Just False <- asConstantPred p = bvLit sym w (BV.zero w)+ | Just False <- asConstantPred p = bvZero sym w | otherwise = sbMakeExpr sym $ BVFill w p bvIte sym c x y@@ -2426,7 +2819,7 @@ -- shift by more than word width returns 0 | let (lo, _hi) = BVD.ubounds (exprAbsValue y) , lo >= intValue (bvWidth x)- = bvLit sym (bvWidth x) (BV.zero (bvWidth x))+ = bvZero sym (bvWidth x) | Just xv <- asBV x, Just n <- asBV y = bvLit sym (bvWidth x) (BV.shl (bvWidth x) xv (BV.asNatural n))@@ -2442,7 +2835,7 @@ -- shift by more than word width returns 0 | let (lo, _hi) = BVD.ubounds (exprAbsValue y) , lo >= intValue (bvWidth x)- = bvLit sym (bvWidth x) (BV.zero (bvWidth x))+ = bvZero sym (bvWidth x) | Just xv <- asBV x, Just n <- asBV y = bvLit sym (bvWidth x) $ BV.lshr (bvWidth x) xv (BV.asNatural n)@@ -2559,9 +2952,20 @@ bvUnary sym $ UnaryBV.uext u w | otherwise = do- Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w- sbMakeExpr sym $ BVZext w x+ pmo <- CFG.getOpt (sbPushMuxOps sym)+ if | pmo+ , Just (BaseIte _ _ c a b) <- asApp x+ , Just a_bv <- asBV a+ , Just b_bv <- asBV b -> do+ Just LeqProof <- return $ isPosNat w+ a' <- bvLit sym w $ BV.zext w a_bv+ b' <- bvLit sym w $ BV.zext w b_bv+ bvIte sym c a' b' + | otherwise -> do+ Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w+ sbMakeExpr sym $ BVZext w x+ bvSext sym w x | Just xv <- asBV x = do -- Add dynamic check for GHC typechecker.@@ -2582,11 +2986,22 @@ bvUnary sym $ UnaryBV.sext u w | otherwise = do- Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w- sbMakeExpr sym (BVSext w x)+ pmo <- CFG.getOpt (sbPushMuxOps sym)+ if | pmo+ , Just (BaseIte _ _ c a b) <- asApp x+ , Just a_bv <- asBV a+ , Just b_bv <- asBV b -> do+ Just LeqProof <- return $ isPosNat w+ a' <- bvLit sym w $ BV.sext (bvWidth x) w a_bv+ b' <- bvLit sym w $ BV.sext (bvWidth x) w b_bv+ bvIte sym c a' b' + | otherwise -> do+ Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w+ sbMakeExpr sym (BVSext w x)+ bvXorBits sym x y- | x == y = bvLit sym (bvWidth x) (BV.zero (bvWidth x)) -- special case: x `xor` x = 0+ | x == y = bvZero sym (bvWidth x) -- special case: x `xor` x = 0 | otherwise = let sr = SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x) in semiRingAdd sym sr x y@@ -2603,9 +3018,29 @@ = return x -- absorption law | otherwise- = let sr = SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x)- in semiRingMul sym sr x y+ = do pmo <- CFG.getOpt (sbPushMuxOps sym)+ if | pmo+ , Just (BaseIte _ _ c a b) <- asApp x+ , Just a_bv <- asBV a+ , Just b_bv <- asBV b+ , Just y_bv <- asBV y -> do+ a' <- bvLit sym (bvWidth x) $ BV.and a_bv y_bv+ b' <- bvLit sym (bvWidth x) $ BV.and b_bv y_bv+ bvIte sym c a' b' + | pmo+ , Just (BaseIte _ _ c a b) <- asApp y+ , Just a_bv <- asBV a+ , Just b_bv <- asBV b+ , Just x_bv <- asBV x -> do+ a' <- bvLit sym (bvWidth x) $ BV.and x_bv a_bv+ b' <- bvLit sym (bvWidth x) $ BV.and x_bv b_bv+ bvIte sym c a' b'++ | otherwise+ -> let sr = SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x)+ in semiRingMul sym sr x y+ -- XOR by the all-1 constant of the bitwise semiring. -- This is equivalant to negation bvNotBits sym x@@ -2613,8 +3048,17 @@ = bvLit sym (bvWidth x) $ xv `BV.xor` (BV.maxUnsigned (bvWidth x)) | otherwise- = let sr = (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x))- in semiRingSum sym $ WSum.addConstant sr (asWeightedSum sr x) (BV.maxUnsigned (bvWidth x))+ = do pmo <- CFG.getOpt (sbPushMuxOps sym)+ if | pmo+ , Just (BaseIte _ _ c a b) <- asApp x+ , Just a_bv <- asBV a+ , Just b_bv <- asBV b -> do+ a' <- bvLit sym (bvWidth x) $ BV.complement (bvWidth x) a_bv+ b' <- bvLit sym (bvWidth x) $ BV.complement (bvWidth x) b_bv+ bvIte sym c a' b'+ | otherwise ->+ let sr = (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x))+ in semiRingSum sym $ WSum.addConstant sr (asWeightedSum sr x) (BV.maxUnsigned (bvWidth x)) bvOrBits sym x y = case (asBV x, asBV y) of@@ -2691,14 +3135,23 @@ bvNeg sym x | Just xv <- asBV x = bvLit sym (bvWidth x) (BV.negate (bvWidth x) xv)- | otherwise =- do ut <- CFG.getOpt (sbUnaryThreshold sym)- let ?unaryThreshold = fromInteger ut- sbTryUnaryTerm sym- (do ux <- asUnaryBV sym x- Just (UnaryBV.neg sym ux))- (do let sr = SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x)- scalarMul sym sr (BV.mkBV (bvWidth x) (-1)) x)+ | otherwise = do+ pmo <- CFG.getOpt (sbPushMuxOps sym)+ if | pmo+ , Just (BaseIte _ _ c a b) <- asApp x+ , Just a_bv <- asBV a+ , Just b_bv <- asBV b -> do+ a' <- bvLit sym (bvWidth x) $ BV.negate (bvWidth x) a_bv+ b' <- bvLit sym (bvWidth x) $ BV.negate (bvWidth x) b_bv+ bvIte sym c a' b'+ | otherwise -> do+ ut <- CFG.getOpt (sbUnaryThreshold sym)+ let ?unaryThreshold = fromInteger ut+ sbTryUnaryTerm sym+ (do ux <- asUnaryBV sym x+ Just (UnaryBV.neg sym ux))+ (do let sr = SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x)+ scalarMul sym sr (BV.mkBV (bvWidth x) (-1)) x) bvIsNonzero sym x | Just (BaseIte _ _ p t f) <- asApp x@@ -2724,7 +3177,7 @@ ubv | otherwise = do let w = bvWidth x- zro <- bvLit sym w (BV.zero w)+ zro <- bvZero sym w notPred sym =<< bvEq sym x zro bvUdiv = bvBinDivOp (const BV.uquot) BVUdiv@@ -2991,26 +3444,28 @@ else sbMakeExpr sym $ ArrayMap idx_tps baseRepr new_map def_map - arrayIte sym p x y- -- Extract all concrete updates out.- | 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 = 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 -> mkIte sym p x y arrayEq sym x y | x == y =@@ -3074,7 +3529,7 @@ predToBV sym p w | Just b <- asConstantPred p =- if b then bvLit sym w (BV.one w) else bvLit sym w (BV.zero w)+ if b then bvOne sym w else bvZero sym w | otherwise = case testNatCases w (knownNat @1) of NatCaseEQ -> sbMakeExpr sym (BVFill (knownNat @1) p)@@ -4076,6 +4531,48 @@ , fnTable = fn_tbl } evalBoundVars' tbls sym e++ transformPredBV2LIA sym exprs = do+ expr_tbl <- stToIO PH.new+ fn_tbl <- stToIO PH.new+ let tbls = EvalHashTables+ { exprTable = expr_tbl+ , fnTable = fn_tbl+ }+ subst <- H.new+ fn_subst <- H.new+ let transformer_tbls = ExprTransformerTables+ { evalTables = tbls+ , transformerSubst = subst+ , transformerFnSubst = fn_subst+ }+ let ?transformCmpTp1ToTp2 = transformCmpBV2LIA+ ?transformExprTp1ToTp2 = transformExprBV2LIA+ lia_exprs <- either fail return =<<+ runExprTransformer (mapM (transformPred sym) exprs) transformer_tbls+ bv_to_lia_fn_subst <- Map.fromList <$>+ map (\(SomeExprSymFn f, SomeExprSymFn g) -> (SomeSymFn f, SomeSymFn g)) <$>+ H.toList fn_subst+ return (lia_exprs, bv_to_lia_fn_subst)++ transformSymFnLIA2BV sym (SomeSymFn fn) = do+ expr_tbl <- stToIO PH.new+ fn_tbl <- stToIO PH.new+ let tbls = EvalHashTables+ { exprTable = expr_tbl+ , fnTable = fn_tbl+ }+ subst <- H.new+ fn_subst <- H.new+ let transformer_tbls = ExprTransformerTables+ { evalTables = tbls+ , transformerSubst = subst+ , transformerFnSubst = fn_subst+ }+ let ?transformCmpTp1ToTp2 = transformCmpLIA2BV+ ?transformExprTp1ToTp2 = transformExprLIA2BV+ either fail (\(SomeExprSymFn fn') -> return $ SomeSymFn fn') =<<+ runExprTransformer (transformFn sym $ SomeExprSymFn fn) transformer_tbls instance IsInterpretedFloatExprBuilder (ExprBuilder t st fs) => IsInterpretedFloatSymExprBuilder (ExprBuilder t st fs)
src/What4/Expr/MATLAB.hs view
@@ -106,7 +106,7 @@ clampedIntMul sym x y = do let w = bvWidth x (hi,lo) <- signedWideMultiplyBV sym x y- zro <- bvLit sym w (BV.zero w)+ zro <- bvZero sym w ones <- maxUnsignedBV sym w ok_pos <- join $ andPred sym <$> (notPred sym =<< bvIsNeg sym lo) <*> bvEq sym hi zro@@ -178,7 +178,7 @@ sym no_underflow (bvSub sym x y) -- Perform subtraction if y >= x- (bvLit sym w (BV.zero w)) -- Otherwise return min int+ (bvZero sym w) -- Otherwise return min int clampedUIntMul :: (IsExprBuilder sym, 1 <= w) => sym
src/What4/Interface.hs view
@@ -156,6 +156,10 @@ , SymEncoder(..) -- * Utility combinators+ -- ** Bitvector operations+ , bvZero+ , bvOne+ -- ** Boolean operations , backendPred , andAllOf@@ -205,6 +209,7 @@ import Data.Coerce (coerce) import Data.Foldable import Data.Kind ( Type )+import Data.Map.Strict (Map) import qualified Data.Map as Map import Data.Parameterized.Classes import qualified Data.Parameterized.Context as Ctx@@ -691,7 +696,8 @@ 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.+ -- This returns 'Nothing' for terms that do not have annotations,+ -- or for terms that cannot be separated from their annotations. getUnannotatedTerm :: sym -> SymExpr sym tp -> Maybe (SymExpr sym tp) ----------------------------------------------------------------------@@ -943,7 +949,7 @@ -- | Return true if bitvector is negative. bvIsNeg :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)- bvIsNeg sym x = bvSlt sym x =<< bvLit sym (bvWidth x) (BV.zero (bvWidth x))+ bvIsNeg sym x = bvSlt sym x =<< bvZero sym (bvWidth x) -- | If-then-else applied to bitvectors. bvIte :: (1 <= w)@@ -1691,7 +1697,7 @@ -- Handle case where i < 0 min_sym <- intLit sym 0 is_lt <- intLt sym i min_sym- iteM bvIte sym is_lt (bvLit sym w (BV.zero w)) $ do+ iteM bvIte sym is_lt (bvZero sym w) $ do -- Handle case where i > maxUnsigned w let max_val = maxUnsigned w max_val_bv = BV.maxUnsigned w@@ -1741,7 +1747,7 @@ intToUInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n) intToUInt sym e w = do p <- bvIsNeg sym e- iteM bvIte sym p (bvLit sym w (BV.zero w)) (uintSetWidth sym e w)+ iteM bvIte sym p (bvZero sym w) (uintSetWidth sym e w) -- | Convert an unsigned bitvector to the nearest signed bitvector with -- the given width (clamp on overflow).@@ -2729,6 +2735,12 @@ data SomeSymFn sym = forall args ret . SomeSymFn (SymFn sym args ret) +instance IsSymFn (SymFn sym) => Eq (SomeSymFn sym) where+ (SomeSymFn fn1) == (SomeSymFn fn2) = isJust $ fnTestEquality fn1 fn2++instance IsSymFn (SymFn sym) => Ord (SomeSymFn sym) where+ compare (SomeSymFn fn1) (SomeSymFn fn2) = toOrdering $ fnCompare fn1 fn2+ -- | Wrapper for `SymFn` that concatenates the arguments and the return types. -- -- This is useful for implementing `TestEquality` and `OrdF` instances for@@ -2968,6 +2980,21 @@ SymExpr sym tp -> IO (SymExpr sym tp) + -- | Transform a BV predicate into an LIA predicate by replacing all bitvector+ -- (BV) operations with LIA operations, and replacing all BV variables with+ -- LIA variables. This transformation is not sound, but in practice it is+ -- useful. It returns the transformed predicate and a map from the original+ -- uninterpreted function symbols to the trnasformed uninterpreted function+ -- symbols.+ transformPredBV2LIA :: sym -> [Pred sym] -> IO ([Pred sym], Map (SomeSymFn sym) (SomeSymFn sym))++ -- | Transform a LIA defined boolean function into a BV defined boolean+ -- function by replacing all LIA operations with BV operations. Currently, the+ -- BV width for function parameters is set to 64, and for operations is set to+ -- 72.+ transformSymFnLIA2BV :: sym -> SomeSymFn sym -> IO (SomeSymFn sym)++ -- | This returns true if the value corresponds to a concrete value. baseIsConcrete :: forall e bt . IsExpr e@@ -3004,7 +3031,7 @@ case bt of BaseBoolRepr -> return $! falsePred sym BaseIntegerRepr -> intLit sym 0- BaseBVRepr w -> bvLit sym w (BV.zero w)+ BaseBVRepr w -> bvZero sym w BaseRealRepr -> return $! realZero sym BaseFloatRepr fpp -> floatPZero sym fpp BaseComplexRepr -> mkComplexLit sym (0 :+ 0)@@ -3271,3 +3298,17 @@ zeroStatistics :: Statistics zeroStatistics = Statistics { statAllocs = 0 , statNonLinearOps = 0 }++----------------------------------------------------------------------+-- Bitvector utilities++-- | An alias for 'minUnsignedBv'.+--+-- Useful in contexts where you want to convey the zero-ness of the value more+-- than its minimality.+bvZero :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> IO (SymBV sym w)+bvZero = minUnsignedBV++-- | A bitvector that is all zeroes except the LSB, which is one.+bvOne :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> IO (SymBV sym w)+bvOne sym w = bvLit sym w (BV.one w)
src/What4/Protocol/SMTLib2.hs view
@@ -101,16 +101,18 @@ import Control.Applicative import Control.Exception-import Control.Monad (forM, forM_, replicateM_, unless, when)+import Control.Monad (forM, replicateM_, unless, when) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Except (MonadError(..), ExceptT, runExceptT) import Control.Monad.Reader (MonadReader(..), ReaderT(..), asks) import qualified Data.Bimap as Bimap import qualified Data.BitVector.Sized as BV import Data.Char (digitToInt, isAscii)+import Data.Foldable import Data.HashMap.Lazy (HashMap) import qualified Data.HashMap.Lazy as HashMap import Data.IORef+import qualified Data.List as List import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Monoid@@ -151,6 +153,7 @@ import qualified What4.Expr.Builder as B import What4.Expr.GroundEval import qualified What4.Interface as I+import What4.Panic import What4.ProblemFeatures import What4.Protocol.Online import What4.Protocol.ReadDecimal@@ -984,7 +987,7 @@ let let_env = HashMap.fromList $ zip nms $ map (mapSome $ I.varExpr sym) vars proc_res <- runProcessor (ProcessorEnv { procSym = sym, procLetEnv = let_env }) $ parseExpr sym body_sexp Some body_expr <- either fail return proc_res- I.SomeSymFn <$> I.definedFn sym (I.safeSymbol $ Text.unpack nm) vars_assign body_expr I.NeverUnfold+ I.SomeSymFn <$> I.definedFn sym (I.safeSymbol $ Text.unpack nm) vars_assign body_expr I.AlwaysUnfold parseVar :: I.IsSymExprBuilder sym => sym -> SExp -> IO (Text, Some (I.BoundVar sym)) parseVar sym sexp = case sexp of@@ -1065,7 +1068,16 @@ Op sym data Assoc = RightAssoc | LeftAssoc+ deriving (Eq, Ord, Show) +opAssoc :: Op sym -> Maybe Assoc+opAssoc = \case+ Op1{} -> Nothing+ Op2 _ assoc _ -> assoc+ BVOp1{} -> Nothing+ BVOp2 assoc _ -> assoc+ BVComp2{} -> Nothing+ newtype Processor sym a = Processor (ExceptT String (ReaderT (ProcessorEnv sym) IO) a) deriving (Functor, Applicative, Monad, MonadIO, MonadError String, MonadReader (ProcessorEnv sym)) @@ -1168,7 +1180,44 @@ BVProof{} <- getBVProof arg1_expr BVProof{} <- getBVProof arg2_expr liftIO $ Some <$> I.bvConcat sym arg1_expr arg2_expr+ SApp [SApp ["_", "extract", i_sexp, j_sexp], arg]+ | Just i <- parseIntSolverValue i_sexp+ , Just j <- parseIntSolverValue j_sexp -> do+ let n = i - j + 1+ Some j_repr <- return $ mkNatRepr $ fromIntegral j+ Some n_repr <- return $ mkNatRepr $ fromIntegral n+ Some arg_expr <- parseExpr sym arg+ BVProof w_repr <- getBVProof arg_expr+ case (isPosNat n_repr, testLeq (addNat j_repr n_repr) w_repr) of+ (Just LeqProof, Just LeqProof) ->+ liftIO $ Some <$> I.bvSelect sym j_repr n_repr arg_expr+ _ -> throwError "" SApp ((SAtom operator) : operands) -> case HashMap.lookup operator (opTable @sym) of+ -- Sometimes, binary operators can be applied to more than two operands,+ -- e.g., (+ 1 2 3 4). We want to uniformly represent binary operators such+ -- that they are always applied to two operands, so this case converts the+ -- expression above to:+ --+ -- - (+ (+ (+ 1 2) 3) 4) (if + is left-associative)+ -- - (+ 1 (+ 2 (+ 3 4))) (if + is right-associative)+ --+ -- We then call `parseExpr` and recurse, which will reach one of the cases+ -- below.+ Just op+ | Just LeftAssoc <- opAssoc op+ , op1:op2:op3:ops <- operands ->+ parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, acc, arg]) op1 (op2:op3:ops)++ -- For right-associative operators, we could alternatively call+ -- init/last on the list of operands and call foldr on the results. The+ -- downside, however, is that init/last are partial functions. To avoid+ -- this partiality, we instead match on `reverse operands` and call+ -- foldl on the results (with the order of acc/arg swapped). This+ -- achieves the same end result and maintains the same asymptotic+ -- complexity as using init/tail.+ | Just RightAssoc <- opAssoc op+ , op1:op2:op3:ops <- List.reverse operands ->+ parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, arg, acc]) op1 (op2:op3:ops) Just (Op1 arg_types fn) -> do args <- mapM (parseExpr sym) operands exprAssignment arg_types args >>= \case@@ -1209,6 +1258,7 @@ (show n) _ -> throwError "" _ -> throwError ""+ -- | Verify a list of arguments has a single argument and -- return it, else raise an error. readOneArg ::@@ -1333,8 +1383,10 @@ AckUnsat -> Just $ Unsat () AckUnknown -> Just Unknown _ -> Nothing- in getLimitedSolverResponse "sat result" satRsp s- (head $ reverse $ checkCommands p)+ cmd = case reverse $ checkCommands p of+ cmd':_ -> cmd'+ [] -> panic "smtSatResult" ["Empty list of checkCommands"]+ in getLimitedSolverResponse "sat result" satRsp s cmd smtUnsatAssumptionsResult p s = let unsatAssumpRsp = \case
src/What4/Protocol/SMTWriter.hs view
@@ -829,13 +829,15 @@ cacheValueFn conn n lifetime value = cacheValue conn lifetime $ \entry -> stToIO $ PH.insert (symFnCache entry) n value +-- | Construct a function/name bimap. Each function is associated with its+-- cached name if there is one, otherwise with its original name. cacheLookupFnNameBimap :: WriterConn t h -> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text) cacheLookupFnNameBimap conn fns = Bimap.fromList <$> mapM (\some_fn@(SomeExprSymFn fn) -> do maybe_smt_sym_fn <- cacheLookupFn conn $ symFnId fn- case maybe_smt_sym_fn of- Just (SMTSymFn nm _ _) -> return (some_fn, nm)- Nothing -> fail $ "Could not find function in cache: " ++ show fn)+ return $ case maybe_smt_sym_fn of+ Just (SMTSymFn nm _ _) -> (some_fn, nm)+ Nothing -> (some_fn, solverSymbolAsText $ symFnName fn)) fns -- | Run state with handle.
src/What4/Solver.hs view
@@ -32,6 +32,16 @@ , runExternalABCInOverride , writeABCSMT2File + -- * Bitwuzla+ , Bitwuzla(..)+ , bitwuzlaAdapter+ , bitwuzlaPath+ , bitwuzlaTimeout+ , runBitwuzlaInOverride+ , withBitwuzla+ , bitwuzlaOptions+ , bitwuzlaFeatures+ -- * Boolector , Boolector(..) , boolectorAdapter@@ -107,6 +117,7 @@ ) where import What4.Solver.Adapter+import What4.Solver.Bitwuzla import What4.Solver.Boolector import What4.Solver.CVC4 import What4.Solver.CVC5
+ src/What4/Solver/Bitwuzla.hs view
@@ -0,0 +1,158 @@+------------------------------------------------------------------------+-- |+-- Module : What4.Solver.Bitwuzla+-- Description : Interface for running Bitwuzla+-- Copyright : (c) Galois, Inc 2014-2023+-- License : BSD3+-- Maintainer : Ryan Scott <rscott@galois.com>+-- Stability : provisional+--+-- This module provides an interface for running Bitwuzla and parsing+-- the results back.+------------------------------------------------------------------------+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}+module What4.Solver.Bitwuzla+ ( Bitwuzla(..)+ , bitwuzlaPath+ , bitwuzlaTimeout+ , bitwuzlaOptions+ , bitwuzlaAdapter+ , runBitwuzlaInOverride+ , withBitwuzla+ , bitwuzlaFeatures+ ) where++import Control.Monad+import Data.Bits ( (.|.) )++import What4.BaseTypes+import What4.Concrete+import What4.Config+import What4.Expr.Builder+import What4.Expr.GroundEval+import What4.Interface+import What4.ProblemFeatures+import What4.Protocol.Online+import qualified What4.Protocol.SMTLib2 as SMT2+import qualified What4.Protocol.SMTLib2.Syntax as Syntax+import What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )+import What4.SatResult+import What4.Solver.Adapter+import What4.Utils.Process++data Bitwuzla = Bitwuzla deriving Show++-- | Path to bitwuzla+bitwuzlaPath :: ConfigOption (BaseStringType Unicode)+bitwuzlaPath = configOption knownRepr "solver.bitwuzla.path"++-- | Per-check timeout, in milliseconds (zero is none)+bitwuzlaTimeout :: ConfigOption BaseIntegerType+bitwuzlaTimeout = configOption knownRepr "solver.bitwuzla.timeout"++-- | Control strict parsing for Bitwuzla solver responses (defaults+-- to solver.strict-parsing option setting).+bitwuzlaStrictParsing :: ConfigOption BaseBoolType+bitwuzlaStrictParsing = configOption knownRepr "solver.bitwuzla.strict_parsing"++bitwuzlaOptions :: [ConfigDesc]+bitwuzlaOptions =+ let bpOpt co = mkOpt+ co+ executablePathOptSty+ (Just "Path to bitwuzla executable")+ (Just (ConcreteString "bitwuzla"))+ mkTmo co = mkOpt co+ integerOptSty+ (Just "Per-check timeout in milliseconds (zero is none)")+ (Just (ConcreteInteger 0))+ bp = bpOpt bitwuzlaPath+ in [ bp+ , mkTmo bitwuzlaTimeout+ , copyOpt (const $ configOptionText bitwuzlaStrictParsing) strictSMTParseOpt+ ] <> SMT2.smtlib2Options++bitwuzlaAdapter :: SolverAdapter st+bitwuzlaAdapter =+ SolverAdapter+ { solver_adapter_name = "bitwuzla"+ , solver_adapter_config_options = bitwuzlaOptions+ , solver_adapter_check_sat = runBitwuzlaInOverride+ , solver_adapter_write_smt2 =+ SMT2.writeDefaultSMT2 () "Bitwuzla" defaultWriteSMTLIB2Features+ (Just bitwuzlaStrictParsing)+ }++instance SMT2.SMTLib2Tweaks Bitwuzla where+ smtlib2tweaks = Bitwuzla++runBitwuzlaInOverride+ :: ExprBuilder t st fs+ -> LogData+ -> [BoolExpr t]+ -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)+ -> IO a+runBitwuzlaInOverride =+ SMT2.runSolverInOverride Bitwuzla SMT2.nullAcknowledgementAction+ bitwuzlaFeatures (Just bitwuzlaStrictParsing)++-- | Run Bitwuzla in a session. Bitwuzla will be configured to produce models, but+-- otherwise left with the default configuration.+withBitwuzla+ :: ExprBuilder t st fs+ -> FilePath+ -- ^ Path to Bitwuzla executable+ -> LogData+ -> (SMT2.Session t Bitwuzla -> IO a)+ -- ^ Action to run+ -> IO a+withBitwuzla = SMT2.withSolver Bitwuzla SMT2.nullAcknowledgementAction+ bitwuzlaFeatures (Just bitwuzlaStrictParsing)++bitwuzlaFeatures :: ProblemFeatures+bitwuzlaFeatures = useBitvectors+ .|. useFloatingPoint+ .|. useQuantifiers+ .|. useSymbolicArrays+ .|. useUninterpFunctions+ .|. useUnsatCores+ .|. useUnsatAssumptions++instance SMT2.SMTLib2GenericSolver Bitwuzla where+ defaultSolverPath _ = findSolverPath bitwuzlaPath . getConfiguration+ defaultSolverArgs _ sym = do+ let cfg = getConfiguration sym+ timeout <- getOption =<< getOptionSetting bitwuzlaTimeout cfg+ let extraOpts = case timeout of+ Just (ConcreteInteger n) | n > 0 -> ["-t", show n]+ _ -> []+ return $ ["--lang", "smt2"] ++ extraOpts+ defaultFeatures _ = bitwuzlaFeatures+ setDefaultLogicAndOptions writer = do+ SMT2.setLogic writer Syntax.allLogic+ SMT2.setProduceModels writer True++setInteractiveLogicAndOptions ::+ SMT2.SMTLib2Tweaks a =>+ SMT2.WriterConn t (SMT2.Writer a) ->+ IO ()+setInteractiveLogicAndOptions writer = do+ SMT2.setOption writer "print-success" "true"+ SMT2.setOption writer "produce-models" "true"+ SMT2.setOption writer "global-declarations" "true"+ when (SMT2.supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do+ SMT2.setOption writer "produce-unsat-cores" "true"+ SMT2.setLogic writer Syntax.allLogic++instance OnlineSolver (SMT2.Writer Bitwuzla) where+ startSolverProcess feat mbIOh sym = do+ timeout <- SolverGoalTimeout <$>+ (getOpt =<< getOptionSetting bitwuzlaTimeout (getConfiguration sym))+ SMT2.startSolver Bitwuzla SMT2.smtAckResult+ setInteractiveLogicAndOptions+ timeout+ feat+ (Just bitwuzlaStrictParsing) mbIOh sym+ shutdownSolverProcess = SMT2.shutdownSolver Bitwuzla
src/What4/Solver/Z3.hs view
@@ -12,7 +12,9 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-}@@ -36,12 +38,15 @@ import qualified Data.Bimap as Bimap import Data.Bits import Data.Foldable+import Data.Map.Strict (Map)+import qualified Data.Map as Map import Data.String import Data.Text (Text) import qualified Data.Text as T import System.IO import Data.Parameterized.Map (MapF)+import qualified Data.Parameterized.Map as MapF import Data.Parameterized.Some import What4.BaseTypes import What4.Concrete@@ -248,14 +253,32 @@ -- -- CHCs are represented as pure SMT-LIB2 implications. For more information, see -- the [Z3 guide](https://microsoft.github.io/z3guide/docs/fixedpoints/intro/).+--+-- There are two ways to solve the CHCs: either by directly solving the problem+-- as is, or by transforming the problem into a set of linear integer arithmetic+-- (LIA) CHCs and solving that instead. The latter is done by replacing all+-- bitvector (BV) operations with LIA operations, and replacing all BV variables+-- with LIA variables. This transformation is not sound, but in practice it is a+-- useful heuristic. Then the result is transformed back into a BV result, and+-- checked for satisfiability. The satisfiability check is necessary because the+-- transformation is not sound, so LIA solution may not be a solution to the BV+-- CHCs. runZ3Horn ::+ forall sym t st fs . sym ~ ExprBuilder t st fs => sym ->+ Bool {- transform the BV CHCs into LIA CHCs -} -> LogData -> [SomeSymFn sym] -> [BoolExpr t] -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())-runZ3Horn sym log_data inv_fns horn_clauses = do+runZ3Horn sym do_bv_to_lia_transform log_data inv_fns horn_clauses = do+ (lia_inv_fns, lia_horn_clauses, bv_to_lia_fn_subst) <- transformHornClausesForZ3+ sym+ do_bv_to_lia_transform+ inv_fns+ horn_clauses+ logSolverEvent sym (SolverStartSATQuery $ SolverStartSATQueryRec { satQuerySolverName = show Z3@@ -263,9 +286,10 @@ }) path <- SMT2.defaultSolverPath Z3 sym- withZ3 sym path (log_data { logVerbosity = 2 }) $ \session -> do- writeHornProblem sym (SMT2.sessionWriter session) inv_fns horn_clauses- result <- RSP.getLimitedSolverResponse "check-sat"+ get_value_result <- withZ3 sym path (log_data { logVerbosity = 2 }) $ \session -> do+ writeHornProblem sym (SMT2.sessionWriter session) lia_inv_fns lia_horn_clauses++ check_sat_result <- RSP.getLimitedSolverResponse "check-sat" (\case RSP.AckSat -> Just $ Sat () RSP.AckUnsat -> Just $ Unsat ()@@ -276,7 +300,7 @@ logSolverEvent sym (SolverEndSATQuery $ SolverEndSATQueryRec- { satQueryResult = result+ { satQueryResult = check_sat_result , satQueryError = Nothing }) @@ -288,18 +312,59 @@ _ -> Nothing) (SMT2.sessionWriter session) (Syntax.getValue [])- SMT2.parseFnValues sym (SMT2.sessionWriter session) inv_fns sexp)+ SMT2.parseFnValues sym (SMT2.sessionWriter session) lia_inv_fns sexp) return- result+ check_sat_result + let transform_result_lia_to_bv ::+ SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) () ->+ IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())+ transform_result_lia_to_bv = \case+ Sat lia_defined_fns -> do+ defined_inv_fns <- MapF.fromList <$> mapM+ (\(SomeSymFn fn) ->+ if| Just (SomeSymFn lia_fn) <- Map.lookup (SomeSymFn fn) bv_to_lia_fn_subst+ , Just (SymFnWrapper lia_defined_fn) <- MapF.lookup (SymFnWrapper lia_fn) lia_defined_fns -> do+ some_defined_fn <- transformSymFnLIA2BV sym $ SomeSymFn lia_defined_fn+ case some_defined_fn of+ SomeSymFn defined_fn+ | Just Refl <- testEquality (fnArgTypes fn) (fnArgTypes defined_fn)+ , Just Refl <- testEquality (fnReturnType fn) (fnReturnType defined_fn) ->+ return $ MapF.Pair (SymFnWrapper fn) (SymFnWrapper defined_fn)+ _ -> fail $ "runZ3Horn: function type mismatch in solver result: " ++ show fn+ | otherwise -> fail $ "runZ3Horn: function not found in solver result: " ++ show fn)+ inv_fns++ all_unsat <- and <$> mapM+ (\clause -> do+ defined_clause <- notPred sym =<< substituteSymFns sym defined_inv_fns clause+ runZ3InOverride sym (log_data { logVerbosity = 2 }) [defined_clause] $ return . isUnsat)+ horn_clauses++ return $ if all_unsat then Sat defined_inv_fns else Unknown++ _ -> return Unknown++ if do_bv_to_lia_transform then+ transform_result_lia_to_bv get_value_result+ else+ return get_value_result+ writeZ3HornSMT2File :: sym ~ ExprBuilder t st fs => sym ->+ Bool {- transform the BV CHCs into LIA CHCs -} -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO ()-writeZ3HornSMT2File sym h inv_fns horn_clauses = do+writeZ3HornSMT2File sym do_bv_to_lia_transform h inv_fns horn_clauses = do+ (lia_inv_fns, lia_horn_clauses, _bv_to_lia_fn_subst) <- transformHornClausesForZ3+ sym+ do_bv_to_lia_transform+ inv_fns+ horn_clauses+ writer <- SMT2.defaultFileWriter Z3 (show Z3)@@ -308,8 +373,22 @@ sym h SMT2.setDefaultLogicAndOptions writer- writeHornProblem sym writer inv_fns horn_clauses+ writeHornProblem sym writer lia_inv_fns lia_horn_clauses SMT2.writeExit writer++transformHornClausesForZ3 ::+ sym ~ ExprBuilder t st fs =>+ sym ->+ Bool ->+ [SomeSymFn sym] ->+ [BoolExpr t] ->+ IO ([SomeSymFn sym], [BoolExpr t], Map (SomeSymFn sym) (SomeSymFn sym))+transformHornClausesForZ3 sym do_bv_to_lia_transform inv_fns horn_clauses =+ if do_bv_to_lia_transform then do+ (lia_horn_clauses, bv_to_lia_fn_subst) <- transformPredBV2LIA sym horn_clauses+ let lia_inv_fns = Map.elems bv_to_lia_fn_subst+ return (lia_inv_fns, lia_horn_clauses, bv_to_lia_fn_subst)+ else return (inv_fns, horn_clauses, Map.empty) writeHornProblem :: sym ~ ExprBuilder t st fs =>
test/AdapterTest.hs view
@@ -33,7 +33,9 @@ import What4.Config import What4.Expr+import What4.Expr.Builder ( asApp, pushMuxOpsOption ) import What4.Interface+import What4.Panic import What4.Protocol.SMTLib2.Response ( strictSMTParsing ) import What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness(..) ) import What4.Protocol.VerilogWriter@@ -45,6 +47,7 @@ , cvc5Adapter , yicesAdapter , z3Adapter+ , bitwuzlaAdapter , boolectorAdapter , externalABCAdapter #ifdef TEST_STP@@ -85,6 +88,7 @@ [ testGroup "deprecated configs" (deprecatedConfigTests adapters) , testGroup "strict parsing config" (strictParseConfigTests adapters)+ , testGroup "push mux ops config" (pushMuxOpsConfigTests adapters) ] where wantOptSetFailure withText res = case res of@@ -222,7 +226,50 @@ ] in fmap mkPCTest adaptrs + pushMuxOpsConfigTests adaptrs =+ let -- A basic test that ensures that pushMuxOps actually takes effect+ -- when enabled or disabled.+ mkPushZextMuxTest ::+ forall a.+ Bool ->+ (forall t. Expr t (BaseBVType 64) -> IO a) ->+ IO a+ mkPushZextMuxTest pushMuxOpsVal k =+ withAdapters adaptrs $ \sym -> do+ pmo <- getOptionSetting pushMuxOpsOption (getConfiguration sym)+ show <$> setOpt pmo pushMuxOpsVal >>= (@?= "[]")+ let w = knownNat @32+ a <- bvLit sym w $ mkBV w 27+ b <- bvLit sym w $ mkBV w 42+ c <- freshConstant sym (safeSymbol "c") BaseBoolRepr+ ite <- bvIte sym c a b+ zextIte <- bvZext sym (knownNat @64) ite+ k zextIte+ in [ testCase "enable pushMuxOps" $+ mkPushZextMuxTest True $ \zextIte ->+ case asApp zextIte of+ Just (BaseIte {}) -> pure ()+ _ -> assertFailure $ unlines+ [ "zext not pushed down through ite"+ , show $ printSymExpr zextIte+ ]++ , testCase "disable pushMuxOps" $+ mkPushZextMuxTest False $ \zextIte ->+ case asApp zextIte of+ Just (BVZext {}) -> pure ()+ _ -> assertFailure $ unlines+ [ "zext should be at the head of the application"+ , show $ printSymExpr zextIte+ ]+ ]+ deprecatedConfigTests adaptrs =+ let firstAdapter adptrs =+ case adptrs of+ adptr:_ -> adptr+ [] -> panic "deprecatedConfigTests" ["Empty list of adapters"]+ in [ testCaseSteps "deprecated default_solver is equivalent to solver.default" $@@ -257,7 +304,7 @@ step "Update the value via regular (text identification)" res2 <- try $ setUnicodeOpt settera $- pack $ solver_adapter_name $ head adaptrs+ pack $ solver_adapter_name $ firstAdapter adaptrs case res2 of Right warns -> fmap show warns @?= [] Left (SomeException e) -> assertFailure $ show e@@ -282,7 +329,7 @@ step "Reset to original value" res4 <- try $ setOpt settera' $- pack $ solver_adapter_name $ head adaptrs+ pack $ solver_adapter_name $ firstAdapter adaptrs case res4 of Right warns -> fmap show warns @?= [] Left (SomeException e) -> assertFailure $ show e@@ -540,7 +587,7 @@ nonlinearRealTest :: SolverAdapter EmptyExprBuilderState -> TestTree nonlinearRealTest adpt =- let wrap = if solver_adapter_name adpt `elem` [ "ABC", "boolector", "stp" ]+ let wrap = if solver_adapter_name adpt `elem` [ "ABC", "bitwuzla", "boolector", "stp" ] then expectFailBecause (solver_adapter_name adpt <> " does not support this type of linear arithmetic term")
test/ConfigTest.hs view
@@ -471,10 +471,12 @@ withChecklist "builtins" $ do cfg <- initialConfig 0 [] help <- configHelp "" cfg+ let nonEmptyOr :: (a -> b) -> b -> [a] -> b+ nonEmptyOr f = foldr (\h _ -> f h) help `checkValues` (Empty :> Val "num" length 1- :> Val "verbosity" (L.isInfixOf "verbosity =" . show . head) True+ :> Val "verbosity" (nonEmptyOr (L.isInfixOf "verbosity =" . show) False) True )
test/ExprBuilderSMTLib2.hs view
@@ -1068,7 +1068,7 @@ let idx = Ctx.Empty Ctx.:> idxInt let arrLookup = arrayLookup sym arr idx elt <- arrLookup- bvZero <- bvLit sym w (BV.zero w)+ bvZero <- bvZero sym w p <- bvEq sym elt bvZero checkSatisfiableWithModel solver "test" p $ \case@@ -1133,7 +1133,7 @@ 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)+ e1B <- bvAdd sym e1A' =<< bvOne sym w case asBV e1B of Just bv -> bv @?= BV.mkBV w 3 Nothing -> assertFailure $ unlines@@ -1151,7 +1151,7 @@ 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)+ e2D <- bvAdd sym e2C' =<< bvOne sym w case asBV e2D of Just bv -> bv @?= BV.mkBV w 3 Nothing -> assertFailure $ unlines
test/InvariantSynthesis.hs view
@@ -75,8 +75,8 @@ inv <- freshTotalUninterpFn sym (safeSymbol "inv") knownRepr knownRepr i <- freshConstant sym (safeSymbol "i") $ BaseBVRepr $ knownNat @64 n <- freshConstant sym (safeSymbol "n") knownRepr- zero <- bvLit sym knownNat $ BV.zero knownNat- one <- bvLit sym knownNat $ BV.one knownNat+ zero <- bvZero sym knownNat+ one <- bvOne sym knownNat ult_1_n <- bvUlt sym one n inv_0_n <- applySymFn sym inv $ Empty :> zero :> n -- 1 < n ==> inv(0, n)@@ -148,6 +148,7 @@ failureZ3 = "failure with older Z3 versions; upgrade to at least 4.8.9" defaultMain $ testGroup "Tests" $ [ synthesis_test "int" intProblem "cvc5" CVC5.runCVC5SyGuS CVC5.runCVC5InOverride- , skipPre4_8_9 failureZ3 $ synthesis_test "int" intProblem "z3" Z3.runZ3Horn Z3.runZ3InOverride+ , skipPre4_8_9 failureZ3 $ synthesis_test "int" intProblem "z3" (\sym -> Z3.runZ3Horn sym False) Z3.runZ3InOverride , synthesis_test "bv" bvProblem "cvc5" CVC5.runCVC5SyGuS CVC5.runCVC5InOverride+ , skipPre4_8_9 failureZ3 $ synthesis_test "bv->int" bvProblem "z3" (\sym -> Z3.runZ3Horn sym True) Z3.runZ3InOverride ]
test/OnlineSolverTest.hs view
@@ -63,6 +63,8 @@ , AnOnlineSolver @(SMT2.Writer CVC5) Proxy, cvc5Features, cvc5Options, Just cvc5Timeout) , (SolverName "Yices" , AnOnlineSolver @Yices.Connection Proxy, yicesDefaultFeatures, yicesOptions, Just yicesGoalTimeout)+ , (SolverName "Bitwuzla"+ , AnOnlineSolver @(SMT2.Writer Bitwuzla) Proxy, bitwuzlaFeatures, bitwuzlaOptions, Just bitwuzlaTimeout) , (SolverName "Boolector" , AnOnlineSolver @(SMT2.Writer Boolector) Proxy, boolectorFeatures, boolectorOptions, Just boolectorTimeout) #ifdef TEST_STP@@ -378,6 +380,7 @@ , (SolverName "CVC4", 7.5 % Second) -- CVC4 1.8 , (SolverName "CVC5", 0.40 % Second) -- CVC5 1.0.0 , (SolverName "Yices", 2.9 % Second) -- Yices 2.6.1+ , (SolverName "Bitwuzla", 0.51 % Second) -- Bitwuzla 0.3.0 , (SolverName "Boolector", 7.2 % Second) -- Boolector 3.2.1 , (SolverName "STP", 1.35 % Second) -- STP 2.3.3 ]
test/ProbeSolvers.hs view
@@ -27,7 +27,9 @@ if r == ExitSuccess then let ol = lines o in return $ Right $ SolverVersion- $ if null ol then (solver <> " v??") else head ol+ $ case ol of+ [] -> solver <> " v??"+ olh:_ -> olh else return $ Left $ solver <> " version error: " <> show r <> " /;/ " <> e Left (err :: SomeException) -> return $ Left $ solver <> " invocation error: " <> show err
what4.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.4 Name: what4-Version: 1.5.1+Version: 1.6 Author: Galois Inc. Maintainer: rscott@galois.com, kquick@galois.com Copyright: (c) Galois, Inc 2014-2023@@ -16,7 +16,7 @@ What4 is a generic library for representing values as symbolic formulae which may contain references to symbolic values, representing unknown variables. It provides support for communicating with a variety of SAT and SMT solvers,- including Z3, CVC4, CVC5, Yices, Boolector, STP, and dReal.+ including Z3, CVC4, CVC5, Yices, Bitwuzla, Boolector, STP, and dReal. The data representation types make heavy use of GADT-style type indices to ensure type-correct manipulation of symbolic values.@@ -126,7 +126,7 @@ stm, temporary >= 1.2, template-haskell,- text >= 1.2.4.0 && < 2.1,+ 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,@@ -190,6 +190,7 @@ What4.Solver What4.Solver.Adapter+ What4.Solver.Bitwuzla What4.Solver.Boolector What4.Solver.CVC4 What4.Solver.CVC5