You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Aug 22, 2024. It is now read-only.
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))]externcrate mirai_annotations;use mirai_annotations::*;#[cfg(mirai)]use mirai_annotations::TagPropagationSet;#[cfg(mirai)]structSecretTaintKind<constMASK:TagPropagationSet>{}#[cfg(mirai)]constSECRET_TAINT:TagPropagationSet = TAG_PROPAGATION_ALL;#[cfg(mirai)]typeSecretTaint = SecretTaintKind<SECRET_TAINT>;#[cfg(not(mirai))]typeSecretTaint = ();structA(u32);structB(u32);structC(u32);fna_to_b(a:A) -> B{precondition!(has_tag!(&a, SecretTaint));let b = B(a.0 + 1);
b
}fnb_to_c(b:B) -> C{precondition!(has_tag!(&b, SecretTaint));let c = C(b.0 + 1);
c
}fnmain(){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.
The text was updated successfully, but these errors were encountered:
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
Expected Behavior
Satisfied verification
Actual Results
MIRAI complains:
Environment
rustc 1.61.0-nightly (c84f39e6c 2022-03-20)
I'm using the latest MIRAI with the same rust toolchain version.
The text was updated successfully, but these errors were encountered: