What4.Utils.BVDomain

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.

Bitvector abstract domains

data BVDomain (w :: Nat)

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.

Constructors

BVDArith !(Domain w)

BVDBitwise !(Domain w)

Instances

Show (BVDomain w)

Defined in What4.Utils.BVDomain

Methods

showsPrec :: Int -> BVDomain w -> ShowS

show :: BVDomain w -> String

showList :: [BVDomain w] -> ShowS

proper :: NatRepr w -> BVDomain w -> Bool

Test if the domain satisfies its invariants

member :: BVDomain w -> Integer -> Bool

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

size :: BVDomain w -> Integer

Compute how many concrete elements are in the abstract domain

Domain transfer functions

asArithDomain :: BVDomain w -> Domain w

asBitwiseDomain :: BVDomain w -> Domain w

asXorDomain :: BVDomain w -> Domain w

fromXorDomain :: Domain w -> BVDomain w

arithToXorDomain :: Domain w -> Domain w

bitwiseToXorDomain :: Domain w -> Domain w

xorToBitwiseDomain :: Domain w -> Domain w

Projection functions

asSingleton :: BVDomain w -> Maybe Integer

Return value if this is a singleton.

eq :: BVDomain w -> BVDomain w -> Maybe Bool

slt :: 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool

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

ult :: 1 <= w => BVDomain w -> BVDomain w -> Maybe Bool

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

testBit

Arguments

:: NatRepr w

-> BVDomain w

-> Natural

Index of bit (least-significant bit has index 0)

-> Maybe Bool

Return Just if every bitvector in the domain has the same bit at the given index.

domainsOverlap :: BVDomain w -> BVDomain w -> Bool

Return true if domains contain a common element.

ubounds :: BVDomain w -> (Integer, Integer)

sbounds :: 1 <= w => NatRepr w -> BVDomain w -> (Integer, Integer)

arithDomainData :: Domain w -> Maybe (Integer, Integer)

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.

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

Bitwise lower and upper bounds

Operations

any :: 1 <= w => NatRepr w -> BVDomain w

Represents all values

singleton :: (HasCallStack, 1 <= w) => NatRepr w -> Integer -> BVDomain w

Create a bitvector domain representing the integer.

range :: NatRepr w -> Integer -> Integer -> BVDomain 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.

fromAscEltList :: 1 <= w => NatRepr w -> [Integer] -> BVDomain w

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

union :: 1 <= w => BVDomain w -> BVDomain w -> BVDomain w

Return union of two domains.

concat :: NatRepr u -> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)

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 :: (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n

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

zext :: (1 <= w, (w + 1) <= u) => BVDomain w -> NatRepr u -> BVDomain u

sext :: forall w u. (1 <= w, (w + 1) <= u) => NatRepr w -> BVDomain w -> NatRepr u -> BVDomain u

Shifts and rotates

shl :: 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

lshr :: 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

ashr :: 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

rol :: 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

ror :: 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

Arithmetic

add :: 1 <= w => BVDomain w -> BVDomain w -> BVDomain w

negate :: 1 <= w => BVDomain w -> BVDomain w

scale :: 1 <= w => Integer -> BVDomain w -> BVDomain w

mul :: 1 <= w => BVDomain w -> BVDomain w -> BVDomain w

udiv :: 1 <= w => BVDomain w -> BVDomain w -> BVDomain w

urem :: 1 <= w => BVDomain w -> BVDomain w -> BVDomain w

sdiv :: 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

srem :: 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

Bitwise

not :: BVDomain w -> BVDomain w

Complement bits in range.

and :: BVDomain w -> BVDomain w -> BVDomain w

or :: BVDomain w -> BVDomain w -> BVDomain w

xor :: BVDomain w -> BVDomain w -> BVDomain w

Misc

popcnt :: NatRepr w -> BVDomain w -> BVDomain w

clz :: NatRepr w -> BVDomain w -> BVDomain w

ctz :: NatRepr w -> BVDomain w -> BVDomain w

Useful bitvector computations

bitwiseRoundAbove

Arguments

:: Integer

bvmask, based on the width of the bitvectors in question

-> Integer

x

-> Integer

lomask

-> Integer

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.

bitwiseRoundBetween

Arguments

:: Integer

bvmask, based on the width of the bitvectors in question

-> Integer

x

-> Integer

lomask

-> Integer

himask

-> Integer

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.

Correctness properties

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

Generate a random nonempty domain

genElement :: BVDomain w -> Gen Integer

Generate a random element from a domain, which is assumed to be nonempty

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

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

correct_arithToBitwise :: NatRepr n -> (Domain n, Integer) -> Property

correct_bitwiseToArith :: NatRepr n -> (Domain n, Integer) -> Property

correct_bitwiseToXorDomain :: NatRepr n -> (Domain n, Integer) -> Property

correct_arithToXorDomain :: NatRepr n -> (Domain n, Integer) -> Property

correct_xorToBitwiseDomain :: NatRepr n -> (Domain n, Integer) -> Property

correct_asXorDomain :: NatRepr n -> (BVDomain n, Integer) -> Property

correct_fromXorDomain :: NatRepr n -> (Domain n, Integer) -> Property

correct_bra1 :: NatRepr n -> Integer -> Integer -> Property

correct_bra2 :: NatRepr n -> Integer -> Integer -> Integer -> Property

correct_brb1 :: NatRepr n -> Integer -> Integer -> Integer -> Property

correct_brb2 :: NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property

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

correct_ubounds :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property

correct_sbounds :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property

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

correct_overlap :: BVDomain n -> BVDomain n -> Integer -> Property

precise_overlap :: BVDomain n -> BVDomain n -> Property

correct_union :: 1 <= n => NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property

correct_zero_ext :: (1 <= w, (w + 1) <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property

correct_sign_ext :: (1 <= w, (w + 1) <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property

correct_concat :: NatRepr m -> (BVDomain m, Integer) -> NatRepr n -> (BVDomain n, Integer) -> Property

correct_select :: (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> (BVDomain w, Integer) -> Property

correct_add :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_neg :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property

correct_mul :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_scale :: 1 <= n => NatRepr n -> Integer -> (BVDomain n, Integer) -> Property

correct_udiv :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_urem :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_sdiv :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_srem :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_shl :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_lshr :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_ashr :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_rol :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_ror :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_eq :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_ult :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_slt :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

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

correct_or :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property

correct_not :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property

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

correct_testBit :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Natural -> Property

correct_popcnt :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property

correct_clz :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property

correct_ctz :: 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property