MIRAI only sees one member of a workspace

TomMD commented 1 year ago

Issue

MIRAI is overly quiet, hiding errors due to non-clean and workspace confusion.

Steps to Reproduce

~/hardware-security-common/MIRAI/examples/tag_analysis$ cat Cargo.toml
[workspace]
members = [ "timing_channels", "trait_methods", "verification_status" ]

resolver = "2"

[workspace.dependencies]
mirai-annotations = { path = "../../annotations" }

And optionally:

$ git diff
diff --git a/examples/tag_analysis/timing_channels/Cargo.toml b/examples/tag_analysis/timing_channels/Cargo.toml
index 0fd536f..a9ce058 100644
--- a/examples/tag_analysis/timing_channels/Cargo.toml
+++ b/examples/tag_analysis/timing_channels/Cargo.toml
@@ -11,4 +11,4 @@ test = false # we have no unit tests
 doctest = false # and no doc tests

 [dependencies]
-mirai-annotations = { path = "../../../annotations" }
+mirai-annotations = { workspace = true }

Then run:

$ cargo clean && cargo mirai
...
   Compiling proc-macro2 v1.0.66
   Compiling unicode-ident v1.0.11
   Compiling syn v1.0.109
    Checking mirai-annotations v1.12.1 (/home/admin/hardware-security-common/MIRAI/annotations)
    Checking timing_channels v0.1.0 (/home/admin/hardware-security-common/MIRAI/examples/tag_analysis/timing_channels)
    Checking verification_status v0.1.0 (/home/admin/hardware-security-common/MIRAI/examples/tag_analysis/verification_status)
   Compiling quote v1.0.32
   Compiling contracts v0.6.3
    Checking trait_methods v0.1.0 (/home/admin/hardware-security-common/MIRAI/examples/tag_analysis/trait_methods)
    Finished dev [unoptimized + debuginfo] target(s) in 4.06s
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s

Disappointing. Lets add const time flags.

$ cargo clean ; MIRAI_FLAGS="--constant_time=SecretTaintKind" cargo mirai
   Compiling proc-macro2 v1.0.66
   Compiling unicode-ident v1.0.11
   Compiling syn v1.0.109
    Checking mirai-annotations v1.12.1 (/home/admin/hardware-security-common/MIRAI/annotations)
    Checking verification_status v0.1.0 (/home/admin/hardware-security-common/MIRAI/examples/tag_analysis/verification_status)
    Checking timing_channels v0.1.0 (/home/admin/hardware-security-common/MIRAI/examples/tag_analysis/timing_channels)
warning: the branch condition may have a SecretTaintKind tag
  --> timing_channels/src/lib.rs:45:16
   |
45 |             if secret[i] != public[i] {
   |                ^^^^^^^^^^^^^^^^^^^^^^

warning: `timing_channels` (lib) generated 1 warning

Better, but what about the non-timing_channels packages?

Expected Behavior

All packages report result and the report is identical regardless of starting from cargo clean or otherwise.

Actual Results

As shown above, we only see results from one arbitrary member of the workspace. Also the results are finick and might or might not appear unless we have cleaned prior to the run.

Environment

x86_64 Ubuntu with mirai 1.1.8 as reported by --version. Installed today. Also:

$ rustc --version
rustc 1.73.0-nightly (500647fd8 2023-07-27)

hermanventer commented 1 year ago

By design, cargo mirai behaves as much as possible as cargo check does. If you have not yet run cargo mirai on a workspace, it should be rebuilding all members of the workspace because it needs to run rustc with different compiler flags than is the case with cargo check.

Something that may be tripping you up is that you only see diagnostics for issues that are reachable from an entry point. Only public, non generic functions can be entry points. Even then, by default, you only see issues that are very likely to be real issues. See the discussion here: https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Overview.md

It seems that a much more extensive tutorial would be useful. Perhaps we can collaborate on producing one. I have significant time constraints, so it would be very helpful if you take the lead on it, if this interests you.

hermanventer commented 1 year ago

Also, perhaps start out with MIRAI_FLAGS="--diag=paranoid" and then downgrade from there as you become more comfortable with how to run MIRAI and more annoyed with all the false positives.

TomMD commented 1 year ago

Herman, thanks for taking the time to respond. Your reminder about reachability is great but I do still think there is a bug. Consider the earlier modification to examples/tag_analysis, making it a workspace with members of "timing_channels", "trait_methods", "verification_status". We can run cargo mirai and get no results. We can even make modifications to the main routine of trait_methods such as:

--- a/examples/tag_analysis/trait_methods/src/lib.rs
+++ b/examples/tag_analysis/trait_methods/src/lib.rs
@@ -46,6 +46,7 @@ impl ProcessWithoutTaint for Block {

 pub fn main() {
     let mut block = Block { content: 99991 };
+    add_tag!(&block, SecretTaint);
     verify!(does_not_have_tag!(&block, SecretTaint));

If we cd examples/tag_analysis/trait_methods ; cargo mirai then we do see the error on line 50 of a " provably false verification condition". So far so good.

If we cd examples/tag_anslysis ; cargo clean with our workspace in place and cargo mirai then there are absolutely no errors. Did I misunderstand? Should this issue errors for all reachable code for all packages in the workspace?

hermanventer commented 1 year ago

I think the problem might be due to a heuristic that causes MIRAI to suppress any error message that does not originate in the root crate of a compilation. Perhaps when you run it over a workspace such as examples/tag_analysis, it treats the workspace as the root and suppresses the errors that come from the members of the workspace. I don't have time to chase this down and fix it. If you set the directory to a particular example, you will see output.

facebookexperimental / MIRAI