Lang.Crucible.Utils.MuxTree

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.

Documentation

data MuxTree sym a

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

mergeMuxTree :: (Ord a, IsExprBuilder sym) => sym -> Pred sym -> MuxTree sym a -> MuxTree sym a -> IO (MuxTree sym a)

Compute the if-then-else operation on mux trees.

viewMuxTree :: MuxTree sym a -> [(a, Pred sym)]

muxTreeUnaryOp :: (Ord b, IsExprBuilder sym) => sym -> (a -> IO b) -> MuxTree sym a -> IO (MuxTree sym b)

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)

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.

muxTreeCmpOp

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

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)

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)

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)

Compute a less-than predicate on mux trees.

NOTE! This assumes the order relation defined by Ord is the semantic order relation on a.

muxTreeGe :: (Ord a, IsExprBuilder sym) => sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym)

Compute a greater-than-or-equal predicate on mux trees.

NOTE! This assumes the order relation defined by Ord is the semantic order relation on a.

muxTreeGt :: (Ord a, IsExprBuilder sym) => sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym)

Compute a greater-than predicate on mux trees.

NOTE! This assumes the order relation defined by Ord is the semantic order relation on a.