what4-domains-0.1: Abstract domains for What4 term simplification
Copyright(c) Galois Inc 2019-2020
LicenseBSD3
Maintainerhuffman@galois.com
Safe HaskellNone
LanguageHaskell2010

What4.Domains.BV

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.Domains.BV

Methods

showsPrec :: Int -> BVDomain w -> ShowS #

show :: BVDomain w -> String #

showList :: [BVDomain w] -> ShowS #

Eq (BVDomain w) Source # 
Instance details

Defined in What4.Domains.BV

Methods

(==) :: BVDomain w -> BVDomain w -> Bool #

(/=) :: BVDomain w -> BVDomain w -> Bool #

Ord (BVDomain w) Source # 
Instance details

Defined in What4.Domains.BV

Methods

compare :: BVDomain w -> BVDomain w -> Ordering #

(<) :: BVDomain w -> BVDomain w -> Bool #

(<=) :: BVDomain w -> BVDomain w -> Bool #

(>) :: BVDomain w -> BVDomain w -> Bool #

(>=) :: BVDomain w -> BVDomain w -> Bool #

max :: BVDomain w -> BVDomain w -> BVDomain w #

min :: BVDomain w -> BVDomain w -> BVDomain w #

proper :: forall (w :: Nat). NatRepr w -> BVDomain w -> Bool Source #

Test if the domain satisfies its invariants

member :: forall (w :: Nat). BVDomain w -> Integer -> Bool Source #

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

size :: forall (w :: Nat). BVDomain w -> Integer Source #

Compute how many concrete elements are in the abstract domain

Domain transfer functions

asArithDomain :: forall (w :: Nat). BVDomain w -> Domain w Source #

asBitwiseDomain :: forall (w :: Nat). BVDomain w -> Domain w Source #

asXorDomain :: forall (w :: Nat). BVDomain w -> Domain w Source #

fromXorDomain :: forall (w :: Nat). Domain w -> BVDomain w Source #

arithToXorDomain :: forall (w :: Nat). Domain w -> Domain w Source #

bitwiseToXorDomain :: forall (w :: Nat). Domain w -> Domain w Source #

xorToBitwiseDomain :: forall (w :: Nat). Domain w -> Domain w Source #

Projection functions

asSingleton :: forall (w :: Nat). BVDomain w -> Maybe Integer Source #

Return value if this is a singleton.

eq :: forall (w :: Nat). BVDomain w -> BVDomain w -> Maybe Bool Source #

slt :: forall (w :: Natural). 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 :: forall (w :: Natural). 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

:: forall (w :: Nat). 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 :: forall (w :: Nat). BVDomain w -> BVDomain w -> Bool Source #

Return true if domains contain a common element.

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

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

isUltSumCommonEquiv :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w -> Bool Source #

Check if (bvult (bvadd a c) (bvadd b c)) is equivalent to (bvult a b)

arithDomainData :: forall (w :: Nat). 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 :: forall (w :: Nat). Domain w -> (Integer, Integer) Source #

O(1). Bitwise lower and upper bounds.

Lattice operations

top :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w Source #

Top element of the lattice: represents all bitvectors of width w.

any :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w Source #

Deprecated: Use top instead

Represents all values.

bottom :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w Source #

Bottom element of the lattice: represents the empty set of bitvectors. This is an improper domain whose membership predicate is unsatisfiable.

isBottom :: forall (w :: Nat). BVDomain w -> Bool Source #

join :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

Lattice join (least upper bound) of two domains.

union :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

Deprecated: Use join instead

Return union of two domains.

meet :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

Lattice meet: an over-approximation of the intersection of two domains. For any concrete value x, if x is a member of both a and b, then x is a member of meet a b.

For mixed-representation arguments (one BVDArith, one BVDBitwise), the left argument's representation is preserved and the right argument is converted to match. The result is always precisely a subset of the left argument (no precision loss on the left); the right argument is approximated by the conversion, so the result may contain values that were not members of the original right argument. The single-representation cases (meet, meet) preserve precision exactly on both arguments.

leq :: forall (w :: Nat). BVDomain w -> BVDomain w -> Bool Source #

