Module mini 

Macros

list

Construct a List.

Structs

Access

Access contains all information the data race detection needs about a single access.

Align

This type is basically a copy of the Align type in the Rust compiler. See Align.

AllocId

BasicBlock

A basic block is a sequence of statements followed by a terminator.

BasicMemory

BbName

ConcurrentMemory

DynWrite

Garbage-collected data structure representing a write stream and implementing Copy.

FnName

Opaque types of names for functions, vtables, trait methods, and globals. The internal representations of these types do not matter.

Function

A MiniRust function.

GcCow

A gargabe-collected pointer type implementing Copy.

Global

A global allocation.

GlobalName

Int

Garbage collected big integer that implements Copy and supports construction in const contexts.

IntPtrCast

IntType

List

Garbage-collected Vec-like datastructure implementing Copy. Note that functions which seem to mutate the List, actually clone the list and allocate a new GcCow under the hood.

LocalName

Opaque types of names for local variables and basic blocks.

Machine

This type contains everything that needs to be tracked during the execution of a MiniRust program.

Map

Garbage-collected hash map implementing Copy. This implements Ord but the order is not meaningful; this is just so one can use BTreeMaps. In particular, the order might differ across two runs of the same program.

Name

Wrapper-type for names of any kind.

PointeeInfo

Describes what we know about data behind a pointer.

Pointer

A “pointer” is the thin pointer with optionally some metadata, making it a wide pointer. This corresponds to the Rust raw pointer types, as well as references and boxes.

Program

A closed MiniRust program.

ProvenanceFrag

A one-byte provenance fragment stores the provenance and which position in the pointer this fragment had.

Relocation

A pointer into a global allocation.

Set

Garbage-collected hash set implementing Copy. This implements Ord but the order is not meaningful; this is just so one can use BTreeMaps. In particular, the order might differ across two runs of the same program.

Size

Size represents a non-negative number of bytes or bits.

String

Garbage-collected wrapper around std::string::String implementing Copy.

ThinPointer

A “thin pointer” is an address together with its Provenance. Provenance can be absent; those pointers are invalid for all non-zero-sized accesses.

Thread

TraitMethodName

TraitName

A “trait name” is an identifier for the trait a vtable is for. This depends on the defined methods and the marker traits.

TreeBorrowsFrameExtra

TreeBorrowsMemory

TreeBorrowsParams

Global parameters controlling Tree Borrows behavior.

TupleHeadLayout

Describes what is needed to define the layout of the sized head of a tuple (head.., tail).

VTable

A vtable for a trait-type pair. This is pointed to by the trait object metadata.

VTableName

Variant

x86_64

Enums

AbstractByte

AllocationKind

The “kind” of an allocation is used to distinguish, for instance, stack from heap memory.

ArgumentExpr

Function arguments can be passed by-value or in-place.

Atomicity

The different kinds of atomicity.

BbKind

The kind of a basic block in the CFG.

BinOp

CallingConvention

The CallingConvention defines how function arguments and return values are passed.

CastOp

Constant

Constants are basically values, but cannot have explicit provenance. Currently we do not support Ptr and Union constants.

Discriminator

The decision tree that computes the discriminant out of the tag for a specific enum type.

Endianness

Either LittleEndian or BigEndian.

IntBinOp

IntBinOpWithOverflow

IntUnOp

IntrinsicLockOp

IntrinsicOp

The intrinsic operations supported by MiniRust. Generally we only make things intrinsics if they cannot be operands, i.e. they are non-deterministic or mutate the global state. We also make them intrinsic if they return (), because an operand that does not return anything is kind of odd.

LayoutStrategy

Describes how the size and align of the value can be determined.

LockState

Mutability

Either Mutable or Immutable.

PlaceExpr

A “place expression” evaluates to a Place.

PointerMeta

The runtime metadata that can be stored in a wide pointer.

PointerMetaKind

The statically known kind of metadata stored in a pointer. This determines the type of the metadata, while Option<PointerMeta> determines its value.

PtrType

Stores all the information that we need to know about a pointer.

RelOp

A relational operator indicates how two values are to be compared. Unless noted otherwise, these all return a Boolean.

Signedness

Expresses whether an integer has a sign or not

Statement

Terminator

ThreadState

Type

The types of MiniRust.

UnOp

UnsafeCellStrategy

Describes where in a potentially unsized type the UnsafeCell are. Separate from LayoutStrategy since we must be able to compute LayoutStrategy from a MiniRust Type, but that does not have enough information for an UnsafeCellStrategy. FIXME: maybe it should?

ValueExpr

A “value expression” evaluates to a Value.

Traits

GcWrite

An object that fulfills both GcCompat and Write.

Memory

Note: All memory operations can be non-deterministic, which means that executing the same operation on the same memory can have different results. We also let read operations potentially mutate memory (they actually can change the current state in concurrent memory models and in Stacked Borrows).

OptionExt

Extension trait to implement try_map on Options.

Target

Functions

pick

The pick function from the minirust spec. See Non-determinism.

predict

The predict function from the minirust spec. See Non-determinism.

ret

Wraps a value i as Some(i), Ok(i) or something similar of type T.

unit_ty

Returns the type of a zero-sized, one aligned-tuple.

Type Aliases

Address

An “address” is a location in memory. This corresponds to the actual location in the real program. We make it a mathematical integer, but of course it is bounded by the size of the address space.

Fields

LockId

ThreadId

The ID of a thread is an index into the machine’s threads list.