Merge remote-tracking branch 'origin/main' into nixos

docs/src/cargo-kani.md

@@ -11,6 +11,10 @@ cargo kani [<kani-args>]*
 `cargo kani` is the recommended approach for using Kani on a project, due to its
 ability to handle external dependencies and the option add configurations via the `Cargo.toml` file.
 
+If your proof harness is placed under `tests/`, you will need to run
+`cargo kani` with the `--tests` for Kani to be able to find your
+harness.
+
 ## Configuration
 
 Users can add a default configuration to the `Cargo.toml` file for running harnesses in a package.

docs/src/cheat-sheets.md

@@ -110,15 +110,6 @@ git submodule foreach --recursive git clean -xffd
 git submodule update --init
 ```
 
-```bash
-# Done with that PR, time for a new one?
-git switch main
-git pull origin
-git submodule update --init
-cd src/kani-compiler
-cargo build --workspace
-```
-
 ```bash
 # Need to update local branch (e.g. for an open pull request?)
 git fetch origin
@@ -134,16 +125,20 @@ git switch pr/$ID
 ```
 
 ```bash
-# Search only git-tracked files
-git grep codegen_panic
+# Push to someone else's pull request
+git origin add $USER $GIR_URL_FOR_THAT_USER
+git push $USER $LOCAL_BRANCH:$THEIR_PR_BRANCH_NAME
 ```
 
 ```bash
-# See all commits that are part of Kani, not part of Rust
-git log --graph --oneline origin/upstream-rustc..origin/main
+# Search only git-tracked files
+git grep codegen_panic
 ```
 
 ```bash
-# See all files modified by Kani (compared to upstream Rust)
-git diff --stat origin/upstream-rustc..origin/main
+# Accidentally commit to main?
+# "Move" commit to a branch:
+git checkout -b my_branch
+# Fix main:
+git branch --force main origin/main
 ```

docs/src/rustc-hacks.md

@@ -33,6 +33,25 @@ You may also need to install the `rustc-dev` package using rustup
 rustup toolchain install nightly --component rustc-dev
 ```
 
