Module bitvec::index [−][src]
Expand description
Typed metadata of registers.
This module provides types which guarantee certain properties about working with individual bits of registers.
The main advantage of the types in this module is that they provide type-dependent range constrictions for index values, making it impossible to have an index out of bounds for a register, and creating a sequence of type transformations that give assurance about the continued validity of each value in its surrounding context.
By eliminating public constructors from arbitrary integers, bitvec can
guarantee that only it can produce seed values, and only trusted functions can
transform their numeric values or types, until the program reaches the property
it requires. This chain of assurance means that operations that interact with
memory can be confident in the correctness of their actions and effects.
Type Sequence
The library produces BitIdx values from region computation. These types cannot
be publicly constructed, and are only ever the result of pointer analysis. As
such, they rely on correctness of the memory regions provided to library entry
points, and those entry points can leverage the Rust type system to ensure
safety there.
BitIdx is transformed to BitPos through the BitOrder trait, which has an
associated verification function to prove that implementations are correct.
BitPos is the only type that can describe memory operations, and is used to
create selection masks of BitSel and BitMask.
Structs
A semantic index of a single bit within a register R.
A multi-bit selection mask.
An electrical position of a single bit within a register R.
A one-hot selection mask, to be applied to a register R.
Semantic index of a dead bit after a live region.
Traits
Marks that an integer can be used in a processor register.