Copyright	(c) Galois Inc 2019-2020
License	BSD3
Maintainer	[email protected]
Safe Haskell	None
Language	Haskell2010

What4.Utils.BVDomain.XOR

Contents

XOR Domains
- Operations
Correctness properties

Description

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

Synopsis

data Domain (w :: Nat) = BVDXor !Integer !Integer !Integer
proper :: forall (w :: Nat). NatRepr w -> Domain w -> Bool
bvdMask :: forall (w :: Nat). Domain w -> Integer
member :: forall (w :: Nat). Domain w -> Integer -> Bool
pmember :: forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
interval :: forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
bitbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
asSingleton :: forall (w :: Nat). Domain w -> Maybe Integer
singleton :: forall (w :: Nat). NatRepr w -> Integer -> Domain w
xor :: forall (w :: Nat). Domain w -> Domain w -> Domain w
and :: forall (w :: Nat). Domain w -> Domain w -> Domain w
and_scalar :: forall (w :: Nat). Integer -> Domain w -> Domain w
genDomain :: forall (w :: Nat). NatRepr w -> Gen (Domain w)
genElement :: forall (w :: Nat). Domain w -> Gen Integer
genPair :: forall (w :: Nat). NatRepr w -> Gen (Domain w, Integer)
correct_singleton :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Integer -> Property
correct_xor :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_and :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_and_scalar :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> (Domain n, Integer) -> Property
correct_bitbounds :: forall (n :: Nat). Domain n -> Integer -> Property

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

Instances details

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

Test if the domain satisfies its invariants

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

Return the bitvector mask value from this domain

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

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

pmember :: forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool Source #

Check that a domain is proper, and that the given value is a member

range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w Source #

Construct a domain from bitwise lower and upper bounds

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

Unsafe constructor for internal use.

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

Bitwise lower and upper bounds

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

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

Operations

singleton :: forall (w :: Nat). NatRepr w -> Integer -> Domain w Source #

Return a domain containing just the given value

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

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

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

Correctness properties

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

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

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

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

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

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

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

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

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

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