+#### Debugging in VS code
+
+To debug Kani in VS code, first install the [CodeLLDB extension](https://marketplace.visualstudio.com/items?itemName=vadimcn.vscode-lldb).
+Then add the following lines at the start of the `main` function (see [the CodeLLDB manual](https://github.com/vadimcn/vscode-lldb/blob/master/MANUAL.md#attaching-debugger-to-the-current-process-rust) for details):
+
+```rust
+{
+    let url = format!(
+        "vscode://vadimcn.vscode-lldb/launch/config?{{'request':'attach','sourceLanguages':['rust'],'waitFor':true,'pid':{}}}",
+        std::process::id()
+    );
+    std::process::Command::new("code").arg("--open-url").arg(url).output().unwrap();
+}
+```
+
+Note that pretty printing for the Rust nightly toolchain (which Kani uses) is not very good as of June 2022.
+For example, a vector may be displayed as `vec![{...}, {...}]` on nightly Rust, when it would be displayed as `vec![Some(0), None]` on stable Rust.
+Hopefully, this will be fixed soon.
+
 ### CLion / IntelliJ
 This is not a great solution, but it works for now (see <https://github.com/intellij-rust/intellij-rust/issues/1618>
 for more details).
@@ -50,6 +69,91 @@ rustc_interface = { path = "~/.rustup/toolchains/<toolchain>/lib/rustlib/rustc-s
 
 **Don't forget to rollback the changes before you create your PR.**
 
+### EMACS (with `use-package`)
+First, `Cargo.toml` and `rustup toolchain` steps are identical to VS
+Code. Install Rust-analyzer binary under `~/.cargo/bin/`.
+
+On EMACS, add the following to your EMACS lisp files. They will
+install the necessary packages using the `use-package` manager.
+```elisp
+;; Install LSP
+(use-package lsp-mode
+  :commands lsp)
+(use-package lsp-ui)
+
+;; Install Rust mode
+(use-package toml-mode)
+(use-package rust-mode)
+
+(setq lsp-rust-server 'rust-analyzer)
+(setenv "PATH" (concat (getenv "PATH") ":/home/USER/.cargo/bin/"))
+```
+If EMACS complains that it cannot find certain packages, try running
+`M-x package-refresh-contents`.
+
+For LSP to be able to find `rustc_private` files used by Kani, you
+will need to modify variable `lsp-rust-analyzer-rustc-source`. Run
+`M-x customize-variable`, type in `lsp-rust-analyzer-rustc-source`,
+click `Value Menu` and change it to `Path`. Paste in the path to
+`Cargo.toml` of `rustc`'s source code. You can find the source code
+under `.rustup`, and the path should end with
+`compiler/rustc/Cargo.toml`. **Important**: make sure that this
+`rustc` is the same version and architecture as what Kani uses. If
+not, LSP features like definition lookup may be break.
+
+This ends the basic install for EMACS. You can test your configuration
+with the following steps.
+1. Opening up a rust file with at least one `rustc_private` import.
+2. Activate LSP mode with `M-x lsp`.
+3. When asked about the root of the project, pick one of them. **Make
+   sure** that whichever root you pick has a `Cargo.toml` with
+   `rustc_private=true` added.
+4. If LSP asks if you want to watch all files, select yes. For less
+   powerful machines, you may want to adjust that later.
+5. On the file with `rustc_private` imports, do the following. If both
+   work, then you are set up.
+   - Hover mouse over the `rustc_private` import. If LSP is working,
+	 you should get information about the imported item.
+   - With text cursor over the same `rustc_private` import, run `M-x
+     lsp-find-definition`. This should jump to the definition within
+     `rustc`'s source code.
+
+LSP mode can integrate with `flycheck` for instant error checking and
+`company` for auto-complete. Consider adding the following to the
+configuration.
+```elisp
+(use-package flycheck
+  :hook (prog-mode . flycheck-mode))
+
+(use-package company
+  :hook (prog-mode . company-mode)
+  :config
+   (global-company-mode))
+```
+
+`clippy` linter can be added by changing the LSP install to:
+```elisp
+(use-package lsp-mode
+  :commands lsp
+  :custom
+  (lsp-rust-analyzer-cargo-watch-command "clippy"))
+```
+
+Finally lsp-mode can run rust-analyzer via TRAMP for remote
+development. **We found this way of using rust-analyzer to be unstable
+as of 2022-06**. If you want to give it a try you will need to add a
+new LSP client for that remote with the following code.
+```elisp
+(lsp-register-client
+  (make-lsp-client
+	:new-connection (lsp-tramp-connection "/full/path/to/remote/machines/rust-analyzer")
+	:major-modes '(rust-mode)
+	:remote? t
+	:server-id 'rust-analyzer-remote))
+```
+
+For further details, please see https://emacs-lsp.github.io/lsp-mode/page/remote/.
+
 ## Custom `rustc`
 
 There are a few reasons why you may want to use your own copy of `rustc`. E.g.:

kani-driver/src/call_cbmc_viewer.rs

@@ -70,6 +70,15 @@ impl KaniSession {
         // Let the user know
         if !self.args.quiet {
             println!("Report written to: {}/html/index.html", report_dir.to_string_lossy());
+            // If using VS Code with Remote-SSH, suggest an option for remote viewing:
+            if std::env::var("VSCODE_IPC_HOOK_CLI").is_ok()
+                && std::env::var("SSH_CONNECTION").is_ok()
+            {
+                println!(
+                    "VS Code automatically forwards ports for locally hosted servers. To view the report remotely,\nTry:  python3 -m http.server --directory {}/html",
+                    report_dir.to_string_lossy()
+                );
+            }
         }
 
         Ok(())