[][src]Crate solana_libra_bytecode_verifier

Verifies bytecode sanity.

Re-exports

pub use check_duplication::DuplicationChecker;
pub use code_unit_verifier::CodeUnitVerifier;
pub use resources::ResourceTransitiveChecker;
pub use signature::SignatureChecker;
pub use stack_usage_verifier::StackUsageVerifier;
pub use struct_defs::RecursiveStructDefChecker;
pub use unused_entries::UnusedEntryChecker;
pub use verifier::verify_main_signature;
pub use verifier::verify_module_dependencies;
pub use verifier::verify_script_dependencies;
pub use verifier::VerifiedModule;
pub use verifier::VerifiedScript;

Modules

absint
abstract_state

This module defines the abstract state for the type and memory safety analysis.

acquires_list_verifier

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) accesssed by BorrowGlobal, MoveFrom, and any transitive function calls The list of acquired resources (stored in FunctionDefinition's acquires_global_resources field) must have:

check_duplication

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:

code_unit_verifier

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.

control_flow_graph

This module defines the control-flow graph uses for bytecode verification.

instantiation_loops

This implements an algorithm that detects loops during the instantiation of generics.

nonce

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.

partition

This module defines the partition data structure used for tracking equality among nonces.

resources

This module implements a checker for verifying that a non-resource struct does not have resource fields inside it.

signature

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.

stack_usage_verifier

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.

struct_defs

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.

type_memory_safety

This module defines the transfer functions for verifying type and memory safety of a procedure body.

unused_entries
verifier

This module contains the public APIs supported by the bytecode verifier.