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

What4.Utils.BVDomain

Contents

Bitvector abstract domains
- Domain transfer functions
- Projection functions
Operations
Useful bitvector computations
Correctness properties

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

data BVDomain (w :: Nat)
- = BVDArith !(Domain w)
- | BVDBitwise !(Domain w)
proper :: NatRepr w -> BVDomain w -> Bool
member :: BVDomain w -> Integer -> Bool
size :: BVDomain w -> Integer
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
asSingleton :: BVDomain w -> Maybe Integer
eq :: BVDomain w -> BVDomain w -> Maybe Bool
slt :: 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
ult :: 1 <= w => BVDomain w -> BVDomain w -> Maybe Bool
testBit :: NatRepr w -> BVDomain w -> Natural -> Maybe Bool
domainsOverlap :: BVDomain w -> BVDomain w -> Bool
ubounds :: BVDomain w -> (Integer, Integer)
sbounds :: 1 <= w => NatRepr w -> BVDomain w -> (Integer, Integer)
arithDomainData :: Domain w -> Maybe (Integer, Integer)
bitbounds :: Domain w -> (Integer, Integer)
any :: 1 <= w => NatRepr w -> BVDomain w
singleton :: (HasCallStack, 1 <= w) => NatRepr w -> Integer -> BVDomain w
range :: NatRepr w -> Integer -> Integer -> BVDomain w
fromAscEltList :: 1 <= w => NatRepr w -> [Integer] -> BVDomain w
union :: 1 <= w => BVDomain w -> BVDomain w -> BVDomain w
concat :: NatRepr u -> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
select :: (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n
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
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
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
not :: BVDomain w -> BVDomain w
and :: BVDomain w -> BVDomain w -> BVDomain w
or :: BVDomain w -> BVDomain w -> BVDomain w
xor :: BVDomain w -> BVDomain w -> BVDomain w
popcnt :: NatRepr w -> BVDomain w -> BVDomain w
clz :: NatRepr w -> BVDomain w -> BVDomain w
ctz :: NatRepr w -> BVDomain w -> BVDomain w
bitwiseRoundAbove :: Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween :: Integer -> Integer -> Integer -> Integer -> Integer
genDomain :: NatRepr w -> Gen (BVDomain w)
genElement :: BVDomain w -> Gen Integer
genPair :: NatRepr w -> Gen (BVDomain w, Integer)
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

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 details 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 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

size :: BVDomain w -> Integer Source #

Compute how many concrete elements are in the abstract domain

Domain transfer functions

asArithDomain :: BVDomain w -> Domain w Source #

asBitwiseDomain :: BVDomain w -> Domain w Source #

asXorDomain :: BVDomain w -> Domain w Source #

fromXorDomain :: Domain w -> BVDomain w Source #

arithToXorDomain :: Domain w -> Domain w Source #

bitwiseToXorDomain :: Domain w -> Domain w Source #

xorToBitwiseDomain :: Domain w -> Domain w Source #

Projection functions

asSingleton :: BVDomain w -> Maybe Integer Source #

Return value if this is a singleton.

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

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.

testBit Source #

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

Return true if domains contain a common element.

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

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

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 #

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.

and :: BVDomain w -> BVDomain w -> BVDomain w Source #

or :: BVDomain w -> BVDomain w -> BVDomain w Source #

xor :: BVDomain w -> BVDomain w -> BVDomain w Source #

Misc

popcnt :: NatRepr w -> BVDomain w -> BVDomain w Source #

clz :: NatRepr w -> BVDomain w -> BVDomain w Source #

ctz :: NatRepr w -> BVDomain w -> BVDomain w Source #

Useful bitvector computations

bitwiseRoundAbove Source #

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

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.