Lattice ordering: leq a b returns True if every concrete value represented by a is also represented by b.

Operations

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

Create a bitvector domain representing the integer.

range :: forall (w :: Nat). 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 :: forall (w :: Natural). 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.

concat :: forall (u :: Nat) (v :: Nat). 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 :: forall (n :: Natural) (i :: Natural) (w :: Natural). (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 :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => BVDomain w -> NatRepr u -> BVDomain u Source #

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

Shifts and rotates

shl :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

lshr :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

ashr :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

rol :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

ror :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

Arithmetic

add :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

negate :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w Source #

scale :: forall (w :: Natural). 1 <= w => Integer -> BVDomain w -> BVDomain w Source #

mul :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

udiv :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

urem :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

sdiv :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

srem :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

Arithmetic (SMT-LIB div-by-zero semantics)

udivSmtlib :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

Like udiv, but using the SMT-LIB FixedSizeBitVectors theory's div-by-zero semantics. See udivSmtlib.

uremSmtlib :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

Like urem, but using the SMT-LIB FixedSizeBitVectors theory's div-by-zero semantics. See uremSmtlib.

sdivSmtlib :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

Like sdiv, but using the SMT-LIB QF_BV logic's div-by-zero semantics. See sdivSmtlib.

sremSmtlib :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

Like srem, but using the SMT-LIB QF_BV logic's div-by-zero semantics. See sremSmtlib.

Bitwise

not :: forall (w :: Nat). BVDomain w -> BVDomain w Source #

Complement bits in range.

and :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w Source #

or :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w Source #

xor :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w Source #

Misc

popcnt :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w Source #

clz :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w Source #

ctz :: forall (w :: Nat). 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.

Correctness properties

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

Generate a random nonempty domain

genElement :: forall (w :: Nat). BVDomain w -> Gen Integer Source #

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

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

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

correct_arithToBitwise :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_bitwiseToArith :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_bitwiseToXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_arithToXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_xorToBitwiseDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_asXorDomain :: forall (n :: Nat). NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_fromXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_bra1 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Property Source #

correct_bra2 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Integer -> Property Source #

correct_brb1 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Integer -> Property Source #

correct_brb2 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property Source #

correct_any :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Property Source #

correct_ubounds :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_sbounds :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_singleton :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Integer -> Property Source #

correct_overlap :: forall (n :: Nat). BVDomain n -> BVDomain n -> Integer -> Property Source #

precise_overlap :: forall (n :: Nat). BVDomain n -> BVDomain n -> Property Source #

correct_asSingleton :: forall (n :: Natural). 1 <= n => NatRepr n -> BVDomain n -> Property Source #

correct_mixed_domain_overlap :: forall (n :: Nat). Domain n -> Domain n -> Integer -> Property Source #

If an arithmetic and a bitwise domain share a common element, then mixedDomainsOverlap returns True.

correct_mixed_domain_overlap_inv :: forall (n :: Nat). Domain n -> Domain n -> Property Source #

If mixedDomainsOverlap returns True (and the bitwise domain is non-empty), then a shared witness exists among mixedCandidates.

correct_union :: forall (n :: Natural). 1 <= n => NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property Source #

correct_join :: forall (n :: Natural). 1 <= n => NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property Source #

correct_meet :: forall (n :: Natural). 1 <= n => BVDomain n -> BVDomain n -> Integer -> Property Source #

correct_leq :: forall (n :: Nat). BVDomain n -> BVDomain n -> Integer -> Property Source #

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

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

correct_concat :: forall (m :: Nat) (n :: Nat). NatRepr m -> (BVDomain m, Integer) -> NatRepr n -> (BVDomain n, Integer) -> Property Source #

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

correct_add :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_neg :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_mul :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_scale :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> (BVDomain n, Integer) -> Property Source #

correct_udiv :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_urem :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_sdiv :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_srem :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_shl :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_lshr :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_ashr :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_rol :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_ror :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_eq :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_ult :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_slt :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_and :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_or :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_not :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_xor :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_testBit :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Natural -> Property Source #

correct_popcnt :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_clz :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_ctz :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #