Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix extended checks #76

Open
wants to merge 2 commits into
base: starcoin-main-v6
Choose a base branch
from
Open

fix extended checks #76

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5efe281
using ReferenceKind instead raw bool type
simonjiao Aug 9, 2024
2f9c168
add todo for function Parameter
simonjiao Aug 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions language/move-model/src/builder/exp_translator.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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::{
Expand Down Expand Up @@ -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),
Expand Down Expand Up @@ -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)),
Expand Down
79 changes: 41 additions & 38 deletions language/move-model/src/model.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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());
}
Expand Down Expand Up @@ -1405,15 +1406,15 @@ impl GlobalEnv {
}

/// Returns an iterator for all modules in the environment.
pub fn get_modules(&self) -> impl Iterator<Item = ModuleEnv<'_>> {
pub fn get_modules(&self) -> impl Iterator<Item=ModuleEnv<'_>> {
self.module_data.iter().map(move |module_data| ModuleEnv {
env: self,
data: module_data,
})
}

/// Returns an iterator for all bytecode modules in the environment.
pub fn get_bytecode_modules(&self) -> impl Iterator<Item = &CompiledModule> {
pub fn get_bytecode_modules(&self) -> impl Iterator<Item=&CompiledModule> {
self.module_data
.iter()
.map(|module_data| &module_data.module)
Expand Down Expand Up @@ -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<Item = NamedConstantEnv<'env>> {
pub fn get_named_constants(&'env self) -> impl Iterator<Item=NamedConstantEnv<'env>> {
self.clone().into_named_constants()
}

/// Returns an iterator over `NamedConstantEnv`s in this module.
pub fn into_named_constants(self) -> impl Iterator<Item = NamedConstantEnv<'env>> {
pub fn into_named_constants(self) -> impl Iterator<Item=NamedConstantEnv<'env>> {
self.data
.named_constants
.iter()
Expand Down Expand Up @@ -2071,12 +2072,12 @@ impl<'env> ModuleEnv<'env> {
}

/// Returns iterator over FunctionEnvs in this module.
pub fn get_functions(&'env self) -> impl Iterator<Item = FunctionEnv<'env>> {
pub fn get_functions(&'env self) -> impl Iterator<Item=FunctionEnv<'env>> {
self.clone().into_functions()
}

/// Returns iterator over FunctionEnvs in this module.
pub fn into_functions(self) -> impl Iterator<Item = FunctionEnv<'env>> {
pub fn into_functions(self) -> impl Iterator<Item=FunctionEnv<'env>> {
self.data
.function_data
.iter()
Expand Down Expand Up @@ -2174,12 +2175,12 @@ impl<'env> ModuleEnv<'env> {
}

/// Returns iterator over structs in this module.
pub fn get_structs(&'env self) -> impl Iterator<Item = StructEnv<'env>> {
pub fn get_structs(&'env self) -> impl Iterator<Item=StructEnv<'env>> {
self.clone().into_structs()
}

/// Returns iterator over structs in this module.
pub fn into_structs(self) -> impl Iterator<Item = StructEnv<'env>> {
pub fn into_structs(self) -> impl Iterator<Item=StructEnv<'env>> {
self.data
.struct_data
.iter()
Expand All @@ -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) => {
Expand Down Expand Up @@ -2285,7 +2288,7 @@ impl<'env> ModuleEnv<'env> {
}

/// Returns specification variables of this module.
pub fn get_spec_vars(&'env self) -> impl Iterator<Item = (&'env SpecVarId, &'env SpecVarDecl)> {
pub fn get_spec_vars(&'env self) -> impl Iterator<Item=(&'env SpecVarId, &'env SpecVarDecl)> {
self.data.spec_vars.iter()
}

Expand All @@ -2304,7 +2307,7 @@ impl<'env> ModuleEnv<'env> {
}

/// Returns specification functions of this module.
pub fn get_spec_funs(&'env self) -> impl Iterator<Item = (&'env SpecFunId, &'env SpecFunDecl)> {
pub fn get_spec_funs(&'env self) -> impl Iterator<Item=(&'env SpecFunId, &'env SpecFunDecl)> {
self.data.spec_funs.iter()
}

Expand All @@ -2329,7 +2332,7 @@ impl<'env> ModuleEnv<'env> {
pub fn get_spec_funs_of_name(
&self,
name: Symbol,
) -> impl Iterator<Item = (&'env SpecFunId, &'env SpecFunDecl)> {
) -> impl Iterator<Item=(&'env SpecFunId, &'env SpecFunDecl)> {
self.data
.spec_funs
.iter()
Expand Down Expand Up @@ -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<Item = FieldEnv<'env>> {
pub fn get_fields(&'env self) -> impl Iterator<Item=FieldEnv<'env>> {
self.data
.field_data
.values()
Expand Down Expand Up @@ -2917,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 {
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -3250,19 +3253,19 @@ 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.
pub fn has_unknown_callers(&self) -> bool {
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
Expand Down
43 changes: 34 additions & 9 deletions language/move-model/src/ty.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,20 +27,48 @@ pub enum Type {
Vector(Box<Type>),
Struct(ModuleId, StructId, Vec<Type>),
TypeParameter(u16),
// todo(simon): change args type to Box<Type>?
Fun(/*args*/ Vec<Type>, /*result*/ Box<Type>),

// Types only appearing in programs.
Reference(bool, Box<Type>),
Reference(ReferenceKind, Box<Type>),

// Types only appearing in specifications
Fun(Vec<Type>, Box<Type>),
TypeDomain(Box<Type>),
ResourceDomain(ModuleId, StructId, Option<Vec<Type>>),

// 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);

Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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"))))
Expand Down Expand Up @@ -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) => {
Expand Down
6 changes: 3 additions & 3 deletions language/move-prover/bytecode/src/eliminate_imm_refs.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {}

Expand Down Expand Up @@ -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
Expand Down
Loading