diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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 diff --git a/doc/README.md b/doc/README.md deleted file mode 100644 --- a/doc/README.md +++ /dev/null @@ -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 (). - -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. diff --git a/doc/arithdomain.cry b/doc/arithdomain.cry deleted file mode 100644 --- a/doc/arithdomain.cry +++ /dev/null @@ -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} diff --git a/doc/bitsdomain.cry b/doc/bitsdomain.cry deleted file mode 100644 --- a/doc/bitsdomain.cry +++ /dev/null @@ -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} diff --git a/doc/bvdomain.cry b/doc/bvdomain.cry deleted file mode 100644 --- a/doc/bvdomain.cry +++ /dev/null @@ -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} diff --git a/doc/xordomain.cry b/doc/xordomain.cry deleted file mode 100644 --- a/doc/xordomain.cry +++ /dev/null @@ -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} diff --git a/src/Test/Verification.hs b/src/Test/Verification.hs --- a/src/Test/Verification.hs +++ b/src/Test/Verification.hs @@ -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 diff --git a/src/What4/Config.hs b/src/What4/Config.hs --- a/src/What4/Config.hs +++ b/src/What4/Config.hs @@ -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. diff --git a/src/What4/Expr/Allocator.hs b/src/What4/Expr/Allocator.hs --- a/src/What4/Expr/Allocator.hs +++ b/src/What4/Expr/Allocator.hs @@ -19,7 +19,7 @@ , cacheOptDesc ) where -import Control.Lens ( (&) ) +import Lens.Micro ( (&) ) import Control.Monad.ST (stToIO) import Data.IORef diff --git a/src/What4/Expr/App.hs b/src/What4/Expr/App.hs --- a/src/What4/Expr/App.hs +++ b/src/What4/Expr/App.hs @@ -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{} -> () diff --git a/src/What4/Expr/BoolMap.hs b/src/What4/Expr/BoolMap.hs --- a/src/What4/Expr/BoolMap.hs +++ b/src/What4/Expr/BoolMap.hs @@ -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) diff --git a/src/What4/Expr/Builder.hs b/src/What4/Expr/Builder.hs --- a/src/What4/Expr/Builder.hs +++ b/src/What4/Expr/Builder.hs @@ -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) diff --git a/src/What4/Expr/GroundEval.hs b/src/What4/Expr/GroundEval.hs --- a/src/What4/Expr/GroundEval.hs +++ b/src/What4/Expr/GroundEval.hs @@ -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 diff --git a/src/What4/Expr/Simplify.hs b/src/What4/Expr/Simplify.hs --- a/src/What4/Expr/Simplify.hs +++ b/src/What4/Expr/Simplify.hs @@ -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) diff --git a/src/What4/Expr/UnaryBV.hs b/src/What4/Expr/UnaryBV.hs --- a/src/What4/Expr/UnaryBV.hs +++ b/src/What4/Expr/UnaryBV.hs @@ -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 diff --git a/src/What4/Expr/VarIdentification.hs b/src/What4/Expr/VarIdentification.hs --- a/src/What4/Expr/VarIdentification.hs +++ b/src/What4/Expr/VarIdentification.hs @@ -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 diff --git a/src/What4/Expr/WeightedSum.hs b/src/What4/Expr/WeightedSum.hs --- a/src/What4/Expr/WeightedSum.hs +++ b/src/What4/Expr/WeightedSum.hs @@ -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) => diff --git a/src/What4/Interface.hs b/src/What4/Interface.hs --- a/src/What4/Interface.hs +++ b/src/What4/Interface.hs @@ -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 . 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) diff --git a/src/What4/LabeledPred.hs b/src/What4/LabeledPred.hs --- a/src/What4/LabeledPred.hs +++ b/src/What4/LabeledPred.hs @@ -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) diff --git a/src/What4/Partial.hs b/src/What4/Partial.hs --- a/src/What4/Partial.hs +++ b/src/What4/Partial.hs @@ -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) diff --git a/src/What4/ProgramLoc.hs b/src/What4/ProgramLoc.hs --- a/src/What4/ProgramLoc.hs +++ b/src/What4/ProgramLoc.hs @@ -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 diff --git a/src/What4/Protocol/Online.hs b/src/What4/Protocol/Online.hs --- a/src/What4/Protocol/Online.hs +++ b/src/What4/Protocol/Online.hs @@ -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) diff --git a/src/What4/Protocol/PolyRoot.hs b/src/What4/Protocol/PolyRoot.hs --- a/src/What4/Protocol/PolyRoot.hs +++ b/src/What4/Protocol/PolyRoot.hs @@ -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 diff --git a/src/What4/Protocol/ReadDecimal.hs b/src/What4/Protocol/ReadDecimal.hs --- a/src/What4/Protocol/ReadDecimal.hs +++ b/src/What4/Protocol/ReadDecimal.hs @@ -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 diff --git a/src/What4/Protocol/SExp.hs b/src/What4/Protocol/SExp.hs --- a/src/What4/Protocol/SExp.hs +++ b/src/What4/Protocol/SExp.hs @@ -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 diff --git a/src/What4/Protocol/SMTLib2/Syntax.hs b/src/What4/Protocol/SMTLib2/Syntax.hs --- a/src/What4/Protocol/SMTLib2/Syntax.hs +++ b/src/What4/Protocol/SMTLib2/Syntax.hs @@ -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 ':') . diff --git a/src/What4/Protocol/SMTWriter.hs b/src/What4/Protocol/SMTWriter.hs --- a/src/What4/Protocol/SMTWriter.hs +++ b/src/What4/Protocol/SMTWriter.hs @@ -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 diff --git a/src/What4/SFloat.hs b/src/What4/SFloat.hs --- a/src/What4/SFloat.hs +++ b/src/What4/SFloat.hs @@ -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 diff --git a/src/What4/Solver/DReal.hs b/src/What4/Solver/DReal.hs --- a/src/What4/Solver/DReal.hs +++ b/src/What4/Solver/DReal.hs @@ -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) diff --git a/src/What4/Solver/Yices.hs b/src/What4/Solver/Yices.hs --- a/src/What4/Solver/Yices.hs +++ b/src/What4/Solver/Yices.hs @@ -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 diff --git a/src/What4/Utils/AbstractDomains.hs b/src/What4/Utils/AbstractDomains.hs --- a/src/What4/Utils/AbstractDomains.hs +++ b/src/What4/Utils/AbstractDomains.hs @@ -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 diff --git a/src/What4/Utils/AnnotatedMap.hs b/src/What4/Utils/AnnotatedMap.hs --- a/src/What4/Utils/AnnotatedMap.hs +++ b/src/What4/Utils/AnnotatedMap.hs @@ -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 diff --git a/src/What4/Utils/Arithmetic.hs b/src/What4/Utils/Arithmetic.hs --- a/src/What4/Utils/Arithmetic.hs +++ b/src/What4/Utils/Arithmetic.hs @@ -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 -} -> diff --git a/src/What4/Utils/BVDomain.hs b/src/What4/Utils/BVDomain.hs --- a/src/What4/Utils/BVDomain.hs +++ b/src/What4/Utils/BVDomain.hs @@ -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 diff --git a/src/What4/Utils/BVDomain/Arith.hs b/src/What4/Utils/BVDomain/Arith.hs --- a/src/What4/Utils/BVDomain/Arith.hs +++ b/src/What4/Utils/BVDomain/Arith.hs @@ -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 diff --git a/src/What4/Utils/BVDomain/Bitwise.hs b/src/What4/Utils/BVDomain/Bitwise.hs --- a/src/What4/Utils/BVDomain/Bitwise.hs +++ b/src/What4/Utils/BVDomain/Bitwise.hs @@ -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 diff --git a/src/What4/Utils/BVDomain/XOR.hs b/src/What4/Utils/BVDomain/XOR.hs --- a/src/What4/Utils/BVDomain/XOR.hs +++ b/src/What4/Utils/BVDomain/XOR.hs @@ -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 diff --git a/src/What4/Utils/Endian.hs b/src/What4/Utils/Endian.hs --- a/src/What4/Utils/Endian.hs +++ b/src/What4/Utils/Endian.hs @@ -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) diff --git a/src/What4/Utils/FloatHelpers.hs b/src/What4/Utils/FloatHelpers.hs --- a/src/What4/Utils/FloatHelpers.hs +++ b/src/What4/Utils/FloatHelpers.hs @@ -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 diff --git a/src/What4/Utils/ResolveBounds/BV.hs b/src/What4/Utils/ResolveBounds/BV.hs --- a/src/What4/Utils/ResolveBounds/BV.hs +++ b/src/What4/Utils/ResolveBounds/BV.hs @@ -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. diff --git a/test/AdapterTest.hs b/test/AdapterTest.hs --- a/test/AdapterTest.hs +++ b/test/AdapterTest.hs @@ -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 diff --git a/test/BVDomTests.hs b/test/BVDomTests.hs deleted file mode 100644 --- a/test/BVDomTests.hs +++ /dev/null @@ -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 - ] diff --git a/test/ExprBuilderSMTLib2.hs b/test/ExprBuilderSMTLib2.hs --- a/test/ExprBuilderSMTLib2.hs +++ b/test/ExprBuilderSMTLib2.hs @@ -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 diff --git a/test/ExprsTest.hs b/test/ExprsTest.hs --- a/test/ExprsTest.hs +++ b/test/ExprsTest.hs @@ -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 ] diff --git a/test/HH/VerifyBindings.hs b/test/HH/VerifyBindings.hs deleted file mode 100644 --- a/test/HH/VerifyBindings.hs +++ /dev/null @@ -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)) diff --git a/test/OnlineSolverTest.hs b/test/OnlineSolverTest.hs --- a/test/OnlineSolverTest.hs +++ b/test/OnlineSolverTest.hs @@ -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 ] diff --git a/test/QC/VerifyBindings.hs b/test/QC/VerifyBindings.hs deleted file mode 100644 --- a/test/QC/VerifyBindings.hs +++ /dev/null @@ -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)) diff --git a/test/WeightedSum.hs b/test/WeightedSum.hs new file mode 100644 --- /dev/null +++ b/test/WeightedSum.hs @@ -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 + ] + ] diff --git a/what4.cabal b/what4.cabal --- a/what4.cabal +++ b/what4.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.4 Name: what4 -Version: 1.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