verify => spec

MystenLabs · Dec 20, 2024 · 186b201 · 186b201
1 parent 30cd739
commit 186b201
Show file tree

Hide file tree

Showing 7 changed files with 28 additions and 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
@@ -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
@@ -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<H::Var, VarInfo>,
-}
-
 #[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
@@ -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
@@ -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
@@ -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<AttributePosition> {
         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<TestingAttribute> for KnownAttribute {
         Self::Testing(a)
     }
 }
-impl From<VerificationAttribute> for KnownAttribute {
-    fn from(a: VerificationAttribute) -> Self {
-        Self::Verification(a)
+impl From<SpecAttribute> for KnownAttribute {
+    fn from(a: SpecAttribute) -> Self {
+        Self::Spec(a)
     }
 }
 impl From<NativeAttribute> 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
@@ -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
@@ -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(_)