what4 1.7.3 → 1.8

raw patch · 49 files changed

+1276/−4712 lines, 49 filesdep +microlensdep +microlens-mtldep +microlens-thdep −QuickCheckdep −lensdep −tasty-quickcheckdep ~basedep ~hashabledep ~hedgehogPVP ok

version bump matches the API change (PVP)

Dependencies added: microlens, microlens-mtl, microlens-th, what4-domains

Dependencies removed: QuickCheck, lens, tasty-quickcheck

Dependency ranges changed: base, hashable, hedgehog, parameterized-utils, tasty, tasty-hedgehog, transformers

API changes (from Hackage documentation)

Files

• CHANGES.md +41/−0
• doc/README.md +0/−23
• doc/arithdomain.cry +0/−723
• doc/bitsdomain.cry +0/−284
• doc/bvdomain.cry +0/−287
• doc/xordomain.cry +0/−53
• src/Test/Verification.hs +4/−199
• src/What4/Config.hs +5/−3
• src/What4/Expr/Allocator.hs +1/−1
• src/What4/Expr/App.hs +90/−10
• src/What4/Expr/BoolMap.hs +16/−6
• src/What4/Expr/Builder.hs +27/−13
• src/What4/Expr/GroundEval.hs +1/−1
• src/What4/Expr/Simplify.hs +1/−1
• src/What4/Expr/UnaryBV.hs +3/−3
• src/What4/Expr/VarIdentification.hs +8/−7
• src/What4/Expr/WeightedSum.hs +102/−23
• src/What4/Interface.hs +136/−6
• src/What4/LabeledPred.hs +4/−3
• src/What4/Partial.hs +1/−1
• src/What4/ProgramLoc.hs +1/−1
• src/What4/Protocol/Online.hs +2/−1
• src/What4/Protocol/PolyRoot.hs +1/−1
• src/What4/Protocol/ReadDecimal.hs +1/−1
• src/What4/Protocol/SExp.hs +8/−1
• src/What4/Protocol/SMTLib2/Syntax.hs +1/−2
• src/What4/Protocol/SMTWriter.hs +61/−19
• src/What4/SFloat.hs +162/−9
• src/What4/Solver/DReal.hs +1/−1
• src/What4/Solver/Yices.hs +5/−1
• src/What4/Utils/AbstractDomains.hs +4/−4
• src/What4/Utils/AnnotatedMap.hs +5/−2
• src/What4/Utils/Arithmetic.hs +40/−14
• src/What4/Utils/BVDomain.hs +3/−878
• src/What4/Utils/BVDomain/Arith.hs +3/−882
• src/What4/Utils/BVDomain/Bitwise.hs +3/−447
• src/What4/Utils/BVDomain/XOR.hs +3/−190
• src/What4/Utils/Endian.hs +1/−1
• src/What4/Utils/FloatHelpers.hs +2/−1
• src/What4/Utils/ResolveBounds/BV.hs +1/−1
• test/AdapterTest.hs +1/−1
• test/BVDomTests.hs +0/−497
• test/ExprBuilderSMTLib2.hs +123/−2
• test/ExprsTest.hs +2/−0
• test/HH/VerifyBindings.hs +0/−36
• test/OnlineSolverTest.hs +148/−1
• test/QC/VerifyBindings.hs +0/−35
• test/WeightedSum.hs +241/−0
• what4.cabal +13/−36

@@ -1,3 +1,44 @@+# 1.8 -- 2026-09-01++* The `What4.Utils.BVDomain`, `What4.Utils.BVDomain.Arith`,+  `What4.Utils.BVDomain.Bitwise`, and `What4.Utils.BVDomain.XOR` modules have+  moved to the new `what4-domains` package as `What4.Domains.BV`,+  `What4.Domains.BV.Arith`, `What4.Domains.BV.Bitwise`, and+  `What4.Domains.BV.XOR`, respectively. The old names are deprecated+  re-exports and will be removed in a future release.+* `Test.Verification` has moved to `what4-domains` as+  `What4.Domains.Verification`. The old name is a deprecated re-export.+* Deprecate `What4.Utils.Endian`, use `Data.Parameterized.Utils.Endian` instead.+* Fix a bug where persistent side conditions (e.g., @Nat >= 0@ constraints)+  were lost after @reset-assertions@. These constraints are now properly+  re-asserted after reset. This fix ensures that variables cached with+  @DeleteNever@ maintain their necessary constraints across solver resets.+* What4 now gives a proper error message when preparing to send a query to+  Bitwuzla involving the `floatToReal` operation (which Bitwuzla does not+  support) instead of throwing a parse exception.+* Replace `lens` with `microlens-{,-mtl,-th}`.+* Fix a bug where `what4` could produce incorrect models involving the+  `floatToBV` operation when using the `RNA` rounding mode.+* Fix a bug where `what4` could produce incorrect models involving the `bvSDiv`+  operation.+* Add `bvUdivSmtlib`, `bvUremSmtlib`, `bvSdivSmtlib`, and `bvSremSmtlib` to+  `IsExprBuilder`. These mirror the existing `bv{U,S}{Div,Rem}` operations+  but follow the SMT-LIB-specified div-by-zero semantics+  (`bvudiv s 0 = ~0`, `bvurem s 0 = s`, `bvsdiv s 0 = if s < 0 then 1 else ~0`,+  `bvsrem s 0 = s`). See Note `[SMT-LIB division]` in `What4.Interface`.+* Add `fpNegZero`, `fpPosZero`, `fpRem`, `fpNe`, `fpNeIEEE`, `fpLeIEEE`,+  `fpGeIEEE`, `fpIsPos`, `fpCast`, `fpFromBV`, `fpFromSBV`, `fpToBV`, and+  `fpToSBV` to `What4.SFloat`.+* Fix a bug in which `fpToRational` could return an invalid rational number+  with a zero denominator.+* Fix a bug in which calling `solver_adapter_write_smt2 yicesAdapter` would+  always fail.+* Fix a bug in which `baseIsConcrete` would incorrectly claim that concrete+  `SymFloat`s are not concrete.+* Calling `iFloatRound` with the `RNE` rounding mode when using the `FloatReal`+  interpretation now dispatches to `realRoundEven` instead of throwing an+  error.+ # 1.7.3 -- 2026-01-26  * Fix a bug in which `what4`'s Bitwuzla adapter would generate invalid code

@@ -1,23 +0,0 @@-# Bitvector Abstract Domain Formalization--The module `What4.Utils.BVDomain` implements an abstract domain for-sized bitvectors, using an interval-based representation. Many of the-algorithms in this module are subtle and not obviously correct.--To increase confidence in the correctness of that code, the file-`bvdomain.cry` in this directory contains a formalization of those-algorithms in Cryptol (<https://cryptol.net>).--Use the following command to prove all of the correctness properties-in the Cryptol specification using the z3 prover:--    cryptol bvdomain.cry -c :prove--NOTE: This verification only asserts the correctness of the Cryptol-specification, not of the actual Haskell implementation; the-correspondence between the Haskell and Cryptol versions must be-checked by manual inspection. Keep in mind that the Haskell version-uses the unbounded `Integer` type throughout, and uses bitwise masking-to reduce modulo 2^n; on the other hand, the Cryptol code uses-fixed-width bitvector types where this masking is implicit. Otherwise-the structure of the code is very similar.

@@ -1,723 +0,0 @@-/*--This file contains a Cryptol implementation of the arithmetic-bitvector abstract domain operations from module What4.Utils.Domain in what4.--In addition to the algorithms themselves, this file also contains-specifications of correctness for each of the operations. All of the-correctness properties can be formally proven (each at some specific-bit width) by loading this file in cryptol and entering ":prove".--*/-module arithdomain where--////////////////////////////////////////////////////////////-// Library--bit : {i, n} (fin n, n > i) => [n]-bit = 1 # (0 : [i])--mask : {i, n} (fin n, n >= i) => [n]-mask = 0 # (~ 0 : [i])--/** Checked unsigned addition, asserted not to overflow. */-infixl 80 .+.-(.+.) : {n} (fin n) => [n] -> [n] -> [n]-x .+. y = if carry x y then error "overflow" else x + y--/** Checked unsigned subtraction, asserted not to underflow. */-infixl 80 .-.-(.-.) : {n} (fin n) => [n] -> [n] -> [n]-x .-. y = if x < y then error "underflow" else x - y--/** Minimum of two signed values. */-smin : {a} (SignedCmp a) => a -> a -> a-smin x y = if x <$ y then x else y--/** Maximum of two signed values. */-smax : {a} (SignedCmp a) => a -> a -> a-smax x y = if x >$ y then x else y--////////////////////////////////////////////////////////////--type Dom n = { lo : [n], sz : [n] }--interval : {n} (fin n) => [n] -> [n] -> Dom n-interval l s = { lo = l, sz = s }--range : {n} (fin n) => [n] -> [n] -> Dom n-range lo hi = interval lo (hi - lo)--/** Membership predicate that defines the set of concrete values-represented by an abstract domain element. */-mem : {n} (fin n) => Dom n -> [n] -> Bit-mem a x = x - a.lo <= a.sz--umem : {n} (fin n) => ([n], [n]) -> [n] -> Bit-umem (lo, hi) x = lo <= x /\ x <= hi--smem : {n} (fin n, n >= 1) => ([n], [n]) -> [n] -> Bit-smem (lo, hi) x = lo <=$ x /\ x <=$ hi--top : {n} (fin n) => Dom n-top = interval 0 (~ 0)--singleton : {n} (fin n) => [n] -> Dom n-singleton x = interval x 0--isSingleton : {n} (fin n) => Dom n -> Bit-isSingleton a = a.sz == 0--ubounds : {n} (fin n) => Dom n -> ([n], [n])-ubounds a =-  if carry a.lo a.sz then (0, ~0) else (a.lo, a.lo + a.sz)--sbounds : {n} (fin n, n >= 1) => Dom n -> ([n], [n])-sbounds a = (lo - delta, hi - delta)-  where-    delta = reverse 1-    (lo, hi) = ubounds (interval (a.lo + delta) a.sz)--/** Nonzero signed values in a domain with the least and greatest-reciprocals. Note that this coincides with the greatest and least-nonzero values using the unsigned ordering. */-rbounds : {n} (fin n, n >= 1) => Dom n -> ([n], [n])-rbounds a =-  if a.lo == 0 then (a_hi, 1) else-  if a_hi == 0 then (-1, a.lo) else-  if a_hi < a.lo then (-1, 1) else-  (a_hi, a.lo)-  where a_hi = a.lo + a.sz--overlap : {n} (fin n) => Dom n -> Dom n -> Bit-overlap a b = diff <= b.sz \/ carry diff a.sz-  where diff = a.lo - b.lo--// To compute the union of two intervals, we choose representatives of-// the endpoints modulo 2^n such that their midpoints are no more than-// 2^(n-1) apart. In the code below, am and bm are equal to twice the-// midpoints of intervals a and b, respectively.-union : {n} (fin n) => Dom n -> Dom n -> Dom n-union a b =-  if cw >= size then top else interval (drop`{2} cl) (drop`{2} cw)-  where-    size : [n+2]-    size = bit`{n}-    am = 2 * zext a.lo .+. zext a.sz-    bm = 2 * zext b.lo .+. zext b.sz-    al' = if am .+. size < bm then zext a.lo .+. size else zext a.lo-    bl' = if bm .+. size < am then zext b.lo .+. size else zext b.lo-    ah' = al' .+. zext a.sz-    bh' = bl' .+. zext b.sz-    cl = min al' bl'-    ch = max ah' bh'-    cw = ch .-. cl--////////////////////////////////////////////////////////////--zero_ext : {m, n} (fin m, m >= n) => Dom n -> Dom m-zero_ext a = interval (zext lo) (zext (hi .-. lo))-  where (lo, hi) = ubounds a--sign_ext : {m, n} (fin m, m >= n, n >= 1) => Dom n -> Dom m-sign_ext a = interval (sext lo) (zext (hi - lo))-  where (lo, hi) = sbounds a--concat : {m, n} (fin m, fin n) => Dom m -> Dom n -> Dom (m + n)-concat a b = interval (a.lo # lo) (a.sz # sz)-  where-    (lo, hi) = ubounds b-    sz = hi .-. lo--shrink : {m, n} (fin m, fin n) => Dom (m + n) -> Dom m-shrink a =-  if b_sz >= size then top-  else interval (tail b_lo) (tail b_sz)-  where-    size : [1 + m]-    size = bit`{m}-    b_lo, b_hi, b_sz : [1 + m]-    b_lo = take`{back=n} (zext a.lo)-    b_hi = take`{back=n} (zext a.lo .+. zext a.sz)-    b_sz = b_hi .-. b_lo--trunc : {m, n} (fin m, fin n) => Dom (m + n) -> Dom n-trunc a =-  if a.sz > mask`{n} then top-  else interval (drop`{m} a.lo) (drop`{m} a.sz)--////////////////////////////////////////////////////////////-// Arithmetic operations--add : {n} (fin n) => Dom n -> Dom n -> Dom n-add a b =-  if carry a.sz b.sz then top-  else interval (a.lo + b.lo) (a.sz .+. b.sz)--neg : {n} (fin n) => Dom n -> Dom n-neg a = interval (- (a.lo + a.sz)) a.sz--// Turns out, bitwise complement is easy to specify-// in this domain also-bnot : {n} (fin n) => Dom n -> Dom n-bnot a = interval (~ ah) a.sz-  where ah = a.lo + a.sz--mul : {n} (fin n) => Dom n -> Dom n -> Dom n-mul a b =-  if sz >= bit`{n} then top-  else interval (drop lo) (drop sz)-  where-    (lo, hi) = mulRange (zbounds a) (zbounds b)-    sz = hi - lo--zbounds : {n} (fin n) => Dom n -> ([1 + n], [1 + n])-zbounds a = (lo', lo' + zext a.sz)-  where-    size : [2 + n]-    size = bit`{n}-    lo' = if 2 * zext a.lo .+. zext a.sz >= size then 0b1 # a.lo else 0b0 # a.lo--mulRange : {m, n} (fin m, fin n, m >= 1, n >= 1) => ([m], [m]) -> ([n], [n]) -> ([m+n], [m+n])-mulRange (xl, xh) (yl, yh) = (zl, zh)-  where-    (xlyl, xlyh) = scaleRange xl (yl, yh)-    (xhyl, xhyh) = scaleRange xh (yl, yh)-    zl = smin xlyl xhyl-    zh = smax xlyh xhyh--scaleRange : {m, n} (fin m, fin n, m >= 1, n >= 1) => [m] -> ([n], [n]) -> ([m+n], [m+n])-scaleRange k (lo, hi) = if k <$ 0 then (hi', lo') else (lo', hi')-  where-    lo' = sext k * sext lo-    hi' = sext k * sext hi--udiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n-udiv a b = range cl ch-  where-    (al, ah) = ubounds a-    (bl, bh) = ubounds b-    bl' = max 1 bl // assume that division by 0 does not happen-    bh' = max 1 bh // assume that division by 0 does not happen-    cl = al / bh'-    ch = ah / bl'--urem : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n-urem a b =-  if ql == qh then range rl rh-  else interval 0 (bh - 1)-  where-    (al, ah) = ubounds a-    (bl, bh) = ubounds b-    bl' = max 1 bl // assume that division by 0 does not happen-    bh' = max 1 bh-    (ql, rl) = (al / bh', al % bh')-    (qh, rh) = (ah / bl', ah % bl')--// The first argument is an ordinary signed interval, but the second-// argument is a reciaprocal interval: The arguments should satisfy 'al-// <=$ ah' (signed) and '1/bl <= 1/bh' (signed), or equivalently, 'bh-// <= bl' (unsigned).-sdivRange : {n} (fin n, n >= 1) => ([n], [n]) -> ([n], [n]) -> ([1+n], [1+n])-sdivRange (al, ah) (bl, bh) = (ql, qh)-  where-    (ql1, qh1) = shrinkRange (al, ah) bh-    (ql2, qh2) = shrinkRange (al, ah) bl-    ql = smin ql1 ql2-    qh = smax qh1 qh2--// Extra bit of output is to handle the 'INTMIN / -1' overflow case.-shrinkRange : {n} (fin n, n >= 1) => ([n], [n]) -> [n] -> ([1+n], [1+n])-shrinkRange (lo, hi) k =-  if k >$ 0 then (lo ./. k, hi ./. k) else-  if k <$ 0 then (hi ./. k, lo ./. k) else (sext lo, sext hi)-  where-    x ./. y = sext x /$ sext y--sdiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n-sdiv a b =-  if sz >= bit`{n} then top-  else interval (drop lo) (drop sz)-  where-    (lo, hi) = sdivRange (sbounds a) (rbounds b)-    sz = hi - lo--srem : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n-srem a b =-  if ql == qh then-    (if ql <$ 0-     then range (al - drop ql * bl) (ah - drop ql * bh)-     else range (al - drop ql * bh) (ah - drop ql * bl))-  else range rl rh-  where-    (al, ah) = sbounds a-    (bl, bh) = sbounds b-    (ql, qh) = sdivRange (al, ah) (rbounds b)-    rl = if al <$ 0 then smin (bl+1) (-bh+1) else 0-    rh = if ah >$ 0 then smax (-bl-1) (bh-1) else 0--////////////////////////////////////////////////////////////-// Shifts--shl : {n} (fin n) => Dom n -> Dom n -> Dom n-shl a b =-  if sz > mask`{n} then top-  else interval (drop lo) (drop sz)-  where-    al, ah : [n + 1]-    (al, ah) = zbounds a-    bl, bh : [n]-    (bl, bh) = ubounds b-    // [n + 2] is enough to avoid signed overflow in shift-    cl, ch : [n + 2]-    cl = if bl < `n then 1 << bl else bit`{n}-    ch = if bh < `n then 1 << bh else bit`{n}-    (lo, hi) = mulRange (al, ah) (cl, ch)-    sz = hi - lo--lshr : {n} (fin n) => Dom n -> Dom n -> Dom n-lshr a b = interval cl (ch - cl)-  where-    (al, ah) = ubounds a-    (bl, bh) = ubounds b-    cl = al >> bh-    ch = ah >> bl--ashr : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n-ashr a b = interval cl (ch - cl)-  where-    (al, ah) = sbounds a-    (bl, bh) = ubounds b-    cl = al >>$ (if al <$ 0 then bl else bh)-    ch = ah >>$ (if ah <$ 0 then bh else bl)--////////////////////////////////////////////////////////////-// Comparisons--ult : {n} (fin n) => Dom n -> Dom n -> Bit-ult a b = (ubounds a).1 < (ubounds b).0--ule : {n} (fin n) => Dom n -> Dom n -> Bit-ule a b = (ubounds a).1 <= (ubounds b).0--slt : {n} (fin n, n >= 1) => Dom n -> Dom n -> Bit-slt a b = (sbounds a).1 <$ (sbounds b).0--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]-unknowns a = if carry a.lo a.sz then ~0 else bits- where- bits = fillright diff- diff = a.lo ^ (a.lo + a.sz)--fillright : {n} (fin n, n >= 1) => [n] -> [n]-fillright x = tail (scanl (||) False x)--fillright_alt : {n} (fin n, n >= 1) => [n] -> [n]-fillright_alt x = x || ((1 << lg2 x) - 1)--property fillright_equiv x = fillright`{16} x == fillright_alt x--////////////////////////////////////////////////////////////---///////////////////////////////////////////////////////////-// Correctness properties--infix 20 =@=--/** Equivalence of bitvector domains. */-(=@=) : {n} (fin n) => Dom n -> Dom n -> Bit-a =@= b = (a.sz == ~0 /\ b.sz == ~0) \/ (a == b)--infix 5 <==>--(<==>) : Bit -> Bit -> Bit-(<==>) = (==)--////////////////////////////////////////////////////////////-// Soundness properties--correct_top : {n} (fin n) => [n] -> Bit-correct_top x = mem top x--correct_ubounds : {n} (fin n) => Dom n -> [n] -> Bit-correct_ubounds a x =-  mem a x ==> umem (ubounds a) x--correct_sbounds : {n} (fin n, n >= 1) => Dom n -> [n] -> Bit-correct_sbounds a x =-  mem a x ==> smem (sbounds a) x--correct_singleton : {n} (fin n) => [n] -> [n] -> Bit-correct_singleton x y =-  mem (singleton x) y <==> x == y--correct_overlap : {n} (fin n) => Dom n -> Dom n -> [n] -> Bit-correct_overlap a b x =-  mem a x ==> mem b x ==> overlap a b--correct_overlap_inv : {n} (fin n) => Dom n -> Dom n -> Bit-correct_overlap_inv a b =-  overlap a b ==> (mem a witness /\ mem b witness)-- where- witness = if mem a b.lo then b.lo else a.lo--correct_union : {n} (fin n) => Dom n -> Dom n -> [n] -> Bit-correct_union a b x =-  (mem a x \/ mem b x) ==> mem (union a b) x--correct_zero_ext : {m, n} (fin m, m >= n) => Dom n -> [n] -> Bit-correct_zero_ext a x =-  mem a x ==> mem (zero_ext`{m} a) (zext`{m} x)--correct_sign_ext : {m, n} (fin m, m >= n, n >= 1) => Dom n -> [n] -> Bit-correct_sign_ext a x =-  mem a x ==> mem (sign_ext`{m} a) (sext`{m} x)--correct_concat : {m, n} (fin m, fin n) => Dom m -> Dom n -> [m] -> [n] -> Bit-correct_concat a b x y =-  mem a x ==> mem b y ==> mem (concat a b) (x # y)--correct_shrink : {m, n} (fin m, fin n) => Dom (m + n) -> [m + n] -> Bit-correct_shrink a x =-  mem a x ==> mem (shrink`{m} a) (take`{m} x)--correct_trunc : {m, n} (fin m, fin n) => Dom (m + n) -> [m + n] -> Bit-correct_trunc a x =-  mem a x ==> mem (trunc`{m} a) (drop`{m} x)--correct_add : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_add a b x y =-  mem a x ==> mem b y ==> mem (add a b) (x + y)--correct_neg : {n} (fin n) => Dom n -> [n] -> Bit-correct_neg a x =-  mem a x <==> mem (neg a) (- x)--correct_mul : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_mul a b x y =-  mem a x ==> mem b y ==> mem (mul a b) (x * y)--correct_mulRange : {n} (fin n, n >= 1) => ([n], [n]) -> ([n], [n]) -> [n] -> [n] -> Bit-correct_mulRange a b x y =-  smem a x ==> smem b y ==> smem (mulRange a b) (sext x * sext y)--correct_udiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_udiv a b x y =-  mem a x ==> mem b y ==> y != 0 ==> mem (udiv a b) (x / y)--correct_urem : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_urem a b x y =-  mem a x ==> mem b y ==> y != 0 ==> mem (urem a b) (x % y)--correct_sdivRange : {n} (fin n, n >= 1) => ([n], [n]) -> ([n], [n]) -> [n] -> [n] -> Bit-correct_sdivRange a b x y =-  smem a x ==> umem b y ==> y != 0 ==> smem (sdivRange a (b.1, b.0)) (sext x /$ sext y)--correct_shrinkRange : {n} (fin n, n >= 1) => ([n], [n]) -> [n] -> [n] -> Bit-correct_shrinkRange a x y =-  smem a x ==> y != 0 ==> smem (shrinkRange a y) (sext x /$ sext y)--correct_sdiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_sdiv a b x y =-  mem a x ==> mem b y ==> y != 0 ==> mem (sdiv a b) (x /$ y)--correct_srem : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_srem a b x y =-  mem a x ==> mem b y ==> y != 0 ==> mem (srem a b) (x %$ y)--correct_shl : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_shl a b x y =-  mem a x ==> mem b y ==> mem (shl a b) (x << y)--correct_lshr : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_lshr a b x y =-  mem a x ==> mem b y ==> mem (lshr a b) (x >> y)--correct_ashr : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_ashr a b x y =-  mem a x ==> mem b y ==> mem (ashr a b) (x >>$ y)--correct_slt : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_slt a b x y =-  slt a b ==> mem a x ==> mem b y ==> x <$ y--correct_sle : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_sle a b x y =-  sle a b ==> mem a x ==> mem b y ==> x <=$ y--correct_ult : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_ult a b x y =-  ult a b ==> mem a x ==> mem b y ==> x < y--correct_ule : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit-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)--correct_isSingleton : {n} (fin n) => Dom n -> Bit-correct_isSingleton a =-  isSingleton a ==> a == singleton a.lo--correct_unknowns : {n} (fin n, n >= 1) => Dom n -> [n] -> [n] -> Bit-correct_unknowns a x y =-  mem a x ==> mem a y ==> (x || unknowns a) == (y || unknowns a)--property p1 = correct_top`{16}-property p2 = correct_ubounds`{16}-property p3 = correct_sbounds`{16}-property p4 = correct_singleton`{16}-property p5 = correct_overlap`{16}-property p5_inv = correct_overlap_inv`{16}-property p6 = correct_union`{8}-property p7 = correct_zero_ext`{32, 16}-property p8 = correct_sign_ext`{32, 16}-property p9 = correct_concat`{16, 16}-property p10 = correct_shrink`{8, 8}-property p11 = correct_trunc`{8, 8}-property p12 = correct_unknowns`{16}-property p13 = correct_isSingleton`{16}--property a1 = correct_add`{8}-property a2 = correct_neg`{16}-property a3 = correct_mul`{4}-property a4 = correct_udiv`{8}-property a5 = correct_urem`{6}-property a6 = correct_sdiv`{6}-property a7 = correct_srem`{6}-property a8 = correct_bnot`{16}-property a9 = correct_sdivRange`{6}--property s1 = correct_shl`{8}-property s2 = correct_lshr`{8}-property s3 = correct_ashr`{8}--property o1 = correct_slt`{16}-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--singleton_overlap : {n} (fin n) => [n] -> [n] -> Bit-singleton_overlap x y =-  overlap (singleton x) (singleton y) == (x == y)--singleton_zero_ext : {m, n} (fin m, m >= n) => [n] -> Bit-singleton_zero_ext x =-  zero_ext`{m} (singleton x) == singleton (zext`{m} x)--singleton_sign_ext : {m, n} (fin m, m >= n, n >= 1) => [n] -> Bit-singleton_sign_ext x =-  sign_ext`{m} (singleton x) == singleton (sext`{m} x)--singleton_concat : {m, n} (fin m, fin n) => [m] -> [n] -> Bit-singleton_concat x y =-  concat (singleton x) (singleton y) == singleton (x # y)--singleton_shrink : {m, n} (fin m, fin n) => [m + n] -> Bit-singleton_shrink x =-  shrink`{m} (singleton x) == singleton (take`{m} x)--singleton_trunc : {m, n} (fin m, fin n) => [m + n] -> Bit-singleton_trunc x =-  trunc`{m} (singleton x) == singleton (drop`{m} x)--singleton_add : {n} (fin n) => [n] -> [n] -> Bit-singleton_add x y =-  add (singleton x) (singleton y) == singleton (x + y)--singleton_neg : {n} (fin n) => [n] -> Bit-singleton_neg x =-  neg (singleton x) == singleton (- x)--singleton_mul : {n} (fin n) => [n] -> [n] -> Bit-singleton_mul x y =-  mul (singleton x) (singleton y) == singleton (x * y)--singleton_mulRange : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_mulRange x y =-  mulRange (x, x) (y, y) == (sext x * sext y, sext x * sext y)--singleton_udiv : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_udiv x y =-  y != 0 ==> udiv (singleton x) (singleton y) == singleton (x / y)--singleton_urem : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_urem x y =-  y != 0 ==> urem (singleton x) (singleton y) == singleton (x % y)--singleton_sdiv : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_sdiv x y =-  y != 0 ==> sdiv (singleton x) (singleton y) == singleton (x /$ y)--singleton_srem : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_srem x y =-  y != 0 ==> srem (singleton x) (singleton y) == singleton (x %$ y)--singleton_shl : {n} (fin n) => [n] -> [n] -> Bit-singleton_shl x y =-  shl (singleton x) (singleton y) == singleton (x << y)--singleton_lshr : {n} (fin n) => [n] -> [n] -> Bit-singleton_lshr x y =-  lshr (singleton x) (singleton y) == singleton (x >> y)--singleton_ashr : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_ashr x y =-  ashr (singleton x) (singleton y) == singleton (x >>$ y)--singleton_slt : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_slt x y =-  slt (singleton x) (singleton y) == (x <$ y)--singleton_sle : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_sle x y =-  sle (singleton x) (singleton y) == (x <=$ y)--singleton_ult : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_ult x y =-  ult (singleton x) (singleton y) == (x < y)--singleton_ule : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_ule x y =-  ule (singleton x) (singleton y) == (x <= y)--property i01 = singleton_overlap`{16}-property i02 = singleton_zero_ext`{32, 16}-property i03 = singleton_sign_ext`{32, 16}-property i04 = singleton_concat`{16, 16}-property i05 = singleton_shrink`{8, 8}-property i06 = singleton_trunc`{8, 8}-property i07 = singleton_add`{8}-property i08 = singleton_neg`{16}-property i09 = singleton_mul`{4}-property i10 = singleton_udiv`{8}-property i11 = singleton_urem`{8}-property i12 = singleton_sdiv`{8}-property i13 = singleton_srem`{8}-property i14 = singleton_shl`{8}-property i15 = singleton_lshr`{8}-property i16 = singleton_ashr`{8}-property i17 = singleton_slt`{16}-property i18 = singleton_sle`{16}-property i19 = singleton_ult`{16}-property i20 = singleton_ule`{16}--////////////////////////////////////////////////////////////-// Associativity/commutativity properties--comm_overlap : {n} (fin n) => Dom n -> Dom n -> Bit-comm_overlap a b = overlap a b <==> overlap b a--comm_add : {n} (fin n) => Dom n -> Dom n -> Bit-comm_add a b = add a b == add b a--assoc_add : {n} (fin n) => Dom n -> Dom n -> Dom n -> Bit-assoc_add a b c = add a (add b c) =@= add (add a b) c--comm_mul : {n} (fin n) => Dom n -> Dom n -> Bit-comm_mul a b = mul a b == mul b a--/* mul is not associative! */-assoc_mul : {n} (fin n) => Dom n -> Dom n -> Dom n -> Bit-assoc_mul a b c = mul a (mul b c) =@= mul (mul a b) c--comm_mulRange :-  {i, j} (fin i, fin j, i >= 1, j >= 1) => ([i], [i]) -> ([j], [j]) -> Bit-comm_mulRange a b =-  a.0 <=$ a.1 ==> b.0 <=$ b.1 ==> mulRange a b == mulRange b a--assoc_mulRange :-  {i, j, k} (fin i, fin j, fin k, i >= 1, j >= 1, k >= 1) =>-  ([i], [i]) -> ([j], [j]) -> ([k], [k]) -> Bit-assoc_mulRange a b c =-  a.0 <=$ a.1 ==>-  b.0 <=$ b.1 ==>-  c.0 <=$ c.1 ==>-  mulRange a (mulRange b c) == mulRange (mulRange a b) c--property c1 = comm_overlap`{16}-property c2 = comm_add`{16}-property c3 = assoc_add`{16}-property c4 = comm_mul`{4}-property c5 = comm_mulRange`{4,4}-property c6 = assoc_mulRange`{3,3,3}--////////////////////////////////////////////////////////////-// Additional properties about union--comm_union : {n} (fin n) => Dom n -> Dom n -> Bit-comm_union a b = union a b == union b a--/* union is actually not associative! */-assoc_union : {n} (fin n) => Dom n -> Dom n -> Dom n -> Bit-assoc_union a b c = union a (union b c) == union (union a b) c--/* union always has a lower bound equal to one of the input lower bounds */-lo_union : {n} (fin n) => Dom n -> Dom n -> Bit-lo_union a b =-  union a b == top \/ (union a b).lo == a.lo \/ (union a b).lo == b.lo--/* union always has an upper bound equal to one of the input upper bounds */-hi_union : {n} (fin n) => Dom n -> Dom n -> Bit-hi_union a b = c == top \/ c_hi == a_hi \/ c_hi == b_hi-  where-    c = union a b-    a_hi = a.lo + a.sz-    b_hi = b.lo + b.sz-    c_hi = c.lo + c.sz--/* union doesn't return top unless necessary */-nontriv_union : {n} (fin n) => Dom n -> Dom n -> [n] -> Bit-nontriv_union a b x =-  union a b =@= top ==> mem a x \/ mem b x--/* union of opposite intervals prefers to exclude zero */-nonzero_union : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-nonzero_union lo sz =-  mem (union a b) half /\-  (~ mem a 0 ==> ~ mem b 0 ==> ~ mem (union a b) 0)-  where-    half : [n]-    half = reverse 1-    a = interval lo sz-    b = interval (lo + half) sz--property u1 = comm_union`{16}-property u2 = lo_union`{16}-property u3 = hi_union`{16}-property u4 = nontriv_union`{8}-property u5 = nonzero_union`{16}

