Verifies bytecode sanity.
This module defines the abstract state for the type and memory safety analysis.
This module implements a checker for verifying properties about the acquires list on function
definitions. Function definitions must annotate the global resources (declared in that module)
This module implements a checker for verifying that each vector in a CompiledModule contains distinct values. Successful verification implies that an index in vector can be used to uniquely name the entry at that index. Additionally, the checker also verifies the following:
This module implements the checker for verifying correctness of function bodies. The overall verification is split between stack_usage_verifier.rs and abstract_interpreter.rs. CodeUnitVerifier simply orchestrates calls into these two files.
This module defines the control-flow graph uses for bytecode verification.
This implements an algorithm that detects loops during the instantiation of generics.
This module implements the Nonce type used for borrow checking in the abstract interpreter. A Nonce instance represents an arbitrary reference or access path. The integer inside a Nonce is meaningless; only equality and borrow relationships are meaningful.
This module defines the partition data structure used for tracking equality among nonces.
This module implements a checker for verifying that a non-resource struct does not have resource fields inside it.
This module implements a checker for verifying signature tokens used in types of function parameters, locals, and fields of structs are well-formed. References can only occur at the top-level in all tokens. Additionally, references cannot occur at all in field types.
This module implements a checker for verifying that basic blocks in the bytecode instruction sequence of a function use the evaluation stack in a balanced manner. Every basic block, except those that end in Ret (return to caller) opcode, must leave the stack height the same as at the beginning of the block. A basic block that ends in Ret opcode must increase the stack height by the number of values returned by the function as indicated in its signature. Additionally, the stack height must not dip below that at the beginning of the block for any basic block.
This module provides a checker for verifing that struct definitions in a module are not recursive. Since the module dependency graph is acylic by construction, applying this checker to each module in isolation guarantees that there is no structural recursion globally.
This module defines the transfer functions for verifying type and memory safety of a procedure body.
This module contains the public APIs supported by the bytecode verifier.