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

Copyright | (c) Galois Inc 2014-2020
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.WordMap

Description

Synopsis

- data WordMap sym w tp = SimpleWordMap !(SymExpr sym (BaseArrayType (EmptyCtx ::> BaseBVType w) BaseBoolType)) !(SymExpr sym (BaseArrayType (EmptyCtx ::> BaseBVType w) tp))
- emptyWordMap :: (IsExprBuilder sym, 1 <= w) => sym -> NatRepr w -> BaseTypeRepr a -> IO (WordMap sym w a)
- muxWordMap :: IsExprBuilder sym => sym -> NatRepr w -> BaseTypeRepr a -> Pred sym -> WordMap sym w a -> WordMap sym w a -> IO (WordMap sym w a)
- insertWordMap :: IsExprBuilder sym => sym -> NatRepr w -> BaseTypeRepr a -> SymBV sym w -> SymExpr sym a -> WordMap sym w a -> IO (WordMap sym w a)
- lookupWordMap :: IsExprBuilder sym => sym -> NatRepr w -> BaseTypeRepr a -> SymBV sym w -> WordMap sym w a -> IO (PartExpr (Pred sym) (SymExpr sym a))

# Documentation

data WordMap sym w tp Source #

A `WordMap` represents a finite partial map from bitvectors of width `w` to elements of type `tp`.

Constructors

SimpleWordMap !(SymExpr sym (BaseArrayType (EmptyCtx ::> BaseBVType w) BaseBoolType)) !(SymExpr sym (BaseArrayType (EmptyCtx ::> BaseBVType w) tp)) |

emptyWordMap :: (IsExprBuilder sym, 1 <= w) => sym -> NatRepr w -> BaseTypeRepr a -> IO (WordMap sym w a) Source #

Create a word map where every element is undefined.

muxWordMap :: IsExprBuilder sym => sym -> NatRepr w -> BaseTypeRepr a -> Pred sym -> WordMap sym w a -> WordMap sym w a -> IO (WordMap sym w a) Source #

Compute a pointwise if-then-else operation on the elements of two word maps.

insertWordMap Source #

Arguments

:: IsExprBuilder sym |
=> sym |
-> NatRepr w |
-> BaseTypeRepr a |
-> SymBV sym w | index
-> SymExpr sym a | new value
-> WordMap sym w a | word map to update
-> IO (WordMap sym w a) |

Update a word map at the given index.

lookupWordMap Source #

Arguments

:: IsExprBuilder sym |
=> sym |
-> NatRepr w |
-> BaseTypeRepr a |
-> SymBV sym w | index
-> WordMap sym w a |
-> IO (PartExpr (Pred sym) (SymExpr sym a)) |

Lookup the value of an index in a word map.