Copyright	(c) Galois Inc 2019-2020
License	BSD3
Maintainer	huffman@galois.com
Safe Haskell	None
Language	Haskell2010

What4.Utils.BVDomain.Arith

Contents

Projection functions
Operations
Correctness properties

Description

Provides an interval-based implementation of bitvector abstract domains.

Synopsis

data Domain (w :: Nat)
- = BVDAny !Integer
- | BVDInterval !Integer !Integer !Integer
proper :: NatRepr w -> Domain w -> Bool
bvdMask :: Domain w -> Integer
member :: Domain w -> Integer -> Bool
pmember :: NatRepr n -> Domain n -> Integer -> Bool
interval :: Integer -> Integer -> Integer -> Domain w
size :: Domain w -> Integer
asSingleton :: Domain w -> Maybe Integer
ubounds :: Domain w -> (Integer, Integer)
sbounds :: 1 <= w => NatRepr w -> Domain w -> (Integer, Integer)
eq :: Domain w -> Domain w -> Maybe Bool
slt :: 1 <= w => NatRepr w -> Domain w -> Domain w -> Maybe Bool
ult :: 1 <= w => Domain w -> Domain w -> Maybe Bool
domainsOverlap :: Domain w -> Domain w -> Bool
arithDomainData :: Domain w -> Maybe (Integer, Integer)
bitbounds :: Domain w -> (Integer, Integer)
unknowns :: Domain w -> Integer
fillright :: Integer -> Integer
any :: 1 <= w => NatRepr w -> Domain w
singleton :: (HasCallStack, 1 <= w) => NatRepr w -> Integer -> Domain w
range :: NatRepr w -> Integer -> Integer -> Domain w
fromAscEltList :: 1 <= w => NatRepr w -> [Integer] -> Domain w
union :: 1 <= w => Domain w -> Domain w -> Domain w
concat :: NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
select :: (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> Domain w -> Domain n
zext :: (1 <= w, (w + 1) <= u) => Domain w -> NatRepr u -> Domain u
sext :: forall w u. (1 <= w, (w + 1) <= u) => NatRepr w -> Domain w -> NatRepr u -> Domain u
shl :: 1 <= w => NatRepr w -> Domain w -> Domain w -> Domain w
lshr :: 1 <= w => NatRepr w -> Domain w -> Domain w -> Domain w
ashr :: 1 <= w => NatRepr w -> Domain w -> Domain w -> Domain w
add :: 1 <= w => Domain w -> Domain w -> Domain w
negate :: 1 <= w => Domain w -> Domain w
scale :: 1 <= w => Integer -> Domain w -> Domain w
mul :: 1 <= w => Domain w -> Domain w -> Domain w
udiv :: 1 <= w => Domain w -> Domain w -> Domain w
urem :: 1 <= w => Domain w -> Domain w -> Domain w
sdiv :: 1 <= w => NatRepr w -> Domain w -> Domain w -> Domain w
srem :: 1 <= w => NatRepr w -> Domain w -> Domain w -> Domain w
not :: Domain w -> Domain w
genDomain :: NatRepr w -> Gen (Domain w)
genElement :: Domain w -> Gen Integer
genPair :: NatRepr w -> Gen (Domain w, Integer)
correct_any :: 1 <= n => NatRepr n -> Integer -> Property
correct_ubounds :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Property
correct_sbounds :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Property
correct_singleton :: 1 <= n => NatRepr n -> Integer -> Integer -> Property
correct_overlap :: Domain n -> Domain n -> Integer -> Property
correct_union :: 1 <= n => NatRepr n -> Domain n -> Domain n -> Integer -> Property
correct_zero_ext :: (1 <= w, (w + 1) <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
correct_sign_ext :: (1 <= w, (w + 1) <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
correct_concat :: NatRepr m -> (Domain m, Integer) -> NatRepr n -> (Domain n, Integer) -> Property
correct_shrink :: NatRepr i -> NatRepr n -> (Domain (i + n), Integer) -> Property
correct_trunc :: n <= w => NatRepr n -> (Domain w, Integer) -> Property
correct_select :: (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> (Domain w, Integer) -> Property
correct_add :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_neg :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Property
correct_mul :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_scale :: 1 <= n => NatRepr n -> Integer -> (Domain n, Integer) -> Property
correct_scale_eq :: 1 <= n => NatRepr n -> Integer -> Domain n -> Property
correct_udiv :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_urem :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_sdivRange :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer -> Property
correct_sdiv :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_srem :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_not :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Property
correct_shl :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_lshr :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_ashr :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_eq :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_ult :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_slt :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_unknowns :: 1 <= n => Domain n -> Integer -> Integer -> Property
correct_bitbounds :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Property

Documentation

data Domain (w :: Nat) Source #

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.

Constructors

BVDAny !Integer	The set of all bitvectors of width `w`. Argument caches `2^w-1`.
BVDInterval !Integer !Integer !Integer	Intervals are represented by a starting value and a size. `BVDInterval mask l d` represents the set of values of the form `x mod 2^w` for `x` such that `l <= x <= l + d`. It should satisfy the invariants `0 <= l < 2^w` and `0 <= d < 2^w`. The first argument caches the value `2^w-1`.

Instances

Show (Domain w) Source #
Instance details Defined in What4.Utils.BVDomain.Arith Methods showsPrec :: Int -> Domain w -> ShowS # show :: Domain w -> String # showList :: [Domain w] -> ShowS #

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

Check if the domain satisfies its invariants

bvdMask :: Domain w -> Integer Source #

Return the bitvector mask value from this domain

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

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

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

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

interval :: Integer -> Integer -> Integer -> Domain w Source #

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

size :: Domain w -> Integer Source #

Compute how many concrete elements are in the abstract domain

Projection functions

asSingleton :: Domain w -> Maybe Integer Source #

Return value if this is a singleton.

ubounds :: Domain w -> (Integer, Integer) Source #

Return unsigned bounds for domain.

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

Return signed bounds for domain.

eq :: Domain w -> Domain w -> Maybe Bool Source #

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

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

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

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

domainsOverlap :: Domain w -> Domain w -> Bool Source #

Return true if domains contain a common element.

arithDomainData :: Domain w -> Maybe (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 #

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

unknowns :: Domain w -> Integer Source #

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

fillright :: Integer -> Integer Source #

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

Operations

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

Represents all values

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

Create a bitvector domain representing the integer.

range :: NatRepr w -> Integer -> Integer -> Domain 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] -> Domain w Source #

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

union :: 1 <= w => Domain w -> Domain w -> Domain w Source #

Return union of two domains.

concat :: NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (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 -> Domain w -> Domain n Source #

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

zext :: (1 <= w, (w + 1) <= u) => Domain w -> NatRepr u -> Domain u Source #

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