From 186b2012d478ec5ec81a28bd147cbc04a3a54689 Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Fri, 20 Dec 2024 14:19:20 -0800 Subject: [PATCH] verify => spec --- .../move-compiler/src/command_line/mod.rs | 3 +-- .../crates/move-compiler/src/compiled_unit.rs | 7 ----- .../move-compiler/src/expansion/translate.rs | 2 +- .../parser/verification_attribute_filter.rs | 13 ++++------ .../src/shared/known_attributes.rs | 26 +++++++++---------- .../crates/move-compiler/src/shared/mod.rs | 15 +++++------ .../src/unit_test/filter_test_members.rs | 2 +- 7 files changed, 28 insertions(+), 40 deletions(-) diff --git a/external-crates/move/crates/move-compiler/src/command_line/mod.rs b/external-crates/move/crates/move-compiler/src/command_line/mod.rs index 954d376242c6b..1223a7bd81c48 100644 --- a/external-crates/move/crates/move-compiler/src/command_line/mod.rs +++ b/external-crates/move/crates/move-compiler/src/command_line/mod.rs @@ -26,8 +26,7 @@ pub const SOURCE_MAP_SHORT: char = 'm'; pub const TEST: &str = "test"; pub const TEST_SHORT: char = 't'; -pub const VERIFY: &str = "verify"; -pub const VERIFY_SHORT: char = 'v'; +pub const SPEC: &str = "verify"; pub const WARNINGS_ARE_ERRORS: &str = "warnings-are-errors"; diff --git a/external-crates/move/crates/move-compiler/src/compiled_unit.rs b/external-crates/move/crates/move-compiler/src/compiled_unit.rs index 4011c30e568ac..aaad99430e312 100644 --- a/external-crates/move/crates/move-compiler/src/compiled_unit.rs +++ b/external-crates/move/crates/move-compiler/src/compiled_unit.rs @@ -29,13 +29,6 @@ pub struct VarInfo { pub index: F::LocalIndex, } -#[derive(Debug, Clone)] -pub struct SpecInfo { - pub offset: F::CodeOffset, - // Free locals that are used but not declared in the block - pub used_locals: UniqueMap, -} - #[derive(Debug, Clone)] pub struct FunctionInfo { pub parameters: Vec<(H::Var, VarInfo)>, diff --git a/external-crates/move/crates/move-compiler/src/expansion/translate.rs b/external-crates/move/crates/move-compiler/src/expansion/translate.rs index 8071f0c28b3a0..6f42400daebbe 100644 --- a/external-crates/move/crates/move-compiler/src/expansion/translate.rs +++ b/external-crates/move/crates/move-compiler/src/expansion/translate.rs @@ -1141,7 +1141,7 @@ fn known_attributes( fn gate_known_attribute(context: &mut Context, loc: Loc, known: &KnownAttribute) { match known { KnownAttribute::Testing(_) - | KnownAttribute::Verification(_) + | KnownAttribute::Spec(_) | KnownAttribute::Native(_) | KnownAttribute::Diagnostic(_) | KnownAttribute::DefinesPrimitive(_) diff --git a/external-crates/move/crates/move-compiler/src/parser/verification_attribute_filter.rs b/external-crates/move/crates/move-compiler/src/parser/verification_attribute_filter.rs index 49ce5f03343b1..93478cc230b8e 100644 --- a/external-crates/move/crates/move-compiler/src/parser/verification_attribute_filter.rs +++ b/external-crates/move/crates/move-compiler/src/parser/verification_attribute_filter.rs @@ -48,15 +48,14 @@ impl FilterContext for Context<'_> { // An AST element should be removed if: // * It is annotated #[spec_only] and verify mode is not set fn should_remove_by_attributes(&mut self, attrs: &[P::Attributes]) -> bool { - if self.env.flags().is_verifying() { + if self.env.flags().is_spec() { return false; } - use known_attributes::VerificationAttribute; + use known_attributes::SpecAttribute; let flattened_attrs: Vec<_> = attrs.iter().flat_map(verification_attributes).collect(); // let is_spec_only = flattened_attrs.iter().find(|(_, attr)| { - matches!(attr, VerificationAttribute::SpecOnly) - || matches!(attr, VerificationAttribute::Spec) + matches!(attr, SpecAttribute::SpecOnly) || matches!(attr, SpecAttribute::Spec) }); self.has_spec_code = self.has_spec_code || is_spec_only.is_some(); is_spec_only.is_some() @@ -120,16 +119,14 @@ pub fn program(compilation_env: &CompilationEnv, prog: P::Program) -> P::Program filter_program(&mut context, prog) } -fn verification_attributes( - attrs: &P::Attributes, -) -> Vec<(Loc, known_attributes::VerificationAttribute)> { +fn verification_attributes(attrs: &P::Attributes) -> Vec<(Loc, known_attributes::SpecAttribute)> { use known_attributes::KnownAttribute; attrs .value .iter() .filter_map( |attr| match KnownAttribute::resolve(attr.value.attribute_name().value)? { - KnownAttribute::Verification(verify_attr) => Some((attr.loc, verify_attr)), + KnownAttribute::Spec(verify_attr) => Some((attr.loc, verify_attr)), _ => None, }, ) diff --git a/external-crates/move/crates/move-compiler/src/shared/known_attributes.rs b/external-crates/move/crates/move-compiler/src/shared/known_attributes.rs index 4923212e85b59..689f46f78a315 100644 --- a/external-crates/move/crates/move-compiler/src/shared/known_attributes.rs +++ b/external-crates/move/crates/move-compiler/src/shared/known_attributes.rs @@ -20,7 +20,7 @@ pub enum AttributePosition { #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] pub enum KnownAttribute { Testing(TestingAttribute), - Verification(VerificationAttribute), + Spec(SpecAttribute), Native(NativeAttribute), Diagnostic(DiagnosticAttribute), DefinesPrimitive(DefinesPrimitive), @@ -43,7 +43,7 @@ pub enum TestingAttribute { } #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] -pub enum VerificationAttribute { +pub enum SpecAttribute { // Denotes a function is a spec Spec, // Focus on this function, deactivates verification for all other functions @@ -102,9 +102,9 @@ impl KnownAttribute { TestingAttribute::TEST_ONLY => TestingAttribute::TestOnly.into(), TestingAttribute::EXPECTED_FAILURE => TestingAttribute::ExpectedFailure.into(), TestingAttribute::RAND_TEST => TestingAttribute::RandTest.into(), - VerificationAttribute::SPEC => VerificationAttribute::Spec.into(), - VerificationAttribute::SPEC_ONLY => VerificationAttribute::SpecOnly.into(), - VerificationAttribute::FOCUS => VerificationAttribute::Focus.into(), + SpecAttribute::SPEC => SpecAttribute::Spec.into(), + SpecAttribute::SPEC_ONLY => SpecAttribute::SpecOnly.into(), + SpecAttribute::FOCUS => SpecAttribute::Focus.into(), NativeAttribute::BYTECODE_INSTRUCTION => NativeAttribute::BytecodeInstruction.into(), DiagnosticAttribute::ALLOW => DiagnosticAttribute::Allow.into(), DiagnosticAttribute::LINT_ALLOW => DiagnosticAttribute::LintAllow.into(), @@ -120,7 +120,7 @@ impl KnownAttribute { pub const fn name(&self) -> &str { match self { Self::Testing(a) => a.name(), - Self::Verification(a) => a.name(), + Self::Spec(a) => a.name(), Self::Native(a) => a.name(), Self::Diagnostic(a) => a.name(), Self::DefinesPrimitive(a) => a.name(), @@ -134,7 +134,7 @@ impl KnownAttribute { pub fn expected_positions(&self) -> &'static BTreeSet { match self { Self::Testing(a) => a.expected_positions(), - Self::Verification(a) => a.expected_positions(), + Self::Spec(a) => a.expected_positions(), Self::Native(a) => a.expected_positions(), Self::Diagnostic(a) => a.expected_positions(), Self::DefinesPrimitive(a) => a.expected_positions(), @@ -203,7 +203,7 @@ impl TestingAttribute { } } -impl VerificationAttribute { +impl SpecAttribute { pub const SPEC: &'static str = "spec"; pub const SPEC_ONLY: &'static str = "spec_only"; pub const FOCUS: &'static str = "focus"; @@ -393,7 +393,7 @@ impl fmt::Display for KnownAttribute { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Self::Testing(a) => a.fmt(f), - Self::Verification(a) => a.fmt(f), + Self::Spec(a) => a.fmt(f), Self::Native(a) => a.fmt(f), Self::Diagnostic(a) => a.fmt(f), Self::DefinesPrimitive(a) => a.fmt(f), @@ -411,7 +411,7 @@ impl fmt::Display for TestingAttribute { } } -impl fmt::Display for VerificationAttribute { +impl fmt::Display for SpecAttribute { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "{}", self.name()) } @@ -468,9 +468,9 @@ impl From for KnownAttribute { Self::Testing(a) } } -impl From for KnownAttribute { - fn from(a: VerificationAttribute) -> Self { - Self::Verification(a) +impl From for KnownAttribute { + fn from(a: SpecAttribute) -> Self { + Self::Spec(a) } } impl From for KnownAttribute { diff --git a/external-crates/move/crates/move-compiler/src/shared/mod.rs b/external-crates/move/crates/move-compiler/src/shared/mod.rs index 8668debf2cd38..14d12e5d2bd3b 100644 --- a/external-crates/move/crates/move-compiler/src/shared/mod.rs +++ b/external-crates/move/crates/move-compiler/src/shared/mod.rs @@ -607,10 +607,9 @@ pub struct Flags { /// Compile in verify mode #[clap( - short = cli::VERIFY_SHORT, - long = cli::VERIFY, + long = cli::SPEC, )] - verify: bool, + spec: bool, /// If set, warnings become errors. #[clap( @@ -664,7 +663,7 @@ impl Flags { pub fn empty() -> Self { Self { test: false, - verify: false, + spec: false, shadow: false, bytecode_version: None, warnings_are_errors: false, @@ -679,7 +678,7 @@ impl Flags { pub fn testing() -> Self { Self { test: true, - verify: false, + spec: false, shadow: false, bytecode_version: None, warnings_are_errors: false, @@ -693,7 +692,7 @@ impl Flags { pub fn set_verify(self, value: bool) -> Self { Self { - verify: value, + spec: value, ..self } } @@ -755,8 +754,8 @@ impl Flags { self.test } - pub fn is_verifying(&self) -> bool { - self.verify + pub fn is_spec(&self) -> bool { + self.spec } pub fn keep_testing_functions(&self) -> bool { diff --git a/external-crates/move/crates/move-compiler/src/unit_test/filter_test_members.rs b/external-crates/move/crates/move-compiler/src/unit_test/filter_test_members.rs index b0f62859233be..0aad7ff9ddd29 100644 --- a/external-crates/move/crates/move-compiler/src/unit_test/filter_test_members.rs +++ b/external-crates/move/crates/move-compiler/src/unit_test/filter_test_members.rs @@ -247,7 +247,7 @@ fn test_attributes(attrs: &P::Attributes) -> Vec<(Loc, known_attributes::Testing .filter_map( |attr| match KnownAttribute::resolve(attr.value.attribute_name().value)? { KnownAttribute::Testing(test_attr) => Some((attr.loc, test_attr)), - KnownAttribute::Verification(_) + KnownAttribute::Spec(_) | KnownAttribute::Native(_) | KnownAttribute::Diagnostic(_) | KnownAttribute::DefinesPrimitive(_)