Crate move_stackless_bytecode
source · [−]Modules
This file contains an abstraction of concrete access paths, which are canonical names for a particular cell in memory. Some examples of concrete paths are:
The obvious approach to abstracting a set of concrete paths is using a set of abstract paths.
An access path trie represents a set of paths in a way that avoids redundant representations of
the same memory. Root nodes are access path roots and each internal node is an access path offset.
Each node is (optionally) associated with abstract value of a generic type T.
Data flow analysis computing borrow information for preparation of memory_instrumentation.
Transformation which injects data invariants into the bytecode.
Adapted from AbstractInterpreter for Bytecode, this module defines the data-flow analysis framework for stackless bytecode.
This module defines traits and representations of domains used in dataflow analysis.
Transformation which injects trace instructions which are used to visualize execution.
This escape analysis flags procedures that return a reference pointing inside of a struct type declared in the current module.
Provides a builder for FunctionData, including building expressions and rewriting
bytecode.
Instrument assert false; in strategic locations in the program such that if proved, signals
an inconsistency among the specifications.
Analysis which computes information needed in backends for monomorphization. This computes the distinct type instantiations in the model for structs and inlined functions.
Transformation which mutates code for mutation testing in various ways
The read/write set analysis is a compositional analysis that starts from the leaves of the call graph and analyzes each procedure once. The result is a summary of the abstract paths read/written by each procedure and the value(s) returned by the procedure.
Adapted from control_flow_graph for Bytecode, this module defines the control-flow graph on Stackless Bytecode used in analysis as part of Move prover.
Analysis which computes an annotation for each function on whether this function should be verified or inlined. It also calculates the set of global invariants that are applicable to each function as well as collect information on how these invariants should be handled (i.e., checked after bytecode, checked at function exit, or deferred to caller).
Analysis which computes an annotation for each function whether
Transformation which injects well-formed assumptions at top-level entry points of verified functions. These assumptions are both about parameters and any memory referred to by the code. For ghost memory, the transformation also assumes initial values if provided.
Functions
Print function targets for testing and debugging.