diff --git a/crates/ide-assists/src/assist_context.rs b/crates/ide-assists/src/assist_context.rs index d3cac105b20a..c74889e69936 100644 --- a/crates/ide-assists/src/assist_context.rs +++ b/crates/ide-assists/src/assist_context.rs @@ -16,6 +16,12 @@ use crate::{ pub(crate) use ide_db::source_change::{SourceChangeBuilder, TreeMutator}; +/// +/// Majority of Proof action APIs are associated with AssistContext as its `impl`, +/// as those need broader information (e.g., info for the whole project) +/// +/// +/// /// `AssistContext` allows to apply an assist or check if it could be applied. /// /// Assists use a somewhat over-engineered approach, given the current needs. @@ -46,7 +52,7 @@ pub(crate) use ide_db::source_change::{SourceChangeBuilder, TreeMutator}; /// Note, however, that we don't actually use such two-phase logic at the /// moment, because the LSP API is pretty awkward in this place, and it's much /// easier to just compute the edit eagerly :-) -pub(crate) struct AssistContext<'a> { +pub struct AssistContext<'a> { pub(crate) config: &'a AssistConfig, pub(crate) sema: Semantics<'a, RootDatabase>, frange: FileRange, diff --git a/crates/ide-assists/src/lib.rs b/crates/ide-assists/src/lib.rs index 383e70dffeb8..38d5ee257a61 100644 --- a/crates/ide-assists/src/lib.rs +++ b/crates/ide-assists/src/lib.rs @@ -66,7 +66,7 @@ macro_rules! eprintln { } pub(crate) mod assist_config; -mod assist_context; +pub mod assist_context; // #[cfg(test)] pub(crate) mod tests; pub mod utils; diff --git a/crates/ide-assists/src/proof_plumber_api.rs b/crates/ide-assists/src/proof_plumber_api.rs index a59ad0524c8a..8f11790f9db2 100644 --- a/crates/ide-assists/src/proof_plumber_api.rs +++ b/crates/ide-assists/src/proof_plumber_api.rs @@ -1,12 +1,38 @@ //! ProofPlumber APIs //! -//! ProofPlumber APIs include functions inside this module +//! ProofPlumber APIs include functions inside each module. +//! +//! These APIs provide ways to utilize functionalities +//! for a developer to write proof actions +//! +//! See [`crate::AssistContext`] for APIs that utilize context information +//! For the rest, see [`verus_error`] and [`vst_ext`]. +//! +//! Aside from above APIs, there are several traits already implemented for TOST nodes +//! +//! TOST nodes (aka VST node) implement various traits including `TryFrom` and `Display` +//! `TryFrom` is used to convert CST node into a TOST Node +//! `Display` is used to convert a TOST node into a concrete code text. +//! +//! +//! `new` function is implemented for all TOST nodes. +//! `From` is implemented between various TOST nodes to make it easy to convert between those. +//! For example, +//! ```rust +//! for e in split_exprs { +//! let split_assert = AssertExpr::new(e); +//! stmts.statements.push(split_assert.into()); // convert AssertExpr into Stmt +//! } +//! ``` +//! +//! +//! For Verus syntax definition, read `ungram` file at `syntax` crate. +//! +//! We use +//! `syntax/src/tests/sourcegen_vst.rs` to auto-generate `syntax/src/ast/generated/vst_nodes.rs` +//! hand-written pars are at `syntax/src/vst.rs` +//! //! -//! For further referece, see -//! `syntax/src/vst`, -//! `syntax/src/tests/sourcegen_vst.rs`, -//! and `ungram` file at `syntax` crate. -//! pub mod proof_action_context; pub mod verus_error; pub mod run_fmt; diff --git a/crates/ide-assists/src/proof_plumber_api/inline_function_api.rs b/crates/ide-assists/src/proof_plumber_api/inline_function_api.rs index cd238f23f65d..ffc34e119db7 100644 --- a/crates/ide-assists/src/proof_plumber_api/inline_function_api.rs +++ b/crates/ide-assists/src/proof_plumber_api/inline_function_api.rs @@ -15,9 +15,9 @@ use syntax::{ impl<'a> AssistContext<'a> { /// inline function call /// for now, assume one file only - /// TODO: handle Verus builtin types -- for example, `type_of_expr` panics for `int` - /// TODO: properly register req/ens/etc in semantics db - /// TODO: currently inline can panic when the inlining expr does not fully use all the parameters + // TODO: handle Verus builtin types -- for example, `type_of_expr` panics for `int` + // TODO: properly register req/ens/etc in semantics db + // TODO: currently inline can panic when the inlining expr does not fully use all the parameters pub fn vst_inline_call( &self, name_ref: vst::NameRef, // the name of the function to inline **at the callsite**. from `name_ref`, we get its arguments diff --git a/crates/ide-assists/src/proof_plumber_api/proof_action_context.rs b/crates/ide-assists/src/proof_plumber_api/proof_action_context.rs index 4ce12df500ed..bd765034fa2e 100644 --- a/crates/ide-assists/src/proof_plumber_api/proof_action_context.rs +++ b/crates/ide-assists/src/proof_plumber_api/proof_action_context.rs @@ -13,7 +13,7 @@ impl<'a> AssistContext<'a> { /// Get TOST node(VST node) from the current cursor position /// This is a wrapper around `find_node_at_offset` that returns a TOST node(VST node) // REVIEW: to remove type annotation, consider auto-generating all sorts of this function - pub(crate) fn vst_find_node_at_offset(&self) -> Option + pub fn vst_find_node_at_offset(&self) -> Option where VSTT: TryFrom, CSTT: AstNode, @@ -22,7 +22,7 @@ impl<'a> AssistContext<'a> { VSTT::try_from(cst_node).ok() } - pub(crate) fn verus_errors(&self) -> Vec { + pub fn verus_errors(&self) -> Vec { self.verus_errors.clone() } @@ -30,7 +30,7 @@ impl<'a> AssistContext<'a> { // note that `pre` uses `pre.callsite` instead of `pre.failing_pre`. // technically, the failing pre condition is not the error of that function. // it is error of the callsite - pub(crate) fn verus_errors_inside_fn(&self, func: &vst::Fn) -> Option> { + pub fn verus_errors_inside_fn(&self, func: &vst::Fn) -> Option> { let surrounding_fn: &ast::Fn = func.cst.as_ref()?; let surrounding_range = surrounding_fn.syntax().text_range(); let filtered_verus_errs = self @@ -46,7 +46,7 @@ impl<'a> AssistContext<'a> { } /// Get precondition failures that was generated by calling this function - pub(crate) fn pre_failures_by_calling_this_fn(&self, func: &vst::Fn) -> Option> { + pub fn pre_failures_by_calling_this_fn(&self, func: &vst::Fn) -> Option> { let surrounding_fn: &ast::Fn = func.cst.as_ref()?; let surrounding_range: text_edit::TextRange = surrounding_fn.syntax().text_range(); let filtered_verus_errs: Vec = self @@ -61,27 +61,27 @@ impl<'a> AssistContext<'a> { } /// Gather every precondition failures - pub(crate) fn pre_failures(&self) -> Vec { + pub fn pre_failures(&self) -> Vec { filter_pre_failuires(&self.verus_errors) } /// Gather every postcondition failrues - pub(crate) fn post_failures(&self) -> Vec { + pub fn post_failures(&self) -> Vec { filter_post_failuires(&self.verus_errors) } /// From a Precondition Failure, retreive the TOST expression of the failing predicate - pub(crate) fn expr_from_pre_failure(&self, pre: PreFailure) -> Option { + pub fn expr_from_pre_failure(&self, pre: PreFailure) -> Option { self.find_node_at_given_range::(pre.failing_pre)?.try_into().ok() } /// From a Postcondition Failure, retreive the TOST expression of the failing predicate - pub(crate) fn expr_from_post_failure(&self, post: PostFailure) -> Option { + pub fn expr_from_post_failure(&self, post: PostFailure) -> Option { self.find_node_at_given_range::(post.failing_post)?.try_into().ok() } /// Specify the syntax token to invoke a proof action - pub(crate) fn at_this_token(&self, token: SyntaxKind) -> Option<()> { + pub fn at_this_token(&self, token: SyntaxKind) -> Option<()> { let assert_keyword = self.find_token_syntax_at_offset(token)?; let cursor_in_range = assert_keyword.text_range().contains_range(self.selection_trimmed()); if !cursor_in_range { @@ -91,7 +91,7 @@ impl<'a> AssistContext<'a> { } /// helper routine to replace statement - pub(crate) fn replace_statement(&self, func: &vst::Fn, old: ST0, new: ST1) -> Option + pub fn replace_statement(&self, func: &vst::Fn, old: ST0, new: ST1) -> Option where ST0: Into + std::clone::Clone, ST1: Into + std::clone::Clone, @@ -131,7 +131,7 @@ impl<'a> AssistContext<'a> { } /// helper routine to reduce a list of predicate into &&-ed predicate - pub(crate) fn reduce_exprs(&self, es: Vec) -> Option { + pub fn reduce_exprs(&self, es: Vec) -> Option { es.into_iter().reduce(|acc, e| { vst::Expr::BinExpr(Box::new(vst::BinExpr::new( acc, diff --git a/crates/ide-assists/src/proof_plumber_api/run_fmt.rs b/crates/ide-assists/src/proof_plumber_api/run_fmt.rs index 62736a8c4aed..d80f3ac37292 100644 --- a/crates/ide-assists/src/proof_plumber_api/run_fmt.rs +++ b/crates/ide-assists/src/proof_plumber_api/run_fmt.rs @@ -1,6 +1,6 @@ //! ProofPlumber API for formatting //! -//! Uses verusfmt at https://github.com/verus-lang/verusfmt +//! Uses verusfmt at //! //! Since TOST node (VST node) abstracts away whitespace, indentation, newline and stuff //! for easier manipulation, we need to restore those @@ -36,7 +36,7 @@ impl<'a> AssistContext<'a> { /// 1) print the function into a temporary file (ugly, but syntactically correct one) /// 2) run verusfmt on the temporary file /// 3) return the formatted function as a string - pub(crate) fn fmt( + pub fn fmt( &self, sth_to_remove: N, // old text_to_replace: String, // new diff --git a/crates/ide-assists/src/proof_plumber_api/run_verus.rs b/crates/ide-assists/src/proof_plumber_api/run_verus.rs index e54742dd48c8..0f3389856d1e 100644 --- a/crates/ide-assists/src/proof_plumber_api/run_verus.rs +++ b/crates/ide-assists/src/proof_plumber_api/run_verus.rs @@ -1,3 +1,6 @@ +//! Run Verus and return the verification result + + use std::{process::Command, collections::hash_map::DefaultHasher, time::Instant, env, path::Path, hash::{Hasher, Hash}, fs::File, io::Write}; use crate::AssistContext; use syntax::ast::{self, vst, HasModuleItem, HasName}; @@ -12,23 +15,15 @@ impl<'a> AssistContext<'a> { // TODO: pass the whole project to verus, instead of this single file // TODO: projects with multiple file/module -- `verify-module` flag --verify-function flag // output: None -> compile error + /// We only replace the function in the input + /// we use the remaining codebase when invoking Verus + /// Output None when Verus fails to start (e.g., compile error on the modified function) pub(crate) fn try_verus( &self, vst_fn: &vst::Fn, // only replace this function and run ) -> Option { let source_file = &self.source_file; - // let verus_exec_path = &self.config.verus_path; - // if verus_exec_path.len() == 0 { - // dbg!("verus path not set"); - // } - // #[cfg(test)] // We get verus path from config of editor. In test, we use a hardcoded path - // let verus_exec_path = HARDCODED_VERUS_PATH_FOR_TEST.to_string(); // TODO: maybe move this to test config let verus_exec_path = std::env::var("VERUS_BINARY_PATH").expect("please set VERUS_BINARY_PATH environment variable"); - // if verus_exec_path.len() == 0 { - // dbg!("verus path not set"); - // } - - let mut text_string = String::new(); // in VST, we should also be able to "print" and verify // display for VST should be correct modulo whitespace diff --git a/crates/ide-assists/src/proof_plumber_api/semantic_info.rs b/crates/ide-assists/src/proof_plumber_api/semantic_info.rs index e47bfedc520d..7793c7e718f8 100644 --- a/crates/ide-assists/src/proof_plumber_api/semantic_info.rs +++ b/crates/ide-assists/src/proof_plumber_api/semantic_info.rs @@ -1,6 +1,5 @@ //! Various helper functions related to type resolution to work with TOST Nodes (VST Nodes) //! -//! //! Utilizes Rust-analyzer's type `hir` implementation //! #![allow(dead_code)] @@ -35,6 +34,7 @@ impl<'a> AssistContext<'a> { None } + /// From a pattern, get the Enum definition of that pat. pub fn type_of_pat_enum(&self, pat: &vst::Pat) -> Option { let sema: &Semantics<'_, ide_db::RootDatabase> = &self.sema; let hir_ty: Vec = @@ -50,6 +50,7 @@ impl<'a> AssistContext<'a> { None } + /// Get the Struct definition of an expression pub fn type_of_expr_struct(&self, expr: &vst::Expr) -> Option { let typename = self.type_of_expr_adt(expr)?; if let vst::Adt::Struct(e) = typename { @@ -58,6 +59,7 @@ impl<'a> AssistContext<'a> { None } + /// Get the struct deinition of a pat pub fn type_of_pat_struct(&self, pat: &vst::Pat) -> Option { let sema: &Semantics<'_, ide_db::RootDatabase> = &self.sema; let hir_ty: Vec = @@ -73,6 +75,7 @@ impl<'a> AssistContext<'a> { None } + /// From a Type usage, get the definition of the enum pub fn resolve_type_enum(&self, ty: &vst::Type) -> Option { let sema: &Semantics<'_, ide_db::RootDatabase> = &self.sema; let hir_ty: Vec = @@ -93,6 +96,7 @@ impl<'a> AssistContext<'a> { None } + /// Get the NameRef at the callsite pub fn name_ref_from_call_expr(&self, call: &vst::CallExpr) -> Option { let path = match &*call.expr { vst::Expr::PathExpr(path) => &path.path, @@ -102,7 +106,8 @@ impl<'a> AssistContext<'a> { Some(*name_ref.clone()) } - pub(crate) fn vst_find_fn(&self, call: &vst::CallExpr) -> Option { + /// Get function definition from the callsite + pub fn vst_find_fn(&self, call: &vst::CallExpr) -> Option { for item in self.source_file.items() { let v_item: ast::generated::vst_nodes::Item = match item.try_into() { @@ -124,7 +129,8 @@ impl<'a> AssistContext<'a> { return None; } - pub(crate) fn is_opaque(&self, func: &vst::Fn) -> bool { + /// Query if this function is opaque (non-visible to the solver) + pub fn is_opaque(&self, func: &vst::Fn) -> bool { for attr in &func.attrs { if attr.to_string().contains("opaque") { return true; @@ -133,10 +139,4 @@ impl<'a> AssistContext<'a> { return false; } - // fn type_of_pat(&self, pat: &vst::Pat) -> Option { - // let sema: &Semantics<'_, ide_db::RootDatabase> = &self.sema; - // let hir_ty: Vec = - // sema.type_of_pat(&pat.cst()?)?.adjusted().autoderef(sema.db).collect::>(); - // let hir_ty = hir_ty.first()?.hir_fmt() - // } } diff --git a/crates/ide-assists/src/proof_plumber_api/vst_ext.rs b/crates/ide-assists/src/proof_plumber_api/vst_ext.rs index f05626037cbd..5d9d21927b36 100644 --- a/crates/ide-assists/src/proof_plumber_api/vst_ext.rs +++ b/crates/ide-assists/src/proof_plumber_api/vst_ext.rs @@ -14,6 +14,7 @@ pub fn vst_walk_expr(expr: &vst::Expr, cb: &mut dyn FnMut(vst::Expr)) { }) } +/// Map a VST Node recursively pub fn vst_map_expr_visitor(exp: EE, cb: &FF) -> Result where EE: Into, @@ -132,9 +133,10 @@ pub fn vst_preorder_expr(exp: &vst::Expr, cb: &mut dyn FnMut(vst::Expr) -> bool) } } +/// Map each tail expressions // For now, just gather each returning expression // TODO: `match` -// TODO: `return` +// TODO: `return` pub fn vst_map_each_tail_expr(exp: EE, cb: &FF) -> Result where EE: Into, diff --git a/crates/ide-assists/src/proof_plumber_api/vst_from_text.rs b/crates/ide-assists/src/proof_plumber_api/vst_from_text.rs index ba10c6f2ed8f..6f982989e230 100644 --- a/crates/ide-assists/src/proof_plumber_api/vst_from_text.rs +++ b/crates/ide-assists/src/proof_plumber_api/vst_from_text.rs @@ -1,13 +1,20 @@ +//! It can be cumbersom to generate a new TOST node using `new` +//! Below are some helper functions in this case. +//! We can generate commonly used TOST nodes from text using the following APIs. +//! + use crate::AssistContext; use syntax::ast::{self, vst}; impl<'a> AssistContext<'a> { + /// Generate Path from text pub fn vst_path_from_text(&self, text: &str) -> Option { let path = ast::make::path_from_text(text); let vst_path = vst::Path::try_from(path).ok()?; return Some(vst_path); } + /// Generate CallExpr from Text and ArgList pub fn vst_call_expr_from_text(&self, fn_name: &str, arglist: vst::ArgList) -> Option { let fn_name_as_path: vst::Path = self.vst_path_from_text(fn_name)?; let fn_name_as_pathexpr: vst::PathExpr = vst::PathExpr::new(fn_name_as_path); @@ -15,12 +22,14 @@ impl<'a> AssistContext<'a> { return Some(vst_call_expr); } + /// Generate NameRef from text pub fn vst_nameref_from_text(&self, s: &str) -> Option { let mut name = vst::NameRef::new(); name.ident_token = Some(String::from(s)); Some(name) } + /// Generate Expr from text pub fn vst_expr_from_text(&self, s: &str) -> Option { let ret: vst::Expr = vst::Literal::new(s.to_string()).into(); Some(ret)