From 5efe28127720df14fb315fbb94f99cf046714768 Mon Sep 17 00:00:00 2001 From: simonjiao Date: Fri, 9 Aug 2024 16:47:14 +0800 Subject: [PATCH 1/2] using ReferenceKind instead raw bool type --- .../move-model/src/builder/exp_translator.rs | 8 +- language/move-model/src/model.rs | 77 ++++++++++--------- language/move-model/src/ty.rs | 47 ++++++++--- .../bytecode/src/eliminate_imm_refs.rs | 6 +- .../bytecode/src/spec_instrumentation.rs | 33 ++++---- .../src/stackless_bytecode_generator.rs | 40 ++++++---- .../interpreter/src/concrete/player.rs | 3 +- .../interpreter/src/concrete/runtime.rs | 3 +- .../interpreter/src/concrete/ty.rs | 6 +- .../move-prover/move-abigen/src/abigen.rs | 3 +- 10 files changed, 136 insertions(+), 90 deletions(-) diff --git a/language/move-model/src/builder/exp_translator.rs b/language/move-model/src/builder/exp_translator.rs index 28cea32fe9..f5969e148a 100644 --- a/language/move-model/src/builder/exp_translator.rs +++ b/language/move-model/src/builder/exp_translator.rs @@ -16,6 +16,7 @@ use move_compiler::{ use move_core_types::value::MoveValue; use move_ir_types::location::Spanned; +use crate::ty::ReferenceKind; use crate::{ ast::{Exp, ExpData, LocalVarDecl, ModuleName, Operation, QualifiedSymbol, QuantKind, Value}, builder::{ @@ -531,7 +532,7 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo if ty == Type::Error { Type::Error } else { - Type::Reference(*is_mut, Box::new(ty)) + Type::Reference(ReferenceKind::from_is_mut(*is_mut), Box::new(ty)) } } Base(ty) => self.translate_hlir_base_type(ty), @@ -680,7 +681,10 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo rty } } - Ref(is_mut, ty) => Type::Reference(*is_mut, Box::new(self.translate_type(ty))), + Ref(is_mut, ty) => Type::Reference( + ReferenceKind::from_is_mut(*is_mut), + Box::new(self.translate_type(ty)), + ), Fun(args, result) => Type::Fun( self.translate_types(args), Box::new(self.translate_type(result)), diff --git a/language/move-model/src/model.rs b/language/move-model/src/model.rs index 6faefc33ed..554e4b9f9e 100644 --- a/language/move-model/src/model.rs +++ b/language/move-model/src/model.rs @@ -61,6 +61,7 @@ use move_core_types::{ }; use move_disassembler::disassembler::{Disassembler, DisassemblerOptions}; +use crate::ty::ReferenceKind; use crate::{ ast::{ Attribute, ConditionKind, Exp, ExpData, GlobalInvariant, ModuleName, PropertyBag, @@ -1032,9 +1033,9 @@ impl GlobalEnv { let decl = module.get_spec_fun(caller.id); decl.callees.contains(&fun) || decl - .callees - .iter() - .any(|trans_caller| is_caller(env, visited, *trans_caller, fun)) + .callees + .iter() + .any(|trans_caller| is_caller(env, visited, *trans_caller, fun)) } let module = self.get_module(id.module_id); let is_recursive = *module.get_spec_fun(id.id).is_recursive.borrow(); @@ -1343,14 +1344,14 @@ impl GlobalEnv { for func_env in module_env.into_functions() { if Self::enclosing_span(func_env.get_loc().span(), loc.span()) || Self::enclosing_span( - func_env - .get_spec() - .loc - .clone() - .unwrap_or_else(|| self.unknown_loc.clone()) - .span(), - loc.span(), - ) + func_env + .get_spec() + .loc + .clone() + .unwrap_or_else(|| self.unknown_loc.clone()) + .span(), + loc.span(), + ) { return Some(func_env.clone()); } @@ -1405,7 +1406,7 @@ impl GlobalEnv { } /// Returns an iterator for all modules in the environment. - pub fn get_modules(&self) -> impl Iterator> { + pub fn get_modules(&self) -> impl Iterator> { self.module_data.iter().map(move |module_data| ModuleEnv { env: self, data: module_data, @@ -1413,7 +1414,7 @@ impl GlobalEnv { } /// Returns an iterator for all bytecode modules in the environment. - pub fn get_bytecode_modules(&self) -> impl Iterator { + pub fn get_bytecode_modules(&self) -> impl Iterator { self.module_data .iter() .map(|module_data| &module_data.module) @@ -2027,12 +2028,12 @@ impl<'env> ModuleEnv<'env> { } /// Returns iterator over `NamedConstantEnv`s in this module. - pub fn get_named_constants(&'env self) -> impl Iterator> { + pub fn get_named_constants(&'env self) -> impl Iterator> { self.clone().into_named_constants() } /// Returns an iterator over `NamedConstantEnv`s in this module. - pub fn into_named_constants(self) -> impl Iterator> { + pub fn into_named_constants(self) -> impl Iterator> { self.data .named_constants .iter() @@ -2071,12 +2072,12 @@ impl<'env> ModuleEnv<'env> { } /// Returns iterator over FunctionEnvs in this module. - pub fn get_functions(&'env self) -> impl Iterator> { + pub fn get_functions(&'env self) -> impl Iterator> { self.clone().into_functions() } /// Returns iterator over FunctionEnvs in this module. - pub fn into_functions(self) -> impl Iterator> { + pub fn into_functions(self) -> impl Iterator> { self.data .function_data .iter() @@ -2174,12 +2175,12 @@ impl<'env> ModuleEnv<'env> { } /// Returns iterator over structs in this module. - pub fn get_structs(&'env self) -> impl Iterator> { + pub fn get_structs(&'env self) -> impl Iterator> { self.clone().into_structs() } /// Returns iterator over structs in this module. - pub fn into_structs(self) -> impl Iterator> { + pub fn into_structs(self) -> impl Iterator> { self.data .struct_data .iter() @@ -2201,12 +2202,14 @@ impl<'env> ModuleEnv<'env> { SignatureToken::U256 => Type::Primitive(PrimitiveType::U256), SignatureToken::Address => Type::Primitive(PrimitiveType::Address), SignatureToken::Signer => Type::Primitive(PrimitiveType::Signer), - SignatureToken::Reference(t) => { - Type::Reference(false, Box::new(self.globalize_signature(t))) - } - SignatureToken::MutableReference(t) => { - Type::Reference(true, Box::new(self.globalize_signature(t))) - } + SignatureToken::Reference(t) => Type::Reference( + ReferenceKind::Immutable, + Box::new(self.globalize_signature(t)), + ), + SignatureToken::MutableReference(t) => Type::Reference( + ReferenceKind::Mutable, + Box::new(self.globalize_signature(t)), + ), SignatureToken::TypeParameter(index) => Type::TypeParameter(*index), SignatureToken::Vector(bt) => Type::Vector(Box::new(self.globalize_signature(bt))), SignatureToken::Struct(handle_idx) => { @@ -2285,7 +2288,7 @@ impl<'env> ModuleEnv<'env> { } /// Returns specification variables of this module. - pub fn get_spec_vars(&'env self) -> impl Iterator { + pub fn get_spec_vars(&'env self) -> impl Iterator { self.data.spec_vars.iter() } @@ -2304,7 +2307,7 @@ impl<'env> ModuleEnv<'env> { } /// Returns specification functions of this module. - pub fn get_spec_funs(&'env self) -> impl Iterator { + pub fn get_spec_funs(&'env self) -> impl Iterator { self.data.spec_funs.iter() } @@ -2329,7 +2332,7 @@ impl<'env> ModuleEnv<'env> { pub fn get_spec_funs_of_name( &self, name: Symbol, - ) -> impl Iterator { + ) -> impl Iterator { self.data .spec_funs .iter() @@ -2576,7 +2579,7 @@ impl<'env> StructEnv<'env> { } /// Get an iterator for the fields, ordered by offset. - pub fn get_fields(&'env self) -> impl Iterator> { + pub fn get_fields(&'env self) -> impl Iterator> { self.data .field_data .values() @@ -3125,8 +3128,8 @@ impl<'env> FunctionEnv<'env> { env.get_num_property(&self.get_spec().properties, name) .is_some() || env - .get_num_property(&self.module_env.get_spec().properties, name) - .is_some() + .get_num_property(&self.module_env.get_spec().properties, name) + .is_some() } /// Returns the value of a numeric pragma for this function. This first looks up a @@ -3250,9 +3253,9 @@ impl<'env> FunctionEnv<'env> { self.module_env.is_script_module() || self.definition_view().is_entry() || match self.definition_view().visibility() { - Visibility::Public | Visibility::Friend => true, - Visibility::Private => false, - } + Visibility::Public | Visibility::Friend => true, + Visibility::Private => false, + } } /// Return whether this function is exposed outside of the module. @@ -3260,9 +3263,9 @@ impl<'env> FunctionEnv<'env> { self.module_env.is_script_module() || self.definition_view().is_entry() || match self.definition_view().visibility() { - Visibility::Public => true, - Visibility::Private | Visibility::Friend => false, - } + Visibility::Public => true, + Visibility::Private | Visibility::Friend => false, + } } /// Returns true if the function is a script function diff --git a/language/move-model/src/ty.rs b/language/move-model/src/ty.rs index c460ac906d..0a4bd5fd93 100644 --- a/language/move-model/src/ty.rs +++ b/language/move-model/src/ty.rs @@ -27,20 +27,48 @@ pub enum Type { Vector(Box), Struct(ModuleId, StructId, Vec), TypeParameter(u16), + // todo(simon): change args type to Box? + Fun(/*args*/ Vec, /*result*/ Box), // Types only appearing in programs. - Reference(bool, Box), + Reference(ReferenceKind, Box), // Types only appearing in specifications - Fun(Vec, Box), TypeDomain(Box), ResourceDomain(ModuleId, StructId, Option>), // Temporary types used during type checking Error, + // todo(simon) change Var type to u32? Var(u16), } +/// Represents a reference kind. +#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Clone, Copy)] +pub enum ReferenceKind { + Immutable, + Mutable, +} + +impl ReferenceKind { + pub fn from_is_mut(is_mut: bool) -> ReferenceKind { + if is_mut { + ReferenceKind::Mutable + } else { + ReferenceKind::Immutable + } + } +} + +impl fmt::Display for ReferenceKind { + fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { + match self { + ReferenceKind::Immutable => f.write_str("`&`"), + ReferenceKind::Mutable => f.write_str("`&mut`"), + } + } +} + pub const BOOL_TYPE: Type = Type::Primitive(PrimitiveType::Bool); pub const NUM_TYPE: Type = Type::Primitive(PrimitiveType::Num); @@ -120,12 +148,12 @@ impl Type { /// Determines whether this is a mutable reference. pub fn is_mutable_reference(&self) -> bool { - matches!(self, Type::Reference(true, _)) + matches!(self, Type::Reference(ReferenceKind::Mutable, _)) } /// Determines whether this is an immutable reference. pub fn is_immutable_reference(&self) -> bool { - matches!(self, Type::Reference(false, _)) + matches!(self, Type::Reference(ReferenceKind::Immutable, _)) } /// Determines whether this type is a struct. @@ -434,7 +462,7 @@ impl Type { .expect("Invariant violation: vector type argument contains incomplete, tuple, or spec type")) )), Reference(r, t) => - if r { + if r == ReferenceKind::Mutable { Some(MType::MutableReference(Box::new(t.into_normalized_type(env).expect("Invariant violation: reference type contains incomplete, tuple, or spec type")))) } else { Some(MType::Reference(Box::new(t.into_normalized_type(env).expect("Invariant violation: reference type contains incomplete, tuple, or spec type")))) @@ -810,7 +838,7 @@ impl TypeUnificationAdapter { treat_rhs_type_param_as_var_after_index: Option, ) -> Self where - I: Iterator + Clone, + I: Iterator + Clone, { debug_assert!( treat_lhs_type_param_as_var_after_index.is_some() @@ -1087,7 +1115,7 @@ impl TypeInstantiationDerivation { mark_irrelevant_param_as_error: bool, ) -> BTreeSet> where - I: Iterator + Clone, + I: Iterator + Clone, { let initial_param_insts: Vec<_> = (0..params_arity) .map(|idx| Type::TypeParameter(idx as TypeParameterIndex)) @@ -1240,10 +1268,7 @@ impl<'a> fmt::Display for TypeDisplay<'a> { Ok(()) } Reference(is_mut, t) => { - f.write_str("&")?; - if *is_mut { - f.write_str("mut ")?; - } + f.write_str(is_mut.to_string().as_str())?; write!(f, "{}", t.display(self.context)) } TypeParameter(idx) => { diff --git a/language/move-prover/bytecode/src/eliminate_imm_refs.rs b/language/move-prover/bytecode/src/eliminate_imm_refs.rs index aa670c0aa5..97b234f59c 100644 --- a/language/move-prover/bytecode/src/eliminate_imm_refs.rs +++ b/language/move-prover/bytecode/src/eliminate_imm_refs.rs @@ -2,14 +2,14 @@ // Copyright (c) The Move Contributors // SPDX-License-Identifier: Apache-2.0 -use move_model::{ast::TempIndex, model::FunctionEnv, ty::Type}; - use crate::{ function_data_builder::FunctionDataBuilder, function_target::FunctionData, function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder}, stackless_bytecode::{AssignKind, Bytecode, Operation}, }; +use move_model::ty::ReferenceKind; +use move_model::{ast::TempIndex, model::FunctionEnv, ty::Type}; pub struct EliminateImmRefsProcessor {} @@ -61,7 +61,7 @@ impl<'a> EliminateImmRefs<'a> { } fn transform_type(&self, ty: Type) -> Type { - if let Type::Reference(false, y) = ty { + if let Type::Reference(ReferenceKind::Immutable, y) = ty { *y } else { ty diff --git a/language/move-prover/bytecode/src/spec_instrumentation.rs b/language/move-prover/bytecode/src/spec_instrumentation.rs index 702e3ed571..5c4cab4c13 100644 --- a/language/move-prover/bytecode/src/spec_instrumentation.rs +++ b/language/move-prover/bytecode/src/spec_instrumentation.rs @@ -11,16 +11,6 @@ use std::{ use itertools::Itertools; -use move_model::{ - ast, - ast::{Exp, ExpData, TempIndex, Value}, - exp_generator::ExpGenerator, - model::{FunId, FunctionEnv, GlobalEnv, Loc, ModuleId, QualifiedId, QualifiedInstId, StructId}, - pragmas::{ABORTS_IF_IS_PARTIAL_PRAGMA, EMITS_IS_PARTIAL_PRAGMA, EMITS_IS_STRICT_PRAGMA}, - spec_translator::{SpecTranslator, TranslatedSpec}, - ty::{Type, TypeDisplayContext, BOOL_TYPE, NUM_TYPE}, -}; - use crate::{ function_data_builder::FunctionDataBuilder, function_target::{FunctionData, FunctionTarget}, @@ -36,6 +26,16 @@ use crate::{ }, usage_analysis, verification_analysis, }; +use move_model::ty::ReferenceKind; +use move_model::{ + ast, + ast::{Exp, ExpData, TempIndex, Value}, + exp_generator::ExpGenerator, + model::{FunId, FunctionEnv, GlobalEnv, Loc, ModuleId, QualifiedId, QualifiedInstId, StructId}, + pragmas::{ABORTS_IF_IS_PARTIAL_PRAGMA, EMITS_IS_PARTIAL_PRAGMA, EMITS_IS_STRICT_PRAGMA}, + spec_translator::{SpecTranslator, TranslatedSpec}, + ty::{Type, TypeDisplayContext, BOOL_TYPE, NUM_TYPE}, +}; const REQUIRES_FAILS_MESSAGE: &str = "precondition does not hold at this call"; const ENSURES_FAILS_MESSAGE: &str = "post-condition does not hold"; @@ -750,9 +750,10 @@ impl<'a> Instrumenter<'a> { // Update memory. We create a mut ref for the location then write the value back to it. let (addr_temp, _) = self.builder.emit_let(addr); - let mem_ref = self - .builder - .new_temp(Type::Reference(true, Box::new(ghost_mem_ty))); + let mem_ref = self.builder.new_temp(Type::Reference( + ReferenceKind::Mutable, + Box::new(ghost_mem_ty), + )); // mem_ref = borrow_global_mut(addr) self.builder.emit_with(|id| { Bytecode::Call( @@ -1161,9 +1162,9 @@ fn check_opaque_modifies_completeness( if !found { let loc = fun_env.get_spec_loc(); env.error(&loc, - &format!("function `{}` is opaque but its specification does not have a modifies clause for `{}`", - fun_env.get_full_name_str(), - env.display(mem)) + &format!("function `{}` is opaque but its specification does not have a modifies clause for `{}`", + fun_env.get_full_name_str(), + env.display(mem)), ) } } diff --git a/language/move-prover/bytecode/src/stackless_bytecode_generator.rs b/language/move-prover/bytecode/src/stackless_bytecode_generator.rs index 180699b5bd..f6877151f2 100644 --- a/language/move-prover/bytecode/src/stackless_bytecode_generator.rs +++ b/language/move-prover/bytecode/src/stackless_bytecode_generator.rs @@ -22,6 +22,7 @@ use move_core_types::{ language_storage::{self, CORE_CODE_ADDRESS}, value::MoveValue, }; +use move_model::ty::ReferenceKind; use move_model::{ ast::{ConditionKind, TempIndex}, model::{FunId, FunctionEnv, Loc, ModuleId, StructId}, @@ -308,10 +309,11 @@ impl<'a> StacklessBytecodeGenerator<'a> { let mutable_ref_index = self.temp_stack.pop().unwrap(); let mutable_ref_sig = self.local_types[mutable_ref_index].clone(); if let Type::Reference(is_mut, signature) = mutable_ref_sig { - if is_mut { + if is_mut == ReferenceKind::Mutable { let immutable_ref_index = self.temp_count; self.temp_stack.push(immutable_ref_index); - self.local_types.push(Type::Reference(false, signature)); + self.local_types + .push(Type::Reference(ReferenceKind::Immutable, signature)); self.code.push(mk_call( Operation::FreezeRef, vec![immutable_ref_index], @@ -342,8 +344,10 @@ impl<'a> StacklessBytecodeGenerator<'a> { )); self.temp_count += 1; let is_mut = matches!(bytecode, MoveBytecode::MutBorrowField(..)); - self.local_types - .push(Type::Reference(is_mut, Box::new(field_type))); + self.local_types.push(Type::Reference( + ReferenceKind::from_is_mut(is_mut), + Box::new(field_type), + )); } MoveBytecode::ImmBorrowFieldGeneric(field_inst_index) @@ -369,8 +373,10 @@ impl<'a> StacklessBytecodeGenerator<'a> { )); self.temp_count += 1; let is_mut = matches!(bytecode, MoveBytecode::MutBorrowFieldGeneric(..)); - self.local_types - .push(Type::Reference(is_mut, Box::new(field_type))); + self.local_types.push(Type::Reference( + ReferenceKind::from_is_mut(is_mut), + Box::new(field_type), + )); } MoveBytecode::LdU8(number) => { @@ -555,7 +561,7 @@ impl<'a> StacklessBytecodeGenerator<'a> { let temp_index = self.temp_count; self.temp_stack.push(temp_index); self.local_types - .push(Type::Reference(true, Box::new(signature))); + .push(Type::Reference(ReferenceKind::Mutable, Box::new(signature))); self.code.push(mk_unary( Operation::BorrowLoc, temp_index, @@ -568,8 +574,10 @@ impl<'a> StacklessBytecodeGenerator<'a> { let signature = self.func_env.get_local_type(*idx as usize); let temp_index = self.temp_count; self.temp_stack.push(temp_index); - self.local_types - .push(Type::Reference(false, Box::new(signature))); + self.local_types.push(Type::Reference( + ReferenceKind::Immutable, + Box::new(signature), + )); self.code.push(mk_unary( Operation::BorrowLoc, temp_index, @@ -1023,7 +1031,7 @@ impl<'a> StacklessBytecodeGenerator<'a> { let operand_index = self.temp_stack.pop().unwrap(); let temp_index = self.temp_count; self.local_types.push(Type::Reference( - is_mut, + ReferenceKind::from_is_mut(is_mut), Box::new(Type::Struct( struct_env.module_env.get_id(), struct_env.get_id(), @@ -1056,7 +1064,7 @@ impl<'a> StacklessBytecodeGenerator<'a> { let temp_index = self.temp_count; let actuals = self.get_type_params(struct_instantiation.type_parameters); self.local_types.push(Type::Reference( - is_mut, + ReferenceKind::from_is_mut(is_mut), Box::new(Type::Struct( struct_env.module_env.get_id(), struct_env.get_id(), @@ -1189,8 +1197,10 @@ impl<'a> StacklessBytecodeGenerator<'a> { let operand2_index = self.temp_stack.pop().unwrap(); let operand1_index = self.temp_stack.pop().unwrap(); let temp_index = self.temp_count; - self.local_types - .push(Type::Reference(is_mut, Box::new(ty.clone()))); + self.local_types.push(Type::Reference( + ReferenceKind::from_is_mut(is_mut), + Box::new(ty.clone()), + )); self.temp_count += 1; self.temp_stack.push(temp_index); let vec_fun = if is_mut { "borrow_mut" } else { "borrow" }; @@ -1261,7 +1271,7 @@ impl<'a> StacklessBytecodeGenerator<'a> { if !operands.is_empty() { let mut_ref_index = self.temp_count; self.local_types.push(Type::Reference( - true, + ReferenceKind::Mutable, Box::new(Type::Vector(Box::new(ty.clone()))), )); self.temp_count += 1; @@ -1292,7 +1302,7 @@ impl<'a> StacklessBytecodeGenerator<'a> { if !temps.is_empty() { let mut_ref_index = self.temp_count; self.local_types.push(Type::Reference( - true, + ReferenceKind::Mutable, Box::new(Type::Vector(Box::new(ty.clone()))), )); self.temp_count += 1; diff --git a/language/move-prover/interpreter/src/concrete/player.rs b/language/move-prover/interpreter/src/concrete/player.rs index b8371c7b97..91da5a6510 100644 --- a/language/move-prover/interpreter/src/concrete/player.rs +++ b/language/move-prover/interpreter/src/concrete/player.rs @@ -18,6 +18,7 @@ use move_core_types::{ language_storage::CORE_CODE_ADDRESS, vm_status::{sub_status, StatusCode}, }; +use move_model::ty::ReferenceKind; use move_model::{ ast::{Exp, MemoryLabel, TempIndex}, model::{FunId, FunctionEnv, ModuleId, StructId}, @@ -2426,7 +2427,7 @@ impl<'env> FunctionContext<'env> { if local_ty != param_decl_ty { assert!(matches!( param_decl_ty, - MT::Type::Reference(false, base_ty) + MT::Type::Reference(ReferenceKind::Immutable, base_ty) if local_ty == base_ty.as_ref())); } let ty = convert_model_local_type(env, local_ty, &self.ty_args); diff --git a/language/move-prover/interpreter/src/concrete/runtime.rs b/language/move-prover/interpreter/src/concrete/runtime.rs index f330a5f99f..f69f0a5d00 100644 --- a/language/move-prover/interpreter/src/concrete/runtime.rs +++ b/language/move-prover/interpreter/src/concrete/runtime.rs @@ -13,6 +13,7 @@ use move_core_types::{ value::MoveValue, vm_status::StatusCode, }; +use move_model::ty::ReferenceKind; use move_model::{ model::{AbilitySet, FunctionEnv, GlobalEnv, TypeParameter}, ty as MT, @@ -136,7 +137,7 @@ fn check_and_convert_type_args_and_args( // TODO (mengxu): clean this up when we no longer accept `&signer` as valid arguments // for transaction scripts and `public(script)` functions. match local_ty { - MT::Type::Reference(false, base_ty) + MT::Type::Reference(ReferenceKind::Immutable, base_ty) if matches!(*base_ty, MT::Type::Primitive(MT::PrimitiveType::Signer)) => { match arg { diff --git a/language/move-prover/interpreter/src/concrete/ty.rs b/language/move-prover/interpreter/src/concrete/ty.rs index 60145f0606..9641323e9d 100644 --- a/language/move-prover/interpreter/src/concrete/ty.rs +++ b/language/move-prover/interpreter/src/concrete/ty.rs @@ -21,6 +21,7 @@ use move_core_types::{ language_storage::{StructTag, TypeTag}, value::{MoveStructLayout, MoveTypeLayout}, }; +use move_model::ty::ReferenceKind; use move_model::{ model::{GlobalEnv, ModuleId, StructId}, ty as MT, @@ -795,9 +796,8 @@ pub fn convert_model_local_type(env: &GlobalEnv, ty: &MT::Type, subst: &[BaseTyp | MT::Type::Vector(..) | MT::Type::Struct(..) | MT::Type::TypeParameter(..) => Type::Base(convert_model_base_type(env, ty, subst)), - MT::Type::Reference(is_mut, base_ty) => { - convert_model_base_type(env, base_ty, subst).into_ref_type(*is_mut) - } + MT::Type::Reference(is_mut, base_ty) => convert_model_base_type(env, base_ty, subst) + .into_ref_type(*is_mut == ReferenceKind::Mutable), _ => unreachable!(), } } diff --git a/language/move-prover/move-abigen/src/abigen.rs b/language/move-prover/move-abigen/src/abigen.rs index c2cc0e4df8..a575bdebe1 100644 --- a/language/move-prover/move-abigen/src/abigen.rs +++ b/language/move-prover/move-abigen/src/abigen.rs @@ -15,6 +15,7 @@ use move_core_types::{ identifier::IdentStr, language_storage::{StructTag, TypeTag}, }; +use move_model::ty::ReferenceKind; use move_model::{ model::{FunctionEnv, GlobalEnv, ModuleEnv}, ty, @@ -189,7 +190,7 @@ impl<'env> Abigen<'env> { .iter() .filter(|param| match ¶m.1 { ty::Type::Primitive(ty::PrimitiveType::Signer) => false, - ty::Type::Reference(false, inner) => { + ty::Type::Reference(ReferenceKind::Immutable, inner) => { !matches!(&**inner, ty::Type::Primitive(ty::PrimitiveType::Signer)) } ty::Type::Struct(module_id, struct_id, _) => { From 2f9c168f9a87b939c571b05e29733afcc29834f4 Mon Sep 17 00:00:00 2001 From: simonjiao Date: Tue, 13 Aug 2024 16:36:33 +0800 Subject: [PATCH 2/2] add todo for function Parameter --- language/move-model/src/model.rs | 2 +- language/move-model/src/ty.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/language/move-model/src/model.rs b/language/move-model/src/model.rs index 554e4b9f9e..68d921f2b3 100644 --- a/language/move-model/src/model.rs +++ b/language/move-model/src/model.rs @@ -2920,7 +2920,7 @@ pub struct AbilityConstraint(pub AbilitySet); /// Represents a parameter. #[derive(Debug, Clone)] -pub struct Parameter(pub Symbol, pub Type); +pub struct Parameter(pub Symbol, pub Type /*TODO(simon),pub Loc*/); #[derive(Debug)] pub struct FunctionData { diff --git a/language/move-model/src/ty.rs b/language/move-model/src/ty.rs index 0a4bd5fd93..a189d4c706 100644 --- a/language/move-model/src/ty.rs +++ b/language/move-model/src/ty.rs @@ -838,7 +838,7 @@ impl TypeUnificationAdapter { treat_rhs_type_param_as_var_after_index: Option, ) -> Self where - I: Iterator + Clone, + I: Iterator + Clone, { debug_assert!( treat_lhs_type_param_as_var_after_index.is_some() @@ -1115,7 +1115,7 @@ impl TypeInstantiationDerivation { mark_irrelevant_param_as_error: bool, ) -> BTreeSet> where - I: Iterator + Clone, + I: Iterator + Clone, { let initial_param_insts: Vec<_> = (0..params_arity) .map(|idx| Type::TypeParameter(idx as TypeParameterIndex))