This module is responsible for managing the absolute addresses that allocations are located at,
and for casting between pointers and integers based on those addresses.
Main evaluator loop and setting up the initial stack frame.
Global machine state as well as implementation of the interpreter engine
Machine trait.
This is a “monotonic FxHashMap”: A FxHashMap that, when shared, can be pushed to but not
otherwise mutated. We also box items in the map. This means we can safely provide
shared references into existing items in the FxHashMap, because they will not be dropped
(from being removed) or moved (because they are boxed).
The API is completely tailored to what memory.rs needs. It is still in
a separate file to minimize the amount of code that has to care about the unsafety.
Implements a map from integer indices to data.
Rather than storing data for every index, internally, this maps entire ranges to the data.
To this end, the APIs all work on ranges, not on individual integers. Ranges are split as
necessary (e.g., when [0,5) is first associated with X, and then [1,2) is mutated).
Users must not depend on whether a range is coalesced or not, even though this is observable
via the iteration APIs.
Extra per-allocation data
Tracking pointer provenance
Holds all of the relevant data for when unwinding hits a try frame.
A monotone clock used for Instant simulation.
0 is used to indicate that the id was not yet assigned and,
therefore, is not a valid identifier.
Type of dynamic symbols (for dlsym et al)
Extra data stored with each stack frame
0 is used to indicate that the id was not yet assigned and,
therefore, is not a valid identifier.
An item in the per-location borrow stack.
Allocation bytes that explicitly handle the layout of the data they’re storing.
This is necessary to interface with native code that accesses the program store in Miri.
Configuration needed to spawn a Miri instance.
The machine itself.
0 is used to indicate that the id was not yet assigned and,
therefore, is not a valid identifier.
Precomputed layouts of primitive types
0 is used to indicate that the id was not yet assigned and,
therefore, is not a valid identifier.
Extra per-location state.
Extra per-allocation state.
The state of all synchronization objects.
A thread identifier.
A set of threads.
Tree structure with both parents and children since we want to be
able to traverse the tree efficiently in both directions.
Indicates which kind of access is being performed.
Valid atomic fence orderings, subset of atomic::Ordering.
Valid atomic read orderings, subset of atomic::Ordering.
Valid atomic read-write orderings, alias of atomic::Ordering (not non-exhaustive).
Valid atomic write orderings, subset of atomic::Ordering.
Keeps track of what the thread is blocked on.
Which borrow tracking method to use
What needs to be done after emulating an item (a shim or an intrinsic) is done.
Extra memory kinds
Miri specific diagnostics
Indicates which permission is granted (by this item to some pointers)
Pointer provenance.
The “extra” information a pointer has over a regular AllocId.
Policy on whether to recurse into fields to retag
Details of premature program termination.
Whether the timeout is relative or absolute.
The clock to use for the timeout you are asking for.