Automatically import vstd and builtin

crates/base-db/src/fixture.rs

@@ -409,6 +409,9 @@ fn parse_crate(crate_str: String) -> (String, CrateOrigin, Option<String>) {
         let crate_origin = match &*crate_str {
             "std" => CrateOrigin::Lang(LangCrateOrigin::Std),
             "core" => CrateOrigin::Lang(LangCrateOrigin::Core),
+            "vstd" => CrateOrigin::Lang(LangCrateOrigin::Vstd),             // Verus 
+            "builtin" => CrateOrigin::Lang(LangCrateOrigin::Builtin),       // Verus 
+            // "builtin_macros" => CrateOrigin::Lang(LangCrateOrigin::BuiltinMacros),  // Verus 
             _ => CrateOrigin::CratesIo { repo: None },
         };
         (crate_str, crate_origin, None)

crates/base-db/src/input.rs

@@ -137,7 +137,7 @@ impl ops::Deref for CrateName {
 pub enum CrateOrigin {
     /// Crates that are from crates.io official registry,
     CratesIo { repo: Option<String> },
-    /// Crates that are provided by the language, like std, core, proc-macro, ...
+    /// Crates that are provided by the language, like std, core, proc-macro, ...   (Verus: vstd, builtin, builtin_macros)
     Lang(LangCrateOrigin),
 }
 
@@ -147,6 +147,9 @@ pub enum LangCrateOrigin {
     Core,
     ProcMacro,
     Std,
+    Vstd,         // Verus 
+    Builtin,      // Verus 
+    // BuiltinMacros, // Verus
     Test,
     Other,
 }
@@ -158,6 +161,9 @@ impl From<&str> for LangCrateOrigin {
             "core" => LangCrateOrigin::Core,
             "proc-macro" => LangCrateOrigin::ProcMacro,
             "std" => LangCrateOrigin::Std,
+            "vstd" => LangCrateOrigin::Vstd,                        // Verus 
+            "builtin" => LangCrateOrigin::Builtin,                  // Verus 
+            // "builtin_macros" => LangCrateOrigin::BuiltinMacros,     // Verus 
             "test" => LangCrateOrigin::Test,
             _ => LangCrateOrigin::Other,
         }
@@ -171,6 +177,9 @@ impl fmt::Display for LangCrateOrigin {
             LangCrateOrigin::Core => "core",
             LangCrateOrigin::ProcMacro => "proc_macro",
             LangCrateOrigin::Std => "std",
+            LangCrateOrigin::Vstd => "vstd",                        // Verus 
+            LangCrateOrigin::Builtin => "builtin",                  // Verus 
+            // LangCrateOrigin::BuiltinMacros => "builtin_macros",     // Verus 
             LangCrateOrigin::Test => "test",
             LangCrateOrigin::Other => "other",
         };

crates/ide-db/src/famous_defs.rs

@@ -25,6 +25,11 @@ impl FamousDefs<'_, '_> {
     pub fn std(&self) -> Option<Crate> {
         self.find_lang_crate(LangCrateOrigin::Std)
     }
+
+    // Verus 
+    pub fn vstd(&self) -> Option<Crate> {
+        self.find_lang_crate(LangCrateOrigin::Vstd)
+    }
 
     pub fn core(&self) -> Option<Crate> {
         self.find_lang_crate(LangCrateOrigin::Core)
@@ -109,6 +114,7 @@ impl FamousDefs<'_, '_> {
     pub fn builtin_crates(&self) -> impl Iterator<Item = Crate> {
         IntoIterator::into_iter([
             self.std(),
+            self.vstd(),// Verus 
             self.core(),
             self.alloc(),
             self.test(),

crates/project-model/src/cargo_workspace.rs

@@ -90,6 +90,7 @@ pub struct CargoConfig {
     pub no_sysroot: bool,
 
     // TODO(verus): import verus pervasive from "config"
+    pub verus_root: Option<String>,
 
     /// rustc private crate source
     pub rustc_source: Option<RustcSource>,

crates/project-model/src/project_json.rs

@@ -21,6 +21,8 @@ pub struct ProjectJson {
     pub(crate) sysroot: Option<AbsPathBuf>,
     /// e.g. `path/to/sysroot/lib/rustlib/src/rust`
     pub(crate) sysroot_src: Option<AbsPathBuf>,
+    // verus root path
+    // pub(crate) verus_root: Option<AbsPathBuf>,
     project_root: AbsPathBuf,
     crates: Vec<Crate>,
 }
@@ -57,6 +59,7 @@ impl ProjectJson {
         ProjectJson {
             sysroot: data.sysroot.map(|it| base.join(it)),
             sysroot_src: data.sysroot_src.map(|it| base.join(it)),
+            // verus_root: data.verus_root.map_or(None, |v| AbsPathBuf::try_from(v).ok()),
             project_root: base.to_path_buf(),
             crates: data
                 .crates
@@ -128,6 +131,7 @@ impl ProjectJson {
 pub struct ProjectJsonData {
     sysroot: Option<PathBuf>,
     sysroot_src: Option<PathBuf>,
+    // verus_root: Option<PathBuf>,
     crates: Vec<CrateData>,
 }
 

crates/project-model/src/sysroot.rs

@@ -4,7 +4,7 @@
 //! but we can't process `.rlib` and need source code instead. The source code
 //! is typically installed with `rustup component add rust-src` command.
 
-use std::{env, fs, iter, ops, path::PathBuf, process::Command};
+use std::{env, fs, iter, ops, path::PathBuf, process::Command, str::FromStr};
 
 use anyhow::{format_err, Result};
 use la_arena::{Arena, Idx};
@@ -49,10 +49,11 @@ impl Sysroot {
         &self.src_root
     }
 
+    // Verus(add vstd here?)
     pub fn public_deps(&self) -> impl Iterator<Item = (&'static str, SysrootCrate, bool)> + '_ {
         // core is added as a dependency before std in order to
         // mimic rustcs dependency order
-        ["core", "alloc", "std"]
+        ["core", "alloc", "std", "vstd", "builtin"]   // Verus 
             .into_iter()
             .zip(iter::repeat(true))
             .chain(iter::once(("test", false)))
@@ -67,11 +68,12 @@ impl Sysroot {
         self.crates.iter().map(|(id, _data)| id)
     }
 
-    pub fn discover(dir: &AbsPath) -> Result<Sysroot> {
+    pub fn discover(dir: &AbsPath, verus_root_dir: Option<String>) -> Result<Sysroot> {
+        dbg!("discover", &verus_root_dir);
         tracing::debug!("Discovering sysroot for {}", dir.display());
         let sysroot_dir = discover_sysroot_dir(dir)?;
         let sysroot_src_dir = discover_sysroot_src_dir(&sysroot_dir, dir)?;
-        let res = Sysroot::load(sysroot_dir, sysroot_src_dir)?;
+        let res = Sysroot::load(sysroot_dir, sysroot_src_dir, verus_root_dir)?;
         Ok(res)
     }
 
@@ -81,7 +83,8 @@ impl Sysroot {
         discover_sysroot_dir(current_dir).ok().and_then(|sysroot_dir| get_rustc_src(&sysroot_dir))
     }
 
-    pub fn load(sysroot_dir: AbsPathBuf, sysroot_src_dir: AbsPathBuf) -> Result<Sysroot> {
+    // add one argument about "verus_root_directory"
+    pub fn load(sysroot_dir: AbsPathBuf, sysroot_src_dir: AbsPathBuf, verus_root_dir: Option<String>) -> Result<Sysroot> {
         let mut sysroot =
             Sysroot { root: sysroot_dir, src_root: sysroot_src_dir, crates: Arena::default() };
 
@@ -100,8 +103,40 @@ impl Sysroot {
                     deps: Vec::new(),
                 });
             }
+
+            // Verus 
+            if name == "vstd" || name == "builtin" { //|| name == "builtin_macros"
+                dbg!(name);
+                let verus_root = verus_root_dir.as_ref();
+                match verus_root {
+                    Some(verus_root) => {
+                        let mut vstd_path = format!("{}/{}/src/lib.rs", verus_root, name);
+                        if name == "vstd" {
+                            // TODO test vstd with actually moving the pervasive files
+                            // vstd_path = "/Users/chanhee/Works/secure-foundations/verus/source/pervasive/mod.rs".to_string();
+                        }
+                        dbg!(&vstd_path);
+                        let pathb = PathBuf::from_str(vstd_path.as_str()).unwrap();
+                        let abspath:AbsPathBuf = AbsPathBuf::assert(pathb);
+                        let root = ManifestPath::try_from(abspath).unwrap();
+                        sysroot.crates.alloc(SysrootCrateData {
+                            name: name.into(),
+                            root,
+                            deps: Vec::new(),
+                        });
+
+                    }
+                    None => {
+                        dbg!("unwrap verus root on sysroot load");
+                    }
+                }
+
+
+            }
+
         }
 
+
         if let Some(std) = sysroot.by_name("std") {
             for dep in STD_DEPS.trim().lines() {
                 if let Some(dep) = sysroot.by_name(dep) {
@@ -110,6 +145,7 @@ impl Sysroot {
             }
         }
 
+
         if let Some(alloc) = sysroot.by_name("alloc") {
             if let Some(core) = sysroot.by_name("core") {
                 sysroot.crates[alloc].deps.push(core);
@@ -207,6 +243,7 @@ fn get_rust_src(sysroot_path: &AbsPath) -> Option<AbsPathBuf> {
     }
 }
 
+// Verus changes made vstd, builtin,   (Removed) -> builtin_macros
 const SYSROOT_CRATES: &str = "
 alloc
 core
@@ -215,6 +252,8 @@ panic_unwind
 proc_macro
 profiler_builtins
 std
+vstd
+builtin
 stdarch/crates/std_detect
 term
 test

crates/project-model/src/tests.rs

@@ -80,7 +80,7 @@ fn get_fake_sysroot() -> Sysroot {
     // fake sysroot, so we give them both the same path:
     let sysroot_dir = AbsPathBuf::assert(sysroot_path);
     let sysroot_src_dir = sysroot_dir.clone();
-    Sysroot::load(sysroot_dir, sysroot_src_dir).unwrap()
+    Sysroot::load(sysroot_dir, sysroot_src_dir, None).unwrap()
 }
 
 fn rooted_project_json(data: ProjectJsonData) -> ProjectJson {

crates/project-model/src/workspace.rs

@@ -148,6 +148,7 @@ impl ProjectWorkspace {
     ) -> Result<ProjectWorkspace> {
         let res = match manifest {
             ProjectManifest::ProjectJson(project_json) => {
+                dbg!("project manifest");
                 let file = fs::read_to_string(&project_json).with_context(|| {
                     format!("Failed to read json file {}", project_json.display())
                 })?;
@@ -159,6 +160,7 @@ impl ProjectWorkspace {
                 ProjectWorkspace::load_inline(project_json, config.target.as_deref())?
             }
             ProjectManifest::CargoToml(cargo_toml) => {
+                dbg!("cargo manifest");
                 let cargo_version = utf8_stdout({
                     let mut cmd = Command::new(toolchain::cargo());
                     cmd.arg("--version");
@@ -182,11 +184,13 @@ impl ProjectWorkspace {
                     )
                 })?;
                 let cargo = CargoWorkspace::new(meta);
+                let verus_path = config.verus_root.as_ref();
+                dbg!(&verus_path);
 
                 let sysroot = if config.no_sysroot {
                     None
                 } else {
-                    Some(Sysroot::discover(cargo_toml.parent()).with_context(|| {
+                    Some(Sysroot::discover(cargo_toml.parent(), verus_path.map_or(None, |v| Some(v.clone()))).with_context(|| {
                         format!(
                             "Failed to find sysroot for Cargo.toml file {}. Is rust-src installed?",
                             cargo_toml.display()
@@ -239,21 +243,21 @@ impl ProjectWorkspace {
         target: Option<&str>,
     ) -> Result<ProjectWorkspace> {
         let sysroot = match (project_json.sysroot.clone(), project_json.sysroot_src.clone()) {
-            (Some(sysroot), Some(sysroot_src)) => Some(Sysroot::load(sysroot, sysroot_src)?),
+            (Some(sysroot), Some(sysroot_src)) => Some(Sysroot::load(sysroot, sysroot_src, None)?),
             (Some(sysroot), None) => {
                 // assume sysroot is structured like rustup's and guess `sysroot_src`
                 let sysroot_src =
                     sysroot.join("lib").join("rustlib").join("src").join("rust").join("library");
 
-                Some(Sysroot::load(sysroot, sysroot_src)?)
+                Some(Sysroot::load(sysroot, sysroot_src, None)?)
             }
             (None, Some(sysroot_src)) => {
                 // assume sysroot is structured like rustup's and guess `sysroot`
                 let mut sysroot = sysroot_src.clone();
                 for _ in 0..5 {
                     sysroot.pop();
                 }
-                Some(Sysroot::load(sysroot, sysroot_src)?)
+                Some(Sysroot::load(sysroot, sysroot_src, None)?)
             }
             (None, None) => None,
         };
@@ -263,11 +267,13 @@ impl ProjectWorkspace {
     }
 
     pub fn load_detached_files(detached_files: Vec<AbsPathBuf>) -> Result<ProjectWorkspace> {
+        dbg!("load detached files");
         let sysroot = Sysroot::discover(
             detached_files
                 .first()
                 .and_then(|it| it.parent())
                 .ok_or_else(|| format_err!("No detached files to load"))?,
+            None,
         )?;
         let rustc_cfg = rustc_cfg::get(None, None);
         Ok(ProjectWorkspace::DetachedFiles { files: detached_files, sysroot, rustc_cfg })
@@ -639,6 +645,7 @@ fn cargo_to_crate_graph(
         }
 
         // Set deps to the core, std and to the lib target of the current package
+        // Verus(add vstd?)
         for (from, kind) in pkg_crates.get(&pkg).into_iter().flatten() {
             // Add sysroot deps first so that a lib target named `core` etc. can overwrite them.
             public_deps.add(*from, &mut crate_graph);
@@ -816,6 +823,7 @@ fn handle_rustc_crates(
                     );
                     pkg_to_lib_crate.insert(pkg, crate_id);
                     // Add dependencies on core / std / alloc for this crate
+                    // Verus(add vstd(pervasive)?)
                     public_deps.add(crate_id, crate_graph);
                     rustc_pkg_crates.entry(pkg).or_insert_with(Vec::new).push(crate_id);
                 }

crates/rust-analyzer/src/config.rs

@@ -985,6 +985,8 @@ impl Config {
             }
         });
 
+        //  grap Verus root path from checkonsave
+
         CargoConfig {
             no_default_features: self.data.cargo_noDefaultFeatures,
             all_features: matches!(self.data.cargo_features, CargoFeatures::All),
@@ -998,6 +1000,7 @@ impl Config {
             unset_test_crates: UnsetTestCrates::Only(self.data.cargo_unsetTest.clone()),
             wrap_rustc_in_build_scripts: self.data.cargo_buildScripts_useRustcWrapper,
             run_build_script_command: self.data.cargo_buildScripts_overrideCommand.clone(),
+            verus_root: self.get_verus_root_path(),
         }
     }
 
@@ -1151,16 +1154,37 @@ impl Config {
         self.experimental("snippetTextEdit")
     }
 
-    pub fn assist(&self) -> AssistConfig {
-        let verus_path = match &self.data.checkOnSave_overrideCommand {
+    // from checkOnSave_overrideCommand, grap tools/rust_verify.sh path for proof action usage
+    fn get_verus_path(&self) -> Option<String> {
+        match &self.data.checkOnSave_overrideCommand {
             Some(args) if !args.is_empty() => {
                 let mut args = args.clone();
                 let command = args.remove(0);
-                command
+                if command.contains("verus") {
+                    Some(command)
+                } else {
+                    None
+                }
             }
-            _ => {String::new()}
-        };
+            _ => {None}
+        }
+    }
 
+    // from checkOnSave_overrideCommand, grap Verus root path, which is verus/source
+    // "/Users/chanhee/Works/secure-foundations/verus/source/tools/rust-verify.sh",
+    fn get_verus_root_path(&self) -> Option<String> {
+        let verus_string = self.get_verus_path()?;
+        dbg!(&verus_string);
+        let verus_path = std::path::Path::new(&verus_string);
+        let verus_root_path = verus_path.parent()?.parent()?;
+        let verus_root_str = verus_root_path.to_str()?;
+        Some(verus_root_str.to_string())
+    }
+
+    pub fn assist(&self) -> AssistConfig {
+        // from checkOnSave_overrideCommand, grap Verus path for proof action usage
+        let verus_path = self.get_verus_path().map_or(String::new(), |v| v);
+
         AssistConfig {
             snippet_cap: SnippetCap::new(self.experimental("snippetTextEdit")),
             allowed: None,