what4 1.4 → 1.5

raw patch · 19 files changed

+143/−28 lines, 19 filesdep −th-abstractiondep ~tasty-sugar

Dependencies removed: th-abstraction

Dependency ranges changed: tasty-sugar

Files

CHANGES.md +11/−0
doc/arithdomain.cry +22/−0
src/What4/Config.hs +2/−2
src/What4/Expr/Builder.hs +8/−0
src/What4/Expr/Simplify.hs +3/−2
src/What4/Expr/VarIdentification.hs +3/−2
src/What4/Expr/WeightedSum.hs +1/−1
src/What4/Partial.hs +1/−1
src/What4/Protocol/SMTLib2.hs +6/−4
src/What4/Protocol/SMTLib2/Parse.hs +2/−1
src/What4/Protocol/SMTWriter.hs +5/−3
src/What4/Protocol/VerilogWriter/AST.hs +3/−1
src/What4/Protocol/VerilogWriter/Backend.hs +2/−1
src/What4/Serialize/Parser.hs +3/−2
src/What4/Serialize/Printer.hs +5/−5
src/What4/Utils/BVDomain.hs +6/−0
src/What4/Utils/BVDomain/Arith.hs +55/−0
test/BVDomTests.hs +3/−0
what4.cabal +2/−3

CHANGES.md view

@@ -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.

doc/arithdomain.cry view

@@ -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

src/What4/Config.hs view

@@ -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(..))

src/What4/Expr/Builder.hs view

@@ -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

src/What4/Expr/Simplify.hs view

@@ -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 ()

src/What4/Expr/VarIdentification.hs view

@@ -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(..))

src/What4/Expr/WeightedSum.hs view

@@ -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

src/What4/Partial.hs view

@@ -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

src/What4/Protocol/SMTLib2.hs view

@@ -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

src/What4/Protocol/SMTLib2/Parse.hs view

@@ -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

src/What4/Protocol/SMTWriter.hs view

@@ -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

src/What4/Protocol/VerilogWriter/AST.hs view

@@ -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

src/What4/Protocol/VerilogWriter/Backend.hs view

@@ -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(..) )

src/What4/Serialize/Parser.hs view

@@ -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 "

src/What4/Serialize/Printer.hs view

@@ -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

src/What4/Utils/BVDomain.hs view

@@ -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

src/What4/Utils/BVDomain/Arith.hs view

@@ -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)

test/BVDomTests.hs view

@@ -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

what4.cabal view

@@ -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