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.

Check if the domain satisfies its invariants

Return the bitvector mask value from this domain

Test if the given integer value is a member of the abstract domain

Check that a domain is proper, and that the given value is a member

Unsafe constructor for internal use only. Caller must ensure that mask = maxUnsigned w, and that aw is non-negative.

Compute how many concrete elements are in the abstract domain

Return value if this is a singleton.

Return unsigned bounds for domain.

Return signed bounds for domain.

Check if all elements in one domain are less than all elements in other.

Check if all elements in one domain are less than all elements in other.

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.

Return true if domains contain a common element.

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.

Return bitwise bounds for domain (i.e. logical AND of all possible values, paired with logical OR of all possible values).

unknowns lo hi returns a bitmask representing the set of bit positions whose values are not constant throughout the range lo..hi.

fillright x rounds up x to the nearest 2^n-1.

Top element of the lattice: represents all bitvectors of width w.

Represents all values.

Bottom element of the lattice: represents the empty set of bitvectors. This is an improper domain whose membership predicate is unsatisfiable.

Returns True if this domain has no members (i.e., is bottom), detected as an improper interval with negative size.

Lattice join (least upper bound) of two domains. If both inputs are proper (or bottom), so is the result.

For two non-bottom intervals, the result is the shortest single interval containing both. The trick is to compare each interval's "average value" 2*lo + sz (twice the midpoint, doubled to avoid fractions). If the averages are more than half the modulus apart, the inputs sit on opposite sides of zero, so we lift the smaller- midpoint interval by 2^w before taking the enclosing range. This yields the shorter of the two enclosing arcs — the one that wraps around zero when appropriate — rather than always going clockwise. interval then collapses sizes >= 2^w to BVDAny.

    Visualize the modular number line [0, mask] as a horizontal strip.

    midpoints close — naive convex hull is already optimal:
           0                                     mask
    a:     [-----]
    b:               [-----]
    naive: [---------------]   (= our result)

    midpoints far apart — naive hull is wasteful, wrapping is shorter:
           0                                     mask
    a:     [-----]
    b:                                   [-----]
    naive: [-----------------------------------]   (covers nearly everything)
    ours:  -----]                        [------   (wraps around; tight)

Return union of two domains.

Lattice meet: an over-approximation of the intersection of two domains. For any concrete value x, if x is a member of both a and b, then x is a member of meet a b. If both inputs are proper (or bottom), so is the result.

Lattice ordering: leq a b returns True if every concrete value represented by a is also represented by b.

Create a bitvector domain representing the integer.

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.

Create an abstract domain from an ascending list of elements. The elements are assumed to be distinct.

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.

select i n a selects n bits starting from index i from a.

Like udiv, but using the SMT-LIB FixedSizeBitVectors theory's div-by-zero semantics:

[[(bvudiv s t)]] := if bv2nat([[t]]) = 0
                    then λx:[0, m). 1
                    else nat2bv[m](bv2nat([[s]]) div bv2nat([[t]]))

i.e. the all-ones bitvector when the divisor is zero. See Note [SMT-LIB division] in What4.Interface for the design rationale.

Like urem, but using the SMT-LIB FixedSizeBitVectors theory's div-by-zero semantics:

[[(bvurem s t)]] := if bv2nat([[t]]) = 0
                    then [[s]]
                    else nat2bv[m](bv2nat([[s]]) mod bv2nat([[t]]))

i.e. the dividend itself when the divisor is zero. See Note [SMT-LIB division] in What4.Interface for the design rationale.

Like sdiv, but using the SMT-LIB QF_BV logic's div-by-zero convention: (bvsdiv s 0) is all-ones when the dividend is non-negative, 1 when it is negative. The signed variants are not in the core FixedSizeBitVectors theory; this convention matches Z3, CVC5, Bitwuzla, and Yices. See Note [SMT-LIB division] in What4.Interface for the design rationale.

Like srem, but using the SMT-LIB QF_BV logic's div-by-zero convention: (bvsrem s 0) is the dividend itself. The signed variants are not in the core FixedSizeBitVectors theory; this convention matches Z3, CVC5, Bitwuzla, and Yices. See Note [SMT-LIB division] in What4.Interface for the design rationale.

Complement bits in range.

Random generator for domain values

Generate a random element from a domain

Generate a random domain and an element contained in that domain.

If domainsOverlap returns True, then a shared witness exists among the low-bound candidates of either domain.