Module isla_lib::bitvector [−][src]
This module defines the bitvector trait BV, and includes modules for concrete bitvectors of up to 64-bits, or up to 129-bits. The 129-bit bitvectors are intended for CHERI architectures as it allows capabilities to be represented without involving the SMT solver. Most functions in isla-lib, and dependent libraries will be parametric over the BV trait.
The reason for having an upper-bound on the size of concrete
bitvectors is so they can be fixed size, which allows them to be
Copy types in rust. This does not affect expressivity, just that
longer bitvectors will also be represented in the SMT solver, and
appear in isla as Val::Symbolic (as defined the ir module).
Modules
| b64 | |
| b129 |
Traits
| BV | This trait allows us to be generic over the representation of concrete bitvectors. Specific users of isla-lib may then choose different representations depending on use case - B64 will likely be the most efficient for ordinary use, but B129 can represent CHERI compressed capabilities concretely. |
Functions
| bzhi_u64 | |
| bzhi_u128 | |
| write_bits64 |