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

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

What4.Utils.BVDomain.Arith

Contents

- Projection functions
- Operations
  - Shifts
  - Arithmetic
  - Bitwise
- Correctness properties

Description

Provides an interval-based implementation of bitvector abstract domains.

Synopsis

- data Domain (w :: Nat)
  - = BVDAny !Integer
  - | BVDInterval !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
- interval :: forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
- size :: forall (w :: Nat). Domain w -> Integer
- asSingleton :: forall (w :: Nat). Domain w -> Maybe Integer
- ubounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
- sbounds :: forall (w :: Natural). 1 <= w => NatRepr w -> Domain w -> (Integer, Integer)
- eq :: forall (w :: Nat). Domain w -> Domain w -> Maybe Bool
- slt :: forall (w :: Natural). 1 <= w => NatRepr w -> Domain w -> Domain w -> Maybe Bool
- ult :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Maybe Bool
- isUltSumCommonEquiv :: forall (w :: Nat). Domain w -> Domain w -> Domain w -> Bool
- domainsOverlap :: forall (w :: Nat). Domain w -> Domain w -> Bool
- arithDomainData :: forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
- bitbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
- unknowns :: forall (w :: Nat). Domain w -> Integer
- fillright :: Integer -> Integer
- any :: forall (w :: Natural). 1 <= w => NatRepr w -> Domain w
- singleton :: forall (w :: Natural). (HasCallStack, 1 <= w) => NatRepr w -> Integer -> Domain w
- range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
- fromAscEltList :: forall (w :: Natural). 1 <= w => NatRepr w -> [Integer] -> Domain w
- union :: forall (w :: Natural). 1 <= w => 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
- shl :: forall (w :: Natural). 1 <= w => NatRepr w -> Domain w -> Domain w -> Domain w
- lshr :: forall (w :: Natural). 1 <= w => NatRepr w -> Domain w -> Domain w -> Domain w
- ashr :: forall (w :: Natural). 1 <= w => NatRepr w -> Domain w -> Domain w -> Domain w
- add :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Domain w
- negate :: forall (w :: Natural). 1 <= w => Domain w -> Domain w
- scale :: forall (w :: Natural). 1 <= w => Integer -> Domain w -> Domain w
- mul :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Domain w
- udiv :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Domain w
- urem :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Domain w
- sdiv :: forall (w :: Natural). 1 <= w => NatRepr w -> Domain w -> Domain w -> Domain w
- srem :: forall (w :: Natural). 1 <= w => NatRepr w -> 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_ubounds :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> Property
- correct_sbounds :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain 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_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_add :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_neg :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> Property
- correct_mul :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_scale :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> (Domain n, Integer) -> Property
- correct_scale_eq :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Domain n -> Property
- correct_udiv :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_urem :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_sdivRange :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer -> Property
- correct_sdiv :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_srem :: 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_shl :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_lshr :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_ashr :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_eq :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_ult :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_slt :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_isUltSumCommonEquiv :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> (Domain n, Integer) -> Property
- correct_unknowns :: forall (n :: Natural). 1 <= n => Domain n -> Integer -> Integer -> Property
- correct_bitbounds :: forall (n :: Natural). 1 <= n => NatRepr n -> (Domain n, Integer) -> Property

# Documentation

data Domain (w :: Nat) Source #

A value of type ``BVDomain` w` represents a set of bitvectors of width `w`. Each `BVDomain` can represent a single contiguous interval of bitvectors that may wrap around from -1 to 0.

Constructors

BVDAny !Integer | The set of all bitvectors of width `w`. Argument caches `2^w-1`.
BVDInterval !Integer !Integer !Integer | Intervals are represented by a starting value and a size. `BVDInterval mask l d` represents the set of values of the form `x mod 2^w` for `x` such that `l <= x <= l + d`. It should satisfy the invariants `0 <= l < 2^w` and `0 <= d < 2^w`. The first argument caches the value `2^w-1`.

#### Instances

Instances details

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

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

Check 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

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

Unsafe constructor for internal use only. Caller must ensure that `mask = maxUnsigned w`, and that `aw` is non-negative.

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

Compute how many concrete elements are in the abstract domain

# Projection functions

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

Return value if this is a singleton.

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

Return unsigned bounds for domain.

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

Return signed bounds for domain.

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

slt :: forall (w :: Natural). 1 <= w => NatRepr w -> Domain w -> Domain w -> Maybe Bool Source #

Check if all elements in one domain are less than all elements in other.

ult :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Maybe Bool Source #

Check if all elements in one domain are less than all elements in other.

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

Check if `(bvult (bvadd a c) (bvadd b c))` is equivalent to `(bvult a b)`.

This is true if and only if for all natural values `i_a`, `i_b`, `i_c` in `a`, `b`, `c`, either both `i_a + i_c` and `i_b + i_c` are less than `2^w`, or both are not. We prove this by contradiction. If `i_a = i_b`, then the property is trivial. Assume that `i_a < i_b`. Then `i_a + i_c < i_b + i_c`. If exactly one of the additions is less than `2^w`, it must be the case that `i_a + i_c < 2^w` and `0 <= i_b + i_c - 2^w < 2^w`. Since `i_b < 2^w`, it follows that `i_b + i_c < 2^w + i_c`, that `i_b + i_c - 2^w < i_c`, and that `i_b + i_c - 2^w < i_a + i_c`. Thus, for these values of `i_a`, `i_b`, `i_c`, `(bvult a b)` is true, but `(bvult (bvadd a c) (bvadd b c))` is false, which is a contradiction.

We check this property by case analysis on whether `c` is a single non-wrapping interval, or it wraps around and is a union of two non-wrapping intervals. For a non-wrapping (sub)interval `c'` of `c`, there are four possible cases: 1. `a` and `b` contain a single value. 2. `(bvadd a c')` and `(bvadd b c')` do not wrap around for any values in `a`, `b`, `c'`. 3. `(bvadd a c')` and `(bvadd b c')` wrap around for all values in `a`, `b`, `c'`.

This is used to simplify `bvult`.

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

Return true if domains contain a common element.

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

Return the `(lo,sz)`, the low bound and size of the given arithmetic interval. A value `x` is in the set defined by this domain iff `(x - lo) `mod` w <= sz` holds. Returns `Nothing` if the domain contains all values.

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

Return bitwise bounds for domain (i.e. logical AND of all possible values, paired with logical OR of all possible values).

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

`unknowns lo hi` returns a bitmask representing the set of bit positions whose values are not constant throughout the range `lo..hi`.

fillright :: Integer -> Integer Source #

`fillright x` rounds up `x` to the nearest 2^n-1.

# Operations

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

Represents all values

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

Create a bitvector domain representing the integer.

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

`range w l u` returns domain containing all bitvectors formed from the `w` low order bits of some `i` in `[l,u]`. Note that per `testBit`, the least significant bit has index `0`.

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

Create an abstract domain from an ascending list of elements. The elements are assumed to be distinct.

union :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Domain w Source #

Return union of two domains.

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 #

## Shifts

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

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

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

## Arithmetic

add :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Domain w Source #

negate :: forall (w :: Natural). 1 <= w => Domain w -> Domain w Source #

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

mul :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Domain w Source #

udiv :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Domain w Source #

urem :: forall (w :: Natural). 1 <= w => Domain w -> Domain w -> Domain w Source #

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

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

## Bitwise

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

Complement bits in range.

# Correctness properties

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

Random generator for domain values

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

Generate a random element from a domain

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

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

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

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

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

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

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

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

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

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

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

correct_sdivRange :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer -> Property Source #

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

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

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

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

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

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

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

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

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

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