Skip to content

Commit

Permalink
a few changes inspired by Wolfgang's last review
Browse files Browse the repository at this point in the history
  • Loading branch information
brmataptos committed Aug 14, 2023
1 parent de3b872 commit b0d354e
Show file tree
Hide file tree
Showing 6 changed files with 68 additions and 51 deletions.
17 changes: 9 additions & 8 deletions aptos-move/framework/src/extended_checks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -45,17 +45,18 @@ pub fn get_all_attribute_names() -> &'static BTreeSet<String> {
VIEW_FUN_ATTRIBUTE,
];

fn add_attribute_names(table: &mut BTreeSet<String>) {
for str in ALL_ATTRIBUTE_NAMES {
table.insert(str.to_string());
}
fn extended_attribute_names() -> BTreeSet<String> {
ALL_ATTRIBUTE_NAMES
.into_iter()
.map(|s| s.to_string())
.collect::<BTreeSet<String>>()
}

static KNOWN_ATTRIBUTES_SET: Lazy<BTreeSet<String>> = Lazy::new(|| {
use known_attributes::AttributeKind;
let mut known_attributes = BTreeSet::new();
known_attributes::KnownAttribute::add_attribute_names(&mut known_attributes);
add_attribute_names(&mut known_attributes);
known_attributes
let mut attributes = extended_attribute_names();
known_attributes::KnownAttribute::add_attribute_names(&mut attributes);
attributes
});
&KNOWN_ATTRIBUTES_SET
}
Expand Down
27 changes: 16 additions & 11 deletions third_party/move/move-compiler/src/attr_derivation/async_deriver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,17 +35,22 @@ const GENERATED_SEND_ATTR: &str = "_generated_send";

const MAX_SEND_PARAM_COUNT: usize = 8;

