Skip to content
This repository has been archived by the owner on Aug 22, 2024. It is now read-only.

Verify tag propagation for multiple type changes #1147

Open
ya0guang opened this issue Mar 31, 2022 · 0 comments
Open

Verify tag propagation for multiple type changes #1147

ya0guang opened this issue Mar 31, 2022 · 0 comments

Comments

@ya0guang
Copy link
Contributor

Issue

MIRAI cannot produce correct result in tag propagation when types are changing multiple times. In my previous issue #1131 , the problem is solved when there is one type change. However, when there are more than one type changes, MIRAI doesn't work.

Steps to Reproduce

#![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]
extern crate mirai_annotations;
use mirai_annotations::*;

#[cfg(mirai)]
use mirai_annotations::TagPropagationSet;
#[cfg(mirai)]
struct SecretTaintKind<const MASK: TagPropagationSet> {}
#[cfg(mirai)]
const SECRET_TAINT: TagPropagationSet = TAG_PROPAGATION_ALL;
#[cfg(mirai)]
type SecretTaint = SecretTaintKind<SECRET_TAINT>;
#[cfg(not(mirai))]
type SecretTaint = ();

struct A(u32);
struct B(u32);
struct C(u32);

fn a_to_b(a: A) -> B {
    precondition!(has_tag!(&a, SecretTaint));
    let b = B(a.0 + 1);
    b
}

fn b_to_c(b: B) -> C {
    precondition!(has_tag!(&b, SecretTaint));
    let c = C(b.0 + 1);
    c
}

fn main() {
    let a = A(1);
    add_tag!(&a, SecretTaint);
    let b = a_to_b(a);
    verify!(has_tag!(&b, SecretTaint));
    let c = b_to_c(b);
    verify!(has_tag!(&c, SecretTaint));
    println!("reachable?");
}

Expected Behavior

Satisfied verification

Actual Results

MIRAI complains:

$ cargo mirai
    Checking mirai_test v0.1.0 (/Users/v_chenhongbo04/Code/mirai_test)
warning: unsatisfied precondition
  --> src/main.rs:43:13
   |
43 |     let c = b_to_c(b);
   |             ^^^^^^^^^
   |
note: related location
  --> src/main.rs:33:5
   |
33 |     precondition!(has_tag!(&b, SecretTaint));
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   = note: this warning originates in the macro `precondition` (in Nightly builds, run with -Z macro-backtrace for more info)

warning: this is unreachable, mark it as such by using the verify_unreachable! macro
  --> src/main.rs:44:5
   |
44 |     verify!(has_tag!(&c, SecretTaint));
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: `mirai_test` (bin "mirai_test") generated 2 warnings
    Finished dev [unoptimized + debuginfo] target(s) in 0.72s

Environment

rustc 1.61.0-nightly (c84f39e6c 2022-03-20)

I'm using the latest MIRAI with the same rust toolchain version.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant