Improve debugging docs (#1263)

* Fix corrupted png's * Add env to generated launch config * Improve debugging docs
viperproject · Dec 21, 2022 · 2190fd2 · 2190fd2
1 parent d86245d
commit 2190fd2
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 3 deletions.
diff --git a/docs/dependency-graph/images/design.png b/docs/dependency-graph/images/design.png
diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md
@@ -173,7 +173,8 @@ When enabled, reborrowing DAGs will be output in debug files.
 
 ## `DUMP_VIPER_PROGRAM`
 
-When enabled, the encoded Viper program will be output.
+When enabled, the encoded Viper programs will be output.
+You can find them either in `log/viper_program` or `target/verify/log/viper_program`.
 
 ## `ENABLE_CACHE`
 
@@ -265,6 +266,9 @@ When enabled, communication with the server will be encoded as JSON instead of t
 
 Log level and filters. See [`env_logger` documentation](https://docs.rs/env_logger/0.7.1/env_logger/index.html#enabling-logging).
 
+For example, `PRUSTI_LOG=prusti_viper=trace` enables trace logging for the prusti-viper crate.
+Debug and trace logs are not available in release builds.
+
 ## `LOG_DIR`
 
 Path to directory in which log files and dumped output will be stored.

diff --git a/docs/dev-guide/src/development/debug.md b/docs/dev-guide/src/development/debug.md
@@ -14,7 +14,7 @@ See the list of [flags](../config/flags.md) for way to configure Prusti. Of part
 
 ## Debugging tests
 
-A proposed way of fixing Prusti limitations is to add a regression test and then use the following command to get Prusti output:
+A proposed way of fixing Prusti limitations is to add a regression test by creating a new file in `prusti-tests/tests` and then use the following command to get Prusti output:
 
 ```bash
 ./x.py build --all && \
@@ -34,6 +34,15 @@ Tip: to see the expanded Prusti specification macros, add the following comment
 // compile-flags: -Zunpretty=expanded
 ```
 
+### Running Prusti in a debugger
+
+The `verify-test` command also generates a VS Code launch config, which allows you to run Prusti in a debugger.
+
+- In the `Cargo.toml`, section `[profile.dev]`, set `debug = 2`. This enables debug symbols.
+- Install the CodeLLDB VS Code extension.
+
+Now you can set breakpoints and launch the debugger.
+
 ### Debugging performance problems
 
 In case you are debugging a performance problem and suspect that it is caused by quantifiers, append `--analyze-quantifiers` to the command after the `<path-to-the-test-file>`. This will run Z3 in tracing mode and produce CSV files with various statistics in `log/smt` directory. In case you want to see all terms that were used to trigger a specific quantifier, you can produce the list of them with the following command:
@@ -44,4 +53,3 @@ PRUSTI_SMT_TRACE_QUANTIFIER_TRIGGERS=<quantifier-id> \
 ```
 
 You can find the list of quantifier ids and names in `log/smt/<function>/trace1.log.unique-triggers.csv`. Running the `smt-log-analyzer` will generate `log/smt/<function>/trace1.log.quantifier-<quantifier-id>-triggers.csv` file containing all triggers used to instantiate the quantifier.
-
diff --git a/docs/static/logo.png b/docs/static/logo.png
diff --git a/scripts/verify_test.py b/scripts/verify_test.py
@@ -48,6 +48,7 @@ def generate_launch_json(args_file, env_file):
                 "--bin=prusti-driver",
                 "--package=prusti"
             ],
+            "env": get_env(),
             "filter": {
                 "name": "prusti-driver",
                 "kind": "bin"