diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,14 @@ +# 1.5 (July 2023) + +* Allow building with GHC 9.6. + +* The `MonadTrans (PartialT sym)` instance now has a `IsExpr (SymExpr sym)` + constraint in its instance context. (This is a requirement imposed by + `MonadTrans` gaining a quantified `Monad` superclass in `mtl-2.3`.) + +* Make `what4` simplify expressions of the form + `(bvult (bvadd a c) (bvadd b c))` to `(bvult a b)` when it is sound to do so. + # 1.4 (January 2023) * Allow building with GHC 9.4. diff --git a/doc/arithdomain.cry b/doc/arithdomain.cry --- a/doc/arithdomain.cry +++ b/doc/arithdomain.cry @@ -306,6 +306,20 @@ sle : {n} (fin n, n >= 1) => Dom n -> Dom n -> Bit sle a b = (sbounds a).1 <=$ (sbounds b).0 +ult_sum_common_equiv : {n} (fin n) => Dom n -> Dom n -> Dom n -> Bit +ult_sum_common_equiv a b c = + if al == ah /\ bl == bh /\ al == bl + then True + else if ~(carry cl c.sz) + then check_same_wrap_interval cl ch + else check_same_wrap_interval cl mask`{n} /\ check_same_wrap_interval 0 ch + where + (cl, ch) = (c.lo, c.lo + c.sz) + (al, ah) = ubounds a + (bl, bh) = ubounds b + check_same_wrap_interval lo hi = + ~(carry ah hi) /\ ~(carry bh hi) \/ carry al lo /\ carry bl lo + // A bitmask indicating which bits cannot be determined // given the interval information in the given domain unknowns : {n} (fin n, n >= 1) => Dom n -> [n] @@ -460,6 +474,13 @@ correct_ule a b x y = ule a b ==> mem a x ==> mem b y ==> x <= y +correct_ult_sum_common_equiv : + {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n -> [n] -> [n] -> [n] -> Bit +correct_ult_sum_common_equiv a b c x y z = + ult_sum_common_equiv a b c ==> + mem a x ==> mem b y ==> mem c z ==> + (x + z < y + z <==> x < y) + correct_bnot : {n} (fin n) => Dom n -> [n] -> Bit correct_bnot a x = mem a x <==> mem (bnot a) (~ x) @@ -505,6 +526,7 @@ property o2 = correct_sle`{16} property o3 = correct_ult`{16} property o4 = correct_ule`{16} +property o5 = correct_ult_sum_common_equiv`{4} //////////////////////////////////////////////////////////// // Operations preserve singletons diff --git a/src/What4/Config.hs b/src/What4/Config.hs --- a/src/What4/Config.hs +++ b/src/What4/Config.hs @@ -175,10 +175,10 @@ import qualified Control.Concurrent.ReadWriteVar as RWV import Control.Lens ((&)) import qualified Control.Lens.Combinators as LC +import Control.Monad (foldM, when) import Control.Monad.Catch import Control.Monad.IO.Class -import Control.Monad.Identity -import Control.Monad.Writer.Strict hiding ((<>)) +import Control.Monad.Writer.Strict (MonadWriter(..), WriterT, execWriterT) import Data.Foldable (toList) import Data.Kind import Data.List.NonEmpty (NonEmpty(..)) diff --git a/src/What4/Expr/Builder.hs b/src/What4/Expr/Builder.hs --- a/src/What4/Expr/Builder.hs +++ b/src/What4/Expr/Builder.hs @@ -2400,6 +2400,14 @@ | x == y = return $! falsePred sym + | sr <- SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x) + , (z, x', y') <- WSum.extractCommon (asWeightedSum sr x) (asWeightedSum sr y) + , not (WSum.isZero sr z) + , BVD.isUltSumCommonEquiv (WSum.sumAbsValue x') (WSum.sumAbsValue y') (WSum.sumAbsValue z) = do + xr <- semiRingSum sym x' + yr <- semiRingSum sym y' + bvUlt sym xr yr + | otherwise = do ut <- CFG.getOpt (sbUnaryThreshold sym) let ?unaryThreshold = fromInteger ut diff --git a/src/What4/Expr/Simplify.hs b/src/What4/Expr/Simplify.hs --- a/src/What4/Expr/Simplify.hs +++ b/src/What4/Expr/Simplify.hs @@ -20,8 +20,9 @@ ) where import Control.Lens ((^.)) +import Control.Monad (void, when) import Control.Monad.ST -import Control.Monad.State +import Control.Monad.State (MonadState(..), State, execState) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Maybe @@ -144,7 +145,7 @@ count_subterms' :: Expr t tp -> Counter () count_subterms' e0 = case e0 of - BoolExpr{} -> pure () + BoolExpr{} -> pure () SemiRingLiteral{} -> pure () StringExpr{} -> pure () FloatExpr{} -> pure () diff --git a/src/What4/Expr/VarIdentification.hs b/src/What4/Expr/VarIdentification.hs --- a/src/What4/Expr/VarIdentification.hs +++ b/src/What4/Expr/VarIdentification.hs @@ -42,9 +42,10 @@ #endif import Control.Lens -import Control.Monad.Reader +import Control.Monad (when) +import Control.Monad.Reader (MonadReader(..), ReaderT(..)) import Control.Monad.ST -import Control.Monad.State +import Control.Monad.State (StateT, execStateT) import Data.Bits import qualified Data.HashTable.ST.Basic as H import Data.List.NonEmpty (NonEmpty(..)) diff --git a/src/What4/Expr/WeightedSum.hs b/src/What4/Expr/WeightedSum.hs --- a/src/What4/Expr/WeightedSum.hs +++ b/src/What4/Expr/WeightedSum.hs @@ -70,7 +70,7 @@ ) where import Control.Lens -import Control.Monad.State +import Control.Monad (unless) import qualified Data.BitVector.Sized as BV import Data.Hashable import Data.Kind diff --git a/src/What4/Partial.hs b/src/What4/Partial.hs --- a/src/What4/Partial.hs +++ b/src/What4/Partial.hs @@ -266,7 +266,7 @@ instance (IsExpr (SymExpr sym), MonadFail m) => MonadFail (PartialT sym m) where fail msg = PartialT $ \_ _ -> fail msg -instance MonadTrans (PartialT sym) where +instance IsExpr (SymExpr sym) => MonadTrans (PartialT sym) where lift m = PartialT $ \_ p -> PE p <$> m instance (IsExpr (SymExpr sym), MonadIO m) => MonadIO (PartialT sym m) where diff --git a/src/What4/Protocol/SMTLib2.hs b/src/What4/Protocol/SMTLib2.hs --- a/src/What4/Protocol/SMTLib2.hs +++ b/src/What4/Protocol/SMTLib2.hs @@ -101,8 +101,10 @@ import Control.Applicative import Control.Exception -import Control.Monad.Except -import Control.Monad.Reader +import Control.Monad (forM, 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) @@ -707,7 +709,7 @@ getUnsatCoreCommand _ = SMT2.getUnsatCore getAbductCommand _ nm e = SMT2.getAbduct nm e getAbductNextCommand _ = SMT2.getAbductNext - + setOptCommand _ = SMT2.setOption declareCommand _proxy v argTypes retType = @@ -1283,7 +1285,7 @@ -> Text -> Term -> IO [String] -runGetAbducts s n nm p = +runGetAbducts s n nm p = if (n > 0) then do writeGetAbduct (sessionWriter s) nm p let valRsp = \x -> case x of diff --git a/src/What4/Protocol/SMTLib2/Parse.hs b/src/What4/Protocol/SMTLib2/Parse.hs --- a/src/What4/Protocol/SMTLib2/Parse.hs +++ b/src/What4/Protocol/SMTLib2/Parse.hs @@ -39,7 +39,8 @@ import qualified Control.Monad.Fail #endif -import Control.Monad.Reader +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 diff --git a/src/What4/Protocol/SMTWriter.hs b/src/What4/Protocol/SMTWriter.hs --- a/src/What4/Protocol/SMTWriter.hs +++ b/src/What4/Protocol/SMTWriter.hs @@ -111,11 +111,13 @@ import Control.Exception import Control.Lens hiding ((.>), Strict) +import Control.Monad (forM_, unless, when) import Control.Monad.IO.Class -import Control.Monad.Reader +import Control.Monad.Reader (ReaderT(..), asks) import Control.Monad.ST -import Control.Monad.State.Strict -import Control.Monad.Trans.Maybe +import Control.Monad.State.Strict (State, runState) +import Control.Monad.Trans (MonadTrans(..)) +import Control.Monad.Trans.Maybe (MaybeT(..)) import Data.Bimap (Bimap) import qualified Data.Bimap as Bimap import qualified Data.BitVector.Sized as BV diff --git a/src/What4/Protocol/VerilogWriter/AST.hs b/src/What4/Protocol/VerilogWriter/AST.hs --- a/src/What4/Protocol/VerilogWriter/AST.hs +++ b/src/What4/Protocol/VerilogWriter/AST.hs @@ -19,7 +19,9 @@ import qualified Data.Set as Set import Data.String import Data.Word -import Control.Monad.Except +import Control.Monad (forM_) +import Control.Monad.Except (ExceptT, MonadError(..)) +import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.State (MonadState(), StateT(..), get, put, modify, gets) import qualified What4.BaseTypes as WT diff --git a/src/What4/Protocol/VerilogWriter/Backend.hs b/src/What4/Protocol/VerilogWriter/Backend.hs --- a/src/What4/Protocol/VerilogWriter/Backend.hs +++ b/src/What4/Protocol/VerilogWriter/Backend.hs @@ -16,8 +16,9 @@ where +import Control.Monad (foldM) import Control.Monad.State (get) -import Control.Monad.Except +import Control.Monad.Except (MonadError(..)) import qualified Data.BitVector.Sized as BV import Data.List.NonEmpty ( NonEmpty(..) ) diff --git a/src/What4/Serialize/Parser.hs b/src/What4/Serialize/Parser.hs --- a/src/What4/Serialize/Parser.hs +++ b/src/What4/Serialize/Parser.hs @@ -34,6 +34,7 @@ , printSExpr ) where +import Control.Monad ( when ) import qualified Control.Monad.Except as E import Control.Monad.IO.Class ( liftIO ) import qualified Control.Monad.Reader as R @@ -886,7 +887,7 @@ readLetFnExpr bindings _body = E.throwError $ "invalid s-expression for let-bindings: " ++ (show bindings) - + -- | Parse an arbitrary expression. readExpr :: forall sym t st fs . (sym ~ W4.ExprBuilder t st fs) @@ -1030,7 +1031,7 @@ Right solverSym -> return solverSym argNames <- readFnArgs argVarsRaw (argTys, _retTy) <- readFnType rawFnType - E.when (not (length argTys == length argNames)) $ + when (not (length argTys == length argNames)) $ E.throwError $ "Function type expected " ++ (show $ length argTys) ++ " args but found " diff --git a/src/What4/Serialize/Printer.hs b/src/What4/Serialize/Printer.hs --- a/src/What4/Serialize/Printer.hs +++ b/src/What4/Serialize/Printer.hs @@ -89,7 +89,7 @@ instance Ord (SomeExprSymFn t) where compare (SomeExprSymFn fn1) (SomeExprSymFn fn2) = - compare (Nonce.indexValue $ W4.symFnId fn1) (Nonce.indexValue $ W4.symFnId fn2) + compare (Nonce.indexValue $ W4.symFnId fn1) (Nonce.indexValue $ W4.symFnId fn2) instance Show (SomeExprSymFn t) where @@ -376,7 +376,7 @@ freshFnName fn = do idCount <- MS.gets envIdCounter MS.modify' $ (\e -> e {envIdCounter = idCount + 1}) - let prefix = case W4.symFnInfo fn of + let prefix = case W4.symFnInfo fn of W4.UninterpFnInfo{} -> "ufn" W4.DefinedFnInfo{} -> "dfn" W4.MatlabSolverFnInfo{} -> "mfn" @@ -412,7 +412,7 @@ sexp <- go initialExpr case sexp of S.A _ -> return sexp -- Don't memoize atomic s-expressions - that's just silly. - _ -> do + _ -> do letVarName <- addLetBinding key sexp (W4.exprType initialExpr) return $ ident letVarName where go :: W4.Expr t tp -> Memo t SExpr @@ -448,7 +448,7 @@ bvs <- MS.gets envBoundVars -- If this variable is not bound (in the standard syntactic sense) -- and free variables are not explicitly permitted, raise an error. - MS.when ((not $ Set.member (Some x) bvs) && (not fvsAllowed)) $ + M.when ((not $ Set.member (Some x) bvs) && (not fvsAllowed)) $ error $ "encountered the free What4 ExprBoundVar `" ++ (T.unpack (W4.solverSymbolAsText (W4.bvarName x))) @@ -683,7 +683,7 @@ ] -- -- -- -- Helper functions! -- -- -- -- - + goE :: forall tp' . W4.Expr t tp' -> Memo t SExpr goE = convertExpr diff --git a/src/What4/Utils/BVDomain.hs b/src/What4/Utils/BVDomain.hs --- a/src/What4/Utils/BVDomain.hs +++ b/src/What4/Utils/BVDomain.hs @@ -51,6 +51,7 @@ , domainsOverlap , ubounds , sbounds + , isUltSumCommonEquiv , A.arithDomainData , B.bitbounds -- * Operations @@ -424,6 +425,11 @@ sbounds :: (1 <= w) => NatRepr w -> BVDomain w -> (Integer, Integer) sbounds w a = A.sbounds w (asArithDomain a) + +-- | Check if (bvult (bvadd a c) (bvadd b c)) is equivalent to (bvult a b) +isUltSumCommonEquiv :: BVDomain w -> BVDomain w -> BVDomain w -> Bool +isUltSumCommonEquiv a b c = + A.isUltSumCommonEquiv (asArithDomain a) (asArithDomain b) (asArithDomain c) -------------------------------------------------------------------------------- -- Operations diff --git a/src/What4/Utils/BVDomain/Arith.hs b/src/What4/Utils/BVDomain/Arith.hs --- a/src/What4/Utils/BVDomain/Arith.hs +++ b/src/What4/Utils/BVDomain/Arith.hs @@ -11,6 +11,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} @@ -30,6 +31,7 @@ , eq , slt , ult + , isUltSumCommonEquiv , domainsOverlap , arithDomainData , bitbounds @@ -94,6 +96,7 @@ , correct_eq , correct_ult , correct_slt + , correct_isUltSumCommonEquiv , correct_unknowns , correct_bitbounds ) where @@ -276,6 +279,46 @@ (a_min, a_max) = ubounds a (b_min, b_max) = ubounds b +-- | Check if @(bvult (bvadd a c) (bvadd b c))@ is equivalent to @(bvult a b)@. +-- +-- This is true if and only if for all natural values @i_a@, @i_b@, @i_c@ in +-- @a@, @b@, @c@, either both @i_a + i_c@ and @i_b + i_c@ are less than @2^w@, +-- or both are not. We prove this by contradiction. If @i_a = i_b@, then the +-- property is trivial. Assume that @i_a < i_b@. Then @i_a + i_c < i_b + i_c@. +-- If exactly one of the additions is less than @2^w@, it must be the case that +-- @i_a + i_c < 2^w@ and @0 <= i_b + i_c - 2^w < 2^w@. Since @i_b < 2^w@, it +-- follows that @i_b + i_c < 2^w + i_c@, that @i_b + i_c - 2^w < i_c@, and that +-- @i_b + i_c - 2^w < i_a + i_c@. Thus, for these values of @i_a@, @i_b@, @i_c@, +-- @(bvult a b)@ is true, but @(bvult (bvadd a c) (bvadd b c))@ is false, which +-- is a contradiction. +-- +-- We check this property by case analysis on whether @c@ is a single +-- non-wrapping interval, or it wraps around and is a union of two non-wrapping +-- intervals. For a non-wrapping (sub)interval @c'@ of @c@, there are four +-- possible cases: +-- 1. @a@ and @b@ contain a single value. +-- 2. @(bvadd a c')@ and @(bvadd b c')@ do not wrap around for any values in +-- @a@, @b@, @c'@. +-- 3. @(bvadd a c')@ and @(bvadd b c')@ wrap around for all values in @a@, @b@, +-- @c'@. +-- +-- This is used to simplify @bvult@. +isUltSumCommonEquiv :: Domain w -> Domain w -> Domain w -> Bool +isUltSumCommonEquiv a b c = if al == ah && bl == bh && al == bl + then True + else if cl + cw == ch + then checkSameWrapInterval cl ch + else checkSameWrapInterval cl mask && checkSameWrapInterval 0 ch + where + (mask, cl, cw) = case c of + BVDInterval mask' cl' cw' -> (mask', cl', cw') + BVDAny mask' -> (mask', 0, mask') + ch = (cl + cw) .&. mask + (al, ah) = ubounds a + (bl, bh) = ubounds b + checkSameWrapInterval lo hi = + ah + hi <= mask && bh + hi <= mask || mask < al + lo && mask < bl + lo + -------------------------------------------------------------------------------- -- Operations @@ -814,6 +857,18 @@ Just True -> toSigned n x < toSigned n y Just False -> toSigned n x >= toSigned n y Nothing -> True + +correct_isUltSumCommonEquiv :: + (1 <= n) => + NatRepr n -> + (Domain n, Integer) -> + (Domain n, Integer) -> + (Domain n, Integer) -> + Property +correct_isUltSumCommonEquiv n (a, x) (b, y) (c, z) = + member a x ==> member b y ==> member c z ==> + isUltSumCommonEquiv a b c ==> + ((toUnsigned n (x + z) < toUnsigned n (y + z)) == (toUnsigned n x < toUnsigned n y)) correct_unknowns :: (1 <= n) => Domain n -> Integer -> Integer -> Property correct_unknowns a x y = member a x ==> member a y ==> ((x .|. u) == (y .|. u)) && (u .|. mask == mask) diff --git a/test/BVDomTests.hs b/test/BVDomTests.hs --- a/test/BVDomTests.hs +++ b/test/BVDomTests.hs @@ -182,6 +182,9 @@ , genTest "correct_slt" $ do SW n <- genWidth A.correct_slt n <$> A.genPair n <*> A.genPair n + , genTest "correct_isUltSumCommonEquiv" $ + do SW n <- genWidth + A.correct_isUltSumCommonEquiv n <$> A.genPair n <*> A.genPair n <*> A.genPair n , genTest "correct_unknowns" $ do SW n <- genWidth a <- A.genDomain n diff --git a/what4.cabal b/what4.cabal --- a/what4.cabal +++ b/what4.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.4 Name: what4 -Version: 1.4 +Version: 1.5 Author: Galois Inc. Maintainer: rscott@galois.com, kquick@galois.com Copyright: (c) Galois, Inc 2014-2023 @@ -127,7 +127,6 @@ temporary >= 1.2, template-haskell, text >= 1.2.4.0 && < 2.1, - th-abstraction >=0.1 && <0.5, th-lift >= 0.8.2 && < 0.9, th-lift-instances >= 0.1 && < 0.2, time >= 1.8 && < 1.13, @@ -422,7 +421,7 @@ , exceptions , io-streams , lumberjack - , tasty-sugar >= 2.0 && < 2.1 + , tasty-sugar >= 2.0 && < 2.3 , text test-suite what4-serialize-tests