Add a simplified harness for testing parsing and lifting to VST (#37)

Also improves the handling of Verus's trigger attributes.
verus-lang · Oct 31, 2024 · b7b9518 · b7b9518
1 parent 64bbeb0
commit b7b9518
Show file tree

Hide file tree

Showing 18 changed files with 272 additions and 103 deletions.
diff --git a/.vscode/launch.json b/.vscode/launch.json
@@ -9,6 +9,21 @@
 
   "version": "0.2.0",
   "configurations": [
+    {
+      // Used for testing the Verus Analyzer server.
+      "name": "Debug Verus Analyzer server",
+      "type": "lldb",
+      "request": "launch",
+      "program": "${workspaceFolder}/target/debug/va-test",
+      "sourceLanguages": [
+        "rust"
+      ],
+      "args": [
+        "${workspaceFolder}/crates/va-test/examples/trigger-bug"
+        //"${workspaceFolder}/crates/va-test/examples/vstd-dep"
+      ],
+      "preLaunchTask": "Build Server",
+    },
     {
       // Used for testing the extension with the installed LSP server.
       "name": "Run Installed Extension",

diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -12,7 +12,7 @@ authors = ["rust-analyzer team"]
 [profile.dev]
 # Disabling debug info speeds up builds a bunch,
 # and we don't rely on it for debugging that much.
-debug = 0
+debug = 2
 
 [profile.dev.package]
 # These speed up local tests.
@@ -82,6 +82,7 @@ syntax = { path = "./crates/syntax", version = "0.0.0" }
 text-edit = { path = "./crates/text-edit", version = "0.0.0" }
 toolchain = { path = "./crates/toolchain", version = "0.0.0" }
 tt = { path = "./crates/tt", version = "0.0.0" }
+va-test = { path = "./crates/va-test", version = "0.0.0" }
 vfs-notify = { path = "./crates/vfs-notify", version = "0.0.0" }
 vfs = { path = "./crates/vfs", version = "0.0.0" }
 

diff --git a/crates/parser/src/grammar/attributes.rs b/crates/parser/src/grammar/attributes.rs
@@ -16,32 +16,6 @@ pub(super) fn outer_attrs(p: &mut Parser<'_>) {
 
 fn attr(p: &mut Parser<'_>, inner: bool) {
     assert!(p.at(T![#]));
-
-    //verus custom trigger attribute
-    // verus trigger attribute is custom syntax
-    // Reference https://github.com/verus-lang/verus/blob/4ef61030aadc4fd66b62f3614f36e3b64e89b855/source/builtin_macros/src/syntax.rs#L1808
-    // Note that verus! macro compares the attributes name with "trigger", and process it
-    // However, the rust-analyzer parser does not have access to string's content.
-    // Therefore, to make a new syntax kind (e.g. TriggerAttribute),
-    // we need to register `trigger` as a reserved keyword.
-    // however, by registering `trigger` as a reserved keyword,
-    // single trigger attribute, which is `#[trigger]` becomes invalid syntax.
-    // therefore, we just special-case `#[trigger]`
-    if p.nth(1) == T![!] && p.nth(2) == T!['['] && p.nth(3) == T![trigger] {
-        verus::trigger_attribute(p);
-        return;
-    }
-    // verus -- #[trigger]
-    if p.nth(1) == T!['['] && p.nth(2) == T![trigger] {
-        let attr = p.start();
-        p.expect(T![#]);
-        p.expect(T!['[']);
-        p.expect(T![trigger]);
-        p.expect(T![']']);
-        attr.complete(p, ERROR);
-        return;
-    }
-
     let attr = p.start();
     p.bump(T![#]);
 
@@ -50,7 +24,11 @@ fn attr(p: &mut Parser<'_>, inner: bool) {
     }
 
     if p.eat(T!['[']) {
-        meta(p);
+        if p.at(T![trigger]) {
+            verus::trigger_attribute(p, inner);
+        } else {
+            meta(p);
+        }
 
         if !p.eat(T![']']) {
             p.error("expected `]`");

diff --git a/crates/parser/src/grammar/verus.rs b/crates/parser/src/grammar/verus.rs
@@ -473,28 +473,25 @@ fn comma_cond(p: &mut Parser<'_>) -> () {
     expressions::expr_no_struct(p);
 }
 
-pub(crate) fn trigger_attribute(p: &mut Parser<'_>) -> CompletedMarker {
+pub(crate) fn trigger_attribute(p: &mut Parser<'_>, inner:bool) -> CompletedMarker {
     let m = p.start();
-    p.expect(T![#]);
-    p.expect(T![!]);
-    p.expect(T!['[']);
-
     p.expect(T![trigger]);
-    expressions::expr_no_struct(p);
-    while !p.at(EOF) && !p.at(T![']']) {
-        if !p.at(T![,]) && !p.at(EOF) && !p.at(T![']']) {
-            break;
-        }
-        p.expect(T![,]);
+    if inner {
         expressions::expr_no_struct(p);
-    }
+        while !p.at(EOF) && !p.at(T![']']) {
+            if !p.at(T![,])
+                break;
+            }
+            p.expect(T![,]);
+            expressions::expr_no_struct(p);
+        }
 
-    if p.at(T![,]) {
-        p.expect(T![,]);
+        if p.at(T![,]) {
+            p.expect(T![,]);
+        }
     }
 
-    p.expect(T![']']);
-    m.complete(p, TRIGGER_ATTRIBUTE) // Review: just replace TRIGGER_ATTRIBUTE with ERROR  to avoid other parts of code indexing getting into trouble
+    m.complete(p, TRIGGER_ATTRIBUTE)
 }
 
 // pub(crate) fn global_clause(p: &mut Parser<'_>, m: Marker) {

diff --git a/crates/syntax/rust.ungram b/crates/syntax/rust.ungram
@@ -321,7 +321,7 @@ Visibility =
   'pub' ('(' 'in'? Path ')')?
 
 Attr =
-  '#' '!'? '[' Meta ']'
+  '#' '!'? '[' (TriggerAttribute | Meta) ']'
 
 Meta =
   'unsafe' '(' Path ('=' Expr | TokenTree)? ')'
@@ -782,7 +782,7 @@ Prover =
   'by' '(' Name ')'
 
 TriggerAttribute =
- '#' '!' '[' 'trigger' (Expr (',' Expr)* ','?) ']'
+ 'trigger' (Expr (',' Expr)* ','?)?
 
 VerusGlobal =
   Attr*

diff --git a/crates/syntax/src/ast/generated/nodes.rs b/crates/syntax/src/ast/generated/nodes.rs
@@ -149,6 +149,7 @@ pub struct Attr {
 }
 impl Attr {
     pub fn meta(&self) -> Option<Meta> { support::child(&self.syntax) }
+    pub fn trigger_attribute(&self) -> Option<TriggerAttribute> { support::child(&self.syntax) }
     pub fn excl_token(&self) -> Option<SyntaxToken> { support::token(&self.syntax, T![!]) }
     pub fn pound_token(&self) -> Option<SyntaxToken> { support::token(&self.syntax, T![#]) }
     pub fn l_brack_token(&self) -> Option<SyntaxToken> { support::token(&self.syntax, T!['[']) }
@@ -1612,10 +1613,6 @@ pub struct TriggerAttribute {
 }
 impl TriggerAttribute {
     pub fn exprs(&self) -> AstChildren<Expr> { support::children(&self.syntax) }
-    pub fn excl_token(&self) -> Option<SyntaxToken> { support::token(&self.syntax, T![!]) }
-    pub fn pound_token(&self) -> Option<SyntaxToken> { support::token(&self.syntax, T![#]) }
-    pub fn l_brack_token(&self) -> Option<SyntaxToken> { support::token(&self.syntax, T!['[']) }
-    pub fn r_brack_token(&self) -> Option<SyntaxToken> { support::token(&self.syntax, T![']']) }
     pub fn trigger_token(&self) -> Option<SyntaxToken> { support::token(&self.syntax, T![trigger]) }
 }
 

diff --git a/crates/syntax/src/ast/generated/vst_nodes.rs b/crates/syntax/src/ast/generated/vst_nodes.rs
@@ -111,7 +111,8 @@ pub struct Attr {
     pub pound_token: bool,
     pub excl_token: bool,
     pub l_brack_token: bool,
-    pub meta: Box<Meta>,
+    pub trigger_attribute: Option<Box<TriggerAttribute>>,
+    pub meta: Option<Box<Meta>>,
     pub r_brack_token: bool,
     pub cst: Option<super::nodes::Attr>,
 }
@@ -1130,12 +1131,8 @@ pub struct TraitAlias {
 }
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct TriggerAttribute {
-    pub pound_token: bool,
-    pub excl_token: bool,
-    pub l_brack_token: bool,
     pub trigger_token: bool,
     pub exprs: Vec<Expr>,
-    pub r_brack_token: bool,
     pub cst: Option<super::nodes::TriggerAttribute>,
 }
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
@@ -1756,11 +1753,14 @@ impl TryFrom<super::nodes::Attr> for Attr {
             pound_token: item.pound_token().is_some(),
             excl_token: item.excl_token().is_some(),
             l_brack_token: item.l_brack_token().is_some(),
-            meta: Box::new(
-                item.meta()
-                    .ok_or(format!("{}", stringify!(meta)))
-                    .map(|it| Meta::try_from(it))??,
-            ),
+            trigger_attribute: match item.trigger_attribute() {
+                Some(it) => Some(Box::new(TriggerAttribute::try_from(it)?)),
+                None => None,
+            },
+            meta: match item.meta() {
+                Some(it) => Some(Box::new(Meta::try_from(it)?)),
+                None => None,
+            },
             r_brack_token: item.r_brack_token().is_some(),
             cst: Some(item.clone()),
         })
@@ -4276,16 +4276,12 @@ impl TryFrom<super::nodes::TriggerAttribute> for TriggerAttribute {
     type Error = String;
     fn try_from(item: super::nodes::TriggerAttribute) -> Result<Self, Self::Error> {
         Ok(Self {
-            pound_token: item.pound_token().is_some(),
-            excl_token: item.excl_token().is_some(),
-            l_brack_token: item.l_brack_token().is_some(),
             trigger_token: item.trigger_token().is_some(),
             exprs: item
                 .exprs()
                 .into_iter()
                 .map(Expr::try_from)
                 .collect::<Result<Vec<Expr>, String>>()?,
-            r_brack_token: item.r_brack_token().is_some(),
             cst: Some(item.clone()),
         })
     }
@@ -5388,8 +5384,14 @@ impl std::fmt::Display for Attr {
             s.push_str(token_ascii(&tmp));
             s.push_str(" ");
         }
-        s.push_str(&self.meta.to_string());
-        s.push_str(" ");
+        if let Some(it) = &self.trigger_attribute {
+            s.push_str(&it.to_string());
+            s.push_str(" ");
+        }
+        if let Some(it) = &self.meta {
+            s.push_str(&it.to_string());
+            s.push_str(" ");
+        }
         if self.r_brack_token {
             let mut tmp = stringify!(r_brack_token).to_string();
             tmp.truncate(tmp.len() - 6);
@@ -8289,37 +8291,13 @@ impl std::fmt::Display for TraitAlias {
 impl std::fmt::Display for TriggerAttribute {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let mut s = String::new();
-        if self.pound_token {
-            let mut tmp = stringify!(pound_token).to_string();
-            tmp.truncate(tmp.len() - 6);
-            s.push_str(token_ascii(&tmp));
-            s.push_str(" ");
-        }
-        if self.excl_token {
-            let mut tmp = stringify!(excl_token).to_string();
-            tmp.truncate(tmp.len() - 6);
-            s.push_str(token_ascii(&tmp));
-            s.push_str(" ");
-        }
-        if self.l_brack_token {
-            let mut tmp = stringify!(l_brack_token).to_string();
-            tmp.truncate(tmp.len() - 6);
-            s.push_str(token_ascii(&tmp));
-            s.push_str(" ");
-        }
         if self.trigger_token {
             let mut tmp = stringify!(trigger_token).to_string();
             tmp.truncate(tmp.len() - 6);
             s.push_str(token_ascii(&tmp));
             s.push_str(" ");
         }
         s.push_str(&self.exprs.iter().map(|it| it.to_string()).collect::<Vec<String>>().join(" "));
-        if self.r_brack_token {
-            let mut tmp = stringify!(r_brack_token).to_string();
-            tmp.truncate(tmp.len() - 6);
-            s.push_str(token_ascii(&tmp));
-            s.push_str(" ");
-        }
         write!(f, "{s}")
     }
 }
@@ -9925,12 +9903,13 @@ impl AssumeExpr {
     }
 }
 impl Attr {
-    pub fn new(meta: Meta) -> Self {
+    pub fn new() -> Self {
         Self {
             pound_token: true,
             excl_token: false,
             l_brack_token: true,
-            meta: Box::new(meta),
+            trigger_attribute: None,
+            meta: None,
             r_brack_token: true,
             cst: None,
         }
@@ -11021,17 +11000,7 @@ impl TraitAlias {
     }
 }
 impl TriggerAttribute {
-    pub fn new() -> Self {
-        Self {
-            pound_token: true,
-            excl_token: true,
-            l_brack_token: true,
-            trigger_token: true,
-            exprs: vec![],
-            r_brack_token: true,
-            cst: None,
-        }
-    }
+    pub fn new() -> Self { Self { trigger_token: true, exprs: vec![], cst: None } }
 }
 impl TryExpr {
     pub fn new<ET0>(expr: ET0) -> Self

diff --git a/crates/va-test/Cargo.toml b/crates/va-test/Cargo.toml
@@ -0,0 +1,24 @@
+[package]
+name = "va-test"
+version = "0.0.0"
+description = "Directly test the Verus Analyzer server"
+
+authors.workspace = true
+edition.workspace = true
+license.workspace = true
+rust-version.workspace = true
+
+[dependencies]
+clap = { version = "4.3.11", features = ["derive"] }
+
+# local deps
+base-db.workspace = true
+ide-assists.workspace = true
+hir.workspace = true
+hir-def.workspace = true
+hir-ty.workspace = true
+load-cargo.workspace = true
+project-model.workspace = true
+#rust_analyzer.workspace = true
+syntax.workspace = true
+vfs.workspace = true
diff --git a/crates/va-test/examples/prost-build-bug/Cargo.toml b/crates/va-test/examples/prost-build-bug/Cargo.toml
@@ -0,0 +1,9 @@
+[package]
+name = "prost-build-bug"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]
+prost-build = "0.13.0"
diff --git a/crates/va-test/examples/prost-build-bug/src/main.rs b/crates/va-test/examples/prost-build-bug/src/main.rs
@@ -0,0 +1,3 @@
+fn main() {
+    println!("Hello, world!");
+}
diff --git a/crates/va-test/examples/schemars-bug/Cargo.toml b/crates/va-test/examples/schemars-bug/Cargo.toml
@@ -0,0 +1,9 @@
+[package]
+name = "schemars-bug"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]
+schemars = "0.8.21"
diff --git a/crates/va-test/examples/schemars-bug/src/main.rs b/crates/va-test/examples/schemars-bug/src/main.rs
@@ -0,0 +1,3 @@
+fn main() {
+    println!("Hello, world!");
+}
diff --git a/crates/va-test/examples/trigger-bug/Cargo.toml b/crates/va-test/examples/trigger-bug/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "trigger-bug"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]