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

Copyright(c) Galois Inc 2019-2020
LicenseBSD3
Maintainerhuffman@galois.com
Safe HaskellNone
LanguageHaskell2010

What4.Utils.BVDomain.XOR

Contents

Description

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

Synopsis

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.

Constructors

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.

Instances
Show (Domain w) Source # 
Instance details

Defined in What4.Utils.BVDomain.XOR

Methods

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

Operations

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.