what4-1.0: Solver-agnostic symbolic values support for issuing queries

What4.Utils.BVDomain

Description

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.

Synopsis

# Bitvector abstract domains

data BVDomain (w :: Nat) Source #

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) Source # Instance detailsDefined in What4.Utils.BVDomain MethodsshowsPrec :: Int -> BVDomain w -> ShowS #show :: BVDomain w -> String #showList :: [BVDomain w] -> ShowS #

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

Test if the domain satisfies its invariants

member :: BVDomain w -> Integer -> Bool Source #

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

Compute how many concrete elements are in the abstract domain

## Projection functions

Return value if this is a singleton.

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

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

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

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

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.

Return true if domains contain a common element.

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

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) Source #

Bitwise lower and upper bounds

# Operations

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

Represents all values

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

Create a bitvector domain representing the integer.

range :: NatRepr w -> Integer -> Integer -> BVDomain w Source #

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 Source #

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 Source #

Return union of two domains.

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

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 Source #

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 Source #

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

## Shifts and rotates

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

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

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

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

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

## Arithmetic

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

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

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

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

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

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

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

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

## Bitwise

not :: BVDomain w -> BVDomain w Source #

Complement bits in range.

# Useful bitvector computations

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.

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) Source #

Generate a random nonempty domain

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

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

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

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

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

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