| Copyright | (c) Galois Inc 2018 |
|---|---|
| License | BSD3 |
| Maintainer | Rob Dockins <rdockins@galois.com> |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.Utils.MuxTree
Description
This module defines a MuxTree type that notionally represents
a collection of values organized into an if-then-else tree. This
data structure allows values that otherwise do not have a useful notion
of symbolic values to nonetheless be merged as control flow merge points
by simply remembering which concrete values were obtained, and the
logical conditions under which they were found.
Note that we require an Ord instance on the type a over which we are
building the mux trees. It is sufficent that this operation be merely
syntactic equality; it is not necessary for correctness that terms with
the same semantics compare equal.
Synopsis
- data MuxTree sym a
- toMuxTree :: IsExprBuilder sym => sym -> a -> MuxTree sym a
- mergeMuxTree :: (Ord a, IsExprBuilder sym) => sym -> Pred sym -> MuxTree sym a -> MuxTree sym a -> IO (MuxTree sym a)
- viewMuxTree :: MuxTree sym a -> [(a, Pred sym)]
- muxTreeUnaryOp :: (Ord b, IsExprBuilder sym) => sym -> (a -> IO b) -> MuxTree sym a -> IO (MuxTree sym b)
- muxTreeBinOp :: (Ord c, IsExprBuilder sym) => sym -> (a -> b -> IO c) -> MuxTree sym a -> MuxTree sym b -> IO (MuxTree sym c)
- muxTreeCmpOp :: IsExprBuilder sym => sym -> (a -> a -> IO (Pred sym)) -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym)
- collapseMuxTree :: IsExprBuilder sym => sym -> (Pred sym -> a -> a -> IO a) -> MuxTree sym a -> IO a
- muxTreeEq :: (Eq a, IsExprBuilder sym) => sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym)
- muxTreeLe :: (Ord a, IsExprBuilder sym) => sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym)
- muxTreeLt :: (Ord a, IsExprBuilder sym) => sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym)
- muxTreeGe :: (Ord a, IsExprBuilder sym) => sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym)
- muxTreeGt :: (Ord a, IsExprBuilder sym) => sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym)
Documentation
A mux tree represents a collection of if-then-else branches over a collection of values. Generally, a mux tree is used to provide a way to conditionally merge values that otherwise do not naturally have a merge operation.
toMuxTree :: IsExprBuilder sym => sym -> a -> MuxTree sym a Source #
mergeMuxTree :: (Ord a, IsExprBuilder sym) => sym -> Pred sym -> MuxTree sym a -> MuxTree sym a -> IO (MuxTree sym a) Source #
Compute the if-then-else operation on mux trees.
viewMuxTree :: MuxTree sym a -> [(a, Pred sym)] Source #
muxTreeUnaryOp :: (Ord b, IsExprBuilder sym) => sym -> (a -> IO b) -> MuxTree sym a -> IO (MuxTree sym b) Source #
Apply a unary operation through a mux tree. The provided operation is applied to each leaf of the tree.
muxTreeBinOp :: (Ord c, IsExprBuilder sym) => sym -> (a -> b -> IO c) -> MuxTree sym a -> MuxTree sym b -> IO (MuxTree sym c) Source #
Apply a binary operation through two mux trees. The provided operation is applied pairwise to each leaf of the two trees, and appropriate path conditions are computed for the resulting values.
Arguments
| :: IsExprBuilder sym | |
| => sym | |
| -> (a -> a -> IO (Pred sym)) | compute the predicate on the underlying type |
| -> MuxTree sym a | |
| -> MuxTree sym a | |
| -> IO (Pred sym) |
Compute a binary boolean predicate between two mux trees. This operation decomposes the mux trees and compares all combinations of the underlying values, conditional on the path conditions leading to those values.
collapseMuxTree :: IsExprBuilder sym => sym -> (Pred sym -> a -> a -> IO a) -> MuxTree sym a -> IO a Source #
Use the provided if-then-else operation to collapse the given mux tree into its underlying type.
muxTreeEq :: (Eq a, IsExprBuilder sym) => sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym) Source #
Compute an equality predicate on mux trees.
NOTE! This assumes the equality relation
defined by Eq is the semantic equality
relation on a.
muxTreeLe :: (Ord a, IsExprBuilder sym) => sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym) Source #
Compute a less-than-or-equal predicate on mux trees.
NOTE! This assumes the order relation
defined by Ord is the semantic order
relation on a.
muxTreeLt :: (Ord a, IsExprBuilder sym) => sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym) Source #
Compute a less-than predicate on mux trees.
NOTE! This assumes the order relation
defined by Ord is the semantic order
relation on a.