diff --git a/language/move-model/src/ast.rs b/language/move-model/src/ast.rs index 12f687960b3c7..5bd199becb20c 100644 --- a/language/move-model/src/ast.rs +++ b/language/move-model/src/ast.rs @@ -18,7 +18,8 @@ use crate::{ exp_rewriter::ExpRewriterFunctions, model::{ EnvDisplay, FieldId, FunId, FunctionVisibility, GlobalEnv, GlobalId, Loc, ModuleId, NodeId, - QualifiedInstId, SchemaId, SpecFunId, StructId, TypeParameter, GHOST_MEMORY_PREFIX, + QualifiedId, QualifiedInstId, SchemaId, SpecFunId, StructId, TypeParameter, + GHOST_MEMORY_PREFIX, }, symbol::{Symbol, SymbolPool}, ty::{Type, TypeDisplayContext}, @@ -26,7 +27,7 @@ use crate::{ use internment::LocalIntern; use itertools::Itertools; use once_cell::sync::Lazy; -use std::{borrow::Borrow, fmt::Debug, hash::Hash, ops::Deref}; +use std::{borrow::Borrow, collections::HashSet, fmt::Debug, hash::Hash, ops::Deref}; // ================================================================================================= /// # Declarations @@ -755,6 +756,52 @@ impl ExpData { } None } + + /// Collect struct-related operations + pub fn struct_usage(&self, usage: &mut BTreeSet>) { + self.visit(&mut |e| { + if let ExpData::Call(_, oper, _) = e { + use Operation::*; + match oper { + Select(mid, sid, ..) | UpdateField(mid, sid, ..) | Pack(mid, sid) => { + usage.insert(mid.qualified(*sid)); + } + _ => {} + } + } + }); + } + + /// Collect field-related operations + pub fn field_usage(&self, usage: &mut BTreeSet<(QualifiedId, FieldId)>) { + self.visit(&mut |e| { + if let ExpData::Call(_, oper, _) = e { + use Operation::*; + match oper { + Select(mid, sid, fid) | UpdateField(mid, sid, fid) => { + usage.insert((mid.qualified(*sid), *fid)); + } + _ => {} + } + } + }); + } + + /// Collect vector-related operations + pub fn vector_usage(&self, usage: &mut HashSet) { + self.visit(&mut |e| { + if let ExpData::Call(_, oper, _) = e { + use Operation::*; + match oper { + Index | Slice | ConcatVec | EmptyVec | SingleVec | UpdateVec | IndexOfVec + | ContainsVec | InRangeVec | RangeVec => { + usage.insert(oper.clone()); + } + _ => {} + } + } + }); + } } struct ExpRewriter<'a> { diff --git a/language/move-model/src/model.rs b/language/move-model/src/model.rs index 5c35d3ac7d617..eab31f89ca3ae 100644 --- a/language/move-model/src/model.rs +++ b/language/move-model/src/model.rs @@ -787,6 +787,11 @@ impl GlobalEnv { self.source_files.source_slice(loc.file_id, loc.span) } + /// Return the source file name for `file_id` + pub fn get_file(&self, file_id: FileId) -> &OsStr { + self.source_files.name(file_id) + } + /// Return the source file names. pub fn get_source_file_names(&self) -> Vec { self.file_name_map @@ -835,12 +840,21 @@ impl GlobalEnv { /// Writes accumulated diagnostics of given or higher severity. pub fn report_diag(&self, writer: &mut W, severity: Severity) { + self.report_diag_with_filter(writer, |d| d.severity >= severity) + } + + /// Writes accumulated diagnostics that pass through `filter` + pub fn report_diag_with_filter) -> bool>( + &self, + writer: &mut W, + filter: F, + ) { let mut shown = BTreeSet::new(); for (diag, reported) in self .diags .borrow_mut() .iter_mut() - .filter(|(d, _)| d.severity >= severity) + .filter(|(d, _)| filter(d)) { if !*reported { // Avoid showing the same message twice. This can happen e.g. because of @@ -891,6 +905,14 @@ impl GlobalEnv { inv_ids } + pub fn get_global_invariants_for_module(&self, module_id: ModuleId) -> Vec<&GlobalInvariant> { + self.global_invariants + .iter() + .filter(|(_, inv)| inv.declaring_module == module_id) + .map(|(_, inv)| inv) + .collect() + } + pub fn get_global_invariants_by_module(&self, module_id: ModuleId) -> BTreeSet { self.global_invariants .iter() @@ -1431,6 +1453,46 @@ impl GlobalEnv { .get(&node_id) .and_then(|info| info.instantiation.clone()) } + + /// Return the total number of declared functions in the modules of `self` + pub fn get_declared_function_count(&self) -> usize { + let mut total = 0; + for m in &self.module_data { + total += m.module.function_defs().len(); + } + total + } + + /// Return the total number of declared structs in the modules of `self` + pub fn get_declared_struct_count(&self) -> usize { + let mut total = 0; + for m in &self.module_data { + total += m.module.struct_defs().len(); + } + total + } + + /// Return the total number of Move bytecode instructions (not stackless bytecode) in the modules of `self` + pub fn get_move_bytecode_instruction_count(&self) -> usize { + let mut total = 0; + for m in self.get_modules() { + for f in m.get_functions() { + total += f.get_bytecode().len(); + } + } + total + } + + /// Return the total number of Move modules that contain specs + pub fn get_modules_with_specs_count(&self) -> usize { + let mut total = 0; + for m in self.get_modules() { + if m.has_specs() { + total += 1 + } + } + total + } } impl Default for GlobalEnv { @@ -2072,6 +2134,32 @@ impl<'env> ModuleEnv<'env> { .disassemble() .expect("Failed to disassemble a verified module") } + + /// Return true if the module has any global, module, function, or struct specs + pub fn has_specs(&self) -> bool { + // module specs + if self.get_spec().has_conditions() { + return true; + } + // function specs + for f in self.get_functions() { + if f.get_spec().has_conditions() || !f.get_spec().on_impl.is_empty() { + return true; + } + } + // struct specs + for s in self.get_structs() { + if s.get_spec().has_conditions() { + return true; + } + } + // global specs + let global_invariants = self.env.get_global_invariants_by_module(self.get_id()); + if !global_invariants.is_empty() { + return true; + } + false + } } // ================================================================================================= diff --git a/language/move-prover/bytecode/src/escape_analysis.rs b/language/move-prover/bytecode/src/escape_analysis.rs new file mode 100644 index 0000000000000..1fd1f31ed6f51 --- /dev/null +++ b/language/move-prover/bytecode/src/escape_analysis.rs @@ -0,0 +1,404 @@ +// Copyright (c) The Diem Core Contributors +// SPDX-License-Identifier: Apache-2.0 + +//! This escape analysis flags procedures that return a reference pointing inside of a struct type +//! declared in the current module. + +use crate::{ + dataflow_analysis::{DataflowAnalysis, TransferFunctions}, + dataflow_domains::{AbstractDomain, JoinResult, MapDomain}, + function_target::FunctionData, + function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder}, + stackless_bytecode::{Bytecode, Operation}, + stackless_control_flow_graph::StacklessControlFlowGraph, +}; +use codespan::FileId; +use codespan_reporting::diagnostic::{Diagnostic, Label, Severity}; +use move_binary_format::file_format::CodeOffset; +use move_model::{ + ast::{Operation as ASTOperation, TempIndex}, + model::{FieldId, FunctionEnv, ModuleId, QualifiedId, StructId}, +}; +use std::{ + cell::RefCell, + cmp::Ordering, + collections::{BTreeMap, BTreeSet, HashSet}, +}; + +// ================================================================================================= +// Data Model + +#[derive(Debug, Clone, Copy, Eq, PartialEq)] +pub enum AbsValue { + NonRef, + OkRef, + InternalRef, +} + +impl AbsValue { + pub fn is_internal_ref(&self) -> bool { + matches!(self, Self::InternalRef) + } +} + +type EscapeAnalysisState = MapDomain; + +impl EscapeAnalysisState { + fn get_local_index(&self, i: &TempIndex) -> &AbsValue { + self.get(i) + .unwrap_or_else(|| panic!("Unbound local index {} in state {:?}", i, self)) + } + + fn assign(&mut self, lhs: TempIndex, rhs: &TempIndex) { + let rhs_value = *self.get_local_index(rhs); + self.insert(lhs, rhs_value); + } + + pub fn call(&mut self, rets: &[TempIndex], args: &[TempIndex], call_env: &FunctionEnv) { + let has_internal_ref_input = args + .iter() + .any(|arg_index| self.get(arg_index).unwrap().is_internal_ref()); + for (ret_index, ret_type) in call_env.get_return_types().iter().enumerate() { + let ret_value = if ret_type.is_reference() { + if has_internal_ref_input { + AbsValue::InternalRef + } else { + AbsValue::OkRef + } + } else { + AbsValue::NonRef + }; + self.insert(rets[ret_index], ret_value); + } + } +} + +// ================================================================================================= +// Joins + +impl PartialOrd for AbsValue { + fn partial_cmp(&self, other: &Self) -> Option { + if self == other { + return Some(Ordering::Equal); + } + match (self, other) { + (_, AbsValue::InternalRef) => Some(Ordering::Less), + _ => None, + } + } +} + +impl AbstractDomain for AbsValue { + fn join(&mut self, other: &Self) -> JoinResult { + if self == other { + return JoinResult::Unchanged; + } + // unequal; use top value + *self = AbsValue::InternalRef; + JoinResult::Changed + } +} + +// ================================================================================================= +// Transfer functions + +#[derive(PartialOrd, PartialEq, Eq, Ord)] +struct WarningId { + ret_index: usize, + offset: CodeOffset, +} + +struct SpecMemoryInfo { + /// Fields that occur in struct, module, or global specs. Leaked references to fields inside + /// this set will be flagged, leaked references to other fields will be allowed. + relevant_fields: BTreeSet<(QualifiedId, FieldId)>, + /// Structs that occur in struct, module, or global specs. Leaked references to fields inside + /// these structs may cause a spec like `invariant forall s: S: s == S { f: 10 }` to be false + relevant_structs: BTreeSet>, + /// Vector-related operations that occur in struct, module, or global specs. Leaked references + /// to vector contents will be allowed if this is empty + vector_operations: HashSet, +} + +struct EscapeAnalysis<'a> { + func_env: &'a FunctionEnv<'a>, + /// Warnings about escaped references to surface to the programmer + // Uses a map instead of a vec to avoid reporting multiple warnings + // at program locations in a loop during fixpoint iteration + escape_warnings: RefCell>>, + /// Information about the memory touched by the specs of the declaring module for this function + /// If the function's declaring module has no specs, this will be None + spec_memory: Option, +} + +impl EscapeAnalysis<'_> { + pub fn add_escaped_return_warning(&self, ret_index: usize, is_mut: bool, offset: CodeOffset) { + let message = format!( + "Leaked {} module-internal reference via return value {}", + if is_mut { "mutable" } else { "immutable" }, + ret_index + ); + let fun_loc = self.func_env.get_loc(); + let label = Label::primary(fun_loc.file_id(), fun_loc.span()); + let severity = if is_mut { + Severity::Error + } else { + Severity::Warning + }; + let warning_id = WarningId { ret_index, offset }; + self.escape_warnings.borrow_mut().insert( + warning_id, + Diagnostic::new(severity) + .with_message(message) + .with_labels(vec![label]), + ); + } + + /// Return true if `fld` is mentioned in a specification of the current module *or* if the + /// module has no specifications (i.e., we consider all fields to be relevant in that case) + pub fn specs_contain_field(&self, mid: &ModuleId, sid: &StructId, fld: &FieldId) -> bool { + if let Some(specs) = &self.spec_memory { + let qsid = mid.qualified(*sid); + specs.relevant_structs.contains(&qsid) || specs.relevant_fields.contains(&(qsid, *fld)) + } else { + true + } + } + + /// Return `true` if vector indexes are mentioned in a specification of the current module *or* + /// if the module has no specifications + pub fn specs_contain_vector_index(&self) -> bool { + use ASTOperation::*; + if let Some(specs) = &self.spec_memory { + for op in &specs.vector_operations { + match op { + // TODO: not sure about SingleVec, IndexOf, ContainsVec, InRangeVec, RangeVec + Index | Slice | UpdateVec | SingleVec | IndexOfVec | ContainsVec + | InRangeVec | RangeVec => return true, + _ => (), + } + } + false + } else { + true + } + } + + /// Returns `true` if vector lengths are mentioned in a specification of the current module *or* + /// if the module has no specifications + pub fn specs_contain_vector_length(&self) -> bool { + use ASTOperation::*; + if let Some(specs) = &self.spec_memory { + for op in &specs.vector_operations { + match op { + // TODO: does every indexing-related operation belong here? + Len | SingleVec | EmptyVec => return true, + _ => (), + } + } + false + } else { + true + } + } +} + +impl<'a> TransferFunctions for EscapeAnalysis<'a> { + type State = EscapeAnalysisState; + const BACKWARD: bool = false; + + fn execute(&self, state: &mut Self::State, instr: &Bytecode, offset: CodeOffset) { + use Bytecode::*; + use Operation::*; + + match instr { + Call(_, rets, oper, args, _) => match oper { + BorrowField(mid, sid, _type_params, offset) => { + let struct_env = self.func_env.module_env.get_struct(*sid); + let field_env = struct_env.get_field_by_offset(*offset); + let field_id = field_env.get_id(); + + let to_propagate = match state.get_local_index(&args[0]) { + AbsValue::OkRef => { + // TODO: or if the field is a vector and specs contain a length + if self.specs_contain_field(mid, sid, &field_id) + || (field_env.get_type().is_vector() + && self.specs_contain_vector_length()) + { + AbsValue::InternalRef + } else { + AbsValue::OkRef + } + } + AbsValue::InternalRef => AbsValue::InternalRef, + AbsValue::NonRef => panic!("Invariant violation: expected reference"), + }; + state.insert(rets[0], to_propagate); + } + BorrowGlobal(_mid, _sid, _types) => { + state.insert(rets[0], AbsValue::InternalRef); + } + ReadRef | MoveFrom(..) | Exists(..) | Pack(..) | Eq | Neq | CastU8 | CastU64 + | CastU128 | Not | Add | Sub | Mul | Div | Mod | BitOr | BitAnd | Xor | Shl + | Shr | Lt | Gt | Le | Ge | Or | And => { + // These operations all produce a non-reference value + state.insert(rets[0], AbsValue::NonRef); + } + BorrowLoc => { + state.insert(rets[0], AbsValue::OkRef); + } + Function(mid, fid, _) => { + let callee_fun_env = self + .func_env + .module_env + .env + .get_function(mid.qualified(*fid)); + if callee_fun_env.is_native() { + // check if this is a modeled native + match ( + callee_fun_env.module_env.get_identifier().as_str(), + callee_fun_env.get_identifier().as_str(), + ) { + ("Vector", "borrow_mut") | ("Vector", "borrow") => { + let vec_arg = 0; + let to_propagate = match state.get_local_index(&args[vec_arg]) { + AbsValue::OkRef => { + if self.specs_contain_vector_index() { + AbsValue::InternalRef + } else { + AbsValue::OkRef + } + } + AbsValue::InternalRef => AbsValue::InternalRef, + AbsValue::NonRef => { + panic!("Invariant violation: expected reference") + } + }; + state.insert(rets[0], to_propagate); + } + _ => { + // unmodeled native, treat the same as ordinary call + state.call(rets, args, &callee_fun_env) + } + } + } else { + state.call(rets, args, &callee_fun_env) + } + } + Unpack(..) => { + for ret_index in rets { + state.insert(*ret_index, AbsValue::NonRef); + } + } + FreezeRef => state.assign(rets[0], &args[0]), + WriteRef | MoveTo(..) => { + // these operations do not assign any locals + } + Destroy => { + state.remove(&args[0]); + } + oper => panic!("unsupported oper {:?}", oper), + }, + Load(_, lhs, _) => { + state.insert(*lhs, AbsValue::NonRef); + } + Assign(_, lhs, rhs, _) => state.assign(*lhs, rhs), + Ret(_, rets) => { + let ret_types = self.func_env.get_return_types(); + for (ret_index, ret) in rets.iter().enumerate() { + if state.get_local_index(ret).is_internal_ref() { + self.add_escaped_return_warning( + ret_index, + ret_types[ret_index].is_mutable_reference(), + offset, + ); + } + } + } + Abort(..) | SaveMem(..) | Prop(..) | SaveSpecVar(..) | Branch(..) | Jump(..) + | Label(..) | Nop(..) => { + // these operations do not assign any locals + } + } + } +} + +impl<'a> DataflowAnalysis for EscapeAnalysis<'a> {} +pub struct EscapeAnalysisProcessor(); +impl EscapeAnalysisProcessor { + pub fn new() -> Box { + Box::new(EscapeAnalysisProcessor()) + } +} + +impl FunctionTargetProcessor for EscapeAnalysisProcessor { + fn process( + &self, + _targets: &mut FunctionTargetsHolder, + func_env: &FunctionEnv<'_>, + data: FunctionData, + ) -> FunctionData { + if func_env.is_native() { + return data; + } + let mut initial_state = EscapeAnalysisState::default(); + // initialize_formals + for (param_index, param_type) in func_env.get_parameter_types().iter().enumerate() { + let param_val = if param_type.is_reference() { + AbsValue::OkRef + } else { + AbsValue::NonRef + }; + initial_state.insert(param_index, param_val); + } + + // compute set of fields and vector ops used in all struct specs + // Note: global and module specs are not relevant here because + // it is not possible to leak a reference to a global outside of + // the module that declares it. + let mut has_specs = false; + let menv = &func_env.module_env; + let mut relevant_fields = BTreeSet::new(); + let mut relevant_structs = BTreeSet::new(); + let mut vector_operations = HashSet::new(); + for struct_env in menv.get_structs() { + let struct_spec = struct_env.get_spec(); + if !struct_spec.conditions.is_empty() { + relevant_structs.insert(struct_env.get_qualified_id()); + } + for condition in &struct_spec.conditions { + for exp in condition.all_exps() { + exp.field_usage(&mut relevant_fields); + exp.struct_usage(&mut relevant_structs); + exp.vector_usage(&mut vector_operations); + has_specs = true + } + } + } + + let cfg = StacklessControlFlowGraph::new_forward(&data.code); + let analysis = EscapeAnalysis { + func_env, + escape_warnings: RefCell::new(BTreeMap::new()), + spec_memory: if has_specs { + Some(SpecMemoryInfo { + relevant_fields, + relevant_structs, + vector_operations, + }) + } else { + None + }, + }; + analysis.analyze_function(initial_state, &data.code, &cfg); + let env = func_env.module_env.env; + for (_, warning) in analysis.escape_warnings.into_inner() { + env.add_diag(warning) + } + data + } + + fn name(&self) -> String { + "escape_analysis".to_string() + } +} diff --git a/language/move-prover/bytecode/src/lib.rs b/language/move-prover/bytecode/src/lib.rs index 6303fd2432fca..20b9833695a77 100644 --- a/language/move-prover/bytecode/src/lib.rs +++ b/language/move-prover/bytecode/src/lib.rs @@ -17,6 +17,7 @@ pub mod dataflow_analysis; pub mod dataflow_domains; pub mod debug_instrumentation; pub mod eliminate_imm_refs; +pub mod escape_analysis; pub mod function_data_builder; pub mod function_target; pub mod function_target_pipeline; diff --git a/language/move-prover/bytecode/tests/escape_analysis/global_spec_relevance.exp b/language/move-prover/bytecode/tests/escape_analysis/global_spec_relevance.exp new file mode 100644 index 0000000000000..51197d2b52581 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/global_spec_relevance.exp @@ -0,0 +1,152 @@ +============ initial translation from Move ================ + +[variant baseline] +public fun GlobalSpecRelevance::create($t0|i: u64, $t1|j: u64): GlobalSpecRelevance::Nonzero { + var $t2: u64 + var $t3: u64 + var $t4: GlobalSpecRelevance::Nonzero + 0: $t2 := copy($t0) + 1: $t3 := copy($t1) + 2: $t4 := pack GlobalSpecRelevance::Nonzero($t2, $t3) + 3: return $t4 +} + + +[variant baseline] +public fun GlobalSpecRelevance::leak_i_bad($t0|n: &mut GlobalSpecRelevance::Nonzero): &mut u64 { + var $t1: &mut GlobalSpecRelevance::Nonzero + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.i($t1) + 2: return $t2 +} + + +[variant baseline] +public fun GlobalSpecRelevance::leak_j_ok($t0|n: &mut GlobalSpecRelevance::Nonzero): &mut u64 { + var $t1: &mut GlobalSpecRelevance::Nonzero + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.j($t1) + 2: return $t2 +} + + +[variant baseline] +public fun GlobalSpecRelevance::publish($t0|account: &signer, $t1|n: GlobalSpecRelevance::Nonzero) { + var $t2|tmp#$2: bool + var $t3|tmp#$3: u64 + var $t4: &GlobalSpecRelevance::Nonzero + var $t5: &u64 + var $t6: u64 + var $t7: u64 + var $t8: bool + var $t9: bool + var $t10: &signer + var $t11: u64 + var $t12: &signer + var $t13: GlobalSpecRelevance::Nonzero + 0: $t4 := borrow_local($t1) + 1: $t5 := borrow_field.i($t4) + 2: $t6 := read_ref($t5) + 3: $t7 := 0 + 4: $t8 := >($t6, $t7) + 5: $t2 := $t8 + 6: $t9 := move($t2) + 7: if ($t9) goto 13 else goto 8 + 8: label L1 + 9: $t10 := move($t0) + 10: destroy($t10) + 11: $t11 := 0 + 12: abort($t11) + 13: label L0 + 14: $t12 := move($t0) + 15: $t13 := move($t1) + 16: move_to($t13, $t12) + 17: return () +} + +============ after pipeline `escape_analysis` ================ + +[variant baseline] +public fun GlobalSpecRelevance::create($t0|i: u64, $t1|j: u64): GlobalSpecRelevance::Nonzero { + var $t2: u64 + var $t3: u64 + var $t4: GlobalSpecRelevance::Nonzero + 0: $t2 := copy($t0) + 1: $t3 := copy($t1) + 2: $t4 := pack GlobalSpecRelevance::Nonzero($t2, $t3) + 3: return $t4 +} + + +[variant baseline] +public fun GlobalSpecRelevance::leak_i_bad($t0|n: &mut GlobalSpecRelevance::Nonzero): &mut u64 { + var $t1: &mut GlobalSpecRelevance::Nonzero + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.i($t1) + 2: return $t2 +} + + +[variant baseline] +public fun GlobalSpecRelevance::leak_j_ok($t0|n: &mut GlobalSpecRelevance::Nonzero): &mut u64 { + var $t1: &mut GlobalSpecRelevance::Nonzero + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.j($t1) + 2: return $t2 +} + + +[variant baseline] +public fun GlobalSpecRelevance::publish($t0|account: &signer, $t1|n: GlobalSpecRelevance::Nonzero) { + var $t2|tmp#$2: bool + var $t3|tmp#$3: u64 + var $t4: &GlobalSpecRelevance::Nonzero + var $t5: &u64 + var $t6: u64 + var $t7: u64 + var $t8: bool + var $t9: bool + var $t10: &signer + var $t11: u64 + var $t12: &signer + var $t13: GlobalSpecRelevance::Nonzero + 0: $t4 := borrow_local($t1) + 1: $t5 := borrow_field.i($t4) + 2: $t6 := read_ref($t5) + 3: $t7 := 0 + 4: $t8 := >($t6, $t7) + 5: $t2 := $t8 + 6: $t9 := move($t2) + 7: if ($t9) goto 13 else goto 8 + 8: label L1 + 9: $t10 := move($t0) + 10: destroy($t10) + 11: $t11 := 0 + 12: abort($t11) + 13: label L0 + 14: $t12 := move($t0) + 15: $t13 := move($t1) + 16: move_to($t13, $t12) + 17: return () +} + +============ Diagnostics ================ +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/global_spec_relevance.move:12:5 + │ +12 │ ╭ public fun leak_j_ok(n: &mut Nonzero): &mut u64 { +13 │ │ &mut n.j +14 │ │ } + │ ╰─────^ + +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/global_spec_relevance.move:7:5 + │ +7 │ ╭ public fun leak_i_bad(n: &mut Nonzero): &mut u64 { +8 │ │ &mut n.i +9 │ │ } + │ ╰─────^ diff --git a/language/move-prover/bytecode/tests/escape_analysis/global_spec_relevance.move b/language/move-prover/bytecode/tests/escape_analysis/global_spec_relevance.move new file mode 100644 index 0000000000000..d659028477819 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/global_spec_relevance.move @@ -0,0 +1,24 @@ +module 0x1::GlobalSpecRelevance { + invariant forall a: address where exists(a): global(a).i > 0; + + struct Nonzero has key { i: u64, j: u64 } + + // Can't leak i because it's involved in a spec + public fun leak_i_bad(n: &mut Nonzero): &mut u64 { + &mut n.i + } + + // Leaking j is ok because specs say nothing about it + public fun leak_j_ok(n: &mut Nonzero): &mut u64 { + &mut n.j + } + + public fun create(i: u64, j: u64): Nonzero { + Nonzero { i, j } + } + + public fun publish(account: &signer, n: Nonzero) { + assert(n.i > 0, 0); + move_to(account, n) + } +} diff --git a/language/move-prover/bytecode/tests/escape_analysis/global_struct_eq.exp b/language/move-prover/bytecode/tests/escape_analysis/global_struct_eq.exp new file mode 100644 index 0000000000000..1de77f9909222 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/global_struct_eq.exp @@ -0,0 +1,72 @@ +============ initial translation from Move ================ + +[variant baseline] +public fun StructEq::leak_f($t0|s: &mut StructEq::S): &mut u64 { + var $t1: &mut StructEq::S + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.f($t1) + 2: return $t2 +} + + +[variant baseline] +public fun StructEq::new(): StructEq::S { + var $t0: u64 + var $t1: StructEq::S + 0: $t0 := 10 + 1: $t1 := pack StructEq::S($t0) + 2: return $t1 +} + + +[variant baseline] +public fun StructEq::publish($t0|account: &signer, $t1|s: StructEq::S) { + var $t2: &signer + var $t3: StructEq::S + 0: $t2 := move($t0) + 1: $t3 := move($t1) + 2: move_to($t3, $t2) + 3: return () +} + +============ after pipeline `escape_analysis` ================ + +[variant baseline] +public fun StructEq::leak_f($t0|s: &mut StructEq::S): &mut u64 { + var $t1: &mut StructEq::S + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.f($t1) + 2: return $t2 +} + + +[variant baseline] +public fun StructEq::new(): StructEq::S { + var $t0: u64 + var $t1: StructEq::S + 0: $t0 := 10 + 1: $t1 := pack StructEq::S($t0) + 2: return $t1 +} + + +[variant baseline] +public fun StructEq::publish($t0|account: &signer, $t1|s: StructEq::S) { + var $t2: &signer + var $t3: StructEq::S + 0: $t2 := move($t0) + 1: $t3 := move($t1) + 2: move_to($t3, $t2) + 3: return () +} + +============ Diagnostics ================ +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/global_struct_eq.move:16:5 + │ +16 │ ╭ public fun leak_f(s: &mut S): &mut u64 { +17 │ │ &mut s.f +18 │ │ } + │ ╰─────^ diff --git a/language/move-prover/bytecode/tests/escape_analysis/global_struct_eq.move b/language/move-prover/bytecode/tests/escape_analysis/global_struct_eq.move new file mode 100644 index 0000000000000..21d036988930b --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/global_struct_eq.move @@ -0,0 +1,19 @@ +module 0x1::StructEq { + + struct S has key { f: u64 } + + invariant forall a: address: global(a).f == 10; + + public fun new(): S { + S { f: 10 } + } + + public fun publish(account: &signer, s: S) { + move_to(account, s) + } + + // should complain + public fun leak_f(s: &mut S): &mut u64 { + &mut s.f + } +} diff --git a/language/move-prover/bytecode/tests/escape_analysis/return_internal_refs.exp b/language/move-prover/bytecode/tests/escape_analysis/return_internal_refs.exp new file mode 100644 index 0000000000000..a7b88be892f87 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/return_internal_refs.exp @@ -0,0 +1,328 @@ +============ initial translation from Move ================ + +[variant baseline] +fun LeakInternalRefs::leak_immut_ref($t0|s: &LeakInternalRefs::S): &u64 { + var $t1: &LeakInternalRefs::S + var $t2: &u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.f($t1) + 2: return $t2 +} + + +[variant baseline] +fun LeakInternalRefs::leak_in_branch($t0|b: bool, $t1|x: &mut u64, $t2|s: &mut LeakInternalRefs::S): &mut u64 { + var $t3|tmp#$3: &mut u64 + var $t4: bool + var $t5: &mut LeakInternalRefs::S + var $t6: &mut u64 + var $t7: &mut u64 + var $t8: &mut LeakInternalRefs::S + var $t9: &mut u64 + var $t10: &mut u64 + 0: $t4 := copy($t0) + 1: if ($t4) goto 4 else goto 2 + 2: label L1 + 3: goto 10 + 4: label L0 + 5: $t5 := move($t2) + 6: destroy($t5) + 7: $t6 := move($t1) + 8: $t3 := $t6 + 9: goto 17 + 10: label L2 + 11: $t7 := move($t1) + 12: destroy($t7) + 13: $t8 := move($t2) + 14: $t9 := borrow_field.f($t8) + 15: $t3 := $t9 + 16: goto 17 + 17: label L3 + 18: $t10 := move($t3) + 19: return $t10 +} + + +[variant baseline] +fun LeakInternalRefs::leak_in_loop($t0|x: &mut u64, $t1|s: &mut LeakInternalRefs::S): &mut u64 { + var $t2|i: u64 + var $t3: u64 + var $t4: u64 + var $t5: u64 + var $t6: bool + var $t7: u64 + var $t8: u64 + var $t9: bool + var $t10: &mut u64 + var $t11: &mut LeakInternalRefs::S + var $t12: &mut u64 + var $t13: u64 + var $t14: u64 + var $t15: u64 + var $t16: &mut LeakInternalRefs::S + var $t17: &mut u64 + 0: $t3 := 0 + 1: $t2 := $t3 + 2: goto 3 + 3: label L6 + 4: $t4 := copy($t2) + 5: $t5 := 10 + 6: $t6 := <($t4, $t5) + 7: if ($t6) goto 10 else goto 8 + 8: label L1 + 9: goto 29 + 10: label L0 + 11: $t7 := copy($t2) + 12: $t8 := 7 + 13: $t9 := ==($t7, $t8) + 14: if ($t9) goto 17 else goto 15 + 15: label L4 + 16: goto 23 + 17: label L3 + 18: $t10 := move($t0) + 19: destroy($t10) + 20: $t11 := move($t1) + 21: $t12 := borrow_field.f($t11) + 22: return $t12 + 23: label L5 + 24: $t13 := copy($t2) + 25: $t14 := 1 + 26: $t15 := +($t13, $t14) + 27: $t2 := $t15 + 28: goto 3 + 29: label L2 + 30: $t16 := move($t1) + 31: destroy($t16) + 32: $t17 := move($t0) + 33: return $t17 +} + + +[variant baseline] +fun LeakInternalRefs::leak_mut_ref($t0|s: &mut LeakInternalRefs::S): &mut u64 { + var $t1: &mut LeakInternalRefs::S + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.f($t1) + 2: return $t2 +} + + +[variant baseline] +fun LeakInternalRefs::leak_two_refs($t0|s: &mut LeakInternalRefs::S): (&mut u64, &mut u64) { + var $t1: &mut LeakInternalRefs::S + var $t2: &mut u64 + var $t3: &mut LeakInternalRefs::S + var $t4: &mut u64 + 0: $t1 := copy($t0) + 1: $t2 := borrow_field.f($t1) + 2: $t3 := move($t0) + 3: $t4 := borrow_field.g($t3) + 4: return ($t2, $t4) +} + + +[variant baseline] +fun LeakInternalRefs::read_but_dont_leak($t0|x: &mut u64, $t1|s: &mut LeakInternalRefs::S): &mut u64 { + var $t2: &mut LeakInternalRefs::S + var $t3: &mut u64 + var $t4: &mut u64 + 0: $t2 := move($t1) + 1: $t3 := borrow_field.f($t2) + 2: destroy($t3) + 3: $t4 := move($t0) + 4: return $t4 +} + +============ after pipeline `escape_analysis` ================ + +[variant baseline] +fun LeakInternalRefs::leak_immut_ref($t0|s: &LeakInternalRefs::S): &u64 { + var $t1: &LeakInternalRefs::S + var $t2: &u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.f($t1) + 2: return $t2 +} + + +[variant baseline] +fun LeakInternalRefs::leak_in_branch($t0|b: bool, $t1|x: &mut u64, $t2|s: &mut LeakInternalRefs::S): &mut u64 { + var $t3|tmp#$3: &mut u64 + var $t4: bool + var $t5: &mut LeakInternalRefs::S + var $t6: &mut u64 + var $t7: &mut u64 + var $t8: &mut LeakInternalRefs::S + var $t9: &mut u64 + var $t10: &mut u64 + 0: $t4 := copy($t0) + 1: if ($t4) goto 4 else goto 2 + 2: label L1 + 3: goto 10 + 4: label L0 + 5: $t5 := move($t2) + 6: destroy($t5) + 7: $t6 := move($t1) + 8: $t3 := $t6 + 9: goto 17 + 10: label L2 + 11: $t7 := move($t1) + 12: destroy($t7) + 13: $t8 := move($t2) + 14: $t9 := borrow_field.f($t8) + 15: $t3 := $t9 + 16: goto 17 + 17: label L3 + 18: $t10 := move($t3) + 19: return $t10 +} + + +[variant baseline] +fun LeakInternalRefs::leak_in_loop($t0|x: &mut u64, $t1|s: &mut LeakInternalRefs::S): &mut u64 { + var $t2|i: u64 + var $t3: u64 + var $t4: u64 + var $t5: u64 + var $t6: bool + var $t7: u64 + var $t8: u64 + var $t9: bool + var $t10: &mut u64 + var $t11: &mut LeakInternalRefs::S + var $t12: &mut u64 + var $t13: u64 + var $t14: u64 + var $t15: u64 + var $t16: &mut LeakInternalRefs::S + var $t17: &mut u64 + 0: $t3 := 0 + 1: $t2 := $t3 + 2: goto 3 + 3: label L6 + 4: $t4 := copy($t2) + 5: $t5 := 10 + 6: $t6 := <($t4, $t5) + 7: if ($t6) goto 10 else goto 8 + 8: label L1 + 9: goto 29 + 10: label L0 + 11: $t7 := copy($t2) + 12: $t8 := 7 + 13: $t9 := ==($t7, $t8) + 14: if ($t9) goto 17 else goto 15 + 15: label L4 + 16: goto 23 + 17: label L3 + 18: $t10 := move($t0) + 19: destroy($t10) + 20: $t11 := move($t1) + 21: $t12 := borrow_field.f($t11) + 22: return $t12 + 23: label L5 + 24: $t13 := copy($t2) + 25: $t14 := 1 + 26: $t15 := +($t13, $t14) + 27: $t2 := $t15 + 28: goto 3 + 29: label L2 + 30: $t16 := move($t1) + 31: destroy($t16) + 32: $t17 := move($t0) + 33: return $t17 +} + + +[variant baseline] +fun LeakInternalRefs::leak_mut_ref($t0|s: &mut LeakInternalRefs::S): &mut u64 { + var $t1: &mut LeakInternalRefs::S + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.f($t1) + 2: return $t2 +} + + +[variant baseline] +fun LeakInternalRefs::leak_two_refs($t0|s: &mut LeakInternalRefs::S): (&mut u64, &mut u64) { + var $t1: &mut LeakInternalRefs::S + var $t2: &mut u64 + var $t3: &mut LeakInternalRefs::S + var $t4: &mut u64 + 0: $t1 := copy($t0) + 1: $t2 := borrow_field.f($t1) + 2: $t3 := move($t0) + 3: $t4 := borrow_field.g($t3) + 4: return ($t2, $t4) +} + + +[variant baseline] +fun LeakInternalRefs::read_but_dont_leak($t0|x: &mut u64, $t1|s: &mut LeakInternalRefs::S): &mut u64 { + var $t2: &mut LeakInternalRefs::S + var $t3: &mut u64 + var $t4: &mut u64 + 0: $t2 := move($t1) + 1: $t3 := borrow_field.f($t2) + 2: destroy($t3) + 3: $t4 := move($t0) + 4: return $t4 +} + +============ Diagnostics ================ +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/return_internal_refs.move:13:5 + │ +13 │ ╭ fun leak_two_refs(s: &mut S): (&mut u64, &mut u64) { +14 │ │ (&mut s.f, &mut s.g) +15 │ │ } + │ ╰─────^ + +error: Leaked mutable module-internal reference via return value 1 + ┌─ tests/escape_analysis/return_internal_refs.move:13:5 + │ +13 │ ╭ fun leak_two_refs(s: &mut S): (&mut u64, &mut u64) { +14 │ │ (&mut s.f, &mut s.g) +15 │ │ } + │ ╰─────^ + +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/return_internal_refs.move:5:5 + │ +5 │ ╭ fun leak_mut_ref(s: &mut S): &mut u64 { +6 │ │ &mut s.f +7 │ │ } + │ ╰─────^ + +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/return_internal_refs.move:25:5 + │ +25 │ ╭ fun leak_in_loop(x: &mut u64, s: &mut S): &mut u64 { +26 │ │ let i = 0; +27 │ │ while (i < 10) { +28 │ │ if (i == 7) { + · │ +33 │ │ x +34 │ │ } + │ ╰─────^ + +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/return_internal_refs.move:17:5 + │ +17 │ ╭ fun leak_in_branch(b: bool, x: &mut u64, s: &mut S): &mut u64 { +18 │ │ if (b) { +19 │ │ x +20 │ │ } else { +21 │ │ &mut s.f +22 │ │ } +23 │ │ } + │ ╰─────^ + +warning: Leaked immutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/return_internal_refs.move:9:5 + │ + 9 │ ╭ fun leak_immut_ref(s: &S): &u64 { +10 │ │ &s.f +11 │ │ } + │ ╰─────^ diff --git a/language/move-prover/bytecode/tests/escape_analysis/return_internal_refs.move b/language/move-prover/bytecode/tests/escape_analysis/return_internal_refs.move new file mode 100644 index 0000000000000..9d5d2663d9850 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/return_internal_refs.move @@ -0,0 +1,41 @@ +module 0x1::LeakInternalRefs { + + struct S { f: u64, g: u64 } + + fun leak_mut_ref(s: &mut S): &mut u64 { + &mut s.f + } + + fun leak_immut_ref(s: &S): &u64 { + &s.f + } + + fun leak_two_refs(s: &mut S): (&mut u64, &mut u64) { + (&mut s.f, &mut s.g) + } + + fun leak_in_branch(b: bool, x: &mut u64, s: &mut S): &mut u64 { + if (b) { + x + } else { + &mut s.f + } + } + + fun leak_in_loop(x: &mut u64, s: &mut S): &mut u64 { + let i = 0; + while (i < 10) { + if (i == 7) { + return &mut s.f + }; + i = i + 1; + }; + x + } + + fun read_but_dont_leak(x: &mut u64, s: &mut S): &mut u64 { + let _ = &mut s.f; + x + } + +} diff --git a/language/move-prover/bytecode/tests/escape_analysis/return_refs_into_vec.exp b/language/move-prover/bytecode/tests/escape_analysis/return_refs_into_vec.exp new file mode 100644 index 0000000000000..987c1648d590e --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/return_refs_into_vec.exp @@ -0,0 +1,220 @@ +============ initial translation from Move ================ + +[variant baseline] +public intrinsic fun Vector::contains<#0>($t0|v: &vector<#0>, $t1|e: �): bool; + + +[variant baseline] +public intrinsic fun Vector::index_of<#0>($t0|v: &vector<#0>, $t1|e: �): (bool, u64); + + +[variant baseline] +public intrinsic fun Vector::append<#0>($t0|lhs: &mut vector<#0>, $t1|other: vector<#0>); + + +[variant baseline] +public native fun Vector::borrow<#0>($t0|v: &vector<#0>, $t1|i: u64): � + + +[variant baseline] +public native fun Vector::borrow_mut<#0>($t0|v: &mut vector<#0>, $t1|i: u64): &mut #0; + + +[variant baseline] +public native fun Vector::destroy_empty<#0>($t0|v: vector<#0>); + + +[variant baseline] +public native fun Vector::empty<#0>(): vector<#0>; + + +[variant baseline] +public intrinsic fun Vector::is_empty<#0>($t0|v: &vector<#0>): bool; + + +[variant baseline] +public native fun Vector::length<#0>($t0|v: &vector<#0>): u64; + + +[variant baseline] +public native fun Vector::pop_back<#0>($t0|v: &mut vector<#0>): #0; + + +[variant baseline] +public native fun Vector::push_back<#0>($t0|v: &mut vector<#0>, $t1|e: #0); + + +[variant baseline] +public intrinsic fun Vector::remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0; + + +[variant baseline] +public intrinsic fun Vector::reverse<#0>($t0|v: &mut vector<#0>); + + +[variant baseline] +public fun Vector::singleton<#0>($t0|e: #0): vector<#0> { + var $t1|v: vector<#0> + var $t2: vector<#0> + var $t3: &mut vector<#0> + var $t4: #0 + var $t5: vector<#0> + 0: $t2 := Vector::empty<#0>() + 1: $t1 := $t2 + 2: $t3 := borrow_local($t1) + 3: $t4 := move($t0) + 4: Vector::push_back<#0>($t3, $t4) + 5: $t5 := move($t1) + 6: return $t5 +} + + +[variant baseline] +public native fun Vector::swap<#0>($t0|v: &mut vector<#0>, $t1|i: u64, $t2|j: u64); + + +[variant baseline] +public intrinsic fun Vector::swap_remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0; + + +[variant baseline] +fun ReturnRefsIntoVec::return_vec_index_immut($t0|v: &vector): &u64 { + var $t1: &vector + var $t2: u64 + var $t3: &u64 + 0: $t1 := move($t0) + 1: $t2 := 0 + 2: $t3 := Vector::borrow($t1, $t2) + 3: return $t3 +} + + +[variant baseline] +fun ReturnRefsIntoVec::return_vec_index_mut($t0|v: &mut vector): &mut u64 { + var $t1: &mut vector + var $t2: u64 + var $t3: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := 0 + 2: $t3 := Vector::borrow_mut($t1, $t2) + 3: return $t3 +} + +============ after pipeline `escape_analysis` ================ + +[variant baseline] +public intrinsic fun Vector::contains<#0>($t0|v: &vector<#0>, $t1|e: �): bool; + + +[variant baseline] +public intrinsic fun Vector::index_of<#0>($t0|v: &vector<#0>, $t1|e: �): (bool, u64); + + +[variant baseline] +public intrinsic fun Vector::append<#0>($t0|lhs: &mut vector<#0>, $t1|other: vector<#0>); + + +[variant baseline] +public native fun Vector::borrow<#0>($t0|v: &vector<#0>, $t1|i: u64): � + + +[variant baseline] +public native fun Vector::borrow_mut<#0>($t0|v: &mut vector<#0>, $t1|i: u64): &mut #0; + + +[variant baseline] +public native fun Vector::destroy_empty<#0>($t0|v: vector<#0>); + + +[variant baseline] +public native fun Vector::empty<#0>(): vector<#0>; + + +[variant baseline] +public intrinsic fun Vector::is_empty<#0>($t0|v: &vector<#0>): bool; + + +[variant baseline] +public native fun Vector::length<#0>($t0|v: &vector<#0>): u64; + + +[variant baseline] +public native fun Vector::pop_back<#0>($t0|v: &mut vector<#0>): #0; + + +[variant baseline] +public native fun Vector::push_back<#0>($t0|v: &mut vector<#0>, $t1|e: #0); + + +[variant baseline] +public intrinsic fun Vector::remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0; + + +[variant baseline] +public intrinsic fun Vector::reverse<#0>($t0|v: &mut vector<#0>); + + +[variant baseline] +public fun Vector::singleton<#0>($t0|e: #0): vector<#0> { + var $t1|v: vector<#0> + var $t2: vector<#0> + var $t3: &mut vector<#0> + var $t4: #0 + var $t5: vector<#0> + 0: $t2 := Vector::empty<#0>() + 1: $t1 := $t2 + 2: $t3 := borrow_local($t1) + 3: $t4 := move($t0) + 4: Vector::push_back<#0>($t3, $t4) + 5: $t5 := move($t1) + 6: return $t5 +} + + +[variant baseline] +public native fun Vector::swap<#0>($t0|v: &mut vector<#0>, $t1|i: u64, $t2|j: u64); + + +[variant baseline] +public intrinsic fun Vector::swap_remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0; + + +[variant baseline] +fun ReturnRefsIntoVec::return_vec_index_immut($t0|v: &vector): &u64 { + var $t1: &vector + var $t2: u64 + var $t3: &u64 + 0: $t1 := move($t0) + 1: $t2 := 0 + 2: $t3 := Vector::borrow($t1, $t2) + 3: return $t3 +} + + +[variant baseline] +fun ReturnRefsIntoVec::return_vec_index_mut($t0|v: &mut vector): &mut u64 { + var $t1: &mut vector + var $t2: u64 + var $t3: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := 0 + 2: $t3 := Vector::borrow_mut($t1, $t2) + 3: return $t3 +} + +============ Diagnostics ================ +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/return_refs_into_vec.move:12:5 + │ +12 │ ╭ fun return_vec_index_mut(v: &mut vector): &mut u64 { +13 │ │ Vector::borrow_mut(v, 0) +14 │ │ } + │ ╰─────^ + +warning: Leaked immutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/return_refs_into_vec.move:7:5 + │ +7 │ ╭ fun return_vec_index_immut(v: &vector): &u64 { +8 │ │ Vector::borrow(v, 0) +9 │ │ } + │ ╰─────^ diff --git a/language/move-prover/bytecode/tests/escape_analysis/return_refs_into_vec.move b/language/move-prover/bytecode/tests/escape_analysis/return_refs_into_vec.move new file mode 100644 index 0000000000000..cc2c949480b09 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/return_refs_into_vec.move @@ -0,0 +1,16 @@ +// dep: ../../move-stdlib/sources/Vector.move + +module 0x1::ReturnRefsIntoVec { + use Std::Vector; + + // should not complain + fun return_vec_index_immut(v: &vector): &u64 { + Vector::borrow(v, 0) + } + + // should complain + fun return_vec_index_mut(v: &mut vector): &mut u64 { + Vector::borrow_mut(v, 0) + } + +} diff --git a/language/move-prover/bytecode/tests/escape_analysis/return_refs_safe.exp b/language/move-prover/bytecode/tests/escape_analysis/return_refs_safe.exp new file mode 100644 index 0000000000000..40ecdb6f023a2 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/return_refs_safe.exp @@ -0,0 +1,85 @@ +============ initial translation from Move ================ + +[variant baseline] +fun ReturnRefsSafe::return_freeze($t0|x: &mut u64): &u64 { + var $t1: &mut u64 + var $t2: &u64 + 0: $t1 := move($t0) + 1: $t2 := freeze_ref($t1) + 2: return $t2 +} + + +[variant baseline] +fun ReturnRefsSafe::return_immut($t0|x: &u64): &u64 { + var $t1: &u64 + 0: $t1 := move($t0) + 1: return $t1 +} + + +[variant baseline] +fun ReturnRefsSafe::return_mut($t0|x: &mut u64): &mut u64 { + var $t1: &mut u64 + 0: $t1 := move($t0) + 1: return $t1 +} + + +[variant baseline] +fun ReturnRefsSafe::return_vec_immut($t0|v: &vector): &vector { + var $t1: &vector + 0: $t1 := move($t0) + 1: return $t1 +} + + +[variant baseline] +fun ReturnRefsSafe::return_vec_mut($t0|v: &mut vector): &mut vector { + var $t1: &mut vector + 0: $t1 := move($t0) + 1: return $t1 +} + +============ after pipeline `escape_analysis` ================ + +[variant baseline] +fun ReturnRefsSafe::return_freeze($t0|x: &mut u64): &u64 { + var $t1: &mut u64 + var $t2: &u64 + 0: $t1 := move($t0) + 1: $t2 := freeze_ref($t1) + 2: return $t2 +} + + +[variant baseline] +fun ReturnRefsSafe::return_immut($t0|x: &u64): &u64 { + var $t1: &u64 + 0: $t1 := move($t0) + 1: return $t1 +} + + +[variant baseline] +fun ReturnRefsSafe::return_mut($t0|x: &mut u64): &mut u64 { + var $t1: &mut u64 + 0: $t1 := move($t0) + 1: return $t1 +} + + +[variant baseline] +fun ReturnRefsSafe::return_vec_immut($t0|v: &vector): &vector { + var $t1: &vector + 0: $t1 := move($t0) + 1: return $t1 +} + + +[variant baseline] +fun ReturnRefsSafe::return_vec_mut($t0|v: &mut vector): &mut vector { + var $t1: &mut vector + 0: $t1 := move($t0) + 1: return $t1 +} diff --git a/language/move-prover/bytecode/tests/escape_analysis/return_refs_safe.move b/language/move-prover/bytecode/tests/escape_analysis/return_refs_safe.move new file mode 100644 index 0000000000000..0398e90191b02 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/return_refs_safe.move @@ -0,0 +1,25 @@ +module 0x1::ReturnRefsSafe { + // Make sure the analysis doesn't complain about returning + // refs to formals or their children + + fun return_immut(x: &u64): &u64 { + x + } + + fun return_mut(x: &mut u64): &mut u64 { + x + } + + fun return_freeze(x: &mut u64): &u64 { + x + } + + fun return_vec_immut(v: &vector): &vector { + v + } + + fun return_vec_mut(v: &mut vector): &mut vector { + v + } + +} diff --git a/language/move-prover/bytecode/tests/escape_analysis/struct_eq.exp b/language/move-prover/bytecode/tests/escape_analysis/struct_eq.exp new file mode 100644 index 0000000000000..0115142a0f655 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/struct_eq.exp @@ -0,0 +1,50 @@ +============ initial translation from Move ================ + +[variant baseline] +public fun StructEq::leak_f($t0|s: &mut StructEq::S): &mut u64 { + var $t1: &mut StructEq::S + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.f($t1) + 2: return $t2 +} + + +[variant baseline] +public fun StructEq::new(): StructEq::S { + var $t0: u64 + var $t1: StructEq::S + 0: $t0 := 10 + 1: $t1 := pack StructEq::S($t0) + 2: return $t1 +} + +============ after pipeline `escape_analysis` ================ + +[variant baseline] +public fun StructEq::leak_f($t0|s: &mut StructEq::S): &mut u64 { + var $t1: &mut StructEq::S + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.f($t1) + 2: return $t2 +} + + +[variant baseline] +public fun StructEq::new(): StructEq::S { + var $t0: u64 + var $t1: StructEq::S + 0: $t0 := 10 + 1: $t1 := pack StructEq::S($t0) + 2: return $t1 +} + +============ Diagnostics ================ +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/struct_eq.move:12:5 + │ +12 │ ╭ public fun leak_f(s: &mut S): &mut u64 { +13 │ │ &mut s.f +14 │ │ } + │ ╰─────^ diff --git a/language/move-prover/bytecode/tests/escape_analysis/struct_eq.move b/language/move-prover/bytecode/tests/escape_analysis/struct_eq.move new file mode 100644 index 0000000000000..33b9ff48059ee --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/struct_eq.move @@ -0,0 +1,15 @@ +module 0x1::StructEq { + + struct S { f: u64 } + + invariant forall s: S: s == S { f: 10 }; + + public fun new(): S { + S { f: 10 } + } + + // should complain + public fun leak_f(s: &mut S): &mut u64 { + &mut s.f + } +} diff --git a/language/move-prover/bytecode/tests/escape_analysis/struct_spec_relevance.exp b/language/move-prover/bytecode/tests/escape_analysis/struct_spec_relevance.exp new file mode 100644 index 0000000000000..a5cb4f0c73f09 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/struct_spec_relevance.exp @@ -0,0 +1,116 @@ +============ initial translation from Move ================ + +[variant baseline] +public fun StructSpecRelevance::create($t0|i: u64, $t1|j: u64): StructSpecRelevance::Nonzero { + var $t2|tmp#$2: bool + var $t3|tmp#$3: u64 + var $t4: u64 + var $t5: u64 + var $t6: bool + var $t7: bool + var $t8: u64 + var $t9: u64 + var $t10: u64 + var $t11: StructSpecRelevance::Nonzero + 0: $t4 := copy($t0) + 1: $t5 := 0 + 2: $t6 := >($t4, $t5) + 3: $t2 := $t6 + 4: $t7 := move($t2) + 5: if ($t7) goto 9 else goto 6 + 6: label L1 + 7: $t8 := 0 + 8: abort($t8) + 9: label L0 + 10: $t9 := copy($t0) + 11: $t10 := copy($t1) + 12: $t11 := pack StructSpecRelevance::Nonzero($t9, $t10) + 13: return $t11 +} + + +[variant baseline] +public fun StructSpecRelevance::leak_i_bad($t0|n: &mut StructSpecRelevance::Nonzero): &mut u64 { + var $t1: &mut StructSpecRelevance::Nonzero + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.i($t1) + 2: return $t2 +} + + +[variant baseline] +public fun StructSpecRelevance::leak_j_ok($t0|n: &mut StructSpecRelevance::Nonzero): &mut u64 { + var $t1: &mut StructSpecRelevance::Nonzero + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.j($t1) + 2: return $t2 +} + +============ after pipeline `escape_analysis` ================ + +[variant baseline] +public fun StructSpecRelevance::create($t0|i: u64, $t1|j: u64): StructSpecRelevance::Nonzero { + var $t2|tmp#$2: bool + var $t3|tmp#$3: u64 + var $t4: u64 + var $t5: u64 + var $t6: bool + var $t7: bool + var $t8: u64 + var $t9: u64 + var $t10: u64 + var $t11: StructSpecRelevance::Nonzero + 0: $t4 := copy($t0) + 1: $t5 := 0 + 2: $t6 := >($t4, $t5) + 3: $t2 := $t6 + 4: $t7 := move($t2) + 5: if ($t7) goto 9 else goto 6 + 6: label L1 + 7: $t8 := 0 + 8: abort($t8) + 9: label L0 + 10: $t9 := copy($t0) + 11: $t10 := copy($t1) + 12: $t11 := pack StructSpecRelevance::Nonzero($t9, $t10) + 13: return $t11 +} + + +[variant baseline] +public fun StructSpecRelevance::leak_i_bad($t0|n: &mut StructSpecRelevance::Nonzero): &mut u64 { + var $t1: &mut StructSpecRelevance::Nonzero + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.i($t1) + 2: return $t2 +} + + +[variant baseline] +public fun StructSpecRelevance::leak_j_ok($t0|n: &mut StructSpecRelevance::Nonzero): &mut u64 { + var $t1: &mut StructSpecRelevance::Nonzero + var $t2: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.j($t1) + 2: return $t2 +} + +============ Diagnostics ================ +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/struct_spec_relevance.move:14:5 + │ +14 │ ╭ public fun leak_j_ok(n: &mut Nonzero): &mut u64 { +15 │ │ &mut n.j +16 │ │ } + │ ╰─────^ + +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/struct_spec_relevance.move:9:5 + │ + 9 │ ╭ public fun leak_i_bad(n: &mut Nonzero): &mut u64 { +10 │ │ &mut n.i +11 │ │ } + │ ╰─────^ diff --git a/language/move-prover/bytecode/tests/escape_analysis/struct_spec_relevance.move b/language/move-prover/bytecode/tests/escape_analysis/struct_spec_relevance.move new file mode 100644 index 0000000000000..ff6b9f98dcbfb --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/struct_spec_relevance.move @@ -0,0 +1,22 @@ +module 0x1::StructSpecRelevance { + struct Nonzero { i: u64, j: u64 } + + spec Nonzero { + invariant i > 0; + } + + // Can't leak i because it's involved in a spec + public fun leak_i_bad(n: &mut Nonzero): &mut u64 { + &mut n.i + } + + // Leaking j is ok because specs say nothing about it + public fun leak_j_ok(n: &mut Nonzero): &mut u64 { + &mut n.j + } + + public fun create(i: u64, j: u64): Nonzero { + assert(i > 0, 0); + Nonzero { i, j } + } +} diff --git a/language/move-prover/bytecode/tests/escape_analysis/vec_eq.exp b/language/move-prover/bytecode/tests/escape_analysis/vec_eq.exp new file mode 100644 index 0000000000000..d77293be0720d --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/vec_eq.exp @@ -0,0 +1,244 @@ +============ initial translation from Move ================ + +[variant baseline] +public intrinsic fun Vector::contains<#0>($t0|v: &vector<#0>, $t1|e: �): bool; + + +[variant baseline] +public intrinsic fun Vector::index_of<#0>($t0|v: &vector<#0>, $t1|e: �): (bool, u64); + + +[variant baseline] +public intrinsic fun Vector::append<#0>($t0|lhs: &mut vector<#0>, $t1|other: vector<#0>); + + +[variant baseline] +public native fun Vector::borrow<#0>($t0|v: &vector<#0>, $t1|i: u64): � + + +[variant baseline] +public native fun Vector::borrow_mut<#0>($t0|v: &mut vector<#0>, $t1|i: u64): &mut #0; + + +[variant baseline] +public native fun Vector::destroy_empty<#0>($t0|v: vector<#0>); + + +[variant baseline] +public native fun Vector::empty<#0>(): vector<#0>; + + +[variant baseline] +public intrinsic fun Vector::is_empty<#0>($t0|v: &vector<#0>): bool; + + +[variant baseline] +public native fun Vector::length<#0>($t0|v: &vector<#0>): u64; + + +[variant baseline] +public native fun Vector::pop_back<#0>($t0|v: &mut vector<#0>): #0; + + +[variant baseline] +public native fun Vector::push_back<#0>($t0|v: &mut vector<#0>, $t1|e: #0); + + +[variant baseline] +public intrinsic fun Vector::remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0; + + +[variant baseline] +public intrinsic fun Vector::reverse<#0>($t0|v: &mut vector<#0>); + + +[variant baseline] +public fun Vector::singleton<#0>($t0|e: #0): vector<#0> { + var $t1|v: vector<#0> + var $t2: vector<#0> + var $t3: &mut vector<#0> + var $t4: #0 + var $t5: vector<#0> + 0: $t2 := Vector::empty<#0>() + 1: $t1 := $t2 + 2: $t3 := borrow_local($t1) + 3: $t4 := move($t0) + 4: Vector::push_back<#0>($t3, $t4) + 5: $t5 := move($t1) + 6: return $t5 +} + + +[variant baseline] +public native fun Vector::swap<#0>($t0|v: &mut vector<#0>, $t1|i: u64, $t2|j: u64); + + +[variant baseline] +public intrinsic fun Vector::swap_remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0; + + +[variant baseline] +public fun VecEq::leak_index_into_v($t0|g: &mut VecEq::G): &mut u64 { + var $t1: &mut VecEq::G + var $t2: &mut vector + var $t3: u64 + var $t4: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.v($t1) + 2: $t3 := 0 + 3: $t4 := Vector::borrow_mut($t2, $t3) + 4: return $t4 +} + + +[variant baseline] +public fun VecEq::leak_v($t0|g: &mut VecEq::G): &mut vector { + var $t1: &mut VecEq::G + var $t2: &mut vector + 0: $t1 := move($t0) + 1: $t2 := borrow_field.v($t1) + 2: return $t2 +} + + +[variant baseline] +public fun VecEq::new(): VecEq::G { + var $t0: u64 + var $t1: vector + var $t2: VecEq::G + 0: $t0 := 10 + 1: $t1 := Vector::singleton($t0) + 2: $t2 := pack VecEq::G($t1) + 3: return $t2 +} + +============ after pipeline `escape_analysis` ================ + +[variant baseline] +public intrinsic fun Vector::contains<#0>($t0|v: &vector<#0>, $t1|e: �): bool; + + +[variant baseline] +public intrinsic fun Vector::index_of<#0>($t0|v: &vector<#0>, $t1|e: �): (bool, u64); + + +[variant baseline] +public intrinsic fun Vector::append<#0>($t0|lhs: &mut vector<#0>, $t1|other: vector<#0>); + + +[variant baseline] +public native fun Vector::borrow<#0>($t0|v: &vector<#0>, $t1|i: u64): � + + +[variant baseline] +public native fun Vector::borrow_mut<#0>($t0|v: &mut vector<#0>, $t1|i: u64): &mut #0; + + +[variant baseline] +public native fun Vector::destroy_empty<#0>($t0|v: vector<#0>); + + +[variant baseline] +public native fun Vector::empty<#0>(): vector<#0>; + + +[variant baseline] +public intrinsic fun Vector::is_empty<#0>($t0|v: &vector<#0>): bool; + + +[variant baseline] +public native fun Vector::length<#0>($t0|v: &vector<#0>): u64; + + +[variant baseline] +public native fun Vector::pop_back<#0>($t0|v: &mut vector<#0>): #0; + + +[variant baseline] +public native fun Vector::push_back<#0>($t0|v: &mut vector<#0>, $t1|e: #0); + + +[variant baseline] +public intrinsic fun Vector::remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0; + + +[variant baseline] +public intrinsic fun Vector::reverse<#0>($t0|v: &mut vector<#0>); + + +[variant baseline] +public fun Vector::singleton<#0>($t0|e: #0): vector<#0> { + var $t1|v: vector<#0> + var $t2: vector<#0> + var $t3: &mut vector<#0> + var $t4: #0 + var $t5: vector<#0> + 0: $t2 := Vector::empty<#0>() + 1: $t1 := $t2 + 2: $t3 := borrow_local($t1) + 3: $t4 := move($t0) + 4: Vector::push_back<#0>($t3, $t4) + 5: $t5 := move($t1) + 6: return $t5 +} + + +[variant baseline] +public native fun Vector::swap<#0>($t0|v: &mut vector<#0>, $t1|i: u64, $t2|j: u64); + + +[variant baseline] +public intrinsic fun Vector::swap_remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0; + + +[variant baseline] +public fun VecEq::leak_index_into_v($t0|g: &mut VecEq::G): &mut u64 { + var $t1: &mut VecEq::G + var $t2: &mut vector + var $t3: u64 + var $t4: &mut u64 + 0: $t1 := move($t0) + 1: $t2 := borrow_field.v($t1) + 2: $t3 := 0 + 3: $t4 := Vector::borrow_mut($t2, $t3) + 4: return $t4 +} + + +[variant baseline] +public fun VecEq::leak_v($t0|g: &mut VecEq::G): &mut vector { + var $t1: &mut VecEq::G + var $t2: &mut vector + 0: $t1 := move($t0) + 1: $t2 := borrow_field.v($t1) + 2: return $t2 +} + + +[variant baseline] +public fun VecEq::new(): VecEq::G { + var $t0: u64 + var $t1: vector + var $t2: VecEq::G + 0: $t0 := 10 + 1: $t1 := Vector::singleton($t0) + 2: $t2 := pack VecEq::G($t1) + 3: return $t2 +} + +============ Diagnostics ================ +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/vec_eq.move:17:5 + │ +17 │ ╭ public fun leak_v(g: &mut G): &mut vector { +18 │ │ &mut g.v +19 │ │ } + │ ╰─────^ + +error: Leaked mutable module-internal reference via return value 0 + ┌─ tests/escape_analysis/vec_eq.move:22:5 + │ +22 │ ╭ public fun leak_index_into_v(g: &mut G): &mut u64 { +23 │ │ Vector::borrow_mut(&mut g.v, 0) +24 │ │ } + │ ╰─────^ diff --git a/language/move-prover/bytecode/tests/escape_analysis/vec_eq.move b/language/move-prover/bytecode/tests/escape_analysis/vec_eq.move new file mode 100644 index 0000000000000..d4a040a0fce44 --- /dev/null +++ b/language/move-prover/bytecode/tests/escape_analysis/vec_eq.move @@ -0,0 +1,25 @@ +// dep: ../../move-stdlib/sources/Vector.move + +module 0x1::VecEq { + use Std::Vector; + + struct G { v: vector } + + spec G { + invariant v == vec(10); + } + + public fun new(): G { + G { v: Vector::singleton(10) } + } + + // should complain + public fun leak_v(g: &mut G): &mut vector { + &mut g.v + } + + // should also complain + public fun leak_index_into_v(g: &mut G): &mut u64 { + Vector::borrow_mut(&mut g.v, 0) + } +} diff --git a/language/move-prover/bytecode/tests/testsuite.rs b/language/move-prover/bytecode/tests/testsuite.rs index 42bd080240f04..3f52e4f8e530f 100644 --- a/language/move-prover/bytecode/tests/testsuite.rs +++ b/language/move-prover/bytecode/tests/testsuite.rs @@ -7,6 +7,7 @@ use bytecode::{ clean_and_optimize::CleanAndOptimizeProcessor, data_invariant_instrumentation::DataInvariantInstrumentationProcessor, eliminate_imm_refs::EliminateImmRefsProcessor, + escape_analysis::EscapeAnalysisProcessor, function_target_pipeline::{ FunctionTargetPipeline, FunctionTargetsHolder, ProcessorResultDisplay, }, @@ -80,6 +81,11 @@ fn get_tested_transformation_pipeline( pipeline.add_processor(BorrowAnalysisProcessor::new()); Ok(Some(pipeline)) } + "escape_analysis" => { + let mut pipeline = FunctionTargetPipeline::default(); + pipeline.add_processor(Box::new(EscapeAnalysisProcessor {})); + Ok(Some(pipeline)) + } "memory_instr" => { let mut pipeline = FunctionTargetPipeline::default(); pipeline.add_processor(EliminateImmRefsProcessor::new()); @@ -259,7 +265,13 @@ fn test_runner(path: &Path) -> datatest_stable::Result<()> { } .to_string(); } - + // add Warning and Error diagnostics to output + let mut error_writer = Buffer::no_color(); + if env.has_errors() || env.has_warnings() { + env.report_diag(&mut error_writer, Severity::Warning); + text += "============ Diagnostics ================\n"; + text += &String::from_utf8_lossy(&error_writer.into_inner()).to_string(); + } text }; let baseline_path = path.with_extension(EXP_EXT); diff --git a/language/move-prover/src/cli.rs b/language/move-prover/src/cli.rs index 06b2c2a999dd5..4d2bfe60207de 100644 --- a/language/move-prover/src/cli.rs +++ b/language/move-prover/src/cli.rs @@ -55,6 +55,8 @@ pub struct Options { pub run_errmapgen: bool, /// Whether to run the read write set analysis instead of the prover pub run_read_write_set: bool, + /// Whether to run the internal reference escape analysis instead of the prover + pub run_escape: bool, /// The paths to the Move sources. pub move_sources: Vec, /// The paths to any dependencies for the Move sources. Those will not be verified but @@ -89,6 +91,7 @@ impl Default for Options { run_abigen: false, run_errmapgen: false, run_read_write_set: false, + run_escape: false, verbosity_level: LevelFilter::Info, move_sources: vec![], move_deps: vec![], @@ -301,6 +304,11 @@ impl Options { .long("packedtypesgen") .help("runs the packed types generator instead of the prover.") ) + .arg( + Arg::with_name("escape") + .long("escape") + .help("runs the escape analysis instead of the prover.") + ) .arg( Arg::with_name("read-write-set") .long("read-write-set") @@ -649,6 +657,9 @@ impl Options { if matches.is_present("read-write-set") { options.run_read_write_set = true; } + if matches.is_present("escape") { + options.run_escape = true; + } if matches.is_present("trace") { options.prover.auto_trace_level = AutoTraceLevel::VerifiedFunction; } diff --git a/language/move-prover/src/lib.rs b/language/move-prover/src/lib.rs index 9efe40812008f..ca565db6a4e91 100644 --- a/language/move-prover/src/lib.rs +++ b/language/move-prover/src/lib.rs @@ -10,11 +10,15 @@ use boogie_backend::{ add_prelude, boogie_wrapper::BoogieWrapper, bytecode_translator::BoogieTranslator, }; use bytecode::{ + escape_analysis::EscapeAnalysisProcessor, function_target_pipeline::{FunctionTargetPipeline, FunctionTargetsHolder}, pipeline_factory, read_write_set_analysis::{self, ReadWriteSetProcessor}, }; -use codespan_reporting::term::termcolor::{ColorChoice, StandardStream, WriteColor}; +use codespan_reporting::{ + diagnostic::Severity, + term::termcolor::{Buffer, ColorChoice, StandardStream, WriteColor}, +}; use docgen::Docgen; use errmapgen::ErrmapGen; #[allow(unused_imports)] @@ -97,6 +101,13 @@ pub fn run_move_prover_with_model( Ok(()) }; } + // Same for escape analysis + if options.run_escape { + return { + run_escape(env, &options, now); + Ok(()) + }; + } // Check correct backend versions. options.backend.check_tool_versions()?; @@ -136,6 +147,13 @@ pub fn run_move_prover_with_model( gen_duration.as_secs_f64(), verify_duration.as_secs_f64() ); + info!( + "Total prover time in ms: {}", + build_duration.as_millis() + + trafo_duration.as_millis() + + gen_duration.as_millis() + + verify_duration.as_millis() + ); check_errors( env, &options, @@ -323,3 +341,41 @@ fn run_read_write_set(env: &GlobalEnv, options: &Options, now: Instant) { let end = now.elapsed(); info!("{:.3}s analyzing", (end - start).as_secs_f64()); } + +fn run_escape(env: &GlobalEnv, options: &Options, now: Instant) { + let mut targets = FunctionTargetsHolder::default(); + for module_env in env.get_modules() { + for func_env in module_env.get_functions() { + targets.add_target(&func_env) + } + } + println!( + "Analyzing {} modules, {} declared functions, {} declared structs, {} total bytecodes", + env.get_module_count(), + env.get_declared_function_count(), + env.get_declared_struct_count(), + env.get_move_bytecode_instruction_count(), + ); + let mut pipeline = FunctionTargetPipeline::default(); + pipeline.add_processor(EscapeAnalysisProcessor::new()); + + let start = now.elapsed(); + pipeline.run(env, &mut targets); + let end = now.elapsed(); + + // print escaped internal refs flagged by analysis. do not report errors in dependencies + let mut error_writer = Buffer::no_color(); + env.report_diag_with_filter(&mut error_writer, |d| { + let fname = env.get_file(d.labels[0].file_id).to_str().unwrap(); + options.move_sources.iter().any(|d| { + let p = Path::new(d); + if p.is_file() { + d == fname + } else { + Path::new(fname).parent().unwrap() == p + } + }) && d.severity >= Severity::Error + }); + println!("{}", String::from_utf8_lossy(&error_writer.into_inner())); + info!("in ms, analysis took {:.3}", (end - start).as_millis()) +}