MIRAI does not complain about missing tag in some cases
andrew-lee-work opened this issue · 3 comments
Issue
With "--paranoid", MIRAI does not complain about a missing tag when it is in fact missing.
Steps to Reproduce
Call cargo check to check the functions check_tag
and check_tag_2
, in the code below, using RUSTC_WRAPPER='mirai'
and MIRAI_FLAGS='--diag=paranoid --single_func={function_to_check}
.
use contracts::*;
use mirai_annotations::*;
#[cfg(mirai)]
use mirai_annotations::{TagPropagation, TagPropagationSet};
#[cfg(mirai)]
pub struct TaintedKind<const MASK: TagPropagationSet> {}
#[cfg(mirai)]
pub const TAINTED_MASK: TagPropagationSet = tag_propagation_set!(TagPropagation::SubComponent);
#[cfg(mirai)]
pub type Tainted = TaintedKind<TAINTED_MASK>;
#[cfg(not(mirai))]
pub type Tainted = ();
#[cfg(mirai)]
pub struct SanitizedKind<const MASK: TagPropagationSet> {}
#[cfg(mirai)]
pub const SANITIZED_MASK: TagPropagationSet = tag_propagation_set!(TagPropagation::SubComponent);
#[cfg(mirai)]
pub type Sanitized = SanitizedKind<SANITIZED_MASK>;
#[cfg(not(mirai))]
pub type Sanitized = ();
#[cfg(mirai)]
pub type Authorized = SanitizedKind<SANITIZED_MASK>;
#[cfg(not(mirai))]
pub type Authorized = ();
pub struct AuthorizedWrapper<T>(pub T);
fn try_authorize<'a>(id: &'a u64) -> Option<AuthorizedWrapper<&'a u64>> {
if id % 10 < 5 {
return None
} else {
let authorized = AuthorizedWrapper(id);
let result = Some(authorized);
add_tag!(&result, Authorized);
result
}
}
fn is_authorized(id: &u64) -> bool {
5 <= id % 10
}
pub fn check_tag() {
let id = 6;
if let Some(aa) = try_authorize(&id) {
sanity_check(&aa)
};
}
pub fn check_tag_2() {
let id = 6;
if is_authorized(&id) {
//add_tag!(&id, Authorized);
sanity_check_2(&id)
};
}
#[requires(has_tag!(id, Authorized))]
fn sanity_check(id: &AuthorizedWrapper<&u64>) {
precondition!(has_tag!(id, Authorized));
verify!(has_tag!(id, Authorized));
}
#[requires(has_tag!(id, Authorized))]
fn sanity_check_2(id: &u64) {
precondition!(has_tag!(id, Authorized));
verify!(has_tag!(id, Authorized));
}
Expected Behavior
There should be a warning or error message at sanity_check_2
about the missing tag.
In contrast, note that check_tag()
behaves as expected when I remove the add_tag
line in try_authorize
. Also note that in sanity_check
, if the add_tag!
in try_authorize
is removed, all three annotations individually will raise a warning if the others are commented out.
Actual Results
No errors or warnings about missing tags are produced.
Environment
Rust version (rustc --version)
rustc 1.52.0-nightly (e37a13cc3 2021-02-28)
mirai --version
MIRAI v1.0.5rustc 1.52.0-nightly (e37a13cc3 2021-02-28)
In sanity_check_2, the precondition puts the onus on the caller to add the tag to id. Thus, given the precondition, the verify! has to succeed. Try removing the precondtion.
Also note that #[requires ..] is an alternative syntax for precondition!, so you would have either the one or the other, but not both.
I reduced the test case to the following:
use mirai_annotations::*;
pub struct SanitizedKind<const MASK: TagPropagationSet> {}
pub const SANITIZED_MASK: TagPropagationSet = tag_propagation_set!(TagPropagation::SubComponent);
pub type Authorized = SanitizedKind<SANITIZED_MASK>;
fn is_authorized(id: &u64) -> bool {
5 <= id % 10
}
pub fn check_tag_2() {
let id = 6;
if is_authorized(&id) {
// add_tag!(&id, Authorized);
sanity_check_2(&id)
};
}
fn sanity_check_2(id: &u64) {
precondition!(has_tag!(id, Authorized));
verify!(has_tag!(id, Authorized));
}
pub fn main() {}
and got this output:
warning: possible unsatisfied precondition
--> tests/run-pass/tag_repro.rs:16:9
|
16 | sanity_check_2(&id)
| ^^^^^^^^^^^^^^^^^^^
|
note: related location
--> tests/run-pass/tag_repro.rs:21:5
|
21 | precondition!(has_tag!(id, Authorized));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= note: this warning originates in a macro (in Nightly builds, run with -Z macro-backtrace for more info)
warning: 1 warning emitted
Uncommenting the add_tag! causes the diagnostic to go away.
I believe this is correct behavior.
@hermanventer I got a different result than you and I figured out that it is because I was using --single_func
. The target of --single_func
was omitted in my original post because I thought it wouldn't matter. I've reproduced the issue below with your simplified test.
use mirai_annotations::*;
pub struct SanitizedKind<const MASK: TagPropagationSet> {}
pub const SANITIZED_MASK: TagPropagationSet = tag_propagation_set!(TagPropagation::SubComponent);
pub type Authorized = SanitizedKind<SANITIZED_MASK>;
fn is_authorized(id: &u64) -> bool {
5 <= id % 10
}
pub fn check_tag_2() {
let id = 6;
if is_authorized(&id) {
// add_tag!(&id, Authorized);
sanity_check_2(&id)
};
}
fn sanity_check_2(id: &u64) {
precondition!(has_tag!(id, Authorized));
verify!(has_tag!(id, Authorized));
}
pub fn main() {}
fn single_func_to_check() {
check_tag_2()
}
If I use export MIRAI_FLAGS="--diag=paranoid --single_func=single_func_to_check"
, I don't get warning: possible unsatisfied precondition
. However, if I either drop the --single_func
or I use --single_func=check_tag_2
then I get the same result as you.
Also note that if I add a line verify!(false);
, then --single_func=single_func_to_check
will catch that.