Tock: Using Miri to help checking unsafe code?

[gendx]

I've recently seen a talk about unsafe code, in which the speaker recommends using Miri as a tool to help finding bugs in unsafe code: https://youtu.be/QAz-maaH0KM?t=1426. Given the amount of unsafe code in Tock, this could be a helpful tool to find and fix potential bugs.

I haven't tried it, and I'm not sure in which scope it could be used (given the specifics of embedded systems), but it could be relevant for the Tock-cells library for example (which are architecture agnostic, and don't depend on memory mapped registers).

For now it's just an idea, but it seems that it could be deployed a check in CI for example.

[labbott]

It looks like Miri doesn't work well with embedded code, I tried running this in both the opentitan and hifive directories:

$ RUST_BACKTRACE=1 cargo miri test
...
thread 'rustc' panicked at 'no main function found!', src/tools/miri/src/bin/miri.rs:42:37
stack backtrace:
   0: backtrace::backtrace::libunwind::trace
             at /cargo/registry/src/github.com-1ecc6299db9ec823/backtrace-0.3.44/src/backtrace/libunwind.rs:86
   1: backtrace::backtrace::trace_unsynchronized
             at /cargo/registry/src/github.com-1ecc6299db9ec823/backtrace-0.3.44/src/backtrace/mod.rs:66
   2: std::sys_common::backtrace::_print_fmt
             at src/libstd/sys_common/backtrace.rs:78
   3: <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt
             at src/libstd/sys_common/backtrace.rs:59
   4: core::fmt::write
             at src/libcore/fmt/mod.rs:1053
   5: std::io::Write::write_fmt
             at src/libstd/io/mod.rs:1428
   6: std::sys_common::backtrace::_print
             at src/libstd/sys_common/backtrace.rs:62
   7: std::sys_common::backtrace::print
             at src/libstd/sys_common/backtrace.rs:49
   8: std::panicking::default_hook::{{closure}}
             at src/libstd/panicking.rs:204
   9: std::panicking::default_hook
             at src/libstd/panicking.rs:224
  10: rustc_driver::report_ice
  11: std::panicking::rust_panic_with_hook
             at src/libstd/panicking.rs:474
  12: rust_begin_unwind
             at src/libstd/panicking.rs:378
  13: core::panicking::panic_fmt
             at src/libcore/panicking.rs:85
  14: core::option::expect_failed
             at src/libcore/option.rs:1203
  15: rustc::ty::context::tls::enter_global
  16: <miri::MiriCompilerCalls as rustc_driver::Callbacks>::after_analysis
  17: rustc_interface::interface::run_compiler_in_existing_thread_pool
  18: rustc_ast::attr::with_globals

Given everything is compiled with #![no_main], I'm guessing something isn't annotated properly but I could also be invoking it incorrectly

[ppannuto]

Trying this in cells, the first thing that happened for me was:

$ cargo miri test
I will run `"/Users/ppannuto/.rustup/toolchains/nightly-2020-03-06-x86_64-apple-darwin/bin/cargo" "install" "xargo" "-f"` to install a recent enough xargo. Proceed? [Y/n]

Which shows some x-platform understanding

---

Follow-up, it seems to run successfully for library crates (where it would expect no main function):

[-bash] Wed 08 Apr 12:32 [[master $] ~/code/helena-project/tock/kernel]
$ cargo miri test
    Checking tock-registers v0.5.0 (/Volumes/code/helena-project/tock/libraries/tock-register-interface)
    Checking tock-cells v0.1.0 (/Volumes/code/helena-project/tock/libraries/tock-cells)
    Checking kernel v0.1.0 (/Volumes/code/helena-project/tock/kernel)

running 5 tests
test common::ring_buffer::test::test_enqueue_dequeue ... ok
test common::ring_buffer::test::test_fill_once ... ok
test common::ring_buffer::test::test_push ... ok
test common::ring_buffer::test::test_refill ... ok
test common::ring_buffer::test::test_retain ... ok

test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out

    Finished test [optimized + debuginfo] target(s) in 3.06s

Tried capsules too:

$ cargo miri test
    Checking enum_primitive v0.1.0 (/Volumes/code/helena-project/tock/libraries/enum_primitive)
    Checking kernel v0.1.0 (/Volumes/code/helena-project/tock/kernel)
    Checking capsules v0.1.0 (/Volumes/code/helena-project/tock/capsules)

running 5 tests
test alarm::test::alarm_after_systick_wrap_expired ... ok
test alarm::test::alarm_after_systick_wrap_time_after_systick_wrap_not_expired ... ok
test alarm::test::alarm_after_systick_wrap_time_before_systick_wrap_not_expired ... ok
test alarm::test::alarm_before_systick_wrap_expired ... ok
test alarm::test::alarm_before_systick_wrap_not_expired ... ok

test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out

    Finished test [optimized + debuginfo] target(s) in 7.39s

---

We unfortunately don't (yet) have many tests for this to exploit, but I don't see any harm in adding this step to CI for all the non-board crates