Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
- data BV = BV !Integer !Integer
- binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV
- unaryBV :: (Integer -> Integer) -> BV -> BV
- bvVal :: BV -> Integer
- mkBv :: Integer -> Integer -> BV
- data SeqMap b w
- lookupSeqMap :: SeqMap b w -> Integer -> Eval (GenValue b w)
- type SeqValMap = SeqMap Bool BV
- finiteSeqMap :: [Eval (GenValue b w)] -> SeqMap b w
- infiniteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w)
- enumerateSeqMap :: Integral n => n -> SeqMap b w -> [Eval (GenValue b w)]
- streamSeqMap :: SeqMap b w -> [Eval (GenValue b w)]
- reverseSeqMap :: Integer -> SeqMap b w -> SeqMap b w
- updateSeqMap :: SeqMap b w -> Integer -> Eval (GenValue b w) -> SeqMap b w
- splitSeqMap :: Integer -> SeqMap b w -> (SeqMap b w, SeqMap b w)
- memoMap :: SeqMap b w -> Eval (SeqMap b w)
- zipSeqMap :: (GenValue b w -> GenValue b w -> Eval (GenValue b w)) -> SeqMap b w -> SeqMap b w -> Eval (SeqMap b w)
- mapSeqMap :: (GenValue b w -> Eval (GenValue b w)) -> SeqMap b w -> Eval (SeqMap b w)
- data WordValue b w
- asWordVal :: BitWord b w => WordValue b w -> Eval w
- asBitsVal :: BitWord b w => WordValue b w -> Seq (Eval b)
- indexWordValue :: BitWord b w => WordValue b w -> Integer -> Eval b
- data GenValue b w
- = VRecord ![(Ident, Eval (GenValue b w))]
- | VTuple ![Eval (GenValue b w)]
- | VBit !b
- | VSeq !Integer !(SeqMap b w)
- | VWord !Integer !(Eval (WordValue b w))
- | VStream !(SeqMap b w)
- | VFun (Eval (GenValue b w) -> Eval (GenValue b w))
- | VPoly (TValue -> Eval (GenValue b w))
- | VNumPoly (Nat' -> Eval (GenValue b w))
- forceWordValue :: WordValue b w -> Eval ()
- forceValue :: GenValue b w -> Eval ()
- type Value = GenValue Bool BV
- data PPOpts = PPOpts {}
- defaultPPOpts :: PPOpts
- atFst :: Functor f => (a -> f b) -> (a, c) -> f (b, c)
- atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b)
- ppValue :: forall b w. BitWord b w => PPOpts -> GenValue b w -> Eval Doc
- asciiMode :: PPOpts -> Integer -> Bool
- integerToChar :: Integer -> Char
- ppBV :: PPOpts -> BV -> Doc
- class BitWord b w | b -> w, w -> b where
- class BitWord b w => EvalPrims b w where
- mask :: Integer -> Integer -> Integer
- word :: BitWord b w => Integer -> Integer -> GenValue b w
- lam :: (Eval (GenValue b w) -> Eval (GenValue b w)) -> GenValue b w
- wlam :: BitWord b w => (w -> Eval (GenValue b w)) -> GenValue b w
- tlam :: (TValue -> GenValue b w) -> GenValue b w
- nlam :: (Nat' -> GenValue b w) -> GenValue b w
- toStream :: [GenValue b w] -> Eval (GenValue b w)
- toFinSeq :: BitWord b w => Integer -> TValue -> [GenValue b w] -> GenValue b w
- boolToWord :: [Bool] -> Value
- toSeq :: BitWord b w => Nat' -> TValue -> [GenValue b w] -> Eval (GenValue b w)
- mkSeq :: Nat' -> TValue -> SeqMap b w -> GenValue b w
- fromVBit :: GenValue b w -> b
- bitsSeq :: BitWord b w => WordValue b w -> Integer -> Eval b
- fromSeq :: forall b w. BitWord b w => String -> GenValue b w -> Eval (SeqMap b w)
- fromStr :: Value -> Eval String
- fromWordVal :: String -> GenValue b w -> Eval (WordValue b w)
- fromVWord :: BitWord b w => String -> GenValue b w -> Eval w
- vWordLen :: BitWord b w => GenValue b w -> Maybe Integer
- tryFromBits :: BitWord b w => [Eval (GenValue b w)] -> Maybe w
- fromWord :: String -> Value -> Eval Integer
- fromVFun :: GenValue b w -> Eval (GenValue b w) -> Eval (GenValue b w)
- fromVPoly :: GenValue b w -> TValue -> Eval (GenValue b w)
- fromVNumPoly :: GenValue b w -> Nat' -> Eval (GenValue b w)
- fromVTuple :: GenValue b w -> [Eval (GenValue b w)]
- fromVRecord :: GenValue b w -> [(Ident, Eval (GenValue b w))]
- lookupRecord :: Ident -> GenValue b w -> Eval (GenValue b w)
- toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr)
Documentation
Concrete bitvector values: width, value Invariant: The value must be within the range 0 .. 2^width-1
binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV Source #
Apply an integer function to the values of bitvectors. This function assumes both bitvectors are the same width.
unaryBV :: (Integer -> Integer) -> BV -> BV Source #
Apply an integer function to the values of a bitvector. This function assumes the function will not require masking.
A sequence map represents a mapping from nonnegative integer indices to values. These are used to represent both finite and infinite sequences.
finiteSeqMap :: [Eval (GenValue b w)] -> SeqMap b w Source #
Generate a finite sequence map from a list of values
infiniteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w) Source #
Generate an infinite sequence map from a stream of values
enumerateSeqMap :: Integral n => n -> SeqMap b w -> [Eval (GenValue b w)] Source #
Create a finite list of length n
of the values from [0..n-1] in
the given the sequence emap.
streamSeqMap :: SeqMap b w -> [Eval (GenValue b w)] Source #
Create an infinite stream of all the values in a sequence map
Reverse the order of a finite sequence map
splitSeqMap :: Integer -> SeqMap b w -> (SeqMap b w, SeqMap b w) Source #
Given a number n
and a sequence map, return two new sequence maps:
the first containing the values from `[0..n-1]` and the next containing
the values from n
onward.
memoMap :: SeqMap b w -> Eval (SeqMap b w) Source #
Given a sequence map, return a new sequence map that is memoized using a finite map memo table.
zipSeqMap :: (GenValue b w -> GenValue b w -> Eval (GenValue b w)) -> SeqMap b w -> SeqMap b w -> Eval (SeqMap b w) Source #
Apply the given evaluation function pointwise to the two given sequence maps.
mapSeqMap :: (GenValue b w -> Eval (GenValue b w)) -> SeqMap b w -> Eval (SeqMap b w) Source #
Apply the given function to each value in the given sequence map
For efficency reasons, we handle finite sequences of bits as special cases in the evaluator. In cases where we know it is safe to do so, we prefer to used a "packed word" representation of bit sequences. This allows us to rely directly on Integer types (in the concrete evalautor) and SBV's Word types (in the symbolic simulator).
However, if we cannot be sure all the bits of the sequence will eventually be forced, we must instead rely on an explicit sequence of bits representation.
asWordVal :: BitWord b w => WordValue b w -> Eval w Source #
Force a word value into packed word form
asBitsVal :: BitWord b w => WordValue b w -> Seq (Eval b) Source #
Force a word value into a sequence of bits
indexWordValue :: BitWord b w => WordValue b w -> Integer -> Eval b Source #
Select an individual bit from a word value
Generic value type, parameterized by bit and word types.
NOTE: we maintain an important invariant regarding sequence types.
VSeq
must never be used for finite sequences of bits.
Always use the VWord
constructor instead! Infinite sequences of bits
are handled by the VStream
constructor, just as for other types.
VRecord ![(Ident, Eval (GenValue b w))] | { .. } |
VTuple ![Eval (GenValue b w)] | ( .. ) |
VBit !b | Bit |
VSeq !Integer !(SeqMap b w) |
|
VWord !Integer !(Eval (WordValue b w)) | [n]Bit |
VStream !(SeqMap b w) | [inf]a |
VFun (Eval (GenValue b w) -> Eval (GenValue b w)) | functions |
VPoly (TValue -> Eval (GenValue b w)) | polymorphic values (kind *) |
VNumPoly (Nat' -> Eval (GenValue b w)) | polymorphic values (kind #) |
forceWordValue :: WordValue b w -> Eval () Source #
Force the evaluation of a word value
forceValue :: GenValue b w -> Eval () Source #
Force the evaluation of a value
integerToChar :: Integer -> Char Source #
class BitWord b w | b -> w, w -> b where Source #
This type class defines a collection of operations on bits and words that are necessary to define generic evaluator primitives that operate on both concrete and symbolic values uniformly.
ppBit, ppWord, wordAsChar, wordLen, bitLit, wordLit, packWord, unpackWord, joinWord, splitWord, extractWord, wordPlus, wordMinus, wordMult
Pretty-print an individual bit
ppWord :: PPOpts -> w -> Doc Source #
Pretty-print a word value
wordAsChar :: w -> Maybe Char Source #
Attempt to render a word value as an ASCII character. Return Nothing
if the character value is unknown (e.g., for symbolic values).
wordLen :: w -> Integer Source #
The number of bits in a word value.
Construct a literal bit value from a boolean.
wordLit :: Integer -> Integer -> w Source #
Construct a literal word value given a bit width and a value.
Construct a word value from a finite sequence of bits. NOTE: this assumes that the sequence of bits is big-endian and finite, so the first element of the list will be the most significant bit.
unpackWord :: w -> [b] Source #
Deconstruct a packed word value in to a finite sequence of bits. NOTE: this produces a list of bits that represent a big-endian word, so the most significant bit is the first element of the list.
joinWord :: w -> w -> w Source #
Concatenate the two given word values. NOTE: the first argument represents the more-significant bits
splitWord :: Integer -> Integer -> w -> (w, w) Source #
Take the most-significant bits, and return those bits and the remainder. The first element of the pair is the most significant bits. The two integer sizes must sum to the length of the given word value.
extractWord :: Integer -> Integer -> w -> w Source #
Extract a subsequence of bits from a packed word value.
The first integer argument is the number of bits in the
resulting word. The second integer argument is the
number of less-significant digits to discard. Stated another
way, the operation `extractWord n i w` is equivelant to
first shifting w
right by i
bits, and then truncating to
n
bits.
wordPlus :: w -> w -> w Source #
2's complement addition of packed words. The arguments must have equal bit width, and the result is of the same width. Overflow is silently discarded.
wordMinus :: w -> w -> w Source #
2's complement subtraction of packed words. The arguments must have equal bit width, and the result is of the same width. Overflow is silently discarded.
wordMult :: w -> w -> w Source #
2's complement multiplication of packed words. The arguments must have equal bit width, and the result is of the same width. The high bits of the multiplication are silently discarded.
class BitWord b w => EvalPrims b w where Source #
This class defines additional operations necessary to define generic evaluation functions.
evalPrim :: Decl -> GenValue b w Source #
Eval prim binds primitive declarations to the primitive values that implement them.
iteValue :: b -> Eval (GenValue b w) -> Eval (GenValue b w) -> Eval (GenValue b w) Source #
ifthenelse operation. Choose either the 'then' value or the 'else' value depending on the value of the test bit.
wlam :: BitWord b w => (w -> Eval (GenValue b w)) -> GenValue b w Source #
Functions that assume word inputs
boolToWord :: [Bool] -> Value Source #
This is strict!
toSeq :: BitWord b w => Nat' -> TValue -> [GenValue b w] -> Eval (GenValue b w) Source #
Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.
mkSeq :: Nat' -> TValue -> SeqMap b w -> GenValue b w Source #
Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.
fromSeq :: forall b w. BitWord b w => String -> GenValue b w -> Eval (SeqMap b w) Source #
Extract a sequence.
tryFromBits :: BitWord b w => [Eval (GenValue b w)] -> Maybe w Source #
If the given list of values are all fully-evaluated thunks
containing bits, return a packed word built from the same bits.
However, if any value is not a fully-evaluated bit, return Nothing
.
fromWord :: String -> Value -> Eval Integer Source #
Turn a value into an integer represented by w bits.
fromVFun :: GenValue b w -> Eval (GenValue b w) -> Eval (GenValue b w) Source #
Extract a function from a value.
fromVPoly :: GenValue b w -> TValue -> Eval (GenValue b w) Source #
Extract a polymorphic function from a value.
fromVNumPoly :: GenValue b w -> Nat' -> Eval (GenValue b w) Source #
Extract a polymorphic function from a value.