Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Synopsis
- data GenValue sym
- = VRecord !(RecordMap Ident (SEval sym (GenValue sym)))
- | VTuple ![SEval sym (GenValue sym)]
- | VBit !(SBit sym)
- | VInteger !(SInteger sym)
- | VRational !(SRational sym)
- | VFloat !(SFloat sym)
- | VSeq !Integer !(SeqMap sym)
- | VWord !Integer !(SEval sym (WordValue sym))
- | VStream !(SeqMap sym)
- | VFun (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
- | VPoly (TValue -> SEval sym (GenValue sym))
- | VNumPoly (Nat' -> SEval sym (GenValue sym))
- forceWordValue :: Backend sym => WordValue sym -> SEval sym ()
- forceValue :: Backend sym => GenValue sym -> SEval sym ()
- class MonadIO (SEval sym) => Backend sym where
- type SBit sym :: Type
- type SWord sym :: Type
- type SInteger sym :: Type
- type SFloat sym :: Type
- type SEval sym :: Type -> Type
- isReady :: sym -> SEval sym a -> Bool
- sDeclareHole :: sym -> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())
- sDelayFill :: sym -> SEval sym a -> SEval sym a -> SEval sym (SEval sym a)
- sSpark :: sym -> SEval sym a -> SEval sym (SEval sym a)
- mergeEval :: sym -> (SBit sym -> a -> a -> SEval sym a) -> SBit sym -> SEval sym a -> SEval sym a -> SEval sym a
- assertSideCondition :: sym -> SBit sym -> EvalError -> SEval sym ()
- raiseError :: sym -> EvalError -> SEval sym a
- ppBit :: sym -> SBit sym -> Doc
- ppWord :: sym -> PPOpts -> SWord sym -> Doc
- ppInteger :: sym -> PPOpts -> SInteger sym -> Doc
- ppFloat :: sym -> PPOpts -> SFloat sym -> Doc
- bitAsLit :: sym -> SBit sym -> Maybe Bool
- wordLen :: sym -> SWord sym -> Integer
- wordAsLit :: sym -> SWord sym -> Maybe (Integer, Integer)
- wordAsChar :: sym -> SWord sym -> Maybe Char
- integerAsLit :: sym -> SInteger sym -> Maybe Integer
- bitLit :: sym -> Bool -> SBit sym
- wordLit :: sym -> Integer -> Integer -> SEval sym (SWord sym)
- integerLit :: sym -> Integer -> SEval sym (SInteger sym)
- fpLit :: sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
- iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
- iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
- bitEq :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
- bitOr :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
- bitAnd :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
- bitXor :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
- bitComplement :: sym -> SBit sym -> SEval sym (SBit sym)
- wordBit :: sym -> SWord sym -> Integer -> SEval sym (SBit sym)
- wordUpdate :: sym -> SWord sym -> Integer -> SBit sym -> SEval sym (SWord sym)
- packWord :: sym -> [SBit sym] -> SEval sym (SWord sym)
- unpackWord :: sym -> SWord sym -> SEval sym [SBit sym]
- wordFromInt :: sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
- joinWord :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- splitWord :: sym -> Integer -> Integer -> SWord sym -> SEval sym (SWord sym, SWord sym)
- extractWord :: sym -> Integer -> Integer -> SWord sym -> SEval sym (SWord sym)
- wordOr :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- wordAnd :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- wordXor :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- wordComplement :: sym -> SWord sym -> SEval sym (SWord sym)
- wordPlus :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- wordMinus :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- wordMult :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- wordDiv :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- wordMod :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- wordSignedDiv :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- wordSignedMod :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- wordNegate :: sym -> SWord sym -> SEval sym (SWord sym)
- wordLg2 :: sym -> SWord sym -> SEval sym (SWord sym)
- wordEq :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
- wordSignedLessThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
- wordLessThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
- wordGreaterThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
- wordToInt :: sym -> SWord sym -> SEval sym (SInteger sym)
- intPlus :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
- intNegate :: sym -> SInteger sym -> SEval sym (SInteger sym)
- intMinus :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
- intMult :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
- intDiv :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
- intMod :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
- intEq :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
- intLessThan :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
- intGreaterThan :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
- intToZn :: sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
- znToInt :: sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
- znPlus :: sym -> Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
- znNegate :: sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
- znMinus :: sym -> Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
- znMult :: sym -> Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
- znEq :: sym -> Integer -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
- fpEq :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
- fpLessThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
- fpGreaterThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
- fpPlus, fpMinus, fpMult, fpDiv :: FPArith2 sym
- fpNeg :: sym -> SFloat sym -> SEval sym (SFloat sym)
- fpToInteger :: sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
- fpFromInteger :: sym -> Integer -> Integer -> SWord sym -> SInteger sym -> SEval sym (SFloat sym)
- asciiMode :: PPOpts -> Integer -> Bool
- word :: Backend sym => sym -> Integer -> Integer -> GenValue sym
- lam :: (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -> GenValue sym
- wlam :: Backend sym => sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
- flam :: Backend sym => (SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym
- tlam :: Backend sym => (TValue -> GenValue sym) -> GenValue sym
- nlam :: Backend sym => (Nat' -> GenValue sym) -> GenValue sym
- ilam :: Backend sym => (Integer -> GenValue sym) -> GenValue sym
- toStream :: Backend sym => [GenValue sym] -> SEval sym (GenValue sym)
- toFinSeq :: Backend sym => sym -> Integer -> TValue -> [GenValue sym] -> GenValue sym
- toSeq :: Backend sym => sym -> Nat' -> TValue -> [GenValue sym] -> SEval sym (GenValue sym)
- mkSeq :: Backend sym => Nat' -> TValue -> SeqMap sym -> GenValue sym
- fromVBit :: GenValue sym -> SBit sym
- fromVInteger :: GenValue sym -> SInteger sym
- fromVRational :: GenValue sym -> SRational sym
- fromVFloat :: GenValue sym -> SFloat sym
- fromVSeq :: GenValue sym -> SeqMap sym
- fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym)
- fromWordVal :: Backend sym => String -> GenValue sym -> SEval sym (WordValue sym)
- asIndex :: Backend sym => sym -> String -> TValue -> GenValue sym -> SEval sym (Either (SInteger sym) (WordValue sym))
- fromVWord :: Backend sym => sym -> String -> GenValue sym -> SEval sym (SWord sym)
- vWordLen :: Backend sym => GenValue sym -> Maybe Integer
- tryFromBits :: Backend sym => sym -> [SEval sym (GenValue sym)] -> Maybe (SEval sym (SWord sym))
- fromVFun :: GenValue sym -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
- fromVPoly :: GenValue sym -> TValue -> SEval sym (GenValue sym)
- fromVNumPoly :: GenValue sym -> Nat' -> SEval sym (GenValue sym)
- fromVTuple :: GenValue sym -> [SEval sym (GenValue sym)]
- fromVRecord :: GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
- lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym)
- defaultPPOpts :: PPOpts
- ppValue :: forall sym. Backend sym => sym -> PPOpts -> GenValue sym -> SEval sym Doc
- data SeqMap sym
- lookupSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym)
- finiteSeqMap :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SeqMap sym
- infiniteSeqMap :: Backend sym => [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
- enumerateSeqMap :: Integral n => n -> SeqMap sym -> [SEval sym (GenValue sym)]
- streamSeqMap :: SeqMap sym -> [SEval sym (GenValue sym)]
- reverseSeqMap :: Integer -> SeqMap sym -> SeqMap sym
- updateSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
- dropSeqMap :: Integer -> SeqMap sym -> SeqMap sym
- concatSeqMap :: Integer -> SeqMap sym -> SeqMap sym -> SeqMap sym
- splitSeqMap :: Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
- memoMap :: (MonadIO m, Backend sym) => SeqMap sym -> m (SeqMap sym)
- zipSeqMap :: Backend sym => (GenValue sym -> GenValue sym -> SEval sym (GenValue sym)) -> SeqMap sym -> SeqMap sym -> SEval sym (SeqMap sym)
- mapSeqMap :: Backend sym => (GenValue sym -> SEval sym (GenValue sym)) -> SeqMap sym -> SEval sym (SeqMap sym)
- largeBitSize :: Integer
- data WordValue sym
- = WordVal !(SWord sym)
- | LargeBitsVal !Integer !(SeqMap sym)
- asWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (SWord sym)
- asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym
- enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]
- enumerateWordValueRev :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]
- wordValueSize :: Backend sym => sym -> WordValue sym -> Integer
- indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
- updateWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym)
GenericValue
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 !(RecordMap Ident (SEval sym (GenValue sym))) | { .. } |
VTuple ![SEval sym (GenValue sym)] | ( .. ) |
VBit !(SBit sym) | Bit |
VInteger !(SInteger sym) |
|
VRational !(SRational sym) | Rational |
VFloat !(SFloat sym) | |
VSeq !Integer !(SeqMap sym) |
|
VWord !Integer !(SEval sym (WordValue sym)) | [n]Bit |
VStream !(SeqMap sym) | [inf]a |
VFun (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) | functions |
VPoly (TValue -> SEval sym (GenValue sym)) | polymorphic values (kind *) |
VNumPoly (Nat' -> SEval sym (GenValue sym)) | polymorphic values (kind #) |
Instances
forceWordValue :: Backend sym => WordValue sym -> SEval sym () Source #
Force the evaluation of a word value
class MonadIO (SEval sym) => Backend sym where Source #
This type class defines a collection of operations on bits, words and integers that are necessary to define generic evaluator primitives that operate on both concrete and symbolic values uniformly.
type SBit sym :: Type Source #
type SWord sym :: Type Source #
type SInteger sym :: Type Source #
isReady :: sym -> SEval sym a -> Bool Source #
Check if an operation is "ready", which means its evaluation will be trivial.
sDeclareHole :: sym -> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ()) Source #
Produce a thunk value which can be filled with its associated computation after the fact. A preallocated thunk is returned, along with an operation to fill the thunk with the associated computation. This is used to implement recursive declaration groups.
sDelayFill :: sym -> SEval sym a -> SEval sym a -> SEval sym (SEval sym a) Source #
Delay the given evaluation computation, returning a thunk
which will run the computation when forced. Run the retry
computation instead if the resulting thunk is forced during
its own evaluation.
sSpark :: sym -> SEval sym a -> SEval sym (SEval sym a) Source #
Begin evaluating the given computation eagerly in a separate thread and return a thunk which will await the completion of the given computation when forced.
:: sym | |
-> (SBit sym -> a -> a -> SEval sym a) | A merge operation on values |
-> SBit sym | The condition |
-> SEval sym a | The "then" computation |
-> SEval sym a | The "else" computation |
-> SEval sym a |
Merge the two given computations according to the predicate.
assertSideCondition :: sym -> SBit sym -> EvalError -> SEval sym () Source #
Assert that a condition must hold, and indicate what sort of error is indicated if the condition fails.
raiseError :: sym -> EvalError -> SEval sym a Source #
Indiciate that an error condition exists
ppBit :: sym -> SBit sym -> Doc Source #
Pretty-print an individual bit
ppWord :: sym -> PPOpts -> SWord sym -> Doc Source #
Pretty-print a word value
ppInteger :: sym -> PPOpts -> SInteger sym -> Doc Source #
Pretty-print an integer value
ppFloat :: sym -> PPOpts -> SFloat sym -> Doc Source #
Pretty-print a floating-point value
bitAsLit :: sym -> SBit sym -> Maybe Bool Source #
Determine if this symbolic bit is a boolean literal
wordLen :: sym -> SWord sym -> Integer Source #
The number of bits in a word value.
wordAsLit :: sym -> SWord sym -> Maybe (Integer, Integer) Source #
Determine if this symbolic word is a literal. If so, return the bit width and value.
wordAsChar :: sym -> SWord sym -> 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).
integerAsLit :: sym -> SInteger sym -> Maybe Integer Source #
Determine if this symbolic integer is a literal
bitLit :: sym -> Bool -> SBit sym Source #
Construct a literal bit value from a boolean.
Construct a literal word value given a bit width and a value.
Construct a literal integer value from the given integer.
:: sym | |
-> Integer | exponent bits |
-> Integer | precision bits |
-> Rational | The rational |
-> SEval sym (SFloat sym) |
Construct a floating point value from the given rational.
iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #
iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #
iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #
bitEq :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #
bitOr :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #
bitAnd :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #
bitXor :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #
bitComplement :: sym -> SBit sym -> SEval sym (SBit sym) Source #
Extract the numbered bit from the word.
NOTE: this assumes that the sequence of bits is big-endian and finite, so the bit numbered 0 is the most significant bit.
Update the numbered bit in the word.
NOTE: this assumes that the sequence of bits is big-endian and finite, so the bit numbered 0 is the most significant bit.
packWord :: sym -> [SBit sym] -> SEval sym (SWord sym) Source #
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 :: sym -> SWord sym -> SEval sym [SBit sym] 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.
Construct a packed word of the specified width from an integer value.
joinWord :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #
Concatenate the two given word values. NOTE: the first argument represents the more-significant bits
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.
:: sym | |
-> Integer | Number of bits to take |
-> Integer | starting bit |
-> SWord sym | |
-> SEval sym (SWord sym) |
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 equivalent to
first shifting w
right by i
bits, and then truncating to
n
bits.
wordOr :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #
Bitwise OR
wordAnd :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #
Bitwise AND
wordXor :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #
Bitwise XOR
wordComplement :: sym -> SWord sym -> SEval sym (SWord sym) Source #
Bitwise complement
wordPlus :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) 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 :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) 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 :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) 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.
wordDiv :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #
2's complement unsigned division of packed words. The arguments must have equal bit width, and the result is of the same width. It is illegal to call with a second argument concretely equal to 0.
wordMod :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #
2's complement unsigned modulus of packed words. The arguments must have equal bit width, and the result is of the same width. It is illegal to call with a second argument concretely equal to 0.
wordSignedDiv :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #
2's complement signed division of packed words. The arguments must have equal bit width, and the result is of the same width. It is illegal to call with a second argument concretely equal to 0.
wordSignedMod :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #
2's complement signed modulus of packed words. The arguments must have equal bit width, and the result is of the same width. It is illegal to call with a second argument concretely equal to 0.
wordNegate :: sym -> SWord sym -> SEval sym (SWord sym) Source #
2's complement negation of bitvectors
wordLg2 :: sym -> SWord sym -> SEval sym (SWord sym) Source #
Compute rounded-up log-2 of the input
wordEq :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym) Source #
Test if two words are equal. Arguments must have the same width.
wordSignedLessThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym) Source #
Signed less-than comparison on words. Arguments must have the same width.
wordLessThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym) Source #
Unsigned less-than comparison on words. Arguments must have the same width.
wordGreaterThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym) Source #
Unsigned greater-than comparison on words. Arguments must have the same width.
wordToInt :: sym -> SWord sym -> SEval sym (SInteger sym) Source #
Construct an integer value from the given packed word.
intPlus :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #
Addition of unbounded integers.
intNegate :: sym -> SInteger sym -> SEval sym (SInteger sym) Source #
Negation of unbounded integers
intMinus :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #
Subtraction of unbounded integers.
intMult :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #
Multiplication of unbounded integers.
intDiv :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #
Integer division, rounding down. It is illegal to
call with a second argument concretely equal to 0.
Same semantics as Haskell's div
operation.
intMod :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #
Integer modulus, with division rounding down. It is illegal to
call with a second argument concretely equal to 0.
Same semantics as Haskell's mod
operation.
intEq :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym) Source #
Equality comparison on integers
intLessThan :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym) Source #
Less-than comparison on integers
intGreaterThan :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym) Source #
Greater-than comparison on integers
Turn an integer into a value in Z_n
Transform a Z_n value into an integer, ensuring the value is properly reduced modulo n
Addition of integers modulo n, for a concrete positive integer n.
Additive inverse of integers modulo n
Subtraction of integers modulo n, for a concrete positive integer n.
Multiplication of integers modulo n, for a concrete positive integer n.
Equality test of integers modulo n
fpEq :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym) Source #
fpLessThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym) Source #
fpGreaterThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym) Source #
fpPlus :: FPArith2 sym Source #
fpMinus :: FPArith2 sym Source #
fpMult :: FPArith2 sym Source #
fpDiv :: FPArith2 sym Source #
fpNeg :: sym -> SFloat sym -> SEval sym (SFloat sym) Source #
Instances
Value introduction operations
word :: Backend sym => sym -> Integer -> Integer -> GenValue sym Source #
Create a packed word of n bits.
wlam :: Backend sym => sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym Source #
Functions that assume word inputs
flam :: Backend sym => (SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym Source #
Functions that assume floating point inputs
tlam :: Backend sym => (TValue -> GenValue sym) -> GenValue sym Source #
A type lambda that expects a Type
.
nlam :: Backend sym => (Nat' -> GenValue sym) -> GenValue sym Source #
A type lambda that expects a Type
of kind #.
ilam :: Backend sym => (Integer -> GenValue sym) -> GenValue sym Source #
A type lambda that expects a finite numeric type.
toSeq :: Backend sym => sym -> Nat' -> TValue -> [GenValue sym] -> SEval sym (GenValue sym) 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 :: Backend sym => Nat' -> TValue -> SeqMap sym -> GenValue sym 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.
Value eliminators
fromVInteger :: GenValue sym -> SInteger sym Source #
Extract an integer value.
fromVRational :: GenValue sym -> SRational sym Source #
Extract a rational value.
fromVFloat :: GenValue sym -> SFloat sym Source #
fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym) Source #
Extract a sequence.
asIndex :: Backend sym => sym -> String -> TValue -> GenValue sym -> SEval sym (Either (SInteger sym) (WordValue sym)) Source #
fromVWord :: Backend sym => sym -> String -> GenValue sym -> SEval sym (SWord sym) Source #
Extract a packed word.
tryFromBits :: Backend sym => sym -> [SEval sym (GenValue sym)] -> Maybe (SEval sym (SWord sym)) 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
.
fromVFun :: GenValue sym -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #
Extract a function from a value.
fromVPoly :: GenValue sym -> TValue -> SEval sym (GenValue sym) Source #
Extract a polymorphic function from a value.
fromVNumPoly :: GenValue sym -> Nat' -> SEval sym (GenValue sym) Source #
Extract a polymorphic function from a value.
fromVRecord :: GenValue sym -> RecordMap Ident (SEval sym (GenValue sym)) Source #
Extract a record from a value.
lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym) Source #
Lookup a field in a record.
Pretty printing
Sequence Maps
A sequence map represents a mapping from nonnegative integer indices to values. These are used to represent both finite and infinite sequences.
finiteSeqMap :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SeqMap sym Source #
Generate a finite sequence map from a list of values
infiniteSeqMap :: Backend sym => [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym) Source #
Generate an infinite sequence map from a stream of values
enumerateSeqMap :: Integral n => n -> SeqMap sym -> [SEval sym (GenValue sym)] Source #
Create a finite list of length n
of the values from [0..n-1]
in
the given the sequence emap.
streamSeqMap :: SeqMap sym -> [SEval sym (GenValue sym)] Source #
Create an infinite stream of all the values in a sequence map
Reverse the order of a finite sequence map
dropSeqMap :: Integer -> SeqMap sym -> SeqMap sym Source #
Drop the first n
elements of the given SeqMap
.
concatSeqMap :: Integer -> SeqMap sym -> SeqMap sym -> SeqMap sym Source #
Concatenate the first n
values of the first sequence map onto the
beginning of the second sequence map.
splitSeqMap :: Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym) 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 :: (MonadIO m, Backend sym) => SeqMap sym -> m (SeqMap sym) Source #
Given a sequence map, return a new sequence map that is memoized using a finite map memo table.
zipSeqMap :: Backend sym => (GenValue sym -> GenValue sym -> SEval sym (GenValue sym)) -> SeqMap sym -> SeqMap sym -> SEval sym (SeqMap sym) Source #
Apply the given evaluation function pointwise to the two given sequence maps.
mapSeqMap :: Backend sym => (GenValue sym -> SEval sym (GenValue sym)) -> SeqMap sym -> SEval sym (SeqMap sym) Source #
Apply the given function to each value in the given sequence map
largeBitSize :: Integer Source #
An arbitrarily-chosen number of elements where we switch from a dense
sequence representation of bit-level words to SeqMap
representation.
WordValue
For efficiency 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 evaluator) 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.
WordVal !(SWord sym) | Packed word representation for bit sequences. |
LargeBitsVal !Integer !(SeqMap sym) | A large bitvector sequence, represented as a
|
Instances
Generic (WordValue sym) Source # | |
type Rep (WordValue sym) Source # | |
Defined in Cryptol.Eval.Value type Rep (WordValue sym) = D1 (MetaData "WordValue" "Cryptol.Eval.Value" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" False) (C1 (MetaCons "WordVal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SWord sym))) :+: C1 (MetaCons "LargeBitsVal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SeqMap sym)))) |
asWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (SWord sym) Source #
Force a word value into packed word form
asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym Source #
Force a word value into a sequence of bits
enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym] Source #
Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in big-endian order.
enumerateWordValueRev :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym] Source #
Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in reverse of the usual order, which is little-endian order.
wordValueSize :: Backend sym => sym -> WordValue sym -> Integer Source #
Compute the size of a word value