Struct move_model::model::GlobalEnv

pub struct GlobalEnv {
    pub module_data: Vec<ModuleData>,
    pub used_spec_funs: BTreeSet<QualifiedId<SpecFunId>>,
    /* private fields */
}

Global Environment

Global environment for a set of modules.

Fields

module_data: Vec<ModuleData>

List of loaded modules, in order they have been provided using add.

used_spec_funs: BTreeSet<QualifiedId<SpecFunId>>

A set containing spec functions which are called/used in specs. Note that these are represented without type instantiation because we assume the backend can handle generics in the expression language.

Implementations

impl GlobalEnv

pub fn new() -> Self

Creates a new environment.

pub fn display<'a, T>(&'a self, val: &'a T) -> EnvDisplay<'a, T>

Creates a display container for the given value. There must be an implementation of fmt::Display for an instance to work in formatting.

pub fn set_extension<T: Any>(&self, x: T)

Stores extension data in the environment. This can be arbitrary data which is indexed by type. Used by tools which want to store their own data in the environment, like a set of tool dependent options/flags. This can also be used to update extension data.

pub fn get_extension<T: Any>(&self) -> Option<Rc<T>>

Retrieves extension data from the environment. Use as in env.get_extension::<T>(). An Rc is returned because extension data is stored in a RefCell and we can’t use lifetimes (&'a T) to control borrowing.

pub fn update_extension<T: Any + Clone>(&self, f: impl FnOnce(&mut T))

Updates extension data. If they are no outstanding references to this extension it is updated in place, otherwise it will be cloned before the update.

pub fn has_extension<T: Any>(&self) -> bool

Checks whether there is an extension of type T.

pub fn clear_extension<T: Any>(&self) -> Option<Rc<T>>

Clear extension data from the environment (return the data if it is previously set). Use as in env.clear_extension::<T>() and an Rc<T> is returned if the extension data is previously stored in the environment.

pub fn new_global_id(&self) -> GlobalId

Create a new global id unique to this environment.

pub fn symbol_pool(&self) -> &SymbolPool

Returns a reference to the symbol pool owned by this environment.

pub fn add_source(
    &mut self,
    file_hash: FileHash,
    address_aliases: Rc<BTreeMap<Symbol, NumericalAddress>>,
    file_name: &str,
    source: &str,
    is_dep: bool
) -> FileId

Adds a source to this environment, returning a FileId for it.

pub fn get_target_modules(&self) -> Vec<ModuleEnv<'_>>

Find all target modules and return in a vector

pub fn add_documentation(
    &mut self,
    file_id: FileId,
    docs: BTreeMap<ByteIndex, String>
)

Adds documentation for a file.

pub fn add_diag(&self, diag: Diagnostic<FileId>)

Adds diagnostic to the environment.

pub fn error(&self, loc: &Loc, msg: &str)

Adds an error to this environment, without notes.

pub fn error_with_notes(&self, loc: &Loc, msg: &str, notes: Vec<String>)

Adds an error to this environment, with notes.

pub fn diag(&self, severity: Severity, loc: &Loc, msg: &str)

Adds a diagnostic of given severity to this environment.

pub fn diag_with_notes(
    &self,
    severity: Severity,
    loc: &Loc,
    msg: &str,
    notes: Vec<String>
)

Adds a diagnostic of given severity to this environment, with notes.

pub fn diag_with_labels(
    &self,
    severity: Severity,
    loc: &Loc,
    msg: &str,
    labels: Vec<(Loc, String)>
)

Adds a diagnostic of given severity to this environment, with secondary labels.

pub fn has_diag(&self, pattern: &str) -> bool

Checks whether any of the diagnostics contains string.

pub fn clear_diag(&self)

Clear all accumulated diagnosis.

pub fn unknown_loc(&self) -> Loc

Returns the unknown location.

pub fn unknown_move_ir_loc(&self) -> MoveIrLoc

Returns a Move IR version of the unknown location which is guaranteed to map to the regular unknown location via to_loc.

pub fn internal_loc(&self) -> Loc

Returns the internal location.

pub fn to_loc(&self, loc: &MoveIrLoc) -> Loc

Converts a Loc as used by the move-compiler compiler to the one we are using here. TODO: move-compiler should use FileId as well so we don’t need this here. There is already a todo in their code to remove the current use of &'static str for file names in Loc.

pub fn get_file_id(&self, fhash: FileHash) -> Option<FileId>

Returns the file id for a file name, if defined.

pub fn file_id_to_idx(&self, file_id: FileId) -> u16

Maps a FileId to an index which can be mapped back to a FileId.

pub fn file_idx_to_id(&self, file_idx: u16) -> FileId

Maps a an index which was obtained by file_id_to_idx back to a FileId.

pub fn get_file_and_location(&self, loc: &Loc) -> Option<(String, Location)>

Returns file name and line/column position for a location, if available.

pub fn get_location(&self, loc: &Loc) -> Option<Location>

Returns line/column position for a location, if available.

pub fn get_source(&self, loc: &Loc) -> Result<&str, Error>

Return the source text for the given location.

pub fn get_file(&self, file_id: FileId) -> &OsStr

Return the source file name for file_id

pub fn get_source_file_names(&self) -> Vec<String>

Return the source file names.

pub fn get_source_file_ids(&self) -> Vec<FileId>

Return the source file ids.

pub fn get_file_count(&self) -> usize

pub fn has_errors(&self) -> bool

Returns true if diagnostics have error severity or worse.

pub fn diag_count(&self, min_severity: Severity) -> usize

Returns the number of diagnostics.

pub fn error_count(&self) -> usize

Returns the number of errors.

pub fn has_warnings(&self) -> bool

Returns true if diagnostics have warning severity or worse.

pub fn report_diag<W: WriteColor>(&self, writer: &mut W, severity: Severity)

Writes accumulated diagnostics of given or higher severity.

pub fn report_diag_with_filter<W: WriteColor, F: Fn(&Diagnostic<FileId>) -> bool>(
    &self,
    writer: &mut W,
    filter: F
)

Writes accumulated diagnostics that pass through filter

pub fn add_global_invariant(&mut self, inv: GlobalInvariant)

Adds a global invariant to this environment.

pub fn get_global_invariant(&self, id: GlobalId) -> Option<&GlobalInvariant>

Get global invariant by id.

pub fn get_global_invariants_for_memory(
    &self,
    memory: &QualifiedInstId<StructId>
) -> BTreeSet<GlobalId>

Return the global invariants which refer to the given memory.

pub fn get_global_invariants_for_module(
    &self,
    module_id: ModuleId
) -> Vec<&GlobalInvariant>

pub fn get_global_invariants_by_module(
    &self,
    module_id: ModuleId
) -> BTreeSet<GlobalId>

pub fn is_spec_fun_used(&self, id: QualifiedId<SpecFunId>) -> bool

Returns true if a spec fun is used in specs.

pub fn is_spec_fun_recursive(&self, id: QualifiedId<SpecFunId>) -> bool

Determines whether the given spec fun is recursive.

pub fn is_wellknown_event_handle_type(&self, ty: &Type) -> bool

Returns true if the type represents the well-known event handle type.

pub fn add(
    &mut self,
    loc: Loc,
    attributes: Vec<Attribute>,
    module: CompiledModule,
    source_map: SourceMap,
    named_constants: BTreeMap<NamedConstantId, NamedConstantData>,
    struct_data: BTreeMap<StructId, StructData>,
    function_data: BTreeMap<FunId, FunctionData>,
    spec_vars: Vec<SpecVarDecl>,
    spec_funs: Vec<SpecFunDecl>,
    module_spec: Spec,
    spec_block_infos: Vec<SpecBlockInfo>
)

Adds a new module to the environment. StructData and FunctionData need to be provided in definition index order. See create_function_data and create_struct_data for how to create them.

pub fn create_named_constant_data(
    &self,
    name: Symbol,
    loc: Loc,
    typ: Type,
    value: Value
) -> NamedConstantData

Creates data for a named constant.

pub fn create_function_data(
    &self,
    module: &CompiledModule,
    def_idx: FunctionDefinitionIndex,
    name: Symbol,
    loc: Loc,
    attributes: Vec<Attribute>,
    arg_names: Vec<Symbol>,
    type_arg_names: Vec<Symbol>,
    spec: Spec
) -> FunctionData

Creates data for a function, adding any information not contained in bytecode. This is a helper for adding a new module to the environment.

pub fn create_move_struct_data(
    &self,
    module: &CompiledModule,
    def_idx: StructDefinitionIndex,
    name: Symbol,
    loc: Loc,
    attributes: Vec<Attribute>,
    spec: Spec
) -> StructData

Creates data for a struct declared in Move. Currently all information is contained in the byte code. This is a helper for adding a new module to the environment.

pub fn ghost_memory_name(&self, spec_var_name: Symbol) -> Symbol

Return the name of the ghost memory associated with spec var.

pub fn find_module(&self, name: &ModuleName) -> Option<ModuleEnv<'_>>

Finds a module by name and returns an environment for it.

pub fn find_module_by_name(&self, simple_name: Symbol) -> Option<ModuleEnv<'_>>

Finds a module by simple name and returns an environment for it. TODO: we may need to disallow this to support modules of the same simple name but with different addresses in one verification session.

pub fn find_module_by_language_storage_id(
    &self,
    id: &ModuleId
) -> Option<ModuleEnv<'_>>

Find a module by its bytecode format ID

pub fn find_function_by_language_storage_id_name(
    &self,
    id: &ModuleId,
    name: &IdentStr
) -> Option<FunctionEnv<'_>>

Find a function by its bytecode format name and ID

pub fn find_struct_by_tag(
    &self,
    tag: &StructTag
) -> Option<QualifiedId<StructId>>

Gets a StructEnv in this module by its StructTag

pub fn get_enclosing_module(&self, loc: &Loc) -> Option<ModuleEnv<'_>>

Return the module enclosing this location.

pub fn get_enclosing_function(&self, loc: &Loc) -> Option<FunctionEnv<'_>>

Returns the function enclosing this location.

pub fn get_enclosing_struct(&self, loc: &Loc) -> Option<StructEnv<'_>>

Returns the struct enclosing this location.

pub fn get_function(&self, fun: QualifiedId<FunId>) -> FunctionEnv<'_>

Return the FunctionEnv for fun

pub fn get_struct(&self, str: QualifiedId<StructId>) -> StructEnv<'_>

Return the StructEnv for str

pub fn get_module_count(&self) -> usize

pub fn get_module(&self, id: ModuleId) -> ModuleEnv<'_>

Gets a module by id.

pub fn get_struct_qid(&self, qid: QualifiedId<StructId>) -> StructEnv<'_>

Gets a struct by qualified id.

pub fn get_function_qid(&self, qid: QualifiedId<FunId>) -> FunctionEnv<'_>

Gets a function by qualified id.

pub fn get_modules(&self) -> impl Iterator<Item = ModuleEnv<'_>>

Returns an iterator for all modules in the environment.

pub fn get_bytecode_modules(&self) -> impl Iterator<Item = &CompiledModule>

Returns an iterator for all bytecode modules in the environment.

pub fn get_all_structs_with_conditions(&self) -> Vec<Type>

Returns all structs in all modules which carry invariants.

pub fn to_module_name(&self, storage_id: &ModuleId) -> ModuleName

Converts a storage module id into an AST module name.

pub fn get_doc(&self, loc: &Loc) -> &str

Get documentation associated with an item at Loc.

pub fn is_property_true(
    &self,
    properties: &PropertyBag,
    name: &str
) -> Option<bool>

Returns true if the boolean property is true.

pub fn get_num_property(
    &self,
    properties: &PropertyBag,
    name: &str
) -> Option<usize>

Returns the value of a number property.

pub fn get_struct_tag(
    &self,
    mid: ModuleId,
    sid: StructId,
    ts: &[Type]
) -> Option<StructTag>

Attempt to compute a struct tag for (mid, sid, ts). Returns Some if all types in ts are closed, None otherwise

pub fn get_struct_type(
    &self,
    mid: ModuleId,
    sid: StructId,
    ts: &[Type]
) -> Option<MType>

Attempt to compute a struct type for (mid, sid, ts).

pub fn get_node_loc(&self, node_id: NodeId) -> Loc

Gets the location of the given node.

pub fn get_node_type(&self, node_id: NodeId) -> Type

Gets the type of the given node.

pub fn get_node_type_opt(&self, node_id: NodeId) -> Option<Type>

Gets the type of the given node, if available.

pub fn index_to_node_id(&self, index: usize) -> Option<NodeId>

Converts an index into a node id.

pub fn next_free_node_number(&self) -> usize

Returns the next free node number.

pub fn new_node_id(&self) -> NodeId

Allocates a new node id.

pub fn new_node(&self, loc: Loc, ty: Type) -> NodeId

Allocates a new node id and assigns location and type to it.

pub fn update_node_type(&self, node_id: NodeId, ty: Type)

Updates type for the given node id. Must have been set before.

pub fn set_node_instantiation(&self, node_id: NodeId, instantiation: Vec<Type>)

Sets instantiation for the given node id. Must not have been set before.

pub fn update_node_instantiation(
    &self,
    node_id: NodeId,
    instantiation: Vec<Type>
)

Updates instantiation for the given node id. Must have been set before.

pub fn get_node_instantiation(&self, node_id: NodeId) -> Vec<Type>

Gets the type parameter instantiation associated with the given node.

pub fn get_node_instantiation_opt(&self, node_id: NodeId) -> Option<Vec<Type>>

Gets the type parameter instantiation associated with the given node, if it is available.

pub fn get_declared_function_count(&self) -> usize

Return the total number of declared functions in the modules of self

pub fn get_declared_struct_count(&self) -> usize

Return the total number of declared structs in the modules of self

pub fn get_move_bytecode_instruction_count(&self) -> usize

Return the total number of Move bytecode instructions (not stackless bytecode) in the modules of self

pub fn get_modules_with_specs_count(&self) -> usize

Return the total number of Move modules that contain specs

pub fn override_module_spec(&mut self, mid: ModuleId, spec: Spec)

Override the specification for a given module

pub fn override_function_spec(&mut self, fid: QualifiedId<FunId>, spec: Spec)

Override the specification for a given function

pub fn override_inline_spec(
    &mut self,
    fid: QualifiedId<FunId>,
    code_offset: CodeOffset,
    spec: Spec
)

Override the specification for a given code location

pub fn get_type_display_ctx(&self) -> TypeDisplayContext<'_>

Produce a TypeDisplayContext to print types within the scope of this env

pub fn get_stdlib_address(&self) -> BigUint

Returns the address where the standard lib is defined.

pub fn get_extlib_address(&self) -> BigUint

Returns the address where the extensions libs are defined.

Trait Implementations

impl Debug for GlobalEnv

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for GlobalEnv

fn default() -> Self

Returns the “default value” for a type.