What4.Utils.BVDomain.XOR

Provides an implementation of bitvector abstract domains optimized for performing XOR operations.

XOR Domains

data Domain (w :: Nat)

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.

Constructors

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.

Instances

Show (Domain w)

Defined in What4.Utils.BVDomain.XOR

Methods

showsPrec :: Int -> Domain w -> ShowS

show :: Domain w -> String

showList :: [Domain w] -> ShowS

proper :: NatRepr w -> Domain w -> Bool

Test if the domain satisfies its invariants

bvdMask :: Domain w -> Integer

Return the bitvector mask value from this domain

member :: Domain w -> Integer -> Bool

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

pmember :: NatRepr n -> Domain n -> Integer -> Bool

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

range :: NatRepr w -> Integer -> Integer -> Domain w

Construct a domain from bitwise lower and upper bounds

interval :: Integer -> Integer -> Integer -> Domain w

Unsafe constructor for internal use.

bitbounds :: Domain w -> (Integer, Integer)

Bitwise lower and upper bounds

asSingleton :: Domain w -> Maybe Integer

Test if this domain contains a single value, and return it if so

Operations

singleton :: NatRepr w -> Integer -> Domain w

Return a domain containing just the given value

xor :: Domain w -> Domain w -> Domain w

and :: Domain w -> Domain w -> Domain w

and_scalar :: Integer -> Domain w -> Domain w

Correctness properties

genDomain :: NatRepr w -> Gen (Domain w)

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

genElement :: Domain w -> Gen Integer

genPair :: NatRepr w -> Gen (Domain w, Integer)

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

correct_singleton :: 1 <= n => NatRepr n -> Integer -> Integer -> Property

correct_xor :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property

correct_and :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property

correct_and_scalar :: 1 <= n => NatRepr n -> Integer -> (Domain n, Integer) -> Property

correct_bitbounds :: Domain n -> Integer -> Property