what4-1.0: Solver-agnostic symbolic values support for issuing queries

Copyright(c) Galois Inc 2019-2020
Safe HaskellNone




Provides an implementation of bitvector abstract domains optimized for performing XOR operations.


XOR Domains

data Domain (w :: Nat) Source #

A value of type BVDomain w represents a set of bitvectors of width w. This is an alternate representation of the bitwise domain values, optimized to compute XOR operations.


BVDXor !Integer !Integer !Integer

BVDXor mask hi unknown represents a set of values where hi is a bitwise high bound, and unknown represents the bits whose values are not known. The value mask caches the value 2^w-1.

Show (Domain w) Source # 
Instance details

Defined in What4.Utils.BVDomain.XOR


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

show :: Domain w -> String #

showList :: [Domain w] -> ShowS #

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

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.

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

Bitwise lower and upper bounds

asSingleton :: Domain w -> Maybe Integer Source #

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


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

Return a domain containing just the given value

xor :: Domain w -> Domain w -> Domain w Source #

and :: Domain w -> Domain w -> Domain w Source #

Correctness properties

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

Random generator for domain values. We always generate nonempty domain values.

genPair :: NatRepr w -> Gen (Domain w, Integer) Source #

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