diff --git a/crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs b/crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs index 6f9486f425..4d87e21748 100644 --- a/crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs +++ b/crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs @@ -388,6 +388,30 @@ impl<'env> BoogieTranslator<'env> { } // Add given type declarations for type parameters. + // Collect type param indices that appear in UID's dynamic field entries. + // These cannot be declared as datatypes containing UID (would create a cycle). + let uid_df_type_params: BTreeSet = env + .uid_qid() + .map(|uid_qid| { + let uid_type = Type::Datatype(uid_qid.module_id, uid_qid.id, vec![]); + let df_info = dynamic_field_analysis::get_env_info(env); + let mut params = BTreeSet::new(); + for (name, value) in df_info.dynamic_field_names_values(&uid_type) { + name.visit(&mut |t| { + if let Type::TypeParameter(idx) = t { + params.insert(*idx); + } + }); + value.visit(&mut |t| { + if let Type::TypeParameter(idx) = t { + params.insert(*idx); + } + }); + } + params + }) + .unwrap_or_default(); + emitln!(writer, "\n\n// Given Types for Type Parameters\n"); for idx in &mono_info.type_params { let param_type = boogie_type_param(env, *idx); @@ -397,9 +421,10 @@ impl<'env> BoogieTranslator<'env> { .find_datatype_by_tag(&StructTag::from_str("0x2::object::UID").unwrap()) .and_then(|uid_qid| mono_info.structs.get(&uid_qid)) .is_some(); - if is_uid { + if is_uid && !uid_df_type_params.contains(idx) { // Sui-specific to allow "using" unresolved type params as Sui objects in Boogie - // (otherwise Boogie compilation errors may occur) + // (otherwise Boogie compilation errors may occur). + // Skip if this type param appears in UID's dynamic fields to avoid circularity. emitln!(writer, "datatype {} {{", param_type); emitln!(writer, " {}($id: $2_object_UID)", param_type); emitln!(writer, "}"); @@ -467,6 +492,7 @@ impl<'env> BoogieTranslator<'env> { self.env, self.targets, &struct_env.get_qualified_id(), + type_inst, ), } .translate(); @@ -491,6 +517,7 @@ impl<'env> BoogieTranslator<'env> { self.env, self.targets, &enum_env.get_qualified_id(), + type_inst, ), } .translate(); @@ -1436,10 +1463,16 @@ impl<'env> StructTranslator<'env> { ) }); let dynamic_fields = dynamic_field_names_values.iter().map(|(name, value)| { + let value_type = boogie_type(env, value); + let value_type = if value_type.contains(' ') { + format!("({})", value_type) + } else { + value_type + }; format!( "{}: (Table int {})", boogie_dynamic_field_sel(self.parent.env, name, value), - boogie_type(env, value), + value_type, ) }); let all_fields = fields.chain(dynamic_fields).join(", "); @@ -1486,12 +1519,18 @@ impl<'env> StructTranslator<'env> { ); } for (pos, (name, value)) in dynamic_field_names_values.iter().enumerate() { + let value_type = boogie_type(env, value); + let value_type = if value_type.contains(' ') { + format!("({})", value_type) + } else { + value_type + }; self.emit_function( &format!( "{}(s: {}, x: (Table int {})): {}", boogie_dynamic_field_update(struct_env, self.type_inst, name, value), struct_name, - boogie_type(env, value), + value_type, struct_name ), || { diff --git a/crates/move-prover-boogie-backend/src/boogie_backend/lib.rs b/crates/move-prover-boogie-backend/src/boogie_backend/lib.rs index 407a2101d8..b91898bd44 100644 --- a/crates/move-prover-boogie-backend/src/boogie_backend/lib.rs +++ b/crates/move-prover-boogie-backend/src/boogie_backend/lib.rs @@ -230,12 +230,12 @@ pub fn add_prelude( .collect_vec(); let mut table_instances = vec![]; if let Some(table_qid) = env.table_qid() { - if mono_info.is_used_datatype(env, targets, &table_qid) { + if mono_info.is_used_datatype(env, targets, &table_qid, &[]) { table_instances.push(TableImpl::table(env, options, &mono_info, table_qid, false)); } } if let Some(object_table_qid) = env.object_table_qid() { - if mono_info.is_used_datatype(env, targets, &object_table_qid) { + if mono_info.is_used_datatype(env, targets, &object_table_qid, &[]) { table_instances.push(TableImpl::object_table( env, options, @@ -249,11 +249,13 @@ pub fn add_prelude( let uid_qid = env.uid_qid(); for info in dynamic_field_analysis::get_env_info(env).dynamic_fields() { let (struct_qid, type_inst) = info.0.get_datatype().unwrap(); - if mono_info.is_used_datatype(env, targets, &struct_qid) - && mono_info - .structs - .get(&struct_qid) - .is_some_and(|type_inst_set| type_inst_set.contains(type_inst)) + let is_uid_type = uid_qid.as_ref().is_some_and(|uid| *uid == struct_qid); + if is_uid_type + || (mono_info.is_used_datatype(env, targets, &struct_qid, &[]) + && mono_info + .structs + .get(&struct_qid) + .is_some_and(|type_inst_set| type_inst_set.contains(type_inst))) { dynamic_field_instances.push(DynamicFieldInfo::dynamic_field( env, options, info.0, info.1, false, @@ -305,7 +307,7 @@ pub fn add_prelude( .find_struct(env.symbol_pool().make("Option")) .unwrap(); let option_instances = - if mono_info.is_used_datatype(env, targets, &option_env.get_qualified_id()) { + if mono_info.is_used_datatype(env, targets, &option_env.get_qualified_id(), &[]) { mono_info .structs .get(&option_env.get_qualified_id()) @@ -323,18 +325,22 @@ pub fn add_prelude( let vec_set_struct_env = vec_set_module_env .find_struct(env.symbol_pool().make("VecSet")) .unwrap(); - let vec_set_instances = - if mono_info.is_used_datatype(env, targets, &vec_set_struct_env.get_qualified_id()) { - mono_info - .structs - .get(&vec_set_struct_env.get_qualified_id()) - .unwrap_or(&BTreeSet::new()) - .iter() - .map(|tys| TypeInfo::new(env, options, &tys[0], false)) - .collect_vec() - } else { - vec![] - }; + let vec_set_instances = if mono_info.is_used_datatype( + env, + targets, + &vec_set_struct_env.get_qualified_id(), + &[], + ) { + mono_info + .structs + .get(&vec_set_struct_env.get_qualified_id()) + .unwrap_or(&BTreeSet::new()) + .iter() + .map(|tys| TypeInfo::new(env, options, &tys[0], false)) + .collect_vec() + } else { + vec![] + }; context.insert("vec_set_instances", &vec_set_instances); } @@ -342,23 +348,27 @@ pub fn add_prelude( let vec_map_struct_env = vec_map_module_env .find_struct(env.symbol_pool().make("VecMap")) .unwrap(); - let vec_map_instances = - if mono_info.is_used_datatype(env, targets, &vec_map_struct_env.get_qualified_id()) { - mono_info - .structs - .get(&vec_map_struct_env.get_qualified_id()) - .unwrap_or(&BTreeSet::new()) - .iter() - .map(|tys| { - ( - TypeInfo::new(env, options, &tys[0], false), - TypeInfo::new(env, options, &tys[1], false), - ) - }) - .collect_vec() - } else { - vec![] - }; + let vec_map_instances = if mono_info.is_used_datatype( + env, + targets, + &vec_map_struct_env.get_qualified_id(), + &[], + ) { + mono_info + .structs + .get(&vec_map_struct_env.get_qualified_id()) + .unwrap_or(&BTreeSet::new()) + .iter() + .map(|tys| { + ( + TypeInfo::new(env, options, &tys[0], false), + TypeInfo::new(env, options, &tys[1], false), + ) + }) + .collect_vec() + } else { + vec![] + }; context.insert("vec_map_instances", &vec_map_instances); } @@ -368,7 +378,7 @@ pub fn add_prelude( .find_struct(env.symbol_pool().make("TableVec")) .unwrap(); let table_vec_instances = - if mono_info.is_used_datatype(env, targets, &table_vec_env.get_qualified_id()) { + if mono_info.is_used_datatype(env, targets, &table_vec_env.get_qualified_id(), &[]) { mono_info .structs .get(&table_vec_env.get_qualified_id()) diff --git a/crates/move-stackless-bytecode/src/dynamic_field_analysis.rs b/crates/move-stackless-bytecode/src/dynamic_field_analysis.rs index eed7a81443..273e9d3255 100644 --- a/crates/move-stackless-bytecode/src/dynamic_field_analysis.rs +++ b/crates/move-stackless-bytecode/src/dynamic_field_analysis.rs @@ -14,10 +14,11 @@ use crate::{ use codespan_reporting::diagnostic::{Diagnostic, Label, Severity}; use itertools::Itertools; use move_model::{ - model::{FunctionEnv, GlobalEnv, StructEnv}, + model::{FunctionEnv, GlobalEnv, QualifiedId, StructEnv}, ty::Type, }; use std::{ + cell::Cell, collections::{BTreeMap, BTreeSet}, rc::Rc, }; @@ -57,6 +58,21 @@ impl NameValueInfo { NameValueInfo::NameOnly(name) => name, } } + + pub fn instantiate(&self, type_inst: &[Type]) -> Self { + match self { + NameValueInfo::NameValue { + name, + value, + is_mut, + } => NameValueInfo::NameValue { + name: name.instantiate(type_inst), + value: value.instantiate(type_inst), + is_mut: *is_mut, + }, + NameValueInfo::NameOnly(name) => NameValueInfo::NameOnly(name.instantiate(type_inst)), + } + } } impl DynamicFieldInfo { @@ -117,20 +133,7 @@ impl DynamicFieldInfo { ty.instantiate(type_inst), name_value_set .iter() - .map(|name_value_info| match name_value_info { - NameValueInfo::NameValue { - name, - value, - is_mut, - } => NameValueInfo::NameValue { - name: name.instantiate(type_inst), - value: value.instantiate(type_inst), - is_mut: *is_mut, - }, - NameValueInfo::NameOnly(name) => { - NameValueInfo::NameOnly(name.instantiate(type_inst)) - } - }) + .map(|nv| nv.instantiate(type_inst)) .collect(), ) }) @@ -176,91 +179,74 @@ pub fn get_function_return_local_pos(local_idx: usize, code: &[Bytecode]) -> Opt return_pos } -/// Collect dynamic field type information from a function's bytecode -fn collect_dynamic_field_info( - targets: &FunctionTargetsHolder, - builder: &mut FunctionDataBuilder, - verified_or_inlined: bool, -) -> DynamicFieldInfo { - let dynamic_field_name_value_fun_qids = vec![ +/// Collect all dynamic field function QualifiedIds from the environment +fn collect_df_qids(env: &GlobalEnv) -> DfQids { + let name_value = vec![ // dynamic field operations - builder.fun_env.module_env.env.dynamic_field_borrow_qid(), - builder - .fun_env - .module_env - .env - .dynamic_field_exists_with_type_qid(), + env.dynamic_field_borrow_qid(), + env.dynamic_field_exists_with_type_qid(), // dynamic object field operations - builder - .fun_env - .module_env - .env - .dynamic_object_field_borrow_qid(), - builder - .fun_env - .module_env - .env - .dynamic_object_field_exists_with_type_qid(), + env.dynamic_object_field_borrow_qid(), + env.dynamic_object_field_exists_with_type_qid(), ] .into_iter() - .filter_map(|x| x) + .flatten() .collect_vec(); - let dynamic_field_name_value_fun_mut_qids = vec![ + let name_value_mut = vec![ // dynamic field operations - builder.fun_env.module_env.env.dynamic_field_add_qid(), - builder - .fun_env - .module_env - .env - .dynamic_field_borrow_mut_qid(), - builder.fun_env.module_env.env.dynamic_field_remove_qid(), - builder - .fun_env - .module_env - .env - .dynamic_field_remove_if_exists_qid(), + env.dynamic_field_add_qid(), + env.dynamic_field_borrow_mut_qid(), + env.dynamic_field_remove_qid(), + env.dynamic_field_remove_if_exists_qid(), // dynamic object field operations - builder - .fun_env - .module_env - .env - .dynamic_object_field_add_qid(), - builder - .fun_env - .module_env - .env - .dynamic_object_field_borrow_mut_qid(), - builder - .fun_env - .module_env - .env - .dynamic_object_field_remove_qid(), + env.dynamic_object_field_add_qid(), + env.dynamic_object_field_borrow_mut_qid(), + env.dynamic_object_field_remove_qid(), ] .into_iter() - .filter_map(|x| x) + .flatten() .collect_vec(); - let dynamic_field_name_only_fun_qids = vec![ + let name_only = vec![ // dynamic field operations - builder.fun_env.module_env.env.dynamic_field_exists_qid(), + env.dynamic_field_exists_qid(), // dynamic object field operations - builder - .fun_env - .module_env - .env - .dynamic_object_field_exists_qid(), + env.dynamic_object_field_exists_qid(), ] .into_iter() - .filter_map(|x| x) - .collect_vec(); - let all_dynamic_field_fun_qids = [ - &dynamic_field_name_value_fun_qids, - &dynamic_field_name_value_fun_mut_qids, - &dynamic_field_name_only_fun_qids, - ] - .into_iter() - .cloned() .flatten() .collect_vec(); + let all = [&name_value, &name_value_mut, &name_only] + .into_iter() + .cloned() + .flatten() + .collect_vec(); + DfQids { + name_value, + name_value_mut, + name_only, + all, + } +} + +struct DfQids { + name_value: Vec>, + name_value_mut: Vec>, + name_only: Vec>, + all: Vec>, +} + +/// Collect dynamic field type information from a function's bytecode +fn collect_dynamic_field_info( + targets: &FunctionTargetsHolder, + builder: &mut FunctionDataBuilder, + verified_or_inlined: bool, + use_uid: bool, +) -> DynamicFieldInfo { + let env = builder.fun_env.module_env.env; + let df_qids = collect_df_qids(env); + let uid_type = env + .uid_qid() + .map(|qid| Type::Datatype(qid.module_id, qid.id, vec![])); // compute map of temp index that load object ids to type of object let uid_info = compute_uid_info(&builder.get_target(), targets, &builder.data.code); @@ -273,74 +259,76 @@ fn collect_dynamic_field_info( Bytecode::Call(_, _, Operation::Function(module_id, fun_id, type_inst), srcs, _) => { let callee_id = module_id.qualified(*fun_id); - let uid_object_type_not_found_error = || { - if !verified_or_inlined - && !builder + // Determine the object type for this df call. + // When use_uid is set (detected in initialize), always use UID type. + // Otherwise, look up the parent object type, falling back to UID + // with a warning when the parent can't be determined. + let get_obj_type = |offset: usize| -> Option { + if use_uid { + return uid_type.clone(); + } + if let Some((_, obj_type)) = + get_uid_object_type(&uid_info, &alias_info, srcs[0], offset) + { + return Some(obj_type.clone()); + } + // UID fallback: emit warning when parent is unknown + let uid_qid = env.uid_qid()?; + if verified_or_inlined + || builder .fun_env .get_return_types() .iter() .any(|x| x.is_mutable_reference()) { - return; + let loc = builder.get_loc(bc.get_attr_id()); + env.add_diag( + Diagnostic::new(Severity::Warning) + .with_message( + "UID object type not found, dynamic fields will be placed under UID", + ) + .with_labels(vec![Label::primary(loc.file_id(), loc.span())]), + ); } - - let loc = builder.get_loc(bc.get_attr_id()); - builder.fun_env.module_env.env.add_diag( - Diagnostic::new(Severity::Error) - .with_code("E0022") - .with_message(&format!("UID object type not found: {}", srcs[0])) - .with_labels(vec![Label::primary(loc.file_id(), loc.span())]), - ); + Some(Type::Datatype(uid_qid.module_id, uid_qid.id, vec![])) }; if callee_id == builder.fun_env.get_qualified_id() { return None; } - if dynamic_field_name_value_fun_qids.contains(&callee_id) { - if let Some((_, obj_type)) = - get_uid_object_type(&uid_info, &alias_info, srcs[0], offset) - { + if df_qids.name_value.contains(&callee_id) { + if let Some(obj_type) = get_obj_type(offset) { return Some(DynamicFieldInfo::singleton( - obj_type.clone(), + obj_type, NameValueInfo::NameValue { name: type_inst[0].clone(), value: type_inst[1].clone(), is_mut: false, }, )); - } else { - uid_object_type_not_found_error(); } } - if dynamic_field_name_value_fun_mut_qids.contains(&callee_id) { - if let Some((_, obj_type)) = - get_uid_object_type(&uid_info, &alias_info, srcs[0], offset) - { + if df_qids.name_value_mut.contains(&callee_id) { + if let Some(obj_type) = get_obj_type(offset) { return Some(DynamicFieldInfo::singleton( - obj_type.clone(), + obj_type, NameValueInfo::NameValue { name: type_inst[0].clone(), value: type_inst[1].clone(), is_mut: true, }, )); - } else { - uid_object_type_not_found_error(); } } - if dynamic_field_name_only_fun_qids.contains(&callee_id) { - if let Some((_, obj_type)) = - get_uid_object_type(&uid_info, &alias_info, srcs[0], offset) - { + if df_qids.name_only.contains(&callee_id) { + if let Some(obj_type) = get_obj_type(offset) { return Some(DynamicFieldInfo::singleton( - obj_type.clone(), + obj_type, NameValueInfo::NameOnly(type_inst[0].clone()), )); - } else { - uid_object_type_not_found_error(); } } @@ -348,25 +336,15 @@ fn collect_dynamic_field_info( .get_callee_spec_qid(&builder.fun_env.get_qualified_id(), &callee_id) .unwrap_or(&callee_id); - let func_env = builder - .fun_env - .module_env - .env - .get_function(*fun_id_with_info); + let func_env = env.get_function(*fun_id_with_info); - // native, reachable or intrinsic functions do not access dynamic fields - if func_env.is_native() || get_info(&builder.get_target()).reachable { + if func_env.is_native() || func_env.is_intrinsic() { return None; } let info = targets .get_data(fun_id_with_info, &FunctionVariant::Baseline) - .map(|data| get_fun_info(data)) - .expect(&format!( - "callee `{}` of `{}` was filtered out", - func_env.get_full_name_str(), - builder.fun_env.get_full_name_str() - )); + .map(|data| get_fun_info(data))?; Some(info.instantiate(type_inst)) } _ => None, @@ -384,12 +362,19 @@ fn collect_dynamic_field_info( Operation::Function(module_id, fun_id, mut type_inst), mut srcs, aa, - ) if all_dynamic_field_fun_qids.contains(&module_id.qualified(fun_id)) => { - if let Some((obj_local, obj_type)) = + ) if df_qids.all.contains(&module_id.qualified(fun_id)) => { + if use_uid { + // All df operations use UID type directly + if let Some(ref uid_ty) = uid_type { + type_inst.push(uid_ty.clone()); + } + } else if let Some((obj_local, obj_type)) = get_uid_object_type(&info.uid_info, &alias_info, srcs[0], offset) { srcs[0] = *obj_local; - if !dynamic_field_name_value_fun_mut_qids.contains(&module_id.qualified(fun_id)) + if !df_qids + .name_value_mut + .contains(&module_id.qualified(fun_id)) && builder.get_local_type(srcs[0]).is_mutable_reference() { srcs[0] = builder.emit_let_read_ref(srcs[0]); @@ -411,6 +396,79 @@ fn collect_dynamic_field_info( info } +/// Like `compute_uid_info` but runs before `process` (no callee annotations available). +/// Computes callee uid_info on-the-fly instead of reading annotations. +fn compute_uid_info_local( + fun_target: &FunctionTarget, + targets: &FunctionTargetsHolder, + code: &[Bytecode], +) -> BTreeMap { + let env = fun_target.global_env(); + code.iter() + .filter_map(|bc| match bc { + Bytecode::Call( + attr_id, + dests, + Operation::BorrowField(mid, sid, tys, offset), + srcs, + _, + ) if is_uid_field_access(&env.get_struct(mid.qualified(*sid)), *offset) + && !dests.is_empty() => + { + Some(( + dests[0], + (srcs[0], Type::Datatype(*mid, *sid, tys.clone()), *attr_id), + )) + } + Bytecode::Call(attr_id, dests, Operation::GetField(mid, sid, tys, offset), srcs, _) + if is_uid_field_access(&env.get_struct(mid.qualified(*sid)), *offset) + && !dests.is_empty() => + { + Some(( + dests[0], + (srcs[0], Type::Datatype(*mid, *sid, tys.clone()), *attr_id), + )) + } + Bytecode::Call(attr_id, dests, Operation::Function(mid, fid, tys), srcs, _) + if !dests.is_empty() => + { + let callee_id = mid.qualified(*fid); + if callee_id == fun_target.global_env().type_inv_qid() { + return None; + } + + let callee_data = targets.get_data(&callee_id, &FunctionVariant::Baseline)?; + let callee_env = env.get_function(callee_id); + let callee_target = FunctionTarget::new(&callee_env, callee_data); + let callee_uid_info = + compute_uid_info_local(&callee_target, targets, &callee_data.code); + + for key in callee_uid_info.keys() { + if let Some(ret_pos) = get_function_return_local_pos(*key, &callee_data.code) { + let (_, obj_type) = callee_uid_info.get(key).unwrap(); + return Some(( + dests[ret_pos], + (srcs[0], obj_type.instantiate(tys), *attr_id), + )); + } + } + + None + } + _ => None, + }) + .into_group_map() + .into_iter() + .filter_map(|(temp_idx, types)| { + if types.len() == 1 { + Some((temp_idx, (types[0].0, types[0].1.clone()))) + } else { + None + } + }) + .collect() +} + /// Computes a mapping from temporary indices to the objects and types of objects they reference fn compute_uid_info( fun_target: &FunctionTarget, @@ -559,15 +617,69 @@ fn get_uid_object_type<'a>( }) } -pub struct DynamicFieldAnalysisProcessor(); +pub struct DynamicFieldAnalysisProcessor { + use_uid: Cell, +} impl DynamicFieldAnalysisProcessor { pub fn new() -> Box { - Box::new(Self()) + Box::new(Self { + use_uid: Cell::new(false), + }) } } impl FunctionTargetProcessor for DynamicFieldAnalysisProcessor { + fn initialize(&self, env: &GlobalEnv, targets: &mut FunctionTargetsHolder) { + if env.uid_qid().is_none() { + return; + } + let df_qids = collect_df_qids(env); + + // Check if any accessible function has a df call where the parent + // object type can't be resolved locally. When that happens, fall back + // to UID type for ALL df operations for consistency. + let mut use_uid = false; + for fun_id in targets.get_funs().collect_vec() { + let fun_env = env.get_function(fun_id); + if fun_env.is_native() || fun_env.is_intrinsic() { + continue; + } + let data = match targets.get_data(&fun_id, &FunctionVariant::Baseline) { + Some(d) => d, + None => continue, + }; + let target = FunctionTarget::new(&fun_env, data); + let info = get_info(&target); + if !info.accessible() { + continue; + } + + let uid_info = compute_uid_info_local(&target, targets, &data.code); + let alias_info = ReachingDefProcessor::analyze_reaching_definitions(&fun_env, data); + + for (offset, bc) in data.code.iter().enumerate() { + if let Bytecode::Call(attr_id, _, Operation::Function(mid, fid, _), srcs, _) = bc { + if df_qids.all.contains(&mid.qualified(*fid)) + && get_uid_object_type(&uid_info, &alias_info, srcs[0], offset).is_none() + { + use_uid = true; + let loc = target.get_bytecode_loc(*attr_id); + env.add_diag( + Diagnostic::new(Severity::Warning) + .with_message( + "UID object type not found, dynamic fields will be placed under UID", + ) + .with_labels(vec![Label::primary(loc.file_id(), loc.span())]), + ); + } + } + } + } + + self.use_uid.set(use_uid); + } + fn process( &self, targets: &mut FunctionTargetsHolder, @@ -586,10 +698,17 @@ impl FunctionTargetProcessor for DynamicFieldAnalysisProcessor { return data; } + let use_uid = self.use_uid.get(); + let mut builder = FunctionDataBuilder::new(fun_env, data); // Collect the dynamic field info - let info = collect_dynamic_field_info(targets, &mut builder, info.verified || info.inlined); + let info = collect_dynamic_field_info( + targets, + &mut builder, + info.verified || info.inlined, + use_uid, + ); builder .data diff --git a/crates/move-stackless-bytecode/src/mono_analysis.rs b/crates/move-stackless-bytecode/src/mono_analysis.rs index 8a6740f960..cf24dda5be 100644 --- a/crates/move-stackless-bytecode/src/mono_analysis.rs +++ b/crates/move-stackless-bytecode/src/mono_analysis.rs @@ -61,7 +61,18 @@ impl MonoInfo { env: &GlobalEnv, targets: &FunctionTargetsHolder, dt_qid: &QualifiedId, + type_inst: &[Type], ) -> bool { + // A struct with dynamic fields must not be opaque + let struct_type = Type::Datatype(dt_qid.module_id, dt_qid.id, type_inst.to_vec()); + if dynamic_field_analysis::get_env_info(env) + .dynamic_field_names_values(&struct_type) + .next() + .is_some() + { + return true; + } + if env .get_extension::() .unwrap() diff --git a/crates/sui-prover/tests/inputs/dynamic_field/uid_param.ok.move b/crates/sui-prover/tests/inputs/dynamic_field/uid_param.ok.move new file mode 100644 index 0000000000..17a0dc870e --- /dev/null +++ b/crates/sui-prover/tests/inputs/dynamic_field/uid_param.ok.move @@ -0,0 +1,24 @@ +module 0x42::foo; + +use prover::prover::{requires, ensures}; +use sui::dynamic_field as df; + +public struct WhitelistKey has copy, store, drop { + address: address, +} + +public struct MyObject has key { + id: UID, +} + +public fun add_whitelist_address(uid: &mut UID, addr: address) { + df::add(uid, WhitelistKey { address: addr }, true); +} + +#[spec(prove)] +fun add_whitelist_spec(obj: &mut MyObject, addr: address) { + requires(!df::exists_with_type(&obj.id, WhitelistKey { address: addr })); + add_whitelist_address(&mut obj.id, addr); + ensures(df::exists_with_type(&obj.id, WhitelistKey { address: addr })); + ensures(*df::borrow(&obj.id, WhitelistKey { address: addr }) == true); +} diff --git a/crates/sui-prover/tests/inputs/dynamic_field/uid_param_exists.ok.move b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_exists.ok.move new file mode 100644 index 0000000000..b6064976e7 --- /dev/null +++ b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_exists.ok.move @@ -0,0 +1,20 @@ +module 0x42::foo; + +use sui::dynamic_field as df; + +public struct WhitelistKey has copy, store, drop { + address: address, +} + +public struct MyObject has key { + id: UID, +} + +public fun in_whitelist(uid: &UID, addr: address): bool { + df::exists_with_type(uid, WhitelistKey { address: addr }) +} + +#[spec(prove)] +fun check_in_whitelist(obj: &MyObject, addr: address): bool { + in_whitelist(&obj.id, addr) +} diff --git a/crates/sui-prover/tests/inputs/dynamic_field/uid_param_multi_ops.ok.move b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_multi_ops.ok.move new file mode 100644 index 0000000000..1e8887bffe --- /dev/null +++ b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_multi_ops.ok.move @@ -0,0 +1,26 @@ +module 0x42::foo; + +use prover::prover::{requires, ensures}; +use sui::dynamic_field as df; + +public struct NameKey has copy, store, drop {} +public struct CountKey has copy, store, drop {} + +public struct MyObject has key { + id: UID, +} + +public fun initialize(uid: &mut UID, count: u64) { + df::add(uid, NameKey {}, true); + df::add(uid, CountKey {}, count); +} + +#[spec(prove)] +fun verify_initialize(obj: &mut MyObject, count: u64) { + requires(!df::exists_with_type(&obj.id, NameKey {})); + requires(!df::exists_with_type(&obj.id, CountKey {})); + initialize(&mut obj.id, count); + ensures(df::exists_with_type(&obj.id, NameKey {})); + ensures(df::exists_with_type(&obj.id, CountKey {})); + ensures(*df::borrow(&obj.id, CountKey {}) == count); +} diff --git a/crates/sui-prover/tests/inputs/dynamic_field/uid_param_multi_type_params.ok.move b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_multi_type_params.ok.move new file mode 100644 index 0000000000..ccf6829a72 --- /dev/null +++ b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_multi_type_params.ok.move @@ -0,0 +1,24 @@ +module 0x42::foo; + +use prover::prover::{requires, ensures}; +use sui::dynamic_field as df; + +public struct MyObject has key { + id: UID, +} + +public fun generic_add(uid: &mut UID, key: K, val: V) { + df::add(uid, key, val); +} + +public fun generic_exists(uid: &UID, key: K): bool { + df::exists_with_type(uid, key) +} + +#[spec(prove)] +fun generic_add_u64_bool_spec(obj: &mut MyObject, key: u64, val: bool) { + requires(!df::exists_with_type(&obj.id, key)); + generic_add(&mut obj.id, key, val); + ensures(df::exists_with_type(&obj.id, key)); + ensures(*df::borrow(&obj.id, key) == val); +} diff --git a/crates/sui-prover/tests/inputs/dynamic_field/uid_param_nested_generic.ok.move b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_nested_generic.ok.move new file mode 100644 index 0000000000..27e1e6563a --- /dev/null +++ b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_nested_generic.ok.move @@ -0,0 +1,29 @@ +module 0x42::foo; + +use prover::prover::{requires, ensures}; +use sui::dynamic_field as df; + +public struct MyObject has key { + id: UID, +} + +public fun has_field(uid: &UID, key: K): bool { + df::exists_with_type(uid, key) +} + +public fun get_field(uid: &UID, key: K, default: V): V { + if (has_field(uid, key)) { + *df::borrow(uid, key) + } else { + default + } +} + +#[spec(prove)] +fun verify_get_field(obj: &MyObject, key: u64): u64 { + requires(df::exists_with_type(&obj.id, key)); + requires(*df::borrow(&obj.id, key) == 42); + let result = get_field(&obj.id, key, 0); + ensures(result == 42); + result +} diff --git a/crates/sui-prover/tests/inputs/dynamic_field/uid_param_target.ok.move b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_target.ok.move new file mode 100644 index 0000000000..6ca2f24aa4 --- /dev/null +++ b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_target.ok.move @@ -0,0 +1,42 @@ +module 0x42::foo; + +use sui::dynamic_field as df; +use prover::prover::asserts; + +public struct WhitelistKey has copy, store, drop { + address: address, +} + +public struct AllowAllKey has copy, store, drop {} + +public struct MyObject has key { + id: UID, +} + +public fun add_whitelist_address(uid: &mut UID, addr: address) { + df::add(uid, WhitelistKey { address: addr }, true); +} + +public fun allow_all(uid: &mut UID) { + df::add(uid, AllowAllKey {}, true); +} + +public fun whitelist_key(addr: address): WhitelistKey { + WhitelistKey { address: addr } +} + +public fun allow_all_key(): AllowAllKey { + AllowAllKey {} +} + +#[spec(prove, target = add_whitelist_address)] +fun add_whitelist_address_spec(uid: &mut UID, addr: address) { + asserts(!df::exists_with_type(uid, whitelist_key(addr))); + add_whitelist_address(uid, addr); +} + +#[spec(prove, target = allow_all)] +fun allow_all_spec(uid: &mut UID) { + asserts(!df::exists_with_type(uid, allow_all_key())); + allow_all(uid); +} diff --git a/crates/sui-prover/tests/inputs/dynamic_field/uid_param_vec_value.ok.move b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_vec_value.ok.move new file mode 100644 index 0000000000..8f6b045403 --- /dev/null +++ b/crates/sui-prover/tests/inputs/dynamic_field/uid_param_vec_value.ok.move @@ -0,0 +1,20 @@ +module 0x42::foo; + +use prover::prover::{requires, ensures}; +use sui::dynamic_field as df; + +public struct MyObject has key { + id: UID, +} + +public fun set_scores(uid: &mut UID, key: u64, scores: vector) { + df::add(uid, key, scores); +} + +#[spec(prove)] +fun verify_set_scores(obj: &mut MyObject, key: u64, scores: vector) { + requires(!df::exists_with_type>(&obj.id, key)); + set_scores(&mut obj.id, key, scores); + ensures(df::exists_with_type>(&obj.id, key)); + ensures(*df::borrow>(&obj.id, key) == scores); +} diff --git a/crates/sui-prover/tests/inputs/dynamic_field/vec_value_concrete.ok.move b/crates/sui-prover/tests/inputs/dynamic_field/vec_value_concrete.ok.move new file mode 100644 index 0000000000..45112b4292 --- /dev/null +++ b/crates/sui-prover/tests/inputs/dynamic_field/vec_value_concrete.ok.move @@ -0,0 +1,20 @@ +module 0x42::foo; + +use prover::prover::{requires, ensures}; +use sui::dynamic_field as df; + +public struct Foo has key { + id: UID, +} + +fun store_list(x: &mut Foo, key: u64, items: vector) { + df::add>(&mut x.id, key, items); +} + +#[spec(prove)] +fun store_list_spec(x: &mut Foo, key: u64, items: vector) { + requires(!df::exists_with_type>(&x.id, key)); + store_list(x, key, items); + ensures(df::exists_with_type>(&x.id, key)); + ensures(*df::borrow>(&x.id, key) == items); +} diff --git a/crates/sui-prover/tests/snapshots/dynamic_field/issue-237.fail.move.snap b/crates/sui-prover/tests/snapshots/dynamic_field/issue-237.fail.move.snap index e2ea6d088f..b8c67ad7f3 100644 --- a/crates/sui-prover/tests/snapshots/dynamic_field/issue-237.fail.move.snap +++ b/crates/sui-prover/tests/snapshots/dynamic_field/issue-237.fail.move.snap @@ -1,10 +1,9 @@ --- source: crates/sui-prover/tests/integration.rs -assertion_line: 260 expression: output --- -exiting with bytecode transformation errors -error[E0022]: UID object type not found: 2 +Verification successful +warning: UID object type not found, dynamic fields will be placed under UID ┌─ tests/inputs/dynamic_field/issue-237.fail.move:19:5 │ 19 │ dynamic_field::borrow_mut(id, version) diff --git a/crates/sui-prover/tests/snapshots/dynamic_field/uid_param.ok.move.snap b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param.ok.move.snap new file mode 100644 index 0000000000..212afffbdc --- /dev/null +++ b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param.ok.move.snap @@ -0,0 +1,11 @@ +--- +source: crates/sui-prover/tests/integration.rs +assertion_line: 297 +expression: output +--- +Verification successful +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param.ok.move:15:5 + │ +15 │ df::add(uid, WhitelistKey { address: addr }, true); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_exists.ok.move.snap b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_exists.ok.move.snap new file mode 100644 index 0000000000..c18f8c7e05 --- /dev/null +++ b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_exists.ok.move.snap @@ -0,0 +1,11 @@ +--- +source: crates/sui-prover/tests/integration.rs +assertion_line: 297 +expression: output +--- +Verification successful +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_exists.ok.move:14:5 + │ +14 │ df::exists_with_type(uid, WhitelistKey { address: addr }) + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_multi_ops.ok.move.snap b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_multi_ops.ok.move.snap new file mode 100644 index 0000000000..6df5076c57 --- /dev/null +++ b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_multi_ops.ok.move.snap @@ -0,0 +1,16 @@ +--- +source: crates/sui-prover/tests/integration.rs +expression: output +--- +Verification successful +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_multi_ops.ok.move:14:5 + │ +14 │ df::add(uid, NameKey {}, true); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_multi_ops.ok.move:15:5 + │ +15 │ df::add(uid, CountKey {}, count); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_multi_type_params.ok.move.snap b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_multi_type_params.ok.move.snap new file mode 100644 index 0000000000..5583eded25 --- /dev/null +++ b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_multi_type_params.ok.move.snap @@ -0,0 +1,10 @@ +--- +source: crates/sui-prover/tests/integration.rs +expression: output +--- +Verification successful +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_multi_type_params.ok.move:11:5 + │ +11 │ df::add(uid, key, val); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_nested_generic.ok.move.snap b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_nested_generic.ok.move.snap new file mode 100644 index 0000000000..b467181011 --- /dev/null +++ b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_nested_generic.ok.move.snap @@ -0,0 +1,16 @@ +--- +source: crates/sui-prover/tests/integration.rs +expression: output +--- +Verification successful +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_nested_generic.ok.move:16:10 + │ +16 │ *df::borrow(uid, key) + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_nested_generic.ok.move:11:5 + │ +11 │ df::exists_with_type(uid, key) + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_target.ok.move.snap b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_target.ok.move.snap new file mode 100644 index 0000000000..0c484f478c --- /dev/null +++ b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_target.ok.move.snap @@ -0,0 +1,29 @@ +--- +source: crates/sui-prover/tests/integration.rs +assertion_line: 297 +expression: output +--- +Verification successful +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_target.ok.move:17:5 + │ +17 │ df::add(uid, WhitelistKey { address: addr }, true); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_target.ok.move:34:14 + │ +34 │ asserts(!df::exists_with_type(uid, whitelist_key(addr))); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_target.ok.move:21:5 + │ +21 │ df::add(uid, AllowAllKey {}, true); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_target.ok.move:40:14 + │ +40 │ asserts(!df::exists_with_type(uid, allow_all_key())); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_vec_value.ok.move.snap b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_vec_value.ok.move.snap new file mode 100644 index 0000000000..94125bc8ee --- /dev/null +++ b/crates/sui-prover/tests/snapshots/dynamic_field/uid_param_vec_value.ok.move.snap @@ -0,0 +1,10 @@ +--- +source: crates/sui-prover/tests/integration.rs +expression: output +--- +Verification successful +warning: UID object type not found, dynamic fields will be placed under UID + ┌─ tests/inputs/dynamic_field/uid_param_vec_value.ok.move:11:5 + │ +11 │ df::add(uid, key, scores); + │ ^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/crates/sui-prover/tests/snapshots/dynamic_field/vec_value_concrete.ok.move.snap b/crates/sui-prover/tests/snapshots/dynamic_field/vec_value_concrete.ok.move.snap new file mode 100644 index 0000000000..95d8a7083e --- /dev/null +++ b/crates/sui-prover/tests/snapshots/dynamic_field/vec_value_concrete.ok.move.snap @@ -0,0 +1,5 @@ +--- +source: crates/sui-prover/tests/integration.rs +expression: output +--- +Verification successful