Verify tag propagation for multiple type changes

[ya0guang]

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.