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.

O(w). Test if the domain satisfies its invariants.

O(1). Return the bitvector mask value from this domain.

O(w). 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

O(w). Compute how many concrete elements are in the abstract domain.

O(w). Test if this domain contains a single value, and return it if so.

O(w). Returns true iff there is at least one element in this bitwise domain.

O(w). Decide equality of two domains: 'Just True' if both are the same singleton, 'Just False' if they're disjoint, Nothing otherwise.

O(w). Check if all elements in one domain are signed-less-than all elements in the other.

O(w). Check if all elements in one domain are unsigned-less-than all elements in the other.

O(w). Returns true iff the domains have some value in common.

O(1). Bitwise lower and upper bounds.

O(1). Unsigned bounds for the domain. The low bit-pattern bound is also the unsigned minimum, and the high bit-pattern bound is also the unsigned maximum: setting unknown bits to 0 minimizes, setting them to 1 maximizes.

O(w). Signed bounds for the domain.

O(1). Top element of the lattice: represents all bitvectors of width w.

O(w). Bitwise domain containing every bitvector value.

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

O(1).

O(w). Lattice join: pointwise least upper bound on the bit-level bitle ordering.

O(w). Lattice meet: pointwise greatest lower bound on the bit-level bitle ordering. If both inputs are proper (or bottom), so is the result.

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

O(w). Return a domain containing just the given value.

O(w). Construct a domain from bitwise lower and upper bounds.

O(1). Unsafe constructor for internal use.

O(u + v). concat a y returns a 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.

O(w). select i n a selects n bits starting from index i from a.

O(w). Zero-extend a domain to a larger width.

O(w). Sign-extend a domain to a larger width.

O(w). Test bit i of every value in the domain: 'Just True' if it is set in every member, 'Just False' if clear in every member, Nothing if it varies.

O(w). Shift left by a known amount.

O(w). Logical (zero-fill) shift right by a known amount.

O(w). Arithmetic (sign-extending) shift right by a known amount.

O(w). Rotate left by a known amount.

O(w). Rotate right by a known amount.

O(w²). Shift left by an amount drawn from the domain b. See foldShifts for the algorithm.

More precisely, O(n · w) where w is the bitvector width and n = min(bh − bl + 1, w + 1) is the number of candidate shift amounts considered, with bl and bh the unsigned bounds of b.

O(w²). Logical (zero-fill) shift right by an amount drawn from the domain b. See foldShifts for the algorithm.

More precisely, O(n · w) where w is the bitvector width and n = min(bh − bl + 1, w + 1) is the number of candidate shift amounts considered, with bl and bh the unsigned bounds of b.

O(w²). Arithmetic (sign-extending) shift right by an amount drawn from the domain b. See foldShifts for the algorithm.

More precisely, O(n · w) where w is the bitvector width and n = min(bh − bl + 1, w + 1) is the number of candidate shift amounts considered, with bl and bh the unsigned bounds of b.

O(w²). Rotate left by an amount drawn from the domain b. See foldRotates for the algorithm.

More precisely, O(r · w) where w is the bitvector width and r is the number of distinct residues mod w that are reachable from b (at most w).

O(w²). Rotate right by an amount drawn from the domain b. Mirrors rolAbstract.

More precisely, O(r · w) where w is the bitvector width and r is the number of distinct residues mod w that are reachable from b (at most w).

Declarative reference variant of shlAbstract: for every member y of the shift-amount domain, compute the per-shift result and union them all. Strictly slower; used to validate shlAbstract.

O(w). Add two bitwise domains.

O(w). Subtract: sub a b = add a (negate b).

O(w). Two's complement negation: negate a = not a + 1.

O(w²). Multiply by a constant. Uses mulPrecise since the shift-and-add algorithm gives bit-level precision when one operand is concrete.

O(w). Multiply two bitwise domains via interval and trailing-zero analysis. Captures known leading bits (both 0s and 1s) derived from [aMin*bMin, aMax*bMax], plus known trailing zeros from the operands.