@@ -1,284 +0,0 @@-/*--This file contains a Cryptol implementation of the bitwise-bitvector abstract domain operations from What4.Utils.BVDomain--In addition to the algorithms themselves, this file also contains-specifications of correctness for each of the operations. All of the-correctness properties can be formally proven (each at some specific-bit width) by loading this file in cryptol and entering ":prove".--*/-module bitsdomain where--// This type represents _bitwise_ bounds as opposed to the-// arithmetic bounds described by BVDom.  Note that-// this representation allows the empty set if-// lomask is not bitwise below himask.  However, all-// the operations (other than intersection) preserve the property-// of being nonempty (implied by their various soundness properties).-type Dom n = { lomask : [n] , himask : [n] }--/** Membership predicate that defines the set of concrete values-represented by a bitwise abstract domain element. */-mem : {n} (fin n) => Dom n -> [n] -> Bit-mem a x = bitle a.lomask x /\ bitle x a.himask--bitle : {n} (fin n) => [n] -> [n] -> Bit-bitle x y = x || y == y--nonempty : {n} (fin n) => Dom n -> Bit-nonempty b = bitle b.lomask b.himask--singleton : {n} (fin n) => [n] -> Dom n-singleton x = { lomask = x, himask = x }--isSingleton : {n} (fin n) => Dom n -> Bit-isSingleton a = a.lomask == a.himask--top : {n} (fin n) => Dom n-top = { lomask = 0, himask = ~0 }--overlap : {n} (fin n) => Dom n -> Dom n -> Bit-overlap a b = nonempty (intersection a b)--intersection : {n} (fin n) => Dom n -> Dom n -> Dom n-intersection a b = { lomask = a.lomask || b.lomask, himask = a.himask && b.himask }--union : {n} (fin n) => Dom n -> Dom n -> Dom n-union a b = { lomask = a.lomask && b.lomask, himask = a.himask || b.himask }--zero_ext : {m, n} (fin m, m >= n) => Dom n -> Dom m-zero_ext a = { lomask = zext a.lomask, himask = zext a.himask }--sign_ext : {m, n} (fin m, m >= n, n >= 1) => Dom n -> Dom m-sign_ext a = { lomask = sext a.lomask, himask = sext a.himask }--concat : {m, n} (fin m, fin n) => Dom m -> Dom n -> Dom (m + n)-concat a b = { lomask = a.lomask # b.lomask, himask = a.himask # b.himask }--shrink : {m, n} (fin m, fin n) => Dom (m + n) -> Dom m-shrink a = { lomask = take`{m} a.lomask, himask = take`{m} a.himask }--trunc : {m, n} (fin m, fin n) => Dom (m + n) -> Dom n-trunc a = { lomask = drop`{m} a.lomask, himask = drop`{m} a.himask }--bnot : {n} (fin n) => Dom n -> Dom n-bnot b = { lomask = ~b.himask, himask = ~b.lomask }--band : {n} (fin n) => Dom n -> Dom n -> Dom n-band a b = { lomask = a.lomask && b.lomask, himask = a.himask && b.himask }--bor : {n} (fin n) => Dom n -> Dom n -> Dom n-bor a b = { lomask = a.lomask || b.lomask, himask = a.himask || b.himask }--// Note, this requires quite a few more operations than AND and OR.-// See "xordomain.cry" for a domain optimized for XOR and AND operations.-bxor : {n} (fin n) => Dom n -> Dom n -> Dom n-bxor a b = { lomask = lo, himask = hi }-  where-  ua = a.lomask ^ a.himask-  ub = b.lomask ^ b.himask-  c  = a.lomask ^ b.lomask-  u  = ua || ub-  hi = c || u-  lo = hi ^ u--// Note: shift and rotate operations in this domain only apply-// when the shift amount is known-shl : {n} (fin n) => Dom n -> [n] -> Dom n-shl a x = { lomask = a.lomask << x', himask = a.himask << x' }-  where x' = if x < `n then x else `n--lshr : {n} (fin n) => Dom n -> [n] -> Dom n-lshr a x = { lomask = a.lomask >> x', himask = a.himask >> x' }-  where x' = if x < `n then x else `n--ashr : {n} (fin n, n >= 1) => Dom n -> [n] -> Dom n-ashr a x = { lomask = a.lomask >>$ x', himask = a.himask >>$ x' }-  where x' = if x < `n then x else `n--rol : {n} (fin n) => Dom n -> [n] -> Dom n-rol a x = { lomask = a.lomask <<< x, himask = a.himask <<< x }--ror : {n} (fin n) => Dom n -> [n] -> Dom n-ror a x = { lomask = a.lomask >>> x, himask = a.himask >>> x }--////////////////////////////////////////////////////////////-// Soundness properties--correct_top : {n} (fin n) => [n] -> Bit-correct_top x = mem top x--correct_singleton : {n} (fin n) => [n] -> [n] -> Bit-correct_singleton x y = mem (singleton x) y == (x == y)--correct_overlap : {n} (fin n) => Dom n -> Dom n -> [n] -> Bit-correct_overlap a b x =-  mem a x ==> mem b x ==> overlap a b--correct_overlap_inv : {n} (fin n) => Dom n -> Dom n -> Bit-correct_overlap_inv a b =-  overlap a b ==> (mem a (a.lomask || b.lomask) /\ mem b (a.lomask || b.lomask))--correct_union : {n} (fin n) => Dom n -> Dom n -> [n] -> Bit-correct_union a b x =-  (mem a x \/ mem b x) ==> mem (union a b) x--correct_intersection : {n} (fin n) => Dom n -> Dom n -> [n] -> Bit-correct_intersection a b x =-  (mem a x /\ mem b x) == mem (intersection a b) x--correct_zero_ext : {m, n} (fin m, m >= n) => Dom n -> [n] -> Bit-correct_zero_ext a x =-  mem a x ==> mem (zero_ext`{m} a) (zext`{m} x)--correct_sign_ext : {m, n} (fin m, m >= n, n >= 1) => Dom n -> [n] -> Bit-correct_sign_ext a x =-  mem a x ==> mem (sign_ext`{m} a) (sext`{m} x)--correct_concat : {m, n} (fin m, fin n) => Dom m -> Dom n -> [m] -> [n] -> Bit-correct_concat a b x y =-  mem a x ==> mem b y ==> mem (concat a b) (x # y)--correct_shrink : {m, n} (fin m, fin n) => Dom (m + n) -> [m+n] -> Bit-correct_shrink a x =-  mem a x ==> mem (shrink`{m} a) (take`{m} x)--correct_trunc : {m, n} (fin m, fin n) => Dom (m + n) -> [m+n] -> Bit-correct_trunc a x =-  mem a x ==> mem (trunc`{m} a) (drop`{m} x)--correct_isSingleton : {n} (fin n) => Dom n -> Bit-correct_isSingleton a =-  isSingleton a ==> a == singleton a.lomask--correct_bnot : {n} (fin n) => Dom n -> [n] -> Bit-correct_bnot a x =-  mem a x == mem (bnot a) (~ x)--correct_band : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_band a b x y =-  mem a x ==> mem b y ==> mem (band a b) (x && y)--correct_bor : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_bor a b x y =-  mem a x ==> mem b y ==> mem (bor a b) (x || y)--correct_bxor : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_bxor a b x y =-  mem a x ==> mem b y ==> mem (bxor a b) (x ^ y)--correct_shl : {n} (fin n) => Dom n -> [n] -> [n] -> Bit-correct_shl a x y =-  mem a x ==> mem (shl a y) (x << y)--correct_lshr : {n} (fin n) => Dom n -> [n] -> [n] -> Bit-correct_lshr a x y =-  mem a x ==> mem (lshr a y) (x >> y)--correct_ashr : {n} (fin n, n >= 1) => Dom n -> [n] -> [n] -> Bit-correct_ashr a x y =-  mem a x ==> mem (ashr a y) (x >>$ y)--correct_rol : {n} (fin n) => Dom n -> [n] -> [n] -> Bit-correct_rol a x y =-  mem a x ==> mem (rol a y) (x <<< y)--correct_ror : {n} (fin n) => Dom n -> [n] -> [n] -> Bit-correct_ror a x y =-  mem a x ==> mem (ror a y) (x >>> y)--property b1 = correct_top`{16}-property b2 = correct_singleton`{16}-property b3 = correct_overlap`{16}-property b4 = correct_overlap_inv`{16}-property b5 = correct_union`{8}-property b6 = correct_intersection`{8}-property b7 = correct_zero_ext`{32, 16}-property b8 = correct_sign_ext`{32, 16}-property b9 = correct_concat`{16, 16}-property b10 = correct_shrink`{8, 8}-property b11 = correct_trunc`{8, 8}-property b12 = correct_isSingleton`{16}--property l1 = correct_bnot`{16}-property l2 = correct_band`{16}-property l3 = correct_bor`{16}-property l4 = correct_bxor`{16}--property s1 = correct_shl`{16}-property s2 = correct_lshr`{16}-property s3 = correct_ashr`{16}-property s4 = correct_rol`{16}-property s5 = correct_ror`{16}---////////////////////////////////////////////////////////////-// Operations preserve singletons--singleton_overlap : {n} (fin n) => [n] -> [n] -> Bit-singleton_overlap x y =-  overlap (singleton x) (singleton y) == (x == y)--singleton_zero_ext : {m, n} (fin m, m >= n) => [n] -> Bit-singleton_zero_ext x =-  zero_ext`{m} (singleton x) == singleton (zext`{m} x)--singleton_sign_ext : {m, n} (fin m, m >= n, n >= 1) => [n] -> Bit-singleton_sign_ext x =-  sign_ext`{m} (singleton x) == singleton (sext`{m} x)--singleton_concat : {m, n} (fin m, fin n) => [m] -> [n] -> Bit-singleton_concat x y =-  concat (singleton x) (singleton y) == singleton (x # y)--singleton_shrink : {m, n} (fin m, fin n) => [m + n] -> Bit-singleton_shrink x =-  shrink`{m} (singleton x) == singleton (take`{m} x)--singleton_trunc : {m, n} (fin m, fin n) => [m + n] -> Bit-singleton_trunc x =-  trunc`{m} (singleton x) == singleton (drop`{m} x)--singleton_bnot : {n} (fin n) => [n] -> Bit-singleton_bnot x =-  bnot (singleton x) == singleton (~ x)--singleton_band : {n} (fin n) => [n] -> [n] -> Bit-singleton_band x y =-  band (singleton x) (singleton y) == singleton (x && y)--singleton_bor : {n} (fin n) => [n] -> [n] -> Bit-singleton_bor x y =-  bor (singleton x) (singleton y) == singleton (x || y)--singleton_bxor : {n} (fin n) => [n] -> [n] -> Bit-singleton_bxor x y =-  bxor (singleton x) (singleton y) == singleton (x ^ y)--singleton_shl : {n} (fin n) => [n] -> [n] -> Bit-singleton_shl x y =-  shl (singleton x) y == singleton (x << y)--singleton_lshr : {n} (fin n) => [n] -> [n] -> Bit-singleton_lshr x y =-  lshr (singleton x) y == singleton (x >> y)--singleton_ashr : {n} (fin n, n >= 1) => [n] -> [n] -> Bit-singleton_ashr x y =-  ashr (singleton x) y == singleton (x >>$ y)--property i01 = singleton_overlap`{16}-property i02 = singleton_zero_ext`{32, 16}-property i03 = singleton_sign_ext`{32, 16}-property i04 = singleton_concat`{16, 16}-property i05 = singleton_shrink`{8, 8}-property i06 = singleton_trunc`{8, 8}-property i07 = singleton_band`{16}-property i08 = singleton_bor`{16}-property i09 = singleton_bxor`{16}-property i10 = singleton_bnot`{16}-property i11 = singleton_shl`{8}-property i12 = singleton_lshr`{8}-property i13 = singleton_ashr`{8}

@@ -1,287 +0,0 @@-/*--This file gives Cryptol implementations for transferring between-the various bitvector domain representations and proofs of the-correctness of these operations.-*/--module bvdomain where--import arithdomain as A-import bitsdomain as B-import xordomain as X---// Precondition `x <= mask`.  Find the (arithmetically) smallest-//  `z` above `x` which is bitwise above `mask`.  In other words-// find the smallest `z` such that `x <= z` and `mask || z == z`.--bitwise_round_above : {n} (fin n, n >= 1) => [n] -> [n] -> [n]-bitwise_round_above x mask = (x && ~q) ^ (mask && q)-  where-  q = A::fillright_alt ((x || mask) ^ x)--bra_correct1 : {n} (fin n, n>=1) => [n] -> [n] -> Bit-bra_correct1 x mask = mask <= x ==> (x <= q /\ B::bitle mask q)-  where-  q = bitwise_round_above x mask--bra_correct2 : {n} (fin n, n>=1) => [n] -> [n] -> [n] -> Bit-bra_correct2 x mask q' = (x <= q' /\ B::bitle mask q') ==> q <= q'-  where-  q = bitwise_round_above x mask--property bra1 = bra_correct1`{64}-property bra2 = bra_correct2`{64}---// Precondition `lomask <= x <= himask` and `lomask || himask == himask`.-// Find the (arithmetically) smallest `z` above `x` which is bitwise between-// `lomask` and `himask`.  In otherwords, find the smallest `z` such that-//  `x <= z` and `lomask || z = z` and `z || himask == himask`.-bitwise_round_between : {n} (fin n, n >= 1) => [n] -> [n] -> [n] -> [n]-bitwise_round_between x lomask himask = if r == 0 then loup else final-  // Read these steps from the bottom up...-  where--  // Finally mask out the low bits and only set those requried by the lomask-  final = (upper && ~lowbits) || lomask--  // add the correcting bit and mask out any extraneous bits set in-  // the previous step-  upper = (z + highbit) && himask--  // set ourselves up so that when we add the high bit to correct,-  // the carry will ripple until it finds a bit position that we-  // are allowed to set.-  z = loup || ~himask--  // isolate just the highest incorrect bit-  highbit = rmask ^ lowbits--  // A mask for all the bits lower than the high bit of r-  lowbits = rmask >> 1--  // set all the bits to the right of the highest incorrect bit-  rmask = A::fillright_alt r--  // now compute all the bits that are set that are not allowed-  // to be set according to the himask-  r = loup && ~himask--  // first, round up to the lomask-  loup = bitwise_round_above x lomask---brb_correct1 : {n} (fin n, n>=1) => [n] -> [n] -> [n] -> Bit-brb_correct1 x lomask himask =-    (B::bitle lomask himask /\ lomask <= x /\ x <= himask) ==>-    (x <= q /\ B::bitle lomask q /\ B::bitle q himask)--  where-  q = bitwise_round_between x lomask himask--brb_correct2 : {n} (fin n, n>=1) => [n] -> [n] -> [n] -> [n] -> Bit-brb_correct2 x lomask himask q' = (x <= q' /\ B::bitle lomask q' /\ B::bitle q' himask) ==> q <= q'-  where-  q = bitwise_round_between x lomask himask--property brb1 = brb_correct1`{64}-property brb2 = brb_correct2`{64}--// Interesting fact about arithmetic domains: the low values of the two domains-// represent overlap candidates.  If neither low value is contained in the other domain,-// then they do not overlap.-arith_overlap_candidates : {n} (fin n, n >= 1) => A::Dom n -> A::Dom n -> [n] -> Bit-arith_overlap_candidates a b x =-  A::mem a x ==>-  A::mem b x ==>-  ((A::mem a b.lo /\ A::mem b b.lo) \/-   (A::mem a a.lo /\ A::mem b a.lo))--// Bitwise domains, if they overlap, must overlap in some specific points.  The bitwise-// union of the low bounds is one.-bitwise_overlap_candidates : {n} (fin n, n >= 1) => B::Dom n -> B::Dom n -> [n] -> Bit-bitwise_overlap_candidates a b x =-  B::mem a x ==>-  B::mem b x ==>-  (B::mem a witness /\ B::mem b witness)-- where- witness = a.lomask || b.lomask--// If mixed domains have some common value, then they must definintely overlap at one-// of the following three listed candidate points.-mixed_overlap_candidates : {n} (fin n, n >= 1) => A::Dom n -> B::Dom n -> [n] -> Bit-mixed_overlap_candidates a b x =-  A::mem a x ==>-  B::mem b x ==>-  (A::mem a b.lomask /\ B::mem b b.lomask) \/-  (A::mem a b.himask /\ B::mem b b.himask) \/-  (A::mem a next     /\ B::mem b next)-- where- next = bitwise_round_between a.lo b.lomask b.himask---// A mixed domain overlap test.  It relies on testing special candidate overlap values.-//-// If none of the overlap candidates are found in both domains, then the domains do not overlap.-// On the other hand, if any canadiate is in both domains, it is a constructive witness of-// overlap.-mixed_domain_overlap : {n} (fin n, n >= 1) => A::Dom n -> B::Dom n -> Bit-mixed_domain_overlap a b =-  A::mem a b.lomask \/ A::mem a b.himask \/ A::mem a (bitwise_round_between a.lo b.lomask b.himask)--// If mixed domains have a common element, the overlap test will be true.-correct_mixed_domain_overlap : {n} (fin n, n >= 1) => A::Dom n -> B::Dom n -> [n] -> Bit-correct_mixed_domain_overlap a b x =-  A::mem a x ==>-  B::mem b x ==>-  mixed_domain_overlap a b--// If the overlap test is true, then we can find some element they share in common,-// provided the bitwise domain is nonempty.-correct_mixed_domain_overlap_inv : {n} (fin n, n >= 1) => A::Dom n -> B::Dom n -> Bit-correct_mixed_domain_overlap_inv a b =-  B::nonempty b ==> mixed_domain_overlap a b ==> (A::mem a witness /\ B::mem b witness)-- where- witness = if A::mem a b.lomask then b.lomask else-           if A::mem a b.himask then b.himask else-           bitwise_round_between a.lo b.lomask b.himask--property mx = correct_mixed_domain_overlap`{64}-property mx_inv = correct_mixed_domain_overlap_inv`{64}---// Operations that transfer between the domains--arithToBitDom : {n} (fin n, n >= 1) => A::Dom n -> B::Dom n-arithToBitDom a = { lomask = lo, himask = hi }-  where-  u  = A::unknowns a-  hi = a.lo || u-  lo = hi ^ u--bitToArithDom : {n} (fin n) => B::Dom n -> A::Dom n-bitToArithDom b = A::range b.lomask b.himask--bitToXorDom : {n} (fin n) => B::Dom n -> X::Dom n-bitToXorDom b = { val = b.himask, unknown = b.lomask ^ b.himask }--xorToBitDom : {n} (fin n) => X::Dom n -> B::Dom n-xorToBitDom x = { lomask = x.val ^ x.unknown, himask = x.val }--arithToXorDom : {n} (fin n, n >= 1) => A::Dom n -> X::Dom n-arithToXorDom a = { val = a.lo || u, unknown = u }-  where-  u = A::unknowns a--// A small collection of operations that start in one-// domain and end in the other--popcount : {n} (fin n, n>=1) => [n] -> [n]-popcount bs = sum [ zero#[b] | b <- bs ]--countLeadingZeros : {n} (fin n, n>=1) => [n] -> [n]-countLeadingZeros x = loop 0- where- loop n =-   if n >= length x then-     length x-   else-     if x@n then n else loop (n+1)--countTrailingZeros : {n} (fin n, n>=1) => [n] -> [n]-countTrailingZeros xs = countLeadingZeros (reverse xs)----popcnt : {n} (fin n, n>=1) => B::Dom n -> A::Dom n-popcnt b = A::range lo hi-  where-  lo = popcount b.lomask-  hi = popcount b.himask--clz : {n} (fin n, n>=1) => B::Dom n -> A::Dom n-clz b = A::range lo hi- where- lo = countLeadingZeros b.himask- hi = countLeadingZeros b.lomask--ctz : {n} (fin n, n>=1) => B::Dom n -> A::Dom n-ctz b = A::range lo hi- where- lo = countTrailingZeros b.himask- hi = countTrailingZeros b.lomask---//////////////////////////////////////////////////////////////-// Correctness properties--correct_arithToBitDom : {n} (fin n, n >= 1) => A::Dom n -> [n] -> Bit-correct_arithToBitDom a x =-  A::mem a x ==> B::mem (arithToBitDom a) x--correct_bitToArithDom : {n} (fin n) => B::Dom n -> [n] -> Bit-correct_bitToArithDom b x =-  B::mem b x ==> A::mem (bitToArithDom b) x--correct_bitToXorDom : {n} (fin n) => B::Dom n -> [n] -> Bit-correct_bitToXorDom b x =-  B::mem b x == X::mem (bitToXorDom b) x--correct_xorToBitDom : {n} (fin n) => X::Dom n -> [n] -> Bit-correct_xorToBitDom b x =-  X::mem b x == B::mem (xorToBitDom b) x--correct_arithToXorDom : {n} (fin n, n >= 1) => A::Dom n -> [n] -> Bit-correct_arithToXorDom a x =-  A::mem a x ==> X::mem (arithToXorDom a) x--property t1 = correct_arithToBitDom`{16}-property t2 = correct_bitToArithDom`{16}-property t3 = correct_bitToXorDom`{16}-property t4 = correct_xorToBitDom`{16}-property t5 = correct_arithToXorDom`{16}--correct_popcnt : {n} (fin n, n>=1) => B::Dom n -> [n] -> Bit-correct_popcnt a x =-  B::mem a x ==> A::mem (popcnt a) (popcount x)--correct_clz : {n} (fin n, n>=1) => B::Dom n -> [n] -> Bit-correct_clz a x =-  B::mem a x ==> A::mem (clz a) (countLeadingZeros x)--correct_ctz : {n} (fin n, n>=1) => B::Dom n -> [n] -> Bit-correct_ctz a x =-  B::mem a x ==> A::mem (ctz a) (countTrailingZeros x)--property w1 = correct_popcnt`{16}-property w2 = correct_clz`{16}-property w3 = correct_ctz`{16}--////////////////////////////////////////////////////////////////-// Proofs that the XOR domain is really just an alternate way-// to compute the same thing as the bitsdomain operations.-// For "band" this requires the input domains to be nonempty,-// which should be the case for all actual values of interest.--equiv_bxor : {n} (fin n) => B::Dom n -> B::Dom n -> Bit-equiv_bxor a b =-  B::bxor a b == xorToBitDom (X::bxor (bitToXorDom a) (bitToXorDom b))--equiv_band : {n} (fin n) => B::Dom n -> B::Dom n -> Bit-equiv_band a b =-  B::nonempty a /\ B::nonempty b ==>-  B::band a b == xorToBitDom (X::band (bitToXorDom a) (bitToXorDom b))--equiv_band_scalar : {n} (fin n) => B::Dom n -> [n] -> Bit-equiv_band_scalar a x =-  B::band a (B::singleton x) == xorToBitDom (X::band_scalar (bitToXorDom a) x)---property e1 = equiv_bxor`{16}-property e2 = equiv_band`{16}-property e3 = equiv_band_scalar`{16}

@@ -1,53 +0,0 @@-/*-This file contains a Cryptol implementation of a specialzed bitwise-abstract domain that is optimized for the XOR/AND semiring representation.-The standard bitwise domain from "bitsdomain.cry" requires 6 bitwise-operations to compute XOR, whereas AND and OR only requre 2.-In this domain, XOR and AND both can be computed in 3 bitwise operations,-and scalar AND can be computed in 2.-*/--module xordomain where--// In this presentation "val" is a bitwise upper bound on-// the values in the set, and "unknown" represents all the-// bits whose values are not concretely known-type Dom n = { val : [n], unknown : [n] }--// Membership predicate for the XOR bitwise domain-mem : {n} (fin n) => Dom n -> [n] -> Bit-mem a x = a.val == x || a.unknown--bxor : {n} (fin n) => Dom n -> Dom n -> Dom n-bxor a b = { val = v || u, unknown = u }-  where-  v = a.val ^ b.val-  u = a.unknown || b.unknown--band : {n} (fin n) => Dom n -> Dom n -> Dom n-band a b = { val = v, unknown = u && v }-  where-  v   = a.val && b.val-  u   = a.unknown || b.unknown--band_scalar : {n} (fin n) => Dom n -> [n] -> Dom n-band_scalar a x = { val = a.val && x, unknown = a.unknown && x }--////////////////////////////////////////////////////////////-// Soundness properties--correct_bxor : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_bxor a b x y =-  mem a x ==> mem b y ==> mem (bxor a b) (x ^ y)--correct_band : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Bit-correct_band a b x y =-  mem a x ==> mem b y ==> mem (band a b) (x && y)--correct_band_scalar : {n} (fin n) => Dom n -> [n] -> [n] -> Bit-correct_band_scalar a x y =-  mem a x ==> mem (band_scalar a y) (x && y)--property x1 = correct_bxor`{16}-property x2 = correct_band`{16}-property x3 = correct_band_scalar`{16}

@@ -1,200 +1,5 @@-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE RankNTypes #-}--{- |-Module      : Test.Verification-Description : Testing abstraction layer-Copyright   : (c) Galois Inc, 2020-License     : BSD3-Maintainer  : kquick@galois.com--This is a testing abstraction layer that allows the integration of-test properties and functions into the What4 library without requiring-a binding to a specific testing library or version thereof-(e.g. QuickCheck, Hedgehog, etc.).  All test properties and functions-should be specified using the primary set of functions in this module,-and then the actual test code will specify a binding of these-abstractions to a specific test library.--In this way, the What4 can implement not only local tests but the test-functionality can be exported to enable downstream modules to perform-extended testing.--The actual tests should be written using only the functions exported-in the testing exports section of this module.  Note that only the set-of functions needed for What4 is defined by this testing abstraction;-if additional testing functions are needed, the GenEnv context should be-extended to add an adaptation entry and the function should be defined-here for use by the tests.--The overlap (common subset) between testing libraries such as-QuickCheck and Hedgehog is only of moderate size: both libraries (and-especially Hedgehog) provide functionality that is not present in the-other library.  This module does not attempt to provide full coverage-for the functionality in both libraries; the intent is that test-functions can be written using the proxy functions defined here and-that downstream code using either of QuickCheck or Hedgehog can-utilize these support functions in their own tests.  As such, it is-recommended that the What4 integrated tests are limited in expression-to the common subset that can be described here.--A specific test configuration will need to use the functions and-definitions in the concretization exports to bind these abstracted-test functions to the specific library being used by that test suite.--For example, to bind to QuickCheck, specify:--> import QuickCheck-> import qualified Test.Verification as V->-> quickCheckGenerators = V.GenEnv { V.genChooseBool = elements [ True, False ]->                                 , V.genChooseInteger = \r -> choose r->                                 , V.genChooseInt = \r -> choose r->                                 , V.genGetSize = getSize->                                 }->-> genTest :: String -> V.Gen V.Property -> TestTree-> genTest nm p = testProperty nm->                (property $ V.toNativeProperty quickCheckGenerators p)---}--module Test.Verification-  (-    -- * Testing definitions--    -- | These definitions should be used by the tests themselves.  Most-    -- of these parallel a corresponding function in QuickCheck or-    -- Hedgehog, so the adaptation is minimal.-    assuming-  , (==>)-  , property-  , chooseBool-  , chooseInt-  , chooseInteger-  , Gen-  , getSize-  , Verifiable(..)--    -- * Test concretization--    -- | Used by test implementation functions to map from this-    -- Verification abstraction to the actual test mechanism-    -- (e.g. QuickCheck, HedgeHog, etc.)-  , Property(..)-  , Assumption(..)-  , GenEnv(..)-  , toNativeProperty-  )-where--import Control.Monad.Trans (lift)-import Control.Monad.Trans.Reader---- | Local definition of a Property: intended to be a proxy for a--- QuickCheck Property or a Hedgehog Property.  The 'toNativeProperty'--- implementation function converts from these proxy Properties to the--- native Property implementation.------ Tests should only use the 'Property' type as an output; the--- constructors and internals should be used only by the test--- concretization.-data Property = BoolProperty Bool-              | AssumptionProp Assumption-  deriving Show---- | A class specifying things that can be verified by constructing a--- local Property.-class Verifiable prop where-  verifying :: prop -> Property--instance Verifiable Bool where verifying = BoolProperty---- | Used by testing code to assert a boolean property.-property :: Bool -> Property-property = verifying---- | Internal data structure to store the two elements to the '==>'--- assumption operator.-data Assumption  = Assuming { preCondition :: Bool,-                              assumedProp :: Property }-  deriving Show----- | The named form of the '==>' assumption operator-assuming :: Verifiable t => Bool -> t -> Property-assuming precond test = AssumptionProp $ Assuming precond $ verifying test---- | The assumption operator that performs the property test (second--- element) only when the first argument is true (the assumption guard--- for the test).  This is the analog to the corresponding QuickCheck--- ==> operator.-(==>) :: Verifiable t => Bool -> t -> Property-(==>) = assuming-infixr 0 ==>---instance Verifiable Property where-  verifying = id---- -------------------------------------------------------------------------- | This is the reader environment for the surface level proxy--- testing monad.  This environment will be provided by the actual--- test code to map these proxy operations to the specific testing--- implementation.-data GenEnv m = GenEnv { genChooseBool :: m Bool-                       , genChooseInt :: (Int, Int) -> m Int-                       , genChooseInteger :: (Integer, Integer) -> m Integer-                       , genGetSize :: m Int-                       }---- | This is the generator monad for the Verification proxy tests.--- The inner monad will be the actual test implementation's monadic--- generator, and the 'a' return type is the type returned by running--- this monad.------ Tests should only use the 'Gen TYPE' as an output; the--- constructors and internals should be used only by the test--- concretization.-newtype Gen a =-  Gen { unGen :: forall m. Monad m => ReaderT (GenEnv m) m a }--instance Functor Gen where-  fmap f (Gen m) = Gen (fmap f m)--instance Applicative Gen where-  pure x = Gen (pure x)-  (Gen f) <*> (Gen x) = Gen (f <*> x)--instance Monad Gen where-  Gen x >>= f = Gen (x >>= \x' -> unGen (f x'))---- | A test generator that returns True or False-chooseBool :: Gen Bool-chooseBool = Gen (asks genChooseBool >>= lift)---- | A test generator that returns an 'Int' value between the--- specified (inclusive) bounds.-chooseInt :: (Int, Int) -> Gen Int-chooseInt r = Gen (asks genChooseInt >>= lift . ($ r))---- | A test generator that returns an 'Integer' value between the--- specified (inclusive) bounds.-chooseInteger :: (Integer, Integer) -> Gen Integer-chooseInteger r = Gen (asks genChooseInteger >>= lift . ($ r))---- | A test generator that returns the current shrink size of the--- generator functionality.-getSize :: Gen Int-getSize = Gen (asks genGetSize >>= lift)+module Test.Verification {-# DEPRECATED "Use What4.Domains.Verification instead" #-}+  ( module What4.Domains.Verification+  ) where --- | This function should be called by the testing code to convert the--- proxy tests in this module into the native tests (e.g. QuickCheck--- or Hedgehog).  This function is provided with the mapping--- environment between the proxy tests here and the native--- equivalents, and a local Generator monad expression, returning a--- native Generator equivalent.-toNativeProperty :: Monad m => GenEnv m -> Gen b -> m b-toNativeProperty gens (Gen gprops) = runReaderT gprops gens+import What4.Domains.Verification

@@ -173,8 +173,7 @@ import           Control.Applicative ( Const(..), (<|>) ) import           Control.Concurrent.MVar import qualified Control.Concurrent.ReadWriteVar as RWV-import           Control.Lens ((&))-import qualified Control.Lens.Combinators as LC+import           Lens.Micro ((&)) import           Control.Monad (foldM, when) import           Control.Monad.Catch import           Control.Monad.IO.Class@@ -318,8 +317,11 @@  instance Show (OptionSetting tp) where   show = (<> " option setting") .-         LC.cons '\'' . flip LC.snoc '\'' .+         cons '\'' . flip snoc '\'' .          show . optionSettingName+    where+      cons x l = x : l+      snoc l x = l ++ [x] instance ShowF OptionSetting  -- | An option defines some metadata about how a configuration option behaves.

@@ -19,7 +19,7 @@ , cacheOptDesc ) where -import           Control.Lens ( (&) )+import           Lens.Micro ( (&) ) import           Control.Monad.ST (stToIO) import           Data.IORef 

