release 2.0.0 candidate: Python API overhaul

Author: pickx

.circleci/config.yml

@@ -2,11 +2,11 @@ defines:
   smoke-test: &smoke-test
     name: Smoke test
     command: |
-      wget https://raw.githubusercontent.com/Certora/natspecTools/master/tests/basic_tests/definition_test.spec
+      wget https://raw.githubusercontent.com/Certora/cvldocTool/master/tests/basic_tests/definition_test.spec
 
       python -c "import cvldoc_parser
-      parsed = cvldoc_parser.parse([\"definition_test.spec\"])
-      assert len(parsed[0]) == 3, \"should parse to 3 elements\""
+      parsed = cvldoc_parser.parse(\"definition_test.spec\")
+      assert len(parsed) == 3, \"should parse to 3 elements\""
 
   store-and-persist:
     - store_artifacts: &store-wheel

.gitignore

@@ -2,4 +2,4 @@
 **/Cargo.lock
 **/.DS_Store
 BUGS
-**/python_wrapper/.env
+**/.env

CHANGELOG.md

@@ -1,4 +1,13 @@
 # Changelog
+## [2.0.0] - 2023-09-13
+### Added
+- Support parsing of `hook`, `use`, `using`, `import` statements.
+- Python module API has been simplified.
+### Changed
+- CVL2 syntax is now enforced. Parsing of code which is not compliant with CVL2 has been removed.
+### Fixed
+- Some issues with `Invariant` parsing have been fixed.
+
 ## [1.0.3] - 2023-05-27
 ### Fixed
 - Fix issue that could cause infinite recursion on certain input

Cargo.toml

@@ -1,17 +1,17 @@
 [package]
 name = "cvldoc_parser_core"
-version = "1.0.3"
+version = "2.0.0"
 edition = "2021"
 
 [dependencies]
 assert_matches = "1.5.0"
 chumsky = "0.9.2"
 color-eyre = "0.6.2"
-indoc = "2.0.1"
-itertools = "0.10.5"
+indoc = "2"
+itertools = "0.11"
 lsp-types = "0.94.0"
 once_cell = "1.17.1"
-regex = "1.8.2"
+regex = "1"
 ropey = "1.6.0"
-serde = { version = "1.0.163", features = ["derive"] }
-tap = "1.0.1"
+serde = { version = "1", features = ["derive"] }
+tap = "1"

src/diagnostics.rs

@@ -10,10 +10,10 @@ impl Ast {
             Ast::Invariant { .. } => &[Title, Notice, Dev, Param],
             Ast::Function { .. } => &[Notice, Dev, Param, Return],
             Ast::Definition { .. } => &[Notice, Dev, Param, Return],
-            Ast::Ghost { .. } | Ast::GhostMapping { .. } => &[Notice, Dev, Param, Return],
+            Ast::GhostFunction { .. } | Ast::GhostMapping { .. } => &[Notice, Dev, Param, Return],
             Ast::Methods { .. } => &[Notice, Dev],
             Ast::FreeFormComment { .. } => &[Notice, Dev],
-            Ast::Import(..)
+            Ast::Import { .. }
             | Ast::Using { .. }
             | Ast::UseRule { .. }
             | Ast::UseBuiltinRule { .. }
@@ -42,6 +42,7 @@ const WARNING: DiagnosticSeverity = DiagnosticSeverity::WARNING;
 const ERROR: DiagnosticSeverity = DiagnosticSeverity::ERROR;
 
 enum DiagSpan<'a> {
+    #[allow(unused)]
     EntireDoc,
     SingleTag(&'a DocumentationTag),
 }
@@ -50,58 +51,60 @@ impl CvlElement {
     pub fn enumerate_diagnostics(&self, converter: RangeConverter) -> Vec<Diagnostic> {
         let mut diagnostics = Vec::new();
 
-        if let Some(doc) = &self.doc {
-            let mut add = |message, diag_span, severity| {
-                let span = match diag_span {
-                    DiagSpan::EntireDoc => self.element_span.clone(),
-                    DiagSpan::SingleTag(tag) => tag.span.clone(),
-                };
+        let mut add = |message, diag_span, severity| {
+            let span = match diag_span {
+                DiagSpan::EntireDoc => self.element_span.clone(),
+                DiagSpan::SingleTag(tag) => tag.span.clone(),
+            };
 
-                let diag = Diagnostic {
-                    range: converter.to_range(span),
-                    severity: Some(severity),
-                    message,
-                    ..Default::default()
-                };
-                diagnostics.push(diag);
+            let diag = Diagnostic {
+                range: converter.to_range(span),
+                severity: Some(severity),
+                message,
+                ..Default::default()
             };
+            diagnostics.push(diag);
+        };
 
-            if doc.iter().all(|tag| tag.kind != TagKind::Notice) {
-                //Any applicable item is missing a notice
-                let message = "associated element is undocumented".to_string();
-                add(message, DiagSpan::EntireDoc, WARNING);
-            }
+        // disabled for now. this diagnostic is overly broad.
+        // if self.doc.iter().all(|tag| tag.kind != TagKind::Notice) {
+        //     //Any applicable item is missing a notice
+        //     let message = "associated element is undocumented".to_string();
+        //     add(message, DiagSpan::EntireDoc, WARNING);
+        // }
 
-            let tags_with_params = doc.iter().filter_map(|tag| {
-                let param = tag.param_name()?;
-                Some((tag, param))
-            });
+        let tags_with_params = self.doc.iter().filter_map(|tag| {
+            let param = tag.param_name()?;
+            Some((tag, param))
+        });
 
-            for (i, (tag, param)) in tags_with_params.enumerate() {
-                if !self.ast.defines_param(param) {
-                    //A @param is provided for a non-existent parameter
-                    let message = format!("no such parameter: {param}");
-                    add(message, DiagSpan::SingleTag(tag), ERROR);
-                } else if doc[..i].iter().any(|tag| tag.param_name() == Some(param)) {
-                    //Each parameter must be documented at most once
-                    let message = "parameter is already documented".to_string();
-                    add(message, DiagSpan::SingleTag(tag), ERROR);
-                }
+        for (i, (tag, param)) in tags_with_params.enumerate() {
+            if !self.ast.defines_param(param) {
+                //A @param is provided for a non-existent parameter
+                let message = format!("no such parameter: {param}");
+                add(message, DiagSpan::SingleTag(tag), ERROR);
+            } else if self.doc[..i]
+                .iter()
+                .any(|tag| tag.param_name() == Some(param))
+            {
+                //Each parameter must be documented at most once
+                let message = "parameter is already documented".to_string();
+                add(message, DiagSpan::SingleTag(tag), ERROR);
             }
+        }
 
-            for tag in doc {
-                if !self.ast.supports(&tag.kind) {
-                    let message = format!("this tag is unsupported for {} blocks", self.ast);
-                    add(message, DiagSpan::SingleTag(tag), ERROR);
-                }
+        for tag in &self.doc {
+            if !self.ast.supports(&tag.kind) {
+                let message = format!("this tag is unsupported for {} blocks", self.ast);
+                add(message, DiagSpan::SingleTag(tag), ERROR);
             }
+        }
 
-            for tag in doc {
-                if let TagKind::Unexpected(unexpected_tag) = &tag.kind {
-                    //Unrecognized tags appear anywhere
-                    let message = format!("@{unexpected_tag} is unrecognized");
-                    add(message, DiagSpan::SingleTag(tag), WARNING);
-                }
+        for tag in &self.doc {
+            if let TagKind::Unexpected(unexpected_tag) = &tag.kind {
+                //Unrecognized tags appear anywhere
+                let message = format!("@{unexpected_tag} is unrecognized");
+                add(message, DiagSpan::SingleTag(tag), WARNING);
             }
         }
 

src/lib.rs

@@ -2,16 +2,18 @@ pub mod diagnostics;
 pub mod parse;
 pub mod util;
 
+use serde::Serialize;
 use std::fmt::{Debug, Display};
 use std::sync::Arc;
 use util::{ByteSpan, Span};
 
-#[derive(Clone, PartialEq, Eq)]
+#[derive(Clone, PartialEq, Eq, Serialize)]
 pub struct CvlElement {
-    pub doc: Option<Vec<DocumentationTag>>,
+    pub doc: Vec<DocumentationTag>,
     pub ast: Ast,
     pub element_span: Span,
     pub doc_span: Option<Span>,
+    #[serde(skip)]
     pub src: Arc<str>,
 }
 
@@ -26,7 +28,7 @@ impl Debug for CvlElement {
     }
 }
 
-#[derive(Clone, Debug, PartialEq, Eq)]
+#[derive(Clone, Debug, PartialEq, Eq, Serialize)]
 pub struct Param {
     pub ty: String,
     pub name: String,
@@ -40,7 +42,8 @@ impl Param {
     }
 }
 
-#[derive(Debug, Clone, PartialEq, Eq)]
+#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
+#[serde(tag = "type")]
 pub enum Ast {
     FreeFormComment {
         text: String,
@@ -70,7 +73,7 @@ pub enum Ast {
         returns: String,
         definition: String,
     },
-    Ghost {
+    GhostFunction {
         name: String,
         ty_list: Vec<String>,
         returns: String,
@@ -84,7 +87,9 @@ pub enum Ast {
     Methods {
         block: String,
     },
-    Import(String),
+    Import {
+        imported: String,
+    },
     Using {
         contract_name: String,
         spec_name: String,
@@ -125,14 +130,14 @@ pub enum Ast {
 
 impl CvlElement {
     pub fn title(&self) -> Option<String> {
-        let from_title_tag = self.doc.iter().flatten().find_map(|tag| {
-            if tag.kind == TagKind::Title {
+        let from_title_tag = self.doc.iter().find_map(|tag| {
+            if matches!(tag.kind, TagKind::Title) {
                 Some(tag.description.clone())
             } else {
                 None
             }
         });
-        let from_name = || self.ast.name().map(String::from);
+        let from_name = || self.ast.name().map(ToOwned::to_owned);
 
         from_title_tag.or_else(from_name)
     }
@@ -154,7 +159,7 @@ impl CvlElement {
     }
 }
 
-#[derive(Debug, Clone, PartialEq, Eq)]
+#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
 pub struct DocumentationTag {
     pub kind: TagKind,
     pub description: String,
@@ -192,7 +197,7 @@ impl DocumentationTag {
     }
 }
 
-#[derive(Debug, PartialEq, Eq, Clone, Hash, Default)]
+#[derive(Debug, PartialEq, Eq, Clone, Hash, Default, Serialize)]
 pub enum TagKind {
     Title,
     #[default]
@@ -275,10 +280,10 @@ impl Display for Ast {
             Ast::Invariant { .. } => "invariant",
             Ast::Function { .. } => "function",
             Ast::Definition { .. } => "definition",
-            Ast::Ghost { .. } | Ast::GhostMapping { .. } => "ghost",
+            Ast::GhostFunction { .. } | Ast::GhostMapping { .. } => "ghost",
             Ast::Methods { .. } => "methods",
             Ast::FreeFormComment { .. } => "freeform comment",
-            Ast::Import(..) => "import",
+            Ast::Import { .. } => "import",
             Ast::Using { .. } => "using",
             Ast::UseRule { .. } | Ast::UseBuiltinRule { .. } | Ast::UseInvariant { .. } => "use",
             Ast::HookSload { .. }
@@ -298,7 +303,7 @@ impl Ast {
             | Ast::Invariant { name, .. }
             | Ast::Function { name, .. }
             | Ast::Definition { name, .. }
-            | Ast::Ghost { name, .. }
+            | Ast::GhostFunction { name, .. }
             | Ast::GhostMapping { name, .. } => Some(name.as_str()),
             _ => None,
         }
@@ -325,7 +330,7 @@ impl Ast {
             | Ast::HookOpcode { block, .. } => Some(block.as_str()),
 
             Ast::Invariant { proof: block, .. }
-            | Ast::Ghost { axioms: block, .. }
+            | Ast::GhostFunction { axioms: block, .. }
             | Ast::GhostMapping { axioms: block, .. } => block.as_ref().map(String::as_str),
 
             _ => None,
@@ -334,15 +339,17 @@ impl Ast {
 
     pub fn returns(&self) -> Option<&str> {
         match self {
-            Ast::Function { returns, .. } => returns.as_ref().map(String::as_str),
-            Ast::Definition { returns, .. } | Ast::Ghost { returns, .. } => Some(returns.as_str()),
+            Ast::Function { returns, .. } => returns.as_deref(),
+            Ast::Definition { returns, .. } | Ast::GhostFunction { returns, .. } => {
+                Some(returns.as_str())
+            }
             _ => None,
         }
     }
 
     pub fn ty_list(&self) -> Option<&[String]> {
         match self {
-            Ast::Ghost { ty_list, .. } => Some(ty_list),
+            Ast::GhostFunction { ty_list, .. } => Some(ty_list),
             _ => None,
         }
     }