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

Copyright | (c) Galois Inc 2020
License | BSD3
Maintainer | huffman@galois.com
Safe Haskell | None
Language | Haskell2010

What4.Utils.BVDomain.Bitwise

Contents

- Operations
  - shifts and rotates
  - bitwise logical
- Correctness properties

Description

Provides a bitwise implementation of bitvector abstract domains.

Synopsis

- data Domain (w :: Nat) = BVBitInterval !Integer !Integer !Integer
- bitle :: Integer -> Integer -> Bool
- 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
- size :: forall (w :: Nat). Domain w -> Integer
- asSingleton :: forall (w :: Nat). Domain w -> Maybe Integer
- nonempty :: forall (w :: Nat). Domain w -> Bool
- eq :: forall (w :: Nat). Domain w -> Domain w -> Maybe Bool
- domainsOverlap :: forall (w :: Nat). Domain w -> Domain w -> Bool
- bitbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
- any :: forall (w :: Nat). NatRepr w -> Domain w
- singleton :: forall (w :: Nat). NatRepr w -> Integer -> Domain w
- range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
- interval :: forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
- union :: forall (w :: Nat). Domain w -> Domain w -> Domain w
- intersection :: forall (w :: Nat). Domain w -> Domain w -> Domain w
- concat :: forall (u :: Nat) (v :: Nat). NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
- select :: forall (n :: Natural) (i :: Natural) (w :: Natural). (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> Domain w -> Domain n
- zext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => Domain w -> NatRepr u -> Domain u
- sext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => NatRepr w -> Domain w -> NatRepr u -> Domain u
- testBit :: forall (w :: Nat). Domain w -> Natural -> Maybe Bool
- shl :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
- lshr :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
- ashr :: forall (w :: Natural). 1 <= w => NatRepr w -> Domain w -> Integer -> Domain w
- rol :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
- ror :: forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
- and :: forall (w :: Nat). Domain w -> Domain w -> Domain w
- or :: forall (w :: Nat). Domain w -> Domain w -> Domain w
- xor :: forall (w :: Nat). Domain w -> Domain w -> Domain w
- not :: forall (w :: Nat). 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_any :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Property
- correct_singleton :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Integer -> Property
- correct_overlap :: forall (n :: Nat). Domain n -> Domain n -> Integer -> Property
- correct_union :: forall (n :: Natural). 1 <= n => NatRepr n -> Domain n -> Domain n -> Integer -> Property
- correct_intersection :: forall (n :: Natural). 1 <= n => Domain n -> Domain n -> Integer -> Property
- correct_zero_ext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
- correct_sign_ext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => NatRepr w -> Domain w -> NatRepr u -> Integer -> Property
- correct_concat :: forall (m :: Nat) (n :: Nat). NatRepr m -> (Domain m, Integer) -> NatRepr n -> (Domain n, Integer) -> Property
- correct_shrink :: forall (i :: Nat) (n :: Nat). NatRepr i -> NatRepr n -> (Domain (i + n), Integer) -> Property
- correct_trunc :: forall (n :: Nat) (w :: Nat). n <= w => NatRepr n -> (Domain w, Integer) -> Property
- correct_select :: forall (n :: Natural) (i :: Natural) (w :: Natural). (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> (Domain w, Integer) -> Property
- correct_shl :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> Integer -> Property
- correct_lshr :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> Integer -> Property
- correct_ashr :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> Integer -> Property
- correct_rol :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> Integer -> Property
- correct_ror :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> Integer -> Property
- correct_eq :: 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_or :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_not :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> Property
- correct_xor :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_testBit :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> Natural -> Property

# Documentation

data Domain (w :: Nat) Source #

A bitwise interval domain, defined via a bitwise upper and lower bound. The ordering used here to construct the interval is the pointwise ordering on bits. In particular `x [= y iff x .|. y == y`, and a value `x` is in the set defined by the pair `(lo,hi)` just when `lo [= x && x [= hi`.

Constructors

BVBitInterval !Integer !Integer !Integer | `BVDBitInterval mask lo hi`. `mask` caches the value of `2^w - 1`

#### Instances

Instances details

Show (Domain w) Source # |
Instance details Defined in What4.Utils.BVDomain.Bitwise Methods showsPrec :: Int -> Domain w -> ShowS Source # show :: Domain w -> String Source # showList :: [Domain w] -> ShowS Source #

bitle :: Integer -> Integer -> Bool Source #

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

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

Compute how many concrete elements are in the abstract domain

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

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

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

Returns true iff there is at least on element in this bitwise domain.

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

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

Returns true iff the domains have some value in common

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

Bitwise lower and upper bounds

# Operations

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

Bitwise domain containing every bitvector value

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

Return a domain containing just the given value

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.

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

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

concat :: forall (u :: Nat) (v :: Nat). NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (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 -> Domain w -> Domain 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) => Domain w -> NatRepr u -> Domain u Source #

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

testBit :: forall (w :: Nat). Domain w -> Natural -> Maybe Bool Source #

## shifts and rotates

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

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

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

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

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

## bitwise logical

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

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

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

not :: forall (w :: Nat). 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_any :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Property Source #

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

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

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

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

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

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

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

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

correct_trunc :: forall (n :: Nat) (w :: Nat). n <= w => NatRepr n -> (Domain w, Integer) -> Property Source #

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

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

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

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

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

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

correct_eq :: 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_or :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property Source #

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

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

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