what4-1.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2019-2020
LicenseBSD3
Maintainerhuffman@galois.com
Safe HaskellNone
LanguageHaskell2010

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

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

Projection functions

asSingleton :: BVDomain w -> Maybe Integer Source #

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.

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.

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.

Misc

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.

Correctness properties

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

Generate a random nonempty domain

genElement :: BVDomain w -> Gen Integer Source #

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 #