pub(crate) fn add_attributes_for_async(known_attributes: &mut BTreeSet<String>) {
known_attributes.insert(ACTOR_ATTR.to_string());
known_attributes.insert(CONT_ATTR.to_string());
known_attributes.insert(EVENT_ATTR.to_string());
known_attributes.insert(INIT_ATTR.to_string());
known_attributes.insert(MESSAGE_ATTR.to_string());
known_attributes.insert(RPC_ATTR.to_string());
known_attributes.insert(STATE_ATTR.to_string());
known_attributes.insert(GENERATED_CONT_ATTR.to_string());
known_attributes.insert(GENERATED_RPC_ATTR.to_string());
known_attributes.insert(GENERATED_SEND_ATTR.to_string());
pub(crate) fn add_attributes_for_async(attributes: &mut BTreeSet<String>) {
const ALL_ATTRIBUTE_NAMES: [&str; 10] = [
ACTOR_ATTR,
CONT_ATTR,
EVENT_ATTR,
INIT_ATTR,
MESSAGE_ATTR,
RPC_ATTR,
STATE_ATTR,
GENERATED_CONT_ATTR,
GENERATED_RPC_ATTR,
GENERATED_SEND_ATTR,
];
ALL_ATTRIBUTE_NAMES.into_iter().for_each(|elt| {
attributes.insert(elt.to_string());
});
}

pub(crate) fn derive_for_async(
Expand Down
61 changes: 32 additions & 29 deletions third_party/move/move-compiler/src/attr_derivation/evm_deriver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -43,35 +43,38 @@ const RECEIVE_ATTR: &str = "receive";
const VIEW_ATTR: &str = "view";
const PURE_ATTR: &str = "pure";

pub(crate) fn add_attributes_for_evm(known_attributes: &mut BTreeSet<String>) {
known_attributes.insert(CALLABLE_ATTR.to_string());
known_attributes.insert(CONTRACT_ATTR.to_string());
known_attributes.insert(EXTERNAL_ATTR.to_string());

known_attributes.insert(ABI_STRUCT_ATTR.to_string());
known_attributes.insert(ACTOR_ATTR.to_string());
known_attributes.insert(CREATE_ATTR.to_string());
known_attributes.insert(DECODE_ATTR.to_string());
known_attributes.insert(DELETE_ATTR.to_string());
known_attributes.insert(ENCODE_ATTR.to_string());
known_attributes.insert(ENCODE_PACKED_ATTR.to_string());
known_attributes.insert(EVENT_ATTR.to_string());
known_attributes.insert(EVM_ARITH_ATTR.to_string());
known_attributes.insert(EVM_TEST_ATTR.to_string());
known_attributes.insert(FALLBACK_ATTR.to_string());
known_attributes.insert(INIT_ATTR.to_string());
known_attributes.insert(INTERFACE_ATTR.to_string());
known_attributes.insert(INTERFACE_ID_ATTR.to_string());
known_attributes.insert(MESSAGE_ATTR.to_string());
known_attributes.insert(SELECTOR_ATTR.to_string());
known_attributes.insert(STATE_ATTR.to_string());
known_attributes.insert(STORAGE_ATTR.to_string());

known_attributes.insert(EVM_CONTRACT_ATTR.to_string());
known_attributes.insert(PAYABLE_ATTR.to_string());
known_attributes.insert(RECEIVE_ATTR.to_string());
known_attributes.insert(VIEW_ATTR.to_string());
known_attributes.insert(PURE_ATTR.to_string());
pub(crate) fn add_attributes_for_evm(attributes: &mut BTreeSet<String>) {
const ALL_ATTRIBUTE_NAMES: [&str; 26] = [
CALLABLE_ATTR,
CONTRACT_ATTR,
EXTERNAL_ATTR,
ABI_STRUCT_ATTR,
ACTOR_ATTR,
CREATE_ATTR,
DECODE_ATTR,
DELETE_ATTR,
ENCODE_ATTR,
ENCODE_PACKED_ATTR,
EVENT_ATTR,
EVM_ARITH_ATTR,
EVM_TEST_ATTR,
FALLBACK_ATTR,
INIT_ATTR,
INTERFACE_ATTR,
INTERFACE_ID_ATTR,
MESSAGE_ATTR,
SELECTOR_ATTR,
STATE_ATTR,
STORAGE_ATTR,
EVM_CONTRACT_ATTR,
PAYABLE_ATTR,
RECEIVE_ATTR,
VIEW_ATTR,
PURE_ATTR,
];
ALL_ATTRIBUTE_NAMES.into_iter().for_each(|elt| {
attributes.insert(elt.to_string());
});
}

pub(crate) fn derive_for_evm(
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
module aptos_std::M {
// Test that warnings about unknown "#[testonly]" attribute is
// suppressed in apts_std module.
module aptos_std::module_with_suppressed_warnings {
#[a, a(x = 0)]
fun foo() {}

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
module aptos_std::M {
// Test that warnings about unknown "#[testonly]" attribute is
// suppressed in apts_std module.
module aptos_std::module_with_suppressed_warnings {
#[a, a(x = 0)]
fun foo() {}

Expand Down
6 changes: 5 additions & 1 deletion third_party/move/move-prover/lab/src/benchmark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ use clap::{
use codespan_reporting::term::termcolor::{ColorChoice, StandardStream};
use itertools::Itertools;
use log::LevelFilter;
use move_compiler::shared::PackagePaths;
use move_compiler::shared::{known_attributes::KnownAttribute, PackagePaths};
use move_model::{
model::{FunctionEnv, GlobalEnv, ModuleEnv, VerificationScope},
parse_addresses_from_options, run_model_builder_with_options,
Expand Down Expand Up @@ -150,6 +150,8 @@ fn run_benchmark(
};
let addrs = parse_addresses_from_options(options.move_named_address_values.clone())?;
options.move_deps.append(&mut dep_dirs.to_vec());
let skip_attribute_checks = true;
let known_attributes = KnownAttribute::get_all_attribute_names().clone();
let env = run_model_builder_with_options(
vec![PackagePaths {
name: None,
Expand All @@ -162,6 +164,8 @@ fn run_benchmark(
named_address_map: addrs,
}],
options.model_builder.clone(),
skip_attribute_checks,
&known_attributes,
)?;
let mut error_writer = StandardStream::stderr(ColorChoice::Auto);

Expand Down

0 comments on commit b0d354e

Please sign in to comment.