@@ -1,11 +1,79 @@ {-| Module      : What4.Expr.App-Copyright   : (c) Galois Inc, 2015-2020+Copyright   : (c) Galois Inc, 2015-2026 License     : BSD3-Maintainer  : jhendrix@galois.com+Maintainer  : langston@galois.com -This module defines datastructures that encode the basic-syntax formers used in What4.ExprBuilder.+This module defines datastructures that encode the syntax of expressions used in+"What4.Expr.Builder".++As described there, the 'Expr' type makes extensive use of data structures that+by their very structure (partially) normalize expressions of the given kind.+Examples include 'WeightedSum', 'SemiRingProduct', 'BVOrSet', and 'BM.ConjMap'.++To understand these normalizing data structures, first consider a \"naive\"+representation of SMT terms in a tree-like AST. Consider in particular+conjunction (@AND@). Perhaps the simplest way to represent conjunction would be+a binary constructor:++> data Expr t tp where+>   And :: Expr t BaseBoolType ->  Expr t BaseBoolType -> Expr t BaseBoolType++However, this representation makes semantically equivalent terms structurally+unequal, for example @x and (y and z)@ would be @And x (And y z)@ whereas+@(x and y) and z@ would be @And (And x y) z@. To solve this problem with+associativity, we could consider storing a list of conjuncts in @And@:++> data Expr t tp where+>   And :: [Expr t BaseBoolType] -> Expr t BaseBoolType++Then with a bit of help (e.g., a smart constructor) both expressions would+become @And [x, y, z]@. While this improved representation normalizes @and@+expressions with respect to associativity, it ignores several other important+algebraic properties of @and@:++* Idempotency: @x and x = x@+* Commutativity: @x and y = y and x@+* Complementation: @x and ~x = false@++For example, @(x and y) and x@ would be @And [x, y, x]@ whereas @(x and x)+and y@ would be @And [x, x, y]@. Again, we have semantically equivalent but+structurally different terms.++We can normalize with respect to idempotency and commutativity by moving to a+set datastructure:++> data Expr t tp where+>   And :: Set (Expr t BaseBoolType) -> Expr t BaseBoolType++Both of our problematic expressions would now be represented as @And {x, y}@.++Finally, to normalize with respect to complementation, we can move from a set to+a map:++> data Polarity = Positive | Negative+>+> data Expr t tp where+>   And :: Map (Expr t BaseBoolType) Polarity -> Expr t BaseBoolType++On insertion, we check if the expression already appears with opposite polarity.+If so, the entire expression collapses to @false@.++We basically just invented 'BM.ConjMap'. As it turns out, all of the same laws+hold for @or@, where complements collapse to @true@. Noticing this brings us all+the way to 'BoolMap' (of which 'BM.ConjMap' is a wrapper).++We could play a similar game with addition and multiplication over+integers, bitvectors, and reals, which would lead us to 'WeightedSum' and+'SemiRingProduct'.++What does this normalization buy us? It can keep predicates concrete, obviating+solver calls. However, notice that the move from lists to sets came with a+significant trade-off: construction of terms jumped from @O(n)@ to @O(n log+n)@. This was considered an acceptable trade-off when What4 was created, but+we do not have comprehensive benchmarks justifying this choice with modern+SMT solvers. It may be that the overhead of constructing 'Expr's outweighs the+benefits of normalization. -} {-# LANGUAGE CPP #-} {-# LANGUAGE BangPatterns #-}@@ -38,11 +106,12 @@ module What4.Expr.App where  import qualified Control.Exception as Ex-import           Control.Lens hiding (asIndex, (:>), Empty)+import           Lens.Micro import           Control.Monad import           Control.Monad.ST import qualified Data.BitVector.Sized as BV import           Data.Foldable+import           Data.Functor.Const (Const(..)) import           Data.Hashable import qualified Data.HashTable.Class as H (toList) import qualified Data.HashTable.ST.Basic as H@@ -75,6 +144,7 @@  import           What4.BaseTypes import           What4.Concrete+import qualified What4.Domains.BV as BVD import           What4.Interface import           What4.ProgramLoc import qualified What4.SemiRing as SR@@ -91,7 +161,6 @@  import           What4.Utils.AbstractDomains import           What4.Utils.Arithmetic-import qualified What4.Utils.BVDomain as BVD import           What4.Utils.Complex import           What4.Utils.IncrHash import qualified What4.Utils.AnnotatedMap as AM@@ -787,7 +856,13 @@  traverseApp :: (Applicative m, OrdF f, Eq (f (BaseBoolType)), HashableF f, HasAbsValue f)             => (forall tp. e tp -> m (f tp))-            -> App e utp -> m ((App f) utp)+            -> App e utp -> m (App f utp)++-- This is the type at its use in 'evalBoundVars'+{-# SPECIALIZE traverseApp ::+  (forall tp. Expr t tp -> IO (Expr t tp))+  -> App (Expr t) utp -> IO (App (Expr t) utp) #-}+ traverseApp =   $(structuralTraversal [t|App|]     [ ( ConType [t|UnaryBV|] `TypeApp` AnyType `TypeApp` AnyType@@ -1741,6 +1816,11 @@ traverseBVOrSet f (BVOrSet m) =   foldr bvOrInsert (BVOrSet AM.empty) <$> traverse (f . unWrap . fst) (AM.toList m) +-- This is the type at its use in 'evalBoundVars'+{-# SPECIALIZE traverseBVOrSet ::+  (forall tp. Expr t tp -> IO (Expr t tp))+  -> BVOrSet (Expr t) utp -> IO (BVOrSet (Expr t) utp) #-}+ bvOrInsert :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w bvOrInsert e (BVOrSet m) = BVOrSet $ AM.insert (Wrap e) (BVOrNote (mkIncrHash (hashF e)) (getAbsValue e)) () m @@ -2016,12 +2096,12 @@     FloatRound{} -> ()     FloatFromBinary{} -> ()     FloatToBinary fpp _ -> case floatPrecisionToBVType fpp of-      BaseBVRepr w -> BVD.any w+      BaseBVRepr w -> BVD.top w     BVToFloat{} -> ()     SBVToFloat{} -> ()     RealToFloat{} -> ()-    FloatToBV w _ _ -> BVD.any w-    FloatToSBV w _ _ -> BVD.any w+    FloatToBV w _ _ -> BVD.top w+    FloatToSBV w _ _ -> BVD.top w     FloatToReal{} -> ravUnbounded     FloatSpecialFunction{} -> () 

@@ -5,9 +5,10 @@ License     : BSD3 Maintainer  : rdockins@galois.com -Declares a datatype for representing n-way conjunctions or disjunctions-in a way that efficiently captures important algebraic-laws like commutativity, associativity and resolution.+Declares a datatype for representing n-way conjunctions or disjunctions in+a way that efficiently captures important algebraic laws like commutativity,+associativity and resolution. See "What4.Expr.App" for an overview of such+normalizing data structures generally, with 'BoolMap' as an extended example. -}  {-# LANGUAGE DataKinds #-}@@ -46,7 +47,7 @@   , evalConj   ) where -import           Control.Lens (_1, over)+import           Lens.Micro (_1, over) import           Data.Coerce (coerce) import           Data.Hashable import qualified Data.List as List (foldl')@@ -118,12 +119,21 @@ foldMapVars f (BoolMap am) = foldMap (f . unWrap . fst) (AM.toList am)  -- | Traverse the expressions in a bool map, and rebuild the map.-traverseVars :: (Applicative m, HashableF g, OrdF g) =>+traverseVars ::+  (Applicative m, HashableF g, OrdF g) =>   (f BaseBoolType -> m (g (BaseBoolType))) ->-  BoolMap f -> m (BoolMap g)+  BoolMap f ->+  m (BoolMap g) traverseVars _ InconsistentMap = pure InconsistentMap traverseVars f (BoolMap m) =   fromVars <$> traverse (_1 (f . unWrap)) (AM.toList m)+-- This signature is used in betaReduce/evalBoundVars with f = g = Expr t+{-# SPECIALIZE traverseVars ::+  (HashableF g, OrdF g) =>+  (f BaseBoolType -> IO (g (BaseBoolType))) ->+  BoolMap f ->+  IO (BoolMap g)+ #-}  elementHash :: HashableF f => f BaseBoolType -> Polarity -> IncrHash elementHash x p = mkIncrHash (hashWithSaltF (hash p) x)

@@ -1,14 +1,29 @@ {-| Module      : What4.Expr.Builder Description : Main definitions of the What4 expression representation-Copyright   : (c) Galois Inc, 2015-2020+Copyright   : (c) Galois Inc, 2015-2026 License     : BSD3-Maintainer  : jhendrix@galois.com+Maintainer  : langston@galois.com  This module defines the canonical implementation of the solver interface from "What4.Interface". Type @'ExprBuilder' t st@ is an instance of the classes 'IsExprBuilder' and 'IsSymExprBuilder'. +'ExprBuilder' tries hard to keep symbolic expressions as simple and concrete as+possible. It does so using three techniques:++* Local rewrites when expressions are constructed (see the 'IsExprBuilder'+  instance of 'ExprBuilder'). Such rewrites often result in a partially+  normalized format for expressions of a given type.+* Abstract domains (see "What4.Utils.AbstractDomains").+* Data structures that by their very structure (partially) normalize+  expressions of the given kind. See "What4.Expr.App" for more details.++Together, these techniques can actually solve a surprising number of SMT+problems without ever consulting an external solver.++-- * Concurrency+ Notes regarding concurrency: The expression builder datatype contains a number of mutable storage locations.  These are designed so they may reasonably be used in a multithreaded context.  In particular,@@ -200,7 +215,7 @@   ) where  import qualified Control.Exception as Ex-import           Control.Lens hiding (asIndex, (:>), Empty)+import           Lens.Micro import           Control.Monad import           Control.Monad.Except import           Control.Monad.Reader@@ -210,6 +225,7 @@ import           Data.Bimap (Bimap) import qualified Data.Bimap as Bimap +import           Data.Functor.Identity (Identity(..)) import           Data.Hashable import qualified Data.HashTable.Class as HC import qualified Data.HashTable.IO as H@@ -238,6 +254,7 @@ import           What4.Concrete import qualified What4.Config as CFG import           What4.FloatMode+import qualified What4.Domains.BV as BVD import           What4.Interface import           What4.InterpretedFloatingPoint import           What4.ProgramLoc@@ -260,7 +277,6 @@  import           What4.Utils.AbstractDomains import           What4.Utils.Arithmetic-import qualified What4.Utils.BVDomain as BVD import           What4.Utils.Complex import           What4.Utils.FloatHelpers import           What4.Utils.StringLiteral@@ -437,22 +453,22 @@ type instance BoundVar (ExprBuilder t st fs) = ExprBoundVar t type instance SymAnnotation (ExprBuilder t st fs) = Nonce t -exprCounter :: Getter (ExprBuilder t st fs) (NonceGenerator IO t)+exprCounter :: SimpleGetter (ExprBuilder t st fs) (NonceGenerator IO t) exprCounter = to sbExprCounter  userState :: Lens' (ExprBuilder t st fs) (st t) userState = lens sbUserState (\sym st -> sym{ sbUserState = st }) -unaryThreshold :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseIntegerType)+unaryThreshold :: SimpleGetter (ExprBuilder t st fs) (CFG.OptionSetting BaseIntegerType) unaryThreshold = to sbUnaryThreshold -cacheStartSize :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseIntegerType)+cacheStartSize :: SimpleGetter (ExprBuilder t st fs) (CFG.OptionSetting BaseIntegerType) cacheStartSize = to sbCacheStartSize -pushMuxOps :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseBoolType)+pushMuxOps :: SimpleGetter (ExprBuilder t st fs) (CFG.OptionSetting BaseBoolType) pushMuxOps = to sbPushMuxOps -uninterpFnCache :: Getter (ExprBuilder t st fs) (IORef (UninterpFunCache t st fs))+uninterpFnCache :: SimpleGetter (ExprBuilder t st fs) (IORef (UninterpFunCache t st fs)) uninterpFnCache = to sbUninterpFnCache  -- | Return a new expr builder where the configuration object has@@ -4115,10 +4131,8 @@       RNA -> realRound sym x       RTP -> realCeil sym x       RTN -> realFloor sym x-      RTZ -> do-        is_pos <- realLt sym (realZero sym) x-        iteM intIte sym is_pos (realFloor sym x) (realCeil sym x)-      RNE -> fail "Unsupported rond to nearest even for real values."+      RTZ -> realTrunc sym x+      RNE -> realRoundEven sym x   iFloatFromBinary sym _ x     | Just (FnApp fn args) <- asNonceApp x     , "uninterpreted_real_to_float_binary" == solverSymbolAsText (symFnName fn)

@@ -450,7 +450,7 @@             myRem u v = BV.urem u v     BVSdiv w x y -> myDiv <$> f x <*> f y       where myDiv _ (BV.BV 0) = BV.zero w-            myDiv u v = BV.sdiv w u v+            myDiv u v = BV.squot w u v     BVSrem w x y -> myRem <$> f x <*> f y       where myRem u (BV.BV 0) = u             myRem u v = BV.srem w u v

@@ -19,7 +19,7 @@   , count_subterms   ) where -import           Control.Lens ((^.))+import           Lens.Micro ((^.)) import           Control.Monad (void, when) import           Control.Monad.ST import           Control.Monad.State (MonadState(..), State, execState)

@@ -56,7 +56,7 @@   ) where  import           Control.Exception (assert)-import           Control.Lens+import           Lens.Micro import           Control.Monad import           Data.Bits import           Data.Hashable@@ -66,8 +66,8 @@  import           What4.BaseTypes import           What4.Interface-import           What4.Utils.BVDomain (BVDomain)-import qualified What4.Utils.BVDomain as BVD+import           What4.Domains.BV (BVDomain)+import qualified What4.Domains.BV as BVD  import qualified Data.Map.Strict as Map 

@@ -41,7 +41,8 @@ import Control.Monad.Fail( MonadFail ) #endif -import           Control.Lens+import           Lens.Micro+import           Lens.Micro.Mtl import           Control.Monad (when) import           Control.Monad.Reader (MonadReader(..), ReaderT(..)) import           Control.Monad.ST@@ -103,28 +104,28 @@                       }  -- | Describes types of functionality required by solver based on the problem.-problemFeatures :: Simple Lens (CollectedVarInfo t) ProblemFeatures+problemFeatures :: Lens' (CollectedVarInfo t) ProblemFeatures problemFeatures = lens _problemFeatures (\s v -> s { _problemFeatures = v }) -uninterpConstants :: Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))+uninterpConstants :: Lens' (CollectedVarInfo t) (Set (Some (ExprBoundVar t))) uninterpConstants = lens _uninterpConstants (\s v -> s { _uninterpConstants = v })  -- | Expressions appearing in the problem as existentially quantified when -- the problem is expressed in negation normal form.  This is a map -- from the existential quantifier element to the info.-existQuantifiers :: Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)+existQuantifiers :: Lens' (CollectedVarInfo t) (QuantifierInfoMap t) existQuantifiers = lens _existQuantifiers (\s v -> s { _existQuantifiers = v })  -- | Expressions appearing in the problem as existentially quantified when -- the problem is expressed in negation normal form.  This is a map -- from the existential quantifier element to the info.-forallQuantifiers :: Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)+forallQuantifiers :: Lens' (CollectedVarInfo t) (QuantifierInfoMap t) forallQuantifiers = lens _forallQuantifiers (\s v -> s { _forallQuantifiers = v }) -latches :: Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))+latches :: Lens' (CollectedVarInfo t) (Set (Some (ExprBoundVar t))) latches = lens _latches (\s v -> s { _latches = v }) -varErrors :: Simple Lens (CollectedVarInfo t) (Seq (Doc Void))+varErrors :: Lens' (CollectedVarInfo t) (Seq (Doc Void)) varErrors = lens _varErrors (\s v -> s { _varErrors = v })  -- | Return variables needed to define element as a predicate

@@ -5,15 +5,17 @@ License     : BSD3 Maintainer  : jhendrix@galois.com -Declares a weighted sum type used for representing sums over variables and an offset-in one of the supported semirings.  This module also implements a representation of-semiring products.+Declares a weighted sum type used for representing sums over variables and+an offset in one of the supported semirings.  This module also implements a+representation of semiring products. See "What4.Expr.App" for an overview of+normalizing data structures such as these. -} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PolyKinds #-}@@ -69,7 +71,9 @@   , prodContains   ) where -import           Control.Lens+import qualified Control.Exception as Ex+import           Data.Functor.Identity (Identity(..))+import           Lens.Micro import           Control.Monad (unless) import qualified Data.BitVector.Sized as BV import           Data.Hashable@@ -79,13 +83,13 @@ import           Data.Parameterized.Classes  import           What4.BaseTypes+import qualified What4.Domains.BV as BVD+import qualified What4.Domains.BV.Arith as A+import qualified What4.Domains.BV.XOR as X import qualified What4.SemiRing as SR import           What4.Utils.AnnotatedMap (AnnotatedMap) import qualified What4.Utils.AnnotatedMap as AM import qualified What4.Utils.AbstractDomains as AD-import qualified What4.Utils.BVDomain.Arith as A-import qualified What4.Utils.BVDomain.XOR as X-import qualified What4.Utils.BVDomain as BVD  import           What4.Utils.IncrHash @@ -154,6 +158,25 @@     SRAbsBVAdd   x -> BVD.BVDArith x     SRAbsBVXor   x -> BVD.fromXorDomain x +-- | Returns 'Just' when the abstract value is a singleton.+asCoeff ::+  AD.HasAbsValue f =>+  SR.SemiRingRepr sr ->+  f (SR.SemiRingBase sr) ->+  Maybe (SR.Coefficient sr)+asCoeff =+  \case+    SR.SemiRingIntegerRepr -> AD.asSingleRange . AD.getAbsValue+    SR.SemiRingRealRepr -> AD.asSingleRange . AD.ravRange . AD.getAbsValue+    SR.SemiRingBVRepr _ w -> fmap (BV.mkBV w) . BVD.asSingleton . AD.getAbsValue++varIsConst ::+  AD.HasAbsValue f =>+  SR.SemiRingRepr sr ->+  f (SR.SemiRingBase sr) ->+  Bool+varIsConst sr = isJust . asCoeff sr+ --------------------------------------------------------------------------------  type Tm f = (HashableF f, OrdF f, AD.HasAbsValue f)@@ -247,12 +270,21 @@   ProdMap f sr singletonProdMap sr occ t = AM.singleton (WrapF t) (mkProdNote sr occ t) occ +-- | Returns a 'SumMap' together with the sum of all 'SR.Cofficient'-only terms. fromListSumMap ::   Tm f =>   SR.SemiRingRepr sr ->-  [(f (SR.SemiRingBase sr), SR.Coefficient sr)] -> SumMap f sr-fromListSumMap _ [] = AM.empty-fromListSumMap sr ((t, c) : xs) = insertSumMap sr c t (fromListSumMap sr xs)+  [(f (SR.SemiRingBase sr), SR.Coefficient sr)] ->+  (SumMap f sr, SR.Coefficient sr)+fromListSumMap sr = foldr go (AM.empty, SR.zero sr)+  where+  go (t, c) (m, acc) =+    if SR.eq sr (SR.zero sr) c+    then (m, acc)+    else+      case asCoeff sr t of+        Just c' -> (m, SR.add sr (SR.mul sr c c') acc)+        Nothing -> (insertSumMap sr c t m, acc)  toListSumMap :: SumMap f sr -> [(f (SR.SemiRingBase sr), SR.Coefficient sr)] toListSumMap am = [ (t, c) | (WrapF t, c) <- AM.toList am ]@@ -261,9 +293,15 @@ --   an affine operation on the underlying expressions. data WeightedSum (f :: BaseType -> Type) (sr :: SR.SemiRing)    = WeightedSum { _sumMap     :: !(SumMap f sr)+                   -- ^ Map from terms to their coefficients+                   --+                   -- INVARIANT: The terms in the map should not be constant+                   -- (i.e., according to 'varIsConst') and the coefficients+                   -- should not be 'SR.zero'. This is not a safety invariant,+                   -- but helps ensure normalized terms.                  , _sumOffset  :: !(SR.Coefficient sr)                  , sumRepr     :: !(SR.SemiRingRepr sr)-                     -- ^ Runtime representation of the semiring for this sum.+                   -- ^ Runtime representation of the semiring for this sum.                  }  -- | A product of semiring values.@@ -318,17 +356,23 @@ instance OrdF f => Eq (WeightedSum f sr) where   x == y = isJust (testEquality x y) - -- | Created a weighted sum directly from a map and constant. ----- Note. When calling this, one should ensure map values equal to '0'--- have been removed.+-- When calling this, one should ensure values with coefficients equal to+-- @'SR.zero'@ have been removed and none of the terms of the map satisfy+-- 'varIsConst'. See INVARIANT on '_sumMap'. unfilteredSum ::+  AD.HasAbsValue f =>   SR.SemiRingRepr sr ->   SumMap f sr ->   SR.Coefficient sr ->   WeightedSum f sr-unfilteredSum sr m c = WeightedSum m c sr+unfilteredSum sr m c =+  Ex.assert (all (uncurry notConst) (toListSumMap m)) $+    WeightedSum m c sr+  where+  notConst v coeff =+    not (varIsConst sr v) && not (SR.eq sr (SR.zero sr) coeff)  -- | Retrieve the mapping from terms to coefficients. sumMap :: Lens' (WeightedSum f sr) (SumMap f sr)@@ -397,6 +441,19 @@ constant :: Tm f => SR.SemiRingRepr sr -> SR.Coefficient sr -> WeightedSum f sr constant sr c = unfilteredSum sr AM.empty c +-- | Create a sum from a single affine variable (@st + c@).+affineVar ::+  Tm f =>+  SR.SemiRingRepr sr ->+  SR.Coefficient sr ->+  f (SR.SemiRingBase sr) ->+  SR.Coefficient sr ->+  WeightedSum f sr+affineVar sr s t c+  | SR.eq sr (SR.zero sr) s = constant sr c+  | Just s' <- asCoeff sr t = constant sr (SR.add sr (SR.mul sr s s') c)+  | otherwise = unfilteredSum sr (singletonSumMap sr s t) c+ -- | Traverse the expressions in a weighted sum. traverseVars :: forall k j m sr.   (Applicative m, Tm k) =>@@ -408,6 +465,14 @@   traverse (_1 f) (toListSumMap (_sumMap w))   where sr = sumRepr w +-- This is the type at its use in 'evalBoundVars'+{-# SPECIALIZE traverseVars :: forall k sr.+  Tm k =>+  (k (SR.SemiRingBase sr) -> IO (k (SR.SemiRingBase sr))) ->+  WeightedSum k sr ->+  IO (WeightedSum k sr)+ #-}+ -- | Traverse the coefficients in a weighted sum. traverseCoeffs :: forall m f sr.   (Applicative m, Tm f) =>@@ -434,16 +499,21 @@   sr = prodRepr pd   rebuild = List.foldl' (\m (WrapF t, occ) -> AM.insert (WrapF t) (mkProdNote sr occ t) occ m) AM.empty +-- This is the type at its use in 'evalBoundVars'+{-# SPECIALIZE traverseProdVars :: forall k sr.+  Tm k =>+  (k (SR.SemiRingBase sr) -> IO (k (SR.SemiRingBase sr))) ->+  SemiRingProduct k sr ->+  IO (SemiRingProduct k sr)+ #-}  -- | This returns a variable times a constant. scaledVar :: Tm f => SR.SemiRingRepr sr -> SR.Coefficient sr -> f (SR.SemiRingBase sr) -> WeightedSum f sr-scaledVar sr s t-  | SR.eq sr (SR.zero sr) s = unfilteredSum sr AM.empty (SR.zero sr)-  | otherwise = unfilteredSum sr (singletonSumMap sr s t) (SR.zero sr)+scaledVar sr s t = affineVar sr s t (SR.zero sr)  -- | Create a weighted sum corresponding to the given variable. var :: Tm f => SR.SemiRingRepr sr -> f (SR.SemiRingBase sr) -> WeightedSum f sr-var sr t = unfilteredSum sr (singletonSumMap sr (SR.one sr) t) (SR.zero sr)+var sr t = scaledVar sr (SR.one sr) t  -- | Add two sums, collecting terms as necessary and deleting terms whose --   coefficients sum to 0.@@ -489,9 +559,16 @@   | otherwise = unfilteredSum sr m' (SR.mul sr c (wsum^.sumOffset))   where     m' = AM.mapMaybeWithKey f (wsum^.sumMap)-    f (WrapF t) _ x-      | SR.eq sr (SR.zero sr) cx = Nothing-      | otherwise = Just (mkNote sr cx t, cx)+    f (WrapF t) _ x =+      Ex.assert (not (varIsConst sr t)) $  -- INVARIANT+      -- Filter out terms that become zero after scaling. This can happen in+      -- bitvector arthmetic. For example, for 8-bit bitvectors c and x where+      -- c = 2 and x = 128, c * x mod 256 = 0.+      --+      -- Necessary to uphold INVARIANT.+      if SR.eq sr (SR.zero sr) cx+      then Nothing+      else Just (mkNote sr cx t, cx)       where cx = SR.mul sr c x  -- | Produce a weighted sum from a list of terms and an offset.@@ -501,7 +578,9 @@   [(f (SR.SemiRingBase sr), SR.Coefficient sr)] ->   SR.Coefficient sr ->   WeightedSum f sr-fromTerms sr tms offset = unfilteredSum sr (fromListSumMap sr tms) offset+fromTerms sr tms offset =+  let (m, offset') = fromListSumMap sr tms in+  unfilteredSum sr m (SR.add sr offset offset')  -- | Apply update functions to the terms and coefficients of a weighted sum. transformSum :: (Applicative m, Tm g) =>

@@ -202,7 +202,7 @@ #endif  import           Control.Exception (assert, Exception)-import           Control.Lens+import           Lens.Micro import           Control.Monad import           Control.Monad.IO.Class import qualified Data.BitVector.Sized as BV@@ -940,6 +940,136 @@          -> SymBV sym w          -> IO (SymBV sym w) +  {-+  Note [SMT-LIB division]+  ~~~~~~~~~~~~~~~~~~~~~~~++  The 'bvUdiv', 'bvUrem', 'bvSdiv', and 'bvSrem' methods document+  their behavior on a zero divisor as /undefined/. Backends are free+  to fold @bvUdiv x 0@ to anything they like; the abstract domain in+  "What4.Domains.BV.Arith" assumes @y /= 0@ when computing bounds, and+  the symbolic-eval machinery may constant-fold a div-by-zero+  expression to whatever the abstract value happens to be.++  The SMT-LIB @FixedSizeBitVectors@ theory, by contrast, /defines/ a+  value for division by zero:++  * @(bvudiv s 0)@ is the all-ones bitvector,+  * @(bvurem s 0)@ is @s@.++  See <https://smt-lib.org/theories-FixedSizeBitVectors.shtml>. The+  signed variants @bvsdiv@ and @bvsrem@ are not in the core theory but+  are uniformly implemented by Z3, CVC5, Bitwuzla, and Yices as++  * @(bvsdiv s 0) = if s < 0 then 1 else \-1@,+  * @(bvsrem s 0) = s@.++  Tools that translate SMT-LIB input through What4 (notably @w4smt2@)+  must therefore use a div/rem operator that respects these defined+  values, otherwise the abstract evaluator can produce concretely+  wrong constant folds for div-by-zero corners.++  We expose the SMT-LIB-faithful variants as separate methods rather than+  changing 'bvUdiv'\/etc., to preserve precisions for frontends with their own+  div-by-zero handling (e.g., by asserting to the solver that the denominator is+  not zero).++  /Why no dedicated @App@ constructor?/  The default implementations+  use 'bvIte' to splice the SMT-LIB-mandated value over the existing+  primitive: @bvUdivSmtlib x y = ite (y == 0) maxUnsigned (bvUdiv x+  y)@. Abstract evaluation of the resulting 'BaseIte' computes the+  union of the two branches' abstract values, which matches what a+  dedicated constructor would do via 'A.udivSmtlib'\/etc.\ — including+  in the constant-folding cases — so the only thing a dedicated+  constructor would buy is more compact SMT output, which is not+  worth the cross-cutting boilerplate.+  -}++  -- | Unsigned bitvector division, using the SMT-LIB+  -- @FixedSizeBitVectors@ theory's div-by-zero semantics:+  --+  -- @+  -- bvUdivSmtlib x 0 = bvNotBits 0   -- the all-ones bitvector+  -- @+  --+  -- Otherwise behaves like 'bvUdiv'. See @Note [SMT-LIB division]@.+  bvUdivSmtlib :: (1 <= w)+               => sym+               -> SymBV sym w+               -> SymBV sym w+               -> IO (SymBV sym w)+  bvUdivSmtlib sym x y = do+    let w = bvWidth x+    zero <- bvZero sym w+    isZero <- bvEq sym y zero+    allOnes <- bvLit sym w (BV.maxUnsigned w)+    safeQuot <- bvUdiv sym x y+    bvIte sym isZero allOnes safeQuot++  -- | Unsigned bitvector remainder, using the SMT-LIB+  -- @FixedSizeBitVectors@ theory's div-by-zero semantics:+  --+  -- @+  -- bvUremSmtlib x 0 = x+  -- @+  --+  -- Otherwise behaves like 'bvUrem'. See @Note [SMT-LIB division]@.+  bvUremSmtlib :: (1 <= w)+               => sym+               -> SymBV sym w+               -> SymBV sym w+               -> IO (SymBV sym w)+  bvUremSmtlib sym x y = do+    let w = bvWidth x+    zero <- bvZero sym w+    isZero <- bvEq sym y zero+    safeRem <- bvUrem sym x y+    bvIte sym isZero x safeRem++  -- | Signed bitvector division, using the SMT-LIB QF_BV logic's+  -- div-by-zero convention (matching Z3, CVC5, Bitwuzla, Yices):+  --+  -- @+  -- bvSdivSmtlib x 0 = if x \>= 0 then -1 else 1+  -- @+  --+  -- Otherwise behaves like 'bvSdiv'. See @Note [SMT-LIB division]@.+  bvSdivSmtlib :: (1 <= w)+               => sym+               -> SymBV sym w+               -> SymBV sym w+               -> IO (SymBV sym w)+  bvSdivSmtlib sym x y = do+    let w = bvWidth x+    zero <- bvZero sym w+    isZero <- bvEq sym y zero+    isNeg <- bvIsNeg sym x+    one <- bvLit sym w (BV.one w)+    allOnes <- bvLit sym w (BV.maxUnsigned w)+    onZero <- bvIte sym isNeg one allOnes+    safeQuot <- bvSdiv sym x y+    bvIte sym isZero onZero safeQuot++  -- | Signed bitvector remainder, using the SMT-LIB QF_BV logic's+  -- div-by-zero convention (matching Z3, CVC5, Bitwuzla, Yices):+  --+  -- @+  -- bvSremSmtlib x 0 = x+  -- @+  --+  -- Otherwise behaves like 'bvSrem'. See @Note [SMT-LIB division]@.+  bvSremSmtlib :: (1 <= w)+               => sym+               -> SymBV sym w+               -> SymBV sym w+               -> IO (SymBV sym w)+  bvSremSmtlib sym x y = do+    let w = bvWidth x+    zero <- bvZero sym w+    isZero <- bvEq sym y zero+    safeRem <- bvSrem sym x y+    bvIte sym isZero x safeRem+   -- | Returns true if the corresponding bit in the bitvector is set.   testBitBV :: (1 <= w)             => sym@@ -3006,7 +3136,7 @@     BaseIntegerRepr -> isJust $ asInteger x     BaseBVRepr _    -> isJust $ asBV x     BaseRealRepr    -> isJust $ asRational x-    BaseFloatRepr _ -> False+    BaseFloatRepr _ -> isJust $ asFloat x     BaseStringRepr{} -> isJust $ asString x     BaseComplexRepr -> isJust $ asComplex x     BaseStructRepr _ -> case asStruct x of@@ -3103,18 +3233,18 @@ -- | Compute the conjunction of a sequence of predicates. andAllOf :: IsExprBuilder sym          => sym-         -> Fold s (Pred sym)+         -> SimpleFold s (Pred sym)          -> s          -> IO (Pred sym)-andAllOf sym f s = foldlMOf f (andPred sym) (truePred sym) s+andAllOf sym f s = foldM (andPred sym) (truePred sym) (toListOf f s)  -- | Compute the disjunction of a sequence of predicates. orOneOf :: IsExprBuilder sym          => sym-         -> Fold s (Pred sym)+         -> SimpleFold s (Pred sym)          -> s          -> IO (Pred sym)-orOneOf sym f s = foldlMOf f (orPred sym) (falsePred sym) s+orOneOf sym f s = foldM (orPred sym) (falsePred sym) (toListOf f s)  -- | Return predicate that holds if value is non-zero. isNonZero :: IsExprBuilder sym => sym -> SymCplx sym -> IO (Pred sym)

@@ -28,11 +28,12 @@   , partitionLabeledPreds   ) where -import Control.Lens+import Lens.Micro+import Lens.Micro.Extras (view) import Data.Bifunctor.TH (deriveBifunctor, deriveBifoldable, deriveBitraversable)+import Data.Functor.Identity (Identity(..)) import Data.Data (Data) import Data.Coerce (coerce)-import Data.Data (Typeable) import Data.Eq.Deriving (deriveEq1, deriveEq2) import Data.Foldable (foldrM) import Data.Ord.Deriving (deriveOrd1, deriveOrd2)@@ -49,7 +50,7 @@        -- | Message added when assumption/assertion was made.      , _labeledPredMsg :: !msg      }-   deriving (Eq, Data, Functor, Foldable, Generic, Generic1, Ord, Show, Traversable, Typeable)+   deriving (Eq, Data, Functor, Foldable, Generic, Generic1, Ord, Show, Traversable)  $(deriveBifunctor     ''LabeledPred) $(deriveBifoldable    ''LabeledPred)

@@ -75,7 +75,7 @@ import What4.Interface (IsExprBuilder, SymExpr, IsExpr, Pred) import What4.Interface (truePred, andPred, notPred, itePred, asConstantPred) -import Control.Lens.TH (makeLenses)+import Lens.Micro.TH (makeLenses) import Data.Bifunctor.TH (deriveBifunctor, deriveBifoldable, deriveBitraversable) import Data.Eq.Deriving (deriveEq1, deriveEq2) import Data.Ord.Deriving (deriveOrd1, deriveOrd2)

@@ -33,7 +33,7 @@   ) where  import           Control.DeepSeq-import           Control.Lens+import           Lens.Micro import           Data.Text (Text) import qualified Data.Text as Text import           Data.Word

