Run Miri twice, with two different flag sets, and add documentation on using Miri to identify as much undefined behavior as possible.
diff --git a/Makefile b/Makefile
index a37e40c..b8d1f70 100644
--- a/Makefile
+++ b/Makefile
@@ -84,12 +84,19 @@
# Important: This tests a platform without atomic instructions.
PLATFORM=opentitan cargo build --release --target=riscv32imc-unknown-none-elf --examples -p libtock -p libtock_core
+# Arguments to pass to cargo to exclude libtock_runtime and crates that depend
+# on libtock_runtime. Used when we need to build a crate for the host OS, as
+# libtock_runtime only suppors running on Tock.
+EXCLUDE_RUNTIME := --exclude libtock_runtime
+
.PHONY: test
test: examples test-qemu-hifive
LIBTOCK_PLATFORM=nrf52 PLATFORM=nrf52 cargo fmt --all -- --check
PLATFORM=nrf52 cargo clippy --all-targets --exclude libtock_runtime --workspace
LIBTOCK_PLATFORM=hifive1 cargo clippy --target=riscv32imac-unknown-none-elf -p libtock_runtime
- PLATFORM=nrf52 cargo miri test --exclude libtock_runtime --workspace
+ PLATFORM=nrf52 cargo miri test $(EXCLUDE_RUNTIME) --workspace
+ MIRIFLAGS="-Zmiri-symbolic-alignment-check -Zmiri-track-raw-pointers" \
+ PLATFORM=nrf52 cargo miri test $(EXCLUDE_RUNTIME) --workspace
echo '[ SUCCESS ] libtock-rs tests pass'
.PHONY: analyse-stack-sizes
diff --git a/doc/MiriTips.md b/doc/MiriTips.md
new file mode 100644
index 0000000..5c88964
--- /dev/null
+++ b/doc/MiriTips.md
@@ -0,0 +1,42 @@
+Miri Tips
+=========
+
+`libtock-rs` runs most of its unit tests under
+[Miri](https://github.com/rust-lang/miri) to detect undefined behavior. However,
+Miri does not detect all undefined behavior encountered. This document lists
+techniques for maximizing the amount of undefined behavior identified by Miri.
+
+## Miri flags
+
+Miri has [configuration
+flags](https://github.com/rust-lang/miri#miri--z-flags-and-environment-variables),
+which can be set using the `MIRIFLAGS` environment variable. We run the tests
+both with and without `-Zmiri-track-raw-pointers`, as both versions of Stacked
+Borrows has undefined behavior the other does not (see [this
+discussion](https://github.com/rust-lang/miri/pull/1748) for more information).
+On the run with `-Zmiri-track-raw-pointers`, we also set
+`-Zmiri-symbolic-alignment-check` to make Miri's alignment check more pendantic.
+
+## Detecting invalid values
+
+Miri does not always detect undefined behavior when an invalid value is created
+but not used. Here are some cases that Miri currently accepts:
+
+1. Unused reference to an invalid value
+ (https://github.com/rust-lang/miri/issues/1638)
+1. Unused uninitialized value (https://github.com/rust-lang/miri/issues/1340)
+1. Slices pointing to invalid values
+ (https://github.com/rust-lang/miri/issues/1240)
+
+Note that copying the value around (including passing it to functions) does
+*not* count as a use for the purpose of this check.
+
+For types that implement `core::fmt::Debug` (i.e. most types), you can check a
+value is valid by attempting to debug-print it:
+
+```rust
+format!("{:?}", value);
+```
+
+If `value` is invalid, then Miri will identify undefined behavior in the above
+code.
