Problems in tag analysis for vector operations

[ya0guang]

Issue

1. Adding tag to a vector doesn't propagate the tag to the elements in this vector.
2. 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)