libtock-rs
runs most of its unit tests under 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 has configuration flags, 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 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.
Miri does not always detect undefined behavior when an invalid value is created but not used. Here are some cases that Miri currently accepts:
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:
format!("{:?}", value);
If value
is invalid, then Miri will identify undefined behavior in the above code.