@@ -305,7 +305,8 @@      n <- popEntryStackToTop c      writeIORef (solverEarlyUnsat p) Nothing      if solverSupportsResetAssertions p then-       addCommand c (resetCommand c)+       do addCommand c (resetCommand c)+          reassertPersistentSideConditions c      else        do mapM_ (addCommand c) (popManyCommands c n)           addCommand c (pushCommand c)

@@ -24,7 +24,7 @@   ) where  import           Control.Applicative-import           Control.Lens+import           Lens.Micro import qualified Data.Attoparsec.Text as Atto import qualified Data.Map as Map import           Data.Ratio

@@ -18,7 +18,7 @@ import Control.Monad.Fail( MonadFail ) #endif -import Control.Lens (over, _1)+import Lens.Micro (over, _1) import Data.Ratio  -- | Read decimal number, returning rational and rest of string, or a failure

@@ -58,10 +58,17 @@ isTokenChar '(' = False isTokenChar ')' = False isTokenChar '"' = False+isTokenChar '|' = False  -- Reserved for quoted symbols isTokenChar c = not (isSpace c)  readToken :: Parser Text-readToken = takeWhile1 isTokenChar+readToken = quotedSymbol <|> takeWhile1 isTokenChar+  where+    quotedSymbol = do+      _ <- char '|'+      content <- takeWhile (/= '|')+      _ <- char '|'+      return content  -- | Parses an SExp.  If the input is a string (recognized by the -- 'readString' argument), return that as an 'SString'; if the input

@@ -162,7 +162,6 @@  import           GHC.Generics (Generic) import           Data.Data (Data)-import           Data.Typeable (Typeable)  import qualified Prelude import           Prelude hiding (and, or, concat, negate, div, mod, abs, not)@@ -891,7 +890,7 @@   | Version   | ErrorBehavior   | InfoKeyword Text-  deriving (Data, Eq, Ord, Generic, Show, Typeable)+  deriving (Data, Eq, Ord, Generic, Show)  flagToSExp :: SMTInfoFlag -> Text flagToSExp = (cons ':') .

@@ -64,6 +64,7 @@               )   , connState   , newWriterConn+  , reassertPersistentSideConditions   , resetEntryStack   , popEntryStackToTop   , entryStackHeight@@ -110,7 +111,8 @@ #endif  import           Control.Exception-import           Control.Lens hiding ((.>), Strict)+import           Lens.Micro+import           Lens.Micro.Mtl (use, (+=), (.=)) import           Control.Monad (forM_, unless, when) import           Control.Monad.IO.Class import           Control.Monad.Reader (ReaderT(..), asks)@@ -149,6 +151,7 @@  import           What4.BaseTypes import qualified What4.Config as CFG+import qualified What4.Domains.BV as BVD import qualified What4.Expr.ArrayUpdateMap as AUM import qualified What4.Expr.BoolMap as BM import           What4.Expr.Builder@@ -164,7 +167,6 @@ import qualified What4.SpecialFunctions as SFn import           What4.Symbol import           What4.Utils.AbstractDomains-import qualified What4.Utils.BVDomain as BVD import           What4.Utils.Complex import           What4.Utils.FloatHelpers import           What4.Utils.StringLiteral@@ -643,6 +645,12 @@              , consumeAcknowledgement :: AcknowledgementAction t h                -- ^ Consume an acknowledgement notifications the solver, if                --   it produces one+             , persistentSideConditions :: !(IORef [Term h])+               -- ^ Persistent side conditions that must be re-asserted after+               --   a @(reset-assertions)@ command. These arise from+               --   'addPartialSideCond' for variables cached with+               --   'DeleteNever', whose cache entries survive a reset but whose+               --   solver-level assertions do not.              }  -- | An action for consuming an acknowledgement message from the solver,@@ -729,6 +737,7 @@   entry <- newStackEntry   stk_ref <- newIORef [entry]   r <- newIORef emptyState+  scRef <- newIORef []   return $! WriterConn { smtWriterName = solver_name                        , connHandle    = h                        , connInputHandle = in_h@@ -742,6 +751,7 @@                        , varBindings  = bindings                        , connState    = cs                        , consumeAcknowledgement = ack+                       , persistentSideConditions = scRef                        }  -- | Strictness level for parsing solver responses.@@ -1075,6 +1085,16 @@       addCommand conn $ declareCommand conn var_name Ctx.empty smt_type       cacheValueExpr conn (bvarId var) DeleteOnPop $ SMTName smt_type var_name +-- | Re-assert all persistent side conditions that were recorded by 'addPartialSideCond'.+--+-- See 'persistentSideConditions' for more details.+reassertPersistentSideConditions :: SMTWriter h => WriterConn t h -> IO ()+reassertPersistentSideConditions conn = do+  conds <- readIORef (persistentSideConditions conn)+  -- This adds them back in the reverse order they were originally added, but+  -- that shouldn't matter semantically.+  mapM_ (assumeFormula conn) conds+ -- | Assume that the given formula holds. assumeFormula :: SMTWriter h => WriterConn t h -> Term h -> IO () assumeFormula c p = addCommand c (assertCommand c p)@@ -1343,6 +1363,10 @@   where tp = smtExprType t  -- | Assert a predicate holds as a side condition to some formula.+--+-- For conditions that must persist across resets (e.g., constraints on+-- 'DeleteNever' variables), use 'addPersistentSideCondition' or+-- 'addPartialSideCond' instead. addSideCondition ::    String {- ^ Reason that condition is being added. -} ->    Term h {- ^ Predicate that should hold. -} ->@@ -1358,6 +1382,23 @@      fail $ "Cannot add a side condition within a function needed to define the "        ++ nm ++ " term created at " ++ show loc ++ "." +-- | Add a persistent side condition that will be re-asserted after reset.+--+-- This is specifically for side conditions on DeleteNever variables (like+-- UninterpVarKind variables from freshNat, freshConstant, etc.) whose+-- constraints must persist across reset. See 'persistentSideConditions'.+addPersistentSideCondition ::+   SMTWriter h =>+   WriterConn t h ->+   String {- ^ Reason that condition is being added. -} ->+   Term h {- ^ Predicate that should hold. -} ->+   SMTCollector t h ()+addPersistentSideCondition conn nm t = do+  addSideCondition nm t+  liftIO $ modifyIORef' (persistentSideConditions conn) (t:)++-- | Add side conditions arising from the abstract value of a fresh variable via+-- 'addPersistentSideCondition'. addPartialSideCond ::   forall t h tp.   SMTWriter h =>@@ -1371,53 +1412,53 @@ addPartialSideCond _ _ _ Nothing = return ()  addPartialSideCond _ _ BoolTypeMap (Just Nothing) = return ()-addPartialSideCond _ t BoolTypeMap (Just (Just b)) =+addPartialSideCond conn t BoolTypeMap (Just (Just b)) =    -- This is a weird case, but technically possible, so...-  addSideCondition "bool_val" $ t .== boolExpr b+  addPersistentSideCondition conn "bool_val" $ t .== boolExpr b -addPartialSideCond _ t IntegerTypeMap (Just rng) =+addPartialSideCond conn t IntegerTypeMap (Just rng) =   do case rangeLowBound rng of        Unbounded -> return ()-       Inclusive lo -> addSideCondition "int_range" $ t .>= integerTerm lo+       Inclusive lo -> addPersistentSideCondition conn "int_range" $ t .>= integerTerm lo      case rangeHiBound rng of        Unbounded -> return ()-       Inclusive hi -> addSideCondition "int_range" $ t .<= integerTerm hi+       Inclusive hi -> addPersistentSideCondition conn "int_range" $ t .<= integerTerm hi -addPartialSideCond _ t RealTypeMap (Just rng) =+addPartialSideCond conn t RealTypeMap (Just rng) =   do case rangeLowBound (ravRange rng) of        Unbounded -> return ()-       Inclusive lo -> addSideCondition "real_range" $ t .>= rationalTerm lo+       Inclusive lo -> addPersistentSideCondition conn "real_range" $ t .>= rationalTerm lo      case rangeHiBound (ravRange rng) of        Unbounded -> return ()-       Inclusive hi -> addSideCondition "real_range" $ t .<= rationalTerm hi+       Inclusive hi -> addPersistentSideCondition conn "real_range" $ t .<= rationalTerm hi -addPartialSideCond _ t (BVTypeMap w) (Just (BVD.BVDArith rng)) = assertRange (BVD.arithDomainData rng)+addPartialSideCond conn t (BVTypeMap w) (Just (BVD.BVDArith rng)) = assertRange (BVD.arithDomainData rng)    where    assertRange Nothing = return ()    assertRange (Just (lo, sz)) =-     addSideCondition "bv_range" $ bvULe (bvSub t (bvTerm w (BV.mkBV w lo))) (bvTerm w (BV.mkBV w sz))+     addPersistentSideCondition conn "bv_range" $ bvULe (bvSub t (bvTerm w (BV.mkBV w lo))) (bvTerm w (BV.mkBV w sz)) -addPartialSideCond _ t (BVTypeMap w) (Just (BVD.BVDBitwise rng)) = assertBitRange (BVD.bitbounds rng)+addPartialSideCond conn t (BVTypeMap w) (Just (BVD.BVDBitwise rng)) = assertBitRange (BVD.bitbounds rng)    where    assertBitRange (lo, hi) = do      when (lo > 0) $-       addSideCondition "bv_bitrange" $ (bvOr (bvTerm w (BV.mkBV w lo)) t) .== t+       addPersistentSideCondition conn "bv_bitrange" $ (bvOr (bvTerm w (BV.mkBV w lo)) t) .== t      when (hi < maxUnsigned w) $-       addSideCondition "bv_bitrange" $ (bvOr t (bvTerm w (BV.mkBV w hi))) .== (bvTerm w (BV.mkBV w hi))+       addPersistentSideCondition conn "bv_bitrange" $ (bvOr t (bvTerm w (BV.mkBV w hi))) .== (bvTerm w (BV.mkBV w hi)) -addPartialSideCond _ t (UnicodeTypeMap) (Just (StringAbs len)) =+addPartialSideCond conn t (UnicodeTypeMap) (Just (StringAbs len)) =   do case rangeLowBound len of        Inclusive lo ->-          addSideCondition "string length low range" $+          addPersistentSideCondition conn "string length low range" $              integerTerm (max 0 lo) .<= stringLength @h t        Unbounded ->-          addSideCondition "string length low range" $+          addPersistentSideCondition conn "string length low range" $              integerTerm 0 .<= stringLength @h t       case rangeHiBound len of        Unbounded -> return ()        Inclusive hi ->-         addSideCondition "string length high range" $+         addPersistentSideCondition conn "string length high range" $            stringLength @h t .<= integerTerm hi  addPartialSideCond _ _ (FloatTypeMap _) (Just ()) = return ()@@ -2636,6 +2677,7 @@       xe <- mkBaseExpr x       freshBoundTerm (BVTypeMap w) $ floatToSBV (natValue w) r xe     FloatToReal x -> do+      checkLinearSupport i       xe <- mkBaseExpr x       freshBoundTerm RealTypeMap $ floatToReal xe     FloatSpecialFunction{} -> unsupportedTerm i

@@ -18,6 +18,8 @@     -- * Constants   , fpFresh   , fpNaN+  , fpPosZero+  , fpNegZero   , fpPosInf   , fpNegInf   , fpFromLit@@ -30,9 +32,14 @@     -- * Relations   , SFloatRel   , fpEq+  , fpNe   , fpEqIEEE+  , fpNeIEEE+  , fpLeIEEE   , fpLtIEEE+  , fpGeIEEE   , fpGtIEEE+  , fpUnordered      -- * Arithmetic   , SFloatBinArith@@ -43,6 +50,7 @@   , fpSub   , fpMul   , fpDiv+  , fpRem   , fpMin   , fpMax   , fpFMA@@ -54,12 +62,18 @@   , fpFromRational   , fpToRational   , fpFromInteger+  , fpCast+  , fpFromBV+  , fpFromSBV+  , fpToBV+  , fpToSBV      -- * Queries   , fpIsInf   , fpIsNaN   , fpIsZero   , fpIsNeg+  , fpIsPos   , fpIsSubnorm   , fpIsNorm @@ -70,6 +84,7 @@  import Control.Exception import LibBF (BigFloat)+import Numeric.Natural  import Data.Parameterized.Some import Data.Parameterized.NatRepr@@ -150,13 +165,14 @@   case exprType f of     BaseFloatRepr (FloatingPointPrecisionRepr e p) -> (intValue e, intValue p) +-- | See 'asFloat'. fpAsLit :: SFloat sym -> Maybe BigFloat fpAsLit (SFloat f) = asFloat f  -------------------------------------------------------------------------------- -- Constants --- | A fresh variable of the given type.+-- | A fresh variable of the given type (see 'freshConstant'). fpFresh ::   IsSymExprBuilder sym =>   sym ->@@ -168,7 +184,7 @@     SFloat <$> freshConstant sym emptySymbol (BaseFloatRepr fpp)   | otherwise = unsupported "fpFresh" e p --- | Not a number+-- | Not a number (see 'floatNaN'). fpNaN ::   IsExprBuilder sym =>   sym ->@@ -179,8 +195,29 @@   | Just (Some fpp) <- fpRepr e p = SFloat <$> floatNaN sym fpp   | otherwise = unsupported "fpNaN" e p +-- | Positive zero (see 'floatPZero').+fpPosZero ::+  IsExprBuilder sym =>+  sym ->+  Integer {- ^ Exponent width -} ->+  Integer {- ^ Precision width -} ->+  IO (SFloat sym)+fpPosZero sym e p+  | Just (Some fpp) <- fpRepr e p = SFloat <$> floatPZero sym fpp+  | otherwise = unsupported "fpPosZero" e p --- | Positive infinity+-- | Negative zero (see 'floatNZero').+fpNegZero ::+  IsExprBuilder sym =>+  sym ->+  Integer {- ^ Exponent width -} ->+  Integer {- ^ Precision width -} ->+  IO (SFloat sym)+fpNegZero sym e p+  | Just (Some fpp) <- fpRepr e p = SFloat <$> floatNZero sym fpp+  | otherwise = unsupported "fpNegZero" e p++-- | Positive infinity (see 'floatPInf'). fpPosInf ::   IsExprBuilder sym =>   sym ->@@ -191,7 +228,7 @@   | Just (Some fpp) <- fpRepr e p = SFloat <$> floatPInf sym fpp   | otherwise = unsupported "fpPosInf" e p --- | Negative infinity+-- | Negative infinity (see 'floatNInf'). fpNegInf ::   IsExprBuilder sym =>   sym ->@@ -203,7 +240,8 @@   | otherwise = unsupported "fpNegInf" e p  --- | A floating point number corresponding to the given BigFloat.+-- | A floating point number corresponding to the given BigFloat (see+-- 'floatLit'). fpFromLit ::   IsExprBuilder sym =>   sym ->@@ -215,7 +253,8 @@   | Just (Some fpp) <- fpRepr e p = SFloat <$> floatLit sym fpp f   | otherwise = unsupported "fpFromLit" e p --- | A floating point number corresponding to the given rational.+-- | A floating point number corresponding to the given rational (see+-- 'floatLitRational'). fpFromRationalLit ::   IsExprBuilder sym =>   sym ->@@ -228,7 +267,8 @@   | otherwise = unsupported "fpFromRationalLit" e p  --- | Make a floating point number with the given bit representation.+-- | Make a floating point number with the given bit representation (see+-- 'floatFromBinary'). fpFromBinary ::   IsExprBuilder sym =>   sym ->@@ -250,6 +290,7 @@         | otherwise -> panic "fpFromBits" [ "1 >= 2" ]   | otherwise = unsupported "fpFromBits" e p +-- | See 'floatToBinary'. fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym) fpToBinary sym (SFloat f)   | FloatingPointPrecisionRepr e p <- fpReprOf sym f@@ -261,12 +302,15 @@ -------------------------------------------------------------------------------- -- Arithmetic +-- | See 'floatNeg'. fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym) fpNeg sym (SFloat fl) = SFloat <$> floatNeg sym fl +-- | See 'floatAbs'. fpAbs :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym) fpAbs sym (SFloat fl) = SFloat <$> floatAbs sym fl +-- | See 'floatSqrt'. fpSqrt :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym) fpSqrt sym r (SFloat fl) = SFloat <$> floatSqrt sym r fl @@ -291,18 +335,33 @@ type SFloatBinArith sym =   sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym) +-- | See 'floatAdd'. fpAdd :: IsExprBuilder sym => SFloatBinArith sym fpAdd = fpBinArith floatAdd +-- | See 'floatSub'. fpSub :: IsExprBuilder sym => SFloatBinArith sym fpSub = fpBinArith floatSub +-- | See 'floatMul'. fpMul :: IsExprBuilder sym => SFloatBinArith sym fpMul = fpBinArith floatMul +-- | See 'floatDiv'. fpDiv :: IsExprBuilder sym => SFloatBinArith sym fpDiv = fpBinArith floatDiv +-- | See 'floatRem'.+fpRem :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)+fpRem sym (SFloat x) (SFloat y) =+  let t1 = sym `fpReprOf` x+      t2 = sym `fpReprOf` y+  in+  case testEquality t1 t2 of+    Just Refl -> SFloat <$> floatRem sym x y+    _         -> fpTypeError t1 t2++-- | See 'floatMin'. fpMin :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) fpMin sym (SFloat x) (SFloat y) =   let t1 = sym `fpReprOf` x@@ -312,6 +371,7 @@     Just Refl -> SFloat <$> floatMin sym x y     _         -> fpTypeError t1 t2 +-- | See 'floatMax'. fpMax :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) fpMax sym (SFloat x) (SFloat y) =   let t1 = sym `fpReprOf` x@@ -321,6 +381,7 @@     Just Refl -> SFloat <$> floatMax sym x y     _         -> fpTypeError t1 t2 +-- | See 'floatRMA'. fpFMA :: IsExprBuilder sym =>   sym -> RoundingMode -> SFloat sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) fpFMA sym r (SFloat x) (SFloat y) (SFloat z) =@@ -333,6 +394,7 @@      (Nothing, _) -> fpTypeError t1 t2      (_, Nothing) -> fpTypeError t2 t3 +-- | See 'floatIte'. fpIte :: IsExprBuilder sym =>   sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) fpIte sym p (SFloat x) (SFloat y) =@@ -368,28 +430,53 @@ type SFloatRel sym =   sym -> SFloat sym -> SFloat sym -> IO (Pred sym) +-- | See 'floatEq'. fpEq :: IsExprBuilder sym => SFloatRel sym fpEq = fpRel floatEq +-- | See 'floatNe'.+fpNe :: IsExprBuilder sym => SFloatRel sym+fpNe = fpRel floatNe++-- | See 'floatFpEq'. fpEqIEEE :: IsExprBuilder sym => SFloatRel sym fpEqIEEE = fpRel floatFpEq +-- | See 'floatFpApart'.+fpNeIEEE :: IsExprBuilder sym => SFloatRel sym+fpNeIEEE = fpRel floatFpApart++-- | See 'floatLe'.+fpLeIEEE :: IsExprBuilder sym => SFloatRel sym+fpLeIEEE = fpRel floatLe++-- | See 'floatLt'. fpLtIEEE :: IsExprBuilder sym => SFloatRel sym fpLtIEEE = fpRel floatLt +-- | See 'floatGe'.+fpGeIEEE :: IsExprBuilder sym => SFloatRel sym+fpGeIEEE = fpRel floatGe++-- | See 'floatGt'. fpGtIEEE :: IsExprBuilder sym => SFloatRel sym fpGtIEEE = fpRel floatGt +-- | See 'floatFpUnordered'.+fpUnordered :: IsExprBuilder sym => SFloatRel sym+fpUnordered = fpRel floatFpUnordered  --------------------------------------------------------------------------------+-- | See 'floatRound'. fpRound ::   IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym) fpRound sym r (SFloat x) = SFloat <$> floatRound sym r x --- | This is undefined on "special" values (NaN,infinity)+-- | See 'floatToReal'. This is undefined on "special" values (NaN,infinity) fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym) fpToReal sym (SFloat x) = floatToReal sym x +-- | See 'realToFloat'. fpFromReal ::   IsExprBuilder sym =>   sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym)@@ -427,29 +514,95 @@   do r    <- fpToReal sym fp      x    <- freshConstant sym emptySymbol BaseIntegerRepr      y    <- freshConstant sym emptySymbol BaseIntegerRepr+     one  <- intLit sym 1+     -- Avoid rationals with zero denominators, which are invalid.+     yPos <- intLt sym one y      num  <- integerToReal sym x      den  <- integerToReal sym y      res  <- realDiv sym num den      same <- realEq sym r res-     pure (same, x, y)+     rel  <- andPred sym yPos same+     pure (rel, x, y) +-- | Change the precision of a floating point number (see 'floatCast').+fpCast ::+  IsExprBuilder sym =>+  sym -> Integer -> Integer -> RoundingMode -> SFloat sym -> IO (SFloat sym)+fpCast sym e p r (SFloat x)+  | Just (Some repr) <- fpRepr e p = SFloat <$> floatCast sym repr r x+  | otherwise = unsupported "fpFromReal" e p +-- | Convert a unsigned bitvector to a floating point number (see 'bvToFloat').+fpFromBV ::+  IsExprBuilder sym =>+  sym -> Integer -> Integer -> RoundingMode -> SWord sym -> IO (SFloat sym)+fpFromBV sym e p r swe+  | DBV sw <- swe+  , Just (Some fpp) <- fpRepr e p =+    SFloat <$> bvToFloat sym fpp r sw+  | otherwise = unsupported "fpFromBV" e p +-- | Convert a signed bitvector to a floating point number (see 'sbvToFloat').+fpFromSBV ::+  IsExprBuilder sym =>+  sym -> Integer -> Integer -> RoundingMode -> SWord sym -> IO (SFloat sym)+fpFromSBV sym e p r swe+  | DBV sw <- swe+  , Just (Some fpp) <- fpRepr e p =+    SFloat <$> sbvToFloat sym fpp r sw+  | otherwise = unsupported "fpFromSBV" e p++-- | Convert a floating point number to a unsigned bitvector (see 'floatToBV').+-- Precondition: the supplied 'Natural' (the bit width of the returned+-- bitvector) is non-zero.+fpToBV ::+  IsExprBuilder sym =>+  sym -> Natural -> RoundingMode -> SFloat sym -> IO (SWord sym)+fpToBV sym n r (SFloat x) =+  case mkNatRepr n of+    Some nr ->+      case isPosNat nr of+        Nothing -> panic "fpToBV" ["bit width must be non-zero"]+        Just LeqProof -> DBV <$> floatToBV sym nr r x++-- | Convert a floating point number to a signed bitvector (see 'floatToSBV').+-- Precondition: the supplied 'Natural' (the bit width of the returned+-- bitvector) is non-zero.+fpToSBV ::+  IsExprBuilder sym =>+  sym -> Natural -> RoundingMode -> SFloat sym -> IO (SWord sym)+fpToSBV sym n r (SFloat x) =+  case mkNatRepr n of+    Some nr ->+      case isPosNat nr of+        Nothing -> panic "fpToSBV" ["bit width must be non-zero"]+        Just LeqProof -> DBV <$> floatToSBV sym nr r x+ --------------------------------------------------------------------------------+-- | See 'floatIsInf'. fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) fpIsInf sym (SFloat x) = floatIsInf sym x +-- | See 'floatIsNaN'. fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) fpIsNaN sym (SFloat x) = floatIsNaN sym x +-- | See 'floatIsZero'. fpIsZero :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) fpIsZero sym (SFloat x) = floatIsZero sym x +-- | See 'floatIsNeg'. fpIsNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) fpIsNeg sym (SFloat x) = floatIsNeg sym x +-- | See 'floatIsPos'.+fpIsPos :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)+fpIsPos sym (SFloat x) = floatIsPos sym x++-- | See 'floatIsSubnorm'. fpIsSubnorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) fpIsSubnorm sym (SFloat x) = floatIsSubnorm sym x +-- | See 'floatIsNorm'. fpIsNorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) fpIsNorm sym (SFloat x) = floatIsNorm sym x

@@ -28,7 +28,7 @@  import           Control.Concurrent import           Control.Exception-import           Control.Lens(folded)+import           Lens.Micro(folded) import           Control.Monad import           Data.Attoparsec.ByteString.Char8 hiding (try) import           Data.ByteString (ByteString)

