what4 1.7.1.0 → 1.7.2

raw patch · 4 files changed

+67/−6 lines, 4 files

Files

• CHANGES.md +5/−0
• src/What4/Protocol/SMTWriter.hs +24/−5
• test/ExprBuilderSMTLib2.hs +37/−0
• what4.cabal +1/−1

@@ -1,3 +1,8 @@+# 1.7.2 (November 2025)++* Fix a regression in `what4-1.7.1` in which `sbvToInteger` could compute+  incorrect results for symbolic bitvectors.+ # 1.7.1 (November 2025)  * Add `asGround :: IsExpr e => e tp -> Maybe (GroundValue tp)`

@@ -1599,8 +1599,15 @@           -> v           -> v bvIntTerm w x = sumExpr digits- where -- Precondition: 1 <= w. This is upheld by the `1 <= w` constraint in-       -- bvIntTerm's type signature.+ where -- Note that the `1 <= w` constraint in `bvIntTerm`'s type signature is+       -- a slightly stronger assumption that what is needed here. This+       -- definition would also work if `w == 0`, since `[1..natValue w]` would+       -- evaluate to an empty list, producing no digits (as expected). Since+       -- nearly every bitvector-related operation in what4 assumes `1 <= w`,+       -- we include the constraint here as well for consistency.+       --+       -- Contrast this with the definition of `digits` in `sbvIntTerm`, where+       -- the `1 <= w` assumption in crucial.        digits :: [v]        digits = (\i -> digit (i-1)) <$> [1..natValue w] @@ -1611,8 +1618,10 @@  -- @sbvIntTerm w x@ builds an integer term that has the same value as the -- signed integer value of the bitvector @x@. This is done by explicitly--- decomposing the positional notation of the bitvector into a sum of powers of--- 2, plus an offset to ensure that the number is signed appropriately.+-- decomposing the positional notation of the bitvector's @w-1@ least+-- significant bits into a sum of powers of 2, plus an offset (based on whether+-- the most significant bit is set or not) to ensure that the number is signed+-- appropriately. sbvIntTerm :: forall v w             . (SupportTermOps v, 1 <= w)            => NatRepr w@@ -1626,8 +1635,18 @@                           (fromInteger (negate (2^(widthVal w - 1))))                           0 +       -- Note that unlike the corresponding `digits` value in `bvIntTerm`,+       -- this `digits` value only takes the @w-1@ least significant bits of+       -- `x` into consideration, as the most significant bit is used to+       -- compute `signedOffset` instead.+       --+       -- NB: If `w == 1`, then `[1..(natValue w - 1)]` will evaluate to an+       -- empty list, producing no digits (as expected).+       --+       -- Precondition: 1 <= w. This is upheld by the `1 <= w` constraint in+       -- sbvIntTerm's type signature.        digits :: [v]-       digits = (\i -> digit (i-1)) <$> [1..natValue w]+       digits = (\i -> digit (i-1)) <$> [1..(natValue w - 1)]         digit :: SupportTermOps v => Natural -> v        digit d = ite (bvTestBit w d x)

@@ -1114,6 +1114,40 @@        _ -> fail "expected satisfible model" +-- | A regression test for #329.+issue329Test ::+  OnlineSolver solver =>+  SimpleExprBuilder t fs ->+  SolverProcess t solver ->+  IO ()+issue329Test sym solver = do+    -- This test shows that the following proposition (written in Cryptol) is+    -- falsifiable when `x == 2`:+    --+    --   \(x : [2]) -> x == 2 ==> ((toSignedInteger x - 1) == -1)+    let w = knownNat @2+    x <- freshConstant sym (safeSymbol "x") (BaseBVRepr w)+    bvTwo <- bvLit sym w (BV.mkBV w 2)+    xEqBvTwo <- bvEq sym x bvTwo+    notXEqBvTwo <- notPred sym xEqBvTwo+    xsi <- sbvToInteger sym x+    intOne <- intLit sym 1+    intNegOne <- intLit sym (-1)+    xsiDec <- intSub sym xsi intOne+    xsiDecEqIntNegOne <- intEq sym xsiDec intNegOne+    p <- orPred sym notXEqBvTwo xsiDecEqIntNegOne++    -- Check if `p` is not valid for all `x` by checking if its negation+    -- (`notP`) is satisfiable. If `notP` is satisfiable, then we have found a+    -- counterexample to `p`.+    notP <- notPred sym p+    checkSatisfiableWithModel solver "test" notP $ \case+      Sat fn ->+        do xEval <- groundEval fn x+           (xEval == BV.mkBV w 2) @? "result other than 2"++      _ -> fail "expected satisfible model"+ -- | These tests simply ensure that no exceptions are raised. testSolverInfo :: TestTree testSolverInfo = testGroup "solver info queries" $@@ -1277,6 +1311,7 @@          , testCase "Z3 #182 test case" $ withOnlineZ3 issue182Test         , testCase "Z3 #315 test case" $ withOnlineZ3 issue315Test+        , testCase "Z3 #329 test case" $ withOnlineZ3 issue329Test          , arrayCopyTest         , arraySetTest@@ -1328,6 +1363,7 @@          , cvcTestCase "#182 test case" $ withCVC issue182Test         , cvcTestCase "#315 test case" $ withCVC issue315Test+        , cvcTestCase "#329 test case" $ withCVC issue329Test         ]   let cvc4Tests = cvcTests CVC4   let cvc5Tests = cvcTests CVC5@@ -1342,6 +1378,7 @@         , testCase "Yices rounding" $ withYices roundingTest         , testCase "Yices #182 test case" $ withYices issue182Test         , testCase "Yices #315 test case" $ withYices issue315Test+        , testCase "Yices #329 test case" $ withYices issue329Test         ]   let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id                             else fmap (ignoreTestBecause (nm <> " not present"))

@@ -1,6 +1,6 @@ Cabal-version: 2.4 Name:          what4-Version:       1.7.1.0+Version:       1.7.2 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com Copyright:     (c) Galois, Inc 2014-2023