Problems in tag analysis for vector operations
ya0guang opened this issue · 0 comments
Issue
- Adding tag to a vector doesn't propagate the tag to the elements in this vector.
- Unexpected tag analysis result when using
into_iter()
to iterate a vector of struct.
Steps to Reproduce
For problem 1, I found this test which exactly meets my verification conditions. MIRAI should not complain about this but it actually complains.
However, this line is commented and I don't know why. I'd be more than grateful if you can provide more details.
For the second problem, I create a vector of struct I
and tag each element. When iterating the vector using into_iter
, MIRAI can detect that elements have tags (provably false verification condition
in the following snippet). However, when the lines are uncommented, MIRAI doesn't complain anymore, and I think this is problematic.
#![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)]
pub struct SecretTaintKind<const MASK: TagPropagationSet> {}
#[cfg(mirai)]
const SECRET_TAINT: TagPropagationSet = TAG_PROPAGATION_ALL;
#[cfg(mirai)]
pub type SecretTaint = SecretTaintKind<SECRET_TAINT>;
use std::vec::Vec;
struct I(u32);
fn main() {
let va = vec![I(1), I(2), I(3)];
for i in va.iter() {
add_tag!(i, SecretTaint);
}
let mut vb: Vec<I> = Vec::new();
// let mut vb: Vec<i32> = Vec::new();
for i in va.into_iter() {
verify!(does_not_have_tag!(&i, SecretTaint));
// vb.push(i);
}
}
Expected Behavior
When the commented lines are uncommented, MIRAI should complain at verify!(does_not_have_tag!(&i, SecretTaint));
.
Actual Results
When the commented lines are uncommented, MIRAI doesn't complain.
Environment
rustc 1.61.0-nightly (c84f39e6c 2022-03-20)