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_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-lang compiler to the one we are using here. TODO: move-lang 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, fname: MoveStringSymbol) -> 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_source_file_names(&self) -> Vec<String>

Return the source file names.

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 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_by_module( &self, module_id: ModuleId ) -> BTreeSet<GlobalId>

pub fn is_spec_fun_used( &self, module_id: ModuleId, spec_fun_id: SpecFunId ) -> bool

Returns true if a spec fun is used in specs.

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, 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, 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_struct_data( &self, module: &CompiledModule, def_idx: StructDefinitionIndex, name: Symbol, loc: Loc, spec: Spec ) -> StructData

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

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: &Identifier ) -> 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 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]) -> 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.

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.