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

What4.Utils.BVDomain.Bitwise

Contents

Operations
- shifts and rotates
- bitwise logical
Correctness properties

Description

Provides a bitwise implementation of bitvector abstract domains.

Synopsis

data Domain (w :: Nat) = BVBitInterval !Integer !Integer !Integer
bitle :: Integer -> Integer -> Bool
proper :: NatRepr w -> Domain w -> Bool
bvdMask :: Domain w -> Integer
member :: Domain w -> Integer -> Bool
pmember :: NatRepr n -> Domain n -> Integer -> Bool
size :: Domain w -> Integer
asSingleton :: Domain w -> Maybe Integer
nonempty :: Domain w -> Bool
eq :: Domain w -> Domain w -> Maybe Bool
domainsOverlap :: Domain w -> Domain w -> Bool
bitbounds :: Domain w -> (Integer, Integer)
any :: NatRepr w -> Domain w
singleton :: NatRepr w -> Integer -> Domain w
range :: NatRepr w -> Integer -> Integer -> Domain w
interval :: Integer -> Integer -> Integer -> Domain w
union :: Domain w -> Domain w -> Domain w
intersection :: 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 :: (1 <= w, (w + 1) <= u) => NatRepr w -> Domain w -> NatRepr u -> Domain u
testBit :: Domain w -> Natural -> Maybe Bool
shl :: NatRepr w -> Domain w -> Integer -> Domain w
lshr :: NatRepr w -> Domain w -> Integer -> Domain w
ashr :: 1 <= w => NatRepr w -> Domain w -> Integer -> Domain w
rol :: NatRepr w -> Domain w -> Integer -> Domain w
ror :: NatRepr w -> Domain w -> Integer -> Domain w
and :: Domain w -> Domain w -> Domain w
or :: Domain w -> Domain w -> Domain w
xor :: 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_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_intersection :: 1 <= 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_shl :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_lshr :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_ashr :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_rol :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_ror :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Integer -> Property
correct_eq :: 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_or :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_not :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Property
correct_xor :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_testBit :: 1 <= n => NatRepr n -> (Domain n, Integer) -> Natural -> Property

Documentation

data Domain (w :: Nat) Source #

A bitwise interval domain, defined via a bitwise upper and lower bound. The ordering used here to construct the interval is the pointwise ordering on bits. In particular x [= y iff x .|. y == y, and a value x is in the set defined by the pair (lo,hi) just when lo [= x && x [= hi.

Constructors

BVBitInterval !Integer !Integer !Integer

BVDBitInterval mask lo hi. mask caches the value of 2^w - 1

Instances

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

bitle :: Integer -> Integer -> Bool Source #

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

Test 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

size :: Domain w -> Integer Source #

Compute how many concrete elements are in the abstract domain

asSingleton :: Domain w -> Maybe Integer Source #

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

nonempty :: Domain w -> Bool Source #

Returns true iff there is at least on element in this bitwise domain.

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

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

Returns true iff the domains have some value in common

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

Bitwise lower and upper bounds

Operations

any :: NatRepr w -> Domain w Source #

Bitwise domain containing every bitvector value

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

Return a domain containing just the given value

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

Construct a domain from bitwise lower and upper bounds

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

Unsafe constructor for internal use.

union :: Domain w -> Domain w -> Domain w Source #

intersection :: Domain w -> Domain w -> Domain w Source #

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 :: (1 <= w, (w + 1) <= u) => NatRepr w -> Domain w -> NatRepr u -> Domain u Source #

testBit :: Domain w -> Natural -> Maybe Bool Source #