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

Copyright(c) Galois Inc 2014-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Safe HaskellNone
LanguageHaskell2010

What4.WordMap

Description

 
Synopsis

Documentation

data WordMap sym w tp Source #

A WordMap represents a finite partial map from bitvectors of width w to elements of type 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.