Merge #281
281: Run Miri with more flag combinations, and add a Miri Tips doc. r=alistair23 a=jrvanwhy
[Rendered doc](https://github.com/jrvanwhy/libtock-rs/blob/miri-flags/doc/MiriTips.md)
This runs code under Miri with the `-Zmiri-symbolic-alignment-check` flag, as well as both with and without `-Zmiri-track-raw-pointers`. This identifies a lot of "gray area" behavior -- that may or may not become specified as undefined behavior in the future -- as undefined behavior.
I also added a tip on how to write tests that identify undefined behavior that Miri doesn't catch by default, such as having uninitialized values in local variables. The documentation tip will be used in the `libtock_unittest` crate as well as per-crate unit tests.
Co-authored-by: Johnathan Van Why <jrvanwhy@google.com>
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.