@@ -72,7 +72,7 @@ import           Control.Concurrent.Async ( race ) import           Control.Exception                    (assert, SomeException(..), tryJust, throw, displayException, Exception(..))-import           Control.Lens ((^.), folded)+import           Lens.Micro ((^.), folded) import           Control.Monad import           Control.Monad.Identity import qualified Data.Attoparsec.Text as Atto@@ -1001,6 +1001,10 @@       t = mkTmout yicesGoalTimeout   in [ p, m, i, t      , copyOpt (const $ configOptionText yicesStrictParsing) strictSMTParseOpt+       -- Make sure to also include the original 'strictSMTParseOpt'. Since+       -- Yices doesn't inherit the 'smtlib2Options' like other solvers do, we+       -- have to include this option explicitly.+     , strictSMTParseOpt      , deprecatedOpt [p] $ mkPath yicesPathOLD      , deprecatedOpt [m] $ mkMCSat yicesEnableMCSatOLD      , deprecatedOpt [i] $ mkIntr yicesEnableInteractiveOLD

@@ -108,8 +108,8 @@ import           Data.Ratio (denominator)  import           What4.BaseTypes-import           What4.Utils.BVDomain (BVDomain)-import qualified What4.Utils.BVDomain as BVD+import           What4.Domains.BV (BVDomain)+import qualified What4.Domains.BV as BVD import           What4.Utils.Complex import           What4.Utils.StringLiteral @@ -692,7 +692,7 @@     BaseRealRepr    -> ravUnbounded     BaseComplexRepr -> ravUnbounded :+ ravUnbounded     BaseStringRepr _ -> stringAbsTop-    BaseBVRepr w    -> BVD.any w+    BaseBVRepr w    -> BVD.top w     BaseFloatRepr{} -> ()     BaseArrayRepr _a b -> avTop b     BaseStructRepr flds -> fmapFC (\etp -> AbstractValueWrapper (avTop etp)) flds@@ -768,7 +768,7 @@  -- Bitvectors always have a lower and upper bound (represented as unsigned numbers) instance (1 <= w) => Abstractable (BaseBVType w) where-  avJoin (BaseBVRepr _) = BVD.union+  avJoin (BaseBVRepr _) = BVD.join   avOverlap _ = BVD.domainsOverlap   avCheckEq _ = BVD.eq 

@@ -143,8 +143,11 @@   | f x y = listEqBy f xs ys listEqBy _ _ _ = False -eqBy :: Eq k => (a -> a -> Bool) -> AnnotatedMap k v a -> AnnotatedMap k v a -> Bool-eqBy f x y = listEqBy (\(kx,ax) (ky,ay) -> kx == ky && f ax ay) (toList x) (toList y)+eqBy :: (Eq k, Ord k, Semigroup v) => (a -> a -> Bool) -> AnnotatedMap k v a -> AnnotatedMap k v a -> Bool+eqBy f x y =+  -- optimization for a common case: sizes not equal+  size x == size y &&+    listEqBy (\(kx,ax) (ky,ay) -> kx == ky && f ax ay) (toList x) (toList y)  null :: AnnotatedMap k v a -> Bool null (AnnotatedMap ft) = FT.null ft

@@ -8,12 +8,14 @@ -- Stability        : provisional ------------------------------------------------------------------------ {-# LANGUAGE BangPatterns #-}-{-# LANGUAGE CPP #-} module What4.Utils.Arithmetic   ( -- * Arithmetic utilities     isPow2+  , isPow2Integer   , lg+  , intLog2   , lgCeil+  , intLogCeil   , nextMultiple   , nextPow2Multiple   , tryIntSqrt@@ -31,40 +33,64 @@  import Data.Parameterized.NatRepr +import What4.Domains.Arithmetic.Internal+  ( ctzOpt, clzOpt, intLog2Opt, isPow2IntegerOpt )+ -- | Returns true if number is a power of two. isPow2 :: (Bits a, Num a) => a -> Bool isPow2 x = x .&. (x-1) == 0 --- | Returns floor of log base 2.+-- | Returns true if Integer is a power of two. On GHC 9.0+ this uses a fast+-- primop from @ghc-bignum@; on earlier GHCs it falls back to 'isPow2'.+isPow2Integer :: Integer -> Bool+isPow2Integer = isPow2IntegerOpt+{-# INLINE isPow2Integer #-}++-- | Returns floor of log base 2. Polymorphic over bit-like types.+--+-- Note: For @Integer@ specifically, prefer 'intLog2' which uses fast primops+-- on GHC 9.0+. lg :: (Bits a, Num a, Ord a) => a -> Int lg i0 | i0 > 0 = go 0 (i0 `shiftR` 1)       | otherwise = error "lg given number that is not positive."   where go r 0 = r         go r n = go (r+1) (n `shiftR` 1) --- | Returns ceil of log base 2.---   We define @lgCeil 0 = 0@+-- | @intLog2 n@ for @n >= 1@: floor of base-2 logarithm. Undefined for+-- @n <= 0@. On GHC 9.0+ this delegates to a fast primop in @ghc-bignum@;+-- on earlier GHCs it falls back to 'lg'.+intLog2 :: Integer -> Int+intLog2 = intLog2Opt+{-# INLINE intLog2 #-}++-- | Returns ceil of log base 2. Polymorphic over bit-like types.+--   We define @lgCeil 0 = 0@ and @lgCeil 1 = 0@.+--+-- Note: For @Integer@ specifically, prefer 'intLogCeil' which uses fast primops+-- on GHC 9.0+. lgCeil :: (Bits a, Num a, Ord a) => a -> Int lgCeil 0 = 0 lgCeil 1 = 0 lgCeil i | i > 1 = 1 + lg (i-1)          | otherwise = error "lgCeil given number that is not positive." +-- | @intLogCeil n@ for @n >= 0@: ceiling of base-2 logarithm. We define+-- @intLogCeil 0 = 0@ and @intLogCeil 1 = 0@. On GHC 9.0+ this uses fast primops+-- from @ghc-bignum@; on earlier GHCs it falls back to 'lgCeil'.+intLogCeil :: Integer -> Int+intLogCeil 0 = 0+intLogCeil 1 = 0+intLogCeil i | i > 1 = 1 + intLog2 (i - 1)+             | otherwise = error "intLogCeil given number that is not positive."+{-# INLINE intLogCeil #-}+ -- | Count trailing zeros ctz :: NatRepr w -> Integer -> Integer-ctz w x = go 0- where- go !i-   | i < toInteger (natValue w) && testBit x (fromInteger i) == False = go (i+1)-   | otherwise = i+ctz = ctzOpt  -- | Count leading zeros clz :: NatRepr w -> Integer -> Integer-clz w x = go 0- where- go !i-   | i < toInteger (natValue w) && testBit x (widthVal w - fromInteger i - 1) == False = go (i+1)-   | otherwise = i+clz = clzOpt  rotateRight ::   NatRepr w {- ^ width -} ->

@@ -1,880 +1,5 @@-{-|-Module      : What4.Utils.BVDomain-Description : Abstract domains for bitvectors-Copyright   : (c) Galois Inc, 2019-2020-License     : BSD3-Maintainer  : huffman@galois.com--Provides an implementation of abstract domains for bitvectors.-This abstract domain has essentially two modes: arithmetic-and bitvector modes. The arithmetic mode is a fairly straightforward-interval domain, albeit one that is carefully implemented to deal-properly with intervals that "cross zero", as is relatively common-when using 2's complement signed representations. The bitwise-mode tracks the values of individual bits independently in a-3-valued logic (true, false or unknown).  The abstract domain-transitions between the two modes when necessary, but attempts-to retain as much precision as possible.--The operations of these domains are formalized in the companion-Cryptol files found together in this package under the \"doc\"-directory, and their soundness properties stated and established.--}--{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE ViewPatterns #-}--module What4.Utils.BVDomain-  ( -- * Bitvector abstract domains-    BVDomain(..)-  , proper-  , member-  , size-    -- ** Domain transfer functions-  , asArithDomain-  , asBitwiseDomain-  , asXorDomain-  , fromXorDomain-  , arithToXorDomain-  , bitwiseToXorDomain-  , xorToBitwiseDomain-    -- ** Projection functions-  , asSingleton-  , eq-  , slt-  , ult-  , testBit-  , domainsOverlap-  , ubounds-  , sbounds-  , isUltSumCommonEquiv-  , A.arithDomainData-  , B.bitbounds-    -- * Operations-  , any-  , singleton-  , range-  , fromAscEltList-  , union-  , concat-  , select-  , zext-  , sext-    -- ** Shifts and rotates-  , shl-  , lshr-  , ashr-  , rol-  , ror-    -- ** Arithmetic-  , add-  , negate-  , scale-  , mul-  , udiv-  , urem-  , sdiv-  , srem-    -- ** Bitwise-  , What4.Utils.BVDomain.not-  , and-  , or-  , xor--    -- ** Misc-  , popcnt-  , clz-  , ctz--    -- * Useful bitvector computations-  , bitwiseRoundAbove-  , bitwiseRoundBetween--    -- * Correctness properties-  , genDomain-  , genElement-  , genPair--  , correct_arithToBitwise-  , correct_bitwiseToArith-  , correct_bitwiseToXorDomain-  , correct_arithToXorDomain-  , correct_xorToBitwiseDomain-  , correct_asXorDomain-  , correct_fromXorDomain--  , correct_bra1-  , correct_bra2-  , correct_brb1-  , correct_brb2--  , correct_any-  , correct_ubounds-  , correct_sbounds-  , correct_singleton-  , correct_overlap-  , precise_overlap-  , correct_union-  , correct_zero_ext-  , correct_sign_ext-  , correct_concat-  , correct_select-  , correct_add-  , correct_neg-  , correct_mul-  , correct_scale-  , correct_udiv-  , correct_urem-  , correct_sdiv-  , correct_srem-  , correct_shl-  , correct_lshr-  , correct_ashr-  , correct_rol-  , correct_ror-  , correct_eq-  , correct_ult-  , correct_slt-  , correct_and-  , correct_or-  , correct_not-  , correct_xor-  , correct_testBit-  , correct_popcnt-  , correct_clz-  , correct_ctz+module What4.Utils.BVDomain {-# DEPRECATED "Use What4.Domains.BV instead" #-}+  ( module What4.Domains.BV   ) where -import qualified Data.Bits as Bits-import           Data.Bits hiding (testBit, xor)-import qualified Data.List as List-import           Data.Parameterized.NatRepr-import           Numeric.Natural-import           GHC.TypeNats-import           GHC.Stack--import qualified Prelude-import           Prelude hiding (any, concat, negate, and, or, not)--import qualified What4.Utils.Arithmetic as Arith--import qualified What4.Utils.BVDomain.Arith as A-import qualified What4.Utils.BVDomain.Bitwise as B-import qualified What4.Utils.BVDomain.XOR as X--import           Test.Verification ( Property, property, (==>), Gen, chooseBool )---arithToBitwiseDomain :: A.Domain w -> B.Domain w-arithToBitwiseDomain a =-  let mask = A.bvdMask a in-  case A.arithDomainData a of-    Nothing -> B.interval mask 0 mask-    Just (alo,_) -> B.interval mask lo hi-      where-        u = A.unknowns a-        hi = alo .|. u-        lo = hi `Bits.xor` u--bitwiseToArithDomain :: B.Domain w -> A.Domain w-bitwiseToArithDomain b = A.interval mask lo ((hi - lo) .&. mask)-  where-  mask = B.bvdMask b-  (lo,hi) = B.bitbounds b--bitwiseToXorDomain :: B.Domain w -> X.Domain w-bitwiseToXorDomain b = X.interval mask lo hi-  where-  mask = B.bvdMask b-  (lo,hi) = B.bitbounds b--arithToXorDomain :: A.Domain w -> X.Domain w-arithToXorDomain a =-  let mask = A.bvdMask a in-  case A.arithDomainData a of-    Nothing -> X.BVDXor mask mask mask-    Just (alo,_) -> X.BVDXor mask hi u-      where-        u = A.unknowns a-        hi = alo .|. u--xorToBitwiseDomain :: X.Domain w -> B.Domain w-xorToBitwiseDomain x = B.interval mask lo hi-  where-  mask = X.bvdMask x-  (lo, hi) = X.bitbounds x--asXorDomain :: BVDomain w -> X.Domain w-asXorDomain (BVDArith a) = arithToXorDomain a-asXorDomain (BVDBitwise b) = bitwiseToXorDomain b--fromXorDomain :: X.Domain w -> BVDomain w-fromXorDomain x = BVDBitwise (xorToBitwiseDomain x)--asArithDomain :: BVDomain w -> A.Domain w-asArithDomain (BVDArith a)   = a-asArithDomain (BVDBitwise b) = bitwiseToArithDomain b--asBitwiseDomain :: BVDomain w -> B.Domain w-asBitwiseDomain (BVDArith a)   = arithToBitwiseDomain a-asBitwiseDomain (BVDBitwise b) = b------------------------------------------------------------------------------------- BVDomain definition---- | A value of type @'BVDomain' w@ represents a set of bitvectors of--- width @w@. A BVDomain represents either an arithmetic interval, or--- a bitwise interval.--data BVDomain (w :: Nat)-  = BVDArith !(A.Domain w)-  | BVDBitwise !(B.Domain w)-  deriving Show---- | Return the bitvector mask value from this domain-bvdMask :: BVDomain w -> Integer-bvdMask x =-  case x of-    BVDArith a   -> A.bvdMask a-    BVDBitwise b -> B.bvdMask b---- | Test if the domain satisfies its invariants-proper :: NatRepr w -> BVDomain w -> Bool-proper w (BVDArith a) = A.proper w a-proper w (BVDBitwise b) = B.proper w b---- | Test if the given integer value is a member of the abstract domain-member :: BVDomain w -> Integer -> Bool-member (BVDArith a) x = A.member a x-member (BVDBitwise a) x = B.member a x---- | Compute how many concrete elements are in the abstract domain-size :: BVDomain w -> Integer-size (BVDArith a)   = A.size a-size (BVDBitwise b) = B.size b---- | Generate a random nonempty domain-genDomain :: NatRepr w -> Gen (BVDomain w)-genDomain w =-  do b <- chooseBool-     if b then-       BVDArith <$> A.genDomain w-     else-       BVDBitwise <$> B.genDomain w---- | Generate a random element from a domain, which---   is assumed to be nonempty-genElement :: BVDomain w -> Gen Integer-genElement (BVDArith a) = A.genElement a-genElement (BVDBitwise b) = B.genElement b---- | Generate a random nonempty domain and an element---   contained in that domain.-genPair :: NatRepr w -> Gen (BVDomain w, Integer)-genPair w =-  do a <- genDomain w-     x <- genElement a-     return (a,x)------------------------------------------------------------------------------------- Projection functions---- | Return value if this is a singleton.-asSingleton :: BVDomain w -> Maybe Integer-asSingleton (BVDArith a)   = A.asSingleton a-asSingleton (BVDBitwise b) = B.asSingleton b--{- |- Precondition: @x <= lomask@.  Find the (arithmetically) smallest- @z@ above @x@ which is bitwise above @lomask@.  In other words- find the smallest @z@ such that @x <= z@ and @lomask .|. z == z@.--}-bitwiseRoundAbove ::-  Integer {- ^ @bvmask@, based on the width of the bitvectors in question -} ->-  Integer {- ^ @x@ -} ->-  Integer {- ^ @lomask@ -} ->-  Integer-bitwiseRoundAbove bvmask x lomask = upperbits .|. lowerbits-  where-  upperbits = x .&. (bvmask `Bits.xor` fillmask)-  lowerbits = lomask .&. fillmask-  fillmask = A.fillright ((x .|. lomask) `Bits.xor` x)--{- |- Precondition: @lomask <= x <= himask@ and @lomask .|. himask == himask@.- Find the (arithmetically) smallest @z@ above @x@ which is bitwise between- @lomask@ and @himask@.  In other words, find the smallest @z@ such that- @x <= z@ and @lomask .|. z = z@ and @z .|. himask == himask@.--}-bitwiseRoundBetween ::-  Integer {- ^ @bvmask@, based on the width of the bitvectors in question -} ->-  Integer {- ^ @x@ -} ->-  Integer {- ^ @lomask@ -} ->-  Integer {- ^ @himask@ -} ->-  Integer-bitwiseRoundBetween bvmask x lomask himask = final-  -- read these steps bottom up...-  where-  -- Finally mask out the low bits and only set those required by the lomask-  final = (upper .&. (lobits `Bits.xor` bvmask)) .|. lomask--  -- add the correcting bit and mask out any extraneous bits set in-  -- the previous step-  upper = (z + highbit) .&. himask--  -- set ourselves up so that when we add the high bit to correct,-  -- the carry will ripple until it finds a bit position that we-  -- are allowed to set.-  z = loup .|. himask'--  -- isolate just the highest incorrect bit-  highbit = rmask `Bits.xor` lobits--  -- a mask for all the bits to the right of the highest incorrect bit-  lobits = rmask `shiftR` 1--  -- set all the bits to the right of the highest incorrect bit-  rmask = A.fillright r--  -- now, compute all the bits that are set, but are not-  -- allowed to be set according to the himask-  r = loup .&. himask'--  -- complement of the highmask-  himask' = himask `Bits.xor` bvmask--  -- first, round up to the lomask-  loup = bitwiseRoundAbove bvmask x lomask----- | Test if an arithmetic domain overlaps with a bitwise domain-mixedDomainsOverlap :: A.Domain a -> B.Domain b -> Bool-mixedDomainsOverlap a b =-   case A.arithDomainData a of-     Nothing -> B.nonempty b-     Just (alo,_) ->-       let (lomask,himask) = B.bitbounds b-           brb = bitwiseRoundBetween (A.bvdMask a) alo lomask himask-        in B.nonempty b && (A.member a lomask || A.member a himask || A.member a brb)----- | Return true if domains contain a common element.-domainsOverlap :: BVDomain w -> BVDomain w -> Bool-domainsOverlap (BVDBitwise a) (BVDBitwise b) = B.domainsOverlap a b-domainsOverlap (BVDArith a)   (BVDArith b)   = A.domainsOverlap a b-domainsOverlap (BVDArith a)   (BVDBitwise b) = mixedDomainsOverlap a b-domainsOverlap (BVDBitwise b) (BVDArith a)   = mixedDomainsOverlap a b--arithDomainLo :: A.Domain w -> Integer-arithDomainLo a =-  case A.arithDomainData a of-    Nothing -> 0-    Just (lo,_) -> lo--mixedCandidates :: A.Domain w -> B.Domain w -> [Integer]-mixedCandidates a b =-  case A.arithDomainData a of-    Nothing -> [ lomask ]-    Just (alo,_) -> [ lomask, himask, bitwiseRoundBetween (A.bvdMask a) alo lomask himask ]- where- (lomask,himask) = B.bitbounds b---- | Return a list of "candidate" overlap elements.  If two domains---   overlap, then they will definitely share one of the given---   values.-overlapCandidates :: BVDomain w -> BVDomain w -> [Integer]-overlapCandidates (BVDArith a)   (BVDBitwise b) = mixedCandidates a b-overlapCandidates (BVDBitwise b) (BVDArith a)   = mixedCandidates a b-overlapCandidates (BVDArith a)   (BVDArith b)   = [ arithDomainLo a, arithDomainLo b ]-overlapCandidates (BVDBitwise a) (BVDBitwise b) = [ loa .|. lob ]-  where-  (loa,_) = B.bitbounds a-  (lob,_) = B.bitbounds b---eq :: BVDomain w -> BVDomain w -> Maybe Bool-eq a b-  | Just x <- asSingleton a-  , Just y <- asSingleton b = Just (x == y)-  | domainsOverlap a b == False = Just False-  | otherwise = Nothing---- | Check if all elements in one domain are less than all elements in other.-slt :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool-slt w a b = A.slt w (asArithDomain a) (asArithDomain b)---- | Check if all elements in one domain are less than all elements in other.-ult :: (1 <= w) => BVDomain w -> BVDomain w -> Maybe Bool-ult a b = A.ult (asArithDomain a) (asArithDomain b)---- | Return @Just@ if every bitvector in the domain has the same bit--- at the given index.-testBit ::-  NatRepr w ->-  BVDomain w ->-  Natural {- ^ Index of bit (least-significant bit has index 0) -} ->-  Maybe Bool-testBit _w a i = B.testBit (asBitwiseDomain a) i--ubounds :: BVDomain w -> (Integer, Integer)-ubounds a = A.ubounds (asArithDomain a)--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---- | Represents all values-any :: (1 <= w) => NatRepr w -> BVDomain w-any w = BVDBitwise (B.any w)---- | Create a bitvector domain representing the integer.-singleton :: (HasCallStack, 1 <= w) => NatRepr w -> Integer -> BVDomain w-singleton w x = BVDArith (A.singleton w x)---- | @range w l u@ returns domain containing all bitvectors formed--- from the @w@ low order bits of some @i@ in @[l,u]@.  Note that per--- @testBit@, the least significant bit has index @0@.-range :: NatRepr w -> Integer -> Integer -> BVDomain w-range w al ah = BVDArith (A.range w al ah)---- | Create an abstract domain from an ascending list of elements.--- The elements are assumed to be distinct.-fromAscEltList :: (1 <= w) => NatRepr w -> [Integer] -> BVDomain w-fromAscEltList w xs = BVDArith (A.fromAscEltList w xs)---- | Return union of two domains.-union :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w-union (BVDBitwise a) (BVDBitwise b) = BVDBitwise (B.union a b)-union (BVDArith a) (BVDArith b) = BVDArith (A.union a b)-union (BVDBitwise a) (BVDArith b) = mixedUnion b a-union (BVDArith a) (BVDBitwise b) = mixedUnion a b--mixedUnion :: (1 <= w) => A.Domain w -> B.Domain w  -> BVDomain w-mixedUnion a b-  | Just _ <- A.asSingleton a = BVDBitwise (B.union (arithToBitwiseDomain a) b)-  | otherwise = BVDArith (A.union a (bitwiseToArithDomain b))---- | @concat a y@ returns domain where each element in @a@ has been--- concatenated with an element in @y@.  The most-significant bits--- are @a@, and the least significant bits are @y@.-concat :: NatRepr u -> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)-concat u (BVDArith a) v (BVDArith b) = BVDArith (A.concat u a v b)-concat u (asBitwiseDomain -> a) v (asBitwiseDomain -> b) = BVDBitwise (B.concat u a v b)---- | @select i n a@ selects @n@ bits starting from index @i@ from @a@.-select ::-  (1 <= n, i + n <= w) =>-  NatRepr i ->-  NatRepr n ->-  BVDomain w -> BVDomain n-select i n (BVDArith a)   = BVDArith (A.select i n a)-select i n (BVDBitwise b) = BVDBitwise (B.select i n b)--zext :: (1 <= w, w+1 <= u) => BVDomain w -> NatRepr u -> BVDomain u-zext (BVDArith a) u   = BVDArith (A.zext a u)-zext (BVDBitwise b) u = BVDBitwise (B.zext b u)--sext ::-  forall w u. (1 <= w, w + 1 <= u) =>-  NatRepr w ->-  BVDomain w ->-  NatRepr u ->-  BVDomain u-sext w (BVDArith a) u   = BVDArith (A.sext w a u)-sext w (BVDBitwise b) u = BVDBitwise (B.sext w b u)------------------------------------------------------------------------------------- Shifts---- An arbitrary value; if we have to union together more than this many--- bitwise shifts or rotates we'll fall back on some default instead-shiftBound :: Integer-shiftBound = 16--shl :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w-shl w (BVDBitwise a) (asArithDomain -> b)-  | lo <= hi' && hi' - lo <= shiftBound =-      BVDBitwise $ foldl1 B.union [ B.shl w a y | y <- [lo .. hi'] ]-  where-  (lo, hi) = A.ubounds b-  hi' = max hi (intValue w)--shl w (asArithDomain -> a) (asArithDomain -> b) = BVDArith (A.shl w a b)---lshr :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w-lshr w (BVDBitwise a) (asArithDomain -> b)-  | lo <= hi' && hi' - lo <= shiftBound =-      BVDBitwise $ foldl1 B.union [ B.lshr w a y | y <- [lo .. hi'] ]-  where-  (lo, hi) = A.ubounds b-  hi' = max hi (intValue w)--lshr w (asArithDomain -> a) (asArithDomain -> b) = BVDArith (A.lshr w a b)----ashr :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w-ashr w (BVDBitwise a) (asArithDomain -> b)-  | lo <= hi' && hi' - lo <= shiftBound =-      BVDBitwise $ foldl1 B.union [ B.ashr w a y | y <- [lo .. hi'] ]-  where-  (lo, hi) = A.ubounds b-  hi' = max hi (intValue w)--ashr w (asArithDomain -> a) (asArithDomain -> b) = BVDArith (A.ashr w a b)---rol :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w---- Special cases, rotating all 0 or all 1 bits makes no difference-rol _w a@(asSingleton -> Just x) _-  | x == 0 = a-  | x == bvdMask a = a--rol w (asBitwiseDomain -> a) (asArithDomain -> b) =-    if (lo <= hi && hi - lo <= shiftBound) then-      BVDBitwise $ foldl1 B.union [ B.rol w a y | y <- [lo .. hi] ]-    else-      any w--  where-  (lo, hi) = A.ubounds (A.urem b (A.singleton w (intValue w)))---ror :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w---- Special cases, rotating all 0 or all 1 bits makes no difference-ror _w a@(asSingleton -> Just x) _-  | x == 0 = a-  | x == bvdMask a = a--ror w (asBitwiseDomain -> a) (asArithDomain -> b) =-    if (lo <= hi && hi - lo <= shiftBound) then-      BVDBitwise $ foldl1 B.union [ B.ror w a y | y <- [lo .. hi] ]-    else-      any w--  where-  (lo, hi) = A.ubounds (A.urem b (A.singleton w (intValue w)))------------------------------------------------------------------------------------- Arithmetic--add :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w-add a b-  | Just 0 <- asSingleton a = b-  | Just 0 <- asSingleton b = a-  | otherwise = BVDArith (A.add (asArithDomain a) (asArithDomain b))--negate :: (1 <= w) => BVDomain w -> BVDomain w-negate (asArithDomain -> a) = BVDArith (A.negate a)--scale :: (1 <= w) => Integer -> BVDomain w -> BVDomain w-scale k a-  | k == 1 = a-  | otherwise = BVDArith (A.scale k (asArithDomain a))--mul :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w-mul a b-  | Just 1 <- asSingleton a = b-  | Just 1 <- asSingleton b = a-  | otherwise = BVDArith (A.mul (asArithDomain a) (asArithDomain b))--udiv :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w-udiv (asArithDomain -> a) (asArithDomain -> b) = BVDArith (A.udiv a b)--urem :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w-urem (asArithDomain -> a) (asArithDomain -> b) = BVDArith (A.urem a b)--sdiv :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w-sdiv w (asArithDomain -> a) (asArithDomain -> b) = BVDArith (A.sdiv w a b)--srem :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w-srem w (asArithDomain -> a) (asArithDomain -> b) = BVDArith (A.srem w a b)------------------------------------------------------------------------------------- Bitwise logical---- | Complement bits in range.-not :: BVDomain w -> BVDomain w-not (BVDArith a) = BVDArith (A.not a)-not (BVDBitwise b) = BVDBitwise (B.not b)--and :: BVDomain w -> BVDomain w -> BVDomain w-and a b-  | Just x <- asSingleton a, x == mask = b-  | Just x <- asSingleton b, x == mask = a-  | otherwise = BVDBitwise (B.and (asBitwiseDomain a) (asBitwiseDomain b))- where- mask = bvdMask a--or :: BVDomain w -> BVDomain w -> BVDomain w-or a b-  | Just 0 <- asSingleton a = b-  | Just 0 <- asSingleton b = a-  | otherwise = BVDBitwise (B.or (asBitwiseDomain a) (asBitwiseDomain b))--xor :: BVDomain w -> BVDomain w -> BVDomain w-xor a b-  | Just 0 <- asSingleton a = b-  | Just 0 <- asSingleton b = a-  | otherwise = BVDBitwise (B.xor (asBitwiseDomain a) (asBitwiseDomain b))------------------------------------------------------------------------------------ Misc operations--popcnt :: NatRepr w -> BVDomain w -> BVDomain w-popcnt w (asBitwiseDomain -> b) = BVDArith (A.range w lo hi)-  where-  (bitlo, bithi) = B.bitbounds b-  lo = toInteger (Bits.popCount bitlo)-  hi = toInteger (Bits.popCount bithi)--clz :: NatRepr w -> BVDomain w -> BVDomain w-clz w (asBitwiseDomain -> b) = BVDArith (A.range w lo hi)-  where-  (bitlo, bithi) = B.bitbounds b-  lo = Arith.clz w bithi-  hi = Arith.clz w bitlo--ctz :: NatRepr w -> BVDomain w -> BVDomain w-ctz w (asBitwiseDomain -> b) = BVDArith (A.range w lo hi)-  where-  (bitlo, bithi) = B.bitbounds b-  lo = Arith.ctz w bithi-  hi = Arith.ctz w bitlo------------------------------------------------------------------------ Correctness properties---- | Check that a domain is proper, and that---   the given value is a member-pmember :: NatRepr n -> BVDomain n -> Integer -> Bool-pmember n a x = proper n a && member a x--correct_arithToBitwise :: NatRepr n -> (A.Domain n, Integer) -> Property-correct_arithToBitwise n (a,x) = A.member a x ==> B.pmember n (arithToBitwiseDomain a) x--correct_bitwiseToArith :: NatRepr n -> (B.Domain n, Integer) -> Property-correct_bitwiseToArith n (b,x) = B.member b x ==> A.pmember n (bitwiseToArithDomain b) x--correct_bitwiseToXorDomain :: NatRepr n -> (B.Domain n, Integer) -> Property-correct_bitwiseToXorDomain n (b,x) = B.member b x ==> X.pmember n (bitwiseToXorDomain b) x--correct_arithToXorDomain :: NatRepr n -> (A.Domain n, Integer) -> Property-correct_arithToXorDomain n (a,x) = A.member a x ==> X.pmember n (arithToXorDomain a) x--correct_xorToBitwiseDomain :: NatRepr n -> (X.Domain n, Integer) -> Property-correct_xorToBitwiseDomain n (a,x) = X.member a x ==> B.pmember n (xorToBitwiseDomain a) x--correct_asXorDomain :: NatRepr n -> (BVDomain n, Integer) -> Property-correct_asXorDomain n (a, x) = member a x ==> X.pmember n (asXorDomain a) x--correct_fromXorDomain :: NatRepr n -> (X.Domain n, Integer) -> Property-correct_fromXorDomain n (a, x) = X.member a x ==> pmember n (fromXorDomain a) x---correct_bra1 :: NatRepr n -> Integer -> Integer -> Property-correct_bra1 n x lomask = lomask <= x ==> (x <= q && B.bitle lomask q)- where- q = bitwiseRoundAbove (maxUnsigned n) x lomask--correct_bra2 :: NatRepr n -> Integer -> Integer -> Integer -> Property-correct_bra2 n x lomask q' = (x <= q' && B.bitle lomask q') ==> q <= q'- where- q = bitwiseRoundAbove (maxUnsigned n) x lomask--correct_brb1 :: NatRepr n -> Integer -> Integer -> Integer -> Property-correct_brb1 n x lomask himask =-    (B.bitle lomask himask && lomask <= x && x <= himask) ==>-    (x <= q && B.bitle lomask q && B.bitle q himask)-  where-  q = bitwiseRoundBetween (maxUnsigned n) x lomask himask--correct_brb2 :: NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property-correct_brb2 n x lomask himask q' =-    (x <= q' && B.bitle lomask q' && B.bitle q' himask) ==> q <= q'-  where-  q = bitwiseRoundBetween (maxUnsigned n) x lomask himask--correct_any :: (1 <= n) => NatRepr n -> Integer -> Property-correct_any n x = property (pmember n (any n) x)--correct_ubounds :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property-correct_ubounds n (a,x) = member a x' ==> lo <= x' && x' <= hi-  where-  x' = toUnsigned n x-  (lo,hi) = ubounds a--correct_sbounds :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property-correct_sbounds n (a,x) = member a x' ==> lo <= x' && x' <= hi-  where-  x' = toSigned n x-  (lo,hi) = sbounds n a--correct_singleton :: (1 <= n) => NatRepr n -> Integer -> Integer -> Property-correct_singleton n x y = property (member (singleton n x') y' == (x' == y'))-  where-  x' = toUnsigned n x-  y' = toUnsigned n y--correct_overlap :: BVDomain n -> BVDomain n -> Integer -> Property-correct_overlap a b x =-  member a x && member b x ==> domainsOverlap a b--precise_overlap :: BVDomain n -> BVDomain n -> Property-precise_overlap a b =-  domainsOverlap a b ==> List.or [ member a x && member b x | x <- overlapCandidates a b ]--correct_union :: (1 <= n) => NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property-correct_union n a b x =-  (member a x || member b x) ==> pmember n (union a b) x--correct_zero_ext :: (1 <= w, w+1 <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property-correct_zero_ext w a u x = member a x' ==> pmember u (zext a u) x'-  where-  x' = toUnsigned w x--correct_sign_ext :: (1 <= w, w+1 <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property-correct_sign_ext w a u x = member a x' ==> pmember u (sext w a u) x'-  where-  x' = toSigned w x--correct_concat :: NatRepr m -> (BVDomain m,Integer) -> NatRepr n -> (BVDomain n,Integer) -> Property-correct_concat m (a,x) n (b,y) =-    member a x ==> member b y ==> pmember (addNat m n) (concat m a n b) z-  where-  z = (x `shiftL` (widthVal n)) .|. y--correct_select :: (1 <= n, i + n <= w) =>-  NatRepr i -> NatRepr n -> (BVDomain w, Integer) -> Property-correct_select i n (a, x) = member a x ==> pmember n (select i n a) y-  where-  y = toUnsigned n ((x .&. bvdMask a) `shiftR` (widthVal i))--correct_add :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_add n (a,x) (b,y) = member a x ==> member b y ==> pmember n (add a b) (x + y)--correct_neg :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property-correct_neg n (a,x) = member a x ==> pmember n (negate a) (Prelude.negate x)--correct_mul :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_mul n (a,x) (b,y) = member a x ==> member b y ==> pmember n (mul a b) (x * y)--correct_scale :: (1 <= n) => NatRepr n -> Integer -> (BVDomain n, Integer) -> Property-correct_scale n k (a,x) = member a x ==> pmember n (scale k' a) (k' * x)-  where-  k' = toSigned n k--correct_udiv :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_udiv n (a,x) (b,y) = member a x' ==> member b y' ==> y' /= 0 ==> pmember n (udiv a b) (x' `quot` y')-  where-  x' = toUnsigned n x-  y' = toUnsigned n y--correct_urem :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_urem n (a,x) (b,y) = member a x' ==> member b y' ==> y' /= 0 ==> pmember n (urem a b) (x' `rem` y')-  where-  x' = toUnsigned n x-  y' = toUnsigned n y--correct_sdiv :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_sdiv n (a,x) (b,y) =-    member a x' ==> member b y' ==> y' /= 0 ==> pmember n (sdiv n a b) (x' `quot` y')-  where-  x' = toSigned n x-  y' = toSigned n y--correct_srem :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_srem n (a,x) (b,y) =-    member a x' ==> member b y' ==> y' /= 0 ==> pmember n (srem n a b) (x' `rem` y')-  where-  x' = toSigned n x-  y' = toSigned n y--correct_shl :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_shl n (a,x) (b,y) = member a x ==> member b y ==> pmember n (shl n a b) z-  where-  z = (toUnsigned n x) `shiftL` fromInteger (min (intValue n) y)--correct_lshr :: (1 <= n) => NatRepr n ->  (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_lshr n (a,x) (b,y) = member a x ==> member b y ==> pmember n (lshr n a b) z-  where-  z = (toUnsigned n x) `shiftR` fromInteger (min (intValue n) y)--correct_ashr :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_ashr n (a,x) (b,y) = member a x ==> member b y ==> pmember n (ashr n a b) z-  where-  z = (toSigned n x) `shiftR` fromInteger (min (intValue n) y)--correct_rol :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_rol n (a,x) (b,y) = member a x ==> member b y ==> pmember n (rol n a b) (Arith.rotateLeft n x y)--correct_ror :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_ror n (a,x) (b,y) = member a x ==> member b y ==> pmember n (ror n a b) (Arith.rotateRight n x y)--correct_eq :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_eq n (a,x) (b,y) =-  member a x ==> member b y ==>-    case eq a b of-      Just True  -> toUnsigned n x == toUnsigned n y-      Just False -> toUnsigned n x /= toUnsigned n y-      Nothing    -> True--correct_ult :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_ult n (a,x) (b,y) =-  member a x ==> member b y ==>-    case ult a b of-      Just True  -> toUnsigned n x < toUnsigned n y-      Just False -> toUnsigned n x >= toUnsigned n y-      Nothing    -> True--correct_slt :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_slt n (a,x) (b,y) =-  member a x ==> member b y ==>-    case slt n a b of-      Just True  -> toSigned n x < toSigned n y-      Just False -> toSigned n x >= toSigned n y-      Nothing    -> True--correct_not :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property-correct_not n (a,x) = member a x ==> pmember n (not a) (complement x)--correct_and :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_and n (a,x) (b,y) = member a x ==> member b y ==> pmember n (and a b) (x .&. y)--correct_or :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_or n (a,x) (b,y) = member a x ==> member b y ==> pmember n (or a b) (x .|. y)--correct_xor :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property-correct_xor n (a,x) (b,y) = member a x ==> member b y ==> pmember n (xor a b) (x `Bits.xor` y)--correct_testBit :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Natural -> Property-correct_testBit n (a,x) i =-  i < natValue n ==>-    case testBit n a i of-      Just True  -> Bits.testBit x (fromIntegral i)-      Just False -> Prelude.not (Bits.testBit x (fromIntegral i))-      Nothing    -> True--correct_popcnt :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property-correct_popcnt n (a,x) = member a x ==> pmember n (popcnt n a) (toInteger (Bits.popCount x))--correct_ctz :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property-correct_ctz n (a,x) = member a x ==> pmember n (ctz n a) (Arith.ctz n x)--correct_clz :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property-correct_clz n (a,x) = member a x ==> pmember n (clz n a) (Arith.clz n x)+import What4.Domains.BV

@@ -1,884 +1,5 @@-{-|-Module      : What4.Utils.BVDomain.Arith-Copyright   : (c) Galois Inc, 2019-2020-License     : BSD3-Maintainer  : huffman@galois.com--Provides an interval-based implementation of bitvector abstract-domains.--}--{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}--module What4.Utils.BVDomain.Arith-  ( Domain(..)-  , proper-  , bvdMask-  , member-  , pmember-  , interval-  , size-  -- * Projection functions-  , asSingleton-  , ubounds-  , sbounds-  , eq-  , slt-  , ult-  , isUltSumCommonEquiv-  , domainsOverlap-  , arithDomainData-  , bitbounds-  , unknowns-  , fillright-    -- * Operations-  , any-  , singleton-  , range-  , fromAscEltList-  , union-  , concat-  , select-  , zext-  , sext-    -- ** Shifts-  , shl-  , lshr-  , ashr-    -- ** Arithmetic-  , add-  , negate-  , scale-  , mul-  , udiv-  , urem-  , sdiv-  , srem-    -- ** Bitwise-  , What4.Utils.BVDomain.Arith.not--  -- * Correctness properties-  , genDomain-  , genElement-  , genPair-  , correct_any-  , correct_ubounds-  , correct_sbounds-  , correct_singleton-  , correct_overlap-  , correct_union-  , correct_zero_ext-  , correct_sign_ext-  , correct_concat-  , correct_shrink-  , correct_trunc-  , correct_select-  , correct_add-  , correct_neg-  , correct_mul-  , correct_scale-  , correct_scale_eq-  , correct_udiv-  , correct_urem-  , correct_sdivRange-  , correct_sdiv-  , correct_srem-  , correct_not-  , correct_shl-  , correct_lshr-  , correct_ashr-  , correct_eq-  , correct_ult-  , correct_slt-  , correct_isUltSumCommonEquiv-  , correct_unknowns-  , correct_bitbounds+module What4.Utils.BVDomain.Arith {-# DEPRECATED "Use What4.Domains.BV.Arith instead" #-}+  ( module What4.Domains.BV.Arith   ) where -import qualified Data.Bits as Bits-import           Data.Bits hiding (testBit, xor)-import           Data.Parameterized.NatRepr-import           GHC.TypeNats-import           GHC.Stack--import qualified Prelude-import           Prelude hiding (any, concat, negate, and, or, not)--import           Test.Verification ( Property, property, (==>), Gen, chooseInteger )------------------------------------------------------------------------------------- BVDomain definition---- | A value of type @'BVDomain' w@ represents a set of bitvectors of--- width @w@. Each 'BVDomain' can represent a single contiguous--- interval of bitvectors that may wrap around from -1 to 0.-data Domain (w :: Nat)-  = BVDAny !Integer-  -- ^ The set of all bitvectors of width @w@. Argument caches @2^w-1@.-  | BVDInterval !Integer !Integer !Integer-  -- ^ Intervals are represented by a starting value and a size.-  -- @BVDInterval mask l d@ represents the set of values of the form-  -- @x mod 2^w@ for @x@ such that @l <= x <= l + d@. It should-  -- satisfy the invariants @0 <= l < 2^w@ and @0 <= d < 2^w@. The-  -- first argument caches the value @2^w-1@.-  deriving Show--sameDomain :: Domain w -> Domain w -> Bool-sameDomain (BVDAny _) (BVDAny _) = True-sameDomain (BVDInterval _ x w) (BVDInterval _ x' w') = x == x' && w == w'-sameDomain _ _ = False---- | Compute how many concrete elements are in the abstract domain-size :: Domain w -> Integer-size (BVDAny mask)        = mask + 1-size (BVDInterval _ _ sz) = sz + 1---- | Test if the given integer value is a member of the abstract domain-member :: Domain w -> Integer -> Bool-member (BVDAny _) _ = True-member (BVDInterval mask lo sz) x = ((x' - lo) .&. mask) <= sz-  where x' = x .&. mask---- | Check if the domain satisfies its invariants-proper :: NatRepr w -> Domain w -> Bool-proper w (BVDAny mask) = mask == maxUnsigned w-proper w (BVDInterval mask lo sz) =-  mask == maxUnsigned w &&-  lo .|. mask == mask &&-  sz .|. mask == mask &&-  sz < mask---- | Return the bitvector mask value from this domain-bvdMask :: Domain w -> Integer-bvdMask x =-  case x of-    BVDAny mask -> mask-    BVDInterval mask _ _ -> mask---- | Random generator for domain values-genDomain :: NatRepr w -> Gen (Domain w)-genDomain w =-  do let mask = maxUnsigned w-     lo <- chooseInteger (0, mask)-     sz <- chooseInteger (0, mask)-     pure $! interval mask lo sz---- | Generate a random element from a domain-genElement :: Domain w -> Gen Integer-genElement (BVDAny mask) = chooseInteger (0, mask)-genElement (BVDInterval mask lo sz) =-   do x <- chooseInteger (0, sz)-      pure ((x+lo) .&. mask)---- | Generate a random domain and an element---   contained in that domain.-genPair :: NatRepr w -> Gen (Domain w, Integer)-genPair w =-  do a <- genDomain w-     x <- genElement a-     return (a,x)-------------------------------------------------------------------------------------- | @halfRange n@ returns @2^(n-1)@.-halfRange :: (1 <= w) => NatRepr w -> Integer-halfRange w = bit (widthVal w - 1)------------------------------------------------------------------------------------- Projection functions---- | Return value if this is a singleton.-asSingleton :: Domain w -> Maybe Integer-asSingleton x =-  case x of-    BVDAny _ -> Nothing-    BVDInterval _ xl xd-      | xd == 0 -> Just xl-      | otherwise -> Nothing--isSingletonZero :: Domain w -> Bool-isSingletonZero x =-  case x of-    BVDInterval _ 0 0 -> True-    _ -> False--isBVDAny :: Domain w -> Bool-isBVDAny x =-  case x of-    BVDAny {} -> True-    BVDInterval {} -> False---- | Return unsigned bounds for domain.-ubounds :: Domain w -> (Integer, Integer)-ubounds a =-  case a of-    BVDAny mask -> (0, mask)-    BVDInterval mask al aw-      | ah > mask -> (0, mask)-      | otherwise -> (al, ah)-      where ah = al + aw---- | Return signed bounds for domain.-sbounds :: (1 <= w) => NatRepr w -> Domain w -> (Integer, Integer)-sbounds w a = (lo - delta, hi - delta)-  where-    delta = halfRange w-    (lo, hi) = ubounds (add a (BVDInterval (bvdMask a) delta 0))---- | Return the @(lo,sz)@, the low bound and size---   of the given arithmetic interval.  A value @x@ is in---   the set defined by this domain iff---   @(x - lo) `mod` w <= sz@ holds.---   Returns @Nothing@ if the domain contains all values.-arithDomainData :: Domain w -> Maybe (Integer, Integer)-arithDomainData (BVDAny _) = Nothing-arithDomainData (BVDInterval _ al aw) = Just (al, aw)---- | Return true if domains contain a common element.-domainsOverlap :: Domain w -> Domain w -> Bool-domainsOverlap a b =-  case a of-    BVDAny _ -> True-    BVDInterval _ al aw ->-      case b of-        BVDAny _ -> True-        BVDInterval mask bl bw ->-          diff <= bw || diff + aw > mask-          where diff = (al - bl) .&. mask--eq :: Domain w -> Domain w -> Maybe Bool-eq a b-  | Just x <- asSingleton a-  , Just y <- asSingleton b = Just (x == y)-  | domainsOverlap a b == False = Just False-  | otherwise = Nothing---- | Check if all elements in one domain are less than all elements in other.-slt :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Maybe Bool-slt w a b-  | a_max < b_min = Just True-  | a_min >= b_max = Just False-  | otherwise = Nothing-  where-    (a_min, a_max) = sbounds w a-    (b_min, b_max) = sbounds w b---- | Check if all elements in one domain are less than all elements in other.-ult :: (1 <= w) => Domain w -> Domain w -> Maybe Bool-ult a b-  | a_max < b_min = Just True-  | a_min >= b_max = Just False-  | otherwise = Nothing-  where-    (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---- | Represents all values-any :: (1 <= w) => NatRepr w -> Domain w-any w = BVDAny (maxUnsigned w)---- | Create a bitvector domain representing the integer.-singleton :: (HasCallStack, 1 <= w) => NatRepr w -> Integer -> Domain w-singleton w x = BVDInterval mask (x .&. mask) 0-  where mask = maxUnsigned w---- | @range w l u@ returns domain containing all bitvectors formed--- from the @w@ low order bits of some @i@ in @[l,u]@.  Note that per--- @testBit@, the least significant bit has index @0@.-range :: NatRepr w -> Integer -> Integer -> Domain w-range w al ah = interval mask al ((ah - al) .&. mask)-  where mask = maxUnsigned w---- | Unsafe constructor for internal use only. Caller must ensure that--- @mask = maxUnsigned w@, and that @aw@ is non-negative.-interval :: Integer -> Integer -> Integer -> Domain w-interval mask al aw =-  if aw >= mask then BVDAny mask else BVDInterval mask (al .&. mask) aw---- | Create an abstract domain from an ascending list of elements.--- The elements are assumed to be distinct.-fromAscEltList :: (1 <= w) => NatRepr w -> [Integer] -> Domain w-fromAscEltList w [] = singleton w 0-fromAscEltList w [x] = singleton w x-fromAscEltList w (x0 : x1 : xs) = go (x0, x0) (x1, x1) xs-  where-    -- Invariant: the gap between @b@ and @c@ is the biggest we've-    -- seen between adjacent values so far.-    go (a, b) (c, d) [] = union (range w a b) (range w c d)-    go (a, b) (c, d) (e : rest)-      | e - d > c - b = go (a, d) (e, e) rest-      | otherwise     = go (a, b) (c, e) rest---- | Return union of two domains.-union :: (1 <= w) => Domain w -> Domain w -> Domain w-union a b =-  case a of-    BVDAny _ -> a-    BVDInterval _ al aw ->-      case b of-        BVDAny _ -> b-        BVDInterval mask bl bw ->-          interval mask cl (ch - cl)-          where-            sz = mask + 1-            ac = 2 * al + aw -- twice the average value of a-            bc = 2 * bl + bw -- twice the average value of b-            -- If the averages are 2^(w-1) or more apart,-            -- then shift the lower interval up by 2^w.-            al' = if ac + mask < bc then al + sz else al-            bl' = if bc + mask < ac then bl + sz else bl-            ah' = al' + aw-            bh' = bl' + bw-            cl = min al' bl'-            ch = max ah' bh'---- | @concat a y@ returns domain where each element in @a@ has been--- concatenated with an element in @y@.  The most-significant bits--- are @a@, and the least significant bits are @y@.-concat :: NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)-concat u a v b =-  case a of-    BVDAny _ -> BVDAny mask-    BVDInterval _ al aw -> interval mask (cat al bl) (cat aw bw)-  where-    cat i j = (i `shiftL` widthVal v) + j-    mask = maxUnsigned (addNat u v)-    (bl, bh) = ubounds b-    bw = bh - bl---- | @shrink i a@ drops the @i@ least significant bits from @a@.-shrink ::-  NatRepr i ->-  Domain (i + n) -> Domain n-shrink i a =-  case a of-    BVDAny mask -> BVDAny (shr mask)-    BVDInterval mask al aw ->-      interval (shr mask) bl (bh - bl)-      where-        bl = shr al-        bh = shr (al + aw)-  where-    shr x = x `shiftR` widthVal i---- | @trunc n d@ selects the @n@ least significant bits from @d@.-trunc ::-  (n <= w) =>-  NatRepr n ->-  Domain w -> Domain n-trunc n a =-  case a of-    BVDAny _ -> BVDAny mask-    BVDInterval _ al aw -> interval mask al aw-  where-    mask = maxUnsigned n---- | @select i n a@ selects @n@ bits starting from index @i@ from @a@.-select ::-  (1 <= n, i + n <= w) =>-  NatRepr i ->-  NatRepr n ->-  Domain w -> Domain n-select i n a = shrink i (trunc (addNat i n) a)--zext :: (1 <= w, w+1 <= u) => Domain w -> NatRepr u -> Domain u-zext a u = range u al ah-  where (al, ah) = ubounds a--sext ::-  forall w u. (1 <= w, w + 1 <= u) =>-  NatRepr w ->-  Domain w ->-  NatRepr u ->-  Domain u-sext w a u =-  case fProof of-    LeqProof ->-      range u al ah-      where (al, ah) = sbounds w a-  where-    wProof :: LeqProof 1 w-    wProof = LeqProof-    uProof :: LeqProof (w+1) u-    uProof = LeqProof-    fProof :: LeqProof 1 u-    fProof = leqTrans (leqAdd wProof (knownNat :: NatRepr 1)) uProof------------------------------------------------------------------------------------- Shifts--shl :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w-shl w a b-  | isBVDAny a = a-  | isSingletonZero a = a-  | isSingletonZero b = a-  | otherwise = interval mask lo (hi - lo)-    where-      mask = bvdMask a-      sz = mask + 1-      (bl, bh) = ubounds b-      bl' = clamp w bl-      bh' = clamp w bh-      -- compute bounds for c = 2^b-      cl = if (mask `shiftR` bl' == 0) then sz else bit bl'-      ch = if (mask `shiftR` bh' == 0) then sz else bit bh'-      (lo, hi) = mulRange (zbounds a) (cl, ch)--lshr :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w-lshr w a b = interval mask cl (ch - cl)-  where-    mask = bvdMask a-    (al, ah) = ubounds a-    (bl, bh) = ubounds b-    cl = al `shiftR` clamp w bh-    ch = ah `shiftR` clamp w bl--ashr :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w-ashr w a b = interval mask cl (ch - cl)-  where-    mask = bvdMask a-    (al, ah) = sbounds w a-    (bl, bh) = ubounds b-    cl = al `shiftR` (if al < 0 then clamp w bl else clamp w bh)-    ch = ah `shiftR` (if ah < 0 then clamp w bh else clamp w bl)---- | Clamp the given shift amount to the word width indicated by the---   nat repr-clamp :: NatRepr w -> Integer -> Int-clamp w x = fromInteger (min (intValue w) x)------------------------------------------------------------------------------------- Arithmetic--add :: (1 <= w) => Domain w -> Domain w -> Domain w-add a b =-  case a of-    BVDAny _ -> a-    BVDInterval _ al aw ->-      case b of-        BVDAny _ -> b-        BVDInterval mask bl bw ->-          interval mask (al + bl) (aw + bw)--negate :: (1 <= w) => Domain w -> Domain w-negate a =-  case a of-    BVDAny _ -> a-    BVDInterval mask al aw -> BVDInterval mask ((-ah) .&. mask) aw-      where ah = al + aw--scale :: (1 <= w) => Integer -> Domain w -> Domain w-scale k a-  | k == 0 = BVDInterval (bvdMask a) 0 0-  | k == 1 = a-  | otherwise =-    case a of-      BVDAny _ -> a-      BVDInterval mask al aw-        | k >= 0 -> interval mask (k * al) (k * aw)-        | otherwise -> interval mask (k * ah) (abs k * aw)-        where ah = al + aw--mul :: (1 <= w) => Domain w -> Domain w -> Domain w-mul a b-  | isSingletonZero a = a-  | isSingletonZero b = b-  | isBVDAny a = a-  | isBVDAny b = b-  | otherwise = interval mask cl (ch - cl)-    where-      mask = bvdMask a-      (cl, ch) = mulRange (zbounds a) (zbounds b)---- | Choose a representative integer range (positive or negative) for--- the given bitvector domain such that the endpoints are as close to--- zero as possible.-zbounds :: Domain w -> (Integer, Integer)-zbounds a =-  case a of-    BVDAny mask -> (0, mask)-    BVDInterval mask lo sz -> (lo', lo' + sz)-      where lo' = if 2*lo + sz > mask then lo - (mask + 1) else lo--mulRange :: (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)-mulRange (al, ah) (bl, bh) = (cl, ch)-  where-    (albl, albh) = scaleRange al (bl, bh)-    (ahbl, ahbh) = scaleRange ah (bl, bh)-    cl = min albl ahbl-    ch = max albh ahbh--scaleRange :: Integer -> (Integer, Integer) -> (Integer, Integer)-scaleRange k (lo, hi)-  | k < 0 = (k * hi, k * lo)-  | otherwise = (k * lo, k * hi)--udiv :: (1 <= w) => Domain w -> Domain w -> Domain w-udiv a b = interval mask ql (qh - ql)-  where-    mask = bvdMask a-    (al, ah) = ubounds a-    (bl, bh) = ubounds b-    ql = al `div` max 1 bh -- assume that division by 0 does not happen-    qh = ah `div` max 1 bl -- assume that division by 0 does not happen--urem :: (1 <= w) => Domain w -> Domain w -> Domain w-urem a b-  | qh == ql = interval mask rl (rh - rl)-  | otherwise = interval mask 0 (bh - 1)-  where-    mask = bvdMask a-    (al, ah) = ubounds a-    (bl, bh) = ubounds b-    (ql, rl) = al `divMod` max 1 bh -- assume that division by 0 does not happen-    (qh, rh) = ah `divMod` max 1 bl -- assume that division by 0 does not happen---- | Pairs of nonzero integers @(lo, hi)@ such that @1\/lo <= 1\/hi@.--- This pair represents the set of all nonzero integers @x@ such that--- @1\/lo <= 1\/x <= 1\/hi@.-data ReciprocalRange = ReciprocalRange Integer Integer---- | Nonzero signed values in a domain with the least and greatest--- reciprocals.-rbounds :: (1 <= w) => NatRepr w -> Domain w -> ReciprocalRange-rbounds w a =-  case a of-    BVDAny _ -> ReciprocalRange (-1) 1-    BVDInterval mask al aw-      | ah > mask + 1 -> ReciprocalRange (-1) 1-      | otherwise     -> ReciprocalRange (signed (min mask ah)) (signed (max 1 al))-      where-        ah = al + aw-        signed x = if x < halfRange w then x else x - (mask + 1)---- | Interval arithmetic for integer division (rounding towards 0).--- Given @a@ and @b@ with @al <= a <= ah@ and @1\/bl <= 1\/b <= 1/bh@,--- @sdivRange (al, ah) (ReciprocalRange bl bh)@ returns @(ql, qh)@--- such that @ql <= a `quot` b <= qh@.-sdivRange :: (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)-sdivRange (al, ah) (ReciprocalRange bl bh) = (ql, qh)-  where-    (ql1, qh1) = scaleDownRange (al, ah) bh-    (ql2, qh2) = scaleDownRange (al, ah) bl-    ql = min ql1 ql2-    qh = max qh1 qh2---- | @scaleDownRange (lo, hi) k@ returns an interval @(ql, qh)@ such that for any--- @x@ in @[lo..hi]@, @x `quot` k@ is in @[ql..qh]@.-scaleDownRange :: (Integer, Integer) -> Integer -> (Integer, Integer)-scaleDownRange (lo, hi) k-  | k > 0 = (lo `quot` k, hi `quot` k)-  | k < 0 = (hi `quot` k, lo `quot` k)-  | otherwise = (lo, hi) -- assume k is nonzero---sdiv :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w-sdiv w a b = interval mask ql (qh - ql)-  where-    mask = bvdMask a-    (ql, qh) = sdivRange (sbounds w a) (rbounds w b)--srem :: (1 <= w) => NatRepr w -> Domain w -> Domain w -> Domain w-srem w a b =-  -- If the quotient is a singleton @q@, then we compute the remainder-  -- @r = a - q*b@.-  if ql == qh then-    (if ql < 0-     then interval mask (al - ql * bl) (aw - ql * bw)-     else interval mask (al - ql * bh) (aw + ql * bw))-  -- Otherwise the range of possible remainders is determined by the-  -- modulus and the sign of the first argument.-  else interval mask rl (rh - rl)-  where-    mask = bvdMask a-    (al, ah) = sbounds w a-    (bl, bh) = sbounds w b-    (ql, qh) = sdivRange (al, ah) (rbounds w b)-    rl = if al < 0 then min (bl+1) (-bh+1) else 0-    rh = if ah > 0 then max (-bl-1) (bh-1) else 0-    aw = ah - al-    bw = bh - bl------------------------------------------------------------------------------------- Bitwise logical---- | Complement bits in range.-not :: Domain w -> Domain w-not a =-  case a of-    BVDAny _ -> a-    BVDInterval mask al aw ->-      BVDInterval mask (complement ah .&. mask) aw-      where ah = al + aw---- | Return bitwise bounds for domain (i.e. logical AND of all--- possible values, paired with logical OR of all possible values).-bitbounds :: Domain w -> (Integer, Integer)-bitbounds a =-  case a of-    BVDAny mask -> (0, mask)-    BVDInterval mask al aw-      | al + aw > mask -> (0, mask)-      | otherwise -> (lo, hi)-      where-        au = unknowns a-        hi = al .|. au-        lo = hi `Bits.xor` au---- | @unknowns lo hi@ returns a bitmask representing the set of bit--- positions whose values are not constant throughout the range--- @lo..hi@.-unknowns :: Domain w -> Integer-unknowns (BVDAny mask) = mask-unknowns (BVDInterval mask al aw) = mask .&. (fillright (al `Bits.xor` (al+aw)))--bitle :: Integer -> Integer -> Bool-bitle x y = (x .|. y) == y---- | @fillright x@ rounds up @x@ to the nearest 2^n-1.-fillright :: Integer -> Integer-fillright = go 1-  where-  go :: Int -> Integer -> Integer-  go i x-    | x' == x = x-    | otherwise = go (2 * i) x'-    where x' = x .|. (x `shiftR` i)----------------------------------------------------------------------- Correctness properties---- | Check that a domain is proper, and that---   the given value is a member-pmember :: NatRepr n -> Domain n -> Integer -> Bool-pmember n a x = proper n a && member a x--correct_any :: (1 <= n) => NatRepr n -> Integer -> Property-correct_any w x = property (pmember w (any w) x)--correct_ubounds :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property-correct_ubounds n (a,x) = pmember n a x' ==> lo <= x' && x' <= hi-  where-  x' = toUnsigned n x-  (lo,hi) = ubounds a--correct_sbounds :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property-correct_sbounds n (a,x) = pmember n a x' ==> lo <= x' && x' <= hi-  where-  x' = toSigned n x-  (lo,hi) = sbounds n a--correct_singleton :: (1 <= n) => NatRepr n -> Integer -> Integer -> Property-correct_singleton n x y = property (pmember n (singleton n x') y' == (x' == y'))-  where-  x' = toUnsigned n x-  y' = toUnsigned n y--correct_overlap :: Domain n -> Domain n -> Integer -> Property-correct_overlap a b x =-  member a x && member b x ==> domainsOverlap a b--correct_union :: (1 <= n) => NatRepr n -> Domain n -> Domain n -> Integer -> Property-correct_union n a b x =-  (member a x || member b x) ==> pmember n (union a b) x--correct_zero_ext :: (1 <= w, w+1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property-correct_zero_ext w a u x = member a x' ==> pmember u (zext a u) x'-  where-  x' = toUnsigned w x--correct_sign_ext :: (1 <= w, w+1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property-correct_sign_ext w a u x = member a x' ==> pmember u (sext w a u) x'-  where-  x' = toSigned w x--correct_concat :: NatRepr m -> (Domain m,Integer) -> NatRepr n -> (Domain n,Integer) -> Property-correct_concat m (a,x) n (b,y) = member a x' ==> member b y' ==> pmember (addNat m n) (concat m a n b) z-  where-  x' = toUnsigned m x-  y' = toUnsigned n y-  z  = x' `shiftL` (widthVal n) .|. y'--correct_shrink :: NatRepr i -> NatRepr n -> (Domain (i + n), Integer) -> Property-correct_shrink i n (a,x) = member a x' ==> pmember n (shrink i a) (x' `shiftR` widthVal i)-  where-  x' = x .&. bvdMask a--correct_trunc :: (n <= w) => NatRepr n -> (Domain w, Integer) -> Property-correct_trunc n (a,x) = member a x' ==> pmember n (trunc n a) (toUnsigned n x')-  where-  x' = x .&. bvdMask a--correct_select :: (1 <= n, i + n <= w) =>-  NatRepr i -> NatRepr n -> (Domain w, Integer) -> Property-correct_select i n (a, x) = member a x ==> pmember n (select i n a) y-  where-  y = toUnsigned n ((x .&. bvdMask a) `shiftR` (widthVal i))--correct_add :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_add n (a,x) (b,y) = member a x ==> member b y ==> pmember n (add a b) (x + y)--correct_neg :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property-correct_neg n (a,x) = member a x ==> pmember n (negate a) (Prelude.negate x)--correct_not :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property-correct_not n (a,x) = member a x ==> pmember n (not a) (complement x)--correct_mul :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_mul n (a,x) (b,y) = member a x ==> member b y ==> pmember n (mul a b) (x * y)--correct_scale :: (1 <= n) => NatRepr n -> Integer -> (Domain n, Integer) -> Property-correct_scale n k (a,x) = member a x ==> pmember n (scale k' a) (k' * x)-  where-  k' = toSigned n k--correct_scale_eq :: (1 <= n) => NatRepr n -> Integer -> Domain n -> Property-correct_scale_eq n k a = property $ sameDomain (scale k' a) (mul (singleton n k) a)-  where-  k' = toSigned n k--correct_udiv :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_udiv n (a,x) (b,y) = member a x' ==> member b y' ==> y' /= 0 ==> pmember n (udiv a b) (x' `quot` y')-  where-  x' = toUnsigned n x-  y' = toUnsigned n y--correct_urem :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_urem n (a,x) (b,y) = member a x' ==> member b y' ==> y' /= 0 ==> pmember n (urem a b) (x' `rem` y')-  where-  x' = toUnsigned n x-  y' = toUnsigned n y--correct_sdivRange :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer -> Property-correct_sdivRange a b x y =-   mem a x ==> mem b y ==> y /= 0 ==> mem (sdivRange a b') (x `quot` y)- where- b' = ReciprocalRange (snd b) (fst b)- mem (lo,hi) v = lo <= v && v <= hi--correct_sdiv :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_sdiv n (a,x) (b,y) =-    member a x ==> member b y ==> y /= 0 ==> pmember n (sdiv n a b) (x' `quot` y')-  where-  x' = toSigned n x-  y' = toSigned n y--correct_srem :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_srem n (a,x) (b,y) =-    member a x ==> member b y ==> y /= 0 ==> pmember n (srem n a b) (x' `rem` y')-  where-  x' = toSigned n x-  y' = toSigned n y--correct_shl :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_shl n (a,x) (b,y) = member a x ==> member b y ==> pmember n (shl n a b) z-  where-  z = (toUnsigned n x) `shiftL` fromInteger (min (intValue n) y)--correct_lshr :: (1 <= n) => NatRepr n ->  (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_lshr n (a,x) (b,y) = member a x ==> member b y ==> pmember n (lshr n a b) z-  where-  z = (toUnsigned n x) `shiftR` fromInteger (min (intValue n) y)--correct_ashr :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_ashr n (a,x) (b,y) = member a x ==> member b y ==> pmember n (ashr n a b) z-  where-  z = (toSigned n x) `shiftR` fromInteger (min (intValue n) y)--correct_eq :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_eq n (a,x) (b,y) =-  member a x ==> member b y ==>-    case eq a b of-      Just True  -> toUnsigned n x == toUnsigned n y-      Just False -> toUnsigned n x /= toUnsigned n y-      Nothing    -> True--correct_ult :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_ult n (a,x) (b,y) =-  member a x ==> member b y ==>-    case ult a b of-      Just True  -> toUnsigned n x < toUnsigned n y-      Just False -> toUnsigned n x >= toUnsigned n y-      Nothing    -> True--correct_slt :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_slt n (a,x) (b,y) =-  member a x ==> member b y ==>-    case slt n a b of-      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)-  where-  u = unknowns a-  mask = bvdMask a--correct_bitbounds :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property-correct_bitbounds n (a,x) =-    member a x ==> (bitle lo x' && bitle x' hi && bitle hi (maxUnsigned n))-  where-  x' = toUnsigned n x-  (lo, hi) = bitbounds a+import What4.Domains.BV.Arith

@@ -1,449 +1,5 @@-{-|-Module      : What4.Utils.BVDomain.Bitwise-Copyright   : (c) Galois Inc, 2020-License     : BSD3-Maintainer  : huffman@galois.com--Provides a bitwise implementation of bitvector abstract domains.--}--{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators #-}--module What4.Utils.BVDomain.Bitwise-  ( Domain(..)-  , bitle-  , proper-  , bvdMask-  , member-  , pmember-  , size-  , asSingleton-  , nonempty-  , eq-  , domainsOverlap-  , bitbounds-  -- * Operations-  , any-  , singleton-  , range-  , interval-  , union-  , intersection-  , concat-  , select-  , zext-  , sext-  , testBit-  -- ** shifts and rotates-  , shl-  , lshr-  , ashr-  , rol-  , ror-  -- ** bitwise logical-  , and-  , or-  , xor-  , not--  -- * Correctness properties-  , genDomain-  , genElement-  , genPair-  , correct_any-  , correct_singleton-  , correct_overlap-  , correct_union-  , correct_intersection-  , correct_zero_ext-  , correct_sign_ext-  , correct_concat-  , correct_shrink-  , correct_trunc-  , correct_select-  , correct_shl-  , correct_lshr-  , correct_ashr-  , correct_rol-  , correct_ror-  , correct_eq-  , correct_and-  , correct_or-  , correct_not-  , correct_xor-  , correct_testBit+module What4.Utils.BVDomain.Bitwise {-# DEPRECATED "Use What4.Domains.BV.Bitwise instead" #-}+  ( module What4.Domains.BV.Bitwise   ) where -import           Data.Bits hiding (testBit, xor)-import qualified Data.Bits as Bits-import           Data.Parameterized.NatRepr-import           Numeric.Natural-import           GHC.TypeNats-import           Test.Verification (Property, property, (==>), Gen, chooseInteger)--import qualified Prelude-import           Prelude hiding (any, concat, negate, and, or, not)--import qualified What4.Utils.Arithmetic as Arith---- | A bitwise interval domain, defined via a---   bitwise upper and lower bound.  The ordering---   used here to construct the interval is the pointwise---   ordering on bits.  In particular @x [= y iff x .|. y == y@,---   and a value @x@ is in the set defined by the pair @(lo,hi)@---   just when @lo [= x && x [= hi@.-data Domain (w :: Nat) =-  BVBitInterval !Integer !Integer !Integer-  -- ^ @BVDBitInterval mask lo hi@.-  --  @mask@ caches the value of @2^w - 1@- deriving (Show)---- | Test if the domain satisfies its invariants-proper :: NatRepr w -> Domain w -> Bool-proper w (BVBitInterval mask lo hi) =-  mask == maxUnsigned w &&-  bitle lo mask &&-  bitle hi mask &&-  bitle lo hi---- | Test if the given integer value is a member of the abstract domain-member :: Domain w -> Integer -> Bool-member (BVBitInterval mask lo hi) x = bitle lo x' && bitle x' hi-  where x' = x .&. mask---- | Compute how many concrete elements are in the abstract domain-size :: Domain w -> Integer-size (BVBitInterval _ lo hi)-  | bitle lo hi = Bits.bit p-  | otherwise   = 0- where- u = Bits.xor lo hi- p = Bits.popCount u--bitle :: Integer -> Integer -> Bool-bitle x y = (x .|. y) == y---- | Return the bitvector mask value from this domain-bvdMask :: Domain w -> Integer-bvdMask (BVBitInterval mask _ _) = mask---- | Random generator for domain values.  We always generate---   nonempty domain values.-genDomain :: NatRepr w -> Gen (Domain w)-genDomain w =-  do let mask = maxUnsigned w-     lo <- chooseInteger (0, mask)-     hi <- chooseInteger (0, mask)-     pure $! interval mask lo (lo .|. hi)---- This generator goes to some pains to try--- to generate a good statistical distribution--- of the values in the domain.  It only choses--- random bits for the "unknown" values of--- the domain, then stripes them out among--- the unknown bit positions.-genElement :: Domain w -> Gen Integer-genElement (BVBitInterval _mask lo hi) =-  do x <- chooseInteger (0, bit bs - 1)-     pure $ stripe lo x 0-- where- u = Bits.xor lo hi- bs = Bits.popCount u- stripe val x i-   | x == 0 = val-   | Bits.testBit u i =-       let val' = if Bits.testBit x 0 then setBit val i else val in-       stripe val' (x `shiftR` 1) (i+1)-   | otherwise = stripe val x (i+1)--{- A faster generator, but I worry that it-   doesn't have very good statistical properties...--genElement :: Domain w -> Gen Integer-genElement (BVBitInterval mask lo hi) =-  do let u = Bits.xor lo hi-     x <- chooseInteger (0, mask)-     pure ((x .&. u) .|. lo)--}---- | Generate a random nonempty domain and an element---   contained in that domain.-genPair :: NatRepr w -> Gen (Domain w, Integer)-genPair w =-  do a <- genDomain w-     x <- genElement a-     return (a,x)---- | Unsafe constructor for internal use.-interval :: Integer -> Integer -> Integer -> Domain w-interval mask lo hi = BVBitInterval mask lo hi---- | Construct a domain from bitwise lower and upper bounds-range :: NatRepr w -> Integer -> Integer -> Domain w-range w lo hi = BVBitInterval (maxUnsigned w) lo' hi'-  where-  lo'  = lo .&. mask-  hi'  = hi .&. mask-  mask = maxUnsigned w---- | Bitwise lower and upper bounds-bitbounds :: Domain w -> (Integer, Integer)-bitbounds (BVBitInterval _ lo hi) = (lo, hi)---- | Test if this domain contains a single value, and return it if so-asSingleton :: Domain w -> Maybe Integer-asSingleton (BVBitInterval _ lo hi) = if lo == hi then Just lo else Nothing---- | Returns true iff there is at least on element---   in this bitwise domain.-nonempty :: Domain w -> Bool-nonempty (BVBitInterval _mask lo hi) = bitle lo hi---- | Return a domain containing just the given value-singleton :: NatRepr w -> Integer -> Domain w-singleton w x = BVBitInterval mask x' x'-  where-  x' = x .&. mask-  mask = maxUnsigned w---- | Bitwise domain containing every bitvector value-any :: NatRepr w -> Domain w-any w = BVBitInterval mask 0 mask-  where-  mask = maxUnsigned w---- | Returns true iff the domains have some value in common-domainsOverlap :: Domain w -> Domain w -> Bool-domainsOverlap a b = nonempty (intersection a b)--eq :: Domain w -> Domain w -> Maybe Bool-eq a b-  | Just x <- asSingleton a-  , Just y <- asSingleton b-  = Just (x == y)--  | Prelude.not (domainsOverlap a b) = Just False-  | otherwise = Nothing--intersection :: Domain w -> Domain w -> Domain w-intersection (BVBitInterval mask alo ahi) (BVBitInterval _ blo bhi) =-  BVBitInterval mask (alo .|. blo) (ahi .&. bhi)--union :: Domain w -> Domain w -> Domain w-union (BVBitInterval mask alo ahi) (BVBitInterval _ blo bhi) =-  BVBitInterval mask (alo .&. blo) (ahi .|. bhi)---- | @concat a y@ returns domain where each element in @a@ has been--- concatenated with an element in @y@.  The most-significant bits--- are @a@, and the least significant bits are @y@.-concat :: NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)-concat u (BVBitInterval _ alo ahi) v (BVBitInterval _ blo bhi) =-    BVBitInterval mask (cat alo blo) (cat ahi bhi)-  where-    cat i j = (i `shiftL` widthVal v) + j-    mask = maxUnsigned (addNat u v)---- | @shrink i a@ drops the @i@ least significant bits from @a@.-shrink ::-  NatRepr i ->-  Domain (i + n) -> Domain n-shrink i (BVBitInterval mask lo hi) = BVBitInterval (shr mask) (shr lo) (shr hi)-  where-  shr x = x `shiftR` widthVal i---- | @trunc n d@ selects the @n@ least significant bits from @d@.-trunc ::-  (n <= w) =>-  NatRepr n ->-  Domain w ->-  Domain n-trunc n (BVBitInterval _ lo hi) = range n lo hi---- | @select i n a@ selects @n@ bits starting from index @i@ from @a@.-select ::-  (1 <= n, i + n <= w) =>-  NatRepr i ->-  NatRepr n ->-  Domain w -> Domain n-select i n a = shrink i (trunc (addNat i n) a)--zext :: (1 <= w, w+1 <= u) => Domain w -> NatRepr u -> Domain u-zext (BVBitInterval _ lo hi) u = range u lo hi--sext :: (1 <= w, w+1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Domain u-sext w (BVBitInterval _ lo hi) u = range u lo' hi'-  where-  lo' = toSigned w lo-  hi' = toSigned w hi--testBit :: Domain w -> Natural -> Maybe Bool-testBit (BVBitInterval _mask lo hi) i = if lob == hib then Just lob else Nothing-  where-  lob = Bits.testBit lo j-  hib = Bits.testBit hi j-  j = fromIntegral i--shl :: NatRepr w -> Domain w -> Integer -> Domain w-shl w (BVBitInterval mask lo hi) y = BVBitInterval mask (shleft lo) (shleft hi)-  where-  y' = fromInteger (min y (intValue w))-  shleft x = (x `shiftL` y') .&. mask--rol :: NatRepr w -> Domain w -> Integer -> Domain w-rol w (BVBitInterval mask lo hi) y =-  BVBitInterval mask (Arith.rotateLeft w lo y) (Arith.rotateLeft w hi y)--ror :: NatRepr w -> Domain w -> Integer -> Domain w-ror w (BVBitInterval mask lo hi) y =-  BVBitInterval mask (Arith.rotateRight w lo y) (Arith.rotateRight w hi y)--lshr :: NatRepr w -> Domain w -> Integer -> Domain w-lshr w (BVBitInterval mask lo hi) y = BVBitInterval mask (shr lo) (shr hi)-  where-  y' = fromInteger (min y (intValue w))-  shr x = x `shiftR` y'--ashr :: (1 <= w) => NatRepr w -> Domain w -> Integer -> Domain w-ashr w (BVBitInterval mask lo hi) y = BVBitInterval mask (shr lo) (shr hi)-  where-  y' = fromInteger (min y (intValue w))-  shr x = ((toSigned w x) `shiftR` y') .&. mask--not :: Domain w -> Domain w-not (BVBitInterval mask alo ahi) =-  BVBitInterval mask (ahi `Bits.xor` mask) (alo `Bits.xor` mask)--and :: Domain w -> Domain w -> Domain w-and (BVBitInterval mask alo ahi) (BVBitInterval _ blo bhi) =-  BVBitInterval mask (alo .&. blo) (ahi .&. bhi)--or :: Domain w -> Domain w -> Domain w-or (BVBitInterval mask alo ahi) (BVBitInterval _ blo bhi) =-  BVBitInterval mask (alo .|. blo) (ahi .|. bhi)--xor :: Domain w -> Domain w -> Domain w-xor (BVBitInterval mask alo ahi) (BVBitInterval _ blo bhi) = BVBitInterval mask clo chi-  where-  au  = alo `Bits.xor` ahi-  bu  = blo `Bits.xor` bhi-  c   = alo `Bits.xor` blo-  cu  = au .|. bu-  chi = c  .|. cu-  clo = chi `Bits.xor` cu--------------------------------------------------------------------------------------------- Correctness properties---- | Check that a domain is proper, and that---   the given value is a member-pmember :: NatRepr n -> Domain n -> Integer -> Bool-pmember n a x = proper n a && member a x--correct_any :: (1 <= n) => NatRepr n -> Integer -> Property-correct_any n x = property (pmember n (any n) x)--correct_singleton :: (1 <= n) => NatRepr n -> Integer -> Integer -> Property-correct_singleton n x y = property (pmember n (singleton n x') y' == (x' == y'))-  where-  x' = toUnsigned n x-  y' = toUnsigned n y--correct_overlap :: Domain n -> Domain n -> Integer -> Property-correct_overlap a b x =-  member a x && member b x ==> domainsOverlap a b--correct_union :: (1 <= n) => NatRepr n -> Domain n -> Domain n -> Integer -> Property-correct_union n a b x =-  member a x || member b x ==> pmember n (union a b) x--correct_intersection :: (1 <= n) => Domain n -> Domain n -> Integer -> Property-correct_intersection a b x = -- NB, intersection might not be proper-  member a x && member b x ==> member (intersection a b) x--correct_zero_ext :: (1 <= w, w+1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property-correct_zero_ext w a u x = member a x' ==> pmember u (zext a u) x'-  where-  x' = toUnsigned w x--correct_sign_ext :: (1 <= w, w+1 <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property-correct_sign_ext w a u x = member a x' ==> pmember u (sext w a u) x'-  where-  x' = toSigned w x--correct_concat :: NatRepr m -> (Domain m,Integer) -> NatRepr n -> (Domain n,Integer) -> Property-correct_concat m (a,x) n (b,y) = member a x' ==> member b y' ==> pmember (addNat m n) (concat m a n b) z-  where-  x' = toUnsigned m x-  y' = toUnsigned n y-  z  = x' `shiftL` (widthVal n) .|. y'--correct_shrink :: NatRepr i -> NatRepr n -> (Domain (i + n), Integer) -> Property-correct_shrink i n (a,x) = member a x' ==> pmember n (shrink i a) (x' `shiftR` widthVal i)-  where-  x' = x .&. bvdMask a--correct_trunc :: (n <= w) => NatRepr n -> (Domain w, Integer) -> Property-correct_trunc n (a,x) = member a x' ==> pmember n (trunc n a) (toUnsigned n x')-  where-  x' = x .&. bvdMask a--correct_select :: (1 <= n, i + n <= w) =>-  NatRepr i -> NatRepr n -> (Domain w, Integer) -> Property-correct_select i n (a, x) = member a x ==> pmember n (select i n a) y-  where-  y = toUnsigned n ((x .&. bvdMask a) `shiftR` (widthVal i))--correct_eq :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_eq n (a,x) (b,y) =-  member a x ==> member b y ==>-    case eq a b of-      Just True  -> toUnsigned n x == toUnsigned n y-      Just False -> toUnsigned n x /= toUnsigned n y-      Nothing    -> True--correct_shl :: (1 <= n) => NatRepr n -> (Domain n,Integer) -> Integer -> Property-correct_shl n (a,x) y = member a x ==> pmember n (shl n a y) z-  where-  z = (toUnsigned n x) `shiftL` fromInteger (min (intValue n) y)--correct_lshr :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Integer -> Property-correct_lshr n (a,x) y = member a x ==> pmember n (lshr n a y) z-  where-  z = (toUnsigned n x) `shiftR` fromInteger (min (intValue n) y)--correct_ashr :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Integer -> Property-correct_ashr n (a,x) y = member a x ==> pmember n (ashr n a y) z-  where-  z = (toSigned n x) `shiftR` fromInteger (min (intValue n) y)--correct_rol :: (1 <= n) => NatRepr n -> (Domain n,Integer) -> Integer -> Property-correct_rol n (a,x) y = member a x ==> pmember n (rol n a y) (Arith.rotateLeft n x y)--correct_ror :: (1 <= n) => NatRepr n -> (Domain n,Integer) -> Integer -> Property-correct_ror n (a,x) y = member a x ==> pmember n (ror n a y) (Arith.rotateRight n x y)--correct_not :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Property-correct_not n (a,x) = member a x ==> pmember n (not a) (complement x)--correct_and :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_and n (a,x) (b,y) = member a x ==> member b y ==> pmember n (and a b) (x .&. y)--correct_or :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_or n (a,x) (b,y) = member a x ==> member b y ==> pmember n (or a b) (x .|. y)--correct_xor :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_xor n (a,x) (b,y) = member a x ==> member b y ==> pmember n (xor a b) (x `Bits.xor` y)--correct_testBit :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> Natural -> Property-correct_testBit n (a,x) i =-  i < natValue n ==>-    case testBit a i of-      Just True  -> Bits.testBit x (fromIntegral i)-      Just False -> Prelude.not (Bits.testBit x (fromIntegral i))-      Nothing    -> True+import What4.Domains.BV.Bitwise

@@ -1,192 +1,5 @@-{-|-Module      : What4.Utils.BVDomain.XOR-Copyright   : (c) Galois Inc, 2019-2020-License     : BSD3-Maintainer  : huffman@galois.com--Provides an implementation of bitvector abstract domains-optimized for performing XOR operations.--}--{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}--module What4.Utils.BVDomain.XOR-  ( -- * XOR Domains-    Domain(..)-  , proper-  , bvdMask-  , member-  , pmember-  , range-  , interval-  , bitbounds-  , asSingleton-    -- ** Operations-  , singleton-  , xor-  , and-  , and_scalar--    -- * Correctness properties-  , genDomain-  , genElement-  , genPair--  , correct_singleton-  , correct_xor-  , correct_and-  , correct_and_scalar-  , correct_bitbounds+module What4.Utils.BVDomain.XOR {-# DEPRECATED "Use What4.Domains.BV.XOR instead" #-}+  ( module What4.Domains.BV.XOR   ) where --import qualified Data.Bits as Bits-import           Data.Bits hiding (testBit, xor)-import           Data.Parameterized.NatRepr-import           GHC.TypeNats--import           Prelude hiding (any, concat, negate, and, or, not)--import           Test.Verification ( Property, property, (==>), Gen, chooseInteger )---- | A value of type @'BVDomain' w@ represents a set of bitvectors of--- width @w@.  This is an alternate representation of the bitwise--- domain values, optimized to compute XOR operations.-data Domain (w :: Nat) =-    BVDXor !Integer !Integer !Integer-    -- ^ @BVDXor mask hi unknown@ represents a set of values where-    --   @hi@ is a bitwise high bound, and @unknown@ represents-    --   the bits whose values are not known.  The value @mask@-    --   caches the value @2^w-1@.-  deriving (Show)---- | Test if the domain satisfies its invariants-proper :: NatRepr w -> Domain w -> Bool-proper w (BVDXor mask val u) =-  mask == maxUnsigned w &&-  bitle val mask &&-  bitle u mask &&-  bitle u val---- | Test if the given integer value is a member of the abstract domain-member :: Domain w -> Integer -> Bool-member (BVDXor mask hi unknown) x = hi == (x .&. mask) .|. unknown---- | Return the bitvector mask value from this domain-bvdMask :: Domain w -> Integer-bvdMask (BVDXor mask _ _) = mask---- | Construct a domain from bitwise lower and upper bounds-range :: NatRepr w -> Integer -> Integer -> Domain w-range w lo hi = interval mask lo' hi'-  where-  lo'  = lo .&. mask-  hi'  = hi .&. mask-  mask = maxUnsigned w---- | Unsafe constructor for internal use.-interval :: Integer -> Integer -> Integer -> Domain w-interval mask lo hi = BVDXor mask hi (Bits.xor lo hi)---- | Bitwise lower and upper bounds-bitbounds :: Domain w -> (Integer, Integer)-bitbounds (BVDXor _ hi u) = (Bits.xor u hi, hi)---- | Test if this domain contains a single value, and return it if so-asSingleton :: Domain w -> Maybe Integer-asSingleton (BVDXor _ hi u) = if u == 0 then Just hi else Nothing---- | Random generator for domain values.  We always generate---   nonempty domain values.-genDomain :: NatRepr w -> Gen (Domain w)-genDomain w =-  do let mask = maxUnsigned w-     val <- chooseInteger (0, mask)-     u   <- chooseInteger (0, mask)-     pure $ BVDXor mask (val .|. u) u---- This generator goes to some pains to try--- to generate a good statistical distribution--- of the values in the domain.  It only choses--- random bits for the "unknown" values of--- the domain, then stripes them out among--- the unknown bit positions.-genElement :: Domain w -> Gen Integer-genElement (BVDXor _mask v u) =-   do x <- chooseInteger (0, bit bs - 1)-      pure $ stripe lo x 0--  where-  lo = v `Bits.xor` u-  bs = Bits.popCount u-  stripe val x i-   | x == 0 = val-   | Bits.testBit u i =-       let val' = if Bits.testBit x 0 then setBit val i else val in-       stripe val' (x `shiftR` 1) (i+1)-   | otherwise = stripe val x (i+1)---- | Generate a random nonempty domain and an element---   contained in that domain.-genPair :: NatRepr w -> Gen (Domain w, Integer)-genPair w =-  do a <- genDomain w-     x <- genElement a-     pure (a,x)---- | Return a domain containing just the given value-singleton :: NatRepr w -> Integer -> Domain w-singleton w x = BVDXor mask (x .&. mask) 0-  where-  mask = maxUnsigned w--xor :: Domain w -> Domain w -> Domain w-xor (BVDXor mask va ua) (BVDXor _ vb ub) = BVDXor mask (v .|. u) u-  where-  v = Bits.xor va vb-  u = ua .|. ub--and :: Domain w -> Domain w -> Domain w-and (BVDXor mask va ua) (BVDXor _ vb ub) = BVDXor mask v (v .&. u)-  where-  v = va .&. vb-  u = ua .|. ub--and_scalar :: Integer -> Domain w -> Domain w-and_scalar x (BVDXor mask va ua) = BVDXor mask (va .&. x) (ua .&. x)---------------------------------------------------------------------------- Correctness properties---- | Check that a domain is proper, and that---   the given value is a member-pmember :: NatRepr n -> Domain n -> Integer -> Bool-pmember n a x = proper n a && member a x--correct_singleton :: (1 <= n) => NatRepr n -> Integer -> Integer -> Property-correct_singleton n x y = property (pmember n (singleton n x') y' == (x' == y'))-  where-  x' = toUnsigned n x-  y' = toUnsigned n y--correct_xor :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_xor n (a,x) (b,y) = member a x ==> member b y ==> pmember n (xor a b) (x `Bits.xor` y)--correct_and :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property-correct_and n (a,x) (b,y) = member a x ==> member b y ==> pmember n (and a b) (x .&. y)--correct_and_scalar :: (1 <= n) => NatRepr n -> Integer -> (Domain n, Integer) -> Property-correct_and_scalar n y (a,x) = member a x ==> pmember n (and_scalar y a) (y .&. x)--bitle :: Integer -> Integer -> Bool-bitle x y = (x .|. y) == y--correct_bitbounds :: Domain n -> Integer -> Property-correct_bitbounds a x = property (member a x == (bitle lo x && bitle x hi))-  where-  (lo,hi) = bitbounds a+import What4.Domains.BV.XOR

@@ -1,3 +1,3 @@-module What4.Utils.Endian where+module What4.Utils.Endian {-# DEPRECATED "Use Data.Parameterized.Utils.Endian instead" #-} where  data Endian = LittleEndian | BigEndian deriving (Eq,Show,Ord)

@@ -14,6 +14,7 @@  import What4.BaseTypes import What4.Panic (panic)+import What4.Utils.Arithmetic (roundAway)  -- | Rounding modes for IEEE-754 floating point operations. data RoundingMode@@ -95,7 +96,7 @@   do rat <- floatToRational fp      pure case r of             RNE -> round rat-            RNA -> if rat > 0 then ceiling rat else floor rat+            RNA -> roundAway rat             RTP -> ceiling rat             RTN -> floor rat             RTZ -> truncate rat

@@ -31,7 +31,7 @@ import qualified What4.Protocol.Online as WPO import qualified What4.Protocol.SMTWriter as WPS import qualified What4.SatResult as WSat-import qualified What4.Utils.BVDomain.Arith as WUBA+import qualified What4.Domains.BV.Arith as WUBA  -- | The results of an 'WPO.OnlineSolver' trying to resolve a 'WI.SymBV' as -- concrete.

@@ -13,7 +13,6 @@ {-# LANGUAGE TypeApplications #-}  import           Control.Exception ( displayException, try, SomeException(..), fromException )-import           Control.Lens (folded) import           Control.Monad ( forM, unless ) import           Control.Monad.Except ( runExceptT ) import           Data.BitVector.Sized ( mkBV )@@ -21,6 +20,7 @@ import qualified Data.List as L import           Data.Maybe ( fromMaybe ) import           Data.Text ( pack )+import           Lens.Micro ( folded ) import           System.Environment ( lookupEnv )  import           ProbeSolvers

@@ -1,497 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--{--Module      : BVDomTest-Copyright   : (c) Galois Inc, 2020-License     : BSD3-Maintainer  : rdockins@galois.com--This module performs randomized testing of the bitvector abstract domain-computations, which are among relatively complex.--The intended meaning of the abstract domain computations are-specified using Cryptol in "doc/bvdoman.cry" and realated files.-In those files soundness properites are proved for the implementations.-These tests are intended to supplement those proofs for the actual-implementations, which are transliterated from the Cryptol.--}--import qualified Data.Bits as Bits-import           Test.Tasty-import           Test.Verification-import           VerifyBindings-import           Data.Parameterized.NatRepr-import           Data.Parameterized.Some--import qualified What4.Utils.BVDomain as O-import qualified What4.Utils.BVDomain.Arith as A-import qualified What4.Utils.BVDomain.Bitwise as B-import qualified What4.Utils.BVDomain.XOR as X---main :: IO ()-main = defaultMain $-  setTestOptions $--    testGroup "Bitvector Domain"-    [ arithDomainTests-    , bitwiseDomainTests-    , xorDomainTests-    , overallDomainTests-    , transferTests-    ]--data SomeWidth where-  SW :: (1 <= w) => NatRepr w -> SomeWidth--genWidth :: Gen SomeWidth-genWidth =-  do sz <- getSize-     x <- chooseInt (1, sz+4)-     case someNat x of-       Just (Some n)-         | Just LeqProof <- isPosNat n -> pure (SW n)-       _ -> error "test panic! genWidth"--genBV :: NatRepr w -> Gen Integer-genBV w = chooseInteger (minUnsigned w, maxUnsigned w)---arithDomainTests :: TestTree-arithDomainTests = testGroup "Arith Domain"-  [ genTest "correct_any" $-      do SW n <- genWidth-         A.correct_any n <$> genBV n-  , genTest "correct_ubounds" $-      do SW n <- genWidth-         A.correct_ubounds n <$> A.genPair n-  , genTest "correct_sbounds" $-      do SW n <- genWidth-         A.correct_sbounds n <$> A.genPair n-  , genTest "correct_singleton" $-      do SW n <- genWidth-         A.correct_singleton n <$> genBV n <*> genBV n-  , genTest "correct_overlap" $-      do SW n <- genWidth-         A.correct_overlap <$> A.genDomain n <*> A.genDomain n <*> genBV n-  , genTest "correct_union" $-      do SW n <- genWidth-         A.correct_union n <$> A.genDomain n <*> A.genDomain n <*> genBV n-  , genTest "correct_zero_ext" $-      do SW w <- genWidth-         SW n <- genWidth-         let u = addNat w n-         case testLeq (addNat w (knownNat @1)) u of-           Nothing -> error "impossible!"-           Just LeqProof ->-             do a <- A.genDomain w-                x <- A.genElement a-                pure $ A.correct_zero_ext w a u x-  , genTest "correct_sign_ext" $-      do SW w <- genWidth-         SW n <- genWidth-         let u = addNat w n-         case testLeq (addNat w (knownNat @1)) u of-           Nothing -> error "impossible!"-           Just LeqProof ->-             do a <- A.genDomain w-                x <- A.genElement a-                pure $ A.correct_sign_ext w a u x-  , genTest "correct_concat" $-      do SW m <- genWidth-         SW n <- genWidth-         A.correct_concat m <$> A.genPair m <*> pure n <*> A.genPair n-  , genTest "correct_shrink" $-      do SW i <- genWidth-         SW n <- genWidth-         A.correct_shrink i n <$> A.genPair (addNat i n)-  , genTest "correct_trunc" $-      do SW n <- genWidth-         SW m <- genWidth-         let w = addNat n m-         LeqProof <- pure $ addIsLeq n m-         A.correct_trunc n <$> A.genPair w-  , genTest "correct_select" $-      do SW n <- genWidth-         SW i <- genWidth-         SW z <- genWidth-         let i_n = addNat i n-         let w = addNat i_n z-         LeqProof <- pure $ addIsLeq i_n z-         A.correct_select i n <$> A.genPair w-  , genTest "correct_add" $-      do SW n <- genWidth-         A.correct_add n <$> A.genPair n <*> A.genPair n-  , genTest "correct_neg" $-      do SW n <- genWidth-         A.correct_neg n <$> A.genPair n-  , genTest "correct_not" $-      do SW n <- genWidth-         A.correct_not n <$> A.genPair n-  , genTest "correct_mul" $-      do SW n <- genWidth-         A.correct_mul n <$> A.genPair n <*> A.genPair n-  , genTest "correct_scale" $-      do SW n <- genWidth-         A.correct_scale n <$> genBV n <*> A.genPair n-  , genTest "correct_scale_eq" $-      do SW n <- genWidth-         A.correct_scale_eq n <$> genBV n <*> A.genDomain n-  , genTest "correct_udiv" $-      do SW n <- genWidth-         A.correct_udiv n <$> A.genPair n <*> A.genPair n-  , genTest "correct_urem" $-      do SW n <- genWidth-         A.correct_urem n <$> A.genPair n <*> A.genPair n-  , genTest "correct_sdiv" $-      do SW n <- genWidth-         A.correct_sdiv n <$> A.genPair n <*> A.genPair n-  , genTest "correct_sdivRange" $-      do SW n <- genWidth-         a <- (,) <$> genBV n <*> genBV n-         b <- (,) <$> genBV n <*> genBV n-         x <- genBV n-         y <- genBV n-         pure $ A.correct_sdivRange a b x y-  , genTest "correct_srem" $-      do SW n <- genWidth-         A.correct_srem n <$> A.genPair n <*> A.genPair n-  , genTest "correct_shl"$-      do SW n <- genWidth-         A.correct_shl n <$> A.genPair n <*> A.genPair n-  , genTest "correct_lshr"$-      do SW n <- genWidth-         A.correct_lshr n <$> A.genPair n <*> A.genPair n-  , genTest "correct_ashr"$-      do SW n <- genWidth-         A.correct_ashr n <$> A.genPair n <*> A.genPair n-  , genTest "correct_eq" $-      do SW n <- genWidth-         A.correct_eq n <$> A.genPair n <*> A.genPair n-  , genTest "correct_ult" $-      do SW n <- genWidth-         A.correct_ult n <$> A.genPair n <*> A.genPair n-  , 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-         x <- A.genElement a-         y <- A.genElement a-         pure $ A.correct_unknowns a x y-  , genTest "correct_bitbounds" $-      do SW n <- genWidth-         A.correct_bitbounds n <$> A.genPair n-  ]--xorDomainTests :: TestTree-xorDomainTests =-  testGroup "XOR Domain"-  [ genTest "correct_singleton" $-      do SW n <- genWidth-         X.correct_singleton n <$> genBV n <*> genBV n-  , genTest "correct_xor" $-      do SW n <- genWidth-         X.correct_xor n <$> X.genPair n <*> X.genPair n-  , genTest "correct_and" $-      do SW n <- genWidth-         X.correct_and n <$> X.genPair n <*> X.genPair n-  , genTest "correct_and_scalar" $-      do SW n <- genWidth-         X.correct_and_scalar n <$> genBV n <*> X.genPair n-  , genTest "correct_bitbounds" $-      do SW n <- genWidth-         X.correct_bitbounds <$> X.genDomain n <*> genBV n-  ]--bitwiseDomainTests :: TestTree-bitwiseDomainTests =-  testGroup "Bitwise Domain"-  [ genTest "correct_any" $-      do SW n <- genWidth-         B.correct_any n <$> genBV n-  , genTest "correct_singleton" $-      do SW n <- genWidth-         B.correct_singleton n <$> genBV n <*> genBV n-  , genTest "correct_overlap" $-      do SW n <- genWidth-         B.correct_overlap <$> B.genDomain n <*> B.genDomain n <*> genBV n-  , genTest "correct_union1" $-      do SW n <- genWidth-         (a,x) <- B.genPair n-         b <- B.genDomain n-         pure $ B.correct_union n a b x-  , genTest "correct_union2" $-      do SW n <- genWidth-         a <- B.genDomain n-         (b,x) <- B.genPair n-         pure $ B.correct_union n a b x-  , genTest "correct_intersection" $-      do SW n <- genWidth-         B.correct_intersection <$> B.genDomain n <*> B.genDomain n <*> genBV n-  , genTest "correct_zero_ext" $-      do SW w <- genWidth-         SW n <- genWidth-         let u = addNat w n-         case testLeq (addNat w (knownNat @1)) u of-           Nothing -> error "impossible!"-           Just LeqProof ->-             do a <- B.genDomain w-                x <- B.genElement a-                pure $ B.correct_zero_ext w a u x-  , genTest "correct_sign_ext" $-      do SW w <- genWidth-         SW n <- genWidth-         let u = addNat w n-         case testLeq (addNat w (knownNat @1)) u of-           Nothing -> error "impossible!"-           Just LeqProof ->-             do a <- B.genDomain w-                x <- B.genElement a-                pure $ B.correct_sign_ext w a u x-  , genTest "correct_concat" $-      do SW m <- genWidth-         SW n <- genWidth-         B.correct_concat m <$> B.genPair m <*> pure n <*> B.genPair n-  , genTest "correct_shrink" $-      do SW i <- genWidth-         SW n <- genWidth-         B.correct_shrink i n <$> B.genPair (addNat i n)-  , genTest "correct_trunc" $-      do SW n <- genWidth-         SW m <- genWidth-         let w = addNat n m-         LeqProof <- pure $ addIsLeq n m-         B.correct_trunc n <$> B.genPair w-  , genTest "correct_select" $-      do SW n <- genWidth-         SW i <- genWidth-         SW z <- genWidth-         let i_n = addNat i n-         let w = addNat i_n z-         LeqProof <- pure $ addIsLeq i_n z-         B.correct_select i n <$> B.genPair w-  , genTest "correct_shl"$-      do SW n <- genWidth-         B.correct_shl n <$> B.genPair n <*> chooseInteger (0, intValue n)-  , genTest "correct_lshr"$-      do SW n <- genWidth-         B.correct_lshr n <$> B.genPair n <*> chooseInteger (0, intValue n)-  , genTest "correct_ashr"$-      do SW n <- genWidth-         B.correct_ashr n <$> B.genPair n <*> chooseInteger (0, intValue n)-  , genTest "correct_rol"$-      do SW n <- genWidth-         B.correct_rol n <$> B.genPair n <*> chooseInteger (0, intValue n)-  , genTest "correct_ror"$-      do SW n <- genWidth-         B.correct_ror n <$> B.genPair n <*> chooseInteger (0, intValue n)-  , genTest "correct_eq" $-      do SW n <- genWidth-         B.correct_eq n <$> B.genPair n <*> B.genPair n-  , genTest "correct_not" $-      do SW n <- genWidth-         B.correct_not n <$> B.genPair n-  , genTest "correct_and" $-      do SW n <- genWidth-         B.correct_and n <$> B.genPair n <*> B.genPair n-  , genTest "correct_or" $-      do SW n <- genWidth-         B.correct_or n <$> B.genPair n <*> B.genPair n-  , genTest "correct_xor" $-      do SW n <- genWidth-         B.correct_xor n <$> B.genPair n <*> B.genPair n-  , genTest "correct_testBit" $-      do SW n <- genWidth-         i <- fromInteger <$> chooseInteger (0, intValue n - 1)-         B.correct_testBit n <$> B.genPair n <*> pure i-  ]--overallDomainTests :: TestTree-overallDomainTests = testGroup "Overall Domain"-  [ -- test that the union of consecutive singletons gives a precise interval-    genTest "singleton/union size" $-      do SW n <- genWidth-         let w =  maxUnsigned n-         x <- genBV n-         y <- min 1000 <$> genBV n-         let as = [ O.singleton n ((x + i) Bits..&. w) | i <- [0 .. y] ]-         let a = foldl1 O.union as-         pure $ property (O.size a == y+1)-  , genTest "correct_bra1" $-      do SW n <- genWidth-         O.correct_bra1 n <$> genBV n <*> genBV n-  , genTest "correct_bra2" $-      do SW n <- genWidth-         O.correct_bra2 n <$> genBV n <*> genBV n <*> genBV n-  , genTest "correct_brb1" $-      do SW n <- genWidth-         O.correct_brb1 n <$> genBV n <*> genBV n <*> genBV n-  , genTest "correct_brb2" $-      do SW n <- genWidth-         O.correct_brb2 n <$> genBV n <*> genBV n <*> genBV n <*> genBV n-  , genTest "correct_any" $-      do SW n <- genWidth-         O.correct_any n <$> genBV n-  , genTest "correct_ubounds" $-      do SW n <- genWidth-         O.correct_ubounds n <$> O.genPair n-  , genTest "correct_sbounds" $-      do SW n <- genWidth-         O.correct_sbounds n <$> O.genPair n-  , genTest "correct_singleton" $-      do SW n <- genWidth-         O.correct_singleton n <$> genBV n <*> genBV n-  , genTest "correct_overlap" $-      do SW n <- genWidth-         O.correct_overlap <$> O.genDomain n <*> O.genDomain n <*> genBV n-  , genTest "precise_overlap" $-      do SW n <- genWidth-         O.precise_overlap <$> O.genDomain n <*> O.genDomain n-  , genTest "correct_union" $-      do SW n <- genWidth-         O.correct_union n <$> O.genDomain n <*> O.genDomain n <*> genBV n-  , genTest "correct_zero_ext" $-      do SW w <- genWidth-         SW n <- genWidth-         let u = addNat w n-         case testLeq (addNat w (knownNat @1)) u of-           Nothing -> error "impossible!"-           Just LeqProof ->-             do a <- O.genDomain w-                x <- O.genElement a-                pure $ O.correct_zero_ext w a u x-  , genTest "correct_sign_ext" $-      do SW w <- genWidth-         SW n <- genWidth-         let u = addNat w n-         case testLeq (addNat w (knownNat @1)) u of-           Nothing -> error "impossible!"-           Just LeqProof ->-             do a <- O.genDomain w-                x <- O.genElement a-                pure $ O.correct_sign_ext w a u x-  , genTest "correct_concat" $-      do SW m <- genWidth-         SW n <- genWidth-         O.correct_concat m <$> O.genPair m <*> pure n <*> O.genPair n-  , genTest "correct_select" $-      do SW n <- genWidth-         SW i <- genWidth-         SW z <- genWidth-         let i_n = addNat i n-         let w = addNat i_n z-         LeqProof <- pure $ addIsLeq i_n z-         O.correct_select i n <$> O.genPair w-  , genTest "correct_add" $-      do SW n <- genWidth-         O.correct_add n <$> O.genPair n <*> O.genPair n-  , genTest "correct_neg" $-      do SW n <- genWidth-         O.correct_neg n <$> O.genPair n-  , genTest "correct_scale" $-      do SW n <- genWidth-         O.correct_scale n <$> genBV n <*> O.genPair n-  , genTest "correct_mul" $-      do SW n <- genWidth-         O.correct_mul n <$> O.genPair n <*> O.genPair n-  , genTest "correct_udiv" $-      do SW n <- genWidth-         O.correct_udiv n <$> O.genPair n <*> O.genPair n-  , genTest "correct_urem" $-      do SW n <- genWidth-         O.correct_urem n <$> O.genPair n <*> O.genPair n-  , genTest "correct_sdiv" $-      do SW n <- genWidth-         O.correct_sdiv n <$> O.genPair n <*> O.genPair n-  , genTest "correct_srem" $-      do SW n <- genWidth-         O.correct_srem n <$> O.genPair n <*> O.genPair n-  , genTest "correct_shl"$-      do SW n <- genWidth-         O.correct_shl n <$> O.genPair n <*> O.genPair n-  , genTest "correct_lshr"$-      do SW n <- genWidth-         O.correct_lshr n <$> O.genPair n <*> O.genPair n-  , genTest "correct_ashr"$-      do SW n <- genWidth-         O.correct_ashr n <$> O.genPair n <*> O.genPair n-  , genTest "correct_rol"$-      do SW n <- genWidth-         O.correct_rol n <$> O.genPair n <*> O.genPair n-  , genTest "correct_ror"$-      do SW n <- genWidth-         O.correct_ror n <$> O.genPair n <*> O.genPair n-  , genTest "correct_eq" $-      do SW n <- genWidth-         O.correct_eq n <$> O.genPair n <*> O.genPair n-  , genTest "correct_ult" $-      do SW n <- genWidth-         O.correct_ult n <$> O.genPair n <*> O.genPair n-  , genTest "correct_slt" $-      do SW n <- genWidth-         O.correct_slt n <$> O.genPair n <*> O.genPair n-  , genTest "correct_not" $-      do SW n <- genWidth-         O.correct_not n <$> O.genPair n-  , genTest "correct_and" $-      do SW n <- genWidth-         O.correct_and n <$> O.genPair n <*> O.genPair n-  , genTest "correct_or" $-      do SW n <- genWidth-         O.correct_or n <$> O.genPair n <*> O.genPair n-  , genTest "correct_xor" $-      do SW n <- genWidth-         O.correct_xor n <$> O.genPair n <*> O.genPair n-  , genTest "correct_testBit" $-      do SW n <- genWidth-         i <- fromInteger <$> chooseInteger (0, intValue n - 1)-         O.correct_testBit n <$> O.genPair n <*> pure i-  , genTest "correct_popcnt" $-      do SW n <- genWidth-         O.correct_popcnt n <$> O.genPair n-  , genTest "correct_clz" $-      do SW n <- genWidth-         O.correct_clz n <$> O.genPair n-  , genTest "correct_ctz" $-      do SW n <- genWidth-         O.correct_ctz n <$> O.genPair n-  ]---transferTests :: TestTree-transferTests = testGroup "Transfer"-  [ genTest "correct_arithToBitwise" $-     do SW n <- genWidth-        O.correct_arithToBitwise n <$> A.genPair n-  , genTest "correct_bitwiseToArith" $-     do SW n <- genWidth-        O.correct_bitwiseToArith n <$> B.genPair n-  , genTest "correct_bitwiseToXorDomain" $-     do SW n <- genWidth-        O.correct_bitwiseToXorDomain n <$> B.genPair n-  , genTest "correct_arithToXorDomain" $-     do SW n <- genWidth-        O.correct_arithToXorDomain n <$> A.genPair n-  , genTest "correct_xorToBitwiseDomain" $-     do SW n <- genWidth-        O.correct_xorToBitwiseDomain n <$> X.genPair n-  , genTest "correct_asXorDomain" $-     do SW n <- genWidth-        O.correct_asXorDomain n <$> O.genPair n-  , genTest "correct_fromXorDomain" $-     do SW n <- genWidth-        O.correct_fromXorDomain n <$> X.genPair n-  ]

@@ -57,8 +57,8 @@ import qualified What4.Solver.CVC5 as CVC5 import qualified What4.Solver.Z3 as Z3 import qualified What4.Solver.Yices as Yices-import qualified What4.Utils.BVDomain as WUB-import qualified What4.Utils.BVDomain.Arith as WUBA+import qualified What4.Domains.BV as WUB+import qualified What4.Domains.BV.Arith as WUBA import qualified What4.Utils.ResolveBounds.BV as WURB import           What4.Utils.StringLiteral import           What4.Utils.Versions (ver, SolverBounds(..), emptySolverBounds)@@ -358,6 +358,38 @@       e1 <- iFloatFromBinary sym SingleFloatRepr e0       e1 @?= x +testRealFloatRounding :: TestTree+testRealFloatRounding =+  testCase "real float rounding" $+    withSym FloatRealRepr $ \sym -> do+      x <- iFloatLitSingle sym 1.5+      xUp <- iFloatLitSingle sym 2.0+      xDown <- iFloatLitSingle sym 1.0+      xRNA <- iFloatRound sym RNA x+      xRTP <- iFloatRound sym RTP x+      xRTN <- iFloatRound sym RTN x+      xRTZ <- iFloatRound sym RTZ x+      xRNE <- iFloatRound sym RNE x+      xRNA @?= xUp+      xRTP @?= xUp+      xRTN @?= xDown+      xRTZ @?= xDown+      xRNE @?= xUp++      y <- iFloatLitSingle sym (-1.5)+      yUp <- iFloatLitSingle sym (-1.0)+      yDown <- iFloatLitSingle sym (-2.0)+      yRNA <- iFloatRound sym RNA y+      yRTP <- iFloatRound sym RTP y+      yRTN <- iFloatRound sym RTN y+      yRTZ <- iFloatRound sym RTZ y+      yRNE <- iFloatRound sym RNE y+      yRNA @?= yDown+      yRTP @?= yUp+      yRTN @?= yDown+      yRTZ @?= yUp+      yRNE @?= yDown+ testFloatCastSimplification :: TestTree testFloatCastSimplification = testCase "float cast simplification" $   withSym FloatIEEERepr $ \sym -> do@@ -1161,6 +1193,89 @@        _ -> fail "expected satisfible model" +-- | A regression test for #377.+issue377Test ::+  OnlineSolver solver =>+  SimpleExprBuilder t fs ->+  SolverProcess t solver ->+  IO ()+issue377Test sym solver = do+    -- Construct the following proposition (written in pseudo-Cryptol):+    --+    --   \(f : Float32) (bv3 : [32]) -> lit == f /\ bv2 == bv3+    --     where+    --       lit : Float32+    --       lit = 0.25+    --+    --       bv1, bv2 : [32]+    --       bv1 = fpFromBV rna lit+    --       bv2 = fpFromBV rna f+    let w :: NatRepr 32+        w = knownNat+    let fpp :: FloatPrecisionRepr Prec32+        fpp = knownRepr+    lit <- floatLit sym fpp (bfFromDouble 0.25)+    f <- freshConstant sym (safeSymbol "f") (BaseFloatRepr fpp)+    p1 <- floatEq sym lit f+    bv1 <- floatToBV sym w RNA lit+    bv2 <- floatToBV sym w RNA f+    bv3 <- freshConstant sym (safeSymbol "bv") (BaseBVRepr w)+    p2 <- bvEq sym bv2 bv3+    p <- andPred sym p1 p2++    -- Check that the proposition is satisfiaible and that the model that what4+    -- computes evaluates all of the `bv*` values to `0`.+    checkSatisfiableWithModel solver "test" p $ \case+      Sat fn ->+        do bv1Eval <- groundEval fn bv1+           bv2Eval <- groundEval fn bv2+           bv3Eval <- groundEval fn bv3+           let expected = BV.mkBV w 0+           (all (== expected) [bv1Eval, bv2Eval, bv3Eval]) @? "result other than 0"++      _ -> fail "expected satisfible model"++-- | A regression test for #391.+issue391Test ::+  OnlineSolver solver =>+  SimpleExprBuilder t fs ->+  SolverProcess t solver ->+  IO ()+issue391Test sym solver = do+    -- Construct the following proposition (written in Cryptol):+    --+    --   \(x : [32]) (y : [32]) -> x == xLit /\ y == yLit+    --     where+    --       xLit, yLit : [32]+    --       xLit = 7+    --       yLit = -3+    --+    --       zLit, zSdiv : [32]+    --       zLit = xLit /$ yLit+    --       zSdiv = x /$ y+    let w32 :: NatRepr 32+        w32 = knownNat+    x <- freshConstant sym (safeSymbol "x") (BaseBVRepr w32)+    y <- freshConstant sym (safeSymbol "y") (BaseBVRepr w32)+    xLit <- bvLit sym w32 (BV.mkBV w32 7)+    yLit <- bvLit sym w32 (BV.mkBV w32 (-3))+    xp <- bvEq sym x xLit+    yp <- bvEq sym y yLit+    zLit <- bvSdiv sym xLit yLit+    zSdiv <- bvSdiv sym x y+    p <- andPred sym xp yp++    -- Check that the proposition is satisfiable and that the model that what4+    -- computes evaluates both `zLit` and `zSdiv` to `-2`.+    checkSatisfiableWithModel solver "test" p $ \case+      Sat fn ->+        do zLitEval <- groundEval fn zLit+           zSdivEval <- groundEval fn zSdiv+           let expected = BV.mkBV w32 (-2)+           (all (== expected) [zLitEval, zSdivEval]) @? "result other than -2"++      _ -> fail "expected satisfible model"+ -- | These tests simply ensure that no exceptions are raised. testSolverInfo :: TestTree testSolverInfo = testGroup "solver info queries" $@@ -1325,6 +1440,8 @@         , testCase "Z3 #182 test case" $ withOnlineZ3 issue182Test         , testCase "Z3 #315 test case" $ withOnlineZ3 issue315Test         , testCase "Z3 #329 test case" $ withOnlineZ3 issue329Test+        , testCase "Z3 #377 test case" $ withOnlineZ3 issue377Test+        , testCase "Z3 #391 test case" $ withOnlineZ3 issue391Test          , arrayCopyTest         , arraySetTest@@ -1377,6 +1494,8 @@         , cvcTestCase "#182 test case" $ withCVC issue182Test         , cvcTestCase "#315 test case" $ withCVC issue315Test         , cvcTestCase "#329 test case" $ withCVC issue329Test+        , cvcTestCase "#377 test case" $ withCVC issue377Test+        , cvcTestCase "#391 test case" $ withCVC issue391Test         ]   let cvc4Tests = cvcTests CVC4   let cvc5Tests = cvcTests CVC5@@ -1392,6 +1511,7 @@         , testCase "Yices #182 test case" $ withYices issue182Test         , testCase "Yices #315 test case" $ withYices issue315Test         , testCase "Yices #329 test case" $ withYices issue329Test+        , testCase "Yices #391 test case" $ withYices issue391Test         ]   let bitwuzlaTests =         [ testCase "Bitwuzla multidim array" $ withBitwuzla multidimArrayTest@@ -1404,6 +1524,7 @@     , testInterpretedFloatIEEE     , testFloatBinarySimplification     , testRealFloatBinarySimplification+    , testRealFloatRounding     , testFloatCastSimplification     , testFloatCastNoSimplification     , testBVSelectShl

@@ -35,6 +35,7 @@ import           What4.Internal (assertionsEnabled)  import Bool (boolTests)+import WeightedSum (weightedSumTests)  type IteExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs @@ -392,4 +393,5 @@     (fromConcreteString <$> s) === Just ""   , testInjectiveConversions   , boolTests+  , weightedSumTests   ]

@@ -1,36 +0,0 @@-{-# LANGUAGE LambdaCase #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}--module VerifyBindings where--import           Control.Applicative-import           Hedgehog-import qualified Hedgehog.Gen as Gen-import qualified Hedgehog.Range as Range-import           Test.Tasty-import           Test.Tasty.Hedgehog.Alt-import qualified Test.Verification as V---verifyGenerators :: V.GenEnv Gen-verifyGenerators = V.GenEnv { V.genChooseBool = Gen.bool-                            , V.genChooseInteger = \r -> Gen.integral (uncurry Range.linear r)-                            , V.genChooseInt = \r -> Gen.int (uncurry Range.linear r)-                            , V.genGetSize = Gen.sized (\s -> return $ unSize s)-                            }---genTest :: String -> V.Gen V.Property -> TestTree-genTest nm p = testProperty nm $ property $ mkProp =<< (forAll $ V.toNativeProperty verifyGenerators p)-  where mkProp (V.BoolProperty b) = test $ assert b-        mkProp (V.AssumptionProp a) = if (V.preCondition a) then (mkProp $ V.assumedProp a) else discard---setTestOptions :: TestTree -> TestTree-setTestOptions =-  -- some tests discard a lot of values based on preconditions;-  -- this helps prevent those tests from failing for insufficent coverage-  localOption (HedgehogDiscardLimit (Just 500000)) .--  -- run at least 5000 tests-  adjustOption (\(HedgehogTestLimit x) -> HedgehogTestLimit (max 5000 <$> x <|> Just 5000))

@@ -17,7 +17,6 @@  import           Control.Concurrent ( threadDelay ) import           Control.Concurrent.Async ( race )-import           Control.Lens (folded) import           Control.Monad ( forM ) import           Control.Monad.Catch ( MonadMask ) import           Control.Monad.IO.Class ( MonadIO )@@ -28,6 +27,7 @@ import           Data.Metrology.SI ( Time, milli, micro, nano, Second(..) ) import           Data.Metrology.Show () import           Data.Proxy+import           Lens.Micro ( folded ) import qualified Prettyprinter as PP import           System.Clock import           System.Environment ( lookupEnv )@@ -293,6 +293,150 @@ ----------------------------------------------------------------------  +-- | Test that persistent side conditions (e.g., Nat >= 0) are preserved after 'reset'.+--+-- When a fresh Nat variable is created and sent to the solver, 'mkExpr'+-- declares it and adds a side condition @n >= 0@ via 'addPartialSideCond'.+-- After 'reset' (which sends @(reset-assertions)@), these side conditions+-- should still hold.+--+-- We use an unconstrained integer @m@ linked to @n@ via @m = n@ to prevent+-- the ExprBuilder from optimizing away the check based on abstract domains.+mkResetSideCondTest :: (SolverTestData, SolverVersion) -> TestTree+mkResetSideCondTest ((SolverName nm, AnOnlineSolver (Proxy :: Proxy s), features, opts, _), _)+  | not (hasProblemFeature features useIntegerArithmetic) || nm == "STP" -- stp times out+  = testCase nm $ assertBool "skipped (no integer support)" True+  | otherwise+  = testCase nm $ withIONonceGenerator $ \gen -> do+    sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen+    extendConfig opts (getConfiguration sym)+    proc <- startSolverProcess @s features Nothing sym+    let conn = solverConn proc++    n <- freshNat sym (safeSymbol "n")+    nInt <- natToInteger sym n+    m <- freshConstant sym (safeSymbol "m") BaseIntegerRepr+    mEqN <- intEq sym m nInt++    -- Force mkExpr to process n (which declares it and adds n >= 0 side condition)+    inNewFrame proc $ do+      assume conn mEqN+      check proc "m = n before reset" >>= \case+        Unsat _ -> fail "m = n should be SAT"+        Unknown -> fail "Solver returned UNKNOWN"+        Sat _ -> return ()++    -- Reset clears all assertions via (reset-assertions), including n >= 0+    reset proc++    -- After reset, re-assert m = n and check if m < 0 is satisfiable.+    -- With n >= 0 side condition: m = n >= 0, so m < 0 is UNSAT.+    -- Without n >= 0 side condition: m = n, n unconstrained, m < 0 is SAT.+    zero <- intLit sym 0+    mNeg <- intLt sym m zero+    inNewFrame proc $ do+      assume conn mEqN+      assume conn mNeg+      check proc "m < 0 after reset" >>= \case+        Unsat _ -> return ()  -- Correct: n >= 0 side condition preserved+        Unknown -> fail "Solver returned UNKNOWN"+        Sat _ -> assertFailure+          "Side conditions lost after reset: m = n and m < 0 was SAT (n should be >= 0)"++-- | Test that reset actually clears regular assertions.+--+-- This test verifies the basic semantics of reset: that it forgets+-- all previously asserted formulas. We assert a formula, reset, then+-- assert its negation. If reset worked, the negation should be SAT.+-- If reset failed to clear the original assertion, we'd get UNSAT.+mkResetClearsAssertionsTest :: (SolverTestData, SolverVersion) -> TestTree+mkResetClearsAssertionsTest ((SolverName nm, AnOnlineSolver (Proxy :: Proxy s), features, opts, _), _)+  | not (hasProblemFeature features useIntegerArithmetic) || nm == "STP" -- stp times out+  = testCase nm $ assertBool "skipped (no integer support)" True+  | otherwise+  = testCase nm $ withIONonceGenerator $ \gen -> do+    sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen+    extendConfig opts (getConfiguration sym)+    proc <- startSolverProcess @s features Nothing sym+    let conn = solverConn proc++    -- Create an unconstrained integer variable+    n <- freshConstant sym (safeSymbol "n") BaseIntegerRepr+    zero <- intLit sym 0++    -- Assert n >= 0 and verify it's satisfiable+    nNonNegative <- intLe sym zero n+    inNewFrame proc $ do+      assume conn nNonNegative+      check proc "n >= 0 before reset" >>= \case+        Unsat _ -> fail "n >= 0 should be SAT"+        Unknown -> fail "Solver returned UNKNOWN"+        Sat _ -> return ()++    -- Reset should clear all assertions including n >= 0+    reset proc++    -- Now assert n < 0, which contradicts the previous assertion.+    -- If reset worked: n < 0 should be SAT (previous assertion cleared)+    -- If reset failed: n < 0 would be UNSAT (n >= 0 still asserted)+    nNegative <- intLt sym n zero+    inNewFrame proc $ do+      assume conn nNegative+      check proc "n < 0 after reset" >>= \case+        Sat _ -> return ()  -- Correct: reset cleared the previous assertion+        Unknown -> fail "Solver returned UNKNOWN"+        Unsat _ -> assertFailure+          "Reset failed to clear assertions: n < 0 is UNSAT (n >= 0 still asserted)"++-- | Test that operation-specific side conditions are not recorded as persistent.+--+-- Operations like RealSqrt add side conditions via addSideCondition within appSMTExpr.+-- These should NOT be added to the persistentSideConditions list (only side conditions+-- from addPartialSideCond for DeleteNever variables should persist). This test verifies+-- that sqrt operations work correctly across reset with independent fresh variables.+mkResetOperationSideCondsTest :: (SolverTestData, SolverVersion) -> TestTree+mkResetOperationSideCondsTest ((SolverName nm, AnOnlineSolver (Proxy :: Proxy s), features, opts, _), _)+  | not (hasProblemFeature features useNonlinearArithmetic)+  = testCase nm $ assertBool "skipped (no real/nonlinear support)" True+  | otherwise+  = testCase nm $ withIONonceGenerator $ \gen -> do+    sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen+    extendConfig opts (getConfiguration sym)+    proc <- startSolverProcess @s features Nothing sym+    let conn = solverConn proc++    -- Create x1 and assert sqrt(x1) = 2+    -- This creates fresh variable for sqrt result with side conditions+    x1 <- freshConstant sym (safeSymbol "x1") BaseRealRepr+    sqrt_x1 <- realSqrt sym x1+    two <- realLit sym 2+    sqrt_eq_2 <- realEq sym sqrt_x1 two++    inNewFrame proc $ do+      assume conn sqrt_eq_2+      check proc "sqrt(x1) = 2 before reset" >>= \case+        Unsat _ -> fail "sqrt(x1) = 2 should be SAT"+        Unknown -> fail "Solver returned UNKNOWN"+        Sat _ -> return ()++    -- Reset clears all assertions (but not variable declarations)+    reset proc++    -- Create x2 and assert sqrt(x2) = 3+    -- This creates a NEW fresh variable for this sqrt result+    -- Operation side conditions are NOT persistent, only freshConstant bounds are+    x2 <- freshConstant sym (safeSymbol "x2") BaseRealRepr+    sqrt_x2 <- realSqrt sym x2+    three <- realLit sym 3+    sqrt_eq_3 <- realEq sym sqrt_x2 three++    inNewFrame proc $ do+      assume conn sqrt_eq_3+      check proc "sqrt(x2) = 3 after reset" >>= \case+        Unsat _ -> fail "sqrt(x2) = 3 should be SAT"+        Unknown -> fail "Solver returned UNKNOWN"+        Sat _ -> return ()  -- Correct: independent sqrt operation works+ main :: IO () main = do   testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"@@ -305,6 +449,9 @@       testGroup "SmokeTest" $ map mkSmokeTest solvers     , testGroup "QuickStart Framed" $ map (quickstartTest True)  solvers     , testGroup "QuickStart Direct" $ map (quickstartTest False) solvers+    , testGroup "Reset Side Conditions" $ map mkResetSideCondTest solvers+    , testGroup "Reset Clears Assertions" $ map mkResetClearsAssertionsTest solvers+    , testGroup "Reset Operation Side Conditions" $ map mkResetOperationSideCondsTest solvers     , timeoutTests testLevel solvers     ] 

@@ -1,35 +0,0 @@-{-# LANGUAGE LambdaCase #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}--module VerifyBindings where--import           Test.Tasty-import           Test.Tasty.QuickCheck-import qualified Test.Verification as V---instance Testable V.Property where-  property = \case-    V.BoolProperty b -> property b-    V.AssumptionProp a -> (V.preCondition a) ==> (V.assumedProp a)--verifyGenerators :: V.GenEnv Gen-verifyGenerators = V.GenEnv { V.genChooseBool = elements [ True, False ]-                            , V.genChooseInteger = \r -> choose r-                            , V.genChooseInt = \r -> choose r-                            , V.genGetSize = getSize-                            }---genTest :: String -> V.Gen V.Property -> TestTree-genTest nm p = testProperty nm (property $ V.toNativeProperty verifyGenerators p)---setTestOptions :: TestTree -> TestTree-setTestOptions =-  -- some tests discard a lot of values based on preconditions;-  -- this helps prevent those tests from failing for insufficent coverage-  localOption (QuickCheckMaxRatio 1000) .--  -- run at least 5000 tests-  adjustOption (\(QuickCheckTests x) -> QuickCheckTests (max x 5000))

@@ -0,0 +1,241 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module WeightedSum (weightedSumTests) where++import Data.Hashable (Hashable(..))+import qualified Data.BitVector.Sized as BV+import Data.Maybe (isNothing)+import Data.Parameterized.Classes++import qualified Hedgehog as H+import qualified Hedgehog.Gen as Gen+import qualified Hedgehog.Range as Range++import Test.Tasty (TestTree, testGroup)+import Test.Tasty.Hedgehog.Alt++import What4.BaseTypes+import qualified What4.Expr.WeightedSum as WSum+import qualified What4.SemiRing as SR+import qualified What4.Utils.AbstractDomains as AD++-------------------------------------------------------------------------------+-- Mock Expression Type+-------------------------------------------------------------------------------++-- | Mock expression type for testing WeightedSum without a full ExprBuilder+--+-- The Int field serves as a unique identifier for each mock expression,+-- allowing us to define Eq, Ord, and Hashable instances based solely on identity.+data MockExpr (tp :: BaseType) = MockExpr Int (BaseTypeRepr tp)+  deriving (Show)++instance Eq (MockExpr tp) where+  MockExpr i _ == MockExpr j _ = i == j++instance Ord (MockExpr tp) where+  compare (MockExpr i _) (MockExpr j _) = compare i j++instance Hashable (MockExpr tp) where+  hashWithSalt s (MockExpr i _) = s `hashWithSalt` i++instance TestEquality MockExpr where+  testEquality (MockExpr i repr1) (MockExpr j repr2)+    | i == j = testEquality repr1 repr2+    | otherwise = Nothing++instance OrdF MockExpr where+  compareF (MockExpr i repr1) (MockExpr j repr2) =+    case compare i j of+      LT -> LTF+      GT -> GTF+      EQ -> case compareF repr1 repr2 of+        LTF -> LTF+        GTF -> GTF+        EQF -> EQF++instance HashableF MockExpr where+  hashWithSaltF s (MockExpr i _) = s `hashWithSalt` i++instance AD.HasAbsValue MockExpr where+  getAbsValue (MockExpr _ repr) = AD.avTop repr++-------------------------------------------------------------------------------+-- Generators+-------------------------------------------------------------------------------++genMockExpr :: KnownRepr BaseTypeRepr tp => H.Gen (MockExpr tp)+genMockExpr = MockExpr <$> Gen.int (Range.linear 0 100) <*> pure knownRepr++genBV8Constant :: H.Gen (BV.BV 8)+genBV8Constant = BV.mkBV knownNat . fromIntegral <$> Gen.int (Range.linear 0 255)++genWeightedSumBV8 :: H.Gen (WSum.WeightedSum MockExpr (SR.SemiRingBV SR.BVArith 8))+genWeightedSumBV8 = do+  offset <- genBV8Constant+  numTerms <- Gen.int (Range.linear 0 3)+  terms <- Gen.list (Range.singleton numTerms) $ do+    key <- genMockExpr @(BaseBVType 8)+    coeff <- genBV8Constant+    pure (key, coeff)+  let sr = SR.SemiRingBVRepr SR.BVArithRepr (knownNat @8)+  pure $ WSum.fromTerms sr terms offset++-- Generator for products+genProductBV8 :: H.Gen (WSum.SemiRingProduct MockExpr (SR.SemiRingBV SR.BVBits 8))+genProductBV8 = do+  numTerms <- Gen.int (Range.linear 1 3)+  terms <- Gen.list (Range.singleton numTerms) $ genMockExpr @(BaseBVType 8)+  let sr = SR.SemiRingBVRepr SR.BVBitsRepr (knownNat @8)+  pure $ foldl1 WSum.prodMul (map (WSum.prodVar sr) terms)++-------------------------------------------------------------------------------+-- Properties+-------------------------------------------------------------------------------++-- | Test that addition is associative: (a + b) + c == a + (b + c)+propAddAssociative :: H.Property+propAddAssociative = H.property $ do+  s1 <- H.forAllWith (const "WeightedSum") genWeightedSumBV8+  s2 <- H.forAllWith (const "WeightedSum") genWeightedSumBV8+  s3 <- H.forAllWith (const "WeightedSum") genWeightedSumBV8+  let sr = SR.SemiRingBVRepr SR.BVArithRepr (knownNat @8)+  let lhs = WSum.add sr (WSum.add sr s1 s2) s3+  let rhs = WSum.add sr s1 (WSum.add sr s2 s3)+  H.assert $ lhs == rhs++-- | Test that zero is the additive identity: s + 0 == s+propAddIdentity :: H.Property+propAddIdentity = H.property $ do+  s <- H.forAllWith (const "WeightedSum") genWeightedSumBV8+  let sr = SR.SemiRingBVRepr SR.BVArithRepr (knownNat @8)+  let zero = WSum.constant sr (SR.zero sr)+  let result = WSum.add sr s zero+  H.assert $ result == s++-- | Test that adding constants is associative: (s + c1) + c2 == s + (c1 + c2)+propAddConstantAssociative :: H.Property+propAddConstantAssociative = H.property $ do+  s <- H.forAllWith (const "WeightedSum") genWeightedSumBV8+  c1 <- H.forAll genBV8Constant+  c2 <- H.forAll genBV8Constant+  let sr = SR.SemiRingBVRepr SR.BVArithRepr (knownNat @8)+  let lhs = WSum.addConstant sr (WSum.addConstant sr s c1) c2+  let rhs = WSum.addConstant sr s (SR.add sr c1 c2)+  H.assert $ lhs == rhs++-- | Test scalar multiplication distributivity: (c1 + c2) * x == c1*x + c2*x+propScalarDistributivity :: H.Property+propScalarDistributivity = H.property $ do+  c1 <- H.forAll genBV8Constant+  c2 <- H.forAll genBV8Constant+  x <- H.forAll (genMockExpr @(BaseBVType 8))+  let sr = SR.SemiRingBVRepr SR.BVArithRepr (knownNat @8)+  let lhs = WSum.scaledVar sr (SR.add sr c1 c2) x+  let rhs = WSum.add sr (WSum.scaledVar sr c1 x) (WSum.scaledVar sr c2 x)+  H.assert $ lhs == rhs++-- | Test that scaling is associative: scale c1 (scale c2 s) == scale (c1*c2) s+propScaleAssociative :: H.Property+propScaleAssociative = H.property $ do+  s <- H.forAllWith (const "WeightedSum") genWeightedSumBV8+  c1 <- H.forAll genBV8Constant+  c2 <- H.forAll genBV8Constant+  let sr = SR.SemiRingBVRepr SR.BVArithRepr (knownNat @8)+  let lhs = WSum.scale sr c1 (WSum.scale sr c2 s)+  let rhs = WSum.scale sr (SR.mul sr c1 c2) s+  H.assert $ lhs == rhs++-- | Test that scaling distributes over addition: c * (s1 + s2) == c*s1 + c*s2+propScaleDistributesOverAdd :: H.Property+propScaleDistributesOverAdd = H.property $ do+  s1 <- H.forAllWith (const "WeightedSum") genWeightedSumBV8+  s2 <- H.forAllWith (const "WeightedSum") genWeightedSumBV8+  c <- H.forAll genBV8Constant+  let sr = SR.SemiRingBVRepr SR.BVArithRepr (knownNat @8)+  let lhs = WSum.scale sr c (WSum.add sr s1 s2)+  let rhs = WSum.add sr (WSum.scale sr c s1) (WSum.scale sr c s2)+  H.assert $ lhs == rhs++-- | Test cancellation: adding opposite scalars cancels out (c*x + (-c)*x == 0)+propCancellation :: H.Property+propCancellation = H.property $ do+  c <- H.forAll genBV8Constant+  x <- H.forAll (genMockExpr @(BaseBVType 8))+  let sr = SR.SemiRingBVRepr SR.BVArithRepr (knownNat @8)+  let negC = BV.negate (knownNat @8) c+  let result = WSum.add sr (WSum.scaledVar sr c x) (WSum.scaledVar sr negC x)+  -- After cancellation, should be just the constant (no variable terms)+  H.assert $ isNothing (WSum.asVar result)++-------------------------------------------------------------------------------+-- Product Properties+-------------------------------------------------------------------------------++-- | Test that multiplication is associative: (a * b) * c == a * (b * c)+propMulAssociative :: H.Property+propMulAssociative = H.property $ do+  p1 <- H.forAllWith (const "Product") genProductBV8+  p2 <- H.forAllWith (const "Product") genProductBV8+  p3 <- H.forAllWith (const "Product") genProductBV8+  let lhs = WSum.prodMul (WSum.prodMul p1 p2) p3+  let rhs = WSum.prodMul p1 (WSum.prodMul p2 p3)+  H.assert $ lhs == rhs++-- | Test that multiplication is commutative: a * b == b * a+propMulCommutative :: H.Property+propMulCommutative = H.property $ do+  p1 <- H.forAllWith (const "Product") genProductBV8+  p2 <- H.forAllWith (const "Product") genProductBV8+  let lhs = WSum.prodMul p1 p2+  let rhs = WSum.prodMul p2 p1+  H.assert $ lhs == rhs++-- | Test that single variable product is idempotent: var x * var x == var x+-- (in the BVBits semiring, which is idempotent)+propProdVarIdempotent :: H.Property+propProdVarIdempotent = H.property $ do+  x <- H.forAll (genMockExpr @(BaseBVType 8))+  let sr = SR.SemiRingBVRepr SR.BVBitsRepr (knownNat @8)+  let var_x = WSum.prodVar sr x+  let result = WSum.prodMul var_x var_x+  H.assert $ result == var_x++-------------------------------------------------------------------------------+-- Test Tree+-------------------------------------------------------------------------------++weightedSumTests :: TestTree+weightedSumTests = testGroup "WeightedSum and SemiRingProduct"+  [ testGroup "WeightedSum (Sums)"+      [ testProperty "Addition is associative" $+          H.withTests 2048 propAddAssociative+      , testProperty "Zero is additive identity" $+          H.withTests 2048 propAddIdentity+      , testProperty "Adding constants is associative" $+          H.withTests 2048 propAddConstantAssociative+      , testProperty "Scalar multiplication distributes" $+          H.withTests 2048 propScalarDistributivity+      , testProperty "Scaling is associative" $+          H.withTests 2048 propScaleAssociative+      , testProperty "Scaling distributes over addition" $+          H.withTests 2048 propScaleDistributesOverAdd+      , testProperty "Adding opposite scalars cancels" $+          H.withTests 2048 propCancellation+      ]+  , testGroup "SemiRingProduct (Products)"+      [ testProperty "Multiplication is associative" $+          H.withTests 2048 propMulAssociative+      , testProperty "Multiplication is commutative" $+          H.withTests 2048 propMulCommutative+      , testProperty "Product variable is idempotent (BVBits)" $+          H.withTests 2048 propProdVarIdempotent+      ]+  ]

@@ -1,6 +1,6 @@ Cabal-version: 2.4 Name:          what4-Version:       1.7.3+Version:       1.8 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com Copyright:     (c) Galois, Inc 2014-2023@@ -9,7 +9,7 @@ Build-type:    Simple Homepage:      https://github.com/GaloisInc/what4 Bug-reports:   https://github.com/GaloisInc/what4/issues-Tested-with:   GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.2, GHC==9.4.4, GHC==9.6.2, GHC==9.8.1, GHC==9.10.1+Tested-with:   GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.2, GHC==9.4.4, GHC==9.6.2, GHC==9.8.1, GHC==9.10.1, GHC==9.12.2 Category:      Formal Methods, Theorem Provers, Symbolic Computation, SMT Synopsis:      Solver-agnostic symbolic values support for issuing queries Description:@@ -30,12 +30,7 @@ Extra-doc-files:   README.md   CHANGES.md-  doc/README.md   doc/implementation.md-  doc/bvdomain.cry-  doc/arithdomain.cry-  doc/bitsdomain.cry-  doc/xordomain.cry  source-repository head   type: git@@ -111,13 +106,15 @@     hashable >= 1.3,     hashtables >= 1.2.3,     io-streams >= 1.5,-    lens >= 4.18,+    microlens >= 0.5,+    microlens-mtl,+    microlens-th,     libBF >= 0.6 && < 0.7,     megaparsec >= 8 && < 10,     mtl >= 2.2.1,     ordered-containers >= 0.2 && < 0.3,     panic >= 0.3,-    parameterized-utils >= 2.1 && < 2.2,+    parameterized-utils >= 2.3 && < 2.4,     parsec >= 3 && < 4,     prettyprinter >= 1.7.0,     process >= 1.2,@@ -134,6 +131,7 @@     unordered-containers >= 0.2.10,     vector >= 0.12.1,     versions >= 6.0.2 && < 6.1,+    what4-domains,     zenc >= 0.1.0 && < 0.2.0,    default-extensions:@@ -285,7 +283,7 @@     bv-sized,     bytestring,     containers,-    lens,+    microlens,     mtl >= 2.2.1,     process,     tasty-expected-failure >= 0.12 && < 0.13,@@ -334,7 +332,7 @@     clock,     containers,     exceptions,-    lens,+    microlens,     prettyprinter,     process,     tasty-expected-failure >= 0.12 && < 0.13,@@ -362,7 +360,8 @@     tasty-expected-failure >= 0.12 && < 0.13,     tasty-checklist >= 1.0.3 && < 1.1,     text,-    versions+    versions,+    what4-domains   test-suite exprs_tests@@ -374,9 +373,11 @@   other-modules:     Bool     GenWhat4Expr+    WeightedSum    build-depends: bv-sized                , containers+               , hashable                , mtl  executable bool-normalization@@ -399,30 +400,6 @@    build-depends: bv-sized                , containers >= 0.5.0.0---test-suite bvdomain_tests-  import: bldflags, testdefs-quickcheck-  type: exitcode-stdio-1.0--  hs-source-dirs: test/QC-  main-is: BVDomTests.hs--  other-modules:  VerifyBindings--  build-depends: transformers---test-suite bvdomain_tests_hh-  import: bldflags, testdefs-hedgehog-  type: exitcode-stdio-1.0--  hs-source-dirs: test/HH-  main-is: BVDomTests.hs--  other-modules:  VerifyBindings--  build-depends: transformers   test-suite template_tests