See mul for the algorithm. mulPrecise is strictly more precise; this is the cheaper alternative when middle-bit precision doesn't matter.

O(w²). Multiply two bitwise domains, combining the shift-and-add tristate-number algorithm (BPF tnum_mul) with the interval and trailing-zero analysis of mul. Strictly at least as precise as mul.

O(w). Unsigned division via interval analysis on the quotient bounds. Assumes the divisor is nonzero.

Captures known leading bits (both 0s and 1s) derived from [aMin `quot` bMax, aMax `quot` bMin]. When the divisor is a known power of two, the result is exact (bit-level structure of the dividend is preserved, e.g. udiv (any w) (singleton w (2^k)) has its top k bits known zero). udivPrecise is strictly more precise; this is the cheaper alternative when middle-bit precision doesn't matter.

O(w). Unsigned remainder via leading-zero analysis. Assumes the divisor is nonzero.

The result is bounded above by min(aMax, bMax - 1); bits above that are known zero. (The remainder's lower bound is trivially 0, so the same interval-agreement analysis used in udiv would not yield additional leading bits here.) When the divisor is a known power of two, urem a (singleton w (2^k)) is exactly the low k bits of a.

O(w). Signed division (rounds toward zero). Assumes the divisor is nonzero.

Implemented by splitting each operand on its sign bit into a non-negative "zero circle" and a negative "one circle", applying udiv to the absolute values, fixing up the sign, and joining the resulting subcases.

O(w). Signed remainder (sign of dividend). Assumes the divisor is nonzero.

Implemented like sdiv, except the result takes the sign of the dividend rather than the XOR of the input signs. Additionally, leading bits of the result are refined using magnitude bounds: if the dividend is non-negative, the result has leading zeros from both the dividend and divisor magnitude; if negative and nonzero, it has leading ones similarly.

O(w²). Unsigned division combining abstract schoolbook long division with the interval analysis of udiv. Assumes the divisor is nonzero. Strictly at least as precise as udiv.

The result is the intersection of udiv (interval analysis on the quotient bounds, plus an exact path for power-of-two divisors) and the schoolbook result (which captures middle-bit structure that interval analysis can't see, but joins through any undetermined comparison and so loses on power-of-two divisors).

O(w²). Unsigned remainder combining schoolbook long division with the leading-zero analysis of urem. Assumes the divisor is nonzero. Strictly at least as precise as urem.

O(w). Like udiv, but using the SMT-LIB FixedSizeBitVectors theory's div-by-zero semantics: bvudiv s 0 is the all-ones bitvector. See Note [SMT-LIB division] in What4.Interface for the design rationale.

O(w). Like urem, but using the SMT-LIB FixedSizeBitVectors theory's div-by-zero semantics: bvurem s 0 is the dividend itself (s). See Note [SMT-LIB division] in What4.Interface for the design rationale.

O(w). Like sdiv, but using the SMT-LIB QF_BV logic's div-by-zero convention: bvsdiv s 0 is all-ones when s is non-negative and 1 when s is negative. See Note [SMT-LIB division] in What4.Interface for the design rationale.

O(w). Like srem, but using the SMT-LIB QF_BV logic's div-by-zero convention: bvsrem s 0 is the dividend itself (s). See Note [SMT-LIB division] in What4.Interface for the design rationale.

O(w). Bitwise AND of two domains.

O(w). Bitwise OR of two domains.

O(w). Bitwise XOR of two domains.

O(w). Bitwise complement.

Random generator for domain values. We always generate nonempty domain values.

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

If domainsOverlap returns True, then a shared witness exists at the bitwise OR of the two low masks.

Precision of meet: if x is a member of meet a b, then x is a member of both a and b.

The optimized shlAbstract produces the same domain as the declarative shlAbstractSpec. Together with correct_shlAbstract, this proves shlAbstract is point-wise optimal at this domain.