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

Copyright | (c) Galois Inc 2019-2020
License | BSD3
Maintainer | huffman@galois.com
Safe Haskell | Safe-Inferred
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 :: NatRepr w -> Domain w -> Bool
- bvdMask :: Domain w -> Integer
- member :: Domain w -> Integer -> Bool
- pmember :: NatRepr n -> Domain n -> Integer -> Bool
- range :: NatRepr w -> Integer -> Integer -> Domain w
- interval :: Integer -> Integer -> Integer -> Domain w
- bitbounds :: Domain w -> (Integer, Integer)
- asSingleton :: Domain w -> Maybe Integer
- singleton :: NatRepr w -> Integer -> Domain w
- xor :: Domain w -> Domain w -> Domain w
- and :: Domain w -> Domain w -> Domain w
- and_scalar :: Integer -> Domain w -> Domain w
- genDomain :: NatRepr w -> Gen (Domain w)
- genElement :: Domain w -> Gen Integer
- genPair :: NatRepr w -> Gen (Domain w, Integer)
- correct_singleton :: 1 <= n => NatRepr n -> Integer -> Integer -> Property
- correct_xor :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_and :: 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_and_scalar :: 1 <= n => NatRepr n -> Integer -> (Domain n, Integer) -> Property
- correct_bitbounds :: 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 Source # show :: Domain w -> String Source # showList :: [Domain w] -> ShowS Source #

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 #

and_scalar :: Integer -> 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.

genElement :: Domain w -> Gen Integer Source #

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

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

correct_singleton :: 1 <= n => NatRepr n -> Integer -> Integer -> Property Source #

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

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

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

correct_bitbounds :: Domain n -> Integer -> Property Source #