From 6a46f2a344c0b55e458816883239cebae6fd021f Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Fri, 1 Apr 2022 18:13:31 -0400
Subject: [PATCH] Documentation: Workarounds (new section) (#1005)

* Documentation: Workarounds (new section)

* Update docs/src/workarounds.md

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
---
 docs/src/SUMMARY.md           |  1 +
 docs/src/dev-documentation.md |  7 ++--
 docs/src/workarounds.md       | 66 +++++++++++++++++++++++++++++++++++
 3 files changed, 71 insertions(+), 3 deletions(-)
 create mode 100644 docs/src/workarounds.md

diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md
index 0a0c72d3d7ac..12f459b5d35d 100644
--- a/docs/src/SUMMARY.md
+++ b/docs/src/SUMMARY.md
@@ -15,6 +15,7 @@
   - [Where to start on real code](./tutorial-real-code.md)
 
 - [Developer documentation](dev-documentation.md)
+  - [Workarounds](./workarounds.md)
   - [Command cheat sheets](./cheat-sheets.md)
   - [Working with `rustc`](./rustc-hacks.md)
   - [Testing](./testing.md)
diff --git a/docs/src/dev-documentation.md b/docs/src/dev-documentation.md
index bd036246cb22..611645e8e4a1 100644
--- a/docs/src/dev-documentation.md
+++ b/docs/src/dev-documentation.md
@@ -9,9 +9,10 @@ we recommend looking into [these issues](https://github.com/model-checking/kani/
 
 In this chapter, we provide documentation that might be helpful for Kani
 developers (including external contributors):
- 1. [Useful command-line instructions for Kani/CBMC/Git](./cheat-sheets.md).
- 2. [Development setup recommendations for working with `rustc`](./rustc-hacks.md).
- 3. [Guide for testing in Kani](./testing.md).
+ 1. [Suggested workarounds](./workarounds.md).
+ 2. [Useful command-line instructions for Kani/CBMC/Git](./cheat-sheets.md).
+ 3. [Development setup recommendations for working with `rustc`](./rustc-hacks.md).
+ 4. [Guide for testing in Kani](./testing.md).
 
 > **NOTE:** The developer documentation is intended for Kani developers and not
 users. At present, the project is under heavy development and some items
diff --git a/docs/src/workarounds.md b/docs/src/workarounds.md
new file mode 100644
index 000000000000..546af0df30ca
--- /dev/null
+++ b/docs/src/workarounds.md
@@ -0,0 +1,66 @@
+# Workarounds
+
+This section describes a few workarounds that may help overcome tooling
+issues in the Kani project.
+
+## CBMC arguments
+
+Kani is able to handle common CBMC arguments as if they were its own (e.g.,
+`--unwind <n>`), but sometimes it may be necessary to use CBMC arguments which
+are not handled by Kani.
+
+To pass additional arguments for CBMC, you pass `--cbmc-args` to Kani. Note that
+this "switches modes" from Kani arguments to CBMC arguments: Any arguments that
+appear after `--cbmc-args` are considered to be CBMC arguments, so all Kani
+arguments must be placed before it.
+
+Thus, the command line format to invoke `cargo kani` with CBMC arguments is:
+
+```bash
+cargo kani [<kani-args>]* --cbmc-args [<cbmc-args>]*
+```
+
+> **NOTE**: In cases where CBMC is not expected to emit a verification output,
+> you have to use Kani's argument `--output-format old` to turn off the
+> post-processing of output from CBMC.
+
+### Individual loop bounds
+
+Setting `--unwind <n>` affects every loop in a harness.
+Once you know a particular loop is causing trouble, sometimes it can be helpful to provide a specific bound for it.
+
+In the general case, specifying just the highest bound globally for all loops
+shouldn't cause any problems, except that the solver may take more time because
+_all_ loops will be unwound to the specified bound.
+
+In situations where you need to optimize for the solver, individual bounds for
+each loop can be provided on the command line. To do so, we first need to know
+the labels assigned to each loop with the CBMC argument `--show-loops`:
+
+```
+# kani src/lib.rs --output-format old --cbmc-args --show-loops
+[...]
+Loop _RNvCs6JP7pnlEvdt_3lib17initialize_prefix.0:
+  file ./src/lib.rs line 11 column 5 function initialize_prefix
+
+Loop _RNvMs8_NtNtCswN0xKFrR8r_4core3ops5rangeINtB5_14RangeInclusivejE8is_emptyCs6JP7pnlEvdt_3lib.0:
+  file $RUST/library/core/src/ops/range.rs line 540 column 9 function std::ops::RangeInclusive::<Idx>::is_empty
+
+Loop gen-repeat<[u8; 10]::16806744624734428132>.0:
+```
+
+This command shows us the labels of the loops involved. Note that, as mentioned
+in [CBMC arguments](#cbmc-arguments), we need to use `--output-format old` to
+avoid post-processing the output from CBMC.
+
+> **NOTE**: At the moment, these labels are constructed using the mangled name
+> of the function and an index. Mangled names are likely to change across
+> different versions, so this method is highly unstable.
+
+Then, we can use the CBMC argument `--unwindset
+label_1:bound_1,label_2:bound_2,...` to specify an individual bound for each
+loop as follows:
+
+```bash
+kani src/lib.rs --cbmc-args --unwindset _RNvCs6JP7pnlEvdt_3lib17initialize_prefix.